From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- pretyping/cbv.ml | 80 +++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 50 insertions(+), 30 deletions(-) (limited to 'pretyping/cbv.ml') diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 08ec25be..21bbede0 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -1,19 +1,15 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* CONSTR (c, Array.map (shift_value n) args) let shift_value n v = - if n = 0 then v else shift_value n v + if Int.equal n 0 then v else shift_value n v (* Contracts a fixpoint: given a fixpoint and a bindings, * returns the corresponding fixpoint body, and the bindings in which @@ -111,11 +110,11 @@ let contract_cofixp env (i,(_,_,bds as bodies)) = let make_constr_ref n = function | RelKey p -> mkRel (n+p) | VarKey id -> mkVar id - | ConstKey cst -> mkConst cst + | ConstKey cst -> mkConstU cst (* Adds an application list. Collapse APPs! *) let stack_app appl stack = - if Array.length appl = 0 then stack else + if Int.equal (Array.length appl) 0 then stack else match stack with | APP(args,stk) -> APP(Array.append appl args,stk) | _ -> APP(appl, stack) @@ -125,6 +124,7 @@ let rec stack_concat stk1 stk2 = TOP -> stk2 | APP(v,stk1') -> APP(v,stack_concat stk1' stk2) | CASE(c,b,i,s,stk1') -> CASE(c,b,i,s,stack_concat stk1' stk2) + | PROJ (p,pinfo,stk1') -> PROJ (p,pinfo,stack_concat stk1' stk2) (* merge stacks when there is no shifts in between *) let mkSTACK = function @@ -140,7 +140,7 @@ open RedFlags let red_set_ref flags = function | RelKey _ -> red_set flags fDELTA | VarKey id -> red_set flags (fVAR id) - | ConstKey sp -> red_set flags (fCONST sp) + | ConstKey (sp,_) -> red_set flags (fCONST sp) (* Transfer application lists from a value to the stack * useful because fixpoints may be totally applied in several times. @@ -178,9 +178,9 @@ let cofixp_reducible flgs _ stk = (* The main recursive functions * - * Go under applications and cases (pushed in the stack), expand head - * constants or substitued de Bruijn, and try to make appear a - * constructor, a lambda or a fixp in the head. If not, it is a value + * Go under applications and cases/projections (pushed in the stack), + * expand head constants or substitued de Bruijn, and try to a make a + * constructor, a lambda or a fixp appear in the head. If not, it is a value * and is completely computed here. The head redexes are NOT reduced: * the function returns the pair of a cbv_value and its stack. * * Invariant: if the result of norm_head is CONSTR or (CO)FIXP, it last @@ -197,7 +197,17 @@ let rec norm_head info env t stack = norm_head info env head (stack_app nargs stack) | Case (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack)) | Cast (ct,_,_) -> norm_head info env ct stack - + + | Proj (p, c) -> + let p' = + if red_set (info_flags info) (fCONST (Projection.constant p)) + && red_set (info_flags info) fBETA + then Projection.unfold p + else p + in + let pinfo = Environ.lookup_projection p (info_env info) in + norm_head info env c (PROJ (p', pinfo, stack)) + (* constants, axioms * the first pattern is CRUCIAL, n=0 happens very often: * when reducing closed terms, n is always 0 *) @@ -222,10 +232,10 @@ let rec norm_head info env t stack = let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in norm_head info env' c stack else - (CBN(t,env), stack) (* Considérer une coupure commutative ? *) + (CBN(t,env), stack) (* Should we consider a commutative cut ? *) | Evar ev -> - (match evar_value info ev with + (match evar_value info.i_cache ev with Some c -> norm_head info env c stack | None -> (VAL(0, t), stack)) @@ -255,19 +265,21 @@ and norm_head_ref k info env stack normt = * we build a value. *) and cbv_stack_term info stack env t = - match norm_head info env t stack with - (* a lambda meets an application -> BETA *) - | (LAM (nlams,ctxt,b,env), APP (args, stk)) + cbv_stack_value info env (norm_head info env t stack) + +and cbv_stack_value info env = function + (* a lambda meets an application -> BETA *) + | (LAM (nlams,ctxt,b,env), APP (args, stk)) when red_set (info_flags info) fBETA -> - let nargs = Array.length args in - if nargs == nlams then + let nargs = Array.length args in + if nargs == nlams then cbv_stack_term info stk (subs_cons(args,env)) b else if nlams < nargs then let env' = subs_cons(Array.sub args 0 nlams, env) in let eargs = Array.sub args nlams (nargs-nlams) in cbv_stack_term info (APP(eargs,stk)) env' b else - let ctxt' = list_skipn nargs ctxt in + let ctxt' = List.skipn nargs ctxt in LAM(nlams-nargs,ctxt', b, subs_cons(args,env)) (* a Fix applied enough -> IOTA *) @@ -283,22 +295,28 @@ and cbv_stack_term info stack env t = cbv_stack_term info stk envf redfix (* constructor in a Case -> IOTA *) - | (CONSTR((sp,n),[||]), APP(args,CASE(_,br,ci,env,stk))) + | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk))) when red_set (info_flags info) fIOTA -> let cargs = Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in cbv_stack_term info (stack_app cargs stk) env br.(n-1) (* constructor of arity 0 in a Case -> IOTA *) - | (CONSTR((_,n),[||]), CASE(_,br,_,env,stk)) + | (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk)) when red_set (info_flags info) fIOTA -> cbv_stack_term info stk env br.(n-1) + (* constructor in a Projection -> IOTA *) + | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk))) + when red_set (info_flags info) fIOTA && Projection.unfolded p -> + let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in + cbv_stack_value info env (arg, stk) + (* may be reduced later by application *) | (FIXP(fix,env,[||]), APP(appl,TOP)) -> FIXP(fix,env,appl) | (COFIXP(cofix,env,[||]), APP(appl,TOP)) -> COFIXP(cofix,env,appl) | (CONSTR(c,[||]), APP(appl,TOP)) -> CONSTR(c,appl) - + (* definitely a value *) | (head,stk) -> mkSTACK(head, stk) @@ -316,6 +334,8 @@ let rec apply_stack info t = function (mkCase (ci, cbv_norm_term info env ty, t, Array.map (cbv_norm_term info env) br)) st + | PROJ (p, pinfo, st) -> + apply_stack info (mkProj (p, t)) st (* performs the reduction on a constr, and returns a constr *) and cbv_norm_term info env t = @@ -333,7 +353,7 @@ and cbv_norm_value info = function (* reduction under binders *) map_constr_with_binders subs_lift (cbv_norm_term info) env t | LAM (n,ctxt,b,env) -> let nctxt = - list_map_i (fun i (x,ty) -> + List.map_i (fun i (x,ty) -> (x,cbv_norm_term info (subs_liftn i env) ty)) 0 ctxt in compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b) | FIXP ((lij,(names,lty,bds)),env,args) -> @@ -352,7 +372,7 @@ and cbv_norm_value info = function (* reduction under binders *) (subs_liftn (Array.length lty) env)) bds)), Array.map (cbv_norm_value info) args) | CONSTR (c,args) -> - mkApp(mkConstruct c, Array.map (cbv_norm_value info) args) + mkApp(mkConstructU c, Array.map (cbv_norm_value info) args) (* with profiling *) let cbv_norm infos constr = -- cgit v1.2.3