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 (* {{{ ****************** SATURATION STUFF ***************************)
137 exception UnableToSaturate of AutoCache.cache * int
139 let default_auto maxm _ _ _ _ _ = [],AutoCache.cache_empty,maxm ;;
141 let saturate_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 (UnableToSaturate (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 = default_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
213 let rec aux cache index newmeta = function
214 | [] -> [], newmeta,cache
215 | (Some (_, C.Decl (term)))::tl ->
218 (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
219 let do_find context term =
221 | C.Prod (name, s, t) when is_an_equality t ->
223 let term = S.lift index term in
224 let saturated,cache,newmeta =
225 saturate_term context metasenv newmeta term
230 (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
231 let newmeta, equality =
232 build_equality_of_hypothesis
233 bag index head args newmetas (max newmeta newmeta')
235 equality::acc, newmeta + 1)
236 ([],newmeta) saturated
239 with UnableToSaturate (cache,newmeta) ->
241 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
242 when LibraryObjects.is_eq_URI uri ->
243 let term = S.lift index term in
245 build_equality_of_hypothesis bag index term [] [] newmeta
247 [e], (newmeta+1),cache
248 | _ -> [], newmeta, cache
250 let eqs, newmeta, cache = do_find context term in
251 let rest, newmeta,cache = aux cache (index+1) newmeta tl in
252 List.map (fun x -> index,x) eqs @ rest, newmeta, cache
254 aux cache (index+1) newmeta tl
256 let il, maxm, cache =
257 aux cache 1 newmeta context
259 let indexes, equalities = List.split il in
260 indexes, equalities, maxm, cache
263 let find_library_equalities bag
264 ?(auto = default_auto) caso_strano dbd context status maxmeta cache
266 let module C = Cic in
267 let module S = CicSubstitution in
268 let module T = CicTypeChecker in
269 let proof, goalno = status in
270 let _,metasenv,_,_ = proof in
271 let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
276 | Cic.Appl[Cic.MutInd(u,0,_);eq_ty;l;r] ->
277 (let mainl, sigl = MetadataConstraints.signature_of l in
278 let mainr, sigr = MetadataConstraints.signature_of r in
279 match mainl,mainr with
280 | Some (uril,tyl), Some (urir, tyr)
281 when LibraryObjects.is_eq_URI uril &&
282 LibraryObjects.is_eq_URI urir &&
284 Some (mainl,MetadataConstraints.UriManagerSet.union sigl sigr)
286 let u = (UriManager.uri_of_string
287 (UriManager.string_of_uri u ^ "#xpointer(1/1)")) in
288 let main = Some (u, []) in
289 Some (main,MetadataConstraints.UriManagerSet.union sigl sigr))
295 let eqs = MetadataQuery.equations_for_goal ~dbd ?signature status in
296 let candidates = List.map utty_of_u eqs in
297 let candidates = List.filter is_monomorphic_eq candidates in
298 let candidates = List.filter is_var_free candidates in
299 let rec aux cache newmeta = function
300 | [] -> [], newmeta, cache
301 | (uri, term, termty)::tl ->
304 (Printf.sprintf "Examining: %s (%s)"
305 (CicPp.ppterm term) (CicPp.ppterm termty)));
306 let res, newmeta, cache =
308 | C.Prod (name, s, t) ->
310 let saturated,cache,newmeta =
311 saturate_term context metasenv newmeta termty
316 (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
318 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
319 when LibraryObjects.is_eq_URI uri ->
320 let proof = C.Appl (term::args) in
321 let maxmeta, equality =
322 build_equality bag ty t1 t2 proof newmetas
323 (max newmeta newmeta')
325 equality::acc,maxmeta + 1
327 ([],newmeta) saturated
330 with UnableToSaturate (cache,newmeta) ->
332 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] ->
333 let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in
334 [e], newmeta+1, cache
337 let res = List.map (fun e -> uri, e) res in
338 let tl, newmeta, cache = aux cache newmeta tl in
339 res @ tl, newmeta, cache
341 let found, maxm, cache =
342 aux cache maxmeta candidates
345 let mceq = Equality.meta_convertibility_eq in
347 (fun (s, l) (u, e) ->
348 if List.exists (mceq e) (List.map snd l) then (
351 (Printf.sprintf "NO!! %s already there!"
352 (Equality.string_of_equality e)));
353 (UriManager.UriSet.add u s, l)
354 ) else (UriManager.UriSet.add u s, (u, e)::l))
355 (UriManager.UriSet.empty, []) found)
357 uriset, eqlist, maxm, cache