From 1d9e15c99a90311f8e082fb39615ae1c4aee8084 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Fri, 2 Feb 2018 14:11:33 +0100
Subject: checker: cleanup projection unfolding

This just shares the unfold_projection between Closure and Reduction.
---
 checker/closure.ml   |  8 +++++---
 checker/closure.mli  |  2 ++
 checker/reduction.ml | 13 ++++---------
 3 files changed, 11 insertions(+), 12 deletions(-)

(limited to 'checker')

diff --git a/checker/closure.ml b/checker/closure.ml
index 00fe77485..14b31e09d 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -673,6 +673,9 @@ let contract_fix_vect fix =
   in
   (subs_cons(Array.init nfix make_body, env), thisbody)
 
+let unfold_projection env p =
+  let pb = lookup_projection p env in
+  Zproj (pb.proj_npars, pb.proj_arg, p)
 
 (*********************************************************************)
 (* A machine that inspects the head of a term until it finds an
@@ -694,9 +697,8 @@ let rec knh info m stk =
 
     | FProj (p,c) ->
       if red_set info.i_flags fDELTA then
-        (let pb = lookup_projection p (info.i_env) in
-	   knh info c (Zproj (pb.proj_npars, pb.proj_arg, p)
-		       :: zupdate m stk))
+        let s = unfold_projection info.i_env p in
+        knh info c (s :: zupdate m stk)
       else (m,stk)
 
 (* cases where knh stops *)
diff --git a/checker/closure.mli b/checker/closure.mli
index aace21f2b..7bdc21b60 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -121,6 +121,8 @@ val eta_expand_stack : stack -> stack
 val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> 
    (fconstr * stack) -> stack * stack
 
+val unfold_projection : env -> Projection.t -> stack_member
+
 (* To lazy reduce a constr, create a [clos_infos] with
    [create_clos_infos], inject the term to reduce with [inject]; then use
    a reduction function *)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index d4b258f58..29bb8901e 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -300,11 +300,6 @@ let oracle_order infos l2r k1 k2 =
      if Int.equal n1 n2 then l2r
      else n1 < n2
 
-let unfold_projection infos p c =
-  let pb = lookup_projection p (infos_env infos) in
-  let s = Zproj (pb.proj_npars, pb.proj_arg, p) in
-    (c, s)
-
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
   eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[]))
@@ -374,12 +369,12 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
             eqappr univ cv_pb infos app1 app2)
 	  
     | (FProj (p1,c1), _) ->
-      let (def1, s1) = unfold_projection infos p1 c1 in
-        eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2
+      let s1 = unfold_projection (infos_env infos) p1 in
+        eqappr univ cv_pb infos (lft1, whd_stack infos c1 (s1 :: v1)) appr2
 	  
     | (_, FProj (p2,c2)) ->
-      let (def2, s2) = unfold_projection infos p2 c2 in
-        eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2))
+      let s2 = unfold_projection (infos_env infos) p2 in
+        eqappr univ cv_pb infos appr1 (lft2, whd_stack infos c2 (s2 :: v2))
 
     (* other constructors *)
     | (FLambda _, FLambda _) ->
-- 
cgit v1.2.3