(**************************************************************************)
(*     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_sail

type mode =
  | Evaluation of frame
  | Normal
  | Emacs

let current_mode = ref Normal

let prompt () =
  match !current_mode with
  | Normal -> "sail> "
  | Evaluation _ -> "eval> "
  | Emacs -> ""

let eval_clear = ref true

let mode_clear () =
  match !current_mode with
  | Normal -> ()
  | Evaluation _ -> if !eval_clear then LNoise.clear_screen () else ()
  | Emacs -> ()

let rec user_input callback =
  match LNoise.linenoise (prompt ()) with
  | None -> ()
  | Some v ->
     mode_clear ();
     begin
       try callback v with
       | 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.";
      "Type expressions to evaluate them." ]
  in
  List.map banner logo @ [""] @ help @ [""]

let vs_ids = ref (val_spec_ids !Interactive.ast)

let interactive_state = ref (initial_state !Interactive.ast !Interactive.env Value.primops)

let interactive_bytecode = ref []

let sep = "-----------------------------------------------------" |> Util.blue |> Util.clear

let print_program () =
  match !current_mode with
  | Normal | Emacs -> ()
  | Evaluation (Step (out, _, _, stack))
    | Evaluation (Effect_request(out, _, stack,  _))
    | Evaluation (Fail (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)
  | Evaluation (Done (_, v)) ->
     print_endline (Value.string_of_value v |> Util.green |> Util.clear)
  | Evaluation _ -> ()

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.default_effect_interp state eff)
            with
            | Failure str -> print_endline str; current_mode := Normal
          end;
          run ()
     end

