import Base
import ./lib.bend as S

# to_list(empty) is Nil.
law to_list_empty:
  for -a: Quant
  for -A: Kind(a)
  { S.Stack.to_list(a, A, S.Stack.empty(a, A)) == Nil{} : List<a, A> }

# empty is S{Nil}.
law empty_is_s_nil:
  for -a: Quant
  for -A: Kind(a)
  { S.Stack.empty(a, A) == S.S{Nil{}} : S.Stack<a, A> }

# to_list(S{xs}) exposes the underlying list.
law to_list_s:
  for -a: Quant
  for -A: Kind(a)
  for xs: List<a, A>
  { S.Stack.to_list(a, A, S.S{xs}) == xs : List<a, A> }

# push places the new value at the list head.
law to_list_push:
  for -a: Quant
  for -A: Kind(a)
  for xs: List<a, A>
  for x: A
  { S.Stack.to_list(a, A, S.Stack.push(a, A, S.S{xs}, x)) == x <> xs : List<a, A> }

# push(empty, x) is S{x <> Nil}.
law push_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { S.Stack.push(a, A, S.Stack.empty(a, A), x) == S.S{x <> Nil{}} : S.Stack<a, A> }

# pop(push(empty, x)) recovers x and an empty rest.
law pop_push_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  {
    S.Stack.pop(a, A, S.Stack.push(a, A, S.Stack.empty(a, A), x))
      == Some{S.HD{x, S.Stack.empty(a, A)}}
    : Maybe<a, S.Stack.Pop<a, A>>
  }

# pop(push(s, x)) recovers x and s.
law pop_push:
  for -a: Quant
  for -A: Kind(a)
  for xs: List<a, A>
  for x: A
  {
    S.Stack.pop(a, A, S.Stack.push(a, A, S.S{xs}, x))
      == Some{S.HD{x, S.S{xs}}}
    : Maybe<a, S.Stack.Pop<a, A>>
  }

# pop on a concrete Cons recovers head/rest.
law pop_s_cons:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  { S.Stack.pop(a, A, S.S{h <> t}) == Some{S.HD{h, S.S{t}}} : Maybe<a, S.Stack.Pop<a, A>> }

# peek(push(s, x)) recovers x.
law peek_push:
  for -a: Quant
  for -A: Kind(a)
  for xs: List<a, A>
  for x: A
  { S.Stack.peek(a, A, S.Stack.push(a, A, S.S{xs}, x)) == Some{x} : Maybe<a, A> }

# peek(push(empty, x)) recovers x.
law peek_push_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { S.Stack.peek(a, A, S.Stack.push(a, A, S.Stack.empty(a, A), x)) == Some{x} : Maybe<a, A> }

# peek on Cons recovers head.
law peek_s_cons:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  { S.Stack.peek(a, A, S.S{h <> t}) == Some{h} : Maybe<a, A> }

# is_empty(empty) is true.
law is_empty_empty:
  for -a: Quant
  for -A: Kind(a)
  { S.Stack.is_empty(a, A, S.Stack.empty(a, A)) == True{} : Bool }

# is_empty(S{Nil}) is true.
law is_empty_s_nil:
  for -a: Quant
  for -A: Kind(a)
  { S.Stack.is_empty(a, A, S.S{Nil{}}) == True{} : Bool }

# is_empty after push is false.
law is_empty_push:
  for -a: Quant
  for -A: Kind(a)
  for xs: List<a, A>
  for x: A
  { S.Stack.is_empty(a, A, S.Stack.push(a, A, S.S{xs}, x)) == False{} : Bool }

# is_empty(S{h <> t}) is false.
law is_empty_s_cons:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  { S.Stack.is_empty(a, A, S.S{h <> t}) == False{} : Bool }

# length(empty) is 0.
law length_empty:
  for -a: Quant
  for -A: Kind(a)
  { S.Stack.length(a, A, S.Stack.empty(a, A)) == 0n : Nat }

# length(S{xs}) is List.length(xs).
law length_s:
  for -a: Quant
  for -A: Kind(a)
  for xs: List<a, A>
  { S.Stack.length(a, A, S.S{xs}) == List.length(a, A, xs) : Nat }

# length after push is one plus the prior list length.
law length_push:
  for -a: Quant
  for -A: Kind(a)
  for xs: List<a, A>
  for x: A
  {
    S.Stack.length(a, A, S.Stack.push(a, A, S.S{xs}, x))
      == 1n+List.length(a, A, xs)
    : Nat
  }

# length(push(empty, x)) is 1.
law length_push_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { S.Stack.length(a, A, S.Stack.push(a, A, S.Stack.empty(a, A), x)) == 1n : Nat }

# from_list puts the list directly in stack order.
law from_list_s:
  for -a: Quant
  for -A: Kind(a)
  for xs: List<a, A>
  { S.Stack.from_list(a, A, xs) == S.S{xs} : S.Stack<a, A> }

# to_list ∘ from_list is identity on lists.
law to_list_from_list:
  for -a: Quant
  for -A: Kind(a)
  for xs: List<a, A>
  { S.Stack.to_list(a, A, S.Stack.from_list(a, A, xs)) == xs : List<a, A> }

# from_list ∘ to_list is identity on stacks.
law from_list_to_list:
  for -a: Quant
  for -A: Kind(a)
  for xs: List<a, A>
  { S.Stack.from_list(a, A, S.Stack.to_list(a, A, S.S{xs})) == S.S{xs} : S.Stack<a, A> }

# from_list(Nil) roundtrips to empty via to_list.
law to_list_from_empty:
  for -a: Quant
  for -A: Kind(a)
  { S.Stack.to_list(a, A, S.Stack.from_list(a, A, Nil{})) == Nil{} : List<a, A> }

# pop(empty) is None.
law pop_empty:
  for -a: Quant
  for -A: Kind(a)
  { S.Stack.pop(a, A, S.Stack.empty(a, A)) == None{} : Maybe<a, S.Stack.Pop<a, A>> }

# peek(empty) is None.
law peek_empty:
  for -a: Quant
  for -A: Kind(a)
  { S.Stack.peek(a, A, S.Stack.empty(a, A)) == None{} : Maybe<a, A> }