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/.
26 let _profiler = <:profiler<_profiler>>;;
30 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
32 module Index = Equality_indexing.DT (* path tree based indexing *)
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)) ->
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 apply_subst = Subst.apply_subst
95 let index = Index.index
96 let remove_index = Index.remove_index
97 let in_index = Index.in_index
98 let empty = Index.empty
99 let init_index = Index.init_index
101 let check_disjoint_invariant subst metasenv msg =
103 (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
106 prerr_endline ("not disjoint: " ^ msg);
111 let check_for_duplicates metas msg =
112 if List.length metas <>
113 List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
115 prerr_endline ("DUPLICATI " ^ msg);
116 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
121 let check_res res msg =
123 Some (t, subst, menv, ug, eq_found) ->
124 let eqs = Equality.string_of_equality (snd eq_found) in
125 check_disjoint_invariant subst menv msg;
126 check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
130 let check_target context target msg =
131 let w, proof, (eq_ty, left, right, order), metas,_ =
132 Equality.open_equality target in
133 (* check that metas does not contains duplicates *)
134 let eqs = Equality.string_of_equality target in
135 let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
136 let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
137 @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof) in
138 let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
139 let _ = if menv <> metas then
141 prerr_endline ("extra metas " ^ msg);
142 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
143 prerr_endline "**********************";
144 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
145 prerr_endline ("left: " ^ (CicPp.ppterm left));
146 prerr_endline ("right: " ^ (CicPp.ppterm right));
147 prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
153 ignore(CicTypeChecker.type_of_aux'
154 metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
157 prerr_endline (Inference.string_of_proof proof);
158 prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
159 prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
160 prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
165 (* returns a list of all the equalities in the tree that are in relation
166 "mode" with the given term, where mode can be either Matching or
169 Format of the return value: list of tuples in the form:
170 (position - Left or Right - of the term that matched the given one in this
174 Note that if equality is "left = right", if the ordering is left > right,
175 the position will always be Left, and if the ordering is left < right,
176 position will be Right.
179 let get_candidates ?env mode tree term =
183 let _ = <:start<retrieve_generalizations>> in
184 <:stop<retrieve_generalizations
185 Index.retrieve_generalizations tree term
188 let _ = <:start<retrieve_unifiables>> in
189 <:stop<retrieve_unifiables
190 Index.retrieve_unifiables tree term
194 Index.PosEqSet.elements s
198 finds the first equality in the index that matches "term", of type "termty"
199 termty can be Implicit if it is not needed. The result (one of the sides of
200 the equality, actually) should be not greater (wrt the term ordering) than
203 Format of the return value:
205 (term to substitute, [Cic.Rel 1 properly lifted - see the various
206 build_newtarget functions inside the various
207 demodulation_* functions]
208 substitution used for the matching,
210 ugraph, [substitution, metasenv and ugraph have the same meaning as those
211 returned by CicUnification.fo_unif]
212 (equality where the matching term was found, [i.e. the equality to use as
214 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
215 the equality: this is used to build the proof term, again see one of
216 the build_newtarget functions]
219 let rec find_matches metasenv context ugraph lift_amount term termty =
220 let module C = Cic in
221 let module U = Utils in
222 let module S = CicSubstitution in
223 let module M = CicMetaSubst in
224 let module HL = HelmLibraryObjects in
225 let cmp = !Utils.compare_terms in
226 let check = match termty with C.Implicit None -> false | _ -> true in
230 let pos, equality = candidate in
231 let (_, proof, (ty, left, right, o), metas,_) =
232 Equality.open_equality equality
234 if Utils.debug_metas then
235 ignore(check_target context (snd candidate) "find_matches");
236 if Utils.debug_res then
238 let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
239 let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
240 let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
243 (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
246 check_for_duplicates metas "gia nella metas";
247 check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*))
249 if check && not (fst (CicReduction.are_convertible
250 ~metasenv context termty ty ugraph)) then (
251 find_matches metasenv context ugraph lift_amount term termty tl
254 let subst', metasenv', ugraph' =
256 metasenv metas context term (S.lift lift_amount c) ugraph
258 Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
261 if pos = Utils.Left then left, right
264 if o <> U.Incomparable then
268 with Inference.MatchingFailure ->
269 find_matches metasenv context ugraph lift_amount term termty tl
271 if Utils.debug_res then ignore (check_res res "find1");
276 with Inference.MatchingFailure -> None
278 if Utils.debug_res then ignore (check_res res "find2");
280 | Some (_, s, _, _, _) ->
281 let c' = apply_subst s c in
283 let other' = U.guarded_simpl context (apply_subst s other) in *)
284 let other' = apply_subst s other in
285 let order = cmp c' other' in
290 metasenv context ugraph lift_amount term termty tl
292 find_matches metasenv context ugraph lift_amount term termty tl
295 let find_matches metasenv context ugraph lift_amount term termty =
296 find_matches metasenv context ugraph lift_amount term termty
300 as above, but finds all the matching equalities, and the matching condition
301 can be either Inference.matching or Inference.unification
303 let rec find_all_matches ?(unif_fun=Inference.unification)
304 metasenv context ugraph lift_amount term termty =
305 let module C = Cic in
306 let module U = Utils in
307 let module S = CicSubstitution in
308 let module M = CicMetaSubst in
309 let module HL = HelmLibraryObjects in
310 let cmp = !Utils.compare_terms in
314 let pos, equality = candidate in
315 let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
317 let subst', metasenv', ugraph' =
318 unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
320 (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
323 if pos = Utils.Left then left, right
326 if o <> U.Incomparable then
328 let res = do_match c in
329 res::(find_all_matches ~unif_fun metasenv context ugraph
330 lift_amount term termty tl)
332 | Inference.MatchingFailure
333 | CicUnification.UnificationFailure _
334 | CicUnification.Uncertain _ ->
335 find_all_matches ~unif_fun metasenv context ugraph
336 lift_amount term termty tl
339 let res = do_match c in
342 let c' = apply_subst s c
343 and other' = apply_subst s other in
344 let order = cmp c' other' in
345 if order <> U.Lt && order <> U.Le then
346 res::(find_all_matches ~unif_fun metasenv context ugraph
347 lift_amount term termty tl)
349 find_all_matches ~unif_fun metasenv context ugraph
350 lift_amount term termty tl
352 | Inference.MatchingFailure
353 | CicUnification.UnificationFailure _
354 | CicUnification.Uncertain _ ->
355 find_all_matches ~unif_fun metasenv context ugraph
356 lift_amount term termty tl
360 ?unif_fun metasenv context ugraph lift_amount term termty l
363 ?unif_fun metasenv context ugraph lift_amount term termty l
364 (*prerr_endline "CANDIDATES:";
365 List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
366 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
370 returns true if target is subsumed by some equality in table
373 prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
374 ((pos,equation),_)) -> Equality.string_of_equality equation)l))
377 let subsumption_aux use_unification env table target =
378 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
379 let metasenv, context, ugraph = env in
380 let metasenv = tmetas in
381 let predicate, unif_fun =
382 if use_unification then
383 Unification, Inference.unification
385 Matching, Inference.matching
389 | Cic.Meta _ when not use_unification -> []
391 let leftc = get_candidates predicate table left in
392 find_all_matches ~unif_fun
393 metasenv context ugraph 0 left ty leftc
395 let rec ok what leftorright = function
397 | (_, subst, menv, ug, (pos,equation))::tl ->
398 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
400 let other = if pos = Utils.Left then r else l in
401 let what' = Subst.apply_subst subst what in
402 let other' = Subst.apply_subst subst other in
403 let subst', menv', ug' =
404 unif_fun metasenv m context what' other' ugraph
406 (match Subst.merge_subst_if_possible subst subst' with
407 | None -> ok what leftorright tl
408 | Some s -> Some (s, equation, leftorright <> pos ))
410 | Inference.MatchingFailure
411 | CicUnification.UnificationFailure _ -> ok what leftorright tl
413 match ok right Utils.Left leftr with
414 | Some _ as res -> res
418 | Cic.Meta _ when not use_unification -> []
420 let rightc = get_candidates predicate table right in
421 find_all_matches ~unif_fun
422 metasenv context ugraph 0 right ty rightc
424 ok left Utils.Right rightr
427 let subsumption x y z =
428 subsumption_aux false x y z
431 let unification x y z =
432 subsumption_aux true x y z
435 let rec demodulation_aux ?from ?(typecheck=false)
436 metasenv context ugraph table lift_amount term =
437 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
438 let module C = Cic in
439 let module S = CicSubstitution in
440 let module M = CicMetaSubst in
441 let module HL = HelmLibraryObjects in
444 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
452 CicTypeChecker.type_of_aux' metasenv context term ugraph
454 C.Implicit None, ugraph
457 find_matches metasenv context ugraph lift_amount term termty candidates
459 if Utils.debug_res then ignore(check_res res "demod1");
469 (res, tl @ [S.lift 1 t])
472 demodulation_aux ~from:"1" metasenv context ugraph table
476 | None -> (None, tl @ [S.lift 1 t])
477 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
482 | Some (_, subst, menv, ug, eq_found) ->
483 Some (C.Appl ll, subst, menv, ug, eq_found)
485 | C.Prod (nn, s, t) ->
487 demodulation_aux ~from:"2"
488 metasenv context ugraph table lift_amount s in (
492 demodulation_aux metasenv
493 ((Some (nn, C.Decl s))::context) ugraph
494 table (lift_amount+1) t
498 | Some (t', subst, menv, ug, eq_found) ->
499 Some (C.Prod (nn, (S.lift 1 s), t'),
500 subst, menv, ug, eq_found)
502 | Some (s', subst, menv, ug, eq_found) ->
503 Some (C.Prod (nn, s', (S.lift 1 t)),
504 subst, menv, ug, eq_found)
506 | C.Lambda (nn, s, t) ->
509 metasenv context ugraph table lift_amount s in (
513 demodulation_aux metasenv
514 ((Some (nn, C.Decl s))::context) ugraph
515 table (lift_amount+1) t
519 | Some (t', subst, menv, ug, eq_found) ->
520 Some (C.Lambda (nn, (S.lift 1 s), t'),
521 subst, menv, ug, eq_found)
523 | Some (s', subst, menv, ug, eq_found) ->
524 Some (C.Lambda (nn, s', (S.lift 1 t)),
525 subst, menv, ug, eq_found)
530 if Utils.debug_res then ignore(check_res res "demod_aux output");
536 (** demodulation, when target is an equality *)
537 let rec demodulation_equality ?from eq_uri newmeta env table target =
538 let module C = Cic in
539 let module S = CicSubstitution in
540 let module M = CicMetaSubst in
541 let module HL = HelmLibraryObjects in
542 let module U = Utils in
543 let metasenv, context, ugraph = env in
544 let w, proof, (eq_ty, left, right, order), metas, id =
545 Equality.open_equality target
547 (* first, we simplify *)
548 (* let right = U.guarded_simpl context right in *)
549 (* let left = U.guarded_simpl context left in *)
550 (* let order = !Utils.compare_terms left right in *)
551 (* let stat = (eq_ty, left, right, order) in *)
552 (* let w = Utils.compute_equality_weight stat in*)
553 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
554 if Utils.debug_metas then
555 ignore(check_target context target "demod equalities input");
556 let metasenv' = (* metasenv @ *) metas in
557 let maxmeta = ref newmeta in
559 let build_newtarget is_left (t, subst, menv, ug, eq_found) =
561 if Utils.debug_metas then
563 ignore(check_for_duplicates menv "input1");
564 ignore(check_disjoint_invariant subst menv "input2");
565 let substs = Subst.ppsubst subst in
566 ignore(check_target context (snd eq_found) ("input3" ^ substs))
568 let pos, equality = eq_found in
570 (ty, what, other, _), menv',id') = Equality.open_equality equality in
572 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
573 with CicUtil.Meta_not_found _ -> ty
575 let what, other = if pos = Utils.Left then what, other else other, what in
576 let newterm, newproof =
578 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
579 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
580 let name = C.Name "x" in
582 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
583 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
585 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
586 (Cic.Lambda (name, ty, bo'))))))
588 let newmenv = menv in
589 let left, right = if is_left then newterm, right else left, newterm in
590 let ordering = !Utils.compare_terms left right in
591 let stat = (eq_ty, left, right, ordering) in
593 let w = Utils.compute_equality_weight stat in
594 (Equality.mk_equality (w, newproof, stat,newmenv))
596 if Utils.debug_metas then
597 ignore(check_target context res "buildnew_target output");
601 let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
602 if Utils.debug_res then check_res res "demod result";
603 let newmeta, newtarget =
606 let newmeta, newtarget = build_newtarget true t in
607 assert (not (Equality.meta_convertibility_eq target newtarget));
608 if (Equality.is_weak_identity newtarget) ||
609 (Equality.meta_convertibility_eq target newtarget) then
612 demodulation_equality ?from eq_uri newmeta env table newtarget
614 let res = demodulation_aux metasenv' context ugraph table 0 right in
615 if Utils.debug_res then check_res res "demod result 1";
618 let newmeta, newtarget = build_newtarget false t in
619 if (Equality.is_weak_identity newtarget) ||
620 (Equality.meta_convertibility_eq target newtarget) then
623 demodulation_equality ?from eq_uri newmeta env table newtarget
627 (* newmeta, newtarget *)
632 Performs the beta expansion of the term "term" w.r.t. "table",
633 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
636 let rec betaexpand_term
637 ?(subterms_only=false) metasenv context ugraph table lift_amount term
639 let module C = Cic in
640 let module S = CicSubstitution in
641 let module M = CicMetaSubst in
642 let module HL = HelmLibraryObjects in
644 let res, lifted_term =
650 (fun arg (res, lifted_tl) ->
653 let arg_res, lifted_arg =
654 betaexpand_term metasenv context ugraph table
658 (fun (t, s, m, ug, eq_found) ->
659 (Some t)::lifted_tl, s, m, ug, eq_found)
664 (fun (l, s, m, ug, eq_found) ->
665 (Some lifted_arg)::l, s, m, ug, eq_found)
667 (Some lifted_arg)::lifted_tl)
670 (fun (r, s, m, ug, eq_found) ->
671 None::r, s, m, ug, eq_found) res,
677 (fun (l, s, m, ug, eq_found) ->
678 (C.Meta (i, l), s, m, ug, eq_found)) l'
680 e, C.Meta (i, lifted_l)
683 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
685 | C.Prod (nn, s, t) ->
687 betaexpand_term metasenv context ugraph table lift_amount s in
689 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
690 table (lift_amount+1) t in
693 (fun (t, s, m, ug, eq_found) ->
694 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
697 (fun (t, s, m, ug, eq_found) ->
698 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
699 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
701 | C.Lambda (nn, s, t) ->
703 betaexpand_term metasenv context ugraph table lift_amount s in
705 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
706 table (lift_amount+1) t in
709 (fun (t, s, m, ug, eq_found) ->
710 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
713 (fun (t, s, m, ug, eq_found) ->
714 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
715 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
720 (fun (res, lifted_tl) arg ->
721 let arg_res, lifted_arg =
722 betaexpand_term metasenv context ugraph table lift_amount arg
726 (fun (a, s, m, ug, eq_found) ->
727 a::lifted_tl, s, m, ug, eq_found)
732 (fun (r, s, m, ug, eq_found) ->
733 lifted_arg::r, s, m, ug, eq_found)
735 lifted_arg::lifted_tl)
736 ) ([], []) (List.rev l)
739 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
742 | t -> [], (S.lift lift_amount t)
745 | C.Meta (i, l) -> res, lifted_term
748 C.Implicit None, ugraph
749 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
751 let candidates = get_candidates Unification table term in
753 if subterms_only then
757 metasenv context ugraph lift_amount term termty candidates
764 returns a list of new clauses inferred with a right superposition step
765 between the positive equation "target" and one in the "table" "newmeta" is
766 the first free meta index, i.e. the first number above the highest meta
767 index: its updated value is also returned
769 let superposition_right
770 ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
771 let module C = Cic in
772 let module S = CicSubstitution in
773 let module M = CicMetaSubst in
774 let module HL = HelmLibraryObjects in
775 let module CR = CicReduction in
776 let module U = Utils in
777 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
778 Equality.open_equality target
780 if Utils.debug_metas then
781 ignore (check_target context target "superpositionright");
782 let metasenv' = newmetas in
783 let maxmeta = ref newmeta in
787 fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
789 [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
793 (fun (_, subst, _, _, _) ->
794 let subst = apply_subst subst in
795 let o = !Utils.compare_terms (subst l) (subst r) in
796 o <> U.Lt && o <> U.Le)
797 (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
799 (res left right), (res right left)
801 let build_new ordering (bo, s, m, ug, eq_found) =
802 if Utils.debug_metas then
803 ignore (check_target context (snd eq_found) "buildnew1" );
805 let pos, equality = eq_found in
806 let (_, proof', (ty, what, other, _), menv',id') =
807 Equality.open_equality equality in
808 let what, other = if pos = Utils.Left then what, other else other, what in
810 let newgoal, newproof =
813 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
815 let name = C.Name "x" in
818 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
819 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
823 (s,(Equality.SuperpositionRight,
824 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
826 let newmeta, newequality =
828 if ordering = U.Gt then newgoal, apply_subst s right
829 else apply_subst s left, newgoal in
830 let neworder = !Utils.compare_terms left right in
831 let newmenv = (* Inference.filter s *) m in
832 let stat = (eq_ty, left, right, neworder) in
834 let w = Utils.compute_equality_weight stat in
835 Equality.mk_equality (w, newproof, stat, newmenv) in
836 if Utils.debug_metas then
837 ignore (check_target context eq' "buildnew3");
838 let newm, eq' = Equality.fix_metas !maxmeta eq' in
839 if Utils.debug_metas then
840 ignore (check_target context eq' "buildnew4");
844 if Utils.debug_metas then
845 ignore(check_target context newequality "buildnew2");
848 let new1 = List.map (build_new U.Gt) res1
849 and new2 = List.map (build_new U.Lt) res2 in
850 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
852 (List.filter ok (new1 @ new2)))
855 (** demodulation, when the target is a theorem *)
856 let rec demodulation_theorem newmeta env table theorem =
857 let module C = Cic in
858 let module S = CicSubstitution in
859 let module M = CicMetaSubst in
860 let module HL = HelmLibraryObjects in
861 let metasenv, context, ugraph = env in
862 let maxmeta = ref newmeta in
863 let term, termty, metas = theorem in
864 let metasenv' = metas in
866 let build_newtheorem (t, subst, menv, ug, eq_found) =
867 let pos, equality = eq_found in
868 let (_, proof', (ty, what, other, _), menv',id) =
869 Equality.open_equality equality in
870 let what, other = if pos = Utils.Left then what, other else other, what in
872 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
873 (* let bo' = apply_subst subst t in *)
874 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
877 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
878 Equality.BasicProof (Equality.empty_subst,term))
880 (Equality.build_proof_term_old newproofold, bo)
882 (* TODO, not ported to the new proofs *)
883 if true then assert false; term, bo
885 !maxmeta, (newterm, newty, menv)
888 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
892 let newmeta, newthm = build_newtheorem t in
893 let newt, newty, _ = newthm in
894 if Equality.meta_convertibility termty newty then
897 demodulation_theorem newmeta env table newthm
902 (*****************************************************************************)
903 (** OPERATIONS ON GOALS **)
905 (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
906 (*****************************************************************************)
910 | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
911 assert (LibraryObjects.is_eq_URI uri);
916 let ty_of_goal (_,_,ty) = ty ;;
918 (* checks if two goals are metaconvertible *)
919 let goal_metaconvertibility_eq g1 g2 =
920 Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
923 (* when the betaexpand_term function is called on the left/right side of the
924 * goal, the predicate has to be fixed
925 * C[x] ---> (eq ty unchanged C[x])
926 * [posu] is the side of the [unchanged] term in the original goal
928 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
929 let _,_,eq,ty,l,r = open_goal goal in
930 let unchanged = if posu = Utils.Left then l else r in
931 let unchanged = CicSubstitution.lift 1 unchanged in
932 let ty = CicSubstitution.lift 1 ty in
935 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
936 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
938 (pred, subst, menv, ug, eq_f)
941 (* ginve the old [goal], the side that has not changed [posu] and the
942 * expansion builds a new goal *)
943 let build_newgoal context goal posu rule expansion =
944 let goalproof,_,_,_,_,_ = open_goal goal in
945 let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
946 let pos, equality = eq_found in
947 let (_, proof', (ty, what, other, _), menv',id) =
948 Equality.open_equality equality in
949 let what, other = if pos = Utils.Left then what, other else other, what in
950 let newterm, newgoalproof =
952 Utils.guarded_simpl context
953 (apply_subst subst (CicSubstitution.subst other t))
955 let bo' = (*apply_subst subst*) t in
956 let name = Cic.Name "x" in
957 let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
958 bo, (newgoalproofstep::goalproof)
960 let newmetasenv = (* Inference.filter subst *) menv in
961 (newgoalproof, newmetasenv, newterm)
966 returns a list of new clauses inferred with a left superposition step
967 the negative equation "target" and one of the positive equations in "table"
969 let superposition_left (metasenv, context, ugraph) table goal maxmeta =
970 let names = Utils.names_of_context context in
971 let proof,menv,eq,ty,l,r = open_goal goal in
972 let c = !Utils.compare_terms l r in
974 if c = Utils.Incomparable then
976 let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
977 let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
978 (* prerr_endline "incomparable";
979 prerr_endline (string_of_int (List.length expansionsl));
980 prerr_endline (string_of_int (List.length expansionsr));
982 List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
984 List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
988 | Utils.Gt -> (* prerr_endline "GT"; *)
989 let big,small,possmall = l,r,Utils.Right in
990 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
992 (build_newgoal context goal possmall Equality.SuperpositionLeft)
994 | Utils.Lt -> (* prerr_endline "LT"; *)
995 let big,small,possmall = r,l,Utils.Left in
996 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
998 (build_newgoal context goal possmall Equality.SuperpositionLeft)
1003 ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1006 (* rinfresco le meta *)
1009 let max,g = Equality.fix_metas_goal max g in max,g::acc)
1010 newgoals (maxmeta,[])
1013 (** demodulation, when the target is a goal *)
1014 let rec demodulation_goal env table goal =
1015 let goalproof,menv,_,_,left,right = open_goal goal in
1016 let _, context, ugraph = env in
1017 (* let term = Utils.guarded_simpl (~debug:true) context term in*)
1019 let resright = demodulation_aux menv context ugraph table 0 right in
1023 build_newgoal context goal Utils.Left Equality.Demodulation t
1025 if goal_metaconvertibility_eq goal newg then
1028 true, snd (demodulation_goal env table newg)
1029 | None -> false, goal
1031 let resleft = demodulation_aux menv context ugraph table 0 left in
1034 let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
1035 if goal_metaconvertibility_eq goal newg then
1038 true, snd (demodulation_goal env table newg)
1039 | None -> do_right ()
1042 let get_stats () = <:show<Indexing.>> ;;