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 _ -> Tactics.auto_new ~dbd *)
47 | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
49 (* TODO Zack a lot more of tactics to be implemented here ... *)
50 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
51 | TacticAst.Change of 'term * 'term * 'ident option
52 | TacticAst.Decompose of 'ident * 'ident list
53 | TacticAst.Discriminate of 'ident
54 | TacticAst.Fold of reduction_kind * 'term
55 | TacticAst.Injection of 'ident
56 | TacticAst.LetIn of 'term * 'ident
57 | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
58 | TacticAst.Replace_pattern of 'term pattern * 'term
59 | TacticAst.Rewrite of direction * 'term * 'ident option
63 let eval_tactical status tac =
64 let apply_tactic tactic =
66 ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
71 let (_,metasenv,_,_) = proof in
74 | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
75 | ng::_ -> Incomplete_proof (proof, ng)
77 { status with proof_status = new_status }
79 let rec tactical_of_ast = function
80 | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
81 | TacticAst.Fail loc -> Tacticals.fail
82 | TacticAst.Do (loc, num, tactical) ->
83 Tacticals.do_tactic num (tactical_of_ast tactical)
84 | TacticAst.IdTac loc -> Tacticals.id_tac
85 | TacticAst.Repeat (loc, tactical) ->
86 Tacticals.repeat_tactic (tactical_of_ast tactical)
87 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
88 Tacticals.seq (List.map tactical_of_ast tacticals)
89 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
90 Tacticals.thens (tactical_of_ast tactical)
91 (List.map tactical_of_ast tacticals)
92 | TacticAst.Tries (loc, tacticals) ->
94 (List.map (fun t -> "", tactical_of_ast t) tacticals)
95 | TacticAst.Try (loc, tactical) ->
96 Tacticals.try_tactic (tactical_of_ast tactical)
98 apply_tactic (tactical_of_ast tac)
100 let eval_command status cmd =
102 | TacticAst.Set (loc, name, value) -> set_option status name value
103 | TacticAst.Qed loc ->
104 let uri, metasenv, bo, ty =
105 match status.proof_status with
106 | Proof (Some uri, metasenv, body, ty) ->
107 uri, metasenv, body, ty
108 | Proof (None, metasenv, body, ty) ->
110 ("Someone allows to start a thm without giving the "^
111 "name/uri. This should be fixed!")
112 | _-> command_error "You can't qed an uncomplete theorem"
114 let suri = UriManager.string_of_uri uri in
115 if metasenv <> [] then
116 command_error "Proof not completed! metasenv is not empty!";
117 let proved_ty,ugraph =
118 CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
121 CicReduction.are_convertible [] proved_ty ty ugraph
125 ("The type of your proof is not convertible with the "^
126 "type you've declared!");
127 MatitaLog.message (sprintf "%s defined" suri);
128 let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
129 {status with proof_status = No_proof }
130 | TacticAst.Inductive (loc, dummy_params, types) ->
131 (* dummy_params are not real params, it is a list of nothing, and the only
132 * semantic content is the len, that is leftno (note: leftno and pamaters
133 * have nothing in common).
137 | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
140 let uri = UriManager.uri_of_string suri in
141 let leftno = List.length dummy_params in
142 let obj = Cic.InductiveDefinition (types, [], leftno, []) in
144 CicTypeChecker.typecheck_mutual_inductive_defs uri
145 (types, [], leftno) CicUniv.empty_ugraph
147 MatitaSync.add_inductive_def
148 ~uri ~types ~params:[] ~leftno ~ugraph status;
149 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
151 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
155 match status.proof_status with
156 | Intermediate metasenv ->
157 ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
160 let initial_proof = (Some uri, metasenv, body, ty) in
161 { status with proof_status = Incomplete_proof (initial_proof,goalno)}
162 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
164 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
166 let metasenv = MatitaMisc.get_proof_metasenv status in
167 let (body_type, ugraph) =
168 CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
170 let (subst, metasenv, ugraph) =
171 CicUnification.fo_unif metasenv [] body_type ty ugraph
173 if metasenv <> [] then
175 "metasenv not empty while giving a definition with body";
176 let body = CicMetaSubst.apply_subst subst body in
177 let ty = CicMetaSubst.apply_subst subst ty in
178 MatitaSync.add_constant ~uri ~body ~ty ~ugraph status
179 | TacticAst.Theorem (_, _, None, _, _) ->
180 command_error "The grammas should avoid having unnamed theorems!"
181 | TacticAst.Coercion (loc, term) -> assert false (** TODO *)
182 | TacticAst.Alias (loc, spec) ->
184 | TacticAst.Ident_alias (id,uri) ->
185 {status with aliases =
186 DisambiguateTypes.Environment.add
187 (DisambiguateTypes.Id id)
188 ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
190 | TacticAst.Symbol_alias (symb, instance, desc) ->
191 {status with aliases =
192 DisambiguateTypes.Environment.add
193 (DisambiguateTypes.Symbol (symb,instance))
194 (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
196 | TacticAst.Number_alias (instance,desc) ->
197 {status with aliases =
198 DisambiguateTypes.Environment.add
199 (DisambiguateTypes.Num instance)
200 (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
204 | TacticAst.Tactical (_, tac) -> eval_tactical status tac
205 | TacticAst.Command (_, cmd) -> eval_command status cmd
206 | TacticAst.Macro (_, mac) ->
207 command_error (sprintf "The macro %s can't be in a script"
208 (TacticAstPp.pp_macro_cic mac))
210 let disambiguate_term status term =
211 let (aliases, metasenv, cic, _) =
213 MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
214 ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
215 ~metasenv:(MatitaMisc.get_proof_metasenv status) term
221 match status.proof_status with
222 | No_proof -> Intermediate metasenv
223 | Incomplete_proof ((uri, _, proof, ty), goal) ->
224 Incomplete_proof ((uri, metasenv, proof, ty), goal)
225 | Intermediate _ -> Intermediate metasenv
226 | Proof _ -> assert false
231 proof_status = proof_status }
235 let disambiguate_terms status terms =
236 let term = CicAst.pack terms in
237 let status, term = disambiguate_term status term in
238 status, CicUtil.unpack term
240 let disambiguate_tactic status = function
241 | TacticAst.Transitivity (loc, term) ->
242 let status, cic = disambiguate_term status term in
243 status, TacticAst.Transitivity (loc, cic)
244 | TacticAst.Apply (loc, term) ->
245 let status, cic = disambiguate_term status term in
246 status, TacticAst.Apply (loc, cic)
247 | TacticAst.Absurd (loc, term) ->
248 let status, cic = disambiguate_term status term in
249 status, TacticAst.Absurd (loc, cic)
250 | TacticAst.Exact (loc, term) ->
251 let status, cic = disambiguate_term status term in
252 status, TacticAst.Exact (loc, cic)
253 | TacticAst.Cut (loc, term) ->
254 let status, cic = disambiguate_term status term in
255 status, TacticAst.Cut (loc, cic)
256 | TacticAst.Elim (loc, term, Some term') ->
257 let status, cic1 = disambiguate_term status term in
258 let status, cic2 = disambiguate_term status term' in
259 status, TacticAst.Elim (loc, cic1, Some cic2)
260 | TacticAst.Elim (loc, term, None) ->
261 let status, cic = disambiguate_term status term in
262 status, TacticAst.Elim (loc, cic, None)
263 | TacticAst.ElimType (loc, term) ->
264 let status, cic = disambiguate_term status term in
265 status, TacticAst.ElimType (loc, cic)
266 | TacticAst.Replace (loc, what, with_what) ->
267 let status, cic1 = disambiguate_term status what in
268 let status, cic2 = disambiguate_term status with_what in
269 status, TacticAst.Replace (loc, cic1, cic2)
270 | TacticAst.Change (loc, what, with_what, ident) ->
271 let status, cic1 = disambiguate_term status what in
272 let status, cic2 = disambiguate_term status with_what in
273 status, TacticAst.Change (loc, cic1, cic2, ident)
275 (* TODO Zack a lot more of tactics to be implemented here ... *)
276 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
277 | TacticAst.Change of 'term * 'term * 'ident option
278 | TacticAst.Decompose of 'ident * 'ident list
279 | TacticAst.Discriminate of 'ident
280 | TacticAst.Fold of reduction_kind * 'term
281 | TacticAst.Injection of 'ident
282 | TacticAst.LetIn of 'term * 'ident
283 | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
284 | TacticAst.Replace_pattern of 'term pattern * 'term
285 | TacticAst.Rewrite of direction * 'term * 'ident option
287 | TacticAst.Intros (loc, num, names) ->
288 status, TacticAst.Intros (loc, num, names)
289 | TacticAst.Auto loc -> status, TacticAst.Auto loc
290 | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
291 | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
292 | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
293 | TacticAst.Exists loc -> status, TacticAst.Exists loc
294 | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
295 | TacticAst.Left loc -> status, TacticAst.Left loc
296 | TacticAst.Right loc -> status, TacticAst.Right loc
297 | TacticAst.Ring loc -> status, TacticAst.Ring loc
298 | TacticAst.Split loc -> status, TacticAst.Split loc
299 | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
300 | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
302 print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
305 let rec disambiguate_tactical status = function
306 | TacticAst.Tactic (loc, tactic) ->
307 let status, tac = disambiguate_tactic status tactic in
308 status, TacticAst.Tactic (loc, tac)
309 | TacticAst.Do (loc, num, tactical) ->
310 let status, tac = disambiguate_tactical status tactical in
311 status, TacticAst.Do (loc, num, tac)
312 | TacticAst.Repeat (loc, tactical) ->
313 let status, tac = disambiguate_tactical status tactical in
314 status, TacticAst.Repeat (loc, tac)
315 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
316 let status, tacticals = disambiguate_tacticals status tacticals in
317 let tacticals = List.rev tacticals in
318 status, TacticAst.Seq (loc, tacticals)
319 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
320 let status, tactical = disambiguate_tactical status tactical in
321 let status, tacticals = disambiguate_tacticals status tacticals in
322 status, TacticAst.Then (loc, tactical, tacticals)
323 | TacticAst.Tries (loc, tacticals) ->
324 let status, tacticals = disambiguate_tacticals status tacticals in
325 status, TacticAst.Tries (loc, tacticals)
326 | TacticAst.Try (loc, tactical) ->
327 let status, tactical = disambiguate_tactical status tactical in
328 status, TacticAst.Try (loc, tactical)
329 | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
332 and disambiguate_tacticals status tacticals =
333 let status, tacticals =
335 (fun (status, tacticals) tactical ->
336 let status, tac = disambiguate_tactical status tactical in
337 status, tac :: tacticals)
341 let tacticals = List.rev tacticals in
344 let disambiguate_inddef status params indTypes =
345 let add_pi binders t =
347 (fun (name, ast) acc ->
348 CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
352 List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
354 let binders = ind_binders @ params in
356 let add_ast ast = asts := ast :: !asts in
357 let paramsno = List.length params in
358 let indbindersno = List.length ind_binders in
360 (fun (name, _, typ, constructors) ->
361 add_ast (add_pi params typ);
362 List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
364 let status, terms = disambiguate_terms status !asts in
365 let terms = ref (List.rev terms) in
367 match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
371 | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
375 let counter = ref 0 in
379 CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
382 let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
385 (fun acc (name, inductive, typ, constructors) ->
386 let cicTyp = get_term () in
387 let cicConstructors =
389 (fun acc (name, _) ->
391 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
396 (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
399 let cicIndTypes = List.rev cicIndTypes in
400 status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
402 let disambiguate_command status = function
403 | TacticAst.Inductive (loc, params, types) ->
404 let (status, (uri, (ind_types, vars, paramsno))) =
405 disambiguate_inddef status params types
407 let rec mk_list = function
409 | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
411 (* once we've built the cic inductive types we no longer need terms
412 corresponding to parameters, but we need the leftno, and we encode
413 it as the length of dummy_params
415 let dummy_params = mk_list paramsno in
416 status, TacticAst.Inductive (loc, dummy_params, ind_types)
417 | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
418 let status, ty = disambiguate_term status ty in
421 | None -> status, None
423 let status, body = disambiguate_term status body in
426 status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
427 | TacticAst.Coercion (loc, term) -> assert false (** TODO *)
428 | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
430 | TacticAst.Alias _ as x -> status, x
432 let disambiguate_statement status statement =
434 | TacticAst.Tactical (loc, tac) ->
435 let status, tac = disambiguate_tactical status tac in
436 status, (TacticAst.Tactical (loc, tac))
437 | TacticAst.Command (loc, cmd) ->
438 let status, cmd = disambiguate_command status cmd in
439 status, (TacticAst.Command (loc, cmd))
440 | TacticAst.Macro (_, mac) ->
442 (sprintf ("The engine is not allowed to disambiguate any macro, "^^
443 "in particular %s") (TacticAstPp.pp_macro_ast mac))
445 let eval_ast status ast =
446 let status,st = disambiguate_statement status ast in
447 (* this disambiguation step should be deferred to support tacticals *)
450 let eval_from_stream status str =
451 let st = CicTextualParser2.parse_statement str in
454 let eval_string status str =
455 eval_from_stream status (Stream.of_string str)
457 let default_options () =
459 StringMap.add "baseuri"
461 (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
465 StringMap.add "basedir"
466 (String (Helm_registry.get "matita.basedir" ))
473 aliases = DisambiguateTypes.empty_environment;
474 proof_status = No_proof;
475 options = default_options ();