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 = Subst.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,_,_) -> (Subst.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 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 Subst.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, (eq_ty, left, right, order), metas, id =
597 Equality.open_equality target
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 = Subst.ppsubst subst in
619 ignore(check_target context (snd eq_found) ("input3" ^ substs))
621 let pos, equality = eq_found in
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
641 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
642 (Cic.Lambda (name, ty, bo'))))))
647 prerr_endline "***************************************negative";
651 CicMkImplicit.identity_relocation_list_for_metavariable context in
652 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
653 (* print_newline (); *)
654 C.Meta (!maxmeta, irl)
659 if pos = Utils.Left then [ty; what; other]
660 else [ty; other; what]
662 Equality.ProofSymBlock (termlist, proof'_old)
664 let proof'_new' = assert false (* not implemented *) in
666 if pos = Utils.Left then what, other else other, what
670 (0, (proof'_new',proof'_old'),
671 (ty, other, what, Utils.Incomparable),menv')
676 (subst, eq_URI, (name, ty), bo',
677 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
679 assert false, (* not implemented *)
680 (match snd proof with
681 | Equality.BasicProof _ ->
682 (* print_endline "replacing a BasicProof"; *)
684 | Equality.ProofGoalBlock (_, parent_proof) ->
685 (* print_endline "replacing another ProofGoalBlock"; *)
686 Equality.ProofGoalBlock (pb, parent_proof)
690 C.Appl [C.MutConstruct (* reflexivity *)
691 (LibraryObjects.eq_URI (), 0, 1, []);
692 eq_ty; if is_left then right else left]
695 (assert false, (* not implemented *)
696 Equality.ProofGoalBlock
697 (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
701 let newmenv = (* Inference.filter subst *) menv in
703 if Utils.debug_metas then
704 try ignore(CicTypeChecker.type_of_aux'
706 (Equality.build_proof_term newproof) ugraph);
709 prerr_endline "sempre lui";
710 prerr_endline (Subst.ppsubst subst);
711 prerr_endline (CicPp.ppterm
712 (Equality.build_proof_term newproof));
713 prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
714 prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
715 prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
716 prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
717 prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
722 let left, right = if is_left then newterm, right else left, newterm in
723 let ordering = !Utils.compare_terms left right in
724 let stat = (eq_ty, left, right, ordering) in
725 let time2 = Unix.gettimeofday () in
726 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
728 let w = Utils.compute_equality_weight stat in
729 Equality.mk_equality (w, newproof, stat,newmenv)
731 if Utils.debug_metas then
732 ignore(check_target context res "buildnew_target output");
735 let build_newtarget is_left x =
736 profiler.HExtlib.profile (build_newtarget is_left) x
739 let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
740 if Utils.debug_res then check_res res "demod result";
741 let newmeta, newtarget =
744 let newmeta, newtarget = build_newtarget true t in
745 assert (not (Equality.meta_convertibility_eq target newtarget));
746 if (Equality.is_weak_identity newtarget) ||
747 (Equality.meta_convertibility_eq target newtarget) then
750 demodulation_equality ?from newmeta env table sign newtarget
752 let res = demodulation_aux metasenv' context ugraph table 0 right in
753 if Utils.debug_res then check_res res "demod result 1";
756 let newmeta, newtarget = build_newtarget false t in
757 if (Equality.is_weak_identity newtarget) ||
758 (Equality.meta_convertibility_eq target newtarget) then
761 demodulation_equality ?from newmeta env table sign newtarget
765 (* newmeta, newtarget *)
770 Performs the beta expansion of the term "term" w.r.t. "table",
771 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
774 let rec betaexpand_term metasenv context ugraph table lift_amount term =
775 let module C = Cic in
776 let module S = CicSubstitution in
777 let module M = CicMetaSubst in
778 let module HL = HelmLibraryObjects in
779 let candidates = get_candidates Unification table term in
781 let res, lifted_term =
786 (fun arg (res, lifted_tl) ->
789 let arg_res, lifted_arg =
790 betaexpand_term metasenv context ugraph table
794 (fun (t, s, m, ug, eq_found) ->
795 (Some t)::lifted_tl, s, m, ug, eq_found)
800 (fun (l, s, m, ug, eq_found) ->
801 (Some lifted_arg)::l, s, m, ug, eq_found)
803 (Some lifted_arg)::lifted_tl)
806 (fun (r, s, m, ug, eq_found) ->
807 None::r, s, m, ug, eq_found) res,
813 (fun (l, s, m, ug, eq_found) ->
814 (C.Meta (i, l), s, m, ug, eq_found)) l'
816 e, C.Meta (i, lifted_l)
819 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
821 | C.Prod (nn, s, t) ->
823 betaexpand_term metasenv context ugraph table lift_amount s in
825 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
826 table (lift_amount+1) t in
829 (fun (t, s, m, ug, eq_found) ->
830 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
833 (fun (t, s, m, ug, eq_found) ->
834 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
835 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
837 | C.Lambda (nn, s, t) ->
839 betaexpand_term metasenv context ugraph table lift_amount s in
841 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
842 table (lift_amount+1) t in
845 (fun (t, s, m, ug, eq_found) ->
846 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
849 (fun (t, s, m, ug, eq_found) ->
850 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
851 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
856 (fun arg (res, lifted_tl) ->
857 let arg_res, lifted_arg =
858 betaexpand_term metasenv context ugraph table lift_amount arg
862 (fun (a, s, m, ug, eq_found) ->
863 a::lifted_tl, s, m, ug, eq_found)
868 (fun (r, s, m, ug, eq_found) ->
869 lifted_arg::r, s, m, ug, eq_found)
871 lifted_arg::lifted_tl)
875 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
878 | t -> [], (S.lift lift_amount t)
881 | C.Meta (i, l) -> res, lifted_term
884 C.Implicit None, ugraph
885 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
889 metasenv context ugraph lift_amount term termty candidates
894 let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
896 let betaexpand_term metasenv context ugraph table lift_amount term =
897 profiler.HExtlib.profile
898 (betaexpand_term metasenv context ugraph table lift_amount) term
901 let sup_l_counter = ref 1;;
905 returns a list of new clauses inferred with a left superposition step
906 the negative equation "target" and one of the positive equations in "table"
908 let superposition_left newmeta (metasenv, context, ugraph) table target =
911 let superposition_left newmeta (metasenv, context, ugraph) table target =
912 let module C = Cic in
913 let module S = CicSubstitution in
914 let module M = CicMetaSubst in
915 let module HL = HelmLibraryObjects in
916 let module CR = CicReduction in
917 let module U = Utils in
918 let weight, proof, (eq_ty, left, right, ordering), menv, id =
919 Equality.open_equality target
921 if Utils.debug_metas then
922 ignore(check_target context target "superpositionleft");
924 let term = if ordering = U.Gt then left else right in
925 betaexpand_term metasenv context ugraph table 0 term
927 let maxmeta = ref newmeta in
928 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
929 (* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
930 let time1 = Unix.gettimeofday () in
932 let pos, equality = eq_found in
933 let _,proof',(ty,what,other,_),menv',id'=Equality.open_equality equality in
934 let proof'_new, proof'_old = proof' in
935 let what, other = if pos = Utils.Left then what, other else other, what in
936 let newgoal, newproof =
937 let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
938 let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
942 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
943 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
944 S.lift 1 eq_ty; l; r]
949 CicMkImplicit.identity_relocation_list_for_metavariable context in
950 C.Meta (!maxmeta, irl)
955 if pos = Utils.Left then [ty; what; other]
956 else [ty; other; what]
958 proof'_new, (* MAH????? *)
959 Equality.ProofSymBlock (termlist, proof'_old)
962 if pos = Utils.Left then what, other else other, what
966 (0, proof', (ty, other, what, Utils.Incomparable), menv')
968 let target_proof = assert false (*
971 (s, eq_URI, (name, ty), bo'', eq_found,
972 Equality.BasicProof (Equality.empty_subst,metaproof))
975 | Equality.BasicProof _ ->
976 (* debug_print (lazy "replacing a BasicProof"); *)
978 | Equality.ProofGoalBlock (_, parent_proof) ->
979 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
980 Equality.ProofGoalBlock (pb, parent_proof)
981 | _ -> assert false*)
984 C.Appl [C.MutConstruct (* reflexivity *)
985 (LibraryObjects.eq_URI (), 0, 1, []);
986 eq_ty; if ordering = U.Gt then right else left]
989 (Equality.Step (Equality.SuperpositionLeft,id,(pos,id'),
990 assert false), (* il predicato della beta expand non viene tenuto? *)
991 Equality.ProofGoalBlock
992 (Equality.BasicProof (Equality.empty_subst,refl), target_proof)))
995 if ordering = U.Gt then newgoal, right else left, newgoal in
996 let neworder = !Utils.compare_terms left right in
997 let stat = (eq_ty, left, right, neworder) in
998 let newmenv = (* Inference.filter s *) menv in
999 let time2 = Unix.gettimeofday () in
1000 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1002 let w = Utils.compute_equality_weight stat in
1003 Equality.mk_equality (w, newproof, stat, newmenv)
1006 !maxmeta, List.map build_new expansions
1010 let sup_r_counter = ref 1;;
1014 returns a list of new clauses inferred with a right superposition step
1015 between the positive equation "target" and one in the "table" "newmeta" is
1016 the first free meta index, i.e. the first number above the highest meta
1017 index: its updated value is also returned
1019 let superposition_right newmeta (metasenv, context, ugraph) table target =
1020 let module C = Cic in
1021 let module S = CicSubstitution in
1022 let module M = CicMetaSubst in
1023 let module HL = HelmLibraryObjects in
1024 let module CR = CicReduction in
1025 let module U = Utils in
1026 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
1027 Equality.open_equality target
1029 if Utils.debug_metas then
1030 ignore (check_target context target "superpositionright");
1031 let metasenv' = newmetas in
1032 let maxmeta = ref newmeta in
1034 let betaexpand_term metasenv context ugraph table d term =
1035 let t1 = Unix.gettimeofday () in
1036 let res = betaexpand_term metasenv context ugraph table d term in
1037 let t2 = Unix.gettimeofday () in
1038 beta_expand_time := !beta_expand_time +. (t2 -. t1);
1042 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
1043 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
1047 (fun (_, subst, _, _, _) ->
1048 let subst = apply_subst subst in
1049 let o = !Utils.compare_terms (subst l) (subst r) in
1050 o <> U.Lt && o <> U.Le)
1051 (fst (betaexpand_term metasenv' context ugraph table 0 l))
1053 (res left right), (res right left)
1055 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
1056 if Utils.debug_metas then
1057 ignore (check_target context (snd eq_found) "buildnew1" );
1058 let time1 = Unix.gettimeofday () in
1060 let pos, equality = eq_found in
1061 let (_, proof', (ty, what, other, _), menv',id') =
1062 Equality.open_equality equality in
1063 let what, other = if pos = Utils.Left then what, other else other, what in
1064 let newgoal, newproof =
1067 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
1069 let name = C.Name "x" in
1073 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1074 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1075 S.lift 1 eq_ty; l; r]
1079 (s,(Equality.SuperpositionRight,
1080 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
1082 let newmeta, newequality =
1084 if ordering = U.Gt then newgoal, apply_subst s right
1085 else apply_subst s left, newgoal in
1086 let neworder = !Utils.compare_terms left right in
1087 let newmenv = (* Inference.filter s *) m in
1088 let stat = (eq_ty, left, right, neworder) in
1090 let w = Utils.compute_equality_weight stat in
1091 Equality.mk_equality (w, newproof, stat, newmenv) in
1092 if Utils.debug_metas then
1093 ignore (check_target context eq' "buildnew3");
1094 let newm, eq' = Equality.fix_metas !maxmeta eq' in
1095 if Utils.debug_metas then
1096 ignore (check_target context eq' "buildnew4");
1100 let time2 = Unix.gettimeofday () in
1101 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1102 if Utils.debug_metas then
1103 ignore(check_target context newequality "buildnew2");
1106 let new1 = List.map (build_new U.Gt) res1
1107 and new2 = List.map (build_new U.Lt) res2 in
1108 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1110 (List.filter ok (new1 @ new2)))
1114 (** demodulation, when the target is a goal *)
1115 let rec demodulation_goal newmeta env table goal =
1116 let module C = Cic in
1117 let module S = CicSubstitution in
1118 let module M = CicMetaSubst in
1119 let module HL = HelmLibraryObjects in
1120 let metasenv, context, ugraph = env in
1121 let maxmeta = ref newmeta in
1122 let goalproof, metas, term = goal in
1123 let term = Utils.guarded_simpl (~debug:true) context term in
1124 let goal = goalproof, metas, term in
1125 let metasenv' = metas in
1127 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1128 let pos, equality = eq_found in
1129 let (_, proof', (ty, what, other, _), menv',id) =
1130 Equality.open_equality equality in
1131 let what, other = if pos = Utils.Left then what, other else other, what in
1133 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
1134 with CicUtil.Meta_not_found _ -> ty
1136 let newterm, newgoalproof =
1138 Utils.guarded_simpl context (apply_subst subst(S.subst other t))
1140 let bo' = (*apply_subst subst*) t in
1141 let name = C.Name "x" in
1143 let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
1144 bo, (newgoalproofstep::goalproof)
1146 let newmetasenv = (* Inference.filter subst *) menv in
1147 !maxmeta, (newgoalproof, newmetasenv, newterm)
1150 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
1154 let newmeta, newgoal = build_newgoal t in
1155 let _, _, newg = newgoal in
1156 if Equality.meta_convertibility term newg then
1157 false, newmeta, newgoal
1159 let changed, newmeta, newgoal =
1160 demodulation_goal newmeta env table newgoal
1162 true, newmeta, newgoal
1164 false, newmeta, goal
1167 (** demodulation, when the target is a theorem *)
1168 let rec demodulation_theorem newmeta env table theorem =
1169 let module C = Cic in
1170 let module S = CicSubstitution in
1171 let module M = CicMetaSubst in
1172 let module HL = HelmLibraryObjects in
1173 let metasenv, context, ugraph = env in
1174 let maxmeta = ref newmeta in
1175 let term, termty, metas = theorem in
1176 let metasenv' = metas in
1178 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1179 let pos, equality = eq_found in
1180 let (_, proof', (ty, what, other, _), menv',id) =
1181 Equality.open_equality equality in
1182 let what, other = if pos = Utils.Left then what, other else other, what in
1183 let newterm, newty =
1184 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1185 (* let bo' = apply_subst subst t in *)
1186 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
1190 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1191 Equality.BasicProof (Equality.empty_subst,term))
1193 (Equality.build_proof_term_old newproofold, bo)
1195 (* TODO, not ported to the new proofs *)
1196 if true then assert false; term, bo
1198 !maxmeta, (newterm, newty, menv)
1201 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1205 let newmeta, newthm = build_newtheorem t in
1206 let newt, newty, _ = newthm in
1207 if Equality.meta_convertibility termty newty then
1210 demodulation_theorem newmeta env table newthm