[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.

1 files changed, 15 insertions, 4 deletions

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