From 8fa1d224dafde29f5b527d380c069f196a042c60 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 27 Jul 2017 15:09:14 +0200
Subject: [pp] Minor optimization in `Pp.t` construction and gluing.

The typical Coq `Pp.t` document contains a lot of "gluing" which
produces efficient structures but it is quite painful in
serialization.

We optimize a common document building case so we don't create as much
glue nodes as with the "naive" strategy, and without incurring in the
large performance cost full flattening would produce.

This is a temporal fixup, see #505 for more context on the discussion
and medium-term plans.
---
 lib/pp.ml | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

(limited to 'lib/pp.ml')

diff --git a/lib/pp.ml b/lib/pp.ml
index 88ddcb35b5..c3338688d2 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -82,10 +82,21 @@ let utf8_length s =
   done ;
   !cnt
 
-let app s1 s2 = match s1, s2 with
-  | Ppcmd_empty, s
-  | s, Ppcmd_empty -> s
-  | s1, s2         -> Ppcmd_glue [s1; s2]
+let rec app d1 d2 = match d1, d2 with
+  | Ppcmd_empty,        d
+  | d,                  Ppcmd_empty      -> d
+
+  (* Optimizations *)
+  | Ppcmd_glue [l1;l2], Ppcmd_glue l3    -> Ppcmd_glue (l1 :: l2 :: l3)
+  | Ppcmd_glue [l1;l2], d2               -> Ppcmd_glue [l1 ; l2 ; d2]
+  | d1,                 Ppcmd_glue l2    -> Ppcmd_glue (d1 :: l2)
+
+  | Ppcmd_tag(t1,d1),   Ppcmd_tag(t2,d2)
+    when t1 = t2                         -> Ppcmd_tag(t1,app d1 d2)
+  | d1, d2                               -> Ppcmd_glue [d1; d2]
+  (* Optimizations deemed too costly *)
+  (* | Ppcmd_glue l1,    Ppcmd_glue l2    -> Ppcmd_glue   (l1 @ l2) *)
+  (* | Ppcmd_string s1,  Ppcmd_string s2  -> Ppcmd_string (s1 ^ s2) *)
 
 let seq s = Ppcmd_glue s
 
-- 
cgit v1.2.3