Migrate tests from hand-rolled IO to LSpec framework

Bắt đầu bằng cách đọc test/ParserTest.lean, test/NfaTest.lean, test/MatcherTest.lean và test/Main.lean để hiểu 67 bài kiểm thử hiện có và các điểm vào hiện tại của chúng. Sau đó xem xét lakefile.toml và các yêu cầu tích hợp LSpec. Công việc được hoàn tất khi các bài kiểm thử sử dụng các suite LSpec được nhóm, lake test cung cấp kết quả có cấu trúc và phần scaffolding IO thủ công được loại bỏ.

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