diff options
Diffstat (limited to 'pretyping/cbv.ml')
| -rw-r--r-- | pretyping/cbv.ml | 31 |
1 files changed, 16 insertions, 15 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index cb0fc325..26590998 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 @@ -187,7 +187,7 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_cbv:=a); } -let pr_key = function +let debug_pr_key = function | ConstKey (sp,_) -> Names.Constant.print sp | VarKey id -> Names.Id.print id | RelKey n -> Pp.(str "REL_" ++ int n) @@ -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 *) @@ -320,14 +320,14 @@ 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 | Some body -> - if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt); + if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_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); + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_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); + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt),stack) end @@ -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 *) @@ -455,7 +455,8 @@ let cbv_norm infos constr = (* constant bodies are normalized at the first expansion *) let create_cbv_infos flgs env sigma = let infos = create - (fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c) + ~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 |