diff --git a/bend2/bend.ts b/bend2/bend.ts index 35db96c73b..608f4b47e1 100644 --- a/bend2/bend.ts +++ b/bend2/bend.ts @@ -66,11 +66,11 @@ // Tuple | "(" A ("," B)+ ")" | Tuple{A, Tuple{B, ..}} // 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)? | Succ{..Zero{}}, Succ{..T} +// 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{}}} // 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 and a nat stay one Lit node and unfold a unit 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 | number } // "text", 3n | { $: "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 | number, 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,35 +1174,58 @@ export function u32_to_term(n: U32, s?: Span): LTerm { return Ctr("U32", [word_to_term(n, s)], 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. -export const NAT_LITERAL_MAX = 256; +// Lit +// === +// a string or nat literal is one node holding its text or number: it +// means its chain (SCon per character, Succ per unit) and unfolds one +// 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. + +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)); +} -export function nat_to_term(n: number, s?: Span): LTerm { - if (n > NAT_LITERAL_MAX) { - return App(Ref("U32.to_nat", s), u32_to_term(n, s), s); +// 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 (typeof t.v === "number") { + return t.v === 0 ? Ctr("Zero", [], t.s) : Ctr("Succ", [Lit(t.v - 1, t.s)], t.s); } - let out: LTerm = Ctr("Zero", [], s); - for (let i = 0; i < n; i++) { - out = Ctr("Succ", [out], s); + 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); +} + +// the whole chain: a pattern's view +export function lit_full(t: Extract): LTerm { + if (typeof t.v === "string") { + return lit_chain([...t.v].map((c) => c.codePointAt(0) as U32), t.s); + } + let out: LTerm = Ctr("Zero", [], t.s); + for (let i = 0; i < t.v; i++) { + out = Ctr("Succ", [out], t.s); } return out; } +// past it, "n + T" is Nat.add(n, T) and the compiler emits U32.to_nat(n) +export const NAT_LITERAL_MAX = 256; + +// a Succ chain's count, with the literal it may end in export function nat_from_term(t: LTerm): number | null { let n = 0; while (t.$ === "Ctr" && t.k === "Succ" && t.x.length === 1) { n += 1; t = t.x[0]; } - if (t.$ === "Ctr" && t.k === "Zero" && t.x.length === 0) { - return n; - } - if (n === 0 && t.$ === "App" && t.f.$ === "Ref" && t.f.k === "U32.to_nat") { - return u32_from_term(t.x); - } - return null; + return t.$ === "Ctr" && t.k === "Zero" && t.x.length === 0 ? n + : t.$ === "Lit" && typeof t.v === "number" ? n + t.v : null; } export function u32_from_term(tm: TermOf, k: Name = "U32"): number | null { @@ -1278,11 +1315,12 @@ export function term_show(term: LTerm, top: number = -1, bnd: Name[] = []): stri return [xs, t]; } function term_show_sugar_nat(tm: LTerm, prc: number): string | null { + const k = nat_from_term(tm); + if (k !== null) { + return String(k) + "n"; + } const [xs, t] = term_show_chain(tm, "Succ", 1); const n = xs.length; - if (t.$ === "Ctr" && t.k === "Zero" && t.x.length === 0) { - return String(n) + "n"; - } if (n === 0) { return null; } @@ -1321,12 +1359,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 +1369,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" && typeof t.v === "string" ? 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 +1478,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 typeof tm.v === "number" ? String(tm.v) + "n" : "\"" + lit_text(tm.v) + "\""; + } case "Mat": { const arms: string[] = []; let m: LTerm = tm; @@ -1739,13 +1785,6 @@ export function parse_bind(p: Parse, t: LTerm): PVar { export function parse_patt(p: Parse, t: LTerm): Patt { const book = p.book; - const lit = t.$ === "App" ? nat_from_term(t) : null; - if (lit !== null) { - t = Ctr("Zero", [], t.s); - for (let i = 0; i < lit; i++) { - t = Ctr("Succ", [t], t.s); - } - } switch (t.$) { case "Var": { if (book_ctr(book, parse_reso(p, t.k)) !== null) { @@ -1763,6 +1802,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_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); } @@ -1969,7 +2011,7 @@ export function parse_term_base(p: Parse, beg: Loc): LTerm { if (k === 0 || (k & (k - 1)) !== 0) { throw Err(p.book, ctx_nil(), "a power of two count (^d takes a depth)", undefined, n.s); } - d = nat_to_term(Math.log2(k), n.s); + d = Lit(Math.log2(k), n.s); } return App(App(App(Ref("Array.new", s), T, s), d, s), xs[0], s); } @@ -1996,10 +2038,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); @@ -2283,8 +2322,11 @@ 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) { + return Lit(n + out.v, spn); + } if (n > NAT_LITERAL_MAX) { - return App(App(Ref("Nat.add", spn), nat_to_term(n, spn), spn), out, spn); + return App(App(Ref("Nat.add", spn), Lit(n, spn), spn), out, spn); } for (let i = 0; i < n; i++) { out = Ctr("Succ", [out], spn); @@ -2294,7 +2336,7 @@ export function parse_term_num(p: Parse): LTerm { if (char_is_name(parse_peek(p))) { parse_fail(p, "a nat literal (NUMBER n)"); } - return nat_to_term(n, parse_span(p, beg)); + return Lit(n, parse_span(p, beg)); } export function parse_fill(p: Parse, k: Name, xs: LTerm[], s?: Span): LTerm[] { @@ -2720,7 +2762,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 +3055,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 +3152,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 +3194,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 +3204,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 +3277,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) @@ -3448,7 +3506,8 @@ export function term_infer(book: Book, lhs: LHS, tm: HTerm, qt: Quant, ctx: Ctx, // ------------------------------------------- infer-err // Γ ⊢ x : ⊥ (a goal is needed) default: { - if (tm.$ === "Ctr" && book_ctr(book, tm.k) === null) { + const t = tm.$ === "Lit" ? lit_step(tm) : tm; + if (t.$ === "Ctr" && book_ctr(book, t.k) === null) { throw Err(book, ctx, "a declared constructor", tm, tm.s, lhs.def); } throw Err(book, ctx, "an annotated term (cannot infer)", tm, tm.s, lhs.def); @@ -3559,6 +3618,21 @@ 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 (or Nat) with the literal's head: SNil or SCon (Zero or Succ) + // 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 [T, c] = typeof tm.v === "number" ? ["Nat", tm.v === 0 ? "Zero" : "Succ"] + : ["String", tm.v === "" ? "SNil" : "SCon"]; + if (t_wnf.$ === "ADT" && t_wnf.k === T + && ctrs_find(book_adt(book, t_wnf, ctx, lhs.def).c, c) !== 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 8576a3c74e..74205fe129 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 = new Map(); + // Name // ==== @@ -679,6 +681,7 @@ function tpl(t: Gen, xs: string[]): string { function tpl_nat(u: string, f: string): Gen { return ([p]) => /^\d/.test(p) ? (BigInt(parseInt(p)) + 1n) + u + : /^nat_chk\(.* \+ \d+n?\)$/.test(p) ? p.replace(/(\d+)(n?)\)$/, (_, k, n) => `${+k + 1}${n})`) : tpl(f, [p]); } @@ -696,7 +699,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 @@ -784,7 +787,7 @@ function term_eta(book: Bend.Book, t: HTerm, T: HTerm, n: number): HTerm { } function term_kids(cf: Carb, tm: HTerm): HTerm[] { - const t = Bend.term_force(tm); + const t = term_lit(Bend.term_force(tm)); switch (t.$) { case "Ann": return [t.x]; case "Lam": return [term_open(t).b]; @@ -807,7 +810,7 @@ function term_kids(cf: Carb, tm: HTerm): HTerm[] { // tail position (under annotations, binders, arms and let bodies). function term_any(cf: Carb, t: HTerm, p: (s: HTerm, tail: boolean) => boolean, tail = true, seen: Set = new Set()): boolean { - const s = Bend.term_force(t); + const s = term_lit(Bend.term_force(t)); if (seen.has(s)) { return false; } @@ -828,8 +831,13 @@ function term_nodes(cf: Carb, t: HTerm): number { return n; } +function term_lit(t: HTerm): HTerm { + return t.$ === "Lit" ? memo(LITS, t, () => Bend.term_higher(typeof t.v === "number" && t.v > Bend.NAT_LITERAL_MAX + ? Bend.App(Bend.Ref("U32.to_nat"), Bend.u32_to_term(t.v)) : 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 +937,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 { @@ -2389,7 +2397,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 352704d3a8..d1df0b5f39 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", 43000); allow("bend2/comp.ts", 65000); allow("bend2/main.ts", 10000); allow(/^bend2\/effs\/[a-z0-9_]+\.(c|js)$/, 4000); diff --git a/tests/check/nat_literal_own_nat.bend b/tests/check/nat_literal_own_nat.bend new file mode 100644 index 0000000000..fb5dd024d9 --- /dev/null +++ b/tests/check/nat_literal_own_nat.bend @@ -0,0 +1,16 @@ +# a literal is a Nat only where Nat declares Succ and Zero: a module's +# own Nat with other constructors rejects it +type Nat is Data: + Foo{} + +def n() -> Nat: + 3n + +#|Error: +#|- expected : a declared constructor (Nat declares Foo) +#|- observed : 3n +#|Location: n +#|6 | def n() -> Nat: +#|7>| 3n +#|8 | +#|exit 1 diff --git a/tests/check/nat_literal_pattern_empty.bend b/tests/check/nat_literal_pattern_empty.bend index 59a30218fe..f33f6c19b3 100644 --- a/tests/check/nat_literal_pattern_empty.bend +++ b/tests/check/nat_literal_pattern_empty.bend @@ -1,7 +1,7 @@ # the unchecked literal pattern let a closed term inhabit Empty: the -# longhand U32.to_nat(0) matched a Zero that carries a field as a bare -# Zero, the arm's goal became @w:U -> Empty, and the self-call f(q) -# passed without descending. the literal is refused like Zero{} is +# literal 0n matched a Zero that carries a field as a bare Zero, the +# arm's goal became @w:U -> Empty, and the self-call f(q) passed without +# descending. the literal is refused like Zero{} is type U is Data: Un{} type N is Data: @@ -13,7 +13,7 @@ type Empty is Data: def f(b: N) -> Empty: match b: - case U32.to_nat(0): + case 0n: {\{K: q => w => f(q)} : D -> U -> Empty}(K{Zero{Un{}}}) case Succ{p}: f(p) @@ -25,6 +25,6 @@ def boom() -> Empty: #|- message : a Zero pattern with 1 field #|Location: #|15 | match b: -#|16>| case U32.to_nat(0): +#|16>| case 0n: #|17 | {\{K: q => w => f(q)} : D -> U -> Empty}(K{Zero{Un{}}}) #|exit 1 diff --git a/tests/check/string_literal_descends.bend b/tests/check/string_literal_descends.bend new file mode 100644 index 0000000000..93bbaf2483 --- /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_long.bend b/tests/check/string_literal_long.bend new file mode 100644 index 0000000000..51e9dd3a93 --- /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_own_string.bend b/tests/check/string_literal_own_string.bend new file mode 100644 index 0000000000..433b2da91c --- /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 diff --git a/tests/compile/nat_pattern_deep.bend b/tests/compile/nat_pattern_deep.bend new file mode 100644 index 0000000000..09c9e2afdb --- /dev/null +++ b/tests/compile/nat_pattern_deep.bend @@ -0,0 +1,16 @@ +# a literal pattern past 256 whose default arm uses the scrutinee rebuilds +# it as one checked sum, nat_chk(e, x + 300), not a check per Succ: 300 +# nested calls topped clang's bracket nesting and the C lane failed +import Base + +def down(n: Nat) -> Nat: + match n: + case 300n: + down(299n) + case _: + n + +def main() -> Nat: + Nat.add(down(300n), down(7n)) + +#|306n diff --git a/tests/printer/nat_literal_print.bend b/tests/printer/nat_literal_print.bend new file mode 100644 index 0000000000..2f5e8a924d --- /dev/null +++ b/tests/printer/nat_literal_print.bend @@ -0,0 +1,17 @@ +# a nat literal prints back as a literal, a Succ chain that ends in a +# literal prints as one number, and "n + T" past 256 is Nat.add +import Base + +def small(n: Nat) -> Nat: + 2n+n + +def big(n: Nat) -> Nat: + 300n+n + +def chain() -> Nat: + Succ{Succ{300n}} + +def main(a: Nat, b: Nat) -> Nat: + Nat.add(small(a), Nat.add(big(b), Nat.add(chain(), 4294967295n))) + +#|a => b => 2n+Nat.add(a, 300n+Nat.add(b, 4294967597n)) diff --git a/tests/printer/string_literal_tail.bend b/tests/printer/string_literal_tail.bend new file mode 100644 index 0000000000..ec7050e769 --- /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/nat_literal_unfolds.bend b/tests/proof/nat_literal_unfolds.bend new file mode 100644 index 0000000000..e4dbce4d47 --- /dev/null +++ b/tests/proof/nat_literal_unfolds.bend @@ -0,0 +1,69 @@ +# a nat literal is one Lit node in the checker; it unfolds a Succ at a +# time where a chain is read: 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, and the +# evaluator steps through a literal's count. the laws hold the patterns +# past 256: a compiled match on one rebuilds its scrutinee 300 deep, +# past clang's bracket nesting. +import Base + +law big_is_succ: + {300n == Succ{299n} : Nat} + +def big_is_succ(): + {==} + +law zero_is_zero: + {0n == Zero{} : Nat} + +def zero_is_zero(): + {==} + +law add_lits: + {Nat.add(999n, 1n) == 1000n : Nat} + +def add_lits(): + {==} + +def classify(n: Nat) -> Nat: + match n: + case 300n: + 1n + case 5n: + 2n + case _: + 0n + +law classify_big: + {classify(300n) == 1n : Nat} + +def classify_big(): + {==} + +def down(n: Nat) -> Nat: + match n: + case 300n: + down(299n) + case _: + n + +law down_steps: + {down(300n) == 299n : Nat} + +def down_steps(): + {==} + +def small(n: Nat) -> Nat: + match n: + case 5n: + 2n + case _: + 0n + +def bound() -> Nat: + 4294967295n + +def main() -> List: + [small(5n), small(7n), Nat.add(299n, 1n), Nat.add(0n, bound())] + +#|[2n, 0n, 300n, 4294967295n] diff --git a/tests/proof/string_literal_unfolds.bend b/tests/proof/string_literal_unfolds.bend new file mode 100644 index 0000000000..2126f57368 --- /dev/null +++ b/tests/proof/string_literal_unfolds.bend @@ -0,0 +1,70 @@ +# 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. +# a character is any u32, so a literal may spell a surrogate pair. +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(): + {==} + +law surrogates_two: + {String.length("\u{d83d}\u{de00}") == 2n : Nat} + +def surrogates_two(): + {==} + +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]