helm/matita/matitaInterpreter.ml

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (** Interpreter for textual phrases coming from matita's console (textual entry
  27 * window at the bottom of the main window).
  28 *
  29 * Interpreter is either in `Command state or in `Proof state (see state_tag type
  30 * below). In `Command state commands for starting proofs are accepted, but
  31 * tactic and tactical applications are not. In `Proof state both
  32 * tactic/tacticals and commands are accepted.
  33 *)
  34
  35 open Printf
  36
  37   (** None means: "same state as before" *)
  38 type state_tag = [ `Command | `Proof ] option
  39
  40 exception Command_error of string
  41
  42 let canonical_context metano metasenv =
  43   try
  44     let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in
  45     context
  46   with Not_found ->
  47     failwith (sprintf "Can't find canonical context for %d" metano)
  48
  49 let get_context_and_metasenv (proof_handler:MatitaTypes.proof_handler) =
  50   if proof_handler.MatitaTypes.has_proof () then
  51     let proof = proof_handler.MatitaTypes.get_proof () in
  52     let metasenv = proof#metasenv in
  53     let goal = proof#goal in
  54     (canonical_context goal metasenv, metasenv)
  55   else
  56     ([], [])
  57
  58   (** term AST -> Cic.term. Uses disambiguator and change imperatively the
  59   * metasenv as needed *)
  60 let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~proof_handler ast =
  61   if proof_handler.MatitaTypes.has_proof () then begin
  62     let proof = proof_handler.MatitaTypes.get_proof () in
  63     let metasenv = proof#metasenv in
  64     let goal = proof#goal in
  65     let context = canonical_context goal metasenv in
  66     let (_, metasenv, term) as retval =
  67       disambiguator#disambiguateTermAst ~context ~metasenv ast
  68     in
  69     proof#set_metasenv metasenv;
  70     retval
  71   end else
  72     disambiguator#disambiguateTermAst ast
  73
  74 class virtual interpreterState ~(console: MatitaConsole.console) =
  75   object (self)
  76       (** eval a toplevel phrase in the current state and return the new state
  77       *)
  78     method parsePhrase s = CicTextualParser2.parse_tactical (Stream.of_string s)
  79
  80     method virtual evalTactical:
  81       (CicAst.term, string) TacticAst.tactical -> state_tag
  82
  83     method evalPhrase s = self#evalTactical (self#parsePhrase s)
  84   end
  85
  86 let check_widget: MatitaTypes.sequents_viewer lazy_t = lazy (
  87   let gui = MatitaGui.instance () in
  88   let notebook = GPack.notebook ~show:true ~packing:gui#check#checkWin#add () in
  89   let sequent_viewer = MatitaMathView.sequent_viewer ~show:true () in
  90   MatitaMathView.sequents_viewer ~notebook ~sequent_viewer ())
  91
  92   (** Implements phrases that should be accepted in all states *)
  93 class sharedState
  94   ~(disambiguator: MatitaTypes.disambiguator)
  95   ~(proof_handler: MatitaTypes.proof_handler)
  96   ~(console: MatitaConsole.console)
  97   ()
  98 =
  99   object (self)
 100     inherit interpreterState ~console
 101     method evalTactical = function
 102       | TacticAst.Command TacticAst.Quit ->
 103           proof_handler.MatitaTypes.quit ();
 104           Some `Command (* dummy answer, useless *)
 105       | TacticAst.Command TacticAst.Proof ->
 106             (* do nothing, just for compatibility with coq syntax *)
 107           Some `Command
 108       | TacticAst.Command (TacticAst.Check term) ->
 109           let dummyno = 1023 in
 110           let (_, _, term) = disambiguate ~disambiguator ~proof_handler term in
 111           let (context, metasenv) = get_context_and_metasenv proof_handler in
 112           let sequent = (dummyno, context, term) in
 113           let metadata = Cic2acic.asequent_of_sequent metasenv sequent in
 114           let widget = Lazy.force check_widget in
 115           let gui = MatitaGui.instance () in
 116           gui#check#checkWin#show ();
 117           gui#main#showCheckMenuItem#set_active true;
 118           widget#reset;
 119           widget#load_sequents [dummyno, metadata];
 120           widget#goto_sequent dummyno;
 121           None
 122       | tactical ->
 123           raise (Command_error (TacticAstPp.pp_tactical tactical))
 124   end
 125
 126   (** Implements phrases that should be accepted only in `Command state *)
 127 class commandState
 128   ~(disambiguator: MatitaTypes.disambiguator)
 129   ~(proof_handler: MatitaTypes.proof_handler)
 130   ~(console: MatitaConsole.console)
 131   ()
 132 =
 133   let shared = new sharedState ~disambiguator ~proof_handler ~console () in
 134   object (self)
 135     inherit interpreterState ~console
 136
 137     method evalTactical = function
 138       | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
 139       | TacticAst.Command (TacticAst.Theorem (_, Some name, ast, None)) ->
 140           let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
 141           let proof = MatitaProof.proof ~typ:expr ~metasenv () in
 142           proof_handler.MatitaTypes.new_proof proof;
 143           Some `Proof
 144       | TacticAst.Command TacticAst.Quit ->
 145           proof_handler.MatitaTypes.quit ();
 146           Some `Command (* dummy answer, useless *)
 147       | TacticAst.Command TacticAst.Proof ->
 148             (* do nothing, just for compatibility with coq syntax *)
 149           Some `Command
 150       | tactical -> shared#evalTactical tactical
 151   end
 152
 153   (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
 154   * names as long as they are available, then it fallbacks to name generation
 155   * using FreshNamesGenerator module *)
 156 let namer_of names =
 157   let len = List.length names in
 158   let count = ref 0 in
 159   fun metasenv context name ~typ ->
 160     if !count < len then begin
 161       let name = Cic.Name (List.nth names !count) in
 162       incr count;
 163       name
 164     end else
 165       FreshNamesGenerator.mk_fresh_name metasenv context name ~typ
 166
 167   (** Implements phrases that should be accepted only in `Proof state, basically
 168   * tacticals *)
 169 class proofState
 170   ~(disambiguator: MatitaTypes.disambiguator)
 171   ~(proof_handler: MatitaTypes.proof_handler)
 172   ~(console: MatitaConsole.console)
 173   ()
 174 =
 175   let disambiguate ast =
 176     let (_, _, term) = disambiguate ~disambiguator ~proof_handler ast in
 177     term
 178   in
 179     (** tactic AST -> ProofEngineTypes.tactic *)
 180   let rec lookup_tactic = function
 181     | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic
 182     | TacticAst.Intros (_, names) ->  (* TODO Zack implement intros length *)
 183         PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
 184     | TacticAst.Reflexivity -> EqualityTactics.reflexivity_tac
 185     | TacticAst.Assumption -> VariousTactics.assumption_tac
 186     | TacticAst.Contradiction -> NegationTactics.contradiction_tac
 187     | TacticAst.Exists -> IntroductionTactics.exists_tac
 188     | TacticAst.Fourier -> FourierR.fourier_tac
 189     | TacticAst.Left -> IntroductionTactics.left_tac
 190     | TacticAst.Right -> IntroductionTactics.right_tac
 191     | TacticAst.Ring -> Ring.ring_tac
 192     | TacticAst.Split -> IntroductionTactics.split_tac
 193     | TacticAst.Symmetry -> EqualityTactics.symmetry_tac
 194     | TacticAst.Transitivity term ->
 195         EqualityTactics.transitivity_tac (disambiguate term)
 196     | TacticAst.Apply term -> PrimitiveTactics.apply_tac (disambiguate term)
 197     | TacticAst.Exact term -> PrimitiveTactics.exact_tac (disambiguate term)
 198     | TacticAst.Cut term -> PrimitiveTactics.cut_tac (disambiguate term)
 199     | TacticAst.ElimType term ->
 200         EliminationTactics.elim_type_tac (disambiguate term)
 201     | TacticAst.Replace (what, with_what) ->
 202         EqualityTactics.replace_tac ~what:(disambiguate what)
 203           ~with_what:(disambiguate with_what)
 204   (*
 205     (* TODO Zack a lot more of tactics to be implemented here ... *)
 206     | TacticAst.Absurd
 207     | TacticAst.Change of 'term * 'term * 'ident option
 208     | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
 209     | TacticAst.Decompose of 'ident * 'ident list
 210     | TacticAst.Discriminate of 'ident
 211     | TacticAst.Elim of 'term * 'term option
 212     | TacticAst.Fold of reduction_kind * 'term
 213     | TacticAst.Injection of 'ident
 214     | TacticAst.LetIn of 'term * 'ident
 215     | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
 216     | TacticAst.Replace_pattern of 'term pattern * 'term
 217     | TacticAst.Rewrite of direction * 'term * 'ident option
 218   *)
 219     | _ ->
 220         MatitaTypes.not_implemented "some tactic"
 221   in
 222   let shared = new sharedState ~disambiguator ~proof_handler ~console () in
 223   object (self)
 224     inherit interpreterState ~console
 225
 226     method evalTactical = function
 227       | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
 228       | TacticAst.Command TacticAst.Abort ->
 229           proof_handler.MatitaTypes.abort_proof ();
 230           Some `Command
 231       | TacticAst.Command (TacticAst.Undo steps) ->
 232           (proof_handler.MatitaTypes.get_proof ())#undo ?steps ();
 233           Some `Proof
 234       | TacticAst.Command (TacticAst.Redo steps) ->
 235           (proof_handler.MatitaTypes.get_proof ())#redo ?steps ();
 236           Some `Proof
 237       | TacticAst.Seq tacticals ->
 238           (* TODO Zack check for proof completed at each step? *)
 239           List.iter (fun t -> ignore (self#evalTactical t)) tacticals;
 240           Some `Proof
 241       | TacticAst.Tactic tactic_phrase ->
 242           let tactic = lookup_tactic tactic_phrase in
 243           (proof_handler.MatitaTypes.get_proof ())#apply_tactic tactic;
 244           Some `Proof
 245       | tactical -> shared#evalTactical tactical
 246   end
 247
 248 class interpreter
 249   ~(disambiguator: MatitaTypes.disambiguator)
 250   ~(proof_handler: MatitaTypes.proof_handler)
 251   ~(console: MatitaConsole.console)
 252   ()
 253 =
 254   let commandState =
 255     new commandState ~disambiguator ~proof_handler ~console ()
 256   in
 257   let proofState = new proofState ~disambiguator ~proof_handler ~console () in
 258   object
 259     val mutable state = commandState
 260
 261     method reset = state <- commandState
 262
 263     method evalPhrase s =
 264       try
 265         (match state#evalPhrase s with
 266         | Some `Command -> state <- commandState
 267         | Some `Proof -> state <- proofState
 268         | None -> ())
 269       with exn ->
 270         console#echo_error (sprintf "Uncaught exception: %s"
 271           (Printexc.to_string exn))
 272   end
 273