librarylibs/Check/src/Check.xtl
Check: assertions that report as text, for tests and teaching. Import it with an alias of your choice: "k:" u_se< "Check". Put libs/Check/src on XETAL_PATH ("just path"); the reference is libs/Check/docs. Names with l: are exported; those under h: are private to this file.
A check is a line of text, "ok" or "FAIL: ..." (X_eTaL has no assert and no way to stop with an error of your own yet): it prints when it is a statement, and checks join into a report with a_nd. 6 k:i_s '+ r_/ 1 2 3 # ok "sum" k:t_est 5 k:i_s '+ r_/ 1 2 3 # FAIL: sum: expected 5, got 6 k:r_eport (a k:a_nd b k:a_nd c) # the lines, then "3 checks, all passed"
ʰo̲neLine : Char -> Char
t, its newlines shown as ";", so a value takes one line.
ʰo̲neLine ← { t → m ← t = ʰn̲l @ ((r̲ange t̲ally t) + m × (1 + t̲ally t) − r̲ange t̲ally t) s̲elect t c̲at ";" }
ʰs̲hown : a -> Char
t on one line; when longer than 60 characters, its start and its shape: "1 2 3 ... (shape 100)".
ʰs̲hown ← { t → s ← ʰo̲neLine f̲ormat t 60 ≥ t̲ally s ? s (48 t̲ake s) c̲at " ... (shape " c̲at (f̲ormat s̲hape t) c̲at ")" }
ʰf̲ail : a -> b -> Char
ʰf̲ail ← { w g → "FAIL: expected " c̲at (ʰs̲hown w) c̲at ", got " c̲at ʰs̲hown g }
Checks
ˡi̲s : Match a => a -> a -> Char
want i_s got: ok when got has want's shape and items (m_atch).
ˡi̲s ← { w g → w m̲atch g ? "ok"◆ w ʰf̲ail g }
ˡn̲ear : Num a => a -> a -> Char
want n_ear got: ok when the shapes match and every item is equal within e_q~'s relative tolerance, or within 1e-12 of it (so a computed 1e-17 is near an exact 0, which e_q~ alone never allows).
ˡn̲ear ← { w g → n̲ot (s̲hape w) m̲atch s̲hape g ? w ʰf̲ail g '∧ r̲/ r̲avel (w e̲q~ g) ∨ 0.000000000001 ≥ a̲bs (f̲loat w) − f̲loat g ? "ok" w ʰf̲ail g }
ˡt̲rue : Truthy a => a -> Char
t_rue c: ok when every item of the condition c is true (1).
ˡt̲rue ← { c → '∧ r̲/ r̲avel c ? "ok"◆ "FAIL: expected true, got " c̲at ʰs̲hown c }
Naming a check
ˡt̲est : Char -> Char -> Char
name t_est line: the check's line, named: "ok: name" or "FAIL: name: ...".
ˡt̲est ← { name line → "ok" m̲atch 2 t̲ake line ? "ok: " c̲at name "FAIL: " c̲at name c̲at ": " c̲at 6 d̲rop line }
Reports
ˡa̲nd : Char -> Char -> Char
a a_nd b: two checks (or reports) as one text, a line each.
ˡa̲nd ← { a b → a c̲at "\n" c̲at b }
ˡc̲ount : Char -> Int
c_ount t: how many checks a text holds (its lines).
ˡc̲ount ← { t → 1 + t̲ally w̲here t = ʰn̲l @ }
ˡf̲ailures : Char -> Int
f_ailures t: how many of its checks failed (lines starting FAIL).
ˡf̲ailures ← { t → s ← (ʰn̲l @) c̲at t t̲ally w̲here (-1 d̲rop s = ʰn̲l @) ∧ (1 d̲rop s) = f̲irst "F" }
ˡp̲assed? : Truthy a => Char -> a
p_assed? t: whether every check passed.
ˡp̲assed? ← { t → 0 = ˡf̲ailures t }
ˡr̲eport : Char -> Char
r_eport t: the checks, then a summary line.
ˡr̲eport ← { t → n ← ˡc̲ount t f ← ˡf̲ailures t s ← (f̲ormat n) c̲at " check" c̲at (n ≠ 1) r̲eplicate "s" f = 0 ? t ˡa̲nd s c̲at ", all passed" t ˡa̲nd s c̲at ", " c̲at (f̲ormat f) c̲at " FAILED" }