import Base
import ./lib.bend as R

# Bound and constructor semantics.
law bound_inclusive:
  { R.Range.Bound.is_inclusive(R.Inclusive{}) == True{} : Bool }

law bound_exclusive:
  { R.Range.Bound.is_inclusive(R.Exclusive{}) == False{} : Bool }

law nat_make:
  { R.Range.make(2n, R.Inclusive{}, 5n, R.Exclusive{})
      == R.NR{2n, R.Inclusive{}, 5n, R.Exclusive{}} : R.Range.NatRange }

law nat_closed:
  { R.Range.Nat.closed(2n, 5n) == R.NR{2n, R.Inclusive{}, 5n, R.Inclusive{}}
      : R.Range.NatRange }

law u32_make:
  { R.Range.make_u32(2, R.Inclusive{}, 5, R.Exclusive{})
      == R.UR{2, R.Inclusive{}, 5, R.Exclusive{}} : R.Range.U32Range }

# Nat endpoint semantics, emptiness, cardinality, and enumeration.
law nat_closed_open:
  { R.Range.Nat.to_list(R.Range.Nat.closed_open(2n, 5n))
      == 2n <> 3n <> 4n <> Nil{} : List<&2, Nat> }

law nat_closed_open_length:
  { R.Range.Nat.length(R.Range.Nat.closed_open(2n, 5n)) == 3n : Nat }

law nat_open_closed:
  { R.Range.Nat.to_list(R.Range.Nat.open_closed(2n, 5n))
      == 3n <> 4n <> 5n <> Nil{} : List<&2, Nat> }

law nat_open:
  { R.Range.Nat.to_list(R.Range.Nat.open(2n, 5n))
      == 3n <> 4n <> Nil{} : List<&2, Nat> }

law nat_singleton:
  { R.Range.Nat.length(R.Range.Nat.closed(4n, 4n)) == 1n : Nat }

law nat_open_singleton_empty:
  { R.Range.Nat.is_empty(R.Range.Nat.open(4n, 4n)) == True{} : Bool }

law nat_reversed_empty:
  { R.Range.Nat.to_list(R.Range.Nat.closed(5n, 2n)) == Nil{} : List<&2, Nat> }

law nat_contains_inside:
  { R.Range.Nat.contains(R.Range.Nat.closed_open(2n, 5n), 4n)
      == True{} : Bool }

law nat_contains_excluded_upper:
  { R.Range.Nat.contains(R.Range.Nat.closed_open(2n, 5n), 5n)
      == False{} : Bool }

law nat_contains_excluded_lower:
  { R.Range.Nat.contains(R.Range.Nat.open_closed(2n, 5n), 2n)
      == False{} : Bool }

law nat_overlap_touch_closed:
  { R.Range.Nat.overlap(R.Range.Nat.closed(1n, 3n), R.Range.Nat.closed(3n, 5n))
      == True{} : Bool }

law nat_overlap_touch_open:
  { R.Range.Nat.overlaps(R.Range.Nat.closed(1n, 3n), R.Range.Nat.open(3n, 5n))
      == False{} : Bool }

law nat_overlap_disjoint:
  { R.Range.Nat.overlap(R.Range.Nat.closed(1n, 2n), R.Range.Nat.closed(3n, 5n))
      == False{} : Bool }

law nat_clamp_low:
  { R.Range.Nat.clamp(R.Range.Nat.closed(2n, 5n), 0n) == 2n : Nat }

law nat_clamp_mid:
  { R.Range.Nat.clamp(R.Range.Nat.closed(2n, 5n), 4n) == 4n : Nat }

law nat_clamp_high:
  { R.Range.Nat.clamp(R.Range.Nat.closed(2n, 5n), 9n) == 5n : Nat }

# U32 has the same endpoint semantics and uses Nat for its length.
law u32_closed_open_length:
  { R.Range.U32.length(R.Range.U32.closed_open(2, 5)) == 3n : Nat }

law u32_closed_open_list:
  { R.Range.U32.to_list(R.Range.U32.closed_open(2, 5))
      == 2 <> 3 <> 4 <> Nil{} : List<&2, U32> }

law u32_open_list:
  { R.Range.U32.to_list(R.Range.U32.open(2, 5))
      == 3 <> 4 <> Nil{} : List<&2, U32> }

law u32_singleton:
  { R.Range.U32.length(R.Range.U32.closed(7, 7)) == 1n : Nat }

law u32_open_singleton_empty:
  { R.Range.U32.is_empty(R.Range.U32.open(7, 7)) == True{} : Bool }

law u32_contains_inside:
  { R.Range.U32.contains(R.Range.U32.closed_open(2, 5), 4)
      == True{} : Bool }

law u32_contains_excluded_upper:
  { R.Range.U32.contains(R.Range.U32.closed_open(2, 5), 5)
      == False{} : Bool }

law u32_overlap_touch_open:
  { R.Range.U32.overlap(R.Range.U32.closed(1, 3), R.Range.U32.open(3, 5))
      == False{} : Bool }

law u32_overlap_disjoint:
  { R.Range.U32.overlaps(R.Range.U32.closed(1, 2), R.Range.U32.closed(3, 5))
      == False{} : Bool }

law u32_clamp_low:
  { R.Range.U32.clamp(R.Range.U32.closed(2, 5), 0) == 2 : U32 }

law u32_clamp_high:
  { R.Range.U32.clamp(R.Range.U32.closed(2, 5), 9) == 5 : U32 }