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 bag 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 bag 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 (Founif.build_proof_term proof) CicUniv.empty_ugraph)
157 prerr_endline (Founif.string_of_proof proof);
158 prerr_endline (CicPp.ppterm (Founif.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 Index.retrieve_generalizations tree term
185 Index.retrieve_unifiables tree term
188 Index.PosEqSet.elements s
192 finds the first equality in the index that matches "term", of type "termty"
193 termty can be Implicit if it is not needed. The result (one of the sides of
194 the equality, actually) should be not greater (wrt the term ordering) than
197 Format of the return value:
199 (term to substitute, [Cic.Rel 1 properly lifted - see the various
200 build_newtarget functions inside the various
201 demodulation_* functions]
202 substitution used for the matching,
204 ugraph, [substitution, metasenv and ugraph have the same meaning as those
205 returned by CicUnification.fo_unif]
206 (equality where the matching term was found, [i.e. the equality to use as
208 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
209 the equality: this is used to build the proof term, again see one of
210 the build_newtarget functions]
213 let rec find_matches bag metasenv context ugraph lift_amount term termty =
214 let module C = Cic in
215 let module U = Utils in
216 let module S = CicSubstitution in
217 let module M = CicMetaSubst in
218 let module HL = HelmLibraryObjects in
219 let cmp = !Utils.compare_terms in
220 let check = match termty with C.Implicit None -> false | _ -> true in
224 let pos, equality = candidate in
225 let (_, proof, (ty, left, right, o), metas,_) =
226 Equality.open_equality equality
228 if Utils.debug_metas then
229 ignore(check_target bag context (snd candidate) "find_matches");
230 if Utils.debug_res then
232 let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
233 let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
234 let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
237 (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
240 check_for_duplicates metas "gia nella metas";
241 check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*))
243 if check && not (fst (CicReduction.are_convertible
244 ~metasenv context termty ty ugraph)) then (
245 find_matches bag metasenv context ugraph lift_amount term termty tl
248 let subst', metasenv', ugraph' =
250 metasenv metas context term (S.lift lift_amount c) ugraph
252 Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
255 if pos = Utils.Left then left, right
258 if o <> U.Incomparable then
262 with Founif.MatchingFailure ->
263 find_matches bag metasenv context ugraph lift_amount term termty tl
265 if Utils.debug_res then ignore (check_res res "find1");
270 with Founif.MatchingFailure -> None
272 if Utils.debug_res then ignore (check_res res "find2");
274 | Some (_, s, _, _, _) ->
275 let c' = apply_subst s c in
277 let other' = U.guarded_simpl context (apply_subst s other) in *)
278 let other' = apply_subst s other in
279 let order = cmp c' other' in
284 metasenv context ugraph lift_amount term termty tl
286 find_matches bag metasenv context ugraph lift_amount term termty tl
289 let find_matches metasenv context ugraph lift_amount term termty =
290 find_matches metasenv context ugraph lift_amount term termty
294 as above, but finds all the matching equalities, and the matching condition
295 can be either Founif.matching or Inference.unification
297 (* XXX termty unused *)
298 let rec find_all_matches ?(unif_fun=Founif.unification)
299 metasenv context ugraph lift_amount term termty =
300 let module C = Cic in
301 let module U = Utils in
302 let module S = CicSubstitution in
303 let module M = CicMetaSubst in
304 let module HL = HelmLibraryObjects in
305 let cmp = !Utils.compare_terms in
309 let pos, equality = candidate in
310 let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
312 let subst', metasenv', ugraph' =
313 unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
315 (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
318 if pos = Utils.Left then left, right
321 if o <> U.Incomparable then
323 let res = do_match c in
324 res::(find_all_matches ~unif_fun metasenv context ugraph
325 lift_amount term termty tl)
327 | Founif.MatchingFailure
328 | CicUnification.UnificationFailure _
329 | CicUnification.Uncertain _ ->
330 find_all_matches ~unif_fun metasenv context ugraph
331 lift_amount term termty tl
334 let res = do_match c in
337 let c' = apply_subst s c
338 and other' = apply_subst s other in
339 let order = cmp c' other' in
340 if order <> U.Lt && order <> U.Le then
341 res::(find_all_matches ~unif_fun metasenv context ugraph
342 lift_amount term termty tl)
344 find_all_matches ~unif_fun metasenv context ugraph
345 lift_amount term termty tl
347 | Founif.MatchingFailure
348 | CicUnification.UnificationFailure _
349 | CicUnification.Uncertain _ ->
350 find_all_matches ~unif_fun metasenv context ugraph
351 lift_amount term termty tl
355 ?unif_fun metasenv context ugraph lift_amount term termty l
358 ?unif_fun metasenv context ugraph lift_amount term termty l
359 (*prerr_endline "CANDIDATES:";
360 List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
361 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
365 returns true if target is subsumed by some equality in table
369 prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
370 ((pos,equation),_)) -> Equality.string_of_equality equation)l))
374 let subsumption_aux use_unification env table target =
375 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
376 let _, context, ugraph = env in
377 let metasenv = tmetas in
378 let predicate, unif_fun =
379 if use_unification then
380 Unification, Founif.unification
382 Matching, Founif.matching
386 | Cic.Meta _ when not use_unification -> []
388 let leftc = get_candidates predicate table left in
389 find_all_matches ~unif_fun
390 metasenv context ugraph 0 left ty leftc
392 let rec ok what leftorright = function
394 | (_, subst, menv, ug, (pos,equation))::tl ->
395 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
397 let other = if pos = Utils.Left then r else l in
398 let what' = Subst.apply_subst subst what in
399 let other' = Subst.apply_subst subst other in
400 let subst', menv', ug' =
401 unif_fun metasenv m context what' other' ugraph
403 (match Subst.merge_subst_if_possible subst subst' with
404 | None -> ok what leftorright tl
405 | Some s -> Some (s, equation, leftorright <> pos ))
407 | Founif.MatchingFailure
408 | CicUnification.UnificationFailure _ -> ok what leftorright tl
410 match ok right Utils.Left leftr with
411 | Some _ as res -> res
415 | Cic.Meta _ when not use_unification -> []
417 let rightc = get_candidates predicate table right in
418 find_all_matches ~unif_fun
419 metasenv context ugraph 0 right ty rightc
421 ok left Utils.Right rightr
424 let subsumption x y z =
425 subsumption_aux false x y z
428 let unification x y z =
429 subsumption_aux true x y z
432 let subsumption_aux_all use_unification env table target =
433 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
434 let _, context, ugraph = env in
435 let metasenv = tmetas in
436 let predicate, unif_fun =
437 if use_unification then
438 Unification, Founif.unification
440 Matching, Founif.matching
444 | Cic.Meta _ when not use_unification -> []
446 let leftc = get_candidates predicate table left in
447 find_all_matches ~unif_fun
448 metasenv context ugraph 0 left ty leftc
452 | Cic.Meta _ when not use_unification -> []
454 let rightc = get_candidates predicate table right in
455 find_all_matches ~unif_fun
456 metasenv context ugraph 0 right ty rightc
458 let rec ok_all what leftorright = function
460 | (_, subst, menv, ug, (pos,equation))::tl ->
461 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
463 let other = if pos = Utils.Left then r else l in
464 let what' = Subst.apply_subst subst what in
465 let other' = Subst.apply_subst subst other in
466 let subst', menv', ug' =
467 unif_fun metasenv m context what' other' ugraph
469 (match Subst.merge_subst_if_possible subst subst' with
470 | None -> ok_all what leftorright tl
472 (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
474 | Founif.MatchingFailure
475 | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
477 (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
480 let subsumption_all x y z =
481 subsumption_aux_all false x y z
484 let unification_all x y z =
485 subsumption_aux_all true x y z
487 let rec demodulation_aux bag ?from ?(typecheck=false)
488 metasenv context ugraph table lift_amount term =
489 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
490 let module C = Cic in
491 let module S = CicSubstitution in
492 let module M = CicMetaSubst in
493 let module HL = HelmLibraryObjects in
496 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
504 CicTypeChecker.type_of_aux' metasenv context term ugraph
506 C.Implicit None, ugraph
509 find_matches bag metasenv context ugraph lift_amount term termty candidates
511 if Utils.debug_res then ignore(check_res res "demod1");
521 (res, tl @ [S.lift 1 t])
524 demodulation_aux bag ~from:"1" metasenv context ugraph table
528 | None -> (None, tl @ [S.lift 1 t])
529 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
534 | Some (_, subst, menv, ug, eq_found) ->
535 Some (C.Appl ll, subst, menv, ug, eq_found)
537 | C.Prod (nn, s, t) ->
539 demodulation_aux bag ~from:"2"
540 metasenv context ugraph table lift_amount s in (
544 demodulation_aux bag metasenv
545 ((Some (nn, C.Decl s))::context) ugraph
546 table (lift_amount+1) t
550 | Some (t', subst, menv, ug, eq_found) ->
551 Some (C.Prod (nn, (S.lift 1 s), t'),
552 subst, menv, ug, eq_found)
554 | Some (s', subst, menv, ug, eq_found) ->
555 Some (C.Prod (nn, s', (S.lift 1 t)),
556 subst, menv, ug, eq_found)
558 | C.Lambda (nn, s, t) ->
561 metasenv context ugraph table lift_amount s in (
565 demodulation_aux bag metasenv
566 ((Some (nn, C.Decl s))::context) ugraph
567 table (lift_amount+1) t
571 | Some (t', subst, menv, ug, eq_found) ->
572 Some (C.Lambda (nn, (S.lift 1 s), t'),
573 subst, menv, ug, eq_found)
575 | Some (s', subst, menv, ug, eq_found) ->
576 Some (C.Lambda (nn, s', (S.lift 1 t)),
577 subst, menv, ug, eq_found)
582 if Utils.debug_res then ignore(check_res res "demod_aux output");
588 (** demodulation, when target is an equality *)
589 let rec demodulation_equality bag ?from eq_uri newmeta env table target =
591 prerr_endline ("demodulation_eq:\n");
592 Index.iter table (fun l ->
593 let l = Index.PosEqSet.elements l in
595 List.map (fun (p,e) ->
596 Utils.string_of_pos p ^ Equality.string_of_equality e) l in
597 prerr_endline (String.concat "\n" l)
600 let module C = Cic in
601 let module S = CicSubstitution in
602 let module M = CicMetaSubst in
603 let module HL = HelmLibraryObjects in
604 let module U = Utils in
605 let metasenv, context, ugraph = env in
606 let w, proof, (eq_ty, left, right, order), metas, id =
607 Equality.open_equality target
609 (* first, we simplify *)
610 (* let right = U.guarded_simpl context right in *)
611 (* let left = U.guarded_simpl context left in *)
612 (* let order = !Utils.compare_terms left right in *)
613 (* let stat = (eq_ty, left, right, order) in *)
614 (* let w = Utils.compute_equality_weight stat in*)
615 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
616 if Utils.debug_metas then
617 ignore(check_target bag context target "demod equalities input");
618 let metasenv' = (* metasenv @ *) metas in
619 let maxmeta = ref newmeta in
621 let build_newtarget is_left (t, subst, menv, ug, eq_found) =
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 bag 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 ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
638 let what, other = if pos = Utils.Left then what, other else other, what in
639 let newterm, newproof =
641 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
642 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
643 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 (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
648 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
649 (Cic.Lambda (name, ty, bo'))))))
651 let newmenv = menv in
652 let left, right = if is_left then newterm, right else left, newterm in
653 let ordering = !Utils.compare_terms left right in
654 let stat = (eq_ty, left, right, ordering) in
656 let w = Utils.compute_equality_weight stat in
657 (Equality.mk_equality bag (w, newproof, stat,newmenv))
659 if Utils.debug_metas then
660 ignore(check_target bag context res "buildnew_target output");
665 demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left
667 if Utils.debug_res then check_res res "demod result";
668 let newmeta, newtarget =
671 let newmeta, newtarget = build_newtarget true t in
672 (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
673 if (Equality.is_weak_identity newtarget) (* || *)
674 (*Equality.meta_convertibility_eq target newtarget*) then
677 demodulation_equality bag ?from eq_uri newmeta env table newtarget
679 let res = demodulation_aux bag metasenv' context ugraph table 0 right in
680 if Utils.debug_res then check_res res "demod result 1";
683 let newmeta, newtarget = build_newtarget false t in
684 if (Equality.is_weak_identity newtarget) ||
685 (Equality.meta_convertibility_eq target newtarget) then
688 demodulation_equality bag ?from eq_uri newmeta env table newtarget
692 (* newmeta, newtarget *)
697 Performs the beta expansion of the term "term" w.r.t. "table",
698 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
701 let rec betaexpand_term
702 ?(subterms_only=false) metasenv context ugraph table lift_amount term
704 let module C = Cic in
705 let module S = CicSubstitution in
706 let module M = CicMetaSubst in
707 let module HL = HelmLibraryObjects in
709 let res, lifted_term =
715 (fun arg (res, lifted_tl) ->
718 let arg_res, lifted_arg =
719 betaexpand_term metasenv context ugraph table
723 (fun (t, s, m, ug, eq_found) ->
724 (Some t)::lifted_tl, s, m, ug, eq_found)
729 (fun (l, s, m, ug, eq_found) ->
730 (Some lifted_arg)::l, s, m, ug, eq_found)
732 (Some lifted_arg)::lifted_tl)
735 (fun (r, s, m, ug, eq_found) ->
736 None::r, s, m, ug, eq_found) res,
742 (fun (l, s, m, ug, eq_found) ->
743 (C.Meta (i, l), s, m, ug, eq_found)) l'
745 e, C.Meta (i, lifted_l)
748 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
750 | C.Prod (nn, s, t) ->
752 betaexpand_term metasenv context ugraph table lift_amount s in
754 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
755 table (lift_amount+1) t in
758 (fun (t, s, m, ug, eq_found) ->
759 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
762 (fun (t, s, m, ug, eq_found) ->
763 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
764 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
766 | C.Lambda (nn, s, t) ->
768 betaexpand_term metasenv context ugraph table lift_amount s in
770 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
771 table (lift_amount+1) t in
774 (fun (t, s, m, ug, eq_found) ->
775 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
778 (fun (t, s, m, ug, eq_found) ->
779 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
780 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
785 (fun (res, lifted_tl) arg ->
786 let arg_res, lifted_arg =
787 betaexpand_term metasenv context ugraph table lift_amount arg
791 (fun (a, s, m, ug, eq_found) ->
792 a::lifted_tl, s, m, ug, eq_found)
797 (fun (r, s, m, ug, eq_found) ->
798 lifted_arg::r, s, m, ug, eq_found)
800 lifted_arg::lifted_tl)
801 ) ([], []) (List.rev l)
804 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
807 | t -> [], (S.lift lift_amount t)
810 | C.Meta (i, l) -> res, lifted_term
813 C.Implicit None, ugraph
814 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
816 let candidates = get_candidates Unification table term in
818 if subterms_only then
822 metasenv context ugraph lift_amount term termty candidates
829 returns a list of new clauses inferred with a right superposition step
830 between the positive equation "target" and one in the "table" "newmeta" is
831 the first free meta index, i.e. the first number above the highest meta
832 index: its updated value is also returned
834 let superposition_right bag
835 ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
836 let module C = Cic in
837 let module S = CicSubstitution in
838 let module M = CicMetaSubst in
839 let module HL = HelmLibraryObjects in
840 let module CR = CicReduction in
841 let module U = Utils in
842 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
843 Equality.open_equality target
845 if Utils.debug_metas then
846 ignore (check_target bag context target "superpositionright");
847 let metasenv' = newmetas in
848 let maxmeta = ref newmeta in
852 fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
854 [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
858 (fun (_, subst, _, _, _) ->
859 let subst = apply_subst subst in
860 let o = !Utils.compare_terms (subst l) (subst r) in
861 o <> U.Lt && o <> U.Le)
862 (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
864 (res left right), (res right left)
866 let build_new ordering (bo, s, m, ug, eq_found) =
867 if Utils.debug_metas then
868 ignore (check_target bag context (snd eq_found) "buildnew1" );
870 let pos, equality = eq_found in
871 let (_, proof', (ty, what, other, _), menv',id') =
872 Equality.open_equality equality in
873 let what, other = if pos = Utils.Left then what, other else other, what in
875 let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
876 let newgoal, newproof =
879 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
881 let name = C.Name "x" in
884 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
885 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
889 (s,(Equality.SuperpositionRight,
890 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
892 let newmeta, newequality =
894 if ordering = U.Gt then newgoal, apply_subst s right
895 else apply_subst s left, newgoal in
896 let neworder = !Utils.compare_terms left right in
897 let newmenv = (* Founif.filter s *) m in
898 let stat = (eq_ty, left, right, neworder) in
900 let w = Utils.compute_equality_weight stat in
901 Equality.mk_equality bag (w, newproof, stat, newmenv) in
902 if Utils.debug_metas then
903 ignore (check_target bag context eq' "buildnew3");
904 let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
905 if Utils.debug_metas then
906 ignore (check_target bag context eq' "buildnew4");
910 if Utils.debug_metas then
911 ignore(check_target bag context newequality "buildnew2");
914 let new1 = List.map (build_new U.Gt) res1
915 and new2 = List.map (build_new U.Lt) res2 in
916 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
918 (List.filter ok (new1 @ new2)))
921 (** demodulation, when the target is a theorem *)
922 let rec demodulation_theorem bag env table theorem =
923 let module C = Cic in
924 let module S = CicSubstitution in
925 let module M = CicMetaSubst in
926 let module HL = HelmLibraryObjects in
928 match LibraryObjects.eq_URI() with
930 | None -> assert false in
931 let metasenv, context, ugraph = env in
932 let proof, theo, metas = theorem in
933 let build_newtheorem (t, subst, menv, ug, eq_found) =
934 let pos, equality = eq_found in
935 let (_, proof', (ty, what, other, _), menv',id) =
936 Equality.open_equality equality in
939 | Equality.Exact p -> p
940 | _ -> assert false in
942 if pos = Utils.Left then what, other else other, what in
943 let newtheo = apply_subst subst (S.subst other t) in
944 let name = C.Name "x" in
945 let body = apply_subst subst t in
946 let pred = C.Lambda(name,ty,body) in
950 Equality.mk_eq_ind eq_uri ty what pred proof other peq
952 Equality.mk_eq_ind eq_uri ty what pred proof other peq
956 let res = demodulation_aux bag metas context ugraph table 0 theo in
959 let newproof, newtheo = build_newtheorem t in
960 if Equality.meta_convertibility theo newtheo then
963 demodulation_theorem bag env table (newproof,newtheo,[])
968 (*****************************************************************************)
969 (** OPERATIONS ON GOALS **)
971 (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
972 (*****************************************************************************)
976 | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
977 (* assert (LibraryObjects.is_eq_URI uri); *)
982 let ty_of_goal (_,_,ty) = ty ;;
984 (* checks if two goals are metaconvertible *)
985 let goal_metaconvertibility_eq g1 g2 =
986 Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
989 (* when the betaexpand_term function is called on the left/right side of the
990 * goal, the predicate has to be fixed
991 * C[x] ---> (eq ty unchanged C[x])
992 * [posu] is the side of the [unchanged] term in the original goal
994 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
995 let _,_,eq,ty,l,r = open_goal goal in
996 let unchanged = if posu = Utils.Left then l else r in
997 let unchanged = CicSubstitution.lift 1 unchanged in
998 let ty = CicSubstitution.lift 1 ty in
1001 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1002 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1004 (pred, subst, menv, ug, eq_f)
1007 (* ginve the old [goal], the side that has not changed [posu] and the
1008 * expansion builds a new goal *)
1009 let build_newgoal bag context goal posu rule expansion =
1010 let goalproof,_,_,_,_,_ = open_goal goal in
1011 let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
1012 let pos, equality = eq_found in
1013 let (_, proof', (ty, what, other, _), menv',id) =
1014 Equality.open_equality equality in
1015 let what, other = if pos = Utils.Left then what, other else other, what in
1016 let newterm, newgoalproof =
1018 Utils.guarded_simpl context
1019 (apply_subst subst (CicSubstitution.subst other t))
1021 let bo' = apply_subst subst t in
1022 let ty = apply_subst subst ty in
1023 let name = Cic.Name "x" in
1024 let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
1025 bo, (newgoalproofstep::goalproof)
1027 let newmetasenv = (* Founif.filter subst *) menv in
1028 (newgoalproof, newmetasenv, newterm)
1033 returns a list of new clauses inferred with a left superposition step
1034 the negative equation "target" and one of the positive equations in "table"
1036 let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
1037 let names = Utils.names_of_context context in
1038 let proof,menv,eq,ty,l,r = open_goal goal in
1039 let c = !Utils.compare_terms l r in
1041 if c = Utils.Incomparable then
1043 let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1044 let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1045 (* prerr_endline "incomparable";
1046 prerr_endline (string_of_int (List.length expansionsl));
1047 prerr_endline (string_of_int (List.length expansionsr));
1049 List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1051 List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1055 | Utils.Gt -> (* prerr_endline "GT"; *)
1056 let big,small,possmall = l,r,Utils.Right in
1057 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1059 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1061 | Utils.Lt -> (* prerr_endline "LT"; *)
1062 let big,small,possmall = r,l,Utils.Left in
1063 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1065 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1070 ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1073 (* rinfresco le meta *)
1076 let max,g = Equality.fix_metas_goal max g in max,g::acc)
1077 newgoals (maxmeta,[])
1080 (** demodulation, when the target is a goal *)
1081 let rec demodulation_goal bag env table goal =
1082 let goalproof,menv,_,_,left,right = open_goal goal in
1083 let _, context, ugraph = env in
1084 (* let term = Utils.guarded_simpl (~debug:true) context term in*)
1086 let resright = demodulation_aux bag menv context ugraph table 0 right in
1090 build_newgoal bag context goal Utils.Left Equality.Demodulation t
1092 if goal_metaconvertibility_eq goal newg then
1095 true, snd (demodulation_goal bag env table newg)
1096 | None -> false, goal
1098 let resleft = demodulation_aux bag menv context ugraph table 0 left in
1101 let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
1102 if goal_metaconvertibility_eq goal newg then
1105 true, snd (demodulation_goal bag env table newg)
1106 | None -> do_right ()
1110 type solved = Yes of Equality.goal | No of Equality.goal list
1112 (* returns all the 1 step demodulations *)
1114 module S = CicSubstitution;;
1115 let rec demodulation_all_aux
1116 metasenv context ugraph table lift_amount term
1119 get_candidates ~env:(metasenv,context,ugraph) Matching table term
1124 let termty, ugraph = C.Implicit None, ugraph in
1127 metasenv context ugraph lift_amount term termty candidates
1136 (fun (rel, s, m, ug, c) ->
1137 (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
1138 (demodulation_all_aux
1139 metasenv context ugraph table lift_amount t),
1140 l@[List.hd r], List.tl r)
1141 (res, [], List.map (S.lift 1) l) l
1145 | C.Lambda (nn, s, t) ->
1146 let context = (Some (nn, C.Decl s))::context in
1149 | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t)
1153 (fun (rel, subst, m, ug, c) ->
1154 mk (S.lift 1 s) rel, subst, m, ug, c)
1155 (demodulation_all_aux
1156 metasenv context ugraph table (lift_amount+1) t)
1157 (* we could demodulate also in s, but then t may be badly
1162 let solve_demodulating bag env table initgoal steps =
1163 let _, context, ugraph = env in
1164 let solved goal res side =
1165 let newg = build_newgoal bag context goal side Equality.Demodulation res in
1167 | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right])
1168 when LibraryObjects.is_eq_URI uri ->
1171 Founif.unification m m context left right CicUniv.empty_ugraph
1174 with CicUnification.UnificationFailure _ -> No [newg])
1177 let solved goal res_list side =
1178 let newg = List.map (fun x -> solved goal x side) res_list in
1180 List.find (function Yes _ -> true | _ -> false) newg
1182 No (List.flatten (List.map (function No s -> s | _-> assert false) newg))
1189 | None -> first f tl
1190 | Some x as ok -> ok
1192 let rec aux steps next goal =
1193 if steps = 0 then None else
1194 let goalproof,menv,_,_,left,right = open_goal goal in
1196 demodulation_all_aux menv context ugraph table 0 t
1200 (match do_step left with
1202 (match solved goal res Utils.Right with
1204 (match first (aux (steps - 1) L) newgoals with
1205 | Some g as success -> success
1206 | None -> aux steps R goal)
1207 | Yes newgoal -> Some newgoal)
1208 | [] -> aux steps R goal)
1210 (match do_step right with
1212 (match solved goal res Utils.Left with
1214 (match first (aux (steps - 1) L) newgoals with
1215 | Some g as success -> success
1217 | Yes newgoal -> Some newgoal)
1220 aux steps L initgoal
1223 let get_stats () = "" ;;