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 type goal = Equality.goal_proof * Cic.metasenv * Cic.term
30 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
32 module Index = Equality_indexing.DT (* path tree based indexing *)
35 let beta_expand_time = ref 0.;;
37 let debug_print = Utils.debug_print;;
41 let check_equation env equation msg =
42 let w, proof, (eq_ty, left, right, order), metas, args = equation in
43 let metasenv, context, ugraph = env
44 let metasenv' = metasenv @ metas in
46 CicTypeChecker.type_of_aux' metasenv' context left ugraph;
47 CicTypeChecker.type_of_aux' metasenv' context right ugraph;
50 CicUtil.Meta_not_found _ as exn ->
53 prerr_endline (CicPp.ppterm left);
54 prerr_endline (CicPp.ppterm right);
59 type retrieval_mode = Matching | Unification;;
61 let string_of_res ?env =
64 | Some (t, s, m, u, ((p,e), eq_URI)) ->
65 Printf.sprintf "Some: (%s, %s, %s)"
66 (Utils.string_of_pos p)
67 (Equality.string_of_equality ?env e)
71 let print_res ?env res =
74 (List.map (string_of_res ?env) res))
77 let print_candidates ?env mode term res =
81 prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
83 prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
89 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
90 (Equality.string_of_equality ?env e))
95 let indexing_retrieval_time = ref 0.;;
98 let apply_subst = Subst.apply_subst
100 let index = Index.index
101 let remove_index = Index.remove_index
102 let in_index = Index.in_index
103 let empty = Index.empty
104 let init_index = Index.init_index
106 let check_disjoint_invariant subst metasenv msg =
108 (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
111 prerr_endline ("not disjoint: " ^ msg);
116 let check_for_duplicates metas msg =
117 if List.length metas <>
118 List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
120 prerr_endline ("DUPLICATI " ^ msg);
121 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
126 let check_res res msg =
128 Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
129 let eqs = Equality.string_of_equality (snd eq_found) in
130 check_disjoint_invariant subst menv msg;
131 check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
135 let check_target context target msg =
136 let w, proof, (eq_ty, left, right, order), metas,_ =
137 Equality.open_equality target in
138 (* check that metas does not contains duplicates *)
139 let eqs = Equality.string_of_equality target in
140 let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
141 let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
142 @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof) in
143 let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
144 let _ = if menv <> metas then
146 prerr_endline ("extra metas " ^ msg);
147 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
148 prerr_endline "**********************";
149 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
150 prerr_endline ("left: " ^ (CicPp.ppterm left));
151 prerr_endline ("right: " ^ (CicPp.ppterm right));
152 prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
158 ignore(CicTypeChecker.type_of_aux'
159 metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
162 prerr_endline (Inference.string_of_proof proof);
163 prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
164 prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
165 prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
170 (* returns a list of all the equalities in the tree that are in relation
171 "mode" with the given term, where mode can be either Matching or
174 Format of the return value: list of tuples in the form:
175 (position - Left or Right - of the term that matched the given one in this
179 Note that if equality is "left = right", if the ordering is left > right,
180 the position will always be Left, and if the ordering is left < right,
181 position will be Right.
184 let get_candidates ?env mode tree term =
185 let t1 = Unix.gettimeofday () in
189 | Matching -> Index.retrieve_generalizations tree term
190 | Unification -> Index.retrieve_unifiables tree term
192 Index.PosEqSet.elements s
194 (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
195 (* print_newline (); *)
196 let t2 = Unix.gettimeofday () in
197 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
198 (* make fresh instances *)
202 let profiler = HExtlib.profile "P/Indexing.get_candidates"
204 let get_candidates ?env mode tree term =
205 profiler.HExtlib.profile (get_candidates ?env mode tree) term
207 let match_unif_time_ok = ref 0.;;
208 let match_unif_time_no = ref 0.;;
212 finds the first equality in the index that matches "term", of type "termty"
213 termty can be Implicit if it is not needed. The result (one of the sides of
214 the equality, actually) should be not greater (wrt the term ordering) than
217 Format of the return value:
219 (term to substitute, [Cic.Rel 1 properly lifted - see the various
220 build_newtarget functions inside the various
221 demodulation_* functions]
222 substitution used for the matching,
224 ugraph, [substitution, metasenv and ugraph have the same meaning as those
225 returned by CicUnification.fo_unif]
226 (equality where the matching term was found, [i.e. the equality to use as
228 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
229 the equality: this is used to build the proof term, again see one of
230 the build_newtarget functions]
233 let rec find_matches metasenv context ugraph lift_amount term termty =
234 let module C = Cic in
235 let module U = Utils in
236 let module S = CicSubstitution in
237 let module M = CicMetaSubst in
238 let module HL = HelmLibraryObjects in
239 let cmp = !Utils.compare_terms in
240 let check = match termty with C.Implicit None -> false | _ -> true in
244 let pos, equality = candidate in
245 let (_, proof, (ty, left, right, o), metas,_) =
246 Equality.open_equality equality
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 = "^(Equality.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
256 (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
258 check_for_duplicates metas "gia nella metas";
259 check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
261 if check && not (fst (CicReduction.are_convertible
262 ~metasenv context termty ty ugraph)) then (
263 find_matches metasenv context ugraph lift_amount term termty tl
265 let do_match c eq_URI =
266 let subst', metasenv', ugraph' =
267 let t1 = Unix.gettimeofday () in
270 ( Inference.matching metasenv metas context
271 term (S.lift lift_amount c)) ugraph
273 let t2 = Unix.gettimeofday () in
274 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
277 | Inference.MatchingFailure as e ->
278 let t2 = Unix.gettimeofday () in
279 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
281 | CicUtil.Meta_not_found _ as exn -> raise exn
283 Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph',
286 let c, other, eq_URI =
287 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
288 else right, left, Utils.eq_ind_r_URI ()
290 if o <> U.Incomparable then
294 with Inference.MatchingFailure ->
295 find_matches metasenv context ugraph lift_amount term termty tl
297 if Utils.debug_res then ignore (check_res res "find1");
301 try do_match c eq_URI
302 with Inference.MatchingFailure -> None
304 if Utils.debug_res then ignore (check_res res "find2");
306 | Some (_, s, _, _, _) ->
307 let c' = apply_subst s c in
309 let other' = U.guarded_simpl context (apply_subst s other) in *)
310 let other' = apply_subst s other in
311 let order = cmp c' other' in
316 metasenv context ugraph lift_amount term termty tl
318 find_matches metasenv context ugraph lift_amount term termty tl
322 as above, but finds all the matching equalities, and the matching condition
323 can be either Inference.matching or Inference.unification
325 let rec find_all_matches ?(unif_fun=Inference.unification)
326 metasenv context ugraph lift_amount term termty =
327 let module C = Cic in
328 let module U = Utils in
329 let module S = CicSubstitution in
330 let module M = CicMetaSubst in
331 let module HL = HelmLibraryObjects in
332 let cmp = !Utils.compare_terms in
336 let pos, equality = candidate in
337 let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
338 let do_match c eq_URI =
339 let subst', metasenv', ugraph' =
340 let t1 = Unix.gettimeofday () in
344 | Cic.Meta _, Cic.Appl[Cic.MutInd(u,0,_);_;l;r]
345 when LibraryObjects.is_eq_URI u -> l
347 if Utils.compare_weights (Utils.weight_of_term l)
348 (Utils.weight_of_term r) = Utils.Gt
355 unif_fun metasenv metas context
356 term (S.lift lift_amount c) ugraph in
357 let t2 = Unix.gettimeofday () in
358 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
361 | Inference.MatchingFailure
362 | CicUnification.UnificationFailure _
363 | CicUnification.Uncertain _ as e ->
364 let t2 = Unix.gettimeofday () in
365 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
368 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
371 let c, other, eq_URI =
372 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
373 else right, left, Utils.eq_ind_r_URI ()
375 if o <> U.Incomparable then
377 let res = do_match c eq_URI in
378 res::(find_all_matches ~unif_fun metasenv context ugraph
379 lift_amount term termty tl)
381 | Inference.MatchingFailure
382 | CicUnification.UnificationFailure _
383 | CicUnification.Uncertain _ ->
384 find_all_matches ~unif_fun metasenv context ugraph
385 lift_amount term termty tl
388 let res = do_match c eq_URI in
391 let c' = apply_subst s c
392 and other' = apply_subst s other in
393 let order = cmp c' other' in
394 if order <> U.Lt && order <> U.Le then
395 res::(find_all_matches ~unif_fun metasenv context ugraph
396 lift_amount term termty tl)
398 find_all_matches ~unif_fun metasenv context ugraph
399 lift_amount term termty tl
401 | Inference.MatchingFailure
402 | CicUnification.UnificationFailure _
403 | CicUnification.Uncertain _ ->
404 find_all_matches ~unif_fun metasenv context ugraph
405 lift_amount term termty tl
409 ?unif_fun metasenv context ugraph lift_amount term termty l
413 ?unif_fun metasenv context ugraph lift_amount term termty l
415 (*prerr_endline "CANDIDATES:";
416 List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
417 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
422 returns true if target is subsumed by some equality in table
424 let subsumption_aux use_unification env table target =
425 (* let print_res l =*)
426 (* prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,*)
427 (* ((pos,equation),_)) -> Equality.string_of_equality equation)l))*)
429 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
430 let metasenv, context, ugraph = env in
431 let metasenv = tmetas in
432 let predicate, unif_fun =
433 if use_unification then
434 Unification, Inference.unification
436 Matching, Inference.matching
440 | Cic.Meta _ when not use_unification -> []
442 let leftc = get_candidates predicate table left in
443 find_all_matches ~unif_fun
444 metasenv context ugraph 0 left ty leftc
446 (* print_res leftr;*)
447 let rec ok what = function
449 | (_, subst, menv, ug, ((pos,equation),_))::tl ->
450 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
452 let other = if pos = Utils.Left then r else l in
453 let what' = Subst.apply_subst subst what in
454 let subst', menv', ug' =
455 unif_fun metasenv m context what' other ugraph
457 (match Subst.merge_subst_if_possible subst subst' with
459 | Some s -> Some (s, equation))
461 | Inference.MatchingFailure
462 | CicUnification.UnificationFailure _ -> ok what tl
464 match ok right leftr with
465 | Some _ as res -> res
469 | Cic.Meta _ when not use_unification -> []
471 let rightc = get_candidates predicate table right in
472 find_all_matches ~unif_fun
473 metasenv context ugraph 0 right ty rightc
475 (* print_res rightr;*)
480 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
481 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
484 let subsumption = subsumption_aux false;;
485 let unification = subsumption_aux true;;
487 let rec demodulation_aux ?from ?(typecheck=false)
488 metasenv context ugraph table lift_amount term =
489 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
490 let module C = Cic in
491 let module S = CicSubstitution in
492 let module M = CicMetaSubst in
493 let module HL = HelmLibraryObjects in
496 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
504 CicTypeChecker.type_of_aux' metasenv context term ugraph
506 C.Implicit None, ugraph
509 find_matches metasenv context ugraph lift_amount term termty candidates
511 if Utils.debug_res then ignore(check_res res "demod1");
521 (res, tl @ [S.lift 1 t])
524 demodulation_aux ~from:"1" metasenv context ugraph table
528 | None -> (None, tl @ [S.lift 1 t])
529 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
534 | Some (_, subst, menv, ug, eq_found) ->
535 Some (C.Appl ll, subst, menv, ug, eq_found)
537 | C.Prod (nn, s, t) ->
539 demodulation_aux ~from:"2"
540 metasenv context ugraph table lift_amount s in (
544 demodulation_aux metasenv
545 ((Some (nn, C.Decl s))::context) ugraph
546 table (lift_amount+1) t
550 | Some (t', subst, menv, ug, eq_found) ->
551 Some (C.Prod (nn, (S.lift 1 s), t'),
552 subst, menv, ug, eq_found)
554 | Some (s', subst, menv, ug, eq_found) ->
555 Some (C.Prod (nn, s', (S.lift 1 t)),
556 subst, menv, ug, eq_found)
558 | C.Lambda (nn, s, t) ->
561 metasenv context ugraph table lift_amount s in (
565 demodulation_aux metasenv
566 ((Some (nn, C.Decl s))::context) ugraph
567 table (lift_amount+1) t
571 | Some (t', subst, menv, ug, eq_found) ->
572 Some (C.Lambda (nn, (S.lift 1 s), t'),
573 subst, menv, ug, eq_found)
575 | Some (s', subst, menv, ug, eq_found) ->
576 Some (C.Lambda (nn, s', (S.lift 1 t)),
577 subst, menv, ug, eq_found)
582 if Utils.debug_res then ignore(check_res res "demod_aux output");
587 let build_newtarget_time = ref 0.;;
590 let demod_counter = ref 1;;
594 let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"
596 (** demodulation, when target is an equality *)
597 let rec demodulation_equality ?from newmeta env table sign target =
598 let module C = Cic in
599 let module S = CicSubstitution in
600 let module M = CicMetaSubst in
601 let module HL = HelmLibraryObjects in
602 let module U = Utils in
603 let metasenv, context, ugraph = env in
604 let w, proof, (eq_ty, left, right, order), metas, id =
605 Equality.open_equality target
607 (* first, we simplify *)
608 (* let right = U.guarded_simpl context right in *)
609 (* let left = U.guarded_simpl context left in *)
610 (* let order = !Utils.compare_terms left right in *)
611 (* let stat = (eq_ty, left, right, order) in *)
612 (* let w = Utils.compute_equality_weight stat in*)
613 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
614 if Utils.debug_metas then
615 ignore(check_target context target "demod equalities input");
616 let metasenv' = (* metasenv @ *) metas in
617 let maxmeta = ref newmeta in
619 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
620 let time1 = Unix.gettimeofday () in
622 if Utils.debug_metas then
624 ignore(check_for_duplicates menv "input1");
625 ignore(check_disjoint_invariant subst menv "input2");
626 let substs = Subst.ppsubst subst in
627 ignore(check_target context (snd eq_found) ("input3" ^ substs))
629 let pos, equality = eq_found in
631 (ty, what, other, _), menv',id') = Equality.open_equality equality in
633 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
634 with CicUtil.Meta_not_found _ -> ty
636 let what, other = if pos = Utils.Left then what, other else other, what in
637 let newterm, newproof =
639 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
640 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
641 let name = C.Name "x" in
644 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
645 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
646 S.lift 1 eq_ty; l; r]
648 if sign = Utils.Positive then
649 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
650 (Cic.Lambda (name, ty, bo'))))))
655 prerr_endline "***************************************negative";
659 CicMkImplicit.identity_relocation_list_for_metavariable context in
660 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
661 (* print_newline (); *)
662 C.Meta (!maxmeta, irl)
667 if pos = Utils.Left then [ty; what; other]
668 else [ty; other; what]
670 Equality.ProofSymBlock (termlist, proof'_old)
672 let proof'_new' = assert false (* not implemented *) in
674 if pos = Utils.Left then what, other else other, what
678 (0, (proof'_new',proof'_old'),
679 (ty, other, what, Utils.Incomparable),menv')
684 (subst, eq_URI, (name, ty), bo',
685 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
687 assert false, (* not implemented *)
688 (match snd proof with
689 | Equality.BasicProof _ ->
690 (* print_endline "replacing a BasicProof"; *)
692 | Equality.ProofGoalBlock (_, parent_proof) ->
693 (* print_endline "replacing another ProofGoalBlock"; *)
694 Equality.ProofGoalBlock (pb, parent_proof)
698 C.Appl [C.MutConstruct (* reflexivity *)
699 (LibraryObjects.eq_URI (), 0, 1, []);
700 eq_ty; if is_left then right else left]
703 (assert false, (* not implemented *)
704 Equality.ProofGoalBlock
705 (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
709 let newmenv = (* Inference.filter subst *) menv in
711 if Utils.debug_metas then
712 try ignore(CicTypeChecker.type_of_aux'
714 (Equality.build_proof_term newproof) ugraph);
717 prerr_endline "sempre lui";
718 prerr_endline (Subst.ppsubst subst);
719 prerr_endline (CicPp.ppterm
720 (Equality.build_proof_term newproof));
721 prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
722 prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
723 prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
724 prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
725 prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
730 let left, right = if is_left then newterm, right else left, newterm in
731 let ordering = !Utils.compare_terms left right in
732 let stat = (eq_ty, left, right, ordering) in
733 let time2 = Unix.gettimeofday () in
734 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
736 let w = Utils.compute_equality_weight stat in
737 Equality.mk_equality (w, newproof, stat,newmenv)
739 if Utils.debug_metas then
740 ignore(check_target context res "buildnew_target output");
743 let build_newtarget is_left x =
744 profiler.HExtlib.profile (build_newtarget is_left) x
747 let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
748 if Utils.debug_res then check_res res "demod result";
749 let newmeta, newtarget =
752 let newmeta, newtarget = build_newtarget true t in
753 assert (not (Equality.meta_convertibility_eq target newtarget));
754 if (Equality.is_weak_identity newtarget) ||
755 (Equality.meta_convertibility_eq target newtarget) then
758 demodulation_equality ?from newmeta env table sign newtarget
760 let res = demodulation_aux metasenv' context ugraph table 0 right in
761 if Utils.debug_res then check_res res "demod result 1";
764 let newmeta, newtarget = build_newtarget false t in
765 if (Equality.is_weak_identity newtarget) ||
766 (Equality.meta_convertibility_eq target newtarget) then
769 demodulation_equality ?from newmeta env table sign newtarget
773 (* newmeta, newtarget *)
778 Performs the beta expansion of the term "term" w.r.t. "table",
779 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
782 let rec betaexpand_term metasenv context ugraph table lift_amount term =
783 let module C = Cic in
784 let module S = CicSubstitution in
785 let module M = CicMetaSubst in
786 let module HL = HelmLibraryObjects in
787 let candidates = get_candidates Unification table term in
789 let res, lifted_term =
794 (fun arg (res, lifted_tl) ->
797 let arg_res, lifted_arg =
798 betaexpand_term metasenv context ugraph table
802 (fun (t, s, m, ug, eq_found) ->
803 (Some t)::lifted_tl, s, m, ug, eq_found)
808 (fun (l, s, m, ug, eq_found) ->
809 (Some lifted_arg)::l, s, m, ug, eq_found)
811 (Some lifted_arg)::lifted_tl)
814 (fun (r, s, m, ug, eq_found) ->
815 None::r, s, m, ug, eq_found) res,
821 (fun (l, s, m, ug, eq_found) ->
822 (C.Meta (i, l), s, m, ug, eq_found)) l'
824 e, C.Meta (i, lifted_l)
827 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
829 | C.Prod (nn, s, t) ->
831 betaexpand_term metasenv context ugraph table lift_amount s in
833 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
834 table (lift_amount+1) t in
837 (fun (t, s, m, ug, eq_found) ->
838 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
841 (fun (t, s, m, ug, eq_found) ->
842 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
843 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
845 | C.Lambda (nn, s, t) ->
847 betaexpand_term metasenv context ugraph table lift_amount s in
849 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
850 table (lift_amount+1) t in
853 (fun (t, s, m, ug, eq_found) ->
854 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
857 (fun (t, s, m, ug, eq_found) ->
858 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
859 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
864 (fun arg (res, lifted_tl) ->
865 let arg_res, lifted_arg =
866 betaexpand_term metasenv context ugraph table lift_amount arg
870 (fun (a, s, m, ug, eq_found) ->
871 a::lifted_tl, s, m, ug, eq_found)
876 (fun (r, s, m, ug, eq_found) ->
877 lifted_arg::r, s, m, ug, eq_found)
879 lifted_arg::lifted_tl)
883 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
886 | t -> [], (S.lift lift_amount t)
889 | C.Meta (i, l) -> res, lifted_term
892 C.Implicit None, ugraph
893 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
897 metasenv context ugraph lift_amount term termty candidates
902 let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
904 let betaexpand_term metasenv context ugraph table lift_amount term =
905 profiler.HExtlib.profile
906 (betaexpand_term metasenv context ugraph table lift_amount) term
909 let sup_l_counter = ref 1;;
913 returns a list of new clauses inferred with a left superposition step
914 the negative equation "target" and one of the positive equations in "table"
916 let fix_expansion (eq,ty,unchanged,posu) (t, subst, menv, ug, eq_f) =
917 let unchanged = CicSubstitution.lift 1 unchanged in
918 let ty = CicSubstitution.lift 1 ty in
921 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
922 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
924 (pred, subst, menv, ug, eq_f)
927 let build_newgoal context goalproof goal_info expansion =
928 let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal_info expansion in
929 let pos, equality = eq_found in
930 let (_, proof', (ty, what, other, _), menv',id) =
931 Equality.open_equality equality in
932 let what, other = if pos = Utils.Left then what, other else other, what in
933 let newterm, newgoalproof =
935 Utils.guarded_simpl context
936 (apply_subst subst (CicSubstitution.subst other t))
938 let bo' = (*apply_subst subst*) t in
939 let name = Cic.Name "x" in
940 let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
941 bo, (newgoalproofstep::goalproof)
943 let newmetasenv = (* Inference.filter subst *) menv in
944 (newgoalproof, newmetasenv, newterm)
947 let superposition_left
948 (metasenv, context, ugraph) table (proof,menv,ty)
950 let module C = Cic in
951 let module S = CicSubstitution in
952 let module M = CicMetaSubst in
953 let module HL = HelmLibraryObjects in
954 let module CR = CicReduction in
955 let module U = Utils in
956 let big,small,pos,eq,ty =
958 | Cic.Appl [eq;ty;l;r] ->
960 Utils.compare_weights ~normalize:true
961 (Utils.weight_of_term l) (Utils.weight_of_term r)
964 | Utils.Gt -> l,r,Utils.Right,eq,ty
965 | _ -> r,l,Utils.Left,eq,ty)
967 let names = Utils.names_of_context context in
968 prerr_endline ("NON TROVO UN EQ: " ^ CicPp.pp ty names);
971 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
972 List.map (build_newgoal context proof (eq,ty,small,pos)) expansions
975 let sup_r_counter = ref 1;;
979 returns a list of new clauses inferred with a right superposition step
980 between the positive equation "target" and one in the "table" "newmeta" is
981 the first free meta index, i.e. the first number above the highest meta
982 index: its updated value is also returned
984 let superposition_right newmeta (metasenv, context, ugraph) table target =
985 let module C = Cic in
986 let module S = CicSubstitution in
987 let module M = CicMetaSubst in
988 let module HL = HelmLibraryObjects in
989 let module CR = CicReduction in
990 let module U = Utils in
991 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
992 Equality.open_equality target
994 if Utils.debug_metas then
995 ignore (check_target context target "superpositionright");
996 let metasenv' = newmetas in
997 let maxmeta = ref newmeta in
999 let betaexpand_term metasenv context ugraph table d term =
1000 let t1 = Unix.gettimeofday () in
1001 let res = betaexpand_term metasenv context ugraph table d term in
1002 let t2 = Unix.gettimeofday () in
1003 beta_expand_time := !beta_expand_time +. (t2 -. t1);
1008 fst (betaexpand_term metasenv' context ugraph table 0 left), []
1010 [], fst (betaexpand_term metasenv' context ugraph table 0 right)
1014 (fun (_, subst, _, _, _) ->
1015 let subst = apply_subst subst in
1016 let o = !Utils.compare_terms (subst l) (subst r) in
1017 o <> U.Lt && o <> U.Le)
1018 (fst (betaexpand_term metasenv' context ugraph table 0 l))
1020 (res left right), (res right left)
1022 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
1023 if Utils.debug_metas then
1024 ignore (check_target context (snd eq_found) "buildnew1" );
1025 let time1 = Unix.gettimeofday () in
1027 let pos, equality = eq_found in
1028 let (_, proof', (ty, what, other, _), menv',id') =
1029 Equality.open_equality equality in
1030 let what, other = if pos = Utils.Left then what, other else other, what in
1032 let newgoal, newproof =
1035 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
1037 let name = C.Name "x" in
1041 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1042 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1043 S.lift 1 eq_ty; l; r]
1047 (s,(Equality.SuperpositionRight,
1048 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
1050 let newmeta, newequality =
1052 if ordering = U.Gt then newgoal, apply_subst s right
1053 else apply_subst s left, newgoal in
1054 let neworder = !Utils.compare_terms left right in
1055 let newmenv = (* Inference.filter s *) m in
1056 let stat = (eq_ty, left, right, neworder) in
1058 let w = Utils.compute_equality_weight stat in
1059 Equality.mk_equality (w, newproof, stat, newmenv) in
1060 if Utils.debug_metas then
1061 ignore (check_target context eq' "buildnew3");
1062 let newm, eq' = Equality.fix_metas !maxmeta eq' in
1063 if Utils.debug_metas then
1064 ignore (check_target context eq' "buildnew4");
1068 let time2 = Unix.gettimeofday () in
1069 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1070 if Utils.debug_metas then
1071 ignore(check_target context newequality "buildnew2");
1074 let new1 = List.map (build_new U.Gt) res1
1075 and new2 = List.map (build_new U.Lt) res2 in
1076 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1078 (List.filter ok (new1 @ new2)))
1081 (** demodulation, when the target is a goal *)
1082 let goal_metaconvertibility_eq (_,_,g1) (_,_,g2) =
1083 Equality.meta_convertibility g1 g2
1086 let rec demodulation_goal env table goal =
1087 let metasenv, context, ugraph = env in
1088 let goalproof, metas, term = goal in
1089 let term = Utils.guarded_simpl (~debug:true) context term in
1090 let goal = goalproof, metas, term in
1091 let metasenv' = metas in
1093 let left,right,eq,ty =
1095 | Cic.Appl [eq;ty;l;r] -> l,r,eq,ty
1099 let resright = demodulation_aux metasenv' context ugraph table 0 right in
1102 let newg=build_newgoal context goalproof (eq,ty,left,Utils.Left) t in
1103 if goal_metaconvertibility_eq goal newg then
1106 true, snd (demodulation_goal env table newg)
1107 | None -> false, goal
1110 demodulation_aux (*~typecheck:true*) metasenv' context ugraph table 0 left
1114 let newg = build_newgoal context goalproof (eq,ty,right,Utils.Right) t in
1115 if goal_metaconvertibility_eq goal newg then
1118 true, snd (demodulation_goal env table newg)
1119 | None -> do_right ()
1122 (** demodulation, when the target is a theorem *)
1123 let rec demodulation_theorem newmeta env table theorem =
1124 let module C = Cic in
1125 let module S = CicSubstitution in
1126 let module M = CicMetaSubst in
1127 let module HL = HelmLibraryObjects in
1128 let metasenv, context, ugraph = env in
1129 let maxmeta = ref newmeta in
1130 let term, termty, metas = theorem in
1131 let metasenv' = metas in
1133 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1134 let pos, equality = eq_found in
1135 let (_, proof', (ty, what, other, _), menv',id) =
1136 Equality.open_equality equality in
1137 let what, other = if pos = Utils.Left then what, other else other, what in
1138 let newterm, newty =
1139 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1140 (* let bo' = apply_subst subst t in *)
1141 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
1145 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1146 Equality.BasicProof (Equality.empty_subst,term))
1148 (Equality.build_proof_term_old newproofold, bo)
1150 (* TODO, not ported to the new proofs *)
1151 if true then assert false; term, bo
1153 !maxmeta, (newterm, newty, menv)
1156 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1160 let newmeta, newthm = build_newtheorem t in
1161 let newt, newty, _ = newthm in
1162 if Equality.meta_convertibility termty newty then
1165 demodulation_theorem newmeta env table newthm