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 =
412 (* let print_res l =*)
413 (* prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,*)
414 (* ((pos,equation),_)) -> Equality.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
419 let predicate, unif_fun =
420 if use_unification then
421 Unification, Inference.unification
423 Matching, Inference.matching
427 | Cic.Meta _ when not use_unification -> []
429 let leftc = get_candidates predicate table left in
430 find_all_matches ~unif_fun
431 metasenv context ugraph 0 left ty leftc
433 (* print_res leftr;*)
434 let rec ok what = function
436 | (_, subst, menv, ug, ((pos,equation),_))::tl ->
437 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
439 let other = if pos = Utils.Left then r else l in
440 let what' = Subst.apply_subst subst what in
441 let subst', menv', ug' =
442 unif_fun metasenv m context what' other ugraph
444 (match Subst.merge_subst_if_possible subst subst' with
446 | Some s -> Some (s, equation))
448 | Inference.MatchingFailure
449 | CicUnification.UnificationFailure _ -> ok what tl
451 match ok right leftr with
452 | Some _ as res -> res
456 | Cic.Meta _ when not use_unification -> []
458 let rightc = get_candidates predicate table right in
459 find_all_matches ~unif_fun
460 metasenv context ugraph 0 right ty rightc
462 (* print_res rightr;*)
467 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
468 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
471 let subsumption = subsumption_aux false;;
472 let unification = subsumption_aux true;;
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"
909 let build_newgoal context goalproof (t, subst, menv, ug, (eq_found, eq_URI)) =
910 let pos, equality = eq_found in
911 let (_, proof', (ty, what, other, _), menv',id) =
912 Equality.open_equality equality in
913 let what, other = if pos = Utils.Left then what, other else other, what in
914 let newterm, newgoalproof =
916 Utils.guarded_simpl context
917 (apply_subst subst (CicSubstitution.subst other t))
919 let bo' = (*apply_subst subst*) t in
920 let name = Cic.Name "x" in
921 let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
922 bo, (newgoalproofstep::goalproof)
924 let newmetasenv = (* Inference.filter subst *) menv in
925 (newgoalproof, newmetasenv, newterm)
928 let superposition_left
929 (metasenv, context, ugraph) table (proof,menv,ty)
931 let module C = Cic in
932 let module S = CicSubstitution in
933 let module M = CicMetaSubst in
934 let module HL = HelmLibraryObjects in
935 let module CR = CicReduction in
936 let module U = Utils in
937 let big,small,pos,eq,ty =
939 | Cic.Appl [eq;ty;l;r] ->
941 Utils.compare_weights ~normalize:true
942 (Utils.weight_of_term l) (Utils.weight_of_term r)
945 | Utils.Gt -> l,r,Utils.Right,eq,ty
946 | _ -> r,l,Utils.Left,eq,ty)
949 let small = CicSubstitution.lift 1 small in
950 let ty = CicSubstitution.lift 1 ty in
951 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
952 let fix_preds (t, subst, menv, ug, (eq_found, eq_URI)) =
956 Cic.Appl [eq;ty;small;t]
958 Cic.Appl [eq;ty;t;small]
960 (pred, subst, menv, ug, (eq_found, eq_URI))
962 List.map (build_newgoal context proof)
963 (List.map fix_preds expansions)
966 let sup_r_counter = ref 1;;
970 returns a list of new clauses inferred with a right superposition step
971 between the positive equation "target" and one in the "table" "newmeta" is
972 the first free meta index, i.e. the first number above the highest meta
973 index: its updated value is also returned
975 let superposition_right newmeta (metasenv, context, ugraph) table target =
976 let module C = Cic in
977 let module S = CicSubstitution in
978 let module M = CicMetaSubst in
979 let module HL = HelmLibraryObjects in
980 let module CR = CicReduction in
981 let module U = Utils in
982 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
983 Equality.open_equality target
985 if Utils.debug_metas then
986 ignore (check_target context target "superpositionright");
987 let metasenv' = newmetas in
988 let maxmeta = ref newmeta in
990 let betaexpand_term metasenv context ugraph table d term =
991 let t1 = Unix.gettimeofday () in
992 let res = betaexpand_term metasenv context ugraph table d term in
993 let t2 = Unix.gettimeofday () in
994 beta_expand_time := !beta_expand_time +. (t2 -. t1);
998 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
999 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
1003 (fun (_, subst, _, _, _) ->
1004 let subst = apply_subst subst in
1005 let o = !Utils.compare_terms (subst l) (subst r) in
1006 o <> U.Lt && o <> U.Le)
1007 (fst (betaexpand_term metasenv' context ugraph table 0 l))
1009 (res left right), (res right left)
1011 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
1012 if Utils.debug_metas then
1013 ignore (check_target context (snd eq_found) "buildnew1" );
1014 let time1 = Unix.gettimeofday () in
1016 let pos, equality = eq_found in
1017 let (_, proof', (ty, what, other, _), menv',id') =
1018 Equality.open_equality equality in
1019 let what, other = if pos = Utils.Left then what, other else other, what in
1020 let newgoal, newproof =
1023 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
1025 let name = C.Name "x" in
1029 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1030 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1031 S.lift 1 eq_ty; l; r]
1035 (s,(Equality.SuperpositionRight,
1036 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
1038 let newmeta, newequality =
1040 if ordering = U.Gt then newgoal, apply_subst s right
1041 else apply_subst s left, newgoal in
1042 let neworder = !Utils.compare_terms left right in
1043 let newmenv = (* Inference.filter s *) m in
1044 let stat = (eq_ty, left, right, neworder) in
1046 let w = Utils.compute_equality_weight stat in
1047 Equality.mk_equality (w, newproof, stat, newmenv) in
1048 if Utils.debug_metas then
1049 ignore (check_target context eq' "buildnew3");
1050 let newm, eq' = Equality.fix_metas !maxmeta eq' in
1051 if Utils.debug_metas then
1052 ignore (check_target context eq' "buildnew4");
1056 let time2 = Unix.gettimeofday () in
1057 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1058 if Utils.debug_metas then
1059 ignore(check_target context newequality "buildnew2");
1062 let new1 = List.map (build_new U.Gt) res1
1063 and new2 = List.map (build_new U.Lt) res2 in
1064 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1066 (List.filter ok (new1 @ new2)))
1070 (** demodulation, when the target is a goal *)
1071 let rec demodulation_goal newmeta env table goal =
1072 let module C = Cic in
1073 let module S = CicSubstitution in
1074 let module M = CicMetaSubst in
1075 let module HL = HelmLibraryObjects in
1076 let metasenv, context, ugraph = env in
1077 let maxmeta = ref newmeta in
1078 let goalproof, metas, term = goal in
1079 let term = Utils.guarded_simpl (~debug:true) context term in
1080 let goal = goalproof, metas, term in
1081 let metasenv' = metas in
1083 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1084 let pos, equality = eq_found in
1085 let (_, proof', (ty, what, other, _), menv',id) =
1086 Equality.open_equality equality in
1087 let what, other = if pos = Utils.Left then what, other else other, what in
1089 try fst (CicTypeChecker.type_of_aux' menv' context what ugraph)
1091 | CicUtil.Meta_not_found _
1092 | Invalid_argument("List.fold_left2") -> ty
1094 let newterm, newgoalproof =
1096 Utils.guarded_simpl context (apply_subst subst(S.subst other t))
1098 let bo' = (*apply_subst subst*) t in
1099 let name = C.Name "x" in
1101 let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
1102 bo, (newgoalproofstep::goalproof)
1104 let newmetasenv = (* Inference.filter subst *) menv in
1105 !maxmeta, (newgoalproof, newmetasenv, newterm)
1108 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
1112 let newmeta, newgoal = build_newgoal t in
1113 let _, _, newg = newgoal in
1114 if Equality.meta_convertibility term newg then
1115 false, newmeta, newgoal
1117 let changed, newmeta, newgoal =
1118 demodulation_goal newmeta env table newgoal
1120 true, newmeta, newgoal
1122 false, newmeta, goal
1125 (** demodulation, when the target is a theorem *)
1126 let rec demodulation_theorem newmeta env table theorem =
1127 let module C = Cic in
1128 let module S = CicSubstitution in
1129 let module M = CicMetaSubst in
1130 let module HL = HelmLibraryObjects in
1131 let metasenv, context, ugraph = env in
1132 let maxmeta = ref newmeta in
1133 let term, termty, metas = theorem in
1134 let metasenv' = metas in
1136 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1137 let pos, equality = eq_found in
1138 let (_, proof', (ty, what, other, _), menv',id) =
1139 Equality.open_equality equality in
1140 let what, other = if pos = Utils.Left then what, other else other, what in
1141 let newterm, newty =
1142 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1143 (* let bo' = apply_subst subst t in *)
1144 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
1148 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1149 Equality.BasicProof (Equality.empty_subst,term))
1151 (Equality.build_proof_term_old newproofold, bo)
1153 (* TODO, not ported to the new proofs *)
1154 if true then assert false; term, bo
1156 !maxmeta, (newterm, newty, menv)
1159 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1163 let newmeta, newthm = build_newtheorem t in
1164 let newt, newty, _ = newthm in
1165 if Equality.meta_convertibility termty newty then
1168 demodulation_theorem newmeta env table newthm