Using deep6

Using deep6

yopl is the most demanding consumer of deep6 in the fleet. The solver and rule library together exercise every non-trivial deep6 surface: speculative Env push/pop under backtracking, fresh Variable creation under deep recursion, in-place unification, the _ wildcard, runtime isVariable guards, and result extraction via assemble.

If you're building your own deep6-based engine, or writing a custom predicate in yopl that calls deep6 directly, this page is the worked baseline. Every section names the pattern, points at the yopl source where it appears, and flags the common bugs.

For the deep6 API itself, see the deep6 README. This page is yopl-side how-to.

Imports

import {EnvMap} from 'deep6/env-map.js';
import {_, isVariable, variable} from 'deep6/env.js';
import unify, {open, soft} from 'deep6/unify.js';
import assemble from 'deep6/traverse/assemble.js';

Six imports cover the entire surface yopl exercises. EnvMap is the value-model implementation yopl uses (deep6 1.3.1+); the older Env is still exported by deep6 but yopl no longer uses it.

1. Env lifecycle — speculative bindings under backtracking

The proof loop in src/solve.js allocates one root env and reuses it for the entire query by treating it as a stack of binding frames.

const env = new EnvMap();
env.options.openObjects = true;

// before trying a rule clause:
env.push();

if (unify(headArgs, callArgs, env)) {
  // success: env now has new bindings on top frame
  // proceed deeper
} else {
  env.pop(); // failure: discard the frame, bindings vanish
}

push() snapshots the current binding set; pop() restores it. This is the load-bearing trick that lets the explicit-stack proof loop do backtracking by simply popping a frame — there's no separate "trail" structure, no copy-on-write, no diff. Unification can mutate env freely between matching push/pop pairs because pop reverts.

env.options is a per-call options bag (matching modes for objects, arrays, maps, sets — openObjects, openArrays, openMaps, openSets, loose, circular, ignoreFunctions, signedZero, symbols). yopl sets openObjects: true at root so object literals match subset-style by default. Per-call overrides are handled by unifyOpts in rules/system.js, which saves and restores env.options around the unify call.

Direct binding (no unification) is available via env.bindVal(name, value). yopl uses it to bind the synthetic "call frame" variable that meta-predicates like cut and halt need to walk back up the stack — see src/solve.js:38.

Common bug: forgetting env.pop() after a failed unify. The discarded bindings will pollute the next attempt and produce wrong answers, not crashes. yopl owns the correct sequencing in src/solve.js; user-written inline goals (${({X}) => env => ...}) must not call env.push() themselves — the proof loop has already framed the call.

2. Variable creation — Symbol names under deep recursion

Each rule clause is invoked with a fresh batch of logical variables. yopl mints them with Symbol-typed names:

let counter = 0;
const generateVariables = count => {
  const vars = new Array(count);
  for (let i = 0; i < count; ++i) vars[i] = variable(Symbol(counter++));
  return vars;
};

(src/solve.js, same shape in all four solvers under src/solvers/.)

Why Symbol and not string? A recursive proof tree can instantiate the same clause many times concurrently on the stack — member(X, [_|T]) :- member(X, T). walking a 100-element list has 100 live activations, each with its own X and T. A naïve string-name scheme ('X', 'T') would collide across activations and produce wrong bindings. Symbol(counter++) guarantees uniqueness; the monotonic counter is just for debugger readability.

The IR-level Var('X') you write in source code is not the same object as a runtime Variable — lower.js converts each named IR Var into a positional parameter of the generated rule function. At call time, generateVariables passes fresh variable(Symbol(N)) instances; the rule function closes over them as its lexical scope.

For ad-hoc fragments outside the compiler — e.g., assembling test inputs by hand — call variable() (no arg) for a Symbol()-named fresh var, or variable('Name') for a string name. Symbol names are safer in production code; string names read better in tests where you assemble against them.

3. Variable inspection inside inline goals

Inline JS goals (${({X, Y}) => env => ...}) receive their parameter binding through the rule-function call site and access deep6 vars via the captured names. Three operations are common:

// Is the variable bound?
X.isBound(env)

// Get its bound value (deref through any chained bindings)
X.get(env)

// Runtime check on an arbitrary term (after a get, for example)
isVariable(x)

Pattern: forward-mode predicates verify their inputs are bound, fail otherwise.

rule('isArray', 1)(clause`(X) :- ${({X}) => env =>
  X.isBound(env) && Array.isArray(X.get(env))
}`)

(src/rules/native.js.)

Bidirectional predicates branch on which side is bound (the arrayList rule in src/rules/native.js is the canonical pattern — array→cons when A is bound, cons→array when L is bound, both unbound → fail).

isVariable(x) checks whether x is itself a deep6 Variable instance (not whether some named variable is bound). yopl uses it inside list-walk loops where a cons cell's next might be null, a value, or another unbound Variable (open tail) — see arrayList in src/rules/native.js.

4. Unification — in-place, side-effecting

unify(a, b, env) is the central operation. It returns a truthy value (the same env) on success and false on failure, and mutates env in place — successful bindings land on whatever frame is currently on top.

