Re-implement space-related mapping functions in Sail rather than backends

Uses new primop 'string_take' which is much easier to implement in e.g. C

3 files changed, 16 insertions, 22 deletions

diff --git a/src/gen_lib/sail2_string.lem b/src/gen_lib/sail2_string.lem
index c50db099..de7588dc 100644
--- a/src/gen_lib/sail2_string.lem
+++ b/src/gen_lib/sail2_string.lem
@@ -20,6 +20,10 @@ val string_drop : string -> ii -> string
 let string_drop str n =
   toString (drop (natFromInteger n) (toCharList str))
 
+val string_take : string -> ii -> string
+let string_take str n =
+  toString (take (natFromInteger n) (toCharList str))
+
 val string_length : string -> ii
 let string_length s = integerFromNat (stringLength s)
 
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index eecf9579..a718e6d5 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -530,6 +530,13 @@ let string_startswith (str1, str2) = String.length str1 >= String.length str2 &&
 
 let string_drop (str, n) = if (Big_int.less_equal (Big_int.of_int (String.length str)) n) then "" else let n = Big_int.to_int n in String.sub str n (String.length str - n)
 
+let string_take (str, n) =
+  let n = Big_int.to_int n in
+  if String.length str <= n then
+    str
+  else
+    String.sub str 0 n
+
 let string_length str = Big_int.of_int (String.length str)
 
 let string_append (s1, s2) = s1 ^ s2
@@ -704,28 +711,6 @@ let speculate_conditional_success () = true
 (* Return nanoseconds since epoch. Truncates to ocaml int but will be OK for next 100 years or so... *)
 let get_time_ns () = Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ()))
 
-let rec n_leading_spaces s =
-  match String.length s with
-  | 0 -> 0
-  | 1 -> begin match s with
-         | " " -> 1
-         | _ -> 0
-         end
-  | len -> begin match String.get s 0 with
-           | ' ' -> 1 + (n_leading_spaces (String.sub s 1 (len - 1)))
-           | _ -> 0
-           end
-
-
-let opt_spc_matches_prefix s =
-  ZSome ((), n_leading_spaces s |> Big_int.of_int)
-
-let spc_matches_prefix s =
-  let n = n_leading_spaces s in
-  match n with
-  | 0 -> ZNone ()
-  | n -> ZSome ((), Big_int.of_int n)
-
 (* Python:
 f = """let hex_bits_{0}_matches_prefix s =
   match maybe_int_of_prefix s with
diff --git a/src/value.ml b/src/value.ml
index 6c9990a1..157c16fc 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -219,6 +219,10 @@ let value_string_drop = function
   | [v1; v2] -> V_string (Sail_lib.string_drop (coerce_string v1, coerce_int v2))
   | _ -> failwith "value string_drop"
 
+let value_string_take = function
+  | [v1; v2] -> V_string (Sail_lib.string_take (coerce_string v1, coerce_int v2))
+  | _ -> failwith "value string_take"
+
 let value_string_length = function
   | [v] -> V_int (coerce_string v |> Sail_lib.string_length)
   | _ -> failwith "value string_length"
@@ -549,6 +553,7 @@ let primops =
       ("eq_string", value_eq_string);
       ("string_startswith", value_string_startswith);
       ("string_drop", value_string_drop);
+      ("string_take", value_string_take);
       ("string_length", value_string_length);
       ("eq_bit", value_eq_bit);
       ("eq_anything", value_eq_anything);