1 (* Copyright (C) 2000, 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 exception ReferenceToVariable;;
27 exception RferenceToCurrentProof;;
28 exception ReferenceToInductiveDefinition;;
30 let rec fix_lambdas_wrt_type ty te =
32 let module S = CicSubstitution in
33 (* prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te);
35 (* cast e altra porcheria ???? *)
37 C.Prod (_,_,ty'), C.Lambda (n,s,te') ->
38 C.Lambda (n,s,fix_lambdas_wrt_type ty' te')
39 | C.Prod (_,s,ty'), C.Appl l ->
40 prerr_endline ("******** fl - eta expansion 1: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te);
42 let l' = List.map (S.lift 1) l in
43 C.Lambda (C.Name "x",s,
44 fix_lambdas_wrt_type ty' (C.Appl (l'@[C.Rel 1])))
45 | C.Prod (_,s,ty'), _ ->
46 prerr_endline ("******** fl - eta expansion 2: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te);
48 let te' = S.lift 1 te in
49 C.Lambda (C.Name "x",s,
50 fix_lambdas_wrt_type ty' (C.Appl [te';C.Rel 1]))
54 let fix_according_to_type ty hd tl =
56 let module S = CicSubstitution in
57 let rec aux ty tl res =
58 (* prerr_endline ("entering aux_1 with type=" ^ CicPp.ppterm ty);
69 prerr_endline ("******* fat - too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res));
72 (C.Name "H", C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
73 | C.Cast (v,t) -> aux v tl res
77 prerr_endline ("******* fat - eta expansion: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res));
79 let res' = List.map (S.lift 1) res
82 (C.Name "x", (* Andrea: to do: generate a fresh name *)
84 aux t [] (res'@[C.Rel 1]))
86 let hd' = fix_lambdas_wrt_type s hd
88 aux (S.subst hd' t) tl' (res@[hd']))
89 | C.Lambda _ -> assert false
90 | C.LetIn (n,s,t) -> aux (S.subst s t) tl res
97 | C.CoFix _ -> (* ???? *)
100 | _ -> (* Andrea: to do: generate a fresh name *)
104 C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
109 let eta_fix metasenv t =
111 (* prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t);
113 let module C = Cic in
116 | C.Var (uri,exp_named_subst) ->
117 let exp_named_subst' =
119 (function i,t -> i, (eta_fix' t)) exp_named_subst
121 C.Var (uri,exp_named_subst')
123 let (_,canonical_context,_) =
124 List.find (function (m,_,_) -> n = m) metasenv
131 | _, Some t -> Some (eta_fix' t)
132 | Some _, None -> assert false (* due to typing rules *))
136 | C.Sort s -> C.Sort s
137 | C.Implicit -> C.Implicit
138 | C.Cast (v,t) -> C.Cast (eta_fix' v, eta_fix' t)
139 | C.Prod (n,s,t) -> C.Prod (n, eta_fix' s, eta_fix' t)
140 | C.Lambda (n,s,t) -> C.Lambda (n, eta_fix' s, eta_fix' t)
141 | C.LetIn (n,s,t) -> C.LetIn (n, eta_fix' s, eta_fix' t)
143 let l' = List.map eta_fix' l
146 C.Const(uri,exp_named_subst)::l'' ->
148 (match CicEnvironment.get_obj uri with
149 C.Constant (_,_,ty,_) -> ty
150 | C.Variable _ -> raise ReferenceToVariable
151 | C.CurrentProof (_,_,_,_,params) -> raise RferenceToCurrentProof
152 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
155 fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l''
157 | C.Const (uri,exp_named_subst) ->
158 let exp_named_subst' =
160 (function i,t -> i, (eta_fix' t)) exp_named_subst
162 C.Const (uri,exp_named_subst')
163 | C.MutInd (uri,tyno,exp_named_subst) ->
164 let exp_named_subst' =
166 (function i,t -> i, (eta_fix' t)) exp_named_subst
168 C.MutInd (uri, tyno, exp_named_subst')
169 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
170 let exp_named_subst' =
172 (function i,t -> i, (eta_fix' t)) exp_named_subst
174 C.MutConstruct (uri, tyno, consno, exp_named_subst')
175 | C.MutCase (uri, tyno, outty, term, patterns) ->
176 C.MutCase (uri, tyno, eta_fix' outty,
177 eta_fix' term, List.map eta_fix' patterns)
178 | C.Fix (funno, funs) ->
181 (fun (name, no, ty, bo) ->
182 (name, no, eta_fix' ty, eta_fix' bo)) funs)
183 | C.CoFix (funno, funs) ->
186 (fun (name, ty, bo) ->
187 (name, eta_fix' ty, eta_fix' bo)) funs)