diff --git a/model/prelude.sail b/model/prelude.sail index ae1cafc3a..45d49c0ed 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -99,18 +99,28 @@ overload zeros = {zeros_implicit} val ones : forall 'n, 'n >= 0 . implicit('n) -> bits('n) function ones (n) = sail_ones (n) -val bool_to_bit : bool -> bit -function bool_to_bit x = if x then bitone else bitzero +mapping bool_bit : bool <-> bit = { + true <-> bitone, + false <-> bitzero, +} -val bool_to_bits : bool -> bits(1) -function bool_to_bits x = [bool_to_bit(x)] +mapping bool_bits : bool <-> bits(1) = { + true <-> 0b1, + false <-> 0b0, +} -val bit_to_bool : bit -> bool -function bit_to_bool b = match b { - bitone => true, - bitzero => false +mapping bool_not_bits : bool <-> bits(1) = { + true <-> 0b0, + false <-> 0b1, } +// These aliases make the conversion direction a bit clearer. +function bool_to_bit(x : bool) -> bit = bool_bit(x) +function bit_to_bool(x : bit) -> bool = bool_bit(x) +function bool_to_bits(x : bool) -> bits(1) = bool_bits(x) +function bits_to_bool(x : bits(1)) -> bool = bool_bits(x) + + val to_bits : forall 'l, 'l >= 0.(int('l), int) -> bits('l) function to_bits (l, n) = get_slice_int(l, n, 0) diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 2b1c132ec..d0abec31e 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -357,16 +357,6 @@ enum extop_zbb = {RISCV_SEXTB, RISCV_SEXTH, RISCV_ZEXTH} enum zicondop = {RISCV_CZERO_EQZ, RISCV_CZERO_NEZ} -mapping bool_bits : bool <-> bits(1) = { - true <-> 0b1, - false <-> 0b0 -} - -mapping bool_not_bits : bool <-> bits(1) = { - true <-> 0b0, - false <-> 0b1 -} - // Get the bit encoding of word_width. mapping size_enc : word_width <-> bits(2) = { BYTE <-> 0b00,