src/containers/queue.bend source

src/containers/queue.bend on the hub · documented module

import Baseimport ./types/queue.bend as E# Two-list FIFO queue: front ++ reverse(back). Reverse back only when front# is empty. Enqueue/dequeue/peek are amortized O(1) on consumed histories.# length is cached; to_list is O(n). Independent of the deque and DLL.type Queue<-T: Data> is Type:  QU{front: List<&2, T>, back: List<&2, T>, count: Nat}def new(~T: Data) -> Queue<T>:  QU{Nil{}, Nil{}, 0n}def length(~T: Data, q: Queue<T>) -> Queue<T> & Nat:  QU{f, b, +n} = q  (QU{f, b, n}, n)def enqueue(~T: Data, q: Queue<T>, x: T) -> Queue<T>:  QU{f, b, n} = q  QU{f, Con{x, b}, 1n+n}def ready(~T: Data, q: Queue<T>) -> Queue<T>:  match q:    case QU{Nil{}, b, n}:      QU{List.reverse(&2, T, b), Nil{}, n}    case QU{Con{x, f}, b, n}:      QU{Con{x, f}, b, n}def dequeue_ready(~T: Data, q: Queue<T>) -> Queue<T> & Result<&2, &2, E.Error, T>:  match q:    case QU{Nil{}, b, n}:      (QU{Nil{}, b, n}, Fail{E.EmptyQueue{}})    case QU{Con{x, f}, b, n}:      (QU{f, b, Nat.sub(n, 1n)}, Done{x})def peek_ready(~T: Data, q: Queue<T>) -> Queue<T> & Result<&2, &2, E.Error, T>:  match q:    case QU{Nil{}, b, n}:      (QU{Nil{}, b, n}, Fail{E.EmptyQueue{}})    case QU{Con{+x, f}, b, n}:      (QU{Con{x, f}, b, n}, Done{x})def dequeue(~T: Data, q: Queue<T>) -> Queue<T> & Result<&2, &2, E.Error, T>:  dequeue_ready(~T, ready(~T, q))def peek(~T: Data, q: Queue<T>) -> Queue<T> & Result<&2, &2, E.Error, T>:  peek_ready(~T, ready(~T, q))def to_list(~T: Data, q: Queue<T>) -> Queue<T> & List<&2, T>:  QU{+f, +b, n} = q  (QU{f, b, n}, List.append(&2, T, f, List.reverse(&2, T, b)))# ---- operation traces ----def obs_nat(~T: Data, r: Queue<T> & Nat) -> Queue<T> & E.Obs<T>:  (q, n) = r  (q, E.ONat{n})def obs_item(~T: Data, r: Queue<T> & Result<&2, &2, E.Error, T>) -> Queue<T> & E.Obs<T>:  (q, x) = r  (q, E.OItem{x})def obs_list(~T: Data, r: Queue<T> & List<&2, T>) -> Queue<T> & E.Obs<T>:  (q, xs) = r  (q, E.OList{xs})def step(~T: Data, q: Queue<T>, op: E.Op<T>) -> Queue<T> & E.Obs<T>:  match op:    case E.Length{}:      obs_nat(~T, length(~T, q))    case E.Enqueue{+x}:      (enqueue(~T, q, x), E.OUnit{})    case E.Dequeue{}:      obs_item(~T, dequeue(~T, q))    case E.Peek{}:      obs_item(~T, peek(~T, q))    case E.ToList{}:      obs_list(~T, to_list(~T, q))def record(~T: Data, acc: List<&2, E.Obs<T>>, r: Queue<T> & E.Obs<T>) -> Queue<T> & List<&2, E.Obs<T>>:  (q, o) = r  (q, Con{o, acc})def step_acc(~T: Data, op: E.Op<T>, st: Queue<T> & List<&2, E.Obs<T>>) -> Queue<T> & List<&2, E.Obs<T>>:  (q, acc) = st  record(~T, acc, step(~T, q, op))def run_acc(~T: Data, ops: List<&2, E.Op<T>>, st: Queue<T> & List<&2, E.Obs<T>>) -> Queue<T> & List<&2, E.Obs<T>>:  match ops:    case Nil{}:      st    case Con{op, rest}:      run_acc(~T, rest, step_acc(~T, op, st))def finish(~T: Data, st: Queue<T> & List<&2, E.Obs<T>>) -> Queue<T> & List<&2, E.Obs<T>>:  (q, acc) = st  (q, List.reverse(&2, E.Obs<T>, acc))def run(~T: Data, ops: List<&2, E.Op<T>>, q: Queue<T>) -> Queue<T> & List<&2, E.Obs<T>>:  finish(~T, run_acc(~T, ops, (q, Nil{})))