libsail 0.15 · OCaml Package

module Big_int = Nat_big_num

module StringMap : sig ... end

val print_chan : out_channel ref

val print_redirected : bool ref

val output_redirect : out_channel -> unit

val output_close : unit -> unit

val output : string -> unit

val output_endline : string -> unit

type value =

| V_vector of value list
| V_list of value list
| V_int of Big_int.num
| V_real of Rational.t
| V_bool of bool
| V_bit of Sail_lib.bit
| V_tuple of value list
| V_unit
| V_string of string
| V_ref of string
| V_ctor of string * value list
| V_record of value StringMap.t
| V_attempted_read of string

val is_bit : value -> bool

val string_of_value : value -> string

val eq_value : value -> value -> bool

val coerce_ctor : value -> string * value list

val coerce_bool : value -> bool

val coerce_record : value -> value StringMap.t

val and_bool : value list -> value

val or_bool : value list -> value

val tuple_value : value list -> value

val mk_vector : Sail_lib.bit list -> value

val coerce_bit : value -> Sail_lib.bit

val coerce_tuple : value -> value list

val coerce_list : value -> value list

val coerce_listlike : value -> value list

val coerce_int : value -> Big_int.num

val coerce_real : value -> Rational.t

val coerce_cons : value -> (value * value list) option

val coerce_gv : value -> value list

val coerce_bv : value -> Sail_lib.bit list

val coerce_string : value -> string

val coerce_ref : value -> string

val unit_value : value

val value_eq_int : value list -> value

val value_eq_bool : value list -> value

val value_lteq : value list -> value

val value_gteq : value list -> value

val value_lt : value list -> value

val value_gt : value list -> value

val value_eq_list : value list -> value

val value_eq_string : value list -> value

val value_string_startswith : value list -> value

val value_string_drop : value list -> value

val value_string_take : value list -> value

val value_string_length : value list -> value

val value_eq_bit : value list -> value

val value_length : value list -> value

val value_subrange : value list -> value

val value_access : value list -> value

val value_update : value list -> value

val value_update_subrange : value list -> value

val value_append : value list -> value

val value_append_list : value list -> value

val value_slice : value list -> value

val value_not : value list -> value

val value_not_vec : value list -> value

val value_and_vec : value list -> value

val value_or_vec : value list -> value

val value_xor_vec : value list -> value

val value_uint : value list -> value

val value_sint : value list -> value

val value_get_slice_int : value list -> value

val value_set_slice_int : value list -> value

val value_set_slice : value list -> value

val value_hex_slice : value list -> value

val value_add_int : value list -> value

val value_sub_int : value list -> value

val value_sub_nat : value list -> value

val value_negate : value list -> value

val value_pow2 : value list -> value

val value_int_power : value list -> value

val value_mult : value list -> value

val value_tdiv_int : value list -> value

val value_tmod_int : value list -> value

val value_quotient : value list -> value

val value_modulus : value list -> value

val value_abs_int : value list -> value

val value_add_vec_int : value list -> value

val value_sub_vec_int : value list -> value

val value_add_vec : value list -> value

val value_sub_vec : value list -> value

val value_shl_int : value list -> value

val value_shr_int : value list -> value

val value_max_int : value list -> value

val value_min_int : value list -> value

val value_replicate_bits : value list -> value

val value_count_leading_zeros : value list -> value

val is_ctor : value -> bool

val value_sign_extend : value list -> value

val value_zero_extend : value list -> value

val value_zeros : value list -> value

val value_ones : value list -> value

val value_shiftl : value list -> value

val value_shiftr : value list -> value

val value_arith_shiftr : value list -> value

val value_shift_bits_left : value list -> value

val value_shift_bits_right : value list -> value

val value_vector_truncate : value list -> value

val value_vector_truncateLSB : value list -> value

val value_eq_anything : value list -> value

val value_print : value list -> value

val value_print_endline : value list -> value

val value_internal_pick : value list -> value

val value_undefined_vector : value list -> value

val value_undefined_list : 'a list -> value

val value_undefined_bitvector : value list -> value

val value_read_ram : value list -> value

val value_write_ram : value list -> value

val value_load_raw : value list -> value

val value_putchar : value list -> value

val value_print_bits : value list -> value

val value_print_int : value list -> value

val value_print_string : value list -> value

val value_prerr_bits : value list -> value

val value_prerr_int : value list -> value

val value_prerr_string : value list -> value

val value_concat_str : value list -> value

val value_to_real : value list -> value

val value_print_real : value list -> value

val value_random_real : 'a list -> value

val value_sqrt_real : value list -> value

val value_quotient_real : value list -> value

val value_round_up : value list -> value

val value_round_down : value list -> value

val value_quot_round_zero : value list -> value

val value_rem_round_zero : value list -> value

val value_add_real : value list -> value

val value_sub_real : value list -> value

val value_mult_real : value list -> value

val value_div_real : value list -> value

val value_abs_real : value list -> value

val value_eq_real : value list -> value

val value_lt_real : value list -> value

val value_gt_real : value list -> value

val value_lteq_real : value list -> value

val value_gteq_real : value list -> value

val value_string_append : value list -> value

val value_decimal_string_of_bits : value list -> value

val primops : (value list -> value) StringMap.t ref

val add_primop : StringMap.key -> (value list -> value) -> unit

package libsail