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 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
30 module Index = Equality_indexing.DT (* path tree based indexing *)
33 let beta_expand_time = ref 0.;;
35 let debug_print = Utils.debug_print;;
39 let check_equation env equation msg =
40 let w, proof, (eq_ty, left, right, order), metas, args = equation in
41 let metasenv, context, ugraph = env
42 let metasenv' = metasenv @ metas in
44 CicTypeChecker.type_of_aux' metasenv' context left ugraph;
45 CicTypeChecker.type_of_aux' metasenv' context right ugraph;
48 CicUtil.Meta_not_found _ as exn ->
51 prerr_endline (CicPp.ppterm left);
52 prerr_endline (CicPp.ppterm right);
57 type retrieval_mode = Matching | Unification;;
59 let string_of_res ?env =
62 | Some (t, s, m, u, ((p,e), eq_URI)) ->
63 Printf.sprintf "Some: (%s, %s, %s)"
64 (Utils.string_of_pos p)
65 (Inference.string_of_equality ?env e)
69 let print_res ?env res =
72 (List.map (string_of_res ?env) res))
75 let print_candidates ?env mode term res =
79 prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
81 prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
87 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
88 (Inference.string_of_equality ?env e))
93 let indexing_retrieval_time = ref 0.;;
96 let apply_subst = CicMetaSubst.apply_subst
98 let index = Index.index
99 let remove_index = Index.remove_index
100 let in_index = Index.in_index
101 let empty = Index.empty
102 let init_index = Index.init_index
104 let check_disjoint_invariant subst metasenv msg =
106 (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
109 prerr_endline ("not disjoint: " ^ msg);
114 let check_for_duplicates metas msg =
115 if List.length metas <>
116 List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
118 prerr_endline ("DUPLICATI " ^ msg);
119 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
124 let check_res res msg =
126 Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
127 let eqs = Inference.string_of_equality (snd eq_found) in
128 check_disjoint_invariant subst menv msg;
129 check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
133 let check_target context target msg =
134 let w, proof, (eq_ty, left, right, order), metas = target in
135 (* check that metas does not contains duplicates *)
136 let eqs = Inference.string_of_equality target in
137 let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
138 let actual = (Inference.metas_of_term left)@(Inference.metas_of_term right)
139 @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof) in
140 let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
141 let _ = if menv <> metas then
143 prerr_endline ("extra metas " ^ msg);
144 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
145 prerr_endline "**********************";
146 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
147 prerr_endline ("left: " ^ (CicPp.ppterm left));
148 prerr_endline ("right: " ^ (CicPp.ppterm right));
149 prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
154 CicTypeChecker.type_of_aux'
155 metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph
158 prerr_endline (Inference.string_of_proof proof);
159 prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
160 prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
161 prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
166 (* returns a list of all the equalities in the tree that are in relation
167 "mode" with the given term, where mode can be either Matching or
170 Format of the return value: list of tuples in the form:
171 (position - Left or Right - of the term that matched the given one in this
175 Note that if equality is "left = right", if the ordering is left > right,
176 the position will always be Left, and if the ordering is left < right,
177 position will be Right.
179 let local_max = ref 100;;
181 let make_variant (p,eq) =
182 let maxmeta, eq = Inference.fix_metas !local_max eq in
183 local_max := maxmeta;
187 let get_candidates ?env mode tree term =
188 let t1 = Unix.gettimeofday () in
192 | Matching -> Index.retrieve_generalizations tree term
193 | Unification -> Index.retrieve_unifiables tree term
195 Index.PosEqSet.elements s
197 (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
198 (* print_newline (); *)
199 let t2 = Unix.gettimeofday () in
200 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
201 (* make fresh instances *)
205 let profiler = HExtlib.profile "P/Indexing.get_candidates"
207 let get_candidates ?env mode tree term =
208 profiler.HExtlib.profile (get_candidates ?env mode tree) term
210 let match_unif_time_ok = ref 0.;;
211 let match_unif_time_no = ref 0.;;
215 finds the first equality in the index that matches "term", of type "termty"
216 termty can be Implicit if it is not needed. The result (one of the sides of
217 the equality, actually) should be not greater (wrt the term ordering) than
220 Format of the return value:
222 (term to substitute, [Cic.Rel 1 properly lifted - see the various
223 build_newtarget functions inside the various
224 demodulation_* functions]
225 substitution used for the matching,
227 ugraph, [substitution, metasenv and ugraph have the same meaning as those
228 returned by CicUnification.fo_unif]
229 (equality where the matching term was found, [i.e. the equality to use as
231 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
232 the equality: this is used to build the proof term, again see one of
233 the build_newtarget functions]
236 let rec find_matches metasenv context ugraph lift_amount term termty =
237 let module C = Cic in
238 let module U = Utils in
239 let module S = CicSubstitution in
240 let module M = CicMetaSubst in
241 let module HL = HelmLibraryObjects in
242 let cmp = !Utils.compare_terms in
243 let check = match termty with C.Implicit None -> false | _ -> true in
247 let pos, (_, proof, (ty, left, right, o), metas) = candidate in
248 if Utils.debug_metas then
249 ignore(check_target context (snd candidate) "find_matches");
250 if Utils.debug_res then
252 let c = "eq = " ^ (Inference.string_of_equality (snd candidate)) ^ "\n"in
253 let t = "t = " ^ (CicPp.ppterm term) ^ "\n" in
254 let m = "metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
255 let p = "proof = " ^ (CicPp.ppterm (Inference.build_proof_term proof)) ^ "\n" in
256 check_for_duplicates metas "gia nella metas";
257 check_for_duplicates (metasenv @ metas) ("not disjoint" ^ c ^ t ^ m ^ p)
259 if check && not (fst (CicReduction.are_convertible
260 ~metasenv context termty ty ugraph)) then (
261 find_matches metasenv context ugraph lift_amount term termty tl
263 let do_match c eq_URI =
264 let subst', metasenv', ugraph' =
265 let t1 = Unix.gettimeofday () in
268 ( Inference.matching metasenv metas context
269 term (S.lift lift_amount c)) ugraph
271 let t2 = Unix.gettimeofday () in
272 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
275 | Inference.MatchingFailure as e ->
276 let t2 = Unix.gettimeofday () in
277 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
279 | CicUtil.Meta_not_found _ as exn -> raise exn
281 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
284 let c, other, eq_URI =
285 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
286 else right, left, Utils.eq_ind_r_URI ()
288 if o <> U.Incomparable then
292 with Inference.MatchingFailure ->
293 find_matches metasenv context ugraph lift_amount term termty tl
295 if Utils.debug_res then ignore (check_res res "find1");
299 try do_match c eq_URI
300 with Inference.MatchingFailure -> None
302 if Utils.debug_res then ignore (check_res res "find2");
304 | Some (_, s, _, _, _) ->
305 let c' = apply_subst s c in
307 let other' = U.guarded_simpl context (apply_subst s other) in *)
308 let other' = apply_subst s other in
309 let order = cmp c' other' in
314 metasenv context ugraph lift_amount term termty tl
316 find_matches metasenv context ugraph lift_amount term termty tl
320 as above, but finds all the matching equalities, and the matching condition
321 can be either Inference.matching or Inference.unification
323 let rec find_all_matches ?(unif_fun=Inference.unification)
324 metasenv context ugraph lift_amount term termty =
325 let module C = Cic in
326 let module U = Utils in
327 let module S = CicSubstitution in
328 let module M = CicMetaSubst in
329 let module HL = HelmLibraryObjects in
330 let cmp = !Utils.compare_terms in
334 let pos, (_, _, (ty, left, right, o), metas) = candidate in
335 let do_match c eq_URI =
336 let subst', metasenv', ugraph' =
337 let t1 = Unix.gettimeofday () in
340 unif_fun metasenv metas context
341 term (S.lift lift_amount c) ugraph in
342 let t2 = Unix.gettimeofday () in
343 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
346 | Inference.MatchingFailure
347 | CicUnification.UnificationFailure _
348 | CicUnification.Uncertain _ as e ->
349 let t2 = Unix.gettimeofday () in
350 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
353 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
356 let c, other, eq_URI =
357 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
358 else right, left, Utils.eq_ind_r_URI ()
360 if o <> U.Incomparable then
362 let res = do_match c eq_URI in
363 res::(find_all_matches ~unif_fun metasenv context ugraph
364 lift_amount term termty tl)
366 | Inference.MatchingFailure
367 | CicUnification.UnificationFailure _
368 | CicUnification.Uncertain _ ->
369 find_all_matches ~unif_fun metasenv context ugraph
370 lift_amount term termty tl
373 let res = do_match c eq_URI in
376 let c' = apply_subst s c
377 and other' = apply_subst s other in
378 let order = cmp c' other' in
379 if order <> U.Lt && order <> U.Le then
380 res::(find_all_matches ~unif_fun metasenv context ugraph
381 lift_amount term termty tl)
383 find_all_matches ~unif_fun metasenv context ugraph
384 lift_amount term termty tl
386 | Inference.MatchingFailure
387 | CicUnification.UnificationFailure _
388 | CicUnification.Uncertain _ ->
389 find_all_matches ~unif_fun metasenv context ugraph
390 lift_amount term termty tl
394 ?unif_fun metasenv context ugraph lift_amount term termty l
398 ?unif_fun metasenv context ugraph lift_amount term termty l
400 (*prerr_endline "CANDIDATES:";
401 List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
402 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
407 returns true if target is subsumed by some equality in table
409 let subsumption env table target =
410 let _, _, (ty, left, right, _), tmetas = target in
411 let metasenv, context, ugraph = env in
412 let metasenv = metasenv @ tmetas in
413 let samesubst subst subst' =
414 let tbl = Hashtbl.create (List.length subst) in
415 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
417 (fun (m, (c, t1, t2)) ->
419 let c', t1', t2' = Hashtbl.find tbl m in
420 if (c = c') && (t1 = t1') && (t2 = t2') then true
430 let leftc = get_candidates Matching table left in
431 find_all_matches ~unif_fun:Inference.matching
432 metasenv context ugraph 0 left ty leftc
434 let rec ok what = function
436 | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m)), _))::tl ->
438 let other = if pos = Utils.Left then r else l in
439 let subst', menv', ug' =
440 let t1 = Unix.gettimeofday () in
443 Inference.matching menv m context what other ugraph
445 let t2 = Unix.gettimeofday () in
446 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
448 with Inference.MatchingFailure as e ->
449 let t2 = Unix.gettimeofday () in
450 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
453 if samesubst subst subst' then
457 with Inference.MatchingFailure ->
460 let r, subst = ok right leftr in
469 let rightc = get_candidates Matching table right in
470 find_all_matches ~unif_fun:Inference.matching
471 metasenv context ugraph 0 right ty rightc
478 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
479 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
483 let rec demodulation_aux ?from ?(typecheck=false)
484 metasenv context ugraph table lift_amount term =
485 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
486 let module C = Cic in
487 let module S = CicSubstitution in
488 let module M = CicMetaSubst in
489 let module HL = HelmLibraryObjects in
491 get_candidates ~env:(metasenv,context,ugraph) Matching table term in
492 (* let candidates = List.map make_variant candidates in *)
499 CicTypeChecker.type_of_aux' metasenv context term ugraph
501 C.Implicit None, ugraph
504 find_matches metasenv context ugraph lift_amount term termty candidates
506 if Utils.debug_res then ignore(check_res res "demod1");
516 (res, tl @ [S.lift 1 t])
519 demodulation_aux ~from:"1" metasenv context ugraph table
523 | None -> (None, tl @ [S.lift 1 t])
524 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
529 | Some (_, subst, menv, ug, eq_found) ->
530 Some (C.Appl ll, subst, menv, ug, eq_found)
532 | C.Prod (nn, s, t) ->
534 demodulation_aux ~from:"2"
535 metasenv context ugraph table lift_amount s in (
539 demodulation_aux metasenv
540 ((Some (nn, C.Decl s))::context) ugraph
541 table (lift_amount+1) t
545 | Some (t', subst, menv, ug, eq_found) ->
546 Some (C.Prod (nn, (S.lift 1 s), t'),
547 subst, menv, ug, eq_found)
549 | Some (s', subst, menv, ug, eq_found) ->
550 Some (C.Prod (nn, s', (S.lift 1 t)),
551 subst, menv, ug, eq_found)
553 | C.Lambda (nn, s, t) ->
556 metasenv context ugraph table lift_amount s in (
560 demodulation_aux metasenv
561 ((Some (nn, C.Decl s))::context) ugraph
562 table (lift_amount+1) t
566 | Some (t', subst, menv, ug, eq_found) ->
567 Some (C.Lambda (nn, (S.lift 1 s), t'),
568 subst, menv, ug, eq_found)
570 | Some (s', subst, menv, ug, eq_found) ->
571 Some (C.Lambda (nn, s', (S.lift 1 t)),
572 subst, menv, ug, eq_found)
577 if Utils.debug_res then ignore(check_res res "demod_aux output");
582 let build_newtarget_time = ref 0.;;
585 let demod_counter = ref 1;;
589 let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"
591 (** demodulation, when target is an equality *)
592 let rec demodulation_equality ?from newmeta env table sign target =
593 let module C = Cic in
594 let module S = CicSubstitution in
595 let module M = CicMetaSubst in
596 let module HL = HelmLibraryObjects in
597 let module U = Utils in
598 let metasenv, context, ugraph = env in
599 let w, proof, (eq_ty, left, right, order), metas = target in
600 (* first, we simplify *)
601 let right = U.guarded_simpl context right in
602 let left = U.guarded_simpl context left in
603 let order = !Utils.compare_terms left right in
604 let stat = (eq_ty, left, right, order) in
605 let w = Utils.compute_equality_weight stat in
606 let target = w, proof, stat, metas in
607 if Utils.debug_metas then
608 ignore(check_target context target "demod equalities input");
609 let metasenv' = (* metasenv @ *) metas in
610 let maxmeta = ref newmeta in
612 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
613 let time1 = Unix.gettimeofday () in
615 if Utils.debug_metas then
617 ignore(check_for_duplicates menv "input1");
618 ignore(check_disjoint_invariant subst menv "input2");
619 let substs = CicMetaSubst.ppsubst subst in
620 ignore(check_target context (snd eq_found) ("input3" ^ substs))
622 let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
624 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
625 with CicUtil.Meta_not_found _ -> ty
627 let what, other = if pos = Utils.Left then what, other else other, what in
628 let newterm, newproof =
629 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
630 let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in
633 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
634 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
635 S.lift 1 eq_ty; l; r]
637 if sign = Utils.Positive then
639 Inference.ProofBlock (
640 subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
645 CicMkImplicit.identity_relocation_list_for_metavariable context in
646 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
647 (* print_newline (); *)
648 C.Meta (!maxmeta, irl)
653 if pos = Utils.Left then [ty; what; other]
654 else [ty; other; what]
656 Inference.ProofSymBlock (termlist, proof')
659 if pos = Utils.Left then what, other else other, what
661 pos, (0, proof', (ty, other, what, Utils.Incomparable),menv')
665 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
666 eq_found, Inference.BasicProof metaproof)
669 | Inference.BasicProof _ ->
670 (* print_endline "replacing a BasicProof"; *)
672 | Inference.ProofGoalBlock (_, parent_proof) ->
674 (* print_endline "replacing another ProofGoalBlock"; *)
675 Inference.ProofGoalBlock (pb, parent_proof)
679 C.Appl [C.MutConstruct (* reflexivity *)
680 (LibraryObjects.eq_URI (), 0, 1, []);
681 eq_ty; if is_left then right else left]
684 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
686 let newmenv = (* Inference.filter subst *) menv in
688 if Utils.debug_metas then
689 try ignore(CicTypeChecker.type_of_aux'
690 newmenv context (Inference.build_proof_term newproof) ugraph);
693 prerr_endline "sempre lui";
694 prerr_endline (CicMetaSubst.ppsubst subst);
695 prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
696 prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
697 prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
698 prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
699 prerr_endline ("+++++++++++++subst: " ^ (CicMetaSubst.ppsubst subst));
703 let left, right = if is_left then newterm, right else left, newterm in
704 let ordering = !Utils.compare_terms left right in
705 let stat = (eq_ty, left, right, ordering) in
706 let time2 = Unix.gettimeofday () in
707 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
709 let w = Utils.compute_equality_weight stat in
710 (w, newproof, stat,newmenv) in
711 if Utils.debug_metas then
712 ignore(check_target context res "buildnew_target output");
715 let build_newtarget is_left x =
716 profiler.HExtlib.profile (build_newtarget is_left) x
719 let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
720 if Utils.debug_res then check_res res "demod result";
721 let newmeta, newtarget =
724 let newmeta, newtarget = build_newtarget true t in
725 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
726 (Inference.meta_convertibility_eq target newtarget) then
729 demodulation_equality newmeta env table sign newtarget
731 let res = demodulation_aux metasenv' context ugraph table 0 right in
732 if Utils.debug_res then check_res res "demod result 1";
735 let newmeta, newtarget = build_newtarget false t in
736 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
737 (Inference.meta_convertibility_eq target newtarget) then
740 demodulation_equality newmeta env table sign newtarget
744 (* newmeta, newtarget *)
749 Performs the beta expansion of the term "term" w.r.t. "table",
750 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
753 let rec betaexpand_term metasenv context ugraph table lift_amount term =
754 let module C = Cic in
755 let module S = CicSubstitution in
756 let module M = CicMetaSubst in
757 let module HL = HelmLibraryObjects in
758 let candidates = get_candidates Unification table term in
760 let res, lifted_term =
765 (fun arg (res, lifted_tl) ->
768 let arg_res, lifted_arg =
769 betaexpand_term metasenv context ugraph table
773 (fun (t, s, m, ug, eq_found) ->
774 (Some t)::lifted_tl, s, m, ug, eq_found)
779 (fun (l, s, m, ug, eq_found) ->
780 (Some lifted_arg)::l, s, m, ug, eq_found)
782 (Some lifted_arg)::lifted_tl)
785 (fun (r, s, m, ug, eq_found) ->
786 None::r, s, m, ug, eq_found) res,
792 (fun (l, s, m, ug, eq_found) ->
793 (C.Meta (i, l), s, m, ug, eq_found)) l'
795 e, C.Meta (i, lifted_l)
798 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
800 | C.Prod (nn, s, t) ->
802 betaexpand_term metasenv context ugraph table lift_amount s in
804 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
805 table (lift_amount+1) t in
808 (fun (t, s, m, ug, eq_found) ->
809 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
812 (fun (t, s, m, ug, eq_found) ->
813 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
814 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
816 | C.Lambda (nn, s, t) ->
818 betaexpand_term metasenv context ugraph table lift_amount s in
820 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
821 table (lift_amount+1) t in
824 (fun (t, s, m, ug, eq_found) ->
825 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
828 (fun (t, s, m, ug, eq_found) ->
829 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
830 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
835 (fun arg (res, lifted_tl) ->
836 let arg_res, lifted_arg =
837 betaexpand_term metasenv context ugraph table lift_amount arg
841 (fun (a, s, m, ug, eq_found) ->
842 a::lifted_tl, s, m, ug, eq_found)
847 (fun (r, s, m, ug, eq_found) ->
848 lifted_arg::r, s, m, ug, eq_found)
850 lifted_arg::lifted_tl)
854 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
857 | t -> [], (S.lift lift_amount t)
860 | C.Meta (i, l) -> res, lifted_term
863 C.Implicit None, ugraph
864 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
868 metasenv context ugraph lift_amount term termty candidates
873 let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
875 let betaexpand_term metasenv context ugraph table lift_amount term =
876 profiler.HExtlib.profile
877 (betaexpand_term metasenv context ugraph table lift_amount) term
880 let sup_l_counter = ref 1;;
884 returns a list of new clauses inferred with a left superposition step
885 the negative equation "target" and one of the positive equations in "table"
887 let superposition_left newmeta (metasenv, context, ugraph) table target =
888 let module C = Cic in
889 let module S = CicSubstitution in
890 let module M = CicMetaSubst in
891 let module HL = HelmLibraryObjects in
892 let module CR = CicReduction in
893 let module U = Utils in
894 let weight, proof, (eq_ty, left, right, ordering), menv = target in
895 if Utils.debug_metas then
896 ignore(check_target context target "superpositionleft");
898 let term = if ordering = U.Gt then left else right in
900 let t1 = Unix.gettimeofday () in
901 let res = betaexpand_term metasenv context ugraph table 0 term in
902 let t2 = Unix.gettimeofday () in
903 beta_expand_time := !beta_expand_time +. (t2 -. t1);
907 let maxmeta = ref newmeta in
908 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
909 (* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
910 let time1 = Unix.gettimeofday () in
912 let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
913 let what, other = if pos = Utils.Left then what, other else other, what in
914 let newgoal, newproof =
915 let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
916 let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
920 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
921 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
922 S.lift 1 eq_ty; l; r]
927 CicMkImplicit.identity_relocation_list_for_metavariable context in
928 C.Meta (!maxmeta, irl)
933 if pos = Utils.Left then [ty; what; other]
934 else [ty; other; what]
936 Inference.ProofSymBlock (termlist, proof')
939 if pos = Utils.Left then what, other else other, what
941 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
945 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
946 Inference.BasicProof metaproof)
949 | Inference.BasicProof _ ->
950 (* debug_print (lazy "replacing a BasicProof"); *)
952 | Inference.ProofGoalBlock (_, parent_proof) ->
953 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
954 Inference.ProofGoalBlock (pb, parent_proof)
958 C.Appl [C.MutConstruct (* reflexivity *)
959 (LibraryObjects.eq_URI (), 0, 1, []);
960 eq_ty; if ordering = U.Gt then right else left]
963 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
966 if ordering = U.Gt then newgoal, right else left, newgoal in
967 let neworder = !Utils.compare_terms left right in
968 let stat = (eq_ty, left, right, neworder) in
969 let newmenv = (* Inference.filter s *) menv in
970 let time2 = Unix.gettimeofday () in
971 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
973 let w = Utils.compute_equality_weight stat in
974 (w, newproof, stat, newmenv)
977 !maxmeta, List.map build_new expansions
981 let sup_r_counter = ref 1;;
985 returns a list of new clauses inferred with a right superposition step
986 between the positive equation "target" and one in the "table" "newmeta" is
987 the first free meta index, i.e. the first number above the highest meta
988 index: its updated value is also returned
990 let superposition_right newmeta (metasenv, context, ugraph) table target =
991 let module C = Cic in
992 let module S = CicSubstitution in
993 let module M = CicMetaSubst in
994 let module HL = HelmLibraryObjects in
995 let module CR = CicReduction in
996 let module U = Utils in
997 let w, eqproof, (eq_ty, left, right, ordering), newmetas = target in
998 if Utils.debug_metas then
999 ignore (check_target context target "superpositionright");
1000 let metasenv' = newmetas in
1001 let maxmeta = ref newmeta in
1003 let betaexpand_term metasenv context ugraph table d term =
1004 let t1 = Unix.gettimeofday () in
1005 let res = betaexpand_term metasenv context ugraph table d term in
1006 let t2 = Unix.gettimeofday () in
1007 beta_expand_time := !beta_expand_time +. (t2 -. t1);
1011 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
1012 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
1016 (fun (_, subst, _, _, _) ->
1017 let subst = apply_subst subst in
1018 let o = !Utils.compare_terms (subst l) (subst r) in
1019 o <> U.Lt && o <> U.Le)
1020 (fst (betaexpand_term metasenv' context ugraph table 0 l))
1022 (res left right), (res right left)
1024 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
1025 if Utils.debug_metas then
1026 ignore (check_target context (snd eq_found) "buildnew1" );
1027 let time1 = Unix.gettimeofday () in
1029 let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
1030 let what, other = if pos = Utils.Left then what, other else other, what in
1031 let newgoal, newproof =
1033 let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
1034 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
1038 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1039 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1040 S.lift 1 eq_ty; l; r]
1043 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
1045 let newmeta, newequality =
1047 if ordering = U.Gt then newgoal, apply_subst s right
1048 else apply_subst s left, newgoal in
1049 let neworder = !Utils.compare_terms left right in
1050 let newmenv = (* Inference.filter s *) m in
1051 let stat = (eq_ty, left, right, neworder) in
1053 let w = Utils.compute_equality_weight stat in
1054 (w, newproof, stat, newmenv) in
1055 if Utils.debug_metas then
1056 ignore (check_target context eq' "buildnew3");
1057 let newm, eq' = Inference.fix_metas !maxmeta eq' in
1058 if Utils.debug_metas then
1059 ignore (check_target context eq' "buildnew4");
1063 let time2 = Unix.gettimeofday () in
1064 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1065 if Utils.debug_metas then
1066 ignore(check_target context newequality "buildnew2");
1069 let new1 = List.map (build_new U.Gt) res1
1070 and new2 = List.map (build_new U.Lt) res2 in
1071 let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
1073 (List.filter ok (new1 @ new2)))
1077 (** demodulation, when the target is a goal *)
1078 let rec demodulation_goal newmeta env table goal =
1079 let module C = Cic in
1080 let module S = CicSubstitution in
1081 let module M = CicMetaSubst in
1082 let module HL = HelmLibraryObjects in
1083 let metasenv, context, ugraph = env in
1084 let maxmeta = ref newmeta in
1085 let proof, metas, term = goal in
1086 let term = Utils.guarded_simpl (~debug:true) context term in
1087 let goal = proof, metas, term in
1088 let metasenv' = metas in
1090 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1091 let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
1092 let what, other = if pos = Utils.Left then what, other else other, what in
1094 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
1095 with CicUtil.Meta_not_found _ -> ty
1097 let newterm, newproof =
1098 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1099 let bo' = apply_subst subst t in
1100 let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
1105 CicMkImplicit.identity_relocation_list_for_metavariable context in
1106 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
1107 C.Meta (!maxmeta, irl)
1112 if pos = Utils.Left then [ty; what; other]
1113 else [ty; other; what]
1115 Inference.ProofSymBlock (termlist, proof')
1118 if pos = Utils.Left then what, other else other, what
1120 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
1124 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
1125 eq_found, Inference.BasicProof metaproof)
1127 let rec repl = function
1128 | Inference.NoProof ->
1129 (* debug_print (lazy "replacing a NoProof"); *)
1131 | Inference.BasicProof _ ->
1132 (* debug_print (lazy "replacing a BasicProof"); *)
1134 | Inference.ProofGoalBlock (_, parent_proof) ->
1135 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
1136 Inference.ProofGoalBlock (pb, parent_proof)
1137 | Inference.SubProof (term, meta_index, p) ->
1138 Inference.SubProof (term, meta_index, repl p)
1142 bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
1144 let newmetasenv = (* Inference.filter subst *) menv in
1145 !maxmeta, (newproof, newmetasenv, newterm)
1148 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
1152 let newmeta, newgoal = build_newgoal t in
1153 let _, _, newg = newgoal in
1154 if Inference.meta_convertibility term newg then
1157 demodulation_goal newmeta env table newgoal
1162 (** demodulation, when the target is a theorem *)
1163 let rec demodulation_theorem newmeta env table theorem =
1164 let module C = Cic in
1165 let module S = CicSubstitution in
1166 let module M = CicMetaSubst in
1167 let module HL = HelmLibraryObjects in
1168 let metasenv, context, ugraph = env in
1169 let maxmeta = ref newmeta in
1170 let term, termty, metas = theorem in
1171 let metasenv' = metas in
1173 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1174 let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
1175 let what, other = if pos = Utils.Left then what, other else other, what in
1176 let newterm, newty =
1177 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1178 let bo' = apply_subst subst t in
1179 let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1182 Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1183 Inference.BasicProof term)
1185 (Inference.build_proof_term newproof, bo)
1188 (* let m = Inference.metas_of_term newterm in *)
1189 !maxmeta, (newterm, newty, menv)
1192 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1196 let newmeta, newthm = build_newtheorem t in
1197 let newt, newty, _ = newthm in
1198 if Inference.meta_convertibility termty newty then
1201 demodulation_theorem newmeta env table newthm