1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 type goal = Equality.goal_proof * Cic.metasenv * Cic.term
30 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
32 module Index = Equality_indexing.DT (* path tree based indexing *)
35 let beta_expand_time = ref 0.;;
37 let debug_print = Utils.debug_print;;
41 let check_equation env equation msg =
42 let w, proof, (eq_ty, left, right, order), metas, args = equation in
43 let metasenv, context, ugraph = env
44 let metasenv' = metasenv @ metas in
46 CicTypeChecker.type_of_aux' metasenv' context left ugraph;
47 CicTypeChecker.type_of_aux' metasenv' context right ugraph;
50 CicUtil.Meta_not_found _ as exn ->
53 prerr_endline (CicPp.ppterm left);
54 prerr_endline (CicPp.ppterm right);
59 type retrieval_mode = Matching | Unification;;
61 let string_of_res ?env =
64 | Some (t, s, m, u, ((p,e), eq_URI)) ->
65 Printf.sprintf "Some: (%s, %s, %s)"
66 (Utils.string_of_pos p)
67 (Equality.string_of_equality ?env e)
71 let print_res ?env res =
74 (List.map (string_of_res ?env) res))
77 let print_candidates ?env mode term res =
81 prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
83 prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
89 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
90 (Equality.string_of_equality ?env e))
95 let indexing_retrieval_time = ref 0.;;
98 let apply_subst = Subst.apply_subst
100 let index = Index.index
101 let remove_index = Index.remove_index
102 let in_index = Index.in_index
103 let empty = Index.empty
104 let init_index = Index.init_index
106 let check_disjoint_invariant subst metasenv msg =
108 (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
111 prerr_endline ("not disjoint: " ^ msg);
116 let check_for_duplicates metas msg =
117 if List.length metas <>
118 List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
120 prerr_endline ("DUPLICATI " ^ msg);
121 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
126 let check_res res msg =
128 Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
129 let eqs = Equality.string_of_equality (snd eq_found) in
130 check_disjoint_invariant subst menv msg;
131 check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
135 let check_target context target msg =
136 let w, proof, (eq_ty, left, right, order), metas,_ =
137 Equality.open_equality target in
138 (* check that metas does not contains duplicates *)
139 let eqs = Equality.string_of_equality target in
140 let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
141 let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
142 @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof) in
143 let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
144 let _ = if menv <> metas then
146 prerr_endline ("extra metas " ^ msg);
147 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
148 prerr_endline "**********************";
149 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
150 prerr_endline ("left: " ^ (CicPp.ppterm left));
151 prerr_endline ("right: " ^ (CicPp.ppterm right));
152 prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
158 ignore(CicTypeChecker.type_of_aux'
159 metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
162 prerr_endline (Inference.string_of_proof proof);
163 prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
164 prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
165 prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
170 (* returns a list of all the equalities in the tree that are in relation
171 "mode" with the given term, where mode can be either Matching or
174 Format of the return value: list of tuples in the form:
175 (position - Left or Right - of the term that matched the given one in this
179 Note that if equality is "left = right", if the ordering is left > right,
180 the position will always be Left, and if the ordering is left < right,
181 position will be Right.
184 let get_candidates ?env mode tree term =
185 let t1 = Unix.gettimeofday () in
189 | Matching -> Index.retrieve_generalizations tree term
190 | Unification -> Index.retrieve_unifiables tree term
192 Index.PosEqSet.elements s
194 (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
195 (* print_newline (); *)
196 let t2 = Unix.gettimeofday () in
197 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
198 (* make fresh instances *)
202 let profiler = HExtlib.profile "P/Indexing.get_candidates"
204 let get_candidates ?env mode tree term =
205 profiler.HExtlib.profile (get_candidates ?env mode tree) term
207 let match_unif_time_ok = ref 0.;;
208 let match_unif_time_no = ref 0.;;
212 finds the first equality in the index that matches "term", of type "termty"
213 termty can be Implicit if it is not needed. The result (one of the sides of
214 the equality, actually) should be not greater (wrt the term ordering) than
217 Format of the return value:
219 (term to substitute, [Cic.Rel 1 properly lifted - see the various
220 build_newtarget functions inside the various
221 demodulation_* functions]
222 substitution used for the matching,
224 ugraph, [substitution, metasenv and ugraph have the same meaning as those
225 returned by CicUnification.fo_unif]
226 (equality where the matching term was found, [i.e. the equality to use as
228 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
229 the equality: this is used to build the proof term, again see one of
230 the build_newtarget functions]
233 let rec find_matches metasenv context ugraph lift_amount term termty =
234 let module C = Cic in
235 let module U = Utils in
236 let module S = CicSubstitution in
237 let module M = CicMetaSubst in
238 let module HL = HelmLibraryObjects in
239 let cmp = !Utils.compare_terms in
240 let check = match termty with C.Implicit None -> false | _ -> true in
244 let pos, equality = candidate in
245 let (_, proof, (ty, left, right, o), metas,_) =
246 Equality.open_equality equality in
247 if Utils.debug_metas then
248 ignore(check_target context (snd candidate) "find_matches");
249 if Utils.debug_res then
251 let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
252 let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
253 let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
255 (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
257 check_for_duplicates metas "gia nella metas";
258 check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
260 if check && not (fst (CicReduction.are_convertible
261 ~metasenv context termty ty ugraph)) then (
262 find_matches metasenv context ugraph lift_amount term termty tl
264 let do_match c eq_URI =
265 let subst', metasenv', ugraph' =
266 let t1 = Unix.gettimeofday () in
269 ( Inference.matching metasenv metas context
270 term (S.lift lift_amount c)) ugraph
272 let t2 = Unix.gettimeofday () in
273 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
276 | Inference.MatchingFailure as e ->
277 let t2 = Unix.gettimeofday () in
278 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
280 | CicUtil.Meta_not_found _ as exn -> raise exn
282 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
285 let c, other, eq_URI =
286 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
287 else right, left, Utils.eq_ind_r_URI ()
289 if o <> U.Incomparable then
293 with Inference.MatchingFailure ->
294 find_matches metasenv context ugraph lift_amount term termty tl
296 if Utils.debug_res then ignore (check_res res "find1");
300 try do_match c eq_URI
301 with Inference.MatchingFailure -> None
303 if Utils.debug_res then ignore (check_res res "find2");
305 | Some (_, s, _, _, _) ->
306 let c' = apply_subst s c in
308 let other' = U.guarded_simpl context (apply_subst s other) in *)
309 let other' = apply_subst s other in
310 let order = cmp c' other' in
315 metasenv context ugraph lift_amount term termty tl
317 find_matches metasenv context ugraph lift_amount term termty tl
321 as above, but finds all the matching equalities, and the matching condition
322 can be either Inference.matching or Inference.unification
324 let rec find_all_matches ?(unif_fun=Inference.unification)
325 metasenv context ugraph lift_amount term termty =
326 let module C = Cic in
327 let module U = Utils in
328 let module S = CicSubstitution in
329 let module M = CicMetaSubst in
330 let module HL = HelmLibraryObjects in
331 let cmp = !Utils.compare_terms in
335 let pos, equality = candidate in
336 let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
337 let do_match c eq_URI =
338 let subst', metasenv', ugraph' =
339 let t1 = Unix.gettimeofday () in
342 unif_fun metasenv metas context
343 term (S.lift lift_amount c) ugraph in
344 let t2 = Unix.gettimeofday () in
345 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
348 | Inference.MatchingFailure
349 | CicUnification.UnificationFailure _
350 | CicUnification.Uncertain _ as e ->
351 let t2 = Unix.gettimeofday () in
352 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
355 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
358 let c, other, eq_URI =
359 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
360 else right, left, Utils.eq_ind_r_URI ()
362 if o <> U.Incomparable then
364 let res = do_match c eq_URI in
365 res::(find_all_matches ~unif_fun metasenv context ugraph
366 lift_amount term termty tl)
368 | Inference.MatchingFailure
369 | CicUnification.UnificationFailure _
370 | CicUnification.Uncertain _ ->
371 find_all_matches ~unif_fun metasenv context ugraph
372 lift_amount term termty tl
375 let res = do_match c eq_URI in
378 let c' = apply_subst s c
379 and other' = apply_subst s other in
380 let order = cmp c' other' in
381 if order <> U.Lt && order <> U.Le then
382 res::(find_all_matches ~unif_fun metasenv context ugraph
383 lift_amount term termty tl)
385 find_all_matches ~unif_fun metasenv context ugraph
386 lift_amount term termty tl
388 | Inference.MatchingFailure
389 | CicUnification.UnificationFailure _
390 | CicUnification.Uncertain _ ->
391 find_all_matches ~unif_fun metasenv context ugraph
392 lift_amount term termty tl
396 ?unif_fun metasenv context ugraph lift_amount term termty l
400 ?unif_fun metasenv context ugraph lift_amount term termty l
402 (*prerr_endline "CANDIDATES:";
403 List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
404 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
409 returns true if target is subsumed by some equality in table
411 let subsumption_aux use_unification env table target =
414 prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
415 ((pos,equation),_)) -> Inference.string_of_equality equation)l))
418 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
419 let metasenv, context, ugraph = env in
420 let metasenv = tmetas in
425 let leftc = get_candidates Matching table left in
426 find_all_matches ~unif_fun:Inference.matching
427 metasenv context ugraph 0 left ty leftc
429 (* print_res leftr;*)
430 let rec ok what = function
432 | (_, subst, menv, ug, ((pos,equation),_))::tl ->
433 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
435 let other = if pos = Utils.Left then r else l in
436 let subst', menv', ug' =
437 let t1 = Unix.gettimeofday () in
440 if use_unification then
441 Inference.unification metasenv m context what other ugraph
443 Inference.matching metasenv m context what other ugraph
445 let t2 = Unix.gettimeofday () in
446 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
448 with Inference.MatchingFailure as e ->
449 let t2 = Unix.gettimeofday () in
450 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
453 (match Subst.merge_subst_if_possible subst subst' with
455 | Some s -> Some (s, equation))
456 with Inference.MatchingFailure ->
459 match ok right leftr with
460 | Some _ as res -> res
466 let rightc = get_candidates Matching table right in
467 find_all_matches ~unif_fun:Inference.matching
468 metasenv context ugraph 0 right ty rightc
470 (* print_res rightr;*)
475 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
476 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
479 let subsumption = subsumption_aux false;;
480 let unification = subsumption_aux true;;
482 let rec demodulation_aux ?from ?(typecheck=false)
483 metasenv context ugraph table lift_amount term =
484 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
485 let module C = Cic in
486 let module S = CicSubstitution in
487 let module M = CicMetaSubst in
488 let module HL = HelmLibraryObjects in
490 get_candidates ~env:(metasenv,context,ugraph) (* Unification *) Matching table term in
491 if List.exists (fun (i,_,_) -> i = 2840) metasenv
493 (prerr_endline ("term: " ^(CicPp.ppterm term));
494 List.iter (fun (_,x) -> prerr_endline (Equality.string_of_equality x))
496 prerr_endline ("-------");
497 prerr_endline ("+++++++"));
504 CicTypeChecker.type_of_aux' metasenv context term ugraph
506 C.Implicit None, ugraph
509 find_matches metasenv context ugraph lift_amount term termty candidates
511 if Utils.debug_res then ignore(check_res res "demod1");
521 (res, tl @ [S.lift 1 t])
524 demodulation_aux ~from:"1" metasenv context ugraph table
528 | None -> (None, tl @ [S.lift 1 t])
529 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
534 | Some (_, subst, menv, ug, eq_found) ->
535 Some (C.Appl ll, subst, menv, ug, eq_found)
537 | C.Prod (nn, s, t) ->
539 demodulation_aux ~from:"2"
540 metasenv context ugraph table lift_amount s in (
544 demodulation_aux metasenv
545 ((Some (nn, C.Decl s))::context) ugraph
546 table (lift_amount+1) t
550 | Some (t', subst, menv, ug, eq_found) ->
551 Some (C.Prod (nn, (S.lift 1 s), t'),
552 subst, menv, ug, eq_found)
554 | Some (s', subst, menv, ug, eq_found) ->
555 Some (C.Prod (nn, s', (S.lift 1 t)),
556 subst, menv, ug, eq_found)
558 | C.Lambda (nn, s, t) ->
561 metasenv context ugraph table lift_amount s in (
565 demodulation_aux metasenv
566 ((Some (nn, C.Decl s))::context) ugraph
567 table (lift_amount+1) t
571 | Some (t', subst, menv, ug, eq_found) ->
572 Some (C.Lambda (nn, (S.lift 1 s), t'),
573 subst, menv, ug, eq_found)
575 | Some (s', subst, menv, ug, eq_found) ->
576 Some (C.Lambda (nn, s', (S.lift 1 t)),
577 subst, menv, ug, eq_found)
582 if Utils.debug_res then ignore(check_res res "demod_aux output");
587 let build_newtarget_time = ref 0.;;
590 let demod_counter = ref 1;;
594 let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"
596 (** demodulation, when target is an equality *)
597 let rec demodulation_equality ?from newmeta env table sign target =
598 let module C = Cic in
599 let module S = CicSubstitution in
600 let module M = CicMetaSubst in
601 let module HL = HelmLibraryObjects in
602 let module U = Utils in
603 let metasenv, context, ugraph = env in
604 let w, proof, (eq_ty, left, right, order), metas, id =
605 Equality.open_equality target
607 (* first, we simplify *)
608 (* let right = U.guarded_simpl context right in *)
609 (* let left = U.guarded_simpl context left in *)
610 (* let order = !Utils.compare_terms left right in *)
611 (* let stat = (eq_ty, left, right, order) in *)
612 (* let w = Utils.compute_equality_weight stat in*)
613 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
614 if Utils.debug_metas then
615 ignore(check_target context target "demod equalities input");
616 let metasenv' = (* metasenv @ *) metas in
617 let maxmeta = ref newmeta in
619 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
620 let time1 = Unix.gettimeofday () in
622 if Utils.debug_metas then
624 ignore(check_for_duplicates menv "input1");
625 ignore(check_disjoint_invariant subst menv "input2");
626 let substs = Subst.ppsubst subst in
627 ignore(check_target context (snd eq_found) ("input3" ^ substs))
629 let pos, equality = eq_found in
631 (ty, what, other, _), menv',id') = Equality.open_equality equality in
633 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
634 with CicUtil.Meta_not_found _ -> ty
636 let what, other = if pos = Utils.Left then what, other else other, what in
637 let newterm, newproof =
639 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
640 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
641 let name = C.Name "x" in
644 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
645 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
646 S.lift 1 eq_ty; l; r]
648 if sign = Utils.Positive then
649 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
650 (Cic.Lambda (name, ty, bo'))))))
655 prerr_endline "***************************************negative";
659 CicMkImplicit.identity_relocation_list_for_metavariable context in
660 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
661 (* print_newline (); *)
662 C.Meta (!maxmeta, irl)
667 if pos = Utils.Left then [ty; what; other]
668 else [ty; other; what]
670 Equality.ProofSymBlock (termlist, proof'_old)
672 let proof'_new' = assert false (* not implemented *) in
674 if pos = Utils.Left then what, other else other, what
678 (0, (proof'_new',proof'_old'),
679 (ty, other, what, Utils.Incomparable),menv')
684 (subst, eq_URI, (name, ty), bo',
685 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
687 assert false, (* not implemented *)
688 (match snd proof with
689 | Equality.BasicProof _ ->
690 (* print_endline "replacing a BasicProof"; *)
692 | Equality.ProofGoalBlock (_, parent_proof) ->
693 (* print_endline "replacing another ProofGoalBlock"; *)
694 Equality.ProofGoalBlock (pb, parent_proof)
698 C.Appl [C.MutConstruct (* reflexivity *)
699 (LibraryObjects.eq_URI (), 0, 1, []);
700 eq_ty; if is_left then right else left]
703 (assert false, (* not implemented *)
704 Equality.ProofGoalBlock
705 (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
709 let newmenv = (* Inference.filter subst *) menv in
711 if Utils.debug_metas then
712 try ignore(CicTypeChecker.type_of_aux'
714 (Equality.build_proof_term newproof) ugraph);
717 prerr_endline "sempre lui";
718 prerr_endline (Subst.ppsubst subst);
719 prerr_endline (CicPp.ppterm
720 (Equality.build_proof_term newproof));
721 prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
722 prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
723 prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
724 prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
725 prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
730 let left, right = if is_left then newterm, right else left, newterm in
731 let ordering = !Utils.compare_terms left right in
732 let stat = (eq_ty, left, right, ordering) in
733 let time2 = Unix.gettimeofday () in
734 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
736 let w = Utils.compute_equality_weight stat in
737 Equality.mk_equality (w, newproof, stat,newmenv)
739 if Utils.debug_metas then
740 ignore(check_target context res "buildnew_target output");
743 let build_newtarget is_left x =
744 profiler.HExtlib.profile (build_newtarget is_left) x
747 let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
748 if Utils.debug_res then check_res res "demod result";
749 let newmeta, newtarget =
752 let newmeta, newtarget = build_newtarget true t in
753 assert (not (Equality.meta_convertibility_eq target newtarget));
754 if (Equality.is_weak_identity newtarget) ||
755 (Equality.meta_convertibility_eq target newtarget) then
758 demodulation_equality ?from newmeta env table sign newtarget
760 let res = demodulation_aux metasenv' context ugraph table 0 right in
761 if Utils.debug_res then check_res res "demod result 1";
764 let newmeta, newtarget = build_newtarget false t in
765 if (Equality.is_weak_identity newtarget) ||
766 (Equality.meta_convertibility_eq target newtarget) then
769 demodulation_equality ?from newmeta env table sign newtarget
773 (* newmeta, newtarget *)
778 Performs the beta expansion of the term "term" w.r.t. "table",
779 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
782 let rec betaexpand_term metasenv context ugraph table lift_amount term =
783 let module C = Cic in
784 let module S = CicSubstitution in
785 let module M = CicMetaSubst in
786 let module HL = HelmLibraryObjects in
787 let candidates = get_candidates Unification table term in
789 let res, lifted_term =
794 (fun arg (res, lifted_tl) ->
797 let arg_res, lifted_arg =
798 betaexpand_term metasenv context ugraph table
802 (fun (t, s, m, ug, eq_found) ->
803 (Some t)::lifted_tl, s, m, ug, eq_found)
808 (fun (l, s, m, ug, eq_found) ->
809 (Some lifted_arg)::l, s, m, ug, eq_found)
811 (Some lifted_arg)::lifted_tl)
814 (fun (r, s, m, ug, eq_found) ->
815 None::r, s, m, ug, eq_found) res,
821 (fun (l, s, m, ug, eq_found) ->
822 (C.Meta (i, l), s, m, ug, eq_found)) l'
824 e, C.Meta (i, lifted_l)
827 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
829 | C.Prod (nn, s, t) ->
831 betaexpand_term metasenv context ugraph table lift_amount s in
833 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
834 table (lift_amount+1) t in
837 (fun (t, s, m, ug, eq_found) ->
838 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
841 (fun (t, s, m, ug, eq_found) ->
842 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
843 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
845 | C.Lambda (nn, s, t) ->
847 betaexpand_term metasenv context ugraph table lift_amount s in
849 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
850 table (lift_amount+1) t in
853 (fun (t, s, m, ug, eq_found) ->
854 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
857 (fun (t, s, m, ug, eq_found) ->
858 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
859 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
864 (fun arg (res, lifted_tl) ->
865 let arg_res, lifted_arg =
866 betaexpand_term metasenv context ugraph table lift_amount arg
870 (fun (a, s, m, ug, eq_found) ->
871 a::lifted_tl, s, m, ug, eq_found)
876 (fun (r, s, m, ug, eq_found) ->
877 lifted_arg::r, s, m, ug, eq_found)
879 lifted_arg::lifted_tl)
883 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
886 | t -> [], (S.lift lift_amount t)
889 | C.Meta (i, l) -> res, lifted_term
892 C.Implicit None, ugraph
893 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
897 metasenv context ugraph lift_amount term termty candidates
902 let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
904 let betaexpand_term metasenv context ugraph table lift_amount term =
905 profiler.HExtlib.profile
906 (betaexpand_term metasenv context ugraph table lift_amount) term
909 let sup_l_counter = ref 1;;
913 returns a list of new clauses inferred with a left superposition step
914 the negative equation "target" and one of the positive equations in "table"
917 let build_newgoal context goalproof (t, subst, menv, ug, (eq_found, eq_URI)) =
918 let pos, equality = eq_found in
919 let (_, proof', (ty, what, other, _), menv',id) =
920 Equality.open_equality equality in
921 let what, other = if pos = Utils.Left then what, other else other, what in
922 let newterm, newgoalproof =
924 Utils.guarded_simpl context
925 (apply_subst subst (CicSubstitution.subst other t))
927 let bo' = (*apply_subst subst*) t in
928 let name = Cic.Name "x" in
929 let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
930 bo, (newgoalproofstep::goalproof)
932 let newmetasenv = (* Inference.filter subst *) menv in
933 (newgoalproof, newmetasenv, newterm)
936 let superposition_left
937 (metasenv, context, ugraph) table (proof,menv,ty)
939 let module C = Cic in
940 let module S = CicSubstitution in
941 let module M = CicMetaSubst in
942 let module HL = HelmLibraryObjects in
943 let module CR = CicReduction in
944 let module U = Utils in
945 let big,small,pos,eq,ty =
947 | Cic.Appl [eq;ty;l;r] ->
949 Utils.compare_weights ~normalize:true
950 (Utils.weight_of_term l) (Utils.weight_of_term r)
953 | Utils.Gt -> l,r,Utils.Right,eq,ty
954 | _ -> r,l,Utils.Left,eq,ty)
957 let small = CicSubstitution.lift 1 small in
958 let ty = CicSubstitution.lift 1 ty in
959 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
960 let fix_preds (t, subst, menv, ug, (eq_found, eq_URI)) =
964 Cic.Appl [eq;ty;small;t]
966 Cic.Appl [eq;ty;t;small]
968 (pred, subst, menv, ug, (eq_found, eq_URI))
970 List.map (build_newgoal context proof)
971 (List.map fix_preds expansions)
974 let sup_r_counter = ref 1;;
978 returns a list of new clauses inferred with a right superposition step
979 between the positive equation "target" and one in the "table" "newmeta" is
980 the first free meta index, i.e. the first number above the highest meta
981 index: its updated value is also returned
983 let superposition_right newmeta (metasenv, context, ugraph) table target =
984 let module C = Cic in
985 let module S = CicSubstitution in
986 let module M = CicMetaSubst in
987 let module HL = HelmLibraryObjects in
988 let module CR = CicReduction in
989 let module U = Utils in
990 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
991 Equality.open_equality target
993 if Utils.debug_metas then
994 ignore (check_target context target "superpositionright");
995 let metasenv' = newmetas in
996 let maxmeta = ref newmeta in
998 let betaexpand_term metasenv context ugraph table d term =
999 let t1 = Unix.gettimeofday () in
1000 let res = betaexpand_term metasenv context ugraph table d term in
1001 let t2 = Unix.gettimeofday () in
1002 beta_expand_time := !beta_expand_time +. (t2 -. t1);
1006 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
1007 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
1011 (fun (_, subst, _, _, _) ->
1012 let subst = apply_subst subst in
1013 let o = !Utils.compare_terms (subst l) (subst r) in
1014 o <> U.Lt && o <> U.Le)
1015 (fst (betaexpand_term metasenv' context ugraph table 0 l))
1017 (res left right), (res right left)
1019 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
1020 if Utils.debug_metas then
1021 ignore (check_target context (snd eq_found) "buildnew1" );
1022 let time1 = Unix.gettimeofday () in
1024 let pos, equality = eq_found in
1025 let (_, proof', (ty, what, other, _), menv',id') =
1026 Equality.open_equality equality in
1027 let what, other = if pos = Utils.Left then what, other else other, what in
1028 let newgoal, newproof =
1031 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
1033 let name = C.Name "x" in
1037 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1038 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1039 S.lift 1 eq_ty; l; r]
1043 (s,(Equality.SuperpositionRight,
1044 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
1046 let newmeta, newequality =
1048 if ordering = U.Gt then newgoal, apply_subst s right
1049 else apply_subst s left, newgoal in
1050 let neworder = !Utils.compare_terms left right in
1051 let newmenv = (* Inference.filter s *) m in
1052 let stat = (eq_ty, left, right, neworder) in
1054 let w = Utils.compute_equality_weight stat in
1055 Equality.mk_equality (w, newproof, stat, newmenv) in
1056 if Utils.debug_metas then
1057 ignore (check_target context eq' "buildnew3");
1058 let newm, eq' = Equality.fix_metas !maxmeta eq' in
1059 if Utils.debug_metas then
1060 ignore (check_target context eq' "buildnew4");
1064 let time2 = Unix.gettimeofday () in
1065 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1066 if Utils.debug_metas then
1067 ignore(check_target context newequality "buildnew2");
1070 let new1 = List.map (build_new U.Gt) res1
1071 and new2 = List.map (build_new U.Lt) res2 in
1072 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1074 (List.filter ok (new1 @ new2)))
1078 (** demodulation, when the target is a goal *)
1079 let rec demodulation_goal newmeta env table goal =
1080 let module C = Cic in
1081 let module S = CicSubstitution in
1082 let module M = CicMetaSubst in
1083 let module HL = HelmLibraryObjects in
1084 let metasenv, context, ugraph = env in
1085 let maxmeta = ref newmeta in
1086 let goalproof, metas, term = goal in
1087 let term = Utils.guarded_simpl (~debug:true) context term in
1088 let goal = goalproof, metas, term in
1089 let metasenv' = metas in
1091 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1092 let pos, equality = eq_found in
1093 let (_, proof', (ty, what, other, _), menv',id) =
1094 Equality.open_equality equality in
1095 let what, other = if pos = Utils.Left then what, other else other, what in
1097 try fst (CicTypeChecker.type_of_aux' menv' context what ugraph)
1099 | CicUtil.Meta_not_found _
1100 | Invalid_argument("List.fold_left2") -> ty
1102 let newterm, newgoalproof =
1104 Utils.guarded_simpl context (apply_subst subst(S.subst other t))
1106 let bo' = (*apply_subst subst*) t in
1107 let name = C.Name "x" in
1109 let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
1110 bo, (newgoalproofstep::goalproof)
1112 let newmetasenv = (* Inference.filter subst *) menv in
1113 !maxmeta, (newgoalproof, newmetasenv, newterm)
1116 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
1120 let newmeta, newgoal = build_newgoal t in
1121 let _, _, newg = newgoal in
1122 if Equality.meta_convertibility term newg then
1123 false, newmeta, newgoal
1125 let changed, newmeta, newgoal =
1126 demodulation_goal newmeta env table newgoal
1128 true, newmeta, newgoal
1130 false, newmeta, goal
1133 (** demodulation, when the target is a theorem *)
1134 let rec demodulation_theorem newmeta env table theorem =
1135 let module C = Cic in
1136 let module S = CicSubstitution in
1137 let module M = CicMetaSubst in
1138 let module HL = HelmLibraryObjects in
1139 let metasenv, context, ugraph = env in
1140 let maxmeta = ref newmeta in
1141 let term, termty, metas = theorem in
1142 let metasenv' = metas in
1144 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1145 let pos, equality = eq_found in
1146 let (_, proof', (ty, what, other, _), menv',id) =
1147 Equality.open_equality equality in
1148 let what, other = if pos = Utils.Left then what, other else other, what in
1149 let newterm, newty =
1150 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1151 (* let bo' = apply_subst subst t in *)
1152 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
1156 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1157 Equality.BasicProof (Equality.empty_subst,term))
1159 (Equality.build_proof_term_old newproofold, bo)
1161 (* TODO, not ported to the new proofs *)
1162 if true then assert false; term, bo
1164 !maxmeta, (newterm, newty, menv)
1167 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1171 let newmeta, newthm = build_newtheorem t in
1172 let newt, newty, _ = newthm in
1173 if Equality.meta_convertibility termty newty then
1176 demodulation_theorem newmeta env table newthm