diff options
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 38 |
1 files changed, 36 insertions, 2 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 1ae89347ad..cd975ee9a9 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)) -> @@ -96,7 +107,15 @@ let pure_stack lfts stk = (****************************************************************************) let whd_betaiota env t = - whd_val (create_clos_infos betaiota env) (inject t) + match kind_of_term t with + | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| + Prod _|Lambda _|Fix _|CoFix _) -> t + | App (c, _) -> + begin match kind_of_term c with + | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | LetIn _ -> t + | _ -> whd_val (create_clos_infos betaiota env) (inject t) + end + | _ -> whd_val (create_clos_infos betaiota env) (inject t) let nf_betaiota env t = norm_val (create_clos_infos betaiota env) (inject t) @@ -105,18 +124,33 @@ let whd_betaiotazeta env x = match kind_of_term x with | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> x + | App (c, _) -> + begin match kind_of_term c with + | Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x + | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) + end | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) let whd_all env t = match kind_of_term t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> t + | App (c, _) -> + begin match kind_of_term c with + | Ind _ | Construct _ | Evar _ | Meta _ -> t + | _ -> whd_val (create_clos_infos all env) (inject t) + end | _ -> whd_val (create_clos_infos all env) (inject t) let whd_allnolet env t = match kind_of_term t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t + | App (c, _) -> + begin match kind_of_term c with + | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t + | _ -> whd_val (create_clos_infos allnolet env) (inject t) + end | _ -> whd_val (create_clos_infos allnolet env) (inject t) (********************************************************************) |