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), eq_URI)) ->
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, eq_URI)) ->
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
255 let do_match c eq_URI =
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',
263 let c, other, eq_URI =
264 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
265 else right, left, Utils.eq_ind_r_URI ()
267 if o <> U.Incomparable then
271 with Inference.MatchingFailure ->
272 find_matches metasenv context ugraph lift_amount term termty tl
274 if Utils.debug_res then ignore (check_res res "find1");
278 try do_match c eq_URI
279 with Inference.MatchingFailure -> None
281 if Utils.debug_res then ignore (check_res res "find2");
283 | Some (_, s, _, _, _) ->
284 let c' = apply_subst s c in
286 let other' = U.guarded_simpl context (apply_subst s other) in *)
287 let other' = apply_subst s other in
288 let order = cmp c' other' in
293 metasenv context ugraph lift_amount term termty tl
295 find_matches metasenv context ugraph lift_amount term termty tl
298 let find_matches metasenv context ugraph lift_amount term termty =
299 find_matches metasenv context ugraph lift_amount term termty
303 as above, but finds all the matching equalities, and the matching condition
304 can be either Inference.matching or Inference.unification
306 let rec find_all_matches ?(unif_fun=Inference.unification)
307 metasenv context ugraph lift_amount term termty =
308 let module C = Cic in
309 let module U = Utils in
310 let module S = CicSubstitution in
311 let module M = CicMetaSubst in
312 let module HL = HelmLibraryObjects in
313 let cmp = !Utils.compare_terms in
317 let pos, equality = candidate in
318 let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
319 let do_match c eq_URI =
320 let subst', metasenv', ugraph' =
321 unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
323 (C.Rel (1+lift_amount),subst',metasenv',ugraph',(candidate, eq_URI))
325 let c, other, eq_URI =
326 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
327 else right, left, Utils.eq_ind_r_URI ()
329 if o <> U.Incomparable then
331 let res = do_match c eq_URI in
332 res::(find_all_matches ~unif_fun metasenv context ugraph
333 lift_amount term termty tl)
335 | Inference.MatchingFailure
336 | CicUnification.UnificationFailure _
337 | CicUnification.Uncertain _ ->
338 find_all_matches ~unif_fun metasenv context ugraph
339 lift_amount term termty tl
342 let res = do_match c eq_URI in
345 let c' = apply_subst s c
346 and other' = apply_subst s other in
347 let order = cmp c' other' in
348 if order <> U.Lt && order <> U.Le then
349 res::(find_all_matches ~unif_fun metasenv context ugraph
350 lift_amount term termty tl)
352 find_all_matches ~unif_fun metasenv context ugraph
353 lift_amount term termty tl
355 | Inference.MatchingFailure
356 | CicUnification.UnificationFailure _
357 | CicUnification.Uncertain _ ->
358 find_all_matches ~unif_fun metasenv context ugraph
359 lift_amount term termty tl
363 ?unif_fun metasenv context ugraph lift_amount term termty l
366 ?unif_fun metasenv context ugraph lift_amount term termty l
367 (*prerr_endline "CANDIDATES:";
368 List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
369 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
373 returns true if target is subsumed by some equality in table
376 prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
377 ((pos,equation),_)) -> Equality.string_of_equality equation)l))
380 let subsumption_aux use_unification env table target =
381 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
382 let metasenv, context, ugraph = env in
383 let metasenv = tmetas in
384 let predicate, unif_fun =
385 if use_unification then
386 Unification, Inference.unification
388 Matching, Inference.matching
392 | Cic.Meta _ when not use_unification -> []
394 let leftc = get_candidates predicate table left in
395 find_all_matches ~unif_fun
396 metasenv context ugraph 0 left ty leftc
398 let rec ok what leftorright = function
400 | (_, subst, menv, ug, ((pos,equation),_))::tl ->
401 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
403 let other = if pos = Utils.Left then r else l in
404 let what' = Subst.apply_subst subst what in
405 let other' = Subst.apply_subst subst other in
406 let subst', menv', ug' =
407 unif_fun metasenv m context what' other' ugraph
409 (match Subst.merge_subst_if_possible subst subst' with
410 | None -> ok what leftorright tl
411 | Some s -> Some (s, equation, leftorright <> pos ))
413 | Inference.MatchingFailure
414 | CicUnification.UnificationFailure _ -> ok what leftorright tl
416 match ok right Utils.Left leftr with
417 | Some _ as res -> res
421 | Cic.Meta _ when not use_unification -> []
423 let rightc = get_candidates predicate table right in
424 find_all_matches ~unif_fun
425 metasenv context ugraph 0 right ty rightc
427 ok left Utils.Right rightr
430 let subsumption x y z =
431 subsumption_aux false x y z
434 let unification x y z =
435 subsumption_aux true x y z
438 let rec demodulation_aux ?from ?(typecheck=false)
439 metasenv context ugraph table lift_amount term =
440 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
441 let module C = Cic in
442 let module S = CicSubstitution in
443 let module M = CicMetaSubst in
444 let module HL = HelmLibraryObjects in
447 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
455 CicTypeChecker.type_of_aux' metasenv context term ugraph
457 C.Implicit None, ugraph
460 find_matches metasenv context ugraph lift_amount term termty candidates
462 if Utils.debug_res then ignore(check_res res "demod1");
472 (res, tl @ [S.lift 1 t])
475 demodulation_aux ~from:"1" metasenv context ugraph table
479 | None -> (None, tl @ [S.lift 1 t])
480 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
485 | Some (_, subst, menv, ug, eq_found) ->
486 Some (C.Appl ll, subst, menv, ug, eq_found)
488 | C.Prod (nn, s, t) ->
490 demodulation_aux ~from:"2"
491 metasenv context ugraph table lift_amount s in (
495 demodulation_aux metasenv
496 ((Some (nn, C.Decl s))::context) ugraph
497 table (lift_amount+1) t
501 | Some (t', subst, menv, ug, eq_found) ->
502 Some (C.Prod (nn, (S.lift 1 s), t'),
503 subst, menv, ug, eq_found)
505 | Some (s', subst, menv, ug, eq_found) ->
506 Some (C.Prod (nn, s', (S.lift 1 t)),
507 subst, menv, ug, eq_found)
509 | C.Lambda (nn, s, t) ->
512 metasenv context ugraph table lift_amount s in (
516 demodulation_aux metasenv
517 ((Some (nn, C.Decl s))::context) ugraph
518 table (lift_amount+1) t
522 | Some (t', subst, menv, ug, eq_found) ->
523 Some (C.Lambda (nn, (S.lift 1 s), t'),
524 subst, menv, ug, eq_found)
526 | Some (s', subst, menv, ug, eq_found) ->
527 Some (C.Lambda (nn, s', (S.lift 1 t)),
528 subst, menv, ug, eq_found)
533 if Utils.debug_res then ignore(check_res res "demod_aux output");
539 (** demodulation, when target is an equality *)
540 let rec demodulation_equality ?from newmeta env table sign target =
541 let module C = Cic in
542 let module S = CicSubstitution in
543 let module M = CicMetaSubst in
544 let module HL = HelmLibraryObjects in
545 let module U = Utils in
546 let metasenv, context, ugraph = env in
547 let w, proof, (eq_ty, left, right, order), metas, id =
548 Equality.open_equality target
550 (* first, we simplify *)
551 (* let right = U.guarded_simpl context right in *)
552 (* let left = U.guarded_simpl context left in *)
553 (* let order = !Utils.compare_terms left right in *)
554 (* let stat = (eq_ty, left, right, order) in *)
555 (* let w = Utils.compute_equality_weight stat in*)
556 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
557 if Utils.debug_metas then
558 ignore(check_target context target "demod equalities input");
559 let metasenv' = (* metasenv @ *) metas in
560 let maxmeta = ref newmeta in
562 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
564 if Utils.debug_metas then
566 ignore(check_for_duplicates menv "input1");
567 ignore(check_disjoint_invariant subst menv "input2");
568 let substs = Subst.ppsubst subst in
569 ignore(check_target context (snd eq_found) ("input3" ^ substs))
571 let pos, equality = eq_found in
573 (ty, what, other, _), menv',id') = Equality.open_equality equality in
575 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
576 with CicUtil.Meta_not_found _ -> ty
578 let what, other = if pos = Utils.Left then what, other else other, what in
579 let newterm, newproof =
581 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
582 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
583 let name = C.Name "x" in
585 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
586 C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
587 S.lift 1 eq_ty; l; r]
589 if sign = Utils.Positive then
590 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
591 (Cic.Lambda (name, ty, bo'))))))
596 prerr_endline "***************************************negative";
600 CicMkImplicit.identity_relocation_list_for_metavariable context in
601 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
602 (* print_newline (); *)
603 C.Meta (!maxmeta, irl)
608 if pos = Utils.Left then [ty; what; other]
609 else [ty; other; what]
611 Equality.ProofSymBlock (termlist, proof'_old)
613 let proof'_new' = assert false (* not implemented *) in
615 if pos = Utils.Left then what, other else other, what
619 (0, (proof'_new',proof'_old'),
620 (ty, other, what, Utils.Incomparable),menv')
625 (subst, eq_URI, (name, ty), bo',
626 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
628 assert false, (* not implemented *)
629 (match snd proof with
630 | Equality.BasicProof _ ->
631 (* print_endline "replacing a BasicProof"; *)
633 | Equality.ProofGoalBlock (_, parent_proof) ->
634 (* print_endline "replacing another ProofGoalBlock"; *)
635 Equality.ProofGoalBlock (pb, parent_proof)
639 C.Appl [C.MutConstruct (* reflexivity *)
640 (LibraryObjects.eq_URI (), 0, 1, []);
641 eq_ty; if is_left then right else left]
644 (assert false, (* not implemented *)
645 Equality.ProofGoalBlock
646 (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
650 let newmenv = (* Inference.filter subst *) menv in
653 if Utils.debug_metas then
654 try ignore(CicTypeChecker.type_of_aux'
656 (Equality.build_proof_term newproof) ugraph);
659 prerr_endline "sempre lui";
660 prerr_endline (Subst.ppsubst subst);
661 prerr_endline (CicPp.ppterm
662 (Equality.build_proof_term newproof));
663 prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
664 prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
665 prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
666 prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
667 prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
673 let left, right = if is_left then newterm, right else left, newterm in
674 let ordering = !Utils.compare_terms left right in
675 let stat = (eq_ty, left, right, ordering) in
677 let w = Utils.compute_equality_weight stat in
678 (Equality.mk_equality (w, newproof, stat,newmenv))
680 if Utils.debug_metas then
681 ignore(check_target context res "buildnew_target output");
685 let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
686 if Utils.debug_res then check_res res "demod result";
687 let newmeta, newtarget =
690 let newmeta, newtarget = build_newtarget true t in
691 assert (not (Equality.meta_convertibility_eq target newtarget));
692 if (Equality.is_weak_identity newtarget) ||
693 (Equality.meta_convertibility_eq target newtarget) then
696 demodulation_equality ?from newmeta env table sign newtarget
698 let res = demodulation_aux metasenv' context ugraph table 0 right in
699 if Utils.debug_res then check_res res "demod result 1";
702 let newmeta, newtarget = build_newtarget false t in
703 if (Equality.is_weak_identity newtarget) ||
704 (Equality.meta_convertibility_eq target newtarget) then
707 demodulation_equality ?from newmeta env table sign newtarget
711 (* newmeta, newtarget *)
716 Performs the beta expansion of the term "term" w.r.t. "table",
717 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
720 let rec betaexpand_term
721 ?(subterms_only=false) metasenv context ugraph table lift_amount term
723 let module C = Cic in
724 let module S = CicSubstitution in
725 let module M = CicMetaSubst in
726 let module HL = HelmLibraryObjects in
728 let res, lifted_term =
733 (fun arg (res, lifted_tl) ->
736 let arg_res, lifted_arg =
737 betaexpand_term metasenv context ugraph table
741 (fun (t, s, m, ug, eq_found) ->
742 (Some t)::lifted_tl, s, m, ug, eq_found)
747 (fun (l, s, m, ug, eq_found) ->
748 (Some lifted_arg)::l, s, m, ug, eq_found)
750 (Some lifted_arg)::lifted_tl)
753 (fun (r, s, m, ug, eq_found) ->
754 None::r, s, m, ug, eq_found) res,
760 (fun (l, s, m, ug, eq_found) ->
761 (C.Meta (i, l), s, m, ug, eq_found)) l'
763 e, C.Meta (i, lifted_l)
766 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
768 | C.Prod (nn, s, t) ->
770 betaexpand_term metasenv context ugraph table lift_amount s in
772 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
773 table (lift_amount+1) t in
776 (fun (t, s, m, ug, eq_found) ->
777 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
780 (fun (t, s, m, ug, eq_found) ->
781 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
782 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
784 | C.Lambda (nn, s, t) ->
786 betaexpand_term metasenv context ugraph table lift_amount s in
788 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
789 table (lift_amount+1) t in
792 (fun (t, s, m, ug, eq_found) ->
793 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
796 (fun (t, s, m, ug, eq_found) ->
797 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
798 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
803 (fun arg (res, lifted_tl) ->
804 let arg_res, lifted_arg =
805 betaexpand_term metasenv context ugraph table lift_amount arg
809 (fun (a, s, m, ug, eq_found) ->
810 a::lifted_tl, s, m, ug, eq_found)
815 (fun (r, s, m, ug, eq_found) ->
816 lifted_arg::r, s, m, ug, eq_found)
818 lifted_arg::lifted_tl)
822 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
825 | t -> [], (S.lift lift_amount t)
828 | C.Meta (i, l) -> res, lifted_term
831 C.Implicit None, ugraph
832 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
834 let candidates = get_candidates Unification table term in
836 if subterms_only then
840 metasenv context ugraph lift_amount term termty candidates
847 returns a list of new clauses inferred with a right superposition step
848 between the positive equation "target" and one in the "table" "newmeta" is
849 the first free meta index, i.e. the first number above the highest meta
850 index: its updated value is also returned
852 let superposition_right
853 ?(subterms_only=false) newmeta (metasenv, context, ugraph) table target
855 let module C = Cic in
856 let module S = CicSubstitution in
857 let module M = CicMetaSubst in
858 let module HL = HelmLibraryObjects in
859 let module CR = CicReduction in
860 let module U = Utils in
861 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
862 Equality.open_equality target
864 if Utils.debug_metas then
865 ignore (check_target context target "superpositionright");
866 let metasenv' = newmetas in
867 let maxmeta = ref newmeta in
871 fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
873 [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
877 (fun (_, subst, _, _, _) ->
878 let subst = apply_subst subst in
879 let o = !Utils.compare_terms (subst l) (subst r) in
880 o <> U.Lt && o <> U.Le)
881 (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
883 (res left right), (res right left)
885 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
886 if Utils.debug_metas then
887 ignore (check_target context (snd eq_found) "buildnew1" );
889 let pos, equality = eq_found in
890 let (_, proof', (ty, what, other, _), menv',id') =
891 Equality.open_equality equality in
892 let what, other = if pos = Utils.Left then what, other else other, what in
894 let newgoal, newproof =
897 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
899 let name = C.Name "x" in
902 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
903 C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
904 S.lift 1 eq_ty; l; r]
908 (s,(Equality.SuperpositionRight,
909 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
911 let newmeta, newequality =
913 if ordering = U.Gt then newgoal, apply_subst s right
914 else apply_subst s left, newgoal in
915 let neworder = !Utils.compare_terms left right in
916 let newmenv = (* Inference.filter s *) m in
917 let stat = (eq_ty, left, right, neworder) in
919 let w = Utils.compute_equality_weight stat in
920 Equality.mk_equality (w, newproof, stat, newmenv) in
921 if Utils.debug_metas then
922 ignore (check_target context eq' "buildnew3");
923 let newm, eq' = Equality.fix_metas !maxmeta eq' in
924 if Utils.debug_metas then
925 ignore (check_target context eq' "buildnew4");
929 if Utils.debug_metas then
930 ignore(check_target context newequality "buildnew2");
933 let new1 = List.map (build_new U.Gt) res1
934 and new2 = List.map (build_new U.Lt) res2 in
935 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
937 (List.filter ok (new1 @ new2)))
940 (** demodulation, when the target is a theorem *)
941 let rec demodulation_theorem newmeta env table theorem =
942 let module C = Cic in
943 let module S = CicSubstitution in
944 let module M = CicMetaSubst in
945 let module HL = HelmLibraryObjects in
946 let metasenv, context, ugraph = env in
947 let maxmeta = ref newmeta in
948 let term, termty, metas = theorem in
949 let metasenv' = metas in
951 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
952 let pos, equality = eq_found in
953 let (_, proof', (ty, what, other, _), menv',id) =
954 Equality.open_equality equality in
955 let what, other = if pos = Utils.Left then what, other else other, what in
957 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
958 (* let bo' = apply_subst subst t in *)
959 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
962 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
963 Equality.BasicProof (Equality.empty_subst,term))
965 (Equality.build_proof_term_old newproofold, bo)
967 (* TODO, not ported to the new proofs *)
968 if true then assert false; term, bo
970 !maxmeta, (newterm, newty, menv)
973 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
977 let newmeta, newthm = build_newtheorem t in
978 let newt, newty, _ = newthm in
979 if Equality.meta_convertibility termty newty then
982 demodulation_theorem newmeta env table newthm
987 (*****************************************************************************)
988 (** OPERATIONS ON GOALS **)
990 (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
991 (*****************************************************************************)
995 | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
996 assert (LibraryObjects.is_eq_URI uri);
1001 let ty_of_goal (_,_,ty) = ty ;;
1003 (* checks if two goals are metaconvertible *)
1004 let goal_metaconvertibility_eq g1 g2 =
1005 Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
1008 (* when the betaexpand_term function is called on the left/right side of the
1009 * goal, the predicate has to be fixed
1010 * C[x] ---> (eq ty unchanged C[x])
1011 * [posu] is the side of the [unchanged] term in the original goal
1013 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1014 let _,_,eq,ty,l,r = open_goal goal in
1015 let unchanged = if posu = Utils.Left then l else r in
1016 let unchanged = CicSubstitution.lift 1 unchanged in
1017 let ty = CicSubstitution.lift 1 ty in
1020 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1021 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1023 (pred, subst, menv, ug, eq_f)
1026 (* ginve the old [goal], the side that has not changed [posu] and the
1027 * expansion builds a new goal *)
1028 let build_newgoal context goal posu rule expansion =
1029 let goalproof,_,_,_,_,_ = open_goal goal in
1030 let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal posu expansion in
1031 let pos, equality = eq_found in
1032 let (_, proof', (ty, what, other, _), menv',id) =
1033 Equality.open_equality equality in
1034 let what, other = if pos = Utils.Left then what, other else other, what in
1035 let newterm, newgoalproof =
1037 Utils.guarded_simpl context
1038 (apply_subst subst (CicSubstitution.subst other t))
1040 let bo' = (*apply_subst subst*) t in
1041 let name = Cic.Name "x" in
1042 let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
1043 bo, (newgoalproofstep::goalproof)
1045 let newmetasenv = (* Inference.filter subst *) menv in
1046 (newgoalproof, newmetasenv, newterm)
1051 returns a list of new clauses inferred with a left superposition step
1052 the negative equation "target" and one of the positive equations in "table"
1054 let superposition_left (metasenv, context, ugraph) table goal =
1055 let proof,menv,eq,ty,l,r = open_goal goal in
1057 Utils.compare_weights ~normalize:true
1058 (Utils.weight_of_term l) (Utils.weight_of_term r)
1060 let big,small,possmall =
1061 match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
1063 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1064 List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
1067 (** demodulation, when the target is a goal *)
1068 let rec demodulation_goal 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 menv context ugraph table 0 right in
1077 build_newgoal context goal Utils.Left Equality.Demodulation t
1079 if goal_metaconvertibility_eq goal newg then
1082 true, snd (demodulation_goal env table newg)
1083 | None -> false, goal
1085 let resleft = demodulation_aux menv context ugraph table 0 left in
1088 let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
1089 if goal_metaconvertibility_eq goal newg then
1092 true, snd (demodulation_goal env table newg)
1093 | None -> do_right ()
1096 let get_stats () = <:show<Indexing.>> ;;