prolog_engine.lua

-- prolog_engine.lua — native soa32 Prolog / type-inference substrate.
--
-- The execution engine that replaces the compiled-KL CPS Prolog machinery
-- (klambda/prolog.kl runtime + the t-star.kl driver's allocation profile).
-- Design validated by bench/wam_poc_v4.lua ("soa32"):
--
--   * Terms are PLAIN LUA NUMBERS, range-tagged:
--       atom id          v <  VAR_BASE  (2^24)
--       var   VAR_BASE <= v <  CONS_BASE (2^25), idx = v - VAR_BASE
--       cons             v >= CONS_BASE,         pair p = v - CONS_BASE
--     Tag tests are `<` compares; payload extraction is subtraction. There are
--     deliberately NO bit operations and NO 64-bit cdata anywhere — int64
--     tag-packing was measured 2.2x slower (the v2 PoC trap).
--   * Storage is int32_t FFI arrays (cells / vbind / trail / capture buffer),
--     grown by doubling. vbind[idx] == -1 means unbound (terms are >= 0).
--   * Unification is ITERATIVE over explicit goal stacks with a trail;
--     failure unwinds bindings in a batch back to the caller's trail mark.
--   * Continuations are DEFUNCTIONALIZED: an integer handle indexing
--     contFn[h] (a statically-lifted Lua function) + contBase[h] (offset into
--     the int32 capture buffer). No freeze closures. Rare non-int32 captures
--     go to the cold contSpill[h] table.
--   * Choice points live in the LUA STACK FRAME of each predicate function:
--     plain-local marks (trail/var/cont tops) captured at entry, batch-unwound
--     at every alternative-try point. No heap choice-point objects.
--   * Cut is a 1:1 transcription of shen.cut/lock/unlock/unlocked?/fits?
--     (klambda/prolog.kl:80-92) over two scalars lock_open / lock_depth.
--
-- Success propagates as a non-false return value (like the legacy engine —
-- `return` passes the answer term up through the cont chain); failure is the
-- literal `false`.
--
-- This module is loaded by boot.lua unless SHEN_PROLOG_ENGINE=legacy. Until
-- the clause compiler (prolog_compile.lua) and the t-star port
-- (typecheck_native.lua) wire into it, install() is inert.

-- PUC Lua tier: without the FFI the soa32 substrate cannot exist. Return an
-- inert module — boot.lua's install() call becomes a no-op and the kernel
-- keeps the compiled-KL CPS Prolog engine (exactly SHEN_PROLOG_ENGINE=legacy).
local ok_ffi, ffi = pcall(require, "ffi")
if not ok_ffi then
  return { install = function() end }
end
local R = require("runtime")
local SD, SEGRUN, SEG_FRAMES = R.seg.SD, R.seg.run, R.seg.FRAMES

local loadstring = loadstring or load   -- 5.2+ shim (module is FFI-gated anyway)

local M = {}

-- ---------------------------------------------------------------------------
-- tagging
-- ---------------------------------------------------------------------------
local VAR_BASE  = 16777216        -- 2^24
local CONS_BASE = 33554432        -- 2^25
M.VAR_BASE, M.CONS_BASE = VAR_BASE, CONS_BASE

-- ---------------------------------------------------------------------------
-- arenas (int32 FFI arrays, grow-by-doubling)
-- ---------------------------------------------------------------------------
local function newarr(n) return ffi.new("int32_t[?]", n) end
local function grown(arr, cap, need)
  local nc = cap
  repeat nc = nc * 2 until nc >= need
  local na = newarr(nc)
  ffi.copy(na, arr, cap * 4)
  return na, nc
end

local cells, ccap = newarr(65536), 65536      -- cons pairs: car at p, cdr at p+1
local vbind, vcap = newarr(16384), 16384      -- per-var binding; -1 = unbound
local trail, tcap = newarr(16384), 16384      -- bound var indices
local capbuf, kcap = newarr(16384), 16384     -- continuation captures
local gA, gB, gcap = newarr(4096), newarr(4096), 4096  -- unify goal stacks

local cell_top, var_top, trail_top, cap_top = 0, 0, 0, 0

-- Kernel globals / error thrower, bound in install(). Declared up here
-- because newvar's per-query capacity check needs them.
local GLOBALS, ERRFN, KEQ   -- KEQ: the kernel's `=`

-- Per-query variable capacity (the kernel's shen.prolog-vector ceiling).
-- shen.call-prolog allocates ONE absvector of (value shen.*prolog-memory*)
-- slots per query (macros.shen:179); slot 0 holds the printer and slot 1 the
-- next-index ticket, so indices 2..N-1 are available and shen.newpv raises
-- once the ticket reaches N. var_base is this query's var_top at entry, so
-- var_top - var_base is exactly the kernel's (ticket - 2).
local var_base, var_limit = 0, math.huge

-- continuation registry (handles are 1-based ints)
local contFn, contBase, contSpill = {}, {}, {}
local ch_top = 0

-- cut lock (transcribed from the legacy lock absvector {unlocked?, depth})
local lock_open, lock_depth = true, 0

-- inference counter (flushed to GLOBALS["shen.*infs*"] by the typecheck port)
local infs = 0

-- ---------------------------------------------------------------------------
-- atom interning
-- ---------------------------------------------------------------------------
local Symbol, Cons, Vmt, NIL = R.Symbol, R.Cons, R.Vmt, R.NIL
local shen_pvar = R.intern("shen.pvar")
local getmt = getmetatable

local atomval = { [0] = NIL, [1] = true, [2] = false }
local atom_top = 2
local symAtom, numAtom, strAtom = {}, {}, {}
local opqAtom = {}              -- opaque objects, identity-interned
local opq_log, opq_top = {}, 0  -- interned-this-query log (epoch-cleared)

local function atom(x)
  if x == NIL then return 0 end
  local t = type(x)
  local id
  if t == "boolean" then
    return x and 1 or 2
  elseif t == "number" then
    id = numAtom[x]
    if id then return id end
    atom_top = atom_top + 1; id = atom_top
    if id >= VAR_BASE then error("prolog_engine: atom table overflow") end
    numAtom[x] = id; atomval[id] = x
    return id
  elseif t == "string" then
    id = strAtom[x]
    if id then return id end
    atom_top = atom_top + 1; id = atom_top
    if id >= VAR_BASE then error("prolog_engine: atom table overflow") end
    strAtom[x] = id; atomval[id] = x
    return id
  elseif getmt(x) == Symbol then
    id = symAtom[x]
    if id then return id end
    atom_top = atom_top + 1; id = atom_top
    if id >= VAR_BASE then error("prolog_engine: atom table overflow") end
    symAtom[x] = id; atomval[id] = x
    return id
  else
    -- opaque value (freshterm absvector, tuple, stream, closure, ...):
    -- identity-interned, released at query end so a long session can't leak.
    id = opqAtom[x]
    if id then return id end
    atom_top = atom_top + 1; id = atom_top
    if id >= VAR_BASE then error("prolog_engine: atom table overflow") end
    opqAtom[x] = id; atomval[id] = x
    opq_top = opq_top + 1; opq_log[opq_top] = x
    return id
  end
end
M.atom = atom

function M.atomval(v) return atomval[v] end

-- ---------------------------------------------------------------------------
-- term construction / inspection
-- ---------------------------------------------------------------------------
local function newvar()
  local idx = var_top
  if idx - var_base >= var_limit then
    -- The kernel raises an out-of-range absvector index here. The message is
    -- port-specific prose on every port; what has to agree is that the query
    -- RAISES rather than answering.
    ERRFN("prolog vector index out of range: a single query may allocate at "
          .. "most " .. var_limit .. " variables (shen.*prolog-memory*)")
  end
  if idx >= vcap then vbind, vcap = grown(vbind, vcap, idx + 1) end
  vbind[idx] = -1
  var_top = idx + 1
  return VAR_BASE + idx
end
M.newvar = newvar

-- LIFO-pop the most recent var: the translated (shen.gc B E) reclaim, paired
-- 1:1 with a preceding shen.newpv by the stpart emission structure
function M.popvar()
  var_top = var_top - 1
end

local function mkcons(carv, cdrv)
  local p = cell_top
  if p + 2 > ccap then cells, ccap = grown(cells, ccap, p + 2) end
  cells[p] = carv
  cells[p + 1] = cdrv
  cell_top = p + 2
  return CONS_BASE + p
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
function M.is_var(v) return v >= VAR_BASE and v < CONS_BASE end
function M.is_atom(v) return v < VAR_BASE end

-- follow bound-var chains; stops at an unbound var or a non-var
local function lazyderef(v)
  while v >= VAR_BASE and v < CONS_BASE do
    local b = vbind[v - VAR_BASE]
    if b >= 0 then v = b else break end
  end
  return v
end
M.lazyderef = lazyderef

-- ---------------------------------------------------------------------------
-- continuations
-- ---------------------------------------------------------------------------
-- Lifted continuation functions are called as fn(base, h): they read their
-- captures at fixed offsets capbuf[base + i] (and cold spills via
-- contSpill[h]). thaw accepts either a handle (number) or a plain Lua
-- function — call sites are monomorphic, so the type() branch is trace-cheap.
local function thawH(h)
  if type(h) == "number" then
    return contFn[h](contBase[h], h)
  end
  return h()
end
M.thawH = thawH

-- Stack segments (pyrex41/shen-lua#85). The engine is CPS on the Lua stack:
-- a successful proof returns only once the whole query has succeeded, so its
-- depth is the Lua stack depth. LuaJIT's stack is a fixed ~65500 slots per
-- coroutine, which capped a typecheck at ~375 nested rule applications. But
-- every coroutine has its own stack, so a deep proof continues in a fresh
-- coroutine (a segment) and depth becomes bounded by memory instead.
--
-- The trigger counts the engine's own NON-tail continuation calls -- the
-- thaws in unify, bind1 and cut, which must stay non-tail because they undo
-- bindings / set the lock when the continuation fails. Every rule
-- application on a proof path passes through at least one of them, and the
-- generated predicate frames between two of them are bounded by the clause
-- shapes. Tail-called thaws never count, so a loop that runs in constant
-- stack never opens a segment.
local SEG_FRAMES = 96        -- counted frames per segment: a typecheck
                             -- overflowed one stack after ~750 of them
local SEG_MAX = 1000         -- nested segments per query before giving up
local seg_depth, seg_count = 0, 0
local seg_total = 0          -- segments ever opened (M.segments, diagnostics)

-- Thaw `cont` on a fresh coroutine stack and return its value. Errors are
-- rethrown unchanged (Shen exception objects included); a yield from inside
-- (an embedding host's) is passed through to the enclosing coroutine.
local function thaw_segment(cont)
  if seg_count >= SEG_MAX then
    ERRFN("Prolog depth limit exceeded (" .. SEG_MAX .. " stack segments)")
  end
  local saved, saved_count = seg_depth, seg_count
  seg_count = seg_count + 1; seg_depth = 0
  seg_total = seg_total + 1
  -- the runtime's segment runner (runtime.lua, #93): its nesting cap covers
  -- both kinds of segment, which share one C stack
  local ok, r = pcall(SEGRUN, thawH, cont)
  -- assign, not decrement: segments abandoned while suspended never return
  seg_count, seg_depth = saved_count, saved
  if not ok then error(r, 0) end
  return r
end

-- thawH for a non-tail site: counts the frame, or opens a segment. The
-- translated predicates call it (THAWN) wherever a thaw is not their return
-- value. unify, bind1 and cut write the same lines out inline instead, so
-- the counting costs them no extra frame:
--   local d = seg_depth
--   local r
--   if d < SEG_FRAMES then seg_depth = d + 1; r = thawH(cont); seg_depth = d
--   else r = thaw_segment(cont) end
local function thawN(h)
  local d = seg_depth
  if d >= SEG_FRAMES then return thaw_segment(h) end
  seg_depth = d + 1
  local r
  if type(h) == "number" then r = contFn[h](contBase[h], h) else r = h() end
  seg_depth = d
  return r
end
M.thawN = thawN

local function ckroom(n)
  if cap_top + n > kcap then capbuf, kcap = grown(capbuf, kcap, cap_top + n) end
end

function M.newcont0(fn)
  local h = ch_top + 1; ch_top = h
  contFn[h] = fn; contBase[h] = cap_top
  return h
end
function M.newcont1(fn, a)
  ckroom(1)
  local b = cap_top; capbuf[b] = a; cap_top = b + 1
  local h = ch_top + 1; ch_top = h
  contFn[h] = fn; contBase[h] = b
  return h
end
function M.newcont2(fn, a, a2)
  ckroom(2)
  local b = cap_top; capbuf[b] = a; capbuf[b+1] = a2; cap_top = b + 2
  local h = ch_top + 1; ch_top = h
  contFn[h] = fn; contBase[h] = b
  return h
end
function M.newcont3(fn, a, a2, a3)
  ckroom(3)
  local b = cap_top; capbuf[b] = a; capbuf[b+1] = a2; capbuf[b+2] = a3
  cap_top = b + 3
  local h = ch_top + 1; ch_top = h
  contFn[h] = fn; contBase[h] = b
  return h
end
function M.newcont4(fn, a, a2, a3, a4)
  ckroom(4)
  local b = cap_top
  capbuf[b] = a; capbuf[b+1] = a2; capbuf[b+2] = a3; capbuf[b+3] = a4
  cap_top = b + 4
  local h = ch_top + 1; ch_top = h
  contFn[h] = fn; contBase[h] = b
  return h
end
function M.newcont5(fn, a, a2, a3, a4, a5)
  ckroom(5)
  local b = cap_top
  capbuf[b] = a; capbuf[b+1] = a2; capbuf[b+2] = a3; capbuf[b+3] = a4
  capbuf[b+4] = a5
  cap_top = b + 5
  local h = ch_top + 1; ch_top = h
  contFn[h] = fn; contBase[h] = b
  return h
end
function M.newcont6(fn, a, a2, a3, a4, a5, a6)
  ckroom(6)
  local b = cap_top
  capbuf[b] = a; capbuf[b+1] = a2; capbuf[b+2] = a3; capbuf[b+3] = a4
  capbuf[b+4] = a5; capbuf[b+5] = a6
  cap_top = b + 6
  local h = ch_top + 1; ch_top = h
  contFn[h] = fn; contBase[h] = b
  return h
end
function M.newcont7(fn, a, a2, a3, a4, a5, a6, a7)
  ckroom(7)
  local b = cap_top
  capbuf[b] = a; capbuf[b+1] = a2; capbuf[b+2] = a3; capbuf[b+3] = a4
  capbuf[b+4] = a5; capbuf[b+5] = a6; capbuf[b+6] = a7
  cap_top = b + 7
  local h = ch_top + 1; ch_top = h
  contFn[h] = fn; contBase[h] = b
  return h
end
function M.newcont8(fn, a, a2, a3, a4, a5, a6, a7, a8)
  ckroom(8)
  local b = cap_top
  capbuf[b] = a; capbuf[b+1] = a2; capbuf[b+2] = a3; capbuf[b+3] = a4
  capbuf[b+4] = a5; capbuf[b+5] = a6; capbuf[b+6] = a7; capbuf[b+7] = a8
  cap_top = b + 8
  local h = ch_top + 1; ch_top = h
  contFn[h] = fn; contBase[h] = b
  return h
end

-- newcont9..newcont16 (generated): wide conjunctions in compiled clauses can
-- capture more than 8 live variables. Same monomorphic shape as 0-8.
for k = 9, 16 do
  local args, stores = {}, {}
  for i = 1, k do
    args[i] = "x" .. i
    stores[i] = "capbuf[b+" .. (i - 1) .. "] = x" .. i
  end
  local src = ([[
local ckroom, state = ...
return function(fn, %s)
  ckroom(%d)
  local capbuf, b = state.capbuf(), state.cap_top()
  %s
  return state.push(fn, b, %d)
end]]):format(table.concat(args, ", "), k, table.concat(stores, "; "), k)
  -- state accessors keep the generated code valid across arena growth
  local mk = assert(loadstring(src, "@newcont" .. k))
  M["newcont" .. k] = mk(ckroom, {
    capbuf = function() return capbuf end,
    cap_top = function() return cap_top end,
    push = function(fn, b, n)
      cap_top = b + n
      local h = ch_top + 1; ch_top = h
      contFn[h] = fn; contBase[h] = b
      return h
    end,
  })
end

-- varargs fallback for very wide captures (>16): trace-unfriendly but cold —
-- only long conjunctions with many clause variables reach it, once per
-- clause-body entry
function M.newcontV(fn, ...)
  local k = select("#", ...)
  ckroom(k)
  local b = cap_top
  for i = 1, k do
    capbuf[b + i - 1] = select(i, ...)
  end
  cap_top = b + k
  local h = ch_top + 1; ch_top = h
  contFn[h] = fn; contBase[h] = b
  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
  contFn[h] = fn; contBase[h] = cap_top; contSpill[h] = tbl
  return h
end
function M.spill(h) return contSpill[h] end

function M.capref(b, i) return capbuf[b + i] end

-- ---------------------------------------------------------------------------
-- marks / backtracking
-- ---------------------------------------------------------------------------
-- A choice point saves five tops: trail, var, cont-handle, capture-buffer,
-- cell. Cell reclaim at a failed alternative is safe: cells built after the
-- mark are only reachable through (a) bindings made after the mark — unwound
-- by the same undo — or (b) Lua locals of frames that are dead on the failure
-- path. Anything that must survive backtracking (findall solutions, returned
-- answers) is materialized OUT to Shen values first.
local function marks()
  return trail_top, var_top, ch_top, cap_top, cell_top
end
M.marks = marks

local function undo(tm, vm, hm, bm, cm)
  for i = trail_top - 1, tm, -1 do
    vbind[trail[i]] = -1
  end
  trail_top = tm
  var_top = vm
  for h = ch_top, hm + 1, -1 do
    contFn[h] = nil; contSpill[h] = nil
  end
  ch_top = hm
  cap_top = bm
  cell_top = cm
end
M.undo = undo

-- ---------------------------------------------------------------------------
-- unification
-- ---------------------------------------------------------------------------
-- occurs(idx, term): does var idx occur in (derefed) term? Iterative walk
-- using the gB stack scratch (safe: only called outside an active unify loop,
-- before any goal-stack use of the same depth region... NOT safe — use its
-- own small stack instead).
local ostk, ocap = newarr(1024), 1024
local function occurs(idx, v)
  local n = 1
  ostk[0] = v
  while n > 0 do
    n = n - 1
    local x = lazyderef(ostk[n])
    if x >= CONS_BASE then
      local p = x - CONS_BASE
      if n + 2 > ocap then ostk, ocap = grown(ostk, ocap, n + 2) end
      ostk[n] = cells[p]; ostk[n + 1] = cells[p + 1]
      n = n + 2
    elseif x >= VAR_BASE then
      if x - VAR_BASE == idx then return true end
    end
  end
  return false
end
M.occurs = occurs

-- core unify loop. oc = occurs-check var bindings (lzy=! vs lzy=).
-- On structural success thaws cont; if the cont fails, bindings made HERE are
-- unwound (batch, to the entry trail mark) — semantically identical to the
-- legacy per-bind! unwind chain. Returns the cont's value, or false.
local function unify_core(rootA, rootB, cont, oc)
  local n = 1
  gA[0] = rootA; gB[0] = rootB
  local tmark = trail_top
  local tn = tmark
  local ok = true
  while n > 0 do
    n = n - 1
    local x = gA[n]
    local y = gB[n]
    -- inline lazyderef
    while x >= VAR_BASE and x < CONS_BASE do
      local b = vbind[x - VAR_BASE]
      if b >= 0 then x = b else break end
    end
    while y >= VAR_BASE and y < CONS_BASE do
      local b = vbind[y - VAR_BASE]
      if b >= 0 then y = b else break end
    end
    if x == y then
      -- identical atom / same var / same cons cell: success at this goal
    elseif x >= VAR_BASE and x < CONS_BASE then
      local idx = x - VAR_BASE
      if oc and y >= CONS_BASE and occurs(idx, y) then ok = false; break end
      vbind[idx] = y
      if tn >= tcap then trail, tcap = grown(trail, tcap, tn + 1) end
      trail[tn] = idx; tn = tn + 1
    elseif y >= VAR_BASE and y < CONS_BASE then
      local idx = y - VAR_BASE
      if oc and x >= CONS_BASE and occurs(idx, x) then ok = false; break end
      vbind[idx] = x
      if tn >= tcap then trail, tcap = grown(trail, tcap, tn + 1) end
      trail[tn] = idx; tn = tn + 1
    elseif x >= CONS_BASE and y >= CONS_BASE then
      local px, py = x - CONS_BASE, y - CONS_BASE
      if n + 2 > gcap then
        local oldcap = gcap
        gA, gcap = grown(gA, oldcap, n + 2)
        gB = (grown(gB, oldcap, n + 2))
      end
      gA[n] = cells[px + 1]; gB[n] = cells[py + 1]; n = n + 1
      gA[n] = cells[px];     gB[n] = cells[py];     n = n + 1
    else
      ok = false
      break
    end
  end
  if ok then
    trail_top = tn
    local d = seg_depth
    local r
    if d < SEG_FRAMES then seg_depth = d + 1; r = thawH(cont); seg_depth = d
    else r = thaw_segment(cont) end
    if r == false then
      for i = tn - 1, tmark, -1 do vbind[trail[i]] = -1 end
      trail_top = tmark
      return false
    end
    return r
  else
    for i = tn - 1, tmark, -1 do vbind[trail[i]] = -1 end
    -- trail_top was never advanced past tmark on the failure path
    return false
  end
end

function M.unify(a, b, cont)    return unify_core(a, b, cont, false) end  -- lzy=
function M.unify_oc(a, b, cont) return unify_core(a, b, cont, true)  end  -- lzy=!

-- shen.bind! equivalent: bind a (known-unbound) var, thaw, unwind on failure.
function M.bind1(varv, val, cont)
  local idx = varv - VAR_BASE
  vbind[idx] = val
  if trail_top >= tcap then trail, tcap = grown(trail, tcap, trail_top + 1) end
  trail[trail_top] = idx
  trail_top = trail_top + 1
  local d = seg_depth
  local r
  if d < SEG_FRAMES then seg_depth = d + 1; r = thawH(cont); seg_depth = d
  else r = thaw_segment(cont) end
  if r == false then
    vbind[idx] = -1
    trail_top = trail_top - 1
    return false
  end
  return r
end

-- ---------------------------------------------------------------------------
-- cut (transcribed from klambda/prolog.kl:80-92)
-- ---------------------------------------------------------------------------
function M.lock_is_open() return lock_open end

-- shen.cut: thaw; on failure with an open lock, lock at depth n.
function M.cut(n, cont)
  local d = seg_depth
  local r
  if d < SEG_FRAMES then seg_depth = d + 1; r = thawH(cont); seg_depth = d
  else r = thaw_segment(cont) end
  if r == false and lock_open then
    lock_open = false
    lock_depth = n
    return false
  end
  return r
end

-- shen.unlock: re-open iff locked at exactly this depth; always "fails"
-- (it is the value of a fully-exhausted clause sequence).
function M.unlock(n)
  if (not lock_open) and lock_depth == n then
    lock_open = true
  end
  return false
end

-- ---------------------------------------------------------------------------
-- inference counter
-- ---------------------------------------------------------------------------
function M.incinfs() infs = infs + 1 end
function M.getinfs() return infs end
function M.setinfs(n) infs = n end

-- ---------------------------------------------------------------------------
-- Shen-value <-> arena-term boundary
-- ---------------------------------------------------------------------------
-- import: deep-convert a Shen value into an arena term. Legacy-format pvar
-- absvectors map to arena vars via `varmap` (keyed by pvar ticket), creating
-- fresh vars on first sight — callers that need to read bindings back out
-- keep the map. Proper-list spines are converted iteratively (no deep
-- recursion); only car nesting recurses.
local function import(x, varmap)
  if getmt(x) == Cons then
    -- walk the spine, then build cells back-to-front
    local spine, sn = {}, 0
    while getmt(x) == Cons do
      sn = sn + 1; spine[sn] = x[1]
      x = x[2]
    end
    local tail = import(x, varmap)
    for i = sn, 1, -1 do
      local e = spine[i]
      if getmt(e) == Cons then
        -- car nesting recurses: count it (runtime.lua stack segments, #93)
        local d = SD[1]
        if d < SEG_FRAMES then SD[1] = d + 1; e = import(e, varmap); SD[1] = d
        else e = SEGRUN(import, e, varmap) end
      else
        e = import(e, varmap)
      end
      tail = mkcons(e, tail)
    end
    return tail
  elseif getmt(x) == Vmt and x[2] == shen_pvar then
    local key = x[3]
    local v = varmap and varmap[key]
    if v then return v end
    v = newvar()
    if varmap then varmap[key] = v end
    return v
  else
    return atom(x)
  end
end
M.import = import

-- import_cached: identity-memoized import for values re-imported repeatedly
-- within one query (e.g. the shen.*datatypes* assoc list, passed to every
-- search-user-datatypes call). Sound because Shen list structure is immutable
-- and pvar imports go through the identity varmap (no allocation). The memo
-- is cleared at query_end (cells are reclaimed there).
local import_memo = {}
local identity_varmap = setmetatable({}, {
  __index = function(_, idx) return VAR_BASE + idx end,
})
M.identity_varmap = identity_varmap

local function import_cached(x)
  if type(x) == "table" then
    local t = import_memo[x]
    if t then return t end
    t = M.import(x, identity_varmap)
    import_memo[x] = t
    return t
  end
  return M.import(x, identity_varmap)
end
M.import_cached = import_cached

-- maxinferences check, transcribed from shen.maxinfexceeded? (t-star.kl):
-- THROWS "maximum inferences exceeded" past the limit, else returns false
function M.maxinf_exceeded()
  local mx = GLOBALS and GLOBALS["shen.*maxinferences*"]
  if type(mx) == "number" and infs > mx then
    ERRFN("maximum inferences exceeded")
  end
  return false
end

-- materialize: deep deref + export an arena term to a Shen value. Unbound
-- vars become legacy-format pvar absvectors {2, shen.pvar, idx} (cached per
-- idx — they are immutable, so sharing across calls is safe), preserving
-- legacy printing / equality / guard behavior.
local pvcache = {}
local function mat_pvar(idx)
  local pv = pvcache[idx]
  if not pv then
    pv = setmetatable({ 2, shen_pvar, idx }, Vmt)
    pvcache[idx] = pv
  end
  return pv
end

local function materialize(v)
  v = lazyderef(v)
  if v < VAR_BASE then
    return atomval[v]
  elseif v < CONS_BASE then
    return mat_pvar(v - VAR_BASE)
  else
    -- iterative over the cdr spine; recursive on cars
    local items, n = {}, 0
    while true do
      v = lazyderef(v)
      if v >= CONS_BASE then
        local p = v - CONS_BASE
        n = n + 1; items[n] = materialize(cells[p])
        v = cells[p + 1]
      else
        break
      end
    end
    local tail
    if v < VAR_BASE then tail = atomval[v] else tail = mat_pvar(v - VAR_BASE) end
    for i = n, 1, -1 do
      tail = R.cons(items[i], tail)
    end
    return tail
  end
end
M.materialize = materialize

-- eqterm: Shen `=` of two arena terms, i.e. (= (materialize a)
-- (materialize b)), without building either side. Identical terms are equal
-- and a cons never equals a non-cons. Any other pair of distinct non-cons
-- terms (atoms or vars) is decided by the kernel's `=` on their
-- materializations, which are O(1) (an atom's value or a cached pvar), so
-- opaque values such as tuples and vectors keep their structural `=`.
-- Iterative over the cdr spine; car nesting recurses and is counted like
-- import's (runtime.lua stack segments, #93).
local eqterm
eqterm = function(a, b)
  while true do
    a = lazyderef(a); b = lazyderef(b)
    if a == b then return true end
    if a >= CONS_BASE then
      if b < CONS_BASE then return false end
      local pa, pb = a - CONS_BASE, b - CONS_BASE
      local ca, cb = cells[pa], cells[pb]
      if ca ~= cb then
        local same
        local d = SD[1]
        if d < SEG_FRAMES then SD[1] = d + 1; same = eqterm(ca, cb); SD[1] = d
        else same = SEGRUN(eqterm, ca, cb) end
        if not same then return false end
      end
      a = cells[pa + 1]; b = cells[pb + 1]
    elseif b >= CONS_BASE then
      return false
    else
      return KEQ(materialize(a), materialize(b))
    end
  end
end
M.eqterm = eqterm

-- ---------------------------------------------------------------------------
-- goal builtins (legacy 6-arg goal ABI becomes (args..., n, cont))
-- ---------------------------------------------------------------------------
function M.g_when(test, n, cont)             -- (when Test ...) prolog.kl:179
  if test == true then return thawH(cont) end
  return false
end
function M.g_var(v, n, cont)                 -- (var? X ...)    prolog.kl:187
  local d = lazyderef(v)
  if d >= VAR_BASE and d < CONS_BASE then return thawH(cont) end
  return false
end
function M.g_return(v)                       -- (return V ...)  prolog.kl:177
  return materialize(v)
end
-- is/is!/bind compile straight to M.unify / M.unify_oc / M.bind1.
-- fork / findall / call need the clause compiler's dispatch table and are
-- provided by prolog_compile.lua (Phase 2).

-- ---------------------------------------------------------------------------
-- query lifecycle
-- ---------------------------------------------------------------------------
-- Nested queries run above the current tops and fully unwind before the outer
-- resumes; query_begin/query_end save and restore every piece of engine state
-- a query can touch (including the cut lock and the opaque-intern epoch).
function M.query_begin()
  local q = {
    cell_top, var_top, trail_top, cap_top, ch_top,
    lock_open, lock_depth, opq_top,
    var_base, var_limit, seg_depth, seg_count,
  }
  lock_open, lock_depth = true, 0
  -- Fresh bindings vector for this query, exactly as shen.call-prolog does:
  -- the budget is re-read every time, so (prolog-memory N) takes effect on
  -- the next query, and a nested query gets its own full budget.
  var_base = var_top
  local n = GLOBALS and GLOBALS["shen.*prolog-memory*"]
  var_limit = (type(n) == "number" and n > 2) and (n - 2) or math.huge
  return q
end

function M.query_end(q)
  -- unwind trail bindings made during the query
  for i = trail_top - 1, q[3], -1 do
    vbind[trail[i]] = -1
  end
  cell_top, var_top, trail_top, cap_top = q[1], q[2], q[3], q[4]
  for h = ch_top, q[5] + 1, -1 do
    contFn[h] = nil; contSpill[h] = nil
  end
  ch_top = q[5]
  lock_open, lock_depth = q[6], q[7]
  -- release opaque atoms interned during the query
  for i = opq_top, q[8] + 1, -1 do
    local obj = opq_log[i]
    atomval[opqAtom[obj]] = nil
    opqAtom[obj] = nil
    opq_log[i] = nil
  end
  opq_top = q[8]
  var_base, var_limit = q[9], q[10]
  -- an error unwinds past the decrements in unify/bind1/cut; a nested query
  -- shares its caller's stack, so it continues the caller's count
  seg_depth, seg_count = q[11], q[12]
  -- the import memo references cells that are no longer valid
  if next(import_memo) ~= nil then
    for k in pairs(import_memo) do import_memo[k] = nil end
  end
end

-- full reset (tests / benchmarks only)
function M.reset_all()
  cell_top, var_top, trail_top, cap_top, ch_top = 0, 0, 0, 0, 0
  seg_depth, seg_count = 0, 0
  lock_open, lock_depth = true, 0
  var_base, var_limit = 0, math.huge
  infs = 0
  for h in pairs(contFn) do contFn[h] = nil end
  for h in pairs(contSpill) do contSpill[h] = nil end
  for k in pairs(import_memo) do import_memo[k] = nil end
end

-- expose tops read-only for tests/diagnostics
function M.tops()
  return cell_top, var_top, trail_top, cap_top, ch_top
end

-- stack segments: ever opened, currently nested, counted frames in this one
function M.segments() return seg_total, seg_count, seg_depth end
-- set the segment size / nesting cap (tests); returns the previous values
function M.segment_limits(frames, max)
  local f0, m0 = SEG_FRAMES, SEG_MAX
  SEG_FRAMES, SEG_MAX = frames or f0, max or m0
  return f0, m0
end

-- ---------------------------------------------------------------------------
-- predicate dispatch table (filled by prolog_compile.lua / typecheck_native)
-- ---------------------------------------------------------------------------
M.NativePred = {}

-- A translated predicate calls another by name through NativePred. A name
-- with no native predicate used to be `nil(...)`: a plain Lua error that
-- trap-error turns into an ordinary Shen exception, so a typecheck that hit
-- it simply looked like a failed typecheck (wrong answer, exit 0). Call
-- sites now resolve through MISS, which raises this distinct sentinel; the
-- typecheck entry recognises it and reruns the whole query on the kernel's
-- KL engine (typecheck_native.lua).
local MissMT = { __tostring = function(m)
  return "native prolog: no native predicate " .. tostring(m.name)
end }
function M.native_miss(name)
  error(setmetatable({ name = name }, MissMT), 0)
end
function M.is_native_miss(x) return getmetatable(x) == MissMT end

-- ---------------------------------------------------------------------------
-- install: wiring into the running kernel. Inert until prolog_compile.lua
-- (Phase 2) and typecheck_native.lua (Phase 3) register their overrides.
-- ---------------------------------------------------------------------------
function M.install(P)
  M.P = P
  GLOBALS = P.GLOBALS
  ERRFN = P.ERR
  KEQ = function(x, y) return P.F["="](x, y) end
  for _, mod in ipairs({ "prolog_compile", "typecheck_native" }) do
    local ok, m = pcall(require, mod)
    if ok then
      m.install(P, M)
    elseif not tostring(m):find("module '" .. mod .. "' not found", 1, true) then
      error(m)
    end
  end
end

return M