# NonEmpty (aka NEList) — foundational non-empty list for Bend.
# Publish entry for this package. Depends only on Base (does not reimplement List).
#
# Encoding: head + List tail. Emptiness is unrepresentable by construction.
# Quantity: NonEmpty<a, A> is Kind(a), same convention as List/Maybe.
import Base

type NonEmpty<a, -A: Kind(a)> is Kind(a):
  NE{head: A, tail: List<a, A>}

def NonEmpty.one(a, -A: Kind(a), x: A) -> NonEmpty<a, A>:
  NE{x, Nil{}}

def NonEmpty.cons(a, -A: Kind(a), x: A, xs: NonEmpty<a, A>) -> NonEmpty<a, A>:
  match xs:
    case NE{h, t}:
      NE{x, h <> t}

def NonEmpty.from_list(a, -A: Kind(a), xs: List<a, A>) -> Maybe<a, NonEmpty<a, A>>:
  match xs:
    case Nil{}:
      None{}
    case h <> t:
      Some{NE{h, t}}

def NonEmpty.to_list(a, -A: Kind(a), xs: NonEmpty<a, A>) -> List<a, A>:
  match xs:
    case NE{h, t}:
      h <> t

def NonEmpty.head(a, -A: Kind(a), xs: NonEmpty<a, A>) -> A:
  match xs:
    case NE{h, t}:
      h

def NonEmpty.tail(a, -A: Kind(a), xs: NonEmpty<a, A>) -> List<a, A>:
  match xs:
    case NE{h, t}:
      t

def NonEmpty.length(a, -A: Kind(a), xs: NonEmpty<a, A>) -> Nat:
  match xs:
    case NE{h, t}:
      1n+List.length(a, A, t)

# Template map, same shape as List.map (affine NonEmpty<A> = NonEmpty<&1, A>).
def NonEmpty.map(~A: Type, ~B: Type, ~f: A -> B, xs: NonEmpty<A>) -> NonEmpty<B>:
  match xs:
    case NE{h, t}:
      NE{f(h), List.map(~A, ~B, ~f, t)}

def NonEmpty.append(a, -A: Kind(a), xs: NonEmpty<a, A>, ys: NonEmpty<a, A>) ->
  NonEmpty<a, A>:
  match xs:
    case NE{h, t}:
      match ys:
        case NE{yh, yt}:
          NE{h, List.append(a, A, t, yh <> yt)}

def NonEmpty.snoc(a, -A: Kind(a), xs: NonEmpty<a, A>, y: A) -> NonEmpty<a, A>:
  match xs:
    case NE{h, t}:
      NE{h, List.append(a, A, t, y <> Nil{})}