commit 17179a4c821d04b16c76684557f0b069d1a9e8bf
parent 34fcf78b10ce2bb4532c8a2ac8d1fd5a453a7b52
Author: James Eversole <james@eversole.co>
Date: Fri, 16 Oct 2026 21:08:13 -0500
Use direct outer constructor dispatch in stable pattern lowering
Keep optimized and sequential fallback representations unchanged. Candidate controls cover direct-tree targets, ordered/partial demand, scoped captures and fully constructed closed-divergence guards. Prepare an authenticated transition worker for the agreed single Haskell generation review gate; compiler acceptance and publication remain pending.
Diffstat:
6 files changed, 107 insertions(+), 18 deletions(-)
diff --git a/docs/validation.md b/docs/validation.md
@@ -759,6 +759,7 @@ incomplete. These probes neither generate compilers nor publish fixtures.
```sh
python3 test/pattern_lowering.py result/bin/tricu \
+ --reference-unit "$RETAINED_SOURCE_UNIT_BUNDLE" \
--directory /tmp/tricu-pattern-candidate
```
@@ -772,9 +773,19 @@ The Haskell control driver is compiled through Nix. Checks reuse the 75-case
independent equation corpus, exercise constructor/equality workloads on finite
and poisoned inputs, and verify split-column ordering, nested failure, unreached
pins and whole-child captures. Two exact code-generation targets compare ordinary
-equations with independently authored delayed dispatchers; the retained compiler
+equations with independently authored direct dispatchers; the retained compiler
must fail those optimization targets. Non-pattern controls must retain their
-original trees. The existing 46-case local-control suite also runs on the candidate.
+original trees. Optimized-backend function trees must also remain identical;
+stable function construction must tolerate unselected closed divergence while
+application to the divergent branch must not return. The existing 46-case
+local-control suite also runs on the candidate.
+
+Select an authenticated retained `source_unit` bundle with unqualified exports
+for `--reference-unit`; its digest is recorded separately from the shipped
+compiler used to construct the candidate. `--prepare-worker` additionally rebuilds
+all affected consumers through `source_map` and emits a pruned stable transition
+`worker.arboricx`. This is candidate preparation, not a full generation or
+fixed-point acceptance. `--resume` permits diagnostic checkpoint reuse only.
Fresh-process cost probes interleave reference/candidate executions, discard a
warmup, and retain three samples per role. Identical explicit recursion and full
diff --git a/lib/source/pattern.tri b/lib/source/pattern.tri
@@ -118,6 +118,12 @@ spBody node ctx = (let rec
spCase leaf stem fork value = (spApp4 (spLit spSelect)
(spLam (spShift leaf)) (spLam stem) (spLam (spLam fork)) value)
+-- Stable abstraction keeps applications residual beneath the argument binders.
+-- Only the factored outer split uses this direct selector. Nested tests and
+-- sequential failures retain spCase/spIf and their continuation protocol.
+-- Leaf has no extra binder here, so do NOT shift its body as spCase does.
+spDirectCase leaf stem fork value = (spApp4 (spLit triage)
+ leaf (spLam stem) (spLam (spLam fork)) value)
spIf yes no condition = (spApp3 (spLit lazyBool)
(spLam (spShift yes)) (spLam (spShift no)) condition)
@@ -223,18 +229,18 @@ spKnownEquations equations column children ctx = (lazyList (_ : spLit t)
(spShiftContext ctx) (snd equation) (spApp (spVar 0) (spLit t))))
(spLam (spShift (spKnownEquations rest column children ctx))))
(spKnownRowIrrefutable (fst equation) column)) equations)
-spSplitEquations equations column ctx = (let
+spSplitEquationsWith select equations column ctx = (let
rows kind = filter (equation : spRootAccepts kind (nth column (fst equation))) equations
stemCtx = spShiftContext ctx
forkCtx = spShiftContext stemCtx
- in spCase
+ in select
(spKnownEquations (rows 1) column [] ctx)
(spKnownEquations (rows 2) column [(spVar 0)] stemCtx)
(spKnownEquations (rows 3) column [(spVar 1) (spVar 0)] forkCtx)
(nth column (spPending ctx)))
-spEquations equations ctx = (lazyMaybe
+spEquationsWith select equations ctx = (lazyMaybe
(_ : spSequentialEquations equations ctx)
- (column : spSplitEquations equations column ctx)
+ (column : spSplitEquationsWith select equations column ctx)
(spFindSplit equations (fst (fst equations)) 0))
spWrap patterns body = (lazyList (_ : body)
(_ rest : spLam (spWrap rest body)) patterns)
@@ -287,7 +293,7 @@ spValidateEquations equations arity = (lazyList
(sourceCoreStart (snd equation))) t)
(equal? (length (fst equation)) arity)) equations)
-sourceLowerEquations equations = (lazyList
+sourceLowerEquationsWith select equations = (lazyList
(_ : err (spDiagnostic "nonempty equations" t t) t)
(first rest : let patterns = fst first in
let arity = length patterns in
@@ -296,7 +302,11 @@ sourceLowerEquations equations = (lazyList
(sourceCoreStart (snd first))) t)
(_ : lazyResult (problem tail : err problem tail)
(_ tail : ok (spWrap patterns
- (spEquations equations (spContext patterns t (spArguments patterns)))) t)
+ (spEquationsWith select equations (spContext patterns t (spArguments patterns)))) t)
(spValidateEquations equations arity))
(isZero_? arity)) equations)
+
+-- Selection is explicit; the optimized backend retains delayed construction.
+sourceLowerEquations = sourceLowerEquationsWith spCase
+sourceLowerStableEquations = sourceLowerEquationsWith spDirectCase
diff --git a/lib/source/resolve.tri b/lib/source/resolve.tri
@@ -157,15 +157,17 @@ sourceResolveEquation resolve equation binders environment = (lazyResult
(append (reverse (sourceEquationCollect (fst equation) sourceEquationCaptures)) binders)
environment))
(sourceResolveElements (fst equation) sourceResolvePattern binders environment))
-sourceResolveEquations resolve node binders environment = (lazyResult
+sourceResolveEquationsWith lower resolve node binders environment = (lazyResult
(diagnostic remainder : err diagnostic remainder)
(_ unused : lazyResult (diagnostic remainder : err diagnostic remainder)
(equations unused : lazyResult (diagnostic remainder : err diagnostic remainder)
(core unused : ok (sourceCoreWithSpan core (sourceAstStart node) (sourceAstEnd node)) t)
- (sourceLowerEquations equations))
+ (lower equations))
(sourceResolveElements (sourceAstPayload node) (sourceResolveEquation resolve) binders environment))
(sourceEquationCheckGroup node))
+sourceResolveEquations = sourceResolveEquationsWith sourceLowerEquations
+
sourceResolveOrdinary resolve node binders environment = (case sourceAstKind node of
^sourceAstLeafKind = ok (sourceCoreLeaf (sourceAstStart node) (sourceAstEnd node)) t
^sourceAstNameKind = sourceResolveName node binders environment
@@ -222,3 +224,14 @@ sourceResolve node binders environment = (case sourceAstKind node of
^sourceAstCaseKind = sourceResolveCase sourceResolve node binders environment
^sourceAstRecKind = sourceResolveRec sourceResolve node binders environment
_ = sourceResolveOrdinary sourceResolve node binders environment)
+
+-- Keep the ordinary visitor/backend unchanged. The stable visitor intercepts
+-- equation groups, including those reached through local/case/recursive bodies;
+-- all other resolution, lexical scope and diagnostic ordering are shared.
+sourceResolveStable node binders environment = (case sourceAstKind node of
+ ^sourceAstCaseKind = sourceResolveCase sourceResolveStable node binders environment
+ ^sourceAstRecKind = sourceResolveRec sourceResolveStable node binders environment
+ ^sourceAstEquationsKind = sourceResolveEquationsWith sourceLowerStableEquations
+ sourceResolveStable node binders environment
+ _ = sourceResolveOrdinary sourceResolveStable node binders environment)
+resolveStableGateAst environment node = sourceResolveStable node t environment
diff --git a/lib/source/stable.tri b/lib/source/stable.tri
@@ -109,7 +109,7 @@ orderStableProgram environment program = (stableBind
(definitions : orderGateProgram environment (pair definitions (sourceProgramFinal program))))
sourceCompileStableDefinition environment definition = (let recursive = sourceDefinitionSelfRecursive definition in
- stableBind (resolveGateAst environment (lazyBool
+ stableBind (resolveStableGateAst environment (lazyBool
(_ : sourceRecursiveBody definition) (_ : sourceDefinitionBody definition) recursive))
(core : stableBind (stableCompileCore core)
(tree : ok (lazyBool (_ : stableFix tree) (_ : tree) recursive) t)))
diff --git a/test/PatternLowering.hs b/test/PatternLowering.hs
@@ -14,6 +14,7 @@ import Control.Exception
import System.Directory
import Data.List (isSuffixOf,isPrefixOf)
import System.Environment
+import System.Timeout (timeout)
load path = do
bytes <- BS.readFile path
@@ -36,8 +37,9 @@ main = do
[directory] <- getArgs
candidate <- load(directory++"/source_unit.arboricx")
reference <- load "test/fixtures/compiler-library.arboricx"
+ retained <- load(directory++"/reference-unit.arboricx")
let unit = candidate Map.! "compileStableModuleDefinitions"
- old = reference Map.! "source_unit.compileStableModuleDefinitions"
+ old = retained Map.! "compileStableModuleDefinitions"
helpers = ofList [Fork (ofString (drop (length prefix) name)) term | (name,term)<-Map.toList reference, prefix<-["prelude.","parser."],prefix `isPrefixOf` name]
oracle source = bindings (compile old helpers ("main = "++source)) Map.! "main"
corpusBytes <- BS.readFile(directory++"/equations.json")
@@ -97,10 +99,10 @@ main = do
putStrLn("program "++file++": finite/demand controls passed")
-- Independent code-generation targets: ordinary readable equations must now
- -- construct the same tree as the hand-written delayed dispatcher. The retained
+ -- construct the same tree as the hand-written direct dispatcher. The retained
-- compiler must fail that target, rather than being a vacuous semantic control.
let canonical tree = encodeBundle <$> buildBundleShared [("root",tree)]
- forM_ [("copy-equations","copy-delayed"),("pick-equations","pick-delayed")] $ \(authored,manual) -> do
+ forM_ [("copy-equations","copy-triage"),("pick-equations","pick-triage")] $ \(authored,manual) -> do
fresh <- load(output++"/"++authored++".arboricx") >>= canonical . (Map.! "main")
wanted <- load(baseline++"/"++manual++".arboricx") >>= canonical . (Map.! "main")
previous <- load(baseline++"/"++authored++".arboricx") >>= canonical . (Map.! "main")
@@ -109,7 +111,7 @@ main = do
fresh <- load(output++"/"++name++".arboricx") >>= canonical . (Map.! "main")
previous <- load(baseline++"/"++name++".arboricx") >>= canonical . (Map.! "main")
unless(fresh==previous)(error("non-pattern control changed: "++name))
- putStrLn "exact delayed-dispatch targets, wrong-compiler and unchanged-control checks passed"
+ putStrLn "exact direct-dispatch targets, wrong-compiler and unchanged-control checks passed"
let function source = do
let term=bindings(compile unit Leaf source) Map.! "main"
forceTreeShared term
@@ -133,3 +135,38 @@ main = do
Fork first _ | first==ofNumber 23 -> pure ()
_->error "known constructor lost whole-child capture"
putStrLn "split-column, nested-failure, pin and whole-capture demand controls passed"
+
+ -- Ineligible splits must retain the old sequential representation exactly.
+ forM_ ["wanted = t\nmain ^wanted = t t\nmain _ = t",
+ "main whole{t} = t t\nmain _ = t",
+ "main 23 = t t\nmain _ = t",
+ "main _ t = t\nmain (t _) _ = t t\nmain _ _ = t t t"] $ \source -> do
+ fresh <- canonical (bindings(compile unit Leaf source) Map.! "main")
+ previous <- canonical (bindings(compile old Leaf source) Map.! "main")
+ unless(fresh==previous)(error "sequential fallback representation changed")
+ putStrLn "sequential fallback identity controls passed"
+ -- Stable-only change: ordinary optimized lowering retains exact function
+ -- trees. Avoid its known closed-recursion construction hazard in this control.
+ forM_ ["main t = t\nmain (t _) = t t\nmain _ = t t t",
+ "main x = case x of\n (t a b) = a\n _ = t",
+ "main x = let\n f t = x\n f _ = t\n in f x"] $ \source -> do
+ let fresh = bindings(compile (candidate Map.! "compileModuleDefinitions") Leaf source) Map.! "main"
+ previous = bindings(compile (retained Map.! "compileModuleDefinitions") Leaf source) Map.! "main"
+ a <- canonical fresh
+ b <- canonical previous
+ unless(a==b)(error "optimized representation changed")
+ -- Fully publishing a function must not execute a closed divergent branch.
+ -- Both direct top-level matching and a local case exercise stable routing.
+ forM_ ["spin x = spin x\nmain t = spin t\nmain other = other",
+ "spin x = spin x\nmain input = case input of\n t = spin t\n other = other",
+ "spin x = spin x\nmain input = let\n f t = spin t\n f other = other\n in f input"] $ \source -> do
+ term <- function source
+ unless(apply term (Stem Leaf)==Stem Leaf)(error "unselected closed divergence")
+ case apply term (Stem poison) of
+ Stem _ -> pure ()
+ _ -> error "guard inspected ignored child"
+ negative <- timeout 200000 (evaluate (apply term Leaf))
+ case negative of
+ Nothing -> pure ()
+ Just _ -> error "demanded divergent branch returned"
+ putStrLn "optimized identity and stable closed-divergence construction controls passed"
diff --git a/test/pattern_lowering.py b/test/pattern_lowering.py
@@ -128,13 +128,19 @@ def main():
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument('tricu', type=Path)
parser.add_argument('--directory', type=Path, required=True)
+ parser.add_argument('--reference-unit', type=Path, required=True,
+ help='explicit retained source_unit bundle (unqualified exports)')
parser.add_argument('--resume', action='store_true', help='diagnostic checkpoint reuse, not fresh-generation acceptance')
parser.add_argument('--skip-costs', action='store_true')
+ parser.add_argument('--prepare-worker', action='store_true',
+ help='also rebuild affected map-builder consumers for an explicit transition worker')
args = parser.parse_args()
root, host = args.directory.resolve(), args.tricu.resolve()
root.mkdir(parents=True, exist_ok=args.resume)
workspace, store = root / 'workspace', root / 'store'
workspace.mkdir(exist_ok=args.resume)
+ # Do not inherit a parent checkout map when the probe lives under it.
+ (workspace / "tricu.workspace").write_text("tricu.workspace.v1\n")
metadata = verify_compiler()
rows = {row[2]: row for row in verify(ROOT / 'test/fixtures')}
report = dict(complete=False, resumed=args.resume, compiler_sha256=metadata['sha256'],
@@ -175,7 +181,7 @@ def main():
for dep in entries[alias][1]:
visit(dep)
needed.append(alias)
- visit('source_unit')
+ visit('source_map' if args.prepare_worker else 'source_unit')
affected = {'source_pattern'}
for alias in needed:
if any(dep in affected for dep in entries[alias][1]):
@@ -188,6 +194,10 @@ def main():
report['sources'][alias] = sha(data)
if alias not in affected:
assert snapshot_bytes(ROOT / 'test/fixtures', rows[alias][4]) == data, ('stale reuse', alias)
+ reference = root / 'reference-unit.arboricx'
+ reference.write_bytes(args.reference_unit.read_bytes())
+ imported(reference) # authenticate the explicitly selected reference bundle
+ report['reference_unit_sha256'] = sha(reference.read_bytes())
tool = imported(ROOT / metadata['bundle'])
payload = (store / 'objects' / tool[:3] / tool).read_bytes()
assert digest('arboricx.module-manifest.v1', payload) == tool
@@ -212,6 +222,16 @@ def main():
subject = root / 'source_unit.arboricx'
run(['compile', '--file', workspace / 'source_unit.tri', '--toolchain', tool,
'--tool-store', store, '--store', store, '--output', subject, '--compile-timeout', '600'], 630)
+ if args.prepare_worker:
+ full_worker = root / 'source_map.arboricx'
+ run(['compile', '--file', workspace / 'source_map.tri', '--toolchain', tool,
+ '--tool-store', store, '--store', store, '--output', full_worker,
+ '--compile-timeout', '600'], 630)
+ worker = root / 'worker.arboricx'
+ merge_bundles(worker, [(full_worker, [('sourceMapBuildStable', 'sourceMapBuildStable')])],
+ prune_unreachable=True)
+ imported(worker)
+ report['worker_sha256'] = sha(worker.read_bytes())
report['modules'] = audit(workspace, store, producer, report['reused'])
assert imported(subject) == report['modules']['source_unit']['manifest'], 'tested/published unit mismatch'
report['candidate_sha256'] = sha(subject.read_bytes())
@@ -294,8 +314,6 @@ def cost_probes(root, run, imported, report, save):
# oracles for these exact sources have already run in the Haskell driver.
from stable_bundle import byte_tree
reference = root / 'reference-unit.arboricx'
- merge_bundles(reference, [(ROOT / 'test/fixtures/compiler-library.arboricx',
- [('source_unit.compileStableModuleDefinitions', 'compileStableModuleDefinitions')])], prune_unreachable=True)
compilers = {'reference': imported(reference), 'candidate': imported(root / 'source_unit.arboricx')}
environment = root / 'empty-environment.tree'
environment.write_bytes(b'\0')
