diff --git a/bend2/bend.ts b/bend2/bend.ts index 35db96c73..8d470e909 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,36 @@ 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); +} + +// 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 // 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 +1365,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 +1375,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 +1484,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 +1815,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); } @@ -1996,10 +2051,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 +2772,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 +3065,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 +3162,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 +3204,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 +3214,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 +3287,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 +3627,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..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 { @@ -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 352704d3a..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", 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/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_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_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 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..2126f5736 --- /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]