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 assert (not (Equality.meta_convertibility_eq target newtarget));
749 if (Equality.is_weak_identity newtarget) ||
750 (Equality.meta_convertibility_eq target newtarget) then
753 demodulation_equality newmeta env table sign newtarget
755 let res = demodulation_aux metasenv' context ugraph table 0 right in
756 if Utils.debug_res then check_res res "demod result 1";
759 let newmeta, newtarget = build_newtarget false t in
760 if (Equality.is_weak_identity newtarget) ||
761 (Equality.meta_convertibility_eq target newtarget) then
764 demodulation_equality newmeta env table sign newtarget
768 (* newmeta, newtarget *)
773 Performs the beta expansion of the term "term" w.r.t. "table",
774 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
777 let rec betaexpand_term metasenv context ugraph table lift_amount term =
778 let module C = Cic in
779 let module S = CicSubstitution in
780 let module M = CicMetaSubst in
781 let module HL = HelmLibraryObjects in
782 let candidates = get_candidates Unification table term in
784 let res, lifted_term =
789 (fun arg (res, lifted_tl) ->
792 let arg_res, lifted_arg =
793 betaexpand_term metasenv context ugraph table
797 (fun (t, s, m, ug, eq_found) ->
798 (Some t)::lifted_tl, s, m, ug, eq_found)
803 (fun (l, s, m, ug, eq_found) ->
804 (Some lifted_arg)::l, s, m, ug, eq_found)
806 (Some lifted_arg)::lifted_tl)
809 (fun (r, s, m, ug, eq_found) ->
810 None::r, s, m, ug, eq_found) res,
816 (fun (l, s, m, ug, eq_found) ->
817 (C.Meta (i, l), s, m, ug, eq_found)) l'
819 e, C.Meta (i, lifted_l)
822 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
824 | C.Prod (nn, s, t) ->
826 betaexpand_term metasenv context ugraph table lift_amount s in
828 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
829 table (lift_amount+1) t in
832 (fun (t, s, m, ug, eq_found) ->
833 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
836 (fun (t, s, m, ug, eq_found) ->
837 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
838 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
840 | C.Lambda (nn, s, t) ->
842 betaexpand_term metasenv context ugraph table lift_amount s in
844 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
845 table (lift_amount+1) t in
848 (fun (t, s, m, ug, eq_found) ->
849 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
852 (fun (t, s, m, ug, eq_found) ->
853 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
854 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
859 (fun arg (res, lifted_tl) ->
860 let arg_res, lifted_arg =
861 betaexpand_term metasenv context ugraph table lift_amount arg
865 (fun (a, s, m, ug, eq_found) ->
866 a::lifted_tl, s, m, ug, eq_found)
871 (fun (r, s, m, ug, eq_found) ->
872 lifted_arg::r, s, m, ug, eq_found)
874 lifted_arg::lifted_tl)
878 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
881 | t -> [], (S.lift lift_amount t)
884 | C.Meta (i, l) -> res, lifted_term
887 C.Implicit None, ugraph
888 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
892 metasenv context ugraph lift_amount term termty candidates
897 let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
899 let betaexpand_term metasenv context ugraph table lift_amount term =
900 profiler.HExtlib.profile
901 (betaexpand_term metasenv context ugraph table lift_amount) term
904 let sup_l_counter = ref 1;;
908 returns a list of new clauses inferred with a left superposition step
909 the negative equation "target" and one of the positive equations in "table"
911 let superposition_left newmeta (metasenv, context, ugraph) table target =
914 let superposition_left newmeta (metasenv, context, ugraph) table target =
915 let module C = Cic in
916 let module S = CicSubstitution in
917 let module M = CicMetaSubst in
918 let module HL = HelmLibraryObjects in
919 let module CR = CicReduction in
920 let module U = Utils in
921 let weight, proof, (eq_ty, left, right, ordering), menv, id =
922 Equality.open_equality target
924 if Utils.debug_metas then
925 ignore(check_target context target "superpositionleft");
927 let term = if ordering = U.Gt then left else right in
928 betaexpand_term metasenv context ugraph table 0 term
930 let maxmeta = ref newmeta in
931 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
932 (* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
933 let time1 = Unix.gettimeofday () in
935 let pos, equality = eq_found in
936 let _,proof',(ty,what,other,_),menv',id'=Equality.open_equality equality in
937 let proof'_new, proof'_old = proof' in
938 let what, other = if pos = Utils.Left then what, other else other, what in
939 let newgoal, newproof =
940 let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
941 let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
945 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
946 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
947 S.lift 1 eq_ty; l; r]
952 CicMkImplicit.identity_relocation_list_for_metavariable context in
953 C.Meta (!maxmeta, irl)
958 if pos = Utils.Left then [ty; what; other]
959 else [ty; other; what]
961 proof'_new, (* MAH????? *)
962 Equality.ProofSymBlock (termlist, proof'_old)
965 if pos = Utils.Left then what, other else other, what
969 (0, proof', (ty, other, what, Utils.Incomparable), menv')
971 let target_proof = assert false (*
974 (s, eq_URI, (name, ty), bo'', eq_found,
975 Equality.BasicProof (Equality.empty_subst,metaproof))
978 | Equality.BasicProof _ ->
979 (* debug_print (lazy "replacing a BasicProof"); *)
981 | Equality.ProofGoalBlock (_, parent_proof) ->
982 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
983 Equality.ProofGoalBlock (pb, parent_proof)
984 | _ -> assert false*)
987 C.Appl [C.MutConstruct (* reflexivity *)
988 (LibraryObjects.eq_URI (), 0, 1, []);
989 eq_ty; if ordering = U.Gt then right else left]
992 (Equality.Step (Equality.SuperpositionLeft,id,(pos,id'),
993 assert false), (* il predicato della beta expand non viene tenuto? *)
994 Equality.ProofGoalBlock
995 (Equality.BasicProof (Equality.empty_subst,refl), target_proof)))
998 if ordering = U.Gt then newgoal, right else left, newgoal in
999 let neworder = !Utils.compare_terms left right in
1000 let stat = (eq_ty, left, right, neworder) in
1001 let newmenv = (* Inference.filter s *) menv in
1002 let time2 = Unix.gettimeofday () in
1003 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1005 let w = Utils.compute_equality_weight stat in
1006 Equality.mk_equality (w, newproof, stat, newmenv)
1009 !maxmeta, List.map build_new expansions
1013 let sup_r_counter = ref 1;;
1017 returns a list of new clauses inferred with a right superposition step
1018 between the positive equation "target" and one in the "table" "newmeta" is
1019 the first free meta index, i.e. the first number above the highest meta
1020 index: its updated value is also returned
1022 let superposition_right newmeta (metasenv, context, ugraph) table target =
1023 let module C = Cic in
1024 let module S = CicSubstitution in
1025 let module M = CicMetaSubst in
1026 let module HL = HelmLibraryObjects in
1027 let module CR = CicReduction in
1028 let module U = Utils in
1029 let w, (eqproof1,eqproof2), (eq_ty, left, right, ordering), newmetas,id =
1030 Equality.open_equality target
1032 if Utils.debug_metas then
1033 ignore (check_target context target "superpositionright");
1034 let metasenv' = newmetas in
1035 let maxmeta = ref newmeta in
1037 let betaexpand_term metasenv context ugraph table d term =
1038 let t1 = Unix.gettimeofday () in
1039 let res = betaexpand_term metasenv context ugraph table d term in
1040 let t2 = Unix.gettimeofday () in
1041 beta_expand_time := !beta_expand_time +. (t2 -. t1);
1045 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
1046 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
1050 (fun (_, subst, _, _, _) ->
1051 let subst = apply_subst subst in
1052 let o = !Utils.compare_terms (subst l) (subst r) in
1053 o <> U.Lt && o <> U.Le)
1054 (fst (betaexpand_term metasenv' context ugraph table 0 l))
1056 (res left right), (res right left)
1058 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
1059 if Utils.debug_metas then
1060 ignore (check_target context (snd eq_found) "buildnew1" );
1061 let time1 = Unix.gettimeofday () in
1063 let pos, equality = eq_found in
1064 let (_, proof', (ty, what, other, _), menv',id') =
1065 Equality.open_equality equality in
1066 let what, other = if pos = Utils.Left then what, other else other, what in
1067 let newgoal, newproof =
1069 let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
1070 (* let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in*)
1071 let name = C.Name "x" in
1075 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1076 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1077 S.lift 1 eq_ty; l; r]
1080 ( Equality.Step (s,(Equality.SuperpositionRight,
1081 id,(pos,id'),(*apply_subst s*) (Cic.Lambda(name,ty,bo'')))),
1082 Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2))
1085 let newmeta, newequality =
1087 if ordering = U.Gt then newgoal, apply_subst s right
1088 else apply_subst s left, newgoal in
1089 let neworder = !Utils.compare_terms left right in
1090 let newmenv = (* Inference.filter s *) m in
1091 let stat = (eq_ty, left, right, neworder) in
1093 let w = Utils.compute_equality_weight stat in
1094 Equality.mk_equality (w, newproof, stat, newmenv) in
1095 if Utils.debug_metas then
1096 ignore (check_target context eq' "buildnew3");
1097 let newm, eq' = Equality.fix_metas !maxmeta eq' in
1098 if Utils.debug_metas then
1099 ignore (check_target context eq' "buildnew4");
1103 let time2 = Unix.gettimeofday () in
1104 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1105 if Utils.debug_metas then
1106 ignore(check_target context newequality "buildnew2");
1109 let new1 = List.map (build_new U.Gt) res1
1110 and new2 = List.map (build_new U.Lt) res2 in
1111 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1113 (List.filter ok (new1 @ new2)))
1117 (** demodulation, when the target is a goal *)
1118 let rec demodulation_goal newmeta env table goal =
1119 let module C = Cic in
1120 let module S = CicSubstitution in
1121 let module M = CicMetaSubst in
1122 let module HL = HelmLibraryObjects in
1123 let metasenv, context, ugraph = env in
1124 let maxmeta = ref newmeta in
1125 let (cicproof,proof), metas, term = goal in
1126 let term = Utils.guarded_simpl (~debug:true) context term in
1127 let goal = (cicproof,proof), metas, term in
1128 let metasenv' = metas in
1130 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1131 let pos, equality = eq_found in
1132 let (_, (proofnew',proof'), (ty, what, other, _), menv',id) =
1133 Equality.open_equality equality in
1134 let what, other = if pos = Utils.Left then what, other else other, what in
1136 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
1137 with CicUtil.Meta_not_found _ -> ty
1139 let newterm, newproof, newcicproof =
1141 Utils.guarded_simpl context (apply_subst subst(S.subst other t))
1143 let bo' = apply_subst subst t in
1144 (* let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in*)
1145 let name = C.Name "x" in
1150 CicMkImplicit.identity_relocation_list_for_metavariable context *) in
1151 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
1152 C.Meta (!maxmeta, irl)
1155 let eq_found_proof =
1157 if pos = Utils.Left then [ty; what; other]
1158 else [ty; other; what]
1160 Equality.ProofSymBlock (termlist, proof')
1163 if pos = Utils.Left then what, other else other, what
1166 Equality.mk_equality
1167 (0,(proofnew',eq_found_proof), (ty, other, what, Utils.Incomparable), menv')
1172 (subst, eq_URI, (name, ty), bo',
1173 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
1175 let rec repl = function
1176 | Equality.NoProof ->
1177 (* debug_print (lazy "replacing a NoProof"); *)
1179 | Equality.BasicProof _ ->
1180 (* debug_print (lazy "replacing a BasicProof"); *)
1182 | Equality.ProofGoalBlock (_, parent_proof) ->
1183 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
1184 Equality.ProofGoalBlock (pb, parent_proof)
1185 | Equality.SubProof (term, meta_index, p) ->
1186 prerr_endline "subproof!";
1187 Equality.SubProof (term, meta_index, repl p)
1191 let newcicproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
1192 bo, Equality.ProofGoalBlock (Equality.NoProof, goal_proof),
1193 (newcicproofstep::cicproof)
1195 let newmetasenv = (* Inference.filter subst *) menv in
1196 !maxmeta, ((newcicproof,newproof), newmetasenv, newterm)
1199 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
1203 let newmeta, newgoal = build_newgoal t in
1204 let _, _, newg = newgoal in
1205 if Equality.meta_convertibility term newg then
1206 false, newmeta, newgoal
1208 let changed, newmeta, newgoal =
1209 demodulation_goal newmeta env table newgoal
1211 true, newmeta, newgoal
1213 false, newmeta, goal
1216 (** demodulation, when the target is a theorem *)
1217 let rec demodulation_theorem newmeta env table theorem =
1218 let module C = Cic in
1219 let module S = CicSubstitution in
1220 let module M = CicMetaSubst in
1221 let module HL = HelmLibraryObjects in
1222 let metasenv, context, ugraph = env in
1223 let maxmeta = ref newmeta in
1224 let term, termty, metas = theorem in
1225 let metasenv' = metas in
1227 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1228 let pos, equality = eq_found in
1229 let (_, proof', (ty, what, other, _), menv',id) =
1230 Equality.open_equality equality in
1231 let what, other = if pos = Utils.Left then what, other else other, what in
1232 let newterm, newty =
1233 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1234 let bo' = apply_subst subst t in
1235 let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1238 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1239 Equality.BasicProof (Equality.empty_subst,term))
1241 (Equality.build_proof_term_old newproofold, bo)
1243 !maxmeta, (newterm, newty, menv)
1246 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1250 let newmeta, newthm = build_newtheorem t in
1251 let newt, newty, _ = newthm in
1252 if Equality.meta_convertibility termty newty then
1255 demodulation_theorem newmeta env table newthm