import Base
import ./lib.bend as T

# empty is Leaf.
law empty_is_leaf:
  for -a: Quant
  for -A: Kind(a)
  { T.Tree.empty(a, A) == T.Leaf{} : T.Tree<a, A> }

# leaf is Leaf.
law leaf_is_leaf:
  for -a: Quant
  for -A: Kind(a)
  { T.Tree.leaf(a, A) == T.Leaf{} : T.Tree<a, A> }

# leaf equals empty.
law leaf_eq_empty:
  for -a: Quant
  for -A: Kind(a)
  { T.Tree.leaf(a, A) == T.Tree.empty(a, A) : T.Tree<a, A> }

# singleton is Node{Leaf, x, Leaf}.
law singleton_is_node:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { T.Tree.singleton(a, A, x) == T.Node{T.Leaf{}, x, T.Leaf{}} : T.Tree<a, A> }

# size(empty) is 0.
law size_empty:
  for -a: Quant
  for -A: Kind(a)
  { T.Tree.size(a, A, T.Tree.empty(a, A)) == 0n : Nat }

# size(Leaf) is 0.
law size_leaf:
  for -a: Quant
  for -A: Kind(a)
  { T.Tree.size(a, A, T.Leaf{}) == 0n : Nat }

# size(singleton(x)) is 1.
law size_singleton:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { T.Tree.size(a, A, T.Tree.singleton(a, A, x)) == 1n : Nat }

# size(Node{Leaf,x,Leaf}) is 1.
law size_node_leaves:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { T.Tree.size(a, A, T.Node{T.Leaf{}, x, T.Leaf{}}) == 1n : Nat }

# Definitional size of Node.
law size_node_def:
  for -a: Quant
  for -A: Kind(a)
  for l: T.Tree<a, A>
  for v: A
  for r: T.Tree<a, A>
  {
    T.Tree.size(a, A, T.Node{l, v, r})
      == 1n+Nat.add(T.Tree.size(a, A, l), T.Tree.size(a, A, r))
    : Nat
  }

# size(Node{Leaf, x, singleton(y)}) is 2.
law size_left_leaf_right_one:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  for y: A
  {
    T.Tree.size(a, A, T.Node{T.Leaf{}, x, T.Tree.singleton(a, A, y)})
      == 2n
    : Nat
  }

# size of balanced three-node tree is 3.
law size_both_singletons:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  for y: A
  for z: A
  {
    T.Tree.size(a, A, T.Node{T.Tree.singleton(a, A, x), y, T.Tree.singleton(a, A, z)})
      == 3n
    : Nat
  }

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

# to_list(Leaf) is Nil.
law to_list_leaf:
  for -a: Quant
  for -A: Kind(a)
  { T.Tree.to_list(a, A, T.Leaf{}) == Nil{} : List<a, A> }

# to_list(singleton(x)) is x <> Nil.
law to_list_singleton:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { T.Tree.to_list(a, A, T.Tree.singleton(a, A, x)) == x <> Nil{} : List<a, A> }

# to_list(Node{Leaf,x,Leaf}) is x <> Nil.
law to_list_node_leaves:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { T.Tree.to_list(a, A, T.Node{T.Leaf{}, x, T.Leaf{}}) == x <> Nil{} : List<a, A> }

# to_list with right singleton.
law to_list_right_one:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  for y: A
  {
    T.Tree.to_list(a, A, T.Node{T.Leaf{}, x, T.Tree.singleton(a, A, y)})
      == x <> (y <> Nil{})
    : List<a, A>
  }

# to_list with left singleton.
law to_list_left_one:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  for y: A
  {
    T.Tree.to_list(a, A, T.Node{T.Tree.singleton(a, A, x), y, T.Leaf{}})
      == x <> (y <> Nil{})
    : List<a, A>
  }

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

# is_empty(Leaf) is True.
law is_empty_leaf:
  for -a: Quant
  for -A: Kind(a)
  { T.Tree.is_empty(a, A, T.Leaf{}) == True{} : Bool }

# is_empty(singleton(x)) is False.
law is_empty_singleton:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { T.Tree.is_empty(a, A, T.Tree.singleton(a, A, x)) == False{} : Bool }

# is_empty(Node{...}) is False.
law is_empty_node:
  for -a: Quant
  for -A: Kind(a)
  for l: T.Tree<a, A>
  for v: A
  for r: T.Tree<a, A>
  { T.Tree.is_empty(a, A, T.Node{l, v, r}) == False{} : Bool }