Merge remote-tracking branch 'origin/asl_flow2' into sail2

1 files changed, 270 insertions, 148 deletions

diff --git a/src/isail.ml b/src/isail.ml
index 18c59e0b..7d009791 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -59,6 +59,7 @@ type mode =
   | Evaluation of frame
   | Bytecode of Value2.vl Bytecode_interpreter.gstate * Value2.vl Bytecode_interpreter.stack
   | Normal
+  | Emacs
 
 let current_mode = ref Normal
 
@@ -67,6 +68,7 @@ let prompt () =
   | Normal -> "sail> "
   | Evaluation _ -> "eval> "
   | Bytecode _ -> "ir> "
+  | Emacs -> ""
 
 let eval_clear = ref true
 
@@ -75,6 +77,7 @@ let mode_clear () =
   | Normal -> ()
   | Evaluation _ -> if !eval_clear then LNoise.clear_screen () else ()
   | Bytecode _ -> () (* if !eval_clear then LNoise.clear_screen () else () *)
+  | Emacs -> ()
 
 let rec user_input callback =
   match LNoise.linenoise (prompt ()) with
@@ -83,20 +86,22 @@ let rec user_input callback =
      mode_clear ();
      begin
        try callback v with
-       | Reporting.Fatal_error e -> Reporting.report_error e
+       | Reporting.Fatal_error e -> Reporting.print_error e
      end;
      user_input callback
 
 let sail_logo =
   let banner str = str |> Util.bold |> Util.red |> Util.clear in
   let logo =
-    [ {|    ___       ___       ___       ___ |};
-      {|   /\  \     /\  \     /\  \     /\__\|};
-      {|  /::\  \   /::\  \   _\:\  \   /:/  /|};
-      {| /\:\:\__\ /::\:\__\ /\/::\__\ /:/__/ |};
-      {| \:\:\/__/ \/\::/  / \::/\/__/ \:\  \ |};
-      {|  \::/  /    /:/  /   \:\__\    \:\__\|};
-      {|   \/__/     \/__/     \/__/     \/__/|} ]
+    if !Interactive.opt_suppress_banner then []
+    else
+      [ {|    ___       ___       ___       ___ |};
+        {|   /\  \     /\  \     /\  \     /\__\|};
+        {|  /::\  \   /::\  \   _\:\  \   /:/  /|};
+        {| /\:\:\__\ /::\:\__\ /\/::\__\ /:/__/ |};
+        {| \:\:\/__/ \/\::/  / \::/\/__/ \:\  \ |};
+        {|  \::/  /    /:/  /   \:\__\    \:\__\|};
+        {|   \/__/     \/__/     \/__/     \/__/|} ]
   in
   let help =
     [ "Type :commands for a list of commands, and :help <command> for help.";
@@ -104,9 +109,9 @@ let sail_logo =
   in
   List.map banner logo @ [""] @ help @ [""]
 
-let vs_ids = ref (Initial_check.val_spec_ids !interactive_ast)
+let vs_ids = ref (Initial_check.val_spec_ids !Interactive.ast)
 
-let interactive_state = ref (initial_state !interactive_ast Value.primops)
+let interactive_state = ref (initial_state !Interactive.ast Value.primops)
 
 let interactive_bytecode = ref []
 
@@ -114,7 +119,7 @@ let sep = "-----------------------------------------------------" |> Util.blue |
 
 let print_program () =
   match !current_mode with
-  | Normal -> ()
+  | Normal | Emacs -> ()
   | Evaluation (Step (out, _, _, stack)) ->
      List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline (Lazy.force code); print_endline sep);
      print_endline (Lazy.force out)
@@ -140,7 +145,7 @@ let print_program () =
 
 let rec run () =
   match !current_mode with
-  | Normal -> ()
+  | Normal | Emacs -> ()
   | Evaluation frame ->
      begin
        match frame with
@@ -166,7 +171,7 @@ let rec run_steps n =
   print_endline ("step " ^ string_of_int n);
   match !current_mode with
   | _ when n <= 0 -> ()
-  | Normal -> ()
+  | Normal | Emacs -> ()
   | Evaluation frame ->
      begin
        match frame with
