libsail 0.18 (latest) · OCaml Package

val uint_maybe : Sail2_values.bitU list -> Nat_big_num.num option

val uint_fail : 
  'a Sail2_values.bitvector_class ->
  'a ->
  ('c, Nat_big_num.num, 'b) Sail2_prompt_monad.monad

val uint_nondet : 
  'b Sail2_values.register_Value_class ->
  Sail2_values.bitU list ->
  ('b, Nat_big_num.num, 'a) Sail2_prompt_monad.monad

val uint : Sail2_values.bitU list -> Nat_big_num.num

val sint_maybe : Sail2_values.bitU list -> Nat_big_num.num option

val sint_fail : 
  'a Sail2_values.bitvector_class ->
  'a ->
  ('c, Nat_big_num.num, 'b) Sail2_prompt_monad.monad

val sint_nondet : 
  'b Sail2_values.register_Value_class ->
  Sail2_values.bitU list ->
  ('b, Nat_big_num.num, 'a) Sail2_prompt_monad.monad

val sint : Sail2_values.bitU list -> Nat_big_num.num

val extz_vec : 
  Nat_big_num.num ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val exts_vec : 
  Nat_big_num.num ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val zero_extend : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val sign_extend : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val zeros : Nat_big_num.num -> Sail2_values.bitU list

val ones : Nat_big_num.num -> Sail2_values.bitU list

val vector_truncate : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val vector_truncateLSB : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val access_vec_inc : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU

val access_vec_dec : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU

val update_vec_inc : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU ->
  Sail2_values.bitU list

val update_vec_inc_maybe : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU ->
  Sail2_values.bitU list option

val update_vec_inc_fail : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU ->
  ('b, Sail2_values.bitU list, 'a) Sail2_prompt_monad.monad

val update_vec_inc_nondet : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU ->
  ('b, Sail2_values.bitU list, 'a) Sail2_prompt_monad.monad

val update_vec_dec : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU ->
  Sail2_values.bitU list

val update_vec_dec_maybe : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU ->
  Sail2_values.bitU list option

val update_vec_dec_fail : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU ->
  ('b, Sail2_values.bitU list, 'a) Sail2_prompt_monad.monad

val update_vec_dec_nondet : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU ->
  ('b, Sail2_values.bitU list, 'a) Sail2_prompt_monad.monad

val subrange_vec_inc : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val subrange_vec_dec : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val update_subrange_vec_inc : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val update_subrange_vec_dec : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val concat_vec : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val cons_vec : 
  Sail2_values.bitU ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val cons_vec_maybe : 
  Sail2_values.bitU ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list option

val cons_vec_fail : 
  Sail2_values.bitU ->
  Sail2_values.bitU list ->
  ('b, Sail2_values.bitU list, 'a) Sail2_prompt_monad.monad

val cons_vec_nondet : 
  Sail2_values.bitU ->
  Sail2_values.bitU list ->
  ('b, Sail2_values.bitU list, 'a) Sail2_prompt_monad.monad

val cast_unit_vec : Sail2_values.bitU -> Sail2_values.bitU list

val cast_unit_vec_maybe : Sail2_values.bitU -> Sail2_values.bitU list option

val cast_unit_vec_fail : 
  Sail2_values.bitU ->
  ('b, Sail2_values.bitU list, 'a) Sail2_prompt_monad.monad

val cast_unit_vec_nondet : 
  Sail2_values.bitU ->
  ('b, Sail2_values.bitU list, 'a) Sail2_prompt_monad.monad

val vec_of_bit : Nat_big_num.num -> Sail2_values.bitU -> Sail2_values.bitU list

val vec_of_bit_maybe : 
  Nat_big_num.num ->
  Sail2_values.bitU ->
  Sail2_values.bitU list option

val vec_of_bit_fail : 
  Nat_big_num.num ->
  Sail2_values.bitU ->
  ('b, Sail2_values.bitU list, 'a) Sail2_prompt_monad.monad

val vec_of_bit_nondet : 
  Nat_big_num.num ->
  Sail2_values.bitU ->
  ('b, Sail2_values.bitU list, 'a) Sail2_prompt_monad.monad

