diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-02-07 15:55:11 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-07 15:55:11 +0100 |
commit | 54c9c89bd8aac03f002549aad771337442e0279b (patch) | |
tree | 3b33ff0b9671f25c16d2bf844a57667e5685d386 /kernel | |
parent | b4e0aa73bd36ca32fc112ca7c660c474f0b2564a (diff) | |
parent | 783c7d09492f64d3a00673f8d698da3bcef6c503 (diff) |
Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/cClosure.ml | 20 | ||||
-rw-r--r-- | kernel/cClosure.mli | 1 | ||||
-rw-r--r-- | kernel/reduction.ml | 35 |
3 files changed, 24 insertions, 32 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index b1181157e..7ed965b4c 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -847,6 +847,14 @@ 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 + let pb = lookup_projection p (info_env info) in + Some (Zproj (pb.proj_npars, pb.proj_arg, Projection.constant p)) + 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 +873,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 -> |