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 (_, None, names) ->
23 (* TODO Zack implement intros length *)
24 PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
25 | TacticAst.Intros (_, Some num, names) ->
26 (* TODO Zack implement intros length *)
27 PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) ()
28 | TacticAst.Reflexivity _ -> Tactics.reflexivity
29 | TacticAst.Assumption _ -> Tactics.assumption
30 | TacticAst.Contradiction _ -> Tactics.contradiction
31 | TacticAst.Exists _ -> Tactics.exists
32 | TacticAst.Fourier _ -> Tactics.fourier
33 | TacticAst.Goal (_, n) -> Tactics.set_goal n
34 | TacticAst.Left _ -> Tactics.left
35 | TacticAst.Right _ -> Tactics.right
36 | TacticAst.Ring _ -> Tactics.ring
37 | TacticAst.Split _ -> Tactics.split
38 | TacticAst.Symmetry _ -> Tactics.symmetry
39 | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
40 | TacticAst.Apply (_, term) -> Tactics.apply term
41 | TacticAst.Absurd (_, term) -> Tactics.absurd term
42 | TacticAst.Exact (_, term) -> Tactics.exact term
43 | TacticAst.Cut (_, term) -> Tactics.cut term
44 | TacticAst.Elim (_, term, _) ->
45 (* TODO Zack implement "using" argument *)
46 (* old: Tactics.elim_intros_simpl term *)
47 Tactics.elim_intros term
48 | TacticAst.ElimType (_, term) -> Tactics.elim_type term
49 | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
50 | TacticAst.Auto (_,num) ->
51 AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ())
52 | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
54 (* TODO Zack a lot more of tactics to be implemented here ... *)
55 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
56 | TacticAst.Change of 'term * 'term * 'ident option
57 | TacticAst.Decompose of 'ident * 'ident list
58 | TacticAst.Discriminate of 'ident
59 | TacticAst.Fold of reduction_kind * 'term
60 | TacticAst.Injection of 'ident
61 | TacticAst.LetIn of 'term * 'ident
62 | TacticAst.Replace_pattern of 'term pattern * 'term
64 | TacticAst.Reduce (_,reduction_kind,opts) ->
65 let terms, also_in_hypotheses =
67 | Some (l,`Goal) -> Some l, false
68 | Some (l,`Everywhere) -> Some l, true
71 (match reduction_kind with
72 | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms
73 | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms
74 | `Whd -> Tactics.whd ~also_in_hypotheses ~terms)
75 | TacticAst.Rewrite (_,dir,t,ident) ->
77 EqualityTactics.rewrite_tac ~term:t
79 EqualityTactics.rewrite_back_tac ~term:t
82 let eval_tactical status tac =
83 let apply_tactic tactic =
85 ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
90 let (_,metasenv,_,_) = proof in
93 | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
94 | ng::_ -> Incomplete_proof (proof, ng)
96 { status with proof_status = new_status }
98 let rec tactical_of_ast = function
99 | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
100 | TacticAst.Fail loc -> Tacticals.fail
101 | TacticAst.Do (loc, num, tactical) ->
102 Tacticals.do_tactic num (tactical_of_ast tactical)
103 | TacticAst.IdTac loc -> Tacticals.id_tac
104 | TacticAst.Repeat (loc, tactical) ->
105 Tacticals.repeat_tactic (tactical_of_ast tactical)
106 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
107 Tacticals.seq (List.map tactical_of_ast tacticals)
108 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
109 Tacticals.thens (tactical_of_ast tactical)
110 (List.map tactical_of_ast tacticals)
111 | TacticAst.Tries (loc, tacticals) ->
112 Tacticals.try_tactics
113 (List.map (fun t -> "", tactical_of_ast t) tacticals)
114 | TacticAst.Try (loc, tactical) ->
115 Tacticals.try_tactic (tactical_of_ast tactical)
117 apply_tactic (tactical_of_ast tac)
119 (** given a uri and a type list (the contructors types) builds a list of pairs
120 * (name,uri) that is used to generate authomatic aliases **)
121 let extract_alias types uri =
123 fun (acc,i) (name, _, _, cl) ->
124 ((name, UriManager.string_of_uriref (uri,[i]))
126 (fst(List.fold_left (
127 fun (acc,j) (name,_) ->
128 (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1)
132 (** adds a (name,uri) list l to a disambiguation environment e **)
133 let env_of_list l e =
134 let module DT = DisambiguateTypes in
135 let module DTE = DisambiguateTypes.Environment in
140 (uri,fun _ _ _ -> CicUtil.term_of_uri uri)
144 let eval_command status cmd =
146 | TacticAst.Set (loc, name, value) -> set_option status name value
147 | TacticAst.Qed loc ->
148 let uri, metasenv, bo, ty =
149 match status.proof_status with
150 | Proof (Some uri, metasenv, body, ty) ->
151 uri, metasenv, body, ty
152 | Proof (None, metasenv, body, ty) ->
154 ("Someone allows to start a thm without giving the "^
155 "name/uri. This should be fixed!")
156 | _-> command_error "You can't qed an uncomplete theorem"
158 let suri = UriManager.string_of_uri uri in
159 if metasenv <> [] then
160 command_error "Proof not completed! metasenv is not empty!";
161 let proved_ty,ugraph =
162 CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
165 CicReduction.are_convertible [] proved_ty ty ugraph
169 ("The type of your proof is not convertible with the "^
170 "type you've declared!");
171 MatitaLog.message (sprintf "%s defined" suri);
172 let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
174 let name = UriManager.name_of_uri uri in
175 let new_env = env_of_list [(name,suri)] status.aliases in
176 {status with aliases = new_env }
178 {status with proof_status = No_proof }
179 | TacticAst.Inductive (loc, dummy_params, types) ->
180 (* dummy_params are not real params, it is a list of nothing, and the only
181 * semantic content is the len, that is leftno (note: leftno and pamaters
182 * have nothing in common).
186 | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
189 let uri = UriManager.uri_of_string suri in
190 let leftno = List.length dummy_params in
191 let obj = Cic.InductiveDefinition (types, [], leftno, []) in
193 CicTypeChecker.typecheck_mutual_inductive_defs uri
194 (types, [], leftno) CicUniv.empty_ugraph
197 MatitaSync.add_inductive_def
198 ~uri ~types ~params:[] ~leftno ~ugraph status
200 (* aliases for the constructors and types *)
201 let aliases = env_of_list (extract_alias types uri) status.aliases in
202 (* aliases for the eliminations principles *)
204 let base = String.sub suri 0 (String.length suri - 4) in
209 fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix
210 ) status.objects then
211 let u = base ^ suffix in
212 (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc
215 ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases
217 let status = {status with proof_status = No_proof } in
218 { status with aliases = aliases}
219 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
221 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
225 match status.proof_status with
226 | Intermediate metasenv ->
227 ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
230 let initial_proof = (Some uri, metasenv, body, ty) in
231 { status with proof_status = Incomplete_proof (initial_proof,goalno)}
232 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
234 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
236 let metasenv = MatitaMisc.get_proof_metasenv status in
237 let (body_type, ugraph) =
238 CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
240 let (subst, metasenv, ugraph) =
241 CicUnification.fo_unif metasenv [] body_type ty ugraph
243 if metasenv <> [] then
245 "metasenv not empty while giving a definition with body";
246 let body = CicMetaSubst.apply_subst subst body in
247 let ty = CicMetaSubst.apply_subst subst ty in
248 let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
250 let suri = UriManager.string_of_uri uri in
251 let new_env = env_of_list [(name,suri)] status.aliases in
252 {status with aliases = new_env }
254 {status with proof_status = No_proof}
255 | TacticAst.Theorem (_, _, None, _, _) ->
256 command_error "The grammas should avoid having unnamed theorems!"
257 | TacticAst.Coercion (loc, term) -> assert false (** TODO *)
258 | TacticAst.Alias (loc, spec) ->
260 | TacticAst.Ident_alias (id,uri) ->
261 {status with aliases =
262 DisambiguateTypes.Environment.add
263 (DisambiguateTypes.Id id)
264 ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
266 | TacticAst.Symbol_alias (symb, instance, desc) ->
267 {status with aliases =
268 DisambiguateTypes.Environment.add
269 (DisambiguateTypes.Symbol (symb,instance))
270 (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
272 | TacticAst.Number_alias (instance,desc) ->
273 {status with aliases =
274 DisambiguateTypes.Environment.add
275 (DisambiguateTypes.Num instance)
276 (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
278 let eval_executable status ex =
280 | TacticAst.Tactical (_, tac) -> eval_tactical status tac
281 | TacticAst.Command (_, cmd) -> eval_command status cmd
282 | TacticAst.Macro (_, mac) ->
283 command_error (sprintf "The macro %s can't be in a script"
284 (TacticAstPp.pp_macro_cic mac))
286 let eval_comment status c = status
290 | TacticAst.Executable (_,ex) -> eval_executable status ex
291 | TacticAst.Comment (_,c) -> eval_comment status c
293 let disambiguate_term status term =
294 let (aliases, metasenv, cic, _) =
296 MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
297 ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
298 ~metasenv:(MatitaMisc.get_proof_metasenv status) term
304 match status.proof_status with
305 | No_proof -> Intermediate metasenv
306 | Incomplete_proof ((uri, _, proof, ty), goal) ->
307 Incomplete_proof ((uri, metasenv, proof, ty), goal)
308 | Intermediate _ -> Intermediate metasenv
309 | Proof _ -> assert false
314 proof_status = proof_status }
318 let disambiguate_terms status terms =
319 let term = CicAst.pack terms in
320 let status, term = disambiguate_term status term in
321 status, CicUtil.unpack term
323 let disambiguate_tactic status = function
324 | TacticAst.Transitivity (loc, term) ->
325 let status, cic = disambiguate_term status term in
326 status, TacticAst.Transitivity (loc, cic)
327 | TacticAst.Apply (loc, term) ->
328 let status, cic = disambiguate_term status term in
329 status, TacticAst.Apply (loc, cic)
330 | TacticAst.Absurd (loc, term) ->
331 let status, cic = disambiguate_term status term in
332 status, TacticAst.Absurd (loc, cic)
333 | TacticAst.Exact (loc, term) ->
334 let status, cic = disambiguate_term status term in
335 status, TacticAst.Exact (loc, cic)
336 | TacticAst.Cut (loc, term) ->
337 let status, cic = disambiguate_term status term in
338 status, TacticAst.Cut (loc, cic)
339 | TacticAst.Elim (loc, term, Some term') ->
340 let status, cic1 = disambiguate_term status term in
341 let status, cic2 = disambiguate_term status term' in
342 status, TacticAst.Elim (loc, cic1, Some cic2)
343 | TacticAst.Elim (loc, term, None) ->
344 let status, cic = disambiguate_term status term in
345 status, TacticAst.Elim (loc, cic, None)
346 | TacticAst.ElimType (loc, term) ->
347 let status, cic = disambiguate_term status term in
348 status, TacticAst.ElimType (loc, cic)
349 | TacticAst.Replace (loc, what, with_what) ->
350 let status, cic1 = disambiguate_term status what in
351 let status, cic2 = disambiguate_term status with_what in
352 status, TacticAst.Replace (loc, cic1, cic2)
353 | TacticAst.Change (loc, what, with_what, ident) ->
354 let status, cic1 = disambiguate_term status what in
355 let status, cic2 = disambiguate_term status with_what in
356 status, TacticAst.Change (loc, cic1, cic2, ident)
358 (* TODO Zack a lot more of tactics to be implemented here ... *)
359 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
360 | TacticAst.Change of 'term * 'term * 'ident option
361 | TacticAst.Decompose of 'ident * 'ident list
362 | TacticAst.Discriminate of 'ident
363 | TacticAst.Fold of reduction_kind * 'term
364 | TacticAst.Injection of 'ident
365 | TacticAst.LetIn of 'term * 'ident
366 | TacticAst.Replace_pattern of 'term pattern * 'term
368 | TacticAst.Reduce (loc, reduction_kind, opts) ->
371 | None -> status, None
374 List.fold_right (fun t (status,acc) ->
375 let status',t' = disambiguate_term status t in
379 status, Some (l, pat)
381 status, TacticAst.Reduce (loc, reduction_kind, opts)
382 | TacticAst.Rewrite (loc,dir,t,ident) ->
383 let status, term = disambiguate_term status t in
384 status, TacticAst.Rewrite (loc,dir,term,ident)
385 | TacticAst.Intros (loc, num, names) ->
386 status, TacticAst.Intros (loc, num, names)
387 | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
388 | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
389 | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
390 | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
391 | TacticAst.Exists loc -> status, TacticAst.Exists loc
392 | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
393 | TacticAst.Left loc -> status, TacticAst.Left loc
394 | TacticAst.Right loc -> status, TacticAst.Right loc
395 | TacticAst.Ring loc -> status, TacticAst.Ring loc
396 | TacticAst.Split loc -> status, TacticAst.Split loc
397 | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
398 | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
400 print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
403 let rec disambiguate_tactical status = function
404 | TacticAst.Tactic (loc, tactic) ->
405 let status, tac = disambiguate_tactic status tactic in
406 status, TacticAst.Tactic (loc, tac)
407 | TacticAst.Do (loc, num, tactical) ->
408 let status, tac = disambiguate_tactical status tactical in
409 status, TacticAst.Do (loc, num, tac)
410 | TacticAst.Repeat (loc, tactical) ->
411 let status, tac = disambiguate_tactical status tactical in
412 status, TacticAst.Repeat (loc, tac)
413 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
414 let status, tacticals = disambiguate_tacticals status tacticals in
415 let tacticals = List.rev tacticals in
416 status, TacticAst.Seq (loc, tacticals)
417 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
418 let status, tactical = disambiguate_tactical status tactical in
419 let status, tacticals = disambiguate_tacticals status tacticals in
420 status, TacticAst.Then (loc, tactical, tacticals)
421 | TacticAst.Tries (loc, tacticals) ->
422 let status, tacticals = disambiguate_tacticals status tacticals in
423 status, TacticAst.Tries (loc, tacticals)
424 | TacticAst.Try (loc, tactical) ->
425 let status, tactical = disambiguate_tactical status tactical in
426 status, TacticAst.Try (loc, tactical)
427 | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
430 and disambiguate_tacticals status tacticals =
431 let status, tacticals =
433 (fun (status, tacticals) tactical ->
434 let status, tac = disambiguate_tactical status tactical in
435 status, tac :: tacticals)
439 let tacticals = List.rev tacticals in
442 let disambiguate_inddef status params indTypes =
443 let add_pi binders t =
445 (fun (name, ast) acc ->
446 CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
450 List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
452 let binders = ind_binders @ params in
454 let add_ast ast = asts := ast :: !asts in
455 let paramsno = List.length params in
456 let indbindersno = List.length ind_binders in
458 (fun (name, _, typ, constructors) ->
459 add_ast (add_pi params typ);
460 List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
462 let status, terms = disambiguate_terms status !asts in
463 let terms = ref (List.rev terms) in
465 match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
469 | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
473 let counter = ref 0 in
477 CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
480 let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
483 (fun acc (name, inductive, typ, constructors) ->
484 let cicTyp = get_term () in
485 let cicConstructors =
487 (fun acc (name, _) ->
489 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
494 (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
497 let cicIndTypes = List.rev cicIndTypes in
498 status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
500 let disambiguate_command status = function
501 | TacticAst.Inductive (loc, params, types) ->
502 let (status, (uri, (ind_types, vars, paramsno))) =
503 disambiguate_inddef status params types
505 let rec mk_list = function
507 | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
509 (* once we've built the cic inductive types we no longer need terms
510 corresponding to parameters, but we need the leftno, and we encode
511 it as the length of dummy_params
513 let dummy_params = mk_list paramsno in
514 status, TacticAst.Inductive (loc, dummy_params, ind_types)
515 | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
516 let status, ty = disambiguate_term status ty in
519 | None -> status, None
521 let status, body = disambiguate_term status body in
524 status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
525 | TacticAst.Coercion (loc, term) -> assert false (** TODO *)
526 | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
528 | TacticAst.Alias _ as x -> status, x
530 let disambiguate_executable status ex =
532 | TacticAst.Tactical (loc, tac) ->
533 let status, tac = disambiguate_tactical status tac in
534 status, (TacticAst.Tactical (loc, tac))
535 | TacticAst.Command (loc, cmd) ->
536 let status, cmd = disambiguate_command status cmd in
537 status, (TacticAst.Command (loc, cmd))
538 | TacticAst.Macro (_, mac) ->
540 (sprintf ("The engine is not allowed to disambiguate any macro, "^^
541 "in particular %s") (TacticAstPp.pp_macro_ast mac))
543 let disambiguate_comment status c =
545 | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
546 | TacticAst.Code (loc,ex) ->
547 let status, ex = disambiguate_executable status ex in
548 status, TacticAst.Code (loc,ex)
550 let disambiguate_statement status statement =
552 | TacticAst.Comment (loc,c) ->
553 let status, c = disambiguate_comment status c in
554 status, TacticAst.Comment (loc,c)
555 | TacticAst.Executable (loc,ex) ->
556 let status, ex = disambiguate_executable status ex in
557 status, TacticAst.Executable (loc,ex)
559 let eval_ast status ast =
560 let status,st = disambiguate_statement status ast in
561 (* this disambiguation step should be deferred to support tacticals *)
564 let eval_from_stream status str cb =
565 let stl = CicTextualParser2.parse_statements str in
567 (fun status ast -> cb status ast;eval_ast status ast) status
570 let eval_string status str =
571 eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
573 let default_options () =
575 StringMap.add "baseuri"
577 (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
581 StringMap.add "basedir"
582 (String (Helm_registry.get "matita.basedir" ))
589 aliases = DisambiguateTypes.empty_environment;
590 proof_status = No_proof;
591 options = default_options ();