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
43 UriManager.uri_of_string (sprintf "%s/%s" BuildTimeConf.base_uri name)
45 let canonical_context metano metasenv =
47 let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in
50 failwith (sprintf "Can't find canonical context for %d" metano)
52 let get_context_and_metasenv (proof_handler:MatitaTypes.proof_handler) =
53 if proof_handler.MatitaTypes.has_proof () then
54 let proof = proof_handler.MatitaTypes.get_proof () in
55 let metasenv = proof#metasenv in
56 let goal = proof#goal in
57 (canonical_context goal metasenv, metasenv)
61 (** term AST -> Cic.term. Uses disambiguator and change imperatively the
62 * metasenv as needed *)
63 let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~proof_handler ast =
64 if proof_handler.MatitaTypes.has_proof () then begin
65 let proof = proof_handler.MatitaTypes.get_proof () in
66 let metasenv = proof#metasenv in
67 let goal = proof#goal in
68 let context = canonical_context goal metasenv in
69 let (_, metasenv, term) as retval =
70 disambiguator#disambiguateTermAst ~context ~metasenv ast
72 proof#set_metasenv metasenv;
75 disambiguator#disambiguateTermAst ast
77 class virtual interpreterState ~(console: MatitaConsole.console) =
79 (** eval a toplevel phrase in the current state and return the new state
81 method parsePhrase s = CicTextualParser2.parse_tactical (Stream.of_string s)
83 method virtual evalTactical:
84 (CicAst.term, string) TacticAst.tactical -> state_tag
86 method evalPhrase s = self#evalTactical (self#parsePhrase s)
89 let check_widget: MatitaTypes.sequent_viewer lazy_t = lazy
90 (let gui = MatitaGui.instance () in
91 MatitaMathView.sequent_viewer ~show:true ~packing:gui#check#scrolledCheck#add
94 (** Implements phrases that should be accepted in all states *)
96 ~(disambiguator: MatitaTypes.disambiguator)
97 ~(proof_handler: MatitaTypes.proof_handler)
98 ~(console: MatitaConsole.console)
102 inherit interpreterState ~console
103 method evalTactical = function
104 | TacticAst.Command TacticAst.Quit ->
105 proof_handler.MatitaTypes.quit ();
106 Some `Command (* dummy answer, useless *)
107 | TacticAst.Command TacticAst.Proof ->
108 (* do nothing, just for compatibility with coq syntax *)
110 | TacticAst.Command (TacticAst.Check term) ->
111 let (_, _, term) = disambiguate ~disambiguator ~proof_handler term in
112 let (context, metasenv) = get_context_and_metasenv proof_handler in
113 let dummyno = CicMkImplicit.new_meta metasenv [] in
114 let ty = CicTypeChecker.type_of_aux' metasenv context term in
115 let expr = Cic.Cast (term, ty) in
116 let sequent = (dummyno, context, expr) in
117 let widget = Lazy.force check_widget in
118 let gui = MatitaGui.instance () in
119 gui#check#checkWin#show ();
120 gui#main#showCheckMenuItem#set_active true;
121 widget#load_sequent (sequent::metasenv) dummyno;
124 raise (Command_error (TacticAstPp.pp_tactical tactical))
127 (** Implements phrases that should be accepted only in `Command state *)
129 ~(disambiguator: MatitaTypes.disambiguator)
130 ~(proof_handler: MatitaTypes.proof_handler)
131 ~(console: MatitaConsole.console)
134 let shared = new sharedState ~disambiguator ~proof_handler ~console () in
136 inherit interpreterState ~console
138 method evalTactical = function
139 | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
140 | TacticAst.Command (TacticAst.Theorem (_, name_opt, ast, None)) ->
141 let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
145 | Some name -> Some (uri name)
147 let proof = MatitaProof.proof ~typ:expr ?uri ~metasenv () in
148 proof_handler.MatitaTypes.new_proof proof;
150 | TacticAst.Command TacticAst.Quit ->
151 proof_handler.MatitaTypes.quit ();
152 Some `Command (* dummy answer, useless *)
153 | TacticAst.Command TacticAst.Proof ->
154 (* do nothing, just for compatibility with coq syntax *)
156 | tactical -> shared#evalTactical tactical
159 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
160 * names as long as they are available, then it fallbacks to name generation
161 * using FreshNamesGenerator module *)
163 let len = List.length names in
165 fun metasenv context name ~typ ->
166 if !count < len then begin
167 let name = Cic.Name (List.nth names !count) in
171 FreshNamesGenerator.mk_fresh_name metasenv context name ~typ
173 (** Implements phrases that should be accepted only in `Proof state, basically
176 ~(disambiguator: MatitaTypes.disambiguator)
177 ~(proof_handler: MatitaTypes.proof_handler)
178 ~(console: MatitaConsole.console)
181 let disambiguate ast =
182 let (_, _, term) = disambiguate ~disambiguator ~proof_handler ast in
185 (** tactic AST -> ProofEngineTypes.tactic *)
186 let rec lookup_tactic = function
187 | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic
188 | TacticAst.Intros (_, names) -> (* TODO Zack implement intros length *)
189 PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
190 | TacticAst.Reflexivity -> EqualityTactics.reflexivity_tac
191 | TacticAst.Assumption -> VariousTactics.assumption_tac
192 | TacticAst.Contradiction -> NegationTactics.contradiction_tac
193 | TacticAst.Exists -> IntroductionTactics.exists_tac
194 | TacticAst.Fourier -> FourierR.fourier_tac
195 | TacticAst.Left -> IntroductionTactics.left_tac
196 | TacticAst.Right -> IntroductionTactics.right_tac
197 | TacticAst.Ring -> Ring.ring_tac
198 | TacticAst.Split -> IntroductionTactics.split_tac
199 | TacticAst.Symmetry -> EqualityTactics.symmetry_tac
200 | TacticAst.Transitivity term ->
201 EqualityTactics.transitivity_tac (disambiguate term)
202 | TacticAst.Apply term -> PrimitiveTactics.apply_tac (disambiguate term)
203 | TacticAst.Absurd term -> NegationTactics.absurd_tac (disambiguate term)
204 | TacticAst.Exact term -> PrimitiveTactics.exact_tac (disambiguate term)
205 | TacticAst.Cut term -> PrimitiveTactics.cut_tac (disambiguate term)
206 | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *)
207 PrimitiveTactics.elim_intros_simpl_tac (disambiguate term)
208 | TacticAst.ElimType term ->
209 EliminationTactics.elim_type_tac (disambiguate term)
210 | TacticAst.Replace (what, with_what) ->
211 EqualityTactics.replace_tac ~what:(disambiguate what)
212 ~with_what:(disambiguate with_what)
214 (* TODO Zack a lot more of tactics to be implemented here ... *)
215 | TacticAst.Change of 'term * 'term * 'ident option
216 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
217 | TacticAst.Decompose of 'ident * 'ident list
218 | TacticAst.Discriminate of 'ident
219 | TacticAst.Fold of reduction_kind * 'term
220 | TacticAst.Injection of 'ident
221 | TacticAst.LetIn of 'term * 'ident
222 | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
223 | TacticAst.Replace_pattern of 'term pattern * 'term
224 | TacticAst.Rewrite of direction * 'term * 'ident option
227 MatitaTypes.not_implemented "some tactic"
229 let shared = new sharedState ~disambiguator ~proof_handler ~console () in
231 inherit interpreterState ~console
233 method evalTactical = function
234 | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
235 | TacticAst.Command TacticAst.Abort ->
236 proof_handler.MatitaTypes.abort_proof ();
238 | TacticAst.Command (TacticAst.Undo steps) ->
239 (proof_handler.MatitaTypes.get_proof ())#undo ?steps ();
241 | TacticAst.Command (TacticAst.Redo steps) ->
242 (proof_handler.MatitaTypes.get_proof ())#redo ?steps ();
244 | TacticAst.Command (TacticAst.Qed name_opt) ->
245 (* TODO Zack this function probably should not simply fail with
246 * Failure, but rather raise some more meaningful exception *)
247 if not (proof_handler.MatitaTypes.has_proof ()) then assert false;
248 let proof = proof_handler.MatitaTypes.get_proof () in
251 | Some name -> proof#set_uri (uri name));
252 let (uri, metasenv, bo, ty) = proof#proof in
253 let uri = MatitaTypes.unopt_uri uri in
254 if metasenv <> [] then failwith "Proof not completed";
255 let proved_ty = CicTypeChecker.type_of_aux' [] [] bo in
256 if not (CicReduction.are_convertible [] proved_ty ty) then
257 failwith "Wrong proof";
258 (* TODO Zack [] probably wrong *)
259 CicEnvironment.add_type_checked_term uri
260 (Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[]));
261 proof_handler.MatitaTypes.set_proof None;
262 (* TODO Zack a lot more to be done here:
263 * - save object to disk in xml format
265 * - register uri to the getter *)
267 | TacticAst.Seq tacticals ->
268 (* TODO Zack check for proof completed at each step? *)
269 List.iter (fun t -> ignore (self#evalTactical t)) tacticals;
271 | TacticAst.Tactic tactic_phrase ->
272 let tactic = lookup_tactic tactic_phrase in
273 (proof_handler.MatitaTypes.get_proof ())#apply_tactic tactic;
275 | tactical -> shared#evalTactical tactical
279 ~(disambiguator: MatitaTypes.disambiguator)
280 ~(proof_handler: MatitaTypes.proof_handler)
281 ~(console: MatitaConsole.console)
285 new commandState ~disambiguator ~proof_handler ~console ()
287 let proofState = new proofState ~disambiguator ~proof_handler ~console () in
289 val mutable state = commandState
291 method reset = state <- commandState
293 method evalPhrase s =
295 (match state#evalPhrase s with
296 | Some `Command -> state <- commandState
297 | Some `Proof -> state <- proofState
300 console#echo_error (sprintf "Uncaught exception: %s"
301 (Printexc.to_string exn))