src/Pure/General/queue.ML
author haftmann
Tue, 23 Sep 2008 18:11:44 +0200
changeset 28337 93964076e7b8
parent 28127 93ee30a54c9a
child 29606 fedb8be05f24
permissions -rw-r--r--
case default fallback for NBE
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28127
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/queue.ML
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
     4
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
     5
Efficient queues.
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
     6
*)
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
     7
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
     8
signature QUEUE =
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
     9
sig
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    10
  type 'a T
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    11
  val empty: 'a T
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    12
  val is_empty: 'a T -> bool
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    13
  val content: 'a T -> 'a list
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    14
  val enqueue: 'a -> 'a T -> 'a T
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    15
  val dequeue: 'a T -> 'a * 'a T
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    16
end;
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    17
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    18
structure Queue: QUEUE =
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    19
struct
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    20
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    21
datatype 'a T = Queue of 'a list * 'a list;
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    22
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    23
val empty = Queue ([], []);
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    24
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    25
fun is_empty (Queue ([], [])) = true
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    26
  | is_empty _ = false;
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    27
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    28
fun content (Queue (xs, ys)) = ys @ rev xs;
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    29
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    30
fun enqueue x (Queue (xs, ys)) = Queue (x :: xs, ys);
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    31
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    32
fun dequeue (Queue (xs, y :: ys)) = (y, Queue (xs, ys))
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    33
  | dequeue (Queue (xs as _ :: _, [])) = let val y :: ys = rev xs in (y, Queue ([], ys)) end
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    34
  | dequeue (Queue ([], [])) = raise Empty;
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    35
93ee30a54c9a Efficient queues.
wenzelm
parents:
diff changeset
    36
end;