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/.
26 (* let _profiler = <:profiler<_profiler>>;; *)
35 ProofEngineTypes.proof ->
37 ?universe:AutoTypes.universe -> AutoTypes.cache ->
38 ProofEngineTypes.goal list ->
39 Cic.substitution list * AutoTypes.cache * AutoTypes.universe
41 let debug_print s = prerr_endline (Lazy.force s);;
43 let check_disjoint_invariant subst metasenv msg =
45 (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
48 prerr_endline ("not disjoint: " ^ msg);
53 let rec check_irl start = function
55 | None::tl -> check_irl (start+1) tl
56 | (Some (Cic.Rel x))::tl ->
57 if x = start then check_irl (start+1) tl else false
61 let rec is_simple_term = function
62 | Cic.Appl ((Cic.Meta _)::_) -> false
63 | Cic.Appl l -> List.for_all is_simple_term l
64 | Cic.Meta (i, l) -> let l = [] in check_irl 1 l
67 | Cic.MutInd (_, _, []) -> true
68 | Cic.MutConstruct (_, _, _, []) -> true
73 List.exists (fun (j,_,_) -> i = j) menv
76 let unification_simple locked_menv metasenv context t1 t2 ugraph =
78 let module M = CicMetaSubst in
79 let module U = CicUnification in
80 let lookup = Subst.lookup_subst in
81 let rec occurs_check subst what where =
83 | Cic.Meta(i,_) when i = what -> true
84 | C.Appl l -> List.exists (occurs_check subst what) l
86 let t = lookup where subst in
87 if t <> where then occurs_check subst what t else false
90 let rec unif subst menv s t =
91 let s = match s with C.Meta _ -> lookup s subst | _ -> s
92 and t = match t with C.Meta _ -> lookup t subst | _ -> t
96 | s, t when s = t -> subst, menv
97 (* sometimes the same meta has different local contexts; this
98 could create "cyclic" substitutions *)
99 | C.Meta (i, _), C.Meta (j, _) when i=j -> subst, menv
100 | C.Meta (i, _), C.Meta (j, _)
101 when (locked locked_menv i) &&(locked locked_menv j) ->
103 (U.UnificationFailure (lazy "Inference.unification.unif"))
104 | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) ->
106 | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) ->
108 | C.Meta (i,_), t when occurs_check subst i t ->
110 (U.UnificationFailure (lazy "Inference.unification.unif"))
111 | C.Meta (i, l), t when (locked locked_menv i) ->
113 (U.UnificationFailure (lazy "Inference.unification.unif"))
114 | C.Meta (i, l), t -> (
116 let _, _, ty = CicUtil.lookup_meta i menv in
117 assert (not (Subst.is_in_subst i subst));
118 let subst = Subst.buildsubst i context t ty subst in
119 let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
121 with CicUtil.Meta_not_found m ->
122 let names = names_of_context context in
124 (lazy*) prerr_endline
125 (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
126 (CicPp.pp t1 names) (CicPp.pp t2 names)
127 (print_metasenv menv) (print_metasenv metasenv));
130 | _, C.Meta _ -> unif subst menv t s
131 | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
132 raise (U.UnificationFailure (lazy "Inference.unification.unif"))
133 | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
136 (fun (subst', menv) s t -> unif subst' menv s t)
137 (subst, menv) tls tlt
138 with Invalid_argument _ ->
139 raise (U.UnificationFailure (lazy "Inference.unification.unif"))
142 raise (U.UnificationFailure (lazy "Inference.unification.unif"))
144 let subst, menv = unif Subst.empty_subst metasenv t1 t2 in
145 let menv = Subst.filter subst menv in
149 let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]"
150 let profiler2 = HExtlib.profile "P/Inference.unif_simple[flatten_fast]"
151 let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]"
152 let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
154 let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
156 HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2))
157 (* metasenv1 @ metasenv2 *)
159 let subst, menv, ug =
160 if not (is_simple_term t1) || not (is_simple_term t2) then (
163 (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
164 (CicPp.ppterm t1) (CicPp.ppterm t2)));
165 raise (CicUnification.UnificationFailure (lazy "Inference.unification.unif"))
168 (* full unification *)
169 unification_simple [] metasenv context t1 t2 ugraph
171 (* matching: metasenv1 is locked *)
172 unification_simple metasenv1 metasenv context t1 t2 ugraph
174 if Utils.debug_res then
175 ignore(check_disjoint_invariant subst menv "unif");
176 (* let flatten subst =
178 (fun (i, (context, term, ty)) ->
179 let context = apply_subst_context subst context in
180 let term = apply_subst subst term in
181 let ty = apply_subst subst ty in
182 (i, (context, term, ty))) subst
184 let flatten subst = profiler.HExtlib.profile flatten subst in
185 let subst = flatten subst in *)
189 exception MatchingFailure;;
191 (** matching takes in input the _disjoint_ metasenv of t1 and t2;
192 it perform unification in the union metasenv, then check that
193 the first metasenv has not changed *)
194 let matching metasenv1 metasenv2 context t1 t2 ugraph =
196 unification_aux false metasenv1 metasenv2 context t1 t2 ugraph
198 CicUnification.UnificationFailure _ ->
199 raise MatchingFailure
202 let unification m1 m2 c t1 t2 ug =
204 unification_aux true m1 m2 c t1 t2 ug
210 let check_eq context msg eq =
211 let w, proof, (eq_ty, left, right, order), metas = eq in
212 if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty
213 (fst (CicTypeChecker.type_of_aux' metas context left CicUniv.empty_ugraph))
214 CicUniv.empty_ugraph))
223 let default_auto _ _ _ ?(universe:AutoTypes.universe option) _ _ =
224 [],AutoTypes.cache_empty,AutoTypes.empty_universe
227 (* far sta roba e' un casino perche' bisogna pulire il contesto lasciando solo
228 * la roba che non dipende da i *)
229 let pi_of_ctx t i ctx =
230 let rec aux j = function
232 | (Some (nam, Cic.Decl (term)))::tl -> Cic.Prod(nam,term,aux (j-1) tl)
233 | _ -> assert false (* not implemented *)
235 aux (List.length ctx-1) (List.rev ctx)
238 let lambda_of_ctx t i ctx =
239 let rec aux j = function
241 | (Some (nam, Cic.Decl (term)))::tl -> Cic.Lambda(nam,term,aux (j-1) tl)
242 | _ -> assert false (* not implemented *)
244 aux (List.length ctx -1) (List.rev ctx)
247 let rec skip_lambda t l =
249 | Cic.Lambda (_,_,t), _::((_::_) as tl) -> skip_lambda t tl
250 | Cic.Lambda (_,_,t), _::[] -> t
254 let ty_of_eq = function
255 | Cic.Appl [Cic.MutInd (_, _, _); ty; _; _] -> ty
259 exception UnableToSaturate of AutoTypes.universe option * AutoTypes.cache
261 let saturate_term context metasenv oldnewmeta term ?universe cache auto fast =
262 let head, metasenv, args, newmeta =
263 ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
269 let _,_,mt = CicUtil.lookup_meta i metasenv in
271 CicTypeChecker.type_of_aux' metasenv context mt
275 CicReduction.are_convertible ~metasenv context
276 sort (Cic.Sort Cic.Prop) u
278 if b then Some i else None
279 (* maybe unif or conv should be used instead of = *)
283 let results,universe,cache =
284 if args_for_auto = [] then
285 let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
286 [args,metasenv,newmetas,head,newmeta],universe,cache
289 None,metasenv,term,term (* term non e' significativo *)
293 {AutoTypes.timeout = 1.0;maxwidth = 2;maxdepth = 2}
295 {AutoTypes.timeout = 1.0;maxwidth = 3;maxdepth = 3}
297 match auto flags proof context ?universe cache args_for_auto with
298 | [],cache,universe -> raise (UnableToSaturate (Some universe,cache))
299 | substs,cache,universe ->
303 CicMetaSubst.apply_subst_metasenv subst metasenv
305 let head = CicMetaSubst.apply_subst subst head in
307 List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv
309 let args = List.map (CicMetaSubst.apply_subst subst) args in
310 args,metasenv,newmetas,head,newmeta)
314 results,universe,cache
317 let rec is_an_equality = function
318 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2]
319 when (LibraryObjects.is_eq_URI uri) -> true
320 | Cic.Prod (name, s, t) -> is_an_equality t
324 let build_equality_of_hypothesis index head args newmetas =
326 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
328 if args = [] then Cic.Rel index else Cic.Appl ((Cic.Rel index)::args)
332 (Printf.sprintf "OK: %s" (CicPp.ppterm p)));
333 let o = !Utils.compare_terms t1 t2 in
334 let stat = (ty,t1,t2,o) in
335 (* let w = compute_equality_weight stat in *)
337 let proof = Equality.Exact p in
338 Equality.mk_equality (w, proof, stat, newmetas)
342 let build_equality ty t1 t2 proof menv =
343 let o = !Utils.compare_terms t1 t2 in
344 let stat = (ty,t1,t2,o) in
345 let w = compute_equality_weight stat in
346 let proof = Equality.Exact proof in
347 Equality.mk_equality (w, proof, stat, menv)
350 let find_equalities ?(auto = default_auto) context proof ?universe cache =
351 prerr_endline "find_equalities";
352 let module C = Cic in
353 let module S = CicSubstitution in
354 let module T = CicTypeChecker in
355 let _,metasenv,_,_ = proof in
356 let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
357 let rec aux universe cache index newmeta = function
358 | [] -> [], newmeta,universe,cache
359 | (Some (_, C.Decl (term)))::tl ->
362 (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
363 let do_find context term =
365 | C.Prod (name, s, t) when is_an_equality t ->
367 let term = S.lift index term in
368 let saturated ,universe,cache =
369 saturate_term context metasenv newmeta term
370 ?universe cache auto false
374 (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
376 build_equality_of_hypothesis index head args newmetas
378 equality::acc,(max newmeta newmeta' + 1))
381 eqs, newmeta, universe, cache
382 with UnableToSaturate (universe,cache) ->
383 [],newmeta,universe,cache)
384 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
385 when LibraryObjects.is_eq_URI uri ->
386 let term = S.lift index term in
387 let e = build_equality_of_hypothesis index term [] [] in
388 [e], (newmeta+1),universe,cache
389 | _ -> [], newmeta, universe, cache
391 let eqs, newmeta, universe, cache = do_find context term in
393 debug_print (lazy "skipped")
395 debug_print (lazy "ok");
396 let rest, newmeta,universe,cache =
397 aux universe cache (index+1) newmeta tl
399 List.map (fun x -> index,x) eqs @ rest, newmeta, universe, cache
401 aux universe cache (index+1) newmeta tl
403 let il, maxm, universe, cache =
404 aux universe cache 1 newmeta context
406 let indexes, equalities = List.split il in
407 (* ignore (List.iter (check_eq context "find") equalities); *)
408 indexes, equalities, maxm, universe, cache
413 let equations_blacklist =
415 (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
416 UriManager.UriSet.empty [
417 "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
418 "cic:/Coq/Init/Logic/trans_eq.con";
419 "cic:/Coq/Init/Logic/f_equal.con";
420 "cic:/Coq/Init/Logic/f_equal2.con";
421 "cic:/Coq/Init/Logic/f_equal3.con";
422 "cic:/Coq/Init/Logic/f_equal4.con";
423 "cic:/Coq/Init/Logic/f_equal5.con";
424 "cic:/Coq/Init/Logic/sym_eq.con";
425 "cic:/Coq/Init/Logic/eq_ind.con";
426 "cic:/Coq/Init/Logic/eq_ind_r.con";
427 "cic:/Coq/Init/Logic/eq_rec.con";
428 "cic:/Coq/Init/Logic/eq_rec_r.con";
429 "cic:/Coq/Init/Logic/eq_rect.con";
430 "cic:/Coq/Init/Logic/eq_rect_r.con";
431 "cic:/Coq/Logic/Eqdep/UIP.con";
432 "cic:/Coq/Logic/Eqdep/UIP_refl.con";
433 "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
434 "cic:/Coq/ZArith/Zcompare/rename.con";
435 (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
436 perche' questo cacchio di teorema rompe le scatole :'( *)
437 "cic:/Rocq/SUBST/comparith/mult_n_2.con";
439 "cic:/matita/logic/equality/eq_f.con";
440 "cic:/matita/logic/equality/eq_f2.con";
441 "cic:/matita/logic/equality/eq_rec.con";
442 "cic:/matita/logic/equality/eq_rect.con";
446 let equations_blacklist = UriManager.UriSet.empty;;
449 (* let _ = <:start<tty_of_u>> in *)
450 let t = CicUtil.term_of_uri u in
451 let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
452 (* let _ = <:stop<tty_of_u>> in *)
457 let t,ty = tty_of_u u in
461 let find_library_equalities
462 ?(auto = default_auto) caso_strano dbd context status maxmeta ?universe cache
464 prerr_endline "find_library_equalities";
465 let module C = Cic in
466 let module S = CicSubstitution in
467 let module T = CicTypeChecker in
468 (* let _ = <:start<equations_for_goal>> in *)
469 let proof, goalno = status in
470 let _,metasenv,_,_ = proof in
471 let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
476 | Cic.Appl[Cic.MutInd(u,0,_);eq_ty;l;r] ->
477 (let mainl, sigl = MetadataConstraints.signature_of l in
478 let mainr, sigr = MetadataConstraints.signature_of r in
479 match mainl,mainr with
480 | Some (uril,tyl), Some (urir, tyr)
481 when LibraryObjects.is_eq_URI uril &&
482 LibraryObjects.is_eq_URI urir &&
484 Some (mainl,MetadataConstraints.UriManagerSet.union sigl sigr)
486 let u = (UriManager.uri_of_string
487 (UriManager.string_of_uri u ^ "#xpointer(1/1)")) in
488 let main = Some (u, []) in
489 Some (main,MetadataConstraints.UriManagerSet.union sigl sigr))
495 prerr_endline "find_library_equalities.1";
496 let eqs = MetadataQuery.equations_for_goal ~dbd ?signature status in
497 (* let _ = <:stop<equations_for_goal>> in *)
498 prerr_endline "find_library_equalities.2";
499 let is_var_free (_,term,_ty) =
500 let rec is_var_free = function
502 | C.Appl l -> List.for_all is_var_free l
503 | C.Prod (_, s, t) | C.Lambda (_, s, t)
504 | C.LetIn (_, s, t) | C.Cast (s, t) -> (is_var_free s) && (is_var_free t)
509 let is_monomorphic_eq (_,term,termty) =
510 let rec last = function
511 | Cic.Prod(_,_,t) -> last t
514 match last termty with
515 | C.Appl [C.MutInd (_, _, []); Cic.Rel _; _; _] -> false
516 | C.Appl [C.MutInd (_, _, []); _; _; _] -> true
519 let candidates = List.map utty_of_u eqs in
520 let candidates = List.filter is_monomorphic_eq candidates in
521 let candidates = List.filter is_var_free candidates in
522 let rec aux universe cache newmeta = function
523 | [] -> [], newmeta, universe, cache
524 | (uri, term, termty)::tl ->
527 (Printf.sprintf "Examining: %s (%s)"
528 (CicPp.ppterm term) (CicPp.ppterm termty)));
529 let res, newmeta, universe, cache =
531 | C.Prod (name, s, t) ->
533 let saturated, universe,cache =
534 saturate_term context metasenv newmeta termty
535 ?universe cache auto true
539 (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
541 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
542 when LibraryObjects.is_eq_URI uri ->
543 let proof = C.Appl (term::args) in
544 prerr_endline ("PROVA: " ^ CicPp.ppterm proof);
546 build_equality ty t1 t2 proof newmetas
548 equality::acc,(max newmeta newmeta' + 1)
552 eqs, newmeta , universe, cache
553 with UnableToSaturate (universe,cache) ->
554 [], newmeta , universe, cache)
555 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] ->
556 let e = build_equality ty t1 t2 term [] in
557 [e], (newmeta+1), universe, cache
560 let res = List.map (fun e -> uri, e) res in
561 let tl, newmeta, universe, cache = aux universe cache newmeta tl in
562 res @ tl, newmeta, universe, cache
564 let found, maxm, universe, cache =
565 aux universe cache maxmeta candidates
568 let mceq = Equality.meta_convertibility_eq in
570 (fun (s, l) (u, e) ->
571 if List.exists (mceq e) (List.map snd l) then (
574 (Printf.sprintf "NO!! %s already there!"
575 (Equality.string_of_equality e)));
576 (UriManager.UriSet.add u s, l)
577 ) else (UriManager.UriSet.add u s, (u, e)::l))
578 (UriManager.UriSet.empty, []) found)
580 uriset, eqlist, maxm, universe, cache
583 let get_stats () = "" (*<:show<Inference.>>*) ;;