Module `Libsail.Sail2_operators_bitlists`Source

Sourceval 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

Source

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

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

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

Source

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

Source

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

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

Source

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

Source

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

Source

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

Source

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

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

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

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

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

Source

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

Source

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

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

Source

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

Source

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

Source

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

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

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

Source

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

Source

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

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

Sourceval string_of_bits : Sail2_values.bitU list -> string

Source

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

Sourceval decimal_string_of_bits : Sail2_values.bitU list -> string

Source

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

Source

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

Source

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

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

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

Source

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

Source

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

Source

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

Source

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

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

Source

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

Source

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

Source

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

Source

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

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

Source

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

Source

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

Source

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

Source

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

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

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

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

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

Source

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

Source

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

Source

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

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

Source

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

Source

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

Source

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

Source

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

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

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

package libsail

Module Libsail.Sail2_operators_bitlistsSource

Module `Libsail.Sail2_operators_bitlists`Source