From 338bac67b6c1111229d90c45875653171bbed4b3 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 2 Feb 2018 13:57:06 +0100 Subject: kernel: cleanup projection unfolding - use Redflags.red_projection - share unfold_projection between CClosure and Reduction --- kernel/cClosure.ml | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) (limited to 'kernel/cClosure.ml') 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 _| -- cgit v1.2.3