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
60 | TacticAst.Rewrite of direction * 'term * 'ident option
64 let eval_tactical status tac =
65 let apply_tactic tactic =
67 ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
72 let (_,metasenv,_,_) = proof in
75 | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
76 | ng::_ -> Incomplete_proof (proof, ng)
78 { status with proof_status = new_status }
80 let rec tactical_of_ast = function
81 | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
82 | TacticAst.Fail loc -> Tacticals.fail
83 | TacticAst.Do (loc, num, tactical) ->
84 Tacticals.do_tactic num (tactical_of_ast tactical)
85 | TacticAst.IdTac loc -> Tacticals.id_tac
86 | TacticAst.Repeat (loc, tactical) ->
87 Tacticals.repeat_tactic (tactical_of_ast tactical)
88 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
89 Tacticals.seq (List.map tactical_of_ast tacticals)
90 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
91 Tacticals.thens (tactical_of_ast tactical)
92 (List.map tactical_of_ast tacticals)
93 | TacticAst.Tries (loc, tacticals) ->
95 (List.map (fun t -> "", tactical_of_ast t) tacticals)
96 | TacticAst.Try (loc, tactical) ->
97 Tacticals.try_tactic (tactical_of_ast tactical)
99 apply_tactic (tactical_of_ast tac)
101 let eval_command status cmd =
103 | TacticAst.Set (loc, name, value) -> set_option status name value
104 | TacticAst.Qed loc ->
105 let uri, metasenv, bo, ty =
106 match status.proof_status with
107 | Proof (Some uri, metasenv, body, ty) ->
108 uri, metasenv, body, ty
109 | Proof (None, metasenv, body, ty) ->
111 ("Someone allows to start a thm without giving the "^
112 "name/uri. This should be fixed!")
113 | _-> command_error "You can't qed an uncomplete theorem"
115 let suri = UriManager.string_of_uri uri in
116 if metasenv <> [] then
117 command_error "Proof not completed! metasenv is not empty!";
118 let proved_ty,ugraph =
119 CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
122 CicReduction.are_convertible [] proved_ty ty ugraph
126 ("The type of your proof is not convertible with the "^
127 "type you've declared!");
128 MatitaLog.message (sprintf "%s defined" suri);
129 let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
130 {status with proof_status = No_proof }
131 | TacticAst.Inductive (loc, dummy_params, types) ->
132 (* dummy_params are not real params, it is a list of nothing, and the only
133 * semantic content is the len, that is leftno (note: leftno and pamaters
134 * have nothing in common).
138 | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
141 let uri = UriManager.uri_of_string suri in
142 let leftno = List.length dummy_params in
143 let obj = Cic.InductiveDefinition (types, [], leftno, []) in
145 CicTypeChecker.typecheck_mutual_inductive_defs uri
146 (types, [], leftno) CicUniv.empty_ugraph
148 MatitaSync.add_inductive_def
149 ~uri ~types ~params:[] ~leftno ~ugraph status;
150 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
152 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
156 match status.proof_status with
157 | Intermediate metasenv ->
158 ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
161 let initial_proof = (Some uri, metasenv, body, ty) in
162 { status with proof_status = Incomplete_proof (initial_proof,goalno)}
163 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
165 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
167 let metasenv = MatitaMisc.get_proof_metasenv status in
168 let (body_type, ugraph) =
169 CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
171 let (subst, metasenv, ugraph) =
172 CicUnification.fo_unif metasenv [] body_type ty ugraph
174 if metasenv <> [] then
176 "metasenv not empty while giving a definition with body";
177 let body = CicMetaSubst.apply_subst subst body in
178 let ty = CicMetaSubst.apply_subst subst ty in
179 MatitaSync.add_constant ~uri ~body ~ty ~ugraph status
180 | TacticAst.Theorem (_, _, None, _, _) ->
181 command_error "The grammas should avoid having unnamed theorems!"
182 | TacticAst.Coercion (loc, term) -> assert false (** TODO *)
183 | TacticAst.Alias (loc, spec) ->
185 | TacticAst.Ident_alias (id,uri) ->
186 {status with aliases =
187 DisambiguateTypes.Environment.add
188 (DisambiguateTypes.Id id)
189 ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
191 | TacticAst.Symbol_alias (symb, instance, desc) ->
192 {status with aliases =
193 DisambiguateTypes.Environment.add
194 (DisambiguateTypes.Symbol (symb,instance))
195 (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
197 | TacticAst.Number_alias (instance,desc) ->
198 {status with aliases =
199 DisambiguateTypes.Environment.add
200 (DisambiguateTypes.Num instance)
201 (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
205 | TacticAst.Tactical (_, tac) -> eval_tactical status tac
206 | TacticAst.Command (_, cmd) -> eval_command status cmd
207 | TacticAst.Macro (_, mac) ->
208 command_error (sprintf "The macro %s can't be in a script"
209 (TacticAstPp.pp_macro_cic mac))
211 let disambiguate_term status term =
212 let (aliases, metasenv, cic, _) =
214 MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
215 ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
216 ~metasenv:(MatitaMisc.get_proof_metasenv status) term
222 match status.proof_status with
223 | No_proof -> Intermediate metasenv
224 | Incomplete_proof ((uri, _, proof, ty), goal) ->
225 Incomplete_proof ((uri, metasenv, proof, ty), goal)
226 | Intermediate _ -> Intermediate metasenv
227 | Proof _ -> assert false
232 proof_status = proof_status }
236 let disambiguate_terms status terms =
237 let term = CicAst.pack terms in
238 let status, term = disambiguate_term status term in
239 status, CicUtil.unpack term
241 let disambiguate_tactic status = function
242 | TacticAst.Transitivity (loc, term) ->
243 let status, cic = disambiguate_term status term in
244 status, TacticAst.Transitivity (loc, cic)
245 | TacticAst.Apply (loc, term) ->
246 let status, cic = disambiguate_term status term in
247 status, TacticAst.Apply (loc, cic)
248 | TacticAst.Absurd (loc, term) ->
249 let status, cic = disambiguate_term status term in
250 status, TacticAst.Absurd (loc, cic)
251 | TacticAst.Exact (loc, term) ->
252 let status, cic = disambiguate_term status term in
253 status, TacticAst.Exact (loc, cic)
254 | TacticAst.Cut (loc, term) ->
255 let status, cic = disambiguate_term status term in
256 status, TacticAst.Cut (loc, cic)
257 | TacticAst.Elim (loc, term, Some term') ->
258 let status, cic1 = disambiguate_term status term in
259 let status, cic2 = disambiguate_term status term' in
260 status, TacticAst.Elim (loc, cic1, Some cic2)
261 | TacticAst.Elim (loc, term, None) ->
262 let status, cic = disambiguate_term status term in
263 status, TacticAst.Elim (loc, cic, None)
264 | TacticAst.ElimType (loc, term) ->
265 let status, cic = disambiguate_term status term in
266 status, TacticAst.ElimType (loc, cic)
267 | TacticAst.Replace (loc, what, with_what) ->
268 let status, cic1 = disambiguate_term status what in
269 let status, cic2 = disambiguate_term status with_what in
270 status, TacticAst.Replace (loc, cic1, cic2)
271 | TacticAst.Change (loc, what, with_what, ident) ->
272 let status, cic1 = disambiguate_term status what in
273 let status, cic2 = disambiguate_term status with_what in
274 status, TacticAst.Change (loc, cic1, cic2, ident)
276 (* TODO Zack a lot more of tactics to be implemented here ... *)
277 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
278 | TacticAst.Change of 'term * 'term * 'ident option
279 | TacticAst.Decompose of 'ident * 'ident list
280 | TacticAst.Discriminate of 'ident
281 | TacticAst.Fold of reduction_kind * 'term
282 | TacticAst.Injection of 'ident
283 | TacticAst.LetIn of 'term * 'ident
284 | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
285 | TacticAst.Replace_pattern of 'term pattern * 'term
286 | TacticAst.Rewrite of direction * 'term * 'ident option
288 | TacticAst.Intros (loc, num, names) ->
289 status, TacticAst.Intros (loc, num, names)
290 | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
291 | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
292 | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
293 | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
294 | TacticAst.Exists loc -> status, TacticAst.Exists loc
295 | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
296 | TacticAst.Left loc -> status, TacticAst.Left loc
297 | TacticAst.Right loc -> status, TacticAst.Right loc
298 | TacticAst.Ring loc -> status, TacticAst.Ring loc
299 | TacticAst.Split loc -> status, TacticAst.Split loc
300 | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
301 | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
303 print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
306 let rec disambiguate_tactical status = function
307 | TacticAst.Tactic (loc, tactic) ->
308 let status, tac = disambiguate_tactic status tactic in
309 status, TacticAst.Tactic (loc, tac)
310 | TacticAst.Do (loc, num, tactical) ->
311 let status, tac = disambiguate_tactical status tactical in
312 status, TacticAst.Do (loc, num, tac)
313 | TacticAst.Repeat (loc, tactical) ->
314 let status, tac = disambiguate_tactical status tactical in
315 status, TacticAst.Repeat (loc, tac)
316 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
317 let status, tacticals = disambiguate_tacticals status tacticals in
318 let tacticals = List.rev tacticals in
319 status, TacticAst.Seq (loc, tacticals)
320 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
321 let status, tactical = disambiguate_tactical status tactical in
322 let status, tacticals = disambiguate_tacticals status tacticals in
323 status, TacticAst.Then (loc, tactical, tacticals)
324 | TacticAst.Tries (loc, tacticals) ->
325 let status, tacticals = disambiguate_tacticals status tacticals in
326 status, TacticAst.Tries (loc, tacticals)
327 | TacticAst.Try (loc, tactical) ->
328 let status, tactical = disambiguate_tactical status tactical in
329 status, TacticAst.Try (loc, tactical)
330 | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
333 and disambiguate_tacticals status tacticals =
334 let status, tacticals =
336 (fun (status, tacticals) tactical ->
337 let status, tac = disambiguate_tactical status tactical in
338 status, tac :: tacticals)
342 let tacticals = List.rev tacticals in
345 let disambiguate_inddef status params indTypes =
346 let add_pi binders t =
348 (fun (name, ast) acc ->
349 CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
353 List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
355 let binders = ind_binders @ params in
357 let add_ast ast = asts := ast :: !asts in
358 let paramsno = List.length params in
359 let indbindersno = List.length ind_binders in
361 (fun (name, _, typ, constructors) ->
362 add_ast (add_pi params typ);
363 List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
365 let status, terms = disambiguate_terms status !asts in
366 let terms = ref (List.rev terms) in
368 match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
372 | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
376 let counter = ref 0 in
380 CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
383 let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
386 (fun acc (name, inductive, typ, constructors) ->
387 let cicTyp = get_term () in
388 let cicConstructors =
390 (fun acc (name, _) ->
392 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
397 (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
400 let cicIndTypes = List.rev cicIndTypes in
401 status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
403 let disambiguate_command status = function
404 | TacticAst.Inductive (loc, params, types) ->
405 let (status, (uri, (ind_types, vars, paramsno))) =
406 disambiguate_inddef status params types
408 let rec mk_list = function
410 | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
412 (* once we've built the cic inductive types we no longer need terms
413 corresponding to parameters, but we need the leftno, and we encode
414 it as the length of dummy_params
416 let dummy_params = mk_list paramsno in
417 status, TacticAst.Inductive (loc, dummy_params, ind_types)
418 | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
419 let status, ty = disambiguate_term status ty in
422 | None -> status, None
424 let status, body = disambiguate_term status body in
427 status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
428 | TacticAst.Coercion (loc, term) -> assert false (** TODO *)
429 | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
431 | TacticAst.Alias _ as x -> status, x
433 let disambiguate_statement status statement =
435 | TacticAst.Tactical (loc, tac) ->
436 let status, tac = disambiguate_tactical status tac in
437 status, (TacticAst.Tactical (loc, tac))
438 | TacticAst.Command (loc, cmd) ->
439 let status, cmd = disambiguate_command status cmd in
440 status, (TacticAst.Command (loc, cmd))
441 | TacticAst.Macro (_, mac) ->
443 (sprintf ("The engine is not allowed to disambiguate any macro, "^^
444 "in particular %s") (TacticAstPp.pp_macro_ast mac))
446 let eval_ast status ast =
447 let status,st = disambiguate_statement status ast in
448 (* this disambiguation step should be deferred to support tacticals *)
451 let eval_from_stream status str =
452 let st = CicTextualParser2.parse_statement str in
455 let eval_string status str =
456 eval_from_stream status (Stream.of_string str)
458 let default_options () =
460 StringMap.add "baseuri"
462 (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
466 StringMap.add "basedir"
467 (String (Helm_registry.get "matita.basedir" ))
474 aliases = DisambiguateTypes.empty_environment;
475 proof_status = No_proof;
476 options = default_options ();