tur/trail
backtrackable state: mutable cells whose writes undo on demand.
A trail records the previous value of every trailed write, so undoing to a mark restores all of them at once. This is the WAM / CLP shape, and it is what a search loop wants instead of threading a persistent structure through every step: a union-find substitution, a bound stack, a domain bitmap.
The design turns on being able to OPT A CELL OUT, at three granularities, because backtracking in a search is asymmetric -- a solver discards the trail above a backjump point but keeps what it learned:
per cell, forever `g-cell-new` never trailed at all per write `with-untrailed` a write that must survive the undo per level `bt-commit-to!` keep this level's writes
BtCell and GCell are DISTINCT TYPES, so opting out is visible in the signature of anything that touches the cell rather than a flag someone forgets to pass.
RE-ENTRY. A captured continuation restores control, not state, so re-entering one lands in a computation whose trail levels are already gone. A mark carries a generation, so bt-undo-to! on such a mark returns false rather than unwinding whichever level now sits at that index. The typed surface mostly prevents the situation outright: Mark, BtCell and GCell have no Clone instance, so a multi-shot cloneable-shift cannot capture one. The generation check is the backstop for a mark laundered through an :int or through inline-C.
Serializing a continuation inside an open scope is refused -- the undo information is process-local and does not travel with the blob.
THE Bt CAPABILITY. Every function here that mutates the trail -- the writes, the marks, the undo/commit, the pause/resume, and the two bracket forms -- carries #fx{Bt}, and Bt is a real ^capability effect declared below, so the row is CHECKED rather than decorative: a caller that declares its own row (#fx{} or any row without Bt) and reaches the trail fails effect-row checking with TUR-E0009, exactly as a #fx{} caller of an FS-tagged function does. A caller with no row annotation is not checked -- the discipline is opt-in, as for every capability tag. The row also vetoes the refinement solver's purity walk: a body it could otherwise prove pure is never congruence-collapsed once it declares Bt, and that veto propagates to every caller the walk reaches.
See docs/guides/backtrackable-state-guide.md, and docs/archive/solver-extension-plan.md sections 3.2-3.5.
Since: SX1 (graduated from --enable=backtrackable-state 2026-08-29)
Bt
(defeffect Bt [] :nil ^capability)
capability tag for mutating the backtracking trail.
Never performed or handled: it annotates a function's authority to write a trailed cell, push or unwind a trail level, or pause trailing. Declared ^capability, so it is justified by its annotation alone (never TUR-W0031) and propagates from a callee's declared row into the caller's inferred row. It is declared HERE rather than in stdlib/effects.tur because this module is autoloaded and effects.tur is not. An effect name that no defeffect declares used to resolve to nothing, silently -- precisely how the annotation was decorative for a month; it is TUR-E0026 now.
nil (never performed; used only as a #fx{Bt} row annotation)
(defn bind-var [c : BtCell v : int] #fx{Bt} : bool (bt-set! c v))
Since: SX1 (checked since 2026-09-05)
Mark
(defopaque Mark :int)
an opaque handle to a trail level.
Carries a generation as well as a level, so undoing to a mark that was already undone or committed is refused rather than unwinding whichever level happens to sit at that index now.
BtCell
(defopaque BtCell :ptr)
a mutable cell whose writes are trailed and undo on backtrack.
GCell
(defopaque GCell :ptr)
a mutable cell that is NEVER trailed.
The per-cell opt-out: activity scores, a learned-clause database, a simplex basis. Its writes are not undoable effects, which is exactly the property those want. A distinct type from BtCell on purpose -- opting out is then visible in the signature of anything that touches the cell, rather than a flag someone forgets to pass.
bt-cell-new
(bt-cell-new [init :int] :BtCell)
allocate a trailed cell holding init.
| init | the cell's starting value |
A BtCell. Release with bt-cell-free.
(bt-get (bt-cell-new 0)) ; => 0
Since: SX1
bt-lvar-new
(bt-lvar-new [unbound :int] :BtCell)
allocate a WRITE-ONCE trailed cell, initially unbound.
The logic-variable shape: it goes from unbound to bound once per level, and undo returns it to unbound. bt-set! refuses a second binding rather than overwriting.
| unbound | the value bt-get reads while the cell is unbound |
A BtCell in the unbound state.
(bt-bound? (bt-lvar-new 0)) ; => false
Since: SX1
bt-cell-free
(bt-cell-free [c :BtCell] :void)
release a cell.
Free cells OUTSIDE the scope whose writes touched them: a trail entry still pointing at a freed cell dangles until the next undo, and the failure then surfaces inside undo rather than here.
| c | the cell |
(bt-cell-free c)
Since: SX1
bt-get
(bt-get [c :BtCell] :int)
read a trailed cell.
| c | the cell |
Its current value.
(bt-get c) ; => 0
Since: SX1
bt-bound?
(bt-bound? [c :BtCell] :bool)
has this write-once cell been bound?
| c | the cell |
true once bound. Always true for a value cell.
(bt-bound? v) ; => false
Since: SX1
bt-set!
(bt-set! [c :BtCell v :int])
write a trailed cell.
Records the previous value only on the FIRST write per level, so a cell written a thousand times inside one level costs one trail entry.
| c | the cell | |
| v | the new value |
true on success; false when c is a write-once cell that is already
bound -- binding twice is a caller bug, not a silent overwrite.
(bt-set! c 42) ; => true
Since: SX1
g-cell-new
(g-cell-new [init :int] :GCell)
allocate a cell that is never trailed.
| init | the starting value |
A GCell. Release with g-cell-free.
(g-get (g-cell-new 7)) ; => 7
Since: SX1
g-cell-free
(g-cell-free [g :GCell] :void)
release a never-trailed cell.
| g | the cell |
(g-cell-free g)
Since: SX1
g-get
(g-get [g :GCell] :int)
read a never-trailed cell.
| g | the cell |
Its current value.
(g-get g) ; => 7
Since: SX1
g-set!
(g-set! [g :GCell v :int])
write a never-trailed cell. The write survives every undo.
Implemented by pausing the trail across the write rather than by a second cell representation: one cell struct, one set of semantics, and the opt-out is the type that reaches it.
| g | the cell | |
| v | the new value |
(g-set! g 7)
Since: SX1
bt-mark
(bt-mark)
push a trail level and return a handle to it.
A Mark. Pass it to bt-undo-to! to restore, or bt-commit-to! to keep.
(let [m (bt-mark)] (bt-set! c 1) (bt-undo-to! m))
Since: SX1
bt-undo-to!
(bt-undo-to! [m :Mark])
restore every trailed write made since m.
| m | a mark from bt-mark |
true on success; false when m is STALE -- already undone, already
committed, or from a level index that has since been reused. A stale undo
is refused rather than performed: it is what a re-entered continuation
produces, and quietly "succeeding" would restore words belonging to some
other level's cells.
(bt-undo-to! m) ; => true
Since: SX1
bt-commit-to!
(bt-commit-to! [m :Mark])
drop the level but KEEP its writes.
The per-level opt-out: Prolog's assert, ASP's "global", promoting a learned fact out of the level that found it.
| m | a mark from bt-mark |
true on success; false when m is stale.
(bt-commit-to! m) ; => true
Since: SX1
bt-level
(bt-level :int)
the current trail level, 0 when no mark is outstanding.
The level depth.
(bt-level) ; => 0
Since: SX1
bt-depth
(bt-depth :int)
how many entries are on the trail right now.
The stamp discipline is only observable as a count, so this is what a test asserting "a thousand writes cost one entry" reads.
The entry count.
(bt-depth) ; => 1
Since: SX1
untrailed-begin
(untrailed-begin)
suspend trailing until the matching untrailed-end.
The per-write opt-out. Writes in between are permanent -- a node counter or statistic that must outlive the search that produced it. Nests.
(untrailed-begin) (bt-set! counter 1) (untrailed-end)
Since: SX1
untrailed-end
(untrailed-end)
resume trailing.
(untrailed-end)
Since: SX1
bt-scope
(bt-scope [A])
run body in a fresh trail level and undo its writes after.
The bracket form of bt-mark / bt-undo-to!. Prefer it: the halves are easy to leave unpaired on an early return, and this cannot be.
| body | a thunk. Taken ^fat, so a capturing lambda works -- which is the | |
| only interesting case, since the body has to reach the cells. |
Whatever body returned. The VALUE survives; the trailed WRITES do not.
Returning something that points into state the scope just undid is the
caller's problem -- this is a search primitive, not a memory-safe region.
(bt-scope (fn [] (do (bt-set! c 99) (bt-get c)))) ; => 99, c restored
TWO THINGS THAT COMPOSE SURPRISINGLY:
1. `bt-commit-to!` inside the body escapes this scope ENTIRELY, not just one level. Commit means "promote to level 0" -- it discards the undo information rather than merging it into the enclosing level -- so a committed write survives every enclosing `bt-scope` too. That is deliberate (it is how a learned clause outlives a backjump), but it is the opposite of what "commit into the parent" suggests to a Prolog ear.
2. A panic inside `body` that is caught by an enclosing `catch-unwind` still undoes: the restore is a `defer`, so it fires on the unwind and the trail is back at the outer level when the catch returns. An UNCAUGHT panic aborts the process, where the undo is moot.
The bt-undo-to! result is discarded: it reports only that the mark was already spent, which inside this bracket means the body undid or committed its own enclosing level -- covered by note 1.
Carries #fx{Bt} itself (it pushes and unwinds a level); body is deliberately left without a declared row, so a body that also prints or performs its own effects is not rejected at the bracket.
Since: SX2
with-untrailed
(with-untrailed [A])
run body with trailing PAUSED, then resume.
The bracket form of untrailed-begin / untrailed-end, and the per-write opt-out: writes made inside are not recorded, so they survive an undo that unwinds past this point. Nests -- the pause is a depth counter, not a flag.
| body | a thunk, taken ^fat so it can capture the cells it writes. |
Whatever body returned.
(let [m (bt-mark)] (with-untrailed (fn [] (bt-set! c 7))) (bt-undo-to! m) (bt-get c)) ; => 7, not restored
Panic-safe the same way bt-scope is: the resume is a defer, so a panic inside body caught by an enclosing catch-unwind unwinds through it and trailing is back on -- later writes stay undoable.
Since: SX2
trail-reset!
(trail-reset!)
drop every level and entry WITHOUT running undo.
Teardown and tests only; not part of the search protocol.
(trail-reset!)
Since: SX1
Internal definitions
trail/autolink-hint-- internal marker that triggers trail.c compilation in tur build/run.