(* Copyright (C) 2004, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://helm.cs.unibo.it/
 *)

(** Interpreter for textual phrases coming from matita's console (textual entry
* window at the bottom of the main window).
*
* Interpreter is either in `Command state or in `Proof state (see state_tag type
* below). In `Command state commands for starting proofs are accepted, but
* tactic and tactical applications are not. In `Proof state both
* tactic/tacticals and commands are accepted.
*)

open Printf

  (** None means: "same state as before" *)
type state_tag = [ `Command | `Proof ] option

exception Command_error of string

let uri name =
  UriManager.uri_of_string (sprintf "%s/%s" BuildTimeConf.base_uri name)

let canonical_context metano metasenv =
  try
    let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in
    context
  with Not_found ->
    failwith (sprintf "Can't find canonical context for %d" metano)

let get_context_and_metasenv (proof_handler:MatitaTypes.proof_handler) =
  if proof_handler.MatitaTypes.has_proof () then
    let proof = proof_handler.MatitaTypes.get_proof () in
    let metasenv = proof#metasenv in
    let goal = proof#goal in
    (canonical_context goal metasenv, metasenv)
  else
    ([], [])

  (** term AST -> Cic.term. Uses disambiguator and change imperatively the
  * metasenv as needed *)
let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~proof_handler ast =
  if proof_handler.MatitaTypes.has_proof () then begin
    let proof = proof_handler.MatitaTypes.get_proof () in
    let metasenv = proof#metasenv in
    let goal = proof#goal in
    let context = canonical_context goal metasenv in
    let (_, metasenv, term) as retval =
      disambiguator#disambiguateTermAst ~context ~metasenv ast
    in
    proof#set_metasenv metasenv;
    retval
  end else
    disambiguator#disambiguateTermAst ast

class virtual interpreterState ~(console: MatitaConsole.console) =
  object (self)
      (** eval a toplevel phrase in the current state and return the new state
      *)
    method parsePhrase s = CicTextualParser2.parse_tactical (Stream.of_string s)

    method virtual evalTactical:
      (CicAst.term, string) TacticAst.tactical -> state_tag

    method evalPhrase s = self#evalTactical (self#parsePhrase s)

  end

let check_widget: MatitaTypes.sequent_viewer lazy_t = lazy
  (let gui = MatitaGui.instance () in
  MatitaMathView.sequent_viewer ~show:true ~packing:gui#check#scrolledCheck#add
    ())

  (** Implements phrases that should be accepted in all states *)
class sharedState
  ~(disambiguator: MatitaTypes.disambiguator)
  ~(proof_handler: MatitaTypes.proof_handler)
  ~(console: MatitaConsole.console)
  ()
