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;;
36 type retrieval_mode = Matching | Unification;;
38 let print_candidates mode term res =
42 Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
44 Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
50 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
51 (Inference.string_of_equality e))
57 let indexing_retrieval_time = ref 0.;;
60 let apply_subst = CicMetaSubst.apply_subst
62 let index = Index.index
63 let remove_index = Index.remove_index
64 let in_index = Index.in_index
65 let empty = Index.empty
66 let init_index = Index.init_index
68 (* returns a list of all the equalities in the tree that are in relation
69 "mode" with the given term, where mode can be either Matching or
72 Format of the return value: list of tuples in the form:
73 (position - Left or Right - of the term that matched the given one in this
77 Note that if equality is "left = right", if the ordering is left > right,
78 the position will always be Left, and if the ordering is left < right,
79 position will be Right.
81 let get_candidates mode tree term =
82 let t1 = Unix.gettimeofday () in
86 | Matching -> Index.retrieve_generalizations tree term
87 | Unification -> Index.retrieve_unifiables tree term
89 Index.PosEqSet.elements s
91 (* print_candidates mode term res; *)
92 (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
93 (* print_newline (); *)
94 let t2 = Unix.gettimeofday () in
95 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
100 let match_unif_time_ok = ref 0.;;
101 let match_unif_time_no = ref 0.;;
105 finds the first equality in the index that matches "term", of type "termty"
106 termty can be Implicit if it is not needed. The result (one of the sides of
107 the equality, actually) should be not greater (wrt the term ordering) than
110 Format of the return value:
112 (term to substitute, [Cic.Rel 1 properly lifted - see the various
113 build_newtarget functions inside the various
114 demodulation_* functions]
115 substitution used for the matching,
117 ugraph, [substitution, metasenv and ugraph have the same meaning as those
118 returned by CicUnification.fo_unif]
119 (equality where the matching term was found, [i.e. the equality to use as
121 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
122 the equality: this is used to build the proof term, again see one of
123 the build_newtarget functions]
126 let rec find_matches metasenv context ugraph lift_amount term termty =
127 let module C = Cic in
128 let module U = Utils in
129 let module S = CicSubstitution in
130 let module M = CicMetaSubst in
131 let module HL = HelmLibraryObjects in
132 let cmp = !Utils.compare_terms in
133 ignore(CicTypeChecker.type_of_aux' metasenv context term);
134 let check = match termty with C.Implicit None -> false | _ -> true in
138 let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
139 if check && not (fst (CicReduction.are_convertible
140 ~metasenv context termty ty ugraph)) then (
141 find_matches metasenv context ugraph lift_amount term termty tl
143 let do_match c eq_URI =
144 let subst', metasenv', ugraph' =
145 let t1 = Unix.gettimeofday () in
148 Inference.matching (metasenv @ metas) context
149 term (S.lift lift_amount c) ugraph
151 let t2 = Unix.gettimeofday () in
152 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
155 | Inference.MatchingFailure as e ->
156 let t2 = Unix.gettimeofday () in
157 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
159 | CicUtil.Meta_not_found _ as exn ->
160 prerr_endline "siam qua"; raise exn
162 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
165 let c, other, eq_URI =
166 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
167 else right, left, Utils.eq_ind_r_URI ()
169 if o <> U.Incomparable then
172 with Inference.MatchingFailure ->
173 find_matches metasenv context ugraph lift_amount term termty tl
176 try do_match c eq_URI
177 with Inference.MatchingFailure -> None
180 | Some (_, s, _, _, _) ->
181 let c' = apply_subst s c in
183 let other' = U.guarded_simpl context (apply_subst s other) in *)
184 let other' = apply_subst s other in
185 let order = cmp c' other' in
190 metasenv context ugraph lift_amount term termty tl
192 find_matches metasenv context ugraph lift_amount term termty tl
197 as above, but finds all the matching equalities, and the matching condition
198 can be either Inference.matching or Inference.unification
200 let rec find_all_matches ?(unif_fun=Inference.unification)
201 metasenv context ugraph lift_amount term termty =
202 let module C = Cic in
203 let module U = Utils in
204 let module S = CicSubstitution in
205 let module M = CicMetaSubst in
206 let module HL = HelmLibraryObjects in
207 let cmp = !Utils.compare_terms in
211 let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
212 let do_match c eq_URI =
213 let subst', metasenv', ugraph' =
214 let t1 = Unix.gettimeofday () in
217 unif_fun (metasenv @ metas) context
218 term (S.lift lift_amount c) ugraph in
219 let t2 = Unix.gettimeofday () in
220 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
223 | Inference.MatchingFailure
224 | CicUnification.UnificationFailure _
225 | CicUnification.Uncertain _ as e ->
226 let t2 = Unix.gettimeofday () in
227 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
230 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
233 let c, other, eq_URI =
234 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
235 else right, left, Utils.eq_ind_r_URI ()
237 if o <> U.Incomparable then
239 let res = do_match c eq_URI in
240 res::(find_all_matches ~unif_fun metasenv context ugraph
241 lift_amount term termty tl)
243 | Inference.MatchingFailure
244 | CicUnification.UnificationFailure _
245 | CicUnification.Uncertain _ ->
246 find_all_matches ~unif_fun metasenv context ugraph
247 lift_amount term termty tl
250 let res = do_match c eq_URI in
253 let c' = apply_subst s c
254 and other' = apply_subst s other in
255 let order = cmp c' other' in
256 if order <> U.Lt && order <> U.Le then
257 res::(find_all_matches ~unif_fun metasenv context ugraph
258 lift_amount term termty tl)
260 find_all_matches ~unif_fun metasenv context ugraph
261 lift_amount term termty tl
263 | Inference.MatchingFailure
264 | CicUnification.UnificationFailure _
265 | CicUnification.Uncertain _ ->
266 find_all_matches ~unif_fun metasenv context ugraph
267 lift_amount term termty tl
272 returns true if target is subsumed by some equality in table
274 let subsumption env table target =
275 let _, _, (ty, left, right, _), tmetas, _ = target in
276 let metasenv, context, ugraph = env in
277 let metasenv = metasenv @ tmetas in
278 let samesubst subst subst' =
279 let tbl = Hashtbl.create (List.length subst) in
280 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
282 (fun (m, (c, t1, t2)) ->
284 let c', t1', t2' = Hashtbl.find tbl m in
285 if (c = c') && (t1 = t1') && (t2 = t2') then true
295 let leftc = get_candidates Matching table left in
296 find_all_matches ~unif_fun:Inference.matching
297 metasenv context ugraph 0 left ty leftc
299 let rec ok what = function
301 | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
303 let other = if pos = Utils.Left then r else l in
304 let subst', menv', ug' =
305 let t1 = Unix.gettimeofday () in
308 Inference.matching (metasenv @ menv @ m) context what other ugraph
310 let t2 = Unix.gettimeofday () in
311 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
313 with Inference.MatchingFailure as e ->
314 let t2 = Unix.gettimeofday () in
315 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
318 if samesubst subst subst' then
322 with Inference.MatchingFailure ->
325 let r, subst = ok right leftr in
334 let rightc = get_candidates Matching table right in
335 find_all_matches ~unif_fun:Inference.matching
336 metasenv context ugraph 0 right ty rightc
343 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
344 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
349 let rec demodulation_aux ?(typecheck=false)
350 metasenv context ugraph table lift_amount term =
351 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
353 let module C = Cic in
354 let module S = CicSubstitution in
355 let module M = CicMetaSubst in
356 let module HL = HelmLibraryObjects in
357 let candidates = get_candidates Matching table term in
363 CicTypeChecker.type_of_aux' metasenv context term ugraph
365 C.Implicit None, ugraph
368 find_matches metasenv context ugraph lift_amount term termty candidates
379 (res, tl @ [S.lift 1 t])
382 demodulation_aux metasenv context ugraph table
386 | None -> (None, tl @ [S.lift 1 t])
387 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
392 | Some (_, subst, menv, ug, eq_found) ->
393 Some (C.Appl ll, subst, menv, ug, eq_found)
395 | C.Prod (nn, s, t) ->
397 demodulation_aux metasenv context ugraph table lift_amount s in (
401 demodulation_aux metasenv
402 ((Some (nn, C.Decl s))::context) ugraph
403 table (lift_amount+1) t
407 | Some (t', subst, menv, ug, eq_found) ->
408 Some (C.Prod (nn, (S.lift 1 s), t'),
409 subst, menv, ug, eq_found)
411 | Some (s', subst, menv, ug, eq_found) ->
412 Some (C.Prod (nn, s', (S.lift 1 t)),
413 subst, menv, ug, eq_found)
415 | C.Lambda (nn, s, t) ->
417 demodulation_aux metasenv context ugraph table lift_amount s in (
421 demodulation_aux metasenv
422 ((Some (nn, C.Decl s))::context) ugraph
423 table (lift_amount+1) t
427 | Some (t', subst, menv, ug, eq_found) ->
428 Some (C.Lambda (nn, (S.lift 1 s), t'),
429 subst, menv, ug, eq_found)
431 | Some (s', subst, menv, ug, eq_found) ->
432 Some (C.Lambda (nn, s', (S.lift 1 t)),
433 subst, menv, ug, eq_found)
440 let build_newtarget_time = ref 0.;;
443 let demod_counter = ref 1;;
445 (** demodulation, when target is an equality *)
446 let rec demodulation_equality newmeta env table sign target =
447 let module C = Cic in
448 let module S = CicSubstitution in
449 let module M = CicMetaSubst in
450 let module HL = HelmLibraryObjects in
451 let module U = Utils in
452 let metasenv, context, ugraph = env in
453 let w, proof, (eq_ty, left, right, order), metas, args = target in
454 (* first, we simplify *)
455 let right = U.guarded_simpl context right in
456 let left = U.guarded_simpl context left in
457 let w = Utils.compute_equality_weight eq_ty left right in
458 let order = !Utils.compare_terms left right in
459 let target = w, proof, (eq_ty, left, right, order), metas, args in
461 let metasenv' = metasenv @ metas in
463 let maxmeta = ref newmeta in
465 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
466 let time1 = Unix.gettimeofday () in
468 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
470 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
471 with CicUtil.Meta_not_found _ -> ty
473 let what, other = if pos = Utils.Left then what, other else other, what in
474 let newterm, newproof =
475 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
476 let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
479 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
480 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
481 S.lift 1 eq_ty; l; r]
483 if sign = Utils.Positive then
485 Inference.ProofBlock (
486 subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
491 CicMkImplicit.identity_relocation_list_for_metavariable context in
492 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
493 (* print_newline (); *)
494 C.Meta (!maxmeta, irl)
499 if pos = Utils.Left then [ty; what; other]
500 else [ty; other; what]
502 Inference.ProofSymBlock (termlist, proof')
505 if pos = Utils.Left then what, other else other, what
507 pos, (0, proof', (ty, other, what, Utils.Incomparable),
512 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
513 eq_found, Inference.BasicProof metaproof)
516 | Inference.BasicProof _ ->
517 print_endline "replacing a BasicProof";
519 | Inference.ProofGoalBlock (_, parent_proof) ->
520 print_endline "replacing another ProofGoalBlock";
521 Inference.ProofGoalBlock (pb, parent_proof)
525 C.Appl [C.MutConstruct (* reflexivity *)
526 (LibraryObjects.eq_URI (), 0, 1, []);
527 eq_ty; if is_left then right else left]
530 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
532 let left, right = if is_left then newterm, right else left, newterm in
533 let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
534 (* let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') *)
535 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metasenv' @ menv')
538 let ordering = !Utils.compare_terms left right in
540 let time2 = Unix.gettimeofday () in
541 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
544 let w = Utils.compute_equality_weight eq_ty left right in
545 (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
549 let res = demodulation_aux metasenv' context ugraph table 0 left in
550 let newmeta, newtarget =
553 let newmeta, newtarget = build_newtarget true t in
554 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
555 (Inference.meta_convertibility_eq target newtarget) then
558 demodulation_equality newmeta env table sign newtarget
560 let res = demodulation_aux metasenv' context ugraph table 0 right in
563 let newmeta, newtarget = build_newtarget false t in
564 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
565 (Inference.meta_convertibility_eq target newtarget) then
568 demodulation_equality newmeta env table sign newtarget
572 (* newmeta, newtarget *)
578 Performs the beta expansion of the term "term" w.r.t. "table",
579 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
582 let rec betaexpand_term metasenv context ugraph table lift_amount term =
583 let module C = Cic in
584 let module S = CicSubstitution in
585 let module M = CicMetaSubst in
586 let module HL = HelmLibraryObjects in
587 let candidates = get_candidates Unification table term in
588 let res, lifted_term =
593 (fun arg (res, lifted_tl) ->
596 let arg_res, lifted_arg =
597 betaexpand_term metasenv context ugraph table
601 (fun (t, s, m, ug, eq_found) ->
602 (Some t)::lifted_tl, s, m, ug, eq_found)
607 (fun (l, s, m, ug, eq_found) ->
608 (Some lifted_arg)::l, s, m, ug, eq_found)
610 (Some lifted_arg)::lifted_tl)
613 (fun (r, s, m, ug, eq_found) ->
614 None::r, s, m, ug, eq_found) res,
620 (fun (l, s, m, ug, eq_found) ->
621 (C.Meta (i, l), s, m, ug, eq_found)) l'
623 e, C.Meta (i, lifted_l)
626 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
628 | C.Prod (nn, s, t) ->
630 betaexpand_term metasenv context ugraph table lift_amount s in
632 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
633 table (lift_amount+1) t in
636 (fun (t, s, m, ug, eq_found) ->
637 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
640 (fun (t, s, m, ug, eq_found) ->
641 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
642 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
644 | C.Lambda (nn, s, t) ->
646 betaexpand_term metasenv context ugraph table lift_amount s in
648 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
649 table (lift_amount+1) t in
652 (fun (t, s, m, ug, eq_found) ->
653 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
656 (fun (t, s, m, ug, eq_found) ->
657 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
658 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
663 (fun arg (res, lifted_tl) ->
664 let arg_res, lifted_arg =
665 betaexpand_term metasenv context ugraph table lift_amount arg
669 (fun (a, s, m, ug, eq_found) ->
670 a::lifted_tl, s, m, ug, eq_found)
675 (fun (r, s, m, ug, eq_found) ->
676 lifted_arg::r, s, m, ug, eq_found)
678 lifted_arg::lifted_tl)
682 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
685 | t -> [], (S.lift lift_amount t)
688 | C.Meta (i, l) -> res, lifted_term
691 C.Implicit None, ugraph
692 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
696 metasenv context ugraph lift_amount term termty candidates
702 let sup_l_counter = ref 1;;
706 returns a list of new clauses inferred with a left superposition step
707 the negative equation "target" and one of the positive equations in "table"
709 let superposition_left newmeta (metasenv, context, ugraph) table target =
710 let module C = Cic in
711 let module S = CicSubstitution in
712 let module M = CicMetaSubst in
713 let module HL = HelmLibraryObjects in
714 let module CR = CicReduction in
715 let module U = Utils in
716 let weight, proof, (eq_ty, left, right, ordering), _, _ = target in
718 let term = if ordering = U.Gt then left else right in
719 betaexpand_term metasenv context ugraph table 0 term
721 let maxmeta = ref newmeta in
722 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
724 (* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
726 let time1 = Unix.gettimeofday () in
728 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
729 let what, other = if pos = Utils.Left then what, other else other, what in
730 let newgoal, newproof =
731 let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
732 let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
736 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
737 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
738 S.lift 1 eq_ty; l; r]
743 CicMkImplicit.identity_relocation_list_for_metavariable context in
744 C.Meta (!maxmeta, irl)
749 if pos = Utils.Left then [ty; what; other]
750 else [ty; other; what]
752 Inference.ProofSymBlock (termlist, proof')
755 if pos = Utils.Left then what, other else other, what
757 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
761 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
762 Inference.BasicProof metaproof)
765 | Inference.BasicProof _ ->
766 (* debug_print (lazy "replacing a BasicProof"); *)
768 | Inference.ProofGoalBlock (_, parent_proof) ->
769 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
770 Inference.ProofGoalBlock (pb, parent_proof)
774 C.Appl [C.MutConstruct (* reflexivity *)
775 (LibraryObjects.eq_URI (), 0, 1, []);
776 eq_ty; if ordering = U.Gt then right else left]
779 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
782 if ordering = U.Gt then newgoal, right else left, newgoal in
783 let neworder = !Utils.compare_terms left right in
785 let time2 = Unix.gettimeofday () in
786 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
789 let w = Utils.compute_equality_weight eq_ty left right in
790 (w, newproof, (eq_ty, left, right, neworder), [], [])
794 !maxmeta, List.map build_new expansions
798 let sup_r_counter = ref 1;;
802 returns a list of new clauses inferred with a right superposition step
803 between the positive equation "target" and one in the "table" "newmeta" is
804 the first free meta index, i.e. the first number above the highest meta
805 index: its updated value is also returned
807 let superposition_right newmeta (metasenv, context, ugraph) table target =
808 let module C = Cic in
809 let module S = CicSubstitution in
810 let module M = CicMetaSubst in
811 let module HL = HelmLibraryObjects in
812 let module CR = CicReduction in
813 let module U = Utils in
814 let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
815 let metasenv' = metasenv @ newmetas in
816 let maxmeta = ref newmeta in
819 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
820 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
824 (fun (_, subst, _, _, _) ->
825 let subst = apply_subst subst in
826 let o = !Utils.compare_terms (subst l) (subst r) in
827 o <> U.Lt && o <> U.Le)
828 (fst (betaexpand_term metasenv' context ugraph table 0 l))
830 (res left right), (res right left)
832 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
834 let time1 = Unix.gettimeofday () in
836 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
837 let what, other = if pos = Utils.Left then what, other else other, what in
838 let newgoal, newproof =
840 let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
841 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
845 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
846 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
847 S.lift 1 eq_ty; l; r]
850 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
852 let newmeta, newequality =
854 if ordering = U.Gt then newgoal, apply_subst s right
855 else apply_subst s left, newgoal in
856 let neworder = !Utils.compare_terms left right
857 and newmenv = newmetas @ menv'
858 and newargs = args @ args' in
860 let w = Utils.compute_equality_weight eq_ty left right in
861 (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in
862 let newm, eq' = Inference.fix_metas !maxmeta eq' in
867 let time2 = Unix.gettimeofday () in
868 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
872 let new1 = List.map (build_new U.Gt) res1
873 and new2 = List.map (build_new U.Lt) res2 in
875 let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
877 let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
879 (List.filter ok (new1 @ new2)))
883 (** demodulation, when the target is a goal *)
884 let rec demodulation_goal newmeta env table goal =
885 let module C = Cic in
886 let module S = CicSubstitution in
887 let module M = CicMetaSubst in
888 let module HL = HelmLibraryObjects in
889 let metasenv, context, ugraph = env in
890 let maxmeta = ref newmeta in
891 let proof, metas, term = goal in
892 let term = Utils.guarded_simpl (~debug:true) context term in
893 let goal = proof, metas, term in
894 let metasenv' = metasenv @ metas in
896 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
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
900 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
901 with CicUtil.Meta_not_found _ -> ty
903 let newterm, newproof =
905 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
906 let bo' = apply_subst subst t in
907 let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
912 CicMkImplicit.identity_relocation_list_for_metavariable context in
913 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
914 C.Meta (!maxmeta, irl)
919 if pos = Utils.Left then [ty; what; other]
920 else [ty; other; what]
922 Inference.ProofSymBlock (termlist, proof')
925 if pos = Utils.Left then what, other else other, what
927 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
931 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
932 eq_found, Inference.BasicProof metaproof)
934 let rec repl = function
935 | Inference.NoProof ->
936 (* debug_print (lazy "replacing a NoProof"); *)
938 | Inference.BasicProof _ ->
939 (* debug_print (lazy "replacing a BasicProof"); *)
941 | Inference.ProofGoalBlock (_, parent_proof) ->
942 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
943 Inference.ProofGoalBlock (pb, parent_proof)
944 | Inference.SubProof (term, meta_index, p) ->
945 Inference.SubProof (term, meta_index, repl p)
949 bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
951 let m = Inference.metas_of_term newterm in
952 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv')in
953 !maxmeta, (newproof, newmetasenv, newterm)
956 demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
960 let newmeta, newgoal = build_newgoal t in
961 let _, _, newg = newgoal in
962 if Inference.meta_convertibility term newg then
965 demodulation_goal newmeta env table newgoal
971 (** demodulation, when the target is a theorem *)
972 let rec demodulation_theorem newmeta env table theorem =
973 let module C = Cic in
974 let module S = CicSubstitution in
975 let module M = CicMetaSubst in
976 let module HL = HelmLibraryObjects in
977 let metasenv, context, ugraph = env in
978 let maxmeta = ref newmeta in
979 let term, termty, metas = theorem in
980 let metasenv' = metasenv @ metas in
982 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
983 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
984 let what, other = if pos = Utils.Left then what, other else other, what in
987 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
988 let bo' = apply_subst subst t in
989 let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
992 Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
993 Inference.BasicProof term)
995 (Inference.build_proof_term newproof, bo)
998 let m = Inference.metas_of_term newterm in
999 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') in
1000 !maxmeta, (newterm, newty, newmetasenv)
1003 demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty
1007 let newmeta, newthm = build_newtheorem t in
1008 let newt, newty, _ = newthm in
1009 if Inference.meta_convertibility termty newty then
1012 demodulation_theorem newmeta env table newthm