package sail

  1. Overview
  2. Docs
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
type ii = Nat_big_num.num
type nn = Nat_big_num.num
val nat_of_int : Nat_big_num.num -> int
val prerr : string -> unit
val print_int : string -> Nat_big_num.num -> unit
val prerr_int : string -> Nat_big_num.num -> unit
val take_list : Nat_big_num.num -> 'a list -> 'a list
val drop_list : Nat_big_num.num -> 'a list -> 'a list
val repeat : 'a list -> Nat_big_num.num -> 'a list
val duplicate_to_list : 'a -> Nat_big_num.num -> 'a list
val replace : 'a list -> Nat_big_num.num -> 'a -> 'a list
val upper : 'a -> 'a
val max_64u : Nat_big_num.num
val max_64 : Nat_big_num.num
val min_64 : Nat_big_num.num
val max_32u : Nat_big_num.num
val max_32 : Nat_big_num.num
val min_32 : Nat_big_num.num
val max_8 : Nat_big_num.num
val min_8 : Nat_big_num.num
val max_5 : Nat_big_num.num
val min_5 : Nat_big_num.num
val just_list : 'a option list -> 'a list option
val maybe_failwith : 'a option -> 'a
type bitU =
  1. | B0
  2. | B1
  3. | BU
val showBitU : bitU -> string
val bitU_char : bitU -> char
val instance_Show_Show_Sail2_values_bitU_dict : bitU Lem_pervasives_extra.show_class
val compare_bitU : bitU -> bitU -> int
val instance_Basic_classes_Ord_Sail2_values_bitU_dict : bitU Lem_pervasives_extra.ord_class
type !'a bitU_class = {
  1. to_bitU_method : 'a -> bitU;
  2. of_bitU_method : bitU -> 'a;
}
val instance_Sail2_values_BitU_Sail2_values_bitU_dict : bitU bitU_class
val bool_of_bitU : bitU -> bool option
val bitU_of_bool : bool -> bitU
val cast_bit_bool : bitU -> bool option
val not_bit : bitU -> bitU
val is_one : Nat_big_num.num -> bitU
val and_bit : bitU -> bitU -> bitU
val or_bit : bitU -> bitU -> bitU
val xor_bit : bitU -> bitU -> bitU
val bools_of_nat_aux : Nat_big_num.num -> Nat_big_num.num -> bool list -> bool list
val bools_of_nat : Nat_big_num.num -> Nat_big_num.num -> bool list
val nat_of_bools_aux : Nat_big_num.num -> bool list -> Nat_big_num.num
val nat_of_bools : bool list -> Nat_big_num.num
val unsigned_of_bools : bool list -> Nat_big_num.num
val signed_of_bools : bool list -> Nat_big_num.num
val int_of_bools : bool -> bool list -> Nat_big_num.num
val pad_list : 'a -> 'a list -> Nat_big_num.num -> 'a list
val ext_list : 'a -> Nat_big_num.num -> 'a list -> 'a list
val extz_bools : Nat_big_num.num -> bool list -> bool list
val exts_bools : Nat_big_num.num -> bool list -> bool list
val add_one_bool_ignore_overflow_aux : bool list -> bool list
val add_one_bool_ignore_overflow : bool list -> bool list
val bools_of_int : Nat_big_num.num -> Nat_big_num.num -> bool list
val has_undefined_bits : bitU list -> bool
val bits_of_nat : Nat_big_num.num -> Nat_big_num.num -> bitU list
val nat_of_bits : bitU list -> Nat_big_num.num option
val not_bits : bitU list -> bitU list
val binop_list : ('b -> 'c -> 'a) -> 'b list -> 'c list -> 'a list
val unsigned_of_bits : bitU list -> Nat_big_num.num option
val signed_of_bits : bitU list -> Nat_big_num.num option
val int_of_bits : bool -> bitU list -> Nat_big_num.num option
val extz_bits : Nat_big_num.num -> bitU list -> bitU list
val exts_bits : Nat_big_num.num -> bitU list -> bitU list
val add_one_bit_ignore_overflow_aux : bitU list -> bitU list
val add_one_bit_ignore_overflow : bitU list -> bitU list
val bits_of_int : Nat_big_num.num -> Nat_big_num.num -> bitU list
val arith_op_bits : (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) -> bool -> bitU list -> bitU list -> bitU list
val char_of_nibble : (bitU * bitU * bitU * bitU) -> char option
val nibble_of_char : char -> (bitU * bitU * bitU * bitU) option
val hexstring_of_bits : bitU list -> char list option
val show_bitlist_prefix : char -> bitU list -> string
val show_bitlist : bitU list -> string
val hex_char : Nat_big_num.num -> char
val hex_str_aux : Nat_big_num.num -> char list -> char list
val hex_str : Nat_big_num.num -> string
val subrange_list_inc : 'a list -> Nat_big_num.num -> Nat_big_num.num -> 'a list
val subrange_list_dec : 'a list -> Nat_big_num.num -> Nat_big_num.num -> 'a list
val subrange_list : bool -> 'a list -> Nat_big_num.num -> Nat_big_num.num -> 'a list
val update_subrange_list_inc : 'a list -> Nat_big_num.num -> Nat_big_num.num -> 'a list -> 'a list
val update_subrange_list_dec : 'a list -> Nat_big_num.num -> Nat_big_num.num -> 'a list -> 'a list
val update_subrange_list : bool -> 'a list -> Nat_big_num.num -> Nat_big_num.num -> 'a list -> 'a list
val access_list_inc : 'a list -> Nat_big_num.num -> 'a
val access_list_dec : 'a list -> Nat_big_num.num -> 'a
val access_list : bool -> 'a list -> Nat_big_num.num -> 'a
val update_list_inc : 'a list -> Nat_big_num.num -> 'a -> 'a list
val update_list_dec : 'a list -> Nat_big_num.num -> 'a -> 'a list
val update_list : bool -> 'a list -> Nat_big_num.num -> 'a -> 'a list
val extract_only_bit : bitU list -> bitU
val slice_mword_inc : (int * Big_int_impl.BI.big_int) -> Nat_big_num.num -> Nat_big_num.num -> Lem.mword
val slice_mword : bool -> (int * Big_int_impl.BI.big_int) -> Nat_big_num.num -> Nat_big_num.num -> Lem.mword
val update_slice_mword_dec : (int * Big_int_impl.BI.big_int) -> Nat_big_num.num -> Nat_big_num.num -> ('a * Big_int_impl.BI.big_int) -> Lem.mword
val update_slice_mword_inc : (int * Big_int_impl.BI.big_int) -> Nat_big_num.num -> Nat_big_num.num -> ('a * Big_int_impl.BI.big_int) -> Lem.mword
val update_slice_mword : bool -> (int * Big_int_impl.BI.big_int) -> Nat_big_num.num -> Nat_big_num.num -> ('a * Big_int_impl.BI.big_int) -> Lem.mword
val access_mword_dec : ('a * Big_int_impl.BI.big_int) -> Nat_big_num.num -> bitU
val access_mword_inc : (int * Big_int_impl.BI.big_int) -> Nat_big_num.num -> bitU
val access_mword : bool -> (int * Big_int_impl.BI.big_int) -> Nat_big_num.num -> bitU
val update_mword_bool_dec : (int * Nat_big_num.num) -> Nat_big_num.num -> bool -> Lem.mword
val update_mword_dec : (int * Nat_big_num.num) -> Nat_big_num.num -> bitU -> Lem.mword option
val update_mword_bool_inc : (int * Nat_big_num.num) -> Nat_big_num.num -> bool -> Lem.mword
val update_mword_inc : (int * Nat_big_num.num) -> Nat_big_num.num -> bitU -> Lem.mword option
val int_of_mword : bool -> (int * Big_int_impl.BI.big_int) -> Nat_big_num.num
val size_itself_int : 'a Lem_machine_word.size_class -> 'b -> Nat_big_num.num
val make_the_value : 'a -> unit
type !'a bitvector_class = {
  1. bits_of_method : 'a -> bitU list;
  2. of_bits_method : bitU list -> 'a option;
  3. of_bools_method : bool list -> 'a;
  4. length_method : 'a -> Nat_big_num.num;
  5. of_int_method : Nat_big_num.num -> Nat_big_num.num -> 'a;
  6. unsigned_method : 'a -> Nat_big_num.num option;
  7. signed_method : 'a -> Nat_big_num.num option;
  8. arith_op_bv_method : (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) -> bool -> 'a -> 'a -> 'a;
}
val of_bits_failwith : 'a bitvector_class -> bitU list -> 'a
val int_of_bv : 'a bitvector_class -> bool -> 'a -> Nat_big_num.num option
val instance_Sail2_values_Bitvector_list_dict : 'a bitU_class -> 'a list bitvector_class
val instance_Sail2_values_Bitvector_Machine_word_mword_dict : 'a Lem_machine_word.size_class -> Lem.mword bitvector_class
val access_bv_inc : 'a bitvector_class -> 'a -> Nat_big_num.num -> bitU
val access_bv_dec : 'a bitvector_class -> 'a -> Nat_big_num.num -> bitU
val update_bv_inc : 'a bitvector_class -> 'a -> Nat_big_num.num -> bitU -> bitU list
val update_bv_dec : 'a bitvector_class -> 'a -> Nat_big_num.num -> bitU -> bitU list
val subrange_bv_inc : 'a bitvector_class -> 'a -> Nat_big_num.num -> Nat_big_num.num -> bitU list
val subrange_bv_dec : 'a bitvector_class -> 'a -> Nat_big_num.num -> Nat_big_num.num -> bitU list
val update_subrange_bv_inc : 'a bitvector_class -> 'b bitvector_class -> 'b -> Nat_big_num.num -> Nat_big_num.num -> 'a -> bitU list
val update_subrange_bv_dec : 'a bitvector_class -> 'b bitvector_class -> 'b -> Nat_big_num.num -> Nat_big_num.num -> 'a -> bitU list
val extz_bv : 'a bitvector_class -> Nat_big_num.num -> 'a -> bitU list
val exts_bv : 'a bitvector_class -> Nat_big_num.num -> 'a -> bitU list
val nat_of_bv : 'a bitvector_class -> 'a -> int option
val string_of_bv : 'a bitvector_class -> 'a -> string
val print_bits : 'a bitvector_class -> string -> 'a -> unit
val dec_str : Nat_big_num.num -> string
val concat_str : string -> string -> string
val int_of_bit : bitU -> Nat_big_num.num
val count_leading_zero_bits : bitU list -> Nat_big_num.num
val count_leading_zeros_bv : 'a bitvector_class -> 'a -> Nat_big_num.num
val decimal_string_of_bv : 'a bitvector_class -> 'a -> string
type memory_byte = bitU list
val byte_chunks : 'a list -> 'a list list option
val bytes_of_bits : 'a bitvector_class -> 'a -> bitU list list option
val bits_of_bytes : bitU list list -> bitU list
val mem_bytes_of_bits : 'a bitvector_class -> 'a -> bitU list list option
val bits_of_mem_bytes : bitU list list -> bitU list
val reverse_endianness_list : 'a list -> 'a list
type (!'regstate, !'regval, !'a) register_ref = {
  1. name : string;
  2. read_from : 'regstate -> 'a;
  3. write_to : 'a -> 'regstate -> 'regstate;
  4. of_regval : 'regval -> 'a option;
  5. regval_of : 'a -> 'regval;
}
type (!'regstate, !'regval) register_accessors = (string -> 'regstate -> 'regval option) * (string -> 'regval -> 'regstate -> 'regstate option)
type (!'regtype, !'a) field_ref = {
  1. field_name : string;
  2. field_start : Nat_big_num.num;
  3. field_is_inc : bool;
  4. get_field : 'regtype -> 'a;
  5. set_field : 'regtype -> 'a -> 'regtype;
}
val foreach : 'a list -> 'vars -> ('a -> 'vars -> 'vars) -> 'vars
val while0 : 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
val until : 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
type !'a toNatural_class = {
  1. toNatural_method : 'a -> Nat_big_num.num;
}
val instance_Sail2_values_ToNatural_Num_integer_dict : Nat_big_num.num toNatural_class
val instance_Sail2_values_ToNatural_Num_int_dict : int toNatural_class
val instance_Sail2_values_ToNatural_nat_dict : int toNatural_class
val instance_Sail2_values_ToNatural_Num_natural_dict : Nat_big_num.num toNatural_class
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