diff options
Diffstat (limited to 'pretyping/cbv.ml')
-rw-r--r-- | pretyping/cbv.ml | 149 |
1 files changed, 111 insertions, 38 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 84bf849e..cb0fc325 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -1,14 +1,16 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util open Names -open Term +open Constr open Vars open CClosure open Esubst @@ -45,7 +47,7 @@ type cbv_value = | LAM of int * (Name.t * constr) list * constr * cbv_value subs | FIXP of fixpoint * cbv_value subs * cbv_value array | COFIXP of cofixpoint * cbv_value subs * cbv_value array - | CONSTR of constructor puniverses * cbv_value array + | CONSTR of constructor Univ.puniverses * cbv_value array (* type of terms with a hole. This hole can appear only under App or Case. * TOP means the term is considered without context @@ -69,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 * Declarations.projection_body * cbv_stack + | PROJ of Projection.t * Declarations.projection_body * cbv_stack (* les vars pourraient etre des constr, cela permet de retarder les lift: utile ?? *) @@ -132,6 +134,7 @@ 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 } (* Change: zeta reduction cannot be avoided in CBV *) @@ -170,11 +173,68 @@ let fixp_reducible flgs ((reci,i),_) stk = let cofixp_reducible flgs _ stk = if red_set flgs fCOFIX then match stk with - | (CASE _ | APP(_,CASE _)) -> true + | (CASE _ | PROJ _ | APP(_,CASE _) | APP(_,PROJ _)) -> true | _ -> false else false +let debug_cbv = ref false +let _ = Goptions.declare_bool_option { + Goptions.optdepr = false; + Goptions.optname = "cbv visited constants display"; + Goptions.optkey = ["Debug";"Cbv"]; + Goptions.optread = (fun () -> !debug_cbv); + Goptions.optwrite = (fun a -> debug_cbv:=a); +} + +let pr_key = function + | ConstKey (sp,_) -> Names.Constant.print sp + | VarKey id -> Names.Id.print id + | RelKey n -> Pp.(str "REL_" ++ int n) + +let rec reify_stack t = function + | TOP -> t + | APP (args,st) -> + reify_stack (mkApp(t,Array.map reify_value args)) st + | CASE (ty,br,ci,env,st) -> + reify_stack + (mkCase (ci, ty, t,br)) + st + | PROJ (p, pinfo, st) -> + reify_stack (mkProj (p, t)) st + +and reify_value = function (* reduction under binders *) + | VAL (n,t) -> lift n t + | STACK (0,v,stk) -> + reify_stack (reify_value v) stk + | STACK (n,v,stk) -> + lift n (reify_stack (reify_value v) stk) + | CBN(t,env) -> + apply_env env t + | LAM (k,ctxt,b,env) -> + apply_env env @@ + List.fold_left (fun c (n,t) -> + mkLambda (n, t, c)) b ctxt + | FIXP ((lij,(names,lty,bds)),env,args) -> + let fix = mkFix (lij, (names, lty, bds)) in + mkApp (apply_env env fix, Array.map reify_value args) + | COFIXP ((j,(names,lty,bds)),env,args) -> + let cofix = mkCoFix (j, (names,lty,bds)) in + mkApp (apply_env env cofix, Array.map reify_value args) + | CONSTR (c,args) -> + mkApp(mkConstructU c, Array.map reify_value args) + +and apply_env env t = + match kind t with + | Rel i -> + begin match expand_rel i env with + | Inl (k, v) -> + reify_value (shift_value k v) + | Inr (k,_) -> + mkRel k + end + | _ -> + map_with_binders subs_lift apply_env env t (* The main recursive functions * @@ -189,7 +249,7 @@ let cofixp_reducible flgs _ stk = let rec norm_head info env t stack = (* no reduction under binders *) - match kind_of_term t with + match kind t with (* stack grows (remove casts) *) | App (head,args) -> (* Applied terms are normalized immediately; they could be computed when getting out of the stack *) @@ -200,12 +260,12 @@ let rec norm_head info env t stack = | Proj (p, c) -> let p' = - if red_set (info_flags info) (fCONST (Projection.constant p)) - && red_set (info_flags info) fBETA + if red_set (info_flags info.infos) (fCONST (Projection.constant p)) + && red_set (info_flags info.infos) fBETA then Projection.unfold p else p in - let pinfo = Environ.lookup_projection p (info_env info) in + let pinfo = Environ.lookup_projection p (info_env info.infos) in norm_head info env c (PROJ (p', pinfo, stack)) (* constants, axioms @@ -220,14 +280,16 @@ let rec norm_head info env t stack = | Var id -> norm_head_ref 0 info env stack (VarKey id) - | Const sp -> norm_head_ref 0 info env stack (ConstKey sp) + | 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) | 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) fZETA then + if red_set (info_flags info.infos) fZETA then (* New rule: for Cbv, Delta does not apply to locally bound variables - or red_set (info_flags info) fDELTA + or red_set (info_flags info.infos) fDELTA *) let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in norm_head info env' c stack @@ -235,13 +297,16 @@ let rec norm_head info env t stack = (CBN(t,env), stack) (* Should we consider a commutative cut ? *) | Evar ev -> - (match evar_value info.i_cache ev with + (match evar_value info.infos.i_cache ev with Some c -> norm_head info env c stack - | None -> (VAL(0, t), stack)) + | None -> + let e, xs = ev in + let xs' = Array.map (apply_env env) xs in + (VAL(0, mkEvar (e,xs')), stack)) (* non-neutral cases *) | Lambda _ -> - let ctxt,b = decompose_lam t in + let ctxt,b = Term.decompose_lam t in (LAM(List.length ctxt, List.rev ctxt,b,env), stack) | Fix fix -> (FIXP(fix,env,[||]), stack) | CoFix cofix -> (COFIXP(cofix,env,[||]), stack) @@ -252,11 +317,19 @@ 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) normt then - match ref_value_cache info normt with - | Some body -> strip_appl (shift_value k body) stack - | None -> (VAL(0,make_constr_ref k normt),stack) - else (VAL(0,make_constr_ref k normt),stack) + if red_set_ref (info_flags info.infos) normt then + match ref_value_cache info.infos info.tab normt with + | Some body -> + if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt); + strip_appl (shift_value k body) stack + | None -> + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt); + (VAL(0,make_constr_ref k normt),stack) + else + begin + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt); + (VAL(0,make_constr_ref k normt),stack) + end (* cbv_stack_term performs weak reduction on constr t under the subs * env, with context stack, i.e. ([env]t stack). First computes weak @@ -270,7 +343,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) fBETA -> + when red_set (info_flags info.infos) fBETA -> let nargs = Array.length args in if nargs == nlams then cbv_stack_term info stk (subs_cons(args,env)) b @@ -284,31 +357,31 @@ and cbv_stack_value info env = function (* a Fix applied enough -> IOTA *) | (FIXP(fix,env,[||]), stk) - when fixp_reducible (info_flags info) fix stk -> + when fixp_reducible (info_flags info.infos) 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) cofix stk-> + when cofixp_reducible (info_flags info.infos) 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) fMATCH -> + when red_set (info_flags info.infos) 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) fMATCH -> + when red_set (info_flags info.infos) fMATCH -> 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) fMATCH && Projection.unfolded p -> + when red_set (info_flags info.infos) fMATCH && Projection.unfolded p -> let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in cbv_stack_value info env (strip_appl arg stk) @@ -316,7 +389,7 @@ and cbv_stack_value info env = function | (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) @@ -350,12 +423,12 @@ and cbv_norm_value info = function (* reduction under binders *) | STACK (n,v,stk) -> lift n (apply_stack info (cbv_norm_value info v) stk) | CBN(t,env) -> - map_constr_with_binders subs_lift (cbv_norm_term info) env t + Constr.map_with_binders subs_lift (cbv_norm_term info) env t | LAM (n,ctxt,b,env) -> let nctxt = 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) + Term.compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b) | FIXP ((lij,(names,lty,bds)),env,args) -> mkApp (mkFix (lij, @@ -376,14 +449,14 @@ and cbv_norm_value info = function (* reduction under binders *) (* with profiling *) let cbv_norm infos constr = - with_stats (lazy (cbv_norm_term infos (subs_id 0) constr)) - -type cbv_infos = cbv_value infos + let constr = EConstr.Unsafe.to_constr constr in + 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 = - create - (fun old_info c -> cbv_stack_term old_info TOP (subs_id 0) c) + let infos = create + (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) + (Reductionops.safe_evar_value sigma) in + { tab = CClosure.create_tab (); infos; sigma } |