import Base
import ./lib.bend as DQ

# empty is D{Nil, Nil}.
law empty_is_d_nil:
  for -a: Quant
  for -A: Kind(a)
  { DQ.Deque.empty(a, A) == DQ.D{Nil{}, Nil{}} : DQ.Deque<a, A> }

# Empty has no front element.
law peek_front_empty:
  for -a: Quant
  for -A: Kind(a)
  { DQ.Deque.peek_front(a, A, DQ.Deque.empty(a, A)) == None{} : Maybe<a, A> }

# Empty has no back element.
law peek_back_empty:
  for -a: Quant
  for -A: Kind(a)
  { DQ.Deque.peek_back(a, A, DQ.Deque.empty(a, A)) == None{} : Maybe<a, A> }

# Empty pops from either end to None.
law pop_front_empty:
  for -a: Quant
  for -A: Kind(a)
  { DQ.Deque.pop_front(a, A, DQ.Deque.empty(a, A)) == None{} : Maybe<a, DQ.Deque.Pop<a, A>> }

law pop_back_empty:
  for -a: Quant
  for -A: Kind(a)
  { DQ.Deque.pop_back(a, A, DQ.Deque.empty(a, A)) == None{} : Maybe<a, DQ.Deque.Pop<a, A>> }

law to_list_empty:
  for -a: Quant
  for -A: Kind(a)
  { DQ.Deque.to_list(a, A, DQ.Deque.empty(a, A)) == Nil{} : List<a, A> }

law length_empty:
  for -a: Quant
  for -A: Kind(a)
  { DQ.Deque.length(a, A, DQ.Deque.empty(a, A)) == 0n : Nat }

law is_empty_empty:
  for -a: Quant
  for -A: Kind(a)
  { DQ.Deque.is_empty(a, A, DQ.Deque.empty(a, A)) == True{} : Bool }

# Definitional characterization of the two-list order.
law to_list_d:
  for -a: Quant
  for -A: Kind(a)
  for f: List<a, A>
  for r: List<a, A>
  { DQ.Deque.to_list(a, A, DQ.D{f, r}) == List.append(a, A, f, List.reverse(a, A, r)) : List<a, A> }

law length_d:
  for -a: Quant
  for -A: Kind(a)
  for f: List<a, A>
  for r: List<a, A>
  {
    DQ.Deque.length(a, A, DQ.D{f, r})
      == Nat.add(List.length(a, A, f), List.length(a, A, r))
    : Nat
  }

law from_list_d:
  for -a: Quant
  for -A: Kind(a)
  for xs: List<a, A>
  { DQ.Deque.from_list(a, A, xs) == DQ.D{xs, Nil{}} : DQ.Deque<a, A> }

law from_list_empty:
  for -a: Quant
  for -A: Kind(a)
  { DQ.Deque.from_list(a, A, Nil{}) == DQ.Deque.empty(a, A) : DQ.Deque<a, A> }

law from_list_singleton_roundtrip:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.to_list(a, A, DQ.Deque.from_list(a, A, x <> Nil{})) == x <> Nil{} : List<a, A> }

law push_front_d:
  for -a: Quant
  for -A: Kind(a)
  for f: List<a, A>
  for r: List<a, A>
  for x: A
  { DQ.Deque.push_front(a, A, DQ.D{f, r}, x) == DQ.D{x <> f, r} : DQ.Deque<a, A> }

law push_back_d:
  for -a: Quant
  for -A: Kind(a)
  for f: List<a, A>
  for r: List<a, A>
  for x: A
  { DQ.Deque.push_back(a, A, DQ.D{f, r}, x) == DQ.D{f, x <> r} : DQ.Deque<a, A> }

# Pushing at either end produces the same singleton order.
law push_front_singleton:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.to_list(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x)) == x <> Nil{} : List<a, A> }

law push_back_singleton:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.to_list(a, A, DQ.Deque.push_back(a, A, DQ.Deque.empty(a, A), x)) == x <> Nil{} : List<a, A> }

