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 debug_print = Utils.debug_print;;
29 type retrieval_mode = Matching | Unification;;
32 let print_candidates mode term res =
36 Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
38 Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
44 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
45 (Inference.string_of_equality e))
51 let indexing_retrieval_time = ref 0.;;
54 let apply_subst = CicMetaSubst.apply_subst
60 let init_index () = ()
62 let empty_table () = []
64 let index table equality =
65 let _, _, (_, l, r, ordering), _, _ = equality in
67 | Utils.Gt -> (Utils.Left, equality)::table
68 | Utils.Lt -> (Utils.Right, equality)::table
69 | _ -> (Utils.Left, equality)::(Utils.Right, equality)::table
72 let remove_index table equality =
73 List.filter (fun (p, e) -> e != equality) table
76 let in_index table equality =
77 List.exists (fun (p, e) -> e == equality) table
80 let get_candidates mode table term = table
86 let init_index () = ()
89 Path_indexing.PSTrie.empty
92 let index = Path_indexing.index
93 and remove_index = Path_indexing.remove_index
94 and in_index = Path_indexing.in_index;;
96 let get_candidates mode trie term =
97 let t1 = Unix.gettimeofday () in
101 | Matching -> Path_indexing.retrieve_generalizations trie term
102 | Unification -> Path_indexing.retrieve_unifiables trie term
103 (* Path_indexing.retrieve_all trie term *)
105 Path_indexing.PosEqSet.elements s
107 (* print_candidates mode term res; *)
108 let t2 = Unix.gettimeofday () in
109 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
115 (* DISCRIMINATION TREES *)
117 Hashtbl.clear Discrimination_tree.arities;
121 Discrimination_tree.DiscriminationTree.empty
124 let index = Discrimination_tree.index
125 and remove_index = Discrimination_tree.remove_index
126 and in_index = Discrimination_tree.in_index;;
128 let get_candidates mode tree term =
129 let t1 = Unix.gettimeofday () in
133 | Matching -> Discrimination_tree.retrieve_generalizations tree term
134 | Unification -> Discrimination_tree.retrieve_unifiables tree term
136 Discrimination_tree.PosEqSet.elements s
138 (* print_candidates mode term res; *)
139 (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
140 (* print_newline (); *)
141 let t2 = Unix.gettimeofday () in
142 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
147 let match_unif_time_ok = ref 0.;;
148 let match_unif_time_no = ref 0.;;
152 finds the first equality in the index that matches "term", of type "termty"
153 termty can be Implicit if it is not needed. The result (one of the sides of
154 the equality, actually) should be not greater (wrt the term ordering) than
157 let rec find_matches metasenv context ugraph lift_amount term termty =
158 let module C = Cic in
159 let module U = Utils in
160 let module S = CicSubstitution in
161 let module M = CicMetaSubst in
162 let module HL = HelmLibraryObjects in
163 let cmp = !Utils.compare_terms in
164 let check = match termty with C.Implicit None -> false | _ -> true in
168 let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
169 if check && not (fst (CicReduction.are_convertible
170 ~metasenv context termty ty ugraph)) then (
171 find_matches metasenv context ugraph lift_amount term termty tl
173 let do_match c eq_URI =
174 let subst', metasenv', ugraph' =
175 let t1 = Unix.gettimeofday () in
178 Inference.matching (metasenv @ metas) context
179 term (S.lift lift_amount c) ugraph in
180 let t2 = Unix.gettimeofday () in
181 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
183 with Inference.MatchingFailure as e ->
184 let t2 = Unix.gettimeofday () in
185 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
188 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
191 let c, other, eq_URI =
192 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
193 else right, left, Utils.eq_ind_r_URI ()
195 if o <> U.Incomparable then
198 with Inference.MatchingFailure ->
199 find_matches metasenv context ugraph lift_amount term termty tl
202 try do_match c eq_URI
203 with Inference.MatchingFailure -> None
206 | Some (_, s, _, _, _) ->
207 let c' = apply_subst s c
208 and other' = apply_subst s other in
209 let order = cmp c' other' in
210 let names = U.names_of_context context in
215 metasenv context ugraph lift_amount term termty tl
217 find_matches metasenv context ugraph lift_amount term termty tl
222 as above, but finds all the matching equalities, and the matching condition
223 can be either Inference.matching or Inference.unification
225 let rec find_all_matches ?(unif_fun=Inference.unification)
226 metasenv context ugraph lift_amount term termty =
227 let module C = Cic in
228 let module U = Utils in
229 let module S = CicSubstitution in
230 let module M = CicMetaSubst in
231 let module HL = HelmLibraryObjects in
232 let cmp = !Utils.compare_terms in
236 let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
237 let do_match c eq_URI =
238 let subst', metasenv', ugraph' =
239 let t1 = Unix.gettimeofday () in
242 unif_fun (metasenv @ metas) context
243 term (S.lift lift_amount c) ugraph in
244 let t2 = Unix.gettimeofday () in
245 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
248 | Inference.MatchingFailure
249 | CicUnification.UnificationFailure _
250 | CicUnification.Uncertain _ as e ->
251 let t2 = Unix.gettimeofday () in
252 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
255 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
258 let c, other, eq_URI =
259 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
260 else right, left, Utils.eq_ind_r_URI ()
262 if o <> U.Incomparable then
264 let res = do_match c eq_URI in
265 res::(find_all_matches ~unif_fun metasenv context ugraph
266 lift_amount term termty tl)
268 | Inference.MatchingFailure
269 | CicUnification.UnificationFailure _
270 | CicUnification.Uncertain _ ->
271 find_all_matches ~unif_fun metasenv context ugraph
272 lift_amount term termty tl
275 let res = do_match c eq_URI in
278 let c' = apply_subst s c
279 and other' = apply_subst s other in
280 let order = cmp c' other' in
281 let names = U.names_of_context context in
282 if order <> U.Lt && order <> U.Le then
283 res::(find_all_matches ~unif_fun metasenv context ugraph
284 lift_amount term termty tl)
286 find_all_matches ~unif_fun metasenv context ugraph
287 lift_amount term termty tl
289 | Inference.MatchingFailure
290 | CicUnification.UnificationFailure _
291 | CicUnification.Uncertain _ ->
292 find_all_matches ~unif_fun metasenv context ugraph
293 lift_amount term termty tl
298 returns true if target is subsumed by some equality in table
300 let subsumption env table target =
301 let _, _, (ty, left, right, _), tmetas, _ = target in
302 let metasenv, context, ugraph = env in
303 let metasenv = metasenv @ tmetas in
304 let samesubst subst subst' =
305 let tbl = Hashtbl.create (List.length subst) in
306 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
308 (fun (m, (c, t1, t2)) ->
310 let c', t1', t2' = Hashtbl.find tbl m in
311 if (c = c') && (t1 = t1') && (t2 = t2') then true
321 let leftc = get_candidates Matching table left in
322 find_all_matches ~unif_fun:Inference.matching
323 metasenv context ugraph 0 left ty leftc
325 let rec ok what = function
327 | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
329 let other = if pos = Utils.Left then r else l in
330 let subst', menv', ug' =
331 let t1 = Unix.gettimeofday () in
334 Inference.matching (metasenv @ menv @ m) context what other ugraph
336 let t2 = Unix.gettimeofday () in
337 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
339 with Inference.MatchingFailure as e ->
340 let t2 = Unix.gettimeofday () in
341 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
344 if samesubst subst subst' then
348 with Inference.MatchingFailure ->
351 let r, subst = ok right leftr in
360 let rightc = get_candidates Matching table right in
361 find_all_matches ~unif_fun:Inference.matching
362 metasenv context ugraph 0 right ty rightc
369 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
370 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
375 let rec demodulation_aux ?(typecheck=false)
376 metasenv context ugraph table lift_amount term =
377 let module C = Cic in
378 let module S = CicSubstitution in
379 let module M = CicMetaSubst in
380 let module HL = HelmLibraryObjects in
381 let candidates = get_candidates Matching table term in
387 CicTypeChecker.type_of_aux' metasenv context term ugraph
389 C.Implicit None, ugraph
392 find_matches metasenv context ugraph lift_amount term termty candidates
403 (res, tl @ [S.lift 1 t])
406 demodulation_aux metasenv context ugraph table
410 | None -> (None, tl @ [S.lift 1 t])
411 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
416 | Some (_, subst, menv, ug, eq_found) ->
417 Some (C.Appl ll, subst, menv, ug, eq_found)
419 | C.Prod (nn, s, t) ->
421 demodulation_aux metasenv context ugraph table lift_amount s in (
425 demodulation_aux metasenv
426 ((Some (nn, C.Decl s))::context) ugraph
427 table (lift_amount+1) t
431 | Some (t', subst, menv, ug, eq_found) ->
432 Some (C.Prod (nn, (S.lift 1 s), t'),
433 subst, menv, ug, eq_found)
435 | Some (s', subst, menv, ug, eq_found) ->
436 Some (C.Prod (nn, s', (S.lift 1 t)),
437 subst, menv, ug, eq_found)
439 | C.Lambda (nn, s, t) ->
441 demodulation_aux metasenv context ugraph table lift_amount s in (
445 demodulation_aux metasenv
446 ((Some (nn, C.Decl s))::context) ugraph
447 table (lift_amount+1) t
451 | Some (t', subst, menv, ug, eq_found) ->
452 Some (C.Lambda (nn, (S.lift 1 s), t'),
453 subst, menv, ug, eq_found)
455 | Some (s', subst, menv, ug, eq_found) ->
456 Some (C.Lambda (nn, s', (S.lift 1 t)),
457 subst, menv, ug, eq_found)
464 let build_newtarget_time = ref 0.;;
467 let demod_counter = ref 1;;
469 (** demodulation, when target is an equality *)
470 let rec demodulation_equality newmeta env table sign target =
471 let module C = Cic in
472 let module S = CicSubstitution in
473 let module M = CicMetaSubst in
474 let module HL = HelmLibraryObjects in
475 let metasenv, context, ugraph = env in
476 let _, proof, (eq_ty, left, right, order), metas, args = target in
477 let metasenv' = metasenv @ metas in
479 let maxmeta = ref newmeta in
481 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
482 let time1 = Unix.gettimeofday () in
484 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
486 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
487 with CicUtil.Meta_not_found _ -> ty
489 let what, other = if pos = Utils.Left then what, other else other, what in
490 let newterm, newproof =
491 let bo = apply_subst subst (S.subst other t) in
492 let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
495 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
496 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
497 S.lift 1 eq_ty; l; r]
499 if sign = Utils.Positive then
501 Inference.ProofBlock (
502 subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
507 CicMkImplicit.identity_relocation_list_for_metavariable context in
508 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
509 (* print_newline (); *)
510 C.Meta (!maxmeta, irl)
515 if pos = Utils.Left then [ty; what; other]
516 else [ty; other; what]
518 Inference.ProofSymBlock (termlist, proof')
521 if pos = Utils.Left then what, other else other, what
523 pos, (0, proof', (ty, other, what, Utils.Incomparable),
528 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
529 eq_found, Inference.BasicProof metaproof)
532 | Inference.BasicProof _ ->
533 print_endline "replacing a BasicProof";
535 | Inference.ProofGoalBlock (_, parent_proof) ->
536 print_endline "replacing another ProofGoalBlock";
537 Inference.ProofGoalBlock (pb, parent_proof)
541 C.Appl [C.MutConstruct (* reflexivity *)
542 (LibraryObjects.eq_URI (), 0, 1, []);
543 eq_ty; if is_left then right else left]
546 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
548 let left, right = if is_left then newterm, right else left, newterm in
549 let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
550 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
553 let ordering = !Utils.compare_terms left right in
555 let time2 = Unix.gettimeofday () in
556 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
559 let w = Utils.compute_equality_weight eq_ty left right in
560 (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
564 let res = demodulation_aux metasenv' context ugraph table 0 left in
565 let newmeta, newtarget =
568 let newmeta, newtarget = build_newtarget true t in
569 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
570 (Inference.meta_convertibility_eq target newtarget) then
573 demodulation_equality newmeta env table sign newtarget
575 let res = demodulation_aux metasenv' context ugraph table 0 right in
578 let newmeta, newtarget = build_newtarget false t in
579 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
580 (Inference.meta_convertibility_eq target newtarget) then
583 demodulation_equality newmeta env table sign newtarget
587 (* newmeta, newtarget *)
588 (* tentiamo di ridurre usando CicReduction.normalize *)
589 let w, p, (ty, left, right, o), m, a = newtarget in
590 let left' = ProofEngineReduction.simpl context left in
591 let right' = ProofEngineReduction.simpl context right in
593 if !Utils.compare_terms left' left = Utils.Lt then left' else left in
595 if !Utils.compare_terms right' right = Utils.Lt then right' else right in
596 (* if newleft != left || newright != right then ( *)
599 (* (Printf.sprintf "left: %s, left': %s\nright: %s, right': %s\n" *)
600 (* (CicPp.ppterm left) (CicPp.ppterm left') (CicPp.ppterm right) *)
601 (* (CicPp.ppterm right'))) *)
603 let w' = Utils.compute_equality_weight ty newleft newright in
604 let o' = !Utils.compare_terms newleft newright in
605 newmeta, (w', p, (ty, newleft, newright, o'), m, a)
610 Performs the beta expansion of the term "term" w.r.t. "table",
611 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
614 let rec betaexpand_term metasenv context ugraph table lift_amount term =
615 let module C = Cic in
616 let module S = CicSubstitution in
617 let module M = CicMetaSubst in
618 let module HL = HelmLibraryObjects in
619 let candidates = get_candidates Unification table term in
620 let res, lifted_term =
625 (fun arg (res, lifted_tl) ->
628 let arg_res, lifted_arg =
629 betaexpand_term metasenv context ugraph table
633 (fun (t, s, m, ug, eq_found) ->
634 (Some t)::lifted_tl, s, m, ug, eq_found)
639 (fun (l, s, m, ug, eq_found) ->
640 (Some lifted_arg)::l, s, m, ug, eq_found)
642 (Some lifted_arg)::lifted_tl)
645 (fun (r, s, m, ug, eq_found) ->
646 None::r, s, m, ug, eq_found) res,
652 (fun (l, s, m, ug, eq_found) ->
653 (C.Meta (i, l), s, m, ug, eq_found)) l'
655 e, C.Meta (i, lifted_l)
658 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
660 | C.Prod (nn, s, t) ->
662 betaexpand_term metasenv context ugraph table lift_amount s in
664 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
665 table (lift_amount+1) t in
668 (fun (t, s, m, ug, eq_found) ->
669 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
672 (fun (t, s, m, ug, eq_found) ->
673 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
674 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
676 | C.Lambda (nn, s, t) ->
678 betaexpand_term metasenv context ugraph table lift_amount s in
680 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
681 table (lift_amount+1) t in
684 (fun (t, s, m, ug, eq_found) ->
685 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
688 (fun (t, s, m, ug, eq_found) ->
689 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
690 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
695 (fun arg (res, lifted_tl) ->
696 let arg_res, lifted_arg =
697 betaexpand_term metasenv context ugraph table lift_amount arg
701 (fun (a, s, m, ug, eq_found) ->
702 a::lifted_tl, s, m, ug, eq_found)
707 (fun (r, s, m, ug, eq_found) ->
708 lifted_arg::r, s, m, ug, eq_found)
710 lifted_arg::lifted_tl)
714 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
717 | t -> [], (S.lift lift_amount t)
720 | C.Meta (i, l) -> res, lifted_term
723 C.Implicit None, ugraph
724 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
728 metasenv context ugraph lift_amount term termty candidates
734 let sup_l_counter = ref 1;;
738 returns a list of new clauses inferred with a left superposition step
739 the negative equation "target" and one of the positive equations in "table"
741 let superposition_left newmeta (metasenv, context, ugraph) table target =
742 let module C = Cic in
743 let module S = CicSubstitution in
744 let module M = CicMetaSubst in
745 let module HL = HelmLibraryObjects in
746 let module CR = CicReduction in
747 let module U = Utils in
748 let weight, proof, (eq_ty, left, right, ordering), _, _ = target in
750 let term = if ordering = U.Gt then left else right in
751 betaexpand_term metasenv context ugraph table 0 term
753 let maxmeta = ref newmeta in
754 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
756 (* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
758 let time1 = Unix.gettimeofday () in
760 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
761 let what, other = if pos = Utils.Left then what, other else other, what in
762 let newgoal, newproof =
763 let bo' = apply_subst s (S.subst other bo) in
764 let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
768 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
769 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
770 S.lift 1 eq_ty; l; r]
775 CicMkImplicit.identity_relocation_list_for_metavariable context in
776 C.Meta (!maxmeta, irl)
781 if pos = Utils.Left then [ty; what; other]
782 else [ty; other; what]
784 Inference.ProofSymBlock (termlist, proof')
787 if pos = Utils.Left then what, other else other, what
789 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
793 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
794 Inference.BasicProof metaproof)
797 | Inference.BasicProof _ ->
798 (* debug_print (lazy "replacing a BasicProof"); *)
800 | Inference.ProofGoalBlock (_, parent_proof) ->
801 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
802 Inference.ProofGoalBlock (pb, parent_proof)
806 C.Appl [C.MutConstruct (* reflexivity *)
807 (LibraryObjects.eq_URI (), 0, 1, []);
808 eq_ty; if ordering = U.Gt then right else left]
811 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
814 if ordering = U.Gt then newgoal, right else left, newgoal in
815 let neworder = !Utils.compare_terms left right in
817 let time2 = Unix.gettimeofday () in
818 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
821 let w = Utils.compute_equality_weight eq_ty left right in
822 (w, newproof, (eq_ty, left, right, neworder), [], [])
826 !maxmeta, List.map build_new expansions
830 let sup_r_counter = ref 1;;
834 returns a list of new clauses inferred with a right superposition step
835 between the positive equation "target" and one in the "table" "newmeta" is
836 the first free meta index, i.e. the first number above the highest meta
837 index: its updated value is also returned
839 let superposition_right newmeta (metasenv, context, ugraph) table target =
840 let module C = Cic in
841 let module S = CicSubstitution in
842 let module M = CicMetaSubst in
843 let module HL = HelmLibraryObjects in
844 let module CR = CicReduction in
845 let module U = Utils in
846 let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
847 let metasenv' = metasenv @ newmetas in
848 let maxmeta = ref newmeta in
851 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
852 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
856 (fun (_, subst, _, _, _) ->
857 let subst = apply_subst subst in
858 let o = !Utils.compare_terms (subst l) (subst r) in
859 o <> U.Lt && o <> U.Le)
860 (fst (betaexpand_term metasenv' context ugraph table 0 l))
862 (res left right), (res right left)
864 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
866 let time1 = Unix.gettimeofday () in
868 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
869 let what, other = if pos = Utils.Left then what, other else other, what in
870 let newgoal, newproof =
871 let bo' = apply_subst s (S.subst other bo) in
873 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
876 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
877 (name, ty, S.lift 1 eq_ty, l, r)
879 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
883 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
884 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
885 S.lift 1 eq_ty; l; r]
888 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
890 let newmeta, newequality =
892 if ordering = U.Gt then newgoal, apply_subst s right
893 else apply_subst s left, newgoal in
894 let neworder = !Utils.compare_terms left right
895 and newmenv = newmetas @ menv'
896 and newargs = args @ args' in
898 let w = Utils.compute_equality_weight eq_ty left right in
899 (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
900 and env = (metasenv, context, ugraph) in
901 let newm, eq' = Inference.fix_metas !maxmeta eq' in
906 let time2 = Unix.gettimeofday () in
907 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
911 let new1 = List.map (build_new U.Gt) res1
912 and new2 = List.map (build_new U.Lt) res2 in
913 let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
915 (List.filter ok (new1 @ new2)))
919 (** demodulation, when the target is a goal *)
920 let rec demodulation_goal newmeta env table goal =
921 let module C = Cic in
922 let module S = CicSubstitution in
923 let module M = CicMetaSubst in
924 let module HL = HelmLibraryObjects in
925 let metasenv, context, ugraph = env in
926 let maxmeta = ref newmeta in
927 let proof, metas, term = goal in
928 let metasenv' = metasenv @ metas in
930 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
931 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
932 let what, other = if pos = Utils.Left then what, other else other, what in
934 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
935 with CicUtil.Meta_not_found _ -> ty
937 let newterm, newproof =
938 let bo = apply_subst subst (S.subst other t) in
939 let bo' = apply_subst subst t in
940 let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
945 CicMkImplicit.identity_relocation_list_for_metavariable context in
946 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
947 C.Meta (!maxmeta, irl)
952 if pos = Utils.Left then [ty; what; other]
953 else [ty; other; what]
955 Inference.ProofSymBlock (termlist, proof')
958 if pos = Utils.Left then what, other else other, what
960 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
964 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
965 eq_found, Inference.BasicProof metaproof)
967 let rec repl = function
968 | Inference.NoProof ->
969 (* debug_print (lazy "replacing a NoProof"); *)
971 | Inference.BasicProof _ ->
972 (* debug_print (lazy "replacing a BasicProof"); *)
974 | Inference.ProofGoalBlock (_, parent_proof) ->
975 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
976 Inference.ProofGoalBlock (pb, parent_proof)
977 | (Inference.SubProof (term, meta_index, p) as subproof) ->
980 (* (Printf.sprintf "replacing %s" *)
981 (* (Inference.string_of_proof subproof))); *)
982 Inference.SubProof (term, meta_index, repl p)
986 bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
988 let m = Inference.metas_of_term newterm in
989 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
990 !maxmeta, (newproof, newmetasenv, newterm)
993 demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
997 let newmeta, newgoal = build_newgoal t in
998 let _, _, newg = newgoal in
999 if Inference.meta_convertibility term newg then
1002 demodulation_goal newmeta env table newgoal
1008 (** demodulation, when the target is a theorem *)
1009 let rec demodulation_theorem newmeta env table theorem =
1010 let module C = Cic in
1011 let module S = CicSubstitution in
1012 let module M = CicMetaSubst in
1013 let module HL = HelmLibraryObjects in
1014 let metasenv, context, ugraph = env in
1015 let maxmeta = ref newmeta in
1016 let proof, metas, term = theorem in
1017 let term, termty, metas = theorem in
1018 let metasenv' = metasenv @ metas in
1020 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1021 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1022 let what, other = if pos = Utils.Left then what, other else other, what in
1023 let newterm, newty =
1024 let bo = apply_subst subst (S.subst other t) in
1025 let bo' = apply_subst subst t in
1026 let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1029 Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1030 Inference.BasicProof term)
1032 (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 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