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 (Equality.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 (Equality.string_of_equality ?env e))
93 let indexing_retrieval_time = ref 0.;;
96 let apply_subst = Equality.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,_,_) -> (Equality.is_in_subst i 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 = Equality.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,_ =
135 Equality.open_equality target in
136 (* check that metas does not contains duplicates *)
137 let eqs = Equality.string_of_equality target in
138 let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
139 let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
140 @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof) in
141 let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
142 let _ = if menv <> metas then
144 prerr_endline ("extra metas " ^ msg);
145 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
146 prerr_endline "**********************";
147 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
148 prerr_endline ("left: " ^ (CicPp.ppterm left));
149 prerr_endline ("right: " ^ (CicPp.ppterm right));
150 prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
156 ignore(CicTypeChecker.type_of_aux'
157 metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
160 prerr_endline (Inference.string_of_proof proof);
161 prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
162 prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
163 prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
168 (* returns a list of all the equalities in the tree that are in relation
169 "mode" with the given term, where mode can be either Matching or
172 Format of the return value: list of tuples in the form:
173 (position - Left or Right - of the term that matched the given one in this
177 Note that if equality is "left = right", if the ordering is left > right,
178 the position will always be Left, and if the ordering is left < right,
179 position will be Right.
182 let get_candidates ?env mode tree term =
183 let t1 = Unix.gettimeofday () in
187 | Matching -> Index.retrieve_generalizations tree term
188 | Unification -> Index.retrieve_unifiables tree term
190 Index.PosEqSet.elements s
192 (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
193 (* print_newline (); *)
194 let t2 = Unix.gettimeofday () in
195 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
196 (* make fresh instances *)
200 let profiler = HExtlib.profile "P/Indexing.get_candidates"
202 let get_candidates ?env mode tree term =
203 profiler.HExtlib.profile (get_candidates ?env mode tree) term
205 let match_unif_time_ok = ref 0.;;
206 let match_unif_time_no = ref 0.;;
210 finds the first equality in the index that matches "term", of type "termty"
211 termty can be Implicit if it is not needed. The result (one of the sides of
212 the equality, actually) should be not greater (wrt the term ordering) than
215 Format of the return value:
217 (term to substitute, [Cic.Rel 1 properly lifted - see the various
218 build_newtarget functions inside the various
219 demodulation_* functions]
220 substitution used for the matching,
222 ugraph, [substitution, metasenv and ugraph have the same meaning as those
223 returned by CicUnification.fo_unif]
224 (equality where the matching term was found, [i.e. the equality to use as
226 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
227 the equality: this is used to build the proof term, again see one of
228 the build_newtarget functions]
231 let rec find_matches metasenv context ugraph lift_amount term termty =
232 let module C = Cic in
233 let module U = Utils in
234 let module S = CicSubstitution in
235 let module M = CicMetaSubst in
236 let module HL = HelmLibraryObjects in
237 let cmp = !Utils.compare_terms in
238 let check = match termty with C.Implicit None -> false | _ -> true in
242 let pos, equality = candidate in
243 let (_, proof, (ty, left, right, o), metas,_) =
244 Equality.open_equality equality in
245 if Utils.debug_metas then
246 ignore(check_target context (snd candidate) "find_matches");
247 if Utils.debug_res then
249 let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
250 let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
251 let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
253 (CicPp.ppterm(Equality.build_proof_term_old (snd proof)))^"\n"
255 check_for_duplicates metas "gia nella metas";
256 check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
258 if check && not (fst (CicReduction.are_convertible
259 ~metasenv context termty ty ugraph)) then (
260 find_matches metasenv context ugraph lift_amount term termty tl
262 let do_match c eq_URI =
263 let subst', metasenv', ugraph' =
264 let t1 = Unix.gettimeofday () in
267 ( Inference.matching metasenv metas context
268 term (S.lift lift_amount c)) ugraph
270 let t2 = Unix.gettimeofday () in
271 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
274 | Inference.MatchingFailure as e ->
275 let t2 = Unix.gettimeofday () in
276 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
278 | CicUtil.Meta_not_found _ as exn -> raise exn
280 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
283 let c, other, eq_URI =
284 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
285 else right, left, Utils.eq_ind_r_URI ()
287 if o <> U.Incomparable then
291 with Inference.MatchingFailure ->
292 find_matches metasenv context ugraph lift_amount term termty tl
294 if Utils.debug_res then ignore (check_res res "find1");
298 try do_match c eq_URI
299 with Inference.MatchingFailure -> None
301 if Utils.debug_res then ignore (check_res res "find2");
303 | Some (_, s, _, _, _) ->
304 let c' = apply_subst s c in
306 let other' = U.guarded_simpl context (apply_subst s other) in *)
307 let other' = apply_subst s other in
308 let order = cmp c' other' in
313 metasenv context ugraph lift_amount term termty tl
315 find_matches metasenv context ugraph lift_amount term termty tl
319 as above, but finds all the matching equalities, and the matching condition
320 can be either Inference.matching or Inference.unification
322 let rec find_all_matches ?(unif_fun=Inference.unification)
323 metasenv context ugraph lift_amount term termty =
324 let module C = Cic in
325 let module U = Utils in
326 let module S = CicSubstitution in
327 let module M = CicMetaSubst in
328 let module HL = HelmLibraryObjects in
329 let cmp = !Utils.compare_terms in
333 let pos, equality = candidate in
334 let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality 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 =
412 prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
413 ((pos,equation),_)) -> Inference.string_of_equality equation)l))
416 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
417 let metasenv, context, ugraph = env in
418 let metasenv = tmetas in
423 let leftc = get_candidates Matching table left in
424 find_all_matches ~unif_fun:Inference.matching
425 metasenv context ugraph 0 left ty leftc
427 (* print_res leftr;*)
428 let rec ok what = function
430 | (_, subst, menv, ug, ((pos,equation),_))::tl ->
431 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
433 let other = if pos = Utils.Left then r else l in
434 let subst', menv', ug' =
435 let t1 = Unix.gettimeofday () in
438 Inference.matching metasenv m context what other ugraph
440 let t2 = Unix.gettimeofday () in
441 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
443 with Inference.MatchingFailure as e ->
444 let t2 = Unix.gettimeofday () in
445 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
448 (match Equality.merge_subst_if_possible subst subst' with
450 | Some s -> Some (s, equation))
451 with Inference.MatchingFailure ->
454 match ok right leftr with
455 | Some _ as res -> res
461 let rightc = get_candidates Matching table right in
462 find_all_matches ~unif_fun:Inference.matching
463 metasenv context ugraph 0 right ty rightc
465 (* print_res rightr;*)
470 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
471 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
474 let rec demodulation_aux ?from ?(typecheck=false)
475 metasenv context ugraph table lift_amount term =
476 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
477 let module C = Cic in
478 let module S = CicSubstitution in
479 let module M = CicMetaSubst in
480 let module HL = HelmLibraryObjects in
482 get_candidates ~env:(metasenv,context,ugraph) (* Unification *) Matching table term in
483 if List.exists (fun (i,_,_) -> i = 2840) metasenv
485 (prerr_endline ("term: " ^(CicPp.ppterm term));
486 List.iter (fun (_,x) -> prerr_endline (Equality.string_of_equality x))
488 prerr_endline ("-------");
489 prerr_endline ("+++++++"));
496 CicTypeChecker.type_of_aux' metasenv context term ugraph
498 C.Implicit None, ugraph
501 find_matches metasenv context ugraph lift_amount term termty candidates
503 if Utils.debug_res then ignore(check_res res "demod1");
513 (res, tl @ [S.lift 1 t])
516 demodulation_aux ~from:"1" metasenv context ugraph table
520 | None -> (None, tl @ [S.lift 1 t])
521 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
526 | Some (_, subst, menv, ug, eq_found) ->
527 Some (C.Appl ll, subst, menv, ug, eq_found)
529 | C.Prod (nn, s, t) ->
531 demodulation_aux ~from:"2"
532 metasenv context ugraph table lift_amount s in (
536 demodulation_aux metasenv
537 ((Some (nn, C.Decl s))::context) ugraph
538 table (lift_amount+1) t
542 | Some (t', subst, menv, ug, eq_found) ->
543 Some (C.Prod (nn, (S.lift 1 s), t'),
544 subst, menv, ug, eq_found)
546 | Some (s', subst, menv, ug, eq_found) ->
547 Some (C.Prod (nn, s', (S.lift 1 t)),
548 subst, menv, ug, eq_found)
550 | C.Lambda (nn, s, t) ->
553 metasenv context ugraph table lift_amount s in (
557 demodulation_aux metasenv
558 ((Some (nn, C.Decl s))::context) ugraph
559 table (lift_amount+1) t
563 | Some (t', subst, menv, ug, eq_found) ->
564 Some (C.Lambda (nn, (S.lift 1 s), t'),
565 subst, menv, ug, eq_found)
567 | Some (s', subst, menv, ug, eq_found) ->
568 Some (C.Lambda (nn, s', (S.lift 1 t)),
569 subst, menv, ug, eq_found)
574 if Utils.debug_res then ignore(check_res res "demod_aux output");
579 let build_newtarget_time = ref 0.;;
582 let demod_counter = ref 1;;
586 let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"
588 (** demodulation, when target is an equality *)
589 let rec demodulation_equality ?from newmeta env table sign target =
590 let module C = Cic in
591 let module S = CicSubstitution in
592 let module M = CicMetaSubst in
593 let module HL = HelmLibraryObjects in
594 let module U = Utils in
595 let metasenv, context, ugraph = env in
596 let w, ((proof_new, proof_old) as proof),
597 (eq_ty, left, right, order), metas, id =
598 Equality.open_equality target in
599 (* first, we simplify *)
600 let right = U.guarded_simpl context right in
601 let left = U.guarded_simpl context left in
602 let order = !Utils.compare_terms left right in
603 let stat = (eq_ty, left, right, order) in
604 let w = Utils.compute_equality_weight stat in
605 let target = Equality.mk_equality (w, proof, stat, metas) in
606 if Utils.debug_metas then
607 ignore(check_target context target "demod equalities input");
608 let metasenv' = (* metasenv @ *) metas in
609 let maxmeta = ref newmeta in
611 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
612 let time1 = Unix.gettimeofday () in
614 if Utils.debug_metas then
616 ignore(check_for_duplicates menv "input1");
617 ignore(check_disjoint_invariant subst menv "input2");
618 let substs = Equality.ppsubst subst in
619 ignore(check_target context (snd eq_found) ("input3" ^ substs))
621 let pos, equality = eq_found in
622 let (_, (proof'_new,proof'_old),
623 (ty, what, other, _), menv',id') = Equality.open_equality equality in
625 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
626 with CicUtil.Meta_not_found _ -> ty
628 let what, other = if pos = Utils.Left then what, other else other, what in
629 let newterm, newproof =
631 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
632 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
633 let name = C.Name "x" in
636 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
637 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
638 S.lift 1 eq_ty; l; r]
640 if sign = Utils.Positive then
642 (Equality.Step (subst,(Equality.Demodulation,id,(pos,id'),
643 (*apply_subst subst*) (Cic.Lambda (name, ty, bo')))),
644 Equality.ProofBlock (
645 subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof_old)))
650 prerr_endline "***************************************negative";
654 CicMkImplicit.identity_relocation_list_for_metavariable context in
655 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
656 (* print_newline (); *)
657 C.Meta (!maxmeta, irl)
662 if pos = Utils.Left then [ty; what; other]
663 else [ty; other; what]
665 Equality.ProofSymBlock (termlist, proof'_old)
667 let proof'_new' = assert false (* not implemented *) in
669 if pos = Utils.Left then what, other else other, what
673 (0, (proof'_new',proof'_old'),
674 (ty, other, what, Utils.Incomparable),menv')
679 (subst, eq_URI, (name, ty), bo',
680 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
682 assert false, (* not implemented *)
683 (match snd proof with
684 | Equality.BasicProof _ ->
685 (* print_endline "replacing a BasicProof"; *)
687 | Equality.ProofGoalBlock (_, parent_proof) ->
688 (* print_endline "replacing another ProofGoalBlock"; *)
689 Equality.ProofGoalBlock (pb, parent_proof)
693 C.Appl [C.MutConstruct (* reflexivity *)
694 (LibraryObjects.eq_URI (), 0, 1, []);
695 eq_ty; if is_left then right else left]
698 (assert false, (* not implemented *)
699 Equality.ProofGoalBlock
700 (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
704 let newmenv = (* Inference.filter subst *) menv in
706 if Utils.debug_metas then
707 try ignore(CicTypeChecker.type_of_aux'
709 (Equality.build_proof_term_old (snd newproof)) ugraph);
712 prerr_endline "sempre lui";
713 prerr_endline (Equality.ppsubst subst);
714 prerr_endline (CicPp.ppterm
715 (Equality.build_proof_term_old (snd newproof)));
716 prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
717 prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
718 prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
719 prerr_endline ("+++++++++++++subst: " ^ (Equality.ppsubst subst));
720 prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
725 let left, right = if is_left then newterm, right else left, newterm in
726 let ordering = !Utils.compare_terms left right in
727 let stat = (eq_ty, left, right, ordering) in
728 let time2 = Unix.gettimeofday () in
729 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
731 let w = Utils.compute_equality_weight stat in
732 Equality.mk_equality (w, newproof, stat,newmenv)
734 if Utils.debug_metas then
735 ignore(check_target context res "buildnew_target output");
738 let build_newtarget is_left x =
739 profiler.HExtlib.profile (build_newtarget is_left) x
742 let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
743 if Utils.debug_res then check_res res "demod result";
744 let newmeta, newtarget =
747 let newmeta, newtarget = build_newtarget true t in
748 if (Equality.is_weak_identity newtarget) ||
749 (Equality.meta_convertibility_eq target newtarget) then
752 demodulation_equality newmeta env table sign newtarget
754 let res = demodulation_aux metasenv' context ugraph table 0 right in
755 if Utils.debug_res then check_res res "demod result 1";
758 let newmeta, newtarget = build_newtarget false t in
759 if (Equality.is_weak_identity newtarget) ||
760 (Equality.meta_convertibility_eq target newtarget) then
763 demodulation_equality newmeta env table sign newtarget
767 (* newmeta, newtarget *)
772 Performs the beta expansion of the term "term" w.r.t. "table",
773 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
776 let rec betaexpand_term metasenv context ugraph table lift_amount term =
777 let module C = Cic in
778 let module S = CicSubstitution in
779 let module M = CicMetaSubst in
780 let module HL = HelmLibraryObjects in
781 let candidates = get_candidates Unification table term in
783 let res, lifted_term =
788 (fun arg (res, lifted_tl) ->
791 let arg_res, lifted_arg =
792 betaexpand_term metasenv context ugraph table
796 (fun (t, s, m, ug, eq_found) ->
797 (Some t)::lifted_tl, s, m, ug, eq_found)
802 (fun (l, s, m, ug, eq_found) ->
803 (Some lifted_arg)::l, s, m, ug, eq_found)
805 (Some lifted_arg)::lifted_tl)
808 (fun (r, s, m, ug, eq_found) ->
809 None::r, s, m, ug, eq_found) res,
815 (fun (l, s, m, ug, eq_found) ->
816 (C.Meta (i, l), s, m, ug, eq_found)) l'
818 e, C.Meta (i, lifted_l)
821 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
823 | C.Prod (nn, s, t) ->
825 betaexpand_term metasenv context ugraph table lift_amount s in
827 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
828 table (lift_amount+1) t in
831 (fun (t, s, m, ug, eq_found) ->
832 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
835 (fun (t, s, m, ug, eq_found) ->
836 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
837 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
839 | C.Lambda (nn, s, t) ->
841 betaexpand_term metasenv context ugraph table lift_amount s in
843 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
844 table (lift_amount+1) t in
847 (fun (t, s, m, ug, eq_found) ->
848 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
851 (fun (t, s, m, ug, eq_found) ->
852 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
853 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
858 (fun arg (res, lifted_tl) ->
859 let arg_res, lifted_arg =
860 betaexpand_term metasenv context ugraph table lift_amount arg
864 (fun (a, s, m, ug, eq_found) ->
865 a::lifted_tl, s, m, ug, eq_found)
870 (fun (r, s, m, ug, eq_found) ->
871 lifted_arg::r, s, m, ug, eq_found)
873 lifted_arg::lifted_tl)
877 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
880 | t -> [], (S.lift lift_amount t)
883 | C.Meta (i, l) -> res, lifted_term
886 C.Implicit None, ugraph
887 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
891 metasenv context ugraph lift_amount term termty candidates
896 let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
898 let betaexpand_term metasenv context ugraph table lift_amount term =
899 profiler.HExtlib.profile
900 (betaexpand_term metasenv context ugraph table lift_amount) term
903 let sup_l_counter = ref 1;;
907 returns a list of new clauses inferred with a left superposition step
908 the negative equation "target" and one of the positive equations in "table"
910 let superposition_left newmeta (metasenv, context, ugraph) table target =
913 let superposition_left newmeta (metasenv, context, ugraph) table target =
914 let module C = Cic in
915 let module S = CicSubstitution in
916 let module M = CicMetaSubst in
917 let module HL = HelmLibraryObjects in
918 let module CR = CicReduction in
919 let module U = Utils in
920 let weight, proof, (eq_ty, left, right, ordering), menv, id =
921 Equality.open_equality target
923 if Utils.debug_metas then
924 ignore(check_target context target "superpositionleft");
926 let term = if ordering = U.Gt then left else right in
927 betaexpand_term metasenv context ugraph table 0 term
929 let maxmeta = ref newmeta in
930 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
931 (* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
932 let time1 = Unix.gettimeofday () in
934 let pos, equality = eq_found in
935 let _,proof',(ty,what,other,_),menv',id'=Equality.open_equality equality in
936 let proof'_new, proof'_old = proof' in
937 let what, other = if pos = Utils.Left then what, other else other, what in
938 let newgoal, newproof =
939 let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
940 let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
944 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
945 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
946 S.lift 1 eq_ty; l; r]
951 CicMkImplicit.identity_relocation_list_for_metavariable context in
952 C.Meta (!maxmeta, irl)
957 if pos = Utils.Left then [ty; what; other]
958 else [ty; other; what]
960 proof'_new, (* MAH????? *)
961 Equality.ProofSymBlock (termlist, proof'_old)
964 if pos = Utils.Left then what, other else other, what
968 (0, proof', (ty, other, what, Utils.Incomparable), menv')
970 let target_proof = assert false (*
973 (s, eq_URI, (name, ty), bo'', eq_found,
974 Equality.BasicProof (Equality.empty_subst,metaproof))
977 | Equality.BasicProof _ ->
978 (* debug_print (lazy "replacing a BasicProof"); *)
980 | Equality.ProofGoalBlock (_, parent_proof) ->
981 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
982 Equality.ProofGoalBlock (pb, parent_proof)
983 | _ -> assert false*)
986 C.Appl [C.MutConstruct (* reflexivity *)
987 (LibraryObjects.eq_URI (), 0, 1, []);
988 eq_ty; if ordering = U.Gt then right else left]
991 (Equality.Step (Equality.SuperpositionLeft,id,(pos,id'),
992 assert false), (* il predicato della beta expand non viene tenuto? *)
993 Equality.ProofGoalBlock
994 (Equality.BasicProof (Equality.empty_subst,refl), target_proof)))
997 if ordering = U.Gt then newgoal, right else left, newgoal in
998 let neworder = !Utils.compare_terms left right in
999 let stat = (eq_ty, left, right, neworder) in
1000 let newmenv = (* Inference.filter s *) menv in
1001 let time2 = Unix.gettimeofday () in
1002 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1004 let w = Utils.compute_equality_weight stat in
1005 Equality.mk_equality (w, newproof, stat, newmenv)
1008 !maxmeta, List.map build_new expansions
1012 let sup_r_counter = ref 1;;
1016 returns a list of new clauses inferred with a right superposition step
1017 between the positive equation "target" and one in the "table" "newmeta" is
1018 the first free meta index, i.e. the first number above the highest meta
1019 index: its updated value is also returned
1021 let superposition_right newmeta (metasenv, context, ugraph) table target =
1022 let module C = Cic in
1023 let module S = CicSubstitution in
1024 let module M = CicMetaSubst in
1025 let module HL = HelmLibraryObjects in
1026 let module CR = CicReduction in
1027 let module U = Utils in
1028 let w, (eqproof1,eqproof2), (eq_ty, left, right, ordering), newmetas,id =
1029 Equality.open_equality target
1031 if Utils.debug_metas then
1032 ignore (check_target context target "superpositionright");
1033 let metasenv' = newmetas in
1034 let maxmeta = ref newmeta in
1036 let betaexpand_term metasenv context ugraph table d term =
1037 let t1 = Unix.gettimeofday () in
1038 let res = betaexpand_term metasenv context ugraph table d term in
1039 let t2 = Unix.gettimeofday () in
1040 beta_expand_time := !beta_expand_time +. (t2 -. t1);
1044 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
1045 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
1049 (fun (_, subst, _, _, _) ->
1050 let subst = apply_subst subst in
1051 let o = !Utils.compare_terms (subst l) (subst r) in
1052 o <> U.Lt && o <> U.Le)
1053 (fst (betaexpand_term metasenv' context ugraph table 0 l))
1055 (res left right), (res right left)
1057 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
1058 if Utils.debug_metas then
1059 ignore (check_target context (snd eq_found) "buildnew1" );
1060 let time1 = Unix.gettimeofday () in
1062 let pos, equality = eq_found in
1063 let (_, proof', (ty, what, other, _), menv',id') =
1064 Equality.open_equality equality in
1065 let what, other = if pos = Utils.Left then what, other else other, what in
1066 let newgoal, newproof =
1068 let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
1069 (* let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in*)
1070 let name = C.Name "x" in
1074 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1075 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1076 S.lift 1 eq_ty; l; r]
1079 ( Equality.Step (s,(Equality.SuperpositionRight,
1080 id,(pos,id'),(*apply_subst s*) (Cic.Lambda(name,ty,bo'')))),
1081 Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2))
1084 let newmeta, newequality =
1086 if ordering = U.Gt then newgoal, apply_subst s right
1087 else apply_subst s left, newgoal in
1088 let neworder = !Utils.compare_terms left right in
1089 let newmenv = (* Inference.filter s *) m in
1090 let stat = (eq_ty, left, right, neworder) in
1092 let w = Utils.compute_equality_weight stat in
1093 Equality.mk_equality (w, newproof, stat, newmenv) in
1094 if Utils.debug_metas then
1095 ignore (check_target context eq' "buildnew3");
1096 let newm, eq' = Equality.fix_metas !maxmeta eq' in
1097 if Utils.debug_metas then
1098 ignore (check_target context eq' "buildnew4");
1102 let time2 = Unix.gettimeofday () in
1103 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1104 if Utils.debug_metas then
1105 ignore(check_target context newequality "buildnew2");
1108 let new1 = List.map (build_new U.Gt) res1
1109 and new2 = List.map (build_new U.Lt) res2 in
1110 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1112 (List.filter ok (new1 @ new2)))
1116 (** demodulation, when the target is a goal *)
1117 let rec demodulation_goal newmeta env table goal =
1118 let module C = Cic in
1119 let module S = CicSubstitution in
1120 let module M = CicMetaSubst in
1121 let module HL = HelmLibraryObjects in
1122 let metasenv, context, ugraph = env in
1123 let maxmeta = ref newmeta in
1124 let (cicproof,proof), metas, term = goal in
1125 let term = Utils.guarded_simpl (~debug:true) context term in
1126 let goal = (cicproof,proof), metas, term in
1127 let metasenv' = metas in
1129 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1130 let pos, equality = eq_found in
1131 let (_, (proofnew',proof'), (ty, what, other, _), menv',id) =
1132 Equality.open_equality equality in
1133 let what, other = if pos = Utils.Left then what, other else other, what in
1135 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
1136 with CicUtil.Meta_not_found _ -> ty
1138 let newterm, newproof, newcicproof =
1140 Utils.guarded_simpl context (apply_subst subst(S.subst other t))
1142 let bo' = apply_subst subst t in
1143 (* let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in*)
1144 let name = C.Name "x" in
1149 CicMkImplicit.identity_relocation_list_for_metavariable context *) in
1150 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
1151 C.Meta (!maxmeta, irl)
1154 let eq_found_proof =
1156 if pos = Utils.Left then [ty; what; other]
1157 else [ty; other; what]
1159 Equality.ProofSymBlock (termlist, proof')
1162 if pos = Utils.Left then what, other else other, what
1165 Equality.mk_equality
1166 (0,(proofnew',eq_found_proof), (ty, other, what, Utils.Incomparable), menv')
1171 (subst, eq_URI, (name, ty), bo',
1172 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
1174 let rec repl = function
1175 | Equality.NoProof ->
1176 (* debug_print (lazy "replacing a NoProof"); *)
1178 | Equality.BasicProof _ ->
1179 (* debug_print (lazy "replacing a BasicProof"); *)
1181 | Equality.ProofGoalBlock (_, parent_proof) ->
1182 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
1183 Equality.ProofGoalBlock (pb, parent_proof)
1184 | Equality.SubProof (term, meta_index, p) ->
1185 prerr_endline "subproof!";
1186 Equality.SubProof (term, meta_index, repl p)
1190 let newcicproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
1191 bo, Equality.ProofGoalBlock (Equality.NoProof, goal_proof),
1192 (newcicproofstep::cicproof)
1194 let newmetasenv = (* Inference.filter subst *) menv in
1195 !maxmeta, ((newcicproof,newproof), newmetasenv, newterm)
1198 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
1202 let newmeta, newgoal = build_newgoal t in
1203 let _, _, newg = newgoal in
1204 if Equality.meta_convertibility term newg then
1205 true, newmeta, newgoal
1207 demodulation_goal newmeta env table newgoal
1209 false, newmeta, goal
1212 (** demodulation, when the target is a theorem *)
1213 let rec demodulation_theorem newmeta env table theorem =
1214 let module C = Cic in
1215 let module S = CicSubstitution in
1216 let module M = CicMetaSubst in
1217 let module HL = HelmLibraryObjects in
1218 let metasenv, context, ugraph = env in
1219 let maxmeta = ref newmeta in
1220 let term, termty, metas = theorem in
1221 let metasenv' = metas in
1223 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1224 let pos, equality = eq_found in
1225 let (_, proof', (ty, what, other, _), menv',id) =
1226 Equality.open_equality equality in
1227 let what, other = if pos = Utils.Left then what, other else other, what in
1228 let newterm, newty =
1229 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1230 let bo' = apply_subst subst t in
1231 let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1234 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1235 Equality.BasicProof (Equality.empty_subst,term))
1237 (Equality.build_proof_term_old newproofold, bo)
1239 !maxmeta, (newterm, newty, menv)
1242 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1246 let newmeta, newthm = build_newtheorem t in
1247 let newt, newty, _ = newthm in
1248 if Equality.meta_convertibility termty newty then
1251 demodulation_theorem newmeta env table newthm