=
  object (self)
    inherit interpreterState ~console
    method evalTactical = function
      | TacticAst.Command TacticAst.Quit ->
          proof_handler.MatitaTypes.quit ();
          Some `Command (* dummy answer, useless *)
      | TacticAst.Command TacticAst.Proof ->
            (* do nothing, just for compatibility with coq syntax *)
          Some `Command
      | TacticAst.Command (TacticAst.Check term) ->
          let (_, _, term) = disambiguate ~disambiguator ~proof_handler term in
          let (context, metasenv) = get_context_and_metasenv proof_handler in
          let dummyno = CicMkImplicit.new_meta metasenv [] in
          let ty = CicTypeChecker.type_of_aux' metasenv context term in
          let expr = Cic.Cast (term, ty) in
          let sequent = (dummyno, context, expr) in
          let widget = Lazy.force check_widget in
          let gui = MatitaGui.instance () in
          gui#check#checkWin#show ();
          gui#main#showCheckMenuItem#set_active true;
          widget#load_sequent (sequent::metasenv) dummyno;
          None
      | tactical ->
          raise (Command_error (TacticAstPp.pp_tactical tactical))
  end

  (** Implements phrases that should be accepted only in `Command state *)
class commandState
  ~(disambiguator: MatitaTypes.disambiguator)
  ~(proof_handler: MatitaTypes.proof_handler)
  ~(console: MatitaConsole.console)
  ()
=
  let shared = new sharedState ~disambiguator ~proof_handler ~console () in
  object (self)
    inherit interpreterState ~console

    method evalTactical = function
      | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
      | TacticAst.Command (TacticAst.Theorem (_, name_opt, ast, None)) ->
          let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
          let uri =
            match name_opt with
            | None -> None
            | Some name -> Some (uri name)
          in
          let proof = MatitaProof.proof ~typ:expr ?uri ~metasenv () in
          proof_handler.MatitaTypes.new_proof proof;
          Some `Proof
      | TacticAst.Command TacticAst.Quit ->
          proof_handler.MatitaTypes.quit ();
          Some `Command (* dummy answer, useless *)
      | TacticAst.Command TacticAst.Proof ->
            (* do nothing, just for compatibility with coq syntax *)
          Some `Command
      | tactical -> shared#evalTactical tactical
  end

  (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
  * names as long as they are available, then it fallbacks to name generation
  * using FreshNamesGenerator module *)
let namer_of names =
  let len = List.length names in
  let count = ref 0 in
  fun metasenv context name ~typ ->
    if !count < len then begin
      let name = Cic.Name (List.nth names !count) in
      incr count;
      name
    end else
      FreshNamesGenerator.mk_fresh_name metasenv context name ~typ

  (** Implements phrases that should be accepted only in `Proof state, basically
  * tacticals *)
class proofState
  ~(disambiguator: MatitaTypes.disambiguator)
  ~(proof_handler: MatitaTypes.proof_handler)
  ~(console: MatitaConsole.console)
  ()
=
  let disambiguate ast =
    let (_, _, term) = disambiguate ~disambiguator ~proof_handler ast in
    term
  in
    (** tactic AST -> ProofEngineTypes.tactic *)
  let rec lookup_tactic = function
    | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic
    | TacticAst.Intros (_, names) ->  (* TODO Zack implement intros length *)
        PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
    | TacticAst.Reflexivity -> Tactics.reflexivity
    | TacticAst.Assumption -> Tactics.assumption
    | TacticAst.Contradiction -> Tactics.contradiction
    | TacticAst.Exists -> Tactics.exists
    | TacticAst.Fourier -> Tactics.fourier
    | TacticAst.Left -> Tactics.left
    | TacticAst.Right -> Tactics.right
    | TacticAst.Ring -> Tactics.ring
    | TacticAst.Split -> Tactics.split
    | TacticAst.Symmetry -> Tactics.symmetry
    | TacticAst.Transitivity term -> Tactics.transitivity (disambiguate term)
    | TacticAst.Apply term -> Tactics.apply (disambiguate term)
    | TacticAst.Absurd term -> Tactics.absurd (disambiguate term)
    | TacticAst.Exact term -> Tactics.exact (disambiguate term)
    | TacticAst.Cut term -> Tactics.cut (disambiguate term)
    | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *)
        Tactics.elim_intros_simpl (disambiguate term)
    | TacticAst.ElimType term -> Tactics.elim_type (disambiguate term)
    | TacticAst.Replace (what, with_what) ->
        Tactics.replace ~what:(disambiguate what)
          ~with_what:(disambiguate with_what)
  (*
    (* TODO Zack a lot more of tactics to be implemented here ... *)
    | TacticAst.Change of 'term * 'term * 'ident option
    | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
    | TacticAst.Decompose of 'ident * 'ident list
    | TacticAst.Discriminate of 'ident
    | TacticAst.Fold of reduction_kind * 'term
    | TacticAst.Injection of 'ident
    | TacticAst.LetIn of 'term * 'ident
    | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
    | TacticAst.Replace_pattern of 'term pattern * 'term
    | TacticAst.Rewrite of direction * 'term * 'ident option
  *)
    | _ ->
        MatitaTypes.not_implemented "some tactic"
  in
  let shared = new sharedState ~disambiguator ~proof_handler ~console () in
  object (self)
    inherit interpreterState ~console

    method evalTactical = function
      | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
      | TacticAst.Command TacticAst.Abort ->
          proof_handler.MatitaTypes.abort_proof ();
          Some `Command
      | TacticAst.Command (TacticAst.Undo steps) ->
          (proof_handler.MatitaTypes.get_proof ())#undo ?steps ();
          Some `Proof
      | TacticAst.Command (TacticAst.Redo steps) ->
          (proof_handler.MatitaTypes.get_proof ())#redo ?steps ();
          Some `Proof
      | TacticAst.Command (TacticAst.Qed name_opt) ->
          (* TODO Zack this function probably should not simply fail with
          * Failure, but rather raise some more meaningful exception *)
          if not (proof_handler.MatitaTypes.has_proof ()) then assert false;
          let proof = proof_handler.MatitaTypes.get_proof () in
          (match name_opt with
          | None -> ()
          | Some name -> proof#set_uri (uri name));
          let (uri, metasenv, bo, ty) = proof#proof in
          let uri = MatitaTypes.unopt_uri uri in
          if metasenv <> [] then failwith "Proof not completed";
          let proved_ty = CicTypeChecker.type_of_aux' [] [] bo in
          if not (CicReduction.are_convertible [] proved_ty ty) then
            failwith "Wrong proof";
          (* TODO Zack [] probably wrong *)
          CicEnvironment.add_type_checked_term uri
            (Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[]));
          proof_handler.MatitaTypes.set_proof None;
          (* TODO Zack a lot more to be done here:
            * - save object to disk in xml format
            * - collect metadata
            * - register uri to the getter *)
          Some `Command
      | TacticAst.Seq tacticals ->
          (* TODO Zack check for proof completed at each step? *)
          List.iter (fun t -> ignore (self#evalTactical t)) tacticals;
          Some `Proof
      | TacticAst.Tactic tactic_phrase ->
          let tactic = lookup_tactic tactic_phrase in
          (proof_handler.MatitaTypes.get_proof ())#apply_tactic tactic;
          Some `Proof
      | tactical -> shared#evalTactical tactical
  end

class interpreter
  ~(disambiguator: MatitaTypes.disambiguator)
  ~(proof_handler: MatitaTypes.proof_handler)
  ~(console: MatitaConsole.console)
  ()
=
  let commandState =
    new commandState ~disambiguator ~proof_handler ~console ()
  in
  let proofState = new proofState ~disambiguator ~proof_handler ~console () in
  object (self)
    val mutable state = commandState

    method reset = state <- commandState

    method private updateState = function
      | Some `Command -> state <- commandState
      | Some `Proof -> state <- proofState
      | None -> ()

    method evalPhrase s =
      try
        self#updateState (state#evalPhrase s)
      with exn ->
        console#echo_error (sprintf "Uncaught exception: %s"
          (Printexc.to_string exn))

(*
    method evalAll s =
      let get_end_pos = function
        | TacticAst.LocatedTactical ((_, end_pos), _) -> end_pos.Lexing.pos_cnum
        | _ -> assert false
      in
      let str_len = String.length s in
      let rec aux offset =
        let tactical =
          self#parsePhrase (String.sub s offset (str_len - offset))
        in
        self#updateState (state#evalTactical tactical);
        let next_offset = get_end_pos tactical + offset in
        if next_offset = str_len - 1 then
      in
*)

  end