From 326f0dd88df92d3936b7acadb5073802d3f9d77b Mon Sep 17 00:00:00 2001
From: Jon French
Date: Thu, 21 Jun 2018 13:09:29 +0100
Subject: changes to riscv model to support rmem

---
 src/gen_lib/sail2_string.lem | 28 +++++++++++++++++-----------
 1 file changed, 17 insertions(+), 11 deletions(-)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/sail2_string.lem b/src/gen_lib/sail2_string.lem
index 329da942..a54ffa65 100644
--- a/src/gen_lib/sail2_string.lem
+++ b/src/gen_lib/sail2_string.lem
@@ -31,7 +31,7 @@ let string_append = stringAppend
 
 val maybeIntegerOfString : string -> maybe integer
 
-declare ocaml target_rep function maybeIntegerOfString = `(fun s -> match int_of_string_opt s with None -> None | Some i -> Nat_big_num.of_int i)`
+declare ocaml target_rep function maybeIntegerOfString = `(fun s -> match int_of_string_opt s with None -> None | Some i -> Some (Nat_big_num.of_int i))`
 declare isabelle target_rep function maybeIntegerOfString = `maybeIntegerOfString` (* TODO FIXME *)
 declare hol target_rep function maybeIntegerOfString = `maybeIntegerOfString` (* TODO FIXME *)
 
@@ -54,27 +54,33 @@ let maybe_int_of_string = maybeIntegerOfString
 
 val n_leading_spaces : string -> ii
 let rec n_leading_spaces s =
-  match string_length s with
-  | 0 -> 0
-  | 1 -> match s with
+  let len = string_length s in
+  if len = 0 then 0 else
+    if len = 1 then
+      match s with
          | " " -> 1
          | _ -> 0
-         end
-  | len -> match nth s 0 with
+      end
+    else
+      (* match len with
+   *     (\* | 0 -> 0 *\)
+   * (\* | 1 -> *\) 
+   * | len -> *) match nth s 0 with
            | #' ' -> 1 + (n_leading_spaces (string_sub s 1 (len - 1)))
            | _ -> 0
            end
-  end
+  (* end *)
 
 let opt_spc_matches_prefix s =
   Just ((), n_leading_spaces s)
 
 let spc_matches_prefix s =
   let n = n_leading_spaces s in
-  match n with
-  | 0 -> Nothing
-  | n -> Just ((), n)
-  end
+  (* match n with *)
+(* | 0 -> Nothing *)
+  if n = 0 then Nothing else
+  (* | n -> *) Just ((), n)
+  (* end *)
 
 let hex_bits_5_matches_prefix s =
   match maybe_int_of_prefix s with
-- 
cgit v1.2.3