# HG changeset patch
# User wenzelm
# Date 1220539428 -7200
# Node ID 93ee30a54c9ad03814c2dc1823c04f37a735a87e
# Parent  7332b623b569d361067c34656200e16cd84b9542
Efficient queues.

diff -r 7332b623b569 -r 93ee30a54c9a src/Pure/General/queue.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/queue.ML	Thu Sep 04 16:43:48 2008 +0200
@@ -0,0 +1,36 @@
+(*  Title:      Pure/General/queue.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Efficient queues.
+*)
+
+signature QUEUE =
+sig
+  type 'a T
+  val empty: 'a T
+  val is_empty: 'a T -> bool
+  val content: 'a T -> 'a list
+  val enqueue: 'a -> 'a T -> 'a T
+  val dequeue: 'a T -> 'a * 'a T
+end;
+
+structure Queue: QUEUE =
+struct
+
+datatype 'a T = Queue of 'a list * 'a list;
+
+val empty = Queue ([], []);
+
+fun is_empty (Queue ([], [])) = true
+  | is_empty _ = false;
+
+fun content (Queue (xs, ys)) = ys @ rev xs;
+
+fun enqueue x (Queue (xs, ys)) = Queue (x :: xs, ys);
+
+fun dequeue (Queue (xs, y :: ys)) = (y, Queue (xs, ys))
+  | dequeue (Queue (xs as _ :: _, [])) = let val y :: ys = rev xs in (y, Queue ([], ys)) end
+  | dequeue (Queue ([], [])) = raise Empty;
+
+end;