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 other' = Subst.apply_subst subst other in
397 let subst', menv', ug' =
398 unif_fun metasenv m context what' other' ugraph
400 (match Subst.merge_subst_if_possible subst subst' with
402 | Some s -> Some (s, equation))
404 | Inference.MatchingFailure
405 | CicUnification.UnificationFailure _ -> ok what tl
407 match ok right leftr with
408 | Some _ as res -> res
412 | Cic.Meta _ when not use_unification -> []
414 let rightc = get_candidates predicate table right in
415 find_all_matches ~unif_fun
416 metasenv context ugraph 0 right ty rightc
421 let subsumption x y z =
422 subsumption_aux false x y z
425 let unification x y z =
426 subsumption_aux true x y z
429 let rec demodulation_aux ?from ?(typecheck=false)
430 metasenv context ugraph table lift_amount term =
431 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
432 let module C = Cic in
433 let module S = CicSubstitution in
434 let module M = CicMetaSubst in
435 let module HL = HelmLibraryObjects in
438 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
446 CicTypeChecker.type_of_aux' metasenv context term ugraph
448 C.Implicit None, ugraph
451 find_matches metasenv context ugraph lift_amount term termty candidates
453 if Utils.debug_res then ignore(check_res res "demod1");
463 (res, tl @ [S.lift 1 t])
466 demodulation_aux ~from:"1" metasenv context ugraph table
470 | None -> (None, tl @ [S.lift 1 t])
471 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
476 | Some (_, subst, menv, ug, eq_found) ->
477 Some (C.Appl ll, subst, menv, ug, eq_found)
479 | C.Prod (nn, s, t) ->
481 demodulation_aux ~from:"2"
482 metasenv context ugraph table lift_amount s in (
486 demodulation_aux metasenv
487 ((Some (nn, C.Decl s))::context) ugraph
488 table (lift_amount+1) t
492 | Some (t', subst, menv, ug, eq_found) ->
493 Some (C.Prod (nn, (S.lift 1 s), t'),
494 subst, menv, ug, eq_found)
496 | Some (s', subst, menv, ug, eq_found) ->
497 Some (C.Prod (nn, s', (S.lift 1 t)),
498 subst, menv, ug, eq_found)
500 | C.Lambda (nn, s, t) ->
503 metasenv context ugraph table lift_amount s in (
507 demodulation_aux metasenv
508 ((Some (nn, C.Decl s))::context) ugraph
509 table (lift_amount+1) t
513 | Some (t', subst, menv, ug, eq_found) ->
514 Some (C.Lambda (nn, (S.lift 1 s), t'),
515 subst, menv, ug, eq_found)
517 | Some (s', subst, menv, ug, eq_found) ->
518 Some (C.Lambda (nn, s', (S.lift 1 t)),
519 subst, menv, ug, eq_found)
524 if Utils.debug_res then ignore(check_res res "demod_aux output");
530 (** demodulation, when target is an equality *)
531 let rec demodulation_equality ?from newmeta env table sign target =
532 let module C = Cic in
533 let module S = CicSubstitution in
534 let module M = CicMetaSubst in
535 let module HL = HelmLibraryObjects in
536 let module U = Utils in
537 let metasenv, context, ugraph = env in
538 let w, proof, (eq_ty, left, right, order), metas, id =
539 Equality.open_equality target
541 (* first, we simplify *)
542 (* let right = U.guarded_simpl context right in *)
543 (* let left = U.guarded_simpl context left in *)
544 (* let order = !Utils.compare_terms left right in *)
545 (* let stat = (eq_ty, left, right, order) in *)
546 (* let w = Utils.compute_equality_weight stat in*)
547 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
548 if Utils.debug_metas then
549 ignore(check_target context target "demod equalities input");
550 let metasenv' = (* metasenv @ *) metas in
551 let maxmeta = ref newmeta in
553 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
555 if Utils.debug_metas then
557 ignore(check_for_duplicates menv "input1");
558 ignore(check_disjoint_invariant subst menv "input2");
559 let substs = Subst.ppsubst subst in
560 ignore(check_target context (snd eq_found) ("input3" ^ substs))
562 let pos, equality = eq_found in
564 (ty, what, other, _), menv',id') = Equality.open_equality equality in
566 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
567 with CicUtil.Meta_not_found _ -> ty
569 let what, other = if pos = Utils.Left then what, other else other, what in
570 let newterm, newproof =
572 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
573 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
574 let name = C.Name "x" in
576 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
577 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
578 S.lift 1 eq_ty; l; r]
580 if sign = Utils.Positive then
581 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
582 (Cic.Lambda (name, ty, bo'))))))
587 prerr_endline "***************************************negative";
591 CicMkImplicit.identity_relocation_list_for_metavariable context in
592 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
593 (* print_newline (); *)
594 C.Meta (!maxmeta, irl)
599 if pos = Utils.Left then [ty; what; other]
600 else [ty; other; what]
602 Equality.ProofSymBlock (termlist, proof'_old)
604 let proof'_new' = assert false (* not implemented *) in
606 if pos = Utils.Left then what, other else other, what
610 (0, (proof'_new',proof'_old'),
611 (ty, other, what, Utils.Incomparable),menv')
616 (subst, eq_URI, (name, ty), bo',
617 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
619 assert false, (* not implemented *)
620 (match snd proof with
621 | Equality.BasicProof _ ->
622 (* print_endline "replacing a BasicProof"; *)
624 | Equality.ProofGoalBlock (_, parent_proof) ->
625 (* print_endline "replacing another ProofGoalBlock"; *)
626 Equality.ProofGoalBlock (pb, parent_proof)
630 C.Appl [C.MutConstruct (* reflexivity *)
631 (LibraryObjects.eq_URI (), 0, 1, []);
632 eq_ty; if is_left then right else left]
635 (assert false, (* not implemented *)
636 Equality.ProofGoalBlock
637 (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
641 let newmenv = (* Inference.filter subst *) menv in
644 if Utils.debug_metas then
645 try ignore(CicTypeChecker.type_of_aux'
647 (Equality.build_proof_term newproof) ugraph);
650 prerr_endline "sempre lui";
651 prerr_endline (Subst.ppsubst subst);
652 prerr_endline (CicPp.ppterm
653 (Equality.build_proof_term newproof));
654 prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
655 prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
656 prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
657 prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
658 prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
664 let left, right = if is_left then newterm, right else left, newterm in
665 let ordering = !Utils.compare_terms left right in
666 let stat = (eq_ty, left, right, ordering) in
668 let w = Utils.compute_equality_weight stat in
669 (Equality.mk_equality (w, newproof, stat,newmenv))
671 if Utils.debug_metas then
672 ignore(check_target context res "buildnew_target output");
676 let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
677 if Utils.debug_res then check_res res "demod result";
678 let newmeta, newtarget =
681 let newmeta, newtarget = build_newtarget true t in
682 assert (not (Equality.meta_convertibility_eq target newtarget));
683 if (Equality.is_weak_identity newtarget) ||
684 (Equality.meta_convertibility_eq target newtarget) then
687 demodulation_equality ?from newmeta env table sign newtarget
689 let res = demodulation_aux metasenv' context ugraph table 0 right in
690 if Utils.debug_res then check_res res "demod result 1";
693 let newmeta, newtarget = build_newtarget false t in
694 if (Equality.is_weak_identity newtarget) ||
695 (Equality.meta_convertibility_eq target newtarget) then
698 demodulation_equality ?from newmeta env table sign newtarget
702 (* newmeta, newtarget *)
707 Performs the beta expansion of the term "term" w.r.t. "table",
708 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
711 let rec betaexpand_term
712 ?(subterms_only=false) metasenv context ugraph table lift_amount term
714 let module C = Cic in
715 let module S = CicSubstitution in
716 let module M = CicMetaSubst in
717 let module HL = HelmLibraryObjects in
719 let res, lifted_term =
724 (fun arg (res, lifted_tl) ->
727 let arg_res, lifted_arg =
728 betaexpand_term metasenv context ugraph table
732 (fun (t, s, m, ug, eq_found) ->
733 (Some t)::lifted_tl, s, m, ug, eq_found)
738 (fun (l, s, m, ug, eq_found) ->
739 (Some lifted_arg)::l, s, m, ug, eq_found)
741 (Some lifted_arg)::lifted_tl)
744 (fun (r, s, m, ug, eq_found) ->
745 None::r, s, m, ug, eq_found) res,
751 (fun (l, s, m, ug, eq_found) ->
752 (C.Meta (i, l), s, m, ug, eq_found)) l'
754 e, C.Meta (i, lifted_l)
757 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
759 | C.Prod (nn, s, t) ->
761 betaexpand_term metasenv context ugraph table lift_amount s in
763 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
764 table (lift_amount+1) t in
767 (fun (t, s, m, ug, eq_found) ->
768 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
771 (fun (t, s, m, ug, eq_found) ->
772 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
773 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
775 | C.Lambda (nn, s, t) ->
777 betaexpand_term metasenv context ugraph table lift_amount s in
779 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
780 table (lift_amount+1) t in
783 (fun (t, s, m, ug, eq_found) ->
784 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
787 (fun (t, s, m, ug, eq_found) ->
788 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
789 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
794 (fun arg (res, lifted_tl) ->
795 let arg_res, lifted_arg =
796 betaexpand_term metasenv context ugraph table lift_amount arg
800 (fun (a, s, m, ug, eq_found) ->
801 a::lifted_tl, s, m, ug, eq_found)
806 (fun (r, s, m, ug, eq_found) ->
807 lifted_arg::r, s, m, ug, eq_found)
809 lifted_arg::lifted_tl)
813 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
816 | t -> [], (S.lift lift_amount t)
819 | C.Meta (i, l) -> res, lifted_term
822 C.Implicit None, ugraph
823 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
825 let candidates = get_candidates Unification table term in
827 if subterms_only then
831 metasenv context ugraph lift_amount term termty candidates
838 returns a list of new clauses inferred with a right superposition step
839 between the positive equation "target" and one in the "table" "newmeta" is
840 the first free meta index, i.e. the first number above the highest meta
841 index: its updated value is also returned
843 let superposition_right
844 ?(subterms_only=false) newmeta (metasenv, context, ugraph) table target
846 let module C = Cic in
847 let module S = CicSubstitution in
848 let module M = CicMetaSubst in
849 let module HL = HelmLibraryObjects in
850 let module CR = CicReduction in
851 let module U = Utils in
852 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
853 Equality.open_equality target
855 if Utils.debug_metas then
856 ignore (check_target context target "superpositionright");
857 let metasenv' = newmetas in
858 let maxmeta = ref newmeta in
862 fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
864 [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
868 (fun (_, subst, _, _, _) ->
869 let subst = apply_subst subst in
870 let o = !Utils.compare_terms (subst l) (subst r) in
871 o <> U.Lt && o <> U.Le)
872 (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
874 (res left right), (res right left)
876 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
877 if Utils.debug_metas then
878 ignore (check_target context (snd eq_found) "buildnew1" );
880 let pos, equality = eq_found in
881 let (_, proof', (ty, what, other, _), menv',id') =
882 Equality.open_equality equality in
883 let what, other = if pos = Utils.Left then what, other else other, what in
885 let newgoal, newproof =
888 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
890 let name = C.Name "x" in
893 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
894 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
895 S.lift 1 eq_ty; l; r]
899 (s,(Equality.SuperpositionRight,
900 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
902 let newmeta, newequality =
904 if ordering = U.Gt then newgoal, apply_subst s right
905 else apply_subst s left, newgoal in
906 let neworder = !Utils.compare_terms left right in
907 let newmenv = (* Inference.filter s *) m in
908 let stat = (eq_ty, left, right, neworder) in
910 let w = Utils.compute_equality_weight stat in
911 Equality.mk_equality (w, newproof, stat, newmenv) in
912 if Utils.debug_metas then
913 ignore (check_target context eq' "buildnew3");
914 let newm, eq' = Equality.fix_metas !maxmeta eq' in
915 if Utils.debug_metas then
916 ignore (check_target context eq' "buildnew4");
920 if Utils.debug_metas then
921 ignore(check_target context newequality "buildnew2");
924 let new1 = List.map (build_new U.Gt) res1
925 and new2 = List.map (build_new U.Lt) res2 in
926 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
928 (List.filter ok (new1 @ new2)))
931 (** demodulation, when the target is a theorem *)
932 let rec demodulation_theorem newmeta env table theorem =
933 let module C = Cic in
934 let module S = CicSubstitution in
935 let module M = CicMetaSubst in
936 let module HL = HelmLibraryObjects in
937 let metasenv, context, ugraph = env in
938 let maxmeta = ref newmeta in
939 let term, termty, metas = theorem in
940 let metasenv' = metas in
942 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
943 let pos, equality = eq_found in
944 let (_, proof', (ty, what, other, _), menv',id) =
945 Equality.open_equality equality in
946 let what, other = if pos = Utils.Left then what, other else other, what in
948 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
949 (* let bo' = apply_subst subst t in *)
950 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
953 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
954 Equality.BasicProof (Equality.empty_subst,term))
956 (Equality.build_proof_term_old newproofold, bo)
958 (* TODO, not ported to the new proofs *)
959 if true then assert false; term, bo
961 !maxmeta, (newterm, newty, menv)
964 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
968 let newmeta, newthm = build_newtheorem t in
969 let newt, newty, _ = newthm in
970 if Equality.meta_convertibility termty newty then
973 demodulation_theorem newmeta env table newthm
978 (*****************************************************************************)
979 (** OPERATIONS ON GOALS **)
981 (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
982 (*****************************************************************************)
986 | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
987 assert (LibraryObjects.is_eq_URI uri);
992 let ty_of_goal (_,_,ty) = ty ;;
994 (* checks if two goals are metaconvertible *)
995 let goal_metaconvertibility_eq g1 g2 =
996 Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
999 (* when the betaexpand_term function is called on the left/right side of the
1000 * goal, the predicate has to be fixed
1001 * C[x] ---> (eq ty unchanged C[x])
1002 * [posu] is the side of the [unchanged] term in the original goal
1004 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1005 let _,_,eq,ty,l,r = open_goal goal in
1006 let unchanged = if posu = Utils.Left then l else r in
1007 let unchanged = CicSubstitution.lift 1 unchanged in
1008 let ty = CicSubstitution.lift 1 ty in
1011 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1012 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1014 (pred, subst, menv, ug, eq_f)
1017 (* ginve the old [goal], the side that has not changed [posu] and the
1018 * expansion builds a new goal *)
1019 let build_newgoal context goal posu rule expansion =
1020 let goalproof,_,_,_,_,_ = open_goal goal in
1021 let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal posu expansion in
1022 let pos, equality = eq_found in
1023 let (_, proof', (ty, what, other, _), menv',id) =
1024 Equality.open_equality equality in
1025 let what, other = if pos = Utils.Left then what, other else other, what in
1026 let newterm, newgoalproof =
1028 Utils.guarded_simpl context
1029 (apply_subst subst (CicSubstitution.subst other t))
1031 let bo' = (*apply_subst subst*) t in
1032 let name = Cic.Name "x" in
1033 let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
1034 bo, (newgoalproofstep::goalproof)
1036 let newmetasenv = (* Inference.filter subst *) menv in
1037 (newgoalproof, newmetasenv, newterm)
1042 returns a list of new clauses inferred with a left superposition step
1043 the negative equation "target" and one of the positive equations in "table"
1045 let superposition_left (metasenv, context, ugraph) table goal =
1046 let proof,menv,eq,ty,l,r = open_goal goal in
1048 Utils.compare_weights ~normalize:true
1049 (Utils.weight_of_term l) (Utils.weight_of_term r)
1051 let big,small,possmall =
1052 match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
1054 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1055 List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
1058 (** demodulation, when the target is a goal *)
1059 let rec demodulation_goal env table goal =
1060 let goalproof,menv,_,_,left,right = open_goal goal in
1061 let _, context, ugraph = env in
1062 (* let term = Utils.guarded_simpl (~debug:true) context term in*)
1064 let resright = demodulation_aux menv context ugraph table 0 right in
1068 build_newgoal context goal Utils.Left Equality.Demodulation t
1070 if goal_metaconvertibility_eq goal newg then
1073 true, snd (demodulation_goal env table newg)
1074 | None -> false, goal
1076 let resleft = demodulation_aux menv context ugraph table 0 left in
1079 let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
1080 if goal_metaconvertibility_eq goal newg then
1083 true, snd (demodulation_goal env table newg)
1084 | None -> do_right ()
1087 let get_stats () = <:show<Indexing.>> ;;