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 let aliases = env_of_list (extract_alias types uri) status.aliases in
201 let status = {status with proof_status = No_proof } in
202 { status with aliases = aliases}
203 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
205 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
209 match status.proof_status with
210 | Intermediate metasenv ->
211 ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
214 let initial_proof = (Some uri, metasenv, body, ty) in
215 { status with proof_status = Incomplete_proof (initial_proof,goalno)}
216 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
218 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
220 let metasenv = MatitaMisc.get_proof_metasenv status in
221 let (body_type, ugraph) =
222 CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
224 let (subst, metasenv, ugraph) =
225 CicUnification.fo_unif metasenv [] body_type ty ugraph
227 if metasenv <> [] then
229 "metasenv not empty while giving a definition with body";
230 let body = CicMetaSubst.apply_subst subst body in
231 let ty = CicMetaSubst.apply_subst subst ty in
232 let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
234 let suri = UriManager.string_of_uri uri in
235 let new_env = env_of_list [(name,suri)] status.aliases in
236 {status with aliases = new_env }
238 {status with proof_status = No_proof}
239 | TacticAst.Theorem (_, _, None, _, _) ->
240 command_error "The grammas should avoid having unnamed theorems!"
241 | TacticAst.Coercion (loc, term) -> assert false (** TODO *)
242 | TacticAst.Alias (loc, spec) ->
244 | TacticAst.Ident_alias (id,uri) ->
245 {status with aliases =
246 DisambiguateTypes.Environment.add
247 (DisambiguateTypes.Id id)
248 ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
250 | TacticAst.Symbol_alias (symb, instance, desc) ->
251 {status with aliases =
252 DisambiguateTypes.Environment.add
253 (DisambiguateTypes.Symbol (symb,instance))
254 (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
256 | TacticAst.Number_alias (instance,desc) ->
257 {status with aliases =
258 DisambiguateTypes.Environment.add
259 (DisambiguateTypes.Num instance)
260 (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
262 let eval_executable status ex =
264 | TacticAst.Tactical (_, tac) -> eval_tactical status tac
265 | TacticAst.Command (_, cmd) -> eval_command status cmd
266 | TacticAst.Macro (_, mac) ->
267 command_error (sprintf "The macro %s can't be in a script"
268 (TacticAstPp.pp_macro_cic mac))
270 let eval_comment status c = status
274 | TacticAst.Executable (_,ex) -> eval_executable status ex
275 | TacticAst.Comment (_,c) -> eval_comment status c
277 let disambiguate_term status term =
278 let (aliases, metasenv, cic, _) =
280 MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
281 ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
282 ~metasenv:(MatitaMisc.get_proof_metasenv status) term
288 match status.proof_status with
289 | No_proof -> Intermediate metasenv
290 | Incomplete_proof ((uri, _, proof, ty), goal) ->
291 Incomplete_proof ((uri, metasenv, proof, ty), goal)
292 | Intermediate _ -> Intermediate metasenv
293 | Proof _ -> assert false
298 proof_status = proof_status }
302 let disambiguate_terms status terms =
303 let term = CicAst.pack terms in
304 let status, term = disambiguate_term status term in
305 status, CicUtil.unpack term
307 let disambiguate_tactic status = function
308 | TacticAst.Transitivity (loc, term) ->
309 let status, cic = disambiguate_term status term in
310 status, TacticAst.Transitivity (loc, cic)
311 | TacticAst.Apply (loc, term) ->
312 let status, cic = disambiguate_term status term in
313 status, TacticAst.Apply (loc, cic)
314 | TacticAst.Absurd (loc, term) ->
315 let status, cic = disambiguate_term status term in
316 status, TacticAst.Absurd (loc, cic)
317 | TacticAst.Exact (loc, term) ->
318 let status, cic = disambiguate_term status term in
319 status, TacticAst.Exact (loc, cic)
320 | TacticAst.Cut (loc, term) ->
321 let status, cic = disambiguate_term status term in
322 status, TacticAst.Cut (loc, cic)
323 | TacticAst.Elim (loc, term, Some term') ->
324 let status, cic1 = disambiguate_term status term in
325 let status, cic2 = disambiguate_term status term' in
326 status, TacticAst.Elim (loc, cic1, Some cic2)
327 | TacticAst.Elim (loc, term, None) ->
328 let status, cic = disambiguate_term status term in
329 status, TacticAst.Elim (loc, cic, None)
330 | TacticAst.ElimType (loc, term) ->
331 let status, cic = disambiguate_term status term in
332 status, TacticAst.ElimType (loc, cic)
333 | TacticAst.Replace (loc, what, with_what) ->
334 let status, cic1 = disambiguate_term status what in
335 let status, cic2 = disambiguate_term status with_what in
336 status, TacticAst.Replace (loc, cic1, cic2)
337 | TacticAst.Change (loc, what, with_what, ident) ->
338 let status, cic1 = disambiguate_term status what in
339 let status, cic2 = disambiguate_term status with_what in
340 status, TacticAst.Change (loc, cic1, cic2, ident)
342 (* TODO Zack a lot more of tactics to be implemented here ... *)
343 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
344 | TacticAst.Change of 'term * 'term * 'ident option
345 | TacticAst.Decompose of 'ident * 'ident list
346 | TacticAst.Discriminate of 'ident
347 | TacticAst.Fold of reduction_kind * 'term
348 | TacticAst.Injection of 'ident
349 | TacticAst.LetIn of 'term * 'ident
350 | TacticAst.Replace_pattern of 'term pattern * 'term
352 | TacticAst.Reduce (loc, reduction_kind, opts) ->
355 | None -> status, None
358 List.fold_right (fun t (status,acc) ->
359 let status',t' = disambiguate_term status t in
363 status, Some (l, pat)
365 status, TacticAst.Reduce (loc, reduction_kind, opts)
366 | TacticAst.Rewrite (loc,dir,t,ident) ->
367 let status, term = disambiguate_term status t in
368 status, TacticAst.Rewrite (loc,dir,term,ident)
369 | TacticAst.Intros (loc, num, names) ->
370 status, TacticAst.Intros (loc, num, names)
371 | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
372 | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
373 | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
374 | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
375 | TacticAst.Exists loc -> status, TacticAst.Exists loc
376 | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
377 | TacticAst.Left loc -> status, TacticAst.Left loc
378 | TacticAst.Right loc -> status, TacticAst.Right loc
379 | TacticAst.Ring loc -> status, TacticAst.Ring loc
380 | TacticAst.Split loc -> status, TacticAst.Split loc
381 | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
382 | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
384 print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
387 let rec disambiguate_tactical status = function
388 | TacticAst.Tactic (loc, tactic) ->
389 let status, tac = disambiguate_tactic status tactic in
390 status, TacticAst.Tactic (loc, tac)
391 | TacticAst.Do (loc, num, tactical) ->
392 let status, tac = disambiguate_tactical status tactical in
393 status, TacticAst.Do (loc, num, tac)
394 | TacticAst.Repeat (loc, tactical) ->
395 let status, tac = disambiguate_tactical status tactical in
396 status, TacticAst.Repeat (loc, tac)
397 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
398 let status, tacticals = disambiguate_tacticals status tacticals in
399 let tacticals = List.rev tacticals in
400 status, TacticAst.Seq (loc, tacticals)
401 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
402 let status, tactical = disambiguate_tactical status tactical in
403 let status, tacticals = disambiguate_tacticals status tacticals in
404 status, TacticAst.Then (loc, tactical, tacticals)
405 | TacticAst.Tries (loc, tacticals) ->
406 let status, tacticals = disambiguate_tacticals status tacticals in
407 status, TacticAst.Tries (loc, tacticals)
408 | TacticAst.Try (loc, tactical) ->
409 let status, tactical = disambiguate_tactical status tactical in
410 status, TacticAst.Try (loc, tactical)
411 | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
414 and disambiguate_tacticals status tacticals =
415 let status, tacticals =
417 (fun (status, tacticals) tactical ->
418 let status, tac = disambiguate_tactical status tactical in
419 status, tac :: tacticals)
423 let tacticals = List.rev tacticals in
426 let disambiguate_inddef status params indTypes =
427 let add_pi binders t =
429 (fun (name, ast) acc ->
430 CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
434 List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
436 let binders = ind_binders @ params in
438 let add_ast ast = asts := ast :: !asts in
439 let paramsno = List.length params in
440 let indbindersno = List.length ind_binders in
442 (fun (name, _, typ, constructors) ->
443 add_ast (add_pi params typ);
444 List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
446 let status, terms = disambiguate_terms status !asts in
447 let terms = ref (List.rev terms) in
449 match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
453 | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
457 let counter = ref 0 in
461 CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
464 let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
467 (fun acc (name, inductive, typ, constructors) ->
468 let cicTyp = get_term () in
469 let cicConstructors =
471 (fun acc (name, _) ->
473 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
478 (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
481 let cicIndTypes = List.rev cicIndTypes in
482 status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
484 let disambiguate_command status = function
485 | TacticAst.Inductive (loc, params, types) ->
486 let (status, (uri, (ind_types, vars, paramsno))) =
487 disambiguate_inddef status params types
489 let rec mk_list = function
491 | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
493 (* once we've built the cic inductive types we no longer need terms
494 corresponding to parameters, but we need the leftno, and we encode
495 it as the length of dummy_params
497 let dummy_params = mk_list paramsno in
498 status, TacticAst.Inductive (loc, dummy_params, ind_types)
499 | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
500 let status, ty = disambiguate_term status ty in
503 | None -> status, None
505 let status, body = disambiguate_term status body in
508 status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
509 | TacticAst.Coercion (loc, term) -> assert false (** TODO *)
510 | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
512 | TacticAst.Alias _ as x -> status, x
514 let disambiguate_executable status ex =
516 | TacticAst.Tactical (loc, tac) ->
517 let status, tac = disambiguate_tactical status tac in
518 status, (TacticAst.Tactical (loc, tac))
519 | TacticAst.Command (loc, cmd) ->
520 let status, cmd = disambiguate_command status cmd in
521 status, (TacticAst.Command (loc, cmd))
522 | TacticAst.Macro (_, mac) ->
524 (sprintf ("The engine is not allowed to disambiguate any macro, "^^
525 "in particular %s") (TacticAstPp.pp_macro_ast mac))
527 let disambiguate_comment status c =
529 | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
530 | TacticAst.Code (loc,ex) ->
531 let status, ex = disambiguate_executable status ex in
532 status, TacticAst.Code (loc,ex)
534 let disambiguate_statement status statement =
536 | TacticAst.Comment (loc,c) ->
537 let status, c = disambiguate_comment status c in
538 status, TacticAst.Comment (loc,c)
539 | TacticAst.Executable (loc,ex) ->
540 let status, ex = disambiguate_executable status ex in
541 status, TacticAst.Executable (loc,ex)
543 let eval_ast status ast =
544 let status,st = disambiguate_statement status ast in
545 (* this disambiguation step should be deferred to support tacticals *)
548 let eval_from_stream status str cb =
549 let stl = CicTextualParser2.parse_statements str in
551 (fun status ast -> cb status ast;eval_ast status ast) status
554 let eval_string status str =
555 eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
557 let default_options () =
559 StringMap.add "baseuri"
561 (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
565 StringMap.add "basedir"
566 (String (Helm_registry.get "matita.basedir" ))
573 aliases = DisambiguateTypes.empty_environment;
574 proof_status = No_proof;
575 options = default_options ();