kernel: cleanup projection unfolding

- use Redflags.red_projection
- share unfold_projection between CClosure and Reduction

3 files changed, 28 insertions, 32 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index b1181157e..bb5e91d27 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -847,6 +847,18 @@ let contract_fix_vect fix =
   in
   (subs_cons(Array.init nfix make_body, env), thisbody)
 
+let unfold_projection info p =
+  if red_projection info.i_flags p
+  then
+    let open Declarations in
+    try
+      let pb = lookup_projection p (info_env info) in
+      Some (Zproj (pb.proj_npars, pb.proj_arg, Projection.constant p))
+    with Not_found ->
+      (* This is possible because sometimes for beta reduction we use a dummy env *)
+      None
+  else None
+
 (*********************************************************************)
 (* A machine that inspects the head of a term until it finds an
    atom or a subterm that may produce a redex (abstraction,
@@ -865,15 +877,9 @@ let rec knh info m stk =
            | (None, stk') -> (m,stk'))
     | FCast(t,_,_) -> knh info t stk
     | FProj (p,c) ->
-      let unf = Projection.unfolded p in
-        if unf || red_set info.i_flags (fCONST (Projection.constant p)) then
-          (match try Some (lookup_projection p (info_env info)) with Not_found -> None with
-	  | None -> (m, stk)
-	  | Some pb ->
-	     knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg,
-				Projection.constant p)
-			 :: zupdate m stk))
-	else (m,stk)
+      (match unfold_projection info p with
+       | None -> (m, stk)
+       | Some s -> knh info c (s :: zupdate m stk))
 
 (* cases where knh stops *)
     | (FFlex _|FLetIn _|FConstruct _|FEvar _|
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 119b70e30..bf214ae24 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -163,6 +163,7 @@ val stack_tail : int -> stack -> stack
 val stack_nth : stack -> int -> fconstr
 val zip_term : (fconstr -> constr) -> constr -> stack -> constr
 val eta_expand_stack : stack -> stack
+val unfold_projection : 'a infos -> Projection.t -> stack_member option
 
 (** To lazy reduce a constr, create a [clos_infos] with
    [create_clos_infos], inject the term to reduce with [inject]; then use
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c07ac973b..ecfca9057 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -308,17 +308,6 @@ let in_whnf (t,stk) =
     | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true
     | FLOCKED -> assert false
 
-let unfold_projection infos p c =
-  let unf = Projection.unfolded p in
-    if unf || RedFlags.red_set infos.i_flags (RedFlags.fCONST (Projection.constant p)) then
-      (match try Some (lookup_projection p (info_env infos)) with Not_found -> None with
-      | Some pb -> 
-	let s = Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, 
-		       Projection.constant p) in
-	  Some (c, s)
-      | None -> None)
-  else None
-
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
   eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
@@ -396,13 +385,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
       (* Projections: prefer unfolding to first-order unification,
 	 which will happen naturally if the terms c1, c2 are not in constructor
 	 form *)
-      (match unfold_projection infos p1 c1 with
-      | Some (def1,s1) -> 
-        eqappr cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
+      (match unfold_projection infos p1 with
+      | Some s1 ->
+        eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv
       | None ->
-	match unfold_projection infos p2 c2 with
-	| Some (def2,s2) ->
-          eqappr cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
+        match unfold_projection infos p2 with
+        | Some s2 ->
+          eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
 	| None -> 
           if Constant.equal (Projection.constant p1) (Projection.constant p2)
 	     && compare_stack_shape v1 v2 then
@@ -412,9 +401,9 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	    raise NotConvertible)
 
     | (FProj (p1,c1), t2) ->
-      (match unfold_projection infos p1 c1 with
-      | Some (def1,s1) ->
-         eqappr cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
+      (match unfold_projection infos p1 with
+      | Some s1 ->
+         eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv
       | None -> 
 	 (match t2 with 
 	  | FFlex fl2 ->
@@ -425,9 +414,9 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	  | _ -> raise NotConvertible))
       
     | (t1, FProj (p2,c2)) ->
-      (match unfold_projection infos p2 c2 with
-      | Some (def2,s2) -> 
-         eqappr cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
+      (match unfold_projection infos p2 with
+      | Some s2 ->
+         eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
       | None -> 
 	 (match t1 with 
 	  | FFlex fl1 ->