val msb : Sail2_values.bitU list -> Sail2_values.bitU

val int_of_vec_maybe : bool -> Sail2_values.bitU list -> Nat_big_num.num option

val int_of_vec_fail : 
  bool ->
  Sail2_values.bitU list ->
  ('b, Nat_big_num.num, 'a) Sail2_prompt_monad.monad

val int_of_vec_nondet : 
  'b Sail2_values.register_Value_class ->
  bool ->
  Sail2_values.bitU list ->
  ('b, Nat_big_num.num, 'a) Sail2_prompt_monad.monad

val int_of_vec : bool -> Sail2_values.bitU list -> Nat_big_num.num

val string_of_bits : Sail2_values.bitU list -> string

val string_of_bits_subrange : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  string

val decimal_string_of_bits : Sail2_values.bitU list -> string

val and_vec : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val or_vec : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val xor_vec : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val not_vec : Sail2_values.bitU list -> Sail2_values.bitU list

val arith_op_double_bl : 
  'a Sail2_values.bitvector_class ->
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  bool ->
  'a ->
  'a ->
  Sail2_values.bitU list

val add_vec : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val adds_vec : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val sub_vec : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val subs_vec : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val mult_vec : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val mults_vec : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val add_vec_int : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val sub_vec_int : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val mult_vec_int : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val add_int_vec : 
  Nat_big_num.num ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val sub_int_vec : 
  Nat_big_num.num ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val mult_int_vec : 
  Nat_big_num.num ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val add_vec_bool : 'a Sail2_values.bitvector_class -> 'a -> bool -> 'a

val add_vec_bit_maybe : 
  'a Sail2_values.bitvector_class ->
  'a ->
  Sail2_values.bitU ->
  'a option

