Merge branch 'sail2' into mono-tweaks

1 files changed, 126 insertions, 61 deletions

diff --git a/src/isail.ml b/src/isail.ml
index 02908321..dc7858c9 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -113,7 +113,8 @@ let sep = "-----------------------------------------------------" |> Util.blue |
 
 let vs_ids = ref (val_spec_ids !Interactive.ast)
 
-let interactive_state = ref (initial_state ~registers:false !Interactive.ast !Interactive.env !Value.primops)
+let interactive_state =
+  ref (initial_state ~registers:false !Interactive.ast !Interactive.env !Value.primops)
 
 (* We can't set up the elf commands in elf_loader.ml because it's used
    by Sail OCaml emulators at runtime, so set them up here. *)
@@ -192,34 +193,75 @@ let rec run () =
   match !current_mode with
   | Normal | Emacs -> ()
   | Evaluation frame ->
-     begin
-       match frame with
-       | Done (state, v) ->
-          interactive_state := state;
-          print_endline ("Result = " ^ Value.string_of_value v);
-          current_mode := Normal
-       | Fail (_, _, _, _, msg) ->
-          print_endline ("Error: " ^ msg);
-          current_mode := Normal
-       | Step (out, state, _, stack) ->
-          begin
-            try
-              current_mode := Evaluation (eval_frame frame)
-            with
-            | Failure str -> print_endline str; current_mode := Normal
-          end;
-          run ()
-       | Break frame ->
-          print_endline "Breakpoint";
-          current_mode := Evaluation frame
-       | Effect_request (out, state, stack, eff) ->
-          begin
-            try
-              current_mode := Evaluation (!Interpreter.effect_interp state eff)
-            with
-            | Failure str -> print_endline str; current_mode := Normal
-          end;
-          run ()
+     begin match frame with
+     | Done (state, v) ->
+        interactive_state := state;
+        print_endline ("Result = " ^ Value.string_of_value v);
+        current_mode := Normal
+     | Fail (_, _, _, _, msg) ->
+        print_endline ("Error: " ^ msg);
+        current_mode := Normal
+     | Step (out, state, _, stack) ->
+        begin
+          try
+            current_mode := Evaluation (eval_frame frame)
+          with
+          | Failure str -> print_endline str; current_mode := Normal
+        end;
+        run ()
+     | Break frame ->
+        print_endline "Breakpoint";
+        current_mode := Evaluation frame
+     | Effect_request (out, state, stack, eff) ->
+        begin
+          try
+            current_mode := Evaluation (!Interpreter.effect_interp state eff)
+          with
+          | Failure str -> print_endline str; current_mode := Normal
+        end;
+        run ()
+     end
+
+let rec run_function depth =
+  let run_function' stack =
+    match depth with
+    | None -> run_function (Some (List.length stack))
+    | Some n ->
+       if List.compare_length_with stack n >= 0 then
+         run_function depth
+       else
+         ()
+  in
+  match !current_mode with
+  | Normal | Emacs -> ()
+  | Evaluation frame ->
+     begin match frame with
+     | Done (state, v) ->
+        interactive_state := state;
+        print_endline ("Result = " ^ Value.string_of_value v);
+        current_mode := Normal
+     | Fail (_, _, _, _, msg) ->
+        print_endline ("Error: " ^ msg);
+        current_mode := Normal
+     | Step (out, state, _, stack) ->
+        begin
+          try
+            current_mode := Evaluation (eval_frame frame)
+          with
+          | Failure str -> print_endline str; current_mode := Normal
+        end;
+        run_function' stack
+     | Break frame ->
+        print_endline "Breakpoint";
+        current_mode := Evaluation frame
+     | Effect_request (out, state, stack, eff) ->
+        begin
+          try
+            current_mode := Evaluation (!Interpreter.effect_interp state eff)
+          with
+          | Failure str -> print_endline str; current_mode := Normal
+        end;
+        run_function' stack
      end
 
 let rec run_steps n =
@@ -227,36 +269,35 @@ let rec run_steps n =
   | _ when n <= 0 -> ()
   | Normal | Emacs -> ()
   | Evaluation frame ->
