summaryrefslogtreecommitdiff
path: root/pretyping/cbv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cbv.ml')
-rw-r--r--pretyping/cbv.ml149
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 }
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 11:53:22 +0000