From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 pretyping/cbv.ml | 31 ++++++++++++++++---------------
 1 file changed, 16 insertions(+), 15 deletions(-)

(limited to 'pretyping/cbv.ml')

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
-- 
cgit v1.2.3