diff options
Diffstat (limited to 'pretyping/cbv.ml')
| -rw-r--r-- | pretyping/cbv.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index cb0fc32575..da6e26cc4b 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -71,7 +71,7 @@ and cbv_stack = | TOP | APP of cbv_value array * cbv_stack | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack - | PROJ of Projection.t * Declarations.projection_body * cbv_stack + | PROJ of Projection.t * cbv_stack (* les vars pourraient etre des constr, cela permet de retarder les lift: utile ?? *) @@ -126,7 +126,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) + | PROJ (p,stk1') -> PROJ (p,stack_concat stk1' stk2) (* merge stacks when there is no shifts in between *) let mkSTACK = function @@ -200,7 +200,7 @@ let rec reify_stack t = function reify_stack (mkCase (ci, ty, t,br)) st - | PROJ (p, pinfo, st) -> + | PROJ (p, st) -> reify_stack (mkProj (p, t)) st and reify_value = function (* reduction under binders *) @@ -265,8 +265,7 @@ let rec norm_head info env t stack = then Projection.unfold p else p in - let pinfo = Environ.lookup_projection p (info_env info.infos) in - norm_head info env c (PROJ (p', pinfo, stack)) + norm_head info env c (PROJ (p', stack)) (* constants, axioms * the first pattern is CRUCIAL, n=0 happens very often: @@ -281,8 +280,9 @@ let rec norm_head info env t stack = | Var id -> norm_head_ref 0 info env stack (VarKey id) | Const sp -> - Reductionops.reduction_effect_hook (env_of_infos info.infos) info.sigma t (lazy (reify_stack t stack)); - norm_head_ref 0 info env stack (ConstKey sp) + Reductionops.reduction_effect_hook (env_of_infos info.infos) info.sigma + (fst sp) (lazy (reify_stack t stack)); + norm_head_ref 0 info env stack (ConstKey sp) | LetIn (_, b, _, c) -> (* zeta means letin are contracted; delta without zeta means we *) @@ -380,9 +380,9 @@ and cbv_stack_value info env = function cbv_stack_term info stk env br.(n-1) (* constructor in a Projection -> IOTA *) - | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk))) + | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,stk))) when red_set (info_flags info.infos) fMATCH && Projection.unfolded p -> - let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in + let arg = args.(Projection.npars p + Projection.arg p) in cbv_stack_value info env (strip_appl arg stk) (* may be reduced later by application *) @@ -407,7 +407,7 @@ 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) -> + | PROJ (p, st) -> apply_stack info (mkProj (p, t)) st (* performs the reduction on a constr, and returns a constr *) |