changes to riscv model to support rmem

2 files changed, 20 insertions, 14 deletions

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
diff --git a/src/lem_interp/sail2_instr_kinds.lem b/src/lem_interp/sail2_instr_kinds.lem
index d8a2c0c0..13e5304e 100644
--- a/src/lem_interp/sail2_instr_kinds.lem
+++ b/src/lem_interp/sail2_instr_kinds.lem
@@ -198,11 +198,11 @@ type instruction_kind =
   | IK_mem_read  of read_kind
   | IK_mem_write of write_kind
   | IK_mem_rmw   of (read_kind * write_kind)
-  | IK_branch (* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address),
+  | IK_branch    of unit(* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address),
   indirect/computed-branch (single nia of kind NIA_indirect_address)
   and branch/jump (single nia of kind NIA_concrete_address) *)
   | IK_trans     of trans_kind
-  | IK_simple
+  | IK_simple    of unit
 
 
 instance (Show instruction_kind)
@@ -213,7 +213,7 @@ instance (Show instruction_kind)
     | IK_mem_rmw (r, w)       -> "IK_mem_rmw " ^ (show r) ^ " " ^ (show w)
     | IK_branch               -> "IK_branch"
     | IK_trans trans_kind     -> "IK_trans " ^ (show trans_kind)
-    | IK_simple               -> "IK_simple"
+    | IK_simple ()            -> "IK_simple"
   end
 end