src/Pure/General/queue.ML

Reintroduce set_interpreter for Collect and op :.
I removed them by accident when removing old code that dealt with the "set" type.
Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).

(*  Title:      Pure/General/queue.ML
    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;