diff options
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 1ae89347ad..0d7f77edae 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -71,6 +71,17 @@ let rec zlapp v = function Zlapp v2 :: s -> zlapp (Array.append v v2) s | s -> Zlapp v :: s +(** Hand-unrolling of the map function to bypass the call to the generic array + allocation. Type annotation is required to tell OCaml that the array does + not contain floats. *) +let map_lift (l : lift) (v : fconstr array) = match v with +| [||] -> assert false +| [|c0|] -> [|(l, c0)|] +| [|c0; c1|] -> [|(l, c0); (l, c1)|] +| [|c0; c1; c2|] -> [|(l, c0); (l, c1); (l, c2)|] +| [|c0; c1; c2; c3|] -> [|(l, c0); (l, c1); (l, c2); (l, c3)|] +| v -> CArray.Fun1.map (fun l t -> (l, t)) l v + let pure_stack lfts stk = let rec pure_rec lfts stk = match stk with @@ -80,7 +91,7 @@ let pure_stack lfts stk = (Zupdate _,lpstk) -> lpstk | (Zshift n,(l,pstk)) -> (el_shft n l, pstk) | (Zapp a, (l,pstk)) -> - (l,zlapp (Array.map (fun t -> (l,t)) a) pstk) + (l,zlapp (map_lift l a) pstk) | (Zproj (n,m,c), (l,pstk)) -> (l, Zlproj (c,l)::pstk) | (Zfix(fx,a),(l,pstk)) -> |