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 (* XXX termty unused *)
298 let rec find_all_matches ?(unif_fun=Founif.unification)
299 metasenv context ugraph lift_amount term termty =
300 let module C = Cic in
301 let module U = Utils in
302 let module S = CicSubstitution in
303 let module M = CicMetaSubst in
304 let module HL = HelmLibraryObjects in
305 let cmp = !Utils.compare_terms in
309 let pos, equality = candidate in
310 let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
312 let subst', metasenv', ugraph' =
313 unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
315 (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
318 if pos = Utils.Left then left, right
321 if o <> U.Incomparable then
323 let res = do_match c in
324 res::(find_all_matches ~unif_fun metasenv context ugraph
325 lift_amount term termty tl)
327 | Founif.MatchingFailure
328 | CicUnification.UnificationFailure _
329 | CicUnification.Uncertain _ ->
330 find_all_matches ~unif_fun metasenv context ugraph
331 lift_amount term termty tl
334 let res = do_match c in
337 let c' = apply_subst s c
338 and other' = apply_subst s other in
339 let order = cmp c' other' in
340 if order <> U.Lt && order <> U.Le then
341 res::(find_all_matches ~unif_fun metasenv context ugraph
342 lift_amount term termty tl)
344 find_all_matches ~unif_fun metasenv context ugraph
345 lift_amount term termty tl
347 | Founif.MatchingFailure
348 | CicUnification.UnificationFailure _
349 | CicUnification.Uncertain _ ->
350 find_all_matches ~unif_fun metasenv context ugraph
351 lift_amount term termty tl
355 ?unif_fun metasenv context ugraph lift_amount term termty l
358 ?unif_fun metasenv context ugraph lift_amount term termty l
359 (*prerr_endline "CANDIDATES:";
360 List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
361 prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
365 returns true if target is subsumed by some equality in table
369 prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
370 ((pos,equation),_)) -> Equality.string_of_equality equation)l))
374 let subsumption_aux use_unification env table target =
375 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
376 let _, context, ugraph = env in
377 let metasenv = tmetas in
378 let predicate, unif_fun =
379 if use_unification then
380 Unification, Founif.unification
382 Matching, Founif.matching
386 | Cic.Meta _ when not use_unification -> []
388 let leftc = get_candidates predicate table left in
389 find_all_matches ~unif_fun
390 metasenv context ugraph 0 left ty leftc
392 let rec ok what leftorright = function
394 | (_, subst, menv, ug, (pos,equation))::tl ->
395 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
397 let other = if pos = Utils.Left then r else l in
398 let what' = Subst.apply_subst subst what in
399 let other' = Subst.apply_subst subst other in
400 let subst', menv', ug' =
401 unif_fun metasenv m context what' other' ugraph
403 (match Subst.merge_subst_if_possible subst subst' with
404 | None -> ok what leftorright tl
405 | Some s -> Some (s, equation, leftorright <> pos ))
407 | Founif.MatchingFailure
408 | CicUnification.UnificationFailure _ -> ok what leftorright tl
410 match ok right Utils.Left leftr with
411 | Some _ as res -> res
415 | Cic.Meta _ when not use_unification -> []
417 let rightc = get_candidates predicate table right in
418 find_all_matches ~unif_fun
419 metasenv context ugraph 0 right ty rightc
421 ok left Utils.Right rightr
424 let subsumption x y z =
425 subsumption_aux false x y z
428 let unification x y z =
429 subsumption_aux true x y z
432 let subsumption_aux_all use_unification env table target =
433 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
434 let _, context, ugraph = env in
435 let metasenv = tmetas in
436 let predicate, unif_fun =
437 if use_unification then
438 Unification, Founif.unification
440 Matching, Founif.matching
444 | Cic.Meta _ when not use_unification -> []
446 let leftc = get_candidates predicate table left in
447 find_all_matches ~unif_fun
448 metasenv context ugraph 0 left ty leftc
452 | Cic.Meta _ when not use_unification -> []
454 let rightc = get_candidates predicate table right in
455 find_all_matches ~unif_fun
456 metasenv context ugraph 0 right ty rightc
458 let rec ok_all what leftorright = function
460 | (_, subst, menv, ug, (pos,equation))::tl ->
461 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
463 let other = if pos = Utils.Left then r else l in
464 let what' = Subst.apply_subst subst what in
465 let other' = Subst.apply_subst subst other in
466 let subst', menv', ug' =
467 unif_fun metasenv m context what' other' ugraph
469 (match Subst.merge_subst_if_possible subst subst' with
470 | None -> ok_all what leftorright tl
472 (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
474 | Founif.MatchingFailure
475 | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
477 (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
480 let subsumption_all x y z =
481 subsumption_aux_all false x y z
484 let unification_all x y z =
485 subsumption_aux_all true x y z
487 let rec demodulation_aux bag ?from ?(typecheck=false)
488 metasenv context ugraph table lift_amount term =
489 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
490 let module C = Cic in
491 let module S = CicSubstitution in
492 let module M = CicMetaSubst in
493 let module HL = HelmLibraryObjects in
496 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
504 CicTypeChecker.type_of_aux' metasenv context term ugraph
506 C.Implicit None, ugraph
509 find_matches bag metasenv context ugraph lift_amount term termty candidates
511 if Utils.debug_res then ignore(check_res res "demod1");
521 (res, tl @ [S.lift 1 t])
524 demodulation_aux bag ~from:"1" metasenv context ugraph table
528 | None -> (None, tl @ [S.lift 1 t])
529 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
534 | Some (_, subst, menv, ug, eq_found) ->
535 Some (C.Appl ll, subst, menv, ug, eq_found)
537 | C.Prod (nn, s, t) ->
539 demodulation_aux bag ~from:"2"
540 metasenv context ugraph table lift_amount s in (
544 demodulation_aux bag metasenv
545 ((Some (nn, C.Decl s))::context) ugraph
546 table (lift_amount+1) t
550 | Some (t', subst, menv, ug, eq_found) ->
551 Some (C.Prod (nn, (S.lift 1 s), t'),
552 subst, menv, ug, eq_found)
554 | Some (s', subst, menv, ug, eq_found) ->
555 Some (C.Prod (nn, s', (S.lift 1 t)),
556 subst, menv, ug, eq_found)
558 | C.Lambda (nn, s, t) ->
561 metasenv context ugraph table lift_amount s in (
565 demodulation_aux bag metasenv
566 ((Some (nn, C.Decl s))::context) ugraph
567 table (lift_amount+1) t
571 | Some (t', subst, menv, ug, eq_found) ->
572 Some (C.Lambda (nn, (S.lift 1 s), t'),
573 subst, menv, ug, eq_found)
575 | Some (s', subst, menv, ug, eq_found) ->
576 Some (C.Lambda (nn, s', (S.lift 1 t)),
577 subst, menv, ug, eq_found)
582 if Utils.debug_res then ignore(check_res res "demod_aux output");
588 (** demodulation, when target is an equality *)
589 let rec demodulation_equality bag ?from eq_uri newmeta env table target =
590 let module C = Cic in
591 let module S = CicSubstitution in
592 let module M = CicMetaSubst in
593 let module HL = HelmLibraryObjects in
594 let module U = Utils in
595 let metasenv, context, ugraph = env in
596 let w, proof, (eq_ty, left, right, order), metas, id =
597 Equality.open_equality target
599 (* first, we simplify *)
600 (* let right = U.guarded_simpl context right in *)
601 (* let left = U.guarded_simpl context left in *)
602 (* let order = !Utils.compare_terms left right in *)
603 (* let stat = (eq_ty, left, right, order) in *)
604 (* let w = Utils.compute_equality_weight stat in*)
605 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
606 if Utils.debug_metas then
607 ignore(check_target bag context target "demod equalities input");
608 let metasenv' = (* metasenv @ *) metas in
609 let maxmeta = ref newmeta in
611 let build_newtarget is_left (t, subst, menv, ug, eq_found) =
613 if Utils.debug_metas then
615 ignore(check_for_duplicates menv "input1");
616 ignore(check_disjoint_invariant subst menv "input2");
617 let substs = Subst.ppsubst subst in
618 ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
620 let pos, equality = eq_found in
622 (ty, what, other, _), menv',id') = Equality.open_equality equality in
624 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
625 with CicUtil.Meta_not_found _ -> ty
627 let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
628 let what, other = if pos = Utils.Left then what, other else other, what in
629 let newterm, newproof =
631 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
632 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
633 let name = C.Name "x" in
635 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
636 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
638 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
639 (Cic.Lambda (name, ty, bo'))))))
641 let newmenv = menv in
642 let left, right = if is_left then newterm, right else left, newterm in
643 let ordering = !Utils.compare_terms left right in
644 let stat = (eq_ty, left, right, ordering) in
646 let w = Utils.compute_equality_weight stat in
647 (Equality.mk_equality bag (w, newproof, stat,newmenv))
649 if Utils.debug_metas then
650 ignore(check_target bag context res "buildnew_target output");
655 demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left
657 if Utils.debug_res then check_res res "demod result";
658 let newmeta, newtarget =
661 let newmeta, newtarget = build_newtarget true t in
662 (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
663 if (Equality.is_weak_identity newtarget) (* || *)
664 (*Equality.meta_convertibility_eq target newtarget*) then
667 demodulation_equality bag ?from eq_uri newmeta env table newtarget
669 let res = demodulation_aux bag metasenv' context ugraph table 0 right in
670 if Utils.debug_res then check_res res "demod result 1";
673 let newmeta, newtarget = build_newtarget false t in
674 if (Equality.is_weak_identity newtarget) ||
675 (Equality.meta_convertibility_eq target newtarget) then
678 demodulation_equality bag ?from eq_uri newmeta env table newtarget
682 (* newmeta, newtarget *)
687 Performs the beta expansion of the term "term" w.r.t. "table",
688 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
691 let rec betaexpand_term
692 ?(subterms_only=false) metasenv context ugraph table lift_amount term
694 let module C = Cic in
695 let module S = CicSubstitution in
696 let module M = CicMetaSubst in
697 let module HL = HelmLibraryObjects in
699 let res, lifted_term =
705 (fun arg (res, lifted_tl) ->
708 let arg_res, lifted_arg =
709 betaexpand_term metasenv context ugraph table
713 (fun (t, s, m, ug, eq_found) ->
714 (Some t)::lifted_tl, s, m, ug, eq_found)
719 (fun (l, s, m, ug, eq_found) ->
720 (Some lifted_arg)::l, s, m, ug, eq_found)
722 (Some lifted_arg)::lifted_tl)
725 (fun (r, s, m, ug, eq_found) ->
726 None::r, s, m, ug, eq_found) res,
732 (fun (l, s, m, ug, eq_found) ->
733 (C.Meta (i, l), s, m, ug, eq_found)) l'
735 e, C.Meta (i, lifted_l)
738 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
740 | C.Prod (nn, s, t) ->
742 betaexpand_term metasenv context ugraph table lift_amount s in
744 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
745 table (lift_amount+1) t in
748 (fun (t, s, m, ug, eq_found) ->
749 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
752 (fun (t, s, m, ug, eq_found) ->
753 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
754 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
756 | C.Lambda (nn, s, t) ->
758 betaexpand_term metasenv context ugraph table lift_amount s in
760 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
761 table (lift_amount+1) t in
764 (fun (t, s, m, ug, eq_found) ->
765 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
768 (fun (t, s, m, ug, eq_found) ->
769 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
770 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
775 (fun (res, lifted_tl) arg ->
776 let arg_res, lifted_arg =
777 betaexpand_term metasenv context ugraph table lift_amount arg
781 (fun (a, s, m, ug, eq_found) ->
782 a::lifted_tl, s, m, ug, eq_found)
787 (fun (r, s, m, ug, eq_found) ->
788 lifted_arg::r, s, m, ug, eq_found)
790 lifted_arg::lifted_tl)
791 ) ([], []) (List.rev l)
794 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
797 | t -> [], (S.lift lift_amount t)
800 | C.Meta (i, l) -> res, lifted_term
803 C.Implicit None, ugraph
804 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
806 let candidates = get_candidates Unification table term in
808 if subterms_only then
812 metasenv context ugraph lift_amount term termty candidates
819 returns a list of new clauses inferred with a right superposition step
820 between the positive equation "target" and one in the "table" "newmeta" is
821 the first free meta index, i.e. the first number above the highest meta
822 index: its updated value is also returned
824 let superposition_right bag
825 ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
826 let module C = Cic in
827 let module S = CicSubstitution in
828 let module M = CicMetaSubst in
829 let module HL = HelmLibraryObjects in
830 let module CR = CicReduction in
831 let module U = Utils in
832 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
833 Equality.open_equality target
835 if Utils.debug_metas then
836 ignore (check_target bag context target "superpositionright");
837 let metasenv' = newmetas in
838 let maxmeta = ref newmeta in
842 fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
844 [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
848 (fun (_, subst, _, _, _) ->
849 let subst = apply_subst subst in
850 let o = !Utils.compare_terms (subst l) (subst r) in
851 o <> U.Lt && o <> U.Le)
852 (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
854 (res left right), (res right left)
856 let build_new ordering (bo, s, m, ug, eq_found) =
857 if Utils.debug_metas then
858 ignore (check_target bag context (snd eq_found) "buildnew1" );
860 let pos, equality = eq_found in
861 let (_, proof', (ty, what, other, _), menv',id') =
862 Equality.open_equality equality in
863 let what, other = if pos = Utils.Left then what, other else other, what in
865 let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
866 let newgoal, newproof =
869 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
871 let name = C.Name "x" in
874 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
875 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
879 (s,(Equality.SuperpositionRight,
880 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
882 let newmeta, newequality =
884 if ordering = U.Gt then newgoal, apply_subst s right
885 else apply_subst s left, newgoal in
886 let neworder = !Utils.compare_terms left right in
887 let newmenv = (* Founif.filter s *) m in
888 let stat = (eq_ty, left, right, neworder) in
890 let w = Utils.compute_equality_weight stat in
891 Equality.mk_equality bag (w, newproof, stat, newmenv) in
892 if Utils.debug_metas then
893 ignore (check_target bag context eq' "buildnew3");
894 let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
895 if Utils.debug_metas then
896 ignore (check_target bag context eq' "buildnew4");
900 if Utils.debug_metas then
901 ignore(check_target bag context newequality "buildnew2");
904 let new1 = List.map (build_new U.Gt) res1
905 and new2 = List.map (build_new U.Lt) res2 in
906 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
908 (List.filter ok (new1 @ new2)))
911 (** demodulation, when the target is a theorem *)
912 let rec demodulation_theorem bag newmeta env table theorem =
913 let module C = Cic in
914 let module S = CicSubstitution in
915 let module M = CicMetaSubst in
916 let module HL = HelmLibraryObjects in
917 let metasenv, context, ugraph = env in
918 let maxmeta = ref newmeta in
919 let term, termty, metas = theorem in
920 let metasenv' = metas in
922 let build_newtheorem (t, subst, menv, ug, eq_found) =
923 let pos, equality = eq_found in
924 let (_, proof', (ty, what, other, _), menv',id) =
925 Equality.open_equality equality in
926 let what, other = if pos = Utils.Left then what, other else other, what in
928 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
929 (* let bo' = apply_subst subst t in *)
930 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
933 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
934 Equality.BasicProof (Equality.empty_subst,term))
936 (Equality.build_proof_term_old newproofold, bo)
938 (* TODO, not ported to the new proofs *)
939 if true then assert false; term, bo
941 !maxmeta, (newterm, newty, menv)
944 demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty
948 let newmeta, newthm = build_newtheorem t in
949 let newt, newty, _ = newthm in
950 if Equality.meta_convertibility termty newty then
953 demodulation_theorem bag newmeta env table newthm
958 (*****************************************************************************)
959 (** OPERATIONS ON GOALS **)
961 (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
962 (*****************************************************************************)
966 | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
967 (* assert (LibraryObjects.is_eq_URI uri); *)
972 let ty_of_goal (_,_,ty) = ty ;;
974 (* checks if two goals are metaconvertible *)
975 let goal_metaconvertibility_eq g1 g2 =
976 Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
979 (* when the betaexpand_term function is called on the left/right side of the
980 * goal, the predicate has to be fixed
981 * C[x] ---> (eq ty unchanged C[x])
982 * [posu] is the side of the [unchanged] term in the original goal
984 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
985 let _,_,eq,ty,l,r = open_goal goal in
986 let unchanged = if posu = Utils.Left then l else r in
987 let unchanged = CicSubstitution.lift 1 unchanged in
988 let ty = CicSubstitution.lift 1 ty in
991 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
992 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
994 (pred, subst, menv, ug, eq_f)
997 (* ginve the old [goal], the side that has not changed [posu] and the
998 * expansion builds a new goal *)
999 let build_newgoal bag context goal posu rule expansion =
1000 let goalproof,_,_,_,_,_ = open_goal goal in
1001 let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
1002 let pos, equality = eq_found in
1003 let (_, proof', (ty, what, other, _), menv',id) =
1004 Equality.open_equality equality in
1005 let what, other = if pos = Utils.Left then what, other else other, what in
1006 let newterm, newgoalproof =
1008 Utils.guarded_simpl context
1009 (apply_subst subst (CicSubstitution.subst other t))
1011 let bo' = apply_subst subst t in
1012 let ty = apply_subst subst ty in
1013 let name = Cic.Name "x" in
1014 let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
1015 bo, (newgoalproofstep::goalproof)
1017 let newmetasenv = (* Founif.filter subst *) menv in
1018 (newgoalproof, newmetasenv, newterm)
1023 returns a list of new clauses inferred with a left superposition step
1024 the negative equation "target" and one of the positive equations in "table"
1026 let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
1027 let names = Utils.names_of_context context in
1028 let proof,menv,eq,ty,l,r = open_goal goal in
1029 let c = !Utils.compare_terms l r in
1031 if c = Utils.Incomparable then
1033 let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1034 let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1035 (* prerr_endline "incomparable";
1036 prerr_endline (string_of_int (List.length expansionsl));
1037 prerr_endline (string_of_int (List.length expansionsr));
1039 List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1041 List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1045 | Utils.Gt -> (* prerr_endline "GT"; *)
1046 let big,small,possmall = l,r,Utils.Right in
1047 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1049 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1051 | Utils.Lt -> (* prerr_endline "LT"; *)
1052 let big,small,possmall = r,l,Utils.Left in
1053 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1055 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1060 ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1063 (* rinfresco le meta *)
1066 let max,g = Equality.fix_metas_goal max g in max,g::acc)
1067 newgoals (maxmeta,[])
1070 (** demodulation, when the target is a goal *)
1071 let rec demodulation_goal bag env table goal =
1072 let goalproof,menv,_,_,left,right = open_goal goal in
1073 let _, context, ugraph = env in
1074 (* let term = Utils.guarded_simpl (~debug:true) context term in*)
1076 let resright = demodulation_aux bag menv context ugraph table 0 right in
1080 build_newgoal bag context goal Utils.Left Equality.Demodulation t
1082 if goal_metaconvertibility_eq goal newg then
1085 true, snd (demodulation_goal bag env table newg)
1086 | None -> false, goal
1088 let resleft = demodulation_aux bag menv context ugraph table 0 left in
1091 let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
1092 if goal_metaconvertibility_eq goal newg then
1095 true, snd (demodulation_goal bag env table newg)
1096 | None -> do_right ()
1100 type solved = Yes of Equality.goal | No of Equality.goal list
1102 (* returns all the 1 step demodulations *)
1104 module S = CicSubstitution;;
1105 let rec demodulation_all_aux
1106 metasenv context ugraph table lift_amount term
1109 get_candidates ~env:(metasenv,context,ugraph) Matching table term
1114 let termty, ugraph = C.Implicit None, ugraph in
1117 metasenv context ugraph lift_amount term termty candidates
1126 (fun (rel, s, m, ug, c) ->
1127 (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
1128 (demodulation_all_aux
1129 metasenv context ugraph table lift_amount t),
1130 l@[List.hd r], List.tl r)
1131 (res, [], List.map (S.lift 1) l) l
1135 | C.Lambda (nn, s, t) ->
1136 let context = (Some (nn, C.Decl s))::context in
1139 | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t)
1143 (fun (rel, subst, m, ug, c) ->
1144 mk (S.lift 1 s) rel, subst, m, ug, c)
1145 (demodulation_all_aux
1146 metasenv context ugraph table (lift_amount+1) t)
1147 (* we could demodulate also in s, but then t may be badly
1152 let solve_demodulating bag env table initgoal steps =
1153 let _, context, ugraph = env in
1154 let solved goal res side =
1155 let newg = build_newgoal bag context goal side Equality.Demodulation res in
1157 | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right])
1158 when LibraryObjects.is_eq_URI uri ->
1161 Founif.unification m m context left right CicUniv.empty_ugraph
1164 with CicUnification.UnificationFailure _ -> No [newg])
1167 let solved goal res_list side =
1168 let newg = List.map (fun x -> solved goal x side) res_list in
1170 List.find (function Yes _ -> true | _ -> false) newg
1172 No (List.flatten (List.map (function No s -> s | _-> assert false) newg))
1179 | None -> first f tl
1180 | Some x as ok -> ok
1182 let rec aux steps next goal =
1183 if steps = 0 then None else
1184 let goalproof,menv,_,_,left,right = open_goal goal in
1186 demodulation_all_aux menv context ugraph table 0 t
1190 (match do_step left with
1192 (match solved goal res Utils.Right with
1194 (match first (aux (steps - 1) L) newgoals with
1195 | Some g as success -> success
1196 | None -> aux steps R goal)
1197 | Yes newgoal -> Some newgoal)
1198 | [] -> aux steps R goal)
1200 (match do_step right with
1202 (match solved goal res Utils.Left with
1204 (match first (aux (steps - 1) L) newgoals with
1205 | Some g as success -> success
1207 | Yes newgoal -> Some newgoal)
1210 aux steps L initgoal
1213 let get_stats () = "" ;;