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 let rec aux = function
114 | (m,_,_)::tl -> not (List.exists (fun (i, _, _) -> i = m) tl) && aux tl in
118 prerr_endline ("DUPLICATI " ^ msg);
119 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
125 let check_metasenv msg menv =
128 try ignore(CicTypeChecker.type_of_aux' menv ctx ty
129 CicUniv.empty_ugraph)
131 | CicUtil.Meta_not_found _ ->
132 prerr_endline (msg ^ CicMetaSubst.ppmetasenv [] menv);
138 (* the metasenv returned by res must included in the original one,
139 due to matching. If it fails, it is probably because we are not
140 demodulating with a unit equality *)
142 let not_unit_eq ctx eq =
143 let (_,_,(ty,left,right,o),metas,_) = Equality.open_equality eq in
148 let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.empty_ugraph
149 in s = Cic.Sort(Cic.Prop)
151 prerr_endline ("ERROR typing " ^ CicPp.ppterm ty); assert false) metas
154 if b then prerr_endline ("not a unit equality: " ^ Equality.string_of_equality eq); b *)
157 let check_demod_res res metasenv msg =
159 | Some (_, _, menv, _, _) ->
163 (List.exists (fun (j,_,_) -> i=j) metasenv)) menv
167 debug_print (lazy ("extended context " ^ msg));
168 debug_print (lazy (CicMetaSubst.ppmetasenv [] menv));
174 let check_res res msg =
176 | Some (t, subst, menv, ug, eq_found) ->
177 let eqs = Equality.string_of_equality (snd eq_found) in
178 check_metasenv msg menv;
179 check_disjoint_invariant subst menv msg;
180 check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
184 let check_target bag context target msg =
185 let w, proof, (eq_ty, left, right, order), metas,_ =
186 Equality.open_equality target in
187 (* check that metas does not contains duplicates *)
188 let eqs = Equality.string_of_equality target in
189 let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
190 let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
191 @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof bag proof) in
192 let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
193 let _ = if menv <> metas then
195 prerr_endline ("extra metas " ^ msg);
196 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
197 prerr_endline "**********************";
198 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
199 prerr_endline ("left: " ^ (CicPp.ppterm left));
200 prerr_endline ("right: " ^ (CicPp.ppterm right));
201 prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
207 ignore(CicTypeChecker.type_of_aux'
208 metas context (Founif.build_proof_term proof) CicUniv.empty_ugraph)
211 prerr_endline (Founif.string_of_proof proof);
212 prerr_endline (CicPp.ppterm (Founif.build_proof_term proof));
213 prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
214 prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
219 (* returns a list of all the equalities in the tree that are in relation
220 "mode" with the given term, where mode can be either Matching or
223 Format of the return value: list of tuples in the form:
224 (position - Left or Right - of the term that matched the given one in this
228 Note that if equality is "left = right", if the ordering is left > right,
229 the position will always be Left, and if the ordering is left < right,
230 position will be Right.
233 let get_candidates ?env mode tree term =
237 Index.retrieve_generalizations tree term
239 Index.retrieve_unifiables tree term
242 Index.PosEqSet.elements s
246 finds the first equality in the index that matches "term", of type "termty"
247 termty can be Implicit if it is not needed. The result (one of the sides of
248 the equality, actually) should be not greater (wrt the term ordering) than
251 Format of the return value:
253 (term to substitute, [Cic.Rel 1 properly lifted - see the various
254 build_newtarget functions inside the various
255 demodulation_* functions]
256 substitution used for the matching,
258 ugraph, [substitution, metasenv and ugraph have the same meaning as those
259 returned by CicUnification.fo_unif]
260 (equality where the matching term was found, [i.e. the equality to use as
262 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
263 the equality: this is used to build the proof term, again see one of
264 the build_newtarget functions]
267 let rec find_matches bag metasenv context ugraph lift_amount term termty =
268 let module C = Cic in
269 let module U = Utils in
270 let module S = CicSubstitution in
271 let module M = CicMetaSubst in
272 let module HL = HelmLibraryObjects in
273 let cmp = !Utils.compare_terms in
274 let check = match termty with C.Implicit None -> false | _ -> true in
278 let pos, equality = candidate in
279 (* if not_unit_eq context equality then
281 prerr_endline "not a unit";
282 prerr_endline (Equality.string_of_equality equality)
284 let (_, proof, (ty, left, right, o), metas,_) =
285 Equality.open_equality equality
287 if Utils.debug_metas then
288 ignore(check_target bag context (snd candidate) "find_matches");
289 if Utils.debug_res then
291 let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
292 let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
293 let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
294 let ms="metasenv =" ^ (CicMetaSubst.ppmetasenv [] metasenv) ^ "\n" in
296 match LibraryObjects.eq_URI () with
298 | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
300 (CicPp.ppterm(Equality.build_proof_term bag eq_uri [] 0 proof))^"\n"
303 check_for_duplicates metas "gia nella metas";
304 check_for_duplicates metasenv "gia nel metasenv";
305 check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^ms^p)
307 if check && not (fst (CicReduction.are_convertible
308 ~metasenv context termty ty ugraph)) then (
309 find_matches bag metasenv context ugraph lift_amount term termty tl
312 let subst', metasenv', ugraph' =
314 metasenv metas context term (S.lift lift_amount c) ugraph
316 check_metasenv "founif :" metasenv';
317 Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
320 if pos = Utils.Left then left, right
323 if o <> U.Incomparable then
327 with Founif.MatchingFailure ->
328 find_matches bag metasenv context ugraph lift_amount term termty tl
330 if Utils.debug_res then ignore (check_res res "find1");
335 with Founif.MatchingFailure -> None
337 if Utils.debug_res then ignore (check_res res "find2");
339 | Some (_, s, _, _, _) ->
340 let c' = apply_subst s c in
342 let other' = U.guarded_simpl context (apply_subst s other) in *)
343 let other' = apply_subst s other in
344 let order = cmp c' other' in
349 metasenv context ugraph lift_amount term termty tl
351 find_matches bag metasenv context ugraph lift_amount term termty tl
354 let find_matches metasenv context ugraph lift_amount term termty =
355 find_matches metasenv context ugraph lift_amount term termty
359 as above, but finds all the matching equalities, and the matching condition
360 can be either Founif.matching or Inference.unification
362 (* XXX termty unused *)
363 let rec find_all_matches ?(unif_fun=Founif.unification) ?(demod=false)
364 metasenv context ugraph lift_amount term termty =
365 let module C = Cic in
366 let module U = Utils in
367 let module S = CicSubstitution in
368 let module M = CicMetaSubst in
369 let module HL = HelmLibraryObjects in
370 (* prerr_endline ("matching " ^ CicPp.ppterm term); *)
372 let r = !Utils.compare_terms x y in
375 CicPp.ppterm x ^ " " ^
376 Utils.string_of_comparison r ^ " " ^
381 let check = match termty with C.Implicit None -> false | _ -> true in
385 let pos, equality = candidate in
386 let (_,_,(ty,left,right,o),metas,_)= Equality.open_equality equality in
387 if check && not (fst (CicReduction.are_convertible
388 ~metasenv context termty ty ugraph)) then (
389 find_all_matches metasenv context ugraph lift_amount term termty tl
392 let subst', metasenv', ugraph' =
393 unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
395 (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
399 if pos = Utils.Left then left, right
402 if o <> U.Incomparable then
404 let res = do_match c in
405 res::(find_all_matches ~unif_fun metasenv context ugraph
406 lift_amount term termty tl)
408 | Founif.MatchingFailure
409 | CicUnification.UnificationFailure _
410 | CicUnification.Uncertain _ ->
411 find_all_matches ~unif_fun metasenv context ugraph
412 lift_amount term termty tl
415 let res = do_match c in
418 let c' = apply_subst s c
419 and other' = apply_subst s other in
420 let order = cmp c' other' in
421 if (demod && order = U.Gt) ||
422 (not demod && (order <> U.Lt && order <> U.Le))
424 res::(find_all_matches ~unif_fun metasenv context ugraph
425 lift_amount term termty tl)
427 find_all_matches ~unif_fun metasenv context ugraph
428 lift_amount term termty tl
430 | Founif.MatchingFailure
431 | CicUnification.UnificationFailure _
432 | CicUnification.Uncertain _ ->
433 find_all_matches ~unif_fun metasenv context ugraph
434 lift_amount term termty tl
438 ?unif_fun ?demod metasenv context ugraph lift_amount term termty l
441 ?unif_fun ?demod metasenv context ugraph lift_amount term termty l
442 (*prerr_endline "CANDIDATES:";
443 List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
444 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
448 returns true if target is subsumed by some equality in table
452 prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
453 ((pos,equation),_)) -> Equality.string_of_equality equation)l))
457 let subsumption_aux use_unification env table target =
458 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
459 let _, context, ugraph = env in
460 let metasenv = tmetas in
461 let predicate, unif_fun =
462 if use_unification then
463 Unification, Founif.unification
465 Matching, Founif.matching
469 | Cic.Meta _ when not use_unification -> []
471 let leftc = get_candidates predicate table left in
472 find_all_matches ~unif_fun
473 metasenv context ugraph 0 left ty leftc
475 let rec ok what leftorright = function
477 | (_, subst, menv, ug, (pos,equation))::tl ->
478 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
480 let other = if pos = Utils.Left then r else l in
481 let what' = Subst.apply_subst subst what in
482 let other' = Subst.apply_subst subst other in
483 let subst', menv', ug' =
484 unif_fun metasenv m context what' other' ugraph
486 (match Subst.merge_subst_if_possible subst subst' with
487 | None -> ok what leftorright tl
488 | Some s -> Some (s, equation, leftorright <> pos ))
490 | Founif.MatchingFailure
491 | CicUnification.UnificationFailure _ -> ok what leftorright tl
493 match ok right Utils.Left leftr with
494 | Some _ as res -> res
498 | Cic.Meta _ when not use_unification -> []
500 let rightc = get_candidates predicate table right in
501 find_all_matches ~unif_fun
502 metasenv context ugraph 0 right ty rightc
504 ok left Utils.Right rightr
507 let subsumption x y z =
508 subsumption_aux false x y z
511 let unification x y z =
512 subsumption_aux true x y z
515 (* the target must be disjoint from the equations in the table *)
516 let subsumption_aux_all use_unification env table target =
517 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
518 let _, context, ugraph = env in
519 let metasenv = tmetas in
520 check_for_duplicates metasenv "subsumption_aux_all";
521 let predicate, unif_fun =
522 if use_unification then
523 Unification, Founif.unification
525 Matching, Founif.matching
529 | Cic.Meta _ (*when not use_unification*) -> []
531 let leftc = get_candidates predicate table left in
532 find_all_matches ~unif_fun
533 metasenv context ugraph 0 left ty leftc
537 | Cic.Meta _ (*when not use_unification*) -> []
539 let rightc = get_candidates predicate table right in
540 find_all_matches ~unif_fun
541 metasenv context ugraph 0 right ty rightc
543 let rec ok_all what leftorright = function
545 | (_, subst, menv, ug, (pos,equation))::tl ->
546 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
548 let other = if pos = Utils.Left then r else l in
549 let what' = Subst.apply_subst subst what in
550 let other' = Subst.apply_subst subst other in
551 let subst', menv', ug' =
552 unif_fun [] menv context what' other' ugraph
554 (match Subst.merge_subst_if_possible subst subst' with
555 | None -> ok_all what leftorright tl
557 (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
559 | Founif.MatchingFailure
560 | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
562 (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
565 let subsumption_all x y z =
566 subsumption_aux_all false x y z
569 let unification_all x y z =
570 subsumption_aux_all true x y z
573 let rec demodulation_aux bag ?from ?(typecheck=false)
574 metasenv context ugraph table lift_amount term =
575 let module C = Cic in
576 let module S = CicSubstitution in
577 let module M = CicMetaSubst in
578 let module HL = HelmLibraryObjects in
579 check_for_duplicates metasenv "in input a demodulation aux";
582 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
583 in let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates
593 CicTypeChecker.type_of_aux' metasenv context term ugraph
595 C.Implicit None, ugraph
597 find_matches bag metasenv context ugraph
598 lift_amount term termty candidates
600 prerr_endline "type checking error";
601 prerr_endline ("menv :\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
602 prerr_endline ("term: " ^ (CicPp.ppterm term));
607 (if Utils.debug_res then
608 ignore(check_res res "demod1");
609 if check_demod_res res metasenv "demod" then res else None) in
619 (res, tl @ [S.lift 1 t])
622 demodulation_aux bag ~from:"1" metasenv context ugraph table ~typecheck
626 | None -> (None, tl @ [S.lift 1 t])
627 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
632 | Some (_, subst, menv, ug, eq_found) ->
633 Some (C.Appl ll, subst, menv, ug, eq_found)
636 | C.Prod (nn, s, t) ->
638 demodulation_aux bag ~from:"2"
639 metasenv context ugraph table lift_amount s in (
643 demodulation_aux bag metasenv
644 ((Some (nn, C.Decl s))::context) ugraph
645 table (lift_amount+1) t
649 | Some (t', subst, menv, ug, eq_found) ->
650 Some (C.Prod (nn, (S.lift 1 s), t'),
651 subst, menv, ug, eq_found)
653 | Some (s', subst, menv, ug, eq_found) ->
654 Some (C.Prod (nn, s', (S.lift 1 t)),
655 subst, menv, ug, eq_found)
657 | C.Lambda (nn, s, t) ->
658 prerr_endline "siam qui";
661 metasenv context ugraph table lift_amount s in (
665 demodulation_aux bag metasenv
666 ((Some (nn, C.Decl s))::context) ugraph
667 table (lift_amount+1) t
671 | Some (t', subst, menv, ug, eq_found) ->
672 Some (C.Lambda (nn, (S.lift 1 s), t'),
673 subst, menv, ug, eq_found)
675 | Some (s', subst, menv, ug, eq_found) ->
676 Some (C.Lambda (nn, s', (S.lift 1 t)),
677 subst, menv, ug, eq_found)
683 if Utils.debug_res then ignore(check_res res "demod_aux output");
689 (** demodulation, when target is an equality *)
690 let rec demodulation_equality bag ?from eq_uri env table target =
691 let module C = Cic in
692 let module S = CicSubstitution in
693 let module M = CicMetaSubst in
694 let module HL = HelmLibraryObjects in
695 let module U = Utils in
696 let metasenv, context, ugraph = env in
697 let w, proof, (eq_ty, left, right, order), metas, id =
698 Equality.open_equality target
700 (* first, we simplify *)
701 (* let right = U.guarded_simpl context right in *)
702 (* let left = U.guarded_simpl context left in *)
703 (* let order = !Utils.compare_terms left right in *)
704 (* let stat = (eq_ty, left, right, order) in *)
705 (* let w = Utils.compute_equality_weight stat in*)
706 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
707 if Utils.debug_metas then
708 ignore(check_target bag context target "demod equalities input");
709 let metasenv' = (* metasenv @ *) metas in
711 let build_newtarget bag is_left (t, subst, menv, ug, eq_found) =
713 if Utils.debug_metas then
715 ignore(check_for_duplicates menv "input1");
716 ignore(check_disjoint_invariant subst menv "input2");
717 let substs = Subst.ppsubst subst in
718 ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
720 let pos, equality = eq_found in
722 (ty, what, other, _), menv',id') = Equality.open_equality equality in
724 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
725 with CicUtil.Meta_not_found _ -> ty
727 let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
728 let what, other = if pos = Utils.Left then what, other else other, what in
729 let newterm, newproof =
731 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
732 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
733 let name = C.Name "x" in
735 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
736 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
738 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
739 (Cic.Lambda (name, ty, bo'))))))
741 let newmenv = menv in
742 let left, right = if is_left then newterm, right else left, newterm in
743 let ordering = !Utils.compare_terms left right in
744 let stat = (eq_ty, left, right, ordering) in
746 let w = Utils.compute_equality_weight stat in
747 Equality.mk_equality bag (w, newproof, stat,newmenv)
749 if Utils.debug_metas then
750 ignore(check_target bag context res "buildnew_target output");
754 demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left
756 if Utils.debug_res then check_res res "demod result";
760 let bag, newtarget = build_newtarget bag true t in
761 (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
762 if (Equality.is_weak_identity newtarget) (* || *)
763 (*Equality.meta_convertibility_eq target newtarget*) then
766 demodulation_equality bag ?from eq_uri env table newtarget
768 let res = demodulation_aux bag metasenv' context ugraph table 0 right in
769 if Utils.debug_res then check_res res "demod result 1";
772 let bag, newtarget = build_newtarget bag false t in
773 if (Equality.is_weak_identity newtarget) ||
774 (Equality.meta_convertibility_eq target newtarget) then
777 demodulation_equality bag ?from eq_uri env table newtarget
781 (* newmeta, newtarget *)
786 Performs the beta expansion of the term "term" w.r.t. "table",
787 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
790 let rec betaexpand_term
791 ?(subterms_only=false) metasenv context ugraph table lift_amount term
793 let module C = Cic in
794 let module S = CicSubstitution in
795 let module M = CicMetaSubst in
796 let module HL = HelmLibraryObjects in
798 let res, lifted_term =
804 (fun arg (res, lifted_tl) ->
807 let arg_res, lifted_arg =
808 betaexpand_term metasenv context ugraph table
812 (fun (t, s, m, ug, eq_found) ->
813 (Some t)::lifted_tl, s, m, ug, eq_found)
818 (fun (l, s, m, ug, eq_found) ->
819 (Some lifted_arg)::l, s, m, ug, eq_found)
821 (Some lifted_arg)::lifted_tl)
824 (fun (r, s, m, ug, eq_found) ->
825 None::r, s, m, ug, eq_found) res,
831 (fun (l, s, m, ug, eq_found) ->
832 (C.Meta (i, l), s, m, ug, eq_found)) l'
834 e, C.Meta (i, lifted_l)
837 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
839 | C.Prod (nn, s, t) ->
841 betaexpand_term metasenv context ugraph table lift_amount s in
843 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
844 table (lift_amount+1) t in
847 (fun (t, s, m, ug, eq_found) ->
848 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
851 (fun (t, s, m, ug, eq_found) ->
852 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
853 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
855 | C.Lambda (nn, s, t) ->
857 betaexpand_term metasenv context ugraph table lift_amount s in
859 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
860 table (lift_amount+1) t in
863 (fun (t, s, m, ug, eq_found) ->
864 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
867 (fun (t, s, m, ug, eq_found) ->
868 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
869 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
874 (fun (res, lifted_tl) arg ->
875 let arg_res, lifted_arg =
876 betaexpand_term metasenv context ugraph table lift_amount arg
880 (fun (a, s, m, ug, eq_found) ->
881 a::lifted_tl, s, m, ug, eq_found)
886 (fun (r, s, m, ug, eq_found) ->
887 lifted_arg::r, s, m, ug, eq_found)
889 lifted_arg::lifted_tl)
890 ) ([], []) (List.rev l)
893 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
896 | t -> [], (S.lift lift_amount t)
899 | C.Meta (i, l) -> res, lifted_term
902 (* C.Implicit None, ugraph *)
903 CicTypeChecker.type_of_aux' metasenv context term ugraph
905 let candidates = get_candidates Unification table term in
906 (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
908 if subterms_only then
912 metasenv context ugraph lift_amount term termty candidates
919 returns a list of new clauses inferred with a right superposition step
920 between the positive equation "target" and one in the "table" "newmeta" is
921 the first free meta index, i.e. the first number above the highest meta
922 index: its updated value is also returned
924 let superposition_right bag
925 ?(subterms_only=false) eq_uri (metasenv, context, ugraph) table target=
926 let module C = Cic in
927 let module S = CicSubstitution in
928 let module M = CicMetaSubst in
929 let module HL = HelmLibraryObjects in
930 let module CR = CicReduction in
931 let module U = Utils in
932 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
933 Equality.open_equality target
935 if Utils.debug_metas then
936 ignore (check_target bag context target "superpositionright");
937 let metasenv' = newmetas in
941 fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
943 [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
947 (fun (_, subst, _, _, _) ->
948 let subst = apply_subst subst in
949 let o = !Utils.compare_terms (subst l) (subst r) in
950 o <> U.Lt && o <> U.Le)
951 (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
953 (res left right), (res right left)
955 let build_new bag ordering (bo, s, m, ug, eq_found) =
956 if Utils.debug_metas then
957 ignore (check_target bag context (snd eq_found) "buildnew1" );
959 let pos, equality = eq_found in
960 let (_, proof', (ty, what, other, _), menv',id') =
961 Equality.open_equality equality in
962 let what, other = if pos = Utils.Left then what, other else other, what in
964 let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
965 let newgoal, newproof =
968 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
970 let name = C.Name "x" in
973 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
974 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
978 (s,(Equality.SuperpositionRight,
979 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
981 let bag, newequality =
983 if ordering = U.Gt then newgoal, apply_subst s right
984 else apply_subst s left, newgoal in
985 let neworder = !Utils.compare_terms left right in
986 let newmenv = (* Founif.filter s *) m in
987 let stat = (eq_ty, left, right, neworder) in
989 let w = Utils.compute_equality_weight stat in
990 Equality.mk_equality bag (w, newproof, stat, newmenv) in
991 if Utils.debug_metas then
992 ignore (check_target bag context eq' "buildnew3");
993 let bag, eq' = Equality.fix_metas bag eq' in
994 if Utils.debug_metas then
995 ignore (check_target bag context eq' "buildnew4");
998 if Utils.debug_metas then
999 ignore(check_target bag context newequality "buildnew2");
1005 let bag, e = build_new bag U.Gt x in
1006 bag, e::acc) res1 (bag,[])
1011 let bag, e = build_new bag U.Lt x in
1012 bag, e::acc) res2 (bag,[])
1014 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1015 bag, List.filter ok (new1 @ new2)
1018 (** demodulation, when the target is a theorem *)
1019 let rec demodulation_theorem bag env table theorem =
1020 let module C = Cic in
1021 let module S = CicSubstitution in
1022 let module M = CicMetaSubst in
1023 let module HL = HelmLibraryObjects in
1025 match LibraryObjects.eq_URI() with
1027 | None -> assert false in
1028 let metasenv, context, ugraph = env in
1029 let proof, theo, metas = theorem in
1030 let build_newtheorem (t, subst, menv, ug, eq_found) =
1031 let pos, equality = eq_found in
1032 let (_, proof', (ty, what, other, _), menv',id) =
1033 Equality.open_equality equality in
1036 | Equality.Exact p -> p
1037 | _ -> assert false in
1039 if pos = Utils.Left then what, other else other, what in
1040 let newtheo = apply_subst subst (S.subst other t) in
1041 let name = C.Name "x" in
1042 let body = apply_subst subst t in
1043 let pred = C.Lambda(name,ty,body) in
1047 Equality.mk_eq_ind eq_uri ty what pred proof other peq
1049 Equality.mk_eq_ind eq_uri ty what pred proof other peq
1053 let res = demodulation_aux bag metas context ugraph table 0 theo in
1056 let newproof, newtheo = build_newtheorem t in
1057 if Equality.meta_convertibility theo newtheo then
1060 demodulation_theorem bag env table (newproof,newtheo,[])
1065 (*****************************************************************************)
1066 (** OPERATIONS ON GOALS **)
1068 (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
1069 (*****************************************************************************)
1071 (* new: demodulation of non_equality terms *)
1072 let build_newg bag context goal rule expansion =
1073 let goalproof,_,_ = goal in
1074 let (t,subst,menv,ug,eq_found) = expansion in
1075 let pos, equality = eq_found in
1076 let (_, proof', (ty, what, other, _), menv',id) =
1077 Equality.open_equality equality in
1078 let what, other = if pos = Utils.Left then what, other else other, what in
1079 let newterm, newgoalproof =
1081 Utils.guarded_simpl context
1082 (apply_subst subst (CicSubstitution.subst other t))
1084 let name = Cic.Name "x" in
1085 let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1086 let newgoalproofstep = (rule,pos,id,subst,pred) in
1087 bo, (newgoalproofstep::goalproof)
1089 let newmetasenv = (* Founif.filter subst *) menv in
1090 (newgoalproof, newmetasenv, newterm)
1093 let rec demod bag env table goal =
1094 let _,menv,t = goal in
1095 let _, context, ugraph = env in
1096 let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in
1100 build_newg bag context goal Equality.Demodulation newt
1102 let _,_,newt = newg in
1103 if Equality.meta_convertibility t newt then
1106 true, snd (demod bag env table newg)
1113 | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
1114 (* assert (LibraryObjects.is_eq_URI uri); *)
1115 proof,menv,eq,ty,l,r
1118 let ty_of_goal (_,_,ty) = ty ;;
1120 (* checks if two goals are metaconvertible *)
1121 let goal_metaconvertibility_eq g1 g2 =
1122 Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
1125 (* when the betaexpand_term function is called on the left/right side of the
1126 * goal, the predicate has to be fixed
1127 * C[x] ---> (eq ty unchanged C[x])
1128 * [posu] is the side of the [unchanged] term in the original goal
1131 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1132 let _,_,eq,ty,l,r = open_goal goal in
1133 let unchanged = if posu = Utils.Left then l else r in
1134 let unchanged = CicSubstitution.lift 1 unchanged in
1135 let ty = CicSubstitution.lift 1 ty in
1138 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1139 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1141 (pred, subst, menv, ug, eq_f)
1144 (* ginve the old [goal], the side that has not changed [posu] and the
1145 * expansion builds a new goal *)
1146 let build_newgoal bag context goal posu rule expansion =
1147 let goalproof,_,_,_,_,_ = open_goal goal in
1148 let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
1149 let pos, equality = eq_found in
1150 let (_, proof', (ty, what, other, _), menv',id) =
1151 Equality.open_equality equality in
1152 let what, other = if pos = Utils.Left then what, other else other, what in
1153 let newterm, newgoalproof =
1155 Utils.guarded_simpl context
1156 (apply_subst subst (CicSubstitution.subst other t))
1158 let name = Cic.Name "x" in
1159 let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1160 let newgoalproofstep = (rule,pos,id,subst,pred) in
1161 bo, (newgoalproofstep::goalproof)
1163 let newmetasenv = (* Founif.filter subst *) menv in
1164 (newgoalproof, newmetasenv, newterm)
1169 returns a list of new clauses inferred with a left superposition step
1170 the negative equation "target" and one of the positive equations in "table"
1172 let superposition_left bag (metasenv, context, ugraph) table goal =
1173 let names = Utils.names_of_context context in
1174 let proof,menv,eq,ty,l,r = open_goal goal in
1175 let c = !Utils.compare_terms l r in
1177 if c = Utils.Incomparable then
1179 let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1180 let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1181 (* prerr_endline "incomparable";
1182 prerr_endline (string_of_int (List.length expansionsl));
1183 prerr_endline (string_of_int (List.length expansionsr));
1185 List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1187 List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1192 let big,small,possmall = l,r,Utils.Right in
1193 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1195 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1197 | Utils.Lt -> (* prerr_endline "LT"; *)
1198 let big,small,possmall = r,l,Utils.Left in
1199 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1201 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1206 ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1209 (* rinfresco le meta *)
1212 let b,g = Equality.fix_metas_goal b g in
1217 (** demodulation, when the target is a goal *)
1218 let rec demodulation_goal bag env table goal =
1219 let goalproof,menv,_,_,left,right = open_goal goal in
1220 let _, context, ugraph = env in
1221 (* let term = Utils.guarded_simpl (~debug:true) context term in*)
1223 let resright = demodulation_aux bag menv context ugraph table 0 right in
1227 build_newgoal bag context goal Utils.Left Equality.Demodulation t
1229 if goal_metaconvertibility_eq goal newg then
1232 true, snd (demodulation_goal bag env table newg)
1233 | None -> false, goal
1235 let resleft = demodulation_aux bag menv context ugraph table 0 left in
1238 let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
1239 if goal_metaconvertibility_eq goal newg then
1242 true, snd (demodulation_goal bag env table newg)
1243 | None -> do_right ()
1246 (* returns all the 1 step demodulations *)
1248 module S = CicSubstitution;;
1249 let rec demodulation_all_aux
1250 metasenv context ugraph table lift_amount term
1253 get_candidates ~env:(metasenv,context,ugraph) Matching table term
1258 let termty, ugraph = C.Implicit None, ugraph in
1261 ~unif_fun:Founif.matching ~demod:true
1262 metasenv context ugraph lift_amount term termty candidates
1271 (fun (rel, s, m, ug, c) ->
1272 (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
1273 (demodulation_all_aux
1274 metasenv context ugraph table lift_amount t),
1275 l@[List.hd r], List.tl r)
1276 (res, [], List.map (S.lift 1) l) l
1282 let demod_all steps bag env table goal =
1283 let _, context, ugraph = env in
1284 let is_visited l (_,_,t) =
1285 List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l
1287 let rec aux steps visited bag = function
1288 | _ when steps = 0 -> visited, bag, []
1289 | [] -> visited, bag, []
1290 | goal :: rest when is_visited visited goal -> aux steps visited bag rest
1292 let visited = goal :: visited in
1293 let _,menv,t = goal in
1294 let res = demodulation_all_aux menv context ugraph table 0 t in
1295 let steps = if res = [] then steps-1 else steps in
1297 List.map (build_newg bag context goal Equality.Demodulation) res
1299 let visited, bag, res = aux steps visited bag (new_goals @ rest) in
1300 visited, bag, goal :: res
1302 aux steps [] bag [goal]
1306 let solve_demodulating bag env table initgoal steps =
1307 let proof,menv,eq,ty,left,right = open_goal initgoal in
1310 | Cic.MutInd (u,_,_) -> u
1313 let _, context, ugraph = env in
1314 let v1, bag, l_demod = demod_all steps bag env table ([],menv,left) in
1315 let v2, bag, r_demod = demod_all steps bag env table ([],menv,right) in
1316 let is_solved left right ml mr =
1317 let m = ml @ (List.filter
1318 (fun (x,_,_) -> not (List.exists (fun (y,_,_) -> x=y)ml)) mr)
1322 Founif.unification [] m context left right CicUniv.empty_ugraph in
1323 Some (bag, m,s,Equality.Exact (Equality.refl_proof uri ty left))
1324 with CicUnification.UnificationFailure _ ->
1326 unification_all env table (Equality.mk_tmp_equality
1327 (0,(Cic.Implicit None,left,right,Utils.Incomparable),m))
1329 if solutions = [] then None
1331 let s, e, swapped = List.hd solutions in
1332 let _,p,(ty,l,r,_),me,id = Equality.open_equality e in
1334 if swapped then Equality.symmetric bag ty l id uri me else bag, p
1339 HExtlib.list_findopt
1342 let pl,ml,l,bag,m,s,p =
1344 HExtlib.list_findopt (fun (pl,ml,l) _ ->
1345 match is_solved l r ml mr with
1347 | Some (bag,m,s,p) -> Some (pl,ml,l,bag,m,s,p)
1349 with Some x -> x | _ -> raise Not_found
1353 (fun (rule,pos,id,subst,pred) ->
1356 | Cic.Lambda (name,src,tgt) ->
1357 Cic.Lambda (name,src,
1358 Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
1361 rule,pos,id,subst,pred)
1366 (fun (rule,pos,id,subst,pred) ->
1369 | Cic.Lambda (name,src,tgt) ->
1370 Cic.Lambda (name,src,
1371 Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
1374 rule,pos,id,subst,pred)
1377 Some (bag,pr@pl@proof,m,s,p)
1378 with Not_found -> None)