From 754ccaff665429b95f6d090c1a70235d3a85e673 Mon Sep 17 00:00:00 2001 From: Mathews Fernando Date: Tue, 22 Sep 2026 22:54:17 -0300 Subject: [PATCH 1/4] representing u32 and f32 as literals by adding k tag into Lit to differentiate (v was already a value string | number) --- bend2/bend.ts | 42 ++++++++++++++++++++++++++++-------------- 1 file changed, 28 insertions(+), 14 deletions(-) diff --git a/bend2/bend.ts b/bend2/bend.ts index e3201d478..7ef698e76 100644 --- a/bend2/bend.ts +++ b/bend2/bend.ts @@ -67,8 +67,8 @@ // List | "[" [A ","?] "]", A "<>" B | Con{A, ..Nil{}}, Con{A, B} // Array | "[" A ":" T ("*" 2^D "n" | "^" D) "]" | Array.new(T, D, A) // Nat | NUMBER "n" ("+" T)? | Lit, read as Succ{..Zero{}}; Succ{..T} -// U32 | NUMBER | U32{WCon{b, ..WNil{}}} -// F32 | NUMBER "." NUMBER [EXP] | F32{WCon{b, ..WNil{}}} +// U32 | NUMBER | Lit, read as U32{WCon{b, ..WNil{}}} +// F32 | NUMBER "." NUMBER [EXP] | Lit, read as F32{WCon{b, ..WNil{}}} // Chr | "'" CHAR "'" | Chr{U32} // Str | "\"" [CHAR] "\"" | Lit, read as SCon{Chr, ..SNil{}} // Index | x "[" i "]" ("<-" v)? | Array.get(U32, x, i), ..set(..) @@ -91,7 +91,7 @@ // 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, but a -// string and a nat stay one Lit node and unfold a unit at a time where +// string, nat, u32 and f32 stay one Lit node and unfold 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 @@ -288,7 +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 | number } // "text", 3n + | { $: "Lit"; v: string | number; k?: "U32" | "F32" } // "text", 3n; k tags a 32-bit word | { $: "Mat"; k: Name; h: TermOf; m: TermOf } // \{A: h; m} | { $: "Efq" } // \{} | { $: "Eql"; a: TermOf; b: TermOf; T: TermOf } // {a == b : T} @@ -410,8 +410,8 @@ export function Ctr(k: Name, x: TermOf[], s?: Span): TermOf { return { $: "Ctr", k, x, s }; } -export function Lit(v: string | number, s?: Span): TermOf { - return { $: "Lit", v, s }; +export function Lit(v: string | number, s?: Span, k?: "U32" | "F32"): TermOf { + return { $: "Lit", v, s, k }; } export function Mat(k: Name, h: TermOf, m: TermOf, s?: Span): TermOf { @@ -1181,6 +1181,8 @@ export function u32_to_term(n: U32, s?: Span): LTerm { // unit at a time where a chain is read, so the checker pays nothing per // unit. 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. +// U32 and F32 literals tag their raw bits with the enclosing constructor; +// both unfold to that constructor around the same 32-bit Word chain. export function lit_of(cs: U32[], s?: Span): LTerm { return cs.every((c) => c <= 0x10ffff && (c < 0xd800 || c > 0xdfff)) @@ -1194,6 +1196,9 @@ export function lit_chain(cs: U32[], s?: Span): LTerm { // one step: "" is SNil{}, "ct.." is SCon{Chr{c}, "t.."}, 0n is Zero{}, n is Succ{n-1} export function lit_step(t: Extract): LTerm { + if (t.k !== undefined) { + return Ctr(t.k, [word_to_term(t.v as U32, t.s)], t.s); + } if (typeof t.v === "number") { return t.v === 0 ? Ctr("Zero", [], t.s) : Ctr("Succ", [Lit(t.v - 1, t.s)], t.s); } @@ -1204,6 +1209,9 @@ export function lit_step(t: Extract): LTerm { // the whole chain: a pattern's view export function lit_full(t: Extract): LTerm { + if (t.k !== undefined) { + return lit_step(t); + } if (typeof t.v === "string") { return lit_chain([...t.v].map((c) => c.codePointAt(0) as U32), t.s); } @@ -1225,12 +1233,15 @@ export function nat_from_term(t: LTerm): number | null { t = t.x[0]; } return t.$ === "Ctr" && t.k === "Zero" && t.x.length === 0 ? n - : t.$ === "Lit" && typeof t.v === "number" && n + t.v <= 0xffffffff + : t.$ === "Lit" && t.k === undefined && typeof t.v === "number" && n + t.v <= 0xffffffff ? n + t.v : null; } export function u32_from_term(tm: TermOf, k: Name = "U32"): number | null { const w0 = term_strip(tm); + if (w0.$ === "Lit") { + return w0.k === k ? w0.v as U32 : null; + } if (w0.$ !== "Ctr" || w0.k !== k || w0.x.length !== 1) { return null; } @@ -1480,6 +1491,9 @@ export function term_show(term: LTerm, top: number = -1, bnd: Name[] = []): stri return tm.k + "{" + as.join(", ") + "}"; } case "Lit": { + if (tm.k !== undefined) { + return tm.k === "U32" ? String(tm.v) : f32_show(f32_from_bits(tm.v as U32)); + } return typeof tm.v === "number" ? String(tm.v) + "n" : "\"" + lit_text(tm.v) + "\""; } case "Mat": { @@ -2304,7 +2318,7 @@ export function parse_term_num(p: Parse): LTerm { parse_fail(p, "a float literal with a finite f32 value (got " + m[0] + ")"); } const spn = parse_span(p, beg); - return Ctr("F32", [word_to_term(f32_to_bits(v), spn)], spn); + return Lit(f32_to_bits(v), spn, "F32"); } if (m[2] === undefined) { if (char_is_name(parse_peek(p))) { @@ -2314,7 +2328,7 @@ export function parse_term_num(p: Parse): LTerm { if (w > 0xffffffff) { parse_fail(p, "a u32 literal up to 4294967295 (got " + s + ")"); } - return u32_to_term(w, parse_span(p, beg)); + return Lit(w, parse_span(p, beg), "U32"); } const n = Number(s); if (n > 0xffffffff) { @@ -2323,7 +2337,7 @@ export function parse_term_num(p: Parse): LTerm { if (parse_take(p, "+")) { let out = parse_term(p); const spn = parse_span(p, beg); - if (out.$ === "Lit" && typeof out.v === "number" && n + out.v <= 0xffffffff) { + if (out.$ === "Lit" && out.k === undefined && typeof out.v === "number" && n + out.v <= 0xffffffff) { return Lit(n + out.v, spn); } if (n > NAT_LITERAL_MAX) { @@ -3279,7 +3293,7 @@ export function term_compare(mode: "EQ" | "LE", book: Book, lhs: HTerm, rhs: HTe && a.x.every((x, j) => term_compare("EQ", book, x, b.x[j], dep)); } case "Lit": { - return b.$ === "Lit" && a.v === b.v; + return b.$ === "Lit" && a.k === b.k && a.v === b.v; } case "Mat": { return b.$ === "Mat" && a.k === b.k @@ -3619,15 +3633,15 @@ 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 == Base's String (or Nat) with the literal's head: SNil/SCon (Zero/Succ) + // T == Base's String, Nat, U32 or F32 with the literal's head // where any other T checks the literal's first step, which reports // as the constructor it is // ----------------------------------------------------------- check-lit // Γ ⊢ "text" : T ~ {} Γ ⊢ 3n : T ~ {} case "Lit": { const t_wnf = term_wnf(book, ty); - const c = typeof tm.v === "number" ? tm.v === 0 ? "Zero" : "Succ" - : tm.v === "" ? "SNil" : "SCon"; + const c = tm.k ?? (typeof tm.v === "number" ? tm.v === 0 ? "Zero" : "Succ" + : tm.v === "" ? "SNil" : "SCon"); if (t_wnf.$ === "ADT" && book.tlds[t_wnf.k]?.b === true && ctrs_find(book_adt(book, t_wnf, ctx, lhs.def).c, c) !== null) { return Check(tm, ty, uses_nil()); From 7febd82e712715600ec92dfbdc7c661241273441 Mon Sep 17 00:00:00 2001 From: Mathews Fernando Date: Tue, 22 Sep 2026 22:56:09 -0300 Subject: [PATCH 2/4] since u32 and f32 literals also contain numbers, term_force needs to check for k === undefined to ensure that optimization is exclusive to nat --- bend2/comp.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bend2/comp.ts b/bend2/comp.ts index 937bebdd2..ef9996a96 100644 --- a/bend2/comp.ts +++ b/bend2/comp.ts @@ -691,7 +691,7 @@ function term_force(t: HTerm): HTerm { } // a Nat literal past the cap is U32.to_nat of its word return memo(LITS, s, () => Bend.term_higher( - typeof s.v === "number" && s.v > Bend.NAT_LITERAL_MAX + s.k === undefined && typeof s.v === "number" && s.v > Bend.NAT_LITERAL_MAX ? Bend.App(Bend.Ref("U32.to_nat"), Bend.u32_to_term(s.v)) : Bend.lit_full(s))); } From d38b730356553e7cd5981bece494c31a4f888e7e Mon Sep 17 00:00:00 2001 From: Mathews Fernando Date: Tue, 22 Sep 2026 22:56:23 -0300 Subject: [PATCH 3/4] cap size --- gates/repo.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gates/repo.ts b/gates/repo.ts index e75d5a726..ef16447c5 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", 43000); +allow("bend2/bend.ts", 43300); allow("bend2/comp.ts", 64000); allow("bend2/main.ts", 10000); allow(/^bend2\/effs\/[a-z0-9_]+\.(c|js)$/, 4000); From aa823c0a558caaf1e702ec53060ab1905d71aa4b Mon Sep 17 00:00:00 2001 From: Mathews Fernando Date: Tue, 22 Sep 2026 22:56:41 -0300 Subject: [PATCH 4/4] tests for u32, f32 literals --- tests/check/f32_literal_own_f32.bend | 17 ++++++++++ tests/check/u32_literal_own_u32.bend | 17 ++++++++++ tests/compile/f32_literal_word.bend | 18 ++++++++++ tests/compile/u32_literal_word.bend | 27 +++++++++++++++ tests/parse/nat_plus_u32.bend | 16 +++++++++ tests/printer/f32_literal_print.bend | 11 +++++++ tests/printer/u32_literal_print.bend | 11 +++++++ tests/proof/f32_literal_unfolds.bend | 20 ++++++++++++ tests/proof/u32_literal_unfolds.bend | 49 ++++++++++++++++++++++++++++ 9 files changed, 186 insertions(+) create mode 100644 tests/check/f32_literal_own_f32.bend create mode 100644 tests/check/u32_literal_own_u32.bend create mode 100644 tests/compile/f32_literal_word.bend create mode 100644 tests/compile/u32_literal_word.bend create mode 100644 tests/parse/nat_plus_u32.bend create mode 100644 tests/printer/f32_literal_print.bend create mode 100644 tests/printer/u32_literal_print.bend create mode 100644 tests/proof/f32_literal_unfolds.bend create mode 100644 tests/proof/u32_literal_unfolds.bend diff --git a/tests/check/f32_literal_own_f32.bend b/tests/check/f32_literal_own_f32.bend new file mode 100644 index 000000000..8389480e2 --- /dev/null +++ b/tests/check/f32_literal_own_f32.bend @@ -0,0 +1,17 @@ +# a float literal is an F32 only where F32 declares the F32 +# constructor: a module's own F32 with another constructor checks the +# literal's word, which reports as the constructor it is +type F32 is Data: + Foo{} + +def n() -> F32: + 1.5 + +#|Error: +#|- expected : a declared constructor (F32 declares Foo) +#|- observed : 1.5 +#|Location: n +#|7 | def n() -> F32: +#|8>| 1.5 +#|9 | +#|exit 1 diff --git a/tests/check/u32_literal_own_u32.bend b/tests/check/u32_literal_own_u32.bend new file mode 100644 index 000000000..45bdc709d --- /dev/null +++ b/tests/check/u32_literal_own_u32.bend @@ -0,0 +1,17 @@ +# a literal is a U32 only where U32 declares the U32 constructor: a +# module's own U32 with another constructor checks the literal's word, +# which reports as the constructor it is +type U32 is Data: + Foo{} + +def n() -> U32: + 5 + +#|Error: +#|- expected : a declared constructor (U32 declares Foo) +#|- observed : 5 +#|Location: n +#|7 | def n() -> U32: +#|8>| 5 +#|9 | +#|exit 1 diff --git a/tests/compile/f32_literal_word.bend b/tests/compile/f32_literal_word.bend new file mode 100644 index 000000000..6304217d9 --- /dev/null +++ b/tests/compile/f32_literal_word.bend @@ -0,0 +1,18 @@ +# a float literal is one Lit node; the compiler reads it as its word, +# so a float immediate, float arithmetic and a match on float literal +# patterns reach all three lanes as the number they are +import Base + +def key(x: F32) -> U32: + match x: + case 1.5: + 10 + case 2.5: + 20 + case _: + 30 + +def main() -> IO(Unit): + IO.print(F32.show(F32.add(1.5, 2.5)) ++ " " ++ U32.show(key(1.5))) + +#|4 10 diff --git a/tests/compile/u32_literal_word.bend b/tests/compile/u32_literal_word.bend new file mode 100644 index 000000000..8ca1382fd --- /dev/null +++ b/tests/compile/u32_literal_word.bend @@ -0,0 +1,27 @@ +# a u32 literal is one Lit node; the compiler reads it as its word, so a +# wide immediate, a wrapping operation and a match on wide literal +# patterns reach all three lanes as the number they are +import Base + +def key(n: U32) -> U32: + match n: + case 0: + 10 + case 3000000000: + 20 + case 4294967295: + 30 + case _: + 40 + +def word() -> U32: + U32.add(4294967290, 10) + +def main() -> IO(Unit): + a = key(3000000000) + b = key(4294967295) + c = key(7) + d = word() + IO.print(U32.show(U32.add(a, U32.add(b, U32.add(c, d)))) ++ " " ++ Char.show('q')) + +#|94 q diff --git a/tests/parse/nat_plus_u32.bend b/tests/parse/nat_plus_u32.bend new file mode 100644 index 000000000..46db48abe --- /dev/null +++ b/tests/parse/nat_plus_u32.bend @@ -0,0 +1,16 @@ +# a nat literal plus a u32 literal is not a nat sum: 1n+5 is Succ{u32 5} +# whose field is a U32, so it is refused at a Nat rather than folded +import Base + +def main() -> Nat: + 1n+5 + +#| +#|Error: +#|- expected : Nat +#|- observed : U32 +#|Location: main +#|5 | def main() -> Nat: +#|6>| 1n+5 +#|7 | +#|exit 1 diff --git a/tests/printer/f32_literal_print.bend b/tests/printer/f32_literal_print.bend new file mode 100644 index 000000000..e70015aab --- /dev/null +++ b/tests/printer/f32_literal_print.bend @@ -0,0 +1,11 @@ +# a float literal prints back as its number, and a term built on float +# literals prints as it was written +import Base + +def wide(a: F32) -> F32: + F32.add(3.14159, a) + +def main(a: F32, b: F32) -> F32: + F32.add(wide(a), F32.add(1.5e3, b)) + +#|a => b => F32.add(F32.add(3.14159, a), F32.add(1500.0, b)) diff --git a/tests/printer/u32_literal_print.bend b/tests/printer/u32_literal_print.bend new file mode 100644 index 000000000..e22ebf44e --- /dev/null +++ b/tests/printer/u32_literal_print.bend @@ -0,0 +1,11 @@ +# a u32 literal prints back as its number, and a term built on wide +# literals prints as it was written +import Base + +def wide(a: U32) -> U32: + U32.add(3000000000, a) + +def main(a: U32, b: U32) -> U32: + U32.add(wide(a), U32.add(4294967295, b)) + +#|a => b => U32.add(U32.add(3000000000, a), U32.add(4294967295, b)) diff --git a/tests/proof/f32_literal_unfolds.bend b/tests/proof/f32_literal_unfolds.bend new file mode 100644 index 000000000..12dde662d --- /dev/null +++ b/tests/proof/f32_literal_unfolds.bend @@ -0,0 +1,20 @@ +# a float literal is one Lit node holding its bits: two spellings of +# the same f32 compare equal, and the exponent form is the same literal +import Base + +law sci_eq: + {1.5e3 == 1500.0 : F32} + +def sci_eq(): + {==} + +law exp_eq: + {1.25e-2 == 0.0125 : F32} + +def exp_eq(): + {==} + +def main() -> U32: + 0 + +#|0 diff --git a/tests/proof/u32_literal_unfolds.bend b/tests/proof/u32_literal_unfolds.bend new file mode 100644 index 000000000..0b51b2609 --- /dev/null +++ b/tests/proof/u32_literal_unfolds.bend @@ -0,0 +1,49 @@ +# a u32 literal is one Lit node whose word unfolds whole where a chain +# is read: a comparison sees a wide literal as its U32{WCon{..}} and a +# wrapping operation reduces onto one, and a match reads a wide literal +# pattern +import Base + +law wrap_inc: + {U32.inc(4294967295) == 0 : U32} + +def wrap_inc(): + {==} + +law wrap_add: + {U32.add(4294967290, 10) == 4 : U32} + +def wrap_add(): + {==} + +law add_zero: + {U32.add(3000000000, 0) == 3000000000 : U32} + +def add_zero(): + {==} + +law sub_wrap: + {U32.sub(0, 1) == 4294967295 : U32} + +def sub_wrap(): + {==} + +def classify(n: U32) -> U32: + match n: + case 3000000000: + 7 + case 4294967295: + 9 + case _: + 1 + +law classify_big: + {classify(3000000000) == 7 : U32} + +def classify_big(): + {==} + +def main() -> U32: + U32.add(classify(3000000000), classify(4294967295)) + +#|16