diff options
Diffstat (limited to 'model/prelude.sail')
| -rw-r--r-- | model/prelude.sail | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/model/prelude.sail b/model/prelude.sail index c67ec3c..a8faf3d 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -50,16 +50,17 @@ overload operator & = {and_vec} overload operator | = {or_vec} -val cast cast_unit_vec : bit -> bits(1) +val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string -function cast_unit_vec b = match b { - bitzero => 0b0, - bitone => 0b1 -} +val "string_of_bits" : forall 'n. bits('n) -> string -val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string +function string_of_bit(b: bit) -> string = + match b { + bitzero => "0b0", + bitone => "0b1" + } -val BitStr = "string_of_bits" : forall 'n. bits('n) -> string +overload BitStr = {string_of_bits, string_of_bit} val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) @@ -125,10 +126,10 @@ overload zeros = {zeros_implicit} val ones : forall 'n, 'n >= 0 . implicit('n) -> bits('n) function ones (n) = sail_ones (n) -val cast bool_to_bits : bool -> bits(1) +val bool_to_bits : bool -> bits(1) function bool_to_bits x = if x then 0b1 else 0b0 -val cast bit_to_bool : bit -> bool +val bit_to_bool : bit -> bool function bit_to_bool b = match b { bitone => true, bitzero => false |