diff options
| author | Maxime Dénès | 2017-04-05 01:36:48 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-05 01:36:48 +0200 |
| commit | 9f188da28f65341f5c5ecd0b3b4f9b447bbc2b15 (patch) | |
| tree | f30c3bfde8ee4d08d277ab95acfdf3f78045592e /kernel | |
| parent | f22c72ff594408c3a3cac04cfee2234a59f2655b (diff) | |
| parent | 2b8ad7e04002ebe9fec5790da924673418f2fa7f (diff) | |
Merge PR#434: Optimizing array mapping in the kernel.
Diffstat (limited to 'kernel')
| -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 fe9ec5794c..b1dd26119e 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 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)) -> |