libsail 0.15 · OCaml Package

type register_name = string

type address = Sail2_values.bitU list

type ('regval, 'a, 'e) monad =

| Done of 'a
| Read_mem of Sail2_instr_kinds.read_kind * int * int * Sail2_values.memory_byte list -> ('regval, 'a, 'e) monad
| Read_memt of Sail2_instr_kinds.read_kind * int * int * (Sail2_values.memory_byte list * Sail2_values.bitU) -> ('regval, 'a, 'e) monad
| Write_ea of Sail2_instr_kinds.write_kind * int * int * ('regval, 'a, 'e) monad
| Excl_res of bool -> ('regval, 'a, 'e) monad
| Write_mem of Sail2_instr_kinds.write_kind * int * int * Sail2_values.memory_byte list * bool -> ('regval, 'a, 'e) monad
| Write_memt of Sail2_instr_kinds.write_kind * int * int * Sail2_values.memory_byte list * Sail2_values.bitU * bool -> ('regval, 'a, 'e) monad
| Footprint of ('regval, 'a, 'e) monad
| Barrier of Sail2_instr_kinds.barrier_kind * ('regval, 'a, 'e) monad
| Read_reg of register_name * 'regval -> ('regval, 'a, 'e) monad
| Write_reg of register_name * 'regval * ('regval, 'a, 'e) monad
| Choose of string * 'regval -> ('regval, 'a, 'e) monad
| Print of string * ('regval, 'a, 'e) monad
| Fail of string
| Exception of 'e

type 'regval event =

| E_read_mem of Sail2_instr_kinds.read_kind * int * int * Sail2_values.memory_byte list
| E_read_memt of Sail2_instr_kinds.read_kind * int * int * Sail2_values.memory_byte list * Sail2_values.bitU
| E_write_mem of Sail2_instr_kinds.write_kind * int * int * Sail2_values.memory_byte list * bool
| E_write_memt of Sail2_instr_kinds.write_kind * int * int * Sail2_values.memory_byte list * Sail2_values.bitU * bool
| E_write_ea of Sail2_instr_kinds.write_kind * int * int
| E_excl_res of bool
| E_barrier of Sail2_instr_kinds.barrier_kind
| E_footprint
| E_read_reg of register_name * 'regval
| E_write_reg of register_name * 'regval
| E_choose of string * 'regval
| E_print of string

type 'regval trace = 'regval event list

val return : 'a -> ('rv, 'a0, 'e) monad

val bind : 
  ('rv, 'a, 'e) monad ->
  ('c -> ('rv0, 'b, 'e0) monad) ->
  ('rv1, 'b0, 'e1) monad

val exit : unit -> ('rv, 'a, 'e) monad

val assert_exp : bool -> string -> ('rv, unit, 'e) monad

val throw : 'e -> ('rv, 'a, 'e0) monad

val try_catch : 
  ('rv, 'a, 'b) monad ->
  ('c -> ('rv0, 'a0, 'e2) monad) ->
  ('rv1, 'a1, 'e20) monad

type ('rv, 'a, 'r, 'e) monadR = ('rv, 'a, ('r, 'e) Either.either) monad

val early_return : 'r -> ('rv, 'a, ('r0, 'e) Either.either) monad

val catch_early_return : 
  ('rv, 'a, ('a0, 'e) Either.either) monad ->
  ('rv0, 'a1, 'e0) monad

val pure_early_return : ('a, 'a) Either.either -> 'a

val either_bind : 
  ('e, 'a) Either.either ->
  ('c -> ('e0, 'b) Either.either) ->
  ('e0, 'b) Either.either

val liftR : ('rv, 'a, 'e) monad -> ('rv0, 'a0, ('r, 'e0) Either.either) monad

val try_catchR : 
  ('rv, 'a, ('r, 'b) Either.either) monad ->
  ('c -> ('rv, 'a, ('r0, 'e2) Either.either) monad) ->
  ('rv0, 'a0, ('r0, 'e2) Either.either) monad

val maybe_fail : string -> 'a option -> ('rv, 'a, 'e) monad

val choose_regval : string -> ('rv, 'rv, 'e) monad

val choose_convert : ('rv -> 'a option) -> string -> ('rv0, 'a0, 'e) monad

val choose_convert_default : 
  ('rv -> 'a option) ->
  'a0 ->
  string ->
  ('rv0, 'a1, 'e) monad

val choose_bool : 
  'rv Sail2_values.register_Value_class ->
  string ->
  ('rv0, bool, 'e) monad

val choose_bit : 
  'rv Sail2_values.register_Value_class ->
  string ->
  ('rv0, Sail2_values.bitU, 'e) monad

val choose_int : 
  'rv Sail2_values.register_Value_class ->
  string ->
  ('rv0, Nat_big_num.num, 'e) monad

val choose_real : 
  'rv Sail2_values.register_Value_class ->
  string ->
  ('rv0, float, 'e) monad

val choose_string : 
  'rv Sail2_values.register_Value_class ->
  string ->
  ('rv0, string, 'e) monad

val headM : 'a list -> ('rv, 'a, 'e) monad

val tailM : 'a list -> ('rv, 'a list, 'e) monad

val read_memt_bytes : 
  'a Sail2_values.bitvector_class ->
  'b ->
  Sail2_instr_kinds.read_kind ->
  'c ->
  Nat_big_num.num ->
  ('rv, Sail2_values.memory_byte list * Sail2_values.bitU, 'e) monad

val read_memt : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  Sail2_instr_kinds.read_kind ->
  'c ->
  Nat_big_num.num ->
  ('rv, 'b0 * Sail2_values.bitU, 'e) monad

val read_mem_bytes : 
  'a Sail2_values.bitvector_class ->
  'b ->
  Sail2_instr_kinds.read_kind ->
  'c ->
  Nat_big_num.num ->
  ('rv, Sail2_values.memory_byte list, 'e) monad

val read_mem : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  Sail2_instr_kinds.read_kind ->
  'c ->
  'd ->
  Nat_big_num.num ->
  ('rv, 'b0, 'e) monad

val excl_result : unit -> ('rv, bool, 'e) monad

val write_mem_ea : 
  'a Sail2_values.bitvector_class ->
  Sail2_instr_kinds.write_kind ->
  'b ->
  'c ->
  Nat_big_num.num ->
  ('rv, unit, 'e) monad

val write_mem : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  Sail2_instr_kinds.write_kind ->
  'c ->
  'd ->
  Nat_big_num.num ->
  'f ->
  ('rv, bool, 'e) monad

val write_memt : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  Sail2_instr_kinds.write_kind ->
  'c ->
  Nat_big_num.num ->
  'd ->
  Sail2_values.bitU ->
  ('rv, bool, 'e) monad

val read_reg : ('b, 'rv, 'a) Sail2_values.register_ref -> ('rv0, 'a0, 'e) monad

val write_reg : 
  ('a, 'rv, 'b) Sail2_values.register_ref ->
  'c ->
  ('rv0, unit, 'e) monad

val barrier : Sail2_instr_kinds.barrier_kind -> ('rv, unit, 'e) monad

val footprint : 'a -> ('rv, unit, 'e) monad

val emitEvent : 
  'regval Lem_pervasives_extra.eq_class ->
  ('regval0, 'a, 'e) monad ->
  'regval1 event ->
  ('regval2, 'a0, 'e0) monad option

val runTrace : 
  'regval Lem_pervasives_extra.eq_class ->
  'regval event list ->
  ('regval, 'a, 'e) monad ->
  ('regval0, 'a0, 'e0) monad option

val final : ('regval, 'a, 'e) monad -> bool

val hasTrace : 
  'a Lem_pervasives_extra.eq_class ->
  'a event list ->
  ('a, 'b, 'c) monad ->
  bool

val hasException : 
  'a Lem_pervasives_extra.eq_class ->
  'a event list ->
  ('a, 'b, 'c) monad ->
  bool

val hasFailure : 
  'a Lem_pervasives_extra.eq_class ->
  'a event list ->
  ('a, 'b, 'c) monad ->
  bool

type ('regval, 'regstate, 'a, 'e) base_monad = ('regval, 'a, 'e) monad

type ('regval, 'regstate, 'a, 'r, 'e) base_monadR =
  ('regval, 'a, 'r, 'e) monadR

package libsail