fix: sequent rules with up to 194 premises

[pyrex41]

How sequent premises compile (background for review)

Take a rule whose conclusion unpacks a list into N assumptions:

(datatype row
  V1 : piece, ..., VN : piece >> P;
  ________________________________
  [V1 ... VN] : row >> P;)

1. The rule becomes a Prolog predicate. row#type Goal Hyps makes N fresh Prolog variables W1..WN. It then calls a helper to find a matching hypothesis, and continues by proving Goal with the N new assumptions Wi : piece added in front of the remaining hypotheses.

2. The helper is shen.consume<N>. shen.specialise-consume (kernel sequent.kl) gensyms one helper per rule. Its signature is (shen.consumeN Hyps Rest W1 .. WN B L K C), so it takes N+6 arguments: the hypothesis list, the leftover hypotheses, the N output variables, and the four engine arguments (bindings, lock, cut key, continuation). It has two clauses:

• Clause 1 pattern-matches the first hypothesis against [cons E1 [cons E2 ... []]] : row, one hd/tl/lazyderef test per list element. That is about 6 nested lets per premise. It then binds the outputs in a chain: (bind W1 E1 .. (freeze (bind W2 E2 .. (freeze ... (bind Rest Tail .. C))))).
• Clause 2 skips the first hypothesis and recurses. It does this through a curried (lambda Z1 (lambda Z2 ...)) that closes over every argument.

The kernel also registers a lambda entry for the helper: N+6 nested lambdas around one call.

3. Continuations are where the width comes from. Each (freeze ...) in that bind chain is a continuation. When it runs, it needs every value the rest of the chain still uses: the remaining Wi and Ei, Rest, Tail, and B L K C. So the first freeze captures roughly 2N values, and with the helper's own arguments threaded through it is roughly 3N. The continuation that row#type hands to consumeN captures all N fresh variables and builds the N-element assumption list.

4. Two compilers, each with its own continuation representation. Every predicate is compiled twice:

• Legacy compiler (compiler.lua, always used). It compiles the KL defun to Lua. A freeze becomes a constant function KC[i] = function(cap1..capk) ... end. The use site is BIND(KC[i], cap1..capk), which snapshots the captures into a thunk. A value-position if/let is hoisted the same way and called as KC[i](caps). A lambda becomes a Lua closure, so its captures are upvalues.
• Native translator (prolog_compile.lua, used by the typechecker). It translates the same KL into direct Lua over the integer term arena. A continuation is a handle into a capture buffer: NEWCONTk(fn, c1..ck) for k ≤ 16 and NEWCONTV above that, read back with CAPREF(base, i). Statics and helpers are lifted to chunk-level functions that take their free variables as parameters.

5. Where each limit came from. Every limit is a Lua or LuaJIT ceiling hit by a function or call that grows with N. The rows are in the order a growing rule reaches them:

from (premises)	what grows	Lua ceiling	handled by
6	the consume helper's pattern-match continuation (2N+5 captures)	native mkhandle refused more than 16	NEWCONTV
16	native env, one __index table per let	100 chained tables	env flattening
16 native, ~30 legacy	~6 lets per premise in one function	200 locals per function	let split (only when loading fails)
38 legacy, 40 native	continuation captures passed as arguments (~3N)	250 registers per frame	wide mode: captures as one table
64	the kernel's lambda entry: N+6 nested lambdas	200 syntax levels	CURRY
64 native	row#type builds the N-element assumption list as nested CONS calls	250 registers	CONSL (wide mode)
190	row#type's chain of N shen.gc calls, flattened one local per frame	200 locals	one reused local (wide mode)
194	the call (shen.consumeN ...) with N+6 arguments	250 registers	UNPACK (wide mode)
195	the helper's own signature, N+6 parameters	200 locals	not fixed

