-- SPDX-FileCopyrightText: This work was generated by Claude Opus 4.8 in 2026.
--
-- SPDX-License-Identifier: LicenseRef-No-Human-Authorship
module Language.Burro.TCProof.TM2Kondey where
import Data.List (nub, sortOn)
import Language.Turmac.Model
import Language.Turmac.IR
import Language.Turmac.IRCompiler
import Language.Turmac.Analyzer (checkDeterministic)
import Language.Turmac.Normalizer (normalizeRules)
--
-- Translating Turing machines to Kondey
-- =====================================
--
-- Each simulated TM tape cell is represented by a contiguous run of Burro
-- tape cells, a "CellStruct":
--
-- state | tmps_1 .. tmps_n | cell | tmpc_1 .. tmpc_m | carry
--
-- where n = the number of TM states and m = the number of TM symbols.
-- `state` and `cell` hold the TM's local state and tape symbol as *even*
-- integers at rest (they are bumped odd only transiently, while being
-- tested); `tmps`/`tmpc` are scratch cells consumed by the cascading
-- conditional idiom (see Tests.md's "Using and Re-using the idiom"
-- section) when dispatching on state/symbol; `carry` is a relay cell,
-- explained below. A blank (all-zero) run of Burro cells is a valid,
-- ready-to-use CellStruct: state 0, symbol 0. This is why the TM must
-- start in state 0 with a blank tape of 0s: no initialization is needed.
--
-- The current CellStruct is whichever one the Burro tape head is inside;
-- there is no other marker for "where" the TM head is. One execution of
-- the generated Kondey program simulates one step of the TM; the halt
-- flag is toggled to keep Burro's own repetition mechanism looping for
-- as long as the TM has not reached its halt state.
--
-- Why the move must be pulled out of the (state, symbol) dispatch
-- ---------------------------------------------------------------
--
-- The obvious way to write this compiler is: dispatch on `state`, then
-- (inside that) dispatch on `cell`, and inside *that* leaf, move to the
-- adjacent CellStruct and write the new state there. That does not work,
-- because it conflicts with how Kondey's `{a/b/c/...}` conditional
-- (`Language.Kondey.Compiler.genCond`) is built out of Burro's `Test`.
--
-- `Test thn els` (`Language.Burro.Definition`'s `exec (Test thn els)`)
-- reads the current cell, negates it onto a stack cell, runs whichever
-- branch matched, and then swaps a value back onto the tape at wherever
-- the tape head *physically ends up* after the branch runs, not at the
-- cell it started from. `genCond`'s extensible n-way conditional dispatches
-- by a *cascade* of these `Test`s that walks rightward, each `Test` leaving
-- a "work value" in the next scratch cell for the following `Test` to read.
-- This only works if every branch's payload is position-preserving
-- (net-zero head movement): a displacing branch would leave the head at
-- the wrong cell for the rest of the cascade to read, spuriously firing
-- later branches. So no leaf of an `{...}` dispatch may move the head.
--
-- (This also rules out doing the n-way dispatch with a hand-built tree of
-- *nested* raw `Test`s -- an earlier version of this module tried that.
-- Inside a `Test` branch the pivot cell always reads 0, because the swap
-- above replaces it with a fresh stack cell, so a nested `Test` cannot
-- re-read the value it is dispatching on and cannot distinguish more than
-- two cases. Only the sequential, work-value-walking `{...}` cascade can.)
--
-- The design
-- ----------
--
-- All per-transition work is done *inside* the position-preserving nested
-- `{state}{symbol}` dispatch (`compilePhase1State`/`compilePhase1Symbol`),
-- which reaches the exact (state, symbol) leaf. There, with the head parked
-- on `cell`, every action is net-zero head movement:
--
-- * write the new symbol into `cell` (a plain delta -- safe because the
-- enclosing `Test` freshly resets `cell` to 0 before the leaf runs);
-- * reach over to the *destination* CellStruct's `state` cell (one whole
-- CellStruct to the left or right, depending on the move direction),
-- write the new state there, and reach back (net-zero, and safe because
-- an unoccupied CellStruct always has state 0);
-- * write the move direction (+1 / -1) into `carry`, reaching there and
-- back;
-- * toggle the halt flag (`!`) to keep looping -- unless the transition
-- goes to the halt state, in which case leave it alone so Burro stops.
--
-- Because `genCond` undoes every fired-but-not-last branch via the exact
-- `inverse` of its own generated code (Burro's group property), all of
-- these writes -- to `cell`, to the destination, to `carry`, and the halt
-- toggle -- collapse to exactly those of the single leaf that logically
-- fires, however the branches differ.
--
-- The one genuinely displacing action per TM step -- moving the head to
-- the adjacent CellStruct -- is then done as the very last thing, by a
-- single *2-way* raw `Test` on `carry` (`phase2Move`): the `then` side (of
-- a positive `carry`) moves right one CellStruct, the `else` side (negative)
-- moves left one. A 2-way `Test` needs no re-reading of its pivot, so the
-- masking problem above does not arise, and being the final, un-chained
-- action, its head displacement is harmless. As a bonus, a displacing
-- `Test` leaves its pivot (`carry`) reset to 0 for the next iteration,
-- because its swap-back lands at the destination, not back on `carry`.
--
-- Each branch of that final `Test` deliberately overshoots its target
-- `state` cell by one (onto a scratch cell of the destination CellStruct),
-- so that the `Test`'s own swap-back clobbers that scratch cell instead of
-- the state we just wrote; `compileToKondey` then takes one uniform step
-- back to land on the destination `state`.
--
----------------------
-- Helper functions --
----------------------
haltState = "@H"
intercalate i [] = []
intercalate i [last] = last
intercalate i (first:rest) = first ++ i ++ (intercalate i rest)
--
-- Note: we "scale up" all the state IDs and symbols, so that they are all
-- either even numbers (0, 2, 4) when they are stored on the tape, and
-- odd numbers (1, 3, 5, ...) when we are executing conditionals on them,
-- so that they match what the conditional idiom used in Kondey expects.
--
scaleUpEven s = (read s :: Int) * 2
--
-- Given a TM description, return the number of distinct states it defines.
--
countStates :: [TMRule] -> Int
countStates rules =
let
currentStates = [s | (s, _, _, _, _) <- rules]
nextStates = [s | (_, _, _, s, _) <- rules, s /= haltState]
allStates = nub $ currentStates ++ nextStates
in
length allStates
--
-- Given a TM description, return the number of distinct symbols it defines.
--
countSymbols :: [TMRule] -> Int
countSymbols rules =
let
readSymbols = [sym | (_, sym, _, _, _) <- rules]
writeSymbols = [sym | (_, _, sym, _, _) <- rules]
allSymbols = nub $ readSymbols ++ writeSymbols
in
length allSymbols
--
-- Generate a `{a/b/c/...}` conditional branch (cascading, position-
-- preserving branches only -- see the discussion above).
--
genCond branches =
"{" ++ (intercalate "/" branches) ++ "}"
--
-- Write an integer value in Kondey by generating +/- sequences.
--
writeKondeyDelta :: Int -> String
writeKondeyDelta n
| n == 0 = ""
| n > 0 = replicate n '+'
| otherwise = replicate (abs n) '-'
--
-- CellStruct offsets, all measured in Burro cells from the `state` cell
-- of a CellStruct, which is offset 0. See the discussion above for the
-- layout: state | tmps_1..tmps_n | cell | tmpc_1..tmpc_m | carry
--
cellOffset :: Int -> Int
cellOffset numStates = numStates + 1
carryOffset :: Int -> Int -> Int
carryOffset numStates numSymbols = numStates + numSymbols + 2
cellStructSize :: Int -> Int -> Int
cellStructSize numStates numSymbols = numStates + numSymbols + 3
------------------------
-- Compiler functions --
------------------------
compileToKondey :: [TMRule] -> String
compileToKondey tmRules =
let
(Right tmRules') = checkDeterministic tmRules
tmRules'' = normalizeRules tmRules'
(Program (CondState states0)) = buildProgram tmRules''
--
-- The cascading `{...}` dispatch fires branch *index* q for a pivot
-- holding value 2q+1, so branch i must handle the state whose
-- normalized value is i. buildProgram lists states in rule-appearance
-- order, which need not be value order; sort so index == value.
--
states = sortOn (\(s, _) -> read s :: Int) states0
numStates = countStates tmRules''
numSymbols = countSymbols tmRules''
in
unlines [
--
-- We start above the "state keeper" part of the current CellStruct.
-- On the tape, this is an even integer (default 0), but for
-- conditionals we need it to be an odd integer, so we bump it up.
--
"+",
--
-- Dispatch on the current state, and (nested inside) on the current
-- symbol, performing all of the transition's work at the matched leaf.
-- Every branch is position-preserving (see compilePhase1State), so this
-- whole `{...}` leaves the head `numStates` cells to the right of, and
-- the `state` cell back at, exactly 0.
--
genCond [compilePhase1State numStates numSymbols stateId stateProg | (stateId, stateProg) <- states],
--
-- Recenter over the outer chain's branches, back to the `state` cell.
-- The cascade displaces the head by one cell per branch, so undo exactly
-- `length states` (the branch count), mirroring the inner cascade's
-- `replicate (length symbols)` recenter in compilePhase1State. (Given the
-- normalizer's precondition this equals numStates, but the branch count is
-- the honest quantity.)
--
replicate (length states) '<',
--
-- Move to `carry`, which the dispatch left holding the move direction
-- (+1 = right, -1 = left), and perform the one displacing action of the
-- step: move the head to the adjacent CellStruct's `state` cell.
--
replicate (carryOffset numStates numSymbols) '>',
phase2Move numStates numSymbols,
--
-- Each branch of phase2Move overshoots its target `state` cell by one
-- so the Test's swap-back clobbers a scratch cell; undo that overshoot
-- here, uniformly, regardless of which way we moved.
--
"<"
]
--
-- Per state: move to `cell`, bump it odd, dispatch on it, then recenter
-- and return to `state`. Net-zero head movement overall, since this is
-- itself one branch of the outer (state) dispatch.
--
compilePhase1State :: Int -> Int -> StateId -> Prog -> String
compilePhase1State numStates numSymbols stateId (CondSymbol symbols0) =
let
--
-- As with the outer state dispatch, the inner `{...}` fires branch
-- index s for a pivot holding 2s+1, so branch i must handle the
-- symbol whose normalized value is i. Sort so index == value.
--
symbols = sortOn (\(s, _) -> read s :: Int) symbols0
in
unlines [
--
-- Move to the `cell` field of the current CellStruct.
--
replicate (cellOffset numStates) '>',
--
-- Bump the cell up, to convert even numbers on the tape (like default
-- 0) to odd numbers that the conditional idiom can work with.
--
"+",
--
-- Dispatch on the current symbol. Every leaf here is also
-- position-preserving (see compilePhase1Symbol).
--
genCond [compilePhase1Symbol numStates numSymbols stateId symbol symProg | (symbol, symProg) <- symbols],
--
-- Recenter (this `{...}` has (length symbols) branches), back to `cell`.
--
replicate (length symbols) '<',
--
-- Move back to `state`.
--
replicate (cellOffset numStates) '<'
]
--
-- Per (state, symbol) leaf, with the head parked on `cell`. Everything
-- here is net-zero head movement (see the discussion above):
-- * write the new symbol into `cell`;
-- * write the new state into the destination CellStruct's `state`;
-- * record the move direction in `carry`;
-- * toggle the halt flag to keep looping, unless we are halting.
--
compilePhase1Symbol :: Int -> Int -> StateId -> Symbol -> Prog -> String
compilePhase1Symbol numStates numSymbols stateId symbol (Seq [WriteMoveGoto newSym dir newStateId]) =
let
toCarry = numSymbols + 1 -- cell -> carry, within the same CellStruct
in
unlines [
writeKondeyDelta (scaleUpEven newSym),
writeNewStateAtDest numStates numSymbols dir newStateId,
replicate toCarry '>',
--
-- Launder `carry` before writing the direction into it. `carry` is
-- not 0 here on the third and subsequent dispatches of a CellStruct:
-- the previous phase2Move's swap-back deposited into it whatever was
-- on the stack at that moment, which (by the mechanics of the outer
-- cascade's final coda) is the *bumped state from two visits ago* --
-- so a plain delta-write of the direction would produce a wrong,
-- always-positive dispatch value (this was a real, once-latent bug:
-- see eg/bouncing-infinite.turmac). The gadget below exploits the
-- other side of the same swap mechanism: a *displacing* Test leaves
-- in its pivot the value swapped in from the current stack cell.
-- Here that stack cell is at depth 2 (inside the state-Test's frame
-- and the symbol-Test's frame), and it is guaranteed to be 0: the
-- stack is cleared at the start of every iteration, and leaves are
-- the only depth-2 Test activity (undone exactly by the cascade's
-- own inverses between branches). The `++` first makes the pivot
-- reliably positive -- the residue is >= -1 in all cases (0 before
-- a first dispatch, an odd bumped-state >= 1 later, or -1 from the
-- arrival overshoot when the CellStruct has a single scratch cell)
-- -- so the `<` branch always fires, displacing the head one cell
-- left onto tmpc_m, whose value provably never matters (it feeds
-- only a dead-end stack cell). Net effect: carry := 0, garbage
-- parked in tmpc_m, head one cell left of carry.
--
"++(</)",
">",
writeKondeyDelta dir,
replicate toCarry '<',
if newStateId == haltState then "" else "!"
]
compilePhase1Symbol _ _ stateId symbol other =
error (
"Unhandled IR node at stateId '" ++ (show stateId) ++ "', " ++
"symbol '" ++ (show symbol) ++ "': (" ++ (show other) ++ ")"
)
--
-- Reach from `cell` to the destination CellStruct's `state` cell (one
-- whole CellStruct away, left or right per the move direction), write the
-- new state there, and reach back -- net-zero head movement. Writing is a
-- plain delta because an unoccupied CellStruct always has state 0. Nothing
-- is written when the transition halts (there is no next state to store,
-- and Burro stops before the destination would ever be read).
--
writeNewStateAtDest :: Int -> Int -> Direction -> StateId -> String
writeNewStateAtDest numStates numSymbols dir newStateId
| newStateId == haltState = ""
| dir == 1 =
replicate toRight '>' ++ writeKondeyDelta (scaleUpEven newStateId) ++ replicate toRight '<'
| otherwise =
replicate toLeft '<' ++ writeKondeyDelta (scaleUpEven newStateId) ++ replicate toLeft '>'
where
toRight = numSymbols + 2 -- cell -> next CellStruct's state
toLeft = 2 * numStates + numSymbols + 4 -- cell -> previous CellStruct's state
--
-- The single displacing action of a TM step: a 2-way Test on `carry`
-- (holding +1 for a rightward move, -1 for a leftward one). `then` moves
-- one CellStruct right, `else` one CellStruct left. Each side overshoots
-- its target `state` cell by one (landing on a scratch cell of the
-- destination) so the Test's swap-back clobbers that scratch cell rather
-- than the state; compileToKondey then steps back by one.
--
phase2Move :: Int -> Int -> String
phase2Move numStates numSymbols =
let
k = cellStructSize numStates numSymbols
in
"(" ++ ">>" ++ "/" ++ replicate (2 * k - 2) '<' ++ ")"