Feature/nat literal term

[MattCozendey]

A nat literal is one Lit node in the checker

A nat literal up to 256 parsed as a Succ chain, and a larger one as
U32.to_nat(n), an application. Two forms meant one literal: the parser, the
pattern reader and the printer each knew both, and a self-call on a literal
past 256 failed the termination check, since the check reads constructors
and saw a function call. A Lit now holds a number as it holds a text, and
the same peel reads it: 0n is Zero{}, n is Succ{n-1}.

What changes

• The checker unfolds a nat literal one Succ at a time where a chain is
  read: a match frame, a comparison, a descent, and the check rule's
  fallback. Against Nat it checks in O(1), with the same guard the string
  rule has: the Nat in scope must declare Succ and Zero.
• Inference steps a literal once, so an undeclared Nat still reports
  "a declared constructor".
• The printer prints a literal as its number, and a Succ chain that ends
  in a literal as one number.
• "1n+0n" parses as 1n, so a template's ~ key agrees with 1n.
• nat_to_term and the App form of a nat pattern are gone. NAT_LITERAL_MAX
  stays for two uses: "n + T" past it is Nat.add(n, T), and the compiler
  emits U32.to_nat(n) past it. U32.to_nat is an intrinsic ($0 in C,
  BigInt($0) in JS), so this costs nothing at run time.
• comp.ts reads a literal through term_lit in term_kids and term_any, so
  the reference to U32.to_nat counts for reachability.

Emitted code and behavior

• The C and JS of every runnable test are byte-identical to the base.
• The checker's output is the same on every non-IO test (1291).
• 2000 defs of 200n: 1.06 s and 366 MB to 0.18 s and 83 MB.
• case 300n: down(299n) now passes the termination check.

Tests

• tests/proof/nat_literal_unfolds.bend: a comparison sees 300n as
  Succ{299n} and 0n as Zero{}, a match reads a literal pattern past 256
  and a literal scrutinee, a self-call on a smaller literal descends, a
  literal at the u32 bound passes through Nat.add unforced.
• tests/check/nat_literal_own_nat.bend: a module's own Nat with other
  constructors rejects 3n with the base's exact error.
• tests/printer/nat_literal_print.bend: a literal prints back as a
  literal, "n+T" past 256 is Nat.add, a chain that ends in a literal
  prints as one number.
• tests/check/nat_literal_pattern_empty.bend spells its pattern 0n. It
  wrote U32.to_nat(0), the form the parser gave a literal, which is no
  pattern anymore. It prints the same error.

Size: bend2/bend.ts 42981 and bend2/comp.ts 64977 ttok (cl100k), under
the caps of 43000 and 65000 with no room to spare. If your ttok reads
higher, the caps need to move.

🤖 Generated with Claude Code

[MattCozendey]

This should only be considered if(and only if) #907 is merged as well, since it builds from it.

[VictorTaelin]

Merged, thank you very much. Both PRs landed on main as one commit under your authorship, 942573f "A string or nat literal is one Lit node in the checker", and bend.ts's cap moved to 43000 for it. The design is the right one: the core keeps no literal form, the checker reads a compact node and unfolds it one step where a constructor is needed, and the emitters see the chain they always saw. The numbers reproduced here, and a self-call on a literal past 256 passing the termination check is a real fix on its own. It ships in the next release.

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