Generalize UnitTest to run in different monads.

cedar-lean/UnitTest/Decimal.lean

@@ -23,8 +23,8 @@ namespace UnitTest.Decimal
 
 open Cedar.Spec.Ext.Decimal
 
-private def testValid (str : String) (rep : Int) : TestCase :=
-  test str (checkEq (parse str) (decimal? rep))
+private def testValid (str : String) (rep : Int) : TestCase IO :=
+  test str ⟨λ _ => checkEq (parse str) (decimal? rep)⟩
 
 def testsForValidStrings :=
   suite "Decimal.parse for valid strings"
@@ -40,8 +40,8 @@ def testsForValidStrings :=
     testValid "922337203685477.5807" 9223372036854775807
   ]
 
-private def testInvalid (str : String) (msg : String) : TestCase :=
-  test s!"{str} [{msg}]" (checkEq (parse str) .none)
+private def testInvalid (str : String) (msg : String) : TestCase IO :=
+  test s!"{str} [{msg}]" ⟨λ _ => checkEq (parse str) .none⟩
 
 def testsForInvalidStrings :=
   suite "Decimal.parse for invalid strings"

cedar-lean/UnitTest/IPAddr.lean

@@ -29,8 +29,8 @@ private def ipv4 (a₀ a₁ a₂ a₃ : UInt8) (pre : Nat) : IPNet :=
 private def ipv6 (a₀ a₁ a₂ a₃ a₄ a₅ a₆ a₇ : UInt16) (pre : Nat) : IPNet :=
   IPNet.V6 (IPv6Addr.mk a₀ a₁ a₂ a₃ a₄ a₅ a₆ a₇) (Fin.ofNat pre)
 
-private def testValid (str : String) (ip : IPNet) : TestCase :=
-  test str (checkEq (parse str) ip)
+private def testValid (str : String) (ip : IPNet) : TestCase IO :=
+  test str ⟨λ _ => checkEq (parse str) ip⟩
 
 def testsForValidStrings :=
   suite "IPAddr.parse for valid strings"
@@ -45,8 +45,8 @@ def testsForValidStrings :=
     testValid "a::f/120" (ipv6 0xa 0 0 0 0 0 0 0xf 120)
   ]
 
-private def testInvalid (str : String) (msg : String) : TestCase :=
-  test s!"{str} [{msg}]" (checkEq (parse str) .none)
+private def testInvalid (str : String) (msg : String) : TestCase IO :=
+  test s!"{str} [{msg}]" ⟨λ _ => checkEq (parse str) .none⟩
 
 def testsForInvalidStrings :=
   suite "IPAddr.parse for invalid strings"
@@ -78,11 +78,11 @@ private def parse! (str : String) : IPNet :=
   | .none => panic! s!"not a valid IP address {str}"
 
 
-private def testIsLoopback (str : String) (expected : Bool) : TestCase :=
-  test s!"isLoopback {str}" (checkEq (parse! str).isLoopback expected)
+private def testIsLoopback (str : String) (expected : Bool) : TestCase IO :=
+  test s!"isLoopback {str}" ⟨λ _ => checkEq (parse! str).isLoopback expected⟩
 
-private def testToUInt128 (str : String) (expected : UInt128) : TestCase :=
-  test s!"toUInt128 {str}" (checkEq (parse! str).toUInt128 expected)
+private def testToUInt128 (str : String) (expected : UInt128) : TestCase IO :=
+  test s!"toUInt128 {str}" ⟨λ _ => checkEq (parse! str).toUInt128 expected⟩
 
 def testsForIsLoopback :=
   suite "IPAddr.isLoopback"
@@ -106,8 +106,8 @@ def ip! (str : String) : IPNet :=
   | .some ip => ip
   | .none => panic! s!"not a valid IP address {str}"
 
-def testInRange (str₁ str₂ : String) (expected : Bool) : TestCase :=
-  test s!"inRange {str₁} {str₂}" (checkEq ((ip! str₁).inRange (ip! str₂)) expected)
+def testInRange (str₁ str₂ : String) (expected : Bool) : TestCase IO :=
+  test s!"inRange {str₁} {str₂}" ⟨λ _ => checkEq ((ip! str₁).inRange (ip! str₂)) expected⟩
 
 def testsForInRange :=
   suite "IPAddr.inRange"
@@ -137,12 +137,14 @@ def testsForInRange :=
     testInRange "10.0.0.1/24" "10.0.0.0/29" false,
     testInRange "10.0.0.1/29" "10.0.0.0/24" true,
     testInRange "10.0.0.0/32" "10.0.0.0/32" true,
