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 OrderedPosEquality = struct
27 type t = Utils.pos * Inference.equality
28 let compare = Pervasives.compare
31 module PosEqSet = Set.Make(OrderedPosEquality);;
33 module DT = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet);;
35 let debug_print = Utils.debug_print;;
38 type retrieval_mode = Matching | Unification;;
41 let print_candidates mode term res =
45 Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
47 Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
53 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
54 (Inference.string_of_equality e))
60 let indexing_retrieval_time = ref 0.;;
63 let apply_subst = CicMetaSubst.apply_subst
67 let init_index () = ()
69 let empty_table () = []
71 let index table equality =
72 let _, _, (_, l, r, ordering), _, _ = equality in
74 | Utils.Gt -> (Utils.Left, equality)::table
75 | Utils.Lt -> (Utils.Right, equality)::table
76 | _ -> (Utils.Left, equality)::(Utils.Right, equality)::table
79 let remove_index table equality =
80 List.filter (fun (p, e) -> e != equality) table
83 let in_index table equality =
84 List.exists (fun (p, e) -> e == equality) table
87 let get_candidates mode table term = table
93 let init_index () = ()
96 Path_indexing.PSTrie.empty
99 let index = Path_indexing.index
100 let remove_index tree equality =
101 let _, _, (_, l, r, ordering), _, _ = equality in
103 | Utils.Gt -> DT.remove_index tree l equality
104 | Utils.Lt -> DT.remove_index tree r equality
106 DT.remove_index (DT.remove_index tree r equality) l equality
109 let in_index = Path_indexing.in_index;;
111 let get_candidates mode trie term =
112 let t1 = Unix.gettimeofday () in
116 | Matching -> Path_indexing.retrieve_generalizations trie term
117 | Unification -> Path_indexing.retrieve_unifiables trie term
118 (* Path_indexing.retrieve_all trie term *)
120 Path_indexing.PosEqSet.elements s
122 (* print_candidates mode term res; *)
123 let t2 = Unix.gettimeofday () in
124 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
129 (* DISCRIMINATION TREES *)
131 Hashtbl.clear DT.arities;
138 let remove_index tree equality =
139 let _, _, (_, l, r, ordering), _, _ = equality in
141 | Utils.Gt -> DT.remove_index tree l (Utils.Left, equality)
142 | Utils.Lt -> DT.remove_index tree r (Utils.Right, equality)
144 let tree = DT.remove_index tree r (Utils.Right, equality) in
145 DT.remove_index tree l (Utils.Left, equality)
147 let index tree equality =
148 let _, _, (_, l, r, ordering), _, _ = equality in
150 | Utils.Gt -> DT.index tree l (Utils.Left, equality)
151 | Utils.Lt -> DT.index tree r (Utils.Right, equality)
153 let tree = DT.index tree r (Utils.Right, equality) in
154 DT.index tree l (Utils.Left, equality)
157 let in_index tree equality =
158 let _, _, (_, l, r, ordering), _, _ = equality in
159 let meta_convertibility (pos,equality') =
160 Inference.meta_convertibility_eq equality equality'
162 DT.in_index tree l meta_convertibility || DT.in_index tree r meta_convertibility
165 (* returns a list of all the equalities in the tree that are in relation
166 "mode" with the given term, where mode can be either Matching or
169 Format of the return value: list of tuples in the form:
170 (position - Left or Right - of the term that matched the given one in this
174 Note that if equality is "left = right", if the ordering is left > right,
175 the position will always be Left, and if the ordering is left < right,
176 position will be Right.
178 let get_candidates mode tree term =
179 let t1 = Unix.gettimeofday () in
183 | Matching -> DT.retrieve_generalizations tree term
184 | Unification -> DT.retrieve_unifiables tree term
188 (* print_candidates mode term res; *)
189 (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
190 (* print_newline (); *)
191 let t2 = Unix.gettimeofday () in
192 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
197 let match_unif_time_ok = ref 0.;;
198 let match_unif_time_no = ref 0.;;
202 finds the first equality in the index that matches "term", of type "termty"
203 termty can be Implicit if it is not needed. The result (one of the sides of
204 the equality, actually) should be not greater (wrt the term ordering) than
207 Format of the return value:
209 (term to substitute, [Cic.Rel 1 properly lifted - see the various
210 build_newtarget functions inside the various
211 demodulation_* functions]
212 substitution used for the matching,
214 ugraph, [substitution, metasenv and ugraph have the same meaning as those
215 returned by CicUnification.fo_unif]
216 (equality where the matching term was found, [i.e. the equality to use as
218 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
219 the equality: this is used to build the proof term, again see one of
220 the build_newtarget functions]
223 let rec find_matches metasenv context ugraph lift_amount term termty =
224 let module C = Cic in
225 let module U = Utils in
226 let module S = CicSubstitution in
227 let module M = CicMetaSubst in
228 let module HL = HelmLibraryObjects in
229 let cmp = !Utils.compare_terms in
230 let check = match termty with C.Implicit None -> false | _ -> true in
234 let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
235 if check && not (fst (CicReduction.are_convertible
236 ~metasenv context termty ty ugraph)) then (
237 find_matches metasenv context ugraph lift_amount term termty tl
239 let do_match c eq_URI =
240 let subst', metasenv', ugraph' =
241 let t1 = Unix.gettimeofday () in
244 Inference.matching (metasenv @ metas) context
245 term (S.lift lift_amount c) ugraph in
246 let t2 = Unix.gettimeofday () in
247 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
249 with Inference.MatchingFailure as e ->
250 let t2 = Unix.gettimeofday () in
251 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
254 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
257 let c, other, eq_URI =
258 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
259 else right, left, Utils.eq_ind_r_URI ()
261 if o <> U.Incomparable then
264 with Inference.MatchingFailure ->
265 find_matches metasenv context ugraph lift_amount term termty tl
268 try do_match c eq_URI
269 with Inference.MatchingFailure -> None
272 | Some (_, s, _, _, _) ->
273 let c' = apply_subst s c in
274 let other' = U.guarded_simpl context (apply_subst s other) in
275 let order = cmp c' other' in
276 let names = U.names_of_context context in
281 metasenv context ugraph lift_amount term termty tl
283 find_matches metasenv context ugraph lift_amount term termty tl
288 as above, but finds all the matching equalities, and the matching condition
289 can be either Inference.matching or Inference.unification
291 let rec find_all_matches ?(unif_fun=Inference.unification)
292 metasenv context ugraph lift_amount term termty =
293 let module C = Cic in
294 let module U = Utils in
295 let module S = CicSubstitution in
296 let module M = CicMetaSubst in
297 let module HL = HelmLibraryObjects in
298 let cmp = !Utils.compare_terms in
302 let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
303 let do_match c eq_URI =
304 let subst', metasenv', ugraph' =
305 let t1 = Unix.gettimeofday () in
308 unif_fun (metasenv @ metas) context
309 term (S.lift lift_amount c) ugraph in
310 let t2 = Unix.gettimeofday () in
311 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
314 | Inference.MatchingFailure
315 | CicUnification.UnificationFailure _
316 | CicUnification.Uncertain _ as e ->
317 let t2 = Unix.gettimeofday () in
318 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
321 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
324 let c, other, eq_URI =
325 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
326 else right, left, Utils.eq_ind_r_URI ()
328 if o <> U.Incomparable then
330 let res = do_match c eq_URI in
331 res::(find_all_matches ~unif_fun metasenv context ugraph
332 lift_amount term termty tl)
334 | Inference.MatchingFailure
335 | CicUnification.UnificationFailure _
336 | CicUnification.Uncertain _ ->
337 find_all_matches ~unif_fun metasenv context ugraph
338 lift_amount term termty tl
341 let res = do_match c eq_URI in
344 let c' = apply_subst s c
345 and other' = apply_subst s other in
346 let order = cmp c' other' in
347 let names = U.names_of_context context in
348 if order <> U.Lt && order <> U.Le then
349 res::(find_all_matches ~unif_fun metasenv context ugraph
350 lift_amount term termty tl)
352 find_all_matches ~unif_fun metasenv context ugraph
353 lift_amount term termty tl
355 | Inference.MatchingFailure
356 | CicUnification.UnificationFailure _
357 | CicUnification.Uncertain _ ->
358 find_all_matches ~unif_fun metasenv context ugraph
359 lift_amount term termty tl
364 returns true if target is subsumed by some equality in table
366 let subsumption env table target =
367 let _, _, (ty, left, right, _), tmetas, _ = target in
368 let metasenv, context, ugraph = env in
369 let metasenv = metasenv @ tmetas in
370 let samesubst subst subst' =
371 let tbl = Hashtbl.create (List.length subst) in
372 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
374 (fun (m, (c, t1, t2)) ->
376 let c', t1', t2' = Hashtbl.find tbl m in
377 if (c = c') && (t1 = t1') && (t2 = t2') then true
387 let leftc = get_candidates Matching table left in
388 find_all_matches ~unif_fun:Inference.matching
389 metasenv context ugraph 0 left ty leftc
391 let rec ok what = function
393 | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
395 let other = if pos = Utils.Left then r else l in
396 let subst', menv', ug' =
397 let t1 = Unix.gettimeofday () in
400 Inference.matching (metasenv @ menv @ m) context what other ugraph
402 let t2 = Unix.gettimeofday () in
403 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
405 with Inference.MatchingFailure as e ->
406 let t2 = Unix.gettimeofday () in
407 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
410 if samesubst subst subst' then
414 with Inference.MatchingFailure ->
417 let r, subst = ok right leftr in
426 let rightc = get_candidates Matching table right in
427 find_all_matches ~unif_fun:Inference.matching
428 metasenv context ugraph 0 right ty rightc
435 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
436 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
441 let rec demodulation_aux ?(typecheck=false)
442 metasenv context ugraph table lift_amount term =
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 candidates = get_candidates Matching table term in
453 CicTypeChecker.type_of_aux' metasenv context term ugraph
455 C.Implicit None, ugraph
458 find_matches metasenv context ugraph lift_amount term termty candidates
469 (res, tl @ [S.lift 1 t])
472 demodulation_aux metasenv context ugraph table
476 | None -> (None, tl @ [S.lift 1 t])
477 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
482 | Some (_, subst, menv, ug, eq_found) ->
483 Some (C.Appl ll, subst, menv, ug, eq_found)
485 | C.Prod (nn, s, t) ->
487 demodulation_aux metasenv context ugraph table lift_amount s in (
491 demodulation_aux metasenv
492 ((Some (nn, C.Decl s))::context) ugraph
493 table (lift_amount+1) t
497 | Some (t', subst, menv, ug, eq_found) ->
498 Some (C.Prod (nn, (S.lift 1 s), t'),
499 subst, menv, ug, eq_found)
501 | Some (s', subst, menv, ug, eq_found) ->
502 Some (C.Prod (nn, s', (S.lift 1 t)),
503 subst, menv, ug, eq_found)
505 | C.Lambda (nn, s, t) ->
507 demodulation_aux metasenv context ugraph table lift_amount s in (
511 demodulation_aux metasenv
512 ((Some (nn, C.Decl s))::context) ugraph
513 table (lift_amount+1) t
517 | Some (t', subst, menv, ug, eq_found) ->
518 Some (C.Lambda (nn, (S.lift 1 s), t'),
519 subst, menv, ug, eq_found)
521 | Some (s', subst, menv, ug, eq_found) ->
522 Some (C.Lambda (nn, s', (S.lift 1 t)),
523 subst, menv, ug, eq_found)
530 let build_newtarget_time = ref 0.;;
533 let demod_counter = ref 1;;
535 (** demodulation, when target is an equality *)
536 let rec demodulation_equality newmeta env table sign target =
537 let module C = Cic in
538 let module S = CicSubstitution in
539 let module M = CicMetaSubst in
540 let module HL = HelmLibraryObjects in
541 let module U = Utils in
542 let metasenv, context, ugraph = env in
543 let _, proof, (eq_ty, left, right, order), metas, args = target in
544 let metasenv' = metasenv @ metas in
546 let maxmeta = ref newmeta in
548 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
549 let time1 = Unix.gettimeofday () in
551 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
553 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
554 with CicUtil.Meta_not_found _ -> ty
556 let what, other = if pos = Utils.Left then what, other else other, what in
557 let newterm, newproof =
558 let bo = U.guarded_simpl context (apply_subst subst (S.subst other t)) in
559 let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
562 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
563 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
564 S.lift 1 eq_ty; l; r]
566 if sign = Utils.Positive then
568 Inference.ProofBlock (
569 subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
574 CicMkImplicit.identity_relocation_list_for_metavariable context in
575 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
576 (* print_newline (); *)
577 C.Meta (!maxmeta, irl)
582 if pos = Utils.Left then [ty; what; other]
583 else [ty; other; what]
585 Inference.ProofSymBlock (termlist, proof')
588 if pos = Utils.Left then what, other else other, what
590 pos, (0, proof', (ty, other, what, Utils.Incomparable),
595 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
596 eq_found, Inference.BasicProof metaproof)
599 | Inference.BasicProof _ ->
600 print_endline "replacing a BasicProof";
602 | Inference.ProofGoalBlock (_, parent_proof) ->
603 print_endline "replacing another ProofGoalBlock";
604 Inference.ProofGoalBlock (pb, parent_proof)
608 C.Appl [C.MutConstruct (* reflexivity *)
609 (LibraryObjects.eq_URI (), 0, 1, []);
610 eq_ty; if is_left then right else left]
613 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
615 let left, right = if is_left then newterm, right else left, newterm in
616 let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
617 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
620 let ordering = !Utils.compare_terms left right in
622 let time2 = Unix.gettimeofday () in
623 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
626 let w = Utils.compute_equality_weight eq_ty left right in
627 (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
631 let res = demodulation_aux metasenv' context ugraph table 0 left in
632 let newmeta, newtarget =
635 let newmeta, newtarget = build_newtarget true t in
636 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
637 (Inference.meta_convertibility_eq target newtarget) then
640 demodulation_equality newmeta env table sign newtarget
642 let res = demodulation_aux metasenv' context ugraph table 0 right in
645 let newmeta, newtarget = build_newtarget false t in
646 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
647 (Inference.meta_convertibility_eq target newtarget) then
650 demodulation_equality newmeta env table sign newtarget
654 (* newmeta, newtarget *)
655 (* tentiamo di ridurre usando CicReduction.normalize *)
656 let w, p, (ty, left, right, o), m, a = newtarget in
657 let left' = ProofEngineReduction.simpl context left in
658 let right' = ProofEngineReduction.simpl context right in
660 if !Utils.compare_terms left' left = Utils.Lt then left' else left in
662 if !Utils.compare_terms right' right = Utils.Lt then right' else right in
663 (* if newleft != left || newright != right then ( *)
666 (* (Printf.sprintf "left: %s, left': %s\nright: %s, right': %s\n" *)
667 (* (CicPp.ppterm left) (CicPp.ppterm left') (CicPp.ppterm right) *)
668 (* (CicPp.ppterm right'))) *)
670 let w' = Utils.compute_equality_weight ty newleft newright in
671 let o' = !Utils.compare_terms newleft newright in
672 newmeta, (w', p, (ty, newleft, newright, o'), m, a)
677 Performs the beta expansion of the term "term" w.r.t. "table",
678 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
681 let rec betaexpand_term metasenv context ugraph table lift_amount term =
682 let module C = Cic in
683 let module S = CicSubstitution in
684 let module M = CicMetaSubst in
685 let module HL = HelmLibraryObjects in
686 let candidates = get_candidates Unification table term in
687 let res, lifted_term =
692 (fun arg (res, lifted_tl) ->
695 let arg_res, lifted_arg =
696 betaexpand_term metasenv context ugraph table
700 (fun (t, s, m, ug, eq_found) ->
701 (Some t)::lifted_tl, s, m, ug, eq_found)
706 (fun (l, s, m, ug, eq_found) ->
707 (Some lifted_arg)::l, s, m, ug, eq_found)
709 (Some lifted_arg)::lifted_tl)
712 (fun (r, s, m, ug, eq_found) ->
713 None::r, s, m, ug, eq_found) res,
719 (fun (l, s, m, ug, eq_found) ->
720 (C.Meta (i, l), s, m, ug, eq_found)) l'
722 e, C.Meta (i, lifted_l)
725 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
727 | C.Prod (nn, s, t) ->
729 betaexpand_term metasenv context ugraph table lift_amount s in
731 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
732 table (lift_amount+1) t in
735 (fun (t, s, m, ug, eq_found) ->
736 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
739 (fun (t, s, m, ug, eq_found) ->
740 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
741 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
743 | C.Lambda (nn, s, t) ->
745 betaexpand_term metasenv context ugraph table lift_amount s in
747 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
748 table (lift_amount+1) t in
751 (fun (t, s, m, ug, eq_found) ->
752 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
755 (fun (t, s, m, ug, eq_found) ->
756 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
757 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
762 (fun arg (res, lifted_tl) ->
763 let arg_res, lifted_arg =
764 betaexpand_term metasenv context ugraph table lift_amount arg
768 (fun (a, s, m, ug, eq_found) ->
769 a::lifted_tl, s, m, ug, eq_found)
774 (fun (r, s, m, ug, eq_found) ->
775 lifted_arg::r, s, m, ug, eq_found)
777 lifted_arg::lifted_tl)
781 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
784 | t -> [], (S.lift lift_amount t)
787 | C.Meta (i, l) -> res, lifted_term
790 C.Implicit None, ugraph
791 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
795 metasenv context ugraph lift_amount term termty candidates
801 let sup_l_counter = ref 1;;
805 returns a list of new clauses inferred with a left superposition step
806 the negative equation "target" and one of the positive equations in "table"
808 let superposition_left newmeta (metasenv, context, ugraph) table target =
809 let module C = Cic in
810 let module S = CicSubstitution in
811 let module M = CicMetaSubst in
812 let module HL = HelmLibraryObjects in
813 let module CR = CicReduction in
814 let module U = Utils in
815 let weight, proof, (eq_ty, left, right, ordering), _, _ = target in
817 let term = if ordering = U.Gt then left else right in
818 betaexpand_term metasenv context ugraph table 0 term
820 let maxmeta = ref newmeta in
821 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
823 (* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
825 let time1 = Unix.gettimeofday () in
827 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
828 let what, other = if pos = Utils.Left then what, other else other, what in
829 let newgoal, newproof =
830 let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
831 let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
835 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
836 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
837 S.lift 1 eq_ty; l; r]
842 CicMkImplicit.identity_relocation_list_for_metavariable context in
843 C.Meta (!maxmeta, irl)
848 if pos = Utils.Left then [ty; what; other]
849 else [ty; other; what]
851 Inference.ProofSymBlock (termlist, proof')
854 if pos = Utils.Left then what, other else other, what
856 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
860 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
861 Inference.BasicProof metaproof)
864 | Inference.BasicProof _ ->
865 (* debug_print (lazy "replacing a BasicProof"); *)
867 | Inference.ProofGoalBlock (_, parent_proof) ->
868 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
869 Inference.ProofGoalBlock (pb, parent_proof)
873 C.Appl [C.MutConstruct (* reflexivity *)
874 (LibraryObjects.eq_URI (), 0, 1, []);
875 eq_ty; if ordering = U.Gt then right else left]
878 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
881 if ordering = U.Gt then newgoal, right else left, newgoal in
882 let neworder = !Utils.compare_terms left right in
884 let time2 = Unix.gettimeofday () in
885 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
888 let w = Utils.compute_equality_weight eq_ty left right in
889 (w, newproof, (eq_ty, left, right, neworder), [], [])
893 !maxmeta, List.map build_new expansions
897 let sup_r_counter = ref 1;;
901 returns a list of new clauses inferred with a right superposition step
902 between the positive equation "target" and one in the "table" "newmeta" is
903 the first free meta index, i.e. the first number above the highest meta
904 index: its updated value is also returned
906 let superposition_right newmeta (metasenv, context, ugraph) table target =
907 let module C = Cic in
908 let module S = CicSubstitution in
909 let module M = CicMetaSubst in
910 let module HL = HelmLibraryObjects in
911 let module CR = CicReduction in
912 let module U = Utils in
913 let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
914 let metasenv' = metasenv @ newmetas in
915 let maxmeta = ref newmeta in
918 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
919 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
923 (fun (_, subst, _, _, _) ->
924 let subst = apply_subst subst in
925 let o = !Utils.compare_terms (subst l) (subst r) in
926 o <> U.Lt && o <> U.Le)
927 (fst (betaexpand_term metasenv' context ugraph table 0 l))
929 (res left right), (res right left)
931 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
933 let time1 = Unix.gettimeofday () in
935 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
936 let what, other = if pos = Utils.Left then what, other else other, what in
937 let newgoal, newproof =
938 let bo' = apply_subst s (S.subst other bo) in
940 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
943 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
944 (name, ty, S.lift 1 eq_ty, l, r)
946 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
950 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
951 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
952 S.lift 1 eq_ty; l; r]
955 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
957 let newmeta, newequality =
959 if ordering = U.Gt then newgoal, apply_subst s right
960 else apply_subst s left, newgoal in
961 let neworder = !Utils.compare_terms left right
962 and newmenv = newmetas @ menv'
963 and newargs = args @ args' in
965 let w = Utils.compute_equality_weight eq_ty left right in
966 (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
967 and env = (metasenv, context, ugraph) in
968 let newm, eq' = Inference.fix_metas !maxmeta eq' in
973 let time2 = Unix.gettimeofday () in
974 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
978 let new1 = List.map (build_new U.Gt) res1
979 and new2 = List.map (build_new U.Lt) res2 in
980 let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
982 (List.filter ok (new1 @ new2)))
986 (** demodulation, when the target is a goal *)
987 let rec demodulation_goal newmeta env table goal =
988 let module C = Cic in
989 let module S = CicSubstitution in
990 let module M = CicMetaSubst in
991 let module HL = HelmLibraryObjects in
992 let metasenv, context, ugraph = env in
993 let maxmeta = ref newmeta in
994 let proof, metas, term = goal in
995 let metasenv' = metasenv @ metas in
997 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
998 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
999 let what, other = if pos = Utils.Left then what, other else other, what in
1001 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
1002 with CicUtil.Meta_not_found _ -> ty
1004 let newterm, newproof =
1005 let bo = apply_subst subst (S.subst other t) in
1006 let bo' = apply_subst subst t in
1007 let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
1012 CicMkImplicit.identity_relocation_list_for_metavariable context in
1013 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
1014 C.Meta (!maxmeta, irl)
1019 if pos = Utils.Left then [ty; what; other]
1020 else [ty; other; what]
1022 Inference.ProofSymBlock (termlist, proof')
1025 if pos = Utils.Left then what, other else other, what
1027 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
1031 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
1032 eq_found, Inference.BasicProof metaproof)
1034 let rec repl = function
1035 | Inference.NoProof ->
1036 (* debug_print (lazy "replacing a NoProof"); *)
1038 | Inference.BasicProof _ ->
1039 (* debug_print (lazy "replacing a BasicProof"); *)
1041 | Inference.ProofGoalBlock (_, parent_proof) ->
1042 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
1043 Inference.ProofGoalBlock (pb, parent_proof)
1044 | (Inference.SubProof (term, meta_index, p) as subproof) ->
1047 (* (Printf.sprintf "replacing %s" *)
1048 (* (Inference.string_of_proof subproof))); *)
1049 Inference.SubProof (term, meta_index, repl p)
1053 bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
1055 let m = Inference.metas_of_term newterm in
1056 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
1057 !maxmeta, (newproof, newmetasenv, newterm)
1060 demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
1064 let newmeta, newgoal = build_newgoal t in
1065 let _, _, newg = newgoal in
1066 if Inference.meta_convertibility term newg then
1069 demodulation_goal newmeta env table newgoal
1075 (** demodulation, when the target is a theorem *)
1076 let rec demodulation_theorem newmeta env table theorem =
1077 let module C = Cic in
1078 let module S = CicSubstitution in
1079 let module M = CicMetaSubst in
1080 let module HL = HelmLibraryObjects in
1081 let metasenv, context, ugraph = env in
1082 let maxmeta = ref newmeta in
1083 let proof, metas, term = theorem in
1084 let term, termty, metas = theorem in
1085 let metasenv' = metasenv @ metas in
1087 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1088 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1089 let what, other = if pos = Utils.Left then what, other else other, what in
1090 let newterm, newty =
1091 let bo = apply_subst subst (S.subst other t) in
1092 let bo' = apply_subst subst t in
1093 let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1096 Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1097 Inference.BasicProof term)
1099 (Inference.build_proof_term newproof, bo)
1101 let m = Inference.metas_of_term newterm in
1102 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
1103 !maxmeta, (newterm, newty, newmetasenv)
1106 demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty
1110 let newmeta, newthm = build_newtheorem t in
1111 let newt, newty, _ = newthm in
1112 if Inference.meta_convertibility termty newty then
1115 demodulation_theorem newmeta env table newthm