Improve printing of function calls in stepper mode

4 files changed, 72 insertions, 23 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 0bba3b7e..9cdb1246 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -76,6 +76,39 @@ type value =
  | V_register_alias of (alias_spec tannot) * tannot (* Same as above, but to a concatenation of two registers *)
  | V_track of value * (list reg_form) (* Used when memory system wants to track what register(s) a value came from *)
 
+let rec list_to_string format sep lst = match lst with 
+  | [] -> ""
+  | [last] -> format last
+  | one::rest -> (format one) ^ sep ^ (list_to_string format sep rest)
+end
+
+let rec string_of_value v = match v with
+  | V_boxref nat t -> "$#" ^ (show nat) ^ "$"
+  | V_lit (L_aux lit _) -> 
+    (match lit with
+    | L_unit -> "()"
+    | L_zero -> "0"
+    | L_one  -> "1"
+    | L_true -> "true"
+    | L_false -> "false"
+    | L_num num -> show (natFromInteger num)
+    | L_hex hex -> "0x" ^ hex
+    | L_bin bin -> "0b" ^ bin
+    | L_undef -> "undefined"
+    | L_string str-> "\"" ^ str ^ "\"" end)
+  | V_tuple vals -> "(" ^ (list_to_string string_of_value "," vals) ^ ")"
+  | V_list vals -> "[||" ^ (list_to_string string_of_value "," vals) ^ "||]"
+  | V_vector i inc vals -> "[" ^ (list_to_string string_of_value "," vals) ^ "]"
+  | V_vector_sparse _ _ _ _ _ -> "sparse_vector"
+  | V_record t vals ->
+    "{" ^ (list_to_string (fun (id,v) -> (get_id id) ^ "=" ^ (string_of_value v)) ";" vals) ^ "}"
+  | V_ctor id t value -> (get_id id) ^ " " ^ string_of_value value     
+  | V_unknown -> "Unknown"
+  | V_register _ -> "register_as_value"
+  | V_register_alias _ _ -> "register_as_value"
+  | V_track v _ -> string_of_value v
+end
+
 let rec id_value_eq (i, v) (i', v') = i = i' && value_eq v v'
 and value_eq left right =
   (* XXX it is not clear whether t = t' will work in all cases *)
@@ -132,7 +165,7 @@ type action =
  | Nondet of list (exp tannot)
  | Call_extern of string * value
  | Exit of (exp tannot)
- (* For stepper, no action needed. String is function called, value is parameter, on next state being a new function body *)
+ (* For stepper, no action needed. String is function called, value is parameter, on next state is a new function body *)
  | Step of l * maybe string * maybe value 
 
 (* Inverted call stack, where top item on the stack is waiting for an action to resolve and all other frames for the right stack *)
@@ -1012,7 +1045,8 @@ let resolve_outcome to_match value_thunk action_thunk =
 
 let update_stack (Action act stack) fn = Action act (fn stack)  
 
-let debug_out e tl lm le = (Action (Step (get_exp_l e) Nothing Nothing) (Thunk_frame e tl le lm Top),lm,le)
+let debug_out fn value e tl lm le = 
+  (Action (Step (get_exp_l e) fn value) (Thunk_frame e tl le lm Top),lm,le)
 
 let to_exps mode env vals = 
   List.foldr (fun v (es,env) -> let (e,env') = to_exp mode env v in (e::es, union_env env env')) ([],env) vals
@@ -1118,11 +1152,11 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 	  match (value,mode.eager_eval) with
             | (V_lit(L_aux L_true _),true) -> interp_main mode t_level l_env lm thn
 	    | (V_track (V_lit (L_aux L_true _)) _, true) -> interp_main mode t_level l_env lm thn
-	    | (V_lit(L_aux L_true _),false) -> debug_out thn t_level lm l_env 
-	    | (V_track (V_lit (L_aux L_true _)) _, false) -> debug_out thn t_level lm l_env
+	    | (V_lit(L_aux L_true _),false) -> debug_out Nothing Nothing thn t_level lm l_env 
+	    | (V_track (V_lit (L_aux L_true _)) _, false) -> debug_out Nothing Nothing thn t_level lm l_env
 	    | (V_unknown,_) -> interp_main mode t_level l_env lm (E_aux (E_block [thn;els]) (l,annot))
             | (_,true) -> interp_main mode t_level l_env lm els 
-	    | (_,false) -> debug_out els t_level lm l_env end)
+	    | (_,false) -> debug_out Nothing Nothing els t_level lm l_env end)
         (fun a -> update_stack a (add_to_top_frame (fun c env -> (E_aux (E_if c thn els) (l,annot), env))))
     | E_for id from to_ by ((Ord_aux o _) as order) exp ->
       let is_inc = match o with | Ord_inc -> true | _ -> false end in
