1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 let debug_print = Utils.debug_print;;
29 type retrieval_mode = Matching | Unification;;
32 let print_candidates mode term res =
36 Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
38 Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
44 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
45 (Inference.string_of_equality e))
51 let indexing_retrieval_time = ref 0.;;
54 let apply_subst = CicMetaSubst.apply_subst
60 let init_index () = ()
62 let empty_table () = []
64 let index table equality =
65 let _, _, (_, l, r, ordering), _, _ = equality in
67 | Utils.Gt -> (Utils.Left, equality)::table
68 | Utils.Lt -> (Utils.Right, equality)::table
69 | _ -> (Utils.Left, equality)::(Utils.Right, equality)::table
72 let remove_index table equality =
73 List.filter (fun (p, e) -> e != equality) table
76 let in_index table equality =
77 List.exists (fun (p, e) -> e == equality) table
80 let get_candidates mode table term = table
86 let init_index () = ()
89 Path_indexing.PSTrie.empty
92 let index = Path_indexing.index
93 and remove_index = Path_indexing.remove_index
94 and in_index = Path_indexing.in_index;;
96 let get_candidates mode trie term =
97 let t1 = Unix.gettimeofday () in
101 | Matching -> Path_indexing.retrieve_generalizations trie term
102 | Unification -> Path_indexing.retrieve_unifiables trie term
103 (* Path_indexing.retrieve_all trie term *)
105 Path_indexing.PosEqSet.elements s
107 (* print_candidates mode term res; *)
108 let t2 = Unix.gettimeofday () in
109 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
115 (* DISCRIMINATION TREES *)
117 Hashtbl.clear Discrimination_tree.arities;
121 Discrimination_tree.DiscriminationTree.empty
124 let index = Discrimination_tree.index
125 and remove_index = Discrimination_tree.remove_index
126 and in_index = Discrimination_tree.in_index;;
128 let get_candidates mode tree term =
129 let t1 = Unix.gettimeofday () in
133 | Matching -> Discrimination_tree.retrieve_generalizations tree term
134 | Unification -> Discrimination_tree.retrieve_unifiables tree term
136 Discrimination_tree.PosEqSet.elements s
138 (* print_candidates mode term res; *)
139 (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
140 (* print_newline (); *)
141 let t2 = Unix.gettimeofday () in
142 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
147 let match_unif_time_ok = ref 0.;;
148 let match_unif_time_no = ref 0.;;
152 finds the first equality in the index that matches "term", of type "termty"
153 termty can be Implicit if it is not needed. The result (one of the sides of
154 the equality, actually) should be not greater (wrt the term ordering) than
157 Format of the return value:
159 (term to substitute, [Cic.Rel 1 properly lifted - see the various
160 build_newtarget functions inside the various
161 demodulation_* functions]
162 substitution used for the matching,
164 ugraph, [substitution, metasenv and ugraph have the same meaning as those
165 returned by CicUnification.fo_unif]
166 (equality where the matching term was found, [i.e. the equality to use as
168 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
169 the equality: this is used to build the proof term, again see one of
170 the build_newtarget functions]
173 let rec find_matches metasenv context ugraph lift_amount term termty =
174 let module C = Cic in
175 let module U = Utils in
176 let module S = CicSubstitution in
177 let module M = CicMetaSubst in
178 let module HL = HelmLibraryObjects in
179 let cmp = !Utils.compare_terms in
180 let check = match termty with C.Implicit None -> false | _ -> true in
184 let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
185 if check && not (fst (CicReduction.are_convertible
186 ~metasenv context termty ty ugraph)) then (
187 find_matches metasenv context ugraph lift_amount term termty tl
189 let do_match c eq_URI =
190 let subst', metasenv', ugraph' =
191 let t1 = Unix.gettimeofday () in
194 Inference.matching (metasenv @ metas) context
195 term (S.lift lift_amount c) ugraph in
196 let t2 = Unix.gettimeofday () in
197 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
199 with Inference.MatchingFailure as e ->
200 let t2 = Unix.gettimeofday () in
201 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
204 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
207 let c, other, eq_URI =
208 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
209 else right, left, Utils.eq_ind_r_URI ()
211 if o <> U.Incomparable then
214 with Inference.MatchingFailure ->
215 find_matches metasenv context ugraph lift_amount term termty tl
218 try do_match c eq_URI
219 with Inference.MatchingFailure -> None
222 | Some (_, s, _, _, _) ->
223 let c' = apply_subst s c
224 and other' = apply_subst s other in
225 let order = cmp c' other' in
226 let names = U.names_of_context context in
231 metasenv context ugraph lift_amount term termty tl
233 find_matches metasenv context ugraph lift_amount term termty tl
238 as above, but finds all the matching equalities, and the matching condition
239 can be either Inference.matching or Inference.unification
241 let rec find_all_matches ?(unif_fun=Inference.unification)
242 metasenv context ugraph lift_amount term termty =
243 let module C = Cic in
244 let module U = Utils in
245 let module S = CicSubstitution in
246 let module M = CicMetaSubst in
247 let module HL = HelmLibraryObjects in
248 let cmp = !Utils.compare_terms in
252 let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
253 let do_match c eq_URI =
254 let subst', metasenv', ugraph' =
255 let t1 = Unix.gettimeofday () in
258 unif_fun (metasenv @ metas) context
259 term (S.lift lift_amount c) ugraph in
260 let t2 = Unix.gettimeofday () in
261 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
264 | Inference.MatchingFailure
265 | CicUnification.UnificationFailure _
266 | CicUnification.Uncertain _ as e ->
267 let t2 = Unix.gettimeofday () in
268 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
271 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
274 let c, other, eq_URI =
275 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
276 else right, left, Utils.eq_ind_r_URI ()
278 if o <> U.Incomparable then
280 let res = do_match c eq_URI in
281 res::(find_all_matches ~unif_fun metasenv context ugraph
282 lift_amount term termty tl)
284 | Inference.MatchingFailure
285 | CicUnification.UnificationFailure _
286 | CicUnification.Uncertain _ ->
287 find_all_matches ~unif_fun metasenv context ugraph
288 lift_amount term termty tl
291 let res = do_match c eq_URI in
294 let c' = apply_subst s c
295 and other' = apply_subst s other in
296 let order = cmp c' other' in
297 let names = U.names_of_context context in
298 if order <> U.Lt && order <> U.Le then
299 res::(find_all_matches ~unif_fun metasenv context ugraph
300 lift_amount term termty tl)
302 find_all_matches ~unif_fun metasenv context ugraph
303 lift_amount term termty tl
305 | Inference.MatchingFailure
306 | CicUnification.UnificationFailure _
307 | CicUnification.Uncertain _ ->
308 find_all_matches ~unif_fun metasenv context ugraph
309 lift_amount term termty tl
314 returns true if target is subsumed by some equality in table
316 let subsumption env table target =
317 let _, _, (ty, left, right, _), tmetas, _ = target in
318 let metasenv, context, ugraph = env in
319 let metasenv = metasenv @ tmetas in
320 let samesubst subst subst' =
321 let tbl = Hashtbl.create (List.length subst) in
322 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
324 (fun (m, (c, t1, t2)) ->
326 let c', t1', t2' = Hashtbl.find tbl m in
327 if (c = c') && (t1 = t1') && (t2 = t2') then true
337 let leftc = get_candidates Matching table left in
338 find_all_matches ~unif_fun:Inference.matching
339 metasenv context ugraph 0 left ty leftc
341 let rec ok what = function
343 | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
345 let other = if pos = Utils.Left then r else l in
346 let subst', menv', ug' =
347 let t1 = Unix.gettimeofday () in
350 Inference.matching (metasenv @ menv @ m) context what other ugraph
352 let t2 = Unix.gettimeofday () in
353 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
355 with Inference.MatchingFailure as e ->
356 let t2 = Unix.gettimeofday () in
357 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
360 if samesubst subst subst' then
364 with Inference.MatchingFailure ->
367 let r, subst = ok right leftr in
376 let rightc = get_candidates Matching table right in
377 find_all_matches ~unif_fun:Inference.matching
378 metasenv context ugraph 0 right ty rightc
385 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
386 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
391 let rec demodulation_aux ?(typecheck=false)
392 metasenv context ugraph table lift_amount term =
393 let module C = Cic in
394 let module S = CicSubstitution in
395 let module M = CicMetaSubst in
396 let module HL = HelmLibraryObjects in
397 let candidates = get_candidates Matching table term in
403 CicTypeChecker.type_of_aux' metasenv context term ugraph
405 C.Implicit None, ugraph
408 find_matches metasenv context ugraph lift_amount term termty candidates
419 (res, tl @ [S.lift 1 t])
422 demodulation_aux metasenv context ugraph table
426 | None -> (None, tl @ [S.lift 1 t])
427 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
432 | Some (_, subst, menv, ug, eq_found) ->
433 Some (C.Appl ll, subst, menv, ug, eq_found)
435 | C.Prod (nn, s, t) ->
437 demodulation_aux metasenv context ugraph table lift_amount s in (
441 demodulation_aux metasenv
442 ((Some (nn, C.Decl s))::context) ugraph
443 table (lift_amount+1) t
447 | Some (t', subst, menv, ug, eq_found) ->
448 Some (C.Prod (nn, (S.lift 1 s), t'),
449 subst, menv, ug, eq_found)
451 | Some (s', subst, menv, ug, eq_found) ->
452 Some (C.Prod (nn, s', (S.lift 1 t)),
453 subst, menv, ug, eq_found)
455 | C.Lambda (nn, s, t) ->
457 demodulation_aux metasenv context ugraph table lift_amount s in (
461 demodulation_aux metasenv
462 ((Some (nn, C.Decl s))::context) ugraph
463 table (lift_amount+1) t
467 | Some (t', subst, menv, ug, eq_found) ->
468 Some (C.Lambda (nn, (S.lift 1 s), t'),
469 subst, menv, ug, eq_found)
471 | Some (s', subst, menv, ug, eq_found) ->
472 Some (C.Lambda (nn, s', (S.lift 1 t)),
473 subst, menv, ug, eq_found)
480 let build_newtarget_time = ref 0.;;
483 let demod_counter = ref 1;;
485 (** demodulation, when target is an equality *)
486 let rec demodulation_equality newmeta env table sign target =
487 let module C = Cic in
488 let module S = CicSubstitution in
489 let module M = CicMetaSubst in
490 let module HL = HelmLibraryObjects in
491 let metasenv, context, ugraph = env in
492 let _, proof, (eq_ty, left, right, order), metas, args = target in
493 let metasenv' = metasenv @ metas in
495 let maxmeta = ref newmeta in
497 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
498 let time1 = Unix.gettimeofday () in
500 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
502 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
503 with CicUtil.Meta_not_found _ -> ty
505 let what, other = if pos = Utils.Left then what, other else other, what in
506 let newterm, newproof =
507 let bo = apply_subst subst (S.subst other t) in
508 let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
511 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
512 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
513 S.lift 1 eq_ty; l; r]
515 if sign = Utils.Positive then
517 Inference.ProofBlock (
518 subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
523 CicMkImplicit.identity_relocation_list_for_metavariable context in
524 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
525 (* print_newline (); *)
526 C.Meta (!maxmeta, irl)
531 if pos = Utils.Left then [ty; what; other]
532 else [ty; other; what]
534 Inference.ProofSymBlock (termlist, proof')
537 if pos = Utils.Left then what, other else other, what
539 pos, (0, proof', (ty, other, what, Utils.Incomparable),
544 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
545 eq_found, Inference.BasicProof metaproof)
548 | Inference.BasicProof _ ->
549 print_endline "replacing a BasicProof";
551 | Inference.ProofGoalBlock (_, parent_proof) ->
552 print_endline "replacing another ProofGoalBlock";
553 Inference.ProofGoalBlock (pb, parent_proof)
557 C.Appl [C.MutConstruct (* reflexivity *)
558 (LibraryObjects.eq_URI (), 0, 1, []);
559 eq_ty; if is_left then right else left]
562 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
564 let left, right = if is_left then newterm, right else left, newterm in
565 let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
566 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
569 let ordering = !Utils.compare_terms left right in
571 let time2 = Unix.gettimeofday () in
572 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
575 let w = Utils.compute_equality_weight eq_ty left right in
576 (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
580 let res = demodulation_aux metasenv' context ugraph table 0 left in
581 let newmeta, newtarget =
584 let newmeta, newtarget = build_newtarget true t in
585 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
586 (Inference.meta_convertibility_eq target newtarget) then
589 demodulation_equality newmeta env table sign newtarget
591 let res = demodulation_aux metasenv' context ugraph table 0 right in
594 let newmeta, newtarget = build_newtarget false t in
595 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
596 (Inference.meta_convertibility_eq target newtarget) then
599 demodulation_equality newmeta env table sign newtarget
603 (* newmeta, newtarget *)
604 (* tentiamo di ridurre usando CicReduction.normalize *)
605 let w, p, (ty, left, right, o), m, a = newtarget in
606 let left' = ProofEngineReduction.simpl context left in
607 let right' = ProofEngineReduction.simpl context right in
609 if !Utils.compare_terms left' left = Utils.Lt then left' else left in
611 if !Utils.compare_terms right' right = Utils.Lt then right' else right in
612 (* if newleft != left || newright != right then ( *)
615 (* (Printf.sprintf "left: %s, left': %s\nright: %s, right': %s\n" *)
616 (* (CicPp.ppterm left) (CicPp.ppterm left') (CicPp.ppterm right) *)
617 (* (CicPp.ppterm right'))) *)
619 let w' = Utils.compute_equality_weight ty newleft newright in
620 let o' = !Utils.compare_terms newleft newright in
621 newmeta, (w', p, (ty, newleft, newright, o'), m, a)
626 Performs the beta expansion of the term "term" w.r.t. "table",
627 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
630 let rec betaexpand_term metasenv context ugraph table lift_amount term =
631 let module C = Cic in
632 let module S = CicSubstitution in
633 let module M = CicMetaSubst in
634 let module HL = HelmLibraryObjects in
635 let candidates = get_candidates Unification table term in
636 let res, lifted_term =
641 (fun arg (res, lifted_tl) ->
644 let arg_res, lifted_arg =
645 betaexpand_term metasenv context ugraph table
649 (fun (t, s, m, ug, eq_found) ->
650 (Some t)::lifted_tl, s, m, ug, eq_found)
655 (fun (l, s, m, ug, eq_found) ->
656 (Some lifted_arg)::l, s, m, ug, eq_found)
658 (Some lifted_arg)::lifted_tl)
661 (fun (r, s, m, ug, eq_found) ->
662 None::r, s, m, ug, eq_found) res,
668 (fun (l, s, m, ug, eq_found) ->
669 (C.Meta (i, l), s, m, ug, eq_found)) l'
671 e, C.Meta (i, lifted_l)
674 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
676 | C.Prod (nn, s, t) ->
678 betaexpand_term metasenv context ugraph table lift_amount s in
680 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
681 table (lift_amount+1) t in
684 (fun (t, s, m, ug, eq_found) ->
685 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
688 (fun (t, s, m, ug, eq_found) ->
689 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
690 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
692 | C.Lambda (nn, s, t) ->
694 betaexpand_term metasenv context ugraph table lift_amount s in
696 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
697 table (lift_amount+1) t in
700 (fun (t, s, m, ug, eq_found) ->
701 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
704 (fun (t, s, m, ug, eq_found) ->
705 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
706 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
711 (fun arg (res, lifted_tl) ->
712 let arg_res, lifted_arg =
713 betaexpand_term metasenv context ugraph table lift_amount arg
717 (fun (a, s, m, ug, eq_found) ->
718 a::lifted_tl, s, m, ug, eq_found)
723 (fun (r, s, m, ug, eq_found) ->
724 lifted_arg::r, s, m, ug, eq_found)
726 lifted_arg::lifted_tl)
730 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
733 | t -> [], (S.lift lift_amount t)
736 | C.Meta (i, l) -> res, lifted_term
739 C.Implicit None, ugraph
740 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
744 metasenv context ugraph lift_amount term termty candidates
750 let sup_l_counter = ref 1;;
754 returns a list of new clauses inferred with a left superposition step
755 the negative equation "target" and one of the positive equations in "table"
757 let superposition_left newmeta (metasenv, context, ugraph) table target =
758 let module C = Cic in
759 let module S = CicSubstitution in
760 let module M = CicMetaSubst in
761 let module HL = HelmLibraryObjects in
762 let module CR = CicReduction in
763 let module U = Utils in
764 let weight, proof, (eq_ty, left, right, ordering), _, _ = target in
766 let term = if ordering = U.Gt then left else right in
767 betaexpand_term metasenv context ugraph table 0 term
769 let maxmeta = ref newmeta in
770 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
772 (* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
774 let time1 = Unix.gettimeofday () in
776 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
777 let what, other = if pos = Utils.Left then what, other else other, what in
778 let newgoal, newproof =
779 let bo' = apply_subst s (S.subst other bo) in
780 let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
784 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
785 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
786 S.lift 1 eq_ty; l; r]
791 CicMkImplicit.identity_relocation_list_for_metavariable context in
792 C.Meta (!maxmeta, irl)
797 if pos = Utils.Left then [ty; what; other]
798 else [ty; other; what]
800 Inference.ProofSymBlock (termlist, proof')
803 if pos = Utils.Left then what, other else other, what
805 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
809 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
810 Inference.BasicProof metaproof)
813 | Inference.BasicProof _ ->
814 (* debug_print (lazy "replacing a BasicProof"); *)
816 | Inference.ProofGoalBlock (_, parent_proof) ->
817 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
818 Inference.ProofGoalBlock (pb, parent_proof)
822 C.Appl [C.MutConstruct (* reflexivity *)
823 (LibraryObjects.eq_URI (), 0, 1, []);
824 eq_ty; if ordering = U.Gt then right else left]
827 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
830 if ordering = U.Gt then newgoal, right else left, newgoal in
831 let neworder = !Utils.compare_terms left right in
833 let time2 = Unix.gettimeofday () in
834 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
837 let w = Utils.compute_equality_weight eq_ty left right in
838 (w, newproof, (eq_ty, left, right, neworder), [], [])
842 !maxmeta, List.map build_new expansions
846 let sup_r_counter = ref 1;;
850 returns a list of new clauses inferred with a right superposition step
851 between the positive equation "target" and one in the "table" "newmeta" is
852 the first free meta index, i.e. the first number above the highest meta
853 index: its updated value is also returned
855 let superposition_right newmeta (metasenv, context, ugraph) table target =
856 let module C = Cic in
857 let module S = CicSubstitution in
858 let module M = CicMetaSubst in
859 let module HL = HelmLibraryObjects in
860 let module CR = CicReduction in
861 let module U = Utils in
862 let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
863 let metasenv' = metasenv @ newmetas in
864 let maxmeta = ref newmeta in
867 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
868 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
872 (fun (_, subst, _, _, _) ->
873 let subst = apply_subst subst in
874 let o = !Utils.compare_terms (subst l) (subst r) in
875 o <> U.Lt && o <> U.Le)
876 (fst (betaexpand_term metasenv' context ugraph table 0 l))
878 (res left right), (res right left)
880 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
882 let time1 = Unix.gettimeofday () in
884 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
885 let what, other = if pos = Utils.Left then what, other else other, what in
886 let newgoal, newproof =
887 let bo' = apply_subst s (S.subst other bo) in
889 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
892 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
893 (name, ty, S.lift 1 eq_ty, l, r)
895 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
899 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
900 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
901 S.lift 1 eq_ty; l; r]
904 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
906 let newmeta, newequality =
908 if ordering = U.Gt then newgoal, apply_subst s right
909 else apply_subst s left, newgoal in
910 let neworder = !Utils.compare_terms left right
911 and newmenv = newmetas @ menv'
912 and newargs = args @ args' in
914 let w = Utils.compute_equality_weight eq_ty left right in
915 (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
916 and env = (metasenv, context, ugraph) in
917 let newm, eq' = Inference.fix_metas !maxmeta eq' in
922 let time2 = Unix.gettimeofday () in
923 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
927 let new1 = List.map (build_new U.Gt) res1
928 and new2 = List.map (build_new U.Lt) res2 in
929 let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
931 (List.filter ok (new1 @ new2)))
935 (** demodulation, when the target is a goal *)
936 let rec demodulation_goal newmeta env table goal =
937 let module C = Cic in
938 let module S = CicSubstitution in
939 let module M = CicMetaSubst in
940 let module HL = HelmLibraryObjects in
941 let metasenv, context, ugraph = env in
942 let maxmeta = ref newmeta in
943 let proof, metas, term = goal in
944 let metasenv' = metasenv @ metas in
946 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
947 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
948 let what, other = if pos = Utils.Left then what, other else other, what in
950 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
951 with CicUtil.Meta_not_found _ -> ty
953 let newterm, newproof =
954 let bo = apply_subst subst (S.subst other t) in
955 let bo' = apply_subst subst t in
956 let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
961 CicMkImplicit.identity_relocation_list_for_metavariable context in
962 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
963 C.Meta (!maxmeta, irl)
968 if pos = Utils.Left then [ty; what; other]
969 else [ty; other; what]
971 Inference.ProofSymBlock (termlist, proof')
974 if pos = Utils.Left then what, other else other, what
976 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
980 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
981 eq_found, Inference.BasicProof metaproof)
983 let rec repl = function
984 | Inference.NoProof ->
985 (* debug_print (lazy "replacing a NoProof"); *)
987 | Inference.BasicProof _ ->
988 (* debug_print (lazy "replacing a BasicProof"); *)
990 | Inference.ProofGoalBlock (_, parent_proof) ->
991 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
992 Inference.ProofGoalBlock (pb, parent_proof)
993 | (Inference.SubProof (term, meta_index, p) as subproof) ->
996 (* (Printf.sprintf "replacing %s" *)
997 (* (Inference.string_of_proof subproof))); *)
998 Inference.SubProof (term, meta_index, repl p)
1002 bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
1004 let m = Inference.metas_of_term newterm in
1005 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
1006 !maxmeta, (newproof, newmetasenv, newterm)
1009 demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
1013 let newmeta, newgoal = build_newgoal t in
1014 let _, _, newg = newgoal in
1015 if Inference.meta_convertibility term newg then
1018 demodulation_goal newmeta env table newgoal
1024 (** demodulation, when the target is a theorem *)
1025 let rec demodulation_theorem newmeta env table theorem =
1026 let module C = Cic in
1027 let module S = CicSubstitution in
1028 let module M = CicMetaSubst in
1029 let module HL = HelmLibraryObjects in
1030 let metasenv, context, ugraph = env in
1031 let maxmeta = ref newmeta in
1032 let proof, metas, term = theorem in
1033 let term, termty, metas = theorem in
1034 let metasenv' = metasenv @ metas in
1036 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1037 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1038 let what, other = if pos = Utils.Left then what, other else other, what in
1039 let newterm, newty =
1040 let bo = apply_subst subst (S.subst other t) in
1041 let bo' = apply_subst subst t in
1042 let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1045 Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1046 Inference.BasicProof term)
1048 (Inference.build_proof_term newproof, bo)
1050 let m = Inference.metas_of_term newterm in
1051 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
1052 !maxmeta, (newterm, newty, newmetasenv)
1055 demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty
1059 let newmeta, newthm = build_newtheorem t in
1060 let newt, newty, _ = newthm in
1061 if Inference.meta_convertibility termty newty then
1064 demodulation_theorem newmeta env table newthm