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
(* $Id: cbv.ml 11897 2009-02-09 19:28:02Z barras $ *)
22
(**** Call by value reduction ****)
24
(* The type of terms with closure. The meaning of the constructors and
25
* the invariants of this datatype are the following:
26
* VAL(k,c) represents the constr c with a delayed shift of k. c must be
27
* in normal form and neutral (i.e. not a lambda, a construct or a
28
* (co)fix, because they may produce redexes by applying them,
29
* or putting them in a case)
30
* LAM(x,a,b,S) is the term [S]([x:a]b). the bindings is propagated
31
* only when the abstraction is applied, and then we use the rule
32
* ([S]([x:a]b) c) --> [S.c]b
33
* This corresponds to the usual strategy of weak reduction
34
* FIXP(op,bd,S,args) is the fixpoint (Fix or Cofix) of bodies bd under
35
* the bindings S, and then applied to args. Here again,
37
* CONSTR(c,args) is the constructor [c] applied to [args].
39
* Note that any term has not an equivalent in cbv_value: for example,
40
* a product (x:A)B must be in normal form because only VAL may
41
* represent it, and the argument of VAL is always in normal
42
* form. This remark precludes coding a head reduction with these
43
* functions. Anyway, does it make sense to head reduce with a
44
* call-by-value strategy ?
48
| LAM of int * (name * constr) list * constr * cbv_value subs
49
| FIXP of fixpoint * cbv_value subs * cbv_value array
50
| COFIXP of cofixpoint * cbv_value subs * cbv_value array
51
| CONSTR of constructor * cbv_value array
53
(* les vars pourraient etre des constr,
54
cela permet de retarder les lift: utile ?? *)
56
(* relocation of a value; used when a value stored in a context is expanded
57
* in a larger context. e.g. [%k (S.t)](k+1) --> [^k]t (t is shifted of k)
59
let rec shift_value n = function
60
| VAL (k,v) -> VAL ((k+n),v)
61
| LAM (nlams,ctxt,b,s) -> LAM (nlams,ctxt,b,subs_shft (n,s))
62
| FIXP (fix,s,args) ->
63
FIXP (fix,subs_shft (n,s), Array.map (shift_value n) args)
64
| COFIXP (cofix,s,args) ->
65
COFIXP (cofix,subs_shft (n,s), Array.map (shift_value n) args)
67
CONSTR (c, Array.map (shift_value n) args)
69
if n = 0 then v else shift_value n v
71
(* Contracts a fixpoint: given a fixpoint and a bindings,
72
* returns the corresponding fixpoint body, and the bindings in which
73
* it should be evaluated: its first variables are the fixpoint bodies
74
* (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1}))
75
* -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti)
77
let contract_fixp env ((reci,i),(_,_,bds as bodies)) =
78
let make_body j = FIXP(((reci,j),bodies), env, [||]) in
79
let n = Array.length bds in
80
subs_cons(Array.init n make_body, env), bds.(i)
82
let contract_cofixp env (i,(_,_,bds as bodies)) =
83
let make_body j = COFIXP((j,bodies), env, [||]) in
84
let n = Array.length bds in
85
subs_cons(Array.init n make_body, env), bds.(i)
87
let make_constr_ref n = function
88
| RelKey p -> mkRel (n+p)
89
| VarKey id -> mkVar id
90
| ConstKey cst -> mkConst cst
93
(* type of terms with a hole. This hole can appear only under App or Case.
94
* TOP means the term is considered without context
95
* APP(v,stk) means the term is applied to v, and then the context stk
96
* (v.0 is the first argument).
97
* this corresponds to the application stack of the KAM.
98
* The members of l are values: we evaluate arguments before
100
* CASE(t,br,pat,S,stk) means the term is in a case (which is himself in stk
101
* t is the type of the case and br are the branches, all of them under
102
* the subs S, pat is information on the patterns of the Case
103
* (Weak reduction: we propagate the sub only when the selected branch
106
* Important remark: the APPs should be collapsed:
107
* (APP (l,(APP ...))) forbidden
112
| APP of cbv_value array * cbv_stack
113
| CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
115
(* Adds an application list. Collapse APPs! *)
116
let stack_app appl stack =
117
if Array.length appl = 0 then stack else
119
| APP(args,stk) -> APP(Array.append appl args,stk)
120
| _ -> APP(appl, stack)
125
let red_set_ref flags = function
126
| RelKey _ -> red_set flags fDELTA
127
| VarKey id -> red_set flags (fVAR id)
128
| ConstKey sp -> red_set flags (fCONST sp)
130
(* Transfer application lists from a value to the stack
131
* useful because fixpoints may be totally applied in several times
133
let strip_appl head stack =
135
| FIXP (fix,env,app) -> (FIXP(fix,env,[||]), stack_app app stack)
136
| COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[||]), stack_app app stack)
137
| CONSTR (c,app) -> (CONSTR(c,[||]), stack_app app stack)
141
(* Tests if fixpoint reduction is possible. *)
142
let fixp_reducible flgs ((reci,i),_) stk =
143
if red_set flgs fIOTA then
146
Array.length appl > reci.(i) &&
147
(match appl.(reci.(i)) with
154
let cofixp_reducible flgs _ stk =
155
if red_set flgs fIOTA then
157
| (CASE _ | APP(_,CASE _)) -> true
163
(* The main recursive functions
165
* Go under applications and cases (pushed in the stack), expand head
166
* constants or substitued de Bruijn, and try to make appear a
167
* constructor, a lambda or a fixp in the head. If not, it is a value
168
* and is completely computed here. The head redexes are NOT reduced:
169
* the function returns the pair of a cbv_value and its stack. *
170
* Invariant: if the result of norm_head is CONSTR or (CO)FIXP, it last
171
* argument is []. Because we must put all the applied terms in the
174
let rec norm_head info env t stack =
175
(* no reduction under binders *)
176
match kind_of_term t with
177
(* stack grows (remove casts) *)
178
| App (head,args) -> (* Applied terms are normalized immediately;
179
they could be computed when getting out of the stack *)
180
let nargs = Array.map (cbv_stack_term info TOP env) args in
181
norm_head info env head (stack_app nargs stack)
182
| Case (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack))
183
| Cast (ct,_,_) -> norm_head info env ct stack
186
* the first pattern is CRUCIAL, n=0 happens very often:
187
* when reducing closed terms, n is always 0 *)
189
(match expand_rel i env with
190
| Inl (0,v) -> strip_appl v stack
191
| Inl (n,v) -> strip_appl (shift_value n v) stack
192
| Inr (n,None) -> (VAL(0, mkRel n), stack)
193
| Inr (n,Some p) -> norm_head_ref (n-p) info env stack (RelKey p))
195
| Var id -> norm_head_ref 0 info env stack (VarKey id)
197
| Const sp -> norm_head_ref 0 info env stack (ConstKey sp)
199
| LetIn (x, b, t, c) ->
200
(* zeta means letin are contracted; delta without zeta means we *)
201
(* allow bindings but leave let's in place *)
202
let zeta = red_set (info_flags info) fZETA in
205
(* New rule: for Cbv, Delta does not apply to locally bound variables
206
or red_set (info_flags info) fDELTA
209
subs_cons ([|cbv_stack_term info TOP env b|],env)
213
norm_head info env' c stack
216
mkLetIn (x, cbv_norm_term info env b,
217
cbv_norm_term info env t,
218
cbv_norm_term info env' c) in
219
(VAL(0,normt), stack) (* Consid�rer une coupure commutative ? *)
222
(match evar_value info ev with
223
Some c -> norm_head info env c stack
224
| None -> (VAL(0, t), stack))
226
(* non-neutral cases *)
228
let ctxt,b = decompose_lam t in
229
(LAM(List.length ctxt, List.rev ctxt,b,env), stack)
230
| Fix fix -> (FIXP(fix,env,[||]), stack)
231
| CoFix cofix -> (COFIXP(cofix,env,[||]), stack)
232
| Construct c -> (CONSTR(c, [||]), stack)
235
| (Sort _ | Meta _ | Ind _) -> (VAL(0, t), stack)
237
(VAL(0, mkProd (x, cbv_norm_term info env t,
238
cbv_norm_term info (subs_lift env) c)),
241
and norm_head_ref k info env stack normt =
242
if red_set_ref (info_flags info) normt then
243
match ref_value_cache info normt with
244
| Some body -> strip_appl (shift_value k body) stack
245
| None -> (VAL(0,make_constr_ref k normt), stack)
246
else (VAL(0,make_constr_ref k normt), stack)
248
(* cbv_stack_term performs weak reduction on constr t under the subs
249
* env, with context stack, i.e. ([env]t stack). First computes weak
250
* head normal form of t and checks if a redex appears with the stack.
251
* If so, recursive call to reach the real head normal form. If not,
254
and cbv_stack_term info stack env t =
255
match norm_head info env t stack with
256
(* a lambda meets an application -> BETA *)
257
| (LAM (nlams,ctxt,b,env), APP (args, stk))
258
when red_set (info_flags info) fBETA ->
259
let nargs = Array.length args in
260
if nargs == nlams then
261
cbv_stack_term info stk (subs_cons(args,env)) b
262
else if nlams < nargs then
263
let env' = subs_cons(Array.sub args 0 nlams, env) in
264
let eargs = Array.sub args nlams (nargs-nlams) in
265
cbv_stack_term info (APP(eargs,stk)) env' b
267
let ctxt' = list_skipn nargs ctxt in
268
LAM(nlams-nargs,ctxt', b, subs_cons(args,env))
270
(* a Fix applied enough -> IOTA *)
271
| (FIXP(fix,env,_), stk)
272
when fixp_reducible (info_flags info) fix stk ->
273
let (envf,redfix) = contract_fixp env fix in
274
cbv_stack_term info stk envf redfix
276
(* constructor guard satisfied or Cofix in a Case -> IOTA *)
277
| (COFIXP(cofix,env,_), stk)
278
when cofixp_reducible (info_flags info) cofix stk->
279
let (envf,redfix) = contract_cofixp env cofix in
280
cbv_stack_term info stk envf redfix
282
(* constructor in a Case -> IOTA *)
283
| (CONSTR((sp,n),_), APP(args,CASE(_,br,ci,env,stk)))
284
when red_set (info_flags info) fIOTA ->
286
Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in
287
cbv_stack_term info (stack_app cargs stk) env br.(n-1)
289
(* constructor of arity 0 in a Case -> IOTA *)
290
| (CONSTR((_,n),_), CASE(_,br,_,env,stk))
291
when red_set (info_flags info) fIOTA ->
292
cbv_stack_term info stk env br.(n-1)
294
(* may be reduced later by application *)
295
| (head, TOP) -> head
296
| (FIXP(fix,env,_), APP(appl,TOP)) -> FIXP(fix,env,appl)
297
| (COFIXP(cofix,env,_), APP(appl,TOP)) -> COFIXP(cofix,env,appl)
298
| (CONSTR(c,_), APP(appl,TOP)) -> CONSTR(c,appl)
300
(* absurd cases (ill-typed) *)
301
| (LAM _, CASE _) -> assert false
303
(* definitely a value *)
304
| (head,stk) -> VAL(0,apply_stack info (cbv_norm_value info head) stk)
307
(* When we are sure t will never produce a redex with its stack, we
308
* normalize (even under binders) the applied terms and we build the
311
and apply_stack info t = function
314
apply_stack info (mkApp(t,Array.map (cbv_norm_value info) args)) st
315
| CASE (ty,br,ci,env,st) ->
317
(mkCase (ci, cbv_norm_term info env ty, t,
318
Array.map (cbv_norm_term info env) br))
322
(* performs the reduction on a constr, and returns a constr *)
323
and cbv_norm_term info env t =
324
(* reduction under binders *)
325
cbv_norm_value info (cbv_stack_term info TOP env t)
327
(* reduction of a cbv_value to a constr *)
328
and cbv_norm_value info = function (* reduction under binders *)
329
| VAL (n,v) -> lift n v
330
| LAM (n,ctxt,b,env) ->
332
list_map_i (fun i (x,ty) ->
333
(x,cbv_norm_term info (subs_liftn i env) ty)) 0 ctxt in
334
compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b)
335
| FIXP ((lij,(names,lty,bds)),env,args) ->
339
Array.map (cbv_norm_term info env) lty,
340
Array.map (cbv_norm_term info
341
(subs_liftn (Array.length lty) env)) bds)),
342
Array.map (cbv_norm_value info) args)
343
| COFIXP ((j,(names,lty,bds)),env,args) ->
346
(names,Array.map (cbv_norm_term info env) lty,
347
Array.map (cbv_norm_term info
348
(subs_liftn (Array.length lty) env)) bds)),
349
Array.map (cbv_norm_value info) args)
351
mkApp(mkConstruct c, Array.map (cbv_norm_value info) args)
354
let cbv_norm infos constr =
355
with_stats (lazy (cbv_norm_term infos (ESID 0) constr))
358
type cbv_infos = cbv_value infos
360
(* constant bodies are normalized at the first expansion *)
361
let create_cbv_infos flgs env sigma =
363
(fun old_info c -> cbv_stack_term old_info TOP (ESID 0) c)
366
(Reductionops.safe_evar_value sigma)
added
removed
pretyping/cbv.ml
