From 1d9e15c99a90311f8e082fb39615ae1c4aee8084 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert 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 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'checker/closure.ml') 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 *) -- cgit v1.2.3