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 type goal = Equality.goal_proof * Cic.metasenv * Cic.term
32 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
34 module Index = Equality_indexing.DT (* path tree based indexing *)
37 let debug_print = Utils.debug_print;;
41 let check_equation env equation msg =
42 let w, proof, (eq_ty, left, right, order), metas, args = equation in
43 let metasenv, context, ugraph = env
44 let metasenv' = metasenv @ metas in
46 CicTypeChecker.type_of_aux' metasenv' context left ugraph;
47 CicTypeChecker.type_of_aux' metasenv' context right ugraph;
50 CicUtil.Meta_not_found _ as exn ->
53 prerr_endline (CicPp.ppterm left);
54 prerr_endline (CicPp.ppterm right);
59 type retrieval_mode = Matching | Unification;;
61 let string_of_res ?env =
64 | Some (t, s, m, u, (p,e)) ->
65 Printf.sprintf "Some: (%s, %s, %s)"
66 (Utils.string_of_pos p)
67 (Equality.string_of_equality ?env e)
71 let print_res ?env res =
74 (List.map (string_of_res ?env) res))
77 let print_candidates ?env mode term res =
81 prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
83 prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
89 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
90 (Equality.string_of_equality ?env e))
95 let apply_subst = Subst.apply_subst
97 let index = Index.index
98 let remove_index = Index.remove_index
99 let in_index = Index.in_index
100 let empty = Index.empty
101 let init_index = Index.init_index
103 let check_disjoint_invariant subst metasenv msg =
105 (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
108 prerr_endline ("not disjoint: " ^ msg);
113 let check_for_duplicates metas msg =
114 if List.length metas <>
115 List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
117 prerr_endline ("DUPLICATI " ^ msg);
118 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
123 let check_res res msg =
125 Some (t, subst, menv, ug, eq_found) ->
126 let eqs = Equality.string_of_equality (snd eq_found) in
127 check_disjoint_invariant subst menv msg;
128 check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
132 let check_target context target msg =
133 let w, proof, (eq_ty, left, right, order), metas,_ =
134 Equality.open_equality target in
135 (* check that metas does not contains duplicates *)
136 let eqs = Equality.string_of_equality target in
137 let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
138 let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
139 @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof) in
140 let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
141 let _ = if menv <> metas then
143 prerr_endline ("extra metas " ^ msg);
144 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
145 prerr_endline "**********************";
146 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
147 prerr_endline ("left: " ^ (CicPp.ppterm left));
148 prerr_endline ("right: " ^ (CicPp.ppterm right));
149 prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
155 ignore(CicTypeChecker.type_of_aux'
156 metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
159 prerr_endline (Inference.string_of_proof proof);
160 prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
161 prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
162 prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
167 (* returns a list of all the equalities in the tree that are in relation
168 "mode" with the given term, where mode can be either Matching or
171 Format of the return value: list of tuples in the form:
172 (position - Left or Right - of the term that matched the given one in this
176 Note that if equality is "left = right", if the ordering is left > right,
177 the position will always be Left, and if the ordering is left < right,
178 position will be Right.
181 let get_candidates ?env mode tree term =
185 let _ = <:start<retrieve_generalizations>> in
186 <:stop<retrieve_generalizations
187 Index.retrieve_generalizations tree term
190 let _ = <:start<retrieve_unifiables>> in
191 <:stop<retrieve_unifiables
192 Index.retrieve_unifiables tree term
196 Index.PosEqSet.elements s
200 finds the first equality in the index that matches "term", of type "termty"
201 termty can be Implicit if it is not needed. The result (one of the sides of
202 the equality, actually) should be not greater (wrt the term ordering) than
205 Format of the return value:
207 (term to substitute, [Cic.Rel 1 properly lifted - see the various
208 build_newtarget functions inside the various
209 demodulation_* functions]
210 substitution used for the matching,
212 ugraph, [substitution, metasenv and ugraph have the same meaning as those
213 returned by CicUnification.fo_unif]
214 (equality where the matching term was found, [i.e. the equality to use as
216 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
217 the equality: this is used to build the proof term, again see one of
218 the build_newtarget functions]
221 let rec find_matches metasenv context ugraph lift_amount term termty =
222 let module C = Cic in
223 let module U = Utils in
224 let module S = CicSubstitution in
225 let module M = CicMetaSubst in
226 let module HL = HelmLibraryObjects in
227 let cmp = !Utils.compare_terms in
228 let check = match termty with C.Implicit None -> false | _ -> true in
232 let pos, equality = candidate in
233 let (_, proof, (ty, left, right, o), metas,_) =
234 Equality.open_equality equality
236 if Utils.debug_metas then
237 ignore(check_target context (snd candidate) "find_matches");
238 if Utils.debug_res then
240 let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
241 let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
242 let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
245 (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
248 check_for_duplicates metas "gia nella metas";
249 check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*))
251 if check && not (fst (CicReduction.are_convertible
252 ~metasenv context termty ty ugraph)) then (
253 find_matches metasenv context ugraph lift_amount term termty tl
256 let subst', metasenv', ugraph' =
258 metasenv metas context term (S.lift lift_amount c) ugraph
260 Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
263 if pos = Utils.Left then left, right
266 if o <> U.Incomparable then
270 with Inference.MatchingFailure ->
271 find_matches metasenv context ugraph lift_amount term termty tl
273 if Utils.debug_res then ignore (check_res res "find1");
278 with Inference.MatchingFailure -> None
280 if Utils.debug_res then ignore (check_res res "find2");
282 | Some (_, s, _, _, _) ->
283 let c' = apply_subst s c in
285 let other' = U.guarded_simpl context (apply_subst s other) in *)
286 let other' = apply_subst s other in
287 let order = cmp c' other' in
292 metasenv context ugraph lift_amount term termty tl
294 find_matches metasenv context ugraph lift_amount term termty tl
297 let find_matches metasenv context ugraph lift_amount term termty =
298 find_matches metasenv context ugraph lift_amount term termty
302 as above, but finds all the matching equalities, and the matching condition
303 can be either Inference.matching or Inference.unification
305 let rec find_all_matches ?(unif_fun=Inference.unification)
306 metasenv context ugraph lift_amount term termty =
307 let module C = Cic in
308 let module U = Utils in
309 let module S = CicSubstitution in
310 let module M = CicMetaSubst in
311 let module HL = HelmLibraryObjects in
312 let cmp = !Utils.compare_terms in
316 let pos, equality = candidate in
317 let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
319 let subst', metasenv', ugraph' =
320 unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
322 (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
325 if pos = Utils.Left then left, right
328 if o <> U.Incomparable then
330 let res = do_match c in
331 res::(find_all_matches ~unif_fun metasenv context ugraph
332 lift_amount term termty tl)
334 | Inference.MatchingFailure
335 | CicUnification.UnificationFailure _
336 | CicUnification.Uncertain _ ->
337 find_all_matches ~unif_fun metasenv context ugraph
338 lift_amount term termty tl
341 let res = do_match c in
344 let c' = apply_subst s c
345 and other' = apply_subst s other in
346 let order = cmp c' other' in
347 if order <> U.Lt && order <> U.Le then
348 res::(find_all_matches ~unif_fun metasenv context ugraph
349 lift_amount term termty tl)
351 find_all_matches ~unif_fun metasenv context ugraph
352 lift_amount term termty tl
354 | Inference.MatchingFailure
355 | CicUnification.UnificationFailure _
356 | CicUnification.Uncertain _ ->
357 find_all_matches ~unif_fun metasenv context ugraph
358 lift_amount term termty tl
362 ?unif_fun metasenv context ugraph lift_amount term termty l
365 ?unif_fun metasenv context ugraph lift_amount term termty l
366 (*prerr_endline "CANDIDATES:";
367 List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
368 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
372 returns true if target is subsumed by some equality in table
375 prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
376 ((pos,equation),_)) -> Equality.string_of_equality equation)l))
379 let subsumption_aux use_unification env table target =
380 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
381 let metasenv, context, ugraph = env in
382 let metasenv = tmetas in
383 let predicate, unif_fun =
384 if use_unification then
385 Unification, Inference.unification
387 Matching, Inference.matching
391 | Cic.Meta _ when not use_unification -> []
393 let leftc = get_candidates predicate table left in
394 find_all_matches ~unif_fun
395 metasenv context ugraph 0 left ty leftc
397 let rec ok what leftorright = function
399 | (_, subst, menv, ug, (pos,equation))::tl ->
400 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
402 let other = if pos = Utils.Left then r else l in
403 let what' = Subst.apply_subst subst what in
404 let other' = Subst.apply_subst subst other in
405 let subst', menv', ug' =
406 unif_fun metasenv m context what' other' ugraph
408 (match Subst.merge_subst_if_possible subst subst' with
409 | None -> ok what leftorright tl
410 | Some s -> Some (s, equation, leftorright <> pos ))
412 | Inference.MatchingFailure
413 | CicUnification.UnificationFailure _ -> ok what leftorright tl
415 match ok right Utils.Left leftr with
416 | Some _ as res -> res
420 | Cic.Meta _ when not use_unification -> []
422 let rightc = get_candidates predicate table right in
423 find_all_matches ~unif_fun
424 metasenv context ugraph 0 right ty rightc
426 ok left Utils.Right rightr
429 let subsumption x y z =
430 subsumption_aux false x y z
433 let unification x y z =
434 subsumption_aux true x y z
437 let rec demodulation_aux ?from ?(typecheck=false)
438 metasenv context ugraph table lift_amount term =
439 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
440 let module C = Cic in
441 let module S = CicSubstitution in
442 let module M = CicMetaSubst in
443 let module HL = HelmLibraryObjects in
446 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
454 CicTypeChecker.type_of_aux' metasenv context term ugraph
456 C.Implicit None, ugraph
459 find_matches metasenv context ugraph lift_amount term termty candidates
461 if Utils.debug_res then ignore(check_res res "demod1");
471 (res, tl @ [S.lift 1 t])
474 demodulation_aux ~from:"1" metasenv context ugraph table
478 | None -> (None, tl @ [S.lift 1 t])
479 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
484 | Some (_, subst, menv, ug, eq_found) ->
485 Some (C.Appl ll, subst, menv, ug, eq_found)
487 | C.Prod (nn, s, t) ->
489 demodulation_aux ~from:"2"
490 metasenv context ugraph table lift_amount s in (
494 demodulation_aux metasenv
495 ((Some (nn, C.Decl s))::context) ugraph
496 table (lift_amount+1) t
500 | Some (t', subst, menv, ug, eq_found) ->
501 Some (C.Prod (nn, (S.lift 1 s), t'),
502 subst, menv, ug, eq_found)
504 | Some (s', subst, menv, ug, eq_found) ->
505 Some (C.Prod (nn, s', (S.lift 1 t)),
506 subst, menv, ug, eq_found)
508 | C.Lambda (nn, s, t) ->
511 metasenv context ugraph table lift_amount s in (
515 demodulation_aux metasenv
516 ((Some (nn, C.Decl s))::context) ugraph
517 table (lift_amount+1) t
521 | Some (t', subst, menv, ug, eq_found) ->
522 Some (C.Lambda (nn, (S.lift 1 s), t'),
523 subst, menv, ug, eq_found)
525 | Some (s', subst, menv, ug, eq_found) ->
526 Some (C.Lambda (nn, s', (S.lift 1 t)),
527 subst, menv, ug, eq_found)
532 if Utils.debug_res then ignore(check_res res "demod_aux output");
538 (** demodulation, when target is an equality *)
539 let rec demodulation_equality ?from eq_uri newmeta env table sign target =
540 let module C = Cic in
541 let module S = CicSubstitution in
542 let module M = CicMetaSubst in
543 let module HL = HelmLibraryObjects in
544 let module U = Utils in
545 let metasenv, context, ugraph = env in
546 let w, proof, (eq_ty, left, right, order), metas, id =
547 Equality.open_equality target
549 (* first, we simplify *)
550 (* let right = U.guarded_simpl context right in *)
551 (* let left = U.guarded_simpl context left in *)
552 (* let order = !Utils.compare_terms left right in *)
553 (* let stat = (eq_ty, left, right, order) in *)
554 (* let w = Utils.compute_equality_weight stat in*)
555 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
556 if Utils.debug_metas then
557 ignore(check_target context target "demod equalities input");
558 let metasenv' = (* metasenv @ *) metas in
559 let maxmeta = ref newmeta in
561 let build_newtarget is_left (t, subst, menv, ug, eq_found) =
563 if Utils.debug_metas then
565 ignore(check_for_duplicates menv "input1");
566 ignore(check_disjoint_invariant subst menv "input2");
567 let substs = Subst.ppsubst subst in
568 ignore(check_target context (snd eq_found) ("input3" ^ substs))
570 let pos, equality = eq_found in
572 (ty, what, other, _), menv',id') = Equality.open_equality equality in
574 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
575 with CicUtil.Meta_not_found _ -> ty
577 let what, other = if pos = Utils.Left then what, other else other, what in
578 let newterm, newproof =
580 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
581 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
582 let name = C.Name "x" in
584 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
585 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
587 if sign = Utils.Positive then
588 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
589 (Cic.Lambda (name, ty, bo'))))))
594 prerr_endline "***************************************negative";
598 CicMkImplicit.identity_relocation_list_for_metavariable context in
599 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
600 (* print_newline (); *)
601 C.Meta (!maxmeta, irl)
606 if pos = Utils.Left then [ty; what; other]
607 else [ty; other; what]
609 Equality.ProofSymBlock (termlist, proof'_old)
611 let proof'_new' = assert false (* not implemented *) in
613 if pos = Utils.Left then what, other else other, what
617 (0, (proof'_new',proof'_old'),
618 (ty, other, what, Utils.Incomparable),menv')
623 (subst, eq_URI, (name, ty), bo',
624 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
626 assert false, (* not implemented *)
627 (match snd proof with
628 | Equality.BasicProof _ ->
629 (* print_endline "replacing a BasicProof"; *)
631 | Equality.ProofGoalBlock (_, parent_proof) ->
632 (* print_endline "replacing another ProofGoalBlock"; *)
633 Equality.ProofGoalBlock (pb, parent_proof)
637 C.Appl [C.MutConstruct (* reflexivity *)
638 (LibraryObjects.eq_URI (), 0, 1, []);
639 eq_ty; if is_left then right else left]
642 (assert false, (* not implemented *)
643 Equality.ProofGoalBlock
644 (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
648 let newmenv = (* Inference.filter subst *) menv in
651 if Utils.debug_metas then
652 try ignore(CicTypeChecker.type_of_aux'
654 (Equality.build_proof_term newproof) ugraph);
657 prerr_endline "sempre lui";
658 prerr_endline (Subst.ppsubst subst);
659 prerr_endline (CicPp.ppterm
660 (Equality.build_proof_term newproof));
661 prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
662 prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
663 prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
664 prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
665 prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
671 let left, right = if is_left then newterm, right else left, newterm in
672 let ordering = !Utils.compare_terms left right in
673 let stat = (eq_ty, left, right, ordering) in
675 let w = Utils.compute_equality_weight stat in
676 (Equality.mk_equality (w, newproof, stat,newmenv))
678 if Utils.debug_metas then
679 ignore(check_target context res "buildnew_target output");
683 let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
684 if Utils.debug_res then check_res res "demod result";
685 let newmeta, newtarget =
688 let newmeta, newtarget = build_newtarget true t in
689 assert (not (Equality.meta_convertibility_eq target newtarget));
690 if (Equality.is_weak_identity newtarget) ||
691 (Equality.meta_convertibility_eq target newtarget) then
694 demodulation_equality ?from eq_uri newmeta env table sign newtarget
696 let res = demodulation_aux metasenv' context ugraph table 0 right in
697 if Utils.debug_res then check_res res "demod result 1";
700 let newmeta, newtarget = build_newtarget false t in
701 if (Equality.is_weak_identity newtarget) ||
702 (Equality.meta_convertibility_eq target newtarget) then
705 demodulation_equality ?from eq_uri newmeta env table sign newtarget
709 (* newmeta, newtarget *)
714 Performs the beta expansion of the term "term" w.r.t. "table",
715 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
718 let rec betaexpand_term
719 ?(subterms_only=false) metasenv context ugraph table lift_amount term
721 let module C = Cic in
722 let module S = CicSubstitution in
723 let module M = CicMetaSubst in
724 let module HL = HelmLibraryObjects in
726 let res, lifted_term =
732 (fun arg (res, lifted_tl) ->
735 let arg_res, lifted_arg =
736 betaexpand_term metasenv context ugraph table
740 (fun (t, s, m, ug, eq_found) ->
741 (Some t)::lifted_tl, s, m, ug, eq_found)
746 (fun (l, s, m, ug, eq_found) ->
747 (Some lifted_arg)::l, s, m, ug, eq_found)
749 (Some lifted_arg)::lifted_tl)
752 (fun (r, s, m, ug, eq_found) ->
753 None::r, s, m, ug, eq_found) res,
759 (fun (l, s, m, ug, eq_found) ->
760 (C.Meta (i, l), s, m, ug, eq_found)) l'
762 e, C.Meta (i, lifted_l)
765 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
767 | C.Prod (nn, s, t) ->
769 betaexpand_term metasenv context ugraph table lift_amount s in
771 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
772 table (lift_amount+1) t in
775 (fun (t, s, m, ug, eq_found) ->
776 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
779 (fun (t, s, m, ug, eq_found) ->
780 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
781 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
783 | C.Lambda (nn, s, t) ->
785 betaexpand_term metasenv context ugraph table lift_amount s in
787 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
788 table (lift_amount+1) t in
791 (fun (t, s, m, ug, eq_found) ->
792 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
795 (fun (t, s, m, ug, eq_found) ->
796 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
797 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
802 (fun (res, lifted_tl) arg ->
803 let arg_res, lifted_arg =
804 betaexpand_term metasenv context ugraph table lift_amount arg
808 (fun (a, s, m, ug, eq_found) ->
809 a::lifted_tl, s, m, ug, eq_found)
814 (fun (r, s, m, ug, eq_found) ->
815 lifted_arg::r, s, m, ug, eq_found)
817 lifted_arg::lifted_tl)
818 ) ([], []) (List.rev l)
821 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
824 | t -> [], (S.lift lift_amount t)
827 | C.Meta (i, l) -> res, lifted_term
830 C.Implicit None, ugraph
831 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
833 let candidates = get_candidates Unification table term in
835 if subterms_only then
839 metasenv context ugraph lift_amount term termty candidates
846 returns a list of new clauses inferred with a right superposition step
847 between the positive equation "target" and one in the "table" "newmeta" is
848 the first free meta index, i.e. the first number above the highest meta
849 index: its updated value is also returned
851 let superposition_right
852 ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
853 let module C = Cic in
854 let module S = CicSubstitution in
855 let module M = CicMetaSubst in
856 let module HL = HelmLibraryObjects in
857 let module CR = CicReduction in
858 let module U = Utils in
859 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
860 Equality.open_equality target
862 if Utils.debug_metas then
863 ignore (check_target context target "superpositionright");
864 let metasenv' = newmetas in
865 let maxmeta = ref newmeta in
869 fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
871 [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
875 (fun (_, subst, _, _, _) ->
876 let subst = apply_subst subst in
877 let o = !Utils.compare_terms (subst l) (subst r) in
878 o <> U.Lt && o <> U.Le)
879 (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
881 (res left right), (res right left)
883 let build_new ordering (bo, s, m, ug, eq_found) =
884 if Utils.debug_metas then
885 ignore (check_target context (snd eq_found) "buildnew1" );
887 let pos, equality = eq_found in
888 let (_, proof', (ty, what, other, _), menv',id') =
889 Equality.open_equality equality in
890 let what, other = if pos = Utils.Left then what, other else other, what in
892 let newgoal, newproof =
895 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
897 let name = C.Name "x" in
900 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
901 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
905 (s,(Equality.SuperpositionRight,
906 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
908 let newmeta, newequality =
910 if ordering = U.Gt then newgoal, apply_subst s right
911 else apply_subst s left, newgoal in
912 let neworder = !Utils.compare_terms left right in
913 let newmenv = (* Inference.filter s *) m in
914 let stat = (eq_ty, left, right, neworder) in
916 let w = Utils.compute_equality_weight stat in
917 Equality.mk_equality (w, newproof, stat, newmenv) in
918 if Utils.debug_metas then
919 ignore (check_target context eq' "buildnew3");
920 let newm, eq' = Equality.fix_metas !maxmeta eq' in
921 if Utils.debug_metas then
922 ignore (check_target context eq' "buildnew4");
926 if Utils.debug_metas then
927 ignore(check_target context newequality "buildnew2");
930 let new1 = List.map (build_new U.Gt) res1
931 and new2 = List.map (build_new U.Lt) res2 in
932 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
934 (List.filter ok (new1 @ new2)))
937 (** demodulation, when the target is a theorem *)
938 let rec demodulation_theorem newmeta env table theorem =
939 let module C = Cic in
940 let module S = CicSubstitution in
941 let module M = CicMetaSubst in
942 let module HL = HelmLibraryObjects in
943 let metasenv, context, ugraph = env in
944 let maxmeta = ref newmeta in
945 let term, termty, metas = theorem in
946 let metasenv' = metas in
948 let build_newtheorem (t, subst, menv, ug, eq_found) =
949 let pos, equality = eq_found in
950 let (_, proof', (ty, what, other, _), menv',id) =
951 Equality.open_equality equality in
952 let what, other = if pos = Utils.Left then what, other else other, what in
954 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
955 (* let bo' = apply_subst subst t in *)
956 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
959 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
960 Equality.BasicProof (Equality.empty_subst,term))
962 (Equality.build_proof_term_old newproofold, bo)
964 (* TODO, not ported to the new proofs *)
965 if true then assert false; term, bo
967 !maxmeta, (newterm, newty, menv)
970 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
974 let newmeta, newthm = build_newtheorem t in
975 let newt, newty, _ = newthm in
976 if Equality.meta_convertibility termty newty then
979 demodulation_theorem newmeta env table newthm
984 (*****************************************************************************)
985 (** OPERATIONS ON GOALS **)
987 (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
988 (*****************************************************************************)
992 | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
993 assert (LibraryObjects.is_eq_URI uri);
998 let ty_of_goal (_,_,ty) = ty ;;
1000 (* checks if two goals are metaconvertible *)
1001 let goal_metaconvertibility_eq g1 g2 =
1002 Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
1005 (* when the betaexpand_term function is called on the left/right side of the
1006 * goal, the predicate has to be fixed
1007 * C[x] ---> (eq ty unchanged C[x])
1008 * [posu] is the side of the [unchanged] term in the original goal
1010 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1011 let _,_,eq,ty,l,r = open_goal goal in
1012 let unchanged = if posu = Utils.Left then l else r in
1013 let unchanged = CicSubstitution.lift 1 unchanged in
1014 let ty = CicSubstitution.lift 1 ty in
1017 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1018 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1020 (pred, subst, menv, ug, eq_f)
1023 (* ginve the old [goal], the side that has not changed [posu] and the
1024 * expansion builds a new goal *)
1025 let build_newgoal context goal posu rule expansion =
1026 let goalproof,_,_,_,_,_ = open_goal goal in
1027 let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
1028 let pos, equality = eq_found in
1029 let (_, proof', (ty, what, other, _), menv',id) =
1030 Equality.open_equality equality in
1031 let what, other = if pos = Utils.Left then what, other else other, what in
1032 let newterm, newgoalproof =
1034 Utils.guarded_simpl context
1035 (apply_subst subst (CicSubstitution.subst other t))
1037 let bo' = (*apply_subst subst*) t in
1038 let name = Cic.Name "x" in
1039 let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
1040 bo, (newgoalproofstep::goalproof)
1042 let newmetasenv = (* Inference.filter subst *) menv in
1043 (newgoalproof, newmetasenv, newterm)
1048 returns a list of new clauses inferred with a left superposition step
1049 the negative equation "target" and one of the positive equations in "table"
1051 let superposition_left (metasenv, context, ugraph) table goal =
1052 let proof,menv,eq,ty,l,r = open_goal goal in
1053 let c = !Utils.compare_terms l r in
1054 if c = Utils.Incomparable then
1056 let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1057 let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1058 (* prerr_endline "incomparable";
1059 prerr_endline (string_of_int (List.length expansionsl));
1060 prerr_endline (string_of_int (List.length expansionsr));
1062 List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1064 List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1067 let big,small,possmall =
1069 Utils.Gt -> (* prerr_endline "GT"; *) l,r,Utils.Right
1070 | Utils.Lt -> (* prerr_endline "LT"; *) r,l,Utils.Left
1073 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1074 List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
1077 (** demodulation, when the target is a goal *)
1078 let rec demodulation_goal env table goal =
1079 let goalproof,menv,_,_,left,right = open_goal goal in
1080 let _, context, ugraph = env in
1081 (* let term = Utils.guarded_simpl (~debug:true) context term in*)
1083 let resright = demodulation_aux menv context ugraph table 0 right in
1087 build_newgoal context goal Utils.Left Equality.Demodulation t
1089 if goal_metaconvertibility_eq goal newg then
1092 true, snd (demodulation_goal env table newg)
1093 | None -> false, goal
1095 let resleft = demodulation_aux menv context ugraph table 0 left in
1098 let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
1099 if goal_metaconvertibility_eq goal newg then
1102 true, snd (demodulation_goal env table newg)
1103 | None -> do_right ()
1106 let get_stats () = <:show<Indexing.>> ;;