aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-02 14:11:33 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-02 14:41:23 +0100
commit1d9e15c99a90311f8e082fb39615ae1c4aee8084 (patch)
tree83774712b333ff1ebdaf805da0d02be816f9790d
parentc9839e30e1b46e70c85533d95e4f4cc2ae826c66 (diff)
checker: cleanup projection unfolding
This just shares the unfold_projection between Closure and Reduction.
-rw-r--r--checker/closure.ml8
-rw-r--r--checker/closure.mli2
-rw-r--r--checker/reduction.ml13
3 files changed, 11 insertions, 12 deletions
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 _) ->