Quality of Life Improvments

Examples/Examples.lean

@@ -128,4 +128,68 @@ isn't detected
 -/
 #lspec check "left + right > right" $ ∀ pair : Pairs, pair.left + pair.right > pair.right
 
+/-
+## Gen.frequency - Weighted Random Generation
+
+`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.
+-/
+
+/-- A simple command type for testing -/
+inductive Command where
+  | noop
+  | read
+  | write
+  | delete
+deriving Repr, DecidableEq
+
+/--
+Using `Gen.frequency` to create weighted random commands:
+- noop: 10% chance
+- read: 50% chance
+- write: 30% chance
+- delete: 10% chance
+-/
+def commandGen : Gen Command :=
+  Gen.frequency #[
+    (1, pure Command.noop),
+    (5, pure Command.read),
+    (3, pure Command.write),
+    (1, pure Command.delete)
+  ] (pure Command.noop)
+
+instance : Shrinkable Command where
+  shrink := fun _ => []
+
+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
+
+/-
+Another example: generating numbers biased toward smaller values
+-/
+
+/-- 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)
+  ] (pure 0)
+
+/-- A wrapper type to use our biased generator -/
+structure BiasedNat where
+  val : Nat
+deriving Repr
+
+instance : Shrinkable BiasedNat where
+  shrink := fun n => (Shrinkable.shrink n.val).map BiasedNat.mk
+
+instance : SampleableExt BiasedNat := mkSelfContained (BiasedNat.mk <$> biasedSmallGen)
+
+-- Test with biased small numbers
+#lspec check "biased numbers are bounded" $ ∀ n : BiasedNat, n.val ≤ 1000
+
 end SlimCheck

Examples/Testing.lean

@@ -29,6 +29,53 @@ def tGroup : TestSeq := group "test group test" $
   tGroup
   )
 
+-- Testing describe/context aliases (hspec-style grouping)
+section describe_context_tests
+
+/-- Using `describe` for component-level organization -/
+def parserTests : TestSeq :=
+  describe "Parser" $
+    context "when parsing numbers" $
+      test "parses single digits" (true) $
+      test "parses multi-digit numbers" (true) $
+    context "when parsing strings" $
+      test "handles empty strings" (true) $
+      test "handles quoted strings" (true)
+
+#lspec parserTests
+-- Parser:
+--   when parsing numbers:
+--     ✓ parses single digits
+--     ✓ parses multi-digit numbers
+--   when parsing strings:
+--     ✓ handles empty strings
+--     ✓ handles quoted strings
+
+/-- Nested describe/context blocks -/
+def mathTests : TestSeq :=
+  describe "Math operations" $
+    describe "Addition" $
+      test "0 + n = n" (0 + 5 = 5) $
+      test "commutativity" (3 + 4 = 4 + 3) $
+    describe "Multiplication" $
+      test "0 * n = 0" (0 * 5 = 0) $
+      test "1 * n = n" (1 * 5 = 5)
+
+#lspec mathTests
+
+/-- Mixing describe, context, and group -/
+def mixedGrouping : TestSeq :=
+  describe "List operations" $
+    context "with empty list" $
+      test "length is 0" (([] : List Nat).length = 0) $
+      test "isEmpty is true" (([] : List Nat).isEmpty) $
+    group "non-empty list tests" $
+      test "length is positive" ([1,2,3].length > 0)
+
+#lspec mixedGrouping
+
+end describe_context_tests
+
 /--
 Testing using `#lspec` with something of type `LSpec`.
 -/

LSpec/Instances.lean

@@ -48,13 +48,15 @@ instance Nat.Testable_forall_lt
           cases Nat.eq_or_lt_of_le (Nat.le_of_lt_succ hn) with
           | inl hl => cases hl; assumption
           | inr => apply h; assumption
+      | .isPassed msg => .isPassed msg
       | .isMaybe msg => .isMaybe msg
       | .isFalse hb msg =>
         .isFalse (λ h => hb (h _ (Nat.lt_succ_self _))) $
           match msg with
           | some msg => s!"Fails on input {b}. {msg}"
           | none     => s!"Fails on input {b}."
       | .isFailure msg => .isFailure msg
+    | .isPassed msg => .isPassed msg
     | .isMaybe msg => .isMaybe msg
     | .isFalse h msg => .isFalse (λ h' => h λ n hn => h' _ (Nat.le_succ_of_le hn)) msg
     | .isFailure msg => .isFailure msg