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 =
115 if List.length metas <>
116 List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
118 prerr_endline ("DUPLICATI " ^ msg);
119 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
124 let check_res res msg =
126 Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
127 let eqs = Inference.string_of_equality (snd eq_found) in
128 check_disjoint_invariant subst menv msg;
129 check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
133 let check_target context target msg =
134 let w, proof, (eq_ty, left, right, order), metas = target in
135 (* check that metas does not contains duplicates *)
136 let eqs = Inference.string_of_equality target in
137 let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
138 let actual = (Inference.metas_of_term left)@(Inference.metas_of_term right)
139 @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof) in
140 let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
141 let _ = if menv <> metas then
143 prerr_endline ("extra metas " ^ msg);
144 prerr_endline (CicMetaSubst.ppmetasenv [] metas);
145 prerr_endline "**********************";
146 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
147 prerr_endline ("left: " ^ (CicPp.ppterm left));
148 prerr_endline ("right: " ^ (CicPp.ppterm right));
149 prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
154 CicTypeChecker.type_of_aux'
155 metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph
158 prerr_endline (Inference.string_of_proof proof);
159 prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
160 prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
161 prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
166 (* returns a list of all the equalities in the tree that are in relation
167 "mode" with the given term, where mode can be either Matching or
170 Format of the return value: list of tuples in the form:
171 (position - Left or Right - of the term that matched the given one in this
175 Note that if equality is "left = right", if the ordering is left > right,
176 the position will always be Left, and if the ordering is left < right,
177 position will be Right.
179 let local_max = ref 100;;
181 let make_variant (p,eq) =
182 let maxmeta, eq = Inference.fix_metas !local_max eq in
183 local_max := maxmeta;
187 let get_candidates ?env mode tree term =
188 let t1 = Unix.gettimeofday () in
192 | Matching -> Index.retrieve_generalizations tree term
193 | Unification -> Index.retrieve_unifiables tree term
195 Index.PosEqSet.elements s
197 (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
198 (* print_newline (); *)
199 let t2 = Unix.gettimeofday () in
200 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
201 (* make fresh instances *)
206 let match_unif_time_ok = ref 0.;;
207 let match_unif_time_no = ref 0.;;
211 finds the first equality in the index that matches "term", of type "termty"
212 termty can be Implicit if it is not needed. The result (one of the sides of
213 the equality, actually) should be not greater (wrt the term ordering) than
216 Format of the return value:
218 (term to substitute, [Cic.Rel 1 properly lifted - see the various
219 build_newtarget functions inside the various
220 demodulation_* functions]
221 substitution used for the matching,
223 ugraph, [substitution, metasenv and ugraph have the same meaning as those
224 returned by CicUnification.fo_unif]
225 (equality where the matching term was found, [i.e. the equality to use as
227 uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
228 the equality: this is used to build the proof term, again see one of
229 the build_newtarget functions]
232 let rec find_matches metasenv context ugraph lift_amount term termty =
233 let module C = Cic in
234 let module U = Utils in
235 let module S = CicSubstitution in
236 let module M = CicMetaSubst in
237 let module HL = HelmLibraryObjects in
238 let cmp = !Utils.compare_terms in
239 let check = match termty with C.Implicit None -> false | _ -> true in
243 let pos, (_, proof, (ty, left, right, o), metas) = candidate in
244 if Utils.debug_metas then
245 ignore(check_target context (snd candidate) "find_matches");
246 if Utils.debug_res then
248 let c = "eq = " ^ (Inference.string_of_equality (snd candidate)) ^ "\n"in
249 let t = "t = " ^ (CicPp.ppterm term) ^ "\n" in
250 let m = "metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
251 let p = "proof = " ^ (CicPp.ppterm (Inference.build_proof_term proof)) ^ "\n" in
252 check_for_duplicates metas "gia nella metas";
253 check_for_duplicates (metasenv @ metas) ("not disjoint" ^ c ^ t ^ m ^ p)
255 if check && not (fst (CicReduction.are_convertible
256 ~metasenv context termty ty ugraph)) then (
257 find_matches metasenv context ugraph lift_amount term termty tl
259 let do_match c eq_URI =
260 let subst', metasenv', ugraph' =
261 let t1 = Unix.gettimeofday () in
264 ( Inference.matching metasenv metas context
265 term (S.lift lift_amount c)) ugraph
267 let t2 = Unix.gettimeofday () in
268 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
271 | Inference.MatchingFailure as e ->
272 let t2 = Unix.gettimeofday () in
273 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
275 | CicUtil.Meta_not_found _ as exn -> raise exn
277 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
280 let c, other, eq_URI =
281 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
282 else right, left, Utils.eq_ind_r_URI ()
284 if o <> U.Incomparable then
288 with Inference.MatchingFailure ->
289 find_matches metasenv context ugraph lift_amount term termty tl
291 if Utils.debug_res then ignore (check_res res "find1");
295 try do_match c eq_URI
296 with Inference.MatchingFailure -> None
298 if Utils.debug_res then ignore (check_res res "find2");
300 | Some (_, s, _, _, _) ->
301 let c' = apply_subst s c in
303 let other' = U.guarded_simpl context (apply_subst s other) in *)
304 let other' = apply_subst s other in
305 let order = cmp c' other' in
310 metasenv context ugraph lift_amount term termty tl
312 find_matches metasenv context ugraph lift_amount term termty tl
317 as above, but finds all the matching equalities, and the matching condition
318 can be either Inference.matching or Inference.unification
320 let rec find_all_matches ?(unif_fun=Inference.unification)
321 metasenv context ugraph lift_amount term termty =
322 let module C = Cic in
323 let module U = Utils in
324 let module S = CicSubstitution in
325 let module M = CicMetaSubst in
326 let module HL = HelmLibraryObjects in
327 let cmp = !Utils.compare_terms in
331 let pos, (_, _, (ty, left, right, o), metas) = candidate in
332 let do_match c eq_URI =
333 let subst', metasenv', ugraph' =
334 let t1 = Unix.gettimeofday () in
337 unif_fun metasenv metas context
338 term (S.lift lift_amount c) ugraph in
339 let t2 = Unix.gettimeofday () in
340 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
343 | Inference.MatchingFailure
344 | CicUnification.UnificationFailure _
345 | CicUnification.Uncertain _ as e ->
346 let t2 = Unix.gettimeofday () in
347 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
350 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
353 let c, other, eq_URI =
354 if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
355 else right, left, Utils.eq_ind_r_URI ()
357 if o <> U.Incomparable then
359 let res = do_match c eq_URI in
360 res::(find_all_matches ~unif_fun metasenv context ugraph
361 lift_amount term termty tl)
363 | Inference.MatchingFailure
364 | CicUnification.UnificationFailure _
365 | CicUnification.Uncertain _ ->
366 find_all_matches ~unif_fun metasenv context ugraph
367 lift_amount term termty tl
370 let res = do_match c eq_URI in
373 let c' = apply_subst s c
374 and other' = apply_subst s other in
375 let order = cmp c' other' in
376 if order <> U.Lt && order <> U.Le then
377 res::(find_all_matches ~unif_fun metasenv context ugraph
378 lift_amount term termty tl)
380 find_all_matches ~unif_fun metasenv context ugraph
381 lift_amount term termty tl
383 | Inference.MatchingFailure
384 | CicUnification.UnificationFailure _
385 | CicUnification.Uncertain _ ->
386 find_all_matches ~unif_fun metasenv context ugraph
387 lift_amount term termty tl
392 returns true if target is subsumed by some equality in table
394 let subsumption env table target =
395 let _, _, (ty, left, right, _), tmetas = target in
396 let metasenv, context, ugraph = env in
397 let metasenv = metasenv @ tmetas in
398 let samesubst subst subst' =
399 let tbl = Hashtbl.create (List.length subst) in
400 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
402 (fun (m, (c, t1, t2)) ->
404 let c', t1', t2' = Hashtbl.find tbl m in
405 if (c = c') && (t1 = t1') && (t2 = t2') then true
415 let leftc = get_candidates Matching table left in
416 find_all_matches ~unif_fun:Inference.matching
417 metasenv context ugraph 0 left ty leftc
419 let rec ok what = function
421 | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m)), _))::tl ->
423 let other = if pos = Utils.Left then r else l in
424 let subst', menv', ug' =
425 let t1 = Unix.gettimeofday () in
428 Inference.matching menv m context what other ugraph
430 let t2 = Unix.gettimeofday () in
431 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
433 with Inference.MatchingFailure as e ->
434 let t2 = Unix.gettimeofday () in
435 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
438 if samesubst subst subst' then
442 with Inference.MatchingFailure ->
445 let r, subst = ok right leftr in
454 let rightc = get_candidates Matching table right in
455 find_all_matches ~unif_fun:Inference.matching
456 metasenv context ugraph 0 right ty rightc
463 (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
464 (* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
468 let rec demodulation_aux ?from ?(typecheck=false)
469 metasenv context ugraph table lift_amount term =
470 (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
471 let module C = Cic in
472 let module S = CicSubstitution in
473 let module M = CicMetaSubst in
474 let module HL = HelmLibraryObjects in
476 get_candidates ~env:(metasenv,context,ugraph) Matching table term in
477 (* let candidates = List.map make_variant candidates in *)
484 CicTypeChecker.type_of_aux' metasenv context term ugraph
486 C.Implicit None, ugraph
489 find_matches metasenv context ugraph lift_amount term termty candidates
491 if Utils.debug_res then ignore(check_res res "demod1");
501 (res, tl @ [S.lift 1 t])
504 demodulation_aux ~from:"1" metasenv context ugraph table
508 | None -> (None, tl @ [S.lift 1 t])
509 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
514 | Some (_, subst, menv, ug, eq_found) ->
515 Some (C.Appl ll, subst, menv, ug, eq_found)
517 | C.Prod (nn, s, t) ->
519 demodulation_aux ~from:"2"
520 metasenv context ugraph table lift_amount s in (
524 demodulation_aux metasenv
525 ((Some (nn, C.Decl s))::context) ugraph
526 table (lift_amount+1) t
530 | Some (t', subst, menv, ug, eq_found) ->
531 Some (C.Prod (nn, (S.lift 1 s), t'),
532 subst, menv, ug, eq_found)
534 | Some (s', subst, menv, ug, eq_found) ->
535 Some (C.Prod (nn, s', (S.lift 1 t)),
536 subst, menv, ug, eq_found)
538 | C.Lambda (nn, s, t) ->
541 metasenv context ugraph table lift_amount s in (
545 demodulation_aux metasenv
546 ((Some (nn, C.Decl s))::context) ugraph
547 table (lift_amount+1) t
551 | Some (t', subst, menv, ug, eq_found) ->
552 Some (C.Lambda (nn, (S.lift 1 s), t'),
553 subst, menv, ug, eq_found)
555 | Some (s', subst, menv, ug, eq_found) ->
556 Some (C.Lambda (nn, s', (S.lift 1 t)),
557 subst, menv, ug, eq_found)
562 if Utils.debug_res then ignore(check_res res "demod_aux output");
567 let build_newtarget_time = ref 0.;;
570 let demod_counter = ref 1;;
574 (** demodulation, when target is an equality *)
575 let rec demodulation_equality ?from newmeta env table sign target =
576 let module C = Cic in
577 let module S = CicSubstitution in
578 let module M = CicMetaSubst in
579 let module HL = HelmLibraryObjects in
580 let module U = Utils in
581 let metasenv, context, ugraph = env in
582 let w, proof, (eq_ty, left, right, order), metas = target in
583 (* first, we simplify *)
584 let right = U.guarded_simpl context right in
585 let left = U.guarded_simpl context left in
586 let order = !Utils.compare_terms left right in
587 let stat = (eq_ty, left, right, order) in
588 let w = Utils.compute_equality_weight stat in
589 let target = w, proof, stat, metas in
590 if Utils.debug_metas then
591 ignore(check_target context target "demod equalities input");
592 let metasenv' = (* metasenv @ *) metas in
593 let maxmeta = ref newmeta in
595 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
596 let time1 = Unix.gettimeofday () in
598 if Utils.debug_metas then
600 ignore(check_for_duplicates menv "input1");
601 ignore(check_disjoint_invariant subst menv "input2");
602 let substs = CicMetaSubst.ppsubst subst in
603 ignore(check_target context (snd eq_found) ("input3" ^ substs))
605 let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
607 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
608 with CicUtil.Meta_not_found _ -> ty
610 let what, other = if pos = Utils.Left then what, other else other, what in
611 let newterm, newproof =
612 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
613 let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in
616 let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
617 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
618 S.lift 1 eq_ty; l; r]
620 if sign = Utils.Positive then
622 Inference.ProofBlock (
623 subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
628 CicMkImplicit.identity_relocation_list_for_metavariable context in
629 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
630 (* print_newline (); *)
631 C.Meta (!maxmeta, irl)
636 if pos = Utils.Left then [ty; what; other]
637 else [ty; other; what]
639 Inference.ProofSymBlock (termlist, proof')
642 if pos = Utils.Left then what, other else other, what
644 pos, (0, proof', (ty, other, what, Utils.Incomparable),menv')
648 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
649 eq_found, Inference.BasicProof metaproof)
652 | Inference.BasicProof _ ->
653 (* print_endline "replacing a BasicProof"; *)
655 | Inference.ProofGoalBlock (_, parent_proof) ->
657 (* print_endline "replacing another ProofGoalBlock"; *)
658 Inference.ProofGoalBlock (pb, parent_proof)
662 C.Appl [C.MutConstruct (* reflexivity *)
663 (LibraryObjects.eq_URI (), 0, 1, []);
664 eq_ty; if is_left then right else left]
667 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
669 let newmenv = (* Inference.filter subst *) menv in
671 if Utils.debug_metas then
672 try ignore(CicTypeChecker.type_of_aux'
673 newmenv context (Inference.build_proof_term newproof) ugraph);
676 prerr_endline "sempre lui";
677 prerr_endline (CicMetaSubst.ppsubst subst);
678 prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
679 prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
680 prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
681 prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
682 prerr_endline ("+++++++++++++subst: " ^ (CicMetaSubst.ppsubst subst));
686 let left, right = if is_left then newterm, right else left, newterm in
687 let ordering = !Utils.compare_terms left right in
688 let stat = (eq_ty, left, right, ordering) in
689 let time2 = Unix.gettimeofday () in
690 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
692 let w = Utils.compute_equality_weight stat in
693 (w, newproof, stat,newmenv) in
694 if Utils.debug_metas then
695 ignore(check_target context res "buildnew_target output");
699 let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
700 if Utils.debug_res then check_res res "demod result";
701 let newmeta, newtarget =
704 let newmeta, newtarget = build_newtarget true t in
705 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
706 (Inference.meta_convertibility_eq target newtarget) then
709 demodulation_equality newmeta env table sign newtarget
711 let res = demodulation_aux metasenv' context ugraph table 0 right in
712 if Utils.debug_res then check_res res "demod result 1";
715 let newmeta, newtarget = build_newtarget false t in
716 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
717 (Inference.meta_convertibility_eq target newtarget) then
720 demodulation_equality newmeta env table sign newtarget
724 (* newmeta, newtarget *)
730 Performs the beta expansion of the term "term" w.r.t. "table",
731 i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
734 let rec betaexpand_term metasenv context ugraph table lift_amount term =
735 let module C = Cic in
736 let module S = CicSubstitution in
737 let module M = CicMetaSubst in
738 let module HL = HelmLibraryObjects in
739 let candidates = get_candidates Unification table term in
741 let res, lifted_term =
746 (fun arg (res, lifted_tl) ->
749 let arg_res, lifted_arg =
750 betaexpand_term metasenv context ugraph table
754 (fun (t, s, m, ug, eq_found) ->
755 (Some t)::lifted_tl, s, m, ug, eq_found)
760 (fun (l, s, m, ug, eq_found) ->
761 (Some lifted_arg)::l, s, m, ug, eq_found)
763 (Some lifted_arg)::lifted_tl)
766 (fun (r, s, m, ug, eq_found) ->
767 None::r, s, m, ug, eq_found) res,
773 (fun (l, s, m, ug, eq_found) ->
774 (C.Meta (i, l), s, m, ug, eq_found)) l'
776 e, C.Meta (i, lifted_l)
779 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
781 | C.Prod (nn, s, t) ->
783 betaexpand_term metasenv context ugraph table lift_amount s in
785 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
786 table (lift_amount+1) t in
789 (fun (t, s, m, ug, eq_found) ->
790 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
793 (fun (t, s, m, ug, eq_found) ->
794 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
795 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
797 | C.Lambda (nn, s, t) ->
799 betaexpand_term metasenv context ugraph table lift_amount s in
801 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
802 table (lift_amount+1) t in
805 (fun (t, s, m, ug, eq_found) ->
806 C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
809 (fun (t, s, m, ug, eq_found) ->
810 C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
811 l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
816 (fun arg (res, lifted_tl) ->
817 let arg_res, lifted_arg =
818 betaexpand_term metasenv context ugraph table lift_amount arg
822 (fun (a, s, m, ug, eq_found) ->
823 a::lifted_tl, s, m, ug, eq_found)
828 (fun (r, s, m, ug, eq_found) ->
829 lifted_arg::r, s, m, ug, eq_found)
831 lifted_arg::lifted_tl)
835 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
838 | t -> [], (S.lift lift_amount t)
841 | C.Meta (i, l) -> res, lifted_term
844 C.Implicit None, ugraph
845 (* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
849 metasenv context ugraph lift_amount term termty candidates
855 let sup_l_counter = ref 1;;
859 returns a list of new clauses inferred with a left superposition step
860 the negative equation "target" and one of the positive equations in "table"
862 let superposition_left newmeta (metasenv, context, ugraph) table target =
863 let module C = Cic in
864 let module S = CicSubstitution in
865 let module M = CicMetaSubst in
866 let module HL = HelmLibraryObjects in
867 let module CR = CicReduction in
868 let module U = Utils in
869 let weight, proof, (eq_ty, left, right, ordering), menv = target in
870 if Utils.debug_metas then
871 ignore(check_target context target "superpositionleft");
873 let term = if ordering = U.Gt then left else right in
875 let t1 = Unix.gettimeofday () in
876 let res = betaexpand_term metasenv context ugraph table 0 term in
877 let t2 = Unix.gettimeofday () in
878 beta_expand_time := !beta_expand_time +. (t2 -. t1);
882 let maxmeta = ref newmeta in
883 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
884 (* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
885 let time1 = Unix.gettimeofday () in
887 let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
888 let what, other = if pos = Utils.Left then what, other else other, what in
889 let newgoal, newproof =
890 let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
891 let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
895 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
896 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
897 S.lift 1 eq_ty; l; r]
902 CicMkImplicit.identity_relocation_list_for_metavariable context in
903 C.Meta (!maxmeta, irl)
908 if pos = Utils.Left then [ty; what; other]
909 else [ty; other; what]
911 Inference.ProofSymBlock (termlist, proof')
914 if pos = Utils.Left then what, other else other, what
916 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
920 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
921 Inference.BasicProof metaproof)
924 | Inference.BasicProof _ ->
925 (* debug_print (lazy "replacing a BasicProof"); *)
927 | Inference.ProofGoalBlock (_, parent_proof) ->
928 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
929 Inference.ProofGoalBlock (pb, parent_proof)
933 C.Appl [C.MutConstruct (* reflexivity *)
934 (LibraryObjects.eq_URI (), 0, 1, []);
935 eq_ty; if ordering = U.Gt then right else left]
938 Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
941 if ordering = U.Gt then newgoal, right else left, newgoal in
942 let neworder = !Utils.compare_terms left right in
943 let stat = (eq_ty, left, right, neworder) in
944 let newmenv = (* Inference.filter s *) menv in
945 let time2 = Unix.gettimeofday () in
946 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
948 let w = Utils.compute_equality_weight stat in
949 (w, newproof, stat, newmenv)
952 !maxmeta, List.map build_new expansions
956 let sup_r_counter = ref 1;;
960 returns a list of new clauses inferred with a right superposition step
961 between the positive equation "target" and one in the "table" "newmeta" is
962 the first free meta index, i.e. the first number above the highest meta
963 index: its updated value is also returned
965 let superposition_right newmeta (metasenv, context, ugraph) table target =
966 let module C = Cic in
967 let module S = CicSubstitution in
968 let module M = CicMetaSubst in
969 let module HL = HelmLibraryObjects in
970 let module CR = CicReduction in
971 let module U = Utils in
972 let w, eqproof, (eq_ty, left, right, ordering), newmetas = target in
973 if Utils.debug_metas then
974 ignore (check_target context target "superpositionright");
975 let metasenv' = newmetas in
976 let maxmeta = ref newmeta in
978 let betaexpand_term metasenv context ugraph table d term =
979 let t1 = Unix.gettimeofday () in
980 let res = betaexpand_term metasenv context ugraph table d term in
981 let t2 = Unix.gettimeofday () in
982 beta_expand_time := !beta_expand_time +. (t2 -. t1);
986 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
987 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
991 (fun (_, subst, _, _, _) ->
992 let subst = apply_subst subst in
993 let o = !Utils.compare_terms (subst l) (subst r) in
994 o <> U.Lt && o <> U.Le)
995 (fst (betaexpand_term metasenv' context ugraph table 0 l))
997 (res left right), (res right left)
999 let build_new ordering ((bo, s, m, ug, (eq_found, eq_URI)) as input) =
1000 if Utils.debug_metas then
1001 ignore (check_target context (snd eq_found) "buildnew1" );
1002 let time1 = Unix.gettimeofday () in
1004 let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
1005 let what, other = if pos = Utils.Left then what, other else other, what in
1006 let newgoal, newproof =
1008 let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
1009 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
1013 if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1014 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1015 S.lift 1 eq_ty; l; r]
1018 Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
1020 let newmeta, newequality =
1022 if ordering = U.Gt then newgoal, apply_subst s right
1023 else apply_subst s left, newgoal in
1024 let neworder = !Utils.compare_terms left right in
1025 let newmenv = (* Inference.filter s *) m in
1026 let stat = (eq_ty, left, right, neworder) in
1028 let w = Utils.compute_equality_weight stat in
1029 (w, newproof, stat, newmenv) in
1030 if Utils.debug_metas then
1031 ignore (check_target context eq' "buildnew3");
1032 let newm, eq' = Inference.fix_metas !maxmeta eq' in
1033 if Utils.debug_metas then
1034 ignore (check_target context eq' "buildnew4");
1038 let time2 = Unix.gettimeofday () in
1039 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1040 if Utils.debug_metas then
1041 ignore(check_target context newequality "buildnew2");
1044 let new1 = List.map (build_new U.Gt) res1
1045 and new2 = List.map (build_new U.Lt) res2 in
1046 let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
1048 (List.filter ok (new1 @ new2)))
1052 (** demodulation, when the target is a goal *)
1053 let rec demodulation_goal newmeta env table goal =
1054 let module C = Cic in
1055 let module S = CicSubstitution in
1056 let module M = CicMetaSubst in
1057 let module HL = HelmLibraryObjects in
1058 let metasenv, context, ugraph = env in
1059 let maxmeta = ref newmeta in
1060 let proof, metas, term = goal in
1061 let term = Utils.guarded_simpl (~debug:true) context term in
1062 let goal = proof, metas, term in
1063 let metasenv' = metas in
1065 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1066 let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
1067 let what, other = if pos = Utils.Left then what, other else other, what in
1069 try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
1070 with CicUtil.Meta_not_found _ -> ty
1072 let newterm, newproof =
1073 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1074 let bo' = apply_subst subst t in
1075 let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
1080 CicMkImplicit.identity_relocation_list_for_metavariable context in
1081 (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
1082 C.Meta (!maxmeta, irl)
1087 if pos = Utils.Left then [ty; what; other]
1088 else [ty; other; what]
1090 Inference.ProofSymBlock (termlist, proof')
1093 if pos = Utils.Left then what, other else other, what
1095 pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
1099 Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
1100 eq_found, Inference.BasicProof metaproof)
1102 let rec repl = function
1103 | Inference.NoProof ->
1104 (* debug_print (lazy "replacing a NoProof"); *)
1106 | Inference.BasicProof _ ->
1107 (* debug_print (lazy "replacing a BasicProof"); *)
1109 | Inference.ProofGoalBlock (_, parent_proof) ->
1110 (* debug_print (lazy "replacing another ProofGoalBlock"); *)
1111 Inference.ProofGoalBlock (pb, parent_proof)
1112 | Inference.SubProof (term, meta_index, p) ->
1113 Inference.SubProof (term, meta_index, repl p)
1117 bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
1119 let newmetasenv = (* Inference.filter subst *) menv in
1120 !maxmeta, (newproof, newmetasenv, newterm)
1123 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
1127 let newmeta, newgoal = build_newgoal t in
1128 let _, _, newg = newgoal in
1129 if Inference.meta_convertibility term newg then
1132 demodulation_goal newmeta env table newgoal
1138 (** demodulation, when the target is a theorem *)
1139 let rec demodulation_theorem newmeta env table theorem =
1140 let module C = Cic in
1141 let module S = CicSubstitution in
1142 let module M = CicMetaSubst in
1143 let module HL = HelmLibraryObjects in
1144 let metasenv, context, ugraph = env in
1145 let maxmeta = ref newmeta in
1146 let term, termty, metas = theorem in
1147 let metasenv' = metas in
1149 let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1150 let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
1151 let what, other = if pos = Utils.Left then what, other else other, what in
1152 let newterm, newty =
1153 let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1154 let bo' = apply_subst subst t in
1155 let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1158 Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1159 Inference.BasicProof term)
1161 (Inference.build_proof_term newproof, bo)
1164 let m = Inference.metas_of_term newterm in
1165 !maxmeta, (newterm, newty, menv)
1168 demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1172 let newmeta, newthm = build_newtheorem t in
1173 let newt, newty, _ = newthm in
1174 if Inference.meta_convertibility termty newty then
1177 demodulation_theorem newmeta env table newthm