Fix/string literal term

[MattCozendey]

A string literal checks as one node

Pull request for bendlang/bend from fix/string-literal-term.

What changes

A string literal now parses as one term node, Lit, that holds its text.
Its type is String. It means the same SCon chain as before, and the
checker unfolds it one character at a time where a chain is read:

• a match frame in term_wnf reads "ab" as SCon{'a', "b"};
• term_compare compares two literals by text, and unfolds a literal that
  meets a constructor, so {"ab" == SCon{'a', "b"} : String} holds by {==};
• term_descend unfolds a literal argument against a constructor column;
• a literal pattern (case "one":) is its chain's pattern, as before;
• term_check accepts a literal at String when its head constructor is not
  peeled off the type. For any other type it checks the first unfolding, so
  the error message is the one the constructor gave.

Before this change the parser turned "text" into
SCon{Chr{U32{WCon{...}}}, ...}, about 70 term nodes per character. The
checker lifted, copied, checked and kept that chain. A literal cost about
40 KB of memory per character, and a literal past about 5000 characters
overflowed the host stack in term_check. A Nat literal had the same
problem before 2.0.7 (#779, #791).

The compiler sees no difference. def_body in comp.ts expands every literal
back into its chain (lit_expand) before the compiler lifts a body. The
emitted C and JS are byte-identical to main for every test in tests/. The
C, Metal and CUDA lanes run the same code as before.

A JS string holds Unicode scalar values only. A literal that spells a
surrogate or a code point past U+10FFFF still parses as its chain
(tests/check/string_literal_surrogates.bend).

Numbers

Checker peak memory and wall time with --check-only, bun 1.4.2, WSL2 on
x86_64. "before" is main at 6018e28.

Program	before	after
50 defs of one 1000-character literal each	2.60 GB, 4.00 s	74 MB, 0.14 s
one 200,000-character literal	stack overflow	76 MB, 0.17 s
a CLDR table module of 185 K literal characters (out of tree)	11.2 GB, 26 s	248 MB, 0.9 s
a 2466-line check suite over the CLDR plural rules (out of tree)	10.3 GB, 16 s	190 MB, 0.5 s
bench/checker/proofs_3200 (3 runs)	2.38 to 2.56 s, 821 to 843 MB	2.24 to 2.50 s, 831 to 839 MB
bench/checker/generics_3200 (3 runs)	1.12 to 1.28 s, 353 to 369 MB	1.09 to 1.20 s, 350 to 358 MB

Emission: -o x.js and -o x.c of a 4000-character literal overflowed on
main. They work now: 15.5 KB of JS, 255 KB of C. The emitters still walk a
literal as its chain, so one literal past about 8000 characters still
overflows in -o. The checker has no limit.

Files

file	change
bend2/bend.ts	the Lit node: type, Lit, lit_of, lit_chain, lit_step, lit_expand; one case each in term_higher, term_lower, term_snf, term_show, parse_patt, match_flatten; the unfolding in term_wnf, term_compare, term_descend; the check-lit rule; the string case of the parser; chr_show, shared by the char and string printers
bend2/comp.ts	def_body expands literals before lifting
gates/repo.ts	bend2/bend.ts may reach 43500 ttok (was 42000)
tests/check/string_literal_long.bend	a 6000-character literal checks and interprets
tests/check/string_literal_surrogates.bend	a surrogate escape keeps its two characters
tests/printer/string_literal_tail.bend	a literal prints back; a chain that ends in a literal prints as one string
tests/proof/string_literal_unfolds.bend	equalities between literals and chains, String.length, String.append, String.eq, a match on literal patterns

bend2/bend.ts: 41915 -> 43203 ttok (cl100k, counted with js-tiktoken; the
ttok binary was not available here). bend2/comp.ts: 63466 -> 63471.

bend2/bend.lean does not change. The core has no literal forms. Every
literal sugar already lives outside it and means its constructor chain.
Lit follows that convention, as a Nat literal above 256n does since 2.0.7.
The core judges the chain. The checker computes the same judgment on the
compact form, and every read of a Lit unfolds it.

AGENTS.md says bend2/bend.ts is human-written and not to be edited. This
change is in that file because the cost is in the checker's representation.
No other file can remove it. The diff is 130 lines. Every new function is
named lit_* and sits in one section after u32_to_term.

Verified locally

• tests/, 1382 files (1378 on main plus the four here): the JS-lane run
  output (stdout, stderr and exit code) of the 1273 tests outside tests/io is
  identical before and after, except string_literal_long, which overflows
  on main. This harness does not run tests/io, which waits on the gate's
  harness. The emitted C (601 files) and JS (617 files) of every test are
  byte-identical.
• The four new tests pass. On main, string_literal_long overflows the
  stack, and the other three pass with the same output.
• tsc -p bend2/pack/tsconfig.json reports the same two pre-existing errors
  and no new one.
• Not run here: gates/test.ts on the mini cluster. The C, Metal and CUDA
  lanes are covered by the byte-identical emission only. Please run the gate.

Related

• Type checking a large Nat literal overflows the host stack without identifying the literal #779 and Checker recursion depth: valid programs with ~10k-deep terms (e.g. a 10000n literal) fail with "machine stack overflowed" #791: the Nat literal precedent, fixed in 2.0.7 by parsing a large
  literal as U32.to_nat(n).
• Three string-literal match arms exceed 512 MiB during C generation on 2.0.19 #892: three string-literal match arms exceed 512 MiB during C generation.
  That report has the same root, on the emitter side. This change does not
  touch the emitters. A Lit reaches def_body intact, so an emitter that
  wants the text has it.
• Strings are views over adaptive-width buffers; UTF-8 streams in chunks #873: strings as views over buffers in the runtimes. A Lit is a direct
  constant for that representation.