Migrate tests from hand-rolled IO to LSpec framework

Summary

The current test suite uses hand-rolled IO Unit functions with manual IO.println "✓" / throw "✗" for pass/fail reporting. This reimplements scaffolding that existing Lean 4 testing frameworks already provide.

Current state

• 67 tests across ParserTest.lean, NfaTest.lean, MatcherTest.lean
• Each test is a def testFoo : IO Unit that manually prints results
• test/Main.lean calls each test function sequentially
• No structured output, no test counts, no failure summaries

Recommended approach: LSpec

LSpec is the standard Lean 4 testing framework. Tests become declarative assertions:

import LSpec
import Lck.Regex.Parser

def parserSuite := [
    test "single char" (parse "a" = Except.ok (Regex.char 'a')),
    test "reversed range fails" (parse "[z-a]" matches Except.error _),
    test "empty pattern" (parse "" = Except.error RegexError.emptyPattern)
  ]

def main := lspecIO $ .ofList [
    ("parser", parserSuite),
    ("matcher", matcherSuite)
  ]

Benefits:

• Eliminates ~200 lines of boilerplate (manual IO.println/throw per test)
• Structured pass/fail output with counts and summaries
• Standard lake test integration via testDriver
• Consistent with Lean ecosystem conventions

Other approaches worth considering

• #guard: Built-in compile-time assertions (#guard parse "a" = Except.ok (Regex.char 'a')). Zero boilerplate, failures are compilation errors. Good for simple invariants alongside LSpec.
• SlimCheck/Plausible: Property-based testing for discovering edge cases automatically. Could complement LSpec for properties like "any regex that parses successfully can be compiled to an NFA".

Migration plan

1. Add LSpec dependency to lakefile.toml
2. Convert each testFoo : IO Unit to an LSpec test "name" (assertion)
3. Group tests into suites by module
4. Wire up main := lspecIO $ .ofList [...]
5. Configure testDriver in lakefile
6. Remove manual IO scaffolding

Commencez par lire test/ParserTest.lean, test/NfaTest.lean, test/MatcherTest.lean et test/Main.lean afin de comprendre les 67 tests existants et leurs points d’entrée actuels. Examinez ensuite lakefile.toml et les exigences d’intégration de LSpec. La tâche est terminée lorsque les tests utilisent des suites LSpec groupées, que lake test fournit des résultats structurés et que le scaffolding IO manuel est supprimé.