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)
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); *)
371 let cmp = !Utils.compare_terms in
372 let check = match termty with C.Implicit None -> false | _ -> true in
376 let pos, equality = candidate in
377 let (_,_,(ty,left,right,o),metas,_)= Equality.open_equality equality in
378 if check && not (fst (CicReduction.are_convertible
379 ~metasenv context termty ty ugraph)) then (
380 find_all_matches metasenv context ugraph lift_amount term termty tl
383 let subst', metasenv', ugraph' =
384 unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
386 (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
390 if pos = Utils.Left then left, right
393 if o <> U.Incomparable then
395 let res = do_match c in
396 res::(find_all_matches ~unif_fun metasenv context ugraph
397 lift_amount term termty tl)
399 | Founif.MatchingFailure
400 | CicUnification.UnificationFailure _
401 | CicUnification.Uncertain _ ->
402 find_all_matches ~unif_fun metasenv context ugraph
403 lift_amount term termty tl
406 let res = do_match c in
409 let c' = apply_subst s c
410 and other' = apply_subst s other in
411 let order = cmp c' other' in
412 if order <> U.Lt && order <> U.Le then
413 res::(find_all_matches ~unif_fun metasenv context ugraph
414 lift_amount term termty tl)
416 find_all_matches ~unif_fun metasenv context ugraph
417 lift_amount term termty tl
419 | Founif.MatchingFailure
420 | CicUnification.UnificationFailure _
421 | CicUnification.Uncertain _ ->
422 find_all_matches ~unif_fun metasenv context ugraph
423 lift_amount term termty tl
427 ?unif_fun metasenv context ugraph lift_amount term termty l
430 ?unif_fun metasenv context ugraph lift_amount term termty l
431 (*prerr_endline "CANDIDATES:";
432 List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
433 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
437 returns true if target is subsumed by some equality in table
441 prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
442 ((pos,equation),_)) -> Equality.string_of_equality equation)l))
446 let subsumption_aux use_unification env table target =
447 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
448 let _, context, ugraph = env in
449 let metasenv = tmetas in
450 let predicate, unif_fun =
451 if use_unification then
452 Unification, Founif.unification
454 Matching, Founif.matching
458 | Cic.Meta _ when not use_unification -> []
460 let leftc = get_candidates predicate table left in
461 find_all_matches ~unif_fun
462 metasenv context ugraph 0 left ty leftc
464 let rec ok what leftorright = function
466 | (_, subst, menv, ug, (pos,equation))::tl ->
467 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
469 let other = if pos = Utils.Left then r else l in
470 let what' = Subst.apply_subst subst what in
471 let other' = Subst.apply_subst subst other in
472 let subst', menv', ug' =
473 unif_fun metasenv m context what' other' ugraph
475 (match Subst.merge_subst_if_possible subst subst' with
476 | None -> ok what leftorright tl
477 | Some s -> Some (s, equation, leftorright <> pos ))
479 | Founif.MatchingFailure
480 | CicUnification.UnificationFailure _ -> ok what leftorright tl
482 match ok right Utils.Left leftr with
483 | Some _ as res -> res
487 | Cic.Meta _ when not use_unification -> []
489 let rightc = get_candidates predicate table right in
490 find_all_matches ~unif_fun
491 metasenv context ugraph 0 right ty rightc
493 ok left Utils.Right rightr
496 let subsumption x y z =
497 subsumption_aux false x y z
500 let unification x y z =
501 subsumption_aux true x y z
504 (* the target must be disjoint from the equations in the table *)
505 let subsumption_aux_all use_unification env table target =
506 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
507 let _, context, ugraph = env in
508 let metasenv = tmetas in
509 check_for_duplicates metasenv "subsumption_aux_all";
510 let predicate, unif_fun =
511 if use_unification then
512 Unification, Founif.unification
514 Matching, Founif.matching
518 | Cic.Meta _ (*when not use_unification*) -> []
520 let leftc = get_candidates predicate table left in
521 find_all_matches ~unif_fun
522 metasenv context ugraph 0 left ty leftc
526 | Cic.Meta _ (*when not use_unification*) -> []
528 let rightc = get_candidates predicate table right in
529 find_all_matches ~unif_fun
530 metasenv context ugraph 0 right ty rightc
532 let rec ok_all what leftorright = function
534 | (_, subst, menv, ug, (pos,equation))::tl ->
535 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
537 let other = if pos = Utils.Left then r else l in
538 let what' = Subst.apply_subst subst what in
539 let other' = Subst.apply_subst subst other in
540 let subst', menv', ug' =
541 unif_fun [] menv context what' other' ugraph
543 (match Subst.merge_subst_if_possible subst subst' with
544 | None -> ok_all what leftorright tl
546 (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
548 | Founif.MatchingFailure
549 | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
551 (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
554 let subsumption_all x y z =
555 subsumption_aux_all false x y z
558 let unification_all x y z =
559 subsumption_aux_all true x y z
562 let rec demodulation_aux bag ?from ?(typecheck=false)
563 metasenv context ugraph table lift_amount term =
564 let module C = Cic in
565 let module S = CicSubstitution in
566 let module M = CicMetaSubst in
567 let module HL = HelmLibraryObjects in
568 check_for_duplicates metasenv "in input a demodulation aux";
571 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
572 in let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates
582 CicTypeChecker.type_of_aux' metasenv context term ugraph
584 C.Implicit None, ugraph
586 find_matches bag metasenv context ugraph
587 lift_amount term termty candidates
589 prerr_endline "type checking error";
590 prerr_endline ("menv :\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
591 prerr_endline ("term: " ^ (CicPp.ppterm term));
596 (if Utils.debug_res then
597 ignore(check_res res "demod1");
598 if check_demod_res res metasenv "demod" then res else None) in
608 (res, tl @ [S.lift 1 t])
611 demodulation_aux bag ~from:"1" metasenv context ugraph table ~typecheck
615 | None -> (None, tl @ [S.lift 1 t])
616 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
621 | Some (_, subst, menv, ug, eq_found) ->
622 Some (C.Appl ll, subst, menv, ug, eq_found)
625 | C.Prod (nn, s, t) ->
627 demodulation_aux bag ~from:"2"
628 metasenv context ugraph table lift_amount s in (
632 demodulation_aux bag metasenv
633 ((Some (nn, C.Decl s))::context) ugraph
634 table (lift_amount+1) t
638 | Some (t', subst, menv, ug, eq_found) ->
639 Some (C.Prod (nn, (S.lift 1 s), t'),
640 subst, menv, ug, eq_found)
642 | Some (s', subst, menv, ug, eq_found) ->
643 Some (C.Prod (nn, s', (S.lift 1 t)),
644 subst, menv, ug, eq_found)
646 | C.Lambda (nn, s, t) ->
647 prerr_endline "siam qui";
650 metasenv context ugraph table lift_amount s in (
654 demodulation_aux bag metasenv
655 ((Some (nn, C.Decl s))::context) ugraph
656 table (lift_amount+1) t
660 | Some (t', subst, menv, ug, eq_found) ->
661 Some (C.Lambda (nn, (S.lift 1 s), t'),
662 subst, menv, ug, eq_found)
664 | Some (s', subst, menv, ug, eq_found) ->
665 Some (C.Lambda (nn, s', (S.lift 1 t)),
666 subst, menv, ug, eq_found)
672 if Utils.debug_res then ignore(check_res res "demod_aux output");
678 (** demodulation, when target is an equality *)
679 let rec demodulation_equality bag ?from eq_uri env table target =
680 let module C = Cic in
681 let module S = CicSubstitution in
682 let module M = CicMetaSubst in
683 let module HL = HelmLibraryObjects in
684 let module U = Utils in
685 let metasenv, context, ugraph = env in
686 let w, proof, (eq_ty, left, right, order), metas, id =
687 Equality.open_equality target
689 (* first, we simplify *)
690 (* let right = U.guarded_simpl context right in *)
691 (* let left = U.guarded_simpl context left in *)
692 (* let order = !Utils.compare_terms left right in *)
693 (* let stat = (eq_ty, left, right, order) in *)
694 (* let w = Utils.compute_equality_weight stat in*)
695 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
696 if Utils.debug_metas then
697 ignore(check_target bag context target "demod equalities input");
698 let metasenv' = (* metasenv @ *) metas in
700 let build_newtarget bag is_left (t, subst, menv, ug, eq_found) =
702 if Utils.debug_metas then
704 ignore(check_for_duplicates menv "input1");
705 ignore(check_disjoint_invariant subst menv "input2");
706 let substs = Subst.ppsubst subst in
707 ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
709 let pos, equality = eq_found in
711 (ty, what, other, _), menv',id') = Equality.open_equality equality in
713 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
714 with CicUtil.Meta_not_found _ -> ty
716 let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
717 let what, other = if pos = Utils.Left then what, other else other, what in
718 let newterm, newproof =
720 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
721 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
722 let name = C.Name "x" in
724 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
725 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
727 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
728 (Cic.Lambda (name, ty, bo'))))))
730 let newmenv = menv in
731 let left, right = if is_left then newterm, right else left, newterm in
732 let ordering = !Utils.compare_terms left right in
733 let stat = (eq_ty, left, right, ordering) in
735 let w = Utils.compute_equality_weight stat in
736 Equality.mk_equality bag (w, newproof, stat,newmenv)
738 if Utils.debug_metas then
739 ignore(check_target bag context res "buildnew_target output");
743 demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left
745 if Utils.debug_res then check_res res "demod result";
749 let bag, newtarget = build_newtarget bag true t in
750 (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
751 if (Equality.is_weak_identity newtarget) (* || *)
752 (*Equality.meta_convertibility_eq target newtarget*) then
755 demodulation_equality bag ?from eq_uri env table newtarget
757 let res = demodulation_aux bag metasenv' context ugraph table 0 right in
758 if Utils.debug_res then check_res res "demod result 1";
761 let bag, newtarget = build_newtarget bag false t in
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
770 (* newmeta, newtarget *)
775 Performs the beta expansion of the term "term" w.r.t. "table",
776 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
779 let rec betaexpand_term
780 ?(subterms_only=false) metasenv context ugraph table lift_amount term
782 let module C = Cic in
783 let module S = CicSubstitution in
784 let module M = CicMetaSubst in
785 let module HL = HelmLibraryObjects in
787 let res, lifted_term =
793 (fun arg (res, lifted_tl) ->
796 let arg_res, lifted_arg =
797 betaexpand_term metasenv context ugraph table
801 (fun (t, s, m, ug, eq_found) ->
802 (Some t)::lifted_tl, s, m, ug, eq_found)
807 (fun (l, s, m, ug, eq_found) ->
808 (Some lifted_arg)::l, s, m, ug, eq_found)
810 (Some lifted_arg)::lifted_tl)
813 (fun (r, s, m, ug, eq_found) ->
814 None::r, s, m, ug, eq_found) res,
820 (fun (l, s, m, ug, eq_found) ->
821 (C.Meta (i, l), s, m, ug, eq_found)) l'
823 e, C.Meta (i, lifted_l)
826 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
828 | C.Prod (nn, s, t) ->
830 betaexpand_term metasenv context ugraph table lift_amount s in
832 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
833 table (lift_amount+1) t in
836 (fun (t, s, m, ug, eq_found) ->
837 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
840 (fun (t, s, m, ug, eq_found) ->
841 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
842 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
844 | C.Lambda (nn, s, t) ->
846 betaexpand_term metasenv context ugraph table lift_amount s in
848 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
849 table (lift_amount+1) t in
852 (fun (t, s, m, ug, eq_found) ->
853 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
856 (fun (t, s, m, ug, eq_found) ->
857 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
858 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
863 (fun (res, lifted_tl) arg ->
864 let arg_res, lifted_arg =
865 betaexpand_term metasenv context ugraph table lift_amount arg
869 (fun (a, s, m, ug, eq_found) ->
870 a::lifted_tl, s, m, ug, eq_found)
875 (fun (r, s, m, ug, eq_found) ->
876 lifted_arg::r, s, m, ug, eq_found)
878 lifted_arg::lifted_tl)
879 ) ([], []) (List.rev l)
882 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
885 | t -> [], (S.lift lift_amount t)
888 | C.Meta (i, l) -> res, lifted_term
891 (* C.Implicit None, ugraph *)
892 CicTypeChecker.type_of_aux' metasenv context term ugraph
894 let candidates = get_candidates Unification table term in
895 (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
897 if subterms_only then
901 metasenv context ugraph lift_amount term termty candidates
908 returns a list of new clauses inferred with a right superposition step
909 between the positive equation "target" and one in the "table" "newmeta" is
910 the first free meta index, i.e. the first number above the highest meta
911 index: its updated value is also returned
913 let superposition_right bag
914 ?(subterms_only=false) eq_uri (metasenv, context, ugraph) table target=
915 let module C = Cic in
916 let module S = CicSubstitution in
917 let module M = CicMetaSubst in
918 let module HL = HelmLibraryObjects in
919 let module CR = CicReduction in
920 let module U = Utils in
921 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
922 Equality.open_equality target
924 if Utils.debug_metas then
925 ignore (check_target bag context target "superpositionright");
926 let metasenv' = newmetas in
930 fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
932 [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
936 (fun (_, subst, _, _, _) ->
937 let subst = apply_subst subst in
938 let o = !Utils.compare_terms (subst l) (subst r) in
939 o <> U.Lt && o <> U.Le)
940 (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
942 (res left right), (res right left)
944 let build_new bag ordering (bo, s, m, ug, eq_found) =
945 if Utils.debug_metas then
946 ignore (check_target bag context (snd eq_found) "buildnew1" );
948 let pos, equality = eq_found in
949 let (_, proof', (ty, what, other, _), menv',id') =
950 Equality.open_equality equality in
951 let what, other = if pos = Utils.Left then what, other else other, what in
953 let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
954 let newgoal, newproof =
957 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
959 let name = C.Name "x" in
962 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
963 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
967 (s,(Equality.SuperpositionRight,
968 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
970 let bag, newequality =
972 if ordering = U.Gt then newgoal, apply_subst s right
973 else apply_subst s left, newgoal in
974 let neworder = !Utils.compare_terms left right in
975 let newmenv = (* Founif.filter s *) m in
976 let stat = (eq_ty, left, right, neworder) in
978 let w = Utils.compute_equality_weight stat in
979 Equality.mk_equality bag (w, newproof, stat, newmenv) in
980 if Utils.debug_metas then
981 ignore (check_target bag context eq' "buildnew3");
982 let bag, eq' = Equality.fix_metas bag eq' in
983 if Utils.debug_metas then
984 ignore (check_target bag context eq' "buildnew4");
987 if Utils.debug_metas then
988 ignore(check_target bag context newequality "buildnew2");
994 let bag, e = build_new bag U.Gt x in
995 bag, e::acc) res1 (bag,[])
1000 let bag, e = build_new bag U.Lt x in
1001 bag, e::acc) res2 (bag,[])
1003 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1004 bag, List.filter ok (new1 @ new2)
1007 (** demodulation, when the target is a theorem *)
1008 let rec demodulation_theorem bag env table theorem =
1009 let module C = Cic in
1010 let module S = CicSubstitution in
1011 let module M = CicMetaSubst in
1012 let module HL = HelmLibraryObjects in
1014 match LibraryObjects.eq_URI() with
1016 | None -> assert false in
1017 let metasenv, context, ugraph = env in
1018 let proof, theo, metas = theorem in
1019 let build_newtheorem (t, subst, menv, ug, eq_found) =
1020 let pos, equality = eq_found in
1021 let (_, proof', (ty, what, other, _), menv',id) =
1022 Equality.open_equality equality in
1025 | Equality.Exact p -> p
1026 | _ -> assert false in
1028 if pos = Utils.Left then what, other else other, what in
1029 let newtheo = apply_subst subst (S.subst other t) in
1030 let name = C.Name "x" in
1031 let body = apply_subst subst t in
1032 let pred = C.Lambda(name,ty,body) in
1036 Equality.mk_eq_ind eq_uri ty what pred proof other peq
1038 Equality.mk_eq_ind eq_uri ty what pred proof other peq
1042 let res = demodulation_aux bag metas context ugraph table 0 theo in
1045 let newproof, newtheo = build_newtheorem t in
1046 if Equality.meta_convertibility theo newtheo then
1049 demodulation_theorem bag env table (newproof,newtheo,[])
1054 (*****************************************************************************)
1055 (** OPERATIONS ON GOALS **)
1057 (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
1058 (*****************************************************************************)
1060 (* new: demodulation of non_equality terms *)
1061 let build_newg bag context goal rule expansion =
1062 let goalproof,_,_ = goal in
1063 let (t,subst,menv,ug,eq_found) = expansion in
1064 let pos, equality = eq_found in
1065 let (_, proof', (ty, what, other, _), menv',id) =
1066 Equality.open_equality equality in
1067 let what, other = if pos = Utils.Left then what, other else other, what in
1068 let newterm, newgoalproof =
1070 Utils.guarded_simpl context
1071 (apply_subst subst (CicSubstitution.subst other t))
1073 let name = Cic.Name "x" in
1074 let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1075 let newgoalproofstep = (rule,pos,id,subst,pred) in
1076 bo, (newgoalproofstep::goalproof)
1078 let newmetasenv = (* Founif.filter subst *) menv in
1079 (newgoalproof, newmetasenv, newterm)
1082 let rec demod bag env table goal =
1083 let _,menv,t = goal in
1084 let _, context, ugraph = env in
1085 let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in
1089 build_newg bag context goal Equality.Demodulation newt
1091 let _,_,newt = newg in
1092 if Equality.meta_convertibility t newt then
1095 true, snd (demod bag env table newg)
1102 | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
1103 (* assert (LibraryObjects.is_eq_URI uri); *)
1104 proof,menv,eq,ty,l,r
1107 let ty_of_goal (_,_,ty) = ty ;;
1109 (* checks if two goals are metaconvertible *)
1110 let goal_metaconvertibility_eq g1 g2 =
1111 Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
1114 (* when the betaexpand_term function is called on the left/right side of the
1115 * goal, the predicate has to be fixed
1116 * C[x] ---> (eq ty unchanged C[x])
1117 * [posu] is the side of the [unchanged] term in the original goal
1120 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1121 let _,_,eq,ty,l,r = open_goal goal in
1122 let unchanged = if posu = Utils.Left then l else r in
1123 let unchanged = CicSubstitution.lift 1 unchanged in
1124 let ty = CicSubstitution.lift 1 ty in
1127 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1128 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1130 (pred, subst, menv, ug, eq_f)
1133 (* ginve the old [goal], the side that has not changed [posu] and the
1134 * expansion builds a new goal *)
1135 let build_newgoal bag context goal posu rule expansion =
1136 let goalproof,_,_,_,_,_ = open_goal goal in
1137 let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
1138 let pos, equality = eq_found in
1139 let (_, proof', (ty, what, other, _), menv',id) =
1140 Equality.open_equality equality in
1141 let what, other = if pos = Utils.Left then what, other else other, what in
1142 let newterm, newgoalproof =
1144 Utils.guarded_simpl context
1145 (apply_subst subst (CicSubstitution.subst other t))
1147 let name = Cic.Name "x" in
1148 let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1149 let newgoalproofstep = (rule,pos,id,subst,pred) in
1150 bo, (newgoalproofstep::goalproof)
1152 let newmetasenv = (* Founif.filter subst *) menv in
1153 (newgoalproof, newmetasenv, newterm)
1158 returns a list of new clauses inferred with a left superposition step
1159 the negative equation "target" and one of the positive equations in "table"
1161 let superposition_left bag (metasenv, context, ugraph) table goal =
1162 let names = Utils.names_of_context context in
1163 let proof,menv,eq,ty,l,r = open_goal goal in
1164 let c = !Utils.compare_terms l r in
1166 if c = Utils.Incomparable then
1168 let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1169 let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1170 (* prerr_endline "incomparable";
1171 prerr_endline (string_of_int (List.length expansionsl));
1172 prerr_endline (string_of_int (List.length expansionsr));
1174 List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1176 List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1181 let big,small,possmall = l,r,Utils.Right in
1182 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1184 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1186 | Utils.Lt -> (* prerr_endline "LT"; *)
1187 let big,small,possmall = r,l,Utils.Left in
1188 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1190 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1195 ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1198 (* rinfresco le meta *)
1201 let b,g = Equality.fix_metas_goal b g in
1206 (** demodulation, when the target is a goal *)
1207 let rec demodulation_goal bag env table goal =
1208 let goalproof,menv,_,_,left,right = open_goal goal in
1209 let _, context, ugraph = env in
1210 (* let term = Utils.guarded_simpl (~debug:true) context term in*)
1212 let resright = demodulation_aux bag menv context ugraph table 0 right in
1216 build_newgoal bag context goal Utils.Left Equality.Demodulation t
1218 if goal_metaconvertibility_eq goal newg then
1221 true, snd (demodulation_goal bag env table newg)
1222 | None -> false, goal
1224 let resleft = demodulation_aux bag menv context ugraph table 0 left in
1227 let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
1228 if goal_metaconvertibility_eq goal newg then
1231 true, snd (demodulation_goal bag env table newg)
1232 | None -> do_right ()
1235 (* returns all the 1 step demodulations *)
1237 module S = CicSubstitution;;
1238 let rec demodulation_all_aux
1239 metasenv context ugraph table lift_amount term
1242 get_candidates ~env:(metasenv,context,ugraph) Matching table term
1247 let termty, ugraph = C.Implicit None, ugraph in
1250 ~unif_fun:Founif.matching
1251 metasenv context ugraph lift_amount term termty candidates
1260 (fun (rel, s, m, ug, c) ->
1261 (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
1262 (demodulation_all_aux
1263 metasenv context ugraph table lift_amount t),
1264 l@[List.hd r], List.tl r)
1265 (res, [], List.map (S.lift 1) l) l
1271 let demod_all steps bag env table goal =
1272 let _, context, ugraph = env in
1273 let is_visited l (_,_,t) =
1274 List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l
1276 let rec aux steps visited bag = function
1277 | _ when steps = 0 -> visited, bag, []
1278 | [] -> visited, bag, []
1279 | goal :: rest when is_visited visited goal -> aux steps visited bag rest
1281 let visited = goal :: visited in
1282 let _,menv,t = goal in
1283 let res = demodulation_all_aux menv context ugraph table 0 t in
1284 let steps = if res = [] then steps-1 else steps in
1286 List.map (build_newg bag context goal Equality.Demodulation) res
1288 (* we need this cause an equation E like
1290 can add a meta for y in a goal without instantiating it
1291 P (F true) ----> P (F ?y)
1292 and this may cause duplicated in metasenvs
1293 demodulating again with E
1295 let bag, new_goals =
1298 let bag, g = Equality.fix_metas_goal bag g in
1302 let visited, bag, res = aux steps visited bag (new_goals @ rest) in
1303 visited, bag, goal :: res
1305 aux steps [] bag [goal]
1309 let solve_demodulating bag env table initgoal steps =
1310 let proof,menv,eq,ty,left,right = open_goal initgoal in
1313 | Cic.MutInd (u,_,_) -> u
1316 let _, context, ugraph = env in
1317 let v1, bag, l_demod = demod_all steps bag env table ([],menv,left) in
1318 let v2, bag, r_demod = demod_all steps bag env table ([],menv,right) in
1319 let is_solved left right ml mr =
1320 let m = ml @ (List.filter
1321 (fun (x,_,_) -> not (List.exists (fun (y,_,_) -> x=y)ml)) mr)
1325 Founif.unification [] m context left right CicUniv.empty_ugraph in
1326 Some (bag, m,s,Equality.Exact (Equality.refl_proof uri ty left))
1327 with CicUnification.UnificationFailure _ ->
1329 unification_all env table (Equality.mk_tmp_equality
1330 (0,(Cic.Implicit None,left,right,Utils.Incomparable),m))
1332 if solutions = [] then None
1334 let s, e, swapped = List.hd solutions in
1335 let _,p,(ty,l,r,_),me,id = Equality.open_equality e in
1337 if swapped then Equality.symmetric bag ty l id uri me else bag, p
1342 HExtlib.list_findopt
1345 let pl,ml,l,bag,m,s,p =
1347 HExtlib.list_findopt (fun (pl,ml,l) _ ->
1348 match is_solved l r ml mr with
1350 | Some (bag,m,s,p) -> Some (pl,ml,l,bag,m,s,p)
1352 with Some x -> x | _ -> raise Not_found
1356 (fun (rule,pos,id,subst,pred) ->
1359 | Cic.Lambda (name,src,tgt) ->
1360 Cic.Lambda (name,src,
1361 Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
1364 rule,pos,id,subst,pred)
1369 (fun (rule,pos,id,subst,pred) ->
1372 | Cic.Lambda (name,src,tgt) ->
1373 Cic.Lambda (name,src,
1374 Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
1377 rule,pos,id,subst,pred)
1380 Some (bag,pr@pl@proof,m,s,p)
1381 with Not_found -> None)