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 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
28 module Index = Equality_indexing.DT (* path tree based indexing *)
31 let debug_print = Utils.debug_print;;
34 type retrieval_mode = Matching | Unification;;
36 let print_candidates mode term res =
40 Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
42 Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
48 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
49 (Inference.string_of_equality e))
55 let indexing_retrieval_time = ref 0.;;
58 let apply_subst = CicMetaSubst.apply_subst
60 let index = Index.index
61 let remove_index = Index.remove_index
62 let in_index = Index.in_index
63 let empty = Index.empty
64 let init_index = Index.init_index
66 (* returns a list of all the equalities in the tree that are in relation
67 "mode" with the given term, where mode can be either Matching or
70 Format of the return value: list of tuples in the form:
71 (position - Left or Right - of the term that matched the given one in this
75 Note that if equality is "left = right", if the ordering is left > right,
76 the position will always be Left, and if the ordering is left < right,
77 position will be Right.
79 let get_candidates mode tree term =
80 let t1 = Unix.gettimeofday () in
84 | Matching -> Index.retrieve_generalizations tree term
85 | Unification -> Index.retrieve_unifiables tree term
87 Index.PosEqSet.elements s
89 (* print_candidates mode term res; *)
90 (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
91 (* print_newline (); *)
92 let t2 = Unix.gettimeofday () in
93 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
98 let match_unif_time_ok = ref 0.;;
99 let match_unif_time_no = ref 0.;;
103 finds the first equality in the index that matches "term", of type "termty"
104 termty can be Implicit if it is not needed. The result (one of the sides of
105 the equality, actually) should be not greater (wrt the term ordering) than
108 Format of the return value:
110 (term to substitute, [Cic.Rel 1 properly lifted - see the various
111 build_newtarget functions inside the various
112 demodulation_* functions]
113 substitution used for the matching,
115 ugraph, [substitution, metasenv and ugraph have the same meaning as those
116 returned by CicUnification.fo_unif]
117 (equality where the matching term was found, [i.e. the equality to use as
119 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
120 the equality: this is used to build the proof term, again see one of
121 the build_newtarget functions]
124 let rec find_matches metasenv context ugraph lift_amount term termty =
125 let module C = Cic in
126 let module U = Utils in
127 let module S = CicSubstitution in
128 let module M = CicMetaSubst in
129 let module HL = HelmLibraryObjects in
130 let cmp = !Utils.compare_terms in
131 let check = match termty with C.Implicit None -> false | _ -> true in
135 let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
136 if check && not (fst (CicReduction.are_convertible
137 ~metasenv context termty ty ugraph)) then (
138 find_matches metasenv context ugraph lift_amount term termty tl
140 let do_match c eq_URI =
141 let subst', metasenv', ugraph' =
142 let t1 = Unix.gettimeofday () in
145 Inference.matching (metasenv @ metas) context
146 term (S.lift lift_amount c) ugraph in
147 let t2 = Unix.gettimeofday () in
148 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
150 with Inference.MatchingFailure as e ->
151 let t2 = Unix.gettimeofday () in
152 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
155 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
158 let c, other, eq_URI =
159 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
160 else right, left, Utils.eq_ind_r_URI ()
162 if o <> U.Incomparable then
165 with Inference.MatchingFailure ->
166 find_matches metasenv context ugraph lift_amount term termty tl
169 try do_match c eq_URI
170 with Inference.MatchingFailure -> None
173 | Some (_, s, _, _, _) ->
174 let c' = apply_subst s c in
175 let other' = U.guarded_simpl context (apply_subst s other) in
176 let order = cmp c' other' in
177 let names = U.names_of_context context in
182 metasenv context ugraph lift_amount term termty tl
184 find_matches metasenv context ugraph lift_amount term termty tl
189 as above, but finds all the matching equalities, and the matching condition
190 can be either Inference.matching or Inference.unification
192 let rec find_all_matches ?(unif_fun=Inference.unification)
193 metasenv context ugraph lift_amount term termty =
194 let module C = Cic in
195 let module U = Utils in
196 let module S = CicSubstitution in
197 let module M = CicMetaSubst in
198 let module HL = HelmLibraryObjects in
199 let cmp = !Utils.compare_terms in
203 let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
204 let do_match c eq_URI =
205 let subst', metasenv', ugraph' =
206 let t1 = Unix.gettimeofday () in
209 unif_fun (metasenv @ metas) context
210 term (S.lift lift_amount c) ugraph in
211 let t2 = Unix.gettimeofday () in
212 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
215 | Inference.MatchingFailure
216 | CicUnification.UnificationFailure _
217 | CicUnification.Uncertain _ as e ->
218 let t2 = Unix.gettimeofday () in
219 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
222 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
225 let c, other, eq_URI =
226 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
227 else right, left, Utils.eq_ind_r_URI ()
229 if o <> U.Incomparable then
231 let res = do_match c eq_URI in
232 res::(find_all_matches ~unif_fun metasenv context ugraph
233 lift_amount term termty tl)
235 | Inference.MatchingFailure
236 | CicUnification.UnificationFailure _
237 | CicUnification.Uncertain _ ->
238 find_all_matches ~unif_fun metasenv context ugraph
239 lift_amount term termty tl
242 let res = do_match c eq_URI in
245 let c' = apply_subst s c
246 and other' = apply_subst s other in
247 let order = cmp c' other' in
248 let names = U.names_of_context context in
249 if order <> U.Lt && order <> U.Le then
250 res::(find_all_matches ~unif_fun metasenv context ugraph
251 lift_amount term termty tl)
253 find_all_matches ~unif_fun metasenv context ugraph
254 lift_amount term termty tl
256 | Inference.MatchingFailure
257 | CicUnification.UnificationFailure _
258 | CicUnification.Uncertain _ ->
259 find_all_matches ~unif_fun metasenv context ugraph
260 lift_amount term termty tl
265 returns true if target is subsumed by some equality in table
267 let subsumption env table target =
268 let _, _, (ty, left, right, _), tmetas, _ = target in
269 let metasenv, context, ugraph = env in
270 let metasenv = metasenv @ tmetas in
271 let samesubst subst subst' =
272 let tbl = Hashtbl.create (List.length subst) in
273 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
275 (fun (m, (c, t1, t2)) ->
277 let c', t1', t2' = Hashtbl.find tbl m in
278 if (c = c') && (t1 = t1') && (t2 = t2') then true
288 let leftc = get_candidates Matching table left in
289 find_all_matches ~unif_fun:Inference.matching
290 metasenv context ugraph 0 left ty leftc
292 let rec ok what = function
294 | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
296 let other = if pos = Utils.Left then r else l in
297 let subst', menv', ug' =
298 let t1 = Unix.gettimeofday () in
301 Inference.matching (metasenv @ menv @ m) context what other ugraph
303 let t2 = Unix.gettimeofday () in
304 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
306 with Inference.MatchingFailure as e ->
307 let t2 = Unix.gettimeofday () in
308 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
311 if samesubst subst subst' then
315 with Inference.MatchingFailure ->
318 let r, subst = ok right leftr in
327 let rightc = get_candidates Matching table right in
328 find_all_matches ~unif_fun:Inference.matching
329 metasenv context ugraph 0 right ty rightc
336 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
337 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
342 let rec demodulation_aux ?(typecheck=false)
343 metasenv context ugraph table lift_amount term =
344 let module C = Cic in
345 let module S = CicSubstitution in
346 let module M = CicMetaSubst in
347 let module HL = HelmLibraryObjects in
348 let candidates = get_candidates Matching table term in
354 CicTypeChecker.type_of_aux' metasenv context term ugraph
356 C.Implicit None, ugraph
359 find_matches metasenv context ugraph lift_amount term termty candidates
370 (res, tl @ [S.lift 1 t])
373 demodulation_aux metasenv context ugraph table
377 | None -> (None, tl @ [S.lift 1 t])
378 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
383 | Some (_, subst, menv, ug, eq_found) ->
384 Some (C.Appl ll, subst, menv, ug, eq_found)
386 | C.Prod (nn, s, t) ->
388 demodulation_aux metasenv context ugraph table lift_amount s in (
392 demodulation_aux metasenv
393 ((Some (nn, C.Decl s))::context) ugraph
394 table (lift_amount+1) t
398 | Some (t', subst, menv, ug, eq_found) ->
399 Some (C.Prod (nn, (S.lift 1 s), t'),
400 subst, menv, ug, eq_found)
402 | Some (s', subst, menv, ug, eq_found) ->
403 Some (C.Prod (nn, s', (S.lift 1 t)),
404 subst, menv, ug, eq_found)
406 | C.Lambda (nn, s, t) ->
408 demodulation_aux metasenv context ugraph table lift_amount s in (
412 demodulation_aux metasenv
413 ((Some (nn, C.Decl s))::context) ugraph
414 table (lift_amount+1) t
418 | Some (t', subst, menv, ug, eq_found) ->
419 Some (C.Lambda (nn, (S.lift 1 s), t'),
420 subst, menv, ug, eq_found)
422 | Some (s', subst, menv, ug, eq_found) ->
423 Some (C.Lambda (nn, s', (S.lift 1 t)),
424 subst, menv, ug, eq_found)
431 let build_newtarget_time = ref 0.;;
434 let demod_counter = ref 1;;
436 (** demodulation, when target is an equality *)
437 let rec demodulation_equality newmeta env table sign target =
438 let module C = Cic in
439 let module S = CicSubstitution in
440 let module M = CicMetaSubst in
441 let module HL = HelmLibraryObjects in
442 let module U = Utils in
443 let metasenv, context, ugraph = env in
444 let _, proof, (eq_ty, left, right, order), metas, args = target in
445 let metasenv' = metasenv @ metas in
447 let maxmeta = ref newmeta in
449 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
450 let time1 = Unix.gettimeofday () in
452 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
454 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
455 with CicUtil.Meta_not_found _ -> ty
457 let what, other = if pos = Utils.Left then what, other else other, what in
458 let newterm, newproof =
459 let bo = U.guarded_simpl context (apply_subst subst (S.subst other t)) in
460 let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
463 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
464 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
465 S.lift 1 eq_ty; l; r]
467 if sign = Utils.Positive then
469 Inference.ProofBlock (
470 subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
475 CicMkImplicit.identity_relocation_list_for_metavariable context in
476 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
477 (* print_newline (); *)
478 C.Meta (!maxmeta, irl)
483 if pos = Utils.Left then [ty; what; other]
484 else [ty; other; what]
486 Inference.ProofSymBlock (termlist, proof')
489 if pos = Utils.Left then what, other else other, what
491 pos, (0, proof', (ty, other, what, Utils.Incomparable),
496 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
497 eq_found, Inference.BasicProof metaproof)
500 | Inference.BasicProof _ ->
501 print_endline "replacing a BasicProof";
503 | Inference.ProofGoalBlock (_, parent_proof) ->
504 print_endline "replacing another ProofGoalBlock";
505 Inference.ProofGoalBlock (pb, parent_proof)
509 C.Appl [C.MutConstruct (* reflexivity *)
510 (LibraryObjects.eq_URI (), 0, 1, []);
511 eq_ty; if is_left then right else left]
514 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
516 let left, right = if is_left then newterm, right else left, newterm in
517 let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
518 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
521 let ordering = !Utils.compare_terms left right in
523 let time2 = Unix.gettimeofday () in
524 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
527 let w = Utils.compute_equality_weight eq_ty left right in
528 (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
532 let res = demodulation_aux metasenv' context ugraph table 0 left in
533 let newmeta, newtarget =
536 let newmeta, newtarget = build_newtarget true t in
537 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
538 (Inference.meta_convertibility_eq target newtarget) then
541 demodulation_equality newmeta env table sign newtarget
543 let res = demodulation_aux metasenv' context ugraph table 0 right in
546 let newmeta, newtarget = build_newtarget false t in
547 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
548 (Inference.meta_convertibility_eq target newtarget) then
551 demodulation_equality newmeta env table sign newtarget
555 (* newmeta, newtarget *)
556 (* tentiamo di ridurre usando CicReduction.normalize *)
557 let w, p, (ty, left, right, o), m, a = newtarget in
558 let left' = ProofEngineReduction.simpl context left in
559 let right' = ProofEngineReduction.simpl context right in
561 if !Utils.compare_terms left' left = Utils.Lt then left' else left in
563 if !Utils.compare_terms right' right = Utils.Lt then right' else right in
564 (* if newleft != left || newright != right then ( *)
567 (* (Printf.sprintf "left: %s, left': %s\nright: %s, right': %s\n" *)
568 (* (CicPp.ppterm left) (CicPp.ppterm left') (CicPp.ppterm right) *)
569 (* (CicPp.ppterm right'))) *)
571 let w' = Utils.compute_equality_weight ty newleft newright in
572 let o' = !Utils.compare_terms newleft newright in
573 newmeta, (w', p, (ty, newleft, newright, o'), m, a)
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 =
839 let bo' = apply_subst s (S.subst other bo) in
841 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
844 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
845 (name, ty, S.lift 1 eq_ty, l, r)
847 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
851 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
852 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
853 S.lift 1 eq_ty; l; r]
856 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
858 let newmeta, newequality =
860 if ordering = U.Gt then newgoal, apply_subst s right
861 else apply_subst s left, newgoal in
862 let neworder = !Utils.compare_terms left right
863 and newmenv = newmetas @ menv'
864 and newargs = args @ args' in
866 let w = Utils.compute_equality_weight eq_ty left right in
867 (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
868 and env = (metasenv, context, ugraph) in
869 let newm, eq' = Inference.fix_metas !maxmeta eq' in
874 let time2 = Unix.gettimeofday () in
875 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
879 let new1 = List.map (build_new U.Gt) res1
880 and new2 = List.map (build_new U.Lt) res2 in
881 let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
883 (List.filter ok (new1 @ new2)))
887 (** demodulation, when the target is a goal *)
888 let rec demodulation_goal newmeta env table goal =
889 let module C = Cic in
890 let module S = CicSubstitution in
891 let module M = CicMetaSubst in
892 let module HL = HelmLibraryObjects in
893 let metasenv, context, ugraph = env in
894 let maxmeta = ref newmeta in
895 let proof, metas, term = goal in
896 let metasenv' = metasenv @ metas in
898 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
899 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
900 let what, other = if pos = Utils.Left then what, other else other, what in
902 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
903 with CicUtil.Meta_not_found _ -> ty
905 let newterm, newproof =
906 let bo = apply_subst subst (S.subst other t) in
907 let bo' = apply_subst subst t in
908 let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
913 CicMkImplicit.identity_relocation_list_for_metavariable context in
914 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
915 C.Meta (!maxmeta, irl)
920 if pos = Utils.Left then [ty; what; other]
921 else [ty; other; what]
923 Inference.ProofSymBlock (termlist, proof')
926 if pos = Utils.Left then what, other else other, what
928 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
932 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
933 eq_found, Inference.BasicProof metaproof)
935 let rec repl = function
936 | Inference.NoProof ->
937 (* debug_print (lazy "replacing a NoProof"); *)
939 | Inference.BasicProof _ ->
940 (* debug_print (lazy "replacing a BasicProof"); *)
942 | Inference.ProofGoalBlock (_, parent_proof) ->
943 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
944 Inference.ProofGoalBlock (pb, parent_proof)
945 | (Inference.SubProof (term, meta_index, p) as subproof) ->
948 (* (Printf.sprintf "replacing %s" *)
949 (* (Inference.string_of_proof subproof))); *)
950 Inference.SubProof (term, meta_index, repl p)
954 bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
956 let m = Inference.metas_of_term newterm in
957 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
958 !maxmeta, (newproof, newmetasenv, newterm)
961 demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
965 let newmeta, newgoal = build_newgoal t in
966 let _, _, newg = newgoal in
967 if Inference.meta_convertibility term newg then
970 demodulation_goal newmeta env table newgoal
976 (** demodulation, when the target is a theorem *)
977 let rec demodulation_theorem newmeta env table theorem =
978 let module C = Cic in
979 let module S = CicSubstitution in
980 let module M = CicMetaSubst in
981 let module HL = HelmLibraryObjects in
982 let metasenv, context, ugraph = env in
983 let maxmeta = ref newmeta in
984 let proof, metas, term = theorem in
985 let term, termty, metas = theorem in
986 let metasenv' = metasenv @ metas in
988 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
989 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
990 let what, other = if pos = Utils.Left then what, other else other, what in
992 let bo = apply_subst subst (S.subst other t) in
993 let bo' = apply_subst subst t in
994 let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
997 Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
998 Inference.BasicProof term)
1000 (Inference.build_proof_term newproof, bo)
1002 let m = Inference.metas_of_term newterm in
1003 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
1004 !maxmeta, (newterm, newty, newmetasenv)
1007 demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty
1011 let newmeta, newthm = build_newtheorem t in
1012 let newt, newty, _ = newthm in
1013 if Inference.meta_convertibility termty newty then
1016 demodulation_theorem newmeta env table newthm