From 98a710caf5e907344329ee9e9f7b5fd87c50836f Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 22 Apr 2015 09:15:39 +0200
Subject: Do not use list concatenation when gluing streams together, just mark
 them as glued.

Possible improvement: rotate using the left children in the glue function,
so that the iter function becomes mostly tail-recursive. Drawback: two
allocations per glue instead of a single one.

This commit makes the following command go from 7.9s to 3.0s:

coqtop <<< "Require Import BigZ ZBinary Reals OrdersEx. Time SearchPattern _." | tail -n 1
---
 lib/pp.ml | 29 ++++++++++++++++++++++-------
 1 file changed, 22 insertions(+), 7 deletions(-)

(limited to 'lib')

diff --git a/lib/pp.ml b/lib/pp.ml
index 76046a7f91..e8b42ed797 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -26,15 +26,30 @@ module Glue : sig
 
 end = struct
 
-  type 'a t = 'a list
+  type 'a t = GEmpty | GLeaf of 'a | GNode of 'a t * 'a t
 
-  let atom x = [x]
-  let glue x y = y @ x
-  let empty = []
-  let is_empty x = x = []
+  let atom x = GLeaf x
+
+  let glue x y =
+    match x, y with
+    | GEmpty, _ -> y
+    | _, GEmpty -> x
+    | _, _ -> GNode (x,y)
+
+  let empty = GEmpty
+
+  let is_empty x = x = GEmpty
+
+  let rec iter f = function
+    | GEmpty -> ()
+    | GLeaf x -> f x
+    | GNode (x,y) -> iter f x; iter f y
+
+  let rec map f = function
+    | GEmpty -> GEmpty
+    | GLeaf x -> GLeaf (f x)
+    | GNode (x,y) -> GNode (map f x, map f y)
 
-  let iter f g = List.iter f (List.rev g)
-  let map = List.map
 end
 
 module Tag :
-- 
cgit v1.2.3