@@ -223,6 +228,65 @@ let help = function
   | cmd ->
      "Either invalid command passed to help, or no documentation for " ^ cmd ^ ". Try :help :help."
 
+let format_pos_emacs p1 p2 contents =
+  let open Lexing in
+  let b = Buffer.create 160 in
+  Printf.sprintf "(sail-error %d %d %d %d \"%s\")"
+                 p1.pos_lnum (p1.pos_cnum - p1.pos_bol)
+                 p2.pos_lnum (p2.pos_cnum - p2.pos_bol)
+                 contents
+
+let rec emacs_error l contents =
+  match l with
+  | Parse_ast.Unknown -> "(error \"no location info: " ^ contents ^ "\")"
+  | Parse_ast.Range (p1, p2) -> format_pos_emacs p1 p2 contents
+  | Parse_ast.Unique (_, l) -> emacs_error l contents
+  | Parse_ast.Documented (_, l) -> emacs_error l contents
+  | Parse_ast.Generated l -> emacs_error l contents
+
+type session = {
+    id : string;
+    files : string list
+  }
+
+let default_session = {
+    id = "none";
+    files = []
+  }
+
+let session = ref default_session
+
+let parse_session file =
+  let open Yojson.Basic.Util in
+  if Sys.file_exists file then
+    let json = Yojson.Basic.from_file file in
+    let args = Str.split (Str.regexp " +") (json |> member "options" |> to_string) in
+    Arg.parse_argv ~current:(ref 0) (Array.of_list ("sail" :: args)) Sail.options (fun _ -> ()) "";
+    print_endline ("(message \"Using session " ^ file ^ "\")");
+    {
+      id = file;
+      files = json |> member "files" |> convert_each to_string
+    }
+  else
+    default_session
+
+let load_session upto file =
+  match upto with
+  | None -> None
+  | Some upto_file when Filename.basename upto_file = file -> None
+  | Some upto_file ->
+     let (_, ast, env) =
+       load_files ~generate:false !Interactive.env [Filename.concat (Filename.dirname upto_file) file]
+     in
+     Interactive.ast := append_ast !Interactive.ast ast;
+     Interactive.env := env;
+     print_endline ("(message \"Checked " ^ file ^ "...\")\n");
+     Some upto_file
+
+let load_into_session file =
+  let session_file = Filename.concat (Filename.dirname file) "sail.json" in
+  session := (if session_file = !session.id then !session else parse_session session_file);
+  ignore (List.fold_left load_session (Some file) !session.files)
 
 type input = Command of string * string | Expression of string | Empty
 
@@ -251,146 +315,202 @@ let handle_input' input =
   in
 
   (* First handle commands that are mode-independent *)
