Redesign test output to use logical quantifier symbols

Examples/Examples.lean

@@ -1,88 +1,125 @@
 import LSpec
 
+/-!
+# LSpec Examples
+
+This file provides comprehensive examples of using LSpec for testing in Lean 4.
+
+## Quick Reference
+
+| Function | Use Case | Output |
+|----------|----------|--------|
+| `test` | Unit tests | `✓ ∃: name` |
+| `check` | Property tests (simple) | `✓ ∃: name` |
+| `check'` | Property tests (with syntax) | `✓ ∃₁₀₀: "name" (property)` |
+| `checkIO` | Runtime property tests | Same as check |
+| `checkIO'` | Runtime tests (with syntax) | Same as check' |
+-/
+
 section LSpec
-/- In this section we demonstrate the basic usage of `LSpec`. -/
 
 open LSpec
 
-/- The simplest way to invoke `LSpec` is in a file via the `#lspec` command -/
+/-! ## Basic Usage
+
+The simplest way to run tests is with the `#lspec` command.
+-/
+
 #lspec test "Nat equality" (4 ≠ 5)
+-- ✓ ∃: Nat equality
 
-/-
-`#lspec` runs a sequence of tests which are encoded with the inductive type `TestSeq` which allows
-for tests to be composable
+/-!
+Tests can be composed into sequences using `$` or `++`.
+The output shows `✓ ∃:` for each passing unit test.
 -/
+
 #lspec test "bool equality" (42 == 42) $
-  test "list length" ([42].length = 2) $
+  test "list length" ([42].length = 2) $    -- This fails
   test "list nonempty" ¬ [42].isEmpty
+-- ✓ ∃: bool equality
+-- × ∃: list length
+--     Expected to be equal: '1' and '2'
+-- ✓ ∃: list nonempty
 
-/-
-Tests that can be tested are of the `Testable` typeclass, which have a low-priority instance
-`(p : Prop) : Decidable p → Testable p` which can be over-ridden to allow for more intricate
-failure or success messages.
+/-!
+## Bounded Universal Quantification
 
-This instance is generic enough that tests like `∀ n, n < 10 → n - 5 < 5` can be evaluated
+Tests like `∀ n, n < 10 → P n` are automatically iterated.
 -/
+
 #lspec test "all lt" $ ∀ n, n < 10 → n - 5 < 5
+-- ✓ ∃: all lt
 
-/-
-It is also possible to run tests inside the `IO` monad. The purpose of these tests is to plug in
-`LSpec` into a testing script for a `lake script`
--/
+/-!
+## IO-based Tests
 
-def fourIO : IO Nat :=
-  return 4
+For runtime tests, use `lspecIO` with a HashMap of test suites.
+-/
 
-def fiveIO : IO Nat :=
-  return 5
+def fourIO : IO Nat := return 4
+def fiveIO : IO Nat := return 5
 
 def main := do
   let four ← fourIO
   let five ← fiveIO
-  lspecIO $
+  lspecIO (.ofList [("IO tests", [
     test "fourIO equals 4" (four = 4) $
-    test "fiveIO equals 5" (five = 5)
+    test "fiveIO equals 5" (five = 5)])]) []
 
 #eval main
--- ✓ fourIO equals 4
--- ✓ fiveIO equals 5
+-- IO tests
+--   ✓ ∃: fourIO equals 4
+--   ✓ ∃: fiveIO equals 5
 -- 0
 
-/-
-There are even more ways to invoke LSpec tests (`lspecEachIO` for example) for more intricate moandic
-testing
- -/
-
 end LSpec
 
 section SlimCheck
-/-
-In this section we demonstrate the usage of `SlimCheck` in the Lspec library.
+/-!
+## Property-Based Testing with SlimCheck
+
+SlimCheck generates random test cases to verify properties.
+The output shows how many samples were tested.
+
+### Basic Property Tests
+
+Use `check` for simple output or `check'` to see the property syntax.
 -/
 
 open LSpec SlimCheck
 
