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 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 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 (Inference.build_proof_term proof) CicUniv.empty_ugraph)
157 prerr_endline (Inference.string_of_proof proof);
158 prerr_endline (CicPp.ppterm (Inference.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 let _ = <:start<retrieve_generalizations>> in
184 <:stop<retrieve_generalizations
185 Index.retrieve_generalizations tree term
188 let _ = <:start<retrieve_unifiables>> in
189 <:stop<retrieve_unifiables
190 Index.retrieve_unifiables tree term
194 Index.PosEqSet.elements s
198 finds the first equality in the index that matches "term", of type "termty"
199 termty can be Implicit if it is not needed. The result (one of the sides of
200 the equality, actually) should be not greater (wrt the term ordering) than
203 Format of the return value:
205 (term to substitute, [Cic.Rel 1 properly lifted - see the various
206 build_newtarget functions inside the various
207 demodulation_* functions]
208 substitution used for the matching,
210 ugraph, [substitution, metasenv and ugraph have the same meaning as those
211 returned by CicUnification.fo_unif]
212 (equality where the matching term was found, [i.e. the equality to use as
214 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
215 the equality: this is used to build the proof term, again see one of
216 the build_newtarget functions]
219 let rec find_matches metasenv context ugraph lift_amount term termty =
220 let module C = Cic in
221 let module U = Utils in
222 let module S = CicSubstitution in
223 let module M = CicMetaSubst in
224 let module HL = HelmLibraryObjects in
225 let cmp = !Utils.compare_terms in
226 let check = match termty with C.Implicit None -> false | _ -> true in
230 let pos, equality = candidate in
231 let (_, proof, (ty, left, right, o), metas,_) =
232 Equality.open_equality equality
234 if Utils.debug_metas then
235 ignore(check_target context (snd candidate) "find_matches");
236 if Utils.debug_res then
238 let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
239 let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
240 let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
243 (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
246 check_for_duplicates metas "gia nella metas";
247 check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*))
249 if check && not (fst (CicReduction.are_convertible
250 ~metasenv context termty ty ugraph)) then (
251 find_matches metasenv context ugraph lift_amount term termty tl
254 let subst', metasenv', ugraph' =
256 metasenv metas context term (S.lift lift_amount c) ugraph
258 Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
261 if pos = Utils.Left then left, right
264 if o <> U.Incomparable then
268 with Inference.MatchingFailure ->
269 find_matches metasenv context ugraph lift_amount term termty tl
271 if Utils.debug_res then ignore (check_res res "find1");
276 with Inference.MatchingFailure -> None
278 if Utils.debug_res then ignore (check_res res "find2");
280 | Some (_, s, _, _, _) ->
281 let c' = apply_subst s c in
283 let other' = U.guarded_simpl context (apply_subst s other) in *)
284 let other' = apply_subst s other in
285 let order = cmp c' other' in
290 metasenv context ugraph lift_amount term termty tl
292 find_matches metasenv context ugraph lift_amount term termty tl
295 let find_matches metasenv context ugraph lift_amount term termty =
296 find_matches metasenv context ugraph lift_amount term termty
300 as above, but finds all the matching equalities, and the matching condition
301 can be either Inference.matching or Inference.unification
303 let rec find_all_matches ?(unif_fun=Inference.unification)
304 metasenv context ugraph lift_amount term termty =
305 let module C = Cic in
306 let module U = Utils in
307 let module S = CicSubstitution in
308 let module M = CicMetaSubst in
309 let module HL = HelmLibraryObjects in
310 let cmp = !Utils.compare_terms in
314 let pos, equality = candidate in
315 let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
317 let subst', metasenv', ugraph' =
318 unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
320 (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
323 if pos = Utils.Left then left, right
326 if o <> U.Incomparable then
328 let res = do_match c in
329 res::(find_all_matches ~unif_fun metasenv context ugraph
330 lift_amount term termty tl)
332 | Inference.MatchingFailure
333 | CicUnification.UnificationFailure _
334 | CicUnification.Uncertain _ ->
335 find_all_matches ~unif_fun metasenv context ugraph
336 lift_amount term termty tl
339 let res = do_match c in
342 let c' = apply_subst s c
343 and other' = apply_subst s other in
344 let order = cmp c' other' in
345 if order <> U.Lt && order <> U.Le then
346 res::(find_all_matches ~unif_fun metasenv context ugraph
347 lift_amount term termty tl)
349 find_all_matches ~unif_fun metasenv context ugraph
350 lift_amount term termty tl
352 | Inference.MatchingFailure
353 | CicUnification.UnificationFailure _
354 | CicUnification.Uncertain _ ->
355 find_all_matches ~unif_fun metasenv context ugraph
356 lift_amount term termty tl
360 ?unif_fun metasenv context ugraph lift_amount term termty l
363 ?unif_fun metasenv context ugraph lift_amount term termty l
364 (*prerr_endline "CANDIDATES:";
365 List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
366 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
370 returns true if target is subsumed by some equality in table
373 prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
374 ((pos,equation),_)) -> Equality.string_of_equality equation)l))
377 let subsumption_aux use_unification env table target =
378 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
379 let metasenv, context, ugraph = env in
380 let metasenv = tmetas in
381 let predicate, unif_fun =
382 if use_unification then
383 Unification, Inference.unification
385 Matching, Inference.matching
389 | Cic.Meta _ when not use_unification -> []
391 let leftc = get_candidates predicate table left in
392 find_all_matches ~unif_fun
393 metasenv context ugraph 0 left ty leftc
395 let rec ok what leftorright = function
397 | (_, subst, menv, ug, (pos,equation))::tl ->
398 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
400 let other = if pos = Utils.Left then r else l in
401 let what' = Subst.apply_subst subst what in
402 let other' = Subst.apply_subst subst other in
403 let subst', menv', ug' =
404 unif_fun metasenv m context what' other' ugraph
406 (match Subst.merge_subst_if_possible subst subst' with
407 | None -> ok what leftorright tl
408 | Some s -> Some (s, equation, leftorright <> pos ))
410 | Inference.MatchingFailure
411 | CicUnification.UnificationFailure _ -> ok what leftorright tl
413 match ok right Utils.Left leftr with
414 | Some _ as res -> res
418 | Cic.Meta _ when not use_unification -> []
420 let rightc = get_candidates predicate table right in
421 find_all_matches ~unif_fun
422 metasenv context ugraph 0 right ty rightc
424 ok left Utils.Right rightr
427 let subsumption x y z =
428 subsumption_aux false x y z
431 let unification x y z =
432 subsumption_aux true x y z
435 let rec demodulation_aux ?from ?(typecheck=false)
436 metasenv context ugraph table lift_amount term =
437 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
438 let module C = Cic in
439 let module S = CicSubstitution in
440 let module M = CicMetaSubst in
441 let module HL = HelmLibraryObjects in
444 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
452 CicTypeChecker.type_of_aux' metasenv context term ugraph
454 C.Implicit None, ugraph
457 find_matches metasenv context ugraph lift_amount term termty candidates
459 if Utils.debug_res then ignore(check_res res "demod1");
469 (res, tl @ [S.lift 1 t])
472 demodulation_aux ~from:"1" metasenv context ugraph table
476 | None -> (None, tl @ [S.lift 1 t])
477 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
482 | Some (_, subst, menv, ug, eq_found) ->
483 Some (C.Appl ll, subst, menv, ug, eq_found)
485 | C.Prod (nn, s, t) ->
487 demodulation_aux ~from:"2"
488 metasenv context ugraph table lift_amount s in (
492 demodulation_aux metasenv
493 ((Some (nn, C.Decl s))::context) ugraph
494 table (lift_amount+1) t
498 | Some (t', subst, menv, ug, eq_found) ->
499 Some (C.Prod (nn, (S.lift 1 s), t'),
500 subst, menv, ug, eq_found)
502 | Some (s', subst, menv, ug, eq_found) ->
503 Some (C.Prod (nn, s', (S.lift 1 t)),
504 subst, menv, ug, eq_found)
506 | C.Lambda (nn, s, t) ->
509 metasenv context ugraph table lift_amount s in (
513 demodulation_aux metasenv
514 ((Some (nn, C.Decl s))::context) ugraph
515 table (lift_amount+1) t
519 | Some (t', subst, menv, ug, eq_found) ->
520 Some (C.Lambda (nn, (S.lift 1 s), t'),
521 subst, menv, ug, eq_found)
523 | Some (s', subst, menv, ug, eq_found) ->
524 Some (C.Lambda (nn, s', (S.lift 1 t)),
525 subst, menv, ug, eq_found)
530 if Utils.debug_res then ignore(check_res res "demod_aux output");
536 (** demodulation, when target is an equality *)
537 let rec demodulation_equality ?from eq_uri newmeta env table sign target =
538 let module C = Cic in
539 let module S = CicSubstitution in
540 let module M = CicMetaSubst in
541 let module HL = HelmLibraryObjects in
542 let module U = Utils in
543 let metasenv, context, ugraph = env in
544 let w, proof, (eq_ty, left, right, order), metas, id =
545 Equality.open_equality target
547 (* first, we simplify *)
548 (* let right = U.guarded_simpl context right in *)
549 (* let left = U.guarded_simpl context left in *)
550 (* let order = !Utils.compare_terms left right in *)
551 (* let stat = (eq_ty, left, right, order) in *)
552 (* let w = Utils.compute_equality_weight stat in*)
553 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
554 if Utils.debug_metas then
555 ignore(check_target context target "demod equalities input");
556 let metasenv' = (* metasenv @ *) metas in
557 let maxmeta = ref newmeta in
559 let build_newtarget is_left (t, subst, menv, ug, eq_found) =
561 if Utils.debug_metas then
563 ignore(check_for_duplicates menv "input1");
564 ignore(check_disjoint_invariant subst menv "input2");
565 let substs = Subst.ppsubst subst in
566 ignore(check_target context (snd eq_found) ("input3" ^ substs))
568 let pos, equality = eq_found in
570 (ty, what, other, _), menv',id') = Equality.open_equality equality in
572 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
573 with CicUtil.Meta_not_found _ -> ty
575 let what, other = if pos = Utils.Left then what, other else other, what in
576 let newterm, newproof =
578 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
579 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
580 let name = C.Name "x" in
582 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
583 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
585 if sign = Utils.Positive then
586 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
587 (Cic.Lambda (name, ty, bo'))))))
592 prerr_endline "***************************************negative";
596 CicMkImplicit.identity_relocation_list_for_metavariable context in
597 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
598 (* print_newline (); *)
599 C.Meta (!maxmeta, irl)
604 if pos = Utils.Left then [ty; what; other]
605 else [ty; other; what]
607 Equality.ProofSymBlock (termlist, proof'_old)
609 let proof'_new' = assert false (* not implemented *) in
611 if pos = Utils.Left then what, other else other, what
615 (0, (proof'_new',proof'_old'),
616 (ty, other, what, Utils.Incomparable),menv')
621 (subst, eq_URI, (name, ty), bo',
622 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
624 assert false, (* not implemented *)
625 (match snd proof with
626 | Equality.BasicProof _ ->
627 (* print_endline "replacing a BasicProof"; *)
629 | Equality.ProofGoalBlock (_, parent_proof) ->
630 (* print_endline "replacing another ProofGoalBlock"; *)
631 Equality.ProofGoalBlock (pb, parent_proof)
635 C.Appl [C.MutConstruct (* reflexivity *)
636 (LibraryObjects.eq_URI (), 0, 1, []);
637 eq_ty; if is_left then right else left]
640 (assert false, (* not implemented *)
641 Equality.ProofGoalBlock
642 (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
646 let newmenv = (* Inference.filter subst *) menv in
649 if Utils.debug_metas then
650 try ignore(CicTypeChecker.type_of_aux'
652 (Equality.build_proof_term newproof) ugraph);
655 prerr_endline "sempre lui";
656 prerr_endline (Subst.ppsubst subst);
657 prerr_endline (CicPp.ppterm
658 (Equality.build_proof_term newproof));
659 prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
660 prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
661 prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
662 prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
663 prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
669 let left, right = if is_left then newterm, right else left, newterm in
670 let ordering = !Utils.compare_terms left right in
671 let stat = (eq_ty, left, right, ordering) in
673 let w = Utils.compute_equality_weight stat in
674 (Equality.mk_equality (w, newproof, stat,newmenv))
676 if Utils.debug_metas then
677 ignore(check_target context res "buildnew_target output");
681 let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
682 if Utils.debug_res then check_res res "demod result";
683 let newmeta, newtarget =
686 let newmeta, newtarget = build_newtarget true t in
687 assert (not (Equality.meta_convertibility_eq target newtarget));
688 if (Equality.is_weak_identity newtarget) ||
689 (Equality.meta_convertibility_eq target newtarget) then
692 demodulation_equality ?from eq_uri newmeta env table sign newtarget
694 let res = demodulation_aux metasenv' context ugraph table 0 right in
695 if Utils.debug_res then check_res res "demod result 1";
698 let newmeta, newtarget = build_newtarget false t in
699 if (Equality.is_weak_identity newtarget) ||
700 (Equality.meta_convertibility_eq target newtarget) then
703 demodulation_equality ?from eq_uri newmeta env table sign newtarget
707 (* newmeta, newtarget *)
712 Performs the beta expansion of the term "term" w.r.t. "table",
713 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
716 let rec betaexpand_term
717 ?(subterms_only=false) metasenv context ugraph table lift_amount term
719 let module C = Cic in
720 let module S = CicSubstitution in
721 let module M = CicMetaSubst in
722 let module HL = HelmLibraryObjects in
724 let res, lifted_term =
730 (fun arg (res, lifted_tl) ->
733 let arg_res, lifted_arg =
734 betaexpand_term metasenv context ugraph table
738 (fun (t, s, m, ug, eq_found) ->
739 (Some t)::lifted_tl, s, m, ug, eq_found)
744 (fun (l, s, m, ug, eq_found) ->
745 (Some lifted_arg)::l, s, m, ug, eq_found)
747 (Some lifted_arg)::lifted_tl)
750 (fun (r, s, m, ug, eq_found) ->
751 None::r, s, m, ug, eq_found) res,
757 (fun (l, s, m, ug, eq_found) ->
758 (C.Meta (i, l), s, m, ug, eq_found)) l'
760 e, C.Meta (i, lifted_l)
763 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
765 | C.Prod (nn, s, t) ->
767 betaexpand_term metasenv context ugraph table lift_amount s in
769 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
770 table (lift_amount+1) t in
773 (fun (t, s, m, ug, eq_found) ->
774 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
777 (fun (t, s, m, ug, eq_found) ->
778 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
779 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
781 | C.Lambda (nn, s, t) ->
783 betaexpand_term metasenv context ugraph table lift_amount s in
785 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
786 table (lift_amount+1) t in
789 (fun (t, s, m, ug, eq_found) ->
790 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
793 (fun (t, s, m, ug, eq_found) ->
794 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
795 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
800 (fun (res, lifted_tl) arg ->
801 let arg_res, lifted_arg =
802 betaexpand_term metasenv context ugraph table lift_amount arg
806 (fun (a, s, m, ug, eq_found) ->
807 a::lifted_tl, s, m, ug, eq_found)
812 (fun (r, s, m, ug, eq_found) ->
813 lifted_arg::r, s, m, ug, eq_found)
815 lifted_arg::lifted_tl)
816 ) ([], []) (List.rev l)
819 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
822 | t -> [], (S.lift lift_amount t)
825 | C.Meta (i, l) -> res, lifted_term
828 C.Implicit None, ugraph
829 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
831 let candidates = get_candidates Unification table term in
833 if subterms_only then
837 metasenv context ugraph lift_amount term termty candidates
844 returns a list of new clauses inferred with a right superposition step
845 between the positive equation "target" and one in the "table" "newmeta" is
846 the first free meta index, i.e. the first number above the highest meta
847 index: its updated value is also returned
849 let superposition_right
850 ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
851 let module C = Cic in
852 let module S = CicSubstitution in
853 let module M = CicMetaSubst in
854 let module HL = HelmLibraryObjects in
855 let module CR = CicReduction in
856 let module U = Utils in
857 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
858 Equality.open_equality target
860 if Utils.debug_metas then
861 ignore (check_target context target "superpositionright");
862 let metasenv' = newmetas in
863 let maxmeta = ref newmeta in
867 fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
869 [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
873 (fun (_, subst, _, _, _) ->
874 let subst = apply_subst subst in
875 let o = !Utils.compare_terms (subst l) (subst r) in
876 o <> U.Lt && o <> U.Le)
877 (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
879 (res left right), (res right left)
881 let build_new ordering (bo, s, m, ug, eq_found) =
882 if Utils.debug_metas then
883 ignore (check_target context (snd eq_found) "buildnew1" );
885 let pos, equality = eq_found in
886 let (_, proof', (ty, what, other, _), menv',id') =
887 Equality.open_equality equality in
888 let what, other = if pos = Utils.Left then what, other else other, what in
890 let newgoal, newproof =
893 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
895 let name = C.Name "x" in
898 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
899 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
903 (s,(Equality.SuperpositionRight,
904 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
906 let newmeta, newequality =
908 if ordering = U.Gt then newgoal, apply_subst s right
909 else apply_subst s left, newgoal in
910 let neworder = !Utils.compare_terms left right in
911 let newmenv = (* Inference.filter s *) m in
912 let stat = (eq_ty, left, right, neworder) in
914 let w = Utils.compute_equality_weight stat in
915 Equality.mk_equality (w, newproof, stat, newmenv) in
916 if Utils.debug_metas then
917 ignore (check_target context eq' "buildnew3");
918 let newm, eq' = Equality.fix_metas !maxmeta eq' in
919 if Utils.debug_metas then
920 ignore (check_target context eq' "buildnew4");
924 if Utils.debug_metas then
925 ignore(check_target context newequality "buildnew2");
928 let new1 = List.map (build_new U.Gt) res1
929 and new2 = List.map (build_new U.Lt) res2 in
930 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
932 (List.filter ok (new1 @ new2)))
935 (** demodulation, when the target is a theorem *)
936 let rec demodulation_theorem newmeta env table theorem =
937 let module C = Cic in
938 let module S = CicSubstitution in
939 let module M = CicMetaSubst in
940 let module HL = HelmLibraryObjects in
941 let metasenv, context, ugraph = env in
942 let maxmeta = ref newmeta in
943 let term, termty, metas = theorem in
944 let metasenv' = metas in
946 let build_newtheorem (t, subst, menv, ug, eq_found) =
947 let pos, equality = eq_found in
948 let (_, proof', (ty, what, other, _), menv',id) =
949 Equality.open_equality equality in
950 let what, other = if pos = Utils.Left then what, other else other, what in
952 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
953 (* let bo' = apply_subst subst t in *)
954 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
957 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
958 Equality.BasicProof (Equality.empty_subst,term))
960 (Equality.build_proof_term_old newproofold, bo)
962 (* TODO, not ported to the new proofs *)
963 if true then assert false; term, bo
965 !maxmeta, (newterm, newty, menv)
968 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
972 let newmeta, newthm = build_newtheorem t in
973 let newt, newty, _ = newthm in
974 if Equality.meta_convertibility termty newty then
977 demodulation_theorem newmeta env table newthm
982 (*****************************************************************************)
983 (** OPERATIONS ON GOALS **)
985 (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
986 (*****************************************************************************)
990 | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
991 assert (LibraryObjects.is_eq_URI uri);
996 let ty_of_goal (_,_,ty) = ty ;;
998 (* checks if two goals are metaconvertible *)
999 let goal_metaconvertibility_eq g1 g2 =
1000 Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
1003 (* when the betaexpand_term function is called on the left/right side of the
1004 * goal, the predicate has to be fixed
1005 * C[x] ---> (eq ty unchanged C[x])
1006 * [posu] is the side of the [unchanged] term in the original goal
1008 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1009 let _,_,eq,ty,l,r = open_goal goal in
1010 let unchanged = if posu = Utils.Left then l else r in
1011 let unchanged = CicSubstitution.lift 1 unchanged in
1012 let ty = CicSubstitution.lift 1 ty in
1015 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1016 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1018 (pred, subst, menv, ug, eq_f)
1021 (* ginve the old [goal], the side that has not changed [posu] and the
1022 * expansion builds a new goal *)
1023 let build_newgoal context goal posu rule expansion =
1024 let goalproof,_,_,_,_,_ = open_goal goal in
1025 let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
1026 let pos, equality = eq_found in
1027 let (_, proof', (ty, what, other, _), menv',id) =
1028 Equality.open_equality equality in
1029 let what, other = if pos = Utils.Left then what, other else other, what in
1030 let newterm, newgoalproof =
1032 Utils.guarded_simpl context
1033 (apply_subst subst (CicSubstitution.subst other t))
1035 let bo' = (*apply_subst subst*) t in
1036 let name = Cic.Name "x" in
1037 let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
1038 bo, (newgoalproofstep::goalproof)
1040 let newmetasenv = (* Inference.filter subst *) menv in
1041 (newgoalproof, newmetasenv, newterm)
1046 returns a list of new clauses inferred with a left superposition step
1047 the negative equation "target" and one of the positive equations in "table"
1049 let superposition_left (metasenv, context, ugraph) table goal maxmeta =
1050 let names = Utils.names_of_context context in
1051 let proof,menv,eq,ty,l,r = open_goal goal in
1052 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
1068 | Utils.Gt -> (* prerr_endline "GT"; *)
1069 let big,small,possmall = l,r,Utils.Right in
1070 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1072 (build_newgoal context goal possmall Equality.SuperpositionLeft)
1074 | Utils.Lt -> (* prerr_endline "LT"; *)
1075 let big,small,possmall = r,l,Utils.Left in
1076 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1078 (build_newgoal context goal possmall Equality.SuperpositionLeft)
1083 ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1086 (* rinfresco le meta *)
1089 let max,g = Equality.fix_metas_goal max g in max,g::acc)
1090 newgoals (maxmeta,[])
1093 (** demodulation, when the target is a goal *)
1094 let rec demodulation_goal env table goal =
1095 let goalproof,menv,_,_,left,right = open_goal goal in
1096 let _, context, ugraph = env in
1097 (* let term = Utils.guarded_simpl (~debug:true) context term in*)
1099 let resright = demodulation_aux menv context ugraph table 0 right in
1103 build_newgoal context goal Utils.Left Equality.Demodulation t
1105 if goal_metaconvertibility_eq goal newg then
1108 true, snd (demodulation_goal env table newg)
1109 | None -> false, goal
1111 let resleft = demodulation_aux menv context ugraph table 0 left in
1114 let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
1115 if goal_metaconvertibility_eq goal newg then
1118 true, snd (demodulation_goal env table newg)
1119 | None -> do_right ()
1122 let get_stats () = <:show<Indexing.>> ;;