Feature/u32 to nat

[MattCozendey]

A U32 literal is U32.from_nat over a nat literal

Follow-up to #907 and #924, which made a string or nat literal one Lit
node. A bare number now parses as U32.from_nat(3n): one App over
one Lit, where before the parser built a 33-word U32{WCon{..}} chain
of about 100 nodes per number. The compiler no longer expands a nat past
256 into U32.to_nat over a word either.

In bend.ts the parser emits App(Ref("U32.from_nat"), Lit(n)) and
u32_lit reads that shape back. term_wnf takes U32.from_nat on a
nat literal straight to its word (u32_word, one shared term per
number), so a proof over 4294967295 costs what it did before. That
shortcut is a compressed run of the def's own unfolding, and
definitional equality is unchanged. lit_ctr reads any literal as its
constructor, a U32 literal as its word and a string or nat literal one
step, and the termination check, the match frame, term_compare and
check-lit call it where each used to step a Lit by hand. Patterns and
the printer read the shape too: case 0: still matches, and an error
spells 3 rather than U32.from_nat(3n).

In comp.ts a nat Lit is a leaf. lit_word gives the immediate for
either literal and feeds term_const and both emitters, so no
U32.from_nat call and no U32.to_nat chain reaches the output. The
compile-time fold still reads a literal scrutinee as its constructor, so
a match on a literal argument folds as it did.

In base.bend, Word.zero, Word.inc, U32.inc and U32.from_nat
move under def Word(n). Forward references are refused and IO.fork
writes 1 early in the file. The base case is U32{Word.zero(32n)}.

Measured with both trees on tmpfs:

	before	after
2000 defs, each a wide U32 literal	1.03 s, 217 MB	0.26 s, 81 MB
demos/app_slash_boss_3d --check-only	1.80 s, 420 MB	1.43 s, 319 MB
demos/proof_numerics --check-only	0.21 s, 74 MB	0.18 s, 70 MB

The gain scales with how many numbers a program writes. Emitted C over
tests/ and bench/runtime is byte-identical apart from 0 spelled 0ull
and one literal list that now lives in the static image. JS inlines
3000n where it had BigInt(3000). The bench binaries print the same
results.

Two things a user can observe. A literal now infers its own type, since
it is an application of a typed def, where a bare constructor needed a
goal: x = 5 with no annotation types as U32, and
tests/parse/rewrite_non_equation is repinned because the miss is now
the equation rather than the literal. And a file without import Base
that writes a bare number reports an undefined U32.from_nat instead of
an unknown constructor.

New tests: check/u32_literal_proof (wide and wrapping proofs, literal
patterns), check/u32_literal_show (a literal prints as its number) and
compile/u32_literal_word (immediates on all three lanes). Locally the
interpret lane over all 1415 tests has the same pass set as main plus
those three, and the C and JS lanes were built and run on the 118 tests
whose emitted code changed. The cluster gates were not run from here.
Caps move to 43400 for bend.ts (at 43338) and 65300 for comp.ts (at
65193).

bend.ts is edited, in the parser, term_wnf, the printer and the
pattern reader, since the change lives there by nature. The term_wnf
shortcut is keyed on the def name U32.from_nat in three places: the
parser, u32_lit and the guard. A rename in base.bend would fall back
to the slow unfolding without an error. bend.lean says literals are base
constructors, not calculus, and may want a line about this reduction.

🤖 Generated with Claude Code

[nicolas-abril]

Thank you for this. The diagnosis is right and the speedup is real: a U32 literal is 66 constructor nodes today, and parse, lift, check and the report walk each pay per node. One node per literal is the fix.

We are not going to take this shape for it. U32.from_nat(3n) makes a literal a redex instead of a value, so every consumer of terms has to recognize it or unfold it: the name-keyed shortcut in term_wnf, lit_word and term_const in the compiler, the default arm of parse_patt, the printer, lit_ctr through four sites, and the base.bend reorder. Each is a place that drifts, and a rename of U32.from_nat silently falls back to the slow path.

We could either try what #907 and #924 did for Nat and String: make the literal a Lit. A U32 variant whose lit_step is the memoized word rides the seams that already exist with no site-specific code, and the emitter already collapses a word to an immediate. Inference of a bare 5 is a separate change, and nat and string literals do not infer today either.

Note: this reply was written by an AI after it reported the PR to me and I made the decision. If anything here is wrong, reply and I will review it myself.

[MattCozendey]

I'll make a new PR fixing this soon