From d816583a8cfd5568f9c564c9d7b776a2656c6e9f Mon Sep 17 00:00:00 2001 From: Matt Pereira Date: Sun, 20 Sep 2026 12:06:19 -0300 Subject: [PATCH 1/4] A string literal is one Lit node in the checker: no memory and no stack frame per character, and the emitted code is the same The parser turned "text" into SCon{Chr{U32{WCon{..}}}, ..}, about 70 nodes per character; the checker lifted, copied, checked and kept the chain, so a literal cost about 40 KB per character and one past about 5000 characters overflowed the host stack in term_check, as a Nat literal did before 2.0.7. A string literal now parses as one Lit node holding its text, typed String, that unfolds a character at a time where a chain is read: a match frame in term_wnf, term_compare against a constructor, term_descend against a constructor column, a literal pattern, and check-lit's fallback for any type but String. comp.ts expands every literal back into its chain in def_body, so the emitted C and JS are byte-identical to main for every test. 50 defs of a 1000-character literal: 2.60 GB and 4.00 s to 74 MB and 0.14 s; a 200,000-character literal checks in 0.17 s. A literal that spells a surrogate or a code point past U+10FFFF still parses as its chain. bend2/bend.ts may reach 43500 ttok (41915 to 43203). Four tests. Co-Authored-By: Claude Fable 5.1 --- bend2/bend.ts | 134 ++++++++++++++++++--- bend2/comp.ts | 2 +- gates/repo.ts | 2 +- tests/check/string_literal_long.bend | 13 ++ tests/check/string_literal_surrogates.bend | 9 ++ tests/printer/string_literal_tail.bend | 14 +++ tests/proof/string_literal_unfolds.bend | 63 ++++++++++ 7 files changed, 217 insertions(+), 20 deletions(-) create mode 100644 tests/check/string_literal_long.bend create mode 100644 tests/check/string_literal_surrogates.bend create mode 100644 tests/printer/string_literal_tail.bend create mode 100644 tests/proof/string_literal_unfolds.bend diff --git a/bend2/bend.ts b/bend2/bend.ts index 35db96c73..4ab5d411d 100644 --- a/bend2/bend.ts +++ b/bend2/bend.ts @@ -70,7 +70,7 @@ // U32 | NUMBER | U32{WCon{b, ..WNil{}}} // F32 | NUMBER "." NUMBER [EXP] | F32{WCon{b, ..WNil{}}} // Chr | "'" CHAR "'" | Chr{U32} -// Str | "\"" [CHAR] "\"" | SCon{Chr, ..SNil{}} +// Str | "\"" [CHAR] "\"" | Lit, read as SCon{Chr, ..SNil{}} // Index | x "[" i "]" ("<-" v)? | Array.get(U32, x, i), ..set(..) // Fill | D "<" [A ","?] ">" | D<&1.., A..> // Plus | "+" D ("<" [A ","?] ">")? | D<&2.., A..> @@ -90,7 +90,9 @@ // "->" return type. a def after its law takes bare names, no "->". // a bare Bind name is -Name: Quant. Fill and Plus omit a datatype's // leading Quant parameters as a block; Plus alone fills a quant-only D. -// a literal expands to one node per unit, unbounded by design; a full +// a literal expands to one node per unit, unbounded by design, but a +// string stays one Lit node and unfolds a character at a time where a +// chain is read (a match, a comparison, a descent, a pattern); a full // word, a Nat, a Char, a String, a list, a tuple and an array (its // slots) print back as literals; "*" takes a power of two. Arrow is // right-associative; the domain of a written @ or & binder stops at the @@ -286,6 +288,7 @@ export type TermOf = ( | { $: "App"; f: TermOf; x: TermOf } // f(x) | { $: "ADT"; k: Name; x: TermOf[]; r: Name[] } // A | { $: "Ctr"; k: Name; x: TermOf[] } // A{x0,x1,...} + | { $: "Lit"; v: string } // "text" | { $: "Mat"; k: Name; h: TermOf; m: TermOf } // \{A: h; m} | { $: "Efq" } // \{} | { $: "Eql"; a: TermOf; b: TermOf; T: TermOf } // {a == b : T} @@ -407,6 +410,10 @@ export function Ctr(k: Name, x: TermOf[], s?: Span): TermOf { return { $: "Ctr", k, x, s }; } +export function Lit(v: string, s?: Span): TermOf { + return { $: "Lit", v, s }; +} + export function Mat(k: Name, h: TermOf, m: TermOf, s?: Span): TermOf { return { $: "Mat", k, h, m, s }; } @@ -785,6 +792,9 @@ export function term_higher(tm: LTerm, env: Env = null): HTerm { case "Ctr": { return Ctr(tm.k, tm.x.map((x) => term_higher(x, env)), tm.s); } + case "Lit": { + return tm; + } case "Mat": { return Mat(tm.k, term_higher(tm.h, env), term_higher(tm.m, env), tm.s); } @@ -853,6 +863,9 @@ export function term_lower(term: HTerm, d: number = 0): LTerm { case "Ctr": { return Ctr(tm.k, tm.x.map((x) => term_lower(x, d)), tm.s); } + case "Lit": { + return tm; + } case "Mat": { return Mat(tm.k, term_lower(tm.h, d), term_lower(tm.m, d), tm.s); } @@ -881,8 +894,9 @@ export function term_descend(q: Quant, arg: HTerm, col: HTerm): Cmp { if (q.$ === "None") { return "EQ"; } - const a = term_strip(arg); + const s = term_strip(arg); const p = term_strip(col); + const a = s.$ === "Lit" && p.$ === "Ctr" ? term_higher(lit_step(s)) : s; switch (p.$) { case "Var": { if (a.$ === "Var" && a.i === p.i) { @@ -1160,6 +1174,53 @@ export function u32_to_term(n: U32, s?: Span): LTerm { return Ctr("U32", [word_to_term(n, s)], s); } +// Lit +// === +// a string literal is one node holding its text: it means the SCon chain +// of its characters and unfolds a character at a time where a chain is +// read, so the checker pays nothing per character and no literal outgrows +// its stack. a JS string holds Unicode scalar values only, so a literal +// that spells a surrogate or a code point past U+10FFFF is its chain. + +export function lit_of(cs: U32[], s?: Span): LTerm { + return cs.every((c) => c <= 0x10ffff && (c < 0xd800 || c > 0xdfff)) + ? Lit(cs.map((c) => String.fromCodePoint(c)).join(""), s) : lit_chain(cs, s); +} + +export function lit_chain(cs: U32[], s?: Span): LTerm { + return cs.reduceRight((out, c) => + Ctr("SCon", [Ctr("Chr", [u32_to_term(c, s)], s), out], s), Ctr("SNil", [], s)); +} + +// one step: "" is SNil{}, "ct.." is SCon{Chr{c}, "t.."} +export function lit_step(t: Extract): LTerm { + const c = t.v.codePointAt(0); + return c === undefined ? Ctr("SNil", [], t.s) + : Ctr("SCon", [Ctr("Chr", [u32_to_term(c, t.s)], t.s), Lit(t.v.slice(c > 0xffff ? 2 : 1), t.s)], t.s); +} + +// every literal in a first-order term as its chain: the compiler's view +export function lit_expand(tm: LTerm): LTerm { + const go = lit_expand; + switch (tm.$) { + case "Lit": return lit_chain([...tm.v].map((c) => c.codePointAt(0) as U32), tm.s); + case "Var": case "Ref": case "Qnt": case "Qua": case "Efq": case "Rfl": case "Hol": return tm; + case "Sub": return Sub(tm.i, tm.v.$ === "PVar" || tm.v.$ === "PCtr" ? tm.v : go(tm.v), go(tm.f), tm.s); + case "Let": return Let(tm.k, tm.i, tm.v.map(go), go(tm.f), tm.s, tm.q); + case "Typ": return Typ(go(tm.g), tm.s); + case "Min": return Min(go(tm.a), go(tm.b), tm.s); + case "All": return All(tm.q, tm.k, tm.i, go(tm.A), go(tm.B), tm.s); + case "Lam": return Lam(tm.k, tm.i, go(tm.f), tm.s, tm.q); + case "App": return App(go(tm.f), go(tm.x), tm.s); + case "ADT": return ADT(tm.k, tm.x.map(go), tm.s, tm.r); + case "Ctr": return Ctr(tm.k, tm.x.map(go), tm.s); + case "Mat": return Mat(tm.k, go(tm.h), go(tm.m), tm.s); + case "Eql": return Eql(go(tm.a), go(tm.b), go(tm.T), tm.s); + case "Rwt": return Rwt(go(tm.e), go(tm.p), go(tm.f), tm.s); + case "Ann": return Ann(go(tm.x), go(tm.T), tm.s); + } +} + // A nat literal up to NAT_LITERAL_MAX expands into a Succ chain, which the // checker unfolds in patterns and proofs; a larger one, up to the u32 bound, // parses as U32.to_nat(n), so no chain outgrows the checker's stack. @@ -1321,12 +1382,7 @@ export function term_show(term: LTerm, top: number = -1, bnd: Name[] = []): stri } return l.concat(r); } - function term_show_sugar_chr(tm: LTerm, quote: string): string | null { - const n = tm.$ === "Ctr" && tm.k === "Chr" && tm.x.length === 1 - ? u32_from_term(tm.x[0]) : null; - if (n === null) { - return null; - } + function chr_show(n: U32, quote: string): string { const k = Object.keys(ESCAPES).find((k) => ESCAPES[k] === n && ((k !== "'" && k !== '"') || k === quote)); if (k !== undefined) { return "\\" + k; @@ -1336,13 +1392,23 @@ export function term_show(term: LTerm, top: number = -1, bnd: Name[] = []): stri } return String.fromCodePoint(n); } + function lit_text(v: string): string { + return [...v].map((c) => chr_show(c.codePointAt(0) as U32, "\"")).join(""); + } + function term_show_sugar_chr(tm: LTerm, quote: string): string | null { + const n = tm.$ === "Ctr" && tm.k === "Chr" && tm.x.length === 1 + ? u32_from_term(tm.x[0]) : null; + return n === null ? null : chr_show(n, quote); + } function term_show_sugar_str(tm: LTerm): string | null { const [cs, t] = term_show_chain(tm, "SCon", 2); const ss = cs.map((c) => term_show_sugar_chr(c, "\"")); - if (t.$ !== "Ctr" || t.k !== "SNil" || t.x.length !== 0 || ss.includes(null)) { + const tl = t.$ === "Lit" ? lit_text(t.v) + : t.$ === "Ctr" && t.k === "SNil" && t.x.length === 0 ? "" : null; + if (tl === null || ss.includes(null)) { return null; } - return "\"" + ss.join("") + "\""; + return "\"" + ss.join("") + tl + "\""; } function go(tm: LTerm, prc: number): string { switch (tm.$) { @@ -1435,6 +1501,9 @@ export function term_show(term: LTerm, top: number = -1, bnd: Name[] = []): stri const as = tm.x.map((x) => go(x, 0)); return tm.k + "{" + as.join(", ") + "}"; } + case "Lit": { + return "\"" + lit_text(tm.v) + "\""; + } case "Mat": { const arms: string[] = []; let m: LTerm = tm; @@ -1763,6 +1832,9 @@ export function parse_patt(p: Parse, t: LTerm): Patt { } return { $: "PCtr", k: t.k, x: t.x.map((x) => parse_patt(p, x)), s: t.s }; } + case "Lit": { + return parse_patt(p, lit_expand(t)); + } default: { throw Err(book, ctx_nil(), "a pattern (a binder or a constructor)", term_show(term_lower(term_higher(t), 0)), t.s); } @@ -1996,10 +2068,7 @@ export function parse_term_base(p: Parse, beg: Loc): LTerm { } cs.push(parse_char(p)); } - const spn = parse_span(p, beg); - return cs.reduceRight((out, c) => - Ctr("SCon", [Ctr("Chr", [u32_to_term(c, spn)], spn), out], spn), - Ctr("SNil", [], spn)); + return lit_of(cs, parse_span(p, beg)); } case "?": { parse_bump(p); @@ -2720,7 +2789,8 @@ export function match_flatten(m: Match, vars: PVar[], fr: () => number): LTerm { + " name is a def or a consumed binder: give the value its own def)", undefined, e.s); } - case "Ctr": { + case "Ctr": + case "Lit": { throw Err(book_nil(), ctx_nil(), "an undestructed scrutinee (this value is already a constructor: bind its fields directly; if an outer match destructed it, fold the pattern into the outer case)", undefined, m.s); } default: { @@ -3012,6 +3082,9 @@ export function term_wnf(book: Book, term: HTerm): HTerm { continue back; } case "MAT": { + if (tm.$ === "Lit") { + tm = term_higher(lit_step(tm)); + } if (tm.$ === "Ctr") { const ctr = tm; let t: HTerm = fr.t; @@ -3106,6 +3179,9 @@ export function term_snf(book: Book, term: HTerm): HTerm { case "Ctr": { return Ctr(tm.k, tm.x.map((x) => term_snf(book, x)), tm.s); } + case "Lit": { + return tm; + } case "Mat": { return Mat(tm.k, term_snf(book, tm.h), term_snf(book, tm.m), tm.s); } @@ -3145,8 +3221,8 @@ export function term_compare(mode: "EQ" | "LE", book: Book, lhs: HTerm, rhs: HTe if (lhs === rhs) { return true; } - const a = term_wnf(book, lhs); - const b = term_wnf(book, rhs); + let a = term_wnf(book, lhs); + let b = term_wnf(book, rhs); if (a === b) { return true; } @@ -3155,6 +3231,12 @@ export function term_compare(mode: "EQ" | "LE", book: Book, lhs: HTerm, rhs: HTe const x: HTerm = Var(k, dep); return term_compare(mode, book, term_apply(a, x), term_apply(b, x), dep + 1); } + if (a.$ === "Lit" && b.$ === "Ctr") { + a = term_higher(lit_step(a)); + } + if (b.$ === "Lit" && a.$ === "Ctr") { + b = term_higher(lit_step(b)); + } switch (a.$) { case "Var": { return b.$ === "Var" && a.i === b.i; @@ -3222,6 +3304,9 @@ export function term_compare(mode: "EQ" | "LE", book: Book, lhs: HTerm, rhs: HTe return b.$ === "Ctr" && a.k === b.k && a.x.length === b.x.length && a.x.every((x, j) => term_compare("EQ", book, x, b.x[j], dep)); } + case "Lit": { + return b.$ === "Lit" && a.v === b.v; + } case "Mat": { return b.$ === "Mat" && a.k === b.k && term_compare("EQ", book, a.h, b.h, dep) @@ -3559,6 +3644,19 @@ export function term_check(book: Book, lhs: LHS, tm: HTerm, qt: Quant, ty: HTerm const { xs, us } = tele_check(book, lhs, tel, tm.x, qt, ctx, d, tm.s); return Check(Ctr(tm.k, xs, tm.s), ty, us); } + // T == String, with the literal's head (SNil for "", else SCon) + // where any other T checks the literal's first step, which reports + // as the constructor it is + // ----------------------------------------------------------- check-lit + // Γ ⊢ "text" : T ~ {} + case "Lit": { + const t_wnf = term_wnf(book, ty); + if (t_wnf.$ === "ADT" && t_wnf.k === "String" + && ctrs_find(book_adt(book, t_wnf, ctx, lhs.def).c, tm.v === "" ? "SNil" : "SCon") !== null) { + return Check(tm, ty, uses_nil()); + } + return term_check(book, lhs, term_higher(lit_step(tm)), qt, ty, ctx, d); + } // T == @q s:D -> P // D.c[k] = @r1 x1:F1 -> .. -> D // Γ ⊢ h : @s1 x1:F1 -> .. -> P(k{x1, .., xn}) ~ hu diff --git a/bend2/comp.ts b/bend2/comp.ts index 8576a3c74..d6210a6b2 100644 --- a/bend2/comp.ts +++ b/bend2/comp.ts @@ -1424,7 +1424,7 @@ function anf(cb: Carb, t: HTerm, ty: HTerm | null = null): HTerm { function def_body(cb: Carb, k: Bend.Name): TLD | undefined { const tld = cb.book.tlds[k]; if (tld?.$ === "Def" && tld.e !== undefined && tld.h === undefined) { - const h = Bend.term_higher(tld.e); + const h = Bend.term_higher(Bend.lit_expand(tld.e)); const n = tld.n + Math.min(def_raise(cb.book, h, tld.n), tele_unbind(cb.book, tld.T).doms.length - tld.n); cb.book.tlds[k] = { ...tld, n, h }; diff --git a/gates/repo.ts b/gates/repo.ts index 352704d3a..ca6fa94b4 100644 --- a/gates/repo.ts +++ b/gates/repo.ts @@ -39,7 +39,7 @@ allow("LICENSE", 4000); allow("flake.nix", 1500); allow("bend2/base.bend", 32000); allow("bend2/bend.lean", 400000); -allow("bend2/bend.ts", 42000); +allow("bend2/bend.ts", 43500); allow("bend2/comp.ts", 65000); allow("bend2/main.ts", 10000); allow(/^bend2\/effs\/[a-z0-9_]+\.(c|js)$/, 4000); diff --git a/tests/check/string_literal_long.bend b/tests/check/string_literal_long.bend new file mode 100644 index 000000000..51e9dd3a9 --- /dev/null +++ b/tests/check/string_literal_long.bend @@ -0,0 +1,13 @@ +# a 6000-character string literal checks: the checker holds a literal as +# one Lit node, not as a constructor per character (which overflowed its +# stack near 5000 characters). main is a function, so the test is checked +# and interpreted; the interpreter unfolds the literal to count it. +import Base + +def text() -> String: + "abcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghij" + +def main(n: Nat) -> Nat: + Nat.add(n, String.length(text())) + +#|n => Nat.add(n, 6000n) diff --git a/tests/check/string_literal_surrogates.bend b/tests/check/string_literal_surrogates.bend new file mode 100644 index 000000000..7aed1e909 --- /dev/null +++ b/tests/check/string_literal_surrogates.bend @@ -0,0 +1,9 @@ +# a literal that spells a surrogate is not one JS string's worth of +# Unicode scalar values, so it parses as its constructor chain and still +# means two characters +import Base + +def main() -> Nat: + String.length("\u{d83d}\u{de00}") + +#|2n diff --git a/tests/printer/string_literal_tail.bend b/tests/printer/string_literal_tail.bend new file mode 100644 index 000000000..ec7050e76 --- /dev/null +++ b/tests/printer/string_literal_tail.bend @@ -0,0 +1,14 @@ +# a literal prints back as a literal, and a chain that ends in a literal +# prints as one string: SCon{'a', SCon{'b', "cd"}} is "abcd" +import Base + +def greet(b: Bool) -> String: + Bool.pick(String, b, "yes\"\n", "no") + +def cons(s: String) -> String: + SCon{'a', SCon{'b', s}} + +def main(b: Bool) -> String: + String.append(greet(b), cons("cd")) + +#|b => String.append(Bool.pick(String, b, "yes\"\n", "no"), "abcd") diff --git a/tests/proof/string_literal_unfolds.bend b/tests/proof/string_literal_unfolds.bend new file mode 100644 index 000000000..dcfbc8912 --- /dev/null +++ b/tests/proof/string_literal_unfolds.bend @@ -0,0 +1,63 @@ +# a string literal is one Lit node in the checker; it unfolds a character +# at a time where a chain is read: a comparison sees "ab" as +# SCon{'a', "b"}, "" as SNil{}, a match reads a literal pattern and a +# literal scrutinee, and the evaluator steps through a literal's length. +import Base + +law ab_is_chain: + {"ab" == SCon{'a', "b"} : String} + +def ab_is_chain(): + {==} + +law empty_is_nil: + {"" == SNil{} : String} + +def empty_is_nil(): + {==} + +law length_three: + {String.length("abc") == 3n : Nat} + +def length_three(): + {==} + +law append_lits: + {String.append("ab", "cd") == "abcd" : String} + +def append_lits(): + {==} + +law eq_lits: + {String.eq("héllo", "héllo") == True{} : Bool} + +def eq_lits(): + {==} + +def classify(s: String) -> Nat: + match s: + case "": + 0n + case "one": + 1n + case "two": + 2n + case _: + 9n + +law classify_two: + {classify("two") == 2n : Nat} + +def classify_two(): + {==} + +law classify_more: + {classify("twoo") == 9n : Nat} + +def classify_more(): + {==} + +def main() -> List<&2, Nat>: + [classify(""), classify("one"), classify("two"), classify("x"), String.length("😀é")] + +#|[0n, 1n, 2n, 9n, 2n] From 75deac166ad721d31710d71952252675d9c18d8a Mon Sep 17 00:00:00 2001 From: Matt Pereira Date: Sun, 20 Sep 2026 19:59:57 -0300 Subject: [PATCH 2/4] The surrogate test is a law, not a main: the JS runtime rejects a lone surrogate tests/check/string_literal_surrogates.bend ran String.length("\u{d83d}\u{de00}") in main, and every test with a main and Base runs in the C and JS lanes; the JS runtime aborts on a lone surrogate (as on main), so the gate would fail. The same check is now the law surrogates_two in tests/proof/string_literal_unfolds.bend, which the checker verifies and the compiler never emits. Co-Authored-By: Claude Fable 5.1 --- tests/check/string_literal_surrogates.bend | 9 --------- tests/proof/string_literal_unfolds.bend | 7 +++++++ 2 files changed, 7 insertions(+), 9 deletions(-) delete mode 100644 tests/check/string_literal_surrogates.bend diff --git a/tests/check/string_literal_surrogates.bend b/tests/check/string_literal_surrogates.bend deleted file mode 100644 index 7aed1e909..000000000 --- a/tests/check/string_literal_surrogates.bend +++ /dev/null @@ -1,9 +0,0 @@ -# a literal that spells a surrogate is not one JS string's worth of -# Unicode scalar values, so it parses as its constructor chain and still -# means two characters -import Base - -def main() -> Nat: - String.length("\u{d83d}\u{de00}") - -#|2n diff --git a/tests/proof/string_literal_unfolds.bend b/tests/proof/string_literal_unfolds.bend index dcfbc8912..2126f5736 100644 --- a/tests/proof/string_literal_unfolds.bend +++ b/tests/proof/string_literal_unfolds.bend @@ -2,6 +2,7 @@ # at a time where a chain is read: a comparison sees "ab" as # SCon{'a', "b"}, "" as SNil{}, a match reads a literal pattern and a # literal scrutinee, and the evaluator steps through a literal's length. +# a character is any u32, so a literal may spell a surrogate pair. import Base law ab_is_chain: @@ -34,6 +35,12 @@ law eq_lits: def eq_lits(): {==} +law surrogates_two: + {String.length("\u{d83d}\u{de00}") == 2n : Nat} + +def surrogates_two(): + {==} + def classify(s: String) -> Nat: match s: case "": From 6619790bbc109b1eca73cbb79e64961d4144ff15 Mon Sep 17 00:00:00 2001 From: Matt Pereira Date: Sun, 20 Sep 2026 20:11:03 -0300 Subject: [PATCH 3/4] lit_expand is gone: a pattern expands its literal in place, and the compiler expands a literal where it reads a constructor lit_expand walked a whole first-order term to turn every Lit into its chain before compilation, so comp.ts saw no Lit. A Lit has no sub-terms, so parse_patt calls lit_full, the chain of one literal. The compiler matches constructors in term_const, ty_peel and the Mat scrutinee of emit_unfold, so term_lit, memoized per node, hands them a Lit's chain there, and def_body no longer pre-expands. The emitted code is unchanged: the JS of the 164 runnable tests with a string literal is byte-identical, and the checker's output is the same on every non-IO test. bend2/bend.ts may reach 43000 ttok (43203 to 42853). Co-Authored-By: Claude Fable 5.1 --- bend2/bend.ts | 25 ++++--------------------- bend2/comp.ts | 17 ++++++++++++----- gates/repo.ts | 2 +- 3 files changed, 17 insertions(+), 27 deletions(-) diff --git a/bend2/bend.ts b/bend2/bend.ts index 4ab5d411d..8d470e909 100644 --- a/bend2/bend.ts +++ b/bend2/bend.ts @@ -1199,26 +1199,9 @@ export function lit_step(t: Extract): LTerm { : Ctr("SCon", [Ctr("Chr", [u32_to_term(c, t.s)], t.s), Lit(t.v.slice(c > 0xffff ? 2 : 1), t.s)], t.s); } -// every literal in a first-order term as its chain: the compiler's view -export function lit_expand(tm: LTerm): LTerm { - const go = lit_expand; - switch (tm.$) { - case "Lit": return lit_chain([...tm.v].map((c) => c.codePointAt(0) as U32), tm.s); - case "Var": case "Ref": case "Qnt": case "Qua": case "Efq": case "Rfl": case "Hol": return tm; - case "Sub": return Sub(tm.i, tm.v.$ === "PVar" || tm.v.$ === "PCtr" ? tm.v : go(tm.v), go(tm.f), tm.s); - case "Let": return Let(tm.k, tm.i, tm.v.map(go), go(tm.f), tm.s, tm.q); - case "Typ": return Typ(go(tm.g), tm.s); - case "Min": return Min(go(tm.a), go(tm.b), tm.s); - case "All": return All(tm.q, tm.k, tm.i, go(tm.A), go(tm.B), tm.s); - case "Lam": return Lam(tm.k, tm.i, go(tm.f), tm.s, tm.q); - case "App": return App(go(tm.f), go(tm.x), tm.s); - case "ADT": return ADT(tm.k, tm.x.map(go), tm.s, tm.r); - case "Ctr": return Ctr(tm.k, tm.x.map(go), tm.s); - case "Mat": return Mat(tm.k, go(tm.h), go(tm.m), tm.s); - case "Eql": return Eql(go(tm.a), go(tm.b), go(tm.T), tm.s); - case "Rwt": return Rwt(go(tm.e), go(tm.p), go(tm.f), tm.s); - case "Ann": return Ann(go(tm.x), go(tm.T), tm.s); - } +// the whole chain: a pattern's and the compiler's view +export function lit_full(t: Extract): LTerm { + return lit_chain([...t.v].map((c) => c.codePointAt(0) as U32), t.s); } // A nat literal up to NAT_LITERAL_MAX expands into a Succ chain, which the @@ -1833,7 +1816,7 @@ export function parse_patt(p: Parse, t: LTerm): Patt { return { $: "PCtr", k: t.k, x: t.x.map((x) => parse_patt(p, x)), s: t.s }; } case "Lit": { - return parse_patt(p, lit_expand(t)); + return parse_patt(p, lit_full(t)); } default: { throw Err(book, ctx_nil(), "a pattern (a binder or a constructor)", term_show(term_lower(term_higher(t), 0)), t.s); diff --git a/bend2/comp.ts b/bend2/comp.ts index d6210a6b2..667382d11 100644 --- a/bend2/comp.ts +++ b/bend2/comp.ts @@ -631,6 +631,8 @@ const CYCLES: Map = new Map(); const CONSTS: Map = new Map(); +const LITS: Map = new Map(); + // Name // ==== @@ -696,7 +698,7 @@ function memo(m: Map, k: K, f: () => V): V { } function memo_gc(): void { - [OPENS, USES, FOLDS, SPINES, CONSTS].forEach((m) => m.clear()); + [OPENS, USES, FOLDS, SPINES, CONSTS, LITS].forEach((m) => m.clear()); } // Probe @@ -828,8 +830,13 @@ function term_nodes(cf: Carb, t: HTerm): number { return n; } +// A string literal is its constructor chain to the compiler. +function term_lit(t: HTerm): HTerm { + return t.$ === "Lit" ? memo(LITS, t, () => Bend.term_higher(Bend.lit_full(t))) : t; +} + function term_const(t: HTerm): boolean { - const s = Bend.term_strip(t); + const s = term_lit(Bend.term_strip(t)); return s.$ === "Ctr" && memo(CONSTS, s, () => s.x.every(term_const)); } @@ -929,7 +936,7 @@ function ty_peel(tm: HTerm, ty = x.$ === "Ann" ? x.T : ty; x = Bend.term_force(x.$ === "Ann" ? x.x : x.f); } - return [x, ty]; + return [term_lit(x), ty]; } function ty_adt(book: Bend.Book, A: HTerm | null): HAdt | null { @@ -1424,7 +1431,7 @@ function anf(cb: Carb, t: HTerm, ty: HTerm | null = null): HTerm { function def_body(cb: Carb, k: Bend.Name): TLD | undefined { const tld = cb.book.tlds[k]; if (tld?.$ === "Def" && tld.e !== undefined && tld.h === undefined) { - const h = Bend.term_higher(Bend.lit_expand(tld.e)); + const h = Bend.term_higher(tld.e); const n = tld.n + Math.min(def_raise(cb.book, h, tld.n), tele_unbind(cb.book, tld.T).doms.length - tld.n); cb.book.tlds[k] = { ...tld, n, h }; @@ -2389,7 +2396,7 @@ function emit_unfold(fl: File, s: HTerm): HTerm | null { xs = xs.slice(1); continue; } - const c = w.$ === "Mat" ? Bend.term_strip(xs[0]) : null; + const c = w.$ === "Mat" ? term_lit(Bend.term_strip(xs[0])) : null; if (c === null || c.$ !== "Ctr" || !term_const(c)) { return null; } diff --git a/gates/repo.ts b/gates/repo.ts index ca6fa94b4..d1df0b5f3 100644 --- a/gates/repo.ts +++ b/gates/repo.ts @@ -39,7 +39,7 @@ allow("LICENSE", 4000); allow("flake.nix", 1500); allow("bend2/base.bend", 32000); allow("bend2/bend.lean", 400000); -allow("bend2/bend.ts", 43500); +allow("bend2/bend.ts", 43000); allow("bend2/comp.ts", 65000); allow("bend2/main.ts", 10000); allow(/^bend2\/effs\/[a-z0-9_]+\.(c|js)$/, 4000); From 105d0ded25b4bbe950e768b36a1bb92b60c9042a Mon Sep 17 00:00:00 2001 From: Matt Pereira Date: Sun, 20 Sep 2026 20:13:28 -0300 Subject: [PATCH 4/4] Two tests pin where a literal must unfold: the termination check and a module's own String Both hold on main and had no test. A literal argument that is a strict tail of its case's literal pattern descends: case "ab" may call f("b"), which needs term_descend to read the literal as its chain. A literal is a String only where String declares SCon and SNil: a module that declares its own type String is Data: Foo{} rejects "abc" with main's exact error, which needs check-lit's ctrs_find guard. Co-Authored-By: Claude Fable 5.1 --- tests/check/string_literal_descends.bend | 15 +++++++++++++++ tests/check/string_literal_own_string.bend | 16 ++++++++++++++++ 2 files changed, 31 insertions(+) create mode 100644 tests/check/string_literal_descends.bend create mode 100644 tests/check/string_literal_own_string.bend diff --git a/tests/check/string_literal_descends.bend b/tests/check/string_literal_descends.bend new file mode 100644 index 000000000..93bbaf248 --- /dev/null +++ b/tests/check/string_literal_descends.bend @@ -0,0 +1,15 @@ +# a literal argument descends when it is a strict tail of its case's +# literal pattern: the termination check unfolds the literal +import Base + +def f(s: String) -> Nat: + match s: + case "ab": + f("b") + case _: + 0n + +def main() -> Nat: + f("ab") + +#|0n diff --git a/tests/check/string_literal_own_string.bend b/tests/check/string_literal_own_string.bend new file mode 100644 index 000000000..433b2da91 --- /dev/null +++ b/tests/check/string_literal_own_string.bend @@ -0,0 +1,16 @@ +# a literal is a String only where String declares SCon and SNil: a +# module's own String with other constructors rejects it +type String is Data: + Foo{} + +def s() -> String: + "abc" + +#|Error: +#|- expected : a declared constructor (String declares Foo) +#|- observed : "abc" +#|Location: s +#|6 | def s() -> String: +#|7>| "abc" +#|8 | +#|exit 1