1 (* Copyright (C) 2004, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
26 (** Interpreter for textual phrases coming from matita's console (textual entry
27 * window at the bottom of the main window).
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.
37 (** None means: "same state as before" *)
38 type state_tag = [ `Command | `Proof ] option
40 exception Command_error of string
42 let canonical_context metano metasenv =
44 let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in
47 failwith (sprintf "Can't find canonical context for %d" metano)
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)
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
69 proof#set_metasenv metasenv;
72 disambiguator#disambiguateTermAst ast
74 class virtual interpreterState ~(console: MatitaConsole.console) =
76 (** eval a toplevel phrase in the current state and return the new state
78 method parsePhrase s = CicTextualParser2.parse_tactical (Stream.of_string s)
80 method virtual evalTactical:
81 (CicAst.term, string) TacticAst.tactical -> state_tag
83 method evalPhrase s = self#evalTactical (self#parsePhrase s)
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 ())
92 (** Implements phrases that should be accepted in all states *)
94 ~(disambiguator: MatitaTypes.disambiguator)
95 ~(proof_handler: MatitaTypes.proof_handler)
96 ~(console: MatitaConsole.console)
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 *)
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;
119 widget#load_sequents [dummyno, metadata];
120 widget#goto_sequent dummyno;
123 raise (Command_error (TacticAstPp.pp_tactical tactical))
126 (** Implements phrases that should be accepted only in `Command state *)
128 ~(disambiguator: MatitaTypes.disambiguator)
129 ~(proof_handler: MatitaTypes.proof_handler)
130 ~(console: MatitaConsole.console)
133 let shared = new sharedState ~disambiguator ~proof_handler ~console () in
135 inherit interpreterState ~console
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;
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 *)
150 | tactical -> shared#evalTactical tactical
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 *)
157 let len = List.length names in
159 fun metasenv context name ~typ ->
160 if !count < len then begin
161 let name = Cic.Name (List.nth names !count) in
165 FreshNamesGenerator.mk_fresh_name metasenv context name ~typ
167 (** Implements phrases that should be accepted only in `Proof state, basically
170 ~(disambiguator: MatitaTypes.disambiguator)
171 ~(proof_handler: MatitaTypes.proof_handler)
172 ~(console: MatitaConsole.console)
175 let disambiguate ast =
176 let (_, _, term) = disambiguate ~disambiguator ~proof_handler ast 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)
205 (* TODO Zack a lot more of tactics to be implemented here ... *)
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
220 MatitaTypes.not_implemented "some tactic"
222 let shared = new sharedState ~disambiguator ~proof_handler ~console () in
224 inherit interpreterState ~console
226 method evalTactical = function
227 | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
228 | TacticAst.Command TacticAst.Abort ->
229 proof_handler.MatitaTypes.abort_proof ();
231 | TacticAst.Command (TacticAst.Undo steps) ->
232 (proof_handler.MatitaTypes.get_proof ())#undo ?steps ();
234 | TacticAst.Command (TacticAst.Redo steps) ->
235 (proof_handler.MatitaTypes.get_proof ())#redo ?steps ();
237 | TacticAst.Seq tacticals ->
238 (* TODO Zack check for proof completed at each step? *)
239 List.iter (fun t -> ignore (self#evalTactical t)) tacticals;
241 | TacticAst.Tactic tactic_phrase ->
242 let tactic = lookup_tactic tactic_phrase in
243 (proof_handler.MatitaTypes.get_proof ())#apply_tactic tactic;
245 | tactical -> shared#evalTactical tactical
249 ~(disambiguator: MatitaTypes.disambiguator)
250 ~(proof_handler: MatitaTypes.proof_handler)
251 ~(console: MatitaConsole.console)
255 new commandState ~disambiguator ~proof_handler ~console ()
257 let proofState = new proofState ~disambiguator ~proof_handler ~console () in
259 val mutable state = commandState
261 method reset = state <- commandState
263 method evalPhrase s =
265 (match state#evalPhrase s with
266 | Some `Command -> state <- commandState
267 | Some `Proof -> state <- proofState
270 console#echo_error (sprintf "Uncaught exception: %s"
271 (Printexc.to_string exn))