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://helm.cs.unibo.it/
26 let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 ;;
28 let compose_core t2 t1 (proof, goal) =
29 let _,metasenv,_subst,_,_,_ = proof in
30 let _,context,_ = CicUtil.lookup_meta goal metasenv in
32 CicTypeChecker.type_of_aux' metasenv context t1 CicUniv.oblivion_ugraph
35 CicTypeChecker.type_of_aux' metasenv context t2 CicUniv.oblivion_ugraph
37 let saturated_ty2, menv_for_saturated_ty2 =
38 let maxm = CicMkImplicit.new_meta metasenv [] in
39 let ty2, menv, _, _ = TermUtil.saturate_term maxm metasenv context ty2 0 in
42 (* unifies t with saturated_ty2 and gives back a fresh meta of type t *)
45 let n = CicMkImplicit.new_meta menv [] in
47 CicMkImplicit.identity_relocation_list_for_metavariable context
49 Cic.Meta (n,irl), ((n,context,t)::menv)
53 CicUnification.fo_unif menv context t saturated_ty2
54 CicUniv.oblivion_ugraph
58 | CicUnification.UnificationFailure _
59 | CicUnification.Uncertain _ -> false, menv2, m
61 (* check which "positions" in the input arrow unifies with saturated_ty2 *)
62 let rec positions menv cur arity = function
64 let b, newmenv, sb = unif menv s in
67 (positions newmenv (cur + 1) arity (CicSubstitution.subst sb t))
69 positions newmenv (cur + 1) arity (CicSubstitution.subst sb t)
72 (* position is a list of arities, that is if t1 : a -> b -> c and arity is
73 * 0 then the computed term will be (t1 ? t2) of type a -> c
74 * if arity is 1 then (t1 t2 ?) of type b -> c *)
75 let rec generate positions menv acc =
81 CloseCoercionGraph.generate_composite t2 t1 context menv
82 CicUniv.oblivion_ugraph arity false
84 assert (List.length menv1 = List.length menv);
85 generate tl menv (t::acc)
87 | CloseCoercionGraph.UnableToCompose -> generate tl menv acc
90 generate (positions menv_for_saturated_ty2 0 (count_pi ty1) ty1) metasenv []
92 (* the new proof has the resulting metasenv (shouldn't it be the same?) *)
94 let uri, _, _subst, bo, ty, attrs = proof in
95 uri, metasenv, _subst, bo, ty, attrs
97 (* now we have the terms, we generalize them and intros them *)
100 (fun (proof,goal) t ->
102 ProofEngineTypes.const_lazy_term t
105 ProofEngineTypes.apply_tactic
106 (VariousTactics.generalize_tac (Some (lazy_of t), [], None))
109 assert(List.length gl = 1);
113 (proof, goal), List.length terms
116 let compose_tac ?howmany ?mk_fresh_name_callback n t1 t2 proofstatus =
117 let ((proof, goal), k), n =
119 | Some t2 -> compose_core t1 t2 proofstatus, n-1
122 let proof, goal = proofstatus in
123 let _,metasenv,subst,_,_,_ = proof in
124 let _,_,ty = CicUtil.lookup_meta goal metasenv in
125 count_pi (CicMetaSubst.apply_subst subst ty)
129 let (proof, goal), k =
130 (* fix iterates n times the composition *)
131 let rec fix proofstatus k t = function
132 | 0 -> proofstatus, k
134 let t = CicSubstitution.lift k t in
136 ProofEngineTypes.apply_tactic
137 (PrimitiveTactics.intros_tac
138 ~howmany:k ?mk_fresh_name_callback ()) proofstatus
140 assert (List.length gl = 1);
141 let goal = List.hd gl in
143 (* aux compose t with every previous result *)
144 let rec aux k proofstatus = function
145 | 0 -> k, proofstatus
147 let (proof, goal), k1 =
148 compose_core t (Cic.Rel n) proofstatus
150 aux (k+k1) (proof, goal) (n-1)
152 aux 0 (proof, goal) k
154 fix proofstatus k t (n-1)
156 fix (proof, goal) k t1 n
162 if i - k < 0 then (* we should generalize back and clear *) Some 0
165 ProofEngineTypes.apply_tactic
166 (PrimitiveTactics.intros_tac ?howmany ?mk_fresh_name_callback ())
170 let compose_tac ?howmany ?mk_fresh_name_callback times t1 t2 =
171 ProofEngineTypes.mk_tactic
172 (compose_tac ?howmany ?mk_fresh_name_callback times t1 t2)