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 prerr_endline (". " ^ Equality.string_of_equality equality);
246 let (_, proof, (ty, left, right, o), metas,_) =
247 Equality.open_equality equality
249 if Utils.debug_metas then
250 ignore(check_target context (snd candidate) "find_matches");
251 if Utils.debug_res then
253 let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
254 let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
255 let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
257 (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
259 check_for_duplicates metas "gia nella metas";
260 check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
262 if check && not (fst (CicReduction.are_convertible
263 ~metasenv context termty ty ugraph)) then (
264 find_matches metasenv context ugraph lift_amount term termty tl
266 let do_match c eq_URI =
267 let subst', metasenv', ugraph' =
268 let t1 = Unix.gettimeofday () in
271 ( Inference.matching metasenv metas context
272 term (S.lift lift_amount c)) ugraph
274 let t2 = Unix.gettimeofday () in
275 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
278 | Inference.MatchingFailure as e ->
279 let t2 = Unix.gettimeofday () in
280 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
282 | CicUtil.Meta_not_found _ as exn -> raise exn
284 Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph',
287 let c, other, eq_URI =
288 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
289 else right, left, Utils.eq_ind_r_URI ()
291 if o <> U.Incomparable then
295 with Inference.MatchingFailure ->
296 find_matches metasenv context ugraph lift_amount term termty tl
298 if Utils.debug_res then ignore (check_res res "find1");
302 try do_match c eq_URI
303 with Inference.MatchingFailure -> None
305 if Utils.debug_res then ignore (check_res res "find2");
307 | Some (_, s, _, _, _) ->
308 let c' = apply_subst s c in
310 let other' = U.guarded_simpl context (apply_subst s other) in *)
311 let other' = apply_subst s other in
312 let order = cmp c' other' in
317 metasenv context ugraph lift_amount term termty tl
319 find_matches metasenv context ugraph lift_amount term termty tl
323 as above, but finds all the matching equalities, and the matching condition
324 can be either Inference.matching or Inference.unification
326 let rec find_all_matches ?(unif_fun=Inference.unification)
327 metasenv context ugraph lift_amount term termty =
328 let module C = Cic in
329 let module U = Utils in
330 let module S = CicSubstitution in
331 let module M = CicMetaSubst in
332 let module HL = HelmLibraryObjects in
333 let cmp = !Utils.compare_terms in
337 let pos, equality = candidate in
338 let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
339 let do_match c eq_URI =
340 let subst', metasenv', ugraph' =
341 let t1 = Unix.gettimeofday () in
345 | Cic.Meta _, Cic.Appl[Cic.MutInd(u,0,_);_;l;r]
346 when LibraryObjects.is_eq_URI u -> l
348 if Utils.compare_weights (Utils.weight_of_term l)
349 (Utils.weight_of_term r) = Utils.Gt
356 unif_fun metasenv metas context
357 term (S.lift lift_amount c) ugraph in
358 let t2 = Unix.gettimeofday () in
359 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
362 | Inference.MatchingFailure
363 | CicUnification.UnificationFailure _
364 | CicUnification.Uncertain _ as e ->
365 let t2 = Unix.gettimeofday () in
366 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
369 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
372 let c, other, eq_URI =
373 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
374 else right, left, Utils.eq_ind_r_URI ()
376 if o <> U.Incomparable then
378 let res = do_match c eq_URI in
379 res::(find_all_matches ~unif_fun metasenv context ugraph
380 lift_amount term termty tl)
382 | Inference.MatchingFailure
383 | CicUnification.UnificationFailure _
384 | CicUnification.Uncertain _ ->
385 find_all_matches ~unif_fun metasenv context ugraph
386 lift_amount term termty tl
389 let res = do_match c eq_URI in
392 let c' = apply_subst s c
393 and other' = apply_subst s other in
394 let order = cmp c' other' in
395 if order <> U.Lt && order <> U.Le then
396 res::(find_all_matches ~unif_fun metasenv context ugraph
397 lift_amount term termty tl)
399 find_all_matches ~unif_fun metasenv context ugraph
400 lift_amount term termty tl
402 | Inference.MatchingFailure
403 | CicUnification.UnificationFailure _
404 | CicUnification.Uncertain _ ->
405 find_all_matches ~unif_fun metasenv context ugraph
406 lift_amount term termty tl
410 ?unif_fun metasenv context ugraph lift_amount term termty l
414 ?unif_fun metasenv context ugraph lift_amount term termty l
416 (*prerr_endline "CANDIDATES:";
417 List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
418 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
423 returns true if target is subsumed by some equality in table
425 let subsumption_aux use_unification env table target =
426 (* let print_res l =*)
427 (* prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,*)
428 (* ((pos,equation),_)) -> Equality.string_of_equality equation)l))*)
430 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
431 let metasenv, context, ugraph = env in
432 let metasenv = tmetas in
433 let predicate, unif_fun =
434 if use_unification then
435 Unification, Inference.unification
437 Matching, Inference.matching
441 | Cic.Meta _ when not use_unification -> []
443 let leftc = get_candidates predicate table left in
444 find_all_matches ~unif_fun
445 metasenv context ugraph 0 left ty leftc
447 (* print_res leftr;*)
448 let rec ok what = function
450 | (_, subst, menv, ug, ((pos,equation),_))::tl ->
451 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
453 let other = if pos = Utils.Left then r else l in
454 let what' = Subst.apply_subst subst what in
455 let subst', menv', ug' =
456 unif_fun metasenv m context what' other ugraph
458 (match Subst.merge_subst_if_possible subst subst' with
460 | Some s -> Some (s, equation))
462 | Inference.MatchingFailure
463 | CicUnification.UnificationFailure _ -> ok what tl
465 match ok right leftr with
466 | Some _ as res -> res
470 | Cic.Meta _ when not use_unification -> []
472 let rightc = get_candidates predicate table right in
473 find_all_matches ~unif_fun
474 metasenv context ugraph 0 right ty rightc
476 (* print_res rightr;*)
481 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
482 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
485 let subsumption = subsumption_aux false;;
486 let unification = subsumption_aux true;;
488 let rec demodulation_aux ?from ?(typecheck=false)
489 metasenv context ugraph table lift_amount term =
490 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
491 let module C = Cic in
492 let module S = CicSubstitution in
493 let module M = CicMetaSubst in
494 let module HL = HelmLibraryObjects in
497 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
505 CicTypeChecker.type_of_aux' metasenv context term ugraph
507 C.Implicit None, ugraph
510 find_matches metasenv context ugraph lift_amount term termty candidates
512 if Utils.debug_res then ignore(check_res res "demod1");
522 (res, tl @ [S.lift 1 t])
525 demodulation_aux ~from:"1" metasenv context ugraph table
529 | None -> (None, tl @ [S.lift 1 t])
530 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
535 | Some (_, subst, menv, ug, eq_found) ->
536 Some (C.Appl ll, subst, menv, ug, eq_found)
538 | C.Prod (nn, s, t) ->
540 demodulation_aux ~from:"2"
541 metasenv context ugraph table lift_amount s in (
545 demodulation_aux metasenv
546 ((Some (nn, C.Decl s))::context) ugraph
547 table (lift_amount+1) t
551 | Some (t', subst, menv, ug, eq_found) ->
552 Some (C.Prod (nn, (S.lift 1 s), t'),
553 subst, menv, ug, eq_found)
555 | Some (s', subst, menv, ug, eq_found) ->
556 Some (C.Prod (nn, s', (S.lift 1 t)),
557 subst, menv, ug, eq_found)
559 | C.Lambda (nn, s, t) ->
562 metasenv context ugraph table lift_amount s in (
566 demodulation_aux metasenv
567 ((Some (nn, C.Decl s))::context) ugraph
568 table (lift_amount+1) t
572 | Some (t', subst, menv, ug, eq_found) ->
573 Some (C.Lambda (nn, (S.lift 1 s), t'),
574 subst, menv, ug, eq_found)
576 | Some (s', subst, menv, ug, eq_found) ->
577 Some (C.Lambda (nn, s', (S.lift 1 t)),
578 subst, menv, ug, eq_found)
583 if Utils.debug_res then ignore(check_res res "demod_aux output");
588 let build_newtarget_time = ref 0.;;
591 let demod_counter = ref 1;;
595 let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"
597 (** demodulation, when target is an equality *)
598 let rec demodulation_equality ?from newmeta env table sign target =
599 let module C = Cic in
600 let module S = CicSubstitution in
601 let module M = CicMetaSubst in
602 let module HL = HelmLibraryObjects in
603 let module U = Utils in
604 let metasenv, context, ugraph = env in
605 let w, proof, (eq_ty, left, right, order), metas, id =
606 Equality.open_equality target
608 (* first, we simplify *)
609 (* let right = U.guarded_simpl context right in *)
610 (* let left = U.guarded_simpl context left in *)
611 (* let order = !Utils.compare_terms left right in *)
612 (* let stat = (eq_ty, left, right, order) in *)
613 (* let w = Utils.compute_equality_weight stat in*)
614 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
615 if Utils.debug_metas then
616 ignore(check_target context target "demod equalities input");
617 let metasenv' = (* metasenv @ *) metas in
618 let maxmeta = ref newmeta in
620 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
621 let time1 = Unix.gettimeofday () in
623 if Utils.debug_metas then
625 ignore(check_for_duplicates menv "input1");
626 ignore(check_disjoint_invariant subst menv "input2");
627 let substs = Subst.ppsubst subst in
628 ignore(check_target context (snd eq_found) ("input3" ^ substs))
630 let pos, equality = eq_found in
632 (ty, what, other, _), menv',id') = Equality.open_equality equality in
634 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
635 with CicUtil.Meta_not_found _ -> ty
637 let what, other = if pos = Utils.Left then what, other else other, what in
638 let newterm, newproof =
640 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
641 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
642 let name = C.Name "x" in
645 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
646 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
647 S.lift 1 eq_ty; l; r]
649 if sign = Utils.Positive then
650 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
651 (Cic.Lambda (name, ty, bo'))))))
656 prerr_endline "***************************************negative";
660 CicMkImplicit.identity_relocation_list_for_metavariable context in
661 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
662 (* print_newline (); *)
663 C.Meta (!maxmeta, irl)
668 if pos = Utils.Left then [ty; what; other]
669 else [ty; other; what]
671 Equality.ProofSymBlock (termlist, proof'_old)
673 let proof'_new' = assert false (* not implemented *) in
675 if pos = Utils.Left then what, other else other, what
679 (0, (proof'_new',proof'_old'),
680 (ty, other, what, Utils.Incomparable),menv')
685 (subst, eq_URI, (name, ty), bo',
686 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
688 assert false, (* not implemented *)
689 (match snd proof with
690 | Equality.BasicProof _ ->
691 (* print_endline "replacing a BasicProof"; *)
693 | Equality.ProofGoalBlock (_, parent_proof) ->
694 (* print_endline "replacing another ProofGoalBlock"; *)
695 Equality.ProofGoalBlock (pb, parent_proof)
699 C.Appl [C.MutConstruct (* reflexivity *)
700 (LibraryObjects.eq_URI (), 0, 1, []);
701 eq_ty; if is_left then right else left]
704 (assert false, (* not implemented *)
705 Equality.ProofGoalBlock
706 (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
710 let newmenv = (* Inference.filter subst *) menv in
712 if Utils.debug_metas then
713 try ignore(CicTypeChecker.type_of_aux'
715 (Equality.build_proof_term newproof) ugraph);
718 prerr_endline "sempre lui";
719 prerr_endline (Subst.ppsubst subst);
720 prerr_endline (CicPp.ppterm
721 (Equality.build_proof_term newproof));
722 prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
723 prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
724 prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
725 prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
726 prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
731 let left, right = if is_left then newterm, right else left, newterm in
732 let ordering = !Utils.compare_terms left right in
733 let stat = (eq_ty, left, right, ordering) in
734 let time2 = Unix.gettimeofday () in
735 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
737 let w = Utils.compute_equality_weight stat in
738 Equality.mk_equality (w, newproof, stat,newmenv)
740 if Utils.debug_metas then
741 ignore(check_target context res "buildnew_target output");
744 let build_newtarget is_left x =
745 profiler.HExtlib.profile (build_newtarget is_left) x
748 let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
749 if Utils.debug_res then check_res res "demod result";
750 let newmeta, newtarget =
753 let newmeta, newtarget = build_newtarget true t in
754 assert (not (Equality.meta_convertibility_eq target newtarget));
755 if (Equality.is_weak_identity newtarget) ||
756 (Equality.meta_convertibility_eq target newtarget) then
759 demodulation_equality ?from newmeta env table sign newtarget
761 let res = demodulation_aux metasenv' context ugraph table 0 right in
762 if Utils.debug_res then check_res res "demod result 1";
765 let newmeta, newtarget = build_newtarget false t in
766 if (Equality.is_weak_identity newtarget) ||
767 (Equality.meta_convertibility_eq target newtarget) then
770 demodulation_equality ?from newmeta env table sign newtarget
774 (* newmeta, newtarget *)
779 Performs the beta expansion of the term "term" w.r.t. "table",
780 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
783 let rec betaexpand_term metasenv context ugraph table lift_amount term =
784 let module C = Cic in
785 let module S = CicSubstitution in
786 let module M = CicMetaSubst in
787 let module HL = HelmLibraryObjects in
788 let candidates = get_candidates Unification table term in
790 let res, lifted_term =
795 (fun arg (res, lifted_tl) ->
798 let arg_res, lifted_arg =
799 betaexpand_term metasenv context ugraph table
803 (fun (t, s, m, ug, eq_found) ->
804 (Some t)::lifted_tl, s, m, ug, eq_found)
809 (fun (l, s, m, ug, eq_found) ->
810 (Some lifted_arg)::l, s, m, ug, eq_found)
812 (Some lifted_arg)::lifted_tl)
815 (fun (r, s, m, ug, eq_found) ->
816 None::r, s, m, ug, eq_found) res,
822 (fun (l, s, m, ug, eq_found) ->
823 (C.Meta (i, l), s, m, ug, eq_found)) l'
825 e, C.Meta (i, lifted_l)
828 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
830 | C.Prod (nn, s, t) ->
832 betaexpand_term metasenv context ugraph table lift_amount s in
834 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
835 table (lift_amount+1) t in
838 (fun (t, s, m, ug, eq_found) ->
839 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
842 (fun (t, s, m, ug, eq_found) ->
843 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
844 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
846 | C.Lambda (nn, s, t) ->
848 betaexpand_term metasenv context ugraph table lift_amount s in
850 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
851 table (lift_amount+1) t in
854 (fun (t, s, m, ug, eq_found) ->
855 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
858 (fun (t, s, m, ug, eq_found) ->
859 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
860 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
865 (fun arg (res, lifted_tl) ->
866 let arg_res, lifted_arg =
867 betaexpand_term metasenv context ugraph table lift_amount arg
871 (fun (a, s, m, ug, eq_found) ->
872 a::lifted_tl, s, m, ug, eq_found)
877 (fun (r, s, m, ug, eq_found) ->
878 lifted_arg::r, s, m, ug, eq_found)
880 lifted_arg::lifted_tl)
884 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
887 | t -> [], (S.lift lift_amount t)
890 | C.Meta (i, l) -> res, lifted_term
893 C.Implicit None, ugraph
894 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
898 metasenv context ugraph lift_amount term termty candidates
903 let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
905 let betaexpand_term metasenv context ugraph table lift_amount term =
906 profiler.HExtlib.profile
907 (betaexpand_term metasenv context ugraph table lift_amount) term
910 let sup_l_counter = ref 1;;
914 returns a list of new clauses inferred with a left superposition step
915 the negative equation "target" and one of the positive equations in "table"
917 let fix_expansion (eq,ty,unchanged,posu) (t, subst, menv, ug, eq_f) =
918 let unchanged = CicSubstitution.lift 1 unchanged in
919 let ty = CicSubstitution.lift 1 ty in
922 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
923 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
925 (pred, subst, menv, ug, eq_f)
928 let build_newgoal context goalproof goal_info expansion =
929 let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal_info expansion in
930 let pos, equality = eq_found in
931 let (_, proof', (ty, what, other, _), menv',id) =
932 Equality.open_equality equality in
933 let what, other = if pos = Utils.Left then what, other else other, what in
934 let newterm, newgoalproof =
936 Utils.guarded_simpl context
937 (apply_subst subst (CicSubstitution.subst other t))
939 let bo' = (*apply_subst subst*) t in
940 let name = Cic.Name "x" in
941 let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
942 bo, (newgoalproofstep::goalproof)
944 let newmetasenv = (* Inference.filter subst *) menv in
945 (newgoalproof, newmetasenv, newterm)
948 let superposition_left
949 (metasenv, context, ugraph) table (proof,menv,ty)
951 let module C = Cic in
952 let module S = CicSubstitution in
953 let module M = CicMetaSubst in
954 let module HL = HelmLibraryObjects in
955 let module CR = CicReduction in
956 let module U = Utils in
957 let big,small,pos,eq,ty =
959 | Cic.Appl [eq;ty;l;r] ->
961 Utils.compare_weights ~normalize:true
962 (Utils.weight_of_term l) (Utils.weight_of_term r)
965 | Utils.Gt -> l,r,Utils.Right,eq,ty
966 | _ -> r,l,Utils.Left,eq,ty)
968 let names = Utils.names_of_context context in
969 prerr_endline ("NON TROVO UN EQ: " ^ CicPp.pp ty names);
972 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
973 List.map (build_newgoal context proof (eq,ty,small,pos)) expansions
976 let sup_r_counter = ref 1;;
980 returns a list of new clauses inferred with a right superposition step
981 between the positive equation "target" and one in the "table" "newmeta" is
982 the first free meta index, i.e. the first number above the highest meta
983 index: its updated value is also returned
985 let superposition_right newmeta (metasenv, context, ugraph) table target =
986 let module C = Cic in
987 let module S = CicSubstitution in
988 let module M = CicMetaSubst in
989 let module HL = HelmLibraryObjects in
990 let module CR = CicReduction in
991 let module U = Utils in
992 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
993 Equality.open_equality target
995 if Utils.debug_metas then
996 ignore (check_target context target "superpositionright");
997 let metasenv' = newmetas in
998 let maxmeta = ref newmeta in
1000 let betaexpand_term metasenv context ugraph table d term =
1001 let t1 = Unix.gettimeofday () in
1002 let res = betaexpand_term metasenv context ugraph table d term in
1003 let t2 = Unix.gettimeofday () in
1004 beta_expand_time := !beta_expand_time +. (t2 -. t1);
1009 fst (betaexpand_term metasenv' context ugraph table 0 left), []
1011 [], fst (betaexpand_term metasenv' context ugraph table 0 right)
1015 (fun (_, subst, _, _, _) ->
1016 let subst = apply_subst subst in
1017 let o = !Utils.compare_terms (subst l) (subst r) in
1018 o <> U.Lt && o <> U.Le)
1019 (fst (betaexpand_term metasenv' context ugraph table 0 l))
1021 (res left right), (res right left)
1023 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
1024 if Utils.debug_metas then
1025 ignore (check_target context (snd eq_found) "buildnew1" );
1026 let time1 = Unix.gettimeofday () in
1028 let pos, equality = eq_found in
1029 let (_, proof', (ty, what, other, _), menv',id') =
1030 Equality.open_equality equality in
1031 let what, other = if pos = Utils.Left then what, other else other, what in
1033 let newgoal, newproof =
1036 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
1038 let name = C.Name "x" in
1042 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1043 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1044 S.lift 1 eq_ty; l; r]
1048 (s,(Equality.SuperpositionRight,
1049 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
1051 let newmeta, newequality =
1053 if ordering = U.Gt then newgoal, apply_subst s right
1054 else apply_subst s left, newgoal in
1055 let neworder = !Utils.compare_terms left right in
1056 let newmenv = (* Inference.filter s *) m in
1057 let stat = (eq_ty, left, right, neworder) in
1059 let w = Utils.compute_equality_weight stat in
1060 Equality.mk_equality (w, newproof, stat, newmenv) in
1061 if Utils.debug_metas then
1062 ignore (check_target context eq' "buildnew3");
1063 let newm, eq' = Equality.fix_metas !maxmeta eq' in
1064 if Utils.debug_metas then
1065 ignore (check_target context eq' "buildnew4");
1069 let time2 = Unix.gettimeofday () in
1070 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1071 if Utils.debug_metas then
1072 ignore(check_target context newequality "buildnew2");
1075 let new1 = List.map (build_new U.Gt) res1
1076 and new2 = List.map (build_new U.Lt) res2 in
1077 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1079 (List.filter ok (new1 @ new2)))
1082 (** demodulation, when the target is a goal *)
1083 let goal_metaconvertibility_eq (_,_,g1) (_,_,g2) =
1084 Equality.meta_convertibility g1 g2
1087 let rec demodulation_goal env table goal =
1088 let metasenv, context, ugraph = env in
1089 let goalproof, metas, term = goal in
1090 let term = Utils.guarded_simpl (~debug:true) context term in
1091 let goal = goalproof, metas, term in
1092 let metasenv' = metas in
1094 let left,right,eq,ty =
1096 | Cic.Appl [eq;ty;l;r] -> l,r,eq,ty
1100 let resright = demodulation_aux metasenv' context ugraph table 0 right in
1103 let newg=build_newgoal context goalproof (eq,ty,left,Utils.Left) t in
1104 if goal_metaconvertibility_eq goal newg then
1107 true, snd (demodulation_goal env table newg)
1108 | None -> false, goal
1111 demodulation_aux (*~typecheck:true*) metasenv' context ugraph table 0 left
1115 let newg = build_newgoal context goalproof (eq,ty,right,Utils.Right) t in
1116 if goal_metaconvertibility_eq goal newg then
1119 true, snd (demodulation_goal env table newg)
1120 | None -> do_right ()
1123 (** demodulation, when the target is a theorem *)
1124 let rec demodulation_theorem newmeta env table theorem =
1125 let module C = Cic in
1126 let module S = CicSubstitution in
1127 let module M = CicMetaSubst in
1128 let module HL = HelmLibraryObjects in
1129 let metasenv, context, ugraph = env in
1130 let maxmeta = ref newmeta in
1131 let term, termty, metas = theorem in
1132 let metasenv' = metas in
1134 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1135 let pos, equality = eq_found in
1136 let (_, proof', (ty, what, other, _), menv',id) =
1137 Equality.open_equality equality in
1138 let what, other = if pos = Utils.Left then what, other else other, what in
1139 let newterm, newty =
1140 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1141 (* let bo' = apply_subst subst t in *)
1142 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
1146 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1147 Equality.BasicProof (Equality.empty_subst,term))
1149 (Equality.build_proof_term_old newproofold, bo)
1151 (* TODO, not ported to the new proofs *)
1152 if true then assert false; term, bo
1154 !maxmeta, (newterm, newty, menv)
1157 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1161 let newmeta, newthm = build_newtheorem t in
1162 let newt, newty, _ = newthm in
1163 if Equality.meta_convertibility termty newty then
1166 demodulation_theorem newmeta env table newthm