From 38 premises on, the first error on both compilers is the 250-register limit. The rows below it only appear once that is fixed. The upvalue limit (60 per closure, clause 2's lambda) and the native translator's cap of 150 lifted functions never surface first, because wide mode already handles them (LAMW, an LT table). None of this involves the Shen value representation. It is all about how many names one generated Lua function holds.

Summary

Loading a Shen datatype rule with six or more premises over another user-defined type failed with shen.consume<N> is undefined, and wider rules hit the limits above in turn. Rules now work up to 194 premises on both engines (previously 5). Generated Lua is unchanged for everything that compiled before.

Rebased onto current main by merging it in (ShenOSKernel 42.2, #81, and the UTF-8 string primitives, #82). shen.specialise-consume and shen.consume-clause are the same code as in 42.0 apart from gensym numbers and simple-error becoming shen.f-error on partial-function paths. The helper shape did not change, so none of the wide-mode work became unnecessary and none of it had to be rewritten for 42.2.

Changes

Earlier commits (6 to 37 premises):

1. mkhandle → NEWCONTV past 16 captures. NEWCONTV writes the same contiguous capbuf layout and the same contFn/contBase entries as NEWCONT0..16.
2. Native env flattening every 32 let levels, keeping the same root lookup.
3. Native let split, retry only. Used when loadstring rejects a translated predicate for too many locals.
4. Legacy let split. Past 120 declared locals, the rest of a let chain continues in a fresh KC function via a tail call.
5. Pre-existing legacy miscompile. An inline freeze-let thawed inside a hoisted control form lost the freeze's free variables.

Wide mode (38 to 194 premises):

6. Legacy wide mode (compiler.lua, prims.lua). P.eval loads each defun as before. If Lua rejects the code for locals, upvalues, or "too complex", that one defun is recompiled with C.compile_top(form, true):

   • Captures: a hoisted body or freeze with more than 24 captures takes one table T and reads T[i]. Narrower hoists inside a wide body get fresh parameter names.
   • Live sets: let chains split at 80 locals whatever the live set, which travels as T.
   • Failure paths: multi-thaw failure continuations stay BIND/THAW closures instead of a goto label, so no label pins a let chain to one function.
   • Lambdas: a lambda closing over more than 40 names is hoisted and built by LAMW(KC[i], {...}).
   • Call chains: flattened chains reuse one local. Calls with more than 100 arguments pass UNPACK({...}, 1, n).

   Captured values are immutable KL bindings, so copying them into T at the use site observes exactly what the parameter form did.

7. CURRY for curried lambda chains deeper than 32, in every mode (no kernel chain is that deep). Each application returns a fresh closure over its own copy of the arguments so far.

8. Native wide retry (prolog_compile.lua, prolog_engine.lua). Used when the split translation still passes a Lua limit:

   • statics with more than 24 parameters take their free variables as a table;
   • wide continuations read CAPREF(base, i) at each use;
   • handles with more than 48 captures use NEWCONTT(fn, {...}), which has the same capture-buffer layout;
   • cons chains longer than 16 use CONSL({...}, tail);
   • lifted functions live in one LT table.

The merge with main touched three files. compiler.lua and prims.lua combined without conflict markers: the string->n of pos/hdstr fusion and the Unicode string primitives sit next to the wide-mode retry. scripts/run-tests.lua needed both new specs (utf8_strings_spec.lua and wide_compile_spec.lua).

Performance (against current main, ShenOSKernel 42.2)

• Unchanged code. Generated Lua is byte-identical to current main for all 1122 kernel forms, and for 121 native predicates plus 18 typechecker drivers (a kernel-suite run; none refused).
• einsteins-riddle (best of 5, 3 interleaved rounds, answer german on both): main 3.75–5.31 ms, this branch 3.64–4.24 ms. Parity; the 5.31 ms figure is one noisy main run.
• Kernel suite wall time (5 interleaved runs, median): main 2.22 s, this branch 2.20 s. Parity.
• Wide-mode cost, measured before the 42.2 merge by forcing wide code onto rules that also load ordinarily (one call that skips a hypothesis and unpacks the next): at 37 premises, 61–69 µs against 76–80 µs legacy and 13–18 µs against 21–23 µs native. Wide code was not slower. Rules that only load in wide mode: 40 premises 71/20 µs, 64 premises 126/70 µs, 100 premises 222/225 µs, 128 premises 257/657 µs (legacy/native). Native cost is superlinear because every continuation re-captures everything still pending.
• Datatype load time: about 0.5 s at 40 premises, 1.3 s at 64, 3.2 s at 100, 5 s at 128, and about 14 s at 194 (rechecked on 42.2).

Tests (on 42.2)

• make test: 1511 pass, 0 fail across 25 specs (includes test/utf8_strings_spec.lua from Make string primitives count Unicode code points (UTF-8) #82 and test/wide_compile_spec.lua).
• make certify: 143 passed, 0 failed (the 42.2 suite).
• test/datatype_consume_spec.lua (inside make test): 5, 6, 8, 12, 15, 16, 20, 24, 30, 32, 37, 38, 40, 64, 100, and 128 premises, on the native engine and the legacy KL rowN#type. 194 premises by hand: 16 pass, 0 fail. 195 still fails to load: the consume helper's own signature has 201 parameters (function at line 1 has more than 200 local variables).
• test/wide_compile_spec.lua: 27 checks. A 210-let chain with every binding live, the same chain under a two-thaw failure path, a lambda over 70 bindings, and a 40-deep curried chain. Each case first shows the ordinary code is rejected.
• test/engine_spec.lua: newcontT reads back and reclaims 1, 16, 49, and 261 captures; cons_list matches nested cons.

Remaining limits

• 195+ premises: the consume helper's signature has N+6 > 200 parameters, so neither compiler can emit it as a Lua function. Going further would need vararg signatures (function(...) with the parameters in a table) for very wide defuns, in both compilers.
• Native cost is O(N²) per proof for wide rules. A different continuation layout (chained capture frames instead of re-capturing) would fix that, but it would change the native continuation representation.