Simplify prelude.sail by including generic_equality.sail and mapping.…

…sail

This change includes `generic_equality.sail` and `mapping.sail` from the Sail standard library which defines a lot of things that were defined in `prelude.sail`.

I also removed `reg_deref` which as far as I can tell is removed.

`hex_bits_20` is commented out because it is defined by `mapping.sail` (but none of the others are; I am not sure why).

model/prelude.sail

@@ -74,53 +74,20 @@ $include <smt.sail>
 $include <option.sail>
 $include <arith.sail>
 $include <string.sail>
+$include <mapping.sail>
 $include <vector_dec.sail>
 $include <regfp.sail>
+$include <generic_equality.sail>
 
-val string_startswith = "string_startswith" : (string, string) -> bool
-val string_drop = "string_drop" : (string, nat) -> string
-val string_take = "string_take" : (string, nat) -> string
-val string_length = "string_length" : string -> nat
-val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string
-
-val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq", c: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
-
-overload operator == = {eq_string, eq_anything}
-
-val "reg_deref" : forall ('a : Type). register('a) -> 'a
-/* sneaky deref with no effect necessary for bitfield writes */
-val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
-
-val any_vector_update = {ocaml: "update", lem: "update_list_dec", coq: "vector_update"} : forall 'n ('a : Type).
-  (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
-
-overload vector_update = {any_vector_update}
-
-val update_subrange = {ocaml: "update_subrange", interpreter: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
-  (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
-
-val vector_concat = {ocaml: "append", lem: "append_list", coq: "vec_concat"} : forall ('n : Int) ('m : Int) ('a : Type).
-  (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
-
-overload append = {vector_concat}
 
 val not_bit : bit -> bit
-
 function not_bit(b) = if b == bitone then bitzero else bitone
 
 overload ~ = {not_bool, not_vec, not_bit}
 
-val not = pure {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> bool(not('p))
-
-val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
-
-function neq_vec (x, y) = not_bool(eq_bits(x, y))
-
-val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool
-
-function neq_anything (x, y) = not_bool(x == y)
-
-overload operator != = {neq_vec, neq_anything}
+// not_bool alias.
+val not : forall ('p : Bool). bool('p) -> bool(not('p))
+function not(b) = not_bool(b)
 
 overload operator & = {and_vec}
 
@@ -280,50 +247,3 @@ function reverse_bits_in_byte (xs : bits(8)) -> bits(8) = {
 }
 
 overload reverse = {reverse_bits_in_byte}
-
-/* helpers for mappings */
-
-val spc : unit <-> string
-val opt_spc : unit <-> string
-val def_spc : unit <-> string
-
-val "decimal_string_of_bits" : forall 'n. bits('n) -> string
-val hex_bits : forall 'n . (atom('n), bits('n)) <-> string
-
-val n_leading_spaces : string -> nat
-function n_leading_spaces s =
-  match s {
-    "" => 0,
-    _ => match string_take(s, 1) {
-      " " => 1 + n_leading_spaces(string_drop(s, 1)),
-      _ => 0
-    }
-  }
-
-val spc_forwards : unit -> string
-function spc_forwards () = " "
-val spc_backwards : string -> unit
-function spc_backwards s = ()
-val spc_matches_prefix : string -> option((unit, nat))
-function spc_matches_prefix s = {
-  let n = n_leading_spaces(s);
-  match n {
-    0 => None(),
-    _ => Some((), n)
-  }
-}
-
-val opt_spc_forwards : unit -> string
-function opt_spc_forwards () = ""
-val opt_spc_backwards : string -> unit
-function opt_spc_backwards s = ()
-val opt_spc_matches_prefix : string -> option((unit, nat))
-function opt_spc_matches_prefix s =
-  Some((), n_leading_spaces(s))
-
-val def_spc_forwards : unit -> string
-function def_spc_forwards () = " "
-val def_spc_backwards : string -> unit
-function def_spc_backwards s = ()
-val def_spc_matches_prefix : string -> option((unit, nat))
-function def_spc_matches_prefix s = opt_spc_matches_prefix(s)

model/prelude_mapping.sail

@@ -466,24 +466,24 @@ function hex_bits_19_backwards s =
       Some (bv, n) if n == string_length(s) => bv
   }
 
-val hex_bits_20 : bits(20) <-> string
-val hex_bits_20_forwards = "decimal_string_of_bits" : bits(20) -> string
-val hex_bits_20_forwards_matches : bits(20) -> bool
-function hex_bits_20_forwards_matches bv = true
-val "hex_bits_20_matches_prefix" : string -> option((bits(20), nat))
-val hex_bits_20_backwards_matches : string -> bool
-function hex_bits_20_backwards_matches s = match s {
-  s if match hex_bits_20_matches_prefix(s) {
-    Some (_, n) if n == string_length(s) => true,
-    _ => false
-  } => true,
-  _ => false
-}
-val hex_bits_20_backwards : string -> bits(20)
-function hex_bits_20_backwards s =
-  match hex_bits_20_matches_prefix(s) {
-      Some (bv, n) if n == string_length(s) => bv
-  }
+// val hex_bits_20 : bits(20) <-> string
+// val hex_bits_20_forwards = "decimal_string_of_bits" : bits(20) -> string
+// val hex_bits_20_forwards_matches : bits(20) -> bool
+// function hex_bits_20_forwards_matches bv = true
+// val "hex_bits_20_matches_prefix" : string -> option((bits(20), nat))
+// val hex_bits_20_backwards_matches : string -> bool
+// function hex_bits_20_backwards_matches s = match s {
+//   s if match hex_bits_20_matches_prefix(s) {
+//     Some (_, n) if n == string_length(s) => true,
+//     _ => false
+//   } => true,
+//   _ => false
+// }
+// val hex_bits_20_backwards : string -> bits(20)
+// function hex_bits_20_backwards s =
+//   match hex_bits_20_matches_prefix(s) {
+//       Some (bv, n) if n == string_length(s) => bv
+//   }
 
 val hex_bits_21 : bits(21) <-> string
 val hex_bits_21_forwards = "decimal_string_of_bits" : bits(21) -> string

model/riscv_types.sail

@@ -419,11 +419,6 @@ enum extop_zbb = {RISCV_SEXTB, RISCV_SEXTH, RISCV_ZEXTH}
 
 enum zicondop = {RISCV_CZERO_EQZ, RISCV_CZERO_NEZ}
 
-val sep : unit <-> string
-mapping sep : unit <-> string = {
-  ()     <-> opt_spc() ^ "," ^ def_spc()
-}
-
 mapping bool_bits : bool <-> bits(1) = {
   true   <-> 0b1,
   false  <-> 0b0