diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cbv.ml | 68 |
1 files changed, 45 insertions, 23 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 265909980b..5061aeff88 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -134,7 +134,12 @@ let mkSTACK = function | STACK(0,v0,stk0), stk -> STACK(0,v0,stack_concat stk0 stk) | v,stk -> STACK(0,v,stk) -type cbv_infos = { tab : cbv_value infos_tab; infos : cbv_value infos; sigma : Evd.evar_map } +type cbv_infos = { + env : Environ.env; + tab : cbv_value KeyTable.t; + reds : RedFlags.reds; + sigma : Evd.evar_map +} (* Change: zeta reduction cannot be avoided in CBV *) @@ -260,8 +265,8 @@ let rec norm_head info env t stack = | Proj (p, c) -> let p' = - if red_set (info_flags info.infos) (fCONST (Projection.constant p)) - && red_set (info_flags info.infos) fBETA + if red_set info.reds (fCONST (Projection.constant p)) + && red_set info.reds fBETA then Projection.unfold p else p in @@ -280,16 +285,16 @@ 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 + Reductionops.reduction_effect_hook info.env 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 *) (* allow bindings but leave let's in place *) - if red_set (info_flags info.infos) fZETA then + if red_set info.reds fZETA then (* New rule: for Cbv, Delta does not apply to locally bound variables - or red_set (info_flags info.infos) fDELTA + or red_set info.reds fDELTA *) let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in norm_head info env' c stack @@ -297,7 +302,7 @@ let rec norm_head info env t stack = (CBN(t,env), stack) (* Should we consider a commutative cut ? *) | Evar ev -> - (match evar_value info.infos.i_cache ev with + (match Reductionops.safe_evar_value info.sigma ev with Some c -> norm_head info env c stack | None -> let e, xs = ev in @@ -317,8 +322,8 @@ let rec norm_head info env t stack = | Prod _ -> (CBN(t,env), stack) and norm_head_ref k info env stack normt = - if red_set_ref (info_flags info.infos) normt then - match ref_value_cache info.infos info.tab normt with + if red_set_ref info.reds normt then + match cbv_value_cache info normt with | Some body -> if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); strip_appl (shift_value k body) stack @@ -343,7 +348,7 @@ and cbv_stack_term info stack env t = 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.infos) fBETA -> + when red_set info.reds fBETA -> let nargs = Array.length args in if nargs == nlams then cbv_stack_term info stk (subs_cons(args,env)) b @@ -357,31 +362,31 @@ and cbv_stack_value info env = function (* a Fix applied enough -> IOTA *) | (FIXP(fix,env,[||]), stk) - when fixp_reducible (info_flags info.infos) fix stk -> + when fixp_reducible info.reds fix stk -> let (envf,redfix) = contract_fixp env fix in cbv_stack_term info stk envf redfix (* constructor guard satisfied or Cofix in a Case -> IOTA *) | (COFIXP(cofix,env,[||]), stk) - when cofixp_reducible (info_flags info.infos) cofix stk-> + when cofixp_reducible info.reds cofix stk-> let (envf,redfix) = contract_cofixp env cofix in cbv_stack_term info stk envf redfix (* constructor in a Case -> IOTA *) | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk))) - when red_set (info_flags info.infos) fMATCH -> + when red_set info.reds fMATCH -> 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),u),[||]), CASE(_,br,_,env,stk)) - when red_set (info_flags info.infos) fMATCH -> + when red_set info.reds fMATCH -> cbv_stack_term info stk env br.(n-1) (* constructor in a Projection -> IOTA *) | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,stk))) - when red_set (info_flags info.infos) fMATCH && Projection.unfolded p -> + when red_set info.reds fMATCH && Projection.unfolded p -> let arg = args.(Projection.npars p + Projection.arg p) in cbv_stack_value info env (strip_appl arg stk) @@ -393,6 +398,29 @@ and cbv_stack_value info env = function (* definitely a value *) | (head,stk) -> mkSTACK(head, stk) +and cbv_value_cache info ref = match KeyTable.find info.tab ref with +| v -> Some v +| exception Not_found -> + try + let body = match ref with + | RelKey n -> + let open Context.Rel.Declaration in + begin match Environ.lookup_rel n info.env with + | LocalDef (_, c, _) -> lift n c + | LocalAssum _ -> raise Not_found + end + | VarKey id -> + let open Context.Named.Declaration in + begin match Environ.lookup_named id info.env with + | LocalDef (_, c, _) -> c + | LocalAssum _ -> raise Not_found + end + | ConstKey cst -> Environ.constant_value_in info.env cst + in + let v = cbv_stack_term info TOP (subs_id 0) body in + let () = KeyTable.add info.tab ref v in + Some v + with Not_found | Environ.NotEvaluableConst _ -> None (* When we are sure t will never produce a redex with its stack, we * normalize (even under binders) the applied terms and we build the @@ -453,11 +481,5 @@ let cbv_norm infos constr = EConstr.of_constr (with_stats (lazy (cbv_norm_term infos (subs_id 0) constr))) (* constant bodies are normalized at the first expansion *) -let create_cbv_infos flgs env sigma = - let infos = create - ~share:true (** Not used by cbv *) - ~repr:(fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c) - flgs - env - (Reductionops.safe_evar_value sigma) in - { tab = CClosure.create_tab (); infos; sigma } +let create_cbv_infos reds env sigma = + { tab = KeyTable.create 91; reds; env; sigma } |