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

type state_tag = [ `Command | `Proof ]

exception Command_error of string

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

  (** 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 ();
          `Command (* dummy answer, useless *)
      | TacticAst.Command TacticAst.Proof ->
            (* do nothing, just for compatibility with coq syntax *)
          `Command
      | 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 (_, Some name, ast, None)) ->
          let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
          let proof = MatitaProof.proof ~typ:expr ~metasenv () in
          proof_handler.MatitaTypes.new_proof proof;
          `Proof
      | TacticAst.Command TacticAst.Quit ->
          proof_handler.MatitaTypes.quit ();
          `Command (* dummy answer, useless *)
      | TacticAst.Command TacticAst.Proof ->
            (* do nothing, just for compatibility with coq syntax *)
          `Command
      | tactical -> shared#evalTactical tactical
  end

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)

  (** 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)
  ()
=
    (** term AST -> Cic.term. Uses disambiguator and change imperatively the
    * metasenv as needed *)
  let disambiguate ast =
    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) =
      disambiguator#disambiguateTermAst ~context ~metasenv ast
    in
    proof#set_metasenv metasenv;
    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 -> EqualityTactics.reflexivity_tac
    | TacticAst.Assumption -> VariousTactics.assumption_tac
    | TacticAst.Contradiction -> NegationTactics.contradiction_tac
    | TacticAst.Exists -> IntroductionTactics.exists_tac
    | TacticAst.Fourier -> FourierR.fourier_tac
    | TacticAst.Left -> IntroductionTactics.left_tac
    | TacticAst.Right -> IntroductionTactics.right_tac
    | TacticAst.Ring -> Ring.ring_tac
    | TacticAst.Split -> IntroductionTactics.split_tac
    | TacticAst.Symmetry -> EqualityTactics.symmetry_tac
    | TacticAst.Transitivity term ->
        EqualityTactics.transitivity_tac (disambiguate term)
    | TacticAst.Apply term -> PrimitiveTactics.apply_tac (disambiguate term)
    | TacticAst.Exact term -> PrimitiveTactics.exact_tac (disambiguate term)
    | TacticAst.Cut term -> PrimitiveTactics.cut_tac (disambiguate term)
    | TacticAst.ElimType term ->
        EliminationTactics.elim_type_tac (disambiguate term)
    | TacticAst.Replace (what, with_what) ->
        EqualityTactics.replace_tac ~what:(disambiguate what)
          ~with_what:(disambiguate with_what)
  (*
    (* TODO Zack a lot more of tactics to be implemented here ... *)
    | TacticAst.Absurd
    | 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.Elim of 'term * 'term option
    | 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 ();
          `Command
      | TacticAst.Command (TacticAst.Undo steps) ->
          (proof_handler.MatitaTypes.get_proof ())#undo ?steps ();
          `Proof
      | TacticAst.Command (TacticAst.Redo steps) ->
          (proof_handler.MatitaTypes.get_proof ())#redo ?steps ();
          `Proof
      | TacticAst.Seq tacticals ->
          (* TODO Zack check for proof completed at each step? *)
          List.iter (fun t -> ignore (self#evalTactical t)) tacticals;
          `Proof
      | TacticAst.Tactic tactic_phrase ->
          let tactic = lookup_tactic tactic_phrase in
          (proof_handler.MatitaTypes.get_proof ())#apply_tactic tactic;
          `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
    val mutable state = commandState

    method evalPhrase s =
      try
        (match state#evalPhrase s with
        | `Command -> state <- commandState
        | `Proof -> state <- proofState)
      with exn ->
        console#echo_error (sprintf "Uncaught exception: %s"
          (Printexc.to_string exn))
  end