1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
30 module Index = Equality_indexing.DT (* path tree based indexing *)
33 let beta_expand_time = ref 0.;;
35 let debug_print = Utils.debug_print;;
39 let check_equation env equation msg =
40 let w, proof, (eq_ty, left, right, order), metas, args = equation in
41 let metasenv, context, ugraph = env
42 let metasenv' = metasenv @ metas in
44 CicTypeChecker.type_of_aux' metasenv' context left ugraph;
45 CicTypeChecker.type_of_aux' metasenv' context right ugraph;
48 CicUtil.Meta_not_found _ as exn ->
51 prerr_endline (CicPp.ppterm left);
52 prerr_endline (CicPp.ppterm right);
57 type retrieval_mode = Matching | Unification;;
59 let string_of_res ?env =
62 | Some (t, s, m, u, ((p,e), eq_URI)) ->
63 Printf.sprintf "Some: (%s, %s, %s)"
64 (Utils.string_of_pos p)
65 (Equality.string_of_equality ?env e)
69 let print_res ?env res =
72 (List.map (string_of_res ?env) res))
75 let print_candidates ?env mode term res =
79 prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
81 prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
87 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
88 (Equality.string_of_equality ?env e))
93 let indexing_retrieval_time = ref 0.;;
96 let apply_subst = Equality.apply_subst
98 let index = Index.index
99 let remove_index = Index.remove_index
100 let in_index = Index.in_index
101 let empty = Index.empty
102 let init_index = Index.init_index
104 let check_disjoint_invariant subst metasenv msg =
106 (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv)
109 prerr_endline ("not disjoint: " ^ msg);
114 let check_for_duplicates metas msg =
115 if List.length metas <>
116 List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
118 prerr_endline ("DUPLICATI " ^ msg);
119 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
124 let check_res res msg =
126 Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
127 let eqs = Equality.string_of_equality (snd eq_found) in
128 check_disjoint_invariant subst menv msg;
129 check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
133 let check_target context target msg =
134 let w, proof, (eq_ty, left, right, order), metas,_ =
135 Equality.open_equality target in
136 (* check that metas does not contains duplicates *)
137 let eqs = Equality.string_of_equality target in
138 let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
139 let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
140 @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof) in
141 let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
142 let _ = if menv <> metas then
144 prerr_endline ("extra metas " ^ msg);
145 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
146 prerr_endline "**********************";
147 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
148 prerr_endline ("left: " ^ (CicPp.ppterm left));
149 prerr_endline ("right: " ^ (CicPp.ppterm right));
150 prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
156 ignore(CicTypeChecker.type_of_aux'
157 metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
160 prerr_endline (Inference.string_of_proof proof);
161 prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
162 prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
163 prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
168 (* returns a list of all the equalities in the tree that are in relation
169 "mode" with the given term, where mode can be either Matching or
172 Format of the return value: list of tuples in the form:
173 (position - Left or Right - of the term that matched the given one in this
177 Note that if equality is "left = right", if the ordering is left > right,
178 the position will always be Left, and if the ordering is left < right,
179 position will be Right.
182 let get_candidates ?env mode tree term =
183 let t1 = Unix.gettimeofday () in
187 | Matching -> Index.retrieve_generalizations tree term
188 | Unification -> Index.retrieve_unifiables tree term
190 Index.PosEqSet.elements s
192 (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
193 (* print_newline (); *)
194 let t2 = Unix.gettimeofday () in
195 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
196 (* make fresh instances *)
200 let profiler = HExtlib.profile "P/Indexing.get_candidates"
202 let get_candidates ?env mode tree term =
203 profiler.HExtlib.profile (get_candidates ?env mode tree) term
205 let match_unif_time_ok = ref 0.;;
206 let match_unif_time_no = ref 0.;;
210 finds the first equality in the index that matches "term", of type "termty"
211 termty can be Implicit if it is not needed. The result (one of the sides of
212 the equality, actually) should be not greater (wrt the term ordering) than
215 Format of the return value:
217 (term to substitute, [Cic.Rel 1 properly lifted - see the various
218 build_newtarget functions inside the various
219 demodulation_* functions]
220 substitution used for the matching,
222 ugraph, [substitution, metasenv and ugraph have the same meaning as those
223 returned by CicUnification.fo_unif]
224 (equality where the matching term was found, [i.e. the equality to use as
226 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
227 the equality: this is used to build the proof term, again see one of
228 the build_newtarget functions]
231 let rec find_matches metasenv context ugraph lift_amount term termty =
232 let module C = Cic in
233 let module U = Utils in
234 let module S = CicSubstitution in
235 let module M = CicMetaSubst in
236 let module HL = HelmLibraryObjects in
237 let cmp = !Utils.compare_terms in
238 let check = match termty with C.Implicit None -> false | _ -> true in
242 let pos, equality = candidate in
243 let (_, proof, (ty, left, right, o), metas,_) =
244 Equality.open_equality equality in
245 if Utils.debug_metas then
246 ignore(check_target context (snd candidate) "find_matches");
247 if Utils.debug_res then
249 let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
250 let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
251 let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
253 (CicPp.ppterm(Equality.build_proof_term_old (snd proof)))^"\n"
255 check_for_duplicates metas "gia nella metas";
256 check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
258 if check && not (fst (CicReduction.are_convertible
259 ~metasenv context termty ty ugraph)) then (
260 find_matches metasenv context ugraph lift_amount term termty tl
262 let do_match c eq_URI =
263 let subst', metasenv', ugraph' =
264 let t1 = Unix.gettimeofday () in
267 ( Inference.matching metasenv metas context
268 term (S.lift lift_amount c)) ugraph
270 let t2 = Unix.gettimeofday () in
271 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
274 | Inference.MatchingFailure as e ->
275 let t2 = Unix.gettimeofday () in
276 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
278 | CicUtil.Meta_not_found _ as exn -> raise exn
280 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
283 let c, other, eq_URI =
284 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
285 else right, left, Utils.eq_ind_r_URI ()
287 if o <> U.Incomparable then
291 with Inference.MatchingFailure ->
292 find_matches metasenv context ugraph lift_amount term termty tl
294 if Utils.debug_res then ignore (check_res res "find1");
298 try do_match c eq_URI
299 with Inference.MatchingFailure -> None
301 if Utils.debug_res then ignore (check_res res "find2");
303 | Some (_, s, _, _, _) ->
304 let c' = apply_subst s c in
306 let other' = U.guarded_simpl context (apply_subst s other) in *)
307 let other' = apply_subst s other in
308 let order = cmp c' other' in
313 metasenv context ugraph lift_amount term termty tl
315 find_matches metasenv context ugraph lift_amount term termty tl
319 as above, but finds all the matching equalities, and the matching condition
320 can be either Inference.matching or Inference.unification
322 let rec find_all_matches ?(unif_fun=Inference.unification)
323 metasenv context ugraph lift_amount term termty =
324 let module C = Cic in
325 let module U = Utils in
326 let module S = CicSubstitution in
327 let module M = CicMetaSubst in
328 let module HL = HelmLibraryObjects in
329 let cmp = !Utils.compare_terms in
333 let pos, equality = candidate in
334 let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
335 let do_match c eq_URI =
336 let subst', metasenv', ugraph' =
337 let t1 = Unix.gettimeofday () in
340 unif_fun metasenv metas context
341 term (S.lift lift_amount c) ugraph in
342 let t2 = Unix.gettimeofday () in
343 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
346 | Inference.MatchingFailure
347 | CicUnification.UnificationFailure _
348 | CicUnification.Uncertain _ as e ->
349 let t2 = Unix.gettimeofday () in
350 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
353 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
356 let c, other, eq_URI =
357 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
358 else right, left, Utils.eq_ind_r_URI ()
360 if o <> U.Incomparable then
362 let res = do_match c eq_URI in
363 res::(find_all_matches ~unif_fun metasenv context ugraph
364 lift_amount term termty tl)
366 | Inference.MatchingFailure
367 | CicUnification.UnificationFailure _
368 | CicUnification.Uncertain _ ->
369 find_all_matches ~unif_fun metasenv context ugraph
370 lift_amount term termty tl
373 let res = do_match c eq_URI in
376 let c' = apply_subst s c
377 and other' = apply_subst s other in
378 let order = cmp c' other' in
379 if order <> U.Lt && order <> U.Le then
380 res::(find_all_matches ~unif_fun metasenv context ugraph
381 lift_amount term termty tl)
383 find_all_matches ~unif_fun metasenv context ugraph
384 lift_amount term termty tl
386 | Inference.MatchingFailure
387 | CicUnification.UnificationFailure _
388 | CicUnification.Uncertain _ ->
389 find_all_matches ~unif_fun metasenv context ugraph
390 lift_amount term termty tl
394 ?unif_fun metasenv context ugraph lift_amount term termty l
398 ?unif_fun metasenv context ugraph lift_amount term termty l
400 (*prerr_endline "CANDIDATES:";
401 List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
402 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
407 returns true if target is subsumed by some equality in table
409 let subsumption env table target =
412 prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
413 ((pos,equation),_)) -> Inference.string_of_equality equation)l))
416 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
417 let metasenv, context, ugraph = env in
418 let metasenv = tmetas in
423 let leftc = get_candidates Matching table left in
424 find_all_matches ~unif_fun:Inference.matching
425 metasenv context ugraph 0 left ty leftc
427 (* print_res leftr;*)
428 let rec ok what = function
430 | (_, subst, menv, ug, ((pos,equation),_))::tl ->
431 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
433 let other = if pos = Utils.Left then r else l in
434 let subst', menv', ug' =
435 let t1 = Unix.gettimeofday () in
438 Inference.matching metasenv m context what other ugraph
440 let t2 = Unix.gettimeofday () in
441 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
443 with Inference.MatchingFailure as e ->
444 let t2 = Unix.gettimeofday () in
445 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
448 (match Equality.merge_subst_if_possible subst subst' with
450 | Some s -> Some (s, equation))
451 with Inference.MatchingFailure ->
454 match ok right leftr with
455 | Some _ as res -> res
461 let rightc = get_candidates Matching table right in
462 find_all_matches ~unif_fun:Inference.matching
463 metasenv context ugraph 0 right ty rightc
465 (* print_res rightr;*)
470 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
471 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
474 let rec demodulation_aux ?from ?(typecheck=false)
475 metasenv context ugraph table lift_amount term =
476 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
477 let module C = Cic in
478 let module S = CicSubstitution in
479 let module M = CicMetaSubst in
480 let module HL = HelmLibraryObjects in
482 get_candidates ~env:(metasenv,context,ugraph) (* Unification *) Matching table term in
483 if List.exists (fun (i,_,_) -> i = 2840) metasenv
485 (prerr_endline ("term: " ^(CicPp.ppterm term));
486 List.iter (fun (_,x) -> prerr_endline (Equality.string_of_equality x))
488 prerr_endline ("-------");
489 prerr_endline ("+++++++"));
496 CicTypeChecker.type_of_aux' metasenv context term ugraph
498 C.Implicit None, ugraph
501 find_matches metasenv context ugraph lift_amount term termty candidates
503 if Utils.debug_res then ignore(check_res res "demod1");
513 (res, tl @ [S.lift 1 t])
516 demodulation_aux ~from:"1" metasenv context ugraph table
520 | None -> (None, tl @ [S.lift 1 t])
521 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
526 | Some (_, subst, menv, ug, eq_found) ->
527 Some (C.Appl ll, subst, menv, ug, eq_found)
529 | C.Prod (nn, s, t) ->
531 demodulation_aux ~from:"2"
532 metasenv context ugraph table lift_amount s in (
536 demodulation_aux metasenv
537 ((Some (nn, C.Decl s))::context) ugraph
538 table (lift_amount+1) t
542 | Some (t', subst, menv, ug, eq_found) ->
543 Some (C.Prod (nn, (S.lift 1 s), t'),
544 subst, menv, ug, eq_found)
546 | Some (s', subst, menv, ug, eq_found) ->
547 Some (C.Prod (nn, s', (S.lift 1 t)),
548 subst, menv, ug, eq_found)
550 | C.Lambda (nn, s, t) ->
553 metasenv context ugraph table lift_amount s in (
557 demodulation_aux metasenv
558 ((Some (nn, C.Decl s))::context) ugraph
559 table (lift_amount+1) t
563 | Some (t', subst, menv, ug, eq_found) ->
564 Some (C.Lambda (nn, (S.lift 1 s), t'),
565 subst, menv, ug, eq_found)
567 | Some (s', subst, menv, ug, eq_found) ->
568 Some (C.Lambda (nn, s', (S.lift 1 t)),
569 subst, menv, ug, eq_found)
574 if Utils.debug_res then ignore(check_res res "demod_aux output");
579 let build_newtarget_time = ref 0.;;
582 let demod_counter = ref 1;;
586 let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"
588 (** demodulation, when target is an equality *)
589 let rec demodulation_equality ?from newmeta env table sign target =
590 let module C = Cic in
591 let module S = CicSubstitution in
592 let module M = CicMetaSubst in
593 let module HL = HelmLibraryObjects in
594 let module U = Utils in
595 let metasenv, context, ugraph = env in
596 let w, ((proof_new, proof_old) (*as proof*)),
597 (eq_ty, left, right, order), metas, id =
598 Equality.open_equality target in
599 (* first, we simplify *)
600 (* let right = U.guarded_simpl context right in *)
601 (* let left = U.guarded_simpl context left in *)
602 (* let order = !Utils.compare_terms left right in *)
603 (* let stat = (eq_ty, left, right, order) in *)
604 (* let w = Utils.compute_equality_weight stat in*)
605 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
606 if Utils.debug_metas then
607 ignore(check_target context target "demod equalities input");
608 let metasenv' = (* metasenv @ *) metas in
609 let maxmeta = ref newmeta in
611 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
612 let time1 = Unix.gettimeofday () in
614 if Utils.debug_metas then
616 ignore(check_for_duplicates menv "input1");
617 ignore(check_disjoint_invariant subst menv "input2");
618 let substs = Equality.ppsubst subst in
619 ignore(check_target context (snd eq_found) ("input3" ^ substs))
621 let pos, equality = eq_found in
622 let (_, (proof'_new,proof'_old),
623 (ty, what, other, _), menv',id') = Equality.open_equality equality in
625 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
626 with CicUtil.Meta_not_found _ -> ty
628 let what, other = if pos = Utils.Left then what, other else other, what in
629 let newterm, newproof =
631 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
632 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
633 let name = C.Name "x" in
636 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
637 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
638 S.lift 1 eq_ty; l; r]
640 if sign = Utils.Positive then
642 (Equality.Step (subst,(Equality.Demodulation,
644 (*apply_subst subst*) (Cic.Lambda (name, ty, bo')))),
645 Equality.ProofBlock (
646 subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof_old)))
651 prerr_endline "***************************************negative";
655 CicMkImplicit.identity_relocation_list_for_metavariable context in
656 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
657 (* print_newline (); *)
658 C.Meta (!maxmeta, irl)
663 if pos = Utils.Left then [ty; what; other]
664 else [ty; other; what]
666 Equality.ProofSymBlock (termlist, proof'_old)
668 let proof'_new' = assert false (* not implemented *) in
670 if pos = Utils.Left then what, other else other, what
674 (0, (proof'_new',proof'_old'),
675 (ty, other, what, Utils.Incomparable),menv')
680 (subst, eq_URI, (name, ty), bo',
681 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
683 assert false, (* not implemented *)
684 (match snd proof with
685 | Equality.BasicProof _ ->
686 (* print_endline "replacing a BasicProof"; *)
688 | Equality.ProofGoalBlock (_, parent_proof) ->
689 (* print_endline "replacing another ProofGoalBlock"; *)
690 Equality.ProofGoalBlock (pb, parent_proof)
694 C.Appl [C.MutConstruct (* reflexivity *)
695 (LibraryObjects.eq_URI (), 0, 1, []);
696 eq_ty; if is_left then right else left]
699 (assert false, (* not implemented *)
700 Equality.ProofGoalBlock
701 (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
705 let newmenv = (* Inference.filter subst *) menv in
707 if Utils.debug_metas then
708 try ignore(CicTypeChecker.type_of_aux'
710 (Equality.build_proof_term_old (snd newproof)) ugraph);
713 prerr_endline "sempre lui";
714 prerr_endline (Equality.ppsubst subst);
715 prerr_endline (CicPp.ppterm
716 (Equality.build_proof_term_old (snd newproof)));
717 prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
718 prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
719 prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
720 prerr_endline ("+++++++++++++subst: " ^ (Equality.ppsubst subst));
721 prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
726 let left, right = if is_left then newterm, right else left, newterm in
727 let ordering = !Utils.compare_terms left right in
728 let stat = (eq_ty, left, right, ordering) in
729 let time2 = Unix.gettimeofday () in
730 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
732 let w = Utils.compute_equality_weight stat in
733 Equality.mk_equality (w, newproof, stat,newmenv)
735 if Utils.debug_metas then
736 ignore(check_target context res "buildnew_target output");
739 let build_newtarget is_left x =
740 profiler.HExtlib.profile (build_newtarget is_left) x
743 let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
744 if Utils.debug_res then check_res res "demod result";
745 let newmeta, newtarget =
748 let newmeta, newtarget = build_newtarget true t in
749 assert (not (Equality.meta_convertibility_eq target newtarget));
750 if (Equality.is_weak_identity newtarget) ||
751 (Equality.meta_convertibility_eq target newtarget) then
754 demodulation_equality ?from newmeta env table sign newtarget
756 let res = demodulation_aux metasenv' context ugraph table 0 right in
757 if Utils.debug_res then check_res res "demod result 1";
760 let newmeta, newtarget = build_newtarget false t in
761 if (Equality.is_weak_identity newtarget) ||
762 (Equality.meta_convertibility_eq target newtarget) then
765 demodulation_equality ?from newmeta env table sign newtarget
769 (* newmeta, newtarget *)
774 Performs the beta expansion of the term "term" w.r.t. "table",
775 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
778 let rec betaexpand_term metasenv context ugraph table lift_amount term =
779 let module C = Cic in
780 let module S = CicSubstitution in
781 let module M = CicMetaSubst in
782 let module HL = HelmLibraryObjects in
783 let candidates = get_candidates Unification table term in
785 let res, lifted_term =
790 (fun arg (res, lifted_tl) ->
793 let arg_res, lifted_arg =
794 betaexpand_term metasenv context ugraph table
798 (fun (t, s, m, ug, eq_found) ->
799 (Some t)::lifted_tl, s, m, ug, eq_found)
804 (fun (l, s, m, ug, eq_found) ->
805 (Some lifted_arg)::l, s, m, ug, eq_found)
807 (Some lifted_arg)::lifted_tl)
810 (fun (r, s, m, ug, eq_found) ->
811 None::r, s, m, ug, eq_found) res,
817 (fun (l, s, m, ug, eq_found) ->
818 (C.Meta (i, l), s, m, ug, eq_found)) l'
820 e, C.Meta (i, lifted_l)
823 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
825 | C.Prod (nn, s, t) ->
827 betaexpand_term metasenv context ugraph table lift_amount s in
829 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
830 table (lift_amount+1) t in
833 (fun (t, s, m, ug, eq_found) ->
834 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
837 (fun (t, s, m, ug, eq_found) ->
838 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
839 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
841 | C.Lambda (nn, s, t) ->
843 betaexpand_term metasenv context ugraph table lift_amount s in
845 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
846 table (lift_amount+1) t in
849 (fun (t, s, m, ug, eq_found) ->
850 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
853 (fun (t, s, m, ug, eq_found) ->
854 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
855 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
860 (fun arg (res, lifted_tl) ->
861 let arg_res, lifted_arg =
862 betaexpand_term metasenv context ugraph table lift_amount arg
866 (fun (a, s, m, ug, eq_found) ->
867 a::lifted_tl, s, m, ug, eq_found)
872 (fun (r, s, m, ug, eq_found) ->
873 lifted_arg::r, s, m, ug, eq_found)
875 lifted_arg::lifted_tl)
879 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
882 | t -> [], (S.lift lift_amount t)
885 | C.Meta (i, l) -> res, lifted_term
888 C.Implicit None, ugraph
889 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
893 metasenv context ugraph lift_amount term termty candidates
898 let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
900 let betaexpand_term metasenv context ugraph table lift_amount term =
901 profiler.HExtlib.profile
902 (betaexpand_term metasenv context ugraph table lift_amount) term
905 let sup_l_counter = ref 1;;
909 returns a list of new clauses inferred with a left superposition step
910 the negative equation "target" and one of the positive equations in "table"
912 let superposition_left newmeta (metasenv, context, ugraph) table target =
915 let superposition_left newmeta (metasenv, context, ugraph) table target =
916 let module C = Cic in
917 let module S = CicSubstitution in
918 let module M = CicMetaSubst in
919 let module HL = HelmLibraryObjects in
920 let module CR = CicReduction in
921 let module U = Utils in
922 let weight, proof, (eq_ty, left, right, ordering), menv, id =
923 Equality.open_equality target
925 if Utils.debug_metas then
926 ignore(check_target context target "superpositionleft");
928 let term = if ordering = U.Gt then left else right in
929 betaexpand_term metasenv context ugraph table 0 term
931 let maxmeta = ref newmeta in
932 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
933 (* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
934 let time1 = Unix.gettimeofday () in
936 let pos, equality = eq_found in
937 let _,proof',(ty,what,other,_),menv',id'=Equality.open_equality equality in
938 let proof'_new, proof'_old = proof' in
939 let what, other = if pos = Utils.Left then what, other else other, what in
940 let newgoal, newproof =
941 let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
942 let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
946 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
947 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
948 S.lift 1 eq_ty; l; r]
953 CicMkImplicit.identity_relocation_list_for_metavariable context in
954 C.Meta (!maxmeta, irl)
959 if pos = Utils.Left then [ty; what; other]
960 else [ty; other; what]
962 proof'_new, (* MAH????? *)
963 Equality.ProofSymBlock (termlist, proof'_old)
966 if pos = Utils.Left then what, other else other, what
970 (0, proof', (ty, other, what, Utils.Incomparable), menv')
972 let target_proof = assert false (*
975 (s, eq_URI, (name, ty), bo'', eq_found,
976 Equality.BasicProof (Equality.empty_subst,metaproof))
979 | Equality.BasicProof _ ->
980 (* debug_print (lazy "replacing a BasicProof"); *)
982 | Equality.ProofGoalBlock (_, parent_proof) ->
983 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
984 Equality.ProofGoalBlock (pb, parent_proof)
985 | _ -> assert false*)
988 C.Appl [C.MutConstruct (* reflexivity *)
989 (LibraryObjects.eq_URI (), 0, 1, []);
990 eq_ty; if ordering = U.Gt then right else left]
993 (Equality.Step (Equality.SuperpositionLeft,id,(pos,id'),
994 assert false), (* il predicato della beta expand non viene tenuto? *)
995 Equality.ProofGoalBlock
996 (Equality.BasicProof (Equality.empty_subst,refl), target_proof)))
999 if ordering = U.Gt then newgoal, right else left, newgoal in
1000 let neworder = !Utils.compare_terms left right in
1001 let stat = (eq_ty, left, right, neworder) in
1002 let newmenv = (* Inference.filter s *) menv in
1003 let time2 = Unix.gettimeofday () in
1004 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1006 let w = Utils.compute_equality_weight stat in
1007 Equality.mk_equality (w, newproof, stat, newmenv)
1010 !maxmeta, List.map build_new expansions
1014 let sup_r_counter = ref 1;;
1018 returns a list of new clauses inferred with a right superposition step
1019 between the positive equation "target" and one in the "table" "newmeta" is
1020 the first free meta index, i.e. the first number above the highest meta
1021 index: its updated value is also returned
1023 let superposition_right newmeta (metasenv, context, ugraph) table target =
1024 let module C = Cic in
1025 let module S = CicSubstitution in
1026 let module M = CicMetaSubst in
1027 let module HL = HelmLibraryObjects in
1028 let module CR = CicReduction in
1029 let module U = Utils in
1030 let w, (eqproof1,eqproof2), (eq_ty, left, right, ordering), newmetas,id =
1031 Equality.open_equality target
1033 if Utils.debug_metas then
1034 ignore (check_target context target "superpositionright");
1035 let metasenv' = newmetas in
1036 let maxmeta = ref newmeta in
1038 let betaexpand_term metasenv context ugraph table d term =
1039 let t1 = Unix.gettimeofday () in
1040 let res = betaexpand_term metasenv context ugraph table d term in
1041 let t2 = Unix.gettimeofday () in
1042 beta_expand_time := !beta_expand_time +. (t2 -. t1);
1046 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
1047 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
1051 (fun (_, subst, _, _, _) ->
1052 let subst = apply_subst subst in
1053 let o = !Utils.compare_terms (subst l) (subst r) in
1054 o <> U.Lt && o <> U.Le)
1055 (fst (betaexpand_term metasenv' context ugraph table 0 l))
1057 (res left right), (res right left)
1059 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
1060 if Utils.debug_metas then
1061 ignore (check_target context (snd eq_found) "buildnew1" );
1062 let time1 = Unix.gettimeofday () in
1064 let pos, equality = eq_found in
1065 let (_, proof', (ty, what, other, _), menv',id') =
1066 Equality.open_equality equality in
1067 let what, other = if pos = Utils.Left then what, other else other, what in
1068 let newgoal, newproof =
1071 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
1073 let name = C.Name "x" in
1077 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1078 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1079 S.lift 1 eq_ty; l; r]
1083 (s,(Equality.SuperpositionRight,
1084 id,(pos,id'),(Cic.Lambda(name,ty,bo'')))),
1085 Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2))
1088 let newmeta, newequality =
1090 if ordering = U.Gt then newgoal, apply_subst s right
1091 else apply_subst s left, newgoal in
1092 let neworder = !Utils.compare_terms left right in
1093 let newmenv = (* Inference.filter s *) m in
1094 let stat = (eq_ty, left, right, neworder) in
1096 let w = Utils.compute_equality_weight stat in
1097 Equality.mk_equality (w, newproof, stat, newmenv) in
1098 if Utils.debug_metas then
1099 ignore (check_target context eq' "buildnew3");
1100 let newm, eq' = Equality.fix_metas !maxmeta eq' in
1101 if Utils.debug_metas then
1102 ignore (check_target context eq' "buildnew4");
1106 let time2 = Unix.gettimeofday () in
1107 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1108 if Utils.debug_metas then
1109 ignore(check_target context newequality "buildnew2");
1112 let new1 = List.map (build_new U.Gt) res1
1113 and new2 = List.map (build_new U.Lt) res2 in
1114 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1116 (List.filter ok (new1 @ new2)))
1120 (** demodulation, when the target is a goal *)
1121 let rec demodulation_goal newmeta env table goal =
1122 let module C = Cic in
1123 let module S = CicSubstitution in
1124 let module M = CicMetaSubst in
1125 let module HL = HelmLibraryObjects in
1126 let metasenv, context, ugraph = env in
1127 let maxmeta = ref newmeta in
1128 let (cicproof,proof), metas, term = goal in
1129 let term = Utils.guarded_simpl (~debug:true) context term in
1130 let goal = (cicproof,proof), metas, term in
1131 let metasenv' = metas in
1133 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1134 let pos, equality = eq_found in
1135 let (_, (proofnew',proof'), (ty, what, other, _), menv',id) =
1136 Equality.open_equality equality in
1137 let what, other = if pos = Utils.Left then what, other else other, what in
1139 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
1140 with CicUtil.Meta_not_found _ -> ty
1142 let newterm, newproof, newcicproof =
1144 Utils.guarded_simpl context (apply_subst subst(S.subst other t))
1146 let bo' = apply_subst subst t in
1147 (* let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in*)
1148 let name = C.Name "x" in
1153 CicMkImplicit.identity_relocation_list_for_metavariable context *) in
1154 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
1155 C.Meta (!maxmeta, irl)
1158 let eq_found_proof =
1160 if pos = Utils.Left then [ty; what; other]
1161 else [ty; other; what]
1163 Equality.ProofSymBlock (termlist, proof')
1166 if pos = Utils.Left then what, other else other, what
1169 Equality.mk_equality
1170 (0,(proofnew',eq_found_proof), (ty, other, what, Utils.Incomparable), menv')
1175 (subst, eq_URI, (name, ty), bo',
1176 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
1178 let rec repl = function
1179 | Equality.NoProof ->
1180 (* debug_print (lazy "replacing a NoProof"); *)
1182 | Equality.BasicProof _ ->
1183 (* debug_print (lazy "replacing a BasicProof"); *)
1185 | Equality.ProofGoalBlock (_, parent_proof) ->
1186 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
1187 Equality.ProofGoalBlock (pb, parent_proof)
1188 | Equality.SubProof (term, meta_index, p) ->
1189 prerr_endline "subproof!";
1190 Equality.SubProof (term, meta_index, repl p)
1194 let newcicproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
1195 bo, Equality.ProofGoalBlock (Equality.NoProof, goal_proof),
1196 (newcicproofstep::cicproof)
1198 let newmetasenv = (* Inference.filter subst *) menv in
1199 !maxmeta, ((newcicproof,newproof), newmetasenv, newterm)
1202 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
1206 let newmeta, newgoal = build_newgoal t in
1207 let _, _, newg = newgoal in
1208 if Equality.meta_convertibility term newg then
1209 false, newmeta, newgoal
1211 let changed, newmeta, newgoal =
1212 demodulation_goal newmeta env table newgoal
1214 true, newmeta, newgoal
1216 false, newmeta, goal
1219 (** demodulation, when the target is a theorem *)
1220 let rec demodulation_theorem newmeta env table theorem =
1221 let module C = Cic in
1222 let module S = CicSubstitution in
1223 let module M = CicMetaSubst in
1224 let module HL = HelmLibraryObjects in
1225 let metasenv, context, ugraph = env in
1226 let maxmeta = ref newmeta in
1227 let term, termty, metas = theorem in
1228 let metasenv' = metas in
1230 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1231 let pos, equality = eq_found in
1232 let (_, proof', (ty, what, other, _), menv',id) =
1233 Equality.open_equality equality in
1234 let what, other = if pos = Utils.Left then what, other else other, what in
1235 let newterm, newty =
1236 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1237 let bo' = apply_subst subst t in
1238 let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1241 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1242 Equality.BasicProof (Equality.empty_subst,term))
1244 (Equality.build_proof_term_old newproofold, bo)
1246 !maxmeta, (newterm, newty, menv)
1249 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1253 let newmeta, newthm = build_newtheorem t in
1254 let newt, newty, _ = newthm in
1255 if Equality.meta_convertibility termty newty then
1258 demodulation_theorem newmeta env table newthm