import Base
import ./lib.bend as Bs

# Empty is represented by no words.
law to_words_empty:
  { Bs.BitSet.to_words(Bs.BitSet.empty()) == Nil{} : List<&2, U32> }

law is_empty_empty:
  { Bs.BitSet.is_empty(Bs.BitSet.empty()) == True{} : Bool }

law size_empty:
  { Bs.BitSet.size(Bs.BitSet.empty()) == 0n : Nat }

law to_list_empty:
  { Bs.BitSet.to_list(Bs.BitSet.empty()) == Nil{} : List<&2, Nat> }

law contains_empty:
  { Bs.BitSet.contains(Bs.BitSet.empty(), 0n) == False{} : Bool }

# The lowest bit is the first singleton.
law singleton_zero_words:
  { Bs.BitSet.to_words(Bs.BitSet.singleton(0n)) == 1 <> Nil{} : List<&2, U32> }

law singleton_zero_list:
  { Bs.BitSet.to_list(Bs.BitSet.singleton(0n)) == 0n <> Nil{} : List<&2, Nat> }

law singleton_zero_size:
  { Bs.BitSet.size(Bs.BitSet.singleton(0n)) == 1n : Nat }

law singleton_zero_contains:
  { Bs.BitSet.contains(Bs.BitSet.singleton(0n), 0n) == True{} : Bool }

law remove_singleton_zero:
  { Bs.BitSet.remove(Bs.BitSet.singleton(0n), 0n) == Bs.BitSet.empty() : Bs.BitSet }

law insert_singleton_idempotent:
  { Bs.BitSet.insert(Bs.BitSet.singleton(0n), 0n)
      == Bs.BitSet.singleton(0n) : Bs.BitSet }

law union_empty_singleton:
  { Bs.BitSet.union(Bs.BitSet.empty(), Bs.BitSet.singleton(0n))
      == Bs.BitSet.singleton(0n) : Bs.BitSet }

law intersect_empty_singleton:
  { Bs.BitSet.intersect(Bs.BitSet.empty(), Bs.BitSet.singleton(0n))
      == Bs.BitSet.empty() : Bs.BitSet }

# Small boundary cases exercise the word layout.
law singleton_one_words:
  { Bs.BitSet.to_words(Bs.BitSet.singleton(1n)) == 2 <> Nil{} : List<&2, U32> }

law singleton_one_list:
  { Bs.BitSet.to_list(Bs.BitSet.singleton(1n)) == 1n <> Nil{} : List<&2, Nat> }

law singleton_thirty_one:
  { Bs.BitSet.to_list(Bs.BitSet.singleton(31n)) == 31n <> Nil{} : List<&2, Nat> }

law singleton_thirty_two_words:
  { Bs.BitSet.to_words(Bs.BitSet.singleton(32n)) == 0 <> 1 <> Nil{} : List<&2, U32> }

law singleton_thirty_two_list:
  { Bs.BitSet.to_list(Bs.BitSet.singleton(32n)) == 32n <> Nil{} : List<&2, Nat> }

law contains_absent_singleton:
  { Bs.BitSet.contains(Bs.BitSet.singleton(0n), 1n) == False{} : Bool }

law insert_zero_empty:
  { Bs.BitSet.insert(Bs.BitSet.empty(), 0n) == Bs.BitSet.singleton(0n) : Bs.BitSet }

law insert_thirty_two_empty:
  { Bs.BitSet.insert(Bs.BitSet.empty(), 32n)
      == Bs.BitSet.singleton(32n) : Bs.BitSet }

law remove_absent_empty:
  { Bs.BitSet.remove(Bs.BitSet.empty(), 32n) == Bs.BitSet.empty() : Bs.BitSet }

law remove_other_singleton:
  { Bs.BitSet.remove(Bs.BitSet.singleton(0n), 1n)
      == Bs.BitSet.singleton(0n) : Bs.BitSet }

law remove_one_from_two:
  { Bs.BitSet.remove(Bs.BitSet.insert(Bs.BitSet.singleton(0n), 1n), 0n)
      == Bs.BitSet.singleton(1n) : Bs.BitSet }

law union_two_bits:
  { Bs.BitSet.to_list(Bs.BitSet.union(Bs.BitSet.singleton(0n), Bs.BitSet.singleton(1n)))
      == 0n <> 1n <> Nil{} : List<&2, Nat> }

law union_across_words:
  { Bs.BitSet.to_words(Bs.BitSet.union(Bs.BitSet.singleton(0n), Bs.BitSet.singleton(32n)))
      == 1 <> 1 <> Nil{} : List<&2, U32> }

law intersect_disjoint:
  { Bs.BitSet.intersect(Bs.BitSet.singleton(0n), Bs.BitSet.singleton(1n))
      == Bs.BitSet.empty() : Bs.BitSet }

law intersect_same:
  { Bs.BitSet.intersect(Bs.BitSet.singleton(32n), Bs.BitSet.singleton(32n))
      == Bs.BitSet.singleton(32n) : Bs.BitSet }

law from_words_trims_zero_tail:
  { Bs.BitSet.from_words(1 <> 0 <> Nil{})
      == Bs.BitSet.from_words(1 <> Nil{}) : Bs.BitSet }

law from_words_zero_is_empty:
  { Bs.BitSet.from_words(0 <> 0 <> Nil{}) == Bs.BitSet.empty() : Bs.BitSet }

law u32_singleton_wrapper:
  { Bs.BitSet.singleton_u32(0) == Bs.BitSet.singleton(0n) : Bs.BitSet }

law u32_insert_wrapper:
  { Bs.BitSet.insert_u32(Bs.BitSet.empty(), 32)
      == Bs.BitSet.singleton(32n) : Bs.BitSet }