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 (* returns a list of all the equalities in the tree that are in relation
129 "mode" with the given term, where mode can be either Matching or
132 Format of the return value: list of tuples in the form:
133 (position - Left or Right - of the term that matched the given one in this
137 Note that if equality is "left = right", if the ordering is left > right,
138 the position will always be Left, and if the ordering is left < right,
139 position will be Right.
141 let get_candidates mode tree term =
142 let t1 = Unix.gettimeofday () in
146 | Matching -> Discrimination_tree.retrieve_generalizations tree term
147 | Unification -> Discrimination_tree.retrieve_unifiables tree term
149 Discrimination_tree.PosEqSet.elements s
151 (* print_candidates mode term res; *)
152 (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
153 (* print_newline (); *)
154 let t2 = Unix.gettimeofday () in
155 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
160 let match_unif_time_ok = ref 0.;;
161 let match_unif_time_no = ref 0.;;
165 finds the first equality in the index that matches "term", of type "termty"
166 termty can be Implicit if it is not needed. The result (one of the sides of
167 the equality, actually) should be not greater (wrt the term ordering) than
170 Format of the return value:
172 (term to substitute, [Cic.Rel 1 properly lifted - see the various
173 build_newtarget functions inside the various
174 demodulation_* functions]
175 substitution used for the matching,
177 ugraph, [substitution, metasenv and ugraph have the same meaning as those
178 returned by CicUnification.fo_unif]
179 (equality where the matching term was found, [i.e. the equality to use as
181 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
182 the equality: this is used to build the proof term, again see one of
183 the build_newtarget functions]
186 let rec find_matches metasenv context ugraph lift_amount term termty =
187 let module C = Cic in
188 let module U = Utils in
189 let module S = CicSubstitution in
190 let module M = CicMetaSubst in
191 let module HL = HelmLibraryObjects in
192 let cmp = !Utils.compare_terms in
193 let check = match termty with C.Implicit None -> false | _ -> true in
197 let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
198 if check && not (fst (CicReduction.are_convertible
199 ~metasenv context termty ty ugraph)) then (
200 find_matches metasenv context ugraph lift_amount term termty tl
202 let do_match c eq_URI =
203 let subst', metasenv', ugraph' =
204 let t1 = Unix.gettimeofday () in
207 Inference.matching (metasenv @ metas) context
208 term (S.lift lift_amount c) ugraph in
209 let t2 = Unix.gettimeofday () in
210 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
212 with Inference.MatchingFailure as e ->
213 let t2 = Unix.gettimeofday () in
214 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
217 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
220 let c, other, eq_URI =
221 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
222 else right, left, Utils.eq_ind_r_URI ()
224 if o <> U.Incomparable then
227 with Inference.MatchingFailure ->
228 find_matches metasenv context ugraph lift_amount term termty tl
231 try do_match c eq_URI
232 with Inference.MatchingFailure -> None
235 | Some (_, s, _, _, _) ->
236 let c' = apply_subst s c
237 and other' = apply_subst s other in
238 let order = cmp c' other' in
239 let names = U.names_of_context context in
244 metasenv context ugraph lift_amount term termty tl
246 find_matches metasenv context ugraph lift_amount term termty tl
251 as above, but finds all the matching equalities, and the matching condition
252 can be either Inference.matching or Inference.unification
254 let rec find_all_matches ?(unif_fun=Inference.unification)
255 metasenv context ugraph lift_amount term termty =
256 let module C = Cic in
257 let module U = Utils in
258 let module S = CicSubstitution in
259 let module M = CicMetaSubst in
260 let module HL = HelmLibraryObjects in
261 let cmp = !Utils.compare_terms in
265 let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
266 let do_match c eq_URI =
267 let subst', metasenv', ugraph' =
268 let t1 = Unix.gettimeofday () in
271 unif_fun (metasenv @ metas) context
272 term (S.lift lift_amount c) ugraph in
273 let t2 = Unix.gettimeofday () in
274 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
277 | Inference.MatchingFailure
278 | CicUnification.UnificationFailure _
279 | CicUnification.Uncertain _ as e ->
280 let t2 = Unix.gettimeofday () in
281 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
284 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
287 let c, other, eq_URI =
288 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
289 else right, left, Utils.eq_ind_r_URI ()
291 if o <> U.Incomparable then
293 let res = do_match c eq_URI in
294 res::(find_all_matches ~unif_fun metasenv context ugraph
295 lift_amount term termty tl)
297 | Inference.MatchingFailure
298 | CicUnification.UnificationFailure _
299 | CicUnification.Uncertain _ ->
300 find_all_matches ~unif_fun metasenv context ugraph
301 lift_amount term termty tl
304 let res = do_match c eq_URI in
307 let c' = apply_subst s c
308 and other' = apply_subst s other in
309 let order = cmp c' other' in
310 let names = U.names_of_context context in
311 if order <> U.Lt && order <> U.Le then
312 res::(find_all_matches ~unif_fun metasenv context ugraph
313 lift_amount term termty tl)
315 find_all_matches ~unif_fun metasenv context ugraph
316 lift_amount term termty tl
318 | Inference.MatchingFailure
319 | CicUnification.UnificationFailure _
320 | CicUnification.Uncertain _ ->
321 find_all_matches ~unif_fun metasenv context ugraph
322 lift_amount term termty tl
327 returns true if target is subsumed by some equality in table
329 let subsumption env table target =
330 let _, _, (ty, left, right, _), tmetas, _ = target in
331 let metasenv, context, ugraph = env in
332 let metasenv = metasenv @ tmetas in
333 let samesubst subst subst' =
334 let tbl = Hashtbl.create (List.length subst) in
335 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
337 (fun (m, (c, t1, t2)) ->
339 let c', t1', t2' = Hashtbl.find tbl m in
340 if (c = c') && (t1 = t1') && (t2 = t2') then true
350 let leftc = get_candidates Matching table left in
351 find_all_matches ~unif_fun:Inference.matching
352 metasenv context ugraph 0 left ty leftc
354 let rec ok what = function
356 | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
358 let other = if pos = Utils.Left then r else l in
359 let subst', menv', ug' =
360 let t1 = Unix.gettimeofday () in
363 Inference.matching (metasenv @ menv @ m) context what other ugraph
365 let t2 = Unix.gettimeofday () in
366 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
368 with Inference.MatchingFailure as e ->
369 let t2 = Unix.gettimeofday () in
370 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
373 if samesubst subst subst' then
377 with Inference.MatchingFailure ->
380 let r, subst = ok right leftr in
389 let rightc = get_candidates Matching table right in
390 find_all_matches ~unif_fun:Inference.matching
391 metasenv context ugraph 0 right ty rightc
398 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
399 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
404 let rec demodulation_aux ?(typecheck=false)
405 metasenv context ugraph table lift_amount term =
406 let module C = Cic in
407 let module S = CicSubstitution in
408 let module M = CicMetaSubst in
409 let module HL = HelmLibraryObjects in
410 let candidates = get_candidates Matching table term in
416 CicTypeChecker.type_of_aux' metasenv context term ugraph
418 C.Implicit None, ugraph
421 find_matches metasenv context ugraph lift_amount term termty candidates
432 (res, tl @ [S.lift 1 t])
435 demodulation_aux metasenv context ugraph table
439 | None -> (None, tl @ [S.lift 1 t])
440 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
445 | Some (_, subst, menv, ug, eq_found) ->
446 Some (C.Appl ll, subst, menv, ug, eq_found)
448 | C.Prod (nn, s, t) ->
450 demodulation_aux metasenv context ugraph table lift_amount s in (
454 demodulation_aux metasenv
455 ((Some (nn, C.Decl s))::context) ugraph
456 table (lift_amount+1) t
460 | Some (t', subst, menv, ug, eq_found) ->
461 Some (C.Prod (nn, (S.lift 1 s), t'),
462 subst, menv, ug, eq_found)
464 | Some (s', subst, menv, ug, eq_found) ->
465 Some (C.Prod (nn, s', (S.lift 1 t)),
466 subst, menv, ug, eq_found)
468 | C.Lambda (nn, s, t) ->
470 demodulation_aux metasenv context ugraph table lift_amount s in (
474 demodulation_aux metasenv
475 ((Some (nn, C.Decl s))::context) ugraph
476 table (lift_amount+1) t
480 | Some (t', subst, menv, ug, eq_found) ->
481 Some (C.Lambda (nn, (S.lift 1 s), t'),
482 subst, menv, ug, eq_found)
484 | Some (s', subst, menv, ug, eq_found) ->
485 Some (C.Lambda (nn, s', (S.lift 1 t)),
486 subst, menv, ug, eq_found)
493 let build_newtarget_time = ref 0.;;
496 let demod_counter = ref 1;;
498 (** demodulation, when target is an equality *)
499 let rec demodulation_equality newmeta env table sign target =
500 let module C = Cic in
501 let module S = CicSubstitution in
502 let module M = CicMetaSubst in
503 let module HL = HelmLibraryObjects in
504 let metasenv, context, ugraph = env in
505 let _, proof, (eq_ty, left, right, order), metas, args = target in
506 let metasenv' = metasenv @ metas in
508 let maxmeta = ref newmeta in
510 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
511 let time1 = Unix.gettimeofday () in
513 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
515 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
516 with CicUtil.Meta_not_found _ -> ty
518 let what, other = if pos = Utils.Left then what, other else other, what in
519 let newterm, newproof =
520 let bo = apply_subst subst (S.subst other t) in
521 let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
524 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
525 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
526 S.lift 1 eq_ty; l; r]
528 if sign = Utils.Positive then
530 Inference.ProofBlock (
531 subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
536 CicMkImplicit.identity_relocation_list_for_metavariable context in
537 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
538 (* print_newline (); *)
539 C.Meta (!maxmeta, irl)
544 if pos = Utils.Left then [ty; what; other]
545 else [ty; other; what]
547 Inference.ProofSymBlock (termlist, proof')
550 if pos = Utils.Left then what, other else other, what
552 pos, (0, proof', (ty, other, what, Utils.Incomparable),
557 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
558 eq_found, Inference.BasicProof metaproof)
561 | Inference.BasicProof _ ->
562 print_endline "replacing a BasicProof";
564 | Inference.ProofGoalBlock (_, parent_proof) ->
565 print_endline "replacing another ProofGoalBlock";
566 Inference.ProofGoalBlock (pb, parent_proof)
570 C.Appl [C.MutConstruct (* reflexivity *)
571 (LibraryObjects.eq_URI (), 0, 1, []);
572 eq_ty; if is_left then right else left]
575 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
577 let left, right = if is_left then newterm, right else left, newterm in
578 let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
579 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
582 let ordering = !Utils.compare_terms left right in
584 let time2 = Unix.gettimeofday () in
585 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
588 let w = Utils.compute_equality_weight eq_ty left right in
589 (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
593 let res = demodulation_aux metasenv' context ugraph table 0 left in
594 let newmeta, newtarget =
597 let newmeta, newtarget = build_newtarget true t in
598 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
599 (Inference.meta_convertibility_eq target newtarget) then
602 demodulation_equality newmeta env table sign newtarget
604 let res = demodulation_aux metasenv' context ugraph table 0 right in
607 let newmeta, newtarget = build_newtarget false t in
608 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
609 (Inference.meta_convertibility_eq target newtarget) then
612 demodulation_equality newmeta env table sign newtarget
616 (* newmeta, newtarget *)
617 (* tentiamo di ridurre usando CicReduction.normalize *)
618 let w, p, (ty, left, right, o), m, a = newtarget in
619 let left' = ProofEngineReduction.simpl context left in
620 let right' = ProofEngineReduction.simpl context right in
622 if !Utils.compare_terms left' left = Utils.Lt then left' else left in
624 if !Utils.compare_terms right' right = Utils.Lt then right' else right in
625 (* if newleft != left || newright != right then ( *)
628 (* (Printf.sprintf "left: %s, left': %s\nright: %s, right': %s\n" *)
629 (* (CicPp.ppterm left) (CicPp.ppterm left') (CicPp.ppterm right) *)
630 (* (CicPp.ppterm right'))) *)
632 let w' = Utils.compute_equality_weight ty newleft newright in
633 let o' = !Utils.compare_terms newleft newright in
634 newmeta, (w', p, (ty, newleft, newright, o'), m, a)
639 Performs the beta expansion of the term "term" w.r.t. "table",
640 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
643 let rec betaexpand_term metasenv context ugraph table lift_amount term =
644 let module C = Cic in
645 let module S = CicSubstitution in
646 let module M = CicMetaSubst in
647 let module HL = HelmLibraryObjects in
648 let candidates = get_candidates Unification table term in
649 let res, lifted_term =
654 (fun arg (res, lifted_tl) ->
657 let arg_res, lifted_arg =
658 betaexpand_term metasenv context ugraph table
662 (fun (t, s, m, ug, eq_found) ->
663 (Some t)::lifted_tl, s, m, ug, eq_found)
668 (fun (l, s, m, ug, eq_found) ->
669 (Some lifted_arg)::l, s, m, ug, eq_found)
671 (Some lifted_arg)::lifted_tl)
674 (fun (r, s, m, ug, eq_found) ->
675 None::r, s, m, ug, eq_found) res,
681 (fun (l, s, m, ug, eq_found) ->
682 (C.Meta (i, l), s, m, ug, eq_found)) l'
684 e, C.Meta (i, lifted_l)
687 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
689 | C.Prod (nn, s, t) ->
691 betaexpand_term metasenv context ugraph table lift_amount s in
693 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
694 table (lift_amount+1) t in
697 (fun (t, s, m, ug, eq_found) ->
698 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
701 (fun (t, s, m, ug, eq_found) ->
702 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
703 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
705 | C.Lambda (nn, s, t) ->
707 betaexpand_term metasenv context ugraph table lift_amount s in
709 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
710 table (lift_amount+1) t in
713 (fun (t, s, m, ug, eq_found) ->
714 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
717 (fun (t, s, m, ug, eq_found) ->
718 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
719 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
724 (fun arg (res, lifted_tl) ->
725 let arg_res, lifted_arg =
726 betaexpand_term metasenv context ugraph table lift_amount arg
730 (fun (a, s, m, ug, eq_found) ->
731 a::lifted_tl, s, m, ug, eq_found)
736 (fun (r, s, m, ug, eq_found) ->
737 lifted_arg::r, s, m, ug, eq_found)
739 lifted_arg::lifted_tl)
743 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
746 | t -> [], (S.lift lift_amount t)
749 | C.Meta (i, l) -> res, lifted_term
752 C.Implicit None, ugraph
753 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
757 metasenv context ugraph lift_amount term termty candidates
763 let sup_l_counter = ref 1;;
767 returns a list of new clauses inferred with a left superposition step
768 the negative equation "target" and one of the positive equations in "table"
770 let superposition_left newmeta (metasenv, context, ugraph) table target =
771 let module C = Cic in
772 let module S = CicSubstitution in
773 let module M = CicMetaSubst in
774 let module HL = HelmLibraryObjects in
775 let module CR = CicReduction in
776 let module U = Utils in
777 let weight, proof, (eq_ty, left, right, ordering), _, _ = target in
779 let term = if ordering = U.Gt then left else right in
780 betaexpand_term metasenv context ugraph table 0 term
782 let maxmeta = ref newmeta in
783 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
785 (* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
787 let time1 = Unix.gettimeofday () in
789 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
790 let what, other = if pos = Utils.Left then what, other else other, what in
791 let newgoal, newproof =
792 let bo' = apply_subst s (S.subst other bo) in
793 let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
797 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
798 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
799 S.lift 1 eq_ty; l; r]
804 CicMkImplicit.identity_relocation_list_for_metavariable context in
805 C.Meta (!maxmeta, irl)
810 if pos = Utils.Left then [ty; what; other]
811 else [ty; other; what]
813 Inference.ProofSymBlock (termlist, proof')
816 if pos = Utils.Left then what, other else other, what
818 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
822 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
823 Inference.BasicProof metaproof)
826 | Inference.BasicProof _ ->
827 (* debug_print (lazy "replacing a BasicProof"); *)
829 | Inference.ProofGoalBlock (_, parent_proof) ->
830 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
831 Inference.ProofGoalBlock (pb, parent_proof)
835 C.Appl [C.MutConstruct (* reflexivity *)
836 (LibraryObjects.eq_URI (), 0, 1, []);
837 eq_ty; if ordering = U.Gt then right else left]
840 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
843 if ordering = U.Gt then newgoal, right else left, newgoal in
844 let neworder = !Utils.compare_terms left right in
846 let time2 = Unix.gettimeofday () in
847 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
850 let w = Utils.compute_equality_weight eq_ty left right in
851 (w, newproof, (eq_ty, left, right, neworder), [], [])
855 !maxmeta, List.map build_new expansions
859 let sup_r_counter = ref 1;;
863 returns a list of new clauses inferred with a right superposition step
864 between the positive equation "target" and one in the "table" "newmeta" is
865 the first free meta index, i.e. the first number above the highest meta
866 index: its updated value is also returned
868 let superposition_right newmeta (metasenv, context, ugraph) table target =
869 let module C = Cic in
870 let module S = CicSubstitution in
871 let module M = CicMetaSubst in
872 let module HL = HelmLibraryObjects in
873 let module CR = CicReduction in
874 let module U = Utils in
875 let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
876 let metasenv' = metasenv @ newmetas in
877 let maxmeta = ref newmeta in
880 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
881 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
885 (fun (_, subst, _, _, _) ->
886 let subst = apply_subst subst in
887 let o = !Utils.compare_terms (subst l) (subst r) in
888 o <> U.Lt && o <> U.Le)
889 (fst (betaexpand_term metasenv' context ugraph table 0 l))
891 (res left right), (res right left)
893 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
895 let time1 = Unix.gettimeofday () in
897 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
898 let what, other = if pos = Utils.Left then what, other else other, what in
899 let newgoal, newproof =
900 let bo' = apply_subst s (S.subst other bo) in
902 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
905 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
906 (name, ty, S.lift 1 eq_ty, l, r)
908 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
912 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
913 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
914 S.lift 1 eq_ty; l; r]
917 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
919 let newmeta, newequality =
921 if ordering = U.Gt then newgoal, apply_subst s right
922 else apply_subst s left, newgoal in
923 let neworder = !Utils.compare_terms left right
924 and newmenv = newmetas @ menv'
925 and newargs = args @ args' in
927 let w = Utils.compute_equality_weight eq_ty left right in
928 (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
929 and env = (metasenv, context, ugraph) in
930 let newm, eq' = Inference.fix_metas !maxmeta eq' in
935 let time2 = Unix.gettimeofday () in
936 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
940 let new1 = List.map (build_new U.Gt) res1
941 and new2 = List.map (build_new U.Lt) res2 in
942 let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
944 (List.filter ok (new1 @ new2)))
948 (** demodulation, when the target is a goal *)
949 let rec demodulation_goal newmeta env table goal =
950 let module C = Cic in
951 let module S = CicSubstitution in
952 let module M = CicMetaSubst in
953 let module HL = HelmLibraryObjects in
954 let metasenv, context, ugraph = env in
955 let maxmeta = ref newmeta in
956 let proof, metas, term = goal in
957 let metasenv' = metasenv @ metas in
959 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
960 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
961 let what, other = if pos = Utils.Left then what, other else other, what in
963 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
964 with CicUtil.Meta_not_found _ -> ty
966 let newterm, newproof =
967 let bo = apply_subst subst (S.subst other t) in
968 let bo' = apply_subst subst t in
969 let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
974 CicMkImplicit.identity_relocation_list_for_metavariable context in
975 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
976 C.Meta (!maxmeta, irl)
981 if pos = Utils.Left then [ty; what; other]
982 else [ty; other; what]
984 Inference.ProofSymBlock (termlist, proof')
987 if pos = Utils.Left then what, other else other, what
989 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
993 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
994 eq_found, Inference.BasicProof metaproof)
996 let rec repl = function
997 | Inference.NoProof ->
998 (* debug_print (lazy "replacing a NoProof"); *)
1000 | Inference.BasicProof _ ->
1001 (* debug_print (lazy "replacing a BasicProof"); *)
1003 | Inference.ProofGoalBlock (_, parent_proof) ->
1004 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
1005 Inference.ProofGoalBlock (pb, parent_proof)
1006 | (Inference.SubProof (term, meta_index, p) as subproof) ->
1009 (* (Printf.sprintf "replacing %s" *)
1010 (* (Inference.string_of_proof subproof))); *)
1011 Inference.SubProof (term, meta_index, repl p)
1015 bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
1017 let m = Inference.metas_of_term newterm in
1018 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
1019 !maxmeta, (newproof, newmetasenv, newterm)
1022 demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
1026 let newmeta, newgoal = build_newgoal t in
1027 let _, _, newg = newgoal in
1028 if Inference.meta_convertibility term newg then
1031 demodulation_goal newmeta env table newgoal
1037 (** demodulation, when the target is a theorem *)
1038 let rec demodulation_theorem newmeta env table theorem =
1039 let module C = Cic in
1040 let module S = CicSubstitution in
1041 let module M = CicMetaSubst in
1042 let module HL = HelmLibraryObjects in
1043 let metasenv, context, ugraph = env in
1044 let maxmeta = ref newmeta in
1045 let proof, metas, term = theorem in
1046 let term, termty, metas = theorem in
1047 let metasenv' = metasenv @ metas in
1049 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1050 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1051 let what, other = if pos = Utils.Left then what, other else other, what in
1052 let newterm, newty =
1053 let bo = apply_subst subst (S.subst other t) in
1054 let bo' = apply_subst subst t in
1055 let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1058 Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1059 Inference.BasicProof term)
1061 (Inference.build_proof_term newproof, bo)
1063 let m = Inference.metas_of_term newterm in
1064 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
1065 !maxmeta, (newterm, newty, newmetasenv)
1068 demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty
1072 let newmeta, newthm = build_newtheorem t in
1073 let newt, newty, _ = newthm in
1074 if Inference.meta_convertibility termty newty then
1077 demodulation_theorem newmeta env table newthm