-  begin
-    match input with
-    | Command (cmd, arg) ->
-       begin
-         match cmd with
-         | ":n" | ":normal" ->
-            current_mode := Normal
-         | ":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" ->
-            Value.output_close ();
-            exit 0
-         | ":i" | ":infer" ->
-            let exp = Initial_check.exp_of_string arg in
-            let exp = Type_check.infer_exp !interactive_env exp in
-            pretty_sail stdout (doc_typ (Type_check.typ_of exp));
-            print_newline ()
-         | ":canon" ->
-            let typ = Initial_check.typ_of_string arg in
-            print_endline (string_of_typ (Type_check.canonicalize !interactive_env typ))
-         | ":v" | ":verbose" ->
+  begin match input with
+  | Command (cmd, arg) ->
+     begin match cmd with
+     | ":n" | ":normal" ->
+        current_mode := Normal
+     | ":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" ->
+        Value.output_close ();
+        exit 0
+     | ":i" | ":infer" ->
+        let exp = Initial_check.exp_of_string arg in
+        let exp = Type_check.infer_exp !Interactive.env exp in
+        pretty_sail stdout (doc_typ (Type_check.typ_of exp));
+        print_newline ()
+     | ":canon" ->
+        let typ = Initial_check.typ_of_string arg in
+        print_endline (string_of_typ (Type_check.canonicalize !Interactive.env typ))
+     | ":prove" ->
+        let nc = Initial_check.constraint_of_string arg in
+        print_endline (string_of_bool (Type_check.prove __POS__ !Interactive.env nc))
+     | ":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 :output :option";
-                "Normal mode commands - :elf :(l)oad :(u)nload";
-                "Evaluation mode commands - :(r)un :(s)tep :(n)ormal";
-                "";
-                ":(c)ommand can be called as either :c or :command." ]
-            in
-            List.iter print_endline commands
-         | ":poly" ->
-            let is_kopt = match arg with
-              | "Int" -> is_nat_kopt
-              | "Type" -> is_typ_kopt
-              | "Order" -> is_order_kopt
-              | _ -> failwith "Invalid kind"
-            in
-            let ids = Specialize.polymorphic_functions is_kopt !interactive_ast in
-            List.iter (fun id -> print_endline (string_of_id id)) (IdSet.elements ids)
-         | ":option" ->
-            begin
-              try
-                let args = Str.split (Str.regexp " +") arg in
-                Arg.parse_argv ~current:(ref 0) (Array.of_list ("sail" :: args)) Sail.options (fun _ -> ()) "";
-              with
-              | Arg.Bad message | Arg.Help message -> print_endline message
-            end;
-         | ":spec" ->
-            let ast, env = Specialize.specialize !interactive_ast !interactive_env in
-            interactive_ast := ast;
-            interactive_env := env;
-            interactive_state := initial_state !interactive_ast Value.primops
-         | ":pretty" ->
-            print_endline (Pretty_print_sail.to_string (Latex.defs !interactive_ast))
-         | ":compile" ->
-            let open PPrint in
-            let open C_backend in
-            let ast = Process_file.rewrite_ast_c !interactive_ast in
-            let ast, env = Specialize.specialize ast !interactive_env in
-            let ctx = initial_ctx env in
-            interactive_bytecode := bytecode_ast ctx (List.map flatten_cdef) ast
-         | ":ir" ->
-            print_endline arg;
-            let open Bytecode in
-            let open Bytecode_util in
-            let open PPrint in
-            let is_cdef = function
-              | CDEF_fundef (id, _, _, _) when Id.compare id (mk_id arg) = 0 -> true
-              | CDEF_spec (id, _, _) when Id.compare id (mk_id arg) = 0 -> true
-              | _ -> false
-            in
-            let cdefs = List.filter is_cdef !interactive_bytecode in
-            print_endline (Pretty_print_sail.to_string (separate_map hardline pp_cdef cdefs))
-         | ":ast" ->
-            let chan = open_out arg in
-            Pretty_print_sail.pp_defs chan !interactive_ast;
-            close_out chan
-         | ":output" ->
-            let chan = open_out arg in
-            Value.output_redirect chan
-         | ":help" -> print_endline (help arg)
-         | _ -> recognised := false
-       end
-    | _ -> ()
+     | ":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 :output :option";
+            "Normal mode commands - :elf :(l)oad :(u)nload";
+            "Evaluation mode commands - :(r)un :(s)tep :(n)ormal";
+            "";
+            ":(c)ommand can be called as either :c or :command." ]
+        in
+        List.iter print_endline commands
+     | ":poly" ->
+        let is_kopt = match arg with
+          | "Int" -> is_nat_kopt
+          | "Type" -> is_typ_kopt
+          | "Order" -> is_order_kopt
+          | _ -> failwith "Invalid kind"
+        in
+        let ids = Specialize.polymorphic_functions is_kopt !Interactive.ast in
+        List.iter (fun id -> print_endline (string_of_id id)) (IdSet.elements ids)
+     | ":option" ->
+        begin
+          try
+            let args = Str.split (Str.regexp " +") arg in
+            Arg.parse_argv ~current:(ref 0) (Array.of_list ("sail" :: args)) Sail.options (fun _ -> ()) "";
+          with
+          | Arg.Bad message | Arg.Help message -> print_endline message
+        end;
+     | ":spec" ->
+        let ast, env = Specialize.specialize !Interactive.ast !Interactive.env in
+        Interactive.ast := ast;
+        Interactive.env := env;
+        interactive_state := initial_state !Interactive.ast Value.primops
+     | ":pretty" ->
+        print_endline (Pretty_print_sail.to_string (Latex.defs !Interactive.ast))
+     | ":compile" ->
+        let open PPrint in
+        let open C_backend in
+        let ast = Process_file.rewrite_ast_c !Interactive.env !Interactive.ast in
+        let ast, env = Specialize.specialize ast !Interactive.env in
+        let ctx = initial_ctx env in
+        interactive_bytecode := bytecode_ast ctx (List.map flatten_cdef) ast
+     | ":ir" ->
+        print_endline arg;
+        let open Bytecode in
+        let open Bytecode_util in
+        let open PPrint in
+        let is_cdef = function
+          | CDEF_fundef (id, _, _, _) when Id.compare id (mk_id arg) = 0 -> true
+          | CDEF_spec (id, _, _) when Id.compare id (mk_id arg) = 0 -> true
+          | _ -> false
+        in
+        let cdefs = List.filter is_cdef !interactive_bytecode in
+        print_endline (Pretty_print_sail.to_string (separate_map hardline pp_cdef cdefs))
+     | ":ast" ->
+        let chan = open_out arg in
+        Pretty_print_sail.pp_defs chan !Interactive.ast;
+        close_out chan
+     | ":output" ->
+        let chan = open_out arg in
+        Value.output_redirect chan
+     | ":help" -> print_endline (help arg)
+     | _ -> recognised := false
+     end
+  | _ -> ()
   end;
 
   match !current_mode with
   | Normal ->
