Fixed bug in resuming after an action (which was manifesting as an apparent pattern match bug, which was actually working fine).

4 files changed, 19 insertions, 5 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index a43fd241..57b3067b 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -932,7 +932,7 @@ let rec resume_main t_level stack value =
   | Frame id exp env mem stack ->
     match resume_main t_level stack value with
     | Value v -> 
-      match interp_main t_level ((id,value)::env) mem exp with | (o,_,_) -> o end 
+      match interp_main t_level ((id,v)::env) mem exp with | (o,_,_) -> o end 
     | Action action stack -> Action action (Frame id exp env mem stack)
     | Error s -> Error s
     end  
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index ae830ef1..e3f51480 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -41,6 +41,18 @@ let rec val_to_string = function
      sprintf "constructor %s %s" (id_to_string id) (val_to_string value)
 ;;
 
+let rec env_to_string = function
+  | [] -> ""
+  | [id,v] -> sprintf "%s |-> %s" (id_to_string id) (val_to_string v)
+  | (id,v)::env -> sprintf "%s |-> %s, %s" (id_to_string id) (val_to_string v) (env_to_string env)
+
+let rec stack_to_string = function
+  | Top -> "Top"
+  | Frame(id,exp,env,mem,s) ->
+    sprintf "(Frame of %s, e, (%s), m, %s)" (id_to_string id) (env_to_string env) (stack_to_string s)
+;;  
+
+
 let reg_to_string = function Reg (id,_) | SubReg (id,_,_) -> id_to_string id ;;
 let sub_to_string = function None -> "" | Some (x, y) -> sprintf " (%d, %d)" x y
 let act_to_string = function
@@ -88,6 +100,7 @@ let run (name, test) =
   | Value v -> eprintf "%s: returned %s\n" name (val_to_string v)
   | Action (a, s) ->
       eprintf "%s: suspended on action %s\n" name (act_to_string a);
+      (*eprintf "%s: suspended on action %s, with stack %s\n" name (act_to_string a) (stack_to_string s);*)
       let return, env' = perform_action env a in
       eprintf "%s: action returned %s\n" name (val_to_string return);
       loop env' (resume test s return)
diff --git a/src/test/pattern.sail b/src/test/pattern.sail
index 35a6b632..22f0bcc4 100644
--- a/src/test/pattern.sail
+++ b/src/test/pattern.sail
@@ -1,5 +1,5 @@
 
-register nat n
+register nat n 
 register nat x
 register nat y
 
@@ -12,13 +12,13 @@ function unit main _ = {
     case 0 -> { x := 21; x }
     case 1 -> { x := 42; x } 
     case x -> { x := 99; x }
-  });
+  }); 
 
   (* doesn't work - main returns 1 instead of 42 *)
-  n := 1;
+  n := 3;
   switch n {
     case 0 -> { 21 }
     case 1 -> { 42 } 
     case x -> { 99 }
-  }
+  };
 }
diff --git a/src/test/test1.sail b/src/test/test1.sail
index e10608bb..7747783e 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -14,3 +14,4 @@ let bit v = bitzero
 let ( bit [ 32 ] ) v1 = 0b101
 
 function bit main _ = v1[0]
+