test(LambdaCalculus): port the lambda-n-ways normalization corpus

[korbonits]

Closes #711. Supersedes #737, which I could not reopen — gh pr reopen and the REST PATCH state=open both fail on it, and GitHub still reports that PR's head at the pre-rewrite commit, so it appears detached from the branch. Same branch, so the review history there is still readable; there's a summary comment at #737 (comment 5244547139).

@chenson2018 — thanks for the clear steer on #737. This replaces the hand-written unit tests with an actual port of the lams/ corpus from sweirich/lambda-n-ways.

What's here

Under CslibTests/LambdaNWays/:

• lams/ — all 36 X.lam/X.nf.lam pairs from upstream, vendored verbatim (1,492 terms), with a README recording provenance and the MIT notice. The only .lam files left out are the four with no recorded normal form (constructed, fact5, lennartchurch, simple) and the .eval.lam files, which record weak head normal forms for upstream's evaluation benchmark rather than normal forms.
• Basic.lean — a tokenizer/parser for the .lam concrete syntax (including the let sugar that lennart.lam needs), the translation from named terms into Term ℕ, and a fuel-bounded normal-order normalizer transcribed from upstream's lib/LocallyNameless/Ott.hs, built on Term.open', Term.close and Term.subst.
• Corpus.lean — one check per file, grouped the way upstream's tests/Main.hs groups them: strictness, terms that have caught bugs, constructed terms, increasing substitution counts, random terms, and the single large lennart term. The data is pulled in with include_str, so there is no file IO at test time.

Two deliberate departures from a straight transcription

1. The corpus runs twice. Ott's normalizer only ever uses open/close, so Term.subst would go untested — which seemed wrong for an issue about capture-avoiding substitution. So each corpus is checked once contracting a redex as Term.open' b a, and once as (b ^ fvar v)[v := a] for a globally fresh v. The two agree by subst_intro, and the second routes all ~120k of lennart's substitutions through Term.subst.
2. No α-equivalence check. The locally nameless representation is canonical, so results compare with =. Upstream, working with a named representation, has to convert to de Bruijn form first.

Verification

Rather than just trusting a green run, I mutation-tested the harness against deliberately broken primitives:

Mutation	Terms caught
openRec that doesn't shift under a binder	100/100 random15, 9/9 capture10
closeRec that doesn't shift under a binder	98/100 random15, 9/9 capture10
subst that doesn't descend into abstractions	99/100 random15, 9/9 capture10
none (control)	0/100

A mismatch reports the offending term and fails elaboration:

error: lambda-n-ways corpus 'tests': term 0 (Term.open'):
  input:    \x0.(\x1.\x2.x1) x0
  produced: \x0.\x1.x0
  expected: \x0.\x1.x1

lake build --wfail --iofail, lake test --wfail --iofail, lake exe mk_all --check and lake exe checkInitImports all pass locally.

Costs, in case you want them lower

Corpus.lean takes ~28s to elaborate and the data is 1.7MB. Dropping the second (Term.subst) pass halves the time; dropping random16–random19, which are near-duplicates of random15/random20 and are not in upstream's tests/Main.hs, would cut ~440KB. Happy to trim either — just say which.

I also deleted CslibTests/LambdaCalculusLocallyNameless.lean from the earlier version of this branch, since the port supersedes it.

Use of AI

Per CONTRIBUTING: written with Claude Code (Opus 5), driven interactively by me. It read the upstream Haskell (Util/Syntax/Lambda.hs for the grammar, Util/Impl.hs for the file format, LocallyNameless/Ott.hs for the normalizer, tests/Main.hs for the suite structure) and wrote the parser, normalizer and harness; I directed the scope, the decision to also exercise Term.subst, and the mutation testing above. The vendored .lam files are byte-for-byte copies of upstream and were not generated. Worth reviewing with fresh eyes: the parser's handling of let and of application associativity, and the free-variable numbering in Named.toLN (every corpus term happens to be closed, so that path is not exercised by the data).

🤖 Generated with Claude Code