val add_vec_bit_fail : 
  'a Sail2_values.bitvector_class ->
  'a ->
  Sail2_values.bitU ->
  ('d, 'a, 'c) Sail2_prompt_monad.monad

val add_vec_bit_nondet : 
  'a Sail2_values.bitvector_class ->
  'd Sail2_values.register_Value_class ->
  'a ->
  Sail2_values.bitU ->
  ('d, 'a, 'c) Sail2_prompt_monad.monad

val add_vec_bit : 
  Sail2_values.bitU list ->
  Sail2_values.bitU ->
  Sail2_values.bitU list

val adds_vec_bool : 'a Sail2_values.bitvector_class -> 'a -> bool -> 'a

val adds_vec_bit_maybe : 
  'a Sail2_values.bitvector_class ->
  'a ->
  Sail2_values.bitU ->
  'a option

val adds_vec_bit_fail : 
  'a Sail2_values.bitvector_class ->
  'a ->
  Sail2_values.bitU ->
  ('d, 'a, 'c) Sail2_prompt_monad.monad

val adds_vec_bit_nondet : 
  'a Sail2_values.bitvector_class ->
  'd Sail2_values.register_Value_class ->
  'a ->
  Sail2_values.bitU ->
  ('d, 'a, 'c) Sail2_prompt_monad.monad

val adds_vec_bit : 
  Sail2_values.bitU list ->
  Sail2_values.bitU ->
  Sail2_values.bitU list

val sub_vec_bool : 'a Sail2_values.bitvector_class -> 'a -> bool -> 'a

val sub_vec_bit_maybe : 
  'a Sail2_values.bitvector_class ->
  'a ->
  Sail2_values.bitU ->
  'a option

val sub_vec_bit_fail : 
  'a Sail2_values.bitvector_class ->
  'a ->
  Sail2_values.bitU ->
  ('d, 'a, 'c) Sail2_prompt_monad.monad

val sub_vec_bit_nondet : 
  'a Sail2_values.bitvector_class ->
  'd Sail2_values.register_Value_class ->
  'a ->
  Sail2_values.bitU ->
  ('d, 'a, 'c) Sail2_prompt_monad.monad

val sub_vec_bit : 
  Sail2_values.bitU list ->
  Sail2_values.bitU ->
  Sail2_values.bitU list

val subs_vec_bool : 'a Sail2_values.bitvector_class -> 'a -> bool -> 'a

val subs_vec_bit_maybe : 
  'a Sail2_values.bitvector_class ->
  'a ->
  Sail2_values.bitU ->
  'a option

val subs_vec_bit_fail : 
  'a Sail2_values.bitvector_class ->
  'a ->
  Sail2_values.bitU ->
  ('d, 'a, 'c) Sail2_prompt_monad.monad

val subs_vec_bit_nondet : 
  'a Sail2_values.bitvector_class ->
  'd Sail2_values.register_Value_class ->
  'a ->
  Sail2_values.bitU ->
  ('d, 'a, 'c) Sail2_prompt_monad.monad

val subs_vec_bit : 
  Sail2_values.bitU list ->
  Sail2_values.bitU ->
  Sail2_values.bitU list

val shiftl : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val shiftr : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val arith_shiftr : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val rotl : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list

val rotr : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list

val mod_vec : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val mod_vec_maybe : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list option

val mod_vec_fail : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  ('rv, Sail2_values.bitU list, 'e) Sail2_prompt_monad.monad

val mod_vec_nondet : 
  'rv Sail2_values.register_Value_class ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  ('rv, Sail2_values.bitU list, 'e) Sail2_prompt_monad.monad

val quot_vec : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val quot_vec_maybe : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list option

val quot_vec_fail : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  ('rv, Sail2_values.bitU list, 'e) Sail2_prompt_monad.monad

val quot_vec_nondet : 
  'rv Sail2_values.register_Value_class ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  ('rv, Sail2_values.bitU list, 'e) Sail2_prompt_monad.monad

val quots_vec : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val quots_vec_maybe : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list option

val quots_vec_fail : 
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  ('rv, Sail2_values.bitU list, 'e) Sail2_prompt_monad.monad

val quots_vec_nondet : 
  'rv Sail2_values.register_Value_class ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list ->
  ('rv, Sail2_values.bitU list, 'e) Sail2_prompt_monad.monad

val mod_vec_int : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val mod_vec_int_maybe : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU list option

val mod_vec_int_fail : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  ('rv, Sail2_values.bitU list, 'e) Sail2_prompt_monad.monad

val mod_vec_int_nondet : 
  'rv Sail2_values.register_Value_class ->
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  ('rv, Sail2_values.bitU list, 'e) Sail2_prompt_monad.monad

val quot_vec_int : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val quot_vec_int_maybe : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU list option

val quot_vec_int_fail : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  ('rv, Sail2_values.bitU list, 'e) Sail2_prompt_monad.monad

val quot_vec_int_nondet : 
  'rv Sail2_values.register_Value_class ->
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  ('rv, Sail2_values.bitU list, 'e) Sail2_prompt_monad.monad

val replicate_bits : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val duplicate : Sail2_values.bitU -> Nat_big_num.num -> Sail2_values.bitU list

val duplicate_maybe : 
  Sail2_values.bitU ->
  Nat_big_num.num ->
  Sail2_values.bitU list option

val duplicate_fail : 
  Sail2_values.bitU ->
  Nat_big_num.num ->
  ('b, Sail2_values.bitU list, 'a) Sail2_prompt_monad.monad

val duplicate_nondet : 
  'b Sail2_values.register_Value_class ->
  Sail2_values.bitU ->
  Nat_big_num.num ->
  ('b, Sail2_values.bitU list, 'a) Sail2_prompt_monad.monad

val reverse_endianness : Sail2_values.bitU list -> Sail2_values.bitU list

val get_slice_int : 
  Nat_big_num.num ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val set_slice_int : 
  Nat_big_num.num ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Sail2_values.bitU list ->
  Nat_big_num.num

val slice : 
  Sail2_values.bitU list ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val set_slice : 
  Sail2_values.ii ->
  Sail2_values.ii ->
  Sail2_values.bitU list ->
  Sail2_values.ii ->
  Sail2_values.bitU list ->
  Sail2_values.bitU list

val eq_vec : Sail2_values.bitU list -> Sail2_values.bitU list -> bool

val neq_vec : Sail2_values.bitU list -> Sail2_values.bitU list -> bool

package libsail