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

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 ->
     mode_clear ();
     begin
       try callback v with
       | Reporting_basic.Fatal_error e -> Reporting_basic.report_error e
     end;
     user_input callback

let sail_logo =
  let banner str = str |> Util.bold |> Util.red |> Util.clear in
  [ {|    ___       ___       ___       ___ |};
    {|   /\  \     /\  \     /\  \     /\__\|};
    {|  /::\  \   /::\  \   _\:\  \   /:/  /|};
    {| /\:\:\__\ /::\:\__\ /\/::\__\ /:/__/ |};
    {| \:\:\/__/ \/\::/  / \::/\/__/ \:\  \ |};
    {|  \::/  /    /:/  /   \:\__\    \:\__\|};
    {|   \/__/     \/__/     \/__/     \/__/|};
    ""
  ]
  |> List.map banner

let vs_ids = ref (Initial_check.val_spec_ids !interactive_ast)

let interactive_state = ref (initial_state !interactive_ast)

let print_program () =
  match !current_mode with
  | Normal -> ()
  | Evaluation (Step (out, _, _, stack)) ->
     let sep = "-----------------------------------------------------" |> Util.blue |> Util.clear in
     List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline code; print_endline sep);
     print_endline out
  | Evaluation _ -> ()

let rec run () =
  match !current_mode with
  | Normal -> ()
  | Evaluation frame ->
     begin
       match frame with
       | Done (state, v) ->
          interactive_state := state;
          print_endline ("Result = " ^ Value.string_of_value v);
          current_mode := Normal
       | Step (out, state, _, stack) ->
          current_mode := Evaluation (eval_frame !interactive_ast frame);
          run ()
       | Break frame ->
          print_endline "Breakpoint";
          current_mode := Evaluation frame
     end

let rec run_steps n =
  match !current_mode with
  | _ when n <= 0 -> ()
  | Normal -> ()
  | Evaluation frame ->
     begin
       match frame with
       | Done (state, v) ->
          interactive_state := state;
          print_endline ("Result = " ^ Value.string_of_value v);
          current_mode := Normal
       | Step (out, state, _, stack) ->
          current_mode := Evaluation (eval_frame !interactive_ast frame);
          run_steps (n - 1)
       | Break frame ->
          print_endline "Breakpoint";
          current_mode := Evaluation frame
     end

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") else ()
  in

  (* First handle commands that are mode-independent *)
  begin
    match input with
    | Command (cmd, arg) ->
       begin
         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 3;
            print_endline ("Verbosity: " ^ string_of_int !Type_check.opt_tc_debug)
         | _ -> 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
            | _ -> 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 Ast_util.dec_ord str) in
          current_mode := Evaluation (eval_frame !interactive_ast (Step ("", !interactive_state, return exp, [])));
          print_program ()
       | 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)
           | ":n" | ":normal" ->
              current_mode := Normal
           | _ -> 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
            | Step (out, state, _, stack) ->
               interactive_state := state;
               current_mode := Evaluation (eval_frame !interactive_ast frame);
               print_program ()
            | Break frame ->
               print_endline "Breakpoint";
               current_mode := Evaluation frame
          end
     end

let handle_input input =
  try handle_input' input with
  | Type_check.Type_error (l, err) ->
     print_endline (Type_check.string_of_type_error err)
  | exn ->
     print_endline (Printexc.to_string exn)

let () =
  (* Auto complete function names based on val specs *)
  LNoise.set_completion_callback
    begin
      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
      if last_id <> "" then
        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)
      else ()
    end;

  (* 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 !opt_interactive then
    begin
      List.iter print_endline sail_logo;
      user_input handle_input
    end
  else ()