diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-11-23 23:26:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-11-24 00:04:10 +0100 |
| commit | ae61e1397d343ee9b1e9a9715200e96706715e27 (patch) | |
| tree | 5ccadcb1f5ce07b6dcbdbdfc5d8d62ea262eaabe /kernel/closure.ml | |
| parent | a000b714412e4b1f48bf3ffe1479cf6589874b47 (diff) | |
Slightly more efficient zip function in Closure.
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 31 |
1 files changed, 18 insertions, 13 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 96f57f88d..bf39fa42b 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -691,19 +691,24 @@ let rec fstrong unfreeze_fun lfts v = to_constr (fstrong unfreeze_fun) lfts (unfreeze_fun v) *) -let rec zip m stk = - match stk with - | [] -> m - | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s - | Zcase(ci,p,br)::s -> - let t = FCases(ci, p, m, br) in - zip {norm=neutr m.norm; term=t} s - | Zfix(fx,par)::s -> - zip fx (par @ append_stack [|m|] s) - | Zshift(n)::s -> - zip (lift_fconstr n m) s - | Zupdate(rf)::s -> - zip (update rf m.norm m.term) s +let rec zip m stk rem = match stk with +| [] -> + begin match rem with + | [] -> m + | stk :: rem -> zip m stk rem + end +| Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s rem +| Zcase(ci,p,br)::s -> + let t = FCases(ci, p, m, br) in + zip {norm=neutr m.norm; term=t} s rem +| Zfix(fx,par)::s -> + zip fx par ((Zapp [|m|] :: s) :: rem) +| Zshift(n)::s -> + zip (lift_fconstr n m) s rem +| Zupdate(rf)::s -> + zip (update rf m.norm m.term) s rem + +let zip m stk = zip m stk [] let fapp_stack (m,stk) = zip m stk |