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 =
734 (fun arg (res, lifted_tl) ->
737 let arg_res, lifted_arg =
738 betaexpand_term metasenv context ugraph table
742 (fun (t, s, m, ug, eq_found) ->
743 (Some t)::lifted_tl, s, m, ug, eq_found)
748 (fun (l, s, m, ug, eq_found) ->
749 (Some lifted_arg)::l, s, m, ug, eq_found)
751 (Some lifted_arg)::lifted_tl)
754 (fun (r, s, m, ug, eq_found) ->
755 None::r, s, m, ug, eq_found) res,
761 (fun (l, s, m, ug, eq_found) ->
762 (C.Meta (i, l), s, m, ug, eq_found)) l'
764 e, C.Meta (i, lifted_l)
767 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
769 | C.Prod (nn, s, t) ->
771 betaexpand_term metasenv context ugraph table lift_amount s in
773 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
774 table (lift_amount+1) t in
777 (fun (t, s, m, ug, eq_found) ->
778 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
781 (fun (t, s, m, ug, eq_found) ->
782 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
783 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
785 | C.Lambda (nn, s, t) ->
787 betaexpand_term metasenv context ugraph table lift_amount s in
789 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
790 table (lift_amount+1) t in
793 (fun (t, s, m, ug, eq_found) ->
794 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
797 (fun (t, s, m, ug, eq_found) ->
798 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
799 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
804 (fun arg (res, lifted_tl) ->
805 let arg_res, lifted_arg =
806 betaexpand_term metasenv context ugraph table lift_amount arg
810 (fun (a, s, m, ug, eq_found) ->
811 a::lifted_tl, s, m, ug, eq_found)
816 (fun (r, s, m, ug, eq_found) ->
817 lifted_arg::r, s, m, ug, eq_found)
819 lifted_arg::lifted_tl)
823 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
826 | t -> [], (S.lift lift_amount t)
829 | C.Meta (i, l) -> res, lifted_term
832 C.Implicit None, ugraph
833 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
835 let candidates = get_candidates Unification table term in
837 if subterms_only then
841 metasenv context ugraph lift_amount term termty candidates
848 returns a list of new clauses inferred with a right superposition step
849 between the positive equation "target" and one in the "table" "newmeta" is
850 the first free meta index, i.e. the first number above the highest meta
851 index: its updated value is also returned
853 let superposition_right
854 ?(subterms_only=false) newmeta (metasenv, context, ugraph) table target
856 let module C = Cic in
857 let module S = CicSubstitution in
858 let module M = CicMetaSubst in
859 let module HL = HelmLibraryObjects in
860 let module CR = CicReduction in
861 let module U = Utils in
862 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
863 Equality.open_equality target
865 if Utils.debug_metas then
866 ignore (check_target context target "superpositionright");
867 let metasenv' = newmetas in
868 let maxmeta = ref newmeta in
872 fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
874 [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
878 (fun (_, subst, _, _, _) ->
879 let subst = apply_subst subst in
880 let o = !Utils.compare_terms (subst l) (subst r) in
881 o <> U.Lt && o <> U.Le)
882 (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
884 (res left right), (res right left)
886 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
887 if Utils.debug_metas then
888 ignore (check_target context (snd eq_found) "buildnew1" );
890 let pos, equality = eq_found in
891 let (_, proof', (ty, what, other, _), menv',id') =
892 Equality.open_equality equality in
893 let what, other = if pos = Utils.Left then what, other else other, what in
895 let newgoal, newproof =
898 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
900 let name = C.Name "x" in
903 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
904 C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
905 S.lift 1 eq_ty; l; r]
909 (s,(Equality.SuperpositionRight,
910 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
912 let newmeta, newequality =
914 if ordering = U.Gt then newgoal, apply_subst s right
915 else apply_subst s left, newgoal in
916 let neworder = !Utils.compare_terms left right in
917 let newmenv = (* Inference.filter s *) m in
918 let stat = (eq_ty, left, right, neworder) in
920 let w = Utils.compute_equality_weight stat in
921 Equality.mk_equality (w, newproof, stat, newmenv) in
922 if Utils.debug_metas then
923 ignore (check_target context eq' "buildnew3");
924 let newm, eq' = Equality.fix_metas !maxmeta eq' in
925 if Utils.debug_metas then
926 ignore (check_target context eq' "buildnew4");
930 if Utils.debug_metas then
931 ignore(check_target context newequality "buildnew2");
934 let new1 = List.map (build_new U.Gt) res1
935 and new2 = List.map (build_new U.Lt) res2 in
936 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
938 (List.filter ok (new1 @ new2)))
941 (** demodulation, when the target is a theorem *)
942 let rec demodulation_theorem newmeta env table theorem =
943 let module C = Cic in
944 let module S = CicSubstitution in
945 let module M = CicMetaSubst in
946 let module HL = HelmLibraryObjects in
947 let metasenv, context, ugraph = env in
948 let maxmeta = ref newmeta in
949 let term, termty, metas = theorem in
950 let metasenv' = metas in
952 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
953 let pos, equality = eq_found in
954 let (_, proof', (ty, what, other, _), menv',id) =
955 Equality.open_equality equality in
956 let what, other = if pos = Utils.Left then what, other else other, what in
958 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
959 (* let bo' = apply_subst subst t in *)
960 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
963 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
964 Equality.BasicProof (Equality.empty_subst,term))
966 (Equality.build_proof_term_old newproofold, bo)
968 (* TODO, not ported to the new proofs *)
969 if true then assert false; term, bo
971 !maxmeta, (newterm, newty, menv)
974 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
978 let newmeta, newthm = build_newtheorem t in
979 let newt, newty, _ = newthm in
980 if Equality.meta_convertibility termty newty then
983 demodulation_theorem newmeta env table newthm
988 (*****************************************************************************)
989 (** OPERATIONS ON GOALS **)
991 (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
992 (*****************************************************************************)
996 | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
997 assert (LibraryObjects.is_eq_URI uri);
1002 let ty_of_goal (_,_,ty) = ty ;;
1004 (* checks if two goals are metaconvertible *)
1005 let goal_metaconvertibility_eq g1 g2 =
1006 Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
1009 (* when the betaexpand_term function is called on the left/right side of the
1010 * goal, the predicate has to be fixed
1011 * C[x] ---> (eq ty unchanged C[x])
1012 * [posu] is the side of the [unchanged] term in the original goal
1014 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1015 let _,_,eq,ty,l,r = open_goal goal in
1016 let unchanged = if posu = Utils.Left then l else r in
1017 let unchanged = CicSubstitution.lift 1 unchanged in
1018 let ty = CicSubstitution.lift 1 ty in
1021 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1022 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1024 (pred, subst, menv, ug, eq_f)
1027 (* ginve the old [goal], the side that has not changed [posu] and the
1028 * expansion builds a new goal *)
1029 let build_newgoal context goal posu rule expansion =
1030 let goalproof,_,_,_,_,_ = open_goal goal in
1031 let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal posu expansion in
1032 let pos, equality = eq_found in
1033 let (_, proof', (ty, what, other, _), menv',id) =
1034 Equality.open_equality equality in
1035 let what, other = if pos = Utils.Left then what, other else other, what in
1036 let newterm, newgoalproof =
1038 Utils.guarded_simpl context
1039 (apply_subst subst (CicSubstitution.subst other t))
1041 let bo' = (*apply_subst subst*) t in
1042 let name = Cic.Name "x" in
1043 let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
1044 bo, (newgoalproofstep::goalproof)
1046 let newmetasenv = (* Inference.filter subst *) menv in
1047 (newgoalproof, newmetasenv, newterm)
1052 returns a list of new clauses inferred with a left superposition step
1053 the negative equation "target" and one of the positive equations in "table"
1055 let superposition_left (metasenv, context, ugraph) table goal =
1056 let proof,menv,eq,ty,l,r = open_goal goal in
1058 Utils.compare_weights ~normalize:true
1059 (Utils.weight_of_term l) (Utils.weight_of_term r)
1062 if c = Utils.Incomparable then
1063 let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1064 let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1065 prerr_endline "ZZZ";
1066 prerr_endline (string_of_int (List.length expansionsl));
1067 prerr_endline (string_of_int (List.length expansionsr));
1068 List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1070 List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1073 let big,small,possmall =
1074 match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
1076 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1077 List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
1080 (** demodulation, when the target is a goal *)
1081 let rec demodulation_goal env table goal =
1082 let goalproof,menv,_,_,left,right = open_goal goal in
1083 let _, context, ugraph = env in
1084 (* let term = Utils.guarded_simpl (~debug:true) context term in*)
1086 let resright = demodulation_aux menv context ugraph table 0 right in
1090 build_newgoal context goal Utils.Left Equality.Demodulation t
1092 if goal_metaconvertibility_eq goal newg then
1095 true, snd (demodulation_goal env table newg)
1096 | None -> false, goal
1098 let resleft = demodulation_aux menv context ugraph table 0 left in
1101 let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
1102 if goal_metaconvertibility_eq goal newg then
1105 true, snd (demodulation_goal env table newg)
1106 | None -> do_right ()
1109 let get_stats () = <:show<Indexing.>> ;;