import {unify} from 'deep6/unify.js';

env.push();
const ok = unify(L, cell, env);
if (ok) {
  // bindings landed on the new frame
  return true;
}
env.pop();
return false;

The contract is "caller frames the call." If you don't push() before, successful bindings land on whatever frame is current and persist past your call — your caller has to revert them, but it doesn't know they exist. If you do push() but forget pop() on failure, the empty frame leaks until the next outer pop cleans it up.

For inline goals invoking unify directly (the native.js rules do this in their JS handlers), yopl's proof loop has already done the push — return truthy and the loop will eventually pop on backtrack. Return false (failure) and the loop will pop for you too. The handler itself never pushes or pops.

unify is recursive across structure: objects unify field-by-field, arrays element-by-element, cons cells value + next, strings/numbers/booleans by ===. The matching mode for each container kind is read from env.options (so openObjects: true means missing fields in either side are ignored). The open(...) and soft(...) wrappers (see next section) lock the matching mode regardless of env.options.

5. Sentinels — wildcards and subset-matching wrappers

import {_} from 'deep6/env.js';
import {open, soft} from 'deep6/unify.js';

_ is the wildcard sentinel — it unifies with anything and is never bound. yopl re-exports it from yopl/compile so IR construction can splice it without an extra import. Each _ in compiled source lowers to a fresh variable() (since 2026-05-10) — matching ISO Prolog "anonymous variable" semantics, where two _ in the same clause are not the same variable.

open({tag: 'a'}) wraps a value to lock subset-matching regardless of env.options.openObjects. Useful when the surrounding env has open-objects off but a specific term needs it on (e.g., a meta-predicate that intentionally accepts objects with extra fields).

soft(x) flips the open/closed mode for a single term — opposite of open if the env is closed-by-default, etc. Both are pass-through under the Lit-walker — if you embed them in compiled IR via ${Lit(open({...}))}, lowering preserves the wrapper.

6. Result extraction — assemble outside the proof loop

import assemble from 'deep6/traverse/assemble.js';

solve(rules, 'member', [X, list], env => {
  console.log('X =', assemble(X, env));
});

assemble(V, env) walks the binding graph from V and returns a fully-materialized JS value — bound variables substituted, cons cells walked, nested objects/arrays/maps/sets reconstructed. The result has no live references back into env.

Use assemble inside a result callback (where bindings are still valid), never after the callback returns — the proof loop will have pop()ed by then.

For partial inspection inside an inline goal, V.get(env) returns the immediate binding (one level of deref); assemble walks the whole graph. Prefer get in hot paths; reach for assemble only when you actually need the materialized structure.

Common bugs

These are the ones yopl's own development hit; flagged so you can avoid them:

• Mutating env.options without saving/restoring. A predicate that flips openObjects and doesn't restore breaks every later unify on the same branch. yopl's unifyOpts predicate in src/rules/system.js is the template — clone env.options, set the override, run the unify, restore the original. The env's frame stack doesn't capture options.
• Returning env from an inline goal instead of true. The proof loop treats the return value as a control signal — truthy = succeed, false = fail, null = succeed-but-no-new-goals. Returning env is truthy, so it works most of the time, but the loop's discriminator on newGoals (whether to push sub-goals onto the stack) gets confused. Return true for "this inline goal succeeded, continue with the next body goal."
• Calling unify outside an env.push() / env.pop() frame. Bindings leak into the outer frame and survive past the predicate's failure. Only happens in user-authored predicates — the proof loop frames its own unify calls. If you're writing an inline goal that calls unify directly (as arrayList does), the proof loop has already framed you — return truthy/falsy, don't push/pop yourself.
• isVariable(x) vs x.isBound(env). isVariable(x) checks the type of x; x.isBound(env) checks whether a specific Variable has a binding in this env. Two different questions — use the right one. Walking a cons list typically needs isVariable(cell) (is this slot a hole?) followed by cell.isBound(env) (is the hole filled?).
• Forgetting that unification can succeed without binding anything. unify(3, 3, env) returns truthy and changes nothing in env. Predicates that "post-check" by reading env need to assemble the actual term, not check .isBound of an input.

Where these patterns appear in yopl

Pattern	Files
Env lifecycle (push/pop loop)	src/solve.js, src/solvers/{async,asyncGen,gen}.js
Variable creation under recursion	generateVariables in all four solvers
Variable inspection inline	src/rules/{system,comp,math,bits,logic,native}.js
Unify entry from inline goal	src/rules/native.js (arrayList, arrayGet, arraySet, arrayLength, etc.)
_ wildcard in IR	Re-exported by src/compile/ir.js; lowered in src/compile/lower.js
open / soft wrappers	Re-exported by src/compile/ir.js; preserved by the Lit-walker in lower.js
Result extraction	Consumer code in tests/*.js and the solve wiki page examples

See also

• Writing-rules — the hand-written rule encoding that uses these patterns.
• compile-overview — the compiler that lowers IR to these patterns.
• solve — the main entry point that orchestrates the proof loop.
• deep6 on npm — the unification engine.