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 let check = match termty with C.Implicit None -> false | _ -> true in
137 let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
138 if check && not (fst (CicReduction.are_convertible
139 ~metasenv context termty ty ugraph)) then (
140 find_matches metasenv context ugraph lift_amount term termty tl
142 let do_match c eq_URI =
143 let subst', metasenv', ugraph' =
144 let t1 = Unix.gettimeofday () in
147 Inference.matching (metasenv @ metas) context
148 term (S.lift lift_amount c) ugraph
150 let t2 = Unix.gettimeofday () in
151 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
153 with Inference.MatchingFailure as e ->
154 let t2 = Unix.gettimeofday () in
155 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
158 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
161 let c, other, eq_URI =
162 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
163 else right, left, Utils.eq_ind_r_URI ()
165 if o <> U.Incomparable then
168 with Inference.MatchingFailure ->
169 find_matches metasenv context ugraph lift_amount term termty tl
172 try do_match c eq_URI
173 with Inference.MatchingFailure -> None
176 | Some (_, s, _, _, _) ->
177 let c' = apply_subst s c in
179 let other' = U.guarded_simpl context (apply_subst s other) in *)
180 let other' = apply_subst s other in
181 let order = cmp c' other' in
186 metasenv context ugraph lift_amount term termty tl
188 find_matches metasenv context ugraph lift_amount term termty tl
193 as above, but finds all the matching equalities, and the matching condition
194 can be either Inference.matching or Inference.unification
196 let rec find_all_matches ?(unif_fun=Inference.unification)
197 metasenv context ugraph lift_amount term termty =
198 let module C = Cic in
199 let module U = Utils in
200 let module S = CicSubstitution in
201 let module M = CicMetaSubst in
202 let module HL = HelmLibraryObjects in
203 let cmp = !Utils.compare_terms in
207 let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
208 let do_match c eq_URI =
209 let subst', metasenv', ugraph' =
210 let t1 = Unix.gettimeofday () in
213 unif_fun (metasenv @ metas) context
214 term (S.lift lift_amount c) ugraph in
215 let t2 = Unix.gettimeofday () in
216 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
219 | Inference.MatchingFailure
220 | CicUnification.UnificationFailure _
221 | CicUnification.Uncertain _ as e ->
222 let t2 = Unix.gettimeofday () in
223 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
226 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
229 let c, other, eq_URI =
230 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
231 else right, left, Utils.eq_ind_r_URI ()
233 if o <> U.Incomparable then
235 let res = do_match c eq_URI in
236 res::(find_all_matches ~unif_fun metasenv context ugraph
237 lift_amount term termty tl)
239 | Inference.MatchingFailure
240 | CicUnification.UnificationFailure _
241 | CicUnification.Uncertain _ ->
242 find_all_matches ~unif_fun metasenv context ugraph
243 lift_amount term termty tl
246 let res = do_match c eq_URI in
249 let c' = apply_subst s c
250 and other' = apply_subst s other in
251 let order = cmp c' other' in
252 if order <> U.Lt && order <> U.Le then
253 res::(find_all_matches ~unif_fun metasenv context ugraph
254 lift_amount term termty tl)
256 find_all_matches ~unif_fun metasenv context ugraph
257 lift_amount term termty tl
259 | Inference.MatchingFailure
260 | CicUnification.UnificationFailure _
261 | CicUnification.Uncertain _ ->
262 find_all_matches ~unif_fun metasenv context ugraph
263 lift_amount term termty tl
268 returns true if target is subsumed by some equality in table
270 let subsumption env table target =
271 let _, _, (ty, left, right, _), tmetas, _ = target in
272 let metasenv, context, ugraph = env in
273 let metasenv = metasenv @ tmetas in
274 let samesubst subst subst' =
275 let tbl = Hashtbl.create (List.length subst) in
276 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
278 (fun (m, (c, t1, t2)) ->
280 let c', t1', t2' = Hashtbl.find tbl m in
281 if (c = c') && (t1 = t1') && (t2 = t2') then true
291 let leftc = get_candidates Matching table left in
292 find_all_matches ~unif_fun:Inference.matching
293 metasenv context ugraph 0 left ty leftc
295 let rec ok what = function
297 | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
299 let other = if pos = Utils.Left then r else l in
300 let subst', menv', ug' =
301 let t1 = Unix.gettimeofday () in
304 Inference.matching (metasenv @ menv @ m) context what other ugraph
306 let t2 = Unix.gettimeofday () in
307 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
309 with Inference.MatchingFailure as e ->
310 let t2 = Unix.gettimeofday () in
311 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
314 if samesubst subst subst' then
318 with Inference.MatchingFailure ->
321 let r, subst = ok right leftr in
330 let rightc = get_candidates Matching table right in
331 find_all_matches ~unif_fun:Inference.matching
332 metasenv context ugraph 0 right ty rightc
339 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
340 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
345 let rec demodulation_aux ?(typecheck=false)
346 metasenv context ugraph table lift_amount term =
347 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
349 let module C = Cic in
350 let module S = CicSubstitution in
351 let module M = CicMetaSubst in
352 let module HL = HelmLibraryObjects in
353 let candidates = get_candidates Matching table term in
359 CicTypeChecker.type_of_aux' metasenv context term ugraph
361 C.Implicit None, ugraph
364 find_matches metasenv context ugraph lift_amount term termty candidates
375 (res, tl @ [S.lift 1 t])
378 demodulation_aux metasenv context ugraph table
382 | None -> (None, tl @ [S.lift 1 t])
383 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
388 | Some (_, subst, menv, ug, eq_found) ->
389 Some (C.Appl ll, subst, menv, ug, eq_found)
391 | C.Prod (nn, s, t) ->
393 demodulation_aux metasenv context ugraph table lift_amount s in (
397 demodulation_aux metasenv
398 ((Some (nn, C.Decl s))::context) ugraph
399 table (lift_amount+1) t
403 | Some (t', subst, menv, ug, eq_found) ->
404 Some (C.Prod (nn, (S.lift 1 s), t'),
405 subst, menv, ug, eq_found)
407 | Some (s', subst, menv, ug, eq_found) ->
408 Some (C.Prod (nn, s', (S.lift 1 t)),
409 subst, menv, ug, eq_found)
411 | C.Lambda (nn, s, t) ->
413 demodulation_aux metasenv context ugraph table lift_amount s in (
417 demodulation_aux metasenv
418 ((Some (nn, C.Decl s))::context) ugraph
419 table (lift_amount+1) t
423 | Some (t', subst, menv, ug, eq_found) ->
424 Some (C.Lambda (nn, (S.lift 1 s), t'),
425 subst, menv, ug, eq_found)
427 | Some (s', subst, menv, ug, eq_found) ->
428 Some (C.Lambda (nn, s', (S.lift 1 t)),
429 subst, menv, ug, eq_found)
436 let build_newtarget_time = ref 0.;;
439 let demod_counter = ref 1;;
441 (** demodulation, when target is an equality *)
442 let rec demodulation_equality newmeta env table sign target =
443 let module C = Cic in
444 let module S = CicSubstitution in
445 let module M = CicMetaSubst in
446 let module HL = HelmLibraryObjects in
447 let module U = Utils in
448 let metasenv, context, ugraph = env in
449 let _, proof, (eq_ty, left, right, order), metas, args = target in
450 let metasenv' = metasenv @ metas in
452 let maxmeta = ref newmeta in
454 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
455 let time1 = Unix.gettimeofday () in
457 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
459 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
460 with CicUtil.Meta_not_found _ -> ty
462 let what, other = if pos = Utils.Left then what, other else other, what in
463 let newterm, newproof =
464 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
465 let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
468 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
469 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
470 S.lift 1 eq_ty; l; r]
472 if sign = Utils.Positive then
474 Inference.ProofBlock (
475 subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
480 CicMkImplicit.identity_relocation_list_for_metavariable context in
481 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
482 (* print_newline (); *)
483 C.Meta (!maxmeta, irl)
488 if pos = Utils.Left then [ty; what; other]
489 else [ty; other; what]
491 Inference.ProofSymBlock (termlist, proof')
494 if pos = Utils.Left then what, other else other, what
496 pos, (0, proof', (ty, other, what, Utils.Incomparable),
501 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
502 eq_found, Inference.BasicProof metaproof)
505 | Inference.BasicProof _ ->
506 print_endline "replacing a BasicProof";
508 | Inference.ProofGoalBlock (_, parent_proof) ->
509 print_endline "replacing another ProofGoalBlock";
510 Inference.ProofGoalBlock (pb, parent_proof)
514 C.Appl [C.MutConstruct (* reflexivity *)
515 (LibraryObjects.eq_URI (), 0, 1, []);
516 eq_ty; if is_left then right else left]
519 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
521 let left, right = if is_left then newterm, right else left, newterm in
522 let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
523 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv')
526 let ordering = !Utils.compare_terms left right in
528 let time2 = Unix.gettimeofday () in
529 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
532 let w = Utils.compute_equality_weight eq_ty left right in
533 (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
537 let res = demodulation_aux metasenv' context ugraph table 0 left in
538 let newmeta, newtarget =
541 let newmeta, newtarget = build_newtarget true t in
542 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
543 (Inference.meta_convertibility_eq target newtarget) then
546 demodulation_equality newmeta env table sign newtarget
548 let res = demodulation_aux metasenv' context ugraph table 0 right in
551 let newmeta, newtarget = build_newtarget false t in
552 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
553 (Inference.meta_convertibility_eq target newtarget) then
556 demodulation_equality newmeta env table sign newtarget
560 (* newmeta, newtarget *)
561 (* tentiamo di normalizzare *)
562 let w, p, (ty, left, right, o), m, a = newtarget in
563 let left = U.guarded_simpl context left in
564 let right = U.guarded_simpl context right in
565 let w' = Utils.compute_equality_weight ty left right in
566 let o' = !Utils.compare_terms left right in
567 newmeta, (w', p, (ty, left, right, o'), m, a)
572 Performs the beta expansion of the term "term" w.r.t. "table",
573 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
576 let rec betaexpand_term metasenv context ugraph table lift_amount term =
577 let module C = Cic in
578 let module S = CicSubstitution in
579 let module M = CicMetaSubst in
580 let module HL = HelmLibraryObjects in
581 let candidates = get_candidates Unification table term in
582 let res, lifted_term =
587 (fun arg (res, lifted_tl) ->
590 let arg_res, lifted_arg =
591 betaexpand_term metasenv context ugraph table
595 (fun (t, s, m, ug, eq_found) ->
596 (Some t)::lifted_tl, s, m, ug, eq_found)
601 (fun (l, s, m, ug, eq_found) ->
602 (Some lifted_arg)::l, s, m, ug, eq_found)
604 (Some lifted_arg)::lifted_tl)
607 (fun (r, s, m, ug, eq_found) ->
608 None::r, s, m, ug, eq_found) res,
614 (fun (l, s, m, ug, eq_found) ->
615 (C.Meta (i, l), s, m, ug, eq_found)) l'
617 e, C.Meta (i, lifted_l)
620 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
622 | C.Prod (nn, s, t) ->
624 betaexpand_term metasenv context ugraph table lift_amount s in
626 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
627 table (lift_amount+1) t in
630 (fun (t, s, m, ug, eq_found) ->
631 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
634 (fun (t, s, m, ug, eq_found) ->
635 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
636 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
638 | C.Lambda (nn, s, t) ->
640 betaexpand_term metasenv context ugraph table lift_amount s in
642 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
643 table (lift_amount+1) t in
646 (fun (t, s, m, ug, eq_found) ->
647 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
650 (fun (t, s, m, ug, eq_found) ->
651 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
652 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
657 (fun arg (res, lifted_tl) ->
658 let arg_res, lifted_arg =
659 betaexpand_term metasenv context ugraph table lift_amount arg
663 (fun (a, s, m, ug, eq_found) ->
664 a::lifted_tl, s, m, ug, eq_found)
669 (fun (r, s, m, ug, eq_found) ->
670 lifted_arg::r, s, m, ug, eq_found)
672 lifted_arg::lifted_tl)
676 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
679 | t -> [], (S.lift lift_amount t)
682 | C.Meta (i, l) -> res, lifted_term
685 C.Implicit None, ugraph
686 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
690 metasenv context ugraph lift_amount term termty candidates
696 let sup_l_counter = ref 1;;
700 returns a list of new clauses inferred with a left superposition step
701 the negative equation "target" and one of the positive equations in "table"
703 let superposition_left newmeta (metasenv, context, ugraph) table target =
704 let module C = Cic in
705 let module S = CicSubstitution in
706 let module M = CicMetaSubst in
707 let module HL = HelmLibraryObjects in
708 let module CR = CicReduction in
709 let module U = Utils in
710 let weight, proof, (eq_ty, left, right, ordering), _, _ = target in
712 let term = if ordering = U.Gt then left else right in
713 betaexpand_term metasenv context ugraph table 0 term
715 let maxmeta = ref newmeta in
716 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
718 (* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
720 let time1 = Unix.gettimeofday () in
722 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
723 let what, other = if pos = Utils.Left then what, other else other, what in
724 let newgoal, newproof =
725 let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
726 let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
730 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
731 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
732 S.lift 1 eq_ty; l; r]
737 CicMkImplicit.identity_relocation_list_for_metavariable context in
738 C.Meta (!maxmeta, irl)
743 if pos = Utils.Left then [ty; what; other]
744 else [ty; other; what]
746 Inference.ProofSymBlock (termlist, proof')
749 if pos = Utils.Left then what, other else other, what
751 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
755 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
756 Inference.BasicProof metaproof)
759 | Inference.BasicProof _ ->
760 (* debug_print (lazy "replacing a BasicProof"); *)
762 | Inference.ProofGoalBlock (_, parent_proof) ->
763 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
764 Inference.ProofGoalBlock (pb, parent_proof)
768 C.Appl [C.MutConstruct (* reflexivity *)
769 (LibraryObjects.eq_URI (), 0, 1, []);
770 eq_ty; if ordering = U.Gt then right else left]
773 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
776 if ordering = U.Gt then newgoal, right else left, newgoal in
777 let neworder = !Utils.compare_terms left right in
779 let time2 = Unix.gettimeofday () in
780 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
783 let w = Utils.compute_equality_weight eq_ty left right in
784 (w, newproof, (eq_ty, left, right, neworder), [], [])
788 !maxmeta, List.map build_new expansions
792 let sup_r_counter = ref 1;;
796 returns a list of new clauses inferred with a right superposition step
797 between the positive equation "target" and one in the "table" "newmeta" is
798 the first free meta index, i.e. the first number above the highest meta
799 index: its updated value is also returned
801 let superposition_right newmeta (metasenv, context, ugraph) table target =
802 let module C = Cic in
803 let module S = CicSubstitution in
804 let module M = CicMetaSubst in
805 let module HL = HelmLibraryObjects in
806 let module CR = CicReduction in
807 let module U = Utils in
808 let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
809 let metasenv' = metasenv @ newmetas in
810 let maxmeta = ref newmeta in
813 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
814 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
818 (fun (_, subst, _, _, _) ->
819 let subst = apply_subst subst in
820 let o = !Utils.compare_terms (subst l) (subst r) in
821 o <> U.Lt && o <> U.Le)
822 (fst (betaexpand_term metasenv' context ugraph table 0 l))
824 (res left right), (res right left)
826 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
828 let time1 = Unix.gettimeofday () in
830 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
831 let what, other = if pos = Utils.Left then what, other else other, what in
832 let newgoal, newproof =
834 let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
835 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
839 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
840 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
841 S.lift 1 eq_ty; l; r]
844 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
846 let newmeta, newequality =
848 if ordering = U.Gt then newgoal, apply_subst s right
849 else apply_subst s left, newgoal in
850 let neworder = !Utils.compare_terms left right
851 and newmenv = newmetas @ menv'
852 and newargs = args @ args' in
854 let w = Utils.compute_equality_weight eq_ty left right in
855 (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in
856 let newm, eq' = Inference.fix_metas !maxmeta eq' in
861 let time2 = Unix.gettimeofday () in
862 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
866 let new1 = List.map (build_new U.Gt) res1
867 and new2 = List.map (build_new U.Lt) res2 in
868 let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
870 (List.filter ok (new1 @ new2)))
874 (** demodulation, when the target is a goal *)
875 let rec demodulation_goal newmeta env table goal =
876 let module C = Cic in
877 let module S = CicSubstitution in
878 let module M = CicMetaSubst in
879 let module HL = HelmLibraryObjects in
880 let metasenv, context, ugraph = env in
881 let maxmeta = ref newmeta in
882 let proof, metas, term = goal in
883 let metasenv' = metasenv @ metas in
884 Printf.eprintf "siam qua\n";
886 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
887 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
888 let what, other = if pos = Utils.Left then what, other else other, what in
890 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
891 with CicUtil.Meta_not_found _ -> ty
893 let newterm, newproof =
895 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
896 let bo' = apply_subst subst t in
897 let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
902 CicMkImplicit.identity_relocation_list_for_metavariable context in
903 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
904 C.Meta (!maxmeta, irl)
909 if pos = Utils.Left then [ty; what; other]
910 else [ty; other; what]
912 Inference.ProofSymBlock (termlist, proof')
915 if pos = Utils.Left then what, other else other, what
917 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
921 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
922 eq_found, Inference.BasicProof metaproof)
924 let rec repl = function
925 | Inference.NoProof ->
926 (* debug_print (lazy "replacing a NoProof"); *)
928 | Inference.BasicProof _ ->
929 (* debug_print (lazy "replacing a BasicProof"); *)
931 | Inference.ProofGoalBlock (_, parent_proof) ->
932 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
933 Inference.ProofGoalBlock (pb, parent_proof)
934 | Inference.SubProof (term, meta_index, p) ->
935 Inference.SubProof (term, meta_index, repl p)
939 bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
941 let m = Inference.metas_of_term newterm in
942 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
943 !maxmeta, (newproof, newmetasenv, newterm)
945 Printf.eprintf "bum0\n";
947 demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
949 Printf.eprintf "bum\n";
952 let newmeta, newgoal = build_newgoal t in
953 let _, _, newg = newgoal in
954 if Inference.meta_convertibility term newg then
958 Printf.eprintf "reducing %s to %s \n"
959 (CicPp.ppterm term) (CicPp.ppterm newg);
960 demodulation_goal newmeta env table newgoal
967 (** demodulation, when the target is a theorem *)
968 let rec demodulation_theorem newmeta env table theorem =
969 let module C = Cic in
970 let module S = CicSubstitution in
971 let module M = CicMetaSubst in
972 let module HL = HelmLibraryObjects in
973 let metasenv, context, ugraph = env in
974 let maxmeta = ref newmeta in
975 let term, termty, metas = theorem in
976 let metasenv' = metasenv @ metas in
978 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
979 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
980 let what, other = if pos = Utils.Left then what, other else other, what in
983 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
984 let bo' = apply_subst subst t in
985 let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
988 Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
989 Inference.BasicProof term)
991 (Inference.build_proof_term newproof, bo)
994 let m = Inference.metas_of_term newterm in
995 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
996 !maxmeta, (newterm, newty, newmetasenv)
999 demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty
1003 let newmeta, newthm = build_newtheorem t in
1004 let newt, newty, _ = newthm in
1005 if Inference.meta_convertibility termty newty then
1008 demodulation_theorem newmeta env table newthm
1013 let demodulate_tac ~dbd ~pattern (proof,goal) =
1014 let module I = Inference in
1015 let curi,metasenv,pbo,pty = proof in
1016 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1017 let eq_indexes, equalities, maxm = I.find_equalities context proof in
1018 let lib_eq_uris, library_equalities, maxm =
1019 I.find_library_equalities dbd context (proof, goal) (maxm+2) in
1020 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1021 let library_equalities = List.map snd library_equalities in
1022 let goalterm = Cic.Meta (metano,irl) in
1023 let initgoal = Inference.BasicProof goalterm, [], ty in
1024 let equalities = equalities @ library_equalities in
1027 (fun tbl eq -> index tbl eq)
1030 let newmeta,(newproof,newmetasenv, newty) = demodulation_goal
1031 maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal
1033 if newmeta != maxm then
1035 let opengoal = Cic.Meta(maxm,irl) in
1037 Inference.build_proof_term ~noproof:opengoal newproof in
1038 prerr_endline ("proffterm ="^(CicMetaSubst.ppterm_in_context [] proofterm context));
1039 let extended_metasenv = (maxm,context,newty)::metasenv in
1040 prerr_endline ("metasenv ="^(CicMetaSubst.ppmetasenv [] extended_metasenv));
1041 let extended_status =
1042 (curi,extended_metasenv,pbo,pty),goal in
1043 let (status,newgoals) =
1044 ProofEngineTypes.apply_tactic
1045 (PrimitiveTactics.apply_tac ~term:proofterm)
1047 (status,maxm::newgoals)
1049 else raise (ProofEngineTypes.Fail (lazy "no progress"))
1051 let demodulate_tac ~dbd ~pattern =
1052 ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)