# Deque — foundational two-list double-ended queue for Bend.
# Publish entry for this package. Depends only on Base.
#
# Encoding: front + rear (rear stored reversed). Each side is normalized only
# when that side is empty, so transfers are amortized over the operations.
import Base

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

type Deque.Pop<a, -A: Kind(a)> is Kind(a):
  P{value: A, rest: Deque<a, A>}

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

def Deque.push_front(a, -A: Kind(a), q: Deque<a, A>, x: A) -> Deque<a, A>:
  match q:
    case D{f, r}:
      D{x <> f, r}

def Deque.push_back(a, -A: Kind(a), q: Deque<a, A>, x: A) -> Deque<a, A>:
  match q:
    case D{f, r}:
      D{f, x <> r}

# When front is empty, reverse rear into front.
def Deque.norm_front(a, -A: Kind(a), q: Deque<a, A>) -> Deque<a, A>:
  match q:
    case D{f, r}:
      match f:
        case Nil{}:
          D{List.reverse(a, A, r), Nil{}}
        case h <> t:
          D{h <> t, r}

# When rear is empty, reverse front into rear.
def Deque.norm_back(a, -A: Kind(a), q: Deque<a, A>) -> Deque<a, A>:
  match q:
    case D{f, r}:
      match r:
        case Nil{}:
          D{Nil{}, List.reverse(a, A, f)}
        case h <> t:
          D{f, h <> t}

def Deque.pop_front.go(a, -A: Kind(a), q: Deque<a, A>) -> Maybe<a, Deque.Pop<a, A>>:
  match q:
    case D{f, r}:
      match f:
        case Nil{}:
          None{}
        case h <> t:
          Some{P{h, D{t, r}}}

def Deque.pop_front(a, -A: Kind(a), q: Deque<a, A>) -> Maybe<a, Deque.Pop<a, A>>:
  Deque.pop_front.go(a, A, Deque.norm_front(a, A, q))

def Deque.pop_back.go(a, -A: Kind(a), q: Deque<a, A>) -> Maybe<a, Deque.Pop<a, A>>:
  match q:
    case D{f, r}:
      match r:
        case Nil{}:
          None{}
        case h <> t:
          Some{P{h, D{f, t}}}

def Deque.pop_back(a, -A: Kind(a), q: Deque<a, A>) -> Maybe<a, Deque.Pop<a, A>>:
  Deque.pop_back.go(a, A, Deque.norm_back(a, A, q))

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

def Deque.peek_front(a, -A: Kind(a), q: Deque<a, A>) -> Maybe<a, A>:
  Deque.peek_front.go(a, A, Deque.norm_front(a, A, q))

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

def Deque.peek_back(a, -A: Kind(a), q: Deque<a, A>) -> Maybe<a, A>:
  Deque.peek_back.go(a, A, Deque.norm_back(a, A, q))

def Deque.is_empty(a, -A: Kind(a), q: Deque<a, A>) -> Bool:
  match q:
    case D{f, r}:
      match f r:
        case Nil{} Nil{}:
          True{}
        case _ _:
          False{}

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

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

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