Catch up to sail mainline

These definitions are now provided by sail's libraries, as of
rems-project/sail@eb8af69 .

This includes the change in #349
and, presumably, will also not pass CI until the sail version used there
is bumped.

model/prelude.sail

@@ -75,6 +75,7 @@ $include <option.sail>
 $include <arith.sail>
 $include <string.sail>
 $include <vector_dec.sail>
+$include <mapping.sail>
 $include <regfp.sail>
 
 val string_startswith = "string_startswith" : (string, string) -> bool
@@ -164,9 +165,6 @@ overload min = {min_int}
 
 overload max = {max_int}
 
-val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
-
-val print = "print_endline" : string -> unit
 val print_string = "print_string" : (string, string) -> unit
 
 val print_instr    = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit
@@ -293,44 +291,6 @@ 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)
-
 overload operator / = {quot_round_zero}
 overload operator * = {mult_atom, mult_int}
 

model/prelude_mapping.sail

@@ -466,25 +466,6 @@ 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_21 : bits(21) <-> string
 val hex_bits_21_forwards = "decimal_string_of_bits" : bits(21) -> string
 val hex_bits_21_forwards_matches : bits(21) -> bool

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