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