diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-02 14:11:33 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-02 14:41:23 +0100 |
| commit | 1d9e15c99a90311f8e082fb39615ae1c4aee8084 (patch) | |
| tree | 83774712b333ff1ebdaf805da0d02be816f9790d /checker/closure.ml | |
| parent | c9839e30e1b46e70c85533d95e4f4cc2ae826c66 (diff) | |
checker: cleanup projection unfolding
This just shares the unfold_projection between Closure and Reduction.
Diffstat (limited to 'checker/closure.ml')
| -rw-r--r-- | checker/closure.ml | 8 |
1 files changed, 5 insertions, 3 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 *) |