law length_push_front_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.length(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x)) == 1n : Nat }

law length_push_back_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.length(a, A, DQ.Deque.push_back(a, A, DQ.Deque.empty(a, A), x)) == 1n : Nat }

law is_empty_push_front:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.is_empty(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x)) == False{} : Bool }

law is_empty_push_back:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.is_empty(a, A, DQ.Deque.push_back(a, A, DQ.Deque.empty(a, A), x)) == False{} : Bool }

law peek_front_push_front:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.peek_front(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x)) == Some{x} : Maybe<a, A> }

law peek_back_push_back:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.peek_back(a, A, DQ.Deque.push_back(a, A, DQ.Deque.empty(a, A), x)) == Some{x} : Maybe<a, A> }

law peek_front_push_back:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.peek_front(a, A, DQ.Deque.push_back(a, A, DQ.Deque.empty(a, A), x)) == Some{x} : Maybe<a, A> }

law peek_back_push_front:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.peek_back(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x)) == Some{x} : Maybe<a, A> }

# Singleton pops recover the value and an empty deque.
law pop_front_push_front_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.pop_front(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x)) == Some{DQ.P{x, DQ.Deque.empty(a, A)}} : Maybe<a, DQ.Deque.Pop<a, A>> }

law pop_front_push_back_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.pop_front(a, A, DQ.Deque.push_back(a, A, DQ.Deque.empty(a, A), x)) == Some{DQ.P{x, DQ.Deque.empty(a, A)}} : Maybe<a, DQ.Deque.Pop<a, A>> }

law pop_back_push_back_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.pop_back(a, A, DQ.Deque.push_back(a, A, DQ.Deque.empty(a, A), x)) == Some{DQ.P{x, DQ.Deque.empty(a, A)}} : Maybe<a, DQ.Deque.Pop<a, A>> }

law pop_back_push_front_empty:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.pop_back(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x)) == Some{DQ.P{x, DQ.Deque.empty(a, A)}} : Maybe<a, DQ.Deque.Pop<a, A>> }

law pop_front_cons:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  for r: List<a, A>
  {
    DQ.Deque.pop_front(a, A, DQ.D{h <> t, r})
      == Some{DQ.P{h, DQ.D{t, r}}}
    : Maybe<a, DQ.Deque.Pop<a, A>>
  }

law pop_back_cons:
  for -a: Quant
  for -A: Kind(a)
  for f: List<a, A>
  for h: A
  for t: List<a, A>
  {
    DQ.Deque.pop_back(a, A, DQ.D{f, h <> t})
      == Some{DQ.P{h, DQ.D{f, t}}}
    : Maybe<a, DQ.Deque.Pop<a, A>>
  }

law norm_front_cons:
  for -a: Quant
  for -A: Kind(a)
  for h: A
  for t: List<a, A>
  for r: List<a, A>
  { DQ.Deque.norm_front(a, A, DQ.D{h <> t, r}) == DQ.D{h <> t, r} : DQ.Deque<a, A> }

law norm_back_cons:
  for -a: Quant
  for -A: Kind(a)
  for f: List<a, A>
  for h: A
  for t: List<a, A>
  { DQ.Deque.norm_back(a, A, DQ.D{f, h <> t}) == DQ.D{f, h <> t} : DQ.Deque<a, A> }

law norm_front_rear_one:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.norm_front(a, A, DQ.D{Nil{}, x <> Nil{}}) == DQ.D{x <> Nil{}, Nil{}} : DQ.Deque<a, A> }

law norm_back_front_one:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  { DQ.Deque.norm_back(a, A, DQ.D{x <> Nil{}, Nil{}}) == DQ.D{Nil{}, x <> Nil{}} : DQ.Deque<a, A> }

# push_front then push_back order.
law to_list_front_then_back:
  for -a: Quant
  for -A: Kind(a)
  for x: A
  for y: A
  {
    DQ.Deque.to_list(a, A,
      DQ.Deque.push_back(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x), y))
      == x <> (y <> Nil{})
    : List<a, A>
  }