7 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
8 * names as long as they are available, then it fallbacks to name generation
9 * using FreshNamesGenerator module *)
11 let len = List.length names in
13 fun metasenv context name ~typ ->
14 if !count < len then begin
15 let name = Cic.Name (List.nth names !count) in
19 FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
21 let tactic_of_ast = function
22 | TacticAst.Intros (_, _, names) ->
23 (* TODO Zack implement intros length *)
24 PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
25 | TacticAst.Reflexivity _ -> Tactics.reflexivity
26 | TacticAst.Assumption _ -> Tactics.assumption
27 | TacticAst.Contradiction _ -> Tactics.contradiction
28 | TacticAst.Exists _ -> Tactics.exists
29 | TacticAst.Fourier _ -> Tactics.fourier
30 | TacticAst.Goal (_, n) -> Tactics.set_goal n
31 | TacticAst.Left _ -> Tactics.left
32 | TacticAst.Right _ -> Tactics.right
33 | TacticAst.Ring _ -> Tactics.ring
34 | TacticAst.Split _ -> Tactics.split
35 | TacticAst.Symmetry _ -> Tactics.symmetry
36 | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
37 | TacticAst.Apply (_, term) -> Tactics.apply term
38 | TacticAst.Absurd (_, term) -> Tactics.absurd term
39 | TacticAst.Exact (_, term) -> Tactics.exact term
40 | TacticAst.Cut (_, term) -> Tactics.cut term
41 | TacticAst.Elim (_, term, _) ->
42 (* TODO Zack implement "using" argument *)
43 Tactics.elim_intros_simpl term
44 | TacticAst.ElimType (_, term) -> Tactics.elim_type term
45 | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
46 | TacticAst.Auto (_,num) ->
47 AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ())
48 | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
50 (* TODO Zack a lot more of tactics to be implemented here ... *)
51 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
52 | TacticAst.Change of 'term * 'term * 'ident option
53 | TacticAst.Decompose of 'ident * 'ident list
54 | TacticAst.Discriminate of 'ident
55 | TacticAst.Fold of reduction_kind * 'term
56 | TacticAst.Injection of 'ident
57 | TacticAst.LetIn of 'term * 'ident
58 | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
59 | TacticAst.Replace_pattern of 'term pattern * 'term
61 | TacticAst.Rewrite (_,dir,t,ident) ->
63 EqualityTactics.rewrite_tac ~term:t
65 EqualityTactics.rewrite_back_tac ~term:t
68 let eval_tactical status tac =
69 let apply_tactic tactic =
71 ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
76 let (_,metasenv,_,_) = proof in
79 | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
80 | ng::_ -> Incomplete_proof (proof, ng)
82 { status with proof_status = new_status }
84 let rec tactical_of_ast = function
85 | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
86 | TacticAst.Fail loc -> Tacticals.fail
87 | TacticAst.Do (loc, num, tactical) ->
88 Tacticals.do_tactic num (tactical_of_ast tactical)
89 | TacticAst.IdTac loc -> Tacticals.id_tac
90 | TacticAst.Repeat (loc, tactical) ->
91 Tacticals.repeat_tactic (tactical_of_ast tactical)
92 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
93 Tacticals.seq (List.map tactical_of_ast tacticals)
94 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
95 Tacticals.thens (tactical_of_ast tactical)
96 (List.map tactical_of_ast tacticals)
97 | TacticAst.Tries (loc, tacticals) ->
99 (List.map (fun t -> "", tactical_of_ast t) tacticals)
100 | TacticAst.Try (loc, tactical) ->
101 Tacticals.try_tactic (tactical_of_ast tactical)
103 apply_tactic (tactical_of_ast tac)
105 let eval_command status cmd =
107 | TacticAst.Set (loc, name, value) -> set_option status name value
108 | TacticAst.Qed loc ->
109 let uri, metasenv, bo, ty =
110 match status.proof_status with
111 | Proof (Some uri, metasenv, body, ty) ->
112 uri, metasenv, body, ty
113 | Proof (None, metasenv, body, ty) ->
115 ("Someone allows to start a thm without giving the "^
116 "name/uri. This should be fixed!")
117 | _-> command_error "You can't qed an uncomplete theorem"
119 let suri = UriManager.string_of_uri uri in
120 if metasenv <> [] then
121 command_error "Proof not completed! metasenv is not empty!";
122 let proved_ty,ugraph =
123 CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
126 CicReduction.are_convertible [] proved_ty ty ugraph
130 ("The type of your proof is not convertible with the "^
131 "type you've declared!");
132 MatitaLog.message (sprintf "%s defined" suri);
133 let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
134 {status with proof_status = No_proof }
135 | TacticAst.Inductive (loc, dummy_params, types) ->
136 (* dummy_params are not real params, it is a list of nothing, and the only
137 * semantic content is the len, that is leftno (note: leftno and pamaters
138 * have nothing in common).
142 | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
145 let uri = UriManager.uri_of_string suri in
146 let leftno = List.length dummy_params in
147 let obj = Cic.InductiveDefinition (types, [], leftno, []) in
149 CicTypeChecker.typecheck_mutual_inductive_defs uri
150 (types, [], leftno) CicUniv.empty_ugraph
152 MatitaSync.add_inductive_def
153 ~uri ~types ~params:[] ~leftno ~ugraph status;
154 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
156 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
160 match status.proof_status with
161 | Intermediate metasenv ->
162 ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
165 let initial_proof = (Some uri, metasenv, body, ty) in
166 { status with proof_status = Incomplete_proof (initial_proof,goalno)}
167 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
169 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
171 let metasenv = MatitaMisc.get_proof_metasenv status in
172 let (body_type, ugraph) =
173 CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
175 let (subst, metasenv, ugraph) =
176 CicUnification.fo_unif metasenv [] body_type ty ugraph
178 if metasenv <> [] then
180 "metasenv not empty while giving a definition with body";
181 let body = CicMetaSubst.apply_subst subst body in
182 let ty = CicMetaSubst.apply_subst subst ty in
183 MatitaSync.add_constant ~uri ~body ~ty ~ugraph status
184 | TacticAst.Theorem (_, _, None, _, _) ->
185 command_error "The grammas should avoid having unnamed theorems!"
186 | TacticAst.Coercion (loc, term) -> assert false (** TODO *)
187 | TacticAst.Alias (loc, spec) ->
189 | TacticAst.Ident_alias (id,uri) ->
190 {status with aliases =
191 DisambiguateTypes.Environment.add
192 (DisambiguateTypes.Id id)
193 ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
195 | TacticAst.Symbol_alias (symb, instance, desc) ->
196 {status with aliases =
197 DisambiguateTypes.Environment.add
198 (DisambiguateTypes.Symbol (symb,instance))
199 (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
201 | TacticAst.Number_alias (instance,desc) ->
202 {status with aliases =
203 DisambiguateTypes.Environment.add
204 (DisambiguateTypes.Num instance)
205 (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
207 let eval_executable status ex =
209 | TacticAst.Tactical (_, tac) -> eval_tactical status tac
210 | TacticAst.Command (_, cmd) -> eval_command status cmd
211 | TacticAst.Macro (_, mac) ->
212 command_error (sprintf "The macro %s can't be in a script"
213 (TacticAstPp.pp_macro_cic mac))
215 let eval_comment status c = status
219 | TacticAst.Executable (_,ex) -> eval_executable status ex
220 | TacticAst.Comment (_,c) -> eval_comment status c
222 let disambiguate_term status term =
223 let (aliases, metasenv, cic, _) =
225 MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
226 ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
227 ~metasenv:(MatitaMisc.get_proof_metasenv status) term
233 match status.proof_status with
234 | No_proof -> Intermediate metasenv
235 | Incomplete_proof ((uri, _, proof, ty), goal) ->
236 Incomplete_proof ((uri, metasenv, proof, ty), goal)
237 | Intermediate _ -> Intermediate metasenv
238 | Proof _ -> assert false
243 proof_status = proof_status }
247 let disambiguate_terms status terms =
248 let term = CicAst.pack terms in
249 let status, term = disambiguate_term status term in
250 status, CicUtil.unpack term
252 let disambiguate_tactic status = function
253 | TacticAst.Transitivity (loc, term) ->
254 let status, cic = disambiguate_term status term in
255 status, TacticAst.Transitivity (loc, cic)
256 | TacticAst.Apply (loc, term) ->
257 let status, cic = disambiguate_term status term in
258 status, TacticAst.Apply (loc, cic)
259 | TacticAst.Absurd (loc, term) ->
260 let status, cic = disambiguate_term status term in
261 status, TacticAst.Absurd (loc, cic)
262 | TacticAst.Exact (loc, term) ->
263 let status, cic = disambiguate_term status term in
264 status, TacticAst.Exact (loc, cic)
265 | TacticAst.Cut (loc, term) ->
266 let status, cic = disambiguate_term status term in
267 status, TacticAst.Cut (loc, cic)
268 | TacticAst.Elim (loc, term, Some term') ->
269 let status, cic1 = disambiguate_term status term in
270 let status, cic2 = disambiguate_term status term' in
271 status, TacticAst.Elim (loc, cic1, Some cic2)
272 | TacticAst.Elim (loc, term, None) ->
273 let status, cic = disambiguate_term status term in
274 status, TacticAst.Elim (loc, cic, None)
275 | TacticAst.ElimType (loc, term) ->
276 let status, cic = disambiguate_term status term in
277 status, TacticAst.ElimType (loc, cic)
278 | TacticAst.Replace (loc, what, with_what) ->
279 let status, cic1 = disambiguate_term status what in
280 let status, cic2 = disambiguate_term status with_what in
281 status, TacticAst.Replace (loc, cic1, cic2)
282 | TacticAst.Change (loc, what, with_what, ident) ->
283 let status, cic1 = disambiguate_term status what in
284 let status, cic2 = disambiguate_term status with_what in
285 status, TacticAst.Change (loc, cic1, cic2, ident)
287 (* TODO Zack a lot more of tactics to be implemented here ... *)
288 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
289 | TacticAst.Change of 'term * 'term * 'ident option
290 | TacticAst.Decompose of 'ident * 'ident list
291 | TacticAst.Discriminate of 'ident
292 | TacticAst.Fold of reduction_kind * 'term
293 | TacticAst.Injection of 'ident
294 | TacticAst.LetIn of 'term * 'ident
295 | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
296 | TacticAst.Replace_pattern of 'term pattern * 'term
298 | TacticAst.Rewrite (loc,dir,t,ident) ->
299 let status, term = disambiguate_term status t in
300 status, TacticAst.Rewrite (loc,dir,term,ident)
301 | TacticAst.Intros (loc, num, names) ->
302 status, TacticAst.Intros (loc, num, names)
303 | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
304 | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
305 | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
306 | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
307 | TacticAst.Exists loc -> status, TacticAst.Exists loc
308 | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
309 | TacticAst.Left loc -> status, TacticAst.Left loc
310 | TacticAst.Right loc -> status, TacticAst.Right loc
311 | TacticAst.Ring loc -> status, TacticAst.Ring loc
312 | TacticAst.Split loc -> status, TacticAst.Split loc
313 | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
314 | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
316 print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
319 let rec disambiguate_tactical status = function
320 | TacticAst.Tactic (loc, tactic) ->
321 let status, tac = disambiguate_tactic status tactic in
322 status, TacticAst.Tactic (loc, tac)
323 | TacticAst.Do (loc, num, tactical) ->
324 let status, tac = disambiguate_tactical status tactical in
325 status, TacticAst.Do (loc, num, tac)
326 | TacticAst.Repeat (loc, tactical) ->
327 let status, tac = disambiguate_tactical status tactical in
328 status, TacticAst.Repeat (loc, tac)
329 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
330 let status, tacticals = disambiguate_tacticals status tacticals in
331 let tacticals = List.rev tacticals in
332 status, TacticAst.Seq (loc, tacticals)
333 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
334 let status, tactical = disambiguate_tactical status tactical in
335 let status, tacticals = disambiguate_tacticals status tacticals in
336 status, TacticAst.Then (loc, tactical, tacticals)
337 | TacticAst.Tries (loc, tacticals) ->
338 let status, tacticals = disambiguate_tacticals status tacticals in
339 status, TacticAst.Tries (loc, tacticals)
340 | TacticAst.Try (loc, tactical) ->
341 let status, tactical = disambiguate_tactical status tactical in
342 status, TacticAst.Try (loc, tactical)
343 | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
346 and disambiguate_tacticals status tacticals =
347 let status, tacticals =
349 (fun (status, tacticals) tactical ->
350 let status, tac = disambiguate_tactical status tactical in
351 status, tac :: tacticals)
355 let tacticals = List.rev tacticals in
358 let disambiguate_inddef status params indTypes =
359 let add_pi binders t =
361 (fun (name, ast) acc ->
362 CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
366 List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
368 let binders = ind_binders @ params in
370 let add_ast ast = asts := ast :: !asts in
371 let paramsno = List.length params in
372 let indbindersno = List.length ind_binders in
374 (fun (name, _, typ, constructors) ->
375 add_ast (add_pi params typ);
376 List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
378 let status, terms = disambiguate_terms status !asts in
379 let terms = ref (List.rev terms) in
381 match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
385 | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
389 let counter = ref 0 in
393 CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
396 let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
399 (fun acc (name, inductive, typ, constructors) ->
400 let cicTyp = get_term () in
401 let cicConstructors =
403 (fun acc (name, _) ->
405 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
410 (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
413 let cicIndTypes = List.rev cicIndTypes in
414 status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
416 let disambiguate_command status = function
417 | TacticAst.Inductive (loc, params, types) ->
418 let (status, (uri, (ind_types, vars, paramsno))) =
419 disambiguate_inddef status params types
421 let rec mk_list = function
423 | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
425 (* once we've built the cic inductive types we no longer need terms
426 corresponding to parameters, but we need the leftno, and we encode
427 it as the length of dummy_params
429 let dummy_params = mk_list paramsno in
430 status, TacticAst.Inductive (loc, dummy_params, ind_types)
431 | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
432 let status, ty = disambiguate_term status ty in
435 | None -> status, None
437 let status, body = disambiguate_term status body in
440 status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
441 | TacticAst.Coercion (loc, term) -> assert false (** TODO *)
442 | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
444 | TacticAst.Alias _ as x -> status, x
446 let disambiguate_executable status ex =
448 | TacticAst.Tactical (loc, tac) ->
449 let status, tac = disambiguate_tactical status tac in
450 status, (TacticAst.Tactical (loc, tac))
451 | TacticAst.Command (loc, cmd) ->
452 let status, cmd = disambiguate_command status cmd in
453 status, (TacticAst.Command (loc, cmd))
454 | TacticAst.Macro (_, mac) ->
456 (sprintf ("The engine is not allowed to disambiguate any macro, "^^
457 "in particular %s") (TacticAstPp.pp_macro_ast mac))
459 let disambiguate_comment status c =
461 | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
462 | TacticAst.Code (loc,ex) ->
463 let status, ex = disambiguate_executable status ex in
464 status, TacticAst.Code (loc,ex)
466 let disambiguate_statement status statement =
468 | TacticAst.Comment (loc,c) ->
469 let status, c = disambiguate_comment status c in
470 status, TacticAst.Comment (loc,c)
471 | TacticAst.Executable (loc,ex) ->
472 let status, ex = disambiguate_executable status ex in
473 status, TacticAst.Executable (loc,ex)
475 let eval_ast status ast =
476 let status,st = disambiguate_statement status ast in
477 (* this disambiguation step should be deferred to support tacticals *)
480 let eval_from_stream status str =
481 let st = CicTextualParser2.parse_statement str in
484 let eval_string status str =
485 eval_from_stream status (Stream.of_string str)
487 let default_options () =
489 StringMap.add "baseuri"
491 (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
495 StringMap.add "basedir"
496 (String (Helm_registry.get "matita.basedir" ))
503 aliases = DisambiguateTypes.empty_environment;
504 proof_status = No_proof;
505 options = default_options ();