1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: vnorm.ml 11424 2008-09-30 12:10:28Z jforest $ i*)
19
(*******************************************)
20
(* Calcul de la forme normal d'un terme *)
21
(*******************************************)
23
let crazy_type = mkSet
25
let decompose_prod env t =
26
let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in
27
if name = Anonymous then (Name (id_of_string "x"),dom,codom)
30
exception Find_at of int
32
(* rend le numero du constructeur correspondant au tag [tag],
33
[cst] = true si c'est un constructeur constant *)
35
let invert_tag cst tag reloc_tbl =
37
for j = 0 to Array.length reloc_tbl - 1 do
38
let tagj,arity = reloc_tbl.(j) in
39
if tag = tagj && (cst && arity = 0 || not(cst || arity = 0)) then
43
with Find_at j -> (j+1)
44
(* Argggg, ces constructeurs de ... qui commencent a 1*)
46
let find_rectype_a env c =
48
let t = whd_betadeltaiota env c in
49
try destApp t with _ -> (t,[||]) in
50
match kind_of_term t with
52
| _ -> raise Not_found
54
(* Instantiate inductives and parameters in constructor type *)
56
let type_constructor mind mib typ params =
57
let s = ind_subst mind mib in
58
let ctyp = substl s typ in
59
let nparams = Array.length params in
60
if nparams = 0 then ctyp
62
let _,ctyp = decompose_prod_n nparams ctyp in
63
substl (List.rev (Array.to_list params)) ctyp
67
let construct_of_constr const env tag typ =
68
let (mind,_ as ind), allargs = find_rectype_a env typ in
69
(* spiwack : here be a branch for specific decompilation handled by retroknowledge *)
72
((retroknowledge Retroknowledge.get_vm_decompile_constant_info env (Ind ind) tag),
73
typ) (*spiwack: this may need to be changed in case there are parameters in the
74
type which may cause a constant value to have an arity.
75
(type_constructor seems to be all about parameters actually)
76
but it shouldn't really matter since constant values don't use
77
their ctyp in the rest of the code.*)
79
raise Not_found (* No retroknowledge function (yet) for block decompilation *)
81
let mib,mip = lookup_mind_specif env ind in
82
let nparams = mib.mind_nparams in
83
let i = invert_tag const tag mip.mind_reloc_tbl in
84
let params = Array.sub allargs 0 nparams in
85
let ctyp = type_constructor mind mib (mip.mind_nf_lc.(i-1)) params in
86
(mkApp(mkConstruct(ind,i), params), ctyp)
88
let construct_of_constr_const env tag typ =
89
fst (construct_of_constr true env tag typ)
91
let construct_of_constr_block = construct_of_constr false
93
let constr_type_of_idkey env idkey =
96
mkConst cst, Typeops.type_of_constant env cst
98
let (_,_,ty) = lookup_named id env in
101
let n = (nb_rel env - i) in
102
let (_,_,ty) = lookup_rel n env in
105
let type_of_ind env ind =
106
type_of_inductive env (Inductive.lookup_mind_specif env ind)
108
let build_branches_type env (mind,_ as _ind) mib mip params dep p =
109
let rtbl = mip.mind_reloc_tbl in
110
(* [build_one_branch i cty] construit le type de la ieme branche (commence
111
a 0) et les lambda correspondant aux realargs *)
112
let build_one_branch i cty =
113
let typi = type_constructor mind mib cty params in
114
let decl,indapp = Term.decompose_prod typi in
115
let ind,cargs = find_rectype_a env indapp in
116
let nparams = Array.length params in
117
let carity = snd (rtbl.(i)) in
118
let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in
120
let papp = mkApp(p,crealargs) in
122
let cstr = ith_constructor_of_inductive ind (i+1) in
123
let relargs = Array.init carity (fun i -> mkRel (carity-i)) in
124
let dep_cstr = mkApp(mkApp(mkConstruct cstr,params),relargs) in
125
mkApp(papp,[|dep_cstr|])
129
in Array.mapi build_one_branch mip.mind_nf_lc
131
let build_case_type dep p realargs c =
132
if dep then mkApp(mkApp(p, realargs), [|c|])
133
else mkApp(p, realargs)
135
(* La fonction de normalisation *)
137
let rec nf_val env v t = nf_whd env (whd_val v) t
139
and nf_vtype env v = nf_val env v crazy_type
141
and nf_whd env whd typ =
143
| Vsort s -> mkSort s
145
let dom = nf_vtype env (dom p) in
146
let name = Name (id_of_string "x") in
147
let vc = body_of_vfun (nb_rel env) (codom p) in
148
let codom = nf_vtype (push_rel (name,None,dom) env) vc in
149
mkProd(name,dom,codom)
150
| Vfun f -> nf_fun env f typ
151
| Vfix(f,None) -> nf_fix env f
152
| Vfix(f,Some vargs) -> fst (nf_fix_app env f vargs)
153
| Vcofix(cf,_,None) -> nf_cofix env cf
154
| Vcofix(cf,_,Some vargs) ->
155
let cfd = nf_cofix env cf in
156
let i,(_,ta,_) = destCoFix cfd in
158
let _, args = nf_args env vargs t in
160
| Vconstr_const n -> construct_of_constr_const env n typ
162
let capp,ctyp = construct_of_constr_block env (btag b) typ in
163
let args = nf_bargs env b ctyp in
165
| Vatom_stk(Aid idkey, stk) ->
166
let c,typ = constr_type_of_idkey env idkey in
168
| Vatom_stk(Aiddef(idkey,v), stk) ->
169
nf_whd env (whd_stack v stk) typ
170
| Vatom_stk(Aind ind, stk) ->
171
nf_stk env (mkInd ind) (type_of_ind env ind) stk
173
and nf_stk env c t stk =
176
| Zapp vargs :: stk ->
177
let t, args = nf_args env vargs t in
178
nf_stk env (mkApp(c,args)) t stk
179
| Zfix (f,vargs) :: stk ->
180
let fa, typ = nf_fix_app env f vargs in
181
let _,_,codom = try decompose_prod env typ with _ -> exit 120 in
182
nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk
183
| Zswitch sw :: stk ->
184
let (mind,_ as ind),allargs = find_rectype_a env t in
185
let (mib,mip) = Inductive.lookup_mind_specif env ind in
186
let nparams = mib.mind_nparams in
187
let params,realargs = Util.array_chop nparams allargs in
189
hnf_prod_applist env (type_of_ind env ind) (Array.to_list params) in
190
let pT = whd_betadeltaiota env pT in
191
let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in
192
(* Calcul du type des branches *)
193
let btypes = build_branches_type env ind mib mip params dep p in
194
(* calcul des branches *)
195
let bsw = branch_of_switch (nb_rel env) sw in
196
let mkbranch i (n,v) =
197
let decl,codom = btypes.(i) in
200
(fun (name,t) env -> push_rel (name,None,t) env) decl env in
201
let b = nf_val env v codom in
204
let branchs = Array.mapi mkbranch bsw in
205
let tcase = build_case_type dep p realargs c in
206
let ci = case_info sw in
207
nf_stk env (mkCase(ci, p, c, branchs)) tcase stk
209
and nf_predicate env ind mip params v pT =
210
match whd_val v, kind_of_term pT with
212
let k = nb_rel env in
213
let vb = body_of_vfun k f in
214
let name,dom,codom = try decompose_prod env pT with _ -> exit 121 in
216
nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in
217
dep, mkLambda(name,dom,body)
219
let k = nb_rel env in
220
let vb = body_of_vfun k f in
221
let name = Name (id_of_string "c") in
222
let n = mip.mind_nrealargs in
223
let rargs = Array.init n (fun i -> mkRel (n-i)) in
224
let params = if n=0 then params else Array.map (lift n) params in
225
let dom = mkApp(mkInd ind,Array.append params rargs) in
226
let body = nf_vtype (push_rel (name,None,dom) env) vb in
227
true, mkLambda(name,dom,body)
228
| _, _ -> false, nf_val env v crazy_type
230
and nf_args env vargs t =
232
let len = nargs vargs in
236
let _,dom,codom = try decompose_prod env !t with _ -> exit 123 in
237
let c = nf_val env (arg vargs i) dom in
238
t := subst1 c codom; c) in
241
and nf_bargs env b t =
247
let _,dom,codom = try decompose_prod env !t with _ -> exit 124 in
248
let c = nf_val env (bfield b i) dom in
249
t := subst1 c codom; c) in
252
and nf_fun env f typ =
253
let k = nb_rel env in
254
let vb = body_of_vfun k f in
256
try decompose_prod env typ
258
raise (Type_errors.TypeError(env,Type_errors.ReferenceVariables typ))
260
let body = nf_val (push_rel (name,None,dom) env) vb codom in
261
mkLambda(name,dom,body)
264
let init = current_fix f in
265
let rec_args = rec_args f in
266
let k = nb_rel env in
267
let vb, vt = reduce_fix k f in
268
let ndef = Array.length vt in
269
let ft = Array.map (fun v -> nf_val env v crazy_type) vt in
270
let name = Array.init ndef (fun _ -> (Name (id_of_string "Ffix"))) in
271
let env = push_rec_types (name,ft,ft) env in
272
let fb = Util.array_map2 (fun v t -> nf_fun env v t) vb ft in
273
mkFix ((rec_args,init),(name,ft,fb))
275
and nf_fix_app env f vargs =
276
let fd = nf_fix env f in
277
let (_,i),(_,ta,_) = destFix fd in
279
let t, args = nf_args env vargs t in
282
and nf_cofix env cf =
283
let init = current_cofix cf in
284
let k = nb_rel env in
285
let vb,vt = reduce_cofix k cf in
286
let ndef = Array.length vt in
287
let cft = Array.map (fun v -> nf_val env v crazy_type) vt in
288
let name = Array.init ndef (fun _ -> (Name (id_of_string "Fcofix"))) in
289
let env = push_rec_types (name,cft,cft) env in
290
let cfb = Util.array_map2 (fun v t -> nf_val env v t) vb cft in
291
mkCoFix (init,(name,cft,cfb))
294
let transp = transp_values () in
295
if not transp then set_transp_values true;
296
let v = Vconv.val_of_constr env c in
297
let c = nf_val env v t in
298
if not transp then set_transp_values false;
added
removed
pretyping/vnorm.ml
