package sail

  1. Overview
  2. Docs
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 =
  1. | V_vector of value list
  2. | V_list of value list
  3. | V_int of Big_int.num
  4. | V_real of Rational.t
  5. | V_bool of bool
  6. | V_bit of Sail_lib.bit
  7. | V_tuple of value list
  8. | V_unit
  9. | V_string of string
  10. | V_ref of string
  11. | V_ctor of string * value list
  12. | V_record of value StringMap.t
  13. | 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