From ebcdf3abac8fc61232e58d74976d83f956de586b Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 9 Oct 2026 09:00:52 +0000 Subject: [PATCH 1/7] fix: emit consume continuations past five sequent premises A datatype rule with six or more premises over another user type compiled a shen.consume helper whose continuation captured 17 or more locals (two per premise variable, plus the assumption and engine temps). mkhandle refused past 16 captures, so the helper was never registered in NativePred and the caller died with "shen.consumeN is undefined". Five premises captured 15 and fit NEWCONT16. Wider handles now use the existing NEWCONTV path. Co-authored-by: pyrex41 --- prolog_compile.lua | 14 ++- scripts/run-tests.lua | 1 + test/datatype_consume_spec.lua | 150 +++++++++++++++++++++++++++++++++ 3 files changed, 161 insertions(+), 4 deletions(-) create mode 100644 test/datatype_consume_spec.lua diff --git a/prolog_compile.lua b/prolog_compile.lua index eaf5e1b..a388b54 100644 --- a/prolog_compile.lua +++ b/prolog_compile.lua @@ -775,11 +775,15 @@ end -- a zero-param static used as a continuation value: wrap into a handle function CtxMT.mkhandle(ctx, st, out, d) - -- captures = the static's free vars (numbers) - if #st.fvs > 16 then refuse(ctx, "handle captures > 16") end + -- captures = the static's free vars (numbers). NEWCONT0..16 stay + -- monomorphic so LuaJIT traces them. A consume helper for a sequent + -- premise closes over two locals per premise variable plus the + -- assumption and the engine temps (2*N+5): five premises fit in 16, + -- six need 17. Wider handles take NEWCONTV, the same varargs path + -- lift_cont uses. Refusing left NativePred[shen.consumeN] unset, and + -- the compiled caller then died with "shen.consumeN is undefined". local fname = liftname(ctx, "LH") local decls, parts = {}, { fname } - local penv = setmetatable({}, { __index = st.env }) local args = {} for i, vn in ipairs(st.fvs) do decls[#decls + 1] = " local c" .. i .. " = CAPREF(base, " .. (i - 1) .. ")" @@ -791,7 +795,9 @@ function CtxMT.mkhandle(ctx, st, out, d) def[#def + 1] = " return " .. st.fn .. "(" .. table.concat(args, ", ") .. ")" def[#def + 1] = "end" ctx.buf[#ctx.buf + 1] = table.concat(def, "\n") - return "NEWCONT" .. #st.fvs .. "(" .. table.concat(parts, ", ") .. ")" + local ncap = #st.fvs + local mk = (ncap <= 16) and ("NEWCONT" .. ncap) or "NEWCONTV" + return mk .. "(" .. table.concat(parts, ", ") .. ")" end -- --------------------------------------------------------------------------- diff --git a/scripts/run-tests.lua b/scripts/run-tests.lua index a1103bd..03e7040 100644 --- a/scripts/run-tests.lua +++ b/scripts/run-tests.lua @@ -32,6 +32,7 @@ local specs = { "test/boot_cache_spec.lua", "test/cli_spec.lua", "test/checked_integer_spec.lua", + "test/datatype_consume_spec.lua", "test/engine_spec.lua", "test/error_robustness_spec.lua", "test/eval_order_spec.lua", diff --git a/test/datatype_consume_spec.lua b/test/datatype_consume_spec.lua new file mode 100644 index 0000000..75eba21 --- /dev/null +++ b/test/datatype_consume_spec.lua @@ -0,0 +1,150 @@ +-- datatype_consume_spec.lua — sequent rules with many premises. +-- +-- luajit test/datatype_consume_spec.lua +-- +-- A datatype rule whose conclusion context has six or more premises over +-- another user type used to die, once that rule was entered, with +-- "shen.consume is undefined". Five premises worked. +-- +-- shen.specialise-consume gensyms a helper per premise. The native Prolog +-- translator closure-converts that helper's continuation, and the capture +-- count is two locals per premise variable plus the assumption and engine +-- temps (2*N+5). Five premises capture 15 values and fit NEWCONT0..16. +-- Six premises capture 17. mkhandle refused past 16, so NativePred[name] +-- stayed nil and the already-translated caller invoked a missing field. +-- +-- Entering the rule does not require the query to use it: after the datatype +-- is loaded, any typecheck that walks *datatypes* and reaches the predicate +-- (here, "2 : piece", which fails the earlier piece rule) calls it. A +-- matching hypothesis must still succeed, and a miss must still fail. + +local shen = require("shen") +shen.boot{ quiet = true } +local R = require("runtime") +local P = shen.prims +local E = require("prolog_engine") + +local pass, fail = 0, 0 +local function check(desc, got, want) + if got == want then + pass = pass + 1 + else + fail = fail + 1 + print(string.format("FAIL %s: got %s want %s", desc, tostring(got), tostring(want))) + end +end + +local function errmsg(err) + if type(err) == "string" then return P.translate_error(err) end + if type(err) ~= "table" then return P.translate_error(tostring(err)) end + local parts = {} + for k, v in pairs(err) do + parts[#parts + 1] = tostring(k) .. "=" .. tostring(v) + end + return table.concat(parts, " | ") +end + +-- Kernel shen.typecheck, not the embedding helper: the helper turns every +-- error into false, which would hide "shen.consumeN is undefined". +local function typecheck(expr, ty) + P.GLOBALS["shen.*infs*"] = 0 + local forms = P.F["read-from-string"](expr .. " : " .. ty) + local ok, res = pcall(P.F["shen.typecheck"], forms[1], forms[2][2][1]) + if not ok then return nil, errmsg(res) end + return res +end + +local CONS = R.intern("cons") +local COLON = R.intern(":") +local PIECE = R.intern("piece") + +local function cons_form(a, b) + return R.cons(CONS, R.cons(a, R.cons(b, R.NIL))) +end + +local function list_form(xs) + local t = R.NIL + for i = #xs, 1, -1 do t = cons_form(xs[i], t) end + return t +end + +local function judgement(term, ty) + return R.cons(term, R.cons(COLON, R.cons(ty, R.NIL))) +end + +-- Run the datatype predicate the way search-user-datatypes does. +local function run_rule(name, goal, assum) + local fn = E.NativePred[name .. "#type"] + if fn == nil then return nil, "no native predicate " .. name end + local q = E.query_begin() + local done = E.newcont0(function() return true end) + local ok, res = pcall(fn, E.import_cached(goal), E.import_cached(assum), 0, done) + E.query_end(q) + if not ok then return nil, errmsg(res) end + return res +end + +local function varname(i) return string.char(64 + i) end + +local function define_row(n) + local vars, jud = {}, {} + for i = 1, n do + vars[i] = varname(i) + jud[i] = vars[i] .. " : piece" + end + local name = "row" .. n + shen.eval(string.format([[ +(datatype %s + %s >> P; + %s + [%s] : %s >> P;) +]], name, table.concat(jud, ", "), string.rep("_", 16), + table.concat(vars, " "), name)) + return name +end + +shen.eval([[ +(datatype piece + if (element? X [0 1]) + _____________________ + X : piece;) +]]) + +-- Five is the last width that fit the old 16-capture helper. Six is the +-- first that used to be missing. Eight and twelve sit past that threshold +-- and under the later metatable-chain limit on very deep clauses. +for _, n in ipairs({ 5, 6, 8, 12 }) do + local name = define_row(n) + local ty, err = typecheck("0", "piece") + check(n .. " premises: 0 : piece still holds", + err or R.to_str(ty), "piece") + local ty2, err2 = typecheck("2", "piece") + check(n .. " premises: walking the rule does not raise", err2, nil) + check(n .. " premises: 2 : piece is not a piece", + ty2 == false, true) + + local elems = {} + for i = 1, n do elems[i] = (i % 2 == 0) and 1 or 0 end + local row = list_form(elems) + local hyp = R.cons(judgement(row, R.intern(name)), R.NIL) + local goal = judgement(0, PIECE) + local hit, herr = run_rule(name, goal, hyp) + check(n .. " premises: matching hypothesis fires the rule", + herr or hit, true) + local miss, merr = run_rule(name, goal, R.NIL) + check(n .. " premises: empty context misses", merr or miss, false) + + local short = {} + for i = 1, n - 1 do short[i] = 0 end + local bad = R.cons(judgement(list_form(short), R.intern(name)), R.NIL) + local wrong, werr = run_rule(name, goal, bad) + check(n .. " premises: short hypothesis misses", werr or wrong, false) + + local nope = judgement(2, PIECE) + local no, nerr = run_rule(name, nope, hyp) + check(n .. " premises: unpacked rule does not prove 2 : piece", + nerr or no, false) +end + +print(string.format("datatype_consume_spec: %d pass, %d fail", pass, fail)) +os.exit(fail == 0 and 0 or 1) From ec3b4dc656435fd272c91150b0a0166813157e38 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 9 Oct 2026 13:05:16 +0000 Subject: [PATCH 2/7] fix: pass inline freeze captures into hoisted control forms An inline freeze-let thawed inside a value-position control form is expanded inside the hoisted KC function with the freeze's own env, but the KC took only the control form's free variables as parameters. A freeze variable the form did not mention itself resolved to a global: (let G (freeze Z) (let Y (if (= X 0) (thaw G) 5) Y)) returned nil for X = 0. kc_params now adds the free variables of every inline record the form thaws (transitively). Kernel codegen is unchanged. The KC hoisting is factored into hoist_kc for reuse. Co-authored-by: pyrex41 --- compiler.lua | 69 +++++++++++++++++++++++++++++---------- test/freeze_cont_spec.lua | 16 +++++++++ 2 files changed, 67 insertions(+), 18 deletions(-) diff --git a/compiler.lua b/compiler.lua index ff48196..f8d4413 100644 --- a/compiler.lua +++ b/compiler.lua @@ -1590,6 +1590,55 @@ local function push_inline_cont() return saved end +-- Lua names a hoisted KC body must take as parameters. Beyond the form's own +-- free variables, an inline freeze-let thawed inside the form is expanded +-- there with ITS env, so the freeze body's free variables must be passed in +-- too (they are locals of the enclosing function, not visible from KC). +local function kc_params(form, env) + local set = {} + local fv = {} + collect_free(form, env, {}, fv) + for k in pairs(fv) do set[env[k]] = true end + local pending, seen = { form }, {} + while #pending > 0 do + local f = table.remove(pending) + for i = 1, #CONT do + local rec = CONT[i] + if rec.kind == "inline" and not seen[rec] and mentions_name(f, rec.name, {}) then + seen[rec] = true + local rfv = {} + collect_free(rec.expr, rec.env, {}, rfv) + for k in pairs(rfv) do set[rec.env[k]] = true end + pending[#pending + 1] = rec.expr + end + end + end + local lnames = {} + for ln in pairs(set) do lnames[#lnames + 1] = ln end + table.sort(lnames) + return table.concat(lnames, ", "), #lnames +end + +-- Compile `form` (tail-compiled) as a constant chunk-scope KC function taking +-- its free variables as parameters; returns the `KC[i](params)` call. The +-- body is a SEPARATE Lua function: no `goto tco` (SELF cleared), no goto-kind +-- failure continuations, no impl-local fN refs, and its own local budget. +local function hoist_kc(form, env) + local params = kc_params(form, env) + local saved_self = SELF + local saved_h, saved_cc, saved_fnl = HOIST, CCACHE, FNL + local saved_cont = push_inline_cont() + local saved_impl = IN_IMPL + SELF = nil; HOIST = nil; CCACHE = {}; FNL = new_fnl(true); IN_IMPL = false + local body_stmts = ctail(form, env) + if FNL.pt then body_stmts = "local PT = {}; " .. body_stmts end + SELF = saved_self; HOIST = saved_h; CCACHE = saved_cc; FNL = saved_fnl + CONT = saved_cont; IN_IMPL = saved_impl + local idx = #CTX.cbodies + 1 + CTX.cbodies[idx] = "function(" .. params .. ") " .. body_stmts .. " end" + return "KC[" .. idx .. "](" .. params .. ")" +end + -- ------------------------------------------------------------------ -- cexpr : value position (returns a Lua expression string) -- ------------------------------------------------------------------ @@ -1649,12 +1698,6 @@ function cexpr(form, env) -- the body FIRST so any nested freezes/control-forms claim lower KB -- indices before we take ours. if CTX then - local fv = {} - collect_free(form, env, {}, fv) - local lnames = {} - for kname in pairs(fv) do lnames[#lnames+1] = env[kname] end - table.sort(lnames) - local params = table.concat(lnames, ", ") -- Compile the body FIRST so nested freezes/control-forms claim their KC -- indices before we take ours. The body references only its param free -- vars, globals, and KC (a load-time upvalue) -- never an impl local -- @@ -1664,21 +1707,11 @@ function cexpr(form, env) -- would illegally cross the function boundary. Likewise reset the -- chain-hoist state: KC[i] has its own local budget, and locals cached -- in the enclosing function are not in scope here. - local saved_self = SELF - local saved_h, saved_cc, saved_fnl = HOIST, CCACHE, FNL - local saved_cont = push_inline_cont() - local saved_impl = IN_IMPL - SELF = nil; HOIST = nil; CCACHE = {}; FNL = new_fnl(true); IN_IMPL = false - local body_stmts = ctail(form, env) - if FNL.pt then body_stmts = "local PT = {}; " .. body_stmts end - SELF = saved_self; HOIST = saved_h; CCACHE = saved_cc; FNL = saved_fnl - CONT = saved_cont; IN_IMPL = saved_impl - local idx = #CTX.cbodies + 1 - CTX.cbodies[idx] = "function(" .. params .. ") " .. body_stmts .. " end" + local call = hoist_kc(form, env) -- The KC call itself may raise or side-effect: later siblings in the -- enclosing statement must not hoist chains ahead of it. if HOIST then HOIST.pure = false end - return "KC[" .. idx .. "](" .. params .. ")" + return call end -- No per-defun context (top-level eval chunk): fall back to the IIFE. -- (Clear SELF here too: the IIFE is a separate function.) diff --git a/test/freeze_cont_spec.lua b/test/freeze_cont_spec.lua index 62b7ce5..a683029 100644 --- a/test/freeze_cont_spec.lua +++ b/test/freeze_cont_spec.lua @@ -129,5 +129,21 @@ ev([[(defun fc-cap (X) (if false 1 (thaw G)))))]]) check(ev("(fc-cap 8)") == 8, "freeze captures outer X, not inner let") +-- an inline thaw inside a value-position control form: that form is hoisted +-- into a KC function, which must receive the freeze body's free variables +-- (here Z, which the hoisted `if` never mentions itself) +ev([[(defun fc-kc (X Z) + (let G (freeze Z) + (let Y (if (= X 0) (thaw G) 5) + Y)))]]) +check(ev("(fc-kc 0 42)") == 42, "inline thaw in hoisted control form sees freeze captures") +check(ev("(fc-kc 1 42)") == 5, "inline thaw in hoisted control form: other branch") +ev([[(defun fc-kc2 (X Z W) + (let G1 (freeze W) + (let G2 (freeze (+ Z (thaw G1))) + (let Y (if (= X 0) (thaw G2) 5) + Y))))]]) +check(ev("(fc-kc2 0 40 2)") == 42, "nested inline thaws in hoisted control form") + io.write(string.format("freeze_cont_spec: %d pass, %d fail\n", npass, nfail)) os.exit(nfail == 0 and 0 or 1) From 8ba96d748383720479918a570fb493099bf496ce Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 9 Oct 2026 13:05:32 +0000 Subject: [PATCH 3/7] fix: split long KL let chains before Lua's 200-local cap ctail emitted one Lua local per let, so a single function with a long let chain failed to load ("function at line 1 has more than 200 local variables"). The kernel's pattern-matching KL for a sequent rule spends about six lets per premise, so a datatype rule with ~30 premises over a user type failed to load at all. Each Lua function now tracks the locals it has declared (params, lets, chain-hoist steps, snapshot captures, fN refs). Past 120, the rest of the let chain continues in a fresh KC function via a proper tail call (return KC[i](live vars)). The split is refused while a goto-kind failure continuation is active (its label must stay in this function) or when the continuation itself would need 120+ parameters. Kernel codegen is unchanged; no kernel function reaches the budget. Co-authored-by: pyrex41 --- compiler.lua | 43 +++++++++++++++++++++++++++++++------- test/eval_order_spec.lua | 45 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 81 insertions(+), 7 deletions(-) diff --git a/compiler.lua b/compiler.lua index f8d4413..1d2f038 100644 --- a/compiler.lua +++ b/compiler.lua @@ -548,10 +548,13 @@ end local CSE_MAX_LOCALS = 100 local CCACHE = {} -- chain key -> Lua local/slot name, block-scoped via __index local HOIST = nil -- nil, or { out = {stmt strings}, pure = bool } at a flush site -local FNL = { np = 0, npt = 0, pt = false, can_pt = false } -- per-Lua-function +-- nloc: every Lua local this function has declared so far (params, let +-- locals, hoisted chain steps, fN callee refs), summed across branches, so it +-- over-approximates the live count Lua checks against its 200 cap. +local FNL = { np = 0, npt = 0, pt = false, can_pt = false, nloc = 0 } -- per-Lua-function -local function new_fnl(can_pt) - return { np = 0, npt = 0, pt = false, can_pt = can_pt } +local function new_fnl(can_pt, nparams) + return { np = 0, npt = 0, pt = false, can_pt = can_pt, nloc = nparams or 0 } end local function child_cache() @@ -583,6 +586,7 @@ end local function chain_slot(expr) if FNL.np < CSE_MAX_LOCALS then FNL.np = FNL.np + 1 + FNL.nloc = FNL.nloc + 1 local ln = gen("p") HOIST.out[#HOIST.out+1] = "local " .. ln .. " = " .. expr .. "; " return ln @@ -1522,6 +1526,7 @@ local function snapshot_env(eform, env) local ln = env[kname] if type(ln) == "string" and params[ln] then local cap = gen("c") + FNL.nloc = FNL.nloc + 1 stmts[#stmts + 1] = "local " .. cap .. " = " .. ln .. ";" newenv[kname] = cap end @@ -1623,13 +1628,13 @@ end -- its free variables as parameters; returns the `KC[i](params)` call. The -- body is a SEPARATE Lua function: no `goto tco` (SELF cleared), no goto-kind -- failure continuations, no impl-local fN refs, and its own local budget. -local function hoist_kc(form, env) - local params = kc_params(form, env) +local function hoist_kc(form, env, params, nparams) + if not params then params, nparams = kc_params(form, env) end local saved_self = SELF local saved_h, saved_cc, saved_fnl = HOIST, CCACHE, FNL local saved_cont = push_inline_cont() local saved_impl = IN_IMPL - SELF = nil; HOIST = nil; CCACHE = {}; FNL = new_fnl(true); IN_IMPL = false + SELF = nil; HOIST = nil; CCACHE = {}; FNL = new_fnl(true, nparams); IN_IMPL = false local body_stmts = ctail(form, env) if FNL.pt then body_stmts = "local PT = {}; " .. body_stmts end SELF = saved_self; HOIST = saved_h; CCACHE = saved_cc; FNL = saved_fnl @@ -1639,6 +1644,27 @@ local function hoist_kc(form, env) return "KC[" .. idx .. "](" .. params .. ")" end +-- A long let chain in one Lua function (the kernel's pattern-matching KL for +-- a sequent rule with ~30 premises spends ~6 lets per premise) would exceed +-- Lua's 200-locals-per-function cap. Past this budget the rest of the chain +-- continues in a fresh KC function via a proper tail call. The margin covers +-- locals the budget does not see ahead of time (call-chain flattening). +local LET_SPLIT_LOCALS = 120 + +local function try_split_let(form, env) + if not CTX or FNL.nosplit then return nil end + local used = FNL.nloc + (IN_IMPL and #FREF_LIST or 0) + if used < LET_SPLIT_LOCALS then return nil end + -- a goto-kind failure continuation's label lives in this function + for i = 1, #CONT do + if CONT[i].kind == "goto" then return nil end + end + -- a body that needs this many parameters would split again on its first let + local params, nparams = kc_params(form, env) + if nparams >= LET_SPLIT_LOCALS then FNL.nosplit = true; return nil end + return "return " .. hoist_kc(form, env, params, nparams) +end + -- ------------------------------------------------------------------ -- cexpr : value position (returns a Lua expression string) -- ------------------------------------------------------------------ @@ -1909,8 +1935,11 @@ function ctail(form, env) local v = car(cdr(form)) local val = car(cdr(cdr(form))) local body= car(cdr(cdr(cdr(form)))) + local split = try_split_let(form, env) + if split then return split end local lowered = try_lower_freeze_let(v, val, body, env) if lowered then return lowered end + FNL.nloc = FNL.nloc + 1 local ln = gen("v") local pre, valc = cstmt_expr(val, env) local e2 = extend(env, v.name, ln) @@ -2025,7 +2054,7 @@ local function cdefun(form) CTX = new_ctx() -- fresh chain-hoist state for the impl function (see CSE block above ccall) local saved_fnl, saved_cc = FNL, CCACHE - FNL = new_fnl(true) + FNL = new_fnl(true, #params) CCACHE = {} -- Self-tail-call -> loop lowering. Eligible unless: -- * the function is not PURELY tail-recursive -- some self-reference is a diff --git a/test/eval_order_spec.lua b/test/eval_order_spec.lua index 799bfe6..56a27a6 100644 --- a/test/eval_order_spec.lua +++ b/test/eval_order_spec.lua @@ -167,6 +167,51 @@ do "pure chain codegen allocates no scratch table") end +-- --------------------------------------------------------------------------- +-- long let chains: past a local budget the rest of the chain continues in a +-- separate KC function (Lua caps a function at 200 locals). Order, value and +-- tail calls must be unaffected. Each binding feeds the next, as in the +-- kernel's pattern-matching code, so few are live across a split point. +-- --------------------------------------------------------------------------- +do + -- past Lua's 200-local cap; kept shallow otherwise, since the Shen reader + -- recurses several frames per nesting level + local n = 210 + -- L1 = Z + log(1), Li = L(i-1) + log(i); every binding is a local + local function chain(step, final) + local src = final + for i = n, 2, -1 do + src = "(let L" .. i .. " (+ L" .. (i - 1) .. " " .. step(i) .. ") " .. src .. ")" + end + return "(let L1 (+ Z " .. step(1) .. ") " .. src .. ")" + end + local logged = function(i) return "(eo-log " .. i .. ")" end + local Ln = "L" .. n + local total = n * (n + 1) / 2 + + local kl = R.read_all("(defun eo-lets-kl (Z) " .. chain(logged, Ln) .. ")")[1] + check((loadstring or load)(C.cdefun(kl)) ~= nil, "210-let KL defun compiles to loadable Lua") + + shen.eval("(define eo-lets Z -> " .. chain(logged, Ln) .. ")") + eq(trace("(eo-lets 0)"), upto(n), "210-let chain evaluates in source order") + eq(shen.eval("(eo-lets 0)"), total, "210-let chain value") + -- a binding from before the split, read after it + shen.eval("(define eo-lets-early Z -> " .. chain(logged, "(+ L1 " .. Ln .. ")") .. ")") + eq(shen.eval("(eo-lets-early 5)"), 5 + 1 + 5 + total, "binding from before a let split is visible after it") + + -- the same chain in value position (hoisted as a control form first) + shen.eval("(define eo-lets-val Z -> (+ 1 " .. chain(logged, Ln) .. "))") + eq(shen.eval("(eo-lets-val 0)"), total + 1, "210-let chain in value position") + + -- a self-tail call that ends up in the split-off part stays a tail call + local plain = function(i) return tostring(i) end + shen.eval("(define eo-lets-rec 0 Acc -> Acc N Acc -> " + .. chain(plain, "(eo-lets-rec (- N 1) (+ Acc " .. Ln .. "))") + :gsub("%(%+ Z ", "(+ 0 ") .. ")") + eq(shen.eval("(eo-lets-rec 20000 0)"), 20000 * total, + "self tail call past a let split does not grow the stack") +end + -- --------------------------------------------------------------------------- -- collateral: constructs whose order must NOT have changed. -- --------------------------------------------------------------------------- From 22014f929c18f7bec7304cd82dd39a4b5bbfa244 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 9 Oct 2026 13:06:40 +0000 Subject: [PATCH 4/7] fix: translate consume helpers for sequent rules past 15 premises Two limits in the native Prolog translator left NativePred[shen.consumeN] unset for wide sequent rules, so typechecks walking the rule died with "shen.consumeN is undefined": * every let chained a new env table via __index, and from 16 premises the consume helper nested past LuaJIT's 100-table chain limit ("loop in gettable"). extend_env collapses the chain every 32 levels into one table with the same root lookup. * the generated Lua then exceeded 200 locals in one function. When loadstring reports that, the predicate is translated again with let splitting: past 120 locals the rest of a let chain is lifted into a static (the existing let-bound freeze closure conversion) and called. Predicates that already loaded keep byte-identical code, so the split costs nothing on existing hot paths. Lifted statics and continuations now keep the vec/lock bindings in their env, so a misuse refuses as it would in the enclosing scope instead of compiling the name as a symbol. mkhandle and lift_cont share newcont_ctor (NEWCONT0..16, NEWCONTV past that). datatype_consume_spec covers 5..37 premises: every consume helper and the rule translate natively, the last element is unpacked, and misses still miss. engine_spec pins NEWCONTV's capture layout and undo. Co-authored-by: pyrex41 --- prolog_compile.lua | 121 +++++++++++++++++++++++++++------ test/datatype_consume_spec.lua | 51 ++++++++++++-- test/engine_spec.lua | 27 ++++++++ 3 files changed, 174 insertions(+), 25 deletions(-) diff --git a/prolog_compile.lua b/prolog_compile.lua index a388b54..b28d8f1 100644 --- a/prolog_compile.lua +++ b/prolog_compile.lua @@ -145,15 +145,56 @@ local function refuse(ctx, why) error(ctx.fail, 0) end +-- ctx.fnloc counts the locals (params included) declared so far in the Lua +-- function being emitted, across all branches: an upper bound on what Lua +-- checks against its 200-locals-per-function cap. local function newlocal(ctx, pfx) ctx.nlocal = ctx.nlocal + 1 + ctx.fnloc = ctx.fnloc + 1 return (pfx or "v") .. ctx.nlocal end +-- On the split retry (see translate_core), past this many locals a let chain +-- continues in a lifted static. The margin covers locals a single let can +-- add after the check (if-chains, fork, guard imports). +local LET_SPLIT_LOCALS = 120 + local function indent(d) return string.rep(" ", d) end +-- A let extends env with a child table that __index-chains to its parent. +-- LuaJIT gives up on __index chains of 100 tables ("loop in gettable"), and +-- a wide sequent rule's consume helper nests that many lets. Every +-- ENV_FLATTEN levels the chain is collapsed into one table (inner bindings +-- win) whose __index is the chain's root lookup (nil, or a lift_static / +-- lift_cont penv function), so lookups see exactly the same bindings. +-- Parents are never written after a child is created, so the copy is safe. +local ENV_FLATTEN = 32 + +local function extend_env(env) + local mt = getmetatable(env) + local depth = (mt and mt.depth or 0) + 1 + if depth < ENV_FLATTEN then + return setmetatable({}, { __index = env, depth = depth }) + end + local flat, t, root = {}, env, nil + while t do + for k, v in pairs(t) do + if flat[k] == nil then flat[k] = v end + end + local tmt = getmetatable(t) + local idx = tmt and tmt.__index + if type(idx) == "table" then + t = idx + else + root = idx; t = nil + end + end + return setmetatable({}, { __index = setmetatable(flat, { __index = root, depth = 1 }), depth = 2 }) +end + local compile_value -- fwd: control/result position local compile_term -- fwd: term-construction position +local static_fvs -- fwd: free vars of a static about to be lifted -- atom constant: interned at translate time, inlined as a number literal local function atomconst(x) @@ -338,6 +379,14 @@ compile_value = function(ctx, e, env, out, d) -- (let V Expr Body) — including the kernel's multi-binding form -- (let V1 E1 V2 E2 ... Body), which the Shen macro pipeline would desugar if h == SYM["let"] and is_cons(args) and is_cons(args[2]) then + if ctx.split and ctx.fnloc >= LET_SPLIT_LOCALS then + -- a static this wide would split again on its first let + local fvs, implicit = static_fvs({}, e, env) + if #fvs < LET_SPLIT_LOCALS then + local st = ctx:lift_static(nil, {}, e, env, fvs, implicit) + return ctx:callstatic(st, {}, env, out, d) + end + end local v, ex = args[1], args[2][1] local rest = args[2][2] local body @@ -347,7 +396,7 @@ compile_value = function(ctx, e, env, out, d) -- more bindings follow: re-wrap as a nested let body = R.cons(SYM["let"], rest) end - local nenv = setmetatable({}, { __index = env }) + local nenv = extend_env(env) if is_cons(ex) and (ex[1] == SYM["freeze"] or ex[1] == SYM["lambda"]) then -- closure-convert: a let-bound freeze/lambda-chain becomes a static -- chunk-level function with its free vars as trailing parameters @@ -650,6 +699,15 @@ end local CtxMT = {} CtxMT.__index = CtxMT +-- Handle constructor for k captures. NEWCONT0..16 and the varargs NEWCONTV +-- share one layout (k contiguous capbuf slots at contBase[h]). Generated +-- fixed-width constructors past 16 win in isolation but measured ~25% slower +-- on einsteins-riddle, whose wide continuations take NEWCONTV. +local function newcont_ctor(k) + if k <= 16 then return "NEWCONT" .. k end + return "NEWCONTV" +end + local function liftname(ctx, pfx) ctx.nlift = ctx.nlift + 1 local fname = pfx .. ctx.nlift @@ -661,11 +719,10 @@ end -- A static referencing another static is fine (both are chunk-level fns): -- the inner static's free vars are folded into THIS static's free vars so -- they are in scope at the inner call sites. -function CtxMT.lift_static(ctx, name, params, body, env) - local fname = liftname(ctx, "LF") +static_fvs = function(params, body, env) local bound = {} for _, p in ipairs(params) do bound[p.name] = true end - local fvs, fvseen = {}, {} + local fvs, fvseen, implicit = {}, {}, {} local function addfv(vn) if bound[vn] or fvseen[vn] then return end fvseen[vn] = true @@ -675,19 +732,29 @@ function CtxMT.lift_static(ctx, name, params, body, env) for _, f in ipairs(outer.fvs) do addfv(f) end elseif outer.kind == "vec" or outer.kind == "lock" then -- engine-implicit, dropped at use sites + implicit[vn] = outer else fvs[#fvs + 1] = vn end end for _, vn in ipairs(freevars(body)) do addfv(vn) end + return fvs, implicit +end + +function CtxMT.lift_static(ctx, name, params, body, env, fvs, implicit) + if not fvs then fvs, implicit = static_fvs(params, body, env) end + local fname = liftname(ctx, "LF") local st = { kind = "static", fn = fname, params = params, fvs = fvs, body = body, env = env } - -- emit the lifted definition; statics resolve through to chunk scope + -- emit the lifted definition; statics resolve through to chunk scope. + -- The vec/lock params keep their kinds so a misuse refuses exactly as it + -- would have in the enclosing env. local penv = setmetatable({}, { __index = function(_, k) local b = env[k] if b and b.kind == "static" then return b end return nil end }) + for vn, b in pairs(implicit) do penv[vn] = b end local sig = {} for i, p in ipairs(params) do sig[#sig + 1] = "p" .. i @@ -698,7 +765,10 @@ function CtxMT.lift_static(ctx, name, params, body, env) penv[vn] = { lua = "fv" .. i, kind = env[vn].kind } end local fbuf = {} + local saved_loc = ctx.fnloc + ctx.fnloc = #sig local fval = compile_value(ctx, body, penv, fbuf, 1) + ctx.fnloc = saved_loc local def = { fname .. " = function(" .. table.concat(sig, ", ") .. ")" } for _, l in ipairs(fbuf) do def[#def + 1] = l end def[#def + 1] = " return " .. fval @@ -729,7 +799,7 @@ function CtxMT.lift_cont(ctx, body, env, out, d) end -- statics referenced from the cont body are chunk-level fns whose OWN free -- vars must also be captured - local capture, statics, seen = {}, {}, {} + local capture, statics, seen, implicit = {}, {}, {}, {} local function addcap(vn) if seen[vn] then return end seen[vn] = true @@ -740,6 +810,7 @@ function CtxMT.lift_cont(ctx, body, env, out, d) elseif b.kind == "vec" or b.kind == "lock" then -- the prolog vector / lock vector are engine-implicit: dropped at -- every use site, so never captured + implicit[vn] = b else capture[#capture + 1] = vn end @@ -752,6 +823,7 @@ function CtxMT.lift_cont(ctx, body, env, out, d) if b and b.kind == "static" then return b end return nil end }) + for vn, b in pairs(implicit) do penv[vn] = b end local fbuf = {} local decls = {} for i, vn in ipairs(capture) do @@ -759,7 +831,10 @@ function CtxMT.lift_cont(ctx, body, env, out, d) decls[#decls + 1] = "local " .. lv .. " = CAPREF(base, " .. (i - 1) .. ")" penv[vn] = { lua = lv, kind = env[vn].kind } end + local saved_loc = ctx.fnloc + ctx.fnloc = #capture + 2 local fval = compile_value(ctx, body, penv, fbuf, 1) + ctx.fnloc = saved_loc local def = { fname .. " = function(base, h)" } for _, l in ipairs(decls) do def[#def + 1] = " " .. l end for _, l in ipairs(fbuf) do def[#def + 1] = l end @@ -769,19 +844,16 @@ function CtxMT.lift_cont(ctx, body, env, out, d) local parts = { fname } for _, vn in ipairs(capture) do parts[#parts + 1] = env[vn].lua end - local mk = (#capture <= 16) and ("NEWCONT" .. #capture) or "NEWCONTV" - return mk .. "(" .. table.concat(parts, ", ") .. ")" + return newcont_ctor(#capture) .. "(" .. table.concat(parts, ", ") .. ")" end -- a zero-param static used as a continuation value: wrap into a handle function CtxMT.mkhandle(ctx, st, out, d) - -- captures = the static's free vars (numbers). NEWCONT0..16 stay - -- monomorphic so LuaJIT traces them. A consume helper for a sequent - -- premise closes over two locals per premise variable plus the - -- assumption and the engine temps (2*N+5): five premises fit in 16, - -- six need 17. Wider handles take NEWCONTV, the same varargs path - -- lift_cont uses. Refusing left NativePred[shen.consumeN] unset, and - -- the compiled caller then died with "shen.consumeN is undefined". + -- captures = the static's free vars (numbers). A consume helper for a + -- sequent premise closes over two locals per premise variable plus the + -- assumption and the engine temps (2*N+5), so six premises already need + -- 17. The width must not be capped: refusing leaves NativePred[name] + -- unset while the already-translated caller still calls it. local fname = liftname(ctx, "LH") local decls, parts = {}, { fname } local args = {} @@ -795,9 +867,7 @@ function CtxMT.mkhandle(ctx, st, out, d) def[#def + 1] = " return " .. st.fn .. "(" .. table.concat(args, ", ") .. ")" def[#def + 1] = "end" ctx.buf[#ctx.buf + 1] = table.concat(def, "\n") - local ncap = #st.fvs - local mk = (ncap <= 16) and ("NEWCONT" .. ncap) or "NEWCONTV" - return mk .. "(" .. table.concat(parts, ", ") .. ")" + return newcont_ctor(#st.fvs) .. "(" .. table.concat(parts, ", ") .. ")" end -- --------------------------------------------------------------------------- @@ -827,7 +897,7 @@ local VAR_BASE, CONS_BASE = E.VAR_BASE, E.CONS_BASE -- translate_core: shared by defprolog define-forms and the t-star driver -- defuns. `allparams` is the full parameter list whose LAST FOUR entries are -- the Vec / Lock / Count / Cont gensyms (the uniform CPS goal ABI). -local function translate_core(name, allparams, body) +local function translate_once(name, allparams, body, split) local np = #allparams assert(np >= 4, "prolog fn must have at least the B L K C params") local nparams = np - 4 @@ -836,6 +906,7 @@ local function translate_core(name, allparams, body) local ctx = setmetatable({ buf = {}, nlift = 0, nlocal = 0, fail = {}, liftnames = {}, + fnloc = nparams + 2, split = split, }, CtxMT) local env = {} @@ -877,11 +948,21 @@ local function translate_core(name, allparams, body) local chunk, err = loadstring(source, "@prolog:" .. name) if not chunk then - return nil, "luagen: " .. tostring(err) .. "\n" .. source + return nil, "luagen: " .. tostring(err) .. "\n" .. source, nil, err end local fn = chunk(E, NP, F, E.materialize, E.import_cached) return fn, nil, source end + +-- Let-chain splitting (see compile_value) costs a call per split point, so +-- it is only used when the unsplit chunk exceeds Lua's local-variable cap. +local function translate_core(name, allparams, body) + local fn, err, src, lerr = translate_once(name, allparams, body, false) + if lerr and tostring(lerr):find("local variables", 1, true) then + return translate_once(name, allparams, body, true) + end + return fn, err, src +end M.translate_core = translate_core -- translate a (define Name P1..Pk B L K C -> Body) form (defprolog output) diff --git a/test/datatype_consume_spec.lua b/test/datatype_consume_spec.lua index 75eba21..2ee7c3f 100644 --- a/test/datatype_consume_spec.lua +++ b/test/datatype_consume_spec.lua @@ -23,6 +23,7 @@ shen.boot{ quiet = true } local R = require("runtime") local P = shen.prims local E = require("prolog_engine") +local PC = require("prolog_compile") local pass, fail = 0, 0 local function check(desc, got, want) @@ -84,7 +85,7 @@ local function run_rule(name, goal, assum) return res end -local function varname(i) return string.char(64 + i) end +local function varname(i) return "V" .. i end local function define_row(n) local vars, jud = {}, {} @@ -111,10 +112,30 @@ shen.eval([[ ]]) -- Five is the last width that fit the old 16-capture helper. Six is the --- first that used to be missing. Eight and twelve sit past that threshold --- and under the later metatable-chain limit on very deep clauses. -for _, n in ipairs({ 5, 6, 8, 12 }) do - local name = define_row(n) +-- first that used to be missing. From sixteen the native consume helper +-- nested past LuaJIT's 100-table __index chain ("loop in gettable") and then +-- past Lua's 200 locals per function; from about thirty the legacy KL defun +-- did too, and the datatype failed to load at all. Thirty-seven is the +-- widest that loads today (see the note at the end of this file). +local WIDTHS = { 5, 6, 8, 12, 15, 16, 20, 24, 30, 32, 37 } + +local function check_width(n) + local before = {} + for k in pairs(PC.registry) do before[k] = true end + local loaded, name = pcall(define_row, n) + check(n .. " premises: datatype loads", loaded or errmsg(name), true) + if not loaded then return end + local helpers, native = 0, 0 + for k in pairs(PC.registry) do + if not before[k] and k:match("^shen%.consume") then + helpers = helpers + 1 + if E.NativePred[k] ~= nil then native = native + 1 end + end + end + check(n .. " premises: every consume helper translates natively", + helpers > 0 and native == helpers, true) + check(n .. " premises: rule predicate translates natively", + E.NativePred[name .. "#type"] ~= nil, true) local ty, err = typecheck("0", "piece") check(n .. " premises: 0 : piece still holds", err or R.to_str(ty), "piece") @@ -140,11 +161,31 @@ for _, n in ipairs({ 5, 6, 8, 12 }) do local wrong, werr = run_rule(name, goal, bad) check(n .. " premises: short hypothesis misses", werr or wrong, false) + -- the LAST premise is still unpacked: on wide rules it runs in code that + -- a let-chain split moved into a separate function. Only the assumption + -- 7 : piece taken from the last element proves 7 : piece. + local tail = {} + for i = 1, n do tail[i] = elems[i] end + tail[n] = 7 + local tailhyp = R.cons(judgement(list_form(tail), R.intern(name)), R.NIL) + local seven = judgement(7, PIECE) + local thit, therr = run_rule(name, seven, tailhyp) + check(n .. " premises: last element is unpacked", therr or thit, true) + local tmiss, tmerr = run_rule(name, seven, hyp) + check(n .. " premises: 7 : piece needs the last element", tmerr or tmiss, false) + local nope = judgement(2, PIECE) local no, nerr = run_rule(name, nope, hyp) check(n .. " premises: unpacked rule does not prove 2 : piece", nerr or no, false) end +for _, n in ipairs(WIDTHS) do check_width(n) end + +-- Thirty-eight premises still fail to load: the legacy KL compiler hoists +-- each premise's freeze continuation into a function taking all ~3N +-- captures as parameters and passes them on in a nested call, which passes +-- LuaJIT's 250-slot frame limit ("function or expression too complex"). + print(string.format("datatype_consume_spec: %d pass, %d fail", pass, fail)) os.exit(fail == 0 and 0 or 1) diff --git a/test/engine_spec.lua b/test/engine_spec.lua index 0f0d0dd..e61a31e 100644 --- a/test/engine_spec.lua +++ b/test/engine_spec.lua @@ -161,6 +161,33 @@ do return E.spill(hh)[1] == sym end, { sym }) check(E.thawH(hs) == true, "spill captures") + + -- wide handles (the translator emits newcontV past 16 captures): same + -- capbuf layout as newcont16, and reclaimed by undo + local function readback(k, mk) + local vals = {} + for i = 1, k do vals[i] = i * 3 + k end + local seen + local kfn = function(b) + seen = {} + for i = 1, k do seen[i] = E.capref(b, i - 1) end + return true + end + local tm2, vm2, hm2, bm2, cm2 = E.marks() + local hh = mk(kfn, unpack(vals)) + local _, _, _, top = E.tops() + E.thawH(hh) + local ok = #seen == k and top == bm2 + k + for i = 1, k do ok = ok and seen[i] == vals[i] end + E.undo(tm2, vm2, hm2, bm2, cm2) + local _, _, _, top2, ch2 = E.tops() + return ok and top2 == bm2 and ch2 == hm2 + end + check(readback(16, E.newcont16) and readback(16, E.newcontV), + "newcontV matches newcont16 layout") + for _, k in ipairs({ 17, 41, 100 }) do + check(readback(k, E.newcontV), "newcontV " .. k .. " captures read back and reclaim") + end end -- --------------------------------------------------------------------------- From 6c780760fe0fa18e93d18e87fb2d036871a36f8d Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 9 Oct 2026 16:52:33 +0000 Subject: [PATCH 5/7] fix: recompile KL defuns past Lua's width limits in a wide mode A defun whose ordinary Lua does not load (200 locals, 60 upvalues, 250 registers) is recompiled once with captures passed as tables: hoisted bodies and freezes past 24 captures take one table, lambdas closing over more than 40 names become LAMW closures, let chains split at 80 locals whatever the live set, goto failure continuations stay freeze/thaw, flattened call chains reuse one local, and very wide calls pass UNPACK. Curried lambda chains deeper than 32 compile to CURRY in every mode. Code that loads today is unchanged. Co-authored-by: pyrex41 --- compiler.lua | 183 ++++++++++++++++++++++++++++++++----- prims.lua | 48 +++++++++- scripts/run-tests.lua | 1 + test/wide_compile_spec.lua | 167 +++++++++++++++++++++++++++++++++ 4 files changed, 374 insertions(+), 25 deletions(-) create mode 100644 test/wide_compile_spec.lua diff --git a/compiler.lua b/compiler.lua index 1d2f038..99d16a1 100644 --- a/compiler.lua +++ b/compiler.lua @@ -553,6 +553,9 @@ local HOIST = nil -- nil, or { out = {stmt strings}, pure = bool } at a flush -- over-approximates the live count Lua checks against its 200 cap. local FNL = { np = 0, npt = 0, pt = false, can_pt = false, nloc = 0 } -- per-Lua-function +local WIDE = false -- wide mode (see capture_plan) +local WIDE_ARGS = 100 + local function new_fnl(can_pt, nparams) return { np = 0, npt = 0, pt = false, can_pt = can_pt, nloc = nparams or 0 } end @@ -784,8 +787,13 @@ local function try_flatten_call_chain(form, env) call_str = ar and ("APP(" .. symlit(hname) .. ", " .. arg_list .. ")") or unknown_call(hname, arg_list, #prev_strs + 1) end - stmts[#stmts+1] = "local " .. next_name .. " = " .. call_str .. ";" - inner_name = next_name + if WIDE then + -- one local for the whole chain: each step reads only the previous one + stmts[#stmts+1] = inner_name .. " = " .. call_str .. ";" + else + stmts[#stmts+1] = "local " .. next_name .. " = " .. call_str .. ";" + inner_name = next_name + end end -- outermost: emit as return statement local frame = frames[1] @@ -871,6 +879,10 @@ local function ccall(form, env) local cargs = {} for i=1,#args do cargs[i] = cexpr(args[i], env) end local argstr = table.concat(cargs, ", ") + if WIDE and #cargs > WIDE_ARGS then + -- each argument would hold a register until the call + argstr = "UNPACK({" .. argstr .. "}, 1, " .. #cargs .. ")" + end -- Chain-hoist purity: this application runs after its args; anything the -- statement evaluates after it may no longer be hoisted ahead of it unless -- the head is known effect-free and non-raising. @@ -1570,7 +1582,7 @@ local function try_lower_freeze_let(var, val, body, env) CONT[#CONT] = nil return (snap ~= "" and (snap .. " ") or "") .. s end - if nontail > 0 or not HAS_GOTO then return nil end + if nontail > 0 or not HAS_GOTO or WIDE then return nil end local rec = { name = var.name, kind = "goto", expr = eform, env = freeze_env, label = gen("fail"), @@ -1595,11 +1607,75 @@ local function push_inline_cont() return saved end +-- Wide mode (C.compile_top(form, true)): the code shape for a defun whose +-- ordinary Lua exceeded a Lua limit (200 locals, 60 upvalues, 250 registers). +-- prims.lua recompiles only such defuns this way, so everything that loads +-- today keeps its exact code. In wide mode: +-- * a hoisted body (KC function) with more than WIDE_CAPS captures takes +-- ONE table T and reads T[i]; narrower ones whose captures are not plain +-- names (T[i] from an enclosing wide body) get fresh parameter names; +-- * a lambda closing over more than WIDE_UPVALS outer names is hoisted the +-- same way and built by LAMW(KC[i], {captures}); +-- * let chains split at WIDE_SPLIT_LOCALS, passing a wide live set as T; +-- * multi-thaw failure continuations stay BIND/THAW closures instead of a +-- goto label, so no label pins a let chain to one function. +-- Captured values are immutable KL bindings, so copying them into T at the +-- use site observes exactly what the parameter form did. +local WIDE_CAPS = 24 +local WIDE_UPVALS = 40 +local WIDE_SPLIT_LOCALS = 80 + +-- see the lambda case of cexpr; deeper than any curried chain in the kernel +local CURRY_DEPTH = 32 + +local function is_ident(s) + return type(s) == "string" and s:match("^[%a_][%w_]*$") ~= nil +end + +-- How a hoisted body receives `lnames` (sorted Lua expressions): returns the +-- body's parameter list, the call-site argument list, an expr -> expr remap +-- for the body's env (nil = identity), and the number of parameter slots. +local function capture_plan(lnames) + local joined = table.concat(lnames, ", ") + if not WIDE then return joined, joined, nil, #lnames end + local remap = {} + if #lnames > WIDE_CAPS then + local t = gen("T") + for i, ln in ipairs(lnames) do remap[ln] = t .. "[" .. i .. "]" end + return t, "{" .. joined .. "}", remap, 1 + end + local plain = true + for _, ln in ipairs(lnames) do + if not is_ident(ln) then plain = false; break end + end + if plain then return joined, joined, nil, #lnames end + local ps = {} + for i, ln in ipairs(lnames) do ps[i] = gen("q"); remap[ln] = ps[i] end + return table.concat(ps, ", "), joined, remap, #lnames +end + +local function remap_env(env, remap) + if not remap then return env end + local e = {} + for k, v in pairs(env) do e[k] = remap[v] or v end + return e +end + +-- after push_inline_cont: inline records expand inside the hoisted body, so +-- their envs must see the body's names too +local function remap_cont(remap) + if not remap then return end + for i = 1, #CONT do + local r = CONT[i] + CONT[i] = { name = r.name, kind = r.kind, expr = r.expr, env = remap_env(r.env, remap) } + end +end + -- Lua names a hoisted KC body must take as parameters. Beyond the form's own -- free variables, an inline freeze-let thawed inside the form is expanded -- there with ITS env, so the freeze body's free variables must be passed in -- too (they are locals of the enclosing function, not visible from KC). -local function kc_params(form, env) +local function kc_lnames(form, env) local set = {} local fv = {} collect_free(form, env, {}, fv) @@ -1621,27 +1697,29 @@ local function kc_params(form, env) local lnames = {} for ln in pairs(set) do lnames[#lnames + 1] = ln end table.sort(lnames) - return table.concat(lnames, ", "), #lnames + return lnames end -- Compile `form` (tail-compiled) as a constant chunk-scope KC function taking -- its free variables as parameters; returns the `KC[i](params)` call. The -- body is a SEPARATE Lua function: no `goto tco` (SELF cleared), no goto-kind -- failure continuations, no impl-local fN refs, and its own local budget. -local function hoist_kc(form, env, params, nparams) - if not params then params, nparams = kc_params(form, env) end +local function hoist_kc(form, env, lnames) + lnames = lnames or kc_lnames(form, env) + local params, args, remap, nslots = capture_plan(lnames) local saved_self = SELF local saved_h, saved_cc, saved_fnl = HOIST, CCACHE, FNL local saved_cont = push_inline_cont() + remap_cont(remap) local saved_impl = IN_IMPL - SELF = nil; HOIST = nil; CCACHE = {}; FNL = new_fnl(true, nparams); IN_IMPL = false - local body_stmts = ctail(form, env) + SELF = nil; HOIST = nil; CCACHE = {}; FNL = new_fnl(true, nslots); IN_IMPL = false + local body_stmts = ctail(form, remap_env(env, remap)) if FNL.pt then body_stmts = "local PT = {}; " .. body_stmts end SELF = saved_self; HOIST = saved_h; CCACHE = saved_cc; FNL = saved_fnl CONT = saved_cont; IN_IMPL = saved_impl local idx = #CTX.cbodies + 1 CTX.cbodies[idx] = "function(" .. params .. ") " .. body_stmts .. " end" - return "KC[" .. idx .. "](" .. params .. ")" + return "KC[" .. idx .. "](" .. args .. ")" end -- A long let chain in one Lua function (the kernel's pattern-matching KL for @@ -1654,15 +1732,16 @@ local LET_SPLIT_LOCALS = 120 local function try_split_let(form, env) if not CTX or FNL.nosplit then return nil end local used = FNL.nloc + (IN_IMPL and #FREF_LIST or 0) - if used < LET_SPLIT_LOCALS then return nil end + if used < (WIDE and WIDE_SPLIT_LOCALS or LET_SPLIT_LOCALS) then return nil end -- a goto-kind failure continuation's label lives in this function for i = 1, #CONT do if CONT[i].kind == "goto" then return nil end end - -- a body that needs this many parameters would split again on its first let - local params, nparams = kc_params(form, env) - if nparams >= LET_SPLIT_LOCALS then FNL.nosplit = true; return nil end - return "return " .. hoist_kc(form, env, params, nparams) + -- a body that needs this many parameters would split again on its first + -- let (wide mode passes them as one table instead) + local lnames = kc_lnames(form, env) + if not WIDE and #lnames >= LET_SPLIT_LOCALS then FNL.nosplit = true; return nil end + return "return " .. hoist_kc(form, env, lnames) end -- ------------------------------------------------------------------ @@ -1760,7 +1839,54 @@ function cexpr(form, env) if op == "lambda" then local v = car(cdr(form)) local body = car(cdr(cdr(form))) + -- A curried chain this deep (the kernel's lambda entry for an + -- N+6-ary consume helper) nests one Lua function per lambda, past + -- LuaJIT's 200 syntax levels. CURRY(n, f) builds the same curried + -- closures at runtime and calls f with the n arguments as one table. + local depth, inner, vars = 0, form, {} + while is_cons(inner) and car(inner) == form[1] and is_symbol(car(cdr(inner))) + and not is_cons(cdr(cdr(cdr(inner)))) do + depth = depth + 1 + vars[depth] = car(cdr(inner)) + inner = car(cdr(cdr(inner))) + end + if depth > CURRY_DEPTH then + local t = gen("T") + local e2 = env + for i = 1, depth do e2 = extend(e2, vars[i].name, t .. "[" .. i .. "]") end + local saved_h, saved_impl = HOIST, IN_IMPL + HOIST = nil; IN_IMPL = false + local bodyc = cexpr(inner, e2) + HOIST = saved_h; IN_IMPL = saved_impl + return "CURRY(" .. depth .. ", function(" .. t .. ") return " .. bodyc .. " end)" + end local ln = gen("v") + if WIDE and CTX then + -- each distinct outer name the closure reads is one upvalue + local fv = {} + collect_free(form, env, {}, fv) + local lnames, roots, nroots = {}, {}, 0 + for kname in pairs(fv) do + local e = env[kname] + lnames[#lnames + 1] = e + local r = type(e) == "string" and e:match("^[%a_][%w_]*") or e + if not roots[r] then roots[r] = true; nroots = nroots + 1 end + end + if nroots > WIDE_UPVALS then + table.sort(lnames) + local t = gen("T") + local remap = {} + for i, e in ipairs(lnames) do remap[e] = t .. "[" .. i .. "]" end + local saved_h, saved_impl, saved_cont = HOIST, IN_IMPL, CONT + push_inline_cont(); remap_cont(remap) + HOIST = nil; IN_IMPL = false + local bodyc = cexpr(body, extend(remap_env(env, remap), v.name, ln)) + HOIST = saved_h; IN_IMPL = saved_impl; CONT = saved_cont + local idx = #CTX.cbodies + 1 + CTX.cbodies[idx] = "function(" .. ln .. ", " .. t .. ") return " .. bodyc .. " end" + return "LAMW(KC[" .. idx .. "], {" .. table.concat(lnames, ", ") .. "})" + end + end local e2 = extend(env, v.name, ln) -- Deferred body: nothing inside may be hoisted to the creation site. -- Not impl-scope: `fN` locals live in impl, not this nested function. @@ -1783,15 +1909,18 @@ function cexpr(form, env) local lnames = {} for kname in pairs(fv) do lnames[#lnames+1] = env[kname] end table.sort(lnames) -- stable order for caller / body + local params, args, remap = capture_plan(lnames) -- Deferred body: nothing inside may be hoisted to the creation site. local saved_h, saved_impl = HOIST, IN_IMPL + local saved_cont = CONT + if remap then push_inline_cont(); remap_cont(remap) end HOIST = nil; IN_IMPL = false - local body_str = cexpr(body, env) - HOIST = saved_h; IN_IMPL = saved_impl + local body_str = cexpr(body, remap_env(env, remap)) + HOIST = saved_h; IN_IMPL = saved_impl; CONT = saved_cont local idx = #CTX.cbodies + 1 - CTX.cbodies[idx] = "function(" .. table.concat(lnames, ", ") .. ") return " + CTX.cbodies[idx] = "function(" .. params .. ") return " .. body_str .. " end" - local call_args = (#lnames == 0) and "" or (", " .. table.concat(lnames, ", ")) + local call_args = (#lnames == 0) and "" or (", " .. args) return "BIND(KC[" .. idx .. "]" .. call_args .. ")" end local saved_h, saved_impl = HOIST, IN_IMPL @@ -2175,7 +2304,17 @@ local function cdefun(form) end return src end -C.cdefun = cdefun +-- wide: compile in wide mode (see WIDE above) +local function cdefun_mode(form, wide) + if not wide then return cdefun(form) end + local saved = WIDE + WIDE = true + local ok, res = pcall(cdefun, form) + WIDE = saved + if not ok then error(res, 0) end + return res +end +C.cdefun = cdefun_mode -- Pre-scan a list of forms to register arities of all defuns (so mutual / -- forward references compile as direct exact-arity calls). @@ -2197,9 +2336,9 @@ function C.compile_expr_chunk(form) end -- compile any top-level form to a Lua statement string -function C.compile_top(form) +function C.compile_top(form, wide) if is_cons(form) and is_symbol(car(form)) and car(form).name == "defun" then - return cdefun(form) + return cdefun_mode(form, wide) else -- a top-level expression: evaluate for side effects. Wrapped in do..end -- so a whole kernel file can be concatenated into ONE chunk (boot.lua's diff --git a/prims.lua b/prims.lua index 14d79f0..0d12b41 100644 --- a/prims.lua +++ b/prims.lua @@ -1871,6 +1871,26 @@ local ENV = { end return setmetatable({ fn, ... }, Thunk) end, + -- A wide-mode lambda (compiler.lua, WIDE): its body is the constant + -- function fn(x, T) with the captures in the table T. + UNPACK = unpack, + LAMW = function(fn, t) + return MKFUN(1, function(x) return fn(x, t) end) + end, + -- A curried lambda chain n deep (compiler.lua, CURRY_DEPTH): each + -- application returns a fresh closure over its own copy of the arguments + -- so far, exactly like the nested closures; the last calls fn(args). + CURRY = function(n, fn) + local function step(args, i) + return MKFUN(1, function(x) + local a = { unpack(args, 1, i - 1) } + a[i] = x + if i == n then return fn(a) end + return step(a, i + 1) + end) + end + return step({}, 1) + end, -- MKTREE consumes a flat blueprint produced by the compiler for deep -- cons-trees. See compile_cons_tree in compiler.lua. ops is a sequence of -- 'v' followed by a leaf value (push), or 'c' (pop two, push cons). @@ -2117,8 +2137,30 @@ end -- WHILE one of those chunks executes (nested eval-kl, e.g. compile-prolog -- inside process-datatype) are not recorded — replaying the outer chunk -- regenerates them naturally. -local function compile_and_load(luasrc, chunkname) - local fn = load_chunk(luasrc, chunkname) +-- Lua limits the wide code shape avoids (compiler.lua, WIDE) +local function is_width_error(msg) + msg = tostring(msg) + return msg:find("has more than %d+ local variables") ~= nil + or msg:find("has more than %d+ upvalues") ~= nil + or msg:find("function or expression too complex", 1, true) ~= nil +end + +-- defun_form: when the ordinary code for this defun exceeds a Lua limit, +-- recompile it in wide mode (loads that succeed never pay for this) +local function compile_and_load(luasrc, chunkname, defun_form) + local fn + if defun_form then + local ok, res = pcall(load_chunk, luasrc, chunkname) + if ok then + fn = res + elseif is_width_error(res) then + fn = load_chunk(require("compiler").compile_top(defun_form, true), chunkname) + else + error(res, 0) + end + else + fn = load_chunk(luasrc, chunkname) + end local rec = P.FASL_REC if rec and not rec.in_chunk then rec.n = rec.n + 1 @@ -2172,7 +2214,7 @@ function P.eval(form) -- error positions and debug.traceback frames identify the Shen function -- (the REPL's Shen-level backtrace filters on this prefix; repl.lua). local nm = is_cons(form[2]) and is_symbol(form[2][1]) and form[2][1].name or "defun" - compile_and_load(C.compile_top(form), "shen:" .. nm) + compile_and_load(C.compile_top(form), "shen:" .. nm, form) return form[2][1] -- the function NAME symbol (car of cdr), as shen-c returns end return compile_and_load(C.compile_expr_chunk(form), "eval") diff --git a/scripts/run-tests.lua b/scripts/run-tests.lua index 03e7040..ced3f9e 100644 --- a/scripts/run-tests.lua +++ b/scripts/run-tests.lua @@ -52,6 +52,7 @@ local specs = { "test/tailcall_spec.lua", "test/typecheck_api_spec.lua", "test/typecheck_lazy_spec.lua", + "test/wide_compile_spec.lua", } local function sh_quote(s) return "'" .. tostring(s):gsub("'", "'\\''") .. "'" end diff --git a/test/wide_compile_spec.lua b/test/wide_compile_spec.lua new file mode 100644 index 0000000..d519b9c --- /dev/null +++ b/test/wide_compile_spec.lua @@ -0,0 +1,167 @@ +-- test/wide_compile_spec.lua — KL functions too wide for ordinary Lua. +-- +-- luajit test/wide_compile_spec.lua +-- +-- Each case is a defun whose ordinary Lua exceeds a Lua limit (200 locals, +-- 60 upvalues). prims.lua's P.eval then recompiles just that defun in wide +-- mode (compiler.lua, WIDE). Every case checks the ordinary code really is +-- rejected, so the case keeps exercising the wide path, and that the wide +-- code computes the same values with the same evaluation behaviour. + +package.path = (arg[0]:gsub("test/[^/]*$", "")) .. "?.lua;" .. package.path + +local shen = require("shen") +shen.boot{ quiet = true } +local R = require("runtime") +local C = require("compiler") +local P = shen.prims +local F = P.F +local loadstr = loadstring or load + +local npass, nfail = 0, 0 +local function check(cond, name) + if cond then npass = npass + 1 + else + nfail = nfail + 1 + io.write("FAIL: ", name, "\n") + end +end +local function eq(got, want, name) + if got == want then npass = npass + 1 + else + nfail = nfail + 1 + io.write("FAIL: ", name, "\n want: ", tostring(want), + "\n got: ", tostring(got), "\n") + end +end + +local function show(x) + local t = {} + while R.is_cons(x) do t[#t + 1] = tostring(x[1]); x = x[2] end + return table.concat(t, " ") +end + +local function nums(from, to, step) + local t = {} + for i = from, to, step or 1 do t[#t + 1] = tostring(i) end + return table.concat(t, " ") +end + +local function kl_list(xs) + local s = "()" + for i = #xs, 1, -1 do s = "(cons " .. xs[i] .. " " .. s .. ")" end + return s +end + +-- (let N1 E1 (let N2 E2 ... BODY)) from parallel name / expr lists +local function let_chain(names, exprs, body) + local s = body + for i = #names, 1, -1 do s = "(let " .. names[i] .. " " .. exprs[i] .. " " .. s .. ")" end + return s +end + +local function read1(src) return R.read_all(src)[1] end + +-- the ordinary code is rejected with `why`; the wide code loads; P.eval +-- (the path every defun takes) installs a working function +local function define_wide(src, why, name) + local form = read1(src) + local _, err = loadstr(C.compile_top(form)) + check(err ~= nil and tostring(err):find(why, 1, true) ~= nil, + name .. ": ordinary code exceeds " .. why .. " (" .. tostring(err) .. ")") + local wide = C.compile_top(form, true) + check(loadstr(wide) ~= nil, name .. ": wide code loads") + P.eval(form) + return form, wide +end + +local N = 210 + +-- 1) more than 120 bindings live at once: the let split hands the whole live +-- set to the continuation as one table +do + local names, exprs, refs = {}, {}, {} + for i = 1, N do + names[i] = "L" .. i + exprs[i] = "(+ X " .. i .. ")" + refs[i] = names[i] + end + local _, wide = define_wide("(defun wc-live (X) " .. let_chain(names, exprs, kl_list(refs)) .. ")", + "local variables", "all-live let chain") + check(wide:find("return KC%[%d+%]%({") ~= nil, "all-live let chain: split passes a table") + eq(show(F["wc-live"](10)), nums(11, 10 + N), "all-live let chain: every binding survives the split") + + -- the same live set captured by a freeze: BIND(KC[i], {...}) + define_wide("(defun wc-frz (X) " .. let_chain(names, exprs, "(freeze " .. kl_list(refs) .. ")") .. ")", + "local variables", "wide freeze") + local th = F["wc-frz"](0) + eq(show(F["thaw"](th)), nums(1, N), "wide freeze: thaw sees every capture") + eq(show(F["thaw"](th)), nums(1, N), "wide freeze: thawing twice gives the same value") +end + +-- 2) a long let chain under a goto-kind failure continuation: the ordinary +-- code keeps the failure label in one function, which then cannot split. +-- In wide mode the failure path is a freeze/thaw closure instead. +do + local names, exprs = {}, {} + for i = 1, N do + names[i] = "G" .. i + exprs[i] = (i == 1) and "(+ X 1)" or ("(+ G" .. (i - 1) .. " 1)") + end + local body = "(if (= X 0) (thaw K) (if (= X 1) (thaw K) (cons G" .. N .. " (cons G1 ()))))" + local src = "(defun wc-goto (X) (let K (freeze (do (set wc-fails (+ 1 (value wc-fails))) " + .. "(cons fail (cons X ())))) " .. let_chain(names, exprs, body) .. "))" + check(C.compile_top(read1(src)):find("goto fail", 1, true) ~= nil, + "goto failure path: ordinary code uses a goto failure label") + local _, wide = define_wide(src, "local variables", "goto failure path") + check(wide:find("goto fail", 1, true) == nil, "goto failure path: wide code has no failure label") + shen.eval("(set wc-fails 0)") + eq(show(F["wc-goto"](5)), (5 + N) .. " 6", "goto failure path: success path value") + eq(shen.eval("(value wc-fails)"), 0, "goto failure path: failure body not run on success") + eq(show(F["wc-goto"](0)), "fail 0", "goto failure path: first failure exit") + eq(show(F["wc-goto"](1)), "fail 1", "goto failure path: second failure exit") + eq(shen.eval("(value wc-fails)"), 2, "goto failure path: failure body runs once per exit") +end + +-- 3) a lambda closing over more than 60 bindings: LAMW(KC[i], {...}) +do + local names, exprs, refs = {}, {}, { "Y" } + for i = 1, 70 do + names[i] = "A" .. i + exprs[i] = "(+ X " .. i .. ")" + refs[#refs + 1] = names[i] + end + local _, wide = define_wide("(defun wc-lam (X) " .. let_chain(names, exprs, "(lambda Y " .. kl_list(refs) .. ")") .. ")", + "upvalues", "wide lambda") + check(wide:find("LAMW(", 1, true) ~= nil, "wide lambda: built by LAMW") + local f = F["wc-lam"](0) + eq(show(P.APP(f, 99)), "99 " .. nums(1, 70), "wide lambda: applies with every capture") + eq(show(P.APP(f, 7)), "7 " .. nums(1, 70), "wide lambda: reusable") +end + +-- 4) a curried lambda chain deeper than CURRY_DEPTH (the kernel's lambda +-- entry for a many-argument function) compiles to CURRY in ordinary code +do + local depth = 40 + local s = "(cons Y1 (cons Y2 (cons Y" .. depth .. " ())))" + for i = depth, 1, -1 do s = "(lambda Y" .. i .. " " .. s .. ")" end + local form = read1("(defun wc-curry () " .. s .. ")") + local src = C.compile_top(form) + check(src:find("CURRY(", 1, true) ~= nil and loadstr(src) ~= nil, + "curried chain: compiles to CURRY and loads") + P.eval(form) + local f1 = P.APP(F["wc-curry"](), "a") + local fa, fb = P.APP(f1, "b"), P.APP(f1, "c") + for i = 3, depth - 1 do fa = P.APP(fa, i); fb = P.APP(fb, i) end + eq(show(P.APP(fa, "z")), "a b z", "curried chain: one branch") + eq(show(P.APP(fb, "z")), "a c z", "curried chain: a sibling partial application is independent") + eq(show(P.APP(fa, "y")), "a b y", "curried chain: a partial application is reusable") + + local shallow = "(cons Y1 ())" + for i = 8, 1, -1 do shallow = "(lambda Y" .. i .. " " .. shallow .. ")" end + check(C.compile_top(read1("(defun wc-shallow () " .. shallow .. ")")):find("CURRY", 1, true) == nil, + "curried chain: a shallow chain keeps nested closures") +end + +print(string.format("wide_compile_spec: %d pass, %d fail", npass, nfail)) +os.exit(nfail == 0 and 0 or 1) From 4295e61a8cded81295fe10539f6ee5f4d2682df2 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 9 Oct 2026 16:52:33 +0000 Subject: [PATCH 6/7] fix: translate consume helpers past 40 premises with a wide retry When the split translation still passes a Lua limit, translate once more with wide statics (free vars as one table), CAPREF reads in wide continuations, NEWCONTT handles, CONSL cons chains and lifted functions in one LT table. Predicates that translate today are unchanged. Co-authored-by: pyrex41 --- prolog_compile.lua | 147 ++++++++++++++++++++++++++++++++++--------- prolog_engine.lua | 20 ++++++ test/engine_spec.lua | 12 ++++ 3 files changed, 150 insertions(+), 29 deletions(-) diff --git a/prolog_compile.lua b/prolog_compile.lua index b28d8f1..0a7c918 100644 --- a/prolog_compile.lua +++ b/prolog_compile.lua @@ -159,6 +159,24 @@ end -- add after the check (if-chains, fork, guard imports). local LET_SPLIT_LOCALS = 120 +-- The wide retry (see translate_core) is for predicates that still pass a +-- Lua limit after splitting: a 40+ premise consume helper hands ~2N +-- captures to one constructor call (250 registers), its lifted functions +-- outgrow the chunk's locals, and one function can reference more than 60 +-- of them as upvalues. In wide mode: +-- * a static with more than WIDE_CAPS parameters takes its free vars as +-- one table T (read as T[i]), and splitting never refuses; +-- * a continuation with more than WIDE_CAPS captures reads CAPREF(base, i) +-- at each use instead of copying every capture into a local; +-- * a handle with more than WIDE_NEWCONT captures is built by +-- NEWCONTT(fn, {...}): same capbuf layout, no wide argument list; +-- * lifted functions are fields of one chunk table LT; +-- * a cons chain longer than WIDE_CONS is built by CONSL({...}, tail). +local WIDE_SPLIT_LOCALS = 60 +local WIDE_CAPS = 24 +local WIDE_NEWCONT = 48 +local WIDE_CONS = 16 + local function indent(d) return string.rep(" ", d) end -- A let extends env with a child table that __index-chains to its parent. @@ -301,6 +319,20 @@ compile_term = function(ctx, e, env, out, d) if is_cons(e) then local h = e[1] if h == SYM["cons"] and is_cons(e[2]) and is_cons(e[2][2]) then + if ctx.wide then + -- every pending CONS argument holds a register + local elems, t = {}, e + while is_cons(t) and t[1] == SYM["cons"] and is_cons(t[2]) and is_cons(t[2][2]) do + elems[#elems + 1] = t[2][1] + t = t[2][2][1] + end + if #elems > WIDE_CONS then + local parts = {} + for i, x in ipairs(elems) do parts[i] = compile_term(ctx, x, env, out, d) end + return "CONSL({" .. table.concat(parts, ", ") .. "}, " + .. compile_term(ctx, t, env, out, d) .. ")" + end + end local a = compile_term(ctx, e[2][1], env, out, d) local b = compile_term(ctx, e[2][2][1], env, out, d) return "CONS(" .. a .. ", " .. b .. ")" @@ -379,10 +411,11 @@ compile_value = function(ctx, e, env, out, d) -- (let V Expr Body) — including the kernel's multi-binding form -- (let V1 E1 V2 E2 ... Body), which the Shen macro pipeline would desugar if h == SYM["let"] and is_cons(args) and is_cons(args[2]) then - if ctx.split and ctx.fnloc >= LET_SPLIT_LOCALS then - -- a static this wide would split again on its first let + if ctx.split and ctx.fnloc >= (ctx.wide and WIDE_SPLIT_LOCALS or LET_SPLIT_LOCALS) then + -- a static this wide would split again on its first let (a wide + -- static takes them as one table) local fvs, implicit = static_fvs({}, e, env) - if #fvs < LET_SPLIT_LOCALS then + if ctx.wide or #fvs < LET_SPLIT_LOCALS then local st = ctx:lift_static(nil, {}, e, env, fvs, implicit) return ctx:callstatic(st, {}, env, out, d) end @@ -708,10 +741,22 @@ local function newcont_ctor(k) return "NEWCONTV" end +-- the handle construction for continuation function `fname` over the Lua +-- expressions `caps` +local function newcont_call(ctx, fname, caps) + if ctx.wide and #caps > WIDE_NEWCONT then + return "NEWCONTT(" .. fname .. ", {" .. table.concat(caps, ", ") .. "})" + end + local parts = { fname } + for _, c in ipairs(caps) do parts[#parts + 1] = c end + return newcont_ctor(#caps) .. "(" .. table.concat(parts, ", ") .. ")" +end + local function liftname(ctx, pfx) ctx.nlift = ctx.nlift + 1 local fname = pfx .. ctx.nlift ctx.liftnames[#ctx.liftnames + 1] = fname + if ctx.wide then return "LT." .. fname end return fname end @@ -760,9 +805,17 @@ function CtxMT.lift_static(ctx, name, params, body, env, fvs, implicit) sig[#sig + 1] = "p" .. i penv[p.name] = { lua = "p" .. i, kind = "term" } end - for i, vn in ipairs(fvs) do - sig[#sig + 1] = "fv" .. i - penv[vn] = { lua = "fv" .. i, kind = env[vn].kind } + if ctx.wide and #params + #fvs > WIDE_CAPS then + st.wide = true + sig[#sig + 1] = "T" + for i, vn in ipairs(fvs) do + penv[vn] = { lua = "T[" .. i .. "]", kind = env[vn].kind } + end + else + for i, vn in ipairs(fvs) do + sig[#sig + 1] = "fv" .. i + penv[vn] = { lua = "fv" .. i, kind = env[vn].kind } + end end local fbuf = {} local saved_loc = ctx.fnloc @@ -779,12 +832,17 @@ end -- direct invocation of a static (thaw GoTo / (GoTo a b)) function CtxMT.callstatic(ctx, st, call_args, env, out, d) - local parts = {} + local parts, fvp = {}, {} for _, a in ipairs(call_args) do parts[#parts + 1] = a end for _, vn in ipairs(st.fvs) do local b = env[vn] if not b then refuse(ctx, "static fv out of scope: " .. vn) end - parts[#parts + 1] = b.lua + fvp[#fvp + 1] = b.lua + end + if st.wide then + parts[#parts + 1] = "{" .. table.concat(fvp, ", ") .. "}" + else + for _, l in ipairs(fvp) do parts[#parts + 1] = l end end return st.fn .. "(" .. table.concat(parts, ", ") .. ")" end @@ -826,13 +884,18 @@ function CtxMT.lift_cont(ctx, body, env, out, d) for vn, b in pairs(implicit) do penv[vn] = b end local fbuf = {} local decls = {} + local wide = ctx.wide and #capture > WIDE_CAPS for i, vn in ipairs(capture) do - local lv = "c" .. i - decls[#decls + 1] = "local " .. lv .. " = CAPREF(base, " .. (i - 1) .. ")" - penv[vn] = { lua = lv, kind = env[vn].kind } + if wide then + penv[vn] = { lua = "CAPREF(base, " .. (i - 1) .. ")", kind = env[vn].kind } + else + local lv = "c" .. i + decls[#decls + 1] = "local " .. lv .. " = CAPREF(base, " .. (i - 1) .. ")" + penv[vn] = { lua = lv, kind = env[vn].kind } + end end local saved_loc = ctx.fnloc - ctx.fnloc = #capture + 2 + ctx.fnloc = (wide and 0 or #capture) + 2 local fval = compile_value(ctx, body, penv, fbuf, 1) ctx.fnloc = saved_loc local def = { fname .. " = function(base, h)" } @@ -842,9 +905,9 @@ function CtxMT.lift_cont(ctx, body, env, out, d) def[#def + 1] = "end" ctx.buf[#ctx.buf + 1] = table.concat(def, "\n") - local parts = { fname } - for _, vn in ipairs(capture) do parts[#parts + 1] = env[vn].lua end - return newcont_ctor(#capture) .. "(" .. table.concat(parts, ", ") .. ")" + local caps = {} + for _, vn in ipairs(capture) do caps[#caps + 1] = env[vn].lua end + return newcont_call(ctx, fname, caps) end -- a zero-param static used as a continuation value: wrap into a handle @@ -855,19 +918,25 @@ function CtxMT.mkhandle(ctx, st, out, d) -- 17. The width must not be capped: refusing leaves NativePred[name] -- unset while the already-translated caller still calls it. local fname = liftname(ctx, "LH") - local decls, parts = {}, { fname } + local decls, caps = {}, {} local args = {} for i, vn in ipairs(st.fvs) do - decls[#decls + 1] = " local c" .. i .. " = CAPREF(base, " .. (i - 1) .. ")" - args[#args + 1] = "c" .. i - parts[#parts + 1] = st.env[vn].lua + if st.wide then + args[#args + 1] = "CAPREF(base, " .. (i - 1) .. ")" + else + decls[#decls + 1] = " local c" .. i .. " = CAPREF(base, " .. (i - 1) .. ")" + args[#args + 1] = "c" .. i + end + caps[#caps + 1] = st.env[vn].lua end + local call_args = table.concat(args, ", ") + if st.wide then call_args = "{" .. call_args .. "}" end local def = { fname .. " = function(base, h)" } for _, l in ipairs(decls) do def[#def + 1] = l end - def[#def + 1] = " return " .. st.fn .. "(" .. table.concat(args, ", ") .. ")" + def[#def + 1] = " return " .. st.fn .. "(" .. call_args .. ")" def[#def + 1] = "end" ctx.buf[#ctx.buf + 1] = table.concat(def, "\n") - return newcont_ctor(#st.fvs) .. "(" .. table.concat(parts, ", ") .. ")" + return newcont_call(ctx, fname, caps) end -- --------------------------------------------------------------------------- @@ -897,7 +966,8 @@ local VAR_BASE, CONS_BASE = E.VAR_BASE, E.CONS_BASE -- translate_core: shared by defprolog define-forms and the t-star driver -- defuns. `allparams` is the full parameter list whose LAST FOUR entries are -- the Vec / Lock / Count / Cont gensyms (the uniform CPS goal ABI). -local function translate_once(name, allparams, body, split) +-- mode: false, "split" (LET_SPLIT_LOCALS), or "wide" (see WIDE_CAPS) +local function translate_once(name, allparams, body, mode) local np = #allparams assert(np >= 4, "prolog fn must have at least the B L K C params") local nparams = np - 4 @@ -906,7 +976,7 @@ local function translate_once(name, allparams, body, split) local ctx = setmetatable({ buf = {}, nlift = 0, nlocal = 0, fail = {}, liftnames = {}, - fnloc = nparams + 2, split = split, + fnloc = nparams + 2, split = mode and true or false, wide = mode == "wide", }, CtxMT) local env = {} @@ -932,12 +1002,17 @@ local function translate_once(name, allparams, body, split) return nil, tostring(val) end - if #ctx.liftnames > 150 then - return nil, "too many lifted functions (" .. #ctx.liftnames .. ")" - end local src = { CHUNK_PREAMBLE } - if #ctx.liftnames > 0 then - src[#src + 1] = "local " .. table.concat(ctx.liftnames, ", ") + if ctx.wide then + src[#src + 1] = "local NEWCONTT, CONSL = E.newcontT, E.cons_list\nlocal LT = {}" + else + if #ctx.liftnames > 150 then + return nil, "too many lifted functions (" .. #ctx.liftnames .. ")", nil, + "too many lifted functions" + end + if #ctx.liftnames > 0 then + src[#src + 1] = "local " .. table.concat(ctx.liftnames, ", ") + end end for _, def in ipairs(ctx.buf) do src[#src + 1] = def end src[#src + 1] = "return function(" .. table.concat(sig, ", ") .. ")" @@ -956,10 +1031,24 @@ end -- Let-chain splitting (see compile_value) costs a call per split point, so -- it is only used when the unsplit chunk exceeds Lua's local-variable cap. +-- The wide shape (see WIDE_CAPS) is the last resort, for what splitting +-- alone cannot fit. +local function width_error(lerr) + if not lerr then return false end + lerr = tostring(lerr) + return lerr:find("local variables", 1, true) ~= nil + or lerr:find("upvalues", 1, true) ~= nil + or lerr:find("too complex", 1, true) ~= nil + or lerr:find("too many lifted functions", 1, true) ~= nil +end + local function translate_core(name, allparams, body) local fn, err, src, lerr = translate_once(name, allparams, body, false) if lerr and tostring(lerr):find("local variables", 1, true) then - return translate_once(name, allparams, body, true) + fn, err, src, lerr = translate_once(name, allparams, body, "split") + end + if width_error(lerr) then + fn, err, src = translate_once(name, allparams, body, "wide") end return fn, err, src end diff --git a/prolog_engine.lua b/prolog_engine.lua index 40a8eb2..819bd80 100644 --- a/prolog_engine.lua +++ b/prolog_engine.lua @@ -186,6 +186,12 @@ local function mkcons(carv, cdrv) end M.cons = mkcons +-- t[1] . t[2] . ... . tail, allocated innermost first like nested CONS calls +function M.cons_list(t, tail) + for i = #t, 1, -1 do tail = mkcons(t[i], tail) end + return tail +end + function M.car(v) return cells[v - CONS_BASE] end function M.cdr(v) return cells[v - CONS_BASE + 1] end function M.is_cons(v) return v >= CONS_BASE end @@ -344,6 +350,20 @@ function M.newcontV(fn, ...) return h end +-- the captures arrive as one array: the wide translation of a continuation +-- whose argument list alone would pass LuaJIT's 250-register frame limit. +-- Same capbuf layout as newcontV; the table is not kept. +function M.newcontT(fn, t) + local k = #t + ckroom(k) + local b = cap_top + for i = 1, k do capbuf[b + i - 1] = t[i] end + cap_top = b + k + local h = ch_top + 1; ch_top = h + contFn[h] = fn; contBase[h] = b + return h +end + -- handle with a spill table for non-int32 captures (cold path) function M.newcont_spill(fn, tbl) local h = ch_top + 1; ch_top = h diff --git a/test/engine_spec.lua b/test/engine_spec.lua index e61a31e..d432e80 100644 --- a/test/engine_spec.lua +++ b/test/engine_spec.lua @@ -188,6 +188,18 @@ do for _, k in ipairs({ 17, 41, 100 }) do check(readback(k, E.newcontV), "newcontV " .. k .. " captures read back and reclaim") end + -- the wide translation's table-fed constructor + local function newcontT(fn, ...) return E.newcontT(fn, { ... }) end + for _, k in ipairs({ 1, 16, 49, 261 }) do + check(readback(k, newcontT), "newcontT " .. k .. " captures read back and reclaim") + end + + -- cons_list builds the same term as nested cons + local a, b, c = E.newvar(), E.newvar(), E.newvar() + local flat = E.cons_list({ a, b, c }, 0) + check(E.car(flat) == a and E.car(E.cdr(flat)) == b + and E.car(E.cdr(E.cdr(flat))) == c and E.cdr(E.cdr(E.cdr(flat))) == 0, + "cons_list matches nested cons") end -- --------------------------------------------------------------------------- From 7c5ca7a5972e738772143b58950f29d741962de1 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 9 Oct 2026 16:52:33 +0000 Subject: [PATCH 7/7] test: sequent rules up to 128 premises on both engines Co-authored-by: pyrex41 --- test/datatype_consume_spec.lua | 37 +++++++++++++++++++++++++++------- 1 file changed, 30 insertions(+), 7 deletions(-) diff --git a/test/datatype_consume_spec.lua b/test/datatype_consume_spec.lua index 2ee7c3f..370f365 100644 --- a/test/datatype_consume_spec.lua +++ b/test/datatype_consume_spec.lua @@ -85,6 +85,18 @@ local function run_rule(name, goal, assum) return res end +-- The same predicate on the legacy engine: the KL defun, called the way +-- shen.typecheck starts a proof. Wide rules run wide-mode code here +-- (compiler.lua, WIDE). +local function run_legacy(name, goal, assum) + local fn = P.F[name .. "#type"] + local lock = P.F["@v"](true, P.F["@v"](0, P.F["vector"](0))) + local ok, res = pcall(fn, goal, assum, P.F["shen.prolog-vector"](), lock, 0, + function() return true end) + if not ok then return nil, errmsg(res) end + return res +end + local function varname(i) return "V" .. i end local function define_row(n) @@ -115,9 +127,12 @@ shen.eval([[ -- first that used to be missing. From sixteen the native consume helper -- nested past LuaJIT's 100-table __index chain ("loop in gettable") and then -- past Lua's 200 locals per function; from about thirty the legacy KL defun --- did too, and the datatype failed to load at all. Thirty-seven is the --- widest that loads today (see the note at the end of this file). -local WIDTHS = { 5, 6, 8, 12, 15, 16, 20, 24, 30, 32, 37 } +-- did too, and the datatype failed to load at all. From thirty-eight the +-- legacy continuations passed ~3N values (250 registers per frame), which +-- needed wide mode on both compilers, as did 40+ in the native translator. +-- Sixty-four is past the 60-upvalue and 200-syntax-level limits, 100 and +-- 128 past the native 150 lifted functions. See the note at the end. +local WIDTHS = { 5, 6, 8, 12, 15, 16, 20, 24, 30, 32, 37, 38, 40, 64, 100, 128 } local function check_width(n) local before = {} @@ -178,14 +193,22 @@ local function check_width(n) local no, nerr = run_rule(name, nope, hyp) check(n .. " premises: unpacked rule does not prove 2 : piece", nerr or no, false) + + local lt, lterr = run_legacy(name, seven, tailhyp) + check(n .. " premises: legacy: last element is unpacked", lterr or lt, true) + local lm, lmerr = run_legacy(name, seven, hyp) + check(n .. " premises: legacy: 7 : piece needs the last element", lmerr or lm, false) + local ls, lserr = run_legacy(name, goal, bad) + check(n .. " premises: legacy: short hypothesis misses", lserr or ls, false) + local le, leerr = run_legacy(name, goal, R.NIL) + check(n .. " premises: legacy: empty context misses", leerr or le, false) end for _, n in ipairs(WIDTHS) do check_width(n) end --- Thirty-eight premises still fail to load: the legacy KL compiler hoists --- each premise's freeze continuation into a function taking all ~3N --- captures as parameters and passes them on in a nested call, which passes --- LuaJIT's 250-slot frame limit ("function or expression too complex"). +-- 194 premises is the widest that loads (checked by hand, ~15 s, so not in +-- WIDTHS). At 195 the consume helper's own signature has N+6 = 201 +-- parameters, past Lua's 200 locals per function in either compiler. print(string.format("datatype_consume_spec: %d pass, %d fail", pass, fail)) os.exit(fail == 0 and 0 or 1)