src/queue.bend source

src/queue.bend on the hub · documented module

import Baseimport ./list.bend as List# queue.bend: a FIFO queue as two lists, specified by the list it holds.##   import ./queue.bend as Q## push conses onto rear; pop takes from front, and when front is empty the# reversed rear becomes the new front. Queue is linear (Type), so each# queue value is used once; then each element is reversed at most once and# every operation costs O(1) on average.## model(q) is the list q holds. push_model and pop_model state push and# pop in terms of it.type Queue<-A: Data> is Type:  Queue{front: List<&2, A>, rear: List<&2, A>}def empty(-A: Data) -> Queue<A>:  Queue{Nil{}, Nil{}}def model(-A: Data, q: Queue<A>) -> List<&2, A>:  match q:    case Queue{f, r}:      List.append(&2, A, f, List.reverse(&2, A, r))def push(-A: Data, q: Queue<A>, x: A) -> Queue<A>:  match q:    case Queue{f, r}:      Queue{f, x <> r}# front is empty; f is the reversed reardef pop.rot(-A: Data, f: List<&2, A>) -> List.Step<&1, A, Queue<A>>:  match f:    case Nil{}:      List.Stop{}    case h <> t:      List.Next{h, Queue{t, Nil{}}}def pop(-A: Data, q: Queue<A>) -> List.Step<&1, A, Queue<A>>:  match q:    case Queue{Nil{}, r}:      pop.rot(A, List.reverse(&2, A, r))    case Queue{h <> t, r}:      List.Next{h, Queue{t, r}}# pop's result with the remaining queue replaced by its modeldef pop.model(-A: Data, s: List.Step<&1, A, Queue<A>>) -> List.Step<&2, A, List<&2, A>>:  match s:    case List.Stop{}:      List.Stop{}    case List.Next{x, q}:      List.Next{x, model(A, q)}# push appends x to the model.law push_model:  for -A: Data  for q: Queue<A>  for +x: A  {List.append(&2, A, model(A, q), [x]) == model(A, push(A, q, x)) : List<&2, A>}def push_model(A, q, x):  match q:    case Queue{+f, +r}:      %List.reverse_go(A, r, [x]) : {List.append(&2, A, List.append(&2, A, f, List.reverse(&2, A, r)), [x]) == List.append(&2, A, f, _) : List<&2, A>}      Equal.sym(List<&2, A>,        List.append(&2, A, f, List.append(&2, A, List.reverse(&2, A, r), [x])),        List.append(&2, A, List.append(&2, A, f, List.reverse(&2, A, r)), [x]),        List.append_assoc(A, f, List.reverse(&2, A, r), [x]))law pop_model.rot:  for -A: Data  for f: List<&2, A>  {List.uncons(A, f) == pop.model(A, pop.rot(A, f)) : List.Step<&2, A, List<&2, A>>}def pop_model.rot(A, f):  match f:    case Nil{}:      {==}    case h <> t:      %List.append_nil(A, t) : {List.Next{h, t} == List.Next{h, _} : List.Step<&2, A, List<&2, A>>}      {==}# pop returns the model's head and tail.law pop_model:  for -A: Data  for q: Queue<A>  {List.uncons(A, model(A, q)) == pop.model(A, pop(A, q)) : List.Step<&2, A, List<&2, A>>}def pop_model(A, q):  match q:    case Queue{Nil{}, r}:      pop_model.rot(A, List.reverse(&2, A, r))    case Queue{h <> t, r}:      {==}