1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (* let _profiler = <:profiler<_profiler>>;; *)
30 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
32 module Index = Equality_indexing.DT (* path tree based indexing *)
35 let debug_print = Utils.debug_print;;
39 let check_equation env equation msg =
40 let w, proof, (eq_ty, left, right, order), metas, args = equation in
41 let metasenv, context, ugraph = env
42 let metasenv' = metasenv @ metas in
44 CicTypeChecker.type_of_aux' metasenv' context left ugraph;
45 CicTypeChecker.type_of_aux' metasenv' context right ugraph;
48 CicUtil.Meta_not_found _ as exn ->
51 prerr_endline (CicPp.ppterm left);
52 prerr_endline (CicPp.ppterm right);
57 type retrieval_mode = Matching | Unification;;
59 let string_of_res ?env =
62 | Some (t, s, m, u, (p,e)) ->
63 Printf.sprintf "Some: (%s, %s, %s)"
64 (Utils.string_of_pos p)
65 (Equality.string_of_equality ?env e)
69 let print_res ?env res =
72 (List.map (string_of_res ?env) res))
75 let print_candidates ?env mode term res =
79 prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
81 prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
87 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
88 (Equality.string_of_equality ?env e))
93 let apply_subst = Subst.apply_subst
95 let index = Index.index
96 let remove_index = Index.remove_index
97 let in_index = Index.in_index
98 let empty = Index.empty
99 let init_index = Index.init_index
101 let check_disjoint_invariant subst metasenv msg =
103 (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
106 prerr_endline ("not disjoint: " ^ msg);
111 let check_for_duplicates metas msg =
112 if List.length metas <>
113 List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
115 prerr_endline ("DUPLICATI " ^ msg);
116 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
121 let check_res res msg =
123 Some (t, subst, menv, ug, eq_found) ->
124 let eqs = Equality.string_of_equality (snd eq_found) in
125 check_disjoint_invariant subst menv msg;
126 check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
130 let check_target bag context target msg =
131 let w, proof, (eq_ty, left, right, order), metas,_ =
132 Equality.open_equality target in
133 (* check that metas does not contains duplicates *)
134 let eqs = Equality.string_of_equality target in
135 let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
136 let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
137 @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof bag proof) in
138 let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
139 let _ = if menv <> metas then
141 prerr_endline ("extra metas " ^ msg);
142 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
143 prerr_endline "**********************";
144 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
145 prerr_endline ("left: " ^ (CicPp.ppterm left));
146 prerr_endline ("right: " ^ (CicPp.ppterm right));
147 prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
153 ignore(CicTypeChecker.type_of_aux'
154 metas context (Founif.build_proof_term proof) CicUniv.empty_ugraph)
157 prerr_endline (Founif.string_of_proof proof);
158 prerr_endline (CicPp.ppterm (Founif.build_proof_term proof));
159 prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
160 prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
165 (* returns a list of all the equalities in the tree that are in relation
166 "mode" with the given term, where mode can be either Matching or
169 Format of the return value: list of tuples in the form:
170 (position - Left or Right - of the term that matched the given one in this
174 Note that if equality is "left = right", if the ordering is left > right,
175 the position will always be Left, and if the ordering is left < right,
176 position will be Right.
179 let get_candidates ?env mode tree term =
183 Index.retrieve_generalizations tree term
185 Index.retrieve_unifiables tree term
188 Index.PosEqSet.elements s
192 finds the first equality in the index that matches "term", of type "termty"
193 termty can be Implicit if it is not needed. The result (one of the sides of
194 the equality, actually) should be not greater (wrt the term ordering) than
197 Format of the return value:
199 (term to substitute, [Cic.Rel 1 properly lifted - see the various
200 build_newtarget functions inside the various
201 demodulation_* functions]
202 substitution used for the matching,
204 ugraph, [substitution, metasenv and ugraph have the same meaning as those
205 returned by CicUnification.fo_unif]
206 (equality where the matching term was found, [i.e. the equality to use as
208 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
209 the equality: this is used to build the proof term, again see one of
210 the build_newtarget functions]
213 let rec find_matches bag metasenv context ugraph lift_amount term termty =
214 let module C = Cic in
215 let module U = Utils in
216 let module S = CicSubstitution in
217 let module M = CicMetaSubst in
218 let module HL = HelmLibraryObjects in
219 let cmp = !Utils.compare_terms in
220 let check = match termty with C.Implicit None -> false | _ -> true in
224 let pos, equality = candidate in
225 let (_, proof, (ty, left, right, o), metas,_) =
226 Equality.open_equality equality
228 if Utils.debug_metas then
229 ignore(check_target bag context (snd candidate) "find_matches");
230 if Utils.debug_res then
232 let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
233 let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
234 let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
237 (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
240 check_for_duplicates metas "gia nella metas";
241 check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*))
243 if check && not (fst (CicReduction.are_convertible
244 ~metasenv context termty ty ugraph)) then (
245 find_matches bag metasenv context ugraph lift_amount term termty tl
248 let subst', metasenv', ugraph' =
250 metasenv metas context term (S.lift lift_amount c) ugraph
252 Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
255 if pos = Utils.Left then left, right
258 if o <> U.Incomparable then
262 with Founif.MatchingFailure ->
263 find_matches bag metasenv context ugraph lift_amount term termty tl
265 if Utils.debug_res then ignore (check_res res "find1");
270 with Founif.MatchingFailure -> None
272 if Utils.debug_res then ignore (check_res res "find2");
274 | Some (_, s, _, _, _) ->
275 let c' = apply_subst s c in
277 let other' = U.guarded_simpl context (apply_subst s other) in *)
278 let other' = apply_subst s other in
279 let order = cmp c' other' in
284 metasenv context ugraph lift_amount term termty tl
286 find_matches bag metasenv context ugraph lift_amount term termty tl
289 let find_matches metasenv context ugraph lift_amount term termty =
290 find_matches metasenv context ugraph lift_amount term termty
294 as above, but finds all the matching equalities, and the matching condition
295 can be either Founif.matching or Inference.unification
297 let rec find_all_matches ?(unif_fun=Founif.unification)
298 metasenv context ugraph lift_amount term termty =
299 let module C = Cic in
300 let module U = Utils in
301 let module S = CicSubstitution in
302 let module M = CicMetaSubst in
303 let module HL = HelmLibraryObjects in
304 let cmp = !Utils.compare_terms in
308 let pos, equality = candidate in
309 let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
311 let subst', metasenv', ugraph' =
312 unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
314 (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
317 if pos = Utils.Left then left, right
320 if o <> U.Incomparable then
322 let res = do_match c in
323 res::(find_all_matches ~unif_fun metasenv context ugraph
324 lift_amount term termty tl)
326 | Founif.MatchingFailure
327 | CicUnification.UnificationFailure _
328 | CicUnification.Uncertain _ ->
329 find_all_matches ~unif_fun metasenv context ugraph
330 lift_amount term termty tl
333 let res = do_match c in
336 let c' = apply_subst s c
337 and other' = apply_subst s other in
338 let order = cmp c' other' in
339 if order <> U.Lt && order <> U.Le then
340 res::(find_all_matches ~unif_fun metasenv context ugraph
341 lift_amount term termty tl)
343 find_all_matches ~unif_fun metasenv context ugraph
344 lift_amount term termty tl
346 | Founif.MatchingFailure
347 | CicUnification.UnificationFailure _
348 | CicUnification.Uncertain _ ->
349 find_all_matches ~unif_fun metasenv context ugraph
350 lift_amount term termty tl
354 ?unif_fun metasenv context ugraph lift_amount term termty l
357 ?unif_fun metasenv context ugraph lift_amount term termty l
358 (*prerr_endline "CANDIDATES:";
359 List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
360 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
364 returns true if target is subsumed by some equality in table
367 prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
368 ((pos,equation),_)) -> Equality.string_of_equality equation)l))
371 let subsumption_aux use_unification env table target =
372 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
373 let _, context, ugraph = env in
374 let metasenv = tmetas in
375 let predicate, unif_fun =
376 if use_unification then
377 Unification, Founif.unification
379 Matching, Founif.matching
383 | Cic.Meta _ when not use_unification -> []
385 let leftc = get_candidates predicate table left in
386 find_all_matches ~unif_fun
387 metasenv context ugraph 0 left ty leftc
389 let rec ok what leftorright = function
391 | (_, subst, menv, ug, (pos,equation))::tl ->
392 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
394 let other = if pos = Utils.Left then r else l in
395 let what' = Subst.apply_subst subst what in
396 let other' = Subst.apply_subst subst other in
397 let subst', menv', ug' =
398 unif_fun metasenv m context what' other' ugraph
400 (match Subst.merge_subst_if_possible subst subst' with
401 | None -> ok what leftorright tl
402 | Some s -> Some (s, equation, leftorright <> pos ))
404 | Founif.MatchingFailure
405 | CicUnification.UnificationFailure _ -> ok what leftorright tl
407 match ok right Utils.Left leftr with
408 | Some _ as res -> res
412 | Cic.Meta _ when not use_unification -> []
414 let rightc = get_candidates predicate table right in
415 find_all_matches ~unif_fun
416 metasenv context ugraph 0 right ty rightc
418 ok left Utils.Right rightr
421 let subsumption x y z =
422 subsumption_aux false x y z
425 let unification x y z =
426 subsumption_aux true x y z
429 let subsumption_aux_all use_unification env table target =
430 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
431 let _, context, ugraph = env in
432 let metasenv = tmetas in
433 let predicate, unif_fun =
434 if use_unification then
435 Unification, Founif.unification
437 Matching, Founif.matching
441 | Cic.Meta _ when not use_unification -> []
443 let leftc = get_candidates predicate table left in
444 find_all_matches ~unif_fun
445 metasenv context ugraph 0 left ty leftc
449 | Cic.Meta _ when not use_unification -> []
451 let rightc = get_candidates predicate table right in
452 find_all_matches ~unif_fun
453 metasenv context ugraph 0 right ty rightc
455 let rec ok_all what leftorright = function
457 | (_, subst, menv, ug, (pos,equation))::tl ->
458 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
460 let other = if pos = Utils.Left then r else l in
461 let what' = Subst.apply_subst subst what in
462 let other' = Subst.apply_subst subst other in
463 let subst', menv', ug' =
464 unif_fun metasenv m context what' other' ugraph
466 (match Subst.merge_subst_if_possible subst subst' with
467 | None -> ok_all what leftorright tl
469 (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
471 | Founif.MatchingFailure
472 | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
474 (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
477 let subsumption_all x y z =
478 subsumption_aux_all false x y z
481 let unification_all x y z =
482 subsumption_aux_all true x y z
484 let rec demodulation_aux bag ?from ?(typecheck=false)
485 metasenv context ugraph table lift_amount term =
486 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
487 let module C = Cic in
488 let module S = CicSubstitution in
489 let module M = CicMetaSubst in
490 let module HL = HelmLibraryObjects in
493 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
501 CicTypeChecker.type_of_aux' metasenv context term ugraph
503 C.Implicit None, ugraph
506 find_matches bag metasenv context ugraph lift_amount term termty candidates
508 if Utils.debug_res then ignore(check_res res "demod1");
518 (res, tl @ [S.lift 1 t])
521 demodulation_aux bag ~from:"1" metasenv context ugraph table
525 | None -> (None, tl @ [S.lift 1 t])
526 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
531 | Some (_, subst, menv, ug, eq_found) ->
532 Some (C.Appl ll, subst, menv, ug, eq_found)
534 | C.Prod (nn, s, t) ->
536 demodulation_aux bag ~from:"2"
537 metasenv context ugraph table lift_amount s in (
541 demodulation_aux bag metasenv
542 ((Some (nn, C.Decl s))::context) ugraph
543 table (lift_amount+1) t
547 | Some (t', subst, menv, ug, eq_found) ->
548 Some (C.Prod (nn, (S.lift 1 s), t'),
549 subst, menv, ug, eq_found)
551 | Some (s', subst, menv, ug, eq_found) ->
552 Some (C.Prod (nn, s', (S.lift 1 t)),
553 subst, menv, ug, eq_found)
555 | C.Lambda (nn, s, t) ->
558 metasenv context ugraph table lift_amount s in (
562 demodulation_aux bag metasenv
563 ((Some (nn, C.Decl s))::context) ugraph
564 table (lift_amount+1) t
568 | Some (t', subst, menv, ug, eq_found) ->
569 Some (C.Lambda (nn, (S.lift 1 s), t'),
570 subst, menv, ug, eq_found)
572 | Some (s', subst, menv, ug, eq_found) ->
573 Some (C.Lambda (nn, s', (S.lift 1 t)),
574 subst, menv, ug, eq_found)
579 if Utils.debug_res then ignore(check_res res "demod_aux output");
585 (** demodulation, when target is an equality *)
586 let rec demodulation_equality bag ?from eq_uri newmeta env table target =
587 let module C = Cic in
588 let module S = CicSubstitution in
589 let module M = CicMetaSubst in
590 let module HL = HelmLibraryObjects in
591 let module U = Utils in
592 let metasenv, context, ugraph = env in
593 let w, proof, (eq_ty, left, right, order), metas, id =
594 Equality.open_equality target
596 (* first, we simplify *)
597 (* let right = U.guarded_simpl context right in *)
598 (* let left = U.guarded_simpl context left in *)
599 (* let order = !Utils.compare_terms left right in *)
600 (* let stat = (eq_ty, left, right, order) in *)
601 (* let w = Utils.compute_equality_weight stat in*)
602 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
603 if Utils.debug_metas then
604 ignore(check_target bag context target "demod equalities input");
605 let metasenv' = (* metasenv @ *) metas in
606 let maxmeta = ref newmeta in
608 let build_newtarget is_left (t, subst, menv, ug, eq_found) =
610 if Utils.debug_metas then
612 ignore(check_for_duplicates menv "input1");
613 ignore(check_disjoint_invariant subst menv "input2");
614 let substs = Subst.ppsubst subst in
615 ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
617 let pos, equality = eq_found in
619 (ty, what, other, _), menv',id') = Equality.open_equality equality in
621 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
622 with CicUtil.Meta_not_found _ -> ty
624 let what, other = if pos = Utils.Left then what, other else other, what in
625 let newterm, newproof =
627 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
628 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
629 let name = C.Name "x" in
631 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
632 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
634 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
635 (Cic.Lambda (name, ty, bo'))))))
637 let newmenv = menv in
638 let left, right = if is_left then newterm, right else left, newterm in
639 let ordering = !Utils.compare_terms left right in
640 let stat = (eq_ty, left, right, ordering) in
642 let w = Utils.compute_equality_weight stat in
643 (Equality.mk_equality bag (w, newproof, stat,newmenv))
645 if Utils.debug_metas then
646 ignore(check_target bag context res "buildnew_target output");
651 demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left
653 if Utils.debug_res then check_res res "demod result";
654 let newmeta, newtarget =
657 let newmeta, newtarget = build_newtarget true t in
658 (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
659 if (Equality.is_weak_identity newtarget) (* || *)
660 (*Equality.meta_convertibility_eq target newtarget*) then
663 demodulation_equality bag ?from eq_uri newmeta env table newtarget
665 let res = demodulation_aux bag metasenv' context ugraph table 0 right in
666 if Utils.debug_res then check_res res "demod result 1";
669 let newmeta, newtarget = build_newtarget false t in
670 if (Equality.is_weak_identity newtarget) ||
671 (Equality.meta_convertibility_eq target newtarget) then
674 demodulation_equality bag ?from eq_uri newmeta env table newtarget
678 (* newmeta, newtarget *)
683 Performs the beta expansion of the term "term" w.r.t. "table",
684 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
687 let rec betaexpand_term
688 ?(subterms_only=false) metasenv context ugraph table lift_amount term
690 let module C = Cic in
691 let module S = CicSubstitution in
692 let module M = CicMetaSubst in
693 let module HL = HelmLibraryObjects in
695 let res, lifted_term =
701 (fun arg (res, lifted_tl) ->
704 let arg_res, lifted_arg =
705 betaexpand_term metasenv context ugraph table
709 (fun (t, s, m, ug, eq_found) ->
710 (Some t)::lifted_tl, s, m, ug, eq_found)
715 (fun (l, s, m, ug, eq_found) ->
716 (Some lifted_arg)::l, s, m, ug, eq_found)
718 (Some lifted_arg)::lifted_tl)
721 (fun (r, s, m, ug, eq_found) ->
722 None::r, s, m, ug, eq_found) res,
728 (fun (l, s, m, ug, eq_found) ->
729 (C.Meta (i, l), s, m, ug, eq_found)) l'
731 e, C.Meta (i, lifted_l)
734 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
736 | C.Prod (nn, s, t) ->
738 betaexpand_term metasenv context ugraph table lift_amount s in
740 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
741 table (lift_amount+1) t in
744 (fun (t, s, m, ug, eq_found) ->
745 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
748 (fun (t, s, m, ug, eq_found) ->
749 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
750 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
752 | C.Lambda (nn, s, t) ->
754 betaexpand_term metasenv context ugraph table lift_amount s in
756 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
757 table (lift_amount+1) t in
760 (fun (t, s, m, ug, eq_found) ->
761 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
764 (fun (t, s, m, ug, eq_found) ->
765 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
766 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
771 (fun (res, lifted_tl) arg ->
772 let arg_res, lifted_arg =
773 betaexpand_term metasenv context ugraph table lift_amount arg
777 (fun (a, s, m, ug, eq_found) ->
778 a::lifted_tl, s, m, ug, eq_found)
783 (fun (r, s, m, ug, eq_found) ->
784 lifted_arg::r, s, m, ug, eq_found)
786 lifted_arg::lifted_tl)
787 ) ([], []) (List.rev l)
790 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
793 | t -> [], (S.lift lift_amount t)
796 | C.Meta (i, l) -> res, lifted_term
799 C.Implicit None, ugraph
800 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
802 let candidates = get_candidates Unification table term in
804 if subterms_only then
808 metasenv context ugraph lift_amount term termty candidates
815 returns a list of new clauses inferred with a right superposition step
816 between the positive equation "target" and one in the "table" "newmeta" is
817 the first free meta index, i.e. the first number above the highest meta
818 index: its updated value is also returned
820 let superposition_right bag
821 ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
822 let module C = Cic in
823 let module S = CicSubstitution in
824 let module M = CicMetaSubst in
825 let module HL = HelmLibraryObjects in
826 let module CR = CicReduction in
827 let module U = Utils in
828 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
829 Equality.open_equality target
831 if Utils.debug_metas then
832 ignore (check_target bag context target "superpositionright");
833 let metasenv' = newmetas in
834 let maxmeta = ref newmeta in
838 fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
840 [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
844 (fun (_, subst, _, _, _) ->
845 let subst = apply_subst subst in
846 let o = !Utils.compare_terms (subst l) (subst r) in
847 o <> U.Lt && o <> U.Le)
848 (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
850 (res left right), (res right left)
852 let build_new ordering (bo, s, m, ug, eq_found) =
853 if Utils.debug_metas then
854 ignore (check_target bag context (snd eq_found) "buildnew1" );
856 let pos, equality = eq_found in
857 let (_, proof', (ty, what, other, _), menv',id') =
858 Equality.open_equality equality in
859 let what, other = if pos = Utils.Left then what, other else other, what in
861 let newgoal, newproof =
864 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
866 let name = C.Name "x" in
869 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
870 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
874 (s,(Equality.SuperpositionRight,
875 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
877 let newmeta, newequality =
879 if ordering = U.Gt then newgoal, apply_subst s right
880 else apply_subst s left, newgoal in
881 let neworder = !Utils.compare_terms left right in
882 let newmenv = (* Founif.filter s *) m in
883 let stat = (eq_ty, left, right, neworder) in
885 let w = Utils.compute_equality_weight stat in
886 Equality.mk_equality bag (w, newproof, stat, newmenv) in
887 if Utils.debug_metas then
888 ignore (check_target bag context eq' "buildnew3");
889 let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
890 if Utils.debug_metas then
891 ignore (check_target bag context eq' "buildnew4");
895 if Utils.debug_metas then
896 ignore(check_target bag context newequality "buildnew2");
899 let new1 = List.map (build_new U.Gt) res1
900 and new2 = List.map (build_new U.Lt) res2 in
901 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
903 (List.filter ok (new1 @ new2)))
906 (** demodulation, when the target is a theorem *)
907 let rec demodulation_theorem bag newmeta env table theorem =
908 let module C = Cic in
909 let module S = CicSubstitution in
910 let module M = CicMetaSubst in
911 let module HL = HelmLibraryObjects in
912 let metasenv, context, ugraph = env in
913 let maxmeta = ref newmeta in
914 let term, termty, metas = theorem in
915 let metasenv' = metas in
917 let build_newtheorem (t, subst, menv, ug, eq_found) =
918 let pos, equality = eq_found in
919 let (_, proof', (ty, what, other, _), menv',id) =
920 Equality.open_equality equality in
921 let what, other = if pos = Utils.Left then what, other else other, what in
923 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
924 (* let bo' = apply_subst subst t in *)
925 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
928 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
929 Equality.BasicProof (Equality.empty_subst,term))
931 (Equality.build_proof_term_old newproofold, bo)
933 (* TODO, not ported to the new proofs *)
934 if true then assert false; term, bo
936 !maxmeta, (newterm, newty, menv)
939 demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty
943 let newmeta, newthm = build_newtheorem t in
944 let newt, newty, _ = newthm in
945 if Equality.meta_convertibility termty newty then
948 demodulation_theorem bag newmeta env table newthm
953 (*****************************************************************************)
954 (** OPERATIONS ON GOALS **)
956 (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
957 (*****************************************************************************)
961 | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
962 (* assert (LibraryObjects.is_eq_URI uri); *)
967 let ty_of_goal (_,_,ty) = ty ;;
969 (* checks if two goals are metaconvertible *)
970 let goal_metaconvertibility_eq g1 g2 =
971 Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
974 (* when the betaexpand_term function is called on the left/right side of the
975 * goal, the predicate has to be fixed
976 * C[x] ---> (eq ty unchanged C[x])
977 * [posu] is the side of the [unchanged] term in the original goal
979 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
980 let _,_,eq,ty,l,r = open_goal goal in
981 let unchanged = if posu = Utils.Left then l else r in
982 let unchanged = CicSubstitution.lift 1 unchanged in
983 let ty = CicSubstitution.lift 1 ty in
986 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
987 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
989 (pred, subst, menv, ug, eq_f)
992 (* ginve the old [goal], the side that has not changed [posu] and the
993 * expansion builds a new goal *)
994 let build_newgoal bag context goal posu rule expansion =
995 let goalproof,_,_,_,_,_ = open_goal goal in
996 let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
997 let pos, equality = eq_found in
998 let (_, proof', (ty, what, other, _), menv',id) =
999 Equality.open_equality equality in
1000 let what, other = if pos = Utils.Left then what, other else other, what in
1001 let newterm, newgoalproof =
1003 Utils.guarded_simpl context
1004 (apply_subst subst (CicSubstitution.subst other t))
1006 let bo' = (*apply_subst subst*) t in
1009 let ty = apply_subst subst ty in *)
1010 let name = Cic.Name "x" in
1011 let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
1012 bo, (newgoalproofstep::goalproof)
1014 let newmetasenv = (* Founif.filter subst *) menv in
1015 (newgoalproof, newmetasenv, newterm)
1020 returns a list of new clauses inferred with a left superposition step
1021 the negative equation "target" and one of the positive equations in "table"
1023 let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
1024 let names = Utils.names_of_context context in
1025 let proof,menv,eq,ty,l,r = open_goal goal in
1026 let c = !Utils.compare_terms l r in
1028 if c = Utils.Incomparable then
1030 let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1031 let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1032 (* prerr_endline "incomparable";
1033 prerr_endline (string_of_int (List.length expansionsl));
1034 prerr_endline (string_of_int (List.length expansionsr));
1036 List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1038 List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1042 | Utils.Gt -> (* prerr_endline "GT"; *)
1043 let big,small,possmall = l,r,Utils.Right in
1044 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1046 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1048 | Utils.Lt -> (* prerr_endline "LT"; *)
1049 let big,small,possmall = r,l,Utils.Left in
1050 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1052 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1057 ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1060 (* rinfresco le meta *)
1063 let max,g = Equality.fix_metas_goal max g in max,g::acc)
1064 newgoals (maxmeta,[])
1067 (** demodulation, when the target is a goal *)
1068 let rec demodulation_goal bag env table goal =
1069 let goalproof,menv,_,_,left,right = open_goal goal in
1070 let _, context, ugraph = env in
1071 (* let term = Utils.guarded_simpl (~debug:true) context term in*)
1073 let resright = demodulation_aux bag menv context ugraph table 0 right in
1077 build_newgoal bag context goal Utils.Left Equality.Demodulation t
1079 if goal_metaconvertibility_eq goal newg then
1082 true, snd (demodulation_goal bag env table newg)
1083 | None -> false, goal
1085 let resleft = demodulation_aux bag menv context ugraph table 0 left in
1088 let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
1089 if goal_metaconvertibility_eq goal newg then
1092 true, snd (demodulation_goal bag env table newg)
1093 | None -> do_right ()
1096 let get_stats () = "" ;;