let rec run_steps n =
  match !current_mode with
  | _ 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.default_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
  let color c str = str |> c |> clear in
  function
  | ":t" | ":type" ->
     sprintf "(:t | :type) %s - Print the type of a function."
             (color yellow "<function name>")
  | ":q" | ":quit" ->
     "(:q | :quit) - Exit the interpreter."
  | ":i" | ":infer" ->
     sprintf "(:i | :infer) %s - Infer the type of an expression."
             (color yellow "<expression>")
  | ":v" | ":verbose" ->
     "(:v | :verbose) - Increase the verbosity level, or reset to zero at max verbosity."
  | ":b" | ":bind" ->
     sprintf "(:b | :bind) %s : %s - Declare a variable of a specific type"
             (color yellow "<id>") (color yellow "<type>")
  | ":let" ->
     sprintf ":let %s = %s - Bind a variable to expression"
             (color yellow "<id>") (color yellow "<expression>")
  | ":def" ->
     sprintf ":def %s - Evaluate a top-level definition"
             (color yellow "<definition>")
  | ":prove" ->
     sprintf ":prove %s - Try to prove a constraint in the top-level environment"
             (color yellow "<constraint>")
  | ":assume" ->
     sprintf ":assume %s - Add a constraint to the top-level environment"
             (color yellow "<constraint>")
  | ":commands" ->
     ":commands - List all available commands."
  | ":help" ->
     sprintf ":help %s - Get a description of <command>. Commands are prefixed with a colon, e.g. %s."
             (color yellow "<command>") (color green ":help :type")
  | ":elf" ->
     sprintf ":elf %s - Load an ELF file."
       (color yellow "<file>")
  | ":bin" ->
     ":bin <address> <file> - Load a binary file at the given address."
  | ":r" | ":run" ->
     "(:r | :run) - Completely evaluate the currently evaluating expression."
  | ":s" | ":step" ->
     sprintf "(:s | :step) %s - Perform a number of evaluation steps."
             (color yellow "<number>")
  | ":n" | ":normal" ->
     "(:n | :normal) - Exit evaluation mode back to normal mode."
  | ":clear" ->
     sprintf ":clear %s - Set whether to clear the screen or not in evaluation mode."
             (color yellow "(on|off)")
  | ":l" | ":load" -> String.concat "\n"
     [ sprintf "(:l | :load) %s - Load sail files and add their definitions to the interactive environment."
               (color yellow "<files>");
       "Files containing scattered definitions must be loaded together." ]
  | ":u" | ":unload" ->
     "(:u | :unload) - Unload all loaded files."
  | ":output" ->
     sprintf ":output %s - Redirect evaluating expression output to a file."
             (color yellow "<file>")
  | ":option" ->
     sprintf ":option %s - Parse string as if it was an option passed on the command line. e.g. :option -help."
             (color yellow "<string>")
  | ":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")
  | ":rewrites" ->
     sprintf ":rewrites %s - Apply all rewrites for a specific target, valid targets are lem, coq, ocaml, c, and interpreter"
             (color yellow "<target>")
  | ":compile" ->
     sprintf ":compile %s - Compile AST to a specified target, valid targets are lem, coq, ocaml, c, and ir (intermediate representation)"
             (color yellow "<target>")
  | ":slice" ->
     ":slice - Slice AST to the definitions which the functions given by :slice_roots depend on, up to the functions given by :slice_cuts"
  | ":thin_slice" ->
     ":thin_slice - Slice AST to the function definitions given with :slice_roots"
  | "" ->
     sprintf "Type %s for a list of commands, and %s %s for information about a specific command"
             (color green ":commands") (color green ":help") (color yellow "<command>")
  | cmd ->
     sprintf "Either invalid command passed to help, or no documentation for %s. Try %s."
             (color green cmd) (color green ":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

let slice_roots = ref IdSet.empty
let slice_cuts = ref IdSet.empty

let rec describe_rewrite =
  let open Rewrites in
  function
  | String_rewriter rw -> "<string>" :: describe_rewrite (rw "")
  | Bool_rewriter rw -> "<bool>" :: describe_rewrite (rw false)
  | Literal_rewriter rw -> "(ocaml|lem|all)" :: describe_rewrite (rw (fun _ -> true))
  | Basic_rewriter rw -> []

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 ~check:true !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

(* This function is called on every line of input passed to the interpreter *)
let handle_input' input =
  LNoise.history_add input |> ignore;

  (* Process the input and check if it's a command, a raw expression,
     or empty. *)
  let input =
    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
      Command (cmd, arg)
    else if input <> "" then
      Expression input
    else
      Empty
  in

  let recognised = ref true in

  let unrecognised_command cmd =
    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 *)
  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 ()
     | ":prove" ->
        let nc = Initial_check.constraint_of_string arg in
        print_endline (string_of_bool (Type_check.prove __POS__ !Interactive.env nc))
     | ":assume" ->
        let nc = Initial_check.constraint_of_string arg in
        Interactive.env := Type_check.Env.add_constraint nc !Interactive.env
     | ":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 :prove :assume :clear :commands :help :output :option";
            "Normal mode commands - :elf :(l)oad :(u)nload :let :def :(b)ind :rewrite :rewrites :list_rewrites :compile";
            "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
     | ":option" ->
        begin
          try
            let args = Str.split (Str.regexp " +") arg in
            begin match args with
            | opt :: args ->
               Arg.parse_argv ~current:(ref 0) (Array.of_list ["sail"; opt; String.concat " " args]) Sail.options (fun _ -> ()) "";
            | [] -> print_endline "Must provide a valid option"
            end
          with
          | Arg.Bad message | Arg.Help message -> print_endline message
        end;
     | ":spec" ->
        let ast, env = Specialize.(specialize_passes 1 int_specialization !Interactive.env !Interactive.ast) in
        Interactive.ast := ast;
        Interactive.env := env;
        interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops
     | ":pretty" ->
        print_endline (Pretty_print_sail.to_string (Latex.defs !Interactive.ast))
     | ":ir" ->
        print_endline arg;
        let open Jib in
        let open Jib_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
           Interactive.ast := append_ast !Interactive.ast ast;
           interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
           Interactive.env := env;
           vs_ids := val_spec_ids !Interactive.ast
        | ":bin" ->
           begin
             let args = Util.split_on_char ' ' arg in
             match args with
             | [addr_s; filename] ->
                let addr = Big_int.of_string addr_s in
                Elf_loader.load_binary addr filename
             | _ ->
                print_endline "Invalid argument for :bin, expected <addr> <filename>"
           end
        | ":u" | ":unload" ->
           Interactive.ast := Ast.Defs [];
           Interactive.env := Type_check.initial_env;
           interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
           vs_ids := 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 ()
        | ":b" | ":bind" ->
           let args = Str.split (Str.regexp " +") arg in
           begin match args with
           | v :: ":" :: args ->
              let typ = Initial_check.typ_of_string (String.concat " " args) in
              let _, env, _ = Type_check.bind_pat !Interactive.env (mk_pat (P_id (mk_id v))) typ in
              Interactive.env := env
           | _ -> print_endline "Invalid arguments for :bind"
           end
        | ":let" ->
           let args = Str.split (Str.regexp " +") arg in
           begin match args with
           | v :: "=" :: args ->
              let exp = Initial_check.exp_of_string (String.concat " " args) in
              let ast, env = Type_check.check !Interactive.env (Defs [DEF_val (mk_letbind (mk_pat (P_id (mk_id v))) exp)]) in
              Interactive.ast := append_ast !Interactive.ast ast;
              Interactive.env := env;
              interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
           | _ -> print_endline "Invalid arguments for :let"
           end
        | ":def" ->
           let ast = Initial_check.ast_of_def_string_with (Process_file.preprocess_ast options) arg in
           let ast, env = Type_check.check !Interactive.env ast in
           Interactive.ast := append_ast !Interactive.ast ast;
           Interactive.env := env;
           interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
        | ":graph" ->
           let format = if arg = "" then "svg" else arg in
           let dotfile, out_chan = Filename.open_temp_file "sail_graph_" ".gz" in
           let image = Filename.temp_file "sail_graph_" ("." ^ format) in
           Slice.dot_of_ast out_chan !Interactive.ast;
           close_out out_chan;
           let _ = Unix.system (Printf.sprintf "dot -T%s %s -o %s" format dotfile image) in
           let _ = Unix.system (Printf.sprintf "xdg-open %s" image) in
           ()
        | ":slice_roots" ->
           let args = Str.split (Str.regexp " +") arg in
           let ids = List.map mk_id args |> IdSet.of_list in
           Specialize.add_initial_calls ids;
           slice_roots := IdSet.union ids !slice_roots
        | ":slice_cuts" ->
           let args = Str.split (Str.regexp " +") arg in
           let ids = List.map mk_id args |> IdSet.of_list in
           slice_cuts := IdSet.union ids !slice_cuts
        | ":slice" ->
           let open Slice in
           let module SliceNodeSet = Set.Make(Slice.Node) in
           let module G = Graph.Make(Slice.Node) in
           let g = Slice.graph_of_ast !Interactive.ast in
           let roots = !slice_roots |> IdSet.elements |> List.map (fun id -> Function id) |> SliceNodeSet.of_list in
           let cuts = !slice_cuts |> IdSet.elements |> List.map (fun id -> Function id) |> SliceNodeSet.of_list in
           let g = G.prune roots cuts g in
           Interactive.ast := Slice.filter_ast cuts g !Interactive.ast
        | ":thin_slice" ->
           let open Slice in
           let module SliceNodeSet = Set.Make(Slice.Node) in
           let module SliceNodeMap = Map.Make(Slice.Node) in
           let module G = Graph.Make(Slice.Node) in
           let g = Slice.graph_of_ast !Interactive.ast in
           let roots = !slice_roots |> IdSet.elements |> List.map (fun id -> Function id) |> SliceNodeSet.of_list in
           let keep = function
             | (Function id,_) when IdSet.mem id (!slice_roots) -> None
             | (Function id,_) -> Some (Function id)
             | _ -> None
           in
           let cuts = SliceNodeMap.bindings g |> Util.map_filter keep |> SliceNodeSet.of_list in
           let g = G.prune roots cuts g in
           Interactive.ast := Slice.filter_ast cuts g !Interactive.ast
        | ":list_rewrites" ->
           let print_rewrite (name, rw) =
             print_endline (name ^ " " ^ Util.(String.concat " " (describe_rewrite rw) |> yellow |> clear))
           in
           List.sort (fun a b -> String.compare (fst a) (fst b)) Rewrites.all_rewrites
           |> List.iter print_rewrite
        | ":rewrite" ->
           let open Rewrites in
           let args = Str.split (Str.regexp " +") arg in
           let rec parse_args rw args =
             match rw, args with
             | Basic_rewriter rw, [] -> rw
             | Bool_rewriter rw, arg :: args -> parse_args (rw (bool_of_string arg)) args
             | String_rewriter rw, arg :: args -> parse_args (rw arg) args
             | Literal_rewriter rw, arg :: args ->
                begin match arg with
                | "ocaml" -> parse_args (rw rewrite_lit_ocaml) args
                | "lem" -> parse_args (rw rewrite_lit_lem) args
                | "all" -> parse_args (rw (fun _ -> true)) args
                | _ -> failwith "target for literal rewrite must be one of ocaml/lem/all"
                end
             | _, _ -> failwith "Invalid arguments to rewrite"
           in
           begin match args with
           | rw :: args ->
              let rw = List.assoc rw Rewrites.all_rewrites in
              let rw = parse_args rw args in
              Interactive.ast := rw !Interactive.env !Interactive.ast;
           | [] ->
              failwith "Must provide the name of a rewrite, use :list_rewrites for a list of possible rewrites"
           end
        | ":rewrites" ->
           Interactive.ast := Process_file.rewrite_ast_target arg !Interactive.env !Interactive.ast;
           interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops
        | ":prover_regstate" ->
           let env, ast = prover_regstate (Some arg) !Interactive.ast !Interactive.env in
           Interactive.env := env;
           Interactive.ast := ast;
           interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops
        | ":recheck" ->
           let ast, env = Type_check.check Type_check.initial_env !Interactive.ast in
           Interactive.env := env;
           Interactive.ast := ast;
           interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
           vs_ids := val_spec_ids !Interactive.ast
        | ":compile" ->
           let out_name = match !opt_file_out with
             | None -> "out.sail"
             | Some f -> f ^ ".sail"
           in
           target (Some arg) out_name !Interactive.ast !Interactive.env
        | _ -> 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 -> ()
     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 ~check:true !Interactive.env [arg] in
               Interactive.ast := append_ast !Interactive.ast ast;
               interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
               Interactive.env := env;
               vs_ids := 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 !Interactive.env Value.primops;
           vs_ids := 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 Reporting.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) ->
        (* Evaluation mode commands *)
        begin
          match cmd with
          | ":r" | ":run" ->
             run ()
          | ":s" | ":step" ->
             run_steps (int_of_string arg)
          | _ -> unrecognised_command cmd
        end
     | Expression str ->
        print_endline "Already evaluating expression"
     | Empty ->
        (* Empty input will evaluate one step, or switch back to
             normal mode when evaluation is completed. *)
        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
               interactive_state := state;
               current_mode := Evaluation (eval_frame frame);
               print_program ()
             with
             | Failure str -> print_endline str; current_mode := Normal
           end
        | Break frame ->
           print_endline "Breakpoint";
           current_mode := Evaluation frame
        | Effect_request (out, state, stack, eff) ->
           begin
             try
               interactive_state := state;
               current_mode := Evaluation (Interpreter.default_effect_interp state eff);
               print_program ()
             with
             | Failure str -> print_endline str; current_mode := Normal
           end
        end
     end

