diff --git a/WONTFIX.txt b/WONTFIX.txt index 479defde9f..864420899d 100644 --- a/WONTFIX.txt +++ b/WONTFIX.txt @@ -17,8 +17,10 @@ The checker skips dead code (#820, #878, #973, #1091) so `(x => x(x))(x => x(x))` never ends (#973). `~` template arguments are compile-time (#784) - A `~` argument must be closed. A def parameter is a runtime value, so it - cannot fill one. Pass the function as a plain argument instead. + In live code a `~` argument must be closed. A def parameter is a runtime + value, so pass it as a plain argument instead. In a type, `--verdict` + lifts captured runtime Data into explicit kernel parameters (#1483); + this does not admit runtime captures in live template applications. Allocation failure fail-stops the runtime (#792) Out of memory is fatal everywhere, not a `Fail`. A program bounds the `max` diff --git a/bend2/safe.ts b/bend2/safe.ts index 0e0954350c..c6d1fa0645 100644 --- a/bend2/safe.ts +++ b/bend2/safe.ts @@ -36,8 +36,9 @@ // Quant is a kernel value like any other, and a kind converts in the // kernel where it does in bend2: Kind(&0) is *(.Q0), and fits *(.Q1) // (Type) only as bend2's LE does. An item (a book name) goes out -// once per tuple of closed arguments at its template (~) parameters, with -// those parameters gone. Every def goes out after the defs its live code +// once per tuple of template (~) arguments, closed up to explicitly lifted +// Data captures. The ~ parameters go; the captures are kernel parameters. +// Every def goes out after the defs its live code // names; a name in a type may come later. A def with no body (a law, a // native, a foreign fill) goes out opaque at a model: the kernel checks // the model, then never unfolds the def. What the kernel cannot express @@ -108,7 +109,7 @@ type Chain = { n: number; cv: number[] }; // (a tag's fields follow it), whether the tree is built only to count // its uses, and whether it is built again for a convoy type Scope = { c: Bind[]; d: number; D: number; cols: Cols; - self: string; empty: O[]; sub: boolean; kq: Q[]; tags: number[]; dry: boolean; again: boolean }; + self: string; empty: O[]; sub: boolean; kq: Q[]; tags: number[]; dry: boolean; again: boolean; caps?: Map }; // the elaboration: the book, the book models read (a root's constant at // its model), the defs out (an opaque one flagged), each item's kernel @@ -135,6 +136,8 @@ type Safe = { grew: boolean; consts: Map; uses: WeakMap>; + capkeys: Map; + captypes: Map; }; // a model search's fuel left, its round's depth, and whether that round @@ -201,7 +204,7 @@ function safe_book(book: Book): { text: string; oos: Array<[Name, string]> } { function safe_pass(book: Book, groups: Map, inst: Safe["inst"]): { text: string; oos: Array<[Name, string]> } | null { const g0 = groups.size; const e: Safe = { book, mb: { ...book, tlds: Object.create(book.tlds) as Book["tlds"] }, out: [], names: new Map(), seen: new Set(), - todo: [], taken: new Set(), fail: new Map(), groups, inst, stack: [], going: new Set(), grew: false, consts: new Map(), uses: new WeakMap() }; + todo: [], taken: new Set(), fail: new Map(), groups, inst, stack: [], going: new Set(), grew: false, consts: new Map(), uses: new WeakMap(), capkeys: new Map(), captypes: new Map() }; const roots: Array<[Name, string]> = []; for (const k of [...new Set([...book.order].reverse())].reverse().filter((k) => book.tlds[k].b !== true)) { try { @@ -371,9 +374,9 @@ function item_emit(e: Safe, k: Name, cols: Cols, n: string): void { function def_emit(e: Safe, k: Name, cols: Cols, n: string, tld: Def): void { const T = B.tele_fill(e.book, tld.T, cols.slice(0, tld.x) as HTerm[], B.ctx_nil()); const t = tld.e !== undefined ? null : model(e, T) ?? oos("no model for " + (tld.i === undefined ? "" : (tld.b === true ? "base's" : "the") + " foreign def ") + B.name_key(k)); - const s = { ...scope_nil(), self: n }; + const { s, ps: cps } = spec_scope(e, cols, n); const To = term(e, s, T, false); - e.out.push([n, To, t === null ? arm(e, s, k, cols, []) : tree(e, s, t, []), t !== null]); + e.out.push([n, alls(cps, To), lams(e, cps, t === null ? arm(e, s, k, cols, []) : tree(e, s, t, [])), t !== null]); } // D.arms and D, at D's specialized arguments @@ -422,9 +425,83 @@ function tele_open(e: Safe, s: Scope, T: HTerm, cols: Cols, n: number): { s: Sco // Specialize // ---------- -// a specialized argument: closed, in normal form +// Close a specialized argument over explicit kernel parameters, rather +// than treating a run-time capture as a global constant. function spec_val(e: Safe, s: Scope, x: HTerm): HTerm { - return closed_val(e, s, x) ?? oos("a template argument that depends on a run-time value"); + const cap = (i: number): HTerm => { + const b = s.c[i]; + if (b?.T == null) { + return oos("a captured variable without its checked type"); + } + const T = close(b.T); + const key = i + "\n" + B.term_key(B.term_lower(T)); + let k = e.capkeys.get(key); + if (k === undefined) { + k = "\0capture" + e.captypes.size; + e.capkeys.set(key, k); + e.captypes.set(k, T); + } + s.caps!.set(k, { ...b, T }); + return B.Ref(k); + }; + const close = (t: HTerm): HTerm => subst(t, s.d, (o) => + o.$ === "Var" && (o.i as number) >= 0 && (o.i as number) < s.d + ? s.c[o.i as number]?.v ?? cap(o.i as number) : undefined); + return B.term_snf(e.book, close(x)); +} + +// Captures precede dependants, so a captured value's type may name an +// earlier captured type or index. +function spec_caps(e: Safe, cols: Cols): Name[] { + if (e.captypes.size === 0) { + return []; + } + const out = new Set(); + const visit = (x: unknown): void => { + if (typeof x !== "object" || x === null) { + return; + } + const o = x as Record; + if (o.$ === "Ref" && e.captypes.has(o.k as Name)) { + const k = o.k as Name; + if (!out.has(k)) { + visit(B.term_lower(e.captypes.get(k)!)); + out.add(k); + } + } else { + for (const [k, v] of Object.entries(o)) { + if (k !== "s") visit(v); + } + } + }; + for (const c of cols) { + if (c !== null) visit(B.term_lower(c)); + } + return [...out]; +} + +// A lifted instance's explicit capture prefix, shared by ordinary defs +// and the selector encoding of a mutually recursive group. +function spec_scope(e: Safe, cols: Cols, self: string): { s: Scope; ps: Binder[] } { + let s = { ...scope_nil(), self }; + const ps: Binder[] = []; + const cs = spec_caps(e, cols); + if (cs.length > 0) s.caps = new Map(); + for (const c of cs) { + const T = e.captypes.get(c)!; + ps.push([2, s.D, term(e, s, T, false)]); + s.caps!.set(c, { o: { $: "Var", l: s.D }, T }); + s = scope_kq(scope_hide(s), s.D, 2); + } + return { s, ps }; +} + +function spec_apply(e: Safe, s: Scope, cols: Cols, head: O): O { + for (const c of spec_caps(e, cols)) { + head = { $: "App", q: 2, f: head, + x: s.caps?.get(c)?.o ?? oos("a capture outside its scope") }; + } + return head; } // x's normal form, when it is closed; null when it depends on a run-time value @@ -596,6 +673,7 @@ function scope_move(s: Scope, a: number, b: number): Scope { const mv = (o: O): O => o.$ === "Var" ? (o.l === a ? { $: "Var", l: b } : o) : Object.fromEntries(Object.entries(o).map(([k, v]) => [k, is_o(v) ? mv(v) : v])) as O; return { ...s, c: s.c.map((x) => x === undefined ? x : { ...x, o: mv(x.o) }), empty: s.empty.map(mv), + caps: s.caps === undefined ? undefined : new Map([...s.caps].map(([k, b]) => [k, { ...b, o: mv(b.o) }])), tags: s.tags.flatMap((t) => t === a ? [t, b] : [t]) }; } @@ -979,6 +1057,10 @@ function term(e: Safe, s0: Scope, t: HTerm, live: boolean): O { function spine(e: Safe, s: Scope, t: HTerm, live: boolean): O { const [h, xs] = unapply(t); const [f, T] = open(h); + if (f.$ === "Ref" && s.caps?.has(f.k)) { + const b = s.caps.get(f.k)!; + return args(e, s, { $: "Ann", x: b.o, T: term(e, s, b.T!, false) }, b.T, xs, live); + } if (f.$ !== "Ref") { const U = f.$ === "Var" ? s.c[f.i]?.T ?? null : T; const o = term(e, s, h, live); @@ -1007,7 +1089,11 @@ function args(e: Safe, s: Scope, k: Name | O, T: HTerm | null, xs: HTerm[], live if (F?.$ !== "All") { return oos("an application past its head's known type"); } - const v = j < nx ? spec_val(e, s, x) : null; + let v = j < nx ? closed_val(e, s, x) : null; + if (j < nx && v === null) { + s = { ...s, caps: new Map(s.caps) }; + v = spec_val(e, s, x); + } ps.push([quant(F.q), x, F.A, v]); U = F.B(v ?? x); }); @@ -1026,8 +1112,9 @@ function args(e: Safe, s: Scope, k: Name | O, T: HTerm | null, xs: HTerm[], live throw x; } const a = { ...s, sub: live && n === s.self }; - return ps.filter((p) => p[3] === null).reduce((f, [q, x, A]) => ({ $: "App", q, f, x: arg_term(e, a, x, A, live && q > 0) }), - n === null ? k as O : { $: "Ref", k: n }); + const head: O = n === null ? k as O + : spec_apply(e, s, ps.map((p) => p[3]), { $: "Ref", k: n }); + return ps.filter((p) => p[3] === null).reduce((f, [q, x, A]) => ({ $: "App", q, f, x: arg_term(e, a, x, A, live && q > 0) }), head); } // Group @@ -1140,7 +1227,8 @@ function group_call(e: Safe, s: Scope, g: Group, m: Name, ps: Arg[], R: HTerm, l v !== null ? [] : [[qs[j] ?? q, arg_term(e, a, x, A, live && (qs[j] ?? q) > 0)]]); const sel: O = { $: "Tup", q: 1, a: { $: "Lab", k: name_tt(g.k) }, b: { $: "Lab", k: "()" } }; const x = [...args(ps.slice(0, n), g.qs), [1, m === g.k ? sel : { $: "Tup", q: 1, a: { $: "Lab", k: name_tt(m) }, b: sel }] as [Q, O], - ...args(ps.slice(n), [])].reduce((f, [q, x]) => ({ $: "App", q, f, x }), { $: "Ref", k }); + ...args(ps.slice(n), [])].reduce((f, [q, x]) => ({ $: "App", q, f, x }), + spec_apply(e, s, ps.slice(0, n).map((p) => p[3]), { $: "Ref", k })); return { $: "Ann", x, T: term(e, s, R, false) }; } @@ -1148,7 +1236,8 @@ function group_call(e: Safe, s: Scope, g: Group, m: Name, ps: Arg[], R: HTerm, l // (MODE s), MODE the selected member's other parameters and type; its // tree convoys the lead's q=1 variables through the selector's match function group_emit(e: Safe, g: Group, cols: Cols, n: string): void { - const { s, ps: ls, xs: lead } = tele_open(e, { ...scope_nil(), self: n }, e.book.tlds[g.k].T, cols, g.qs.length); + const cap = spec_scope(e, cols, n); + const { s, ps: ls, xs: lead } = tele_open(e, cap.s, e.book.tlds[g.k].T, cols, g.qs.length); // member m past the lead, from scope s1 on: its binders, its terms (but // at its specialized parameters), its cols and type const rest = (s1: Scope, m: Name) => { @@ -1179,7 +1268,7 @@ function group_emit(e: Safe, g: Group, cols: Cols, n: string): void { return lams(e, r.ps, arm(e, r.s, m, r.cs, r.vs)); }, [])); const v = ks.reduce((f, l) => ({ $: "App", q: 1, f, x: { $: "Var", l } }), { $: "App", q: 1, f: body, x: { $: "Var", l: l0 } }); - e.out.push([n, To, lams(e, [...ls, [1, l0]], v), false]); + e.out.push([n, alls(cap.ps, To), lams(e, [...cap.ps, ...ls, [1, l0]], v), false]); } // def k's checked tree at the terms vs (its parameters left to right, diff --git a/tests/check/template_type_capture.bend b/tests/check/template_type_capture.bend new file mode 100644 index 0000000000..612b869547 --- /dev/null +++ b/tests/check/template_type_capture.bend @@ -0,0 +1,51 @@ +# A type-only template can close over run-time Data. Its kernel instance +# must take the actual captures, not freeze them as global constants. +import Base + +def least(lo: Nat, xs: List<&2, Nat>) -> Data: + {List.all(~&2, ~Nat, ~(y => Nat.is_le(lo, y)), xs) == True{} : Bool} + +def least_nil(lo: Nat) -> least(lo, Nil{}): + {==} + +def below(lo: Nat, xs: List<&2, Nat>) -> Data: + {List.all(~&2, ~Nat, ~(y => Nat.is_le(lo, y)), xs) == False{} : Bool} + +def below_one() -> below(2n, [1n]): + {==} + +def bounded(lo: Nat, hi: Nat, xs: List<&2, Nat>) -> Data: + {List.all(~&2, ~Nat, ~(y => Bool.and(Nat.is_le(lo, y), Nat.is_le(y, hi))), xs) == True{} : Bool} + +def bounded_nil(lo: Nat, hi: Nat) -> bounded(lo, hi, Nil{}): + {==} + +def bounded_two() -> bounded(2n, 3n, [2n, 3n]): + {==} + +def outside(lo: Nat, hi: Nat, xs: List<&2, Nat>) -> Data: + {List.all(~&2, ~Nat, ~(y => Bool.and(Nat.is_le(lo, y), Nat.is_le(y, hi))), xs) == False{} : Bool} + +def above_three() -> outside(2n, 3n, [4n]): + {==} + +def shifted(+unused: Nat, lo: Nat, xs: List<&2, Nat>) -> Data: + {List.all(~&2, ~Nat, ~(y => Nat.is_le(lo, y)), xs) == False{} : Bool} + +def shifted_one() -> shifted(99n, 2n, [1n]): + {==} + +type Bounds is Data: + Bounds{lo: Nat, hi: Nat} + +def allows(b: Bounds, +y: Nat) -> Bool: + Bounds{lo, hi} = b + Bool.and(Nat.is_le(lo, y), Nat.is_le(y, hi)) + +def record_bound(b: Bounds, xs: List<&2, Nat>) -> Data: + {List.all(~&2, ~Nat, ~(y => allows(b, y)), xs) == True{} : Bool} + +def record_two() -> record_bound(Bounds{2n, 3n}, [2n, 3n]): + {==} + +#|ALL PROOFS CHECK