6 let debug_print = if debug then prerr_endline else ignore ;;
8 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
9 * names as long as they are available, then it fallbacks to name generation
10 * using FreshNamesGenerator module *)
12 let len = List.length names in
14 fun metasenv context name ~typ ->
15 if !count < len then begin
16 let name = Cic.Name (List.nth names !count) in
20 FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
22 let tactic_of_ast = function
23 | TacticAst.Intros (_, None, names) ->
24 (* TODO Zack implement intros length *)
25 PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
26 | TacticAst.Intros (_, Some num, names) ->
27 (* TODO Zack implement intros length *)
28 PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) ()
29 | TacticAst.Reflexivity _ -> Tactics.reflexivity
30 | TacticAst.Assumption _ -> Tactics.assumption
31 | TacticAst.Contradiction _ -> Tactics.contradiction
32 | TacticAst.Exists _ -> Tactics.exists
33 | TacticAst.Fourier _ -> Tactics.fourier
34 | TacticAst.Goal (_, n) -> Tactics.set_goal n
35 | TacticAst.Left _ -> Tactics.left
36 | TacticAst.Right _ -> Tactics.right
37 | TacticAst.Ring _ -> Tactics.ring
38 | TacticAst.Split _ -> Tactics.split
39 | TacticAst.Symmetry _ -> Tactics.symmetry
40 | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
41 | TacticAst.Apply (_, term) -> Tactics.apply term
42 | TacticAst.Absurd (_, term) -> Tactics.absurd term
43 | TacticAst.Exact (_, term) -> Tactics.exact term
44 | TacticAst.Cut (_, term) -> Tactics.cut term
45 | TacticAst.Elim (_, term, _) ->
46 (* TODO Zack implement "using" argument *)
47 (* old: Tactics.elim_intros_simpl term *)
48 Tactics.elim_intros term
49 | TacticAst.ElimType (_, term) -> Tactics.elim_type term
50 | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
51 | TacticAst.Auto (_,num) ->
52 AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ())
53 | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
55 (* TODO Zack a lot more of tactics to be implemented here ... *)
56 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
57 | TacticAst.Change of 'term * 'term * 'ident option
58 | TacticAst.Decompose of 'ident * 'ident list
59 | TacticAst.Discriminate of 'ident
60 | TacticAst.Fold of reduction_kind * 'term
61 | TacticAst.Injection of 'ident
62 | TacticAst.LetIn of 'term * 'ident
63 | TacticAst.Replace_pattern of 'term pattern * 'term
65 | TacticAst.ReduceAt (_,reduction_kind,ident,path) ->
66 ProofEngineTypes.mk_tactic
67 (fun (((_,metasenv,_,_),goal) as status) ->
68 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
69 let where, also_in_hypotheses =
70 if ident = "goal" then
76 | Some (Cic.Name name,entry) when name = ident -> true
80 Not_found -> raise (ProofEngineTypes.Fail (ident ^ " is not an hypothesis"))
83 | Some (_, Cic.Decl term) -> term
84 | Some (_, Cic.Def (term,ty)) -> term
85 | None -> assert false),true
87 let pointers = CicUtil.select ~term:where ~context:path in
88 (match reduction_kind with
90 ProofEngineTypes.apply_tactic
91 (Tactics.normalize ~also_in_hypotheses ~terms:(Some pointers))
94 ProofEngineTypes.apply_tactic
95 (Tactics.reduce ~also_in_hypotheses ~terms:(Some pointers))
98 ProofEngineTypes.apply_tactic
99 (Tactics.simpl ~also_in_hypotheses ~terms:(Some pointers))
102 ProofEngineTypes.apply_tactic
103 (Tactics.whd ~also_in_hypotheses ~terms:(Some pointers))
105 | TacticAst.Reduce (_,reduction_kind,opts) ->
106 let terms, also_in_hypotheses =
108 | Some (l,`Goal) -> Some l, false
109 | Some (l,`Everywhere) -> Some l, true
110 | None -> None, false
112 (match reduction_kind with
113 | `Normalize -> Tactics.normalize ~also_in_hypotheses ~terms
114 | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms
115 | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms
116 | `Whd -> Tactics.whd ~also_in_hypotheses ~terms)
117 | TacticAst.Rewrite (_,dir,t,ident) ->
119 EqualityTactics.rewrite_tac ~term:t
121 EqualityTactics.rewrite_back_tac ~term:t
124 let eval_tactical status tac =
125 let apply_tactic tactic =
127 ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
132 let (_,metasenv,_,_) = proof in
135 | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
136 | ng::_ -> Incomplete_proof (proof, ng)
138 { status with proof_status = new_status }
140 let rec tactical_of_ast = function
141 | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
142 | TacticAst.Fail loc -> Tacticals.fail
143 | TacticAst.Do (loc, num, tactical) ->
144 Tacticals.do_tactic num (tactical_of_ast tactical)
145 | TacticAst.IdTac loc -> Tacticals.id_tac
146 | TacticAst.Repeat (loc, tactical) ->
147 Tacticals.repeat_tactic (tactical_of_ast tactical)
148 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
149 Tacticals.seq (List.map tactical_of_ast tacticals)
150 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
151 Tacticals.thens (tactical_of_ast tactical)
152 (List.map tactical_of_ast tacticals)
153 | TacticAst.Tries (loc, tacticals) ->
154 Tacticals.try_tactics
155 (List.map (fun t -> "", tactical_of_ast t) tacticals)
156 | TacticAst.Try (loc, tactical) ->
157 Tacticals.try_tactic (tactical_of_ast tactical)
159 apply_tactic (tactical_of_ast tac)
161 (** given a uri and a type list (the contructors types) builds a list of pairs
162 * (name,uri) that is used to generate authomatic aliases **)
163 let extract_alias types uri =
165 fun (acc,i) (name, _, _, cl) ->
166 ((name, UriManager.string_of_uriref (uri,[i]))
168 (fst(List.fold_left (
169 fun (acc,j) (name,_) ->
170 (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1)
174 (** adds a (name,uri) list l to a disambiguation environment e **)
175 let env_of_list l e =
176 let module DT = DisambiguateTypes in
177 let module DTE = DisambiguateTypes.Environment in
182 (uri,fun _ _ _ -> CicUtil.term_of_uri uri)
186 let eval_command status cmd =
188 | TacticAst.Set (loc, name, value) -> set_option status name value
189 | TacticAst.Qed loc ->
190 let uri, metasenv, bo, ty =
191 match status.proof_status with
192 | Proof (Some uri, metasenv, body, ty) ->
193 uri, metasenv, body, ty
194 | Proof (None, metasenv, body, ty) ->
196 ("Someone allows to start a thm without giving the "^
197 "name/uri. This should be fixed!")
198 | _-> command_error "You can't qed an uncomplete theorem"
200 let suri = UriManager.string_of_uri uri in
201 if metasenv <> [] then
202 command_error "Proof not completed! metasenv is not empty!";
203 let proved_ty,ugraph =
204 CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
207 CicReduction.are_convertible [] proved_ty ty ugraph
211 ("The type of your proof is not convertible with the "^
212 "type you've declared!");
213 MatitaLog.message (sprintf "%s defined" suri);
214 let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
216 let name = UriManager.name_of_uri uri in
217 let new_env = env_of_list [(name,suri)] status.aliases in
218 {status with aliases = new_env }
220 {status with proof_status = No_proof }
221 | TacticAst.Inductive (loc, dummy_params, types) ->
222 (* dummy_params are not real params, it is a list of nothing, and the only
223 * semantic content is the len, that is leftno (note: leftno and pamaters
224 * have nothing in common).
228 | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
231 let uri = UriManager.uri_of_string suri in
232 let leftno = List.length dummy_params in
233 let obj = Cic.InductiveDefinition (types, [], leftno, []) in
235 CicTypeChecker.typecheck_mutual_inductive_defs uri
236 (types, [], leftno) CicUniv.empty_ugraph
239 MatitaSync.add_inductive_def
240 ~uri ~types ~params:[] ~leftno ~ugraph status
242 (* aliases for the constructors and types *)
243 let aliases = env_of_list (extract_alias types uri) status.aliases in
244 (* aliases for the eliminations principles *)
246 let base = String.sub suri 0 (String.length suri - 4) in
251 fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix
252 ) status.objects then
253 let u = base ^ suffix in
254 (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc
257 ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases
259 let status = {status with proof_status = No_proof } in
260 { status with aliases = aliases}
261 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
263 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
267 match status.proof_status with
268 | Intermediate metasenv ->
269 ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
272 let initial_proof = (Some uri, metasenv, body, ty) in
273 { status with proof_status = Incomplete_proof (initial_proof,goalno)}
274 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
276 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
278 let metasenv = MatitaMisc.get_proof_metasenv status in
279 let (body_type, ugraph) =
280 CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
282 let (subst, metasenv, ugraph) =
283 CicUnification.fo_unif metasenv [] body_type ty ugraph
285 if metasenv <> [] then
287 "metasenv not empty while giving a definition with body";
288 let body = CicMetaSubst.apply_subst subst body in
289 let ty = CicMetaSubst.apply_subst subst ty in
290 let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
292 let suri = UriManager.string_of_uri uri in
293 let new_env = env_of_list [(name,suri)] status.aliases in
294 {status with aliases = new_env }
296 {status with proof_status = No_proof}
297 | TacticAst.Theorem (_, _, None, _, _) ->
298 command_error "The grammar should avoid having unnamed theorems!"
299 | TacticAst.Coercion (loc, term) -> assert false (** TODO *)
300 | TacticAst.Alias (loc, spec) ->
302 | TacticAst.Ident_alias (id,uri) ->
303 {status with aliases =
304 DisambiguateTypes.Environment.add
305 (DisambiguateTypes.Id id)
306 ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
308 | TacticAst.Symbol_alias (symb, instance, desc) ->
309 {status with aliases =
310 DisambiguateTypes.Environment.add
311 (DisambiguateTypes.Symbol (symb,instance))
312 (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
314 | TacticAst.Number_alias (instance,desc) ->
315 {status with aliases =
316 DisambiguateTypes.Environment.add
317 (DisambiguateTypes.Num instance)
318 (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
320 let eval_executable status ex =
322 | TacticAst.Tactical (_, tac) -> eval_tactical status tac
323 | TacticAst.Command (_, cmd) -> eval_command status cmd
324 | TacticAst.Macro (_, mac) ->
325 command_error (sprintf "The macro %s can't be in a script"
326 (TacticAstPp.pp_macro_cic mac))
328 let eval_comment status c = status
332 | TacticAst.Executable (_,ex) -> eval_executable status ex
333 | TacticAst.Comment (_,c) -> eval_comment status c
335 let disambiguate_term status term =
336 let (aliases, metasenv, cic, _) =
338 MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
339 ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
340 ~metasenv:(MatitaMisc.get_proof_metasenv status) term
346 match status.proof_status with
347 | No_proof -> Intermediate metasenv
348 | Incomplete_proof ((uri, _, proof, ty), goal) ->
349 Incomplete_proof ((uri, metasenv, proof, ty), goal)
350 | Intermediate _ -> Intermediate metasenv
351 | Proof _ -> assert false
356 proof_status = proof_status }
360 let disambiguate_terms status terms =
361 let term = CicAst.pack terms in
362 let status, term = disambiguate_term status term in
363 status, CicUtil.unpack term
365 let disambiguate_tactic status = function
366 | TacticAst.Transitivity (loc, term) ->
367 let status, cic = disambiguate_term status term in
368 status, TacticAst.Transitivity (loc, cic)
369 | TacticAst.Apply (loc, term) ->
370 let status, cic = disambiguate_term status term in
371 status, TacticAst.Apply (loc, cic)
372 | TacticAst.Absurd (loc, term) ->
373 let status, cic = disambiguate_term status term in
374 status, TacticAst.Absurd (loc, cic)
375 | TacticAst.Exact (loc, term) ->
376 let status, cic = disambiguate_term status term in
377 status, TacticAst.Exact (loc, cic)
378 | TacticAst.Cut (loc, term) ->
379 let status, cic = disambiguate_term status term in
380 status, TacticAst.Cut (loc, cic)
381 | TacticAst.Elim (loc, term, Some term') ->
382 let status, cic1 = disambiguate_term status term in
383 let status, cic2 = disambiguate_term status term' in
384 status, TacticAst.Elim (loc, cic1, Some cic2)
385 | TacticAst.Elim (loc, term, None) ->
386 let status, cic = disambiguate_term status term in
387 status, TacticAst.Elim (loc, cic, None)
388 | TacticAst.ElimType (loc, term) ->
389 let status, cic = disambiguate_term status term in
390 status, TacticAst.ElimType (loc, cic)
391 | TacticAst.Replace (loc, what, with_what) ->
392 let status, cic1 = disambiguate_term status what in
393 let status, cic2 = disambiguate_term status with_what in
394 status, TacticAst.Replace (loc, cic1, cic2)
395 | TacticAst.Change (loc, what, with_what, ident) ->
396 let status, cic1 = disambiguate_term status what in
397 let status, cic2 = disambiguate_term status with_what in
398 status, TacticAst.Change (loc, cic1, cic2, ident)
400 (* TODO Zack a lot more of tactics to be implemented here ... *)
401 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
402 | TacticAst.Change of 'term * 'term * 'ident option
403 | TacticAst.Decompose of 'ident * 'ident list
404 | TacticAst.Discriminate of 'ident
405 | TacticAst.Fold of reduction_kind * 'term
406 | TacticAst.Injection of 'ident
407 | TacticAst.LetIn of 'term * 'ident
408 | TacticAst.Replace_pattern of 'term pattern * 'term
410 | TacticAst.ReduceAt (loc, reduction_kind, ident, path) ->
411 let path = Disambiguate.interpretate [] status.aliases path in
412 status, TacticAst.ReduceAt(loc, reduction_kind, ident, path)
413 | TacticAst.Reduce (loc, reduction_kind, opts) ->
416 | None -> status, None
419 List.fold_right (fun t (status,acc) ->
420 let status',t' = disambiguate_term status t in
424 status, Some (l, pat)
426 status, TacticAst.Reduce (loc, reduction_kind, opts)
427 | TacticAst.Rewrite (loc,dir,t,ident) ->
428 let status, term = disambiguate_term status t in
429 status, TacticAst.Rewrite (loc,dir,term,ident)
430 | TacticAst.Intros (loc, num, names) ->
431 status, TacticAst.Intros (loc, num, names)
432 | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
433 | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
434 | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
435 | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
436 | TacticAst.Exists loc -> status, TacticAst.Exists loc
437 | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
438 | TacticAst.Left loc -> status, TacticAst.Left loc
439 | TacticAst.Right loc -> status, TacticAst.Right loc
440 | TacticAst.Ring loc -> status, TacticAst.Ring loc
441 | TacticAst.Split loc -> status, TacticAst.Split loc
442 | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
443 | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
445 print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
448 let rec disambiguate_tactical status = function
449 | TacticAst.Tactic (loc, tactic) ->
450 let status, tac = disambiguate_tactic status tactic in
451 status, TacticAst.Tactic (loc, tac)
452 | TacticAst.Do (loc, num, tactical) ->
453 let status, tac = disambiguate_tactical status tactical in
454 status, TacticAst.Do (loc, num, tac)
455 | TacticAst.Repeat (loc, tactical) ->
456 let status, tac = disambiguate_tactical status tactical in
457 status, TacticAst.Repeat (loc, tac)
458 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
459 let status, tacticals = disambiguate_tacticals status tacticals in
460 let tacticals = List.rev tacticals in
461 status, TacticAst.Seq (loc, tacticals)
462 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
463 let status, tactical = disambiguate_tactical status tactical in
464 let status, tacticals = disambiguate_tacticals status tacticals in
465 status, TacticAst.Then (loc, tactical, tacticals)
466 | TacticAst.Tries (loc, tacticals) ->
467 let status, tacticals = disambiguate_tacticals status tacticals in
468 status, TacticAst.Tries (loc, tacticals)
469 | TacticAst.Try (loc, tactical) ->
470 let status, tactical = disambiguate_tactical status tactical in
471 status, TacticAst.Try (loc, tactical)
472 | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
475 and disambiguate_tacticals status tacticals =
476 let status, tacticals =
478 (fun (status, tacticals) tactical ->
479 let status, tac = disambiguate_tactical status tactical in
480 status, tac :: tacticals)
484 let tacticals = List.rev tacticals in
487 let disambiguate_inddef status params indTypes =
488 let add_pi binders t =
490 (fun (name, ast) acc ->
491 CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
495 List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
497 let binders = ind_binders @ params in
499 let add_ast ast = asts := ast :: !asts in
500 let paramsno = List.length params in
501 let indbindersno = List.length ind_binders in
503 (fun (name, _, typ, constructors) ->
504 add_ast (add_pi params typ);
505 List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
507 let status, terms = disambiguate_terms status !asts in
508 let terms = ref (List.rev terms) in
510 match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
514 | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
518 let counter = ref 0 in
522 CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
525 let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
528 (fun acc (name, inductive, typ, constructors) ->
529 let cicTyp = get_term () in
530 let cicConstructors =
532 (fun acc (name, _) ->
534 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
539 (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
542 let cicIndTypes = List.rev cicIndTypes in
543 status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
545 let disambiguate_command status = function
546 | TacticAst.Inductive (loc, params, types) ->
547 let (status, (uri, (ind_types, vars, paramsno))) =
548 disambiguate_inddef status params types
550 let rec mk_list = function
552 | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
554 (* once we've built the cic inductive types we no longer need terms
555 corresponding to parameters, but we need the leftno, and we encode
556 it as the length of dummy_params
558 let dummy_params = mk_list paramsno in
559 status, TacticAst.Inductive (loc, dummy_params, ind_types)
560 | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
561 let status, ty = disambiguate_term status ty in
564 | None -> status, None
566 let status, body = disambiguate_term status body in
569 status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
570 | TacticAst.Coercion (loc, term) -> assert false (** TODO *)
571 | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
573 | TacticAst.Alias _ as x -> status, x
575 let disambiguate_executable status ex =
577 | TacticAst.Tactical (loc, tac) ->
578 let status, tac = disambiguate_tactical status tac in
579 status, (TacticAst.Tactical (loc, tac))
580 | TacticAst.Command (loc, cmd) ->
581 let status, cmd = disambiguate_command status cmd in
582 status, (TacticAst.Command (loc, cmd))
583 | TacticAst.Macro (_, mac) ->
585 (sprintf ("The engine is not allowed to disambiguate any macro, "^^
586 "in particular %s") (TacticAstPp.pp_macro_ast mac))
588 let disambiguate_comment status c =
590 | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
591 | TacticAst.Code (loc,ex) ->
592 let status, ex = disambiguate_executable status ex in
593 status, TacticAst.Code (loc,ex)
595 let disambiguate_statement status statement =
597 | TacticAst.Comment (loc,c) ->
598 let status, c = disambiguate_comment status c in
599 status, TacticAst.Comment (loc,c)
600 | TacticAst.Executable (loc,ex) ->
601 let status, ex = disambiguate_executable status ex in
602 status, TacticAst.Executable (loc,ex)
604 let eval_ast status ast =
605 let status,st = disambiguate_statement status ast in
606 (* this disambiguation step should be deferred to support tacticals *)
609 let eval_from_stream status str cb =
610 let stl = CicTextualParser2.parse_statements str in
612 (fun status ast -> cb status ast;eval_ast status ast) status
615 let eval_string status str =
616 eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
618 let default_options () =
620 StringMap.add "baseuri"
622 (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
626 StringMap.add "basedir"
627 (String (Helm_registry.get "matita.basedir" ))
634 aliases = DisambiguateTypes.empty_environment;
635 proof_status = No_proof;
636 options = default_options ();