-     begin
-       match input with
-       | Command (cmd, arg) ->
-          (* Normal mode commands *)
-          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 Value.primops;
-               interactive_env := env;
-               vs_ids := Initial_check.val_spec_ids !interactive_ast
-            | ":u" | ":unload" ->
-               interactive_ast := Ast.Defs [];
-               interactive_env := Type_check.initial_env;
-               interactive_state := initial_state !interactive_ast Value.primops;
-               vs_ids := Initial_check.val_spec_ids !interactive_ast;
-               (* See initial_check.mli for an explanation of why we need this. *)
-               Initial_check.have_undefined_builtins := false
-            | ":exec" ->
-               let open Bytecode_interpreter in
-               let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string arg) in
-               let anf = Anf.anf exp in
-               let ctx = C_backend.initial_ctx !interactive_env in
-               let ctyp = C_backend.ctyp_of_typ ctx (Type_check.typ_of exp) in
-               let setup, call, cleanup = C_backend.compile_aexp ctx anf in
-               let instrs = C_backend.flatten_instrs (setup @ [call (CL_id (mk_id "interactive#", ctyp))] @ cleanup) in
-               current_mode := Bytecode (new_gstate !interactive_bytecode, new_stack instrs);
-               print_program ()
-            | _ -> unrecognised_command cmd
-          end
-       | Expression str ->
-          (* An expression in normal mode is type checked, then puts
+     begin match input with
+     | Command (cmd, arg) ->
+        (* Normal mode commands *)
+        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 !Interactive.env ast in
+           Interactive.ast := append_ast !Interactive.ast ast;
+           interactive_state := initial_state !Interactive.ast Value.primops;
+           Interactive.env := env;
+           vs_ids := Initial_check.val_spec_ids !Interactive.ast
+        | ":u" | ":unload" ->
+           Interactive.ast := Ast.Defs [];
+           Interactive.env := Type_check.initial_env;
+           interactive_state := initial_state !Interactive.ast Value.primops;
+           vs_ids := Initial_check.val_spec_ids !Interactive.ast;
+           (* See initial_check.mli for an explanation of why we need this. *)
+           Initial_check.have_undefined_builtins := false;
+           Process_file.clear_symbols ()
+        | ":exec" ->
+           let open Bytecode_interpreter in
+           let exp = Type_check.infer_exp !Interactive.env (Initial_check.exp_of_string arg) in
+           let anf = Anf.anf exp in
+           let ctx = C_backend.initial_ctx !Interactive.env in
+           let ctyp = C_backend.ctyp_of_typ ctx (Type_check.typ_of exp) in
+           let setup, call, cleanup = C_backend.compile_aexp ctx anf in
+           let instrs = C_backend.flatten_instrs (setup @ [call (CL_id (mk_id "interactive#", ctyp))] @ cleanup) in
+           current_mode := Bytecode (new_gstate !interactive_bytecode, new_stack instrs);
+           print_program ()
+        | _ -> unrecognised_command cmd
+        end
+     | Expression str ->
+        (* An expression in normal mode is type checked, then puts
              us in evaluation mode. *)
-          let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string str) in
-          current_mode := Evaluation (eval_frame (Step (lazy "", !interactive_state, return exp, [])));
-          print_program ()
-       | Empty -> ()
+        let exp = Type_check.infer_exp !Interactive.env (Initial_check.exp_of_string str) in
+        current_mode := Evaluation (eval_frame (Step (lazy "", !interactive_state, return exp, [])));
+        print_program ()
+     | Empty -> ()
+     end
+
+  | Emacs ->
+     begin match input with
+     | Command (cmd, arg) ->
+        begin match cmd with
+        | ":load" ->
+           begin
+             try
+               load_into_session arg;
+               let (_, ast, env) = load_files !Interactive.env [arg] in
+               Interactive.ast := append_ast !Interactive.ast ast;
+               interactive_state := initial_state !Interactive.ast Value.primops;
+               Interactive.env := env;
+               vs_ids := Initial_check.val_spec_ids !Interactive.ast;
+               print_endline ("(message \"Checked " ^ arg ^ " done\")\n");
+             with
+             | Reporting.Fatal_error (Err_type (l, msg)) ->
+                print_endline (emacs_error l (String.escaped msg))
+           end
+        | ":unload" ->
+           Interactive.ast := Ast.Defs [];
+           Interactive.env := Type_check.initial_env;
+           interactive_state := initial_state !Interactive.ast Value.primops;
+           vs_ids := Initial_check.val_spec_ids !Interactive.ast;
+           Initial_check.have_undefined_builtins := false;
+           Process_file.clear_symbols ()
+        | ":typeat" ->
+           let args = Str.split (Str.regexp " +") arg in
+           begin match args with
+           | [file; pos] ->
+              let open Lexing in
+              let pos = int_of_string pos in
+              let pos = { dummy_pos with pos_fname = file; pos_cnum = pos - 1 } in
+              let sl = Some (pos, pos) in
+              begin match find_annot_ast sl !Interactive.ast with
+              | Some annot ->
+                 let msg = String.escaped (string_of_typ (Type_check.typ_of_annot annot)) in
+                 begin match simp_loc (fst annot) with
+                 | Some (p1, p2) ->
+                    print_endline ("(sail-highlight-region "
+                                   ^ string_of_int (p1.pos_cnum + 1) ^ " " ^ string_of_int (p2.pos_cnum + 1)
+                                   ^ " \"" ^ msg ^ "\")")
+                 | None ->
+                    print_endline ("(message \"" ^ msg ^ "\")")
+                 end
+              | None ->
+                 print_endline "(message \"No type here\")"
+              end
+           | _ ->
+              print_endline "(error \"Bad arguments for type at cursor\")"
+           end
+        | _ -> ()
+        end
+     | Expression _ | Empty -> ()
      end
+
   | Evaluation frame ->
      begin match input with
      | Command (cmd, arg) ->
@@ -441,7 +561,7 @@ let handle_input' input =
 
 let handle_input input =
   try handle_input' input with
-  | Type_check.Type_error (l, err) ->
+  | Type_check.Type_error (env, l, err) ->
      print_endline (Type_error.string_of_type_error err)
   | Reporting.Fatal_error err ->
      Reporting.print_error err
@@ -488,9 +608,11 @@ let () =
   LNoise.history_load ~filename:"sail_history" |> ignore;
   LNoise.history_set ~max_length:100 |> ignore;
 
-  if !opt_interactive then
+  if !Interactive.opt_interactive then
     begin
-      List.iter print_endline sail_logo;
+      if not !Interactive.opt_emacs_mode then
+        List.iter print_endline sail_logo
+      else (current_mode := Emacs; Util.opt_colors := false);
       user_input handle_input
     end
   else ()