-    testInRange "10.0.0.0/32" "10.0.0.0" true
+    testInRange "10.0.0.0/32" "10.0.0.0" true,
+    testInRange "0.0.0.0/31" "0.0.0.1/31" true,
+    testInRange "0.0.0.1/31" "0.0.0.0/31" true,
   ]
 
-private def testEq (str₁ str₂ : String) (expected : Bool) : TestCase :=
+private def testEq (str₁ str₂ : String) (expected : Bool) : TestCase IO :=
   let eq : Bool := (ip! str₁) = (ip! str₂)
-  test s!"{str₁} == {str₂}" (checkEq eq expected)
+  test s!"{str₁} == {str₂}" ⟨λ _ => checkEq eq expected⟩
 
 def testsForIpNetEquality :=
   suite "IpAddr.eq"
@@ -164,6 +166,6 @@ def tests := [
   testsForIpNetEquality]
 
 -- Uncomment for interactive debugging
--- #eval TestSuite.runAll tests
+#eval TestSuite.runAll tests
 
 end UnitTest.IPAddr

cedar-lean/UnitTest/Run.lean

@@ -20,45 +20,48 @@ import Std
 
 namespace UnitTest
 
-def pass : IO Bool := pure true
+variable [Monad m] [MonadLiftT IO m]
 
-def fail (name : String) (message : String) : IO Bool := do
-  IO.println "--------------------"
-  IO.println s!"FAILED: {name}"
-  IO.println message
-  IO.println "--------------------"
-  pure false
+abbrev TestResult := Except String Unit
 
-def checkEq {α} [DecidableEq α] [Repr α] (actual expected : α) (name : String) : IO Bool :=
+def checkEq {α} [DecidableEq α] [Repr α] (actual expected : α) : m TestResult :=
   if actual = expected
-  then pass
-  else fail name s!"actual: {reprArg actual}\nexpected: {reprArg expected}"
+  then return .ok ()
+  else return .error s!"actual: {reprArg actual}\nexpected: {reprArg expected}"
 
-structure TestCase where
+structure TestCase (m) [Monad m] [MonadLiftT IO m] extends Thunk (m TestResult) where
   name : String
-  exec : String → IO Bool
 
-structure TestSuite where
+structure TestSuite (m) [Monad m] [MonadLiftT IO m] where
   name  : String
-  tests : List TestCase
+  tests : List (TestCase m)
 
-def test (name : String) (exec : String → IO Bool) : TestCase :=
-  TestCase.mk name exec
+def test (name : String) (exec : Thunk (m TestResult)) : TestCase m :=
+  TestCase.mk exec name
 
-def suite (name : String) (tests : List TestCase) : TestSuite :=
+def suite (name : String) (tests : List (TestCase m)) : TestSuite m :=
   TestSuite.mk name tests
 
 /--
 Runs the test case and returns true if the tests passes.
 Otherwise prints the error message and returns false.
 -/
-def TestCase.run (case : TestCase) : IO Bool := case.exec case.name
+def TestCase.run (case : TestCase m) : m Bool := do
+  match (← case.get) with
+  | .ok _      =>
+    return true
+  | .error msg =>
+    IO.println "--------------------"
+    IO.println s!"FAILED: {case.name}"
+    IO.println msg
+    IO.println "--------------------"
+    return false
 
 /--
 Runs the test suite, prints the stats, and returns the number of
 failed test cases.
 -/
-def TestSuite.run (suite : TestSuite) : IO Nat := do
+def TestSuite.run (suite : TestSuite m) : m Nat := do
   IO.println "===================="
   IO.println s!"Running {suite.name}"
   let outcomes ← suite.tests.mapM TestCase.run
@@ -71,7 +74,7 @@ def TestSuite.run (suite : TestSuite) : IO Nat := do
 /--
 Runs all the given test suites and prints the stats.
 -/
-def TestSuite.runAll (suites : List TestSuite) : IO UInt32 := do
+def TestSuite.runAll (suites : List (TestSuite m)) : m UInt32 := do
   let outcomes ← suites.mapM TestSuite.run
   let total := suites.foldl (fun n ts => n + ts.tests.length) 0
   let failures := outcomes.foldl (· + ·) 0

cedar-lean/UnitTest/Wildcard.lean

@@ -23,8 +23,8 @@ namespace UnitTest.Wildcard
 
 open Cedar.Spec
 
-private def testWildcardMatch (str : String) (pat : Pattern) (expected : Bool) : TestCase :=
-  test s!"{expected}: {str} like {reprStr pat}" (checkEq (wildcardMatch str pat) expected)
+private def testWildcardMatch (str : String) (pat : Pattern) (expected : Bool) : TestCase IO :=
+  test s!"{expected}: {str} like {reprStr pat}" ⟨λ _ => checkEq (wildcardMatch str pat) expected⟩
 
 private def justChars : String → Pattern
   | .mk [] => []