package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Library
Module
Module type
Parameter
Class
Class type
type register_name = string
type address = Sail2_values.bitU list
type ('regval, 'a, 'e) monad =
  1. | Done of 'a
  2. | Read_mem of Sail2_instr_kinds.read_kind * int * int * Sail2_values.memory_byte list -> ('regval, 'a, 'e) monad
  3. | Read_memt of Sail2_instr_kinds.read_kind * int * int * (Sail2_values.memory_byte list * Sail2_values.bitU) -> ('regval, 'a, 'e) monad
  4. | Write_ea of Sail2_instr_kinds.write_kind * int * int * ('regval, 'a, 'e) monad
  5. | Excl_res of bool -> ('regval, 'a, 'e) monad
  6. | Write_mem of Sail2_instr_kinds.write_kind * int * int * Sail2_values.memory_byte list * bool -> ('regval, 'a, 'e) monad
  7. | Write_memt of Sail2_instr_kinds.write_kind * int * int * Sail2_values.memory_byte list * Sail2_values.bitU * bool -> ('regval, 'a, 'e) monad
  8. | Footprint of ('regval, 'a, 'e) monad
  9. | Barrier of Sail2_instr_kinds.barrier_kind * ('regval, 'a, 'e) monad
  10. | Read_reg of register_name * 'regval -> ('regval, 'a, 'e) monad
  11. | Write_reg of register_name * 'regval * ('regval, 'a, 'e) monad
  12. | Choose of string * 'regval -> ('regval, 'a, 'e) monad
  13. | Print of string * ('regval, 'a, 'e) monad
  14. | Fail of string
  15. | Exception of 'e
type 'regval event =
  1. | E_read_mem of Sail2_instr_kinds.read_kind * int * int * Sail2_values.memory_byte list
  2. | E_read_memt of Sail2_instr_kinds.read_kind * int * int * Sail2_values.memory_byte list * Sail2_values.bitU
  3. | E_write_mem of Sail2_instr_kinds.write_kind * int * int * Sail2_values.memory_byte list * bool
  4. | E_write_memt of Sail2_instr_kinds.write_kind * int * int * Sail2_values.memory_byte list * Sail2_values.bitU * bool
  5. | E_write_ea of Sail2_instr_kinds.write_kind * int * int
  6. | E_excl_res of bool
  7. | E_barrier of Sail2_instr_kinds.barrier_kind
  8. | E_footprint
  9. | E_read_reg of register_name * 'regval
  10. | E_write_reg of register_name * 'regval
  11. | E_choose of string * 'regval
  12. | E_print of string
type 'regval trace = 'regval event list
val return : 'a -> ('rv, 'a, 'e) monad
val bind : ('rv, 'a, 'e) monad -> ('a -> ('rv, 'b, 'e) monad) -> ('rv, 'b, 'e) monad
val exit : unit -> ('rv, 'a, 'e) monad
val assert_exp : bool -> string -> ('rv, unit, 'e) monad
val throw : 'e -> ('rv, 'a, 'e) monad
val try_catch : ('rv, 'a, 'b) monad -> ('b -> ('rv, 'a, 'e2) monad) -> ('rv, 'a, 'e2) monad
type ('rv, 'a, 'r, 'e) monadR = ('rv, 'a, ('r, 'e) Either.either) monad
val early_return : 'r -> ('rv, 'a, ('r, 'e) Either.either) monad
val catch_early_return : ('rv, 'a, ('a, 'e) Either.either) monad -> ('rv, 'a, 'e) monad
val pure_early_return : ('a, 'a) Either.either -> 'a
val either_bind : ('e, 'a) Either.either -> ('a -> ('e, 'b) Either.either) -> ('e, 'b) Either.either
val liftR : ('rv, 'a, 'e) monad -> ('rv, 'a, ('r, 'e) Either.either) monad
val try_catchR : ('rv, 'a, ('r, 'b) Either.either) monad -> ('b -> ('rv, 'a, ('r, 'e2) Either.either) monad) -> ('rv, 'a, ('r, '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 -> ('rv, 'a, 'e) monad
val choose_convert_default : ('rv -> 'a option) -> 'a -> string -> ('rv, 'a, 'e) monad
val choose_bool : 'rv Sail2_values.register_Value_class -> string -> ('rv, bool, 'e) monad
val choose_bit : 'rv Sail2_values.register_Value_class -> string -> ('rv, Sail2_values.bitU, 'e) monad
val choose_int : 'rv Sail2_values.register_Value_class -> string -> ('rv, Nat_big_num.num, 'e) monad
val choose_real : 'rv Sail2_values.register_Value_class -> string -> ('rv, float, 'e) monad
val choose_string : 'rv Sail2_values.register_Value_class -> string -> ('rv, string, 'e) monad
val headM : 'a list -> ('rv, 'a, 'e) monad
val tailM : 'a list -> ('rv, 'a list, '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 -> 'a -> 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 -> 'a -> Nat_big_num.num -> 'b -> ('rv, bool, 'e) monad
val read_reg : ('b, 'rv, 'a) Sail2_values.register_ref -> ('rv, 'a, 'e) monad
val write_reg : ('a, 'rv, 'b) Sail2_values.register_ref -> 'b -> ('rv, 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 -> ('regval, 'a, 'e) monad -> 'regval event -> ('regval, 'a, 'e) monad option
val runTrace : 'regval Lem_pervasives_extra.eq_class -> 'regval event list -> ('regval, 'a, 'e) monad -> ('regval, 'a, 'e) 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct