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 beta_expand_time = ref 0.;;
35 let debug_print = Utils.debug_print;;
39 let check_equation env equation msg =
40 let w, proof, (eq_ty, left, right, order), metas, args = equation in
41 let metasenv, context, ugraph = env
42 let metasenv' = metasenv @ metas in
44 CicTypeChecker.type_of_aux' metasenv' context left ugraph;
45 CicTypeChecker.type_of_aux' metasenv' context right ugraph;
48 CicUtil.Meta_not_found _ as exn ->
51 prerr_endline (CicPp.ppterm left);
52 prerr_endline (CicPp.ppterm right);
57 type retrieval_mode = Matching | Unification;;
59 let string_of_res ?env =
62 | Some (t, s, m, u, ((p,e), eq_URI)) ->
63 Printf.sprintf "Some: (%s, %s, %s)"
64 (Utils.string_of_pos p)
65 (Inference.string_of_equality ?env e)
69 let print_res ?env res =
72 (List.map (string_of_res ?env) res))
75 let print_candidates ?env mode term res =
79 prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
81 prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
87 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
88 (Inference.string_of_equality ?env e))
93 let indexing_retrieval_time = ref 0.;;
96 let apply_subst = CicMetaSubst.apply_subst
98 let index = Index.index
99 let remove_index = Index.remove_index
100 let in_index = Index.in_index
101 let empty = Index.empty
102 let init_index = Index.init_index
104 let check_disjoint_invariant subst metasenv msg =
106 (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
109 prerr_endline ("not disjoint: " ^ msg);
114 let check_for_duplicates metas msg =
117 ignore(CicUtil.lookup_meta 190 metas);
118 prerr_endline ("eccoci in " ^ msg);
120 CicUtil.Meta_not_found _ -> () in
121 if List.length metas <>
122 List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
124 prerr_endline ("DUPLICATI " ^ msg);
125 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
130 let check_res res msg =
132 Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
133 let eqs = Inference.string_of_equality (snd eq_found) in
134 check_disjoint_invariant subst menv msg;
135 check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
139 let check_target context target msg =
140 let w, proof, (eq_ty, left, right, order), metas, args = target in
141 (* check that metas does not contains duplicates *)
142 let eqs = Inference.string_of_equality target in
143 let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
144 let actual = (Inference.metas_of_term left)@(Inference.metas_of_term right)
145 @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof) in
146 let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
147 let _ = if menv <> metas then
149 prerr_endline ("extra metas " ^ msg);
150 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
151 prerr_endline "**********************";
152 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
153 prerr_endline ("left: " ^ (CicPp.ppterm left));
154 prerr_endline ("right: " ^ (CicPp.ppterm right));
155 prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
160 CicTypeChecker.type_of_aux'
161 metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph
164 prerr_endline (Inference.string_of_proof proof);
165 prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
166 prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
167 prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
172 (* returns a list of all the equalities in the tree that are in relation
173 "mode" with the given term, where mode can be either Matching or
176 Format of the return value: list of tuples in the form:
177 (position - Left or Right - of the term that matched the given one in this
181 Note that if equality is "left = right", if the ordering is left > right,
182 the position will always be Left, and if the ordering is left < right,
183 position will be Right.
185 let local_max = ref 100;;
187 let make_variant (p,eq) =
188 let maxmeta, eq = Inference.fix_metas !local_max eq in
189 local_max := maxmeta;
193 let get_candidates ?env mode tree term =
194 let t1 = Unix.gettimeofday () in
198 | Matching -> Index.retrieve_generalizations tree term
199 | Unification -> Index.retrieve_unifiables tree term
201 Index.PosEqSet.elements s
203 (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
204 (* print_newline (); *)
205 let t2 = Unix.gettimeofday () in
206 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
207 (* make fresh instances *)
212 let match_unif_time_ok = ref 0.;;
213 let match_unif_time_no = ref 0.;;
217 finds the first equality in the index that matches "term", of type "termty"
218 termty can be Implicit if it is not needed. The result (one of the sides of
219 the equality, actually) should be not greater (wrt the term ordering) than
222 Format of the return value:
224 (term to substitute, [Cic.Rel 1 properly lifted - see the various
225 build_newtarget functions inside the various
226 demodulation_* functions]
227 substitution used for the matching,
229 ugraph, [substitution, metasenv and ugraph have the same meaning as those
230 returned by CicUnification.fo_unif]
231 (equality where the matching term was found, [i.e. the equality to use as
233 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
234 the equality: this is used to build the proof term, again see one of
235 the build_newtarget functions]
238 let rec find_matches metasenv context ugraph lift_amount term termty =
239 let module C = Cic in
240 let module U = Utils in
241 let module S = CicSubstitution in
242 let module M = CicMetaSubst in
243 let module HL = HelmLibraryObjects in
244 let cmp = !Utils.compare_terms in
245 let check = match termty with C.Implicit None -> false | _ -> true in
249 let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
250 if Utils.debug_metas then
251 ignore(check_target context (snd candidate) "find_matches");
252 if Utils.debug_res then
254 let c = "eq = " ^ (Inference.string_of_equality (snd candidate)) ^ "\n"in
255 let t = "t = " ^ (CicPp.ppterm term) ^ "\n" in
256 let m = "metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
257 let p = "proof = " ^ (CicPp.ppterm (Inference.build_proof_term proof)) ^ "\n" in
258 check_for_duplicates metas "gia nella metas";
259 check_for_duplicates (metasenv @ metas) ("not disjoint" ^ c ^ t ^ m ^ p)
261 if check && not (fst (CicReduction.are_convertible
262 ~metasenv context termty ty ugraph)) then (
263 find_matches metasenv context ugraph lift_amount term termty tl
265 let do_match c eq_URI =
266 let subst', metasenv', ugraph' =
267 let t1 = Unix.gettimeofday () in
270 ( Inference.matching metasenv metas context
271 term (S.lift lift_amount c)) ugraph
273 let t2 = Unix.gettimeofday () in
274 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
277 | Inference.MatchingFailure as e ->
278 let t2 = Unix.gettimeofday () in
279 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
281 | CicUtil.Meta_not_found _ as exn -> raise exn
283 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
286 let c, other, eq_URI =
287 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
288 else right, left, Utils.eq_ind_r_URI ()
290 if o <> U.Incomparable then
294 with Inference.MatchingFailure ->
295 find_matches metasenv context ugraph lift_amount term termty tl
297 if Utils.debug_res then ignore (check_res res "find1");
301 try do_match c eq_URI
302 with Inference.MatchingFailure -> None
304 if Utils.debug_res then ignore (check_res res "find2");
306 | Some (_, s, _, _, _) ->
307 let c' = apply_subst s c in
309 let other' = U.guarded_simpl context (apply_subst s other) in *)
310 let other' = apply_subst s other in
311 let order = cmp c' other' in
316 metasenv context ugraph lift_amount term termty tl
318 find_matches metasenv context ugraph lift_amount term termty tl
323 as above, but finds all the matching equalities, and the matching condition
324 can be either Inference.matching or Inference.unification
326 let rec find_all_matches ?(unif_fun=Inference.unification)
327 metasenv context ugraph lift_amount term termty =
328 let module C = Cic in
329 let module U = Utils in
330 let module S = CicSubstitution in
331 let module M = CicMetaSubst in
332 let module HL = HelmLibraryObjects in
333 let cmp = !Utils.compare_terms in
337 let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
338 let do_match c eq_URI =
339 let subst', metasenv', ugraph' =
340 let t1 = Unix.gettimeofday () in
343 unif_fun metasenv metas context
344 term (S.lift lift_amount c) ugraph in
345 let t2 = Unix.gettimeofday () in
346 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
349 | Inference.MatchingFailure
350 | CicUnification.UnificationFailure _
351 | CicUnification.Uncertain _ as e ->
352 let t2 = Unix.gettimeofday () in
353 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
356 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
359 let c, other, eq_URI =
360 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
361 else right, left, Utils.eq_ind_r_URI ()
363 if o <> U.Incomparable then
365 let res = do_match c eq_URI in
366 res::(find_all_matches ~unif_fun metasenv context ugraph
367 lift_amount term termty tl)
369 | Inference.MatchingFailure
370 | CicUnification.UnificationFailure _
371 | CicUnification.Uncertain _ ->
372 find_all_matches ~unif_fun metasenv context ugraph
373 lift_amount term termty tl
376 let res = do_match c eq_URI in
379 let c' = apply_subst s c
380 and other' = apply_subst s other in
381 let order = cmp c' other' in
382 if order <> U.Lt && order <> U.Le then
383 res::(find_all_matches ~unif_fun metasenv context ugraph
384 lift_amount term termty tl)
386 find_all_matches ~unif_fun metasenv context ugraph
387 lift_amount term termty tl
389 | Inference.MatchingFailure
390 | CicUnification.UnificationFailure _
391 | CicUnification.Uncertain _ ->
392 find_all_matches ~unif_fun metasenv context ugraph
393 lift_amount term termty tl
398 returns true if target is subsumed by some equality in table
400 let subsumption env table target =
401 let _, _, (ty, left, right, _), tmetas, _ = target in
402 let metasenv, context, ugraph = env in
403 let metasenv = metasenv @ tmetas in
404 let samesubst subst subst' =
405 let tbl = Hashtbl.create (List.length subst) in
406 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
408 (fun (m, (c, t1, t2)) ->
410 let c', t1', t2' = Hashtbl.find tbl m in
411 if (c = c') && (t1 = t1') && (t2 = t2') then true
421 let leftc = get_candidates Matching table left in
422 find_all_matches ~unif_fun:Inference.matching
423 metasenv context ugraph 0 left ty leftc
425 let rec ok what = function
427 | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
429 let other = if pos = Utils.Left then r else l in
430 let subst', menv', ug' =
431 let t1 = Unix.gettimeofday () in
434 Inference.matching menv m context what other ugraph
436 let t2 = Unix.gettimeofday () in
437 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
439 with Inference.MatchingFailure as e ->
440 let t2 = Unix.gettimeofday () in
441 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
444 if samesubst subst subst' then
448 with Inference.MatchingFailure ->
451 let r, subst = ok right leftr in
460 let rightc = get_candidates Matching table right in
461 find_all_matches ~unif_fun:Inference.matching
462 metasenv context ugraph 0 right ty rightc
469 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
470 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
474 let rec demodulation_aux ?from ?(typecheck=false)
475 metasenv context ugraph table lift_amount term =
476 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
477 let module C = Cic in
478 let module S = CicSubstitution in
479 let module M = CicMetaSubst in
480 let module HL = HelmLibraryObjects in
482 get_candidates ~env:(metasenv,context,ugraph) Matching table term in
483 (* let candidates = List.map make_variant candidates in *)
490 CicTypeChecker.type_of_aux' metasenv context term ugraph
492 C.Implicit None, ugraph
495 find_matches metasenv context ugraph lift_amount term termty candidates
497 if Utils.debug_res then ignore(check_res res "demod1");
507 (res, tl @ [S.lift 1 t])
510 demodulation_aux ~from:"1" metasenv context ugraph table
514 | None -> (None, tl @ [S.lift 1 t])
515 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
520 | Some (_, subst, menv, ug, eq_found) ->
521 Some (C.Appl ll, subst, menv, ug, eq_found)
523 | C.Prod (nn, s, t) ->
525 demodulation_aux ~from:"2"
526 metasenv context ugraph table lift_amount s in (
530 demodulation_aux metasenv
531 ((Some (nn, C.Decl s))::context) ugraph
532 table (lift_amount+1) t
536 | Some (t', subst, menv, ug, eq_found) ->
537 Some (C.Prod (nn, (S.lift 1 s), t'),
538 subst, menv, ug, eq_found)
540 | Some (s', subst, menv, ug, eq_found) ->
541 Some (C.Prod (nn, s', (S.lift 1 t)),
542 subst, menv, ug, eq_found)
544 | C.Lambda (nn, s, t) ->
547 metasenv context ugraph table lift_amount s in (
551 demodulation_aux metasenv
552 ((Some (nn, C.Decl s))::context) ugraph
553 table (lift_amount+1) t
557 | Some (t', subst, menv, ug, eq_found) ->
558 Some (C.Lambda (nn, (S.lift 1 s), t'),
559 subst, menv, ug, eq_found)
561 | Some (s', subst, menv, ug, eq_found) ->
562 Some (C.Lambda (nn, s', (S.lift 1 t)),
563 subst, menv, ug, eq_found)
568 if Utils.debug_res then ignore(check_res res "demod_aux output");
573 let build_newtarget_time = ref 0.;;
576 let demod_counter = ref 1;;
580 (** demodulation, when target is an equality *)
581 let rec demodulation_equality ?from newmeta env table sign target =
582 let module C = Cic in
583 let module S = CicSubstitution in
584 let module M = CicMetaSubst in
585 let module HL = HelmLibraryObjects in
586 let module U = Utils in
587 let metasenv, context, ugraph = env in
588 let w, proof, (eq_ty, left, right, order), metas, args = target in
589 (* first, we simplify *)
590 let right = U.guarded_simpl context right in
591 let left = U.guarded_simpl context left in
592 let w = Utils.compute_equality_weight eq_ty left right in
593 let order = !Utils.compare_terms left right in
594 let target = w, proof, (eq_ty, left, right, order), metas, args in
595 if Utils.debug_metas then
596 ignore(check_target context target "demod equalities input");
597 let metasenv' = (* metasenv @ *) metas in
598 let maxmeta = ref newmeta in
600 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
601 let time1 = Unix.gettimeofday () in
603 if Utils.debug_metas then
605 ignore(check_for_duplicates menv "input1");
606 ignore(check_disjoint_invariant subst menv "input2");
607 let substs = CicMetaSubst.ppsubst subst in
608 ignore(check_target context (snd eq_found) ("input3" ^ substs))
610 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
612 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
613 with CicUtil.Meta_not_found _ -> ty
615 let what, other = if pos = Utils.Left then what, other else other, what in
616 let newterm, newproof =
617 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
618 let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in
621 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
622 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
623 S.lift 1 eq_ty; l; r]
625 if sign = Utils.Positive then
627 Inference.ProofBlock (
628 subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
633 CicMkImplicit.identity_relocation_list_for_metavariable context in
634 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
635 (* print_newline (); *)
636 C.Meta (!maxmeta, irl)
641 if pos = Utils.Left then [ty; what; other]
642 else [ty; other; what]
644 Inference.ProofSymBlock (termlist, proof')
647 if pos = Utils.Left then what, other else other, what
649 pos, (0, proof', (ty, other, what, Utils.Incomparable),
654 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
655 eq_found, Inference.BasicProof metaproof)
658 | Inference.BasicProof _ ->
659 (* print_endline "replacing a BasicProof"; *)
661 | Inference.ProofGoalBlock (_, parent_proof) ->
663 (* print_endline "replacing another ProofGoalBlock"; *)
664 Inference.ProofGoalBlock (pb, parent_proof)
668 C.Appl [C.MutConstruct (* reflexivity *)
669 (LibraryObjects.eq_URI (), 0, 1, []);
670 eq_ty; if is_left then right else left]
673 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
675 let newmenv = (* Inference.filter subst *) menv in
677 if Utils.debug_metas then
678 try ignore(CicTypeChecker.type_of_aux'
679 newmenv context (Inference.build_proof_term newproof) ugraph);
682 prerr_endline "sempre lui";
683 prerr_endline (CicMetaSubst.ppsubst subst);
684 prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
685 prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
686 prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
687 prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
688 prerr_endline ("+++++++++++++subst: " ^ (CicMetaSubst.ppsubst subst));
692 let left, right = if is_left then newterm, right else left, newterm in
693 let ordering = !Utils.compare_terms left right in
694 let time2 = Unix.gettimeofday () in
695 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
697 let w = Utils.compute_equality_weight eq_ty left right in
698 (w, newproof, (eq_ty, left, right, ordering),newmenv,args) in
699 if Utils.debug_metas then
700 ignore(check_target context res "buildnew_target output");
704 let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
705 if Utils.debug_res then check_res res "demod result";
706 let newmeta, newtarget =
709 let newmeta, newtarget = build_newtarget true t in
710 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
711 (Inference.meta_convertibility_eq target newtarget) then
714 demodulation_equality newmeta env table sign newtarget
716 let res = demodulation_aux metasenv' context ugraph table 0 right in
717 if Utils.debug_res then check_res res "demod result 1";
720 let newmeta, newtarget = build_newtarget false t in
721 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
722 (Inference.meta_convertibility_eq target newtarget) then
725 demodulation_equality newmeta env table sign newtarget
729 (* newmeta, newtarget *)
735 Performs the beta expansion of the term "term" w.r.t. "table",
736 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
739 let rec betaexpand_term metasenv context ugraph table lift_amount term =
740 let module C = Cic in
741 let module S = CicSubstitution in
742 let module M = CicMetaSubst in
743 let module HL = HelmLibraryObjects in
744 let candidates = get_candidates Unification table term in
746 let res, lifted_term =
751 (fun arg (res, lifted_tl) ->
754 let arg_res, lifted_arg =
755 betaexpand_term metasenv context ugraph table
759 (fun (t, s, m, ug, eq_found) ->
760 (Some t)::lifted_tl, s, m, ug, eq_found)
765 (fun (l, s, m, ug, eq_found) ->
766 (Some lifted_arg)::l, s, m, ug, eq_found)
768 (Some lifted_arg)::lifted_tl)
771 (fun (r, s, m, ug, eq_found) ->
772 None::r, s, m, ug, eq_found) res,
778 (fun (l, s, m, ug, eq_found) ->
779 (C.Meta (i, l), s, m, ug, eq_found)) l'
781 e, C.Meta (i, lifted_l)
784 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
786 | C.Prod (nn, s, t) ->
788 betaexpand_term metasenv context ugraph table lift_amount s in
790 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
791 table (lift_amount+1) t in
794 (fun (t, s, m, ug, eq_found) ->
795 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
798 (fun (t, s, m, ug, eq_found) ->
799 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
800 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
802 | C.Lambda (nn, s, t) ->
804 betaexpand_term metasenv context ugraph table lift_amount s in
806 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
807 table (lift_amount+1) t in
810 (fun (t, s, m, ug, eq_found) ->
811 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
814 (fun (t, s, m, ug, eq_found) ->
815 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
816 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
821 (fun arg (res, lifted_tl) ->
822 let arg_res, lifted_arg =
823 betaexpand_term metasenv context ugraph table lift_amount arg
827 (fun (a, s, m, ug, eq_found) ->
828 a::lifted_tl, s, m, ug, eq_found)
833 (fun (r, s, m, ug, eq_found) ->
834 lifted_arg::r, s, m, ug, eq_found)
836 lifted_arg::lifted_tl)
840 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
843 | t -> [], (S.lift lift_amount t)
846 | C.Meta (i, l) -> res, lifted_term
849 C.Implicit None, ugraph
850 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
854 metasenv context ugraph lift_amount term termty candidates
860 let sup_l_counter = ref 1;;
864 returns a list of new clauses inferred with a left superposition step
865 the negative equation "target" and one of the positive equations in "table"
867 let superposition_left newmeta (metasenv, context, ugraph) table target =
868 let module C = Cic in
869 let module S = CicSubstitution in
870 let module M = CicMetaSubst in
871 let module HL = HelmLibraryObjects in
872 let module CR = CicReduction in
873 let module U = Utils in
874 let weight, proof, (eq_ty, left, right, ordering), menv, _ = target in
875 if Utils.debug_metas then
876 ignore(check_target context target "superpositionleft");
878 let term = if ordering = U.Gt then left else right in
880 let t1 = Unix.gettimeofday () in
881 let res = betaexpand_term metasenv context ugraph table 0 term in
882 let t2 = Unix.gettimeofday () in
883 beta_expand_time := !beta_expand_time +. (t2 -. t1);
887 let maxmeta = ref newmeta in
888 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
889 (* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
890 let time1 = Unix.gettimeofday () in
892 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
893 let what, other = if pos = Utils.Left then what, other else other, what in
894 let newgoal, newproof =
895 let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
896 let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
900 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
901 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
902 S.lift 1 eq_ty; l; r]
907 CicMkImplicit.identity_relocation_list_for_metavariable context in
908 C.Meta (!maxmeta, irl)
913 if pos = Utils.Left then [ty; what; other]
914 else [ty; other; what]
916 Inference.ProofSymBlock (termlist, proof')
919 if pos = Utils.Left then what, other else other, what
921 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
925 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
926 Inference.BasicProof metaproof)
929 | Inference.BasicProof _ ->
930 (* debug_print (lazy "replacing a BasicProof"); *)
932 | Inference.ProofGoalBlock (_, parent_proof) ->
933 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
934 Inference.ProofGoalBlock (pb, parent_proof)
938 C.Appl [C.MutConstruct (* reflexivity *)
939 (LibraryObjects.eq_URI (), 0, 1, []);
940 eq_ty; if ordering = U.Gt then right else left]
943 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
946 if ordering = U.Gt then newgoal, right else left, newgoal in
947 let neworder = !Utils.compare_terms left right in
948 let newmenv = (* Inference.filter s *) menv in
949 let time2 = Unix.gettimeofday () in
950 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
952 let w = Utils.compute_equality_weight eq_ty left right in
953 (w, newproof, (eq_ty, left, right, neworder), newmenv, [])
956 !maxmeta, List.map build_new expansions
960 let sup_r_counter = ref 1;;
964 returns a list of new clauses inferred with a right superposition step
965 between the positive equation "target" and one in the "table" "newmeta" is
966 the first free meta index, i.e. the first number above the highest meta
967 index: its updated value is also returned
969 let superposition_right newmeta (metasenv, context, ugraph) table target =
970 let module C = Cic in
971 let module S = CicSubstitution in
972 let module M = CicMetaSubst in
973 let module HL = HelmLibraryObjects in
974 let module CR = CicReduction in
975 let module U = Utils in
976 let w, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
977 if Utils.debug_metas then
978 ignore (check_target context target "superpositionright");
979 let metasenv' = newmetas in
980 let maxmeta = ref newmeta in
982 let betaexpand_term metasenv context ugraph table d term =
983 let t1 = Unix.gettimeofday () in
984 let res = betaexpand_term metasenv context ugraph table d term in
985 let t2 = Unix.gettimeofday () in
986 beta_expand_time := !beta_expand_time +. (t2 -. t1);
990 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
991 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
995 (fun (_, subst, _, _, _) ->
996 let subst = apply_subst subst in
997 let o = !Utils.compare_terms (subst l) (subst r) in
998 o <> U.Lt && o <> U.Le)
999 (fst (betaexpand_term metasenv' context ugraph table 0 l))
1001 (res left right), (res right left)
1003 let build_new ordering ((bo, s, m, ug, (eq_found, eq_URI)) as input) =
1004 if Utils.debug_metas then
1005 ignore (check_target context (snd eq_found) "buildnew1" );
1006 let time1 = Unix.gettimeofday () in
1008 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1009 let what, other = if pos = Utils.Left then what, other else other, what in
1010 let newgoal, newproof =
1012 let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
1013 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
1017 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1018 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1019 S.lift 1 eq_ty; l; r]
1022 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
1024 let newmeta, newequality =
1026 if ordering = U.Gt then newgoal, apply_subst s right
1027 else apply_subst s left, newgoal in
1028 let neworder = !Utils.compare_terms left right in
1029 let newmenv = (* Inference.filter s *) m in
1030 let newargs = args @ args' in
1032 let w = Utils.compute_equality_weight eq_ty left right in
1033 (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in
1034 if Utils.debug_metas then
1035 ignore (check_target context eq' "buildnew3");
1036 let newm, eq' = Inference.fix_metas !maxmeta eq' in
1037 if Utils.debug_metas then
1038 ignore (check_target context eq' "buildnew4");
1042 let time2 = Unix.gettimeofday () in
1043 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1044 if Utils.debug_metas then
1045 ignore(check_target context newequality "buildnew2");
1048 let new1 = List.map (build_new U.Gt) res1
1049 and new2 = List.map (build_new U.Lt) res2 in
1050 let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
1052 (List.filter ok (new1 @ new2)))
1056 (** demodulation, when the target is a goal *)
1057 let rec demodulation_goal newmeta env table goal =
1058 let module C = Cic in
1059 let module S = CicSubstitution in
1060 let module M = CicMetaSubst in
1061 let module HL = HelmLibraryObjects in
1062 let metasenv, context, ugraph = env in
1063 let maxmeta = ref newmeta in
1064 let proof, metas, term = goal in
1065 let term = Utils.guarded_simpl (~debug:true) context term in
1066 let goal = proof, metas, term in
1067 let metasenv' = metas in
1069 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1070 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1071 let what, other = if pos = Utils.Left then what, other else other, what in
1073 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
1074 with CicUtil.Meta_not_found _ -> ty
1076 let newterm, newproof =
1077 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1078 let bo' = apply_subst subst t in
1079 let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
1084 CicMkImplicit.identity_relocation_list_for_metavariable context in
1085 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
1086 C.Meta (!maxmeta, irl)
1091 if pos = Utils.Left then [ty; what; other]
1092 else [ty; other; what]
1094 Inference.ProofSymBlock (termlist, proof')
1097 if pos = Utils.Left then what, other else other, what
1099 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
1103 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
1104 eq_found, Inference.BasicProof metaproof)
1106 let rec repl = function
1107 | Inference.NoProof ->
1108 (* debug_print (lazy "replacing a NoProof"); *)
1110 | Inference.BasicProof _ ->
1111 (* debug_print (lazy "replacing a BasicProof"); *)
1113 | Inference.ProofGoalBlock (_, parent_proof) ->
1114 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
1115 Inference.ProofGoalBlock (pb, parent_proof)
1116 | Inference.SubProof (term, meta_index, p) ->
1117 Inference.SubProof (term, meta_index, repl p)
1121 bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
1123 let newmetasenv = (* Inference.filter subst *) menv in
1124 !maxmeta, (newproof, newmetasenv, newterm)
1127 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
1131 let newmeta, newgoal = build_newgoal t in
1132 let _, _, newg = newgoal in
1133 if Inference.meta_convertibility term newg then
1136 demodulation_goal newmeta env table newgoal
1142 (** demodulation, when the target is a theorem *)
1143 let rec demodulation_theorem newmeta env table theorem =
1144 let module C = Cic in
1145 let module S = CicSubstitution in
1146 let module M = CicMetaSubst in
1147 let module HL = HelmLibraryObjects in
1148 let metasenv, context, ugraph = env in
1149 let maxmeta = ref newmeta in
1150 let term, termty, metas = theorem in
1151 let metasenv' = metas in
1153 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1154 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1155 let what, other = if pos = Utils.Left then what, other else other, what in
1156 let newterm, newty =
1157 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1158 let bo' = apply_subst subst t in
1159 let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1162 Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1163 Inference.BasicProof term)
1165 (Inference.build_proof_term newproof, bo)
1168 let m = Inference.metas_of_term newterm in
1169 !maxmeta, (newterm, newty, menv)
1172 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1176 let newmeta, newthm = build_newtheorem t in
1177 let newt, newty, _ = newthm in
1178 if Inference.meta_convertibility termty newty then
1181 demodulation_theorem newmeta env table newthm