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 bag 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 bag 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 (Founif.build_proof_term proof) CicUniv.empty_ugraph)
157 prerr_endline (Founif.string_of_proof proof);
158 prerr_endline (CicPp.ppterm (Founif.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 Index.retrieve_generalizations tree term
185 Index.retrieve_unifiables tree term
188 Index.PosEqSet.elements s
192 finds the first equality in the index that matches "term", of type "termty"
193 termty can be Implicit if it is not needed. The result (one of the sides of
194 the equality, actually) should be not greater (wrt the term ordering) than
197 Format of the return value:
199 (term to substitute, [Cic.Rel 1 properly lifted - see the various
200 build_newtarget functions inside the various
201 demodulation_* functions]
202 substitution used for the matching,
204 ugraph, [substitution, metasenv and ugraph have the same meaning as those
205 returned by CicUnification.fo_unif]
206 (equality where the matching term was found, [i.e. the equality to use as
208 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
209 the equality: this is used to build the proof term, again see one of
210 the build_newtarget functions]
213 let rec find_matches bag metasenv context ugraph lift_amount term termty =
214 let module C = Cic in
215 let module U = Utils in
216 let module S = CicSubstitution in
217 let module M = CicMetaSubst in
218 let module HL = HelmLibraryObjects in
219 let cmp = !Utils.compare_terms in
220 let check = match termty with C.Implicit None -> false | _ -> true in
224 let pos, equality = candidate in
225 let (_, proof, (ty, left, right, o), metas,_) =
226 Equality.open_equality equality
228 if Utils.debug_metas then
229 ignore(check_target bag context (snd candidate) "find_matches");
230 if Utils.debug_res then
232 let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
233 let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
234 let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
237 (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
240 check_for_duplicates metas "gia nella metas";
241 check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*))
243 if check && not (fst (CicReduction.are_convertible
244 ~metasenv context termty ty ugraph)) then (
245 find_matches bag metasenv context ugraph lift_amount term termty tl
248 let subst', metasenv', ugraph' =
250 metasenv metas context term (S.lift lift_amount c) ugraph
252 Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
255 if pos = Utils.Left then left, right
258 if o <> U.Incomparable then
262 with Founif.MatchingFailure ->
263 find_matches bag metasenv context ugraph lift_amount term termty tl
265 if Utils.debug_res then ignore (check_res res "find1");
270 with Founif.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 bag 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 Founif.matching or Inference.unification
297 let rec find_all_matches ?(unif_fun=Founif.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
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)
317 if pos = Utils.Left then left, right
320 if o <> U.Incomparable then
322 let res = do_match c in
323 res::(find_all_matches ~unif_fun metasenv context ugraph
324 lift_amount term termty tl)
326 | Founif.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 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 | Founif.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 (Founif.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 _, context, ugraph = env in
374 let metasenv = tmetas in
375 let predicate, unif_fun =
376 if use_unification then
377 Unification, Founif.unification
379 Matching, Founif.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 leftorright = 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
401 | None -> ok what leftorright tl
402 | Some s -> Some (s, equation, leftorright <> pos ))
404 | Founif.MatchingFailure
405 | CicUnification.UnificationFailure _ -> ok what leftorright tl
407 match ok right Utils.Left 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
418 ok left Utils.Right rightr
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 bag ?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 bag 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 bag ~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 bag ~from:"2"
482 metasenv context ugraph table lift_amount s in (
486 demodulation_aux bag 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 bag 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 bag ?from eq_uri newmeta env table 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 bag 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) =
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 bag 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 (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
579 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
580 (Cic.Lambda (name, ty, bo'))))))
582 let newmenv = menv in
583 let left, right = if is_left then newterm, right else left, newterm in
584 let ordering = !Utils.compare_terms left right in
585 let stat = (eq_ty, left, right, ordering) in
587 let w = Utils.compute_equality_weight stat in
588 (Equality.mk_equality bag (w, newproof, stat,newmenv))
590 if Utils.debug_metas then
591 ignore(check_target bag context res "buildnew_target output");
596 demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left
598 if Utils.debug_res then check_res res "demod result";
599 let newmeta, newtarget =
602 let newmeta, newtarget = build_newtarget true t in
603 assert (not (Equality.meta_convertibility_eq target newtarget));
604 if (Equality.is_weak_identity newtarget) (* || *)
605 (*Equality.meta_convertibility_eq target newtarget*) then
608 demodulation_equality bag ?from eq_uri newmeta env table newtarget
610 let res = demodulation_aux bag metasenv' context ugraph table 0 right in
611 if Utils.debug_res then check_res res "demod result 1";
614 let newmeta, newtarget = build_newtarget false t in
615 if (Equality.is_weak_identity newtarget) ||
616 (Equality.meta_convertibility_eq target newtarget) then
619 demodulation_equality bag ?from eq_uri newmeta env table newtarget
623 (* newmeta, newtarget *)
628 Performs the beta expansion of the term "term" w.r.t. "table",
629 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
632 let rec betaexpand_term
633 ?(subterms_only=false) metasenv context ugraph table lift_amount term
635 let module C = Cic in
636 let module S = CicSubstitution in
637 let module M = CicMetaSubst in
638 let module HL = HelmLibraryObjects in
640 let res, lifted_term =
646 (fun arg (res, lifted_tl) ->
649 let arg_res, lifted_arg =
650 betaexpand_term metasenv context ugraph table
654 (fun (t, s, m, ug, eq_found) ->
655 (Some t)::lifted_tl, s, m, ug, eq_found)
660 (fun (l, s, m, ug, eq_found) ->
661 (Some lifted_arg)::l, s, m, ug, eq_found)
663 (Some lifted_arg)::lifted_tl)
666 (fun (r, s, m, ug, eq_found) ->
667 None::r, s, m, ug, eq_found) res,
673 (fun (l, s, m, ug, eq_found) ->
674 (C.Meta (i, l), s, m, ug, eq_found)) l'
676 e, C.Meta (i, lifted_l)
679 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
681 | C.Prod (nn, s, t) ->
683 betaexpand_term metasenv context ugraph table lift_amount s in
685 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
686 table (lift_amount+1) t in
689 (fun (t, s, m, ug, eq_found) ->
690 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
693 (fun (t, s, m, ug, eq_found) ->
694 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
695 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
697 | C.Lambda (nn, s, t) ->
699 betaexpand_term metasenv context ugraph table lift_amount s in
701 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
702 table (lift_amount+1) t in
705 (fun (t, s, m, ug, eq_found) ->
706 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
709 (fun (t, s, m, ug, eq_found) ->
710 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
711 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
716 (fun (res, lifted_tl) arg ->
717 let arg_res, lifted_arg =
718 betaexpand_term metasenv context ugraph table lift_amount arg
722 (fun (a, s, m, ug, eq_found) ->
723 a::lifted_tl, s, m, ug, eq_found)
728 (fun (r, s, m, ug, eq_found) ->
729 lifted_arg::r, s, m, ug, eq_found)
731 lifted_arg::lifted_tl)
732 ) ([], []) (List.rev l)
735 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
738 | t -> [], (S.lift lift_amount t)
741 | C.Meta (i, l) -> res, lifted_term
744 C.Implicit None, ugraph
745 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
747 let candidates = get_candidates Unification table term in
749 if subterms_only then
753 metasenv context ugraph lift_amount term termty candidates
760 returns a list of new clauses inferred with a right superposition step
761 between the positive equation "target" and one in the "table" "newmeta" is
762 the first free meta index, i.e. the first number above the highest meta
763 index: its updated value is also returned
765 let superposition_right bag
766 ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
767 let module C = Cic in
768 let module S = CicSubstitution in
769 let module M = CicMetaSubst in
770 let module HL = HelmLibraryObjects in
771 let module CR = CicReduction in
772 let module U = Utils in
773 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
774 Equality.open_equality target
776 if Utils.debug_metas then
777 ignore (check_target bag context target "superpositionright");
778 let metasenv' = newmetas in
779 let maxmeta = ref newmeta in
783 fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
785 [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
789 (fun (_, subst, _, _, _) ->
790 let subst = apply_subst subst in
791 let o = !Utils.compare_terms (subst l) (subst r) in
792 o <> U.Lt && o <> U.Le)
793 (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
795 (res left right), (res right left)
797 let build_new ordering (bo, s, m, ug, eq_found) =
798 if Utils.debug_metas then
799 ignore (check_target bag context (snd eq_found) "buildnew1" );
801 let pos, equality = eq_found in
802 let (_, proof', (ty, what, other, _), menv',id') =
803 Equality.open_equality equality in
804 let what, other = if pos = Utils.Left then what, other else other, what in
806 let newgoal, newproof =
809 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
811 let name = C.Name "x" in
814 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
815 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
819 (s,(Equality.SuperpositionRight,
820 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
822 let newmeta, newequality =
824 if ordering = U.Gt then newgoal, apply_subst s right
825 else apply_subst s left, newgoal in
826 let neworder = !Utils.compare_terms left right in
827 let newmenv = (* Founif.filter s *) m in
828 let stat = (eq_ty, left, right, neworder) in
830 let w = Utils.compute_equality_weight stat in
831 Equality.mk_equality bag (w, newproof, stat, newmenv) in
832 if Utils.debug_metas then
833 ignore (check_target bag context eq' "buildnew3");
834 let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
835 if Utils.debug_metas then
836 ignore (check_target bag context eq' "buildnew4");
840 if Utils.debug_metas then
841 ignore(check_target bag context newequality "buildnew2");
844 let new1 = List.map (build_new U.Gt) res1
845 and new2 = List.map (build_new U.Lt) res2 in
846 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
848 (List.filter ok (new1 @ new2)))
851 (** demodulation, when the target is a theorem *)
852 let rec demodulation_theorem bag newmeta env table theorem =
853 let module C = Cic in
854 let module S = CicSubstitution in
855 let module M = CicMetaSubst in
856 let module HL = HelmLibraryObjects in
857 let metasenv, context, ugraph = env in
858 let maxmeta = ref newmeta in
859 let term, termty, metas = theorem in
860 let metasenv' = metas in
862 let build_newtheorem (t, subst, menv, ug, eq_found) =
863 let pos, equality = eq_found in
864 let (_, proof', (ty, what, other, _), menv',id) =
865 Equality.open_equality equality in
866 let what, other = if pos = Utils.Left then what, other else other, what in
868 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
869 (* let bo' = apply_subst subst t in *)
870 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
873 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
874 Equality.BasicProof (Equality.empty_subst,term))
876 (Equality.build_proof_term_old newproofold, bo)
878 (* TODO, not ported to the new proofs *)
879 if true then assert false; term, bo
881 !maxmeta, (newterm, newty, menv)
884 demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty
888 let newmeta, newthm = build_newtheorem t in
889 let newt, newty, _ = newthm in
890 if Equality.meta_convertibility termty newty then
893 demodulation_theorem bag newmeta env table newthm
898 (*****************************************************************************)
899 (** OPERATIONS ON GOALS **)
901 (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
902 (*****************************************************************************)
906 | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
907 assert (LibraryObjects.is_eq_URI uri);
912 let ty_of_goal (_,_,ty) = ty ;;
914 (* checks if two goals are metaconvertible *)
915 let goal_metaconvertibility_eq g1 g2 =
916 Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
919 (* when the betaexpand_term function is called on the left/right side of the
920 * goal, the predicate has to be fixed
921 * C[x] ---> (eq ty unchanged C[x])
922 * [posu] is the side of the [unchanged] term in the original goal
924 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
925 let _,_,eq,ty,l,r = open_goal goal in
926 let unchanged = if posu = Utils.Left then l else r in
927 let unchanged = CicSubstitution.lift 1 unchanged in
928 let ty = CicSubstitution.lift 1 ty in
931 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
932 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
934 (pred, subst, menv, ug, eq_f)
937 (* ginve the old [goal], the side that has not changed [posu] and the
938 * expansion builds a new goal *)
939 let build_newgoal bag context goal posu rule expansion =
940 let goalproof,_,_,_,_,_ = open_goal goal in
941 let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
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
946 let newterm, newgoalproof =
948 Utils.guarded_simpl context
949 (apply_subst subst (CicSubstitution.subst other t))
951 let bo' = (*apply_subst subst*) t in
952 let name = Cic.Name "x" in
953 let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
954 bo, (newgoalproofstep::goalproof)
956 let newmetasenv = (* Founif.filter subst *) menv in
957 (newgoalproof, newmetasenv, newterm)
962 returns a list of new clauses inferred with a left superposition step
963 the negative equation "target" and one of the positive equations in "table"
965 let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
966 let names = Utils.names_of_context context in
967 let proof,menv,eq,ty,l,r = open_goal goal in
968 let c = !Utils.compare_terms l r in
970 if c = Utils.Incomparable then
972 let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
973 let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
974 (* prerr_endline "incomparable";
975 prerr_endline (string_of_int (List.length expansionsl));
976 prerr_endline (string_of_int (List.length expansionsr));
978 List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
980 List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
984 | Utils.Gt -> (* prerr_endline "GT"; *)
985 let big,small,possmall = l,r,Utils.Right in
986 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
988 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
990 | Utils.Lt -> (* prerr_endline "LT"; *)
991 let big,small,possmall = r,l,Utils.Left in
992 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
994 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
999 ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1002 (* rinfresco le meta *)
1005 let max,g = Equality.fix_metas_goal max g in max,g::acc)
1006 newgoals (maxmeta,[])
1009 (** demodulation, when the target is a goal *)
1010 let rec demodulation_goal bag env table goal =
1011 let goalproof,menv,_,_,left,right = open_goal goal in
1012 let _, context, ugraph = env in
1013 (* let term = Utils.guarded_simpl (~debug:true) context term in*)
1015 let resright = demodulation_aux bag menv context ugraph table 0 right in
1019 build_newgoal bag context goal Utils.Left Equality.Demodulation t
1021 if goal_metaconvertibility_eq goal newg then
1024 true, snd (demodulation_goal bag env table newg)
1025 | None -> false, goal
1027 let resleft = demodulation_aux bag menv context ugraph table 0 left in
1030 let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
1031 if goal_metaconvertibility_eq goal newg then
1034 true, snd (demodulation_goal bag env table newg)
1035 | None -> do_right ()
1038 let get_stats () = "" ;;