import Base
import ./lib.bend as T

# pass is True.
law pass_true:
  { T.Test.pass() == True{} : Bool }

# fail is False.
law fail_false:
  { T.Test.fail() == False{} : Bool }

# check is the identity on Bool.
law check_id:
  for b: Bool
  { T.Test.check(b) == b : Bool }

# all(Nil) is True (vacuous).
law all_nil:
  { T.Test.all(Nil{}) == True{} : Bool }

# all(True <> Nil) is True.
law all_true_one:
  { T.Test.all(True{} <> Nil{}) == True{} : Bool }

# all(False <> Nil) is False.
law all_false_one:
  { T.Test.all(False{} <> Nil{}) == False{} : Bool }

# all(True <> True <> Nil) is True.
law all_true_true:
  { T.Test.all(True{} <> True{} <> Nil{}) == True{} : Bool }

# all(True <> False <> Nil) is False.
law all_true_false:
  { T.Test.all(True{} <> False{} <> Nil{}) == False{} : Bool }

# and_list is Test.all.
law and_list_all:
  for xs: List<&2, Bool>
  { T.Test.and_list(xs) == T.Test.all(xs) : Bool }

# eq_u32(0, 0) is True.
law eq_u32_zero:
  { T.Test.eq_u32(0, 0) == True{} : Bool }

# eq_u32(1, 2) is False.
law eq_u32_ne:
  { T.Test.eq_u32(1, 2) == False{} : Bool }

# eq_bool(True, True) is True.
law eq_bool_tt:
  { T.Test.eq_bool(True{}, True{}) == True{} : Bool }

# eq_bool(True, False) is False.
law eq_bool_tf:
  { T.Test.eq_bool(True{}, False{}) == False{} : Bool }

# eq_nat(0, 0) is True.
law eq_nat_zero:
  { T.Test.eq_nat(0n, 0n) == True{} : Bool }

# eq_string("", "") is True.
law eq_string_empty:
  { T.Test.eq_string("", "") == True{} : Bool }

# eq_string("a", "b") is False.
law eq_string_ne:
  { T.Test.eq_string("a", "b") == False{} : Bool }

# suite(Nil) is True.
law suite_nil:
  { T.Test.suite(Nil{}) == True{} : Bool }

# suite of one passing case is True.
law suite_one_pass:
  { T.Test.suite(T.Case{"ok", True{}} <> Nil{}) == True{} : Bool }

# suite of one failing case is False.
law suite_one_fail:
  { T.Test.suite(T.Case{"bad", False{}} <> Nil{}) == False{} : Bool }

# case_ok recovers the Bool payload.
law case_ok_payload:
  for n: String
  for b: Bool
  { T.Test.case_ok(T.Case{n, b}) == b : Bool }

# Test.case builds Case{name, ok}.
law case_ctor:
  for n: String
  for b: Bool
  { T.Test.case(n, b) == T.Case{n, b} : T.Test.Case }

# all(False <> True <> Nil) is False.
law all_false_true:
  { T.Test.all(False{} <> True{} <> Nil{}) == False{} : Bool }

# all of three Trues is True.
law all_three_true:
  { T.Test.all(True{} <> True{} <> True{} <> Nil{}) == True{} : Bool }

# eq_bool(False, False) is True.
law eq_bool_ff:
  { T.Test.eq_bool(False{}, False{}) == True{} : Bool }

# eq_bool(False, True) is False.
law eq_bool_ft:
  { T.Test.eq_bool(False{}, True{}) == False{} : Bool }

# eq_nat(1, 1) is True.
law eq_nat_one:
  { T.Test.eq_nat(1n, 1n) == True{} : Bool }

# eq_nat(0, 1) is False.
law eq_nat_ne:
  { T.Test.eq_nat(0n, 1n) == False{} : Bool }

# eq_u32(1, 1) is True.
law eq_u32_one:
  { T.Test.eq_u32(1, 1) == True{} : Bool }

# eq_string("a", "a") is True.
law eq_string_aa:
  { T.Test.eq_string("a", "a") == True{} : Bool }

# suite of two passing cases is True.
law suite_two_pass:
  {
    T.Test.suite(T.Case{"a", True{}} <> T.Case{"b", True{}} <> Nil{})
      == True{}
    : Bool
  }

# suite with a failure is False.
law suite_pass_fail:
  {
    T.Test.suite(T.Case{"a", True{}} <> T.Case{"b", False{}} <> Nil{})
      == False{}
    : Bool
  }

# check on concrete Bools.
law check_true:
  { T.Test.check(True{}) == True{} : Bool }

law check_false:
  { T.Test.check(False{}) == False{} : Bool }

# case_ok ∘ case recovers the Bool.
law case_ok_via_case:
  for n: String
  for b: Bool
  { T.Test.case_ok(T.Test.case(n, b)) == b : Bool }