-     begin
-       match frame with
-       | Done (state, v) ->
-          interactive_state := state;
-          print_endline ("Result = " ^ Value.string_of_value v);
-          current_mode := Normal
-       | Fail (_, _, _, _, msg) ->
-          print_endline ("Error: " ^ msg);
-          current_mode := Normal
-       | Step (out, state, _, stack) ->
-          begin
-            try
-              current_mode := Evaluation (eval_frame frame)
-            with
-            | Failure str -> print_endline str; current_mode := Normal
-          end;
-          run_steps (n - 1)
-       | Break frame ->
-          print_endline "Breakpoint";
-          current_mode := Evaluation frame
-       | Effect_request (out, state, stack, eff) ->
-          begin
-            try
-              current_mode := Evaluation (!Interpreter.effect_interp state eff)
-            with
-            | Failure str -> print_endline str; current_mode := Normal
-          end;
-          run_steps (n - 1)
+     begin match frame with
+     | Done (state, v) ->
+        interactive_state := state;
+        print_endline ("Result = " ^ Value.string_of_value v);
+        current_mode := Normal
+     | Fail (_, _, _, _, msg) ->
+        print_endline ("Error: " ^ msg);
+        current_mode := Normal
+     | Step (out, state, _, stack) ->
+        begin
+          try
+            current_mode := Evaluation (eval_frame frame)
+          with
+          | Failure str -> print_endline str; current_mode := Normal
+        end;
+        run_steps (n - 1)
+     | Break frame ->
+        print_endline "Breakpoint";
+        current_mode := Evaluation frame
+     | Effect_request (out, state, stack, eff) ->
+        begin
+          try
+            current_mode := Evaluation (!Interpreter.effect_interp state eff)
+          with
+          | Failure str -> print_endline str; current_mode := Normal
+        end;
+        run_steps (n - 1)
      end
-
+ 
 let help =
   let open Printf in
   let open Util in
@@ -297,6 +338,8 @@ let help =
   | ":s" | ":step" ->
      sprintf "(:s | :step) %s - Perform a number of evaluation steps."
              (color yellow "<number>")
+  | ":f" | ":step_function" ->
+     sprintf "(:s | :step) - Perform evaluation steps until the currently evaulating function returns."
   | ":n" | ":normal" ->
      "(:n | :normal) - Exit evaluation mode back to normal mode."
   | ":clear" ->
@@ -314,6 +357,8 @@ let help =
   | ":option" ->
      sprintf ":option %s - Parse string as if it was an option passed on the command line. e.g. :option -help."
              (color yellow "<string>")
+  | ":recheck" ->
+     sprintf ":recheck - Re type-check the Sail AST, and synchronize the interpreters internal state to that AST."
   | ":rewrite" ->
      sprintf ":rewrite %s - Apply a rewrite to the AST. %s shows all possible rewrites. See also %s"
              (color yellow "<rewrite> <args>") (color green ":list_rewrites") (color green ":rewrites")
@@ -419,6 +464,9 @@ let handle_input' input =
       let cmd = Str.string_before input n in
       let arg = String.trim (Str.string_after input n) in
       Command (cmd, arg)
+    else if String.length input >= 2 && input.[0] = '/' && input.[1] = '/' then
+      (* Treat anything starting with // as a comment *)
+      Empty
     else if input <> "" then
       Expression input
     else
@@ -468,7 +516,7 @@ let handle_input' input =
         let more_commands = Util.string_of_list " " fst !Interactive.commands in
         let commands =
           [ "Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :prove :assume :clear :commands :help :output :option";
-            "Normal mode commands - :elf :(l)oad :(u)nload :let :def :(b)ind :rewrite :rewrites :list_rewrites :compile " ^ more_commands;
+            "Normal mode commands - :elf :(l)oad :(u)nload :let :def :(b)ind :recheck :rewrite :rewrites :list_rewrites :compile " ^ more_commands;
             "Evaluation mode commands - :(r)un :(s)tep :(n)ormal";
             "";
             ":(c)ommand can be called as either :c or :command." ]
@@ -510,9 +558,15 @@ let handle_input' input =
         | ":l" | ":load" ->
            let files = Util.split_on_char ' ' arg in
            let (_, ast, env) = Process_file.load_files options !Interactive.env files in
+           let ast, env =
+             if !Interactive.opt_auto_interpreter_rewrites then
+               Process_file.rewrite_ast_target "interpreter" env ast
+             else
+               ast, env
+           in
            Interactive.ast := append_ast !Interactive.ast ast;
-           interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops;
            Interactive.env := env;
+           interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops;
            vs_ids := val_spec_ids !Interactive.ast
         | ":u" | ":unload" ->
            Interactive.ast := Ast.Defs [];
@@ -684,7 +738,11 @@ let handle_input' input =
           | ":r" | ":run" ->
              run ()
           | ":s" | ":step" ->
-             run_steps (int_of_string arg)
+             run_steps (int_of_string arg);
+             print_program ()
+          | ":f" | ":step_function" ->
+             run_function None;
+             print_program ()
           | _ -> unrecognised_command cmd
         end
      | Expression str ->
@@ -819,6 +877,13 @@ let () =
          | _ -> None
     );
 
+  if !Interactive.opt_auto_interpreter_rewrites then (
+    let new_ast, new_env = Process_file.rewrite_ast_target "interpreter" !Interactive.env !Interactive.ast in
+    Interactive.ast := new_ast;
+    Interactive.env := new_env;
+    interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops
+  );
+  
   (* Read the script file if it is set with the -is option, and excute them *)
   begin match !opt_interactive_script with
   | None -> ()