From cbbd579354d81f6749d14853a1c6a5cc67728907 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 29 Oct 2013 17:10:51 +0000
Subject: Sharing identity evar filters.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16948 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evd.ml | 27 +++++++++++++++++++++------
 1 file changed, 21 insertions(+), 6 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index f2380e17f0..67cf3a32f2 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -40,6 +40,27 @@ end =
 struct
   type t = bool list
 
+  (** Most of filters we use are identities, so we share their use. *)
+  let identity_pool = Array.make 128 []
+
+  let () =
+    (** Fill the filter pool *)
+    for i = 1 to 127 do
+      let pred = Array.unsafe_get identity_pool (pred i) in
+      let curr = true :: pred in
+      Array.unsafe_set identity_pool i curr
+    done
+
+  let rec identity_gen n accu =
+    if n = 0 then accu
+    else identity_gen (pred n) (true :: accu)
+
+  let identity n =
+    if n < 128 then Array.unsafe_get identity_pool n
+    else
+      let accu = Array.unsafe_get identity_pool 127 in
+      identity_gen (n - 127) accu
+
   let length = List.length
 
   let rec equal l1 l2 = match l1, l2 with
@@ -48,12 +69,6 @@ struct
     (if h1 then h2 else not h2) && equal l1 l2
   | _ -> false
 
-  let rec identity n accu =
-    if n = 0 then accu
-    else identity (pred n) (true :: accu)
-
-  let identity n = identity n []
-
   let rec is_identity = function
   | [] -> true
   | true :: l -> is_identity l
-- 
cgit v1.2.3