@@ -1168,7 +1202,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 					    (l,annot)) in
 				if mode.eager_eval
 				then interp_main mode t_level env lm e 
-				else debug_out e t_level lm env
+				else debug_out Nothing Nothing e t_level lm env
                             | V_unknown -> 
 			      let e = 
 				(E_aux (E_let 
@@ -1204,7 +1238,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
             | [(env,used_unknown,exp)] -> 
 	      if mode.eager_eval
 	      then interp_main mode t_level (union_env env l_env) lm exp
-	      else debug_out exp t_level lm (union_env env l_env)
+	      else debug_out Nothing Nothing exp t_level lm (union_env env l_env)
 	    | multi_matches ->
 	      let lets = List.map (fun (env,_,exp) -> env_to_let mode env exp) multi_matches in
 	      interp_main mode t_level l_env lm (E_aux (E_block lets) (l,annot))
@@ -1610,7 +1644,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 		  resolve_outcome 
                     (if mode.eager_eval 
 		     then (interp_main mode t_level env emem exp)
-		     else (debug_out exp t_level emem env))  
+		     else (debug_out (Just name) (Just v) exp t_level emem env))  
 	            (fun ret lm le -> (Value ret, l_mem,l_env))
                     (fun a -> update_stack a 
 		      (fun stack -> (Hole_frame (id_of_string "0") 
@@ -1631,7 +1665,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 	      resolve_outcome 
                 (if mode.eager_eval 
 		 then (interp_main mode t_level env emem exp)
-		 else (debug_out exp t_level emem env))  
+		 else (debug_out (Just name) (Just v) exp t_level emem env))  
 	        (fun ret lm le -> (Value ret, l_mem,l_env))
                 (fun a -> update_stack a 
 		  (fun stack -> (Hole_frame (id_of_string "0") 
@@ -1649,7 +1683,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
               resolve_outcome 
 		(if mode.eager_eval 
 		 then (interp_main mode t_level env emem exp)
-                 else (debug_out exp t_level emem env))
+                 else (debug_out (Just name) (Just v) exp t_level emem env))
 	        (fun ret lm le -> (Value ret, l_mem,l_env))
                 (fun a -> update_stack a 
 		  (fun stack -> 
@@ -1708,7 +1742,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 			  resolve_outcome 
 			    (if mode.eager_eval
 			     then (interp_main mode t_level env emem exp)
-			     else (debug_out exp t_level emem env)) 
+			     else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level emem env)) 
 			    (fun ret lm le -> (Value ret,l_mem,l_env))
                             (fun a -> update_stack a 
 			      (fun stack -> 
@@ -1725,7 +1759,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 			  resolve_outcome 
 			    (if mode.eager_eval
 			     then (interp_main mode t_level env emem exp)
-			     else (debug_out exp t_level emem env)) 
+			     else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level emem env)) 
 			    (fun ret lm le -> (Value ret,l_mem,l_env))
                             (fun a -> update_stack a 
 			      (fun stack -> (Hole_frame (Id_aux (Id "0") l)
@@ -1741,7 +1775,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 			  resolve_outcome 
 			    (if mode.eager_eval 
 			     then (interp_main mode t_level env emem exp)
-			     else (debug_out exp t_level emem env))
+			     else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level emem env))
 			    (fun ret lm le -> (Value ret,l_mem,l_env))
                             (fun a -> update_stack a 
 			      (fun stack -> (Hole_frame (Id_aux (Id "0") l)
@@ -1764,7 +1798,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
     | ((Value v,lm,le),_) ->
       if mode.eager_eval
       then interp_main mode t_level le lm exp
-      else debug_out exp t_level lm le                                           
+      else debug_out Nothing Nothing exp t_level lm le                                           
     | (((Action a s as o),lm,le),Just lbuild) ->  
       ((update_stack o (add_to_top_frame (fun e env -> (E_aux (E_let (lbuild e) exp) (l,annot), env)))),lm,le)
     | (e,_) -> e end
@@ -1797,13 +1831,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
     | [ exp ] -> 
       if mode.eager_eval
       then interp_main mode t_level local_env local_mem exp
-      else debug_out exp t_level local_mem local_env
+      else debug_out Nothing Nothing exp t_level local_mem local_env
     | exp:: exps ->
       resolve_outcome (interp_main mode t_level local_env local_mem exp)
                       (fun _ lm le -> 
 			if mode.eager_eval
 			then interp_block mode t_level init_env le lm l tannot exps
-			else debug_out (E_aux (E_block exps) (l,tannot)) t_level lm le)
+			else debug_out Nothing Nothing (E_aux (E_block exps) (l,tannot)) t_level lm le)
                       (fun a -> update_stack a (add_to_top_frame (fun e env-> (E_aux (E_block(e::exps)) (l,tannot), env))))
     end
 
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 9c706828..bc9610de 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -127,8 +127,18 @@ let rec interp_to_outcome mode thunk =
     | Interp.Call_extern i value -> 
       match List.lookup i external_functions with
       | Nothing -> Error ("External function not available " ^ i)
-      | Just f  -> interp_to_outcome mode (fun _ -> Interp.resume mode next_state (Just (f value))) end
-    | Interp.Step l _ _ -> Internal (fun _ -> "Function state to string not implemented yet") next_state 
+      | Just f  -> 
+        if (mode.Interp.eager_eval)
+        then interp_to_outcome mode (fun _ -> Interp.resume mode next_state (Just (f value))) 
+        else let new_v = f value in
+             Internal (Just i) 
+                      (Just (fun _ -> Interp.string_of_value value))
+                      (Interp.add_answer_to_stack next_state new_v)
+      end
+    | Interp.Step l Nothing Nothing -> Internal Nothing Nothing next_state 
+    | Interp.Step l (Just name) Nothing -> Internal (Just name) Nothing next_state
+    | Interp.Step l (Just name) (Just value) ->
+      Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) next_state
     end 
   end 
 
@@ -146,7 +156,7 @@ let rec ie_loop mode i_state =
       (E_read_mem read_k loc length tracking)::(ie_loop mode (i_state_fun Unknown))
     | Write_mem write_k loc length l_track value v_track i_state_fun ->
       (E_write_mem write_k loc length l_track value v_track)::(ie_loop mode (i_state_fun true))
-    | Internal _ next -> (ie_loop mode next)
+    | Internal _ _ next -> (ie_loop mode next)
      end ;;
   
 let interp_exhaustive i_state = 
@@ -167,7 +177,7 @@ let rec rr_ie_loop mode i_state =
     | Write_mem write_k loc length l_track value v_track i_state_fun ->
       let (events,outcome) = (rr_ie_loop mode (i_state_fun true)) in
       (((E_write_mem write_k loc length l_track value v_track)::events),outcome)
-    | Internal _ next -> (rr_ie_loop mode next)
+    | Internal _ _ next -> (rr_ie_loop mode next)
      end ;;
 
 let rr_interp_exhaustive mode i_state events = 
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 684257f6..d49edfd5 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -48,7 +48,7 @@ type outcome =
 (* List of instruciton states to be run in parrallel, any order permitted *)
 | Nondet_choice of list instruction_state * instruction_state
 (* Stop for incremental stepping, function can be used to display function call data *)
-| Internal of (unit -> string) * instruction_state
+| Internal of maybe string * maybe (unit -> string) * instruction_state
 | Done
 | Error of string
 
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 17ef81a9..9921d9f4 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -448,10 +448,15 @@ let run
 	| Barrier0(bkind,next) ->
 	  show "mem_barrier" "" "" "";
 	  (step next, env, next)
-	| Internal(msg, next) ->
+	| Internal(None,None, next) ->
           show "breakpoint" "" "" "";
-	  show (msg ()) "" "" "";
           (step ~force:true next,env',next)
+        | Internal((Some fn),None,next) ->
+          show "breakpoint" fn "" "";
+          (step ~force:true next, env',next)
+        | Internal((Some fn),(Some vdisp),next) ->
+          show "breakpoint" (fn ^ " " ^ (vdisp ())) "" "";
+          (step ~force:true next, env', next)
 	| Nondet_choice(nondets, next) ->
 	  let choose_order = List.sort (fun (_,i1) (_,i2) -> compare i1 i2) 
 	    (List.combine nondets (List.map (fun _ -> Random.bits ()) nondets)) in