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

1 files changed, 16 insertions, 14 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index af9f4f077..bdc181bb1 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