1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 let debug_print s = ();;(*prerr_endline (Lazy.force s);;*)
33 ProofEngineTypes.proof ->
36 ProofEngineTypes.goal list ->
37 Cic.substitution list * AutoCache.cache * int
39 let is_var_free (_,term,_ty) =
40 let rec is_var_free = function
42 | Cic.Appl l -> List.for_all is_var_free l
44 | Cic.Lambda (_, s, t)
46 | Cic.Cast (s, t) -> (is_var_free s) && (is_var_free t)
52 let rec is_an_equality = function
53 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2]
54 when (LibraryObjects.is_eq_URI uri) -> true
55 | Cic.Prod (name, s, t) -> is_an_equality t
59 let build_equality_of_hypothesis bag index head args newmetas maxmeta =
61 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
63 if args = [] then Cic.Rel index else Cic.Appl ((Cic.Rel index)::args)
67 (Printf.sprintf "OK: %s" (CicPp.ppterm p)));
68 let o = !Utils.compare_terms t1 t2 in
69 let stat = (ty,t1,t2,o) in
70 (* let w = compute_equality_weight stat in *)
72 let proof = Equality.Exact p in
73 let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
74 (* to clean the local context of metas *)
75 Equality.fix_metas bag maxmeta e
79 let build_equality bag ty t1 t2 proof menv maxmeta =
80 let o = !Utils.compare_terms t1 t2 in
81 let stat = (ty,t1,t2,o) in
82 let w = compute_equality_weight stat in
83 let proof = Equality.Exact proof in
84 let e = Equality.mk_equality bag (w, proof, stat, menv) in
85 (* to clean the local context of metas *)
86 Equality.fix_metas bag maxmeta e
90 let t = CicUtil.term_of_uri u in
91 let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
96 let t,ty = tty_of_u u in
100 let is_monomorphic_eq (_,term,termty) =
101 let rec last = function
102 | Cic.Prod(_,_,t) -> last t
105 match last termty with
106 | Cic.Appl [Cic.MutInd (_, _, []); Cic.Rel _; _; _] -> false
107 | Cic.Appl [Cic.MutInd (_, _, []); _; _; _] -> true
112 let equations_blacklist =
114 "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
115 "cic:/Coq/Init/Logic/trans_eq.con"; "cic:/Coq/Init/Logic/f_equal.con";
116 "cic:/Coq/Init/Logic/f_equal2.con"; "cic:/Coq/Init/Logic/f_equal3.con";
117 "cic:/Coq/Init/Logic/f_equal4.con"; "cic:/Coq/Init/Logic/f_equal5.con";
118 "cic:/Coq/Init/Logic/sym_eq.con"; "cic:/Coq/Init/Logic/eq_ind.con";
119 "cic:/Coq/Init/Logic/eq_ind_r.con"; "cic:/Coq/Init/Logic/eq_rec.con";
120 "cic:/Coq/Init/Logic/eq_rec_r.con"; "cic:/Coq/Init/Logic/eq_rect.con";
121 "cic:/Coq/Init/Logic/eq_rect_r.con"; "cic:/Coq/Logic/Eqdep/UIP.con";
122 "cic:/Coq/Logic/Eqdep/UIP_refl.con";"cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
123 "cic:/Coq/ZArith/Zcompare/rename.con";
124 "cic:/Rocq/SUBST/comparith/mult_n_2.con";
125 "cic:/matita/logic/equality/eq_f.con";"cic:/matita/logic/equality/eq_f2.con";
126 "cic:/matita/logic/equality/eq_rec.con";
127 "cic:/matita/logic/equality/eq_rect.con"; ]
130 (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
131 UriManager.UriSet.empty blacklist
134 let equations_blacklist = UriManager.UriSet.empty;;
136 (*****************************************************************)
137 exception AutoFailure of AutoCache.cache * int
139 let default_auto maxm _ _ _ _ _ = [],AutoCache.cache_empty,maxm ;;
141 let close_hypothesis_of_term context metasenv oldnewmeta term cache auto fast =
142 let head, metasenv, args, newmeta =
143 ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
149 let _,_,mt = CicUtil.lookup_meta i metasenv in
151 CicTypeChecker.type_of_aux' metasenv context mt
155 CicReduction.are_convertible ~metasenv context
156 sort (Cic.Sort Cic.Prop) u
158 if b then Some i else None
159 (* maybe unif or conv should be used instead of = *)
163 let results,cache,newmeta =
164 if args_for_auto = [] then
165 let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
166 [args,metasenv,newmetas,head,newmeta],cache,newmeta
169 None,metasenv,term,term (* term non e' significativo *)
173 {AutoTypes.default_flags() with
174 AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
175 maxwidth = 2;maxdepth = 2;
176 use_paramod=true;use_only_paramod=false}
178 {AutoTypes.default_flags() with
179 AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
180 maxwidth = 2;maxdepth = 4;
181 use_paramod=true;use_only_paramod=false}
183 match auto newmeta flags proof context cache args_for_auto with
184 | [],cache,newmeta -> raise (AutoFailure (cache,newmeta))
185 | substs,cache,newmeta ->
189 CicMetaSubst.apply_subst_metasenv subst metasenv
191 let head = CicMetaSubst.apply_subst subst head in
193 List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv
195 let args = List.map (CicMetaSubst.apply_subst subst) args in
196 let newm = CicMkImplicit.new_meta metasenv subst in
197 args,metasenv,newmetas,head,max newm newmeta)
198 substs, cache, newmeta
200 results,cache,newmeta
202 (* }}} ***************************************************************)
204 let find_context_equalities
205 maxmeta bag auto context proof cache
207 prerr_endline "find_equalities";
208 let module C = Cic in
209 let module S = CicSubstitution in
210 let module T = CicTypeChecker in
211 let _,metasenv,_,_ = proof in
212 let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
215 | None -> default_auto
216 | Some auto -> auto in
217 (* if use_auto is true, we try to close the hypothesis of equational
218 statements using auto; a naif, and probably wrong approach *)
219 let rec aux cache index newmeta = function
220 | [] -> [], newmeta,cache
221 | (Some (_, C.Decl (term)))::tl ->
224 (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
225 let do_find context term =
227 | C.Prod (name, s, t) when is_an_equality t ->
229 let term = S.lift index term in
230 let saturated,cache,newmeta =
231 close_hypothesis_of_term context metasenv newmeta term
236 (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
237 let newmeta, equality =
238 build_equality_of_hypothesis
239 bag index head args newmetas (max newmeta newmeta')
241 equality::acc, newmeta + 1)
242 ([],newmeta) saturated
245 with AutoFailure (cache,newmeta) ->
247 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
248 when LibraryObjects.is_eq_URI uri ->
249 let term = S.lift index term in
251 build_equality_of_hypothesis bag index term [] [] newmeta
253 [e], (newmeta+1),cache
254 | _ -> [], newmeta, cache
256 let eqs, newmeta, cache = do_find context term in
257 let rest, newmeta,cache = aux cache (index+1) newmeta tl in
258 List.map (fun x -> index,x) eqs @ rest, newmeta, cache
260 aux cache (index+1) newmeta tl
262 let il, maxm, cache =
263 aux cache 1 newmeta context
265 let indexes, equalities = List.split il in
266 indexes, equalities, maxm, cache
269 let find_library_equalities bag
270 auto caso_strano dbd context status maxmeta cache
272 let module C = Cic in
273 let module S = CicSubstitution in
274 let module T = CicTypeChecker in
275 let proof, goalno = status in
276 let _,metasenv,_,_ = proof in
277 let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
282 | Cic.Appl[Cic.MutInd(u,0,_);eq_ty;l;r] ->
283 (let mainl, sigl = MetadataConstraints.signature_of l in
284 let mainr, sigr = MetadataConstraints.signature_of r in
285 match mainl,mainr with
286 | Some (uril,tyl), Some (urir, tyr)
287 when LibraryObjects.is_eq_URI uril &&
288 LibraryObjects.is_eq_URI urir &&
290 Some (mainl,MetadataConstraints.UriManagerSet.union sigl sigr)
292 let u = (UriManager.uri_of_string
293 (UriManager.string_of_uri u ^ "#xpointer(1/1)")) in
294 let main = Some (u, []) in
295 Some (main,MetadataConstraints.UriManagerSet.union sigl sigr))
301 let eqs = MetadataQuery.equations_for_goal ~dbd ?signature status in
302 let candidates = List.map utty_of_u eqs in
303 let candidates = List.filter is_monomorphic_eq candidates in
304 let candidates = List.filter is_var_free candidates in
307 | None -> default_auto
308 | Some auto -> auto in
309 (* if use_auto is true, we try to close the hypothesis of equational
310 statements using auto; a naif, and probably wrong approach *)
311 let rec aux cache newmeta = function
312 | [] -> [], newmeta, cache
313 | (uri, term, termty)::tl ->
316 (Printf.sprintf "Examining: %s (%s)"
317 (CicPp.ppterm term) (CicPp.ppterm termty)));
318 let res, newmeta, cache =
320 | C.Prod (name, s, t) ->
322 let saturated,cache,newmeta =
323 close_hypothesis_of_term context metasenv newmeta termty
328 (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
330 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
331 when LibraryObjects.is_eq_URI uri ->
332 let proof = C.Appl (term::args) in
333 let maxmeta, equality =
334 build_equality bag ty t1 t2 proof newmetas
335 (max newmeta newmeta')
337 equality::acc,maxmeta + 1
339 ([],newmeta) saturated
342 with AutoFailure (cache,newmeta) ->
344 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] ->
345 let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in
346 [e], newmeta+1, cache
349 let res = List.map (fun e -> uri, e) res in
350 let tl, newmeta, cache = aux cache newmeta tl in
351 res @ tl, newmeta, cache
353 let found, maxm, cache =
354 aux cache maxmeta candidates
357 let mceq = Equality.meta_convertibility_eq in
359 (fun (s, l) (u, e) ->
360 if List.exists (mceq e) (List.map snd l) then (
363 (Printf.sprintf "NO!! %s already there!"
364 (Equality.string_of_equality e)));
365 (UriManager.UriSet.add u s, l)
366 ) else (UriManager.UriSet.add u s, (u, e)::l))
367 (UriManager.UriSet.empty, []) found)
369 uriset, eqlist, maxm, cache