# Queue — foundational two-list FIFO for Bend.
# Publish entry for this package. Depends only on Base (does not reimplement List).
#
# Encoding: front + rear (rear stored reversed). Amortized O(1) enqueue/dequeue
# via Queue.norm (rotate rear→front when front is empty).
# Quantity: Queue<a, A> is Kind(a), same convention as List/Maybe.
import Base

type Queue<a, -A: Kind(a)> is Kind(a):
  Q{front: List<a, A>, rear: List<a, A>}

# Dequeue view: head + rest queue (Kind-friendly; A & Queue is Type, not Kind(a)).
type Queue.Deq<a, -A: Kind(a)> is Kind(a):
  HD{head: A, rest: Queue<a, A>}

def Queue.empty(a, -A: Kind(a)) -> Queue<a, A>:
  Q{Nil{}, Nil{}}

def Queue.enqueue(a, -A: Kind(a), q: Queue<a, A>, x: A) -> Queue<a, A>:
  match q:
    case Q{f, r}:
      Q{f, x <> r}

# When front is empty, reverse rear into front (and clear rear).
def Queue.norm(a, -A: Kind(a), q: Queue<a, A>) -> Queue<a, A>:
  match q:
    case Q{f, r}:
      match f:
        case Nil{}:
          Q{List.reverse(a, A, r), Nil{}}
        case h <> t:
          Q{h <> t, r}

def Queue.dequeue.go(a, -A: Kind(a), q: Queue<a, A>) -> Maybe<a, Queue.Deq<a, A>>:
  match q:
    case Q{f, r}:
      match f:
        case Nil{}:
          None{}
        case h <> t:
          Some{HD{h, Q{t, r}}}

def Queue.dequeue(a, -A: Kind(a), q: Queue<a, A>) -> Maybe<a, Queue.Deq<a, A>>:
  Queue.dequeue.go(a, A, Queue.norm(a, A, q))

def Queue.peek.go(a, -A: Kind(a), q: Queue<a, A>) -> Maybe<a, A>:
  match q:
    case Q{f, r}:
      match f:
        case Nil{}:
          None{}
        case h <> t:
          Some{h}

def Queue.peek(a, -A: Kind(a), q: Queue<a, A>) -> Maybe<a, A>:
  Queue.peek.go(a, A, Queue.norm(a, A, q))

def Queue.is_empty(a, -A: Kind(a), q: Queue<a, A>) -> Bool:
  match q:
    case Q{f, r}:
      match f:
        case Nil{}:
          List.is_empty(a, A, r)
        case h <> t:
          False{}

def Queue.length(a, -A: Kind(a), q: Queue<a, A>) -> Nat:
  match q:
    case Q{f, r}:
      Nat.add(List.length(a, A, f), List.length(a, A, r))

# FIFO order: front ++ reverse(rear).
def Queue.to_list(a, -A: Kind(a), q: Queue<a, A>) -> List<a, A>:
  match q:
    case Q{f, r}:
      List.append(a, A, f, List.reverse(a, A, r))

def Queue.from_list(a, -A: Kind(a), xs: List<a, A>) -> Queue<a, A>:
  Q{xs, Nil{}}