import Base
import ./lib.bend as P

# empty is P{Nil}.
law empty_is_p_nil:
  { P.Prio.empty() == P.P{Nil{}} : P.Prio }

# to_list(empty) is Nil.
law to_list_empty:
  { P.Prio.to_list(P.Prio.empty()) == Nil{} : List<&2, U32> }

# to_list(P{xs}) exposes the list.
law to_list_p:
  for xs: List<&2, U32>
  { P.Prio.to_list(P.P{xs}) == xs : List<&2, U32> }

# push(empty, x) stores the singleton list.
law to_list_push_empty:
  for x: U32
  { P.Prio.to_list(P.Prio.push(P.Prio.empty(), x)) == x <> Nil{} : List<&2, U32> }

# peek_min(empty) is None.
law peek_empty:
  { P.Prio.peek_min(P.Prio.empty()) == None{} : Maybe<&2, U32> }

# peek_min(push(empty, x)) is x.
law peek_push_empty:
  for x: U32
  { P.Prio.peek_min(P.Prio.push(P.Prio.empty(), x)) == Some{x} : Maybe<&2, U32> }

# peek_min on a concrete Cons recovers the head (min when sorted).
law peek_p_cons:
  for h: U32
  for t: List<&2, U32>
  { P.Prio.peek_min(P.P{h <> t}) == Some{h} : Maybe<&2, U32> }

# pop_min(empty) is None.
law pop_empty:
  { P.Prio.pop_min(P.Prio.empty()) == None{} : Maybe<&2, P.Prio.Pop> }

# pop_min(push(empty, x)) returns x and empty.
law pop_push_empty:
  for x: U32
  {
    P.Prio.pop_min(P.Prio.push(P.Prio.empty(), x))
      == Some{P.PP{x, P.Prio.empty()}}
    : Maybe<&2, P.Prio.Pop>
  }

# pop_min on Cons recovers head/rest.
law pop_p_cons:
  for h: U32
  for t: List<&2, U32>
  { P.Prio.pop_min(P.P{h <> t}) == Some{P.PP{h, P.P{t}}} : Maybe<&2, P.Prio.Pop> }

# size(empty) is 0.
law size_empty:
  { P.Prio.size(P.Prio.empty()) == 0n : Nat }

# size(P{xs}) is List.length(xs).
law size_p:
  for xs: List<&2, U32>
  { P.Prio.size(P.P{xs}) == List.length(&2, U32, xs) : Nat }

# size(push(empty, x)) is 1.
law size_push_empty:
  for x: U32
  { P.Prio.size(P.Prio.push(P.Prio.empty(), x)) == 1n : Nat }

# is_empty(empty) is True.
law is_empty_empty:
  { P.Prio.is_empty(P.Prio.empty()) == True{} : Bool }

law is_empty_p_nil:
  { P.Prio.is_empty(P.P{Nil{}}) == True{} : Bool }

law is_empty_p_cons:
  for h: U32
  for t: List<&2, U32>
  { P.Prio.is_empty(P.P{h <> t}) == False{} : Bool }

law is_empty_push:
  for x: U32
  { P.Prio.is_empty(P.Prio.push(P.Prio.empty(), x)) == False{} : Bool }

# from_list(Nil) is empty.
law from_list_empty:
  { P.Prio.from_list(Nil{}) == P.Prio.empty() : P.Prio }

# from_list(singleton) is the singleton bag.
law from_list_singleton:
  for x: U32
  { P.Prio.from_list(x <> Nil{}) == P.Prio.push(P.Prio.empty(), x) : P.Prio }

# insert into Nil yields singleton.
law insert_nil:
  for x: U32
  { P.Prio.insert(Nil{}, x) == x <> Nil{} : List<&2, U32> }

# Concrete ordering: push 2 then 1 sorts ascending.
law push_two_ordered:
  {
    P.Prio.to_list(P.Prio.push(P.Prio.push(P.Prio.empty(), 2), 1))
      == 1 <> (2 <> Nil{})
    : List<&2, U32>
  }

# Concrete ordering: push 1 then 2 stays ascending.
law push_two_same_order:
  {
    P.Prio.to_list(P.Prio.push(P.Prio.push(P.Prio.empty(), 1), 2))
      == 1 <> (2 <> Nil{})
    : List<&2, U32>
  }

# peek_min of two pushed values is the smaller.
law peek_two_min:
  {
    P.Prio.peek_min(P.Prio.push(P.Prio.push(P.Prio.empty(), 5), 3))
      == Some{3}
    : Maybe<&2, U32>
  }

# size after two pushes is 2.
law size_two:
  {
    P.Prio.size(P.Prio.push(P.Prio.push(P.Prio.empty(), 1), 2))
      == 2n
    : Nat
  }

# from_list sorts into nondecreasing order (concrete).
law from_list_two:
  {
    P.Prio.to_list(P.Prio.from_list(2 <> (1 <> Nil{})))
      == 1 <> (2 <> Nil{})
    : List<&2, U32>
  }