diff options
| -rw-r--r-- | kernel/cClosure.ml | 11 | ||||
| -rw-r--r-- | kernel/reduction.ml | 13 |
2 files changed, 22 insertions, 2 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index fe9ec5794..b1dd26119 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -540,7 +540,16 @@ let mk_clos e t = | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> {norm = Red; term = FCLOS(t,e)} -let mk_clos_vect env v = CArray.Fun1.map mk_clos env v +(** Hand-unrolling of the map function to bypass the call to the generic array + allocation *) +let mk_clos_vect env v = match v with +| [||] -> [||] +| [|v0|] -> [|mk_clos env v0|] +| [|v0; v1|] -> [|mk_clos env v0; mk_clos env v1|] +| [|v0; v1; v2|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2|] +| [|v0; v1; v2; v3|] -> + [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|] +| v -> CArray.Fun1.map mk_clos env v (* Translate the head constructor of t from constr to fconstr. This function is parameterized by the function to apply on the direct diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 1ae89347a..0d7f77eda 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)) -> |