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)
90 let check_widget: MatitaTypes.sequent_viewer lazy_t = lazy
91 (let gui = MatitaGui.instance () in
92 MatitaMathView.sequent_viewer ~show:true ~packing:gui#check#scrolledCheck#add
95 (** Implements phrases that should be accepted in all states *)
97 ~(disambiguator: MatitaTypes.disambiguator)
98 ~(proof_handler: MatitaTypes.proof_handler)
99 ~(console: MatitaConsole.console)
103 inherit interpreterState ~console
104 method evalTactical = function
105 | TacticAst.Command TacticAst.Quit ->
106 proof_handler.MatitaTypes.quit ();
107 Some `Command (* dummy answer, useless *)
108 | TacticAst.Command TacticAst.Proof ->
109 (* do nothing, just for compatibility with coq syntax *)
111 | TacticAst.Command (TacticAst.Check term) ->
112 let (_, _, term) = disambiguate ~disambiguator ~proof_handler term in
113 let (context, metasenv) = get_context_and_metasenv proof_handler in
114 let dummyno = CicMkImplicit.new_meta metasenv [] in
115 let ty = CicTypeChecker.type_of_aux' metasenv context term in
116 let expr = Cic.Cast (term, ty) in
117 let sequent = (dummyno, context, expr) in
118 let widget = Lazy.force check_widget in
119 let gui = MatitaGui.instance () in
120 gui#check#checkWin#show ();
121 gui#main#showCheckMenuItem#set_active true;
122 widget#load_sequent (sequent::metasenv) dummyno;
125 raise (Command_error (TacticAstPp.pp_tactical tactical))
128 (** Implements phrases that should be accepted only in `Command state *)
130 ~(disambiguator: MatitaTypes.disambiguator)
131 ~(proof_handler: MatitaTypes.proof_handler)
132 ~(console: MatitaConsole.console)
135 let shared = new sharedState ~disambiguator ~proof_handler ~console () in
137 inherit interpreterState ~console
139 method evalTactical = function
140 | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
141 | TacticAst.Command (TacticAst.Theorem (_, name_opt, ast, None)) ->
142 let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
146 | Some name -> Some (uri name)
148 let proof = MatitaProof.proof ~typ:expr ?uri ~metasenv () in
149 proof_handler.MatitaTypes.new_proof proof;
151 | TacticAst.Command TacticAst.Quit ->
152 proof_handler.MatitaTypes.quit ();
153 Some `Command (* dummy answer, useless *)
154 | TacticAst.Command TacticAst.Proof ->
155 (* do nothing, just for compatibility with coq syntax *)
157 | tactical -> shared#evalTactical tactical
160 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
161 * names as long as they are available, then it fallbacks to name generation
162 * using FreshNamesGenerator module *)
164 let len = List.length names in
166 fun metasenv context name ~typ ->
167 if !count < len then begin
168 let name = Cic.Name (List.nth names !count) in
172 FreshNamesGenerator.mk_fresh_name metasenv context name ~typ
174 (** Implements phrases that should be accepted only in `Proof state, basically
177 ~(disambiguator: MatitaTypes.disambiguator)
178 ~(proof_handler: MatitaTypes.proof_handler)
179 ~(console: MatitaConsole.console)
182 let disambiguate ast =
183 let (_, _, term) = disambiguate ~disambiguator ~proof_handler ast in
186 (** tactic AST -> ProofEngineTypes.tactic *)
187 let rec lookup_tactic = function
188 | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic
189 | TacticAst.Intros (_, names) -> (* TODO Zack implement intros length *)
190 PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
191 | TacticAst.Reflexivity -> Tactics.reflexivity
192 | TacticAst.Assumption -> Tactics.assumption
193 | TacticAst.Contradiction -> Tactics.contradiction
194 | TacticAst.Exists -> Tactics.exists
195 | TacticAst.Fourier -> Tactics.fourier
196 | TacticAst.Left -> Tactics.left
197 | TacticAst.Right -> Tactics.right
198 | TacticAst.Ring -> Tactics.ring
199 | TacticAst.Split -> Tactics.split
200 | TacticAst.Symmetry -> Tactics.symmetry
201 | TacticAst.Transitivity term -> Tactics.transitivity (disambiguate term)
202 | TacticAst.Apply term -> Tactics.apply (disambiguate term)
203 | TacticAst.Absurd term -> Tactics.absurd (disambiguate term)
204 | TacticAst.Exact term -> Tactics.exact (disambiguate term)
205 | TacticAst.Cut term -> Tactics.cut (disambiguate term)
206 | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *)
207 Tactics.elim_intros_simpl (disambiguate term)
208 | TacticAst.ElimType term -> Tactics.elim_type (disambiguate term)
209 | TacticAst.Replace (what, with_what) ->
210 Tactics.replace ~what:(disambiguate what)
211 ~with_what:(disambiguate with_what)
213 (* TODO Zack a lot more of tactics to be implemented here ... *)
214 | TacticAst.Change of 'term * 'term * 'ident option
215 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
216 | TacticAst.Decompose of 'ident * 'ident list
217 | TacticAst.Discriminate of 'ident
218 | TacticAst.Fold of reduction_kind * 'term
219 | TacticAst.Injection of 'ident
220 | TacticAst.LetIn of 'term * 'ident
221 | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
222 | TacticAst.Replace_pattern of 'term pattern * 'term
223 | TacticAst.Rewrite of direction * 'term * 'ident option
226 MatitaTypes.not_implemented "some tactic"
228 let shared = new sharedState ~disambiguator ~proof_handler ~console () in
230 inherit interpreterState ~console
232 method evalTactical = function
233 | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
234 | TacticAst.Command TacticAst.Abort ->
235 proof_handler.MatitaTypes.abort_proof ();
237 | TacticAst.Command (TacticAst.Undo steps) ->
238 (proof_handler.MatitaTypes.get_proof ())#undo ?steps ();
240 | TacticAst.Command (TacticAst.Redo steps) ->
241 (proof_handler.MatitaTypes.get_proof ())#redo ?steps ();
243 | TacticAst.Command (TacticAst.Qed name_opt) ->
244 (* TODO Zack this function probably should not simply fail with
245 * Failure, but rather raise some more meaningful exception *)
246 if not (proof_handler.MatitaTypes.has_proof ()) then assert false;
247 let proof = proof_handler.MatitaTypes.get_proof () in
250 | Some name -> proof#set_uri (uri name));
251 let (uri, metasenv, bo, ty) = proof#proof in
252 let uri = MatitaTypes.unopt_uri uri in
253 if metasenv <> [] then failwith "Proof not completed";
254 let proved_ty = CicTypeChecker.type_of_aux' [] [] bo in
255 if not (CicReduction.are_convertible [] proved_ty ty) then
256 failwith "Wrong proof";
257 (* TODO Zack [] probably wrong *)
258 CicEnvironment.add_type_checked_term uri
259 (Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[]));
260 proof_handler.MatitaTypes.set_proof None;
261 (* TODO Zack a lot more to be done here:
262 * - save object to disk in xml format
264 * - register uri to the getter *)
266 | TacticAst.Seq tacticals ->
267 (* TODO Zack check for proof completed at each step? *)
268 List.iter (fun t -> ignore (self#evalTactical t)) tacticals;
270 | TacticAst.Tactic tactic_phrase ->
271 let tactic = lookup_tactic tactic_phrase in
272 (proof_handler.MatitaTypes.get_proof ())#apply_tactic tactic;
274 | tactical -> shared#evalTactical tactical
278 ~(disambiguator: MatitaTypes.disambiguator)
279 ~(proof_handler: MatitaTypes.proof_handler)
280 ~(console: MatitaConsole.console)
284 new commandState ~disambiguator ~proof_handler ~console ()
286 let proofState = new proofState ~disambiguator ~proof_handler ~console () in
288 val mutable state = commandState
290 method reset = state <- commandState
292 method private updateState = function
293 | Some `Command -> state <- commandState
294 | Some `Proof -> state <- proofState
297 method evalPhrase s =
299 self#updateState (state#evalPhrase s)
301 console#echo_error (sprintf "Uncaught exception: %s"
302 (Printexc.to_string exn))
306 let get_end_pos = function
307 | TacticAst.LocatedTactical ((_, end_pos), _) -> end_pos.Lexing.pos_cnum
310 let str_len = String.length s in
313 self#parsePhrase (String.sub s offset (str_len - offset))
315 self#updateState (state#evalTactical tactical);
316 let next_offset = get_end_pos tactical + offset in
317 if next_offset = str_len - 1 then