let handle_input input =
  try handle_input' input with
  | Failure str ->
     print_endline ("Error: " ^ str)
  | Type_check.Type_error (env, l, err) ->
     print_endline (Type_error.string_of_type_error err)
  | Reporting.Fatal_error err ->
     Reporting.print_error err
  | exn ->
     print_endline (Printexc.to_string exn)

let () =
  (* Auto complete function names based on val specs, directories if :load command, or rewrites if :rewrite command *)
  LNoise.set_completion_callback (
      fun line_so_far ln_completions ->
      let line_so_far, last_id =
        try
          let p = Str.search_backward (Str.regexp "[^a-zA-Z0-9_/-]") line_so_far (String.length line_so_far - 1) in
          Str.string_before line_so_far (p + 1), Str.string_after line_so_far (p + 1)
        with
        | Not_found -> "", line_so_far
        | Invalid_argument _ -> line_so_far, ""
      in
      let n = try String.index line_so_far ' ' with Not_found -> String.length line_so_far in
      let cmd = Str.string_before line_so_far n in
      if last_id <> "" then
        begin match cmd with
        | ":load" | ":l" ->
           let dirname, basename = Filename.dirname last_id, Filename.basename last_id in
           if Sys.file_exists last_id then
             LNoise.add_completion ln_completions (line_so_far ^ last_id);
           if (try Sys.is_directory dirname with Sys_error _ -> false) then
             let contents = Sys.readdir (Filename.concat (Sys.getcwd ()) dirname) in
             for i = 0 to Array.length contents - 1 do
               if Str.string_match (Str.regexp_string basename) contents.(i) 0 then
                 let is_dir = (try Sys.is_directory (Filename.concat dirname contents.(i)) with Sys_error _ -> false) in
                 LNoise.add_completion ln_completions
                   (line_so_far ^ Filename.concat dirname contents.(i) ^ (if is_dir then Filename.dir_sep else ""))
             done
        | ":rewrite" ->
           List.map fst Rewrites.all_rewrites
           |> List.filter (fun opt -> Str.string_match (Str.regexp_string last_id) opt 0)
           |> List.map (fun completion -> line_so_far ^ completion)
           |> List.iter (LNoise.add_completion ln_completions)
        | ":option" ->
           List.map (fun (opt, _, _) -> opt) options
           |> List.filter (fun opt -> Str.string_match (Str.regexp_string last_id) opt 0)
           |> List.map (fun completion -> line_so_far ^ completion)
           |> List.iter (LNoise.add_completion ln_completions)
        | _ ->
          IdSet.elements !vs_ids
          |> List.map string_of_id
          |> List.filter (fun id -> Str.string_match (Str.regexp_string last_id) id 0)
          |> List.map (fun completion -> line_so_far ^ completion)
          |> List.iter (LNoise.add_completion ln_completions)
        end
      else ()
    );

  LNoise.set_hints_callback (
      fun line_so_far ->
      let hint str = Some (" " ^ str, LNoise.Yellow, false) in
      match String.trim line_so_far with
      | _ when !Interactive.opt_emacs_mode -> None
      | ":load"  | ":l" -> hint "<sail file>"
      | ":bind"  | ":b" -> hint "<id> : <type>"
      | ":infer" | ":i" -> hint "<expression>"
      | ":type"  | ":t" -> hint "<function id>"
      | ":let" -> hint "<id> = <expression>"
      | ":def" -> hint "<definition>"
      | ":prove" -> hint "<constraint>"
      | ":assume" -> hint "<constraint>"
      | ":compile" -> hint "<target>"
      | ":rewrites" -> hint "<target>"
      | str ->
         let args = Str.split (Str.regexp " +") str in
         match args with
         | [":rewrite"] -> hint "<rewrite>"
         | ":rewrite" :: rw :: args ->
            begin match List.assoc_opt rw Rewrites.all_rewrites with
            | Some rw ->
               let hints = describe_rewrite rw in
               let hints = Util.drop (List.length args) hints in
               (match hints with [] -> None | _ ->  hint (String.concat " " hints))
            | None -> None
            end
         | [":option"] -> hint "<flag>"
         | [":option"; flag] ->
            begin match List.find_opt (fun (opt, _, _) -> flag = opt) options with
            | Some (_, _, help) -> hint (Str.global_replace (Str.regexp " +") " " help)
            | None -> None
            end
         | _ -> None
    );

  (* Read the script file if it is set with the -is option, and excute them *)
  begin
    match !opt_interactive_script with
    | None -> ()
    | Some file ->
       let chan = open_in file in
       try
         while true do
           let line = input_line chan in
           handle_input line;
         done;
       with
       | End_of_file -> ()
  end;

  LNoise.history_load ~filename:"sail_history" |> ignore;
  LNoise.history_set ~max_length:100 |> ignore;

  if !Interactive.opt_interactive then
    begin
      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 ()