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/cClosure.ml | |
| parent | f22c72ff594408c3a3cac04cfee2234a59f2655b (diff) | |
| parent | 2b8ad7e04002ebe9fec5790da924673418f2fa7f (diff) | |
Merge PR#434: Optimizing array mapping in the kernel.
Diffstat (limited to 'kernel/cClosure.ml')
| -rw-r--r-- | kernel/cClosure.ml | 11 |
1 files changed, 10 insertions, 1 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 |