[pyrex41]

Fixes #85

Problem

The native Prolog engine runs in continuation-passing style on the Lua stack. A successful proof returns only after the whole query has succeeded, so proof depth equals Lua stack depth. LuaJIT's stack is fixed at about 65500 slots, and on main (e3dec8b) that gives these limits:

• (shen.typecheck (mk 400) peano) fails with shen: stack overflow.
• An 800-element [list number] fails the same way.
• The legacy engine reaches about 1000 levels, and shen-go has no limit.

Why not the issue's suggested fix

The issue suggests tail-calling thawH from unify/bind1 and letting the choice points unwind. That doesn't hold. The translated predicates try their alternatives as if r == false then <next clause>, with no trail marks and no undo (dumped peano#type / shen.system-S), so the undo inside unify_core and bind1 is what restores bindings when a clause fails. Two other frames can't be tail calls either:

• cut sets the lock when its continuation fails.
• A clause sequence ends with (unlock N) after failure.

Removing these frames would change semantics.

Fix: stack segments

Every coroutine has its own Lua stack, so a deep proof now continues on a fresh one.

• What counts. unify, bind1 and cut count their non-tail thaws. The counting is inlined, so no frame is added.
• Translated predicates. They call the new counted E.thawN (THAWN) for every thaw that isn't their return value. tail_return turns a thaw in return position back into a plain tail-called THAW. A tail call therefore never counts, and a constant-stack loop never opens a segment.
• Opening a segment. Every 96 counted frames, the next thaw runs on a new coroutine (thaw_segment). Errors are rethrown unchanged with error(e, 0), so Shen exception objects survive. A host's coroutine.yield from inside is passed through to the enclosing coroutine.
• Restoring the count. query_end restores the count, because an error unwinds past the decrements. A nested query keeps counting its caller's stack.
• Depth limit. Past 1000 nested segments, a query raises the trappable Prolog depth limit exceeded (1000 stack segments) instead of overflowing.

E.segments() and E.segment_limits() are exposed for tests and diagnostics.

Results (repros from the issue)

Run at head 8f50b50 with luajit bin/shen --hush-load <file>:

repro	base e3dec8b	head
nat-400 … nat-2000 (mk from the issue)	shen: stack overflow	peano
tc-800, tc-1000 ([list number])	shen: stack overflow	[list number]
nat-5000	[string "shen:mk"]:1: stack overflow	same (see below)

• nat-5000 isn't the engine. It overflows in the user's own non-tail recursive mk, before the typecheck starts. shen-go has a growable stack. This is a general limit of the port.
• Deeper probes. With an accumulator mk, typechecks now succeed up to 2000 nested [s N] and 4000 list elements. Past that they stop in the kernel's own recursive preprocessing, not in the engine. The frame histogram is 4673 × shen.curry + 4673 × shen.map-h. That limit is the same class as Reader fails on list literals over ~1550 elements with a misleading reader error near here: (suspected Lua stack overflow) #88's tree walkers and is outside this PR.
• e-draft. capcov's e-draft workload typechecks a system specification. On base it dies with shen: .../prolog_engine.lua:213: stack overflow. On this branch alone its payload is identical to shen-go 1f587de (sha256 bc80629a233e75af…).
• b-typed. capcov's b-typed workload also needs this fix as well as Generated Lua exceeds LuaJIT's 200-locals limit: datatype rules with nested conclusion patterns, list literals with 200+ elements #84 (fix: 200-locals shapes and long list literals (#84, #88; builds on #78) #91). Its typed-authority step wraps shen.typecheck in trap-error, so a stack overflow silently became a refused judgement. With Generated Lua exceeds LuaJIT's 200-locals limit: datatype rules with nested conclusion patterns, list literals with 200+ elements #84 alone, 7 of 46 cc-contracts judgements come out ok:false; with SHEN_PROLOG_ENGINE=legacy, 5 do; shen-go has 4. With Generated Lua exceeds LuaJIT's 200-locals limit: datatype rules with nested conclusion patterns, list literals with 200+ elements #84 and this PR together, the payload is identical to shen-go (dd877be7df09f341…).

Cost

• certify. make certify opens 0 segments: I counted with E.segments() around run-kernel-tests.lua, and it printed SEGMENTS 0.
• Microbenchmarks. In-process CPU time, best of N, base and head interleaved four times on a loaded machine (the same luajit build). Everything is within noise:

base: einstein 0.00172  tc-peano100 0.00176  tc-peano300 0.01340  tc-define 0.00028
head: einstein 0.00139  tc-peano100 0.00183  tc-peano300 0.01413  tc-define 0.00026
base: einstein 0.00183  tc-peano100 0.00183  tc-peano300 0.01390  tc-define 0.00025
head: einstein 0.00147  tc-peano100 0.00182  tc-peano300 0.01408  tc-define 0.00026
base: einstein 0.00148  tc-peano100 0.00187  tc-peano300 0.01353  tc-define 0.00024
head: einstein 0.00145  tc-peano100 0.00182  tc-peano300 0.01398  tc-define 0.00026
base: einstein 0.00178  tc-peano100 0.00194  tc-peano300 0.01416  tc-define 0.00026
head: einstein 0.00173  tc-peano100 0.00098  tc-peano300 0.00652  tc-define 0.00026

Tests

test/prolog_semantics_spec.lua gets 13 new checks:

• a 1500-deep peano typecheck and a 3000-element (list number) typecheck, both of which open segments;
• a shallow typecheck that opens none;
• backtracking out of a 3000-deep failing branch, which must undo (is R bottom) before (is R top);
• a cut 3000 levels deep that still prunes;
• an error 3000 levels deep, whose message must be identical to the shallow one;
• the engine staying usable after that error;
• no segment left open;
• a host coroutine.yield from 3000 levels deep reaching the host and resuming, and a yield with no host coroutine raising without leaving a segment open (4456af0);
• the cap, set to 2 via segment_limits, raising a trappable Prolog depth limit exceeded, with the next query still working.

On base, the spec dies at the first deep typecheck with stack overflow.

	make test	make certify (43.1 suite)
base e3dec8b	TOTAL: 1210 pass, 0 fail across 23 specs	passed ... 154 / failed ... 0
head 4456af0	TOTAL: 1223 pass, 0 fail across 23 specs	passed ... 154 / failed ... 0

Both were run with GIT_DIR/GIT_WORK_TREE/GIT_INDEX_FILE unset and a private TMPDIR.

Merge note

This merges cleanly with #78 (which also edits prolog_compile.lua / prolog_engine.lua) and with #91 (#84/#88) and #89 (#86/#87), apart from a trivial CHANGELOG.md conflict. On a local merge of all three (not pushed), make test gave TOTAL: 1706 pass, 0 fail across 26 specs and certify gave passed ... 154 / failed ... 0.

🤖 Generated with Claude Code