# Test — small Bool-check / proof-suite helper for Bend.
# Publish entry for this package. Depends only on Base.
#
# Complements LAWS.bend + PROOF.bend: those are definitional equality proofs
# (`bend PROOF.bend`). This module is for Bool-valued checklists that smoke
# mains and HubLens-style badges can fold at runtime.
#
# Base has no Test module (bend base Test → missing). Zero @unsafe.
#
# Typical use:
#   import ./lib.bend as T
#   ok = T.Test.all(T.Test.eq_u32(1, 1) <> T.Test.eq_string("a", "a") <> Nil{})
#   ok2 = T.Test.suite(T.Case{"len", Nat.is_eq(n, 3n)} <> Nil{})
# Alongside proofs: keep LAWS.bend / PROOF.bend for algebraic identities;
# use Test.* for executable Bool gates in main / CI badges.
import Base

# ---- constants / check gate ----------------------------------------------

def Test.pass() -> Bool:
  True{}

def Test.fail() -> Bool:
  False{}

# Identity on a Bool — documents a check at the call site.
def Test.check(b: Bool) -> Bool:
  b

# ---- equality asserts (thin Base facades) --------------------------------

def Test.eq_bool(a: Bool, b: Bool) -> Bool:
  Cmp.is_eq(Bool.cmp(a, b))

def Test.eq_u32(+a: U32, +b: U32) -> Bool:
  U32.is_eq(a, b)

def Test.eq_nat(a: Nat, b: Nat) -> Bool:
  Nat.is_eq(a, b)

def Test.eq_string(a: String, b: String) -> Bool:
  String.eq(a, b)

# ---- folding Bool lists --------------------------------------------------

# Conjunction of Bool checks. Empty list succeeds (vacuous True).
def Test.all(xs: List<&2, Bool>) -> Bool:
  List.all(~&2, ~Bool, ~(b => b), xs)

def Test.and_list(xs: List<&2, Bool>) -> Bool:
  Test.all(xs)

# ---- named suite ---------------------------------------------------------
# Case is Data (String & Bool), so lists are Kind(&2)-friendly.

type Test.Case is Data:
  Case{name: String, ok: Bool}

def Test.case(name: String, ok: Bool) -> Test.Case:
  Case{name, ok}

def Test.case_ok(c: Test.Case) -> Bool:
  match c:
    case Case{n, b}:
      b

# Fold named cases to a single Bool (ignores names; names are for readers /
# smoke printing). Empty suite succeeds.
def Test.suite(cases: List<&2, Test.Case>) -> Bool:
  List.all(~&2, ~Test.Case, ~(c => Test.case_ok(c)), cases)