import Base
import ./lib.bend as N

# When from_list succeeds on a Cons, the payload is that Cons as NE.
law from_list_cons:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  { N.NonEmpty.from_list(a, A, h <> t) == Some{N.NE{h, t}} : Maybe<a, N.NonEmpty<a, A>> }

# from_list on Nil is None.
law from_list_nil:
  for -a: Quant
  for -A: Kind(a)
  { N.NonEmpty.from_list(a, A, Nil{}) == None{} : Maybe<a, N.NonEmpty<a, A>> }

# to_list undoes the NE encoding: recovers head <> tail.
law to_list_ne:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  { N.NonEmpty.to_list(a, A, N.NE{h, t}) == h <> t : List<a, A> }

# to_list(one(x)) is the singleton list.
law to_list_one:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { N.NonEmpty.to_list(a, A, N.NonEmpty.one(a, A, x)) == x <> Nil{} : List<a, A> }

# from_list ∘ to_list recovers Some{NE{h,t}}.
law from_to_list_ne:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  {
    N.NonEmpty.from_list(a, A, N.NonEmpty.to_list(a, A, N.NE{h, t}))
      == Some{N.NE{h, t}}
    : Maybe<a, N.NonEmpty<a, A>>
  }

# length(NE{h,t}) is always Succ of List.length(t) (hence ≥ 1).
law length_succ_tail:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  { N.NonEmpty.length(a, A, N.NE{h, t}) == 1n+List.length(a, A, t) : Nat }

# length(one(x)) is 1.
law length_one:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { N.NonEmpty.length(a, A, N.NonEmpty.one(a, A, x)) == 1n : Nat }

# head(one(x)) is x.
law head_one:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { N.NonEmpty.head(a, A, N.NonEmpty.one(a, A, x)) == x : A }

# head/tail project the NE constructor.
law head_ne:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  { N.NonEmpty.head(a, A, N.NE{h, t}) == h : A }

law tail_ne:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  { N.NonEmpty.tail(a, A, N.NE{h, t}) == t : List<a, A> }

# tail(one(x)) is Nil.
law tail_one:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { N.NonEmpty.tail(a, A, N.NonEmpty.one(a, A, x)) == Nil{} : List<a, A> }

# one(x) is NE{x, Nil}.
law one_is_ne:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { N.NonEmpty.one(a, A, x) == N.NE{x, Nil{}} : N.NonEmpty<a, A> }

# cons(x, one(y)) prepends x.
law cons_one:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  for y: A
  { N.NonEmpty.cons(a, A, x, N.NonEmpty.one(a, A, y)) == N.NE{x, y <> Nil{}} : N.NonEmpty<a, A> }

# head(cons(x, one(y))) is x.
law head_cons_one:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  for y: A
  { N.NonEmpty.head(a, A, N.NonEmpty.cons(a, A, x, N.NonEmpty.one(a, A, y))) == x : A }

# to_list(cons(x, one(y))) is x <> y <> Nil.
law to_list_cons_one:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  for y: A
  {
    N.NonEmpty.to_list(a, A, N.NonEmpty.cons(a, A, x, N.NonEmpty.one(a, A, y)))
      == x <> (y <> Nil{})
    : List<a, A>
  }

# snoc(one(x), y) appends y.
law snoc_one:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  for y: A
  { N.NonEmpty.snoc(a, A, N.NonEmpty.one(a, A, x), y) == N.NE{x, y <> Nil{}} : N.NonEmpty<a, A> }

# length(snoc(one(x), y)) is 2.
law length_snoc_one:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  for y: A
  { N.NonEmpty.length(a, A, N.NonEmpty.snoc(a, A, N.NonEmpty.one(a, A, x), y)) == 2n : Nat }

# append(one(x), one(y)) is NE{x, y <> Nil}.
law append_ones:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  for y: A
  {
    N.NonEmpty.append(a, A, N.NonEmpty.one(a, A, x), N.NonEmpty.one(a, A, y))
      == N.NE{x, y <> Nil{}}
    : N.NonEmpty<a, A>
  }