Add help to interactive mode, and load files incrementally

4 files changed, 107 insertions, 41 deletions

diff --git a/src/isail.ml b/src/isail.ml
index 3009aeb3..a0e45e45 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -66,10 +66,12 @@ let prompt () =
   | Normal -> "sail> "
   | Evaluation _ -> "eval> "
 
+let eval_clear = ref true
+
 let mode_clear () =
   match !current_mode with
   | Normal -> ()
-  | Evaluation _ -> LNoise.clear_screen ()
+  | Evaluation _ -> if !eval_clear then LNoise.clear_screen () else ()
 
 let rec user_input callback =
   match LNoise.linenoise (prompt ()) with
@@ -84,16 +86,20 @@ let rec user_input callback =
 
 let sail_logo =
   let banner str = str |> Util.bold |> Util.red |> Util.clear in
-  [ {|    ___       ___       ___       ___ |};
-    {|   /\  \     /\  \     /\  \     /\__\|};
-    {|  /::\  \   /::\  \   _\:\  \   /:/  /|};
-    {| /\:\:\__\ /::\:\__\ /\/::\__\ /:/__/ |};
-    {| \:\:\/__/ \/\::/  / \::/\/__/ \:\  \ |};
-    {|  \::/  /    /:/  /   \:\__\    \:\__\|};
-    {|   \/__/     \/__/     \/__/     \/__/|};
-    ""
-  ]
-  |> List.map banner
+  let logo =
+    [ {|    ___       ___       ___       ___ |};
+      {|   /\  \     /\  \     /\  \     /\__\|};
+      {|  /::\  \   /::\  \   _\:\  \   /:/  /|};
+      {| /\:\:\__\ /::\:\__\ /\/::\__\ /:/__/ |};
+      {| \:\:\/__/ \/\::/  / \::/\/__/ \:\  \ |};
+      {|  \::/  /    /:/  /   \:\__\    \:\__\|};
+      {|   \/__/     \/__/     \/__/     \/__/|} ]
+  in
+  let help =
+    [ "Type :commands for a list of commands, and :help <command> for help.";
+      "Type expressions to evaluate them." ]
+  in
+  List.map banner logo @ [""] @ help @ [""]
 
 let vs_ids = ref (Initial_check.val_spec_ids !interactive_ast)
 
@@ -145,6 +151,37 @@ let rec run_steps n =
           current_mode := Evaluation frame
      end
 
+let help = function
+  | ":t" | ":type" ->
+     "(:t | :type) <function name> - Print the type of a function."
+  | ":q" | ":quit" ->
+     "(:q | :quit) - Exit the interpreter."
+  | ":i" | ":infer" ->
+     "(:i | :infer) <expression> - Infer the type of an expression."
+  | ":v" | ":verbose" ->
+     "(:v | :verbose) - Increase the verbosity level, or reset to zero at max verbosity."
+  | ":commands" ->
+     ":commands - List all available commands."
+  | ":help" ->
+     ":help <command> - Get a description of <command>. Commands are prefixed with a colon, e.g. :help :type."
+  | ":elf" ->
+     ":elf <file> - Load an ELF file."
+  | ":r" | ":run" ->
+     "(:r | :run) - Completely evaluate the currently evaluating expression."
+  | ":s" | ":step" ->
+     "(:s | :step) <number> - Perform a number of evaluation steps."
+  | ":n" | ":normal" ->
+     "(:n | :normal) - Exit evaluation mode back to normal mode."
+  | ":clear" ->
+     ":clear (on|off) - Set whether to clear the screen or not in evaluation mode."
+  | ":l" | ":load" -> String.concat "\n"
+     [ "(:l | :load) <files> - Load sail files and add their definitions to the interactive environment.";
+       "Files containing scattered definitions must be loaded together." ]
+  | cmd ->
+     "Either invalid command passed to help, or no documentation for " ^ cmd ^ ". Try :help :help."
+
+let append_ast (Defs ast1) (Defs ast2) = Defs (ast1 @ ast2)
+
 type input = Command of string * string | Expression of string | Empty
 
 (* This function is called on every line of input passed to the interpreter *)
@@ -168,7 +205,7 @@ let handle_input' input =
   let recognised = ref true in
 
   let unrecognised_command cmd =
-    if !recognised = false then print_endline ("Command " ^ cmd ^ " is not a valid command") else ()
+    if !recognised = false then print_endline ("Command " ^ cmd ^ " is not a valid command in this mode.") else ()
   in
 
   (* First handle commands that are mode-independent *)
@@ -190,6 +227,20 @@ let handle_input' input =
          | ":v" | ":verbose" ->
             Type_check.opt_tc_debug := (!Type_check.opt_tc_debug + 1) mod 3;
             print_endline ("Verbosity: " ^ string_of_int !Type_check.opt_tc_debug)
+         | ":clear" ->
+            if arg = "on" then
+              eval_clear := true
+            else if arg = "off" then
+              eval_clear := false
+            else print_endline "Invalid argument for :clear, expected either :clear on or :clear off"
+         | ":commands" ->
+            let commands =
+              [ "Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :clear :commands :help";
+                "Normal mode commands - :elf :(l)oad";
+                "Evaluation mode commands - :(r)un :(s)tep :(n)ormal" ]
+            in
+            List.iter print_endline commands
+         | ":help" -> print_endline (help arg)
          | _ -> recognised := false
        end
     | _ -> ()