-/-
-In this case `Nat` has a `SampleableExt` instance which allows the below examples to be run
--/
+-- Nat has a SampleableExt instance for random generation
 example : SampleableExt Nat := by infer_instance
 
-/- SlimCheck tests are invoked with `check`, and are composable in the same way `test` is -/
-#lspec check "add_comm" (∀ n m : Nat, n + m = m + n) $
-       check "mul_comm" $ ∀ n m : Nat, n * m = m * m
--- ? add_comm
--- × mul_comm
-
--- ===================
--- Found problems!
--- n := 1
--- m := 2
--- issue: 2 = 4 does not hold
--- (2 shrinks)
--- -------------------
-/-
-We can also apply Slimcheck to custom structures if we define the appropriate instances
+/-!
+### Using `check'` (Recommended)
+
+The `check'` macro captures the property syntax for display:
+- Success shows: `✓ ∃₁₀₀: "name" (∀ n m : Nat, n + m = m + n)`
+- Failure shows: `× ∃²/₁₀₀: "name" (property)` with counterexample
+
+The superscript indicates which sample failed, subscript shows total samples.
+-/
+
+#lspec check' "add_comm" (∀ n m : Nat, n + m = m + n)
+-- ✓ ∃₁₀₀: "add_comm" (∀ n m : Nat, n + m = m + n)
+
+#lspec check' "mul_comm_wrong" (∀ n m : Nat, n * m = m * m)
+-- × ∃⁶/₁₀₀: "mul_comm_wrong" (∀ n m : Nat, n * m = m * m)
+--     ===================
+--     Found problems!
+--     n := 1
+--     m := 2
+--     issue: 2 = 4 does not hold
+--     (2 shrinks)
+--     -------------------
+
+/-!
+### Custom Types with SlimCheck
+
+To use SlimCheck with custom types, define `Shrinkable` and `SampleableExt` instances.
 -/
+
 structure Pairs where
   left : Nat
   right : Nat
@@ -92,50 +129,40 @@ private def mkPairs (as : List α) (bs : List β) : List (α × β) :=
   let mkPairsAux (a : α) (bs : List β) : List (α × β) := bs.map fun b => (a, b)
   as.foldl (fun abs a => mkPairsAux a bs ++ abs) []
 
-/- An instance of `Shrinkable` is needed -/
+-- Shrinkable instance for reducing counterexamples
 open Shrinkable in
 instance : Shrinkable Pairs where
   shrink := fun p =>
     let shrinkl := shrink p.left
     let shrinkr := shrink p.right
     mkPairs shrinkl shrinkr |>.map fun (a, b) => ⟨a, b⟩
 
-/-
-As is one for `SampleableExt`.
-
-In both of these cases we are using the instances already written for more primitive types like
-`Nat`, but it's possible to write a these instances by hand if we want more fine-grained behavior.
--/
+-- SampleableExt instance for random generation
 open SampleableExt
 
 def pairsGen : Gen Pairs := return ⟨← Gen.chooseAny Nat, ← Gen.chooseAny Nat⟩
 
-/-
-To generate the instance of `SampleableExt α` we use the `mkSelfContained` function which relies only
-on having a `Gen α`.
-
-It is possible to define more tailored instances of `SampleableExt` by writing it by hand.
--/
 instance : SampleableExt Pairs := mkSelfContained pairsGen
 
-/- Now we can conduct the tests just as we did before for `Nat` -/
-#lspec check "left + 2 is less than right" $ ∀ pair : Pairs, pair.left + 2 ≤ pair.right
+-- Now we can test properties over Pairs
+#lspec check' "left + 2 ≤ right" (∀ pair : Pairs, pair.left + 2 ≤ pair.right)
+-- × ∃¹/₁₀₀: "left + 2 ≤ right" (∀ pair : Pairs, pair.left + 2 ≤ pair.right)
+--     ===================
+--     Found problems!
+--     pair := { left := 0, right := 1 }
+--     issue: 2 ≤ 1 does not hold
+--     ...
 
