diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-22 09:15:39 +0200 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-22 09:15:39 +0200 |
commit | 98a710caf5e907344329ee9e9f7b5fd87c50836f (patch) | |
tree | 6d502b010ed2fce667c0b143a82e8ef1eed407f8 /lib/pp.ml | |
parent | a201b73607d0094c89776ea4b51483bf3d1f9cec (diff) |
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
Diffstat (limited to 'lib/pp.ml')
-rw-r--r-- | lib/pp.ml | 29 |
1 files changed, 22 insertions, 7 deletions
@@ -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 : |