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/.
28 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
30 module Index = Equality_indexing.DT (* path tree based indexing *)
33 let debug_print = Utils.debug_print;;
37 let check_equation env equation msg =
38 let w, proof, (eq_ty, left, right, order), metas, args = equation in
39 let metasenv, context, ugraph = env in
40 let metasenv' = metasenv @ metas in
42 CicTypeChecker.type_of_aux' metasenv' context left ugraph;
43 CicTypeChecker.type_of_aux' metasenv' context right ugraph;
46 CicUtil.Meta_not_found _ as exn ->
49 prerr_endline (CicPp.ppterm left);
50 prerr_endline (CicPp.ppterm right);
55 type retrieval_mode = Matching | Unification;;
57 let print_candidates mode term res =
61 Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
63 Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
69 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
70 (Inference.string_of_equality e))
76 let indexing_retrieval_time = ref 0.;;
79 let apply_subst = CicMetaSubst.apply_subst
81 let index = Index.index
82 let remove_index = Index.remove_index
83 let in_index = Index.in_index
84 let empty = Index.empty
85 let init_index = Index.init_index
87 (* returns a list of all the equalities in the tree that are in relation
88 "mode" with the given term, where mode can be either Matching or
91 Format of the return value: list of tuples in the form:
92 (position - Left or Right - of the term that matched the given one in this
96 Note that if equality is "left = right", if the ordering is left > right,
97 the position will always be Left, and if the ordering is left < right,
98 position will be Right.
100 let get_candidates mode tree term =
101 let t1 = Unix.gettimeofday () in
105 | Matching -> Index.retrieve_generalizations tree term
106 | Unification -> Index.retrieve_unifiables tree term
108 Index.PosEqSet.elements s
110 (* print_candidates mode term res; *)
111 (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
112 (* print_newline (); *)
113 let t2 = Unix.gettimeofday () in
114 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
119 let match_unif_time_ok = ref 0.;;
120 let match_unif_time_no = ref 0.;;
124 finds the first equality in the index that matches "term", of type "termty"
125 termty can be Implicit if it is not needed. The result (one of the sides of
126 the equality, actually) should be not greater (wrt the term ordering) than
129 Format of the return value:
131 (term to substitute, [Cic.Rel 1 properly lifted - see the various
132 build_newtarget functions inside the various
133 demodulation_* functions]
134 substitution used for the matching,
136 ugraph, [substitution, metasenv and ugraph have the same meaning as those
137 returned by CicUnification.fo_unif]
138 (equality where the matching term was found, [i.e. the equality to use as
140 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
141 the equality: this is used to build the proof term, again see one of
142 the build_newtarget functions]
145 let rec find_matches metasenv context ugraph lift_amount term termty =
146 let module C = Cic in
147 let module U = Utils in
148 let module S = CicSubstitution in
149 let module M = CicMetaSubst in
150 let module HL = HelmLibraryObjects in
151 let cmp = !Utils.compare_terms in
152 let check = match termty with C.Implicit None -> false | _ -> true in
156 let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
157 if check && not (fst (CicReduction.are_convertible
158 ~metasenv context termty ty ugraph)) then (
159 find_matches metasenv context ugraph lift_amount term termty tl
161 let do_match c eq_URI =
162 let subst', metasenv', ugraph' =
163 let t1 = Unix.gettimeofday () in
166 Inference.matching (metasenv @ metas) context
167 term (S.lift lift_amount c) ugraph
169 let t2 = Unix.gettimeofday () in
170 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
173 | Inference.MatchingFailure as e ->
174 let t2 = Unix.gettimeofday () in
175 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
177 | CicUtil.Meta_not_found _ as exn ->
178 prerr_endline "zurg";
181 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
184 let c, other, eq_URI =
185 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
186 else right, left, Utils.eq_ind_r_URI ()
188 if o <> U.Incomparable then
191 with Inference.MatchingFailure ->
192 find_matches metasenv context ugraph lift_amount term termty tl
195 try do_match c eq_URI
196 with Inference.MatchingFailure -> None
199 | Some (_, s, _, _, _) ->
200 let c' = apply_subst s c in
202 let other' = U.guarded_simpl context (apply_subst s other) in *)
203 let other' = apply_subst s other in
204 let order = cmp c' other' in
209 metasenv context ugraph lift_amount term termty tl
211 find_matches metasenv context ugraph lift_amount term termty tl
216 as above, but finds all the matching equalities, and the matching condition
217 can be either Inference.matching or Inference.unification
219 let rec find_all_matches ?(unif_fun=Inference.unification)
220 metasenv context ugraph lift_amount term termty =
221 let module C = Cic in
222 let module U = Utils in
223 let module S = CicSubstitution in
224 let module M = CicMetaSubst in
225 let module HL = HelmLibraryObjects in
226 let cmp = !Utils.compare_terms in
230 let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
231 let do_match c eq_URI =
232 let subst', metasenv', ugraph' =
233 let t1 = Unix.gettimeofday () in
236 unif_fun (metasenv @ metas) context
237 term (S.lift lift_amount c) ugraph in
238 let t2 = Unix.gettimeofday () in
239 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
242 | Inference.MatchingFailure
243 | CicUnification.UnificationFailure _
244 | CicUnification.Uncertain _ as e ->
245 let t2 = Unix.gettimeofday () in
246 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
249 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
252 let c, other, eq_URI =
253 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
254 else right, left, Utils.eq_ind_r_URI ()
256 if o <> U.Incomparable then
258 let res = do_match c eq_URI in
259 res::(find_all_matches ~unif_fun metasenv context ugraph
260 lift_amount term termty tl)
262 | Inference.MatchingFailure
263 | CicUnification.UnificationFailure _
264 | CicUnification.Uncertain _ ->
265 find_all_matches ~unif_fun metasenv context ugraph
266 lift_amount term termty tl
269 let res = do_match c eq_URI in
272 let c' = apply_subst s c
273 and other' = apply_subst s other in
274 let order = cmp c' other' in
275 if order <> U.Lt && order <> U.Le then
276 res::(find_all_matches ~unif_fun metasenv context ugraph
277 lift_amount term termty tl)
279 find_all_matches ~unif_fun metasenv context ugraph
280 lift_amount term termty tl
282 | Inference.MatchingFailure
283 | CicUnification.UnificationFailure _
284 | CicUnification.Uncertain _ ->
285 find_all_matches ~unif_fun metasenv context ugraph
286 lift_amount term termty tl
291 returns true if target is subsumed by some equality in table
293 let subsumption env table target =
294 let _, _, (ty, left, right, _), tmetas, _ = target in
295 let metasenv, context, ugraph = env in
296 let metasenv = metasenv @ tmetas in
297 let samesubst subst subst' =
298 let tbl = Hashtbl.create (List.length subst) in
299 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
301 (fun (m, (c, t1, t2)) ->
303 let c', t1', t2' = Hashtbl.find tbl m in
304 if (c = c') && (t1 = t1') && (t2 = t2') then true
314 let leftc = get_candidates Matching table left in
315 find_all_matches ~unif_fun:Inference.matching
316 metasenv context ugraph 0 left ty leftc
318 let rec ok what = function
320 | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
322 let other = if pos = Utils.Left then r else l in
323 let subst', menv', ug' =
324 let t1 = Unix.gettimeofday () in
327 Inference.matching (metasenv @ menv @ m) context what other ugraph
329 let t2 = Unix.gettimeofday () in
330 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
332 with Inference.MatchingFailure as e ->
333 let t2 = Unix.gettimeofday () in
334 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
337 if samesubst subst subst' then
341 with Inference.MatchingFailure ->
344 let r, subst = ok right leftr in
353 let rightc = get_candidates Matching table right in
354 find_all_matches ~unif_fun:Inference.matching
355 metasenv context ugraph 0 right ty rightc
362 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
363 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
368 let rec demodulation_aux ?(typecheck=false)
369 metasenv context ugraph table lift_amount term =
370 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
372 let module C = Cic in
373 let module S = CicSubstitution in
374 let module M = CicMetaSubst in
375 let module HL = HelmLibraryObjects in
376 let candidates = get_candidates Matching table term in
382 CicTypeChecker.type_of_aux' metasenv context term ugraph
384 C.Implicit None, ugraph
387 find_matches metasenv context ugraph lift_amount term termty candidates
398 (res, tl @ [S.lift 1 t])
401 demodulation_aux metasenv context ugraph table
405 | None -> (None, tl @ [S.lift 1 t])
406 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
411 | Some (_, subst, menv, ug, eq_found) ->
412 Some (C.Appl ll, subst, menv, ug, eq_found)
414 | C.Prod (nn, s, t) ->
416 demodulation_aux metasenv context ugraph table lift_amount s in (
420 demodulation_aux metasenv
421 ((Some (nn, C.Decl s))::context) ugraph
422 table (lift_amount+1) t
426 | Some (t', subst, menv, ug, eq_found) ->
427 Some (C.Prod (nn, (S.lift 1 s), t'),
428 subst, menv, ug, eq_found)
430 | Some (s', subst, menv, ug, eq_found) ->
431 Some (C.Prod (nn, s', (S.lift 1 t)),
432 subst, menv, ug, eq_found)
434 | C.Lambda (nn, s, t) ->
436 demodulation_aux metasenv context ugraph table lift_amount s in (
440 demodulation_aux metasenv
441 ((Some (nn, C.Decl s))::context) ugraph
442 table (lift_amount+1) t
446 | Some (t', subst, menv, ug, eq_found) ->
447 Some (C.Lambda (nn, (S.lift 1 s), t'),
448 subst, menv, ug, eq_found)
450 | Some (s', subst, menv, ug, eq_found) ->
451 Some (C.Lambda (nn, s', (S.lift 1 t)),
452 subst, menv, ug, eq_found)
459 let build_newtarget_time = ref 0.;;
462 let demod_counter = ref 1;;
464 (** demodulation, when target is an equality *)
465 let rec demodulation_equality newmeta env table sign target =
466 let module C = Cic in
467 let module S = CicSubstitution in
468 let module M = CicMetaSubst in
469 let module HL = HelmLibraryObjects in
470 let module U = Utils in
471 let metasenv, context, ugraph = env in
472 let w, proof, (eq_ty, left, right, order), metas, args = target in
473 (* first, we simplify *)
474 let right = U.guarded_simpl context right in
475 let left = U.guarded_simpl context left in
476 let w = Utils.compute_equality_weight eq_ty left right in
477 let order = !Utils.compare_terms left right in
478 let target = w, proof, (eq_ty, left, right, order), metas, args in
480 let metasenv' = metasenv @ metas in
482 let maxmeta = ref newmeta in
484 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
485 let time1 = Unix.gettimeofday () in
487 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
489 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
490 with CicUtil.Meta_not_found _ -> ty
492 let what, other = if pos = Utils.Left then what, other else other, what in
493 let newterm, newproof =
494 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
495 let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
498 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
499 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
500 S.lift 1 eq_ty; l; r]
502 if sign = Utils.Positive then
504 Inference.ProofBlock (
505 subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
510 CicMkImplicit.identity_relocation_list_for_metavariable context in
511 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
512 (* print_newline (); *)
513 C.Meta (!maxmeta, irl)
518 if pos = Utils.Left then [ty; what; other]
519 else [ty; other; what]
521 Inference.ProofSymBlock (termlist, proof')
524 if pos = Utils.Left then what, other else other, what
526 pos, (0, proof', (ty, other, what, Utils.Incomparable),
531 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
532 eq_found, Inference.BasicProof metaproof)
535 | Inference.BasicProof _ ->
536 print_endline "replacing a BasicProof";
538 | Inference.ProofGoalBlock (_, parent_proof) ->
539 print_endline "replacing another ProofGoalBlock";
540 Inference.ProofGoalBlock (pb, parent_proof)
544 C.Appl [C.MutConstruct (* reflexivity *)
545 (LibraryObjects.eq_URI (), 0, 1, []);
546 eq_ty; if is_left then right else left]
549 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
551 let left, right = if is_left then newterm, right else left, newterm in
553 (Inference.metas_of_term left)
554 @ (Inference.metas_of_term right)
555 @ (Inference.metas_of_term eq_ty) in
556 (* let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') *)
557 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metasenv' @ menv')
560 let ordering = !Utils.compare_terms left right in
562 let time2 = Unix.gettimeofday () in
563 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
566 let w = Utils.compute_equality_weight eq_ty left right in
567 (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
573 CicTypeChecker.type_of_aux' metasenv' context left ugraph;
574 CicTypeChecker.type_of_aux' metasenv' context right ugraph;
576 CicUtil.Meta_not_found _ as exn ->
578 prerr_endline "siamo in demodulation_equality 1";
579 prerr_endline (CicPp.ppterm left);
580 prerr_endline (CicPp.ppterm right);
584 let res = demodulation_aux metasenv' context ugraph table 0 left in
585 let newmeta, newtarget =
588 let newmeta, newtarget = build_newtarget true t in
589 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
590 (Inference.meta_convertibility_eq target newtarget) then
593 demodulation_equality newmeta env table sign newtarget
595 let res = demodulation_aux metasenv' context ugraph table 0 right in
598 let newmeta, newtarget = build_newtarget false t in
599 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
600 (Inference.meta_convertibility_eq target newtarget) then
603 demodulation_equality newmeta env table sign newtarget
607 (* newmeta, newtarget *)
613 Performs the beta expansion of the term "term" w.r.t. "table",
614 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
617 let rec betaexpand_term metasenv context ugraph table lift_amount term =
618 let module C = Cic in
619 let module S = CicSubstitution in
620 let module M = CicMetaSubst in
621 let module HL = HelmLibraryObjects in
622 let candidates = get_candidates Unification table term in
623 let res, lifted_term =
628 (fun arg (res, lifted_tl) ->
631 let arg_res, lifted_arg =
632 betaexpand_term metasenv context ugraph table
636 (fun (t, s, m, ug, eq_found) ->
637 (Some t)::lifted_tl, s, m, ug, eq_found)
642 (fun (l, s, m, ug, eq_found) ->
643 (Some lifted_arg)::l, s, m, ug, eq_found)
645 (Some lifted_arg)::lifted_tl)
648 (fun (r, s, m, ug, eq_found) ->
649 None::r, s, m, ug, eq_found) res,
655 (fun (l, s, m, ug, eq_found) ->
656 (C.Meta (i, l), s, m, ug, eq_found)) l'
658 e, C.Meta (i, lifted_l)
661 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
663 | C.Prod (nn, s, t) ->
665 betaexpand_term metasenv context ugraph table lift_amount s in
667 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
668 table (lift_amount+1) t in
671 (fun (t, s, m, ug, eq_found) ->
672 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
675 (fun (t, s, m, ug, eq_found) ->
676 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
677 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
679 | C.Lambda (nn, s, t) ->
681 betaexpand_term metasenv context ugraph table lift_amount s in
683 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
684 table (lift_amount+1) t in
687 (fun (t, s, m, ug, eq_found) ->
688 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
691 (fun (t, s, m, ug, eq_found) ->
692 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
693 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
698 (fun arg (res, lifted_tl) ->
699 let arg_res, lifted_arg =
700 betaexpand_term metasenv context ugraph table lift_amount arg
704 (fun (a, s, m, ug, eq_found) ->
705 a::lifted_tl, s, m, ug, eq_found)
710 (fun (r, s, m, ug, eq_found) ->
711 lifted_arg::r, s, m, ug, eq_found)
713 lifted_arg::lifted_tl)
717 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
720 | t -> [], (S.lift lift_amount t)
723 | C.Meta (i, l) -> res, lifted_term
726 C.Implicit None, ugraph
727 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
731 metasenv context ugraph lift_amount term termty candidates
737 let sup_l_counter = ref 1;;
741 returns a list of new clauses inferred with a left superposition step
742 the negative equation "target" and one of the positive equations in "table"
744 let superposition_left newmeta (metasenv, context, ugraph) table target =
745 let module C = Cic in
746 let module S = CicSubstitution in
747 let module M = CicMetaSubst in
748 let module HL = HelmLibraryObjects in
749 let module CR = CicReduction in
750 let module U = Utils in
751 let weight, proof, (eq_ty, left, right, ordering), menv, _ = target in
753 let term = if ordering = U.Gt then left else right in
754 betaexpand_term metasenv context ugraph table 0 term
756 let maxmeta = ref newmeta in
757 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
759 (* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
761 let time1 = Unix.gettimeofday () in
763 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
764 let what, other = if pos = Utils.Left then what, other else other, what in
765 let newgoal, newproof =
766 let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
767 let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
771 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
772 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
773 S.lift 1 eq_ty; l; r]
778 CicMkImplicit.identity_relocation_list_for_metavariable context in
779 C.Meta (!maxmeta, irl)
784 if pos = Utils.Left then [ty; what; other]
785 else [ty; other; what]
787 Inference.ProofSymBlock (termlist, proof')
790 if pos = Utils.Left then what, other else other, what
792 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
796 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
797 Inference.BasicProof metaproof)
800 | Inference.BasicProof _ ->
801 (* debug_print (lazy "replacing a BasicProof"); *)
803 | Inference.ProofGoalBlock (_, parent_proof) ->
804 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
805 Inference.ProofGoalBlock (pb, parent_proof)
809 C.Appl [C.MutConstruct (* reflexivity *)
810 (LibraryObjects.eq_URI (), 0, 1, []);
811 eq_ty; if ordering = U.Gt then right else left]
814 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
817 if ordering = U.Gt then newgoal, right else left, newgoal in
818 let neworder = !Utils.compare_terms left right in
820 let time2 = Unix.gettimeofday () in
821 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
824 let w = Utils.compute_equality_weight eq_ty left right in
825 (w, newproof, (eq_ty, left, right, neworder), menv @ menv', [])
829 !maxmeta, List.map build_new expansions
833 let sup_r_counter = ref 1;;
837 returns a list of new clauses inferred with a right superposition step
838 between the positive equation "target" and one in the "table" "newmeta" is
839 the first free meta index, i.e. the first number above the highest meta
840 index: its updated value is also returned
842 let superposition_right newmeta (metasenv, context, ugraph) table target =
843 let module C = Cic in
844 let module S = CicSubstitution in
845 let module M = CicMetaSubst in
846 let module HL = HelmLibraryObjects in
847 let module CR = CicReduction in
848 let module U = Utils in
849 let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
850 let metasenv' = metasenv @ newmetas in
851 let maxmeta = ref newmeta in
854 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
855 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
859 (fun (_, subst, _, _, _) ->
860 let subst = apply_subst subst in
861 let o = !Utils.compare_terms (subst l) (subst r) in
862 o <> U.Lt && o <> U.Le)
863 (fst (betaexpand_term metasenv' context ugraph table 0 l))
865 (res left right), (res right left)
867 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
869 let time1 = Unix.gettimeofday () in
871 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
872 let what, other = if pos = Utils.Left then what, other else other, what in
873 let newgoal, newproof =
875 let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
876 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
880 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
881 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
882 S.lift 1 eq_ty; l; r]
885 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
887 let newmeta, newequality =
889 if ordering = U.Gt then newgoal, apply_subst s right
890 else apply_subst s left, newgoal in
891 let neworder = !Utils.compare_terms left right
892 and newmenv = newmetas @ menv'
893 and newargs = args @ args' in
895 let w = Utils.compute_equality_weight eq_ty left right in
896 (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in
897 let newm, eq' = Inference.fix_metas !maxmeta eq' in
902 let time2 = Unix.gettimeofday () in
903 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
907 let new1 = List.map (build_new U.Gt) res1
908 and new2 = List.map (build_new U.Lt) res2 in
910 let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
912 let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
914 (List.filter ok (new1 @ new2)))
918 (** demodulation, when the target is a goal *)
919 let rec demodulation_goal newmeta env table goal =
920 let module C = Cic in
921 let module S = CicSubstitution in
922 let module M = CicMetaSubst in
923 let module HL = HelmLibraryObjects in
924 let metasenv, context, ugraph = env in
925 let maxmeta = ref newmeta in
926 let proof, metas, term = goal in
927 let term = Utils.guarded_simpl (~debug:true) context term in
928 let goal = proof, metas, term in
929 let metasenv' = metasenv @ metas in
931 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
932 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
933 let what, other = if pos = Utils.Left then what, other else other, what in
935 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
936 with CicUtil.Meta_not_found _ -> ty
938 let newterm, newproof =
940 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
941 let bo' = apply_subst subst t in
942 let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
947 CicMkImplicit.identity_relocation_list_for_metavariable context in
948 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
949 C.Meta (!maxmeta, irl)
954 if pos = Utils.Left then [ty; what; other]
955 else [ty; other; what]
957 Inference.ProofSymBlock (termlist, proof')
960 if pos = Utils.Left then what, other else other, what
962 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
966 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
967 eq_found, Inference.BasicProof metaproof)
969 let rec repl = function
970 | Inference.NoProof ->
971 (* debug_print (lazy "replacing a NoProof"); *)
973 | Inference.BasicProof _ ->
974 (* debug_print (lazy "replacing a BasicProof"); *)
976 | Inference.ProofGoalBlock (_, parent_proof) ->
977 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
978 Inference.ProofGoalBlock (pb, parent_proof)
979 | Inference.SubProof (term, meta_index, p) ->
980 Inference.SubProof (term, meta_index, repl p)
984 bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
986 let m = Inference.metas_of_term newterm in
988 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (menv @ menv')in
989 !maxmeta, (newproof, newmetasenv, newterm)
992 demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
996 let newmeta, newgoal = build_newgoal t in
997 let _, _, newg = newgoal in
998 if Inference.meta_convertibility term newg then
1001 demodulation_goal newmeta env table newgoal
1007 (** demodulation, when the target is a theorem *)
1008 let rec demodulation_theorem newmeta env table theorem =
1009 let module C = Cic in
1010 let module S = CicSubstitution in
1011 let module M = CicMetaSubst in
1012 let module HL = HelmLibraryObjects in
1013 let metasenv, context, ugraph = env in
1014 let maxmeta = ref newmeta in
1015 let term, termty, metas = theorem in
1016 let metasenv' = metasenv @ metas in
1018 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1019 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1020 let what, other = if pos = Utils.Left then what, other else other, what in
1021 let newterm, newty =
1023 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1024 let bo' = apply_subst subst t in
1025 let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1028 Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1029 Inference.BasicProof term)
1031 (Inference.build_proof_term newproof, bo)
1034 let m = Inference.metas_of_term newterm in
1035 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') in
1036 !maxmeta, (newterm, newty, newmetasenv)
1039 demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty
1043 let newmeta, newthm = build_newtheorem t in
1044 let newt, newty, _ = newthm in
1045 if Inference.meta_convertibility termty newty then
1048 demodulation_theorem newmeta env table newthm