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 =
184 | Matching -> Index.retrieve_generalizations tree term
185 | Unification -> Index.retrieve_unifiables tree term
187 Index.PosEqSet.elements s
191 finds the first equality in the index that matches "term", of type "termty"
192 termty can be Implicit if it is not needed. The result (one of the sides of
193 the equality, actually) should be not greater (wrt the term ordering) than
196 Format of the return value:
198 (term to substitute, [Cic.Rel 1 properly lifted - see the various
199 build_newtarget functions inside the various
200 demodulation_* functions]
201 substitution used for the matching,
203 ugraph, [substitution, metasenv and ugraph have the same meaning as those
204 returned by CicUnification.fo_unif]
205 (equality where the matching term was found, [i.e. the equality to use as
207 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
208 the equality: this is used to build the proof term, again see one of
209 the build_newtarget functions]
212 let rec find_matches metasenv context ugraph lift_amount term termty =
213 let module C = Cic in
214 let module U = Utils in
215 let module S = CicSubstitution in
216 let module M = CicMetaSubst in
217 let module HL = HelmLibraryObjects in
218 let cmp = !Utils.compare_terms in
219 let check = match termty with C.Implicit None -> false | _ -> true in
223 let pos, equality = candidate in
224 let (_, proof, (ty, left, right, o), metas,_) =
225 Equality.open_equality equality
227 if Utils.debug_metas then
228 ignore(check_target context (snd candidate) "find_matches");
229 if Utils.debug_res then
231 let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
232 let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
233 let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
236 (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
239 check_for_duplicates metas "gia nella metas";
240 check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*))
242 if check && not (fst (CicReduction.are_convertible
243 ~metasenv context termty ty ugraph)) then (
244 find_matches metasenv context ugraph lift_amount term termty tl
246 let do_match c eq_URI =
247 let subst', metasenv', ugraph' =
249 metasenv metas context term (S.lift lift_amount c) ugraph
251 Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph',
254 let c, other, eq_URI =
255 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
256 else right, left, Utils.eq_ind_r_URI ()
258 if o <> U.Incomparable then
262 with Inference.MatchingFailure ->
263 find_matches metasenv context ugraph lift_amount term termty tl
265 if Utils.debug_res then ignore (check_res res "find1");
269 try do_match c eq_URI
270 with Inference.MatchingFailure -> None
272 if Utils.debug_res then ignore (check_res res "find2");
274 | Some (_, s, _, _, _) ->
275 let c' = apply_subst s c in
277 let other' = U.guarded_simpl context (apply_subst s other) in *)
278 let other' = apply_subst s other in
279 let order = cmp c' other' in
284 metasenv context ugraph lift_amount term termty tl
286 find_matches metasenv context ugraph lift_amount term termty tl
289 let find_matches metasenv context ugraph lift_amount term termty =
290 find_matches metasenv context ugraph lift_amount term termty
294 as above, but finds all the matching equalities, and the matching condition
295 can be either Inference.matching or Inference.unification
297 let rec find_all_matches ?(unif_fun=Inference.unification)
298 metasenv context ugraph lift_amount term termty =
299 let module C = Cic in
300 let module U = Utils in
301 let module S = CicSubstitution in
302 let module M = CicMetaSubst in
303 let module HL = HelmLibraryObjects in
304 let cmp = !Utils.compare_terms in
308 let pos, equality = candidate in
309 let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
310 let do_match c eq_URI =
311 let subst', metasenv', ugraph' =
312 unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
314 (C.Rel (1+lift_amount),subst',metasenv',ugraph',(candidate, eq_URI))
316 let c, other, eq_URI =
317 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
318 else right, left, Utils.eq_ind_r_URI ()
320 if o <> U.Incomparable then
322 let res = do_match c eq_URI in
323 res::(find_all_matches ~unif_fun metasenv context ugraph
324 lift_amount term termty tl)
326 | Inference.MatchingFailure
327 | CicUnification.UnificationFailure _
328 | CicUnification.Uncertain _ ->
329 find_all_matches ~unif_fun metasenv context ugraph
330 lift_amount term termty tl
333 let res = do_match c eq_URI in
336 let c' = apply_subst s c
337 and other' = apply_subst s other in
338 let order = cmp c' other' in
339 if order <> U.Lt && order <> U.Le then
340 res::(find_all_matches ~unif_fun metasenv context ugraph
341 lift_amount term termty tl)
343 find_all_matches ~unif_fun metasenv context ugraph
344 lift_amount term termty tl
346 | Inference.MatchingFailure
347 | CicUnification.UnificationFailure _
348 | CicUnification.Uncertain _ ->
349 find_all_matches ~unif_fun metasenv context ugraph
350 lift_amount term termty tl
354 ?unif_fun metasenv context ugraph lift_amount term termty l
357 ?unif_fun metasenv context ugraph lift_amount term termty l
358 (*prerr_endline "CANDIDATES:";
359 List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
360 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
364 returns true if target is subsumed by some equality in table
367 prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
368 ((pos,equation),_)) -> Equality.string_of_equality equation)l))
371 let subsumption_aux use_unification env table target =
372 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
373 let metasenv, context, ugraph = env in
374 let metasenv = tmetas in
375 let predicate, unif_fun =
376 if use_unification then
377 Unification, Inference.unification
379 Matching, Inference.matching
383 | Cic.Meta _ when not use_unification -> []
385 let leftc = get_candidates predicate table left in
386 find_all_matches ~unif_fun
387 metasenv context ugraph 0 left ty leftc
389 let rec ok what = function
391 | (_, subst, menv, ug, ((pos,equation),_))::tl ->
392 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
394 let other = if pos = Utils.Left then r else l in
395 let what' = Subst.apply_subst subst what in
396 let subst', menv', ug' =
397 unif_fun metasenv m context what' other ugraph
399 (match Subst.merge_subst_if_possible subst subst' with
401 | Some s -> Some (s, equation))
403 | Inference.MatchingFailure
404 | CicUnification.UnificationFailure _ -> ok what tl
406 match ok right leftr with
407 | Some _ as res -> res
411 | Cic.Meta _ when not use_unification -> []
413 let rightc = get_candidates predicate table right in
414 find_all_matches ~unif_fun
415 metasenv context ugraph 0 right ty rightc
420 let subsumption x y z =
421 subsumption_aux false x y z
424 let unification x y z =
425 subsumption_aux true x y z
428 let rec demodulation_aux ?from ?(typecheck=false)
429 metasenv context ugraph table lift_amount term =
430 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
431 let module C = Cic in
432 let module S = CicSubstitution in
433 let module M = CicMetaSubst in
434 let module HL = HelmLibraryObjects in
437 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
445 CicTypeChecker.type_of_aux' metasenv context term ugraph
447 C.Implicit None, ugraph
450 find_matches metasenv context ugraph lift_amount term termty candidates
452 if Utils.debug_res then ignore(check_res res "demod1");
462 (res, tl @ [S.lift 1 t])
465 demodulation_aux ~from:"1" metasenv context ugraph table
469 | None -> (None, tl @ [S.lift 1 t])
470 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
475 | Some (_, subst, menv, ug, eq_found) ->
476 Some (C.Appl ll, subst, menv, ug, eq_found)
478 | C.Prod (nn, s, t) ->
480 demodulation_aux ~from:"2"
481 metasenv context ugraph table lift_amount s in (
485 demodulation_aux metasenv
486 ((Some (nn, C.Decl s))::context) ugraph
487 table (lift_amount+1) t
491 | Some (t', subst, menv, ug, eq_found) ->
492 Some (C.Prod (nn, (S.lift 1 s), t'),
493 subst, menv, ug, eq_found)
495 | Some (s', subst, menv, ug, eq_found) ->
496 Some (C.Prod (nn, s', (S.lift 1 t)),
497 subst, menv, ug, eq_found)
499 | C.Lambda (nn, s, t) ->
502 metasenv context ugraph table lift_amount s in (
506 demodulation_aux metasenv
507 ((Some (nn, C.Decl s))::context) ugraph
508 table (lift_amount+1) t
512 | Some (t', subst, menv, ug, eq_found) ->
513 Some (C.Lambda (nn, (S.lift 1 s), t'),
514 subst, menv, ug, eq_found)
516 | Some (s', subst, menv, ug, eq_found) ->
517 Some (C.Lambda (nn, s', (S.lift 1 t)),
518 subst, menv, ug, eq_found)
523 if Utils.debug_res then ignore(check_res res "demod_aux output");
529 (** demodulation, when target is an equality *)
530 let rec demodulation_equality ?from newmeta env table sign target =
531 let module C = Cic in
532 let module S = CicSubstitution in
533 let module M = CicMetaSubst in
534 let module HL = HelmLibraryObjects in
535 let module U = Utils in
536 let metasenv, context, ugraph = env in
537 let w, proof, (eq_ty, left, right, order), metas, id =
538 Equality.open_equality target
540 (* first, we simplify *)
541 (* let right = U.guarded_simpl context right in *)
542 (* let left = U.guarded_simpl context left in *)
543 (* let order = !Utils.compare_terms left right in *)
544 (* let stat = (eq_ty, left, right, order) in *)
545 (* let w = Utils.compute_equality_weight stat in*)
546 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
547 if Utils.debug_metas then
548 ignore(check_target context target "demod equalities input");
549 let metasenv' = (* metasenv @ *) metas in
550 let maxmeta = ref newmeta in
552 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
554 if Utils.debug_metas then
556 ignore(check_for_duplicates menv "input1");
557 ignore(check_disjoint_invariant subst menv "input2");
558 let substs = Subst.ppsubst subst in
559 ignore(check_target context (snd eq_found) ("input3" ^ substs))
561 let pos, equality = eq_found in
563 (ty, what, other, _), menv',id') = Equality.open_equality equality in
565 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
566 with CicUtil.Meta_not_found _ -> ty
568 let what, other = if pos = Utils.Left then what, other else other, what in
569 let newterm, newproof =
571 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
572 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
573 let name = C.Name "x" in
575 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
576 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
577 S.lift 1 eq_ty; l; r]
579 if sign = Utils.Positive then
580 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
581 (Cic.Lambda (name, ty, bo'))))))
586 prerr_endline "***************************************negative";
590 CicMkImplicit.identity_relocation_list_for_metavariable context in
591 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
592 (* print_newline (); *)
593 C.Meta (!maxmeta, irl)
598 if pos = Utils.Left then [ty; what; other]
599 else [ty; other; what]
601 Equality.ProofSymBlock (termlist, proof'_old)
603 let proof'_new' = assert false (* not implemented *) in
605 if pos = Utils.Left then what, other else other, what
609 (0, (proof'_new',proof'_old'),
610 (ty, other, what, Utils.Incomparable),menv')
615 (subst, eq_URI, (name, ty), bo',
616 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
618 assert false, (* not implemented *)
619 (match snd proof with
620 | Equality.BasicProof _ ->
621 (* print_endline "replacing a BasicProof"; *)
623 | Equality.ProofGoalBlock (_, parent_proof) ->
624 (* print_endline "replacing another ProofGoalBlock"; *)
625 Equality.ProofGoalBlock (pb, parent_proof)
629 C.Appl [C.MutConstruct (* reflexivity *)
630 (LibraryObjects.eq_URI (), 0, 1, []);
631 eq_ty; if is_left then right else left]
634 (assert false, (* not implemented *)
635 Equality.ProofGoalBlock
636 (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
640 let newmenv = (* Inference.filter subst *) menv in
643 if Utils.debug_metas then
644 try ignore(CicTypeChecker.type_of_aux'
646 (Equality.build_proof_term newproof) ugraph);
649 prerr_endline "sempre lui";
650 prerr_endline (Subst.ppsubst subst);
651 prerr_endline (CicPp.ppterm
652 (Equality.build_proof_term newproof));
653 prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
654 prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
655 prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
656 prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
657 prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
663 let left, right = if is_left then newterm, right else left, newterm in
664 let ordering = !Utils.compare_terms left right in
665 let stat = (eq_ty, left, right, ordering) in
667 let w = Utils.compute_equality_weight stat in
668 (Equality.mk_equality (w, newproof, stat,newmenv))
670 if Utils.debug_metas then
671 ignore(check_target context res "buildnew_target output");
675 let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
676 if Utils.debug_res then check_res res "demod result";
677 let newmeta, newtarget =
680 let newmeta, newtarget = build_newtarget true t in
681 assert (not (Equality.meta_convertibility_eq target newtarget));
682 if (Equality.is_weak_identity newtarget) ||
683 (Equality.meta_convertibility_eq target newtarget) then
686 demodulation_equality ?from newmeta env table sign newtarget
688 let res = demodulation_aux metasenv' context ugraph table 0 right in
689 if Utils.debug_res then check_res res "demod result 1";
692 let newmeta, newtarget = build_newtarget false t in
693 if (Equality.is_weak_identity newtarget) ||
694 (Equality.meta_convertibility_eq target newtarget) then
697 demodulation_equality ?from newmeta env table sign newtarget
701 (* newmeta, newtarget *)
706 Performs the beta expansion of the term "term" w.r.t. "table",
707 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
710 let rec betaexpand_term
711 ?(subterms_only=false) metasenv context ugraph table lift_amount term
713 let module C = Cic in
714 let module S = CicSubstitution in
715 let module M = CicMetaSubst in
716 let module HL = HelmLibraryObjects in
718 let res, lifted_term =
723 (fun arg (res, lifted_tl) ->
726 let arg_res, lifted_arg =
727 betaexpand_term metasenv context ugraph table
731 (fun (t, s, m, ug, eq_found) ->
732 (Some t)::lifted_tl, s, m, ug, eq_found)
737 (fun (l, s, m, ug, eq_found) ->
738 (Some lifted_arg)::l, s, m, ug, eq_found)
740 (Some lifted_arg)::lifted_tl)
743 (fun (r, s, m, ug, eq_found) ->
744 None::r, s, m, ug, eq_found) res,
750 (fun (l, s, m, ug, eq_found) ->
751 (C.Meta (i, l), s, m, ug, eq_found)) l'
753 e, C.Meta (i, lifted_l)
756 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
758 | C.Prod (nn, s, t) ->
760 betaexpand_term metasenv context ugraph table lift_amount s in
762 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
763 table (lift_amount+1) t in
766 (fun (t, s, m, ug, eq_found) ->
767 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
770 (fun (t, s, m, ug, eq_found) ->
771 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
772 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
774 | C.Lambda (nn, s, t) ->
776 betaexpand_term metasenv context ugraph table lift_amount s in
778 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
779 table (lift_amount+1) t in
782 (fun (t, s, m, ug, eq_found) ->
783 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
786 (fun (t, s, m, ug, eq_found) ->
787 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
788 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
793 (fun arg (res, lifted_tl) ->
794 let arg_res, lifted_arg =
795 betaexpand_term metasenv context ugraph table lift_amount arg
799 (fun (a, s, m, ug, eq_found) ->
800 a::lifted_tl, s, m, ug, eq_found)
805 (fun (r, s, m, ug, eq_found) ->
806 lifted_arg::r, s, m, ug, eq_found)
808 lifted_arg::lifted_tl)
812 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
815 | t -> [], (S.lift lift_amount t)
818 | C.Meta (i, l) -> res, lifted_term
821 C.Implicit None, ugraph
822 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
824 let candidates = get_candidates Unification table term in
826 if subterms_only then
830 metasenv context ugraph lift_amount term termty candidates
837 returns a list of new clauses inferred with a right superposition step
838 between the positive equation "target" and one in the "table" "newmeta" is
839 the first free meta index, i.e. the first number above the highest meta
840 index: its updated value is also returned
842 let superposition_right
843 ?(subterms_only=false) newmeta (metasenv, context, ugraph) table target
845 let module C = Cic in
846 let module S = CicSubstitution in
847 let module M = CicMetaSubst in
848 let module HL = HelmLibraryObjects in
849 let module CR = CicReduction in
850 let module U = Utils in
851 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
852 Equality.open_equality target
854 if Utils.debug_metas then
855 ignore (check_target context target "superpositionright");
856 let metasenv' = newmetas in
857 let maxmeta = ref newmeta in
861 fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
863 [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
867 (fun (_, subst, _, _, _) ->
868 let subst = apply_subst subst in
869 let o = !Utils.compare_terms (subst l) (subst r) in
870 o <> U.Lt && o <> U.Le)
871 (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
873 (res left right), (res right left)
875 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
876 if Utils.debug_metas then
877 ignore (check_target context (snd eq_found) "buildnew1" );
879 let pos, equality = eq_found in
880 let (_, proof', (ty, what, other, _), menv',id') =
881 Equality.open_equality equality in
882 let what, other = if pos = Utils.Left then what, other else other, what in
884 let newgoal, newproof =
887 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
889 let name = C.Name "x" in
892 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
893 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
894 S.lift 1 eq_ty; l; r]
898 (s,(Equality.SuperpositionRight,
899 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
901 let newmeta, newequality =
903 if ordering = U.Gt then newgoal, apply_subst s right
904 else apply_subst s left, newgoal in
905 let neworder = !Utils.compare_terms left right in
906 let newmenv = (* Inference.filter s *) m in
907 let stat = (eq_ty, left, right, neworder) in
909 let w = Utils.compute_equality_weight stat in
910 Equality.mk_equality (w, newproof, stat, newmenv) in
911 if Utils.debug_metas then
912 ignore (check_target context eq' "buildnew3");
913 let newm, eq' = Equality.fix_metas !maxmeta eq' in
914 if Utils.debug_metas then
915 ignore (check_target context eq' "buildnew4");
919 if Utils.debug_metas then
920 ignore(check_target context newequality "buildnew2");
923 let new1 = List.map (build_new U.Gt) res1
924 and new2 = List.map (build_new U.Lt) res2 in
925 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
927 (List.filter ok (new1 @ new2)))
930 (** demodulation, when the target is a theorem *)
931 let rec demodulation_theorem newmeta env table theorem =
932 let module C = Cic in
933 let module S = CicSubstitution in
934 let module M = CicMetaSubst in
935 let module HL = HelmLibraryObjects in
936 let metasenv, context, ugraph = env in
937 let maxmeta = ref newmeta in
938 let term, termty, metas = theorem in
939 let metasenv' = metas in
941 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
942 let pos, equality = eq_found in
943 let (_, proof', (ty, what, other, _), menv',id) =
944 Equality.open_equality equality in
945 let what, other = if pos = Utils.Left then what, other else other, what in
947 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
948 (* let bo' = apply_subst subst t in *)
949 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
952 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
953 Equality.BasicProof (Equality.empty_subst,term))
955 (Equality.build_proof_term_old newproofold, bo)
957 (* TODO, not ported to the new proofs *)
958 if true then assert false; term, bo
960 !maxmeta, (newterm, newty, menv)
963 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
967 let newmeta, newthm = build_newtheorem t in
968 let newt, newty, _ = newthm in
969 if Equality.meta_convertibility termty newty then
972 demodulation_theorem newmeta env table newthm
977 (*****************************************************************************)
978 (** OPERATIONS ON GOALS **)
980 (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
981 (*****************************************************************************)
985 | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
986 assert (LibraryObjects.is_eq_URI uri);
991 let ty_of_goal (_,_,ty) = ty ;;
993 (* checks if two goals are metaconvertible *)
994 let goal_metaconvertibility_eq g1 g2 =
995 Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
998 (* when the betaexpand_term function is called on the left/right side of the
999 * goal, the predicate has to be fixed
1000 * C[x] ---> (eq ty unchanged C[x])
1001 * [posu] is the side of the [unchanged] term in the original goal
1003 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1004 let _,_,eq,ty,l,r = open_goal goal in
1005 let unchanged = if posu = Utils.Left then l else r in
1006 let unchanged = CicSubstitution.lift 1 unchanged in
1007 let ty = CicSubstitution.lift 1 ty in
1010 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1011 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1013 (pred, subst, menv, ug, eq_f)
1016 (* ginve the old [goal], the side that has not changed [posu] and the
1017 * expansion builds a new goal *)
1018 let build_newgoal context goal posu expansion =
1019 let goalproof,_,_,_,_,_ = open_goal goal in
1020 let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal posu expansion in
1021 let pos, equality = eq_found in
1022 let (_, proof', (ty, what, other, _), menv',id) =
1023 Equality.open_equality equality in
1024 let what, other = if pos = Utils.Left then what, other else other, what in
1025 let newterm, newgoalproof =
1027 Utils.guarded_simpl context
1028 (apply_subst subst (CicSubstitution.subst other t))
1030 let bo' = (*apply_subst subst*) t in
1031 let name = Cic.Name "x" in
1032 let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
1033 bo, (newgoalproofstep::goalproof)
1035 let newmetasenv = (* Inference.filter subst *) menv in
1036 (newgoalproof, newmetasenv, newterm)
1041 returns a list of new clauses inferred with a left superposition step
1042 the negative equation "target" and one of the positive equations in "table"
1044 let superposition_left (metasenv, context, ugraph) table goal =
1045 let proof,menv,eq,ty,l,r = open_goal goal in
1047 Utils.compare_weights ~normalize:true
1048 (Utils.weight_of_term l) (Utils.weight_of_term r)
1050 let big,small,possmall =
1051 match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
1053 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1054 List.map (build_newgoal context goal possmall) expansions
1057 (** demodulation, when the target is a goal *)
1058 let rec demodulation_goal env table goal =
1059 let goalproof,menv,_,_,left,right = open_goal goal in
1060 let metasenv, context, ugraph = env in
1061 (* let term = Utils.guarded_simpl (~debug:true) context term in*)
1063 let resright = demodulation_aux menv context ugraph table 0 right in
1066 let newg = build_newgoal context goal Utils.Left t in
1067 if goal_metaconvertibility_eq goal newg then
1070 true, snd (demodulation_goal env table newg)
1071 | None -> false, goal
1073 let resleft = demodulation_aux menv context ugraph table 0 left in
1076 let newg = build_newgoal context goal Utils.Right t in
1077 if goal_metaconvertibility_eq goal newg then
1080 true, snd (demodulation_goal env table newg)
1081 | None -> do_right ()
1084 let get_stats () = <:show<Indexing.>> ;;