Migrate tests from hand-rolled IO to LSpec framework

Inizia leggendo test/ParserTest.lean, test/NfaTest.lean, test/MatcherTest.lean e test/Main.lean per comprendere i 67 test esistenti e i loro attuali punti di ingresso. Poi esamina lakefile.toml e i requisiti di integrazione di LSpec. Il lavoro è completato quando i test usano suite LSpec raggruppate, lake test fornisce risultati strutturati e il scaffolding IO manuale viene rimosso.

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