Using allocation-free version of Array higher-order function in critical

cases, which are precisely term manipulation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17054 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 37 insertions, 35 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index e1f3cd582c..517eac6d2b 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -451,7 +451,7 @@ let rec lft_fconstr n ft =
 let lift_fconstr k f =
   if Int.equal k 0 then f else lft_fconstr k f
 let lift_fconstr_vect k v =
-  if Int.equal k 0 then v else Array.map (fun f -> lft_fconstr k f) v
+  if Int.equal k 0 then v else CArray.Fun1.map lft_fconstr k v
 
 let clos_rel e i =
   match expand_rel i e with
@@ -575,7 +575,7 @@ let mk_clos e t =
     | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _) ->
         {norm = Red; term = FCLOS(t,e)}
 
-let mk_clos_vect env v = Array.map (mk_clos env) v
+let mk_clos_vect env 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
@@ -590,11 +590,11 @@ let mk_clos_deep clos_fun env t =
           term = FCast (clos_fun env a, k, clos_fun env b)}
     | App (f,v) ->
         { norm = Red;
-	  term = FApp (clos_fun env f, Array.map (clos_fun env) v) }
+	  term = FApp (clos_fun env f, CArray.Fun1.map clos_fun env v) }
     | Case (ci,p,c,v) ->
         { norm = Red;
 	  term = FCases (ci, clos_fun env p, clos_fun env c,
-			 Array.map (clos_fun env) v) }
+			 CArray.Fun1.map clos_fun env v) }
     | Fix fx ->
         { norm = Cstr; term = FFix (fx, env) }
     | CoFix cfx ->
@@ -628,24 +628,24 @@ let rec to_constr constr_fun lfts v =
     | FCases (ci,p,c,ve) ->
 	mkCase (ci, constr_fun lfts p,
                 constr_fun lfts c,
-		Array.map (constr_fun lfts) ve)
+		CArray.Fun1.map constr_fun lfts ve)
     | FFix ((op,(lna,tys,bds)),e) ->
         let n = Array.length bds in
-        let ftys = Array.map (mk_clos e) tys in
-        let fbds = Array.map (mk_clos (subs_liftn n e)) bds in
+        let ftys = CArray.Fun1.map mk_clos e tys in
+        let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in
 	let lfts' = el_liftn n lfts in
-	mkFix (op, (lna, Array.map (constr_fun lfts) ftys,
-		         Array.map (constr_fun lfts') fbds))
+	mkFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys,
+		         CArray.Fun1.map constr_fun lfts' fbds))
     | FCoFix ((op,(lna,tys,bds)),e) ->
         let n = Array.length bds in
-        let ftys = Array.map (mk_clos e) tys in
-        let fbds = Array.map (mk_clos (subs_liftn n e)) bds in
+        let ftys = CArray.Fun1.map mk_clos e tys in
+        let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in
 	let lfts' = el_liftn (Array.length bds) lfts in
-	mkCoFix (op, (lna, Array.map (constr_fun lfts) ftys,
-		           Array.map (constr_fun lfts') fbds))
+	mkCoFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys,
+		           CArray.Fun1.map constr_fun lfts' fbds))
     | FApp (f,ve) ->
 	mkApp (constr_fun lfts f,
-	       Array.map (constr_fun lfts) ve)
+	       CArray.Fun1.map constr_fun lfts ve)
     | FLambda _ ->
         let (na,ty,bd) = destFLambda mk_clos2 v in
 	mkLambda (na, constr_fun lfts ty,
@@ -973,15 +973,15 @@ and norm_head info m =
       | FProd(na,dom,rng) ->
           mkProd(na, kl info dom, kl info rng)
       | FCoFix((n,(na,tys,bds)),e) ->
-          let ftys = Array.map (mk_clos e) tys in
+          let ftys = CArray.Fun1.map mk_clos e tys in
           let fbds =
-            Array.map (mk_clos (subs_liftn (Array.length na) e)) bds in
-          mkCoFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) fbds))
+            CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
+          mkCoFix(n,(na, CArray.Fun1.map kl info ftys, CArray.Fun1.map kl info fbds))
       | FFix((n,(na,tys,bds)),e) ->
-          let ftys = Array.map (mk_clos e) tys in
+          let ftys = CArray.Fun1.map mk_clos e tys in
           let fbds =
-            Array.map (mk_clos (subs_liftn (Array.length na) e)) bds in
-          mkFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) fbds))
+            CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
+          mkFix(n,(na, CArray.Fun1.map kl info ftys, CArray.Fun1.map kl info fbds))
       | FEvar((i,args),env) ->
           mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args)
       | t -> term_of_fconstr m
