import Base
import ./lib.bend as Q

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

# empty is Q{Nil, Nil}.
law empty_is_q_nil:
  for -a: Quant
  for -A: Kind(a)
  { Q.Queue.empty(a, A) == Q.Q{Nil{}, Nil{}} : Q.Queue<a, A> }

# to_list unfolds to front ++ reverse(rear).
law to_list_q:
  for -a: Quant
  for -A: Kind(a)
  for f: List<a, A>
  for r: List<a, A>
  { Q.Queue.to_list(a, A, Q.Q{f, r}) == List.append(a, A, f, List.reverse(a, A, r)) : List<a, A> }

# Enqueue on empty yields a singleton list in FIFO order.
law to_list_enqueue_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { Q.Queue.to_list(a, A, Q.Queue.enqueue(a, A, Q.Queue.empty(a, A), x)) == x <> Nil{} : List<a, A> }

# enqueue(empty, x) puts x on the rear.
law enqueue_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { Q.Queue.enqueue(a, A, Q.Queue.empty(a, A), x) == Q.Q{Nil{}, x <> Nil{}} : Q.Queue<a, A> }

# enqueue preserves front and conses onto rear.
law enqueue_q:
  for -a: Quant
  for -A: Kind(a)
  for f: List<a, A>
  for r: List<a, A>
  for x: A
  { Q.Queue.enqueue(a, A, Q.Q{f, r}, x) == Q.Q{f, x <> r} : Q.Queue<a, A> }

# dequeue(enqueue(empty, x)) recovers x and an empty rest.
law dequeue_enqueue_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  {
    Q.Queue.dequeue(a, A, Q.Queue.enqueue(a, A, Q.Queue.empty(a, A), x))
      == Some{Q.HD{x, Q.Queue.empty(a, A)}}
    : Maybe<a, Q.Queue.Deq<a, A>>
  }

# dequeue with nonempty front recovers head without rotating.
law dequeue_front_cons:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  for r: List<a, A>
  {
    Q.Queue.dequeue(a, A, Q.Q{h <> t, r})
      == Some{Q.HD{h, Q.Q{t, r}}}
    : Maybe<a, Q.Queue.Deq<a, A>>
  }

# dequeue(from_list(h <> t)) recovers h.
law dequeue_from_cons:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  {
    Q.Queue.dequeue(a, A, Q.Queue.from_list(a, A, h <> t))
      == Some{Q.HD{h, Q.Q{t, Nil{}}}}
    : Maybe<a, Q.Queue.Deq<a, A>>
  }

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

# peek(enqueue(empty, x)) recovers x.
law peek_enqueue_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { Q.Queue.peek(a, A, Q.Queue.enqueue(a, A, Q.Queue.empty(a, A), x)) == Some{x} : Maybe<a, A> }

# peek(from_list(h <> t)) recovers h.
law peek_from_cons:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  { Q.Queue.peek(a, A, Q.Queue.from_list(a, A, h <> t)) == Some{h} : Maybe<a, A> }

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

# length(Q{f,r}) is |f| + |r|.
law length_q:
  for -a: Quant
  for -A: Kind(a)
  for f: List<a, A>
  for r: List<a, A>
  {
    Q.Queue.length(a, A, Q.Q{f, r})
      == Nat.add(List.length(a, A, f), List.length(a, A, r))
    : Nat
  }

# length after enqueue on a concrete Q{f,r}: |f| + Succ(|r|).
law length_enqueue:
  for -a: Quant
  for -A: Kind(a)
  for f: List<a, A>
  for r: List<a, A>
  for x: A
  {
    Q.Queue.length(a, A, Q.Queue.enqueue(a, A, Q.Q{f, r}, x))
      == Nat.add(List.length(a, A, f), 1n+List.length(a, A, r))
    : Nat
  }

# length(enqueue(empty, x)) is 1.
law length_enqueue_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { Q.Queue.length(a, A, Q.Queue.enqueue(a, A, Q.Queue.empty(a, A), x)) == 1n : Nat }

# Definitional characterization of length(from_list(xs)).
law length_from_list_def:
  for -a: Quant
  for -A: Kind(a)
  for xs: List<a, A>
  {
    Q.Queue.length(a, A, Q.Queue.from_list(a, A, xs))
      == Nat.add(List.length(a, A, xs), List.length(a, A, Nil{}))
    : Nat
  }

# from_list puts the whole list in front.
law from_list_q:
  for -a: Quant
  for -A: Kind(a)
  for xs: List<a, A>
  { Q.Queue.from_list(a, A, xs) == Q.Q{xs, Nil{}} : Q.Queue<a, A> }

# Definitional characterization of to_list(from_list(xs)).
law to_list_from_list_def:
  for -a: Quant
  for -A: Kind(a)
  for xs: List<a, A>
  {
    Q.Queue.to_list(a, A, Q.Queue.from_list(a, A, xs))
      == List.append(a, A, xs, List.reverse(a, A, Nil{}))
    : List<a, A>
  }

# dequeue(empty) is None.
law dequeue_empty:
  for -a: Quant
  for -A: Kind(a)
  { Q.Queue.dequeue(a, A, Q.Queue.empty(a, A)) == None{} : Maybe<a, Q.Queue.Deq<a, A>> }

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

# is_empty(enqueue(empty, x)) is false.
law is_empty_enqueue_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { Q.Queue.is_empty(a, A, Q.Queue.enqueue(a, A, Q.Queue.empty(a, A), x)) == False{} : Bool }

# is_empty with nonempty front is false.
law is_empty_front_cons:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  for r: List<a, A>
  { Q.Queue.is_empty(a, A, Q.Q{h <> t, r}) == False{} : Bool }

# is_empty(from_list(Nil)) is true.
law is_empty_from_nil:
  for -a: Quant
  for -A: Kind(a)
  { Q.Queue.is_empty(a, A, Q.Queue.from_list(a, A, Nil{})) == True{} : Bool }

# is_empty(from_list(h <> t)) is false.
law is_empty_from_cons:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  { Q.Queue.is_empty(a, A, Q.Queue.from_list(a, A, h <> t)) == False{} : Bool }

# norm(empty) is empty.
law norm_empty:
  for -a: Quant
  for -A: Kind(a)
  { Q.Queue.norm(a, A, Q.Queue.empty(a, A)) == Q.Q{Nil{}, Nil{}} : Q.Queue<a, A> }

# norm with nonempty front is identity.
law norm_front_cons:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  for r: List<a, A>
  { Q.Queue.norm(a, A, Q.Q{h <> t, r}) == Q.Q{h <> t, r} : Q.Queue<a, A> }

# norm rotates a singleton rear into front.
law norm_rear_singleton:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { Q.Queue.norm(a, A, Q.Q{Nil{}, x <> Nil{}}) == Q.Q{x <> Nil{}, Nil{}} : Q.Queue<a, A> }