@@ -204,6 +255,14 @@ let handle_input' input =
           begin
             match cmd with
             | ":elf" -> Elf_loader.load_elf arg
+            | ":l" | ":load" ->
+               let files = Util.split_on_char ' ' arg in
+               let (_, ast, env) = load_files !interactive_env files in
+               let ast = Process_file.rewrite_ast_interpreter ast in
+               interactive_ast := append_ast !interactive_ast ast;
+               interactive_state := initial_state !interactive_ast;
+               interactive_env := env;
+               vs_ids := Initial_check.val_spec_ids !interactive_ast
             | _ -> unrecognised_command cmd
           end
        | Expression str ->
@@ -254,6 +313,8 @@ let handle_input input =
   try handle_input' input with
   | Type_check.Type_error (l, err) ->
      print_endline (Type_check.string_of_type_error err)
+  | Reporting_basic.Fatal_error err ->
+     Reporting_basic.print_error err
   | exn ->
      print_endline (Printexc.to_string exn)
 
diff --git a/src/process_file.ml b/src/process_file.ml
index 435beb3c..b3c231fe 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -89,9 +89,9 @@ let opt_ddump_tc_ast = ref false
 let opt_ddump_rewrite_ast = ref None
 let opt_dno_cast = ref false
 
-let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t =
-  let ienv = if !opt_dno_cast then Type_check.Env.no_casts Type_check.initial_env else Type_check.initial_env in
-  let ast, env = Type_check.check ienv defs in
+let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t =
+  let env = if !opt_dno_cast then Type_check.Env.no_casts env else env in
+  let ast, env = Type_check.check env defs in
   let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_defs stdout ast else () in
   let () = if !opt_just_check then exit 0 else () in
   (ast, env)
diff --git a/src/process_file.mli b/src/process_file.mli
index bc8936c8..024a8239 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -50,7 +50,7 @@
 
 val parse_file : string -> Parse_ast.defs
 val convert_ast : Ast.order -> Parse_ast.defs -> unit Ast.defs
-val check_ast: unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
+val check_ast: Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
 val monomorphise_ast : ((string * int) * string) list -> Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
 val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
 val rewrite_undefined: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
diff --git a/src/sail.ml b/src/sail.ml
index c8f30e09..774c7d8f 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -180,37 +180,42 @@ let _ =
 let interactive_ast = ref (Ast.Defs [])
 let interactive_env = ref Type_check.initial_env
 
-let main() =
-  if !opt_print_version
-  then Printf.printf "Sail private release \n"
-  else
-    if !opt_memo_z3 then Constraint.load_digests () else ();
+let load_files type_envs files =
+  if !opt_memo_z3 then Constraint.load_digests () else ();
+
+  let parsed = List.map (fun f -> (f, parse_file f)) files in
+  let ast =
+    List.fold_right (fun (_, Parse_ast.Defs ast_nodes) (Parse_ast.Defs later_nodes)
+                     -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
+  let ast = convert_ast Ast_util.inc_ord ast in
 
-    let parsed = (List.map (fun f -> (f,(parse_file f)))  !opt_file_arguments) in
-    let ast =
-      List.fold_right (fun (_,(Parse_ast.Defs ast_nodes)) (Parse_ast.Defs later_nodes) 
-                        -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
-    let ast = convert_ast Ast_util.inc_ord ast in
+  let (ast, type_envs) = check_ast type_envs ast in
 
-    let (ast, type_envs) = check_ast ast in
+  let (ast, type_envs) =
+    match !opt_mono_split, !opt_auto_mono with
+    | [], false -> ast, type_envs
+    | locs, _ -> monomorphise_ast locs type_envs ast
+  in
 
-    let (ast, type_envs) =
-      match !opt_mono_split, !opt_auto_mono with
-      | [], false -> ast, type_envs
-      | locs, _ -> monomorphise_ast locs type_envs ast
-    in
+  let ast =
+    if !Initial_check.opt_undefined_gen then
+      rewrite_undefined (rewrite_ast ast)
+    else rewrite_ast ast in
 
-    let ast =
-      if !Initial_check.opt_undefined_gen then
-        rewrite_undefined (rewrite_ast ast)
-      else rewrite_ast ast in
+  let out_name = match !opt_file_out with
+    | None when parsed = [] -> "out.sail"
+    | None -> fst (List.hd parsed)
+    | Some f -> f ^ ".sail" in
 
-    let out_name = match !opt_file_out with
-      | None when parsed = [] -> "out.sail"
-      | None -> fst (List.hd parsed)
-      | Some f -> f ^ ".sail" in
+  if !opt_memo_z3 then Constraint.save_digests () else ();
 
-    if !opt_memo_z3 then Constraint.save_digests () else ();
+  (out_name, ast, type_envs)
+
+let main() =
+  if !opt_print_version
+  then Printf.printf "Sail private release \n"
+  else
+    let out_name, ast, type_envs = load_files Type_check.initial_env !opt_file_arguments in
 
     (*let _ = Printf.eprintf "Type checked, next to pretty print" in*)
     begin