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 subsumption_aux_all use_unification env table target =
430 let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
431 let _, context, ugraph = env in
432 let metasenv = tmetas in
433 let predicate, unif_fun =
434 if use_unification then
435 Unification, Founif.unification
437 Matching, Founif.matching
441 | Cic.Meta _ when not use_unification -> []
443 let leftc = get_candidates predicate table left in
444 find_all_matches ~unif_fun
445 metasenv context ugraph 0 left ty leftc
449 | Cic.Meta _ when not use_unification -> []
451 let rightc = get_candidates predicate table right in
452 find_all_matches ~unif_fun
453 metasenv context ugraph 0 right ty rightc
455 let rec ok_all what leftorright = function
457 | (_, subst, menv, ug, (pos,equation))::tl ->
458 let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
460 let other = if pos = Utils.Left then r else l in
461 let what' = Subst.apply_subst subst what in
462 let other' = Subst.apply_subst subst other in
463 let subst', menv', ug' =
464 unif_fun metasenv m context what' other' ugraph
466 (match Subst.merge_subst_if_possible subst subst' with
467 | None -> ok_all what leftorright tl
469 (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
471 | Founif.MatchingFailure
472 | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
474 (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
477 let subsumption_all x y z =
478 subsumption_aux_all false x y z
481 let unification_all x y z =
482 subsumption_aux_all true x y z
484 let rec demodulation_aux bag ?from ?(typecheck=false)
485 metasenv context ugraph table lift_amount term =
486 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
487 let module C = Cic in
488 let module S = CicSubstitution in
489 let module M = CicMetaSubst in
490 let module HL = HelmLibraryObjects in
493 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
501 CicTypeChecker.type_of_aux' metasenv context term ugraph
503 C.Implicit None, ugraph
506 find_matches bag metasenv context ugraph lift_amount term termty candidates
508 if Utils.debug_res then ignore(check_res res "demod1");
518 (res, tl @ [S.lift 1 t])
521 demodulation_aux bag ~from:"1" metasenv context ugraph table
525 | None -> (None, tl @ [S.lift 1 t])
526 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
531 | Some (_, subst, menv, ug, eq_found) ->
532 Some (C.Appl ll, subst, menv, ug, eq_found)
534 | C.Prod (nn, s, t) ->
536 demodulation_aux bag ~from:"2"
537 metasenv context ugraph table lift_amount s in (
541 demodulation_aux bag metasenv
542 ((Some (nn, C.Decl s))::context) ugraph
543 table (lift_amount+1) t
547 | Some (t', subst, menv, ug, eq_found) ->
548 Some (C.Prod (nn, (S.lift 1 s), t'),
549 subst, menv, ug, eq_found)
551 | Some (s', subst, menv, ug, eq_found) ->
552 Some (C.Prod (nn, s', (S.lift 1 t)),
553 subst, menv, ug, eq_found)
555 | C.Lambda (nn, s, t) ->
558 metasenv context ugraph table lift_amount s in (
562 demodulation_aux bag metasenv
563 ((Some (nn, C.Decl s))::context) ugraph
564 table (lift_amount+1) t
568 | Some (t', subst, menv, ug, eq_found) ->
569 Some (C.Lambda (nn, (S.lift 1 s), t'),
570 subst, menv, ug, eq_found)
572 | Some (s', subst, menv, ug, eq_found) ->
573 Some (C.Lambda (nn, s', (S.lift 1 t)),
574 subst, menv, ug, eq_found)
579 if Utils.debug_res then ignore(check_res res "demod_aux output");
585 (** demodulation, when target is an equality *)
586 let rec demodulation_equality bag ?from eq_uri newmeta env table target =
587 let module C = Cic in
588 let module S = CicSubstitution in
589 let module M = CicMetaSubst in
590 let module HL = HelmLibraryObjects in
591 let module U = Utils in
592 let metasenv, context, ugraph = env in
593 let w, proof, (eq_ty, left, right, order), metas, id =
594 Equality.open_equality target
596 (* first, we simplify *)
597 (* let right = U.guarded_simpl context right in *)
598 (* let left = U.guarded_simpl context left in *)
599 (* let order = !Utils.compare_terms left right in *)
600 (* let stat = (eq_ty, left, right, order) in *)
601 (* let w = Utils.compute_equality_weight stat in*)
602 (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
603 if Utils.debug_metas then
604 ignore(check_target bag context target "demod equalities input");
605 let metasenv' = (* metasenv @ *) metas in
606 let maxmeta = ref newmeta in
608 let build_newtarget is_left (t, subst, menv, ug, eq_found) =
610 if Utils.debug_metas then
612 ignore(check_for_duplicates menv "input1");
613 ignore(check_disjoint_invariant subst menv "input2");
614 let substs = Subst.ppsubst subst in
615 ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
617 let pos, equality = eq_found in
619 (ty, what, other, _), menv',id') = Equality.open_equality equality in
621 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
622 with CicUtil.Meta_not_found _ -> ty
624 let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
625 let what, other = if pos = Utils.Left then what, other else other, what in
626 let newterm, newproof =
628 Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
629 (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
630 let name = C.Name "x" in
632 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
633 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
635 (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
636 (Cic.Lambda (name, ty, bo'))))))
638 let newmenv = menv in
639 let left, right = if is_left then newterm, right else left, newterm in
640 let ordering = !Utils.compare_terms left right in
641 let stat = (eq_ty, left, right, ordering) in
643 let w = Utils.compute_equality_weight stat in
644 (Equality.mk_equality bag (w, newproof, stat,newmenv))
646 if Utils.debug_metas then
647 ignore(check_target bag context res "buildnew_target output");
652 demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left
654 if Utils.debug_res then check_res res "demod result";
655 let newmeta, newtarget =
658 let newmeta, newtarget = build_newtarget true t in
659 (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
660 if (Equality.is_weak_identity newtarget) (* || *)
661 (*Equality.meta_convertibility_eq target newtarget*) then
664 demodulation_equality bag ?from eq_uri newmeta env table newtarget
666 let res = demodulation_aux bag metasenv' context ugraph table 0 right in
667 if Utils.debug_res then check_res res "demod result 1";
670 let newmeta, newtarget = build_newtarget false t in
671 if (Equality.is_weak_identity newtarget) ||
672 (Equality.meta_convertibility_eq target newtarget) then
675 demodulation_equality bag ?from eq_uri newmeta env table newtarget
679 (* newmeta, newtarget *)
684 Performs the beta expansion of the term "term" w.r.t. "table",
685 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
688 let rec betaexpand_term
689 ?(subterms_only=false) metasenv context ugraph table lift_amount term
691 let module C = Cic in
692 let module S = CicSubstitution in
693 let module M = CicMetaSubst in
694 let module HL = HelmLibraryObjects in
696 let res, lifted_term =
702 (fun arg (res, lifted_tl) ->
705 let arg_res, lifted_arg =
706 betaexpand_term metasenv context ugraph table
710 (fun (t, s, m, ug, eq_found) ->
711 (Some t)::lifted_tl, s, m, ug, eq_found)
716 (fun (l, s, m, ug, eq_found) ->
717 (Some lifted_arg)::l, s, m, ug, eq_found)
719 (Some lifted_arg)::lifted_tl)
722 (fun (r, s, m, ug, eq_found) ->
723 None::r, s, m, ug, eq_found) res,
729 (fun (l, s, m, ug, eq_found) ->
730 (C.Meta (i, l), s, m, ug, eq_found)) l'
732 e, C.Meta (i, lifted_l)
735 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
737 | C.Prod (nn, s, t) ->
739 betaexpand_term metasenv context ugraph table lift_amount s in
741 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
742 table (lift_amount+1) t in
745 (fun (t, s, m, ug, eq_found) ->
746 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
749 (fun (t, s, m, ug, eq_found) ->
750 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
751 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
753 | C.Lambda (nn, s, t) ->
755 betaexpand_term metasenv context ugraph table lift_amount s in
757 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
758 table (lift_amount+1) t in
761 (fun (t, s, m, ug, eq_found) ->
762 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
765 (fun (t, s, m, ug, eq_found) ->
766 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
767 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
772 (fun (res, lifted_tl) arg ->
773 let arg_res, lifted_arg =
774 betaexpand_term metasenv context ugraph table lift_amount arg
778 (fun (a, s, m, ug, eq_found) ->
779 a::lifted_tl, s, m, ug, eq_found)
784 (fun (r, s, m, ug, eq_found) ->
785 lifted_arg::r, s, m, ug, eq_found)
787 lifted_arg::lifted_tl)
788 ) ([], []) (List.rev l)
791 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
794 | t -> [], (S.lift lift_amount t)
797 | C.Meta (i, l) -> res, lifted_term
800 C.Implicit None, ugraph
801 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
803 let candidates = get_candidates Unification table term in
805 if subterms_only then
809 metasenv context ugraph lift_amount term termty candidates
816 returns a list of new clauses inferred with a right superposition step
817 between the positive equation "target" and one in the "table" "newmeta" is
818 the first free meta index, i.e. the first number above the highest meta
819 index: its updated value is also returned
821 let superposition_right bag
822 ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
823 let module C = Cic in
824 let module S = CicSubstitution in
825 let module M = CicMetaSubst in
826 let module HL = HelmLibraryObjects in
827 let module CR = CicReduction in
828 let module U = Utils in
829 let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
830 Equality.open_equality target
832 if Utils.debug_metas then
833 ignore (check_target bag context target "superpositionright");
834 let metasenv' = newmetas in
835 let maxmeta = ref newmeta in
839 fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
841 [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
845 (fun (_, subst, _, _, _) ->
846 let subst = apply_subst subst in
847 let o = !Utils.compare_terms (subst l) (subst r) in
848 o <> U.Lt && o <> U.Le)
849 (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
851 (res left right), (res right left)
853 let build_new ordering (bo, s, m, ug, eq_found) =
854 if Utils.debug_metas then
855 ignore (check_target bag context (snd eq_found) "buildnew1" );
857 let pos, equality = eq_found in
858 let (_, proof', (ty, what, other, _), menv',id') =
859 Equality.open_equality equality in
860 let what, other = if pos = Utils.Left then what, other else other, what in
862 let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
863 let newgoal, newproof =
866 Utils.guarded_simpl context (apply_subst s (S.subst other bo))
868 let name = C.Name "x" in
871 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
872 C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
876 (s,(Equality.SuperpositionRight,
877 id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
879 let newmeta, newequality =
881 if ordering = U.Gt then newgoal, apply_subst s right
882 else apply_subst s left, newgoal in
883 let neworder = !Utils.compare_terms left right in
884 let newmenv = (* Founif.filter s *) m in
885 let stat = (eq_ty, left, right, neworder) in
887 let w = Utils.compute_equality_weight stat in
888 Equality.mk_equality bag (w, newproof, stat, newmenv) in
889 if Utils.debug_metas then
890 ignore (check_target bag context eq' "buildnew3");
891 let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
892 if Utils.debug_metas then
893 ignore (check_target bag context eq' "buildnew4");
897 if Utils.debug_metas then
898 ignore(check_target bag context newequality "buildnew2");
901 let new1 = List.map (build_new U.Gt) res1
902 and new2 = List.map (build_new U.Lt) res2 in
903 let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
905 (List.filter ok (new1 @ new2)))
908 (** demodulation, when the target is a theorem *)
909 let rec demodulation_theorem bag newmeta env table theorem =
910 let module C = Cic in
911 let module S = CicSubstitution in
912 let module M = CicMetaSubst in
913 let module HL = HelmLibraryObjects in
914 let metasenv, context, ugraph = env in
915 let maxmeta = ref newmeta in
916 let term, termty, metas = theorem in
917 let metasenv' = metas in
919 let build_newtheorem (t, subst, menv, ug, eq_found) =
920 let pos, equality = eq_found in
921 let (_, proof', (ty, what, other, _), menv',id) =
922 Equality.open_equality equality in
923 let what, other = if pos = Utils.Left then what, other else other, what in
925 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
926 (* let bo' = apply_subst subst t in *)
927 (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
930 Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
931 Equality.BasicProof (Equality.empty_subst,term))
933 (Equality.build_proof_term_old newproofold, bo)
935 (* TODO, not ported to the new proofs *)
936 if true then assert false; term, bo
938 !maxmeta, (newterm, newty, menv)
941 demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty
945 let newmeta, newthm = build_newtheorem t in
946 let newt, newty, _ = newthm in
947 if Equality.meta_convertibility termty newty then
950 demodulation_theorem bag newmeta env table newthm
955 (*****************************************************************************)
956 (** OPERATIONS ON GOALS **)
958 (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
959 (*****************************************************************************)
963 | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
964 (* assert (LibraryObjects.is_eq_URI uri); *)
969 let ty_of_goal (_,_,ty) = ty ;;
971 (* checks if two goals are metaconvertible *)
972 let goal_metaconvertibility_eq g1 g2 =
973 Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
976 (* when the betaexpand_term function is called on the left/right side of the
977 * goal, the predicate has to be fixed
978 * C[x] ---> (eq ty unchanged C[x])
979 * [posu] is the side of the [unchanged] term in the original goal
981 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
982 let _,_,eq,ty,l,r = open_goal goal in
983 let unchanged = if posu = Utils.Left then l else r in
984 let unchanged = CicSubstitution.lift 1 unchanged in
985 let ty = CicSubstitution.lift 1 ty in
988 | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
989 | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
991 (pred, subst, menv, ug, eq_f)
994 (* ginve the old [goal], the side that has not changed [posu] and the
995 * expansion builds a new goal *)
996 let build_newgoal bag context goal posu rule expansion =
997 let goalproof,_,_,_,_,_ = open_goal goal in
998 let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
999 let pos, equality = eq_found in
1000 let (_, proof', (ty, what, other, _), menv',id) =
1001 Equality.open_equality equality in
1002 let what, other = if pos = Utils.Left then what, other else other, what in
1003 let newterm, newgoalproof =
1005 Utils.guarded_simpl context
1006 (apply_subst subst (CicSubstitution.subst other t))
1008 let bo' = apply_subst subst t in
1009 let ty = apply_subst subst ty in
1010 let name = Cic.Name "x" in
1011 let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
1012 bo, (newgoalproofstep::goalproof)
1014 let newmetasenv = (* Founif.filter subst *) menv in
1015 (newgoalproof, newmetasenv, newterm)
1020 returns a list of new clauses inferred with a left superposition step
1021 the negative equation "target" and one of the positive equations in "table"
1023 let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
1024 let names = Utils.names_of_context context in
1025 let proof,menv,eq,ty,l,r = open_goal goal in
1026 let c = !Utils.compare_terms l r in
1028 if c = Utils.Incomparable then
1030 let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1031 let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1032 (* prerr_endline "incomparable";
1033 prerr_endline (string_of_int (List.length expansionsl));
1034 prerr_endline (string_of_int (List.length expansionsr));
1036 List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1038 List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1042 | Utils.Gt -> (* prerr_endline "GT"; *)
1043 let big,small,possmall = l,r,Utils.Right in
1044 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1046 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1048 | Utils.Lt -> (* prerr_endline "LT"; *)
1049 let big,small,possmall = r,l,Utils.Left in
1050 let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1052 (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1057 ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1060 (* rinfresco le meta *)
1063 let max,g = Equality.fix_metas_goal max g in max,g::acc)
1064 newgoals (maxmeta,[])
1067 (** demodulation, when the target is a goal *)
1068 let rec demodulation_goal bag env table goal =
1069 let goalproof,menv,_,_,left,right = open_goal goal in
1070 let _, context, ugraph = env in
1071 (* let term = Utils.guarded_simpl (~debug:true) context term in*)
1073 let resright = demodulation_aux bag menv context ugraph table 0 right in
1077 build_newgoal bag context goal Utils.Left Equality.Demodulation t
1079 if goal_metaconvertibility_eq goal newg then
1082 true, snd (demodulation_goal bag env table newg)
1083 | None -> false, goal
1085 let resleft = demodulation_aux bag menv context ugraph table 0 left in
1088 let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
1089 if goal_metaconvertibility_eq goal newg then
1092 true, snd (demodulation_goal bag env table newg)
1093 | None -> do_right ()
1096 let get_stats () = "" ;;