Allow stepping through code when evaluating

3 files changed, 136 insertions, 42 deletions

diff --git a/Makefile b/Makefile
index 22d51315..b84e0d22 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
 .PHONY: all sail language clean archs isabelle-lib apply_header
 
-all: sail interpreter
+all: sail
 
 sail:
 	$(MAKE) -C src
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 55fb7b32..1a6e6393 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -287,24 +287,27 @@ let rec get_fundef id (Defs defs) =
   | (DEF_fundef fdef) :: _ when Id.compare id (id_of_fundef fdef) = 0 -> fdef
   | _ :: defs -> get_fundef id (Defs defs)
 
+let rec untilM p f x =
+  if p x then
+    return x
+  else
+    f (return x) >>= fun x' -> untilM p f x'
+
+type trace =
+  | Done of value
+  | Step of (Type_check.tannot exp) monad * (value -> (Type_check.tannot exp) monad) list
+
 let rec eval_exp ast m =
   match m with
-  | Pure v when is_value v -> value_of_exp v
+  | Pure v when is_value v -> Done (value_of_exp v)
   | Pure exp' ->
      Pretty_print_sail2.pretty_sail stdout (Pretty_print_sail2.doc_exp exp');
      print_newline ();
-     eval_exp ast (step exp')
+     Step (step exp', [])
   | Yield (Call (id, vals, cont)) ->
      print_endline ("Calling " ^ string_of_id id |> Util.cyan |> Util.clear);
      let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in
      let body = exp_of_fundef (get_fundef id ast) arg in
-     let v = eval_exp ast (return body) in
-     eval_exp ast (cont v)
+     Step (return body, [cont])
   | _ -> assert false
 
-let rec run_interpreter ast env =
-  let str = read_line () in
-  let exp = Type_check.infer_exp env (Initial_check.exp_of_string Ast_util.dec_ord str) in
-  let v = eval_exp ast (step exp) in
-  print_endline ("Result = " ^ string_of_value v);
-  run_interpreter ast env;
diff --git a/src/isail.ml b/src/isail.ml
index 5a225174..e1860451 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -1,15 +1,83 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
 open Sail
 
 open Ast
 open Ast_util
+open Interpreter
 open Pretty_print_sail2
 
-let rec user_input prompt callback =
-  match LNoise.linenoise prompt with
+type mode =
+  | Evaluation of trace
+  | Normal
+
+let current_mode = ref Normal
+
+let prompt () =
+  match !current_mode with
+  | Normal -> "sail> "
+  | Evaluation _ -> "eval> "
+
+let mode_clear () =
+  match !current_mode with
+  | Normal -> ()
+  | Evaluation _ -> LNoise.clear_screen ()
+
+let rec user_input callback =
+  match LNoise.linenoise (prompt ()) with
   | None -> ()
-  | Some v -> 
+  | Some v ->
+     mode_clear ();
      callback v;
-     user_input prompt callback
+     user_input callback
 
 let termcode n = "\x1B[" ^ string_of_int n ^ "m"
 let bold str = termcode 1 ^ str
@@ -32,32 +100,55 @@ let sail_logo =
 let vs_ids = ref (Initial_check.val_spec_ids !interactive_ast)
 
 let handle_input input =
-  LNoise.history_add input |> ignore;
-
-  if input <> "" && input.[0] = ':' then
-    let n = try String.index input ' ' with Not_found -> String.length input in
-    let cmd = Str.string_before input n in
-    let arg = String.trim (Str.string_after input n) in
-    match cmd with
-    | ":t" | ":type" ->
-       let typq, typ = Type_check.Env.get_val_spec (mk_id arg) !interactive_env in
-       pretty_sail stdout (doc_binding (typq, typ));
-       print_newline ();
-    | ":q" | ":quit" ->
-       exit 0
-    | ":i" | ":infer" ->
-       let exp = Initial_check.exp_of_string dec_ord arg in
-       let exp = Type_check.infer_exp !interactive_env exp in
-       pretty_sail stdout (doc_typ (Type_check.typ_of exp));
-       print_newline ()
-    | ":v" | ":verbose" ->
-       Type_check.opt_tc_debug := (!Type_check.opt_tc_debug + 1) mod 2
-
-    | _ -> print_endline ("Unrecognised command " ^ input)
-  else
-    let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord input) in
-    let v = Interpreter.eval_exp !interactive_ast (Interpreter.step exp) in
-    print_endline ("Result = " ^ Value.string_of_value v)
+  match !current_mode with
+  | Normal ->
+     begin
+       LNoise.history_add input |> ignore;
+
+       if input <> "" && input.[0] = ':' then
+         let n = try String.index input ' ' with Not_found -> String.length input in
+         let cmd = Str.string_before input n in
+         let arg = String.trim (Str.string_after input n) in
+         match cmd with
+         | ":t" | ":type" ->
+            let typq, typ = Type_check.Env.get_val_spec (mk_id arg) !interactive_env in
+            pretty_sail stdout (doc_binding (typq, typ));
+            print_newline ();
+         | ":q" | ":quit" ->
+            exit 0
+         | ":i" | ":infer" ->
+            let exp = Initial_check.exp_of_string dec_ord arg in
+            let exp = Type_check.infer_exp !interactive_env exp in
+            pretty_sail stdout (doc_typ (Type_check.typ_of exp));
+            print_newline ()
+         | ":v" | ":verbose" ->
+            Type_check.opt_tc_debug := (!Type_check.opt_tc_debug + 1) mod 2
+
+         | _ -> print_endline ("Unrecognised command " ^ input)
+       else if input <> "" then
+         let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord input) in
+         current_mode := Evaluation (eval_exp !interactive_ast (return exp))
+       else ()
+     end
+  | Evaluation trace ->
+     begin
+       match trace with
+       | Done v ->
+          print_endline ("Result = " ^ Value.string_of_value v);
+          current_mode := Normal
+       | Step (exp, stack) ->
+          let next = match eval_exp !interactive_ast exp with
+            | Step (exp', stack') -> Evaluation (Step (exp', stack' @ stack))
+            | Done v when stack = [] ->
+               print_endline ("Result = " ^ Value.string_of_value v);
+               Normal
+            | Done v ->
+               print_endline ("Returning: " ^ Value.string_of_value v |> Util.cyan |> Util.clear);
+               Evaluation (Step (List.hd stack v, List.tl stack))
+          in
+          current_mode := next
+     end
+
 
 
 let () =
@@ -88,5 +179,5 @@ let () =
   LNoise.history_set ~max_length:100 |> ignore;
 
   if !opt_interactive then
-    user_input "sail> " handle_input
+    user_input handle_input
   else ()