-/-
-You always have to be careful with your implementation for `shrink` and `SampleableExt` because
-Slimcheck may not flag tests that should fail, in this case `⟨0, 0⟩` should fail the test but
-isn't detected
--/
-#lspec check "left + right > right" $ ∀ pair : Pairs, pair.left + pair.right > pair.right
+-- This passes (but note: ⟨0, 0⟩ would fail, showing shrink limitations)
+#lspec check' "left + right > right" (∀ pair : Pairs, pair.left + pair.right > pair.right)
+-- ✓ ∃₁₀₀: "left + right > right" (∀ pair : Pairs, pair.left + pair.right > pair.right)
 
-/-
-## Gen.frequency - Weighted Random Generation
+/-!
+### Weighted Random Generation with Gen.frequency
 
-`Gen.frequency` allows you to choose from generators with weighted probability.
-This is useful when you want certain values to appear more often than others.
+`Gen.frequency` creates weighted random generators for more realistic test data.
 -/
 
-/-- A simple command type for testing -/
 inductive Command where
   | noop
   | read
@@ -144,11 +171,8 @@ inductive Command where
 deriving Repr, DecidableEq
 
 /--
-Using `Gen.frequency` to create weighted random commands:
-- noop: 10% chance
-- read: 50% chance
-- write: 30% chance
-- delete: 10% chance
+Weighted command generator:
+- noop: 10%, read: 50%, write: 30%, delete: 10%
 -/
 def commandGen : Gen Command :=
   Gen.frequency #[
@@ -163,23 +187,23 @@ instance : Shrinkable Command where
 
 instance : SampleableExt Command := mkSelfContained commandGen
 
--- Test that our generator produces valid commands (trivially true, but demonstrates usage)
-#lspec check "commands are valid" $ ∀ cmd : Command,
-  cmd = Command.noop ∨ cmd = Command.read ∨ cmd = Command.write ∨ cmd = Command.delete
+#lspec check' "commands are valid" (∀ cmd : Command,
+  cmd = Command.noop ∨ cmd = Command.read ∨ cmd = Command.write ∨ cmd = Command.delete)
+-- ✓ ∃₁₀₀: "commands are valid" (∀ cmd : Command, ...)
+
+/-!
+### Biased Number Generation
 
-/-
-Another example: generating numbers biased toward smaller values
+Generate numbers with custom distributions.
 -/
 
-/-- Generate numbers biased toward smaller values -/
 def biasedSmallGen : Gen Nat :=
   Gen.frequency #[
-    (5, Gen.choose Nat 0 10),     -- 50% chance: small numbers (0-10)
-    (3, Gen.choose Nat 11 100),   -- 30% chance: medium numbers (11-100)
-    (2, Gen.choose Nat 101 1000)  -- 20% chance: larger numbers (101-1000)
+    (5, Gen.choose Nat 0 10),     -- 50%: small (0-10)
+    (3, Gen.choose Nat 11 100),   -- 30%: medium (11-100)
+    (2, Gen.choose Nat 101 1000)  -- 20%: larger (101-1000)
   ] (pure 0)
 
-/-- A wrapper type to use our biased generator -/
 structure BiasedNat where
   val : Nat
 deriving Repr
@@ -189,7 +213,7 @@ instance : Shrinkable BiasedNat where
 
 instance : SampleableExt BiasedNat := mkSelfContained (BiasedNat.mk <$> biasedSmallGen)
 
--- Test with biased small numbers
-#lspec check "biased numbers are bounded" $ ∀ n : BiasedNat, n.val ≤ 1000
+#lspec check' "biased numbers bounded" (∀ n : BiasedNat, n.val ≤ 1000)
+-- ✓ ∃₁₀₀: "biased numbers bounded" (∀ n : BiasedNat, n.val ≤ 1000)
 
 end SlimCheck