@@ -996,7 +996,7 @@ let whd_val info v =
 let norm_val info v =
   with_stats (lazy (kl info v))
 
-let inject = mk_clos (subs_id 0)
+let inject c = mk_clos (subs_id 0) c
 
 let whd_stack infos m stk =
   let k = kni infos m stk in
diff --git a/kernel/constr.ml b/kernel/constr.ml
index af9f4f0772..bdc181bb1c 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -265,15 +265,15 @@ let iter_with_binders g f n c = match kind c with
   | Prod (_,t,c) -> f n t; f (g n) c
   | Lambda (_,t,c) -> f n t; f (g n) c
   | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
-  | App (c,l) -> f n c; Array.iter (f n) l
-  | Evar (_,l) -> Array.iter (f n) l
-  | Case (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl
+  | App (c,l) -> f n c; CArray.Fun1.iter f n l
+  | Evar (_,l) -> CArray.Fun1.iter f n l
+  | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
   | Fix (_,(_,tl,bl)) ->
-      Array.iter (f n) tl;
-      Array.iter (f (iterate g (Array.length tl) n)) bl
+      CArray.Fun1.iter f n tl;
+      CArray.Fun1.iter f (iterate g (Array.length tl) n) bl
   | CoFix (_,(_,tl,bl)) ->
-      Array.iter (f n) tl;
-      Array.iter (f (iterate g (Array.length tl) n)) bl
+      CArray.Fun1.iter f n tl;
+      CArray.Fun1.iter f (iterate g (Array.length tl) n) bl
 
 (* [map f c] maps [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
@@ -329,6 +329,8 @@ let map f c = match kind c with
       if tl'==tl && bl'==bl then c
       else mkCoFix (ln,(lna,tl',bl'))
 
+exception Exit of int * constr
+
 (* [map_with_binders g f n c] maps [f n] on the immediate
    subterms of [c]; it carries an extra data [n] (typically a lift
    index) which is processed by [g] (which typically add 1 to [n]) at
@@ -361,29 +363,29 @@ let map_with_binders g f l c0 = match kind c0 with
     else mkLetIn (na, b', t', c')
   | App (c, al) ->
     let c' = f l c in
-    let al' = Array.smartmap (f l) al in
+    let al' = CArray.Fun1.smartmap f l al in
     if c' == c && al' == al then c0
     else mkApp (c', al')
   | Evar (e, al) ->
-    let al' = Array.smartmap (f l) al in
+    let al' = CArray.Fun1.smartmap f l al in
     if al' == al then c0
     else mkEvar (e, al')
   | Case (ci, p, c, bl) ->
     let p' = f l p in
     let c' = f l c in
-    let bl' = Array.smartmap (f l) bl in
+    let bl' = CArray.Fun1.smartmap f l bl in
     if p' == p && c' == c && bl' == bl then c0
     else mkCase (ci, p', c', bl')
   | Fix (ln, (lna, tl, bl)) ->
-    let tl' = Array.smartmap (f l) tl in
+    let tl' = CArray.Fun1.smartmap f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = Array.smartmap (f l') bl in
+    let bl' = CArray.Fun1.smartmap f l' bl in
     if tl' == tl && bl' == bl then c0
     else mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl)) ->
-    let tl' = Array.smartmap (f l) tl in
+    let tl' = CArray.Fun1.smartmap f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = Array.smartmap (f l') bl in
+    let bl' = CArray.Fun1.smartmap f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
 (* [compare f c1 c2] compare [c1] and [c2] using [f] to compare