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.oblivion_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 if Utils.debug_metas then
317 check_metasenv "founif :" metasenv';
318 Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
321 if pos = Utils.Left then left, right
324 if o <> U.Incomparable then
328 with Founif.MatchingFailure ->
329 find_matches bag metasenv context ugraph lift_amount term termty tl
331 if Utils.debug_res then ignore (check_res res "find1");
336 with Founif.MatchingFailure -> None
338 if Utils.debug_res then ignore (check_res res "find2");
340 | Some (_, s, _, _, _) ->
341 let c' = apply_subst s c in
343 let other' = U.guarded_simpl context (apply_subst s other) in *)
344 let other' = apply_subst s other in
345 let order = cmp c' other' in
350 metasenv context ugraph lift_amount term termty tl
352 find_matches bag metasenv context ugraph lift_amount term termty tl
355 let find_matches metasenv context ugraph lift_amount term termty =
356 find_matches metasenv context ugraph lift_amount term termty
360 as above, but finds all the matching equalities, and the matching condition
361 can be either Founif.matching or Inference.unification
363 (* XXX termty unused *)
364 let rec find_all_matches ?(unif_fun=Founif.unification) ?(demod=false)
365 metasenv context ugraph lift_amount term termty =
366 let module C = Cic in
367 let module U = Utils in
368 let module S = CicSubstitution in
369 let module M = CicMetaSubst in
370 let module HL = HelmLibraryObjects in
371 (* prerr_endline ("matching " ^ CicPp.ppterm term); *)
373 let r = !Utils.compare_terms x y in
376 CicPp.ppterm x ^ " " ^
377 Utils.string_of_comparison r ^ " " ^
382 let check = match termty with C.Implicit None -> false | _ -> true in
386 let pos, equality = candidate in
387 let (_,_,(ty,left,right,o),metas,_)= Equality.open_equality equality in
388 if check && not (fst (CicReduction.are_convertible
389 ~metasenv context termty ty ugraph)) then (
390 find_all_matches metasenv context ugraph lift_amount term termty tl
393 let subst', metasenv', ugraph' =
394 unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
396 (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
400 if pos = Utils.Left then left, right
403 if o <> U.Incomparable then
405 let res = do_match c in
406 res::(find_all_matches ~unif_fun metasenv context ugraph
407 lift_amount term termty tl)
409 | Founif.MatchingFailure
410 | CicUnification.UnificationFailure _
411 | CicUnification.Uncertain _ ->
412 find_all_matches ~unif_fun metasenv context ugraph
413 lift_amount term termty tl
416 let res = do_match c in
419 let c' = apply_subst s c
420 and other' = apply_subst s other in
421 let order = cmp c' other' in
422 if (demod && order = U.Gt) ||
423 (not demod && (order <> U.Lt && order <> U.Le))
425 res::(find_all_matches ~unif_fun metasenv context ugraph
426 lift_amount term termty tl)
428 find_all_matches ~unif_fun metasenv context ugraph
429 lift_amount term termty tl
431 | Founif.MatchingFailure
432 | CicUnification.UnificationFailure _
433 | CicUnification.Uncertain _ ->
434 find_all_matches ~unif_fun metasenv context ugraph
435 lift_amount term termty tl
439 ?unif_fun ?demod metasenv context ugraph lift_amount term termty l
442 ?unif_fun ?demod metasenv context ugraph lift_amount term termty l
443 (*prerr_endline "CANDIDATES:";
444 List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
445 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
449 returns true if target is subsumed by some equality in table
453 prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
454 ((pos,equation),_)) -> Equality.string_of_equality equation)l))
458 let subsumption_aux use_unification env table target =
459 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
460 let _, context, ugraph = env in
461 let metasenv = tmetas in
462 let predicate, unif_fun =
463 if use_unification then
464 Unification, Founif.unification
466 Matching, Founif.matching
470 | Cic.Meta _ when not use_unification -> []
472 let leftc = get_candidates predicate table left in
473 find_all_matches ~unif_fun
474 metasenv context ugraph 0 left ty leftc
476 let rec ok what leftorright = function
478 | (_, subst, menv, ug, (pos,equation))::tl ->
479 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
481 let other = if pos = Utils.Left then r else l in
482 let what' = Subst.apply_subst subst what in
483 let other' = Subst.apply_subst subst other in
484 let subst', menv', ug' =
485 unif_fun metasenv m context what' other' ugraph
487 (match Subst.merge_subst_if_possible subst subst' with
488 | None -> ok what leftorright tl
489 | Some s -> Some (s, equation, leftorright <> pos ))
491 | Founif.MatchingFailure
492 | CicUnification.UnificationFailure _ -> ok what leftorright tl
494 match ok right Utils.Left leftr with
495 | Some _ as res -> res
499 | Cic.Meta _ when not use_unification -> []
501 let rightc = get_candidates predicate table right in
502 find_all_matches ~unif_fun
503 metasenv context ugraph 0 right ty rightc
505 ok left Utils.Right rightr
508 let subsumption x y z =
509 subsumption_aux false x y z
512 let unification x y z =
513 subsumption_aux true x y z
516 (* the target must be disjoint from the equations in the table *)
517 let subsumption_aux_all use_unification env table target =
518 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
519 let _, context, ugraph = env in
520 let metasenv = tmetas in
521 if Utils.debug_metas then
522 check_for_duplicates metasenv "subsumption_aux_all";
523 let predicate, unif_fun =
524 if use_unification then
525 Unification, Founif.unification
527 Matching, Founif.matching
531 | Cic.Meta _ (*when not use_unification*) -> []
533 let leftc = get_candidates predicate table left in
534 find_all_matches ~unif_fun
535 metasenv context ugraph 0 left ty leftc
539 | Cic.Meta _ (*when not use_unification*) -> []
541 let rightc = get_candidates predicate table right in
542 find_all_matches ~unif_fun
543 metasenv context ugraph 0 right ty rightc
545 let rec ok_all what leftorright = function
547 | (_, subst, menv, ug, (pos,equation))::tl ->
548 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
550 let other = if pos = Utils.Left then r else l in
551 let what' = Subst.apply_subst subst what in
552 let other' = Subst.apply_subst subst other in
553 let subst', menv', ug' =
554 unif_fun [] menv context what' other' ugraph
556 (match Subst.merge_subst_if_possible subst subst' with
557 | None -> ok_all what leftorright tl
559 (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
561 | Founif.MatchingFailure
562 | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
564 (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
567 let subsumption_all x y z =
568 subsumption_aux_all false x y z
571 let unification_all x y z =
572 subsumption_aux_all true x y z
575 let rec demodulation_aux bag ?from ?(typecheck=false)
576 metasenv context ugraph table lift_amount term =
577 let module C = Cic in
578 let module S = CicSubstitution in
579 let module M = CicMetaSubst in
580 let module HL = HelmLibraryObjects in
581 if Utils.debug_metas then
582 check_for_duplicates metasenv "in input a demodulation aux";
585 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
587 (* let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates in *)
596 CicTypeChecker.type_of_aux' metasenv context term ugraph
598 C.Implicit None, ugraph
600 find_matches bag metasenv context ugraph
601 lift_amount term termty candidates
603 prerr_endline "type checking error";
604 prerr_endline ("menv :\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
605 prerr_endline ("term: " ^ (CicPp.ppterm term));
610 (if Utils.debug_res then
611 ignore(check_res res "demod1");
612 if check_demod_res res metasenv "demod" then res else None) in
622 (res, tl @ [S.lift 1 t])
625 demodulation_aux bag ~from:"1" metasenv context ugraph table ~typecheck
629 | None -> (None, tl @ [S.lift 1 t])
630 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
635 | Some (_, subst, menv, ug, eq_found) ->
636 Some (C.Appl ll, subst, menv, ug, eq_found)
639 | C.Prod (nn, s, t) ->
641 demodulation_aux bag ~from:"2"
642 metasenv context ugraph table lift_amount s in (
646 demodulation_aux bag metasenv
647 ((Some (nn, C.Decl s))::context) ugraph
648 table (lift_amount+1) t
652 | Some (t', subst, menv, ug, eq_found) ->
653 Some (C.Prod (nn, (S.lift 1 s), t'),
654 subst, menv, ug, eq_found)
656 | Some (s', subst, menv, ug, eq_found) ->
657 Some (C.Prod (nn, s', (S.lift 1 t)),
658 subst, menv, ug, eq_found)
660 | C.Lambda (nn, s, t) ->
661 prerr_endline "siam qui";
664 metasenv context ugraph table lift_amount s in (
668 demodulation_aux bag metasenv
669 ((Some (nn, C.Decl s))::context) ugraph
670 table (lift_amount+1) t
674 | Some (t', subst, menv, ug, eq_found) ->
675 Some (C.Lambda (nn, (S.lift 1 s), t'),
676 subst, menv, ug, eq_found)
678 | Some (s', subst, menv, ug, eq_found) ->
679 Some (C.Lambda (nn, s', (S.lift 1 t)),
680 subst, menv, ug, eq_found)
686 if Utils.debug_res then ignore(check_res res "demod_aux output");
692 (** demodulation, when target is an equality *)
693 let rec demodulation_equality bag ?from eq_uri env table target =
694 let module C = Cic in
695 let module S = CicSubstitution in
696 let module M = CicMetaSubst in
697 let module HL = HelmLibraryObjects in
698 let module U = Utils in
699 let metasenv, context, ugraph = env in
700 let w, proof, (eq_ty, left, right, order), metas, id =
701 Equality.open_equality target
703 (* first, we simplify *)
704 (* let right = U.guarded_simpl context right in *)
705 (* let left = U.guarded_simpl context left in *)
706 (* let order = !Utils.compare_terms left right in *)
707 (* let stat = (eq_ty, left, right, order) in *)
708 (* let w = Utils.compute_equality_weight stat in*)
709 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
710 if Utils.debug_metas then
711 ignore(check_target bag context target "demod equalities input");
712 let metasenv' = (* metasenv @ *) metas in
714 let build_newtarget bag is_left (t, subst, menv, ug, eq_found) =
716 if Utils.debug_metas then
718 ignore(check_for_duplicates menv "input1");
719 ignore(check_disjoint_invariant subst menv "input2");
720 let substs = Subst.ppsubst subst in
721 ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
723 let pos, equality = eq_found in
725 (ty, what, other, _), menv',id') = Equality.open_equality equality in
728 try fst (CicTypeChecker.type_of_aux' menv' context what ugraph)
729 with CicUtil.Meta_not_found _ -> ty
731 let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
732 let what, other = if pos = Utils.Left then what, other else other, what in
733 let newterm, newproof =
735 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
736 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
737 let name = C.Name "x" in
739 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
740 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
742 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
743 (Cic.Lambda (name, ty, bo'))))))
745 let newmenv = menv in
746 let left, right = if is_left then newterm, right else left, newterm in
747 let ordering = !Utils.compare_terms left right in
748 let stat = (eq_ty, left, right, ordering) in
750 let w = Utils.compute_equality_weight stat in
751 Equality.mk_equality bag (w, newproof, stat,newmenv)
753 if Utils.debug_metas then
754 ignore(check_target bag context res "buildnew_target output");
758 demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left
760 if Utils.debug_res then check_res res "demod result";
764 let bag, newtarget = build_newtarget bag true t in
765 (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
766 if (Equality.is_weak_identity newtarget) (* || *)
767 (*Equality.meta_convertibility_eq target newtarget*) then
770 demodulation_equality bag ?from eq_uri env table newtarget
772 let res = demodulation_aux bag metasenv' context ugraph table 0 right in
773 if Utils.debug_res then check_res res "demod result 1";
776 let bag, newtarget = build_newtarget bag false t in
777 if (Equality.is_weak_identity newtarget) ||
778 (Equality.meta_convertibility_eq target newtarget) then
781 demodulation_equality bag ?from eq_uri env table newtarget
785 (* newmeta, newtarget *)
790 Performs the beta expansion of the term "term" w.r.t. "table",
791 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
794 let rec betaexpand_term
795 ?(subterms_only=false) metasenv context ugraph table lift_amount term
797 let module C = Cic in
798 let module S = CicSubstitution in
799 let module M = CicMetaSubst in
800 let module HL = HelmLibraryObjects in
802 let res, lifted_term =
808 (fun arg (res, lifted_tl) ->
811 let arg_res, lifted_arg =
812 betaexpand_term metasenv context ugraph table
816 (fun (t, s, m, ug, eq_found) ->
817 (Some t)::lifted_tl, s, m, ug, eq_found)
822 (fun (l, s, m, ug, eq_found) ->
823 (Some lifted_arg)::l, s, m, ug, eq_found)
825 (Some lifted_arg)::lifted_tl)
828 (fun (r, s, m, ug, eq_found) ->
829 None::r, s, m, ug, eq_found) res,
835 (fun (l, s, m, ug, eq_found) ->
836 (C.Meta (i, l), s, m, ug, eq_found)) l'
838 e, C.Meta (i, lifted_l)
841 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
843 | C.Prod (nn, s, t) ->
845 betaexpand_term metasenv context ugraph table lift_amount s in
847 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
848 table (lift_amount+1) t in
851 (fun (t, s, m, ug, eq_found) ->
852 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
855 (fun (t, s, m, ug, eq_found) ->
856 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
857 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
859 | C.Lambda (nn, s, t) ->
861 betaexpand_term metasenv context ugraph table lift_amount s in
863 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
864 table (lift_amount+1) t in
867 (fun (t, s, m, ug, eq_found) ->
868 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
871 (fun (t, s, m, ug, eq_found) ->
872 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
873 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
878 (fun (res, lifted_tl) arg ->
879 let arg_res, lifted_arg =
880 betaexpand_term metasenv context ugraph table lift_amount arg
884 (fun (a, s, m, ug, eq_found) ->
885 a::lifted_tl, s, m, ug, eq_found)
890 (fun (r, s, m, ug, eq_found) ->
891 lifted_arg::r, s, m, ug, eq_found)
893 lifted_arg::lifted_tl)
894 ) ([], []) (List.rev l)
897 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
900 | t -> [], (S.lift lift_amount t)
903 | C.Meta (i, l) -> res, lifted_term
906 C.Implicit None, ugraph
907 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
909 let candidates = get_candidates Unification table term in
910 (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
912 if subterms_only then
916 metasenv context ugraph lift_amount term termty candidates
923 returns a list of new clauses inferred with a right superposition step
924 between the positive equation "target" and one in the "table" "newmeta" is
925 the first free meta index, i.e. the first number above the highest meta
926 index: its updated value is also returned
928 let superposition_right bag
929 ?(subterms_only=false) eq_uri (metasenv, context, ugraph) table target=
930 let module C = Cic in
931 let module S = CicSubstitution in
932 let module M = CicMetaSubst in
933 let module HL = HelmLibraryObjects in
934 let module CR = CicReduction in
935 let module U = Utils in
936 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
937 Equality.open_equality target
939 if Utils.debug_metas then
940 ignore (check_target bag context target "superpositionright");
941 let metasenv' = newmetas in
945 fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
947 [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
951 (fun (_, subst, _, _, _) ->
952 let subst = apply_subst subst in
953 let o = !Utils.compare_terms (subst l) (subst r) in
954 o <> U.Lt && o <> U.Le)
955 (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
957 (res left right), (res right left)
959 let build_new bag ordering (bo, s, m, ug, eq_found) =
960 if Utils.debug_metas then
961 ignore (check_target bag context (snd eq_found) "buildnew1" );
963 let pos, equality = eq_found in
964 let (_, proof', (ty, what, other, _), menv',id') =
965 Equality.open_equality equality in
966 let what, other = if pos = Utils.Left then what, other else other, what in
968 let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
969 let newgoal, newproof =
972 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
974 let name = C.Name "x" in
977 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
978 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
982 (s,(Equality.SuperpositionRight,
983 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
985 let bag, newequality =
987 if ordering = U.Gt then newgoal, apply_subst s right
988 else apply_subst s left, newgoal in
989 let neworder = !Utils.compare_terms left right in
990 let newmenv = (* Founif.filter s *) m in
991 let stat = (eq_ty, left, right, neworder) in
993 let w = Utils.compute_equality_weight stat in
994 Equality.mk_equality bag (w, newproof, stat, newmenv) in
995 if Utils.debug_metas then
996 ignore (check_target bag context eq' "buildnew3");
997 let bag, eq' = Equality.fix_metas bag eq' in
998 if Utils.debug_metas then
999 ignore (check_target bag context eq' "buildnew4");
1002 if Utils.debug_metas then
1003 ignore(check_target bag context newequality "buildnew2");
1009 let bag, e = build_new bag U.Gt x in
1010 bag, e::acc) res1 (bag,[])
1015 let bag, e = build_new bag U.Lt x in
1016 bag, e::acc) res2 (bag,[])
1018 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1019 bag, List.filter ok (new1 @ new2)
1022 (** demodulation, when the target is a theorem *)
1023 let rec demodulation_theorem bag env table theorem =
1024 let module C = Cic in
1025 let module S = CicSubstitution in
1026 let module M = CicMetaSubst in
1027 let module HL = HelmLibraryObjects in
1029 match LibraryObjects.eq_URI() with
1031 | None -> assert false in
1032 let metasenv, context, ugraph = env in
1033 let proof, theo, metas = theorem in
1034 let build_newtheorem (t, subst, menv, ug, eq_found) =
1035 let pos, equality = eq_found in
1036 let (_, proof', (ty, what, other, _), menv',id) =
1037 Equality.open_equality equality in
1040 | Equality.Exact p -> p
1041 | _ -> assert false in
1043 if pos = Utils.Left then what, other else other, what in
1044 let newtheo = apply_subst subst (S.subst other t) in
1045 let name = C.Name "x" in
1046 let body = apply_subst subst t in
1047 let pred = C.Lambda(name,ty,body) in
1051 Equality.mk_eq_ind eq_uri ty what pred proof other peq
1053 Equality.mk_eq_ind eq_uri ty what pred proof other peq
1057 let res = demodulation_aux bag metas context ugraph table 0 theo in
1060 let newproof, newtheo = build_newtheorem t in
1061 if Equality.meta_convertibility theo newtheo then
1064 demodulation_theorem bag env table (newproof,newtheo,[])
1069 (*****************************************************************************)
1070 (** OPERATIONS ON GOALS **)
1072 (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
1073 (*****************************************************************************)
1075 (* new: demodulation of non_equality terms *)
1076 let build_newg bag context goal rule expansion =
1077 let goalproof,_,_ = goal in
1078 let (t,subst,menv,ug,eq_found) = expansion in
1079 let pos, equality = eq_found in
1080 let (_, proof', (ty, what, other, _), menv',id) =
1081 Equality.open_equality equality in
1082 let what, other = if pos = Utils.Left then what, other else other, what in
1083 let newterm, newgoalproof =
1085 Utils.guarded_simpl context
1086 (apply_subst subst (CicSubstitution.subst other t))
1088 let name = Cic.Name "x" in
1089 let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1090 let newgoalproofstep = (rule,pos,id,subst,pred) in
1091 bo, (newgoalproofstep::goalproof)
1093 let newmetasenv = (* Founif.filter subst *) menv in
1094 (newgoalproof, newmetasenv, newterm)
1097 let rec demod bag env table goal =
1098 let _,menv,t = goal in
1099 let _, context, ugraph = env in
1100 let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:false)in
1104 build_newg bag context goal Equality.Demodulation newt
1106 let _,_,newt = newg in
1107 if Equality.meta_convertibility t newt then
1110 true, snd (demod bag env table newg)
1117 | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
1118 (* assert (LibraryObjects.is_eq_URI uri); *)
1119 proof,menv,eq,ty,l,r
1122 let ty_of_goal (_,_,ty) = ty ;;
1124 (* checks if two goals are metaconvertible *)
1125 let goal_metaconvertibility_eq g1 g2 =
1126 Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
1129 (* when the betaexpand_term function is called on the left/right side of the
1130 * goal, the predicate has to be fixed
1131 * C[x] ---> (eq ty unchanged C[x])
1132 * [posu] is the side of the [unchanged] term in the original goal
1135 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1136 let _,_,eq,ty,l,r = open_goal goal in
1137 let unchanged = if posu = Utils.Left then l else r in
1138 let unchanged = CicSubstitution.lift 1 unchanged in
1139 let ty = CicSubstitution.lift 1 ty in
1142 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1143 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1145 (pred, subst, menv, ug, eq_f)
1148 (* ginve the old [goal], the side that has not changed [posu] and the
1149 * expansion builds a new goal *)
1150 let build_newgoal bag context goal posu rule expansion =
1151 let goalproof,_,_,_,_,_ = open_goal goal in
1152 let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
1153 let pos, equality = eq_found in
1154 let (_, proof', (ty, what, other, _), menv',id) =
1155 Equality.open_equality equality in
1156 let what, other = if pos = Utils.Left then what, other else other, what in
1157 let newterm, newgoalproof =
1159 Utils.guarded_simpl context
1160 (apply_subst subst (CicSubstitution.subst other t))
1162 let name = Cic.Name "x" in
1163 let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1164 let newgoalproofstep = (rule,pos,id,subst,pred) in
1165 bo, (newgoalproofstep::goalproof)
1167 let newmetasenv = (* Founif.filter subst *) menv in
1168 (newgoalproof, newmetasenv, newterm)
1173 returns a list of new clauses inferred with a left superposition step
1174 the negative equation "target" and one of the positive equations in "table"
1176 let superposition_left bag (metasenv, context, ugraph) table goal =
1177 let names = Utils.names_of_context context in
1178 let proof,menv,eq,ty,l,r = open_goal goal in
1179 let c = !Utils.compare_terms l r in
1181 if c = Utils.Incomparable then
1183 let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1184 let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1185 (* prerr_endline "incomparable";
1186 prerr_endline (string_of_int (List.length expansionsl));
1187 prerr_endline (string_of_int (List.length expansionsr));
1189 List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1191 List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1196 let big,small,possmall = l,r,Utils.Right in
1197 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1199 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1201 | Utils.Lt -> (* prerr_endline "LT"; *)
1202 let big,small,possmall = r,l,Utils.Left in
1203 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1205 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1210 ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1213 (* rinfresco le meta *)
1216 let b,g = Equality.fix_metas_goal b g in
1221 (** demodulation, when the target is a goal *)
1222 let rec demodulation_goal bag env table goal =
1223 let goalproof,menv,_,_,left,right = open_goal goal in
1224 let _, context, ugraph = env in
1225 (* let term = Utils.guarded_simpl (~debug:true) context term in*)
1227 let resright = demodulation_aux bag menv context ugraph table 0 right in
1231 build_newgoal bag context goal Utils.Left Equality.Demodulation t
1233 if goal_metaconvertibility_eq goal newg then
1236 true, snd (demodulation_goal bag env table newg)
1237 | None -> false, goal
1239 let resleft = demodulation_aux bag menv context ugraph table 0 left in
1242 let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
1243 if goal_metaconvertibility_eq goal newg then
1246 true, snd (demodulation_goal bag env table newg)
1247 | None -> do_right ()
1250 (* returns all the 1 step demodulations *)
1252 module S = CicSubstitution;;
1254 let rec demodulation_all_aux
1255 metasenv context ugraph table lift_amount term
1258 get_candidates ~env:(metasenv,context,ugraph) Matching table term
1263 let termty, ugraph = C.Implicit None, ugraph in
1266 ~unif_fun:Founif.matching ~demod:true
1267 metasenv context ugraph lift_amount term termty candidates
1273 (fun (res,b,l,r) t ->
1274 if not b then res,b,l,r
1277 demodulation_all_aux
1278 metasenv context ugraph table lift_amount t
1280 let b = demods_for_t = [] in
1283 (fun (rel, s, m, ug, c) ->
1284 (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
1285 demods_for_t, b, l@[List.hd r], List.tl r)
1286 (res, true, [], List.map (S.lift 1) l) l
1292 let demod_all steps bag env table goal =
1293 let _, context, ugraph = env in
1294 let is_visited l (_,_,t) =
1295 List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l
1297 let rec aux steps visited nf bag = function
1298 | _ when steps = 0 -> visited, bag, nf
1299 | [] -> visited, bag, nf
1300 | goal :: rest when is_visited visited goal-> aux steps visited nf bag rest
1302 let visited = goal :: visited in
1303 let _,menv,t = goal in
1304 let res = demodulation_all_aux menv context ugraph table 0 t in
1305 let steps = if res = [] then steps-1 else steps in
1307 List.map (build_newg bag context goal Equality.Demodulation) res
1309 let nf = if new_goals = [] then goal :: nf else nf in
1310 aux steps visited nf bag (new_goals @ rest)
1312 aux steps [] [] bag [goal]
1315 let combine_demodulation_proofs bag env goal (pl,ml,l) (pr,mr,r) =
1316 let proof,m,eq,ty,left,right = open_goal goal in
1319 (fun (rule,pos,id,subst,pred) ->
1322 | Cic.Lambda (name,src,tgt) ->
1323 Cic.Lambda (name,src,
1324 Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
1327 rule,pos,id,subst,pred)
1332 (fun (rule,pos,id,subst,pred) ->
1335 | Cic.Lambda (name,src,tgt) ->
1336 Cic.Lambda (name,src,
1337 Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
1340 rule,pos,id,subst,pred)
1343 (pr@pl@proof, m, Cic.Appl [eq;ty;l;r])
1346 let demodulation_all_goal bag env table goal maxnf =
1347 let proof,menv,eq,ty,left,right = open_goal goal in
1348 let v1, bag, l_demod = demod_all maxnf bag env table ([],menv,left) in
1349 let v2, bag, r_demod = demod_all maxnf bag env table ([],menv,right) in
1350 let l_demod = if l_demod = [] then [ [], menv, left ] else l_demod in
1351 let r_demod = if r_demod = [] then [ [], menv, right ] else r_demod in
1353 (fun acc (_,_,l as ld) ->
1355 (fun acc (_,_,r as rd) ->
1356 combine_demodulation_proofs bag env goal ld rd :: acc)
1361 let solve_demodulating bag env table initgoal steps =
1362 let proof,menv,eq,ty,left,right = open_goal initgoal in
1365 | Cic.MutInd (u,_,_) -> u
1368 let _, context, ugraph = env in
1369 let v1, bag, l_demod = demod_all steps bag env table ([],menv,left) in
1370 let v2, bag, r_demod = demod_all steps bag env table ([],menv,right) in
1371 let is_solved left right ml mr =
1372 let m = ml @ (List.filter
1373 (fun (x,_,_) -> not (List.exists (fun (y,_,_) -> x=y)ml)) mr)
1377 Founif.unification [] m context left right CicUniv.empty_ugraph in
1378 Some (bag, m,s,Equality.Exact (Equality.refl_proof uri ty left))
1379 with CicUnification.UnificationFailure _ ->
1381 unification_all env table (Equality.mk_tmp_equality
1382 (0,(Cic.Implicit None,left,right,Utils.Incomparable),m))
1384 if solutions = [] then None
1386 let s, e, swapped = List.hd solutions in
1387 let _,p,(ty,l,r,_),me,id = Equality.open_equality e in
1389 if swapped then Equality.symmetric bag ty l id uri me else bag, p
1394 HExtlib.list_findopt
1397 let pl,ml,l,bag,m,s,p =
1399 HExtlib.list_findopt (fun (pl,ml,l) _ ->
1400 match is_solved l r ml mr with
1402 | Some (bag,m,s,p) -> Some (pl,ml,l,bag,m,s,p)
1404 with Some x -> x | _ -> raise Not_found
1408 (fun (rule,pos,id,subst,pred) ->
1411 | Cic.Lambda (name,src,tgt) ->
1412 Cic.Lambda (name,src,
1413 Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
1416 rule,pos,id,subst,pred)
1421 (fun (rule,pos,id,subst,pred) ->
1424 | Cic.Lambda (name,src,tgt) ->
1425 Cic.Lambda (name,src,
1426 Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
1429 rule,pos,id,subst,pred)
1432 Some (bag,pr@pl@proof,m,s,p)
1433 with Not_found -> None)