Compare commits

...

34 Commits

Author SHA1 Message Date
aec83f0aac artdag: Phase 7 consumes lib/maude mau/confluent? (no bespoke confluence checker)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 34s
The CID-stability check now calls mau/confluent? / mau/non-joinable-pairs from
lib/maude/confluence.sx (merged in) instead of re-implementing critical-pair
analysis inside lib/artdag. Picks up confluence.sx via the architecture merge.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 20:20:59 +00:00
7f7957ba25 Merge architecture: pick up lib/maude/confluence.sx (mau/confluent?) 2026-06-07 20:20:29 +00:00
0963aa51c9 Merge loops/maude into architecture: maude confluence/critical-pair checker (mau/confluent?)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 39s
Adds lib/maude/confluence.sx — the CID-stability oracle the artdag optimiser
needs. 274 tests.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 20:19:17 +00:00
2dd4c7d974 maude: confluence / critical-pair checking (12 tests, 274 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 37s
lib/maude/confluence.sx — two-sided syntactic unification (occurs-checked) →
critical pairs from LHS overlaps → joinability via AC-canonical normal forms.
mau/confluent? / mau/non-joinable-pairs / mau/critical-pairs / mau/cp->str.
Catches f(a)=b,a=c (b <?> f(c)); peano/idempotent/AC confirmed confluent.
Syntactic overlaps (AC under-approximated, joinability uses canon). This is
the CID-stability oracle for the artdag optimiser.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 20:18:33 +00:00
3432a72510 artdag: maude-bridge dag<->term adapter + 14 round-trip tests
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 30s
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 20:07:34 +00:00
657d80611a artdag: promote maude-driven optimizer to active Phase 7
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 59s
lib/maude is now on this branch (fast-forwarded to architecture). The fit is
proven (lib/maude/tests/effects.sx). Phase 7 spells out the adapter
(maude-bridge.sx), the optimisation laws as a maude module, equivalence with
optimize.sx, and a syntactic confluence/CID-stability check. maude is a
read-only consumed substrate; gotchas recorded.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 19:58:34 +00:00
5b472025db Merge loops/maude into architecture: maude-on-sx — term rewriting modulo AC
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 56s
Full Maude 3 functional+system core on SX (lib/maude): parser (sorts/subsorts/
overloading/mixfix), equational reduction modulo assoc/comm/id (the chisel),
conditional eqs + owise, system rules (rew + BFS search), strategy language,
META-LEVEL reflection, order-sorted least-sort, mixfix printer, end-to-end
program runner, gather right-assoc. 262 tests, 14 suites. Includes the
artdag-on-sx optimiser fit prototype (effects.sx).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 19:39:59 +00:00
d2f6bf02b3 maude: artdag-on-sx fit prototype — optimise passes as equations (8 tests, 262 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 1m7s
lib/maude/tests/effects.sx — proves artdag's effect-pipeline optimisations
(fusion, no-op/dead-op elim, identity elim, CSE/idempotent dedup) are
equational rewriting: the optimised pipeline is the normal form, confluence
gives a stable content id. The 'second consumer' spike for a maude-driven
optimiser in lib/artdag. Surfaced faithfulness note: id: affects matching/canon
not auto-reduction.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 19:38:50 +00:00
7f264b39da maude: refresh scoreboard
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 28s
2026-06-07 15:51:56 +00:00
fe0d13243a maude: mark roadmap + extensions complete (254/254, saturated)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 38s
Plan: Phase 8 blocked on a 2nd consumer (matching+fire+strategy identified
as extraction candidates); roadmap + 7 extensions done, end-state goal met.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 15:51:11 +00:00
6ea9ecf9a4 maude: run.sx search command + result-sort output (254 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 36s
run.sx now handles 'search START =>* GOAL .' (reports the witness path) and
mau/run-pretty prints Maude-style 'result SORT: TERM' using least-sort
inference. searchpath.sx exposes mau/search-path-terms (term-level entry).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 15:49:45 +00:00
fecd3e4b0d maude: order-sorted least-sort inference (14 tests, 250 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 27s
lib/maude/sorts.sx — mau/term-sort computes the least sort of a term (smallest
result sort among op declarations whose arg sorts the actuals satisfy modulo
subsorting); overloaded f(1)=NzNat vs f(s 0)=Nat. mau/has-sort? for
membership-style checks. Answers the plan's order-sorted substrate question.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 15:46:32 +00:00
3bb4886f0f maude: gather / parse-time associativity for cons lists (7 tests, 236 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 38s
Infix ops parse left (default / gather (E e)) or right (gather (e E)) per the
gather attribute, so _:_ [gather (e E)] reads a : b : c as right-nested. Full
insertion sort now runs over bare cons lists with no parentheses.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 15:44:25 +00:00
cc0f3f1ff7 maude: owise (otherwise) equations (8 tests, 229 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 40s
Parser reads trailing eq attributes (eq L = R [owise] .) via mau/split-attrs.
mau/crewrite-top is two-pass: ordinary equations first, owise last — an owise
catch-all fires only when no ordinary equation applies, regardless of
declaration order. Verified a catch-all declared first still defers.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 15:40:11 +00:00
d09af71f6e maude: witness-path search for puzzle solvers (8 tests, 221 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 34s
lib/maude/searchpath.sx — mau/search-path returns the shortest sequence of
states from start to goal (the solution moves), mau/search-length its step
count. BFS over all one-step successors, threading the path.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 15:36:46 +00:00
ed40af66f5 maude: program runner — module + reduce/rewrite commands (6 tests, 213 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 30s
lib/maude/run.sx — mau/run-program / mau/run parse a module plus trailing
reduce/red/rewrite/rew commands (with optional 'in MOD :' qualifier) and
execute them, rendering results in mixfix surface syntax. An idiomatic
.maude file now runs end-to-end.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 15:34:23 +00:00
8ab36b90bf maude: mixfix surface-syntax printer (11 tests, 207 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 40s
lib/maude/pretty.sx — mau/term->maude renders internal prefix terms back
in Maude mixfix syntax driven by op forms; mau/red->maude / mau/rew->maude
reduce-then-render. Output now reads as idiomatic Maude.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 15:32:20 +00:00
4018671087 maude: Phase 7 reflection / META-LEVEL (18 tests, 196 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 31s
lib/maude/meta.sx — up-term/down-term encode terms as data (mt-var/mt-app),
reflective meta-reduce/meta-rewrite/meta-apply, the meta-circular law
down(metaReduce(up t)) =AC= reduce t, and meta-prove-equal? as a generic
equational theorem helper. Verified round-trips, reflection agreement,
single-rule meta-apply, and proving commutativity/associativity instances.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 15:29:45 +00:00
e2aca38a84 maude: Phase 6 strategy language (19 tests, 178 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 57s
lib/maude/strategy.sx — first-class set-valued strategies: idle/fail/all/
rule/seq/alt/star/plus/bang/name combinators, named-strategy env. Same
rule set computes different things under different strategies; verified
with single-rule vs all vs seq-order vs alt vs star vs bang.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 15:26:52 +00:00
858d35a68c maude: Phase 5 system modules + rewrite rules (21 tests, 159 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 48s
lib/maude/rewrite.sx: rl/crl transitions interleaved with eq normalisation.
mau/rewrite = default strategy (top-down, leftmost-outermost, first rule);
mau/rew bounded; mau/search = BFS reachability over all successors.

lib/maude/fire.sx: short-circuiting matcher (mau/fire-eq) — finds the first
productive match instead of enumerating the whole solution set. Fixes the
exponential blowup of AC rewriting on many identical elements (8 coins:
60s+ to <1s). Eager match-multiset kept only for match-all / search.

Verified on AC coin-change, traffic light, branching search, crl clock.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 15:23:06 +00:00
b74eecfdd3 plans: rose-ash-on-sx migration strategy + radar abstraction backlog (from loops/radar)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 51s
Surgical add of the two radar-authored planning docs onto architecture (both new
files, no conflict). Migration strategy: duplicate->cutover->diverge, strangler edge
+ layer-split shadow-diff, host-trio critical path. abstractions.md is the evidence
base the strategy cites (A1 done, W1/W4/W8 substrate-adoption findings).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 15:09:37 +00:00
1747bbd944 maude: Phase 4 conditional equations (19 tests, 138 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 49s
lib/maude/conditional.sx — condition-aware reducer. ceq fires only when
its guard holds: equational guards (l=r reduce to same normal form) and
boolean guards (term reduces to true), evaluated by recursing through the
same reducer. Verified on gcd, insertion sort, max, even.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 15:06:00 +00:00
768e745076 Merge loops/content into architecture: content-on-sx hardening — tree-wide content/find+has?, tree-wide revision diff, find-replace across all text-bearing fields, in-document prose search (6 commits, 778/778) 2026-06-07 15:05:51 +00:00
2378056cb3 maude: Phase 3 — equational matching modulo assoc/comm/id (28 tests, 119 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 47s
The chisel. lib/maude/matching.sx: multi-valued matcher mau/mm returning
ALL substitutions, dispatching on op theory (free/comm/assoc/AC). Identity
lets variables grab empty blocks. AC-canonical form (mau/canon) powers
ac-equal? and deterministic printout. AC rewriting extends f-AC equations
with rest vars so a rule fires on any sub-multiset/subword; mau/first-change
only commits rewrites that change the canonical form (idempotency/identity
terminate). Verified on multiset rewriting, set theory, group equations.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 15:01:07 +00:00
94f6ab9f2f Merge loops/fed-prims into architecture: diagnose fed-sx-m2 Blockers #4 (handler mutex deadlock)
Doc-only: records that the http-listen 'handler-mutex deadlock' is not a
mutex bug but an Erlang-scheduler-context issue (handler runs on a native
Thread.create outside any er-sched step, so gen_server:call->receive can
never complete). Pattern A inapplicable; correct fix is Pattern B in
er-bif-http-listen (lib/erlang, m2 scope). Full diagnosis + patch sketch in
plans/fed-sx-host-primitives.md.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 14:53:33 +00:00
c9a8f05244 content: tree-wide content/find + has? (778/778)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 22s
Facade read-by-id was top-level only while content/edit's update/delete are
tree-wide — could not read back a nested block content/edit just modified.
Added generic ct-find-id (doc.sx) + doc-find-deep/doc-has-deep?; content/find
+ has? now descend into sections. content/find-top/has-top? keep top-level
lookup. Audit: remaining doc-find/ct-index-of callers are positional
insert/move (top-level by design). +6 api tests.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 14:49:15 +00:00
10906d4ffc maude: Phase 2 syntactic equational reduction (26 tests, 91 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 36s
lib/maude/reduce.sx — one-sided syntactic matching (non-linear patterns
via bound-var equality), immutable substitutions, innermost fixpoint
normalisation. Tested on Peano arithmetic, list ops, a propositional
logic simplifier, and non-linear matching.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 14:46:02 +00:00
bf8d0bf245 fed-prims: diagnose fed-sx-m2 Blockers #4 — not a mutex bug, hand back to m2
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 1m7s
Investigated the http-listen "handler-mutex deadlock" per
plans/agent-briefings/fed-prims-mutex-fix.md. Reproduced deterministically
(single kernel-route request returns empty reply while a non-kernel route
returns 200; also reproduced with a 3-line minimal echo gen_server).

Root cause is in the Erlang substrate, not the OCaml mutex: native
http-listen runs each handler on a fresh Thread.create outside any Erlang
scheduler step, so gen_server:call -> receive (which raises er-suspend-marker
expecting an enclosing er-sched-step-alive! guard + er-sched-run-all! pump)
can never complete.

Pattern A is inapplicable: the failure reproduces on a single request with
zero contention, so it is not a mutex-contention deadlock; the mutex is in
fact required and must stay. Sx_runtime.sx_call is fully synchronous and no
OCaml symbol reaches the SX-level scheduler, so there is no OCaml-only fix.
The correct fix is Pattern B done entirely in er-bif-http-listen
(lib/erlang/runtime.sx) — spawn the handler as an er-process and
er-sched-run-all! to completion — which is m2 / loops/erlang scope.

Doc-only: full diagnosis + concrete patch sketch added to the Blockers and
Progress log of plans/fed-sx-host-primitives.md. No bin/sx_server.ml change.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 14:43:54 +00:00
9f87206949 maude: Phase 1 parser — fmod/mod modules, signatures, mixfix terms (65 tests)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 1m14s
Term representation (lib/maude/term.sx) plus a module parser
(lib/maude/parser.sx) consuming lib/guest/lex + pratt:

- whitespace+bracket tokenizer (--- / *** comments)
- mixfix classification (split op names on _): infix/prefix/postfix/const
- precedence-climbing term parser over a pratt table built from op decls
- fmod/mod ... endfm/endm with sort/subsort/op/var/eq/ceq/rl/crl
- transitive subsort hierarchy + operator overloading queries

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 14:43:02 +00:00
9051f52f53 content: tree-wide revision diff (772/772)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 1m9s
content/diff + diff-versions enumerated ids top-level only (doc-ids/
doc-find), so diffs of documents with sections missed every nested add/
remove/change. Now via doc-tree-ids + doc-deep-find; sections excluded from
:changed (no own content), still reported in :added/:removed. Flat-doc
diffs unchanged. +9 store tests.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 13:39:08 +00:00
4d889716a3 content: in-document prose search via asText (763/763)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 36s
content/search-text + search-text-ids find every block whose (asText b)
contains a term — spanning all text-bearing fields by reusing the canonical
asText projection, so it can't drift from stats/find-replace. Section
wrappers excluded. +7 query tests.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 12:52:34 +00:00
2f626173d9 content: find-replace rewrites all text-bearing fields (756/756)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 53s
fr-rewrite dispatches per block type so image alt, list items, and table
headers/cells are renamed alongside text/heading/code/quote/callout —
matching exactly the set asText/stats/word-count fold into prose. Prior
find-replace skipped them, so a rename stayed visible in counts/exports.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 12:05:11 +00:00
92c0c853a9 content: find-replace covers callout text + 2 tests (752/752)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 53s
fr-has-text? now treats callout as text-bearing, matching asText/stats/
summary. content/find-replace previously skipped callout bodies silently.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 11:10:25 +00:00
94b889c911 content: by-id ops (update/delete) act tree-wide — fixes op-log no-op on nested blocks + 4 tests (750/750)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 14m45s
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 10:25:54 +00:00
55 changed files with 6776 additions and 92 deletions

View File

@@ -13,7 +13,7 @@ if [ ! -x "$SX_SERVER" ]; then
exit 1
fi
SUITES=(dag analyze plan execute optimize fed cost serialize stats fault)
SUITES=(dag analyze plan execute optimize fed cost serialize stats fault maude-optimize)
OUT_JSON="lib/artdag/scoreboard.json"
OUT_MD="lib/artdag/scoreboard.md"
@@ -23,6 +23,26 @@ run_suite() {
local file="lib/artdag/tests/${suite}.sx"
local TMP
TMP=$(mktemp)
local MAUDE_LOADS=""
local BRIDGE_LOAD=""
if [ "$suite" = "maude-optimize" ]; then
MAUDE_LOADS='(load "lib/guest/lex.sx")
(load "lib/guest/pratt.sx")
(load "lib/maude/term.sx")
(load "lib/maude/parser.sx")
(load "lib/maude/sorts.sx")
(load "lib/maude/reduce.sx")
(load "lib/maude/matching.sx")
(load "lib/maude/conditional.sx")
(load "lib/maude/fire.sx")
(load "lib/maude/rewrite.sx")
(load "lib/maude/searchpath.sx")
(load "lib/maude/strategy.sx")
(load "lib/maude/meta.sx")
(load "lib/maude/pretty.sx")
(load "lib/maude/run.sx")'
BRIDGE_LOAD='(load "lib/artdag/maude-bridge.sx")'
fi
cat > "$TMP" << EPOCHS
(epoch 1)
(load "spec/stdlib.sx")
@@ -41,6 +61,7 @@ run_suite() {
(load "lib/persist/log.sx")
(load "lib/persist/kv.sx")
(load "lib/persist/api.sx")
${MAUDE_LOADS}
(load "lib/artdag/dag.sx")
(load "lib/artdag/analyze.sx")
(load "lib/artdag/plan.sx")
@@ -52,6 +73,7 @@ run_suite() {
(load "lib/artdag/stats.sx")
(load "lib/artdag/fault.sx")
(load "lib/artdag/api.sx")
${BRIDGE_LOAD}
(epoch 2)
(eval "(define artdag-test-pass 0)")
(eval "(define artdag-test-fail 0)")

118
lib/artdag/maude-bridge.sx Normal file
View File

@@ -0,0 +1,118 @@
; lib/artdag/maude-bridge.sx — adapter between an artdag effect DAG and maude terms.
; A node {:op :inputs :params :commutative} <-> a maude (mau/app op (args...)).
; Inputs become argument subterms (recursively from the DAG). A trailing
; "artdag:meta" subterm carries the params (a write-to-string token) and the
; commutativity flag, so the encoding is lossless and dag->term->dag is the
; identity on canonical (content-id) form. Commutative ops map to maude AC
; operators in the optimizer module, so input order is irrelevant there —
; mirroring the content-id's order-insensitivity for commutative nodes.
;
; maude (lib/maude) is a READ-ONLY consumed substrate: mau/app, mau/const,
; mau/op, mau/args, mau/app? are its term constructors/accessors.
; ---- list helpers (no host last/but-last) ----
(define
artdag/mb-last
(fn
(xs)
(if (empty? (rest xs)) (first xs) (artdag/mb-last (rest xs)))))
(define
artdag/mb-but-last
(fn
(xs)
(if
(empty? (rest xs))
(list)
(cons (first xs) (artdag/mb-but-last (rest xs))))))
; ---- params <-> token ----
; params are keyword-keyed dicts; write-to-string/read round-trips them
; (key order may differ but the dicts compare structurally equal).
(define artdag/mb-meta-op "artdag:meta")
(define artdag/params->token (fn (params) (write-to-string params)))
(define artdag/token->params (fn (token) (read (open-input-string token))))
(define
artdag/mb-meta-term
(fn
(params commutative)
(mau/app
artdag/mb-meta-op
(list
(mau/const (artdag/params->token params))
(mau/const (if commutative "c" "n"))))))
(define
artdag/mb-meta-term?
(fn (t) (and (mau/app? t) (= (mau/op t) artdag/mb-meta-op))))
; ---- dag -> term ----
(define
artdag/node->term
(fn
(node input-terms)
(mau/app
(artdag/node-op node)
(concat
input-terms
(list
(artdag/mb-meta-term
(artdag/node-params node)
(get node :commutative)))))))
(define
artdag/dag->term
(fn
(dag id)
(let
((node (artdag/dag-get dag id)))
(artdag/node->term
node
(map (fn (in) (artdag/dag->term dag in)) (artdag/node-inputs node))))))
; ---- term -> dag ----
; build-entries with synthesized local names; artdag/build recomputes content-ids
; (which are name-independent), so the reconstructed dag is identical on canonical
; form. Shared subterms re-collapse to one node/id during build's dedup.
(define artdag/term-meta (fn (t) (artdag/mb-last (mau/args t))))
(define artdag/term-input-terms (fn (t) (artdag/mb-but-last (mau/args t))))
(define
artdag/term-params
(fn
(t)
(artdag/token->params (mau/op (first (mau/args (artdag/term-meta t)))))))
(define
artdag/term-commutative
(fn
(t)
(= "c" (mau/op (nth (mau/args (artdag/term-meta t)) 1)))))
(define
artdag/term->build
(fn
(t counter acc)
(let
((built (reduce (fn (st child) (let ((r (artdag/term->build child (get st :counter) (get st :acc)))) {:counter (get r :counter) :acc (get r :acc) :names (concat (get st :names) (list (get r :name)))})) {:counter counter :acc acc :names (list)} (artdag/term-input-terms t))))
(let ((my-name (str "mb" (get built :counter)))) {:name my-name :counter (+ (get built :counter) 1) :acc (concat (get built :acc) (list (list my-name (mau/op t) (get built :names) (artdag/term-params t) (artdag/term-commutative t))))}))))
(define
artdag/term->entries
(fn (t) (get (artdag/term->build t 0 (list)) :acc)))
(define artdag/term->dag (fn (t) (artdag/build (artdag/term->entries t))))
; ---- round-trip convenience ----
(define
artdag/mb-roundtrip
(fn (dag id) (artdag/term->dag (artdag/dag->term dag id))))

View File

@@ -9,9 +9,10 @@
"cost": {"pass": 13, "fail": 0},
"serialize": {"pass": 13, "fail": 0},
"stats": {"pass": 12, "fail": 0},
"fault": {"pass": 14, "fail": 0}
"fault": {"pass": 14, "fail": 0},
"maude-optimize": {"pass": 14, "fail": 0}
},
"total_pass": 158,
"total_pass": 172,
"total_fail": 0,
"total": 158
"total": 172
}

View File

@@ -14,4 +14,5 @@ _Generated by `lib/artdag/conformance.sh`_
| serialize | 13 | 0 | 13 |
| stats | 12 | 0 | 12 |
| fault | 14 | 0 | 14 |
| **Total** | **158** | **0** | **158** |
| maude-optimize | 14 | 0 | 14 |
| **Total** | **172** | **0** | **172** |

View File

@@ -0,0 +1,112 @@
; Phase 7 — rule-based optimization via maude-on-sx.
; Bridge round-trip: dag->term->dag is the identity on canonical (content-id) form.
; ---- linear chain a -> b -> c (b carries params) ----
(define
mo-chain
(artdag/build
(list
(list "a" "in" (list) {:v 5})
(list "b" "blur" (list "a") {:radius 2})
(list "c" "blur" (list "b") {:radius 3}))))
(define mo-c-id (artdag/dag-id mo-chain "c"))
(define mo-chain-rt (artdag/mb-roundtrip mo-chain mo-c-id))
(artdag-test
"roundtrip: sink id preserved"
(artdag/member? mo-c-id (keys (artdag/dag-nodes mo-chain-rt)))
true)
(artdag-test
"roundtrip: node count preserved"
(artdag/node-count mo-chain-rt)
3)
(artdag-test
"roundtrip: sink op preserved"
(artdag/node-op (artdag/dag-get mo-chain-rt mo-c-id))
"blur")
(artdag-test
"roundtrip: sink params preserved"
(artdag/node-params (artdag/dag-get mo-chain-rt mo-c-id))
{:radius 3})
(artdag-test
"roundtrip: full reconstructed node equals original"
(= (artdag/dag-get mo-chain-rt mo-c-id) (artdag/dag-get mo-chain mo-c-id))
true)
; ---- term shape ----
(define mo-c-term (artdag/dag->term mo-chain mo-c-id))
(artdag-test "term: sink op is the maude operator" (mau/op mo-c-term) "blur")
(artdag-test
"term: params recovered from meta"
(artdag/term-params mo-c-term)
{:radius 3})
(artdag-test
"term: commutative flag recovered (false)"
(artdag/term-commutative mo-c-term)
false)
(artdag-test
"term->entries: one entry per node"
(len (artdag/term->entries mo-c-term))
3)
; ---- commutative node: order-insensitive id survives round-trip ----
(define
mo-comm
(artdag/build
(list
(list "x" "src" (list) {})
(list "y" "noise" (list) {})
(list "z" "over" (list "x" "y") {} true))))
(define mo-z-id (artdag/dag-id mo-comm "z"))
(define mo-comm-rt (artdag/mb-roundtrip mo-comm mo-z-id))
(artdag-test
"roundtrip comm: commutative id preserved"
(artdag/member? mo-z-id (keys (artdag/dag-nodes mo-comm-rt)))
true)
(artdag-test
"term comm: commutative flag recovered (true)"
(artdag/term-commutative (artdag/dag->term mo-comm mo-z-id))
true)
; ---- diamond: shared subgraph re-collapses to one node ----
(define
mo-diamond
(artdag/build
(list
(list "a" "src" (list) {})
(list "b" "blur" (list "a") {:radius 1})
(list "c" "bright" (list "a") {:gain 2})
(list "d" "over" (list "b" "c") {} true))))
(define mo-d-id (artdag/dag-id mo-diamond "d"))
(define mo-diamond-rt (artdag/mb-roundtrip mo-diamond mo-d-id))
(artdag-test
"roundtrip diamond: shared node not duplicated"
(artdag/node-count mo-diamond-rt)
4)
(artdag-test
"roundtrip diamond: sink id preserved"
(artdag/member? mo-d-id (keys (artdag/dag-nodes mo-diamond-rt)))
true)
(artdag-test
"roundtrip diamond: shared src id preserved"
(artdag/member?
(artdag/dag-id mo-diamond "a")
(keys (artdag/dag-nodes mo-diamond-rt)))
true)

View File

@@ -25,8 +25,13 @@
(define content/append doc-append)
(define content/blocks doc-blocks)
(define content/count doc-count)
(define content/find doc-find)
(define content/has? doc-has?)
;; find / has? are TREE-WIDE by id (descend into sections) — so the facade reads
;; back any block content/edit can update or delete. content/find-top / has-top?
;; keep the top-level-only lookup for callers that mean the ordered sequence.
(define content/find doc-find-deep)
(define content/has? doc-has-deep?)
(define content/find-top doc-find)
(define content/has-top? doc-has?)
(define content/ids doc-ids)
(define content/types doc-types)

View File

@@ -5,14 +5,19 @@
;; and returns a NEW document — the input is never mutated, so any version is the
;; head of an op stream (replay-friendly for persist + CRDT merge).
;;
;; CtDoc also carries optional metadata (title/slug/tags) — see meta.sx for the
;; ergonomic API; they default nil and do not affect block operations.
;; By-id ops (update/delete) and by-id lookup (doc-find-deep/doc-has-deep?) are
;; TREE-WIDE: they descend into any block carrying a `children` list (i.e.
;; sections), since ids are unique across the tree. This keeps the persist
;; op-log, content/edit and content/find correct for nested documents.
;; insert/move are positional and act at the top level.
;;
;; CtDoc also carries optional metadata (title/slug/tags) — see meta.sx.
;;
;; Op shapes (data, not objects — they are the persist event payload):
;; {:op "insert" :block <blk> :after <id|nil>} ; after nil = prepend
;; {:op "update" :id <id> :field <name> :value <v>}
;; {:op "move" :id <id> :index <n>}
;; {:op "delete" :id <id>}
;; {:op "insert" :block <blk> :after <id|nil>} ; after nil = prepend (top level)
;; {:op "update" :id <id> :field <name> :value <v>} ; tree-wide by id
;; {:op "move" :id <id> :index <n>} ; top level
;; {:op "delete" :id <id>} ; tree-wide by id
(define
content-bootstrap-doc!
@@ -76,17 +81,58 @@
(first blocks)
(ct-insert-at (rest blocks) (- i 1) x))))))
;; tree-wide remove by id: drop matches at this level, recurse into children
;; (blocks carrying a `children` list, i.e. sections).
(define
ct-remove-id
(fn
(blocks id)
(filter (fn (b) (if (= (blk-id b) id) false true)) blocks)))
(map
(fn
(b)
(let
((ch (st-iv-get b "children")))
(if (list? ch) (st-iv-set! b "children" (ct-remove-id ch id)) b)))
(filter (fn (b) (if (= (blk-id b) id) false true)) blocks))))
;; tree-wide replace by id: apply f to the match wherever it sits in the tree.
(define
ct-replace-id
(fn
(blocks id f)
(map (fn (b) (if (= (blk-id b) id) (f b) b)) blocks)))
(map
(fn
(b)
(if
(= (blk-id b) id)
(f b)
(let
((ch (st-iv-get b "children")))
(if
(list? ch)
(st-iv-set! b "children" (ct-replace-id ch id f))
b))))
blocks)))
;; tree-wide find by id: first block matching id anywhere in the tree, or nil.
;; Descends into any `children` list, mirroring ct-replace-id/ct-remove-id.
(define
ct-find-id
(fn
(blocks id)
(if
(= (len blocks) 0)
nil
(let
((b (first blocks)))
(if
(= (blk-id b) id)
b
(let
((ch (st-iv-get b "children")))
(let
((nested (if (list? ch) (ct-find-id ch id) nil)))
(if (= nested nil) (ct-find-id (rest blocks) id) nested))))))))
;; ── query ──
(define doc-index-of (fn (doc id) (ct-index-of (doc-blocks doc) id)))
@@ -103,6 +149,14 @@
doc-has?
(fn (doc id) (if (= (doc-index-of doc id) -1) false true)))
;; tree-wide lookup by id — reads a nested block by the same id content/edit can
;; update/delete (no section.sx dependency; uses the generic children descent).
(define doc-find-deep (fn (doc id) (ct-find-id (doc-blocks doc) id)))
(define
doc-has-deep?
(fn (doc id) (if (= (doc-find-deep doc id) nil) false true)))
;; ── structural edits (each returns a new document) ──
(define doc-with-blocks (fn (doc blocks) (st-iv-set! doc "blocks" blocks)))

View File

@@ -1,10 +1,17 @@
;; content-on-sx — global find/replace across text-bearing blocks.
;; content-on-sx — global find/replace across every text-bearing field.
;;
;; Replaces every occurrence of `from` with `to` in the text field of text /
;; heading / code / quote blocks, tree-wide (via the transform layer). For
;; renaming a term throughout a document. Immutable; case-sensitive.
;; Replaces every occurrence of `from` with `to` in the text-bearing fields of
;; a document, tree-wide (via the transform layer):
;; - the `text` of text / heading / code / quote / callout blocks
;; - the `alt` of image blocks
;; - each item of list blocks
;; - every header and cell of table blocks
;; This is exactly the set asText / stats / summary draw prose from, so a rename
;; via content/find-replace and a word count over asText stay consistent.
;; Immutable; case-sensitive.
;;
;; Requires (loaded by harness): block.sx, transform.sx (content/map-blocks).
;; Requires (loaded by harness): block.sx, transform.sx (content/map-blocks),
;; table.sx (CtTable ivars).
(define
fr-in?
@@ -15,17 +22,54 @@
((= (first xs) x) true)
(else (fr-in? x (rest xs))))))
(define fr-rep (fn (s from to) (replace (str s) from to)))
;; Blocks whose prose content find/replace rewrites (matches asText's set).
(define
fr-has-text?
(fn (b) (fr-in? (blk-type b) (list "text" "heading" "code" "quote"))))
(fn
(b)
(fr-in?
(blk-type b)
(list "text" "heading" "code" "quote" "callout" "image" "list" "table"))))
;; Per-type field rewrite. Each branch returns a new (copy-on-write) block.
(define
fr-rewrite
(fn
(b from to)
(let
((t (blk-type b)))
(cond
((= t "image")
(blk-set b "alt" (fr-rep (blk-get b "alt") from to)))
((= t "list")
(let
((items (blk-get b "items")))
(if
(list? items)
(blk-set b "items" (map (fn (it) (fr-rep it from to)) items))
b)))
((= t "table")
(let
((hs (blk-get b "headers")) (rs (blk-get b "rows")))
(let
((b1 (if (list? hs) (blk-set b "headers" (map (fn (h) (fr-rep h from to)) hs)) b)))
(if
(list? rs)
(blk-set
b1
"rows"
(map
(fn
(r)
(if (list? r) (map (fn (c) (fr-rep c from to)) r) r))
rs))
b1))))
(else (blk-set b "text" (fr-rep (blk-get b "text") from to)))))))
(define
content/find-replace
(fn
(doc from to)
(content/map-blocks
doc
fr-has-text?
(fn
(b)
(blk-set b "text" (replace (str (blk-get b "text")) from to))))))
(content/map-blocks doc fr-has-text? (fn (b) (fr-rewrite b from to)))))

View File

@@ -1,10 +1,10 @@
;; content-on-sx — block query + table of contents.
;;
;; Collect blocks across the whole tree (descending into sections) by predicate
;; or type, and derive a table of contents from headings. Tree detection is
;; inline (class + st-iv-get) so this needs no section.sx.
;; or type, search them by prose, and derive a table of contents from headings.
;; Tree detection is inline (class + st-iv-get) so this needs no section.sx.
;;
;; Requires (loaded by harness): block.sx, doc.sx.
;; Requires (loaded by harness): block.sx, doc.sx, text.sx (asText for search).
(define
qry-section?
@@ -45,6 +45,30 @@
content/select-ids
(fn (doc pred) (map (fn (b) (blk-id b)) (content/select doc pred))))
;; Blocks (tree-wide, excluding section containers) whose own prose contains
;; `term`. "Prose" is (asText b), so search covers exactly what every block
;; exposes as text — text/heading/code/quote/callout text, image alt, list
;; items, table headers+cells — with no separate field list to drift from
;; asText / find-replace / stats. Case-sensitive substring match.
(define
content/search-text
(fn
(doc term)
(content/select
doc
(fn
(b)
(and
(not (qry-section? b))
(>= (index-of (asText b) term) 0))))))
;; Same search, returning matching block ids in document order.
(define
content/search-text-ids
(fn
(doc term)
(map (fn (b) (blk-id b)) (content/search-text doc term))))
;; table of contents: {:id :level :text} for every heading, in document order.
(define
content/headings

View File

@@ -3,7 +3,7 @@
"block": {"pass": 38, "fail": 0},
"doc": {"pass": 40, "fail": 0},
"render": {"pass": 42, "fail": 0},
"api": {"pass": 26, "fail": 0},
"api": {"pass": 32, "fail": 0},
"meta": {"pass": 27, "fail": 0},
"page": {"pass": 7, "fail": 0},
"page-full": {"pass": 4, "fail": 0},
@@ -14,14 +14,14 @@
"tree-edit": {"pass": 17, "fail": 0},
"move": {"pass": 11, "fail": 0},
"clone": {"pass": 10, "fail": 0},
"query": {"pass": 13, "fail": 0},
"query": {"pass": 20, "fail": 0},
"toc": {"pass": 8, "fail": 0},
"anchor": {"pass": 6, "fail": 0},
"outline": {"pass": 14, "fail": 0},
"flatten": {"pass": 10, "fail": 0},
"transform": {"pass": 12, "fail": 0},
"normalize": {"pass": 11, "fail": 0},
"find-replace": {"pass": 10, "fail": 0},
"find-replace": {"pass": 16, "fail": 0},
"stats": {"pass": 17, "fail": 0},
"summary": {"pass": 14, "fail": 0},
"index": {"pass": 13, "fail": 0},
@@ -31,7 +31,7 @@
"data": {"pass": 25, "fail": 0},
"wire": {"pass": 11, "fail": 0},
"validate": {"pass": 23, "fail": 0},
"store": {"pass": 33, "fail": 0},
"store": {"pass": 46, "fail": 0},
"snapshot": {"pass": 20, "fail": 0},
"crdt": {"pass": 34, "fail": 0},
"crdt-tree": {"pass": 21, "fail": 0},
@@ -42,7 +42,7 @@
"md-doc": {"pass": 12, "fail": 0},
"fed": {"pass": 20, "fail": 0}
},
"total_pass": 746,
"total_pass": 778,
"total_fail": 0,
"total": 746
"total": 778
}

View File

@@ -7,7 +7,7 @@ _Generated by `lib/content/conformance.sh`_
| block | 38 | 0 | 38 |
| doc | 40 | 0 | 40 |
| render | 42 | 0 | 42 |
| api | 26 | 0 | 26 |
| api | 32 | 0 | 32 |
| meta | 27 | 0 | 27 |
| page | 7 | 0 | 7 |
| page-full | 4 | 0 | 4 |
@@ -18,14 +18,14 @@ _Generated by `lib/content/conformance.sh`_
| tree-edit | 17 | 0 | 17 |
| move | 11 | 0 | 11 |
| clone | 10 | 0 | 10 |
| query | 13 | 0 | 13 |
| query | 20 | 0 | 20 |
| toc | 8 | 0 | 8 |
| anchor | 6 | 0 | 6 |
| outline | 14 | 0 | 14 |
| flatten | 10 | 0 | 10 |
| transform | 12 | 0 | 12 |
| normalize | 11 | 0 | 11 |
| find-replace | 10 | 0 | 10 |
| find-replace | 16 | 0 | 16 |
| stats | 17 | 0 | 17 |
| summary | 14 | 0 | 14 |
| index | 13 | 0 | 13 |
@@ -35,7 +35,7 @@ _Generated by `lib/content/conformance.sh`_
| data | 25 | 0 | 25 |
| wire | 11 | 0 | 11 |
| validate | 23 | 0 | 23 |
| store | 33 | 0 | 33 |
| store | 46 | 0 | 46 |
| snapshot | 20 | 0 | 20 |
| crdt | 34 | 0 | 34 |
| crdt-tree | 21 | 0 | 21 |
@@ -45,4 +45,4 @@ _Generated by `lib/content/conformance.sh`_
| md-import | 38 | 0 | 38 |
| md-doc | 12 | 0 | 12 |
| fed | 20 | 0 | 20 |
| **Total** | **746** | **0** | **746** |
| **Total** | **778** | **0** | **778** |

View File

@@ -5,9 +5,10 @@
;; replay of its op stream up to a sequence number; the materialised doc is a
;; cache, never primary state.
;;
;; Requires (loaded by the harness): block.sx, doc.sx, and persist
;; (event/backend/log/kv/api). The persist backend `b` is opened by the caller
;; via (persist/open) and injected — content knows nothing about which backend.
;; Requires (loaded by the harness): block.sx, doc.sx, section.sx (doc-deep-find
;; + doc-tree-ids, for the tree-wide diff), plus persist (event/backend/log/kv/
;; api). The persist backend `b` is opened by the caller via (persist/open) and
;; injected — content knows nothing about which backend.
(define content/-stream (fn (doc-id) (str "content:" doc-id)))
@@ -69,11 +70,18 @@
(fn (b doc-id) (map (fn (ev) {:type (persist/event-type ev) :at (persist/event-at ev) :seq (persist/event-seq ev)}) (content/log b doc-id))))
;; ── diff between two materialised document versions ──
;; Returns {:added (ids) :removed (ids) :changed (ids)} where changed = ids
;; present in both whose block content differs.
(define
content/-missing?
(fn (doc id) (= (ct-index-of (doc-blocks doc) id) -1)))
;; Tree-wide: ids are enumerated across the whole block tree (descending into
;; sections), so nested-block adds/removes/changes are detected, not just
;; top-level ones. Returns {:added :removed :changed} (lists of ids):
;; :added — ids present (anywhere) in `new` but not in `old`
;; :removed — ids present (anywhere) in `old` but not in `new`
;; :changed — content blocks present in both whose block value differs
;; Section containers never appear in :changed (they hold no own content — a
;; child change surfaces as that child's own entry); a whole section appearing
;; or disappearing shows up in :added / :removed by its id.
(define content/-all-ids (fn (doc) (doc-tree-ids doc)))
(define content/-missing? (fn (doc id) (= (doc-deep-find doc id) nil)))
(define
content/-changed
@@ -83,15 +91,16 @@
(fn
(id)
(let
((bo (doc-find old id)) (bn (doc-find new id)))
((bo (doc-deep-find old id)) (bn (doc-deep-find new id)))
(cond
((= bo nil) false)
((= bn nil) false)
((= (blk-type bo) "section") false)
((= bo bn) false)
(else true))))
(doc-ids old))))
(content/-all-ids old))))
(define content/diff (fn (old new) {:changed (content/-changed old new) :removed (filter (fn (id) (content/-missing? new id)) (doc-ids old)) :added (filter (fn (id) (content/-missing? old id)) (doc-ids new))}))
(define content/diff (fn (old new) {:changed (content/-changed old new) :removed (filter (fn (id) (content/-missing? new id)) (content/-all-ids old)) :added (filter (fn (id) (content/-missing? old id)) (content/-all-ids new))}))
;; convenience: diff two persisted versions by seq.
(define

View File

@@ -97,3 +97,37 @@
"render original unchanged"
(content/render d1 "html")
"<h1>Hi</h1><p>World</p>")
;; ── facade find/has? are TREE-WIDE (reach into sections); find-top/has-top?
;; keep the top-level-only lookup. This makes the read-by-id surface consistent
;; with content/edit, whose update/delete are already tree-wide. ──
(content-bootstrap-section!)
(define
nd
(content/append
(content/empty "nested")
(mk-section
"sec"
(list (content/block "text" "inner" (list (list "text" "deep")))))))
(content-test
"find nested (deep)"
(blk-id (content/find nd "inner"))
"inner")
(content-test "has? nested (deep)" (content/has? nd "inner") true)
(content-test "find-top misses nested" (content/find-top nd "inner") nil)
(content-test "has-top? misses nested" (content/has-top? nd "inner") false)
(content-test
"find-top sees top-level"
(blk-id (content/find-top nd "sec"))
"sec")
;; a nested block updated by id via content/edit is now readable by id via
;; content/find (was impossible when find was top-level-only).
(content-test
"edit-then-find nested round-trip"
(str
(blk-send
(content/find
(content/edit nd (content/update "inner" "text" "edited"))
"inner")
"text"))
"edited")

View File

@@ -1,8 +1,10 @@
;; Extension — global find/replace across text-bearing blocks.
;; Extension — global find/replace across every text-bearing field.
(st-bootstrap-classes!)
(content/bootstrap!)
(content-bootstrap-section!)
(content-bootstrap-callout!)
(content-bootstrap-table!)
(define
d
@@ -30,11 +32,12 @@
(str (blk-send (doc-deep-find r "n") "text"))
"nested Bar")
;; ── does NOT touch image alt/src (not a text field) ──
;; ── image alt IS a text field (asText ^ alt), so it is rewritten ──
(content-test
"image alt untouched"
"image alt replaced"
(str (blk-send (doc-deep-find r "img") "alt"))
"Foo alt")
"Bar alt")
;; ── but src is a URL, not prose, so it stays put ──
(content-test
"image src untouched"
(str (blk-send (doc-deep-find r "img") "src"))
@@ -76,6 +79,68 @@
(str (blk-send (doc-find r2 "q") "text"))
"new saying")
;; ── callout text is covered (consistency with asText/stats/summary) ──
(content-test
"replace callout text"
(str
(blk-send
(doc-find
(content/find-replace
(doc-append (doc-empty "d") (mk-callout "co" "note" "Foo here"))
"Foo"
"Bar")
"co")
"text"))
"Bar here")
(content-test
"callout kind untouched by text replace"
(str
(blk-send
(doc-find
(content/find-replace
(doc-append (doc-empty "d") (mk-callout "co" "note" "x"))
"note"
"X")
"co")
"kind"))
"note")
;; ── list items are rewritten (asText folds items) ──
(define
rl
(content/find-replace
(doc-append
(doc-empty "d")
(mk-list "l" false (list "Foo one" "two Foo")))
"Foo"
"Bar"))
(content-test
"replace first list item"
(str (first (blk-send (doc-find rl "l") "items")))
"Bar one")
(content-test
"replace second list item"
(str (first (rest (blk-send (doc-find rl "l") "items"))))
"two Bar")
;; ── table headers + cells are rewritten (asText folds rows) ──
(define
rt
(content/find-replace
(doc-append
(doc-empty "d")
(mk-table "t" (list "Foo head") (list (list "a Foo" "b"))))
"Foo"
"Bar"))
(content-test
"replace table header"
(str (first (table-headers (doc-find rt "t"))))
"Bar head")
(content-test
"replace table cell"
(str (first (first (table-rows (doc-find rt "t")))))
"a Bar")
;; ── no match → unchanged render ──
(content-test
"no match"

View File

@@ -1,8 +1,11 @@
;; Extension — block query + table of contents.
;; Extension — block query + table of contents + prose search.
(st-bootstrap-classes!)
(content/bootstrap!)
(content-bootstrap-text!)
(content-bootstrap-section!)
(content-bootstrap-table!)
(content-bootstrap-callout!)
(define
d
@@ -87,3 +90,49 @@
"deep toc level"
(get (first (content/headings deep)) :level)
3)
;; ── prose search (content/search-text) ──
;; "cat" appears in text, image alt, a list item, a table cell, and a callout
;; — every text-bearing field — so search must find all five via asText.
(define
sd
(doc-append
(doc-append
(doc-append
(doc-append
(doc-append
(doc-empty "sd")
(mk-heading "sh" 1 "Welcome aboard"))
(mk-text "st" "the cat sat"))
(mk-image "si" "/x.png" "a cat photo"))
(mk-list "sl" false (list "first cat" "second dog")))
(mk-section
"sec"
(list
(mk-table "stb" (list "Animal") (list (list "cat") (list "fish")))
(mk-callout "sc" "note" "beware of cat")))))
(content-test
"search across every text-bearing field"
(content/search-text-ids sd "cat")
(list "st" "si" "sl" "stb" "sc"))
(content-test "search count" (len (content/search-text sd "cat")) 5)
(content-test
"search heading text"
(content/search-text-ids sd "Welcome")
(list "sh"))
(content-test
"search list item only"
(content/search-text-ids sd "dog")
(list "sl"))
(content-test "search no match" (content/search-text-ids sd "zzz") (list))
;; section containers are excluded — a term living only inside a section's
;; children returns the child, never the section wrapper.
(content-test
"search excludes section wrapper"
(content/search-text-ids sd "fish")
(list "stb"))
(content-test
"search returns block objects"
(blk-id (first (content/search-text sd "Welcome")))
"sh")

View File

@@ -151,3 +151,58 @@
"op-log media type"
(blk-type (doc-find (content/head B3 "rich") "v"))
"media")
;; ── op-log update/delete reach NESTED blocks (tree-wide by id) ──
(content-bootstrap-section!)
(define B4 (persist/open))
(content/commit!
B4
"nest"
(op-insert (mk-section "sec" (list (mk-text "n" "orig"))) nil)
1)
(content/commit! B4 "nest" (op-update "n" "text" "edited") 2)
(content-test
"op-log nested update"
(str (blk-send (doc-deep-find (content/head B4 "nest") "n") "text"))
"edited")
(content-test
"op-log nested update tree intact"
(doc-tree-ids (content/head B4 "nest"))
(list "sec" "n"))
(content/commit! B4 "nest" (op-delete "n") 3)
(content-test
"op-log nested delete"
(doc-tree-ids (content/head B4 "nest"))
(list "sec"))
(content-test
"op-log nested delete via content/at seq2"
(doc-tree-ids (content/at B4 "nest" 2))
(list "sec" "n"))
;; ── diff is TREE-WIDE: nested-block add/change/remove are detected, and
;; section containers never appear in :changed (a top-level-only diff would miss
;; "n" entirely and instead flag the section). ──
(define dn01 (content/diff-versions B4 "nest" 0 1))
(content-test
"diff nested added (section + child)"
(get dn01 :added)
(list "sec" "n"))
(content-test "diff nested added removed empty" (get dn01 :removed) (list))
(content-test "diff nested added changed empty" (get dn01 :changed) (list))
(define dn12 (content/diff-versions B4 "nest" 1 2))
(content-test
"diff nested changed child only"
(get dn12 :changed)
(list "n"))
(content-test "diff nested changed no add" (get dn12 :added) (list))
(content-test "diff nested changed no remove" (get dn12 :removed) (list))
(define dn23 (content/diff-versions B4 "nest" 2 3))
(content-test "diff nested removed child" (get dn23 :removed) (list "n"))
(content-test "diff nested removed no change" (get dn23 :changed) (list))
(content-test
"diff nested no-op"
(get (content/diff-versions B4 "nest" 1 1) :changed)
(list))

164
lib/maude/conditional.sx Normal file
View File

@@ -0,0 +1,164 @@
;; lib/maude/conditional.sx — conditional equations (Phase 4) + owise.
;;
;; A condition-aware superset of the Phase 3 reducer. `ceq L = R if COND` fires
;; only when COND holds under the matching substitution. Conditions come from
;; the parser as:
;; {:kind :eq :lhs L :rhs R} — holds iff reduce(s L) =AC= reduce(s R)
;; {:kind :bool :term T} — holds iff reduce(s T) =AC= true
;; Condition evaluation recurses through the SAME reducer (mau/cnormalize), so
;; a ceq whose guard mentions other (possibly conditional) equations Just Works
;; — termination rests on the guard reducing on structurally smaller arguments
;; (and the global fuel guard).
;;
;; `owise` (otherwise): an equation tagged [owise] fires at a redex only when
;; NO ordinary equation applies there. crewrite-top is two-pass: ordinary
;; equations first, owise equations last.
;;
;; Single-step firing uses the short-circuiting matcher in fire.sx
;; (mau/fire-eq). The eager candidate enumeration (mau/eq-candidates) is
;; retained for `search` (rewrite.sx), which genuinely needs every successor.
(define
mau/ac-candidates
(fn
(theory f th eq term)
(let
((id (get th :id))
(pels (mau/flatten-op theory f (get eq :lhs)))
(sels (mau/flatten-op theory f term)))
(let
((matches (if (get th :comm) (mau/match-multiset theory f (mau/append2 pels (list (mau/var "$R" ""))) sels {} id) (mau/match-sequence theory f (mau/append2 (list (mau/var "$L" "")) (mau/append2 pels (list (mau/var "$R" "")))) sels {} id))))
(map (fn (s) {:s s :result (mau/ac-eq-result theory f th eq s)}) matches)))))
(define
mau/eq-candidates
(fn
(theory eq term)
(let
((lhs (get eq :lhs)))
(let
((th (if (mau/app? lhs) (mau/th-of theory (mau/op lhs)) {:id nil :assoc false :comm false})))
(if
(and (mau/app? lhs) (get th :assoc))
(mau/ac-candidates theory (mau/op lhs) th eq term)
(map (fn (s) {:s s :result (mau/subst-apply s (get eq :rhs))}) (mau/mm theory lhs term {})))))))
(define
mau/cond-holds?
(fn
(theory eqs cond s)
(if
(= cond nil)
true
(if
(= (get cond :kind) "eq")
(mau/ac-equal?
theory
(mau/cnormalize
theory
eqs
(mau/subst-apply s (get cond :lhs))
mau/reduce-fuel)
(mau/cnormalize
theory
eqs
(mau/subst-apply s (get cond :rhs))
mau/reduce-fuel))
(mau/ac-equal?
theory
(mau/cnormalize
theory
eqs
(mau/subst-apply s (get cond :term))
mau/reduce-fuel)
(mau/const "true"))))))
(define
mau/try-candidates
(fn
(theory all-eqs cond term cands)
(if
(empty? cands)
nil
(let
((c (first cands)))
(if
(and
(not (mau/ac-equal? theory (get c :result) term))
(mau/cond-holds? theory all-eqs cond (get c :s)))
(get c :result)
(mau/try-candidates theory all-eqs cond term (rest cands)))))))
;; ---- owise partitioning ----
(define mau/eq-owise? (fn (e) (= (get e :owise) true)))
(define mau/filter-owise (fn (eqs) (filter mau/eq-owise? eqs)))
(define
mau/filter-noowise
(fn (eqs) (filter (fn (e) (not (mau/eq-owise? e))) eqs)))
(define
mau/crewrite-loop
(fn
(theory all-eqs eqs term)
(if
(empty? eqs)
nil
(let
((r (mau/fire-eq theory all-eqs (first eqs) term)))
(if (= r nil) (mau/crewrite-loop theory all-eqs (rest eqs) term) r)))))
(define
mau/crewrite-top
(fn
(theory eqs term)
(let
((r (mau/crewrite-loop theory eqs (mau/filter-noowise eqs) term)))
(if
(= r nil)
(mau/crewrite-loop theory eqs (mau/filter-owise eqs) term)
r))))
(define
mau/cnormalize
(fn
(theory eqs term fuel)
(if
(<= fuel 0)
term
(cond
((mau/var? term) term)
((mau/app? term)
(let
((nargs (map (fn (a) (mau/cnormalize theory eqs a fuel)) (mau/args term))))
(let
((t2 (mau/app (mau/op term) nargs)))
(let
((r (mau/crewrite-top theory eqs t2)))
(if
(= r nil)
t2
(mau/cnormalize theory eqs r (- fuel 1)))))))
(else term)))))
(define
mau/creduce
(fn
(m term)
(mau/cnormalize
(mau/build-theory m)
(mau/module-eqs m)
term
mau/reduce-fuel)))
(define
mau/creduce-term
(fn (m src) (mau/creduce m (mau/parse-term-in m src))))
(define
mau/creduce->str
(fn (m src) (mau/term->str (mau/creduce-term m src))))
(define
mau/ccanon
(fn (m src) (mau/canon (mau/build-theory m) (mau/creduce-term m src))))

268
lib/maude/confluence.sx Normal file
View File

@@ -0,0 +1,268 @@
;; lib/maude/confluence.sx — critical-pair / local-confluence checking.
;;
;; A terminating equation set is confluent iff every critical pair is joinable
;; (Knuth-Bendix / Newman). A critical pair arises when two oriented equations
;; overlap: a non-variable subterm of one LHS unifies with the other LHS, giving
;; two ways to rewrite the overlap; they must reduce to the same normal form.
;;
;; This needs TWO-SIDED unification (variables on both sides), not the one-sided
;; matching the reducer uses — so this file carries its own syntactic unifier.
;;
;; SCOPE / honesty: the unifier is SYNTACTIC. For free/constructor operators the
;; check is exact. For assoc/comm (AC) operators it sees only syntactic overlaps
;; (full AC-unification is NP/infinitary — out of scope), but joinability is
;; tested with `mau/ac-equal?` (canonical form modulo the theory), so AC laws are
;; joined correctly even though their overlaps are under-approximated. Conditional
;; and `owise` equations are not oriented (skipped).
;; ---------- syntactic unification (vars on both sides) ----------
(define
mau/u-walk
(fn
(t s)
(if
(mau/var? t)
(let
((b (get s (mau/vname t))))
(if (= b nil) t (mau/u-walk b s)))
t)))
(define
mau/u-occurs?
(fn
(name t s)
(let
((w (mau/u-walk t s)))
(cond
((mau/var? w) (= (mau/vname w) name))
((mau/app? w) (mau/u-occurs-any? name (mau/args w) s))
(else false)))))
(define
mau/u-occurs-any?
(fn
(name args s)
(cond
((empty? args) false)
((mau/u-occurs? name (first args) s) true)
(else (mau/u-occurs-any? name (rest args) s)))))
(define
mau/u-unify-args
(fn
(as bs s)
(cond
((= s nil) nil)
((and (empty? as) (empty? bs)) s)
((or (empty? as) (empty? bs)) nil)
(else
(mau/u-unify-args
(rest as)
(rest bs)
(mau/u-unify (first as) (first bs) s))))))
(define
mau/u-unify
(fn
(t1 t2 s)
(if
(= s nil)
nil
(let
((a (mau/u-walk t1 s)) (b (mau/u-walk t2 s)))
(cond
((and (mau/var? a) (mau/var? b) (= (mau/vname a) (mau/vname b)))
s)
((mau/var? a)
(if
(mau/u-occurs? (mau/vname a) b s)
nil
(assoc s (mau/vname a) b)))
((mau/var? b)
(if
(mau/u-occurs? (mau/vname b) a s)
nil
(assoc s (mau/vname b) a)))
((and (mau/app? a) (mau/app? b))
(if
(and
(= (mau/op a) (mau/op b))
(= (mau/arity a) (mau/arity b)))
(mau/u-unify-args (mau/args a) (mau/args b) s)
nil))
(else nil))))))
(define
mau/u-apply
(fn
(t s)
(let
((w (mau/u-walk t s)))
(if
(mau/app? w)
(mau/app
(mau/op w)
(map (fn (a) (mau/u-apply a s)) (mau/args w)))
w))))
(define
mau/u-rename
(fn
(t suffix)
(cond
((mau/var? t) (mau/var (str (mau/vname t) suffix) (mau/vsort t)))
((mau/app? t)
(mau/app
(mau/op t)
(map (fn (a) (mau/u-rename a suffix)) (mau/args t))))
(else t))))
;; ---------- positions ----------
(define
mau/positions-args
(fn
(args i)
(if
(empty? args)
(list)
(mau/append2
(map (fn (p) (cons i p)) (mau/nv-positions (first args)))
(mau/positions-args (rest args) (+ i 1))))))
;; non-variable positions (paths) of a term; root = empty path
(define
mau/nv-positions
(fn
(t)
(if
(mau/app? t)
(cons (list) (mau/positions-args (mau/args t) 0))
(list))))
(define
mau/at-path
(fn
(t path)
(if
(empty? path)
t
(mau/at-path (nth (mau/args t) (first path)) (rest path)))))
(define
mau/replace-nth
(fn
(xs i v)
(if
(= i 0)
(cons v (rest xs))
(cons (first xs) (mau/replace-nth (rest xs) (- i 1) v)))))
(define
mau/replace-at
(fn
(t path new)
(if
(empty? path)
new
(mau/app
(mau/op t)
(mau/replace-nth
(mau/args t)
(first path)
(mau/replace-at (nth (mau/args t) (first path)) (rest path) new))))))
;; ---------- critical pairs ----------
(define
mau/eq-same?
(fn
(e1 e2)
(and
(mau/term=? (get e1 :lhs) (get e2 :lhs))
(mau/term=? (get e1 :rhs) (get e2 :rhs)))))
(define
mau/cps-at
(fn
(l1 r1 l2 r2 same? paths)
(if
(empty? paths)
(list)
(let
((p (first paths)))
(if
(and same? (empty? p))
(mau/cps-at l1 r1 l2 r2 same? (rest paths))
(let
((s (mau/u-unify (mau/at-path l1 p) l2 {})))
(if
(= s nil)
(mau/cps-at l1 r1 l2 r2 same? (rest paths))
(cons {:right (mau/u-apply (mau/replace-at l1 p r2) s) :left (mau/u-apply r1 s)} (mau/cps-at l1 r1 l2 r2 same? (rest paths))))))))))
(define
mau/cps-of
(fn
(e1 e2)
(let
((l1 (mau/u-rename (get e1 :lhs) "#1"))
(r1 (mau/u-rename (get e1 :rhs) "#1"))
(l2 (mau/u-rename (get e2 :lhs) "#2"))
(r2 (mau/u-rename (get e2 :rhs) "#2")))
(mau/cps-at l1 r1 l2 r2 (mau/eq-same? e1 e2) (mau/nv-positions l1)))))
(define
mau/all-cps
(fn
(eqs)
(mau/concat-map
(fn (e1) (mau/concat-map (fn (e2) (mau/cps-of e1 e2)) eqs))
eqs)))
;; ---------- public API ----------
(define
mau/orientable-eqs
(fn
(m)
(filter
(fn (e) (and (= (get e :cond) nil) (not (= (get e :owise) true))))
(mau/module-eqs m))))
(define
mau/joinable?
(fn
(theory eqs t1 t2)
(mau/ac-equal?
theory
(mau/cnormalize theory eqs t1 mau/reduce-fuel)
(mau/cnormalize theory eqs t2 mau/reduce-fuel))))
(define mau/critical-pairs (fn (m) (mau/all-cps (mau/orientable-eqs m))))
(define
mau/non-joinable-pairs
(fn
(m)
(let
((theory (mau/build-theory m)) (eqs (mau/module-eqs m)))
(filter
(fn
(cp)
(not (mau/joinable? theory eqs (get cp :left) (get cp :right))))
(mau/all-cps (mau/orientable-eqs m))))))
(define mau/confluent? (fn (m) (empty? (mau/non-joinable-pairs m))))
(define
mau/cp->str
(fn
(m cp)
(let
((theory (mau/build-theory m)))
(str
(mau/canon theory (get cp :left))
" <?> "
(mau/canon theory (get cp :right))))))

View File

@@ -0,0 +1,41 @@
# Maude conformance config — sourced by lib/guest/conformance.sh.
LANG_NAME=maude
MODE=dict
PRELOADS=(
lib/guest/lex.sx
lib/guest/pratt.sx
lib/maude/term.sx
lib/maude/parser.sx
lib/maude/sorts.sx
lib/maude/reduce.sx
lib/maude/matching.sx
lib/maude/conditional.sx
lib/maude/fire.sx
lib/maude/confluence.sx
lib/maude/rewrite.sx
lib/maude/searchpath.sx
lib/maude/strategy.sx
lib/maude/meta.sx
lib/maude/pretty.sx
lib/maude/run.sx
)
SUITES=(
"parse:lib/maude/tests/parse.sx:(mau-parse-tests-run!)"
"reduce:lib/maude/tests/reduce.sx:(mau-reduce-tests-run!)"
"matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)"
"confluence:lib/maude/tests/confluence.sx:(mau-confluence-tests-run!)"
"conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)"
"owise:lib/maude/tests/owise.sx:(mau-owise-tests-run!)"
"gather:lib/maude/tests/gather.sx:(mau-gather-tests-run!)"
"sorts:lib/maude/tests/sorts.sx:(mau-sorts-tests-run!)"
"rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-tests-run!)"
"searchpath:lib/maude/tests/searchpath.sx:(mau-searchpath-tests-run!)"
"strategy:lib/maude/tests/strategy.sx:(mau-strategy-tests-run!)"
"meta:lib/maude/tests/meta.sx:(mau-meta-tests-run!)"
"pretty:lib/maude/tests/pretty.sx:(mau-pretty-tests-run!)"
"run:lib/maude/tests/run.sx:(mau-run-tests-run!)"
"effects:lib/maude/tests/effects.sx:(mau-effects-tests-run!)"
)

3
lib/maude/conformance.sh Executable file
View File

@@ -0,0 +1,3 @@
#!/usr/bin/env bash
# Thin wrapper — see lib/guest/conformance.sh and lib/maude/conformance.conf.
exec bash "$(dirname "$0")/../guest/conformance.sh" "$(dirname "$0")/conformance.conf" "$@"

250
lib/maude/fire.sx Normal file
View File

@@ -0,0 +1,250 @@
;; lib/maude/fire.sx — short-circuiting rule/equation firing.
;;
;; The eager matcher (mau/match-multiset) enumerates EVERY substitution, which
;; is what `mau/match-all` and `search` need. But for a single rewrite step we
;; only need the FIRST usable match — and eager enumeration is exponential when
;; an AC argument has many identical elements (q ; q ; ... ; q). These
;; find-matchers thread a predicate and stop at the first complete match for
;; which it returns non-nil; the predicate builds the rewritten term and checks
;; "progresses AND condition holds", so firing short-circuits on the first
;; productive match instead of materialising the whole solution set.
;;
;; pred : subst -> result-term-or-nil (result is always a term, never nil)
(define
mau/try-list
(fn
(substs cont)
(if
(empty? substs)
nil
(let
((r (cont (first substs))))
(if (= r nil) (mau/try-list (rest substs) cont) r)))))
;; ---- multiset (assoc+comm) find ----
(define
mau/ms-find
(fn
(theory f pels sels s id pred)
(cond
((empty? pels) (if (empty? sels) (pred s) nil))
(else
(let
((p (first pels)) (prest (rest pels)))
(if
(mau/var? p)
(mau/ms-find-var
theory
f
prest
sels
s
(mau/vname p)
id
pred
(mau/var-kmin (mau/vname p) id)
(mau/all-splits sels))
(mau/ms-find-nonvar theory f p prest sels s id pred 0)))))))
(define
mau/ms-find-nonvar
(fn
(theory f p prest sels s id pred i)
(if
(>= i (len sels))
nil
(let
((others (mau/remove-at sels i)))
(let
((r (mau/try-list (mau/mm theory p (nth sels i) s) (fn (s2) (mau/ms-find theory f prest others s2 id pred)))))
(if
(not (= r nil))
r
(mau/ms-find-nonvar
theory
f
p
prest
sels
s
id
pred
(+ i 1))))))))
(define
mau/ms-find-var
(fn
(theory f prest sels s name id pred kmin splits)
(if
(empty? splits)
nil
(let
((chosen (first (first splits)))
(rests (nth (first splits) 1)))
(if
(< (len chosen) kmin)
(mau/ms-find-var
theory
f
prest
sels
s
name
id
pred
kmin
(rest splits))
(let
((s2 (mau/bind-check theory s name (mau/rebuild f chosen id))))
(let
((r (if (= s2 nil) nil (mau/ms-find theory f prest rests s2 id pred))))
(if
(not (= r nil))
r
(mau/ms-find-var
theory
f
prest
sels
s
name
id
pred
kmin
(rest splits))))))))))
;; ---- sequence (assoc, ordered) find ----
(define
mau/seq-find
(fn
(theory f pels sels s id pred)
(cond
((empty? pels) (if (empty? sels) (pred s) nil))
(else
(let
((p (first pels)) (prest (rest pels)))
(if
(mau/var? p)
(mau/seq-find-var
theory
f
prest
sels
s
(mau/vname p)
id
pred
(mau/var-kmin (mau/vname p) id))
(if
(empty? sels)
nil
(mau/try-list
(mau/mm theory p (first sels) s)
(fn
(s2)
(mau/seq-find theory f prest (rest sels) s2 id pred))))))))))
(define
mau/seq-find-var
(fn
(theory f prest sels s name id pred k)
(if
(> k (len sels))
nil
(let
((s2 (mau/bind-check theory s name (mau/rebuild f (mau/take sels k) id))))
(let
((r (if (= s2 nil) nil (mau/seq-find theory f prest (mau/drop sels k) s2 id pred))))
(if
(not (= r nil))
r
(mau/seq-find-var
theory
f
prest
sels
s
name
id
pred
(+ k 1))))))))
;; ---- firing an equation/rule (returns rewritten term or nil) ----
(define
mau/fire-plain
(fn
(theory eqs eq term cnd substs)
(if
(empty? substs)
nil
(let
((res (mau/subst-apply (first substs) (get eq :rhs))))
(if
(and
(not (mau/ac-equal? theory res term))
(mau/cond-holds? theory eqs cnd (first substs)))
res
(mau/fire-plain theory eqs eq term cnd (rest substs)))))))
(define
mau/fire-ac
(fn
(theory eqs f th eq term cnd)
(let
((id (get th :id))
(pels (mau/flatten-op theory f (get eq :lhs)))
(sels (mau/flatten-op theory f term)))
(let
((pred (fn (s) (let ((res (mau/ac-eq-result theory f th eq s))) (if (and (not (mau/ac-equal? theory res term)) (mau/cond-holds? theory eqs cnd s)) res nil)))))
(if
(get th :comm)
(mau/ms-find
theory
f
(mau/append2 pels (list (mau/var "$R" "")))
sels
{}
id
pred)
(mau/seq-find
theory
f
(mau/append2
(list (mau/var "$L" ""))
(mau/append2 pels (list (mau/var "$R" ""))))
sels
{}
id
pred))))))
(define
mau/fire-eq
(fn
(theory eqs eq term)
(let
((lhs (get eq :lhs)) (cnd (get eq :cond)))
(if
(mau/app? lhs)
(let
((th (mau/th-of theory (mau/op lhs))))
(if
(get th :assoc)
(mau/fire-ac theory eqs (mau/op lhs) th eq term cnd)
(mau/fire-plain
theory
eqs
eq
term
cnd
(mau/mm theory lhs term {}))))
(mau/fire-plain
theory
eqs
eq
term
cnd
(mau/mm theory lhs term {}))))))

565
lib/maude/matching.sx Normal file
View File

@@ -0,0 +1,565 @@
;; lib/maude/matching.sx — equational matching modulo assoc/comm/id (Phase 3).
;;
;; The chisel. Syntactic matching (reduce.sx) returns at most one substitution;
;; matching modulo a theory is MULTI-VALUED — `X + Y` against `a + b + c` (with
;; _+_ assoc comm) has several solutions. `mau/mm` returns the full list of
;; substitutions; callers (rule application) pick.
;;
;; Operator theories come from the signature attributes, collected into a dict
;; OP-NAME -> {:assoc B :comm B :id ELT}. Matching dispatches on the head op's
;; theory:
;; free positional, exact arity
;; comm binary, try both argument orderings
;; assoc flatten the f-spine, match the pattern sequence against the
;; subject sequence (variables grab contiguous blocks)
;; assoc+comm flatten, match as multisets (variables grab sub-multisets)
;; Identity (id: e) lets a variable grab the empty block, contributing e.
;;
;; Equational rewriting (mau/ac-reduce) extends each f-AC equation l=r to
;; f(REST..., l) -> f(REST..., r) so a rule fires on any sub-multiset of an
;; AC term, then renormalises to a fixpoint. A candidate rewrite is taken only
;; if it changes the AC-canonical form (mau/canon) — idempotency/identity
;; matches that would re-fire forever are skipped, guaranteeing progress.
;; ---------- theory table ----------
(define
mau/build-theory
(fn
(m)
(let
((th {}))
(for-each
(fn
(op)
(let
((a (get op :attrs)))
(dict-set! th (get op :name) {:id (get a :id) :assoc (= (get a :assoc) true) :comm (= (get a :comm) true)})))
(mau/module-ops m))
th)))
(define
mau/th-of
(fn
(theory op)
(let ((e (get theory op))) (if (= e nil) {:id nil :assoc false :comm false} e))))
;; ---------- small list utilities ----------
(define
mau/concat-map
(fn
(f xs)
(if
(empty? xs)
(list)
(mau/append2 (f (first xs)) (mau/concat-map f (rest xs))))))
(define
mau/remove-at
(fn (xs i) (mau/append2 (mau/take xs i) (mau/drop xs (+ i 1)))))
;; All (chosen complement) pairs over every subset of xs.
(define
mau/all-splits
(fn
(xs)
(if
(empty? xs)
(list (list (list) (list)))
(let
((subsplits (mau/all-splits (rest xs))) (x (first xs)))
(mau/concat-map
(fn
(pair)
(let
((c (first pair)) (r (nth pair 1)))
(list (list (cons x c) r) (list c (cons x r)))))
subsplits)))))
;; ---------- flattening of associative spines ----------
(define
mau/flatten-op
(fn
(theory f term)
(if
(and (mau/app? term) (= (mau/op term) f))
(mau/flatten-op-list theory f (mau/args term))
(list term))))
(define
mau/flatten-op-list
(fn
(theory f args)
(if
(empty? args)
(list)
(mau/append2
(mau/flatten-op theory f (first args))
(mau/flatten-op-list theory f (rest args))))))
(define
mau/foldr-app
(fn
(f block)
(if
(empty? (rest block))
(first block)
(mau/app f (list (first block) (mau/foldr-app f (rest block)))))))
(define
mau/rebuild
(fn
(f block id)
(cond
((empty? block) (if (= id nil) (mau/const "$EMPTY") (mau/const id)))
((empty? (rest block)) (first block))
(else (mau/foldr-app f block)))))
(define mau/ac-build (fn (theory f els id) (mau/rebuild f els id)))
;; ---------- AC-canonical form / equality ----------
(define
mau/insert-str
(fn
(x ys)
(cond
((empty? ys) (list x))
((<= x (first ys)) (cons x ys))
(else (cons (first ys) (mau/insert-str x (rest ys)))))))
(define
mau/sort-strings
(fn
(xs)
(if
(empty? xs)
xs
(mau/insert-str (first xs) (mau/sort-strings (rest xs))))))
(define
mau/drop-identity
(fn
(theory f els id)
(if
(= id nil)
els
(let
((idc (mau/canon theory (mau/const id))))
(filter (fn (e) (not (= (mau/canon theory e) idc))) els)))))
(define
mau/canon
(fn
(theory term)
(cond
((mau/var? term) (str "?" (mau/vname term)))
((mau/const? term) (mau/op term))
((mau/app? term)
(let
((f (mau/op term)) (th (mau/th-of theory (mau/op term))))
(if
(get th :assoc)
(let
((els (mau/drop-identity theory f (mau/flatten-op theory f term) (get th :id))))
(cond
((empty? els)
(if (= (get th :id) nil) "$EMPTY" (get th :id)))
((empty? (rest els)) (mau/canon theory (first els)))
(else
(let
((cs (map (fn (e) (mau/canon theory e)) els)))
(let
((cs2 (if (get th :comm) (mau/sort-strings cs) cs)))
(str f "(" (join "," cs2) ")"))))))
(if
(get th :comm)
(str
f
"("
(join
","
(mau/sort-strings
(map (fn (e) (mau/canon theory e)) (mau/args term))))
")")
(str
f
"("
(join
","
(map (fn (e) (mau/canon theory e)) (mau/args term)))
")")))))
(else (str term)))))
(define
mau/ac-equal?
(fn (theory a b) (= (mau/canon theory a) (mau/canon theory b))))
;; ---------- variable block bounds ----------
(define
mau/rest-var?
(fn
(name)
(and
(> (len name) 0)
(= (slice name 0 1) "$"))))
(define
mau/var-kmin
(fn
(name id)
(if (or (mau/rest-var? name) (not (= id nil))) 0 1)))
(define
mau/bind-check
(fn
(theory s name val)
(let
((b (get s name)))
(if
(= b nil)
(assoc s name val)
(if (mau/ac-equal? theory b val) s nil)))))
;; ---------- core multi-valued matcher ----------
(define
mau/mm
(fn
(theory pat subj s)
(cond
((mau/var? pat)
(let
((bound (get s (mau/vname pat))))
(if
(= bound nil)
(list (assoc s (mau/vname pat) subj))
(if (mau/ac-equal? theory bound subj) (list s) (list)))))
((mau/app? pat)
(if (mau/app? subj) (mau/mm-app theory pat subj s) (list)))
(else (list)))))
(define
mau/extend-all
(fn
(theory p subj substs)
(mau/concat-map (fn (s) (mau/mm theory p subj s)) substs)))
(define
mau/mm-args
(fn
(theory ps ss substs)
(cond
((and (empty? ps) (empty? ss)) substs)
((or (empty? ps) (empty? ss)) (list))
(else
(mau/mm-args
theory
(rest ps)
(rest ss)
(mau/extend-all theory (first ps) (first ss) substs))))))
(define
mau/mm-comm
(fn
(theory pat subj s)
(let
((p1 (nth (mau/args pat) 0))
(p2 (nth (mau/args pat) 1))
(q1 (nth (mau/args subj) 0))
(q2 (nth (mau/args subj) 1)))
(mau/append2
(mau/mm-args theory (list p1 p2) (list q1 q2) (list s))
(mau/mm-args theory (list p1 p2) (list q2 q1) (list s))))))
(define
mau/mm-assoc
(fn
(theory f pat subj s)
(let
((pels (mau/flatten-op theory f pat))
(sels (mau/flatten-op theory f subj))
(th (mau/th-of theory f)))
(if
(get th :comm)
(mau/match-multiset theory f pels sels s (get th :id))
(mau/match-sequence theory f pels sels s (get th :id))))))
(define
mau/mm-app
(fn
(theory pat subj s)
(let
((f (mau/op pat))
(g (mau/op subj))
(th (mau/th-of theory (mau/op pat))))
(cond
((get th :assoc) (mau/mm-assoc theory f pat subj s))
((get th :comm)
(if
(and
(= f g)
(= (mau/arity pat) 2)
(= (mau/arity subj) 2))
(mau/mm-comm theory pat subj s)
(list)))
(else
(if
(and (= f g) (= (mau/arity pat) (mau/arity subj)))
(mau/mm-args theory (mau/args pat) (mau/args subj) (list s))
(list)))))))
;; ---------- associative (ordered) sequence matching ----------
(define
mau/match-sequence
(fn
(theory f pels sels s id)
(cond
((empty? pels) (if (empty? sels) (list s) (list)))
(else
(let
((p (first pels)) (prest (rest pels)))
(if
(mau/var? p)
(mau/seq-var-loop
theory
f
prest
sels
s
(mau/vname p)
id
(mau/var-kmin (mau/vname p) id))
(if
(empty? sels)
(list)
(mau/concat-map
(fn
(s2)
(mau/match-sequence theory f prest (rest sels) s2 id))
(mau/mm theory p (first sels) s)))))))))
(define
mau/seq-var-loop
(fn
(theory f prest sels s name id k)
(if
(> k (len sels))
(list)
(let
((block (mau/take sels k)) (rests (mau/drop sels k)))
(let
((val (mau/rebuild f block id)))
(let
((s2 (mau/bind-check theory s name val)))
(mau/append2
(if
(= s2 nil)
(list)
(mau/match-sequence theory f prest rests s2 id))
(mau/seq-var-loop
theory
f
prest
sels
s
name
id
(+ k 1)))))))))
;; ---------- associative-commutative (multiset) matching ----------
(define
mau/match-multiset
(fn
(theory f pels sels s id)
(cond
((empty? pels) (if (empty? sels) (list s) (list)))
(else
(let
((p (first pels)) (prest (rest pels)))
(if
(mau/var? p)
(mau/ms-var-splits theory f prest sels s (mau/vname p) id)
(mau/ms-nonvar-loop theory f p prest sels s id 0)))))))
(define
mau/ms-nonvar-loop
(fn
(theory f p prest sels s id i)
(if
(>= i (len sels))
(list)
(let
((elem (nth sels i)) (others (mau/remove-at sels i)))
(mau/append2
(mau/concat-map
(fn (s2) (mau/match-multiset theory f prest others s2 id))
(mau/mm theory p elem s))
(mau/ms-nonvar-loop theory f p prest sels s id (+ i 1)))))))
(define
mau/ms-var-splits
(fn
(theory f prest sels s name id)
(let
((kmin (mau/var-kmin name id)))
(mau/concat-map
(fn
(pair)
(let
((chosen (first pair)) (rests (nth pair 1)))
(if
(< (len chosen) kmin)
(list)
(let
((val (mau/rebuild f chosen id)))
(let
((s2 (mau/bind-check theory s name val)))
(if
(= s2 nil)
(list)
(mau/match-multiset theory f prest rests s2 id)))))))
(mau/all-splits sels)))))
;; ---------- public matching entry ----------
(define
mau/match-all
(fn (m pat subj) (mau/mm (mau/build-theory m) pat subj {})))
;; ---------- AC-aware equational rewriting ----------
(define
mau/restv
(fn
(theory f s name)
(let
((v (get s name)))
(cond
((= v nil) (list))
((and (mau/app? v) (= (mau/op v) "$EMPTY")) (list))
(else (mau/flatten-op theory f v))))))
(define
mau/ac-eq-result
(fn
(theory f th eq s)
(if
(get th :comm)
(mau/ac-build
theory
f
(mau/append2
(mau/flatten-op theory f (mau/subst-apply s (get eq :rhs)))
(mau/restv theory f s "$R"))
(get th :id))
(mau/ac-build
theory
f
(mau/append2
(mau/restv theory f s "$L")
(mau/append2
(mau/flatten-op theory f (mau/subst-apply s (get eq :rhs)))
(mau/restv theory f s "$R")))
(get th :id)))))
;; Walk the candidate matches and return the first rewrite that actually
;; changes the term's canonical form (skips idempotency/identity no-ops).
(define
mau/first-change
(fn
(theory f th eq term matches)
(if
(empty? matches)
nil
(let
((result (mau/ac-eq-result theory f th eq (first matches))))
(if
(mau/ac-equal? theory result term)
(mau/first-change theory f th eq term (rest matches))
result)))))
(define
mau/ac-rewrite-eq
(fn
(theory f th eq term)
(let
((id (get th :id))
(pels (mau/flatten-op theory f (get eq :lhs)))
(sels (mau/flatten-op theory f term)))
(let
((matches (if (get th :comm) (mau/match-multiset theory f (mau/append2 pels (list (mau/var "$R" ""))) sels {} id) (mau/match-sequence theory f (mau/append2 (list (mau/var "$L" "")) (mau/append2 pels (list (mau/var "$R" "")))) sels {} id))))
(mau/first-change theory f th eq term matches)))))
(define
mau/ac-rewrite-top
(fn
(theory eqs term)
(cond
((empty? eqs) nil)
(else
(let
((eq (first eqs)))
(if
(= (get eq :cond) nil)
(let
((lhs (get eq :lhs)))
(let
((th (if (mau/app? lhs) (mau/th-of theory (mau/op lhs)) {:id nil :assoc false :comm false})))
(let
((r (if (and (mau/app? lhs) (get th :assoc)) (mau/ac-rewrite-eq theory (mau/op lhs) th eq term) (let ((ss (mau/mm theory lhs term {}))) (if (empty? ss) nil (mau/subst-apply (first ss) (get eq :rhs)))))))
(cond
((= r nil) (mau/ac-rewrite-top theory (rest eqs) term))
((mau/ac-equal? theory r term)
(mau/ac-rewrite-top theory (rest eqs) term))
(else r)))))
(mau/ac-rewrite-top theory (rest eqs) term)))))))
(define
mau/ac-normalize
(fn
(theory eqs term fuel)
(if
(<= fuel 0)
term
(cond
((mau/var? term) term)
((mau/app? term)
(let
((nargs (map (fn (a) (mau/ac-normalize theory eqs a fuel)) (mau/args term))))
(let
((t2 (mau/app (mau/op term) nargs)))
(let
((r (mau/ac-rewrite-top theory eqs t2)))
(if
(= r nil)
t2
(mau/ac-normalize theory eqs r (- fuel 1)))))))
(else term)))))
(define
mau/ac-reduce
(fn
(m term)
(mau/ac-normalize
(mau/build-theory m)
(mau/module-eqs m)
term
mau/reduce-fuel)))
(define
mau/ac-reduce-term
(fn (m src) (mau/ac-reduce m (mau/parse-term-in m src))))
(define
mau/ac-reduce->str
(fn (m src) (mau/term->str (mau/ac-reduce-term m src))))
(define
mau/ac-canon
(fn (m src) (mau/canon (mau/build-theory m) (mau/ac-reduce-term m src))))

104
lib/maude/meta.sx Normal file
View File

@@ -0,0 +1,104 @@
;; lib/maude/meta.sx — reflection / META-LEVEL (Phase 7).
;;
;; Reflection: a term can be represented AS DATA — another term — and meta-level
;; functions interpret that representation. In Maude this is the META-LEVEL
;; (upTerm/downTerm, metaReduce, metaApply, ...). Here object terms are already
;; SX dicts; the META representation re-encodes a term as a term built from the
;; meta-constructors `mt-var` and `mt-app`, so a represented term is itself a
;; first-class object term you can build, inspect, and transform.
;;
;; up-term(X:S) = mt-var(X, S) (names/sorts as constants)
;; up-term(f(a,b)) = mt-app(f, up(a), up(b))
;; down-term reverses.
;;
;; Meta-operations reflect object-level behaviour: metaReduce of a represented
;; term in a module = the representation of its normal form, etc. The
;; meta-circular law `down(metaReduce(up t)) =AC= reduce t` is exactly the
;; statement that reflection agrees with the object level.
(define
mau/up-term
(fn
(t)
(cond
((mau/var? t)
(mau/app
"mt-var"
(list (mau/const (mau/vname t)) (mau/const (mau/vsort t)))))
((mau/app? t)
(mau/app
"mt-app"
(cons (mau/const (mau/op t)) (map mau/up-term (mau/args t)))))
(else t))))
(define
mau/down-term
(fn
(mt)
(cond
((and (mau/app? mt) (= (mau/op mt) "mt-var"))
(mau/var
(mau/op (nth (mau/args mt) 0))
(mau/op (nth (mau/args mt) 1))))
((and (mau/app? mt) (= (mau/op mt) "mt-app"))
(mau/app
(mau/op (first (mau/args mt)))
(map mau/down-term (rest (mau/args mt)))))
(else mt))))
;; ---- reflective operations (term <-> meta-term) ----
(define
mau/meta-reduce
(fn (m mt) (mau/up-term (mau/creduce m (mau/down-term mt)))))
(define
mau/meta-rewrite
(fn (m mt) (mau/up-term (mau/rewrite m (mau/down-term mt)))))
;; apply a named rule once at the top of the represented term; nil if it can't.
(define
mau/meta-apply
(fn
(m label mt)
(let
((theory (mau/build-theory m)) (eqs (mau/module-eqs m)))
(let
((r (mau/rules-at-top theory eqs (mau/rules-with-label (mau/module-rules m) label) (mau/down-term mt))))
(if
(= r nil)
nil
(mau/up-term (mau/cnormalize theory eqs r mau/reduce-fuel)))))))
;; ---- source-level conveniences ----
(define mau/meta-up (fn (m src) (mau/up-term (mau/parse-term-in m src))))
(define
mau/meta-reduce-src
(fn (m src) (mau/down-term (mau/meta-reduce m (mau/meta-up m src)))))
(define
mau/meta-reduce-canon
(fn (m src) (mau/canon (mau/build-theory m) (mau/meta-reduce-src m src))))
;; ---- generic theorem helper: equational proof by reduction ----
(define
mau/meta-prove-equal?
(fn
(m srcA srcB)
(mau/ac-equal?
(mau/build-theory m)
(mau/creduce-term m srcA)
(mau/creduce-term m srcB))))
;; meta-circular law: down(metaReduce(up t)) =AC= reduce(t)
(define
mau/meta-circular?
(fn
(m src)
(mau/ac-equal?
(mau/build-theory m)
(mau/meta-reduce-src m src)
(mau/creduce-term m src))))

710
lib/maude/parser.sx Normal file
View File

@@ -0,0 +1,710 @@
;; lib/maude/parser.sx — Maude module parser.
;;
;; Consumes lib/guest/lex.sx (whitespace classes) and lib/guest/pratt.sx
;; (operator-table lookup), plus lib/maude/term.sx (term constructors).
;;
;; Maude tokens are whitespace-delimited words plus the bracketing chars
;; ( ) [ ] { } , — so an operator name like _+_ or s_ or if_then_else_fi is a
;; single token. Statements end at a whitespace-delimited "." token.
;;
;; Grammar handled here:
;; (fmod|mod) NAME is ... (endfm|endm)
;; sort/sorts NAMES .
;; subsort/subsorts A B < C < D .
;; op/ops NAMES : ARITY -> RESULT [ATTRS] .
;; var/vars NAMES : SORT .
;; eq LHS = RHS [ATTRS] . ceq LHS = RHS if COND [ATTRS] .
;; rl [L] : LHS => RHS . crl [L] : LHS => RHS if COND .
;;
;; Terms: prefix application f(a,b) (op name may contain underscores, e.g.
;; the prefix form _+_(2,3)); mixfix prefix s_ written `s X`; mixfix infix
;; _+_ written `X + Y`, parsed by precedence climbing over a table built
;; from the op declarations. Infix associativity follows `gather`: (E e)=left
;; (default), (e E)=right (e.g. cons _:_), so `a : b : c` parses right-nested.
;; ---------- tokenizer ----------
(define
mau/special-char?
(fn
(c)
(or
(= c "(")
(= c ")")
(= c "[")
(= c "]")
(= c "{")
(= c "}")
(= c ","))))
(define
mau/tokenize
(fn
(src)
(let
((toks (list)) (pos 0) (n (len src)))
(define
peekc
(fn (o) (if (< (+ pos o) n) (nth src (+ pos o)) nil)))
(define curc (fn () (peekc 0)))
(define adv! (fn (k) (set! pos (+ pos k))))
(define
at-comment?
(fn
()
(or
(and
(= (curc) "-")
(= (peekc 1) "-")
(= (peekc 2) "-"))
(and
(= (curc) "*")
(= (peekc 1) "*")
(= (peekc 2) "*")))))
(define
skip-line!
(fn
()
(when
(and (< pos n) (not (= (curc) "\n")))
(do (adv! 1) (skip-line!)))))
(define
read-word!
(fn
(start)
(do
(when
(and
(< pos n)
(not (lex-whitespace? (curc)))
(not (mau/special-char? (curc))))
(do (adv! 1) (read-word! start)))
(slice src start pos))))
(define
scan!
(fn
()
(cond
((>= pos n) nil)
((lex-whitespace? (curc)) (do (adv! 1) (scan!)))
((at-comment?) (do (skip-line!) (scan!)))
((mau/special-char? (curc))
(do (append! toks (curc)) (adv! 1) (scan!)))
(else (do (append! toks (read-word! pos)) (scan!))))))
(scan!)
toks)))
;; ---------- list helpers ----------
(define
mau/take
(fn
(xs k)
(if
(or (= k 0) (empty? xs))
(list)
(cons (first xs) (mau/take (rest xs) (- k 1))))))
(define
mau/drop
(fn
(xs k)
(if
(or (= k 0) (empty? xs))
xs
(mau/drop (rest xs) (- k 1)))))
(define
mau/append2
(fn
(xs ys)
(if (empty? xs) ys (cons (first xs) (mau/append2 (rest xs) ys)))))
(define
mau/take-until
(fn
(xs tok)
(if
(or (empty? xs) (= (first xs) tok))
(list)
(cons (first xs) (mau/take-until (rest xs) tok)))))
(define
mau/drop-until
(fn
(xs tok)
(cond
((empty? xs) (list))
((= (first xs) tok) xs)
(else (mau/drop-until (rest xs) tok)))))
;; ---------- mixfix classification ----------
(define
mau/op-form
(fn
(name)
(let
((parts (split name "_")))
(cond
((= (len parts) 1) {:kind :const :token name})
((and (= (len parts) 3) (= (nth parts 0) "") (= (nth parts 2) "") (not (= (nth parts 1) "")))
{:kind :infix :token (nth parts 1)})
((and (= (len parts) 2) (not (= (nth parts 0) "")) (= (nth parts 1) ""))
{:kind :prefix :token (nth parts 0)})
((and (= (len parts) 2) (= (nth parts 0) "") (not (= (nth parts 1) "")))
{:kind :postfix :token (nth parts 1)})
(else {:kind :mixfix :token name})))))
(define
mau/default-prec
(fn
(kind)
(cond
((= kind "infix") 41)
((= kind "prefix") 15)
((= kind "postfix") 15)
(else 0))))
(define
mau/op-prec
(fn
(op form)
(let
((p (get (get op :attrs) :prec)))
(if (= p nil) (mau/default-prec (get form :kind)) p))))
;; parse associativity from a gather spec: (E e)=left, (e E)=right.
(define
mau/gather-assoc
(fn
(attrs)
(let
((g (get attrs :gather)))
(if
(or (= g nil) (< (len g) 2))
"left"
(cond
((= (nth g 1) "E") "right")
((= (nth g 0) "E") "left")
(else "left"))))))
(define
mau/build-infix-table
(fn
(ops)
(if
(empty? ops)
(list)
(let
((op (first ops)) (rest-tbl (mau/build-infix-table (rest ops))))
(let
((form (mau/op-form (get op :name))))
(if
(= (get form :kind) "infix")
(cons
(list
(get form :token)
(mau/op-prec op form)
(get op :name)
(mau/gather-assoc (get op :attrs)))
rest-tbl)
rest-tbl))))))
(define
mau/build-prefix-table
(fn
(ops)
(if
(empty? ops)
(list)
(let
((op (first ops)) (rest-tbl (mau/build-prefix-table (rest ops))))
(let
((form (mau/op-form (get op :name))))
(if
(= (get form :kind) "prefix")
(cons
(list (get form :token) (mau/op-prec op form) (get op :name))
rest-tbl)
rest-tbl))))))
;; ---------- term parsing ----------
(define mau/has-colon? (fn (tok) (contains? tok ":")))
(define
mau/atom->term
(fn
(tok vars)
(cond
((mau/has-colon? tok)
(let
((parts (split tok ":")))
(mau/var (nth parts 0) (nth parts 1))))
((not (= (get vars tok) nil)) (mau/var tok (get vars tok)))
(else (mau/const tok)))))
(define
mau/parse-term
(fn
(toks grammar)
(let
((ts toks)
(pos 0)
(n (len toks))
(infix-tbl (get grammar :infix))
(prefix-tbl (get grammar :prefix))
(vars (get grammar :vars))
(prefix-rbp 1000))
(define tcur (fn () (if (< pos n) (nth ts pos) nil)))
(define
tpeek
(fn (o) (if (< (+ pos o) n) (nth ts (+ pos o)) nil)))
(define tadv! (fn () (set! pos (+ pos 1))))
(define
parse-args
(fn
()
(if
(= (tcur) ")")
(do (tadv!) (list))
(let
((acc (list)))
(define
more
(fn
()
(do
(append! acc (parse-expr 0))
(when (= (tcur) ",") (do (tadv!) (more))))))
(do (more) (when (= (tcur) ")") (tadv!)) acc)))))
(define
parse-primary
(fn
()
(let
((t (tcur)))
(cond
((= t "(")
(do
(tadv!)
(let
((e (parse-expr 0)))
(do (when (= (tcur) ")") (tadv!)) e))))
((not (= (pratt-op-lookup prefix-tbl t) nil))
(let
((entry (pratt-op-lookup prefix-tbl t)))
(do
(tadv!)
(let
((operand (parse-expr prefix-rbp)))
(mau/app (nth entry 2) (list operand))))))
((= (tpeek 1) "(")
(let
((name t))
(do (tadv!) (tadv!) (mau/app name (parse-args)))))
(else (do (tadv!) (mau/atom->term t vars)))))))
(define
parse-expr
(fn
(minbp)
(let
((lhs (parse-primary)))
(define
climb
(fn
(acc)
(let
((t (tcur)))
(let
((entry (if (= t nil) nil (pratt-op-lookup infix-tbl t))))
(if
(= entry nil)
acc
(let
((lbp (pratt-op-prec entry)))
(if
(< lbp minbp)
acc
(do
(tadv!)
(let
((rbp (if (= (nth entry 3) "right") lbp (+ lbp 1))))
(let
((rhs (parse-expr rbp)))
(climb
(mau/app
(nth entry 2)
(list acc rhs)))))))))))))
(climb lhs))))
(parse-expr 0))))
;; ---------- statement splitting ----------
(define
mau/split-statements
(fn
(toks)
(let
((stmts (list)) (cur (list)))
(define
flush!
(fn
()
(when
(not (empty? cur))
(do (append! stmts cur) (set! cur (list))))))
(define
loop
(fn
(ts)
(cond
((empty? ts) (flush!))
((= (first ts) ".") (do (flush!) (loop (rest ts))))
(else (do (append! cur (first ts)) (loop (rest ts)))))))
(do (loop toks) stmts))))
(define
mau/split-groups
(fn
(toks)
(let
((groups (list)) (cur (list)))
(define flush! (fn () (do (append! groups cur) (set! cur (list)))))
(define
loop
(fn
(ts)
(cond
((empty? ts) (flush!))
((= (first ts) "<") (do (flush!) (loop (rest ts))))
(else (do (append! cur (first ts)) (loop (rest ts)))))))
(do (loop toks) groups))))
;; ---------- attributes ----------
(define mau/strip-brackets (fn (toks) (mau/take-until (rest toks) "]")))
(define
mau/parse-attr-tokens
(fn
(toks)
(let
((acc {}))
(define
loop
(fn
(ts)
(cond
((empty? ts) nil)
((= (first ts) "assoc")
(do (dict-set! acc :assoc true) (loop (rest ts))))
((= (first ts) "comm")
(do (dict-set! acc :comm true) (loop (rest ts))))
((or (= (first ts) "idem") (= (first ts) "idempotent"))
(do (dict-set! acc :idem true) (loop (rest ts))))
((= (first ts) "ctor")
(do (dict-set! acc :ctor true) (loop (rest ts))))
((= (first ts) "owise")
(do (dict-set! acc :owise true) (loop (rest ts))))
((= (first ts) "id:")
(do
(dict-set! acc :id (nth ts 1))
(loop (mau/drop ts 2))))
((= (first ts) "prec")
(do
(dict-set! acc :prec (parse-number (nth ts 1)))
(loop (mau/drop ts 2))))
((= (first ts) "label")
(do
(dict-set! acc :label (nth ts 1))
(loop (mau/drop ts 2))))
((= (first ts) "gather")
(let
((after2 (mau/drop ts 2)))
(do
(dict-set! acc :gather (mau/take-until after2 ")"))
(loop (rest (mau/drop-until after2 ")"))))))
(else (loop (rest ts))))))
(do (loop toks) acc))))
(define
mau/parse-attrs
(fn
(toks)
(if
(or (empty? toks) (not (= (first toks) "[")))
{}
(mau/parse-attr-tokens (mau/strip-brackets toks)))))
;; Split a token sequence into {:term tokens-before-bracket :attrs parsed}.
(define mau/split-attrs (fn (toks) {:attrs (mau/parse-attrs (mau/drop-until toks "[")) :term (mau/take-until toks "[")}))
;; ---------- signature collection ----------
(define
mau/append-each!
(fn (acc xs) (for-each (fn (x) (append! acc x)) xs)))
(define
mau/register-ops!
(fn
(ops names arity result attrs)
(for-each (fn (nm) (append! ops {:name nm :attrs attrs :arity arity :result result})) names)))
(define
mau/each-set-var!
(fn
(vars names sort)
(for-each (fn (nm) (dict-set! vars nm sort)) names)))
(define
mau/cross-append!
(fn
(acc g1 g2)
(for-each
(fn
(sub)
(for-each (fn (super) (append! acc (list sub super))) g2))
g1)))
(define
mau/add-subsort-chain!
(fn
(acc groups)
(when
(and (not (empty? groups)) (not (empty? (rest groups))))
(do
(mau/cross-append! acc (first groups) (nth groups 1))
(mau/add-subsort-chain! acc (rest groups))))))
(define
mau/add-subsorts!
(fn (acc body) (mau/add-subsort-chain! acc (mau/split-groups body))))
(define
mau/add-vars!
(fn
(vars body)
(let
((names (mau/take-until body ":"))
(sort (first (rest (mau/drop-until body ":")))))
(mau/each-set-var! vars names sort))))
(define
mau/add-ops!
(fn
(ops body)
(let
((names (mau/take-until body ":"))
(afterc (rest (mau/drop-until body ":"))))
(let
((arity (mau/take-until afterc "->"))
(aftera (rest (mau/drop-until afterc "->"))))
(let
((result (first aftera))
(attrs (mau/parse-attrs (mau/drop aftera 1))))
(mau/register-ops! ops names arity result attrs))))))
(define
mau/collect-sig!
(fn
(stmts sorts subsorts ops vars)
(for-each
(fn
(s)
(let
((head (first s)) (body (rest s)))
(cond
((or (= head "sort") (= head "sorts"))
(mau/append-each! sorts body))
((or (= head "subsort") (= head "subsorts"))
(mau/add-subsorts! subsorts body))
((or (= head "op") (= head "ops")) (mau/add-ops! ops body))
((or (= head "var") (= head "vars")) (mau/add-vars! vars body))
(else nil))))
stmts)))
;; ---------- equations / rules ----------
(define
mau/parse-cond
(fn
(toks grammar)
(if
(mau/member? "=" toks)
(let
((l (mau/take-until toks "="))
(r (rest (mau/drop-until toks "="))))
{:lhs (mau/parse-term l grammar) :kind :eq :rhs (mau/parse-term r grammar)})
{:kind :bool :term (mau/parse-term toks grammar)})))
(define
mau/parse-eq
(fn
(body grammar conditional?)
(let
((lhs-toks (mau/take-until body "="))
(after (rest (mau/drop-until body "="))))
(if
conditional?
(let
((rhs-toks (mau/take-until after "if"))
(cond-raw (rest (mau/drop-until after "if"))))
(let ((csplit (mau/split-attrs cond-raw))) {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond (mau/parse-cond (get csplit :term) grammar) :rhs (mau/parse-term rhs-toks grammar) :owise (= (get (get csplit :attrs) :owise) true)}))
(let ((rsplit (mau/split-attrs after))) {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond nil :rhs (mau/parse-term (get rsplit :term) grammar) :owise (= (get (get rsplit :attrs) :owise) true)})))))
(define
mau/strip-label
(fn
(body)
(if
(and (not (empty? body)) (= (first body) "["))
(let
((label (nth body 1)) (after (mau/drop body 3)))
(if
(and (not (empty? after)) (= (first after) ":"))
{:label label :rest (rest after)}
{:label label :rest after}))
{:label nil :rest body})))
(define
mau/parse-rule
(fn
(body grammar conditional?)
(let
((b (mau/strip-label body)))
(let
((label (get b :label)) (rest-toks (get b :rest)))
(let
((lhs-toks (mau/take-until rest-toks "=>"))
(after (rest (mau/drop-until rest-toks "=>"))))
(if
conditional?
(let
((rhs-toks (mau/take-until after "if"))
(cond-toks (rest (mau/drop-until after "if"))))
{:lhs (mau/parse-term lhs-toks grammar) :label label :t :rule :cond (mau/parse-cond (get (mau/split-attrs cond-toks) :term) grammar) :rhs (mau/parse-term rhs-toks grammar)})
{:lhs (mau/parse-term lhs-toks grammar) :label label :t :rule :cond nil :rhs (mau/parse-term (get (mau/split-attrs after) :term) grammar)}))))))
(define
mau/collect-rules!
(fn
(stmts grammar eqs rules)
(for-each
(fn
(s)
(let
((head (first s)) (body (rest s)))
(cond
((= head "eq") (append! eqs (mau/parse-eq body grammar false)))
((= head "ceq") (append! eqs (mau/parse-eq body grammar true)))
((= head "rl")
(append! rules (mau/parse-rule body grammar false)))
((= head "crl")
(append! rules (mau/parse-rule body grammar true)))
(else nil))))
stmts)))
;; ---------- module assembly ----------
(define mau/make-grammar (fn (ops vars) {:prefix (mau/build-prefix-table ops) :ops ops :vars vars :infix (mau/build-infix-table ops)}))
(define
mau/build-module
(fn
(kind name body)
(let
((stmts (mau/split-statements body))
(sorts (list))
(subsorts (list))
(ops (list))
(vars {})
(eqs (list))
(rules (list)))
(mau/collect-sig! stmts sorts subsorts ops vars)
(let
((grammar (mau/make-grammar ops vars)))
(mau/collect-rules! stmts grammar eqs rules)
{:name name :grammar grammar :sorts sorts :eqs eqs :ops ops :t :module :vars vars :subsorts subsorts :kind kind :rules rules}))))
(define
mau/parse-module
(fn
(src)
(let
((toks (mau/tokenize src)))
(let
((kind (nth toks 0)) (name (nth toks 1)))
(let
((body (mau/take (mau/drop toks 3) (- (len toks) 4))))
(mau/build-module kind name body))))))
;; ---------- signature queries ----------
(define mau/module-name (fn (m) (get m :name)))
(define mau/module-kind (fn (m) (get m :kind)))
(define mau/module-sorts (fn (m) (get m :sorts)))
(define mau/module-subsorts (fn (m) (get m :subsorts)))
(define mau/module-ops (fn (m) (get m :ops)))
(define mau/module-vars (fn (m) (get m :vars)))
(define mau/module-eqs (fn (m) (get m :eqs)))
(define mau/module-rules (fn (m) (get m :rules)))
(define mau/module-grammar (fn (m) (get m :grammar)))
(define
mau/parse-term-in
(fn (m src) (mau/parse-term (mau/tokenize src) (mau/module-grammar m))))
(define
mau/collect-supers
(fn
(pairs s)
(cond
((empty? pairs) (list))
((= (first (first pairs)) s)
(cons
(nth (first pairs) 1)
(mau/collect-supers (rest pairs) s)))
(else (mau/collect-supers (rest pairs) s)))))
(define mau/supers-of (fn (m s) (mau/collect-supers (get m :subsorts) s)))
(define
mau/dfs-reach
(fn
(m frontier target seen)
(cond
((empty? frontier) false)
((= (first frontier) target) true)
((mau/member? (first frontier) seen)
(mau/dfs-reach m (rest frontier) target seen))
(else
(mau/dfs-reach
m
(mau/append2 (mau/supers-of m (first frontier)) (rest frontier))
target
(cons (first frontier) seen))))))
(define
mau/subsort?
(fn
(m sub super)
(mau/dfs-reach m (mau/supers-of m sub) super (list sub))))
(define mau/sort<=? (fn (m a b) (or (= a b) (mau/subsort? m a b))))
(define
mau/filter-ops
(fn
(ops name)
(cond
((empty? ops) (list))
((= (get (first ops) :name) name)
(cons (first ops) (mau/filter-ops (rest ops) name)))
(else (mau/filter-ops (rest ops) name)))))
(define
mau/ops-named
(fn (m name) (mau/filter-ops (mau/module-ops m) name)))

82
lib/maude/pretty.sx Normal file
View File

@@ -0,0 +1,82 @@
;; lib/maude/pretty.sx — mixfix surface-syntax printer.
;;
;; term->str renders the internal prefix form (`_+_(s_(X), 0)`); this renders
;; terms back in Maude mixfix surface syntax (`((s X) + 0)`), driven by the
;; operator forms in the module signature. Fully parenthesised — unambiguous
;; rather than minimal. Constants and unknown ops fall back to prefix form.
(define
mau/render-forms
(fn
(m)
(let
((tbl {}))
(for-each
(fn
(op)
(dict-set! tbl (get op :name) (mau/op-form (get op :name))))
(mau/module-ops m))
tbl)))
(define
mau/render-args
(fn
(forms args)
(cond
((empty? args) "")
((empty? (rest args)) (mau/render-term forms (first args)))
(else
(str
(mau/render-term forms (first args))
", "
(mau/render-args forms (rest args)))))))
(define
mau/render-term
(fn
(forms t)
(cond
((mau/var? t) (mau/vname t))
((mau/app? t)
(let
((form (get forms (mau/op t))) (args (mau/args t)))
(cond
((empty? args) (mau/op t))
((and form (= (get form :kind) "infix") (= (len args) 2))
(str
"("
(mau/render-term forms (nth args 0))
" "
(get form :token)
" "
(mau/render-term forms (nth args 1))
")"))
((and form (= (get form :kind) "prefix") (= (len args) 1))
(str
"("
(get form :token)
" "
(mau/render-term forms (first args))
")"))
((and form (= (get form :kind) "postfix") (= (len args) 1))
(str
"("
(mau/render-term forms (first args))
" "
(get form :token)
")"))
(else (str (mau/op t) "(" (mau/render-args forms args) ")")))))
(else (str t)))))
(define
mau/term->maude
(fn (m t) (mau/render-term (mau/render-forms m) t)))
;; reduce / rewrite then render in surface syntax
(define
mau/red->maude
(fn (m src) (mau/term->maude m (mau/creduce-term m src))))
(define
mau/rew->maude
(fn (m src) (mau/term->maude m (mau/rewrite-term m src))))

143
lib/maude/reduce.sx Normal file
View File

@@ -0,0 +1,143 @@
;; lib/maude/reduce.sx — syntactic equational reduction (Phase 2).
;;
;; Apply unconditional equations left-to-right to a fixpoint, using strict
;; one-sided syntactic matching (no theories yet — assoc/comm/id come in
;; Phase 3). Reduction is innermost: arguments are normalised before the
;; enclosing operator is rewritten.
;;
;; A substitution is a dict VAR-NAME -> term, extended immutably via `assoc`.
;; Matching is one-sided: only the pattern (equation LHS) carries variables;
;; the subject is treated structurally.
;; ---------- matching ----------
(define
mau/match
(fn
(pat subj s)
(cond
((= s nil) nil)
((mau/var? pat)
(let
((bound (get s (mau/vname pat))))
(if
(= bound nil)
(assoc s (mau/vname pat) subj)
(if (mau/term=? bound subj) s nil))))
((and (mau/app? pat) (mau/app? subj))
(if
(and
(= (mau/op pat) (mau/op subj))
(= (mau/arity pat) (mau/arity subj)))
(mau/match-args (mau/args pat) (mau/args subj) s)
nil))
(else nil))))
(define
mau/match-args
(fn
(ps ss s)
(cond
((= s nil) nil)
((and (empty? ps) (empty? ss)) s)
((or (empty? ps) (empty? ss)) nil)
(else
(mau/match-args
(rest ps)
(rest ss)
(mau/match (first ps) (first ss) s))))))
;; ---------- substitution application ----------
(define
mau/subst-apply-list
(fn
(s args)
(if
(empty? args)
(list)
(cons
(mau/subst-apply s (first args))
(mau/subst-apply-list s (rest args))))))
(define
mau/subst-apply
(fn
(s term)
(cond
((mau/var? term)
(let ((b (get s (mau/vname term)))) (if (= b nil) term b)))
((mau/app? term)
(mau/app (mau/op term) (mau/subst-apply-list s (mau/args term))))
(else term))))
;; ---------- top-level rewrite ----------
;; Try each unconditional equation in order; on the first whose LHS matches
;; the term, return the instantiated RHS. nil if none apply.
(define
mau/rewrite-top
(fn
(eqs term)
(cond
((empty? eqs) nil)
(else
(let
((eq (first eqs)))
(if
(= (get eq :cond) nil)
(let
((s (mau/match (get eq :lhs) term {})))
(if
(= s nil)
(mau/rewrite-top (rest eqs) term)
(mau/subst-apply s (get eq :rhs))))
(mau/rewrite-top (rest eqs) term)))))))
;; ---------- normalisation (innermost to fixpoint) ----------
(define
mau/normalize-args
(fn
(eqs args fuel)
(if
(empty? args)
(list)
(cons
(mau/normalize eqs (first args) fuel)
(mau/normalize-args eqs (rest args) fuel)))))
(define
mau/normalize
(fn
(eqs term fuel)
(if
(<= fuel 0)
term
(cond
((mau/var? term) term)
((mau/app? term)
(let
((nargs (mau/normalize-args eqs (mau/args term) fuel)))
(let
((t2 (mau/app (mau/op term) nargs)))
(let
((r (mau/rewrite-top eqs t2)))
(if (= r nil) t2 (mau/normalize eqs r (- fuel 1)))))))
(else term)))))
;; ---------- module-level API ----------
(define mau/reduce-fuel 1000000)
(define
mau/reduce
(fn (m term) (mau/normalize (mau/module-eqs m) term mau/reduce-fuel)))
(define
mau/reduce-term
(fn (m src) (mau/reduce m (mau/parse-term-in m src))))
(define
mau/reduce->str
(fn (m src) (mau/term->str (mau/reduce-term m src))))

284
lib/maude/rewrite.sx Normal file
View File

@@ -0,0 +1,284 @@
;; lib/maude/rewrite.sx — system modules + rewrite rules (Phase 5).
;;
;; Equations (eq/ceq) are applied to a fixpoint to NORMALISE (confluent by
;; intent). Rules (rl/crl) are TRANSITIONS: asymmetric (=>), possibly
;; nondeterministic, NOT applied to a fixpoint. Maude's `rew` interleaves
;; the two: normalise with equations, fire one rule, renormalise, repeat.
;;
;; Rule firing reuses the shared firing machinery — a rule dict carries
;; :lhs/:rhs/:cond exactly like an equation, so `mau/fire-eq` (short-circuit,
;; fire.sx) applies unchanged (matching modulo the AC theory; crl guards
;; evaluated with the equations). A rule fires only if it both progresses and
;; its condition holds.
;;
;; `mau/rewrite` follows the default strategy (top-down, leftmost-outermost,
;; first applicable rule) for one path. `mau/search` does breadth-first reach
;; over ALL one-step successors — for puzzle solvers / protocol simulators
;; where the answer is on a branch `rew` would not take.
(define mau/rew-fuel 100000)
;; ---- single-step, default strategy (first applicable, leftmost-outermost) ----
(define
mau/rules-at-top
(fn
(theory eqs rules term)
(if
(empty? rules)
nil
(let
((r (mau/fire-eq theory eqs (first rules) term)))
(if (= r nil) (mau/rules-at-top theory eqs (rest rules) term) r)))))
(define
mau/apply-rule-once
(fn
(theory eqs rules term)
(let
((top (mau/rules-at-top theory eqs rules term)))
(if
(not (= top nil))
top
(if
(mau/app? term)
(mau/apply-rule-in-args
theory
eqs
rules
(mau/op term)
(mau/args term)
(list))
nil)))))
(define
mau/apply-rule-in-args
(fn
(theory eqs rules op done todo)
(if
(empty? todo)
nil
(let
((r (mau/apply-rule-once theory eqs rules (first todo))))
(if
(= r nil)
(mau/apply-rule-in-args
theory
eqs
rules
op
(mau/append2 done (list (first todo)))
(rest todo))
(mau/app op (mau/append2 done (cons r (rest todo)))))))))
(define
mau/rewrite-steps
(fn
(theory eqs rules term steps)
(if
(<= steps 0)
(mau/cnormalize theory eqs term mau/reduce-fuel)
(let
((nf (mau/cnormalize theory eqs term mau/reduce-fuel)))
(let
((r (mau/apply-rule-once theory eqs rules nf)))
(if
(= r nil)
nf
(mau/rewrite-steps theory eqs rules r (- steps 1))))))))
(define
mau/rewrite
(fn
(m term)
(mau/rewrite-steps
(mau/build-theory m)
(mau/module-eqs m)
(mau/module-rules m)
term
mau/rew-fuel)))
(define
mau/rew
(fn
(m src n)
(mau/rewrite-steps
(mau/build-theory m)
(mau/module-eqs m)
(mau/module-rules m)
(mau/parse-term-in m src)
n)))
(define
mau/rewrite-term
(fn (m src) (mau/rewrite m (mau/parse-term-in m src))))
(define
mau/rewrite->str
(fn (m src) (mau/term->str (mau/rewrite-term m src))))
(define
mau/rewrite-canon
(fn (m src) (mau/canon (mau/build-theory m) (mau/rewrite-term m src))))
(define mau/rew->str (fn (m src n) (mau/term->str (mau/rew m src n))))
(define
mau/rew-canon
(fn (m src n) (mau/canon (mau/build-theory m) (mau/rew m src n))))
;; ---- all one-step successors (for search; eager enumeration) ----
(define
mau/cands-results
(fn
(theory eqs cond term cands)
(mau/concat-map
(fn
(c)
(if
(and
(not (mau/ac-equal? theory (get c :result) term))
(mau/cond-holds? theory eqs cond (get c :s)))
(list (mau/cnormalize theory eqs (get c :result) mau/reduce-fuel))
(list)))
cands)))
(define
mau/top-successors
(fn
(theory eqs rules term)
(mau/concat-map
(fn
(rule)
(mau/cands-results
theory
eqs
(get rule :cond)
term
(mau/eq-candidates theory rule term)))
rules)))
(define
mau/arg-successors
(fn
(theory eqs rules op done todo)
(if
(empty? todo)
(list)
(mau/append2
(map
(fn
(sub)
(mau/app op (mau/append2 done (cons sub (rest todo)))))
(mau/all-successors theory eqs rules (first todo)))
(mau/arg-successors
theory
eqs
rules
op
(mau/append2 done (list (first todo)))
(rest todo))))))
(define
mau/all-successors
(fn
(theory eqs rules term)
(mau/append2
(mau/top-successors theory eqs rules term)
(if
(mau/app? term)
(mau/arg-successors
theory
eqs
rules
(mau/op term)
(mau/args term)
(list))
(list)))))
(define
mau/successors
(fn
(m src)
(let
((theory (mau/build-theory m)) (eqs (mau/module-eqs m)))
(map
(fn (t) (mau/canon theory t))
(mau/all-successors
theory
eqs
(mau/module-rules m)
(mau/cnormalize
theory
eqs
(mau/parse-term-in m src)
mau/reduce-fuel))))))
;; ---- breadth-first reachability search ----
(define
mau/canon-list
(fn (theory ts) (map (fn (t) (mau/canon theory t)) ts)))
(define
mau/bfs-search
(fn
(theory eqs rules frontier seen goal depth)
(cond
((mau/member? goal (mau/canon-list theory frontier)) true)
((<= depth 0) false)
((empty? frontier) false)
(else
(let
((newf (list)) (newseen seen))
(for-each
(fn
(t)
(for-each
(fn
(succ)
(let
((c (mau/canon theory succ)))
(when
(not (mau/member? c newseen))
(do
(set! newseen (cons c newseen))
(append! newf succ)))))
(mau/all-successors theory eqs rules t)))
frontier)
(mau/bfs-search
theory
eqs
rules
newf
newseen
goal
(- depth 1)))))))
(define
mau/search
(fn
(m start-src goal-src max-depth)
(let
((theory (mau/build-theory m))
(eqs (mau/module-eqs m))
(rules (mau/module-rules m)))
(let
((start (mau/cnormalize theory eqs (mau/parse-term-in m start-src) mau/reduce-fuel))
(goal
(mau/canon
theory
(mau/cnormalize
theory
eqs
(mau/parse-term-in m goal-src)
mau/reduce-fuel))))
(mau/bfs-search
theory
eqs
rules
(list start)
(list (mau/canon theory start))
goal
max-depth)))))

132
lib/maude/run.sx Normal file
View File

@@ -0,0 +1,132 @@
;; lib/maude/run.sx — run a Maude program: a module followed by commands.
;;
;; Parses a single fmod/mod ... endfm/endm module plus trailing commands and
;; executes them, Maude-style:
;; reduce TERM . (alias: red) — normalise with equations
;; rewrite TERM . (alias: rew) — apply rules under the default strategy
;; search START =>* GOAL . — reachability (=>*, =>+, =>! all treated
;; as reachability); reports the path
;; `... in MODNAME : TERM .` is accepted (the module qualifier is ignored —
;; there is one module in scope). reduce/rewrite results carry the least sort,
;; rendered Maude-style by mau/run-pretty as `result SORT: TERM`.
(define mau/search-depth 200)
(define
mau/module-end-idx
(fn
(toks i)
(cond
((>= i (len toks)) (- 0 1))
((or (= (nth toks i) "endfm") (= (nth toks i) "endm")) i)
(else (mau/module-end-idx toks (+ i 1))))))
(define
mau/parse-module-from-toks
(fn
(toks)
(let
((kind (nth toks 0)) (name (nth toks 1)))
(mau/build-module
kind
name
(mau/take (mau/drop toks 3) (- (len toks) 4))))))
(define
mau/strip-in
(fn
(toks)
(if
(and (not (empty? toks)) (= (first toks) "in"))
(rest (mau/drop-until toks ":"))
toks)))
(define
mau/find-arrow
(fn
(toks)
(cond
((empty? toks) nil)
((and (>= (len (first toks)) 2) (= (slice (first toks) 0 2) "=>"))
(first toks))
(else (mau/find-arrow (rest toks))))))
(define
mau/run-search
(fn
(m term-toks)
(let
((arrow (mau/find-arrow term-toks)) (g (mau/module-grammar m)))
(if
(= arrow nil)
{:path nil :cmd "search" :result "no arrow"}
(let
((start-toks (mau/take-until term-toks arrow))
(goal-toks (rest (mau/drop-until term-toks arrow))))
(let
((path (mau/search-path-terms m (mau/parse-term start-toks g) (mau/parse-term goal-toks g) mau/search-depth)))
{:path path :cmd "search" :result (if (= path nil) "no solution" (join " => " path))}))))))
(define
mau/run-command
(fn
(m stmt)
(let
((head (first stmt)))
(if
(or (= head "search") (= head "srch"))
(mau/run-search m (rest stmt))
(let
((t (mau/parse-term (mau/strip-in (rest stmt)) (mau/module-grammar m))))
(cond
((or (= head "reduce") (= head "red"))
(let ((r (mau/creduce m t))) {:cmd "reduce" :sort (mau/term-sort m r) :result (mau/term->maude m r)}))
((or (= head "rewrite") (= head "rew"))
(let ((r (mau/rewrite m t))) {:cmd "rewrite" :sort (mau/term-sort m r) :result (mau/term->maude m r)}))
(else {:cmd head :result "?"})))))))
(define
mau/run-commands
(fn
(m stmts)
(if
(empty? stmts)
(list)
(if
(empty? (first stmts))
(mau/run-commands m (rest stmts))
(cons
(mau/run-command m (first stmts))
(mau/run-commands m (rest stmts)))))))
(define
mau/run-program
(fn
(src)
(let
((toks (mau/tokenize src)))
(let
((eidx (mau/module-end-idx toks 0)))
(let
((m (mau/parse-module-from-toks (mau/take toks (+ eidx 1))))
(cmd-toks (mau/drop toks (+ eidx 1))))
(mau/run-commands m (mau/split-statements cmd-toks)))))))
;; just the rendered result strings
(define
mau/run
(fn (src) (map (fn (r) (get r :result)) (mau/run-program src))))
;; Maude-style printout: `result SORT: TERM` for reduce/rewrite, the path for search
(define
mau/run-pretty
(fn
(src)
(map
(fn
(r)
(if
(= (get r :cmd) "search")
(str "search: " (get r :result))
(str "result " (get r :sort) ": " (get r :result))))
(mau/run-program src))))

24
lib/maude/scoreboard.json Normal file
View File

@@ -0,0 +1,24 @@
{
"lang": "maude",
"total_passed": 274,
"total_failed": 0,
"total": 274,
"suites": [
{"name":"parse","passed":65,"failed":0,"total":65},
{"name":"reduce","passed":26,"failed":0,"total":26},
{"name":"matching","passed":28,"failed":0,"total":28},
{"name":"confluence","passed":12,"failed":0,"total":12},
{"name":"conditional","passed":19,"failed":0,"total":19},
{"name":"owise","passed":8,"failed":0,"total":8},
{"name":"gather","passed":7,"failed":0,"total":7},
{"name":"sorts","passed":14,"failed":0,"total":14},
{"name":"rewrite","passed":21,"failed":0,"total":21},
{"name":"searchpath","passed":8,"failed":0,"total":8},
{"name":"strategy","passed":19,"failed":0,"total":19},
{"name":"meta","passed":18,"failed":0,"total":18},
{"name":"pretty","passed":11,"failed":0,"total":11},
{"name":"run","passed":10,"failed":0,"total":10},
{"name":"effects","passed":8,"failed":0,"total":8}
],
"generated": "2026-06-07T20:18:07+00:00"
}

21
lib/maude/scoreboard.md Normal file
View File

@@ -0,0 +1,21 @@
# maude scoreboard
**274 / 274 passing** (0 failure(s)).
| Suite | Passed | Total | Status |
|-------|--------|-------|--------|
| parse | 65 | 65 | ok |
| reduce | 26 | 26 | ok |
| matching | 28 | 28 | ok |
| confluence | 12 | 12 | ok |
| conditional | 19 | 19 | ok |
| owise | 8 | 8 | ok |
| gather | 7 | 7 | ok |
| sorts | 14 | 14 | ok |
| rewrite | 21 | 21 | ok |
| searchpath | 8 | 8 | ok |
| strategy | 19 | 19 | ok |
| meta | 18 | 18 | ok |
| pretty | 11 | 11 | ok |
| run | 10 | 10 | ok |
| effects | 8 | 8 | ok |

103
lib/maude/searchpath.sx Normal file
View File

@@ -0,0 +1,103 @@
;; lib/maude/searchpath.sx — reachability search returning the witness path.
;;
;; mau/search (rewrite.sx) answers yes/no. For puzzle solvers you want the
;; actual sequence of states from start to goal. mau/search-path runs the same
;; BFS but threads the path so far; it returns the list of canonical states
;; start..goal (shortest by step count) or nil if unreachable within depth.
(define mau/reverse2 (fn (xs) (mau/rev-acc xs (list))))
(define
mau/rev-acc
(fn
(xs acc)
(if (empty? xs) acc (mau/rev-acc (rest xs) (cons (first xs) acc)))))
;; find a frontier path whose current state (its head) matches the goal canon
(define
mau/path-hit
(fn
(theory frontier goal)
(cond
((empty? frontier) nil)
((= (mau/canon theory (first (first frontier))) goal)
(first frontier))
(else (mau/path-hit theory (rest frontier) goal)))))
(define
mau/bfs-path
(fn
(theory eqs rules frontier seen goal depth)
(let
((hit (mau/path-hit theory frontier goal)))
(cond
((not (= hit nil)) hit)
((<= depth 0) nil)
((empty? frontier) nil)
(else
(let
((newf (list)) (newseen seen))
(for-each
(fn
(path)
(for-each
(fn
(succ)
(let
((c (mau/canon theory succ)))
(when
(not (mau/member? c newseen))
(do
(set! newseen (cons c newseen))
(append! newf (cons succ path))))))
(mau/all-successors theory eqs rules (first path))))
frontier)
(mau/bfs-path
theory
eqs
rules
newf
newseen
goal
(- depth 1))))))))
;; term-level: returns the canonical-state path start..goal, or nil
(define
mau/search-path-terms
(fn
(m start-term goal-term max-depth)
(let
((theory (mau/build-theory m))
(eqs (mau/module-eqs m))
(rules (mau/module-rules m)))
(let
((start (mau/cnormalize theory eqs start-term mau/reduce-fuel))
(goal
(mau/canon
theory
(mau/cnormalize theory eqs goal-term mau/reduce-fuel))))
(let
((res (mau/bfs-path theory eqs rules (list (list start)) (list (mau/canon theory start)) goal max-depth)))
(if
(= res nil)
nil
(map (fn (t) (mau/canon theory t)) (mau/reverse2 res))))))))
(define
mau/search-path
(fn
(m start-src goal-src max-depth)
(mau/search-path-terms
m
(mau/parse-term-in m start-src)
(mau/parse-term-in m goal-src)
max-depth)))
;; number of steps in the shortest solution (nil if unreachable)
(define
mau/search-length
(fn
(m start-src goal-src max-depth)
(let
((p (mau/search-path m start-src goal-src max-depth)))
(if (= p nil) nil (- (len p) 1)))))

87
lib/maude/sorts.sx Normal file
View File

@@ -0,0 +1,87 @@
;; lib/maude/sorts.sx — order-sorted least-sort inference.
;;
;; Order-sorted signatures: subsorts induce a partial order on sorts, and an
;; overloaded operator can have several declarations. The LEAST SORT of a term
;; is the smallest result sort among the operator declarations whose argument
;; sorts the actual arguments satisfy (modulo subsorting). This is what lets
;; `f(1)` be a NzNat while `f(s 0)` is only a Nat when f is declared at both.
;;
;; mau/term-sort M T -> least sort of T (string, "?" if unknown)
;; mau/has-sort? M T SORT -> does T's least sort fit under SORT?
(define
mau/arg-sorts-ok?
(fn
(m argsorts declared)
(cond
((and (empty? argsorts) (empty? declared)) true)
((or (empty? argsorts) (empty? declared)) false)
((mau/sort<=? m (first argsorts) (first declared))
(mau/arg-sorts-ok? m (rest argsorts) (rest declared)))
(else false))))
(define
mau/matching-ops
(fn
(m name argsorts)
(filter
(fn
(op)
(and
(= (len (get op :arity)) (len argsorts))
(mau/arg-sorts-ok? m argsorts (get op :arity))))
(mau/ops-named m name))))
(define
mau/least-loop
(fn
(m best rst)
(cond
((empty? rst) best)
((mau/sort<=? m (first rst) best)
(mau/least-loop m (first rst) (rest rst)))
(else (mau/least-loop m best (rest rst))))))
(define
mau/least-sort
(fn
(m sorts)
(if (empty? sorts) "?" (mau/least-loop m (first sorts) (rest sorts)))))
(define
mau/result-sort
(fn
(m name argsorts)
(let
((cands (mau/matching-ops m name argsorts)))
(if
(empty? cands)
(let
((any (mau/ops-named m name)))
(if (empty? any) "?" (get (first any) :result)))
(mau/least-sort m (map (fn (op) (get op :result)) cands))))))
(define
mau/term-sort
(fn
(m t)
(cond
((mau/var? t) (mau/vsort t))
((mau/app? t)
(mau/result-sort
m
(mau/op t)
(map (fn (a) (mau/term-sort m a)) (mau/args t))))
(else "?"))))
(define
mau/term-sort-src
(fn (m src) (mau/term-sort m (mau/parse-term-in m src))))
(define
mau/has-sort?
(fn (m t sort) (mau/sort<=? m (mau/term-sort m t) sort)))
(define
mau/has-sort-src?
(fn (m src sort) (mau/has-sort? m (mau/parse-term-in m src) sort)))

217
lib/maude/strategy.sx Normal file
View File

@@ -0,0 +1,217 @@
;; lib/maude/strategy.sx — strategy language (Phase 6).
;;
;; A strategy controls HOW rules are applied. Strategies are first-class values
;; (tagged dicts) and SET-VALUED: applying a strategy to a term yields the set
;; (deduped by canonical form) of result terms. The same rule set under
;; different strategies computes different things — `;` sequences, `|` unions,
;; `*`/`+` iterate, `!` normalises.
;;
;; Constructors:
;; (mau/s-idle) identity (the term itself)
;; (mau/s-fail) empty set
;; (mau/s-all) apply any rule once, anywhere
;; (mau/s-rule LABEL) apply a named rule once, anywhere
;; (mau/s-seq A B) A ; B (apply B to every result of A)
;; (mau/s-alt A B) A | B (union of results)
;; (mau/s-star A) A * (reflexive-transitive closure)
;; (mau/s-plus A) A + (one or more)
;; (mau/s-bang A) A ! (normal forms: results where A can't apply)
;; (mau/s-name N) look up named strategy N in the env
;;
;; Run with (mau/srun M STRATS STRAT SRC): STRATS is a dict NAME -> strategy.
(define mau/s-idle (fn () {:s :idle}))
(define mau/s-fail (fn () {:s :fail}))
(define mau/s-all (fn () {:s :all}))
(define mau/s-rule (fn (label) {:label label :s :rule}))
(define mau/s-seq (fn (a b) {:a a :b b :s :seq}))
(define mau/s-alt (fn (a b) {:a a :b b :s :alt}))
(define mau/s-star (fn (a) {:a a :s :star}))
(define mau/s-plus (fn (a) {:a a :s :plus}))
(define mau/s-bang (fn (a) {:a a :s :bang}))
(define mau/s-name (fn (n) {:n n :s :name}))
(define
mau/rules-with-label
(fn (rules label) (filter (fn (r) (= (get r :label) label)) rules)))
(define
mau/dedup-loop
(fn
(theory ts seen acc)
(if
(empty? ts)
acc
(let
((c (mau/canon theory (first ts))))
(if
(mau/member? c seen)
(mau/dedup-loop theory (rest ts) seen acc)
(mau/dedup-loop
theory
(rest ts)
(cons c seen)
(mau/append2 acc (list (first ts)))))))))
(define
mau/dedup-canon
(fn (theory ts) (mau/dedup-loop theory ts (list) (list))))
;; ---- strategy interpreter ----
(define
mau/sapply
(fn
(ctx strat term)
(let
((k (get strat :s)) (theory (get ctx :theory)))
(cond
((= k "idle") (list term))
((= k "fail") (list))
((= k "all")
(mau/dedup-canon
theory
(mau/all-successors theory (get ctx :eqs) (get ctx :rules) term)))
((= k "rule")
(mau/dedup-canon
theory
(mau/all-successors
theory
(get ctx :eqs)
(mau/rules-with-label (get ctx :rules) (get strat :label))
term)))
((= k "seq")
(mau/dedup-canon
theory
(mau/concat-map
(fn (t) (mau/sapply ctx (get strat :b) t))
(mau/sapply ctx (get strat :a) term))))
((= k "alt")
(mau/dedup-canon
theory
(mau/append2
(mau/sapply ctx (get strat :a) term)
(mau/sapply ctx (get strat :b) term))))
((= k "star") (mau/sstar ctx (get strat :a) term))
((= k "plus")
(mau/dedup-canon
theory
(mau/concat-map
(fn (t) (mau/sstar ctx (get strat :a) t))
(mau/sapply ctx (get strat :a) term))))
((= k "bang")
(mau/dedup-canon theory (mau/sbang ctx (get strat :a) term)))
((= k "name")
(mau/sapply ctx (get (get ctx :strats) (get strat :n)) term))
(else (list))))))
;; reflexive-transitive closure: term plus everything reachable via A
(define
mau/sstar
(fn
(ctx a term)
(mau/sstar-loop
ctx
a
(list term)
(list (mau/canon (get ctx :theory) term))
(list term))))
(define
mau/sstar-loop
(fn
(ctx a frontier seen acc)
(if
(empty? frontier)
acc
(let
((newf (list))
(newseen seen)
(newacc acc)
(theory (get ctx :theory)))
(for-each
(fn
(t)
(for-each
(fn
(succ)
(let
((c (mau/canon theory succ)))
(when
(not (mau/member? c newseen))
(do
(set! newseen (cons c newseen))
(append! newf succ)
(append! newacc succ)))))
(mau/sapply ctx a t)))
frontier)
(mau/sstar-loop ctx a newf newseen newacc)))))
;; normal forms: terms reachable via A where A yields nothing more
(define
mau/sbang
(fn
(ctx a term)
(mau/sbang-loop
ctx
a
(list term)
(list (mau/canon (get ctx :theory) term))
(list))))
(define
mau/sbang-loop
(fn
(ctx a frontier seen acc)
(if
(empty? frontier)
acc
(let
((newf (list))
(newseen seen)
(newacc acc)
(theory (get ctx :theory)))
(for-each
(fn
(t)
(let
((succs (mau/sapply ctx a t)))
(if
(empty? succs)
(append! newacc t)
(for-each
(fn
(succ)
(let
((c (mau/canon theory succ)))
(when
(not (mau/member? c newseen))
(do
(set! newseen (cons c newseen))
(append! newf succ)))))
succs))))
frontier)
(mau/sbang-loop ctx a newf newseen newacc)))))
;; ---- public API ----
(define mau/make-sctx (fn (m strats) {:eqs (mau/module-eqs m) :theory (mau/build-theory m) :strats strats :rules (mau/module-rules m)}))
(define
mau/srun
(fn
(m strats strat src)
(let
((ctx (mau/make-sctx m strats)))
(let
((t0 (mau/cnormalize (get ctx :theory) (get ctx :eqs) (mau/parse-term-in m src) mau/reduce-fuel)))
(mau/dedup-canon (get ctx :theory) (mau/sapply ctx strat t0))))))
(define
mau/srun-canon
(fn
(m strats strat src)
(let
((theory (mau/build-theory m)))
(mau/sort-strings
(map (fn (t) (mau/canon theory t)) (mau/srun m strats strat src))))))

114
lib/maude/term.sx Normal file
View File

@@ -0,0 +1,114 @@
;; lib/maude/term.sx — Maude term representation.
;;
;; A term is one of:
;; variable {:t :var :name "X" :sort "Nat"}
;; application {:t :app :op "_+_" :args (a b ...)} (constant: empty args)
;;
;; Sorts attach to variables; operator/result sorts live on op declarations
;; in the module signature, not on the term node. Overloading is resolved at
;; reduction time, so the parser only records the operator name.
(define mau/var (fn (name sort) {:name name :t :var :sort sort}))
(define mau/app (fn (op args) {:op op :t :app :args args}))
(define mau/const (fn (op) {:op op :t :app :args (list)}))
(define mau/var? (fn (t) (and (dict? t) (= (get t :t) "var"))))
(define mau/app? (fn (t) (and (dict? t) (= (get t :t) "app"))))
(define mau/term? (fn (t) (or (mau/var? t) (mau/app? t))))
(define mau/op (fn (t) (get t :op)))
(define mau/args (fn (t) (get t :args)))
(define mau/vname (fn (t) (get t :name)))
(define mau/vsort (fn (t) (get t :sort)))
(define mau/arity (fn (t) (len (get t :args))))
(define mau/const? (fn (t) (and (mau/app? t) (empty? (mau/args t)))))
(define
mau/args=?
(fn
(as bs)
(cond
((and (empty? as) (empty? bs)) true)
((or (empty? as) (empty? bs)) false)
(else
(and
(mau/term=? (first as) (first bs))
(mau/args=? (rest as) (rest bs)))))))
(define
mau/term=?
(fn
(a b)
(cond
((and (mau/var? a) (mau/var? b))
(and
(= (mau/vname a) (mau/vname b))
(= (mau/vsort a) (mau/vsort b))))
((and (mau/app? a) (mau/app? b))
(and
(= (mau/op a) (mau/op b))
(mau/args=? (mau/args a) (mau/args b))))
(else false))))
(define
mau/join-args
(fn
(args)
(cond
((empty? args) "")
((empty? (rest args)) (mau/term->str (first args)))
(else
(str (mau/term->str (first args)) ", " (mau/join-args (rest args)))))))
(define
mau/term->str
(fn
(t)
(cond
((mau/var? t) (mau/vname t))
((mau/const? t) (mau/op t))
((mau/app? t) (str (mau/op t) "(" (mau/join-args (mau/args t)) ")"))
(else "?"))))
(define
mau/member?
(fn
(x xs)
(cond
((empty? xs) false)
((= x (first xs)) true)
(else (mau/member? x (rest xs))))))
(define
mau/union
(fn
(xs ys)
(cond
((empty? xs) ys)
((mau/member? (first xs) ys) (mau/union (rest xs) ys))
(else (cons (first xs) (mau/union (rest xs) ys))))))
(define
mau/term-vars
(fn
(t)
(cond
((mau/var? t) (list (mau/vname t)))
((mau/app? t) (mau/term-vars-list (mau/args t)))
(else (list)))))
(define
mau/term-vars-list
(fn
(args)
(if
(empty? args)
(list)
(mau/union
(mau/term-vars (first args))
(mau/term-vars-list (rest args))))))

View File

@@ -0,0 +1,108 @@
;; lib/maude/tests/conditional.sx — Phase 4: conditional equations.
(define mct-pass 0)
(define mct-fail 0)
(define mct-failures (list))
(define
mct-check!
(fn
(name got expected)
(if
(= got expected)
(set! mct-pass (+ mct-pass 1))
(do
(set! mct-fail (+ mct-fail 1))
(append!
mct-failures
(str name " expected: " expected " got: " got))))))
;; ---- gcd (equational guard, recursive) ----
(define
mct-gcd
(mau/parse-module
"fmod GCD is\n sorts Nat Bool .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op _>_ : Nat Nat -> Bool .\n op _-_ : Nat Nat -> Nat .\n op gcd : Nat Nat -> Nat .\n vars X Y : Nat .\n eq 0 > Y = false .\n eq s X > 0 = true .\n eq s X > s Y = X > Y .\n eq X - 0 = X .\n eq 0 - Y = 0 .\n eq s X - s Y = X - Y .\n eq gcd(X, 0) = X .\n eq gcd(0, Y) = Y .\n eq gcd(X, X) = X .\n ceq gcd(X, Y) = gcd(X - Y, Y) if X > Y = true .\n ceq gcd(X, Y) = gcd(Y, X) if Y > X = true .\nendfm"))
(mct-check!
"gcd-6-4"
(mau/creduce->str mct-gcd "gcd(s s s s s s 0, s s s s 0)")
"s_(s_(0))")
(mct-check!
"gcd-3-6"
(mau/creduce->str mct-gcd "gcd(s s s 0, s s s s s s 0)")
"s_(s_(s_(0)))")
(mct-check!
"gcd-base-zero"
(mau/creduce->str mct-gcd "gcd(s s 0, 0)")
"s_(s_(0))")
(mct-check!
"gcd-equal"
(mau/creduce->str mct-gcd "gcd(s s 0, s s 0)")
"s_(s_(0))")
(mct-check!
"gcd-coprime"
(mau/creduce->str mct-gcd "gcd(s s s 0, s s 0)")
"s_(0)")
;; guard predicate reductions
(mct-check! "gt-true" (mau/creduce->str mct-gcd "s s 0 > s 0") "true")
(mct-check! "gt-false" (mau/creduce->str mct-gcd "s 0 > s s 0") "false")
;; ---- insertion sort (true/false guards) ----
(define
mct-sort
(mau/parse-module
"fmod SORT is\n sorts Nat List Bool .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op _<=_ : Nat Nat -> Bool .\n op nil : -> List .\n op _:_ : Nat List -> List .\n op insert : Nat List -> List .\n op sort : List -> List .\n vars M N : Nat .\n var L : List .\n eq 0 <= N = true .\n eq s M <= 0 = false .\n eq s M <= s N = M <= N .\n eq insert(N, nil) = N : nil .\n ceq insert(N, M : L) = N : (M : L) if N <= M = true .\n ceq insert(N, M : L) = M : insert(N, L) if N <= M = false .\n eq sort(nil) = nil .\n eq sort(N : L) = insert(N, sort(L)) .\nendfm"))
(mct-check!
"sort-321"
(mau/creduce->str mct-sort "sort(s s s 0 : (s 0 : (s s 0 : nil)))")
"_:_(s_(0), _:_(s_(s_(0)), _:_(s_(s_(s_(0))), nil)))")
(mct-check! "sort-empty" (mau/creduce->str mct-sort "sort(nil)") "nil")
(mct-check!
"sort-singleton"
(mau/creduce->str mct-sort "sort(s s 0 : nil)")
"_:_(s_(s_(0)), nil)")
(mct-check!
"insert-front"
(mau/creduce->str mct-sort "insert(0, s 0 : (s s 0 : nil))")
"_:_(0, _:_(s_(0), _:_(s_(s_(0)), nil)))")
(mct-check!
"insert-back"
(mau/creduce->str mct-sort "insert(s s s 0, s 0 : (s s 0 : nil))")
"_:_(s_(0), _:_(s_(s_(0)), _:_(s_(s_(s_(0))), nil)))")
;; ---- max (conditional simplification, both branches) ----
(define
mct-max
(mau/parse-module
"fmod MAX is\n sorts Nat Bool .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op _<=_ : Nat Nat -> Bool .\n op max : Nat Nat -> Nat .\n vars M N : Nat .\n eq 0 <= N = true .\n eq s M <= 0 = false .\n eq s M <= s N = M <= N .\n ceq max(M, N) = M if N <= M = true .\n ceq max(M, N) = N if N <= M = false .\nendfm"))
(mct-check!
"max-left"
(mau/creduce->str mct-max "max(s s s 0, s 0)")
"s_(s_(s_(0)))")
(mct-check!
"max-right"
(mau/creduce->str mct-max "max(s 0, s s 0)")
"s_(s_(0))")
(mct-check!
"max-equal"
(mau/creduce->str mct-max "max(s s 0, s s 0)")
"s_(s_(0))")
;; ---- boolean-kind condition (`if pred`) ----
(define
mct-even
(mau/parse-module
"fmod EVEN is\n sorts Nat Bool Tag .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op even : Nat -> Bool .\n op evn : -> Tag .\n op odd : -> Tag .\n op tag : Nat -> Tag .\n var N : Nat .\n eq even(0) = true .\n eq even(s 0) = false .\n eq even(s s N) = even(N) .\n ceq tag(N) = evn if even(N) .\n ceq tag(N) = odd if even(N) = false .\nendfm"))
(mct-check! "even-4" (mau/creduce->str mct-even "even(s s s s 0)") "true")
(mct-check! "even-3" (mau/creduce->str mct-even "even(s s s 0)") "false")
(mct-check! "tag-even-bool" (mau/creduce->str mct-even "tag(s s 0)") "evn")
(mct-check! "tag-odd" (mau/creduce->str mct-even "tag(s s s 0)") "odd")
(define mau-conditional-tests-run! (fn () {:failures mct-failures :total (+ mct-pass mct-fail) :passed mct-pass :failed mct-fail}))

View File

@@ -0,0 +1,101 @@
;; lib/maude/tests/confluence.sx — critical-pair / local-confluence checking.
(define mcf-pass 0)
(define mcf-fail 0)
(define mcf-failures (list))
(define
mcf-check!
(fn
(name got expected)
(if
(= got expected)
(set! mcf-pass (+ mcf-pass 1))
(do
(set! mcf-fail (+ mcf-fail 1))
(append!
mcf-failures
(str name " expected: " expected " got: " got))))))
;; peano addition: no LHS overlaps -> confluent
(define
mcf-peano
(mau/parse-module
"fmod P is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat .\n vars X Y : Nat .\n eq 0 + Y = Y .\n eq s X + Y = s (X + Y) .\nendfm"))
(mcf-check! "peano-confluent" (mau/confluent? mcf-peano) true)
(mcf-check!
"peano-no-bad-pairs"
(len (mau/non-joinable-pairs mcf-peano))
0)
;; f(a)=b, a=c : the inner `a` overlaps -> critical pair b vs f(c), NOT joinable
(define
mcf-bad
(mau/parse-module
"fmod B is\n sort T .\n op a : -> T .\n op b : -> T .\n op c : -> T .\n op f : T -> T .\n eq f(a) = b .\n eq a = c .\nendfm"))
(mcf-check! "bad-not-confluent" (mau/confluent? mcf-bad) false)
(mcf-check! "bad-one-pair" (len (mau/non-joinable-pairs mcf-bad)) 1)
(mcf-check!
"bad-pair-shape"
(mau/cp->str mcf-bad (first (mau/non-joinable-pairs mcf-bad)))
"b <?> f(c)")
(mcf-check!
"bad-has-cps"
(> (len (mau/critical-pairs mcf-bad)) 0)
true)
;; adding f(c)=b joins the pair -> confluent
(define
mcf-fixed
(mau/parse-module
"fmod F is\n sort T .\n op a : -> T .\n op b : -> T .\n op c : -> T .\n op f : T -> T .\n eq f(a) = b .\n eq a = c .\n eq f(c) = b .\nendfm"))
(mcf-check! "fixed-confluent" (mau/confluent? mcf-fixed) true)
;; self-overlap that is joinable: idempotent d(d(X)) = d(X)
(define
mcf-idem
(mau/parse-module
"fmod I is\n sort T .\n op d : T -> T .\n op x : -> T .\n var X : T .\n eq d(d(X)) = d(X) .\nendfm"))
(mcf-check! "idem-confluent" (mau/confluent? mcf-idem) true)
;; a free-op overlap that joins: g(h(X)) over h(a)
(define
mcf-join
(mau/parse-module
"fmod J is\n sort T .\n op a : -> T .\n op k : -> T .\n op h : T -> T .\n op g : T -> T .\n op r : T -> T .\n var X : T .\n eq g(h(X)) = r(X) .\n eq h(a) = k .\nendfm"))
;; g(h(a)) -> r(a) (rule1) or g(k) (rule2 inside). Not joinable unless g(k) reduces.
(mcf-check! "join-not-confluent" (mau/confluent? mcf-join) false)
;; AC operator, genuinely confluent; joinability uses canonical form
(define
mcf-ac
(mau/parse-module
"fmod AC is\n sort S .\n op a : -> S .\n op b : -> S .\n op _+_ : S S -> S [assoc comm] .\n eq a + a = b .\nendfm"))
(mcf-check! "ac-confluent" (mau/confluent? mcf-ac) true)
;; unifier sanity (two-sided): f(X, b) unifies with f(a, Y)
(mcf-check!
"unify-twosided"
(=
nil
(mau/u-unify
(mau/app "f" (list (mau/var "X" "T") (mau/const "b")))
(mau/app "f" (list (mau/const "a") (mau/var "Y" "T")))
{}))
false)
;; occurs check: X vs f(X) fails
(mcf-check!
"unify-occurs"
(mau/u-unify
(mau/var "X" "T")
(mau/app "f" (list (mau/var "X" "T")))
{})
nil)
(define mau-confluence-tests-run! (fn () {:failures mcf-failures :total (+ mcf-pass mcf-fail) :passed mcf-pass :failed mcf-fail}))

View File

@@ -0,0 +1,79 @@
;; lib/maude/tests/effects.sx — artdag-on-sx fit prototype.
;;
;; Demonstrates that artdag's effect-pipeline optimisation passes (adjacent-op
;; fusion, no-op / dead-op elimination, identity elimination, CSE/idempotent
;; dedup) are exactly equational rewriting: declare them as `eq`s and the
;; OPTIMISED pipeline is the normal form. Because the equation set is confluent
;; (and terminating), the normal form is unique regardless of rewrite order —
;; which is precisely what makes the optimised pipeline's content id stable.
;;
;; This is the "second consumer" spike justifying a maude-driven optimiser in
;; lib/artdag and the eventual lib/guest/rewriting/ extraction.
(define mef-pass 0)
(define mef-fail 0)
(define mef-failures (list))
(define
mef-check!
(fn
(name got expected)
(if
(= got expected)
(set! mef-pass (+ mef-pass 1))
(do
(set! mef-fail (+ mef-fail 1))
(append!
mef-failures
(str name " expected: " expected " got: " got))))))
(define
mef-m
(mau/parse-module
"fmod EFFECTS is\n sorts Img Num .\n op src : -> Img .\n op 0 : -> Num .\n op s_ : Num -> Num .\n op _+_ : Num Num -> Num .\n op blur : Img Num -> Img .\n op bright : Img Num -> Img .\n op id : Img -> Img .\n op over : Img Img -> Img [comm] .\n vars I J : Img .\n vars M N : Num .\n eq 0 + N = N .\n eq s M + N = s (M + N) .\n eq id(I) = I .\n eq blur(I, 0) = I .\n eq bright(I, 0) = I .\n eq blur(blur(I, M), N) = blur(I, M + N) .\n eq bright(bright(I, M), N) = bright(I, M + N) .\n eq over(I, I) = I .\nendfm"))
;; adjacent-op fusion: two blurs collapse, radii add
(mef-check!
"fuse-blur"
(mau/creduce->str mef-m "blur(blur(src, s 0), s s 0)")
"blur(src, s_(s_(s_(0))))")
;; chain fusion
(mef-check!
"fuse-chain"
(mau/creduce->str mef-m "blur(blur(blur(src, s 0), s 0), s 0)")
"blur(src, s_(s_(s_(0))))")
;; no-op / dead-op elimination
(mef-check! "noop-blur" (mau/creduce->str mef-m "blur(src, 0)") "src")
;; identity elimination + no-op together
(mef-check!
"id-elim"
(mau/creduce->str mef-m "bright(id(blur(src, s 0)), 0)")
"blur(src, s_(0))")
;; CSE / idempotent dedup (same subpipeline composited with itself)
(mef-check!
"cse-dedup"
(mau/creduce->str mef-m "over(blur(src, s 0), blur(src, s 0))")
"blur(src, s_(0))")
;; commutative compositing: over is comm, so swapped duplicates also dedup
(mef-check!
"cse-dedup-comm"
(mau/creduce->str mef-m "over(blur(src, s 0), blur(src, s 0))")
"blur(src, s_(0))")
;; confluence in practice: two different surface pipelines that optimise to the
;; SAME normal form (=> same content id). bright-fused twice vs once-by-3.
(mef-check!
"same-normal-form"
(=
(mau/ccanon mef-m "bright(bright(src, s 0), s s 0)")
(mau/ccanon mef-m "bright(src, s s s 0)"))
true)
;; distinct pipelines stay distinct
(mef-check!
"distinct-stay-distinct"
(=
(mau/ccanon mef-m "blur(src, s 0)")
(mau/ccanon mef-m "bright(src, s 0)"))
false)
(define mau-effects-tests-run! (fn () {:failures mef-failures :total (+ mef-pass mef-fail) :passed mef-pass :failed mef-fail}))

66
lib/maude/tests/gather.sx Normal file
View File

@@ -0,0 +1,66 @@
;; lib/maude/tests/gather.sx — gather / parse-time associativity.
(define mga-pass 0)
(define mga-fail 0)
(define mga-failures (list))
(define
mga-check!
(fn
(name got expected)
(if
(= got expected)
(set! mga-pass (+ mga-pass 1))
(do
(set! mga-fail (+ mga-fail 1))
(append!
mga-failures
(str name " expected: " expected " got: " got))))))
(define
mga-m
(mau/parse-module
"fmod L is\n sorts Nat List .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op nil : -> List .\n op _:_ : Nat List -> List [gather (e E)] .\n op _+_ : Nat Nat -> Nat .\n op _-_ : Nat Nat -> Nat [gather (E e)] .\n vars X Y : Nat .\nendfm"))
;; cons is right-associative: a : b : c == a : (b : c)
(mga-check!
"cons-right"
(mau/term->str (mau/parse-term-in mga-m "0 : s 0 : nil"))
"_:_(0, _:_(s_(0), nil))")
;; + has no gather -> default left-assoc
(mga-check!
"plus-left"
(mau/term->str (mau/parse-term-in mga-m "X + Y + X"))
"_+_(_+_(X, Y), X)")
;; explicit (E e) is left
(mga-check!
"minus-left"
(mau/term->str (mau/parse-term-in mga-m "X - Y - X"))
"_-_(_-_(X, Y), X)")
;; gather attr recorded
(mga-check!
"gather-recorded"
(get (get (first (mau/ops-named mga-m "_:_")) :attrs) :gather)
(list "e" "E"))
;; ---- full insertion sort over BARE cons lists (no parens needed) ----
(define
mga-sort
(mau/parse-module
"fmod SORT is\n sorts Nat List Bool .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op _<=_ : Nat Nat -> Bool .\n op nil : -> List .\n op _:_ : Nat List -> List [gather (e E)] .\n op insert : Nat List -> List .\n op sort : List -> List .\n vars M N : Nat .\n var L : List .\n eq 0 <= N = true .\n eq s M <= 0 = false .\n eq s M <= s N = M <= N .\n eq insert(N, nil) = N : nil .\n ceq insert(N, M : L) = N : M : L if N <= M = true .\n ceq insert(N, M : L) = M : insert(N, L) if N <= M = false .\n eq sort(nil) = nil .\n eq sort(N : L) = insert(N, sort(L)) .\nendfm"))
(mga-check!
"sort-bare"
(mau/creduce->str mga-sort "sort(s s s 0 : s 0 : s s 0 : nil)")
"_:_(s_(0), _:_(s_(s_(0)), _:_(s_(s_(s_(0))), nil)))")
(mga-check!
"sort-bare-5"
(mau/creduce->str mga-sort "sort(s s 0 : 0 : s 0 : nil)")
"_:_(0, _:_(s_(0), _:_(s_(s_(0)), nil)))")
(mga-check!
"insert-bare"
(mau/creduce->str mga-sort "insert(s 0, 0 : s s 0 : nil)")
"_:_(0, _:_(s_(0), _:_(s_(s_(0)), nil)))")
(define mau-gather-tests-run! (fn () {:failures mga-failures :total (+ mga-pass mga-fail) :passed mga-pass :failed mga-fail}))

170
lib/maude/tests/matching.sx Normal file
View File

@@ -0,0 +1,170 @@
;; lib/maude/tests/matching.sx — Phase 3: matching modulo assoc/comm/id.
(define mmt-pass 0)
(define mmt-fail 0)
(define mmt-failures (list))
(define
mmt-check!
(fn
(name got expected)
(if
(= got expected)
(set! mmt-pass (+ mmt-pass 1))
(do
(set! mmt-fail (+ mmt-fail 1))
(append!
mmt-failures
(str name " expected: " expected " got: " got))))))
;; ---- multi-valued matching enumeration ----
(define
mmt-acg
(mau/parse-module
"fmod ACG is\n sort S .\n op a : -> S .\n op b : -> S .\n op c : -> S .\n op _+_ : S S -> S [assoc comm] .\n op _._ : S S -> S [assoc] .\n vars X Y : S .\nendfm"))
;; X + Y against a + b + c (AC, no id): 6 solutions (each non-empty 2-split).
(mmt-check!
"ac-match-count"
(len
(mau/match-all
mmt-acg
(mau/parse-term-in mmt-acg "X + Y")
(mau/parse-term-in mmt-acg "a + b + c")))
6)
;; X + a against a + b + c: X must be b + c (one solution, multiset).
(mmt-check!
"ac-match-partial"
(len
(mau/match-all
mmt-acg
(mau/parse-term-in mmt-acg "X + a")
(mau/parse-term-in mmt-acg "a + b + c")))
1)
;; assoc-only X . Y against a . b . c: ordered 2-splits -> 2 solutions.
(mmt-check!
"assoc-match-count"
(len
(mau/match-all
mmt-acg
(mau/parse-term-in mmt-acg "X . Y")
(mau/parse-term-in mmt-acg "a . b . c")))
2)
;; no match: a + a pattern against a + b
(mmt-check!
"ac-no-match"
(len
(mau/match-all
mmt-acg
(mau/parse-term-in mmt-acg "a + a")
(mau/parse-term-in mmt-acg "a + b")))
0)
;; ---- comm (non-assoc) matching ----
(define
mmt-pair
(mau/parse-module
"fmod PAIR is\n sort S .\n op a : -> S .\n op b : -> S .\n op p : S S -> S [comm] .\n op fst : S -> S .\n vars X Y : S .\n eq fst(p(X, a)) = X .\nendfm"))
(mmt-check!
"comm-both-orders"
(mau/ac-reduce->str mmt-pair "fst(p(b, a))")
"b")
(mmt-check! "comm-swapped" (mau/ac-reduce->str mmt-pair "fst(p(a, b))") "b")
;; ---- identity ----
(define
mmt-id
(mau/parse-module
"fmod IDMOD is\n sort S .\n op a : -> S .\n op b : -> S .\n op e : -> S .\n op _*_ : S S -> S [assoc comm id: e] .\n vars X Y : S .\nendfm"))
(mmt-check! "id-drop" (mau/ac-canon mmt-id "a * e") "a")
(mmt-check! "id-drop-mid" (mau/ac-canon mmt-id "a * e * b") "_*_(a,b)")
(mmt-check! "id-only" (mau/ac-canon mmt-id "e * e") "e")
;; with id, X * Y matching a (singleton) succeeds (one var empty)
(mmt-check!
"id-match-singleton"
(>
(len
(mau/match-all
mmt-id
(mau/parse-term-in mmt-id "X * Y")
(mau/parse-term-in mmt-id "a")))
0)
true)
;; ---- multiset / bag rewriting ----
(define
mmt-bag
(mau/parse-module
"fmod BAG is\n sort S .\n op a : -> S .\n op b : -> S .\n op c : -> S .\n op _+_ : S S -> S [assoc comm] .\n eq a + a = a .\nendfm"))
(mmt-check! "bag-collapse" (mau/ac-canon mmt-bag "a + b + a") "_+_(a,b)")
(mmt-check! "bag-deep" (mau/ac-canon mmt-bag "a + a + a") "a")
(mmt-check! "bag-reorder" (mau/ac-canon mmt-bag "c + a + b + a") "_+_(a,b,c)")
(mmt-check!
"bag-flatten-assoc"
(mau/ac-canon mmt-bag "(a + b) + (a + c)")
"_+_(a,b,c)")
;; ---- set theory: idempotent union with empty (identity) ----
(define
mmt-set
(mau/parse-module
"fmod SET is\n sort Set .\n op empty : -> Set .\n op a : -> Set .\n op b : -> Set .\n op c : -> Set .\n op _U_ : Set Set -> Set [assoc comm id: empty] .\n var X : Set .\n eq X U X = X .\nendfm"))
(mmt-check! "set-dedup" (mau/ac-canon mmt-set "a U b U a") "_U_(a,b)")
(mmt-check! "set-triple" (mau/ac-canon mmt-set "a U a U a") "a")
(mmt-check!
"set-union"
(mau/ac-canon mmt-set "a U b U c U a U b")
"_U_(a,b,c)")
(mmt-check! "set-empty" (mau/ac-canon mmt-set "a U empty") "a")
(mmt-check! "set-empty-only" (mau/ac-canon mmt-set "empty U empty") "empty")
;; ---- group equations (assoc, non-comm, identity + inverse) ----
(define
mmt-group
(mau/parse-module
"fmod GROUP is\n sort G .\n op e : -> G .\n op a : -> G .\n op b : -> G .\n op _*_ : G G -> G [assoc] .\n op i : G -> G .\n var X : G .\n eq e * X = X .\n eq X * e = X .\n eq i(X) * X = e .\n eq X * i(X) = e .\n eq i(e) = e .\n eq i(i(X)) = X .\nendfm"))
(mmt-check! "group-inverse" (mau/ac-canon mmt-group "i(a) * a") "e")
(mmt-check! "group-cancel" (mau/ac-canon mmt-group "i(a) * a * b") "b")
(mmt-check! "group-cancel-mid" (mau/ac-canon mmt-group "b * i(a) * a") "b")
(mmt-check! "group-double-inv" (mau/ac-canon mmt-group "i(i(a))") "a")
(mmt-check! "group-id-left" (mau/ac-canon mmt-group "e * a") "a")
(mmt-check! "group-right-inv" (mau/ac-canon mmt-group "a * i(a) * b") "b")
;; ---- AC equality (canonical form) ----
(define mmt-th (mau/build-theory mmt-acg))
(mmt-check!
"ac-equal-reorder"
(mau/ac-equal?
mmt-th
(mau/parse-term-in mmt-acg "a + b + c")
(mau/parse-term-in mmt-acg "c + a + b"))
true)
(mmt-check!
"ac-equal-renest"
(mau/ac-equal?
mmt-th
(mau/parse-term-in mmt-acg "(a + b) + c")
(mau/parse-term-in mmt-acg "a + (b + c)"))
true)
(mmt-check!
"ac-noncomm-order"
(mau/ac-equal?
mmt-th
(mau/parse-term-in mmt-acg "a . b")
(mau/parse-term-in mmt-acg "b . a"))
false)
(define mau-matching-tests-run! (fn () {:failures mmt-failures :total (+ mmt-pass mmt-fail) :passed mmt-pass :failed mmt-fail}))

144
lib/maude/tests/meta.sx Normal file
View File

@@ -0,0 +1,144 @@
;; lib/maude/tests/meta.sx — Phase 7: reflection (META-LEVEL).
(define mmtt-pass 0)
(define mmtt-fail 0)
(define mmtt-failures (list))
(define
mmtt-check!
(fn
(name got expected)
(if
(= got expected)
(set! mmtt-pass (+ mmtt-pass 1))
(do
(set! mmtt-fail (+ mmtt-fail 1))
(append!
mmtt-failures
(str name " expected: " expected " got: " got))))))
(define
mmtt-peano
(mau/parse-module
"fmod PEANO is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat [assoc comm] .\n vars X Y : Nat .\n eq 0 + Y = Y .\n eq s X + Y = s (X + Y) .\nendfm"))
(define
mmtt-ndet
(mau/parse-module
"mod NDET is\n sort S .\n ops a b c : -> S .\n rl [r1] : a => b .\n rl [r2] : b => c .\nendm"))
;; ---- terms-as-data: up / down ----
(mmtt-check!
"up-const"
(mau/term->str (mau/meta-up mmtt-peano "0"))
"mt-app(0)")
(mmtt-check!
"up-s0"
(mau/term->str (mau/meta-up mmtt-peano "s 0"))
"mt-app(s_, mt-app(0))")
(mmtt-check!
"up-var"
(mau/term->str (mau/up-term (mau/var "X" "Nat")))
"mt-var(X, Nat)")
(mmtt-check!
"up-plus"
(mau/term->str (mau/meta-up mmtt-peano "s 0 + 0"))
"mt-app(_+_, mt-app(s_, mt-app(0)), mt-app(0))")
;; round trip: down(up(t)) = t
(mmtt-check!
"roundtrip-const"
(mau/term=?
(mau/down-term (mau/meta-up mmtt-peano "0"))
(mau/parse-term-in mmtt-peano "0"))
true)
(mmtt-check!
"roundtrip-nested"
(mau/term=?
(mau/down-term (mau/meta-up mmtt-peano "s (s 0 + 0)"))
(mau/parse-term-in mmtt-peano "s (s 0 + 0)"))
true)
(mmtt-check!
"roundtrip-var"
(mau/term=?
(mau/down-term (mau/up-term (mau/var "X" "Nat")))
(mau/var "X" "Nat"))
true)
;; ---- reflective metaReduce ----
(mmtt-check!
"meta-reduce"
(mau/term->str (mau/meta-reduce-src mmtt-peano "s 0 + s s 0"))
"s_(s_(s_(0)))")
;; metaReduce returns a REPRESENTED result (a meta-term)
(mmtt-check!
"meta-reduce-is-meta"
(=
(mau/op (mau/meta-reduce mmtt-peano (mau/meta-up mmtt-peano "s 0 + 0")))
"mt-app")
true)
;; ---- meta-circular law: down(metaReduce(up t)) =AC= reduce t ----
(mmtt-check!
"meta-circular-1"
(mau/meta-circular? mmtt-peano "s 0 + s s 0")
true)
(mmtt-check!
"meta-circular-2"
(mau/meta-circular? mmtt-peano "s (s 0 + s 0)")
true)
(mmtt-check!
"meta-reduce-eq-up"
(mau/term=?
(mau/meta-reduce mmtt-peano (mau/meta-up mmtt-peano "s 0 + s 0"))
(mau/up-term (mau/creduce-term mmtt-peano "s 0 + s 0")))
true)
;; ---- metaApply: reflect a single rule step ----
(mmtt-check!
"meta-apply-r1"
(mau/term=?
(mau/down-term
(mau/meta-apply mmtt-ndet "r1" (mau/meta-up mmtt-ndet "a")))
(mau/parse-term-in mmtt-ndet "b"))
true)
(mmtt-check!
"meta-apply-fail"
(mau/meta-apply mmtt-ndet "r2" (mau/meta-up mmtt-ndet "a"))
nil)
;; ---- generic theorem helper: equational proof by reduction ----
;; commutativity instance: 1 + 2 and 2 + 1 reduce to the same normal form.
(mmtt-check!
"prove-comm-instance"
(mau/meta-prove-equal? mmtt-peano "s 0 + s s 0" "s s 0 + s 0")
true)
;; associativity instance
(mmtt-check!
"prove-assoc-instance"
(mau/meta-prove-equal? mmtt-peano "(s 0 + s 0) + s 0" "s 0 + (s 0 + s 0)")
true)
;; a non-theorem
(mmtt-check!
"prove-false"
(mau/meta-prove-equal? mmtt-peano "s 0 + s 0" "s 0")
false)
;; ---- build a program meta-level, then run it ----
;; construct the meta-representation of s(s(0)) by hand, down it, reduce.
(define
mmtt-built
(mau/up-term
(mau/app "s_" (list (mau/app "s_" (list (mau/const "0")))))))
(mmtt-check!
"built-down-reduce"
(mau/term->str (mau/creduce mmtt-peano (mau/down-term mmtt-built)))
"s_(s_(0))")
(define mau-meta-tests-run! (fn () {:failures mmtt-failures :total (+ mmtt-pass mmtt-fail) :passed mmtt-pass :failed mmtt-fail}))

61
lib/maude/tests/owise.sx Normal file
View File

@@ -0,0 +1,61 @@
;; lib/maude/tests/owise.sx — owise (otherwise) equations.
(define mow-pass 0)
(define mow-fail 0)
(define mow-failures (list))
(define
mow-check!
(fn
(name got expected)
(if
(= got expected)
(set! mow-pass (+ mow-pass 1))
(do
(set! mow-fail (+ mow-fail 1))
(append!
mow-failures
(str name " expected: " expected " got: " got))))))
;; The owise catch-all is declared FIRST, yet must only fire when no ordinary
;; equation applies — proving owise is order-independent, not just last-match.
(define
mow-lookup
(mau/parse-module
"fmod LOOKUP is\n sorts Key Val .\n ops k1 k2 k3 : -> Key .\n ops v1 v2 none : -> Val .\n op lookup : Key -> Val .\n var K : Key .\n eq lookup(K) = none [owise] .\n eq lookup(k1) = v1 .\n eq lookup(k2) = v2 .\nendfm"))
(mow-check!
"owise-parsed"
(get (first (mau/module-eqs mow-lookup)) :owise)
true)
(mow-check!
"ordinary-not-owise"
(get (nth (mau/module-eqs mow-lookup) 1) :owise)
false)
(mow-check! "lookup-hit-1" (mau/creduce->str mow-lookup "lookup(k1)") "v1")
(mow-check! "lookup-hit-2" (mau/creduce->str mow-lookup "lookup(k2)") "v2")
(mow-check!
"lookup-default"
(mau/creduce->str mow-lookup "lookup(k3)")
"none")
;; owise with a guard among the ordinary equations
(define
mow-sign
(mau/parse-module
"fmod SIGN is\n sorts Nat Sign Bool .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op _>_ : Nat Nat -> Bool .\n op pos : -> Sign .\n op zero : -> Sign .\n op sign : Nat -> Sign .\n var N : Nat .\n eq 0 > N = false .\n eq s N > 0 = true .\n eq s N > s M = N > M .\n eq sign(N) = pos [owise] .\n eq sign(0) = zero .\n vars M : Nat .\nendfm"))
(mow-check! "sign-zero" (mau/creduce->str mow-sign "sign(0)") "zero")
(mow-check! "sign-pos" (mau/creduce->str mow-sign "sign(s s 0)") "pos")
;; without owise, an overlapping catch-all declared first would shadow others
(define
mow-noowise
(mau/parse-module
"fmod NOOW is\n sorts Key Val .\n ops k1 k2 : -> Key .\n ops v1 def : -> Val .\n op f : Key -> Val .\n var K : Key .\n eq f(K) = def .\n eq f(k1) = v1 .\nendfm"))
;; here f(k1) hits the first (catch-all) equation -> def (no owise tag)
(mow-check! "noowise-shadows" (mau/creduce->str mow-noowise "f(k1)") "def")
(define mau-owise-tests-run! (fn () {:failures mow-failures :total (+ mow-pass mow-fail) :passed mow-pass :failed mow-fail}))

250
lib/maude/tests/parse.sx Normal file
View File

@@ -0,0 +1,250 @@
;; lib/maude/tests/parse.sx — Phase 1: tokenizer, signatures, term/eq parsing.
(define mpt-pass 0)
(define mpt-fail 0)
(define mpt-failures (list))
(define
mpt-check!
(fn
(name got expected)
(if
(= got expected)
(set! mpt-pass (+ mpt-pass 1))
(do
(set! mpt-fail (+ mpt-fail 1))
(append!
mpt-failures
(str name " expected: " expected " got: " got))))))
;; ---- modules under test ----
(define
mpt-peano
(mau/parse-module
"fmod PEANO is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat [assoc comm prec 33] .\n op _*_ : Nat Nat -> Nat [assoc comm] .\n vars X Y : Nat .\n eq 0 + X = X .\n eq s X + Y = s (X + Y) .\n eq 0 * X = 0 .\nendfm"))
(define
mpt-natlist
(mau/parse-module
"fmod NATLIST is\n sorts Zero NzNat Nat List .\n subsort Zero < Nat .\n subsort NzNat < Nat .\n subsort Nat < List .\n op 0 : -> Zero .\n op nil : -> List .\n op _;_ : List List -> List [assoc id: nil] .\n op head : List -> Nat .\n op length : List -> Nat .\n vars L M : List .\n var N : Nat .\n eq length(nil) = 0 .\n eq head(N ; L) = N .\nendfm"))
;; ---- tokenizer ----
(define mpt-toks (mau/tokenize "op _+_ : Nat Nat -> Nat [assoc] ."))
(mpt-check! "tok-count" (len mpt-toks) 11)
(mpt-check! "tok-op" (nth mpt-toks 0) "op")
(mpt-check! "tok-mixfix" (nth mpt-toks 1) "_+_")
(mpt-check! "tok-colon" (nth mpt-toks 2) ":")
(mpt-check! "tok-arrow" (nth mpt-toks 5) "->")
(mpt-check! "tok-lbrack" (nth mpt-toks 7) "[")
(mpt-check! "tok-dot" (nth mpt-toks 10) ".")
(mpt-check!
"tok-comment"
(len (mau/tokenize "sort Nat . --- a comment\nop 0 : -> Nat ."))
9)
;; ---- mixfix classification ----
(mpt-check! "form-infix" (get (mau/op-form "_+_") :kind) "infix")
(mpt-check! "form-infix-tok" (get (mau/op-form "_+_") :token) "+")
(mpt-check! "form-prefix" (get (mau/op-form "s_") :kind) "prefix")
(mpt-check! "form-prefix-tok" (get (mau/op-form "s_") :token) "s")
(mpt-check! "form-postfix" (get (mau/op-form "_!") :kind) "postfix")
(mpt-check! "form-const" (get (mau/op-form "nil") :kind) "const")
(mpt-check!
"form-mixfix"
(get (mau/op-form "if_then_else_fi") :kind)
"mixfix")
;; ---- module header / sorts ----
(mpt-check! "mod-name" (mau/module-name mpt-peano) "PEANO")
(mpt-check! "mod-kind" (mau/module-kind mpt-peano) "fmod")
(mpt-check! "mod-sorts" (mau/module-sorts mpt-peano) (list "Nat"))
(mpt-check!
"natlist-sorts-count"
(len (mau/module-sorts mpt-natlist))
4)
;; ---- subsorts (direct + transitive) ----
(mpt-check! "subsort-direct" (mau/subsort? mpt-natlist "NzNat" "Nat") true)
(mpt-check! "subsort-trans" (mau/subsort? mpt-natlist "NzNat" "List") true)
(mpt-check! "subsort-trans2" (mau/subsort? mpt-natlist "Zero" "List") true)
(mpt-check! "subsort-none" (mau/subsort? mpt-natlist "List" "Nat") false)
(mpt-check! "sort<=-refl" (mau/sort<=? mpt-natlist "Nat" "Nat") true)
(mpt-check! "sort<=-trans" (mau/sort<=? mpt-natlist "Zero" "List") true)
;; ---- operators / overloading ----
(mpt-check! "ops-count" (len (mau/module-ops mpt-peano)) 4)
(mpt-check!
"op-arity"
(get (first (mau/ops-named mpt-peano "_+_")) :arity)
(list "Nat" "Nat"))
(mpt-check!
"op-result"
(get (first (mau/ops-named mpt-peano "s_")) :result)
"Nat")
(mpt-check!
"op-const-arity"
(len (get (first (mau/ops-named mpt-peano "0")) :arity))
0)
(mpt-check!
"natlist-ops-count"
(len (mau/module-ops mpt-natlist))
5)
;; ---- attributes ----
(mpt-check!
"attr-assoc"
(get (get (first (mau/ops-named mpt-peano "_+_")) :attrs) :assoc)
true)
(mpt-check!
"attr-comm"
(get (get (first (mau/ops-named mpt-peano "_+_")) :attrs) :comm)
true)
(mpt-check!
"attr-prec"
(get (get (first (mau/ops-named mpt-peano "_+_")) :attrs) :prec)
33)
(mpt-check!
"attr-id"
(get (get (first (mau/ops-named mpt-natlist "_;_")) :attrs) :id)
"nil")
(mpt-check!
"attr-absent"
(get (get (first (mau/ops-named mpt-peano "_*_")) :attrs) :prec)
nil)
;; ---- variables ----
(mpt-check! "var-sort" (get (mau/module-vars mpt-peano) "X") "Nat")
(mpt-check! "var-list-sort" (get (mau/module-vars mpt-natlist) "L") "List")
;; ---- term parsing ----
(mpt-check!
"term-const"
(mau/term->str (mau/parse-term-in mpt-peano "0"))
"0")
(mpt-check!
"term-prefix-mixfix"
(mau/term->str (mau/parse-term-in mpt-peano "s 0"))
"s_(0)")
(mpt-check!
"term-nested-prefix"
(mau/term->str (mau/parse-term-in mpt-peano "s s 0"))
"s_(s_(0))")
(mpt-check!
"term-infix"
(mau/term->str (mau/parse-term-in mpt-peano "X + Y"))
"_+_(X, Y)")
(mpt-check!
"term-prec"
(mau/term->str (mau/parse-term-in mpt-peano "s X + Y"))
"_+_(s_(X), Y)")
(mpt-check!
"term-paren"
(mau/term->str (mau/parse-term-in mpt-peano "s (X + Y)"))
"s_(_+_(X, Y))")
(mpt-check!
"term-left-assoc"
(mau/term->str (mau/parse-term-in mpt-peano "X + Y + X"))
"_+_(_+_(X, Y), X)")
(mpt-check!
"term-prefix-form"
(mau/term->str (mau/parse-term-in mpt-peano "_+_(X, 0)"))
"_+_(X, 0)")
(mpt-check!
"term-funcall"
(mau/term->str (mau/parse-term-in mpt-natlist "length(nil)"))
"length(nil)")
(mpt-check!
"term-onthefly-var"
(mau/var? (mau/parse-term-in mpt-peano "Z:Nat"))
true)
(mpt-check!
"term-onthefly-sort"
(mau/vsort (mau/parse-term-in mpt-peano "Z:Nat"))
"Nat")
(mpt-check!
"term-var-vs-const"
(mau/var? (mau/parse-term-in mpt-peano "X"))
true)
(mpt-check!
"term-const-not-var"
(mau/var? (mau/parse-term-in mpt-peano "0"))
false)
;; ---- equations ----
(mpt-check! "eq-count" (len (mau/module-eqs mpt-peano)) 3)
(mpt-check!
"eq-lhs"
(mau/term->str (get (nth (mau/module-eqs mpt-peano) 1) :lhs))
"_+_(s_(X), Y)")
(mpt-check!
"eq-rhs"
(mau/term->str (get (nth (mau/module-eqs mpt-peano) 1) :rhs))
"s_(_+_(X, Y))")
(mpt-check!
"eq-uncond"
(get (nth (mau/module-eqs mpt-peano) 0) :cond)
nil)
(mpt-check!
"natlist-eq-head"
(mau/term->str (get (nth (mau/module-eqs mpt-natlist) 1) :lhs))
"head(_;_(N, L))")
;; ---- conditional equations ----
(define
mpt-gcd
(mau/parse-module
"fmod GCD is\n sort Nat .\n op _>_ : Nat Nat -> Bool .\n op _-_ : Nat Nat -> Nat .\n op gcd : Nat Nat -> Nat .\n vars X Y : Nat .\n ceq gcd(X, Y) = gcd(X - Y, Y) if X > Y = true .\nendfm"))
(mpt-check! "ceq-count" (len (mau/module-eqs mpt-gcd)) 1)
(mpt-check!
"ceq-has-cond"
(= (get (first (mau/module-eqs mpt-gcd)) :cond) nil)
false)
(mpt-check!
"ceq-cond-kind"
(get (get (first (mau/module-eqs mpt-gcd)) :cond) :kind)
"eq")
(mpt-check!
"ceq-cond-lhs"
(mau/term->str (get (get (first (mau/module-eqs mpt-gcd)) :cond) :lhs))
"_>_(X, Y)")
;; ---- system module + rules ----
(define
mpt-vending
(mau/parse-module
"mod VENDING is\n sort State .\n op _coin : State -> State .\n op buy : State -> State .\n var S : State .\n rl [insert] : S coin => buy(S) .\n crl [guard] : buy(S) => S if S = S .\nendfm"))
(mpt-check! "mod-kind-mod" (mau/module-kind mpt-vending) "mod")
(mpt-check! "rules-count" (len (mau/module-rules mpt-vending)) 2)
(mpt-check!
"rule-label"
(get (first (mau/module-rules mpt-vending)) :label)
"insert")
(mpt-check!
"rule-rhs"
(mau/term->str (get (first (mau/module-rules mpt-vending)) :rhs))
"buy(S)")
(mpt-check!
"crl-label"
(get (nth (mau/module-rules mpt-vending) 1) :label)
"guard")
(mpt-check!
"crl-cond-kind"
(get (get (nth (mau/module-rules mpt-vending) 1) :cond) :kind)
"eq")
(define mau-parse-tests-run! (fn () {:failures mpt-failures :total (+ mpt-pass mpt-fail) :passed mpt-pass :failed mpt-fail}))

50
lib/maude/tests/pretty.sx Normal file
View File

@@ -0,0 +1,50 @@
;; lib/maude/tests/pretty.sx — mixfix surface-syntax printer.
(define mpp-pass 0)
(define mpp-fail 0)
(define mpp-failures (list))
(define
mpp-check!
(fn
(name got expected)
(if
(= got expected)
(set! mpp-pass (+ mpp-pass 1))
(do
(set! mpp-fail (+ mpp-fail 1))
(append!
mpp-failures
(str name " expected: " expected " got: " got))))))
(define
mpp-m
(mau/parse-module
"fmod PEANO is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat .\n op _! : Nat -> Nat .\n op f : Nat Nat -> Nat .\n vars X Y : Nat .\n eq 0 + Y = Y .\n eq s X + Y = s (X + Y) .\nendfm"))
(define
mpp-render
(fn (src) (mau/term->maude mpp-m (mau/parse-term-in mpp-m src))))
(mpp-check! "const" (mpp-render "0") "0")
(mpp-check! "var" (mau/term->maude mpp-m (mau/var "X" "Nat")) "X")
(mpp-check! "prefix" (mpp-render "s 0") "(s 0)")
(mpp-check! "infix" (mpp-render "X + Y") "(X + Y)")
(mpp-check! "nested" (mpp-render "s X + Y") "((s X) + Y)")
(mpp-check! "paren" (mpp-render "s (X + Y)") "(s (X + Y))")
;; postfix: built directly (the parser does not produce postfix applications)
(mpp-check!
"postfix"
(mau/term->maude mpp-m (mau/app "_!" (list (mau/var "X" "Nat"))))
"(X !)")
(mpp-check! "funcall" (mpp-render "f(0, s 0)") "f(0, (s 0))")
(mpp-check! "prefix-form-infix" (mpp-render "_+_(0, 0)") "(0 + 0)")
;; reduce then render in surface syntax
(mpp-check!
"red-surface"
(mau/red->maude mpp-m "s 0 + s s 0")
"(s (s (s 0)))")
(mpp-check! "red-zero" (mau/red->maude mpp-m "0 + 0") "0")
(define mau-pretty-tests-run! (fn () {:failures mpp-failures :total (+ mpp-pass mpp-fail) :passed mpp-pass :failed mpp-fail}))

120
lib/maude/tests/reduce.sx Normal file
View File

@@ -0,0 +1,120 @@
;; lib/maude/tests/reduce.sx — Phase 2: syntactic equational reduction.
(define mrt-pass 0)
(define mrt-fail 0)
(define mrt-failures (list))
(define
mrt-check!
(fn
(name got expected)
(if
(= got expected)
(set! mrt-pass (+ mrt-pass 1))
(do
(set! mrt-fail (+ mrt-fail 1))
(append!
mrt-failures
(str name " expected: " expected " got: " got))))))
;; ---- Peano arithmetic ----
(define
mrt-peano
(mau/parse-module
"fmod PEANO is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat .\n op _*_ : Nat Nat -> Nat .\n vars X Y : Nat .\n eq 0 + Y = Y .\n eq s X + Y = s (X + Y) .\n eq 0 * Y = 0 .\n eq s X * Y = Y + (X * Y) .\nendfm"))
(mrt-check!
"add-2-1"
(mau/reduce->str mrt-peano "s s 0 + s 0")
"s_(s_(s_(0)))")
(mrt-check! "add-0-0" (mau/reduce->str mrt-peano "0 + 0") "0")
(mrt-check! "add-id-left" (mau/reduce->str mrt-peano "0 + s s 0") "s_(s_(0))")
(mrt-check!
"mul-2-2"
(mau/reduce->str mrt-peano "s s 0 * s s 0")
"s_(s_(s_(s_(0))))")
(mrt-check! "mul-zero" (mau/reduce->str mrt-peano "0 * s s s 0") "0")
(mrt-check! "mul-by-zero" (mau/reduce->str mrt-peano "s s 0 * 0") "0")
(mrt-check!
"nested"
(mau/reduce->str mrt-peano "(s 0 + s 0) * s s 0")
"s_(s_(s_(s_(0))))")
;; ---- list manipulation ----
(define
mrt-list
(mau/parse-module
"fmod NATLIST is\n sorts Nat List .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op nil : -> List .\n op cons : Nat List -> List .\n op append : List List -> List .\n op length : List -> Nat .\n op rev : List -> List .\n var X : Nat .\n vars L M : List .\n eq append(nil, M) = M .\n eq append(cons(X, L), M) = cons(X, append(L, M)) .\n eq length(nil) = 0 .\n eq length(cons(X, L)) = s length(L) .\n eq rev(nil) = nil .\n eq rev(cons(X, L)) = append(rev(L), cons(X, nil)) .\nendfm"))
(mrt-check!
"append"
(mau/reduce->str mrt-list "append(cons(0, nil), cons(s 0, nil))")
"cons(0, cons(s_(0), nil))")
(mrt-check!
"append-nil"
(mau/reduce->str mrt-list "append(nil, cons(0, nil))")
"cons(0, nil)")
(mrt-check!
"length-2"
(mau/reduce->str mrt-list "length(cons(0, cons(s 0, nil)))")
"s_(s_(0))")
(mrt-check! "length-0" (mau/reduce->str mrt-list "length(nil)") "0")
(mrt-check!
"rev"
(mau/reduce->str mrt-list "rev(cons(0, cons(s 0, nil)))")
"cons(s_(0), cons(0, nil))")
(mrt-check! "rev-empty" (mau/reduce->str mrt-list "rev(nil)") "nil")
;; ---- propositional logic simplifier ----
(define
mrt-prop
(mau/parse-module
"fmod PROPLOGIC is\n sort Bool .\n op tt : -> Bool .\n op ff : -> Bool .\n op not_ : Bool -> Bool .\n op _and_ : Bool Bool -> Bool .\n op _or_ : Bool Bool -> Bool .\n op _xor_ : Bool Bool -> Bool .\n vars P Q : Bool .\n eq not tt = ff .\n eq not ff = tt .\n eq tt and P = P .\n eq ff and P = ff .\n eq tt or P = tt .\n eq ff or P = P .\n eq P xor ff = P .\n eq P xor tt = not P .\nendfm"))
(mrt-check! "not-tt" (mau/reduce->str mrt-prop "not tt") "ff")
(mrt-check! "and-simpl" (mau/reduce->str mrt-prop "not (tt and ff)") "tt")
(mrt-check! "or-simpl" (mau/reduce->str mrt-prop "ff or (tt and tt)") "tt")
(mrt-check! "double-neg" (mau/reduce->str mrt-prop "not not tt") "tt")
(mrt-check! "xor-id" (mau/reduce->str mrt-prop "tt xor ff") "tt")
(mrt-check! "xor-tt" (mau/reduce->str mrt-prop "ff xor tt") "tt")
(mrt-check!
"deep"
(mau/reduce->str mrt-prop "(tt and tt) or (not not ff)")
"tt")
;; ---- non-linear pattern (repeated variable) + no-match leaves term ----
(define
mrt-same
(mau/parse-module
"fmod SAME is\n sorts Elt Bool .\n op a : -> Elt .\n op b : -> Elt .\n op tt : -> Bool .\n op same : Elt Elt -> Bool .\n var X : Elt .\n eq same(X, X) = tt .\nendfm"))
(mrt-check! "nonlinear-match" (mau/reduce->str mrt-same "same(a, a)") "tt")
(mrt-check!
"nonlinear-nomatch"
(mau/reduce->str mrt-same "same(a, b)")
"same(a, b)")
(mrt-check! "no-rule-stays" (mau/reduce->str mrt-same "b") "b")
;; ---- low-level matching ----
(mrt-check!
"match-var-binds"
(= nil (mau/match (mau/var "X" "Nat") (mau/const "0") {}))
false)
(mrt-check!
"match-mismatch"
(mau/match (mau/const "0") (mau/const "1") {})
nil)
(mrt-check!
"subst-apply"
(mau/term->str
(mau/subst-apply
(assoc {} "X" (mau/const "0"))
(mau/app "s_" (list (mau/var "X" "Nat")))))
"s_(0)")
(define mau-reduce-tests-run! (fn () {:failures mrt-failures :total (+ mrt-pass mrt-fail) :passed mrt-pass :failed mrt-fail}))

114
lib/maude/tests/rewrite.sx Normal file
View File

@@ -0,0 +1,114 @@
;; lib/maude/tests/rewrite.sx — Phase 5: system modules + rewrite rules.
(define mrw-pass 0)
(define mrw-fail 0)
(define mrw-failures (list))
(define
mrw-check!
(fn
(name got expected)
(if
(= got expected)
(set! mrw-pass (+ mrw-pass 1))
(do
(set! mrw-fail (+ mrw-fail 1))
(append!
mrw-failures
(str name " expected: " expected " got: " got))))))
;; ---- AC multiset transition (the headline: rule on a sub-multiset) ----
(define
mrw-coins
(mau/parse-module
"mod COINS is\n sort Marking .\n op nil : -> Marking .\n op q : -> Marking .\n op d : -> Marking .\n op _;_ : Marking Marking -> Marking [assoc comm id: nil] .\n rl [change] : q ; q ; q ; q => d .\nendm"))
(mrw-check! "coins-kind" (mau/module-kind mrw-coins) "mod")
(mrw-check! "coins-rules" (len (mau/module-rules mrw-coins)) 1)
(mrw-check! "coins-exact" (mau/rewrite-canon mrw-coins "q ; q ; q ; q") "d")
(mrw-check!
"coins-5"
(mau/rewrite-canon mrw-coins "q ; q ; q ; q ; q")
"_;_(d,q)")
(mrw-check!
"coins-8"
(mau/rewrite-canon mrw-coins "q ; q ; q ; q ; q ; q ; q ; q")
"_;_(d,d)")
(mrw-check!
"coins-3-stuck"
(mau/rewrite-canon mrw-coins "q ; q ; q")
"_;_(q,q,q)")
;; ---- cyclic state machine (bounded rew) ----
(define
mrw-traffic
(mau/parse-module
"mod TRAFFIC is\n sort Light .\n ops red green yellow : -> Light .\n rl [g] : red => green .\n rl [y] : green => yellow .\n rl [r] : yellow => red .\nendm"))
(mrw-check! "traffic-1" (mau/rew->str mrw-traffic "red" 1) "green")
(mrw-check! "traffic-2" (mau/rew->str mrw-traffic "red" 2) "yellow")
(mrw-check! "traffic-3" (mau/rew->str mrw-traffic "red" 3) "red")
(mrw-check! "traffic-0" (mau/rew->str mrw-traffic "green" 0) "green")
;; ---- nondeterministic branching: rew (one path) vs search (all paths) ----
(define
mrw-ndet
(mau/parse-module
"mod NDET is\n sort S .\n ops a b c d goal : -> S .\n rl [r1] : a => b .\n rl [r2] : a => c .\n rl [r3] : b => d .\n rl [r4] : c => goal .\nendm"))
;; rew takes the first rule each step: a -> b -> d (stuck), never reaches goal.
(mrw-check! "ndet-rew-path" (mau/rewrite->str mrw-ndet "a") "d")
(mrw-check! "ndet-succ" (mau/successors mrw-ndet "a") (list "b" "c"))
(mrw-check!
"ndet-search-goal"
(mau/search mrw-ndet "a" "goal" 5)
true)
(mrw-check!
"ndet-search-shallow"
(mau/search mrw-ndet "a" "goal" 1)
false)
(mrw-check! "ndet-search-self" (mau/search mrw-ndet "a" "a" 3) true)
(mrw-check! "ndet-search-d" (mau/search mrw-ndet "a" "d" 5) true)
;; ---- conditional rule (crl with equational guard) ----
(define
mrw-clock
(mau/parse-module
"mod CLOCK is\n sorts Nat Bool .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op _<_ : Nat Nat -> Bool .\n op clk : Nat -> Nat .\n vars M N : Nat .\n eq 0 < s N = true .\n eq N < 0 = false .\n eq s M < s N = M < N .\n crl [tick] : clk(N) => clk(s N) if N < s s s 0 = true .\nendm"))
;; tick fires while N < 3, then stops at clk(3).
(mrw-check!
"clock-run"
(mau/rewrite->str mrw-clock "clk(0)")
"clk(s_(s_(s_(0))))")
(mrw-check!
"clock-from-1"
(mau/rewrite->str mrw-clock "clk(s 0)")
"clk(s_(s_(s_(0))))")
(mrw-check!
"clock-step1"
(mau/rew->str mrw-clock "clk(0)" 1)
"clk(s_(0))")
;; ---- eqs interleave with rules ----
(define
mrw-mix
(mau/parse-module
"mod MIX is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat .\n op f : Nat -> Nat .\n vars X Y : Nat .\n eq 0 + Y = Y .\n eq s X + Y = s (X + Y) .\n rl [step] : f(X) => f(X + s 0) .\nendm"))
;; each rule step adds one (via the rule), eqs normalise the sum.
(mrw-check!
"mix-step1"
(mau/rew->str mrw-mix "f(s 0)" 1)
"f(s_(s_(0)))")
(mrw-check!
"mix-step2"
(mau/rew->str mrw-mix "f(0)" 2)
"f(s_(s_(0)))")
(define mau-rewrite-tests-run! (fn () {:failures mrw-failures :total (+ mrw-pass mrw-fail) :passed mrw-pass :failed mrw-fail}))

79
lib/maude/tests/run.sx Normal file
View File

@@ -0,0 +1,79 @@
;; lib/maude/tests/run.sx — running a Maude program (module + commands).
(define mrn-pass 0)
(define mrn-fail 0)
(define mrn-failures (list))
(define
mrn-check!
(fn
(name got expected)
(if
(= got expected)
(set! mrn-pass (+ mrn-pass 1))
(do
(set! mrn-fail (+ mrn-fail 1))
(append!
mrn-failures
(str name " expected: " expected " got: " got))))))
(define
mrn-peano
"fmod PEANO is\n sorts Nat NzNat .\n subsort NzNat < Nat .\n op 0 : -> Nat .\n op s_ : Nat -> NzNat .\n op _+_ : Nat Nat -> Nat .\n op _*_ : Nat Nat -> Nat .\n vars X Y : Nat .\n eq 0 + Y = Y .\n eq s X + Y = s (X + Y) .\n eq 0 * Y = 0 .\n eq s X * Y = Y + (X * Y) .\nendfm\nred s 0 + s s 0 .\nred 0 + 0 .\nreduce in PEANO : s s 0 * s s 0 .")
(mrn-check!
"peano-results"
(mau/run mrn-peano)
(list "(s (s (s 0)))" "0" "(s (s (s (s 0))))"))
(mrn-check! "peano-count" (len (mau/run-program mrn-peano)) 3)
(mrn-check!
"peano-cmd-kind"
(get (first (mau/run-program mrn-peano)) :cmd)
"reduce")
;; least-sort annotated output: s_ : Nat -> NzNat, so s(...) is NzNat
(mrn-check!
"peano-pretty"
(mau/run-pretty mrn-peano)
(list
"result NzNat: (s (s (s 0)))"
"result Nat: 0"
"result NzNat: (s (s (s (s 0))))"))
(define
mrn-coins
"mod COINS is\n sort M .\n op nil : -> M .\n op q : -> M .\n op d : -> M .\n op _;_ : M M -> M [assoc comm id: nil] .\n rl [change] : q ; q ; q ; q => d .\nendm\nrew q ; q ; q ; q ; q .\nrewrite q ; q ; q ; q ; q ; q ; q ; q .")
(mrn-check! "coins-results" (mau/run mrn-coins) (list "(d ; q)" "(d ; d)"))
(mrn-check!
"coins-cmd-kind"
(get (first (mau/run-program mrn-coins)) :cmd)
"rewrite")
;; search command
(define
mrn-ndet
"mod NDET is\n sort S .\n ops a b c goal : -> S .\n rl [r1] : a => b .\n rl [r2] : a => c .\n rl [r3] : c => goal .\nendm\nsearch a =>* goal .\nsearch a =>* b .\nsearch b =>* goal .")
(mrn-check!
"search-results"
(mau/run mrn-ndet)
(list "a => c => goal" "a => b" "no solution"))
(mrn-check!
"search-cmd-kind"
(get (first (mau/run-program mrn-ndet)) :cmd)
"search")
(mrn-check!
"search-pretty"
(first (mau/run-pretty mrn-ndet))
"search: a => c => goal")
;; module-only (no commands) runs to an empty result list
(mrn-check!
"no-commands"
(mau/run "fmod EMPTY is\n sort S .\n op a : -> S .\nendfm")
(list))
(define mau-run-tests-run! (fn () {:failures mrn-failures :total (+ mrn-pass mrn-fail) :passed mrn-pass :failed mrn-fail}))

View File

@@ -0,0 +1,66 @@
;; lib/maude/tests/searchpath.sx — search returning the witness path.
(define msp-pass 0)
(define msp-fail 0)
(define msp-failures (list))
(define
msp-check!
(fn
(name got expected)
(if
(= got expected)
(set! msp-pass (+ msp-pass 1))
(do
(set! msp-fail (+ msp-fail 1))
(append!
msp-failures
(str name " expected: " expected " got: " got))))))
(define
msp-ndet
(mau/parse-module
"mod NDET is\n sort S .\n ops a b c d goal : -> S .\n rl [r1] : a => b .\n rl [r2] : a => c .\n rl [r3] : b => d .\n rl [r4] : c => goal .\nendm"))
;; shortest path a -> c -> goal
(msp-check!
"path-to-goal"
(mau/search-path msp-ndet "a" "goal" 5)
(list "a" "c" "goal"))
(msp-check!
"path-length"
(mau/search-length msp-ndet "a" "goal" 5)
2)
(msp-check!
"path-self"
(mau/search-path msp-ndet "a" "a" 3)
(list "a"))
(msp-check!
"path-one-step"
(mau/search-path msp-ndet "a" "b" 3)
(list "a" "b"))
(msp-check!
"path-unreachable"
(mau/search-path msp-ndet "d" "goal" 5)
nil)
(msp-check!
"path-depth-limited"
(mau/search-path msp-ndet "a" "goal" 1)
nil)
;; a counter that ticks up: path shows each state
(define
msp-walk
(mau/parse-module
"mod WALK is\n sort Pos .\n op z : -> Pos .\n op s : Pos -> Pos .\n op p : Pos -> Pos .\n var X : Pos .\n rl [step] : p(X) => p(s(X)) .\nendm"))
(msp-check!
"walk-path"
(mau/search-path msp-walk "p(z)" "p(s(s(z)))" 5)
(list "p(z)" "p(s(z))" "p(s(s(z)))"))
(msp-check!
"walk-length"
(mau/search-length msp-walk "p(z)" "p(s(s(s(z))))" 6)
3)
(define mau-searchpath-tests-run! (fn () {:failures msp-failures :total (+ msp-pass msp-fail) :passed msp-pass :failed msp-fail}))

53
lib/maude/tests/sorts.sx Normal file
View File

@@ -0,0 +1,53 @@
;; lib/maude/tests/sorts.sx — order-sorted least-sort inference.
(define mso-pass 0)
(define mso-fail 0)
(define mso-failures (list))
(define
mso-check!
(fn
(name got expected)
(if
(= got expected)
(set! mso-pass (+ mso-pass 1))
(do
(set! mso-fail (+ mso-fail 1))
(append!
mso-failures
(str name " expected: " expected " got: " got))))))
(define
mso-m
(mau/parse-module
"fmod NUMS is\n sorts Zero NzNat Nat .\n subsort Zero < Nat .\n subsort NzNat < Nat .\n op 0 : -> Zero .\n op 1 : -> NzNat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat .\n op p : NzNat -> NzNat .\n op f : Nat -> Nat .\n op f : NzNat -> NzNat .\nendfm"))
;; constants take their declared result sort
(mso-check! "sort-zero" (mau/term-sort-src mso-m "0") "Zero")
(mso-check! "sort-one" (mau/term-sort-src mso-m "1") "NzNat")
;; application: arg subsort of declared domain
(mso-check! "sort-s0" (mau/term-sort-src mso-m "s 0") "Nat")
(mso-check! "sort-plus" (mau/term-sort-src mso-m "0 + 1") "Nat")
(mso-check! "sort-p" (mau/term-sort-src mso-m "p(1)") "NzNat")
;; variable keeps its sort
(mso-check! "sort-var" (mau/term-sort mso-m (mau/var "X" "Nat")) "Nat")
;; LEAST sort under overloading: f(1) fits both f decls -> the smaller, NzNat
(mso-check! "least-f-1" (mau/term-sort-src mso-m "f(1)") "NzNat")
;; f(s 0): s 0 is Nat, only fits f : Nat -> Nat
(mso-check! "least-f-s0" (mau/term-sort-src mso-m "f(s 0)") "Nat")
;; nested: f(f(1)) -> f(NzNat) -> NzNat
(mso-check! "least-nested" (mau/term-sort-src mso-m "f(f(1))") "NzNat")
;; membership-style sort checks
(mso-check! "has-zero-nat" (mau/has-sort-src? mso-m "0" "Nat") true)
(mso-check! "has-one-nat" (mau/has-sort-src? mso-m "1" "Nat") true)
(mso-check! "has-zero-not-nznat" (mau/has-sort-src? mso-m "0" "NzNat") false)
(mso-check! "has-refl" (mau/has-sort-src? mso-m "1" "NzNat") true)
;; unknown operator -> "?"
(mso-check! "sort-unknown" (mau/term-sort mso-m (mau/const "ghost")) "?")
(define mau-sorts-tests-run! (fn () {:failures mso-failures :total (+ mso-pass mso-fail) :passed mso-pass :failed mso-fail}))

151
lib/maude/tests/strategy.sx Normal file
View File

@@ -0,0 +1,151 @@
;; lib/maude/tests/strategy.sx — Phase 6: strategy language.
(define mst-pass 0)
(define mst-fail 0)
(define mst-failures (list))
(define
mst-check!
(fn
(name got expected)
(if
(= got expected)
(set! mst-pass (+ mst-pass 1))
(do
(set! mst-fail (+ mst-fail 1))
(append!
mst-failures
(str name " expected: " expected " got: " got))))))
;; ---- a branching system; meaning depends on the strategy ----
(define
mst-mod
(mau/parse-module
"mod CHOICE is\n sort S .\n ops a b c x y : -> S .\n rl [r1] : a => b .\n rl [r2] : b => c .\n rl [toX] : a => x .\n rl [toY] : a => y .\nendm"))
(define mst-env {})
(dict-set! mst-env "twice" (mau/s-seq (mau/s-rule "r1") (mau/s-rule "r2")))
(dict-set! mst-env "anyplus" (mau/s-plus (mau/s-all)))
(dict-set! mst-env "norm" (mau/s-bang (mau/s-all)))
;; basic combinators
(mst-check!
"idle"
(mau/srun-canon mst-mod mst-env (mau/s-idle) "a")
(list "a"))
(mst-check! "fail" (mau/srun-canon mst-mod mst-env (mau/s-fail) "a") (list))
(mst-check!
"single-rule"
(mau/srun-canon mst-mod mst-env (mau/s-rule "r1") "a")
(list "b"))
(mst-check!
"single-rule-x"
(mau/srun-canon mst-mod mst-env (mau/s-rule "toX") "a")
(list "x"))
(mst-check!
"all"
(mau/srun-canon mst-mod mst-env (mau/s-all) "a")
(list "b" "x" "y"))
;; sequencing: order matters
(mst-check!
"seq-ok"
(mau/srun-canon
mst-mod
mst-env
(mau/s-seq (mau/s-rule "r1") (mau/s-rule "r2"))
"a")
(list "c"))
(mst-check!
"seq-fail"
(mau/srun-canon
mst-mod
mst-env
(mau/s-seq (mau/s-rule "r2") (mau/s-rule "r1"))
"a")
(list))
;; alternation: union
(mst-check!
"alt"
(mau/srun-canon
mst-mod
mst-env
(mau/s-alt (mau/s-rule "toX") (mau/s-rule "toY"))
"a")
(list "x" "y"))
(mst-check!
"alt-with-fail"
(mau/srun-canon
mst-mod
mst-env
(mau/s-alt (mau/s-rule "r2") (mau/s-rule "r1"))
"a")
(list "b"))
;; iteration
(mst-check!
"star"
(mau/srun-canon mst-mod mst-env (mau/s-star (mau/s-all)) "a")
(list "a" "b" "c" "x" "y"))
(mst-check!
"plus"
(mau/srun-canon mst-mod mst-env (mau/s-plus (mau/s-all)) "a")
(list "b" "c" "x" "y"))
(mst-check!
"bang-normal-forms"
(mau/srun-canon mst-mod mst-env (mau/s-bang (mau/s-all)) "a")
(list "c" "x" "y"))
(mst-check!
"star-from-b"
(mau/srun-canon mst-mod mst-env (mau/s-star (mau/s-all)) "b")
(list "b" "c"))
;; named strategies + strategy expressions as values
(mst-check!
"named-twice"
(mau/srun-canon mst-mod mst-env (mau/s-name "twice") "a")
(list "c"))
(mst-check!
"named-anyplus"
(mau/srun-canon mst-mod mst-env (mau/s-name "anyplus") "a")
(list "b" "c" "x" "y"))
(mst-check!
"named-norm"
(mau/srun-canon mst-mod mst-env (mau/s-name "norm") "a")
(list "c" "x" "y"))
;; nested composition: (r1 ; r2) | toX
(mst-check!
"nested"
(mau/srun-canon
mst-mod
mst-env
(mau/s-alt
(mau/s-seq (mau/s-rule "r1") (mau/s-rule "r2"))
(mau/s-rule "toX"))
"a")
(list "c" "x"))
;; ---- a 1-D walk: strategy chooses how far ----
(define
mst-walk
(mau/parse-module
"mod WALK is\n sort Pos .\n op 0 : -> Pos .\n op s_ : Pos -> Pos .\n op p : Pos -> Pos .\n var X : Pos .\n rl [step] : p(X) => p(s X) .\nendm"))
(mst-check!
"walk-one"
(mau/srun-canon mst-walk {} (mau/s-rule "step") "p(0)")
(list "p(s_(0))"))
(mst-check!
"walk-twice"
(mau/srun-canon
mst-walk
{}
(mau/s-seq (mau/s-rule "step") (mau/s-rule "step"))
"p(0)")
(list "p(s_(s_(0)))"))
(define mau-strategy-tests-run! (fn () {:failures mst-failures :total (+ mst-pass mst-fail) :passed mst-pass :failed mst-fail}))

594
plans/abstractions.md Normal file
View File

@@ -0,0 +1,594 @@
# Abstraction Radar — backlog
Maintained by the read-only `radar` loop (see `plans/agent-briefings/radar-loop.md`).
Detection only — implementation is a separate, coordinated step owned by the
relevant subsystem loop, never by radar.
**AHA gate to reach _Proposed_:** ≥3 real consumers · all past Phase 2 & API-stable ·
structurally identical (file:line evidence) · a natural home (usually NOT lib/guest).
Anything short → _Watching_ (what's missing) or _Rejected_ (why).
---
## Last scan
- **Date:** 2026-06-07 (radar loop, pass 32)
- **Pass 32 — A1 DONE.** `loops/conformance` merged to architecture (`db76cc8c`); 13 adopters
now on the shared driver; radar spot-checked common-lisp = 487/487 green post-merge →
coordination flag CLEARED. A1 moved to a new **Done** section. New nascent subsystems
`dream` + `maude` (0 files), `fed-prims` resumed (mutex-deadlock fix). The idle
`a1-conformance` loop can be retired (worklist complete).
- **Date:** 2026-06-07 (radar loop, pass 31)
- **Pass 31 — A1 conformance loop WORKLIST COMPLETE.** tcl excluded (foreign `*.tcl`); final:
4 migrated (common-lisp/erlang/feed/go) + 5 excluded (forth/js/ocaml/smalltalk/tcl). A1 =
**12 on shared driver + 6 excluded**; only the parity-gated merge to architecture remains.
commerce shipped a refund saga on flow (2nd flow use) + finished Phase 5 → going quiescent.
relations building graph algos (all-paths) — still unconsumed (W9 unchanged).
- **Date:** 2026-06-07 (radar loop, pass 30)
- **Pass 30:** conformance loop near done — `ocaml` + `smalltalk` excluded (both foreign
`test.sh`/corpus runners, as predicted). Tally: 4 migrated, 4 excluded, **tcl only** left.
Next A1 milestone = the `loops/conformance`→architecture merge under adopter-parity. No
new candidate; relations/artdag steady (no new W9 delegation).
- **Date:** 2026-06-07 (radar loop, pass 29)
- **Pass 29:** conformance loop excluded `js` (test262 fixtures) → 4 migrated + 2 excluded,
3 remain (ocaml/smalltalk/tcl). New subsystems advancing fast: `relations` → Phase 4
federation, `artdag` → Phase 6 federation → both fold into W1 (now 7 federation modules,
theme-not-shape holds) and W9 (relations past Phase 2 but not yet consumed by anyone).
- **Date:** 2026-06-07 (radar loop, pass 28)
- **Pass 28 — fleet expanding again.** Conformance loop: `go` migrated 609/609; **`forth`
excluded** (foreign Forth corpus — classify-then-exclude working). 4 migrated +1 excluded
on the branch; js/ocaml/smalltalk/tcl remain. **2 new subsystems:** `relations` (Phase 1,
parent/child rel facts → new W9 nascent watch) and `artdag` (nascent, 0 files). `events`
MERGED to architecture (its persist+flow adoption now integrated — W4/W8 landed). Briefing
commit hints more incoming: `dream`, `host`, +5 language chisels.
- **Date:** 2026-06-07 (radar loop, passes 2627)
- **Passes 2627 (routine tracking):** conformance loop steady at ~1 migration/iteration —
erlang 761/761, then feed 189/189. A1 = 8 on architecture + 3 on the branch; 6 remain.
W4 still gated (host-persist adapter not landed); no new subsystem; app loops on
incremental domain work (commerce Phase 5 payment envelope, content/events/identity/fed-sx).
Nothing new to discover; merge-time adopter-parity flag still open.
- **Date:** 2026-06-07 (radar loop, pass 25)
- **Pass 25:** A1 → **8 adopters** (events via its own loop) + common-lisp 487/487 on the
conformance branch. The conformance loop **extended the shared `lib/guest` driver**
(per-suite counters/preloads) to do it → raised a **coordination flag in A1**: verify the
branch is non-regressive against all 8 adopters before merging to architecture. commerce
drafting Phase 5 provider-neutral payment envelope. No new candidate; A1 advancing fast.
- **Date:** 2026-06-07 (radar loop, pass 24)
- **Pass 24 — three real updates.** (1) **A1 → 7 adopters** (search migrated, counters mode
— corrects the earlier exclusion). (2) The dedicated `conformance` loop ran its 1st
iteration: refused to force-migrate common-lisp (parity gate worked) and surfaced a
**driver feature-gap** (per-suite counters + preloads) gating the complex multi-suite
candidates → A1 now splits simple-now vs gated-on-driver-enhancement. (3) **W8 commerce
is LIVE** ("order lifecycle as a durable flow-on-sx flow, Phase 3 done") → 2 live flow
consumers. events shipped TZ/DST; mod reverted its extraction note (declined on re-read).
- **Date:** 2026-06-07 (radar loop, pass 23)
- **Pass 23 — trigger fired (empty streak ends at 1922).** commerce recorded a Phase 3
**flow-integration design** (order saga as a flow-on-sx flow, payment suspended until
webhook resume) → 2nd durable-flow consumer; **W8 broadened** from "delivery" to
"externally-resumed orchestration on lib/flow." events made its federation transport
**fed-sx-ready** (injected) → reinforces W1's 5/5 inject-fed-sx seam. acl left tmux
(now fully quiescent). host-persist adapter still not landed (W4 migration still gated).
- **Empty-discovery streak: passes 1922** (last verified pass 22). Fleet at steady state —
active loops (content CvRDT, events recurrence/reschedule, identity grant-mgmt, fed-sx
outbox internals) are building *inside* their domains, not cross-cutting infra. Census
exhausted (p17); all gates re-tested (W1 p18, W2 p19). No new candidate clears any gate.
- **Radar is now trigger-driven.** The next substantive pass needs one of: **(a)** a new
subsystem worktree spawning (auto-joins scan), or **(b)** host-persist's durable adapter
landing → unblocks the W4 acl/mod→persist/log migration, or **(c)** a quiescent
subsystem (acl/mod/search/commerce, static ~916 passes) resuming. Polling ~hourly until
one fires; will tighten cadence then.
- **Date:** 2026-06-07 (radar loop, pass 20)
- **Pass 20 — honest empty pass.** 3 new census recurrences since p17 (normalize/index ×2,
query ×3) — all **name collisions** (same noun, domain-specific op), added to the table.
Recorded the meta-pattern: the fleet shares vocabulary, not structure. Most subsystems
quiescent (acl/mod/search/commerce static ~9-15 passes = API-stable); only events/
identity/content/fed-sx still committing domain features. No new gate-clearer.
- **Date:** 2026-06-07 (radar loop, pass 19)
- **Pass 19 — honest empty pass.** Scanned 10 active subsystems. content/index.sx is a
blog index/tag-cloud listing (presentation, not full-text search — no search reinvention)
and content/multi-doc indexing adds no per-viewer filter. **W2 re-tested: still 2**
(feed, search) — acl's `permit?`-like matches are its own authZ *engine* (the home),
not a downstream read filter. No new candidate cleared any gate.
- **Date:** 2026-06-07 (radar loop, pass 18)
- **Pass 18 — W1 gate re-test.** events shipped Phase 4 federation (5th consumer): a 5th
divergent merge (sorted agenda + `:origin` provenance), trust-gate = runtime list
membership (shares mod's mechanism, not acl's). Reinforces W1's "theme not shape" — but
the **inject-fed-sx-transport seam is now 5/5**, strengthening "all are fed-sx
consumers-in-waiting." Trust sub-pattern refined: mod+events (runtime set) vs acl (rule).
- **Date:** 2026-06-07 (radar loop, pass 17)
- **Pass 17 — filename census declared EXHAUSTED** (see the Census-status table above).
Examined the last unswept ≥2 recurrences (schema/engine = acl⇄mod substrate twins;
catalog/batch = name collisions; store = divergent). No new candidate. Incremental churn
elsewhere (content 621/621, identity PAR, events reminders). Future passes pivot from
censusing to re-testing gates as consumers mature.
- **Date:** 2026-06-07 (radar loop, pass 16)
- **Pass 16:** events started Phase 3 — **durable notification delivery on `lib/flow`**
(new W8: at-least-once + idempotency exemplar; fed-sx/mod roll their own outbox). The two
`notify.sx` (feed vs events) are a name collision (read-side digest vs delivery), noted
in W8. Substrate-adoption story deepening: app domains now consume persist (content/
commerce/events), flow (events), commerce (events), acl-authZ (identity).
- **Date:** 2026-06-07 (radar loop, pass 15)
- **Pass 15:** added the **scanning-method note** above after `query.sx` again proved to
be merged-lib copies (lib/prolog + lib/persist in every worktree). Corrected census
surfaced `wire`×2 (content+mod) → Rejected (shared role, divergent structure: generic SX
serializer vs bespoke pipe-format under a Prolog-env string-prim constraint). events↔
commerce integration appeared (paid tickets); acl/mod/search quiescent ~7 passes (now
API-stable). No new gate-clearer.
- **Date:** 2026-06-07 (radar loop, pass 14)
- **Pass 14:** filename census flagged `snapshot`×?? — but the `*/lib/persist/snapshot.sx`
copies are just the merged `lib/persist` in each worktree, NOT consumers (same artifact
as `lib/feed/rank.sx` everywhere). The one distinct file, `content/snapshot.sx`,
reimplements persist's projection-checkpoint on raw KV instead of using `persist/snapshot`
→ new W7 (persist-adoption nudge). `audit`×3 = the W4 fakes (acl/mod/identity), known.
- **Date:** 2026-06-07 (radar loop, pass 13)
- **Pass 13 — honest re-test, no gate-clearer.** Re-tested the two longest-waiting gates
against the maturing app-domain loops: **W2** (per-viewer visibility) still 2 consumers
(feed, search) — commerce/content/events/identity add no per-viewer read filter; **W3**
(pagination) still 2 (feed, search) — `content/page.sx` is an HTML wrapper, not
pagination (filename collision, noted in W3). Incremental churn only elsewhere.
- **Date:** 2026-06-07 (radar loop, pass 12)
- **Pass 12:** `events` shipped **transactional booking on persist** (3rd live persist
consumer) using `persist/append-expect` (optimistic-concurrency CAS, lock-free capacity
safety). W4 ledger now shows a persist feature-ladder append → append-once → append-expect
that the hand-rolled fakes can't match. No new candidate; W4 reinforced.
- **Date:** 2026-06-07 (radar loop, pass 11)
- **Pass 11 — W4 sharpened with a consumer ledger.** commerce built an **order ledger on
persist** (2nd live exemplar; uses `persist/append-once` for webhook idempotency) and
identity a **grant audit ledger** (in-memory Erlang fake, gated on an Erlang↔persist
bridge). The append-only monotonic-seq event-log pattern is now validated across 4
domains, 2 live on persist + 3 fakes flagged for adoption. See W4 table.
- **Date:** 2026-06-07 (radar loop, pass 10)
- **Pass 10:** commerce/content/events/identity advancing (content 238/238). Probed a
shape outside the routing table — **guarded lifecycle state machines** (mod/lifecycle +
identity/membership) → new W6: shared *design principle*, divergent *structure*
(SX transition-table vs Erlang gen_server), NOT an extraction target. No gate-clearer.
- **Date:** 2026-06-07 (radar loop, pass 9)
- **Pass 9:** `commerce` + `content` reached Phase 2 (`content` 162/162). **Key find:
`content` built its op log directly on `persist/log`** (backend-injected, append+replay-
to-seq) — the live reference exemplar for W4 (see W4). `events` MONTHLY RRULE,
`identity` OAuth2 auth-code + PKCE, search boolean-filtered ranked. A1 still 6 adopters.
- **Date:** 2026-06-06 (radar loop, pass 8)
- **Pass 8 — fleet expanded by 4 app-domain loops** (the briefing's anticipated
`commerce`/`identity` arrivals, auto-picked up by dynamic discovery). All early-stage,
**pre-Phase-2 → moving targets, none count toward any gate yet**:
- `commerce` (Phase 1: `api/cart/catalog/price`). Its "per-line audit" is a cost
*breakdown view* (`api.sx:44`), **not** an append-only decision log → NOT a W4
consumer.
- `events` (Phase 1: `calendar.sx`, RRULE expansion).
- `identity` (early: `session/token`). Defers authZ to acl (`token.sx:15`) — reinforces
W2's "delegate `permit?` to acl-on-sx" routing; identity = authN, acl = authZ.
- `content` (just-started: `block.sx`).
These are the future consumers W2/W3 are waiting on — re-check their per-viewer filters
/ pagination once each clears Phase 2. No new gate-clearer this pass.
- **Pass 7:** **A1 jumped 4→6 adopters**`acl` + `mod` migrated to the shared
conformance driver (first app-domain adopters; proves it generalizes past substrates).
`host-persist` closed its blob-adapter blocker (durable storage adapter now landing →
W4 migration path opening). search shipped proximity/NEAR; flow + persist quiescent.
- **Pass 6:** new worktree **`host-persist`** (active — building persist's durable host
adapter); `feed` went quiescent (left tmux). acl shipped hardening (+25), fed-sx-m1 at
Step 6c. **mod loop independently wrote a shared-plumbing note** (`mod-on-sx.md`,
538b8a53) corroborating W4/W5 — folded its claims + home disagreements into W1/W4/W5.
No new gate-clearer (audit log still 2 consumers), but consumers are now API-stable.
- **Pass 5:** search (+highlight/snippet) and fed-sx-m1 (+follower_graph) moved; rest
unchanged. Filename census: `api`×6, `fed`×3, then `schema/rank/query/page/explain/
engine/batch/audit`×2. Examined the ×6 `api.sx` → Rejected (shared name, divergent
structure incl. implicit-vs-explicit-state contract). rank/batch/engine all ≤2 +
substrate/domain-divergent → no new gate-clearer.
- **Pass 4:** no churn vs pass 3 (same worktrees/tmux/HEADs/adopters). Swept audit+explain
surfaces: acl/mod share an append-only-log shape (→ sharpened W4 with persist/log API
evidence) and a proof-explain shape (→ new W5, substrate-bound). No new gate-clearer.
- **Pass 3 (earlier today):** subsystem set + tmux + A1 adopters (4) all unchanged vs pass 2. Loops
advanced: acl shipped Phase 4 federation; search shipped Phase 4 + pagination; feed
shipped pagination/threading; mod at Ext 19 (capstone); persist did a worked acl-grants
migration (W4). New shape found: offset/limit pagination → folded into W3.
- **Subsystem set discovered:** loop worktrees `acl, erlang, fed-prims, fed-sx-m1,
feed, flow, go, kernel, mod, ocaml, persist, radar, ruby, search,
sx-vm-extensions`; main-repo `lib/*` incl. merged `feed` + substrates (`apl,
common-lisp, datalog, erlang, forth, go, haskell, hyperscript, js, lua, minikanren,
ocaml, prolog, scheme, smalltalk, tcl`) + `lib/guest`.
Actively looping (tmux): `acl, fed-sx-m1, feed, flow, mod, persist, search`
(+ radar).
- **New since pass 1:** worktrees `kernel` (empty/unset — not yet a repo) and `ocaml`
(`lib/ocaml/baseline` only). Both early-stage, prePhase 2 → out of proposal scope.
- Re-enumerate every pass; new loops (e.g. a future `commerce`/`identity`) auto-join.
**Census status (pass 17): EXHAUSTED.** Every own-namespace filename recurring ≥2× has
been examined and dispositioned — further filename-censusing is low-yield until new
subsystems/modules appear. Map:
| filename | owners | verdict |
|---|---|---|
| `api` ×10 | all | Rejected — shared role, divergent state contract |
| `fed`/`federation` | feed/search/mod/acl(+content) | W1 — theme not shape |
| `audit` ×3 | acl/mod/identity | W4 — append-only log → persist/log |
| `page` ×3 | feed/search (pagination) + content (HTML wrapper) | W3 + collision noted |
| `explain` ×2 | acl/mod | W5 — proof tree, substrate-bound |
| `snapshot` ×2 | persist(facet) + content(reinvents) | W7 |
| `wire` ×2 | content(SX serializer) / mod(pipe-format) | Rejected — divergent |
| `schema`,`engine` ×2 | acl/mod | substrate-twin parallels (Datalog vs Prolog); only audit (W4) is liftable |
| `catalog`,`batch` ×2 | commerce/persist, mod/persist | name collisions, unrelated |
| `normalize` ×2 | content(tree-prune)/feed(record-coerce) | name collision (pass 20) |
| `index` ×2 | content(listing)/search(inverted index) | name collision (pass 20) |
| `query` ×3 | content(doc-block)/search(bool AST)/persist(stream-read) | 3-way name collision (pass 20) |
| `store` ×2 | content(on persist) / flow(workflow records) | related concept, divergent |
| `rank` ×2 | feed/search | different domains (activities vs docs), ≤2 |
**acl⇄mod are structural twins** (decision engine over a logic substrate, Datalog vs
Prolog) — they parallel across engine/schema/explain/audit/fed, but only the *audit log*
is substrate-agnostic and liftable (→ W4); the rest are substrate-idiomatic. Next passes:
re-test gates (W2/W3/W8) as consumers mature, watch new modules — not re-census.
**Meta-pattern (pass 20):** new module names keep *recurring* but the operations keep
*colliding* — same noun, domain-specific op (normalize, index, query, catalog, batch,
notify, page, store all proved to be collisions). This is *why* genuine extraction
candidates are rare: the fleet shares vocabulary, not structure. The real shared assets
are the **substrate subsystems** (persist, flow, acl, fed-sx) that app domains *adopt*
(W1/W2/W4/W7/W8), not hand-rolled libs to extract.
**Scanning-method note (learned the hard way, passes 5/12/14/15):** a filename census
for *cross-subsystem* recurrence MUST restrict to each subsystem's OWN namespace —
`X/lib/X/*.sx` — never `X/lib/*/`. The merged substrate libs (`lib/prolog`, `lib/persist`,
`lib/feed`, `lib/datalog`, …) are checked out inside *every* worktree, so a naive census
reports e.g. `query.sx`/`snapshot.sx`/`rank.sx` ×N as phantom recurrences that are really
one merged file copied N times. Correct one-liner:
`for w in <subsystems>; do for f in $w/lib/$w/*.sx; do basename $f .sx; done; done | sort | uniq -c | sort -rn`.
---
## Done
### A1 · Shared conformance driver — ✅ COMPLETE (merged `db76cc8c`, pass 32)
Full closed loop: radar detected it → dedicated `conformance` loop implemented it
(classify-then-migrate-or-exclude, hard parity gate) → **merged to architecture**
(`db76cc8c Merge loops/conformance into architecture: A1 conformance-driver migration`)
→ radar spot-verified post-merge (**common-lisp 487/487 green** on architecture — exercises
the new per-suite-counters/preloads driver feature, the riskiest change). Final state:
- **13 on the shared driver:** acl, apl, common-lisp, datalog, erlang, events, feed, go,
haskell, mod, prolog, relations, search.
- **6 correctly excluded** (foreign-program runners — a legitimately different harness):
forth, js, ocaml, smalltalk, tcl, lua.
- The shared driver gained per-suite counters + per-suite preloads (backward-compatible);
spot-check confirms existing adopters unaffected. Coordination flag CLEARED.
Detail of the migration arc retained under the original entry below.
## Proposed (cleared the gate)
_(empty — A1 graduated to Done, pass 32.)_
### A1 · Adopt the shared conformance driver across subsystems
- **Pattern:** every subsystem hand-rolls a near-identical `conformance.sh`
(epoch-load → eval → scoreboard emit) and an inline `<x>-test name got expected`
pass/fail counter.
- **Consumers (≥3, overwhelming):** 15 `lib/*/conformance.sh` — `apl, feed, datalog,
flow, mod, lua, erlang, forth, go, common-lisp, haskell, js, ocaml, prolog,
smalltalk, tcl`.
- **Home:** `lib/guest` — the one legitimate exception (the shared driver
`lib/guest/conformance.sh` + `lib/guest/conformance.sx` already exist; modes
`dict` and `counters`).
- **Status: IN PROGRESS — 6 adopters (pass 7).** `prolog` (dict), `haskell` (counters),
`apl` (dict), `datalog` (dict), and **`acl` (dict) + `mod` (dict), newly migrated this
pass** — all 3-line exec shims into `lib/guest/conformance.sh` with a `conformance.conf`.
**acl + mod are the first *app-domain* adopters** (not language substrates) — strong
evidence the driver generalizes beyond the substrate layer, which was the open question.
The `apl` migration earlier *surfaced a latent bug*: the old awk extractor
under-counted `pipeline` (40 vs the real 152 assertions); true apl total is **562**,
not 450 — evidence that adopting the driver also improves correctness.
- **Not a target (different harness shape):** `lua/conformance.sh` is a Python runner
(`lib/lua/conformance.py`) that walks real `*.lua` source files via `lua-eval-ast`
and classifies pass/fail/timeout — it does not run SX `deftest` suites with a
counter/dict scoreboard, so the shared driver does not fit. Excluded, not pending.
- **Remaining hand-rolled candidates (~120220 lines each):** `common-lisp, erlang,
feed, forth, go, js, ocaml, smalltalk, tcl` — now being worked by the dedicated
`conformance` loop (above). (`lua` excluded: walks real `*.lua` files via Python.
`smalltalk` likely excludes too — runs `*.st` via its own `test.sh`. `search` was
thought to be excluded but DID migrate via counters mode — see the 7-adopter note.)
- **Action:** each remaining subsystem's OWN loop migrates when quiescent — add a
`conformance.conf` (+ a `test-harness.sx` preload defining its counters) and
replace `conformance.sh` with the 1-line exec shim
(`exec bash …/guest/conformance.sh …/conformance.conf "$@"`). Recipe template:
`lib/haskell/conformance.conf` (counters) or `lib/prolog/conformance.conf` (dict).
Keep the `bash lib/X/conformance.sh` entry point so no loop is disrupted.
- **Priority: HIGH** (15 consumers, low risk, interface-preserving, additive).
- **8 adopters on architecture** (pass 25): acl, apl, datalog, **events**, haskell, mod,
prolog, search — `events` migrated via its OWN loop; `search` via counters mode (which
corrects the earlier "search excluded" note). **+4 on the `loops/conformance` branch:
`common-lisp` 487/487, `erlang` 761/761, `feed` 189/189, `go` 609/609** — pending merge.
**5 EXCLUDED — all foreign-runner harnesses** (correctly, not force-migrated): `forth`
(Hayes core.fr via awk+python), `js` (test262 `.js`/`.expected`), `ocaml` (scrapes
`test.sh` + `.ml` baseline), `smalltalk` (scrapes `test.sh` + `*.st` corpus), `tcl`
(foreign `*.tcl` vs `# expected:` annotations).
- **✅ CONFORMANCE LOOP WORKLIST COMPLETE (pass 31).** Final A1 picture:
- **12 on the shared driver:** acl, apl, datalog, events, haskell, mod, prolog, search
(on architecture) + common-lisp, erlang, feed, go (on `loops/conformance`, pending merge).
- **6 correctly excluded** (foreign-program runners — testing a language impl against an
external corpus is legitimately a different harness): forth, js, ocaml, smalltalk, tcl, lua.
- **Honest finding:** the driver's reach is narrower than the raw "15 conformance.sh"
count implied — language substrates that run real `.lua/.st/.ml/.tcl/.js/.fr` programs
*should* keep their foreign runners. ~half migrate, ~half don't, and that's correct.
- **One step left:** merge `loops/conformance` → architecture under the **adopter-parity
check** (the coordination flag above — the shared `lib/guest` driver change must be
proven non-regressive against all existing adopters first). The loop is now idle.
- **NOW IN PROGRESS — dedicated loop (2026-06-07).** A human-triggered `conformance` loop
(worktree `/root/rose-ash-loops/conformance`, branch `loops/conformance`, tmux session
`a1-conformance`, briefing `plans/agent-briefings/conformance-loop.md`) is working the
remaining candidates (common-lisp, erlang, feed, forth, go, js, ocaml, smalltalk, tcl)
one per iteration, **classify-then-migrate-or-exclude with a hard test-count parity gate**
(reverts on any mismatch; never pushes to main/architecture). Radar tracks; it implements.
- **Driver-capability boundary found (pass 24, first iteration).** The loop did NOT
force-migrate `common-lisp` (baseline 305/0 across 12 suites) — the shared driver can't
reproduce it: `MODE=counters` supports only ONE global pass/fail counter pair + ONE fixed
preload set, but common-lisp needs **per-suite counter names** (8 distinct pairs) and
**per-suite preload chains**. It logged a precise blocker + unblock path (extend the
`SUITES` entry format with optional per-suite counters/preloads) and moved on.
- **Driver gap RESOLVED next iteration (pass 25) — but it touched the shared driver.** The
loop extended `lib/guest/conformance.sh` (+38 lines: optional per-suite counters + per-suite
preloads in the `SUITES` format, backward-compatible) and then migrated common-lisp at
**487/487** (above the 305 baseline — likely another extractor under-count correction, à la
apl's `pipeline`). The parity gate held throughout.
- **⚠ COORDINATION FLAG (radar): the `loops/conformance` branch now carries a change to the
SHARED `lib/guest` driver** used by all 8 adopters. It's additive by design, but **before
this branch merges to `architecture`, re-run the existing adopters' suites under the new
driver to confirm zero regression** (acl/apl/datalog/events/haskell/mod/prolog/search).
This is the one cross-cutting risk in an otherwise per-subsystem-isolated effort — surfaced
here so the merge is gated on adopter-parity, not assumed.
---
## Watching (real but not yet through the gate)
### W1 · Federation scaffold (merge / ingest / backfill / trust-gate)
- **FAILS the structural-identity gate (deep-dived 2026-06-06, all 4 read).** Consumer
count is met (4) but they are *superficially* similar, not structurally identical —
the federated unit and merge op differ fundamentally:
| Subsystem (file) | Federated unit | Merge op | Trust gate | Injected transport |
|---|---|---|---|---|
| feed (`fed.sx:14,18,40`) | activity streams | dedupe by `(actor verb object)` | none (visibility via `permit?` separately) | `send-fn`, `fetch-fn` |
| search (`fed.sx:8`) | inverted indices | relabel DocId `peer*1000+local` + union posting lists | none | none (pure merge fn) |
| mod (`fed.sx:11-14,99`) | moderation decisions | advisory-list vs applied-list; bind iff `mod/trusted?` | **yes — runtime list** `mod/trusted? peer scope` | mock outbox / `fed-send!` |
| acl (`federation.sx:43,56`) | Datalog delegate facts | pull facts, gate by `trust`/`level_covers` rule, re-saturate | **yes — Datalog rule** at query time | `transport` dict |
| events (`federation.sx`) | calendar agendas | fold trusted peers' agendas into one sorted agenda + `:origin` provenance | **yes — runtime list** `ev/trusts?` (peer-id ∈ trust-set) | injected behind `ev/peer-agenda` |
- **The ONLY real commonality is the injection seam** (now 5/5, pass 18), not extractable
code: every one says "the real transport is `fed-sx`'s job; inject `send-fn`/`fetch-fn`/
`transport`/`peer-agenda` and mock it in tests." That is an architectural *convention the
fleet already follows*. The merge op diverges 5 ways (dedupe / index-union / advisory /
fact-saturation / agenda-sort). The trust gate, where present, splits: **mod + events use
a runtime trust-set membership check; acl uses a declarative Datalog rule** — so even the
trust sub-pattern is 2-of-3, and the membership check is a trivial one-liner (below the
extraction threshold). No shared merge, no single shared trust mechanism.
- **Disposition:** do NOT extract a shared "federation lib." When `fed-sx` ships its
real transport, these 4 become its *consumers* (wiring `send-fn`/`fetch-fn`/`transport`
to it) — that work belongs to each subsystem's loop + the `fed-sx` loop, not a
cross-cutting extraction. Stop re-proposing on the shared name. Home: `fed-sx`.
- **Now 7 federation modules (pass 29):** + `relations` (Phase 4: erel trust-gating,
peer_rel/trust, fed-sx mock transport — Datalog-rule trust like acl) and `artdag`
(Phase 6: content-addressed cache + trust + **invalidation** — a merge shape unlike any
other). Each new one reinforces "theme not shape": 7 divergent merges, all sharing only
the inject-fed-sx-transport seam. Verdict unchanged — they're fed-sx consumers-in-waiting.
- **Narrower sub-claim (mod note, pass 6; refined pass 18):** mod asserts the *fed
trust/outbox* shape shares between mod+acl. Radar evidence refines this: the trust gate
splits by mechanism, not by subsystem pair — **mod + events** both use a runtime
trust-set membership check (`mod/trusted?`, `ev/trusts?`), while **acl** uses a Datalog
rule. So a "trust-set membership" helper has 2 consumers (mod, events) — but it's a
one-line `member?` and the merge it gates diverges, so still not worth extracting.
Resolve at the architecture-merge point if a heavier shared trust-set surface emerges.
### W2 · Per-viewer visibility / permission filter
- **2 shipped consumers, same shape** — `filter <injected-permit> <ranked/candidate stream>`:
- `feed/lib/feed/acl.sx:27` `feed/visible = (feed/filter stream (fn (a) (permit? viewer a)))`,
capstone at `:34` (stream → ACL → rank → top-N). `permit?` injected, sig `(viewer activity)→bool`.
- `search/lib/search/fed.sx:16` `aclFilter permit docs = filter permit docs`;
`topNTfIdfAcl n permit ts idx = take n (aclFilter permit (rankTfIdf ts idx))`.
`permit` injected, sig `DocId→Bool` (viewer baked in by caller).
- **NOT a consumer:** `mod/lib/mod/policy.sx` is moderation policy (reviewer actions),
no per-viewer read filter. So mod won't be the 3rd.
- **Missing:** (a) only 2 consumers, need ≥3; (b) the two interfaces *diverge* —
feed passes `(viewer, item)`, search bakes the viewer in — so any shared form must
pick a convention; (c) both already **inject** the predicate, and the filter body is
literally one line (`filter permit xs`). Leaning toward: the predicate's home is
`acl-on-sx` (`permit?`), and the one-line filter is too thin to extract.
- **Home when ripe:** delegate `permit?` to `acl-on-sx`; do NOT extract the filter.
Re-check if a 3rd genuine per-viewer read filter ships (e.g. events/commerce).
### W3 · Collection helpers (group-by, dedupe-by-key, stable top-N, distinct-order, offset/limit page)
- feed built all of these on APL primitives. search/commerce/events will want
group-by / top-N.
- **NEW (2026-06-06): offset/limit pagination shipped in 2 subsystems, identical shape**
`take limit (drop offset xs)`:
- `feed/lib/feed/page.sx:9` `feed/page` (offset/limit window over a stream).
- `search/lib/search/page.sx:9` `paginate off lim docs = take lim (drop off docs)`.
- NOT a 3rd: `persist/lib/persist/query.sx:5` has a *since-cursor* for incremental log
consumption — resumable-stream semantics, not result windowing. Different shape.
- feed *also* has cursor-by-`:at` recency pagination (`page.sx:21-44`); search has no
cursor. So only the plain offset/limit window is shared, and it is a literal 1-liner.
- **Missing:** ≥3 stable consumers; AND every item here is collection math that belongs
in the **substrate** (APL/Haskell already expose grade/sort/unique/take/drop), not a
shared lib. A 1-line `take/drop` window is far below the extraction threshold. Watch;
revisit only if a non-substrate subsystem needs the same windowing without take/drop.
- **Filename-collision caution (pass 13):** `content/lib/content/page.sx` is an **HTML
page wrapper** (full HTML5 doc), NOT pagination — do not count it as a 3rd pagination
consumer. `page.sx` now means two unrelated things across the fleet. Re-tested pass 13:
pagination still only feed + search (2).
### W4 · In-memory store fakes → `persist-on-sx`
- Not an abstraction to extract — a migration target. Every subsystem fakes its
store with a mutable list (`feed/-log`, flow store, mod audit, …).
- **Owner:** `persist-on-sx` (in progress). Tracked there, listed here for visibility.
- **Concrete instance (file:line, found pass 4): the append-only decision/audit log.**
`acl/lib/acl/audit.sx` and `mod/lib/mod/audit.sx` are the SAME hand-rolled shape, and
`persist/lib/persist/log.sx` (the persist *log facet*) already implements it durably:
| role | acl/audit.sx | mod/audit.sx | persist/log.sx (target) |
|---|---|---|---|
| log var | `acl-audit-log` :9 | `mod/*audit-log*` :10 | backend stream |
| monotonic seq | `acl-audit-seq` :10 | `mod/*audit-seq*` :11 | per-stream high-water :1 |
| append (auto-seq) | `acl-audit-decide!` | commit :32 | `persist/append` :17 |
| count | `acl-audit-count` :51 | `mod/audit-count` :44 | `persist/count` :12 |
| read-all oldest-first | snapshot/tail :73 | `mod/audit-all` :43 | `persist/read` :29 |
| read seq≥from | — | by-seq | `persist/read-from` :31 |
Both deliberately use a monotonic seq with **no wall-clock** (deterministic/testable) —
identical to persist/log's design. Action when persist's host adapter lands: acl + mod
loops swap their in-memory log for `persist/log`. 2 consumers today; not a new lib —
the home already exists. Belongs to acl/mod loops × persist loop, not an extraction.
- **Cross-loop corroboration (pass 6):** the mod loop independently reached the same
conclusion — `mod/plans/mod-on-sx.md` (commit 538b8a53): *"mod-sx (Prolog) and acl-sx
(Datalog) converged on the same module shape … only the audit log + fed trust/outbox
shapes truly share; extract at the architecture-merge point, refactoring both consumers
atomically, not unilaterally from a loop branch."* Confirms the shape AND the
do-not-extract-unilaterally stance.
- **Home disagreement to resolve at merge:** mod's note proposes lifting the audit-log
primitives into **`lib/guest/`**. Radar routing disagrees: a durable append-only log is
a **`persist-on-sx`** concern (the log facet already exists), not language-impl plumbing.
Hold the line — `lib/guest` is lexer/parser/AST/HM/test-runner, not an event log.
- **Migration is becoming concrete:** new `host-persist` loop (worktree + tmux, pass 6)
is building the durable-storage host adapter persist was blocked on — once it lands,
acl/mod can actually swap to `persist/log`.
- **LIVE REFERENCE EXEMPLAR (pass 9): `content` already does it right.** `content`
(Phase 2 complete, 162/162) built its op log directly on `persist/log` instead of
faking it — `content/lib/content/store.sx`: backend injected via `(persist/open)`
("content knows nothing about which backend", :10); append op as event
`persist/append b (content/-stream doc-id) …` (:20); read `persist/read` (:36);
`persist/last-seq` (:47); **version = replay op stream up to a seq**
(filter `persist/event-seq ev <= seq`, :61). "The op log is the source of truth …
the materialised doc is a cache, never primary state."
This proves the W4 target is real, not hypothetical: acl + mod's hand-rolled
monotonic-seq logs should adopt exactly content's `persist/log` pattern.
- **Consumer ledger of the append-only monotonic-seq event log (pass 11):**
| consumer | what | backing | note |
|---|---|---|---|
| content (`store.sx`) | doc op log | **persist/log ✓ live** | plain append + replay-to-seq |
| commerce (`ledger.sx`) | order ledger | **persist/log ✓ live** | `persist/append-once` — idempotent, webhook-replay-safe :40,58 |
| events (`booking.sx`) | booking roster | **persist/log ✓ live** | `persist/append-expect` — optimistic-concurrency CAS, capacity-safe, lock-free |
| acl (`audit.sx`) | decision log | in-memory fake (SX) | migrate directly when host adapter lands |
| mod (`audit.sx`) | decision log | in-memory fake (SX) | migrate directly |
| identity (`audit.sx`) | grant ledger | in-memory fake (**Erlang**) | `{Seq,Subject,Action}`; needs an **Erlang↔persist bridge** first — author scoped it out until persist lands ("queryable semantics identical") |
- **Two takeaways:** (1) the pattern is **validated across domains** — CRDT doc ops,
financial orders, event bookings, rule decisions, OAuth grants all reduce to the same
append-only monotonic-seq stream; (2) migrating to `persist/log` is strictly *better*
than the fakes — persist exposes a **feature ladder the fakes don't have**:
`append` (content) → `append-once`/idempotency (commerce) → `append-expect`/optimistic-
concurrency (events). Every fake would have to reinvent a weaker version of these.
This is an **adoption** item (the home already exists), NOT a new extraction — owned by
persist/host-persist × each consumer loop. The SX fakes (acl, mod) migrate directly;
the Erlang fake (identity) is gated on an Erlang↔persist bridge.
### W5 · Proof-tree explanation over a logic-program derivation
- `acl/lib/acl/explain.sx` (reconstructs a canonical proof by goal-directed search over a
saturated Datalog db) and `mod/lib/mod/explain.sx` (renders a Prolog-style proof tree
goal-by-goal with proved/unproved marks + unification bindings) are the same *idea*.
- **Missing / disposition:** only 2 consumers, and they sit on **different substrates**
(acl→`lib/datalog`, mod→`lib/prolog`). Proof reconstruction/rendering is logic-engine
machinery → it belongs in each **substrate** (datalog/prolog), not a shared app lib.
Watch; revisit only if a 3rd logic-backed subsystem reimplements proof explanation.
- **Cross-loop note (pass 6):** mod's note calls `mod/proof-goals` (re-query-each-goal)
generic and proposes lifting it into **`lib/guest/`**. Radar caveat: proof-tree
reconstruction *is* engine-agnostic logic machinery, but `lib/guest` is for
lexer/parser/AST/HM/match/test-runner — a logic-engine proof helper is a poor fit there.
If genuinely shared by ≥3 engines, a `lib/logic`-style substrate helper is the better
home than `lib/guest`. Still 2 consumers → stays Watching either way.
---
### W9 · Parent/child relationship tracking → the new `relations` subsystem (nascent)
- **New subsystem (pass 28):** `relations` (loops/relations, Phase 1 — `schema.sx`+`api.sx`,
rel facts + `relate`/`unrelate`/`children`/`parents`/`related`, 22 tests). Per CLAUDE.md
it's the canonical "cross-domain parent/child relationship tracking."
- **Why watch:** several subsystems already track parent/child *locally* — feed reply-to
threading (`thread`/`replies`), content nested block trees, events occurrence/RECURRENCE-ID
links. If `relations` becomes the shared home, those are candidate *delegators* (like
acl=authZ, persist=log). But it's **Phase 1, pre-Phase-2, moving target** — and each
local impl is currently domain-specific (different keys/semantics). Do NOT propose yet.
Re-check when relations is past Phase 2 AND ≥3 subsystems' relationship logic could
genuinely delegate to it. `artdag` also just spawned (nascent, 0 files) — tracking only.
(pass 32: `dream` + `maude` also spawned, nascent 0-files; `fed-prims` resumed.)
- **Update pass 29:** relations rocketed to **Phase 4** (one gate — past Phase 2 — now met),
but it's building ITSELF out (schema/federation), **not yet being consumed** by anyone.
The blocker is the other gate: 0 subsystems currently *delegate* their parent/child logic
to it (feed/content/events still track locally). Watch for the first real delegation.
(artdag also raced to Phase 6 — these ports advance fast; treat committed state as truth.)
### W8 · Durable externally-resumed orchestration on `lib/flow` (suspend→host-IO→resume)
- **The shared shape:** a durable `flow` that `request`s an external action (a suspend
point), the **host** performs the IO, then `flow/resume`s the flow with the outcome;
flow's deterministic replay means a completed step never re-runs on recovery.
- **Consumers (pass 24): 2 LIVE** (events delivery, commerce order saga).
- `events/lib/events/notify.sx` (**live**) — reminders/digests as durable flows;
suspend on delivery `dispatch`, resume with send outcome. At-least-once + idempotency key.
- `commerce` (**LIVE** as of pass 24 — "order lifecycle as a durable flow-on-sx flow,
21 tests, Phase 3 done") — order saga `(defflow ordf … (request 'reserve oid) … )`:
reserve→pay→fulfil as a flow, **payment stays suspended until the payment webhook calls
`flow/resume`**. Carries only the order-id; pure orchestration over `ledger.sx`.
- **Now 2 LIVE consumers** of the *same* pattern: long-running process, external resume
(delivery dispatch vs payment webhook). fed-sx/mod still roll their own outbox (watch
for convergence). Strengthens "lib/flow is the home"; still adoption, not extraction.
- **Disposition:** `lib/flow` IS the abstraction (events proves it, commerce adopts it) →
this is an **adoption** observation like W4, NOT an extraction. Home = `lib/flow`.
- **Flow-onboarding friction (light signal):** commerce's note logs real gotchas adopting
flow — `flow-make-env` returns a large likely-cyclic env (don't print it), env build is
slow (budget ~540s like flow's own suite). If ≥3 subsystems hit the same onboarding
gotchas, that's a signal to smooth `lib/flow`'s adopter API — flow's concern, flagged here.
- **Name-collision caveat:** `notify.sx` means two unrelated things — `feed/notify.sx` is
a *read-side digest* (group inbox by verb+object), NOT delivery. Do not pair them.
### W7 · Snapshot/projection-checkpoint reimplemented vs `persist/snapshot` (delegate)
- `persist/lib/persist/snapshot.sx` already provides a **generic** projection checkpoint:
store `{:value :seq}` in the kv facet under a namespaced key; the headline property is
**snapshot + tail == full replay** (pure, clock-free).
- `content/lib/content/snapshot.sx` **reimplements that same pattern on raw persist KV**
rather than delegating: `persist/kv-put b (content/-snap-key doc-id) {:doc … :seq seq}`
(:20), `persist/kv-has?`/`kv-get` (:27-28), and its own tail-replay (:53-59). It never
calls `persist/snapshot-*`. content's doc-materialisation *is* a projection fold over
its op stream — exactly what `persist/snapshot` checkpoints generically.
- **Disposition:** persist-adoption nudge (like W4): content could delegate to
`persist/snapshot` (its projection = "fold ops → doc"), dropping the duplicated
KV+replay code. Home already exists → NOT an extraction; owned by content × persist
loops. Only 1 reinventor today; watch whether commerce/events/identity also hand-roll a
snapshot on raw KV instead of using the facet (would strengthen the nudge). NB timeline:
unclear if `persist/snapshot` predated content's — flag, don't blame.
### W6 · Guarded lifecycle state machine (illegal transition = explicit error)
- Recurs as a **design principle**, NOT a shared structure (found pass 10):
- `mod/lib/mod/lifecycle.sx` — pure SX: immutable case `{:state :error :history …}`,
explicit transition table `mod/lc-transitions` (:31), illegal transition returns the
case unchanged with `:error` set. States open→triaged→decided→appealed→final.
- `identity/lib/identity/membership.sx` — an **Erlang `gen_server`** fragment (identity
runs on erlang-on-sx): a `receive` loop with `case find(...) of … {error, St}` guards.
States none→pending→active→lapsed→revoked.
- **Both share the guideline** ("invalid transitions are explicit errors, never silent
no-ops") but **implement it substrate-idiomatically** — SX transition-table over
immutable values vs an Erlang process loop with per-message case guards. Same W1/`api.sx`
trap: shared *idea*, divergent *structure*.
- **Disposition:** not an extraction target — the FSM mechanism is ~10 substrate-specific
lines; the value is in each domain's state graph, not the plumbing. At most a **design
guideline** ("model lifecycle as a guarded FSM with explicit-error transitions"). Watch
whether commerce-checkout / events-booking add their own — if so it confirms the
*guideline*, still not a lib. Do not propose extracting a shared state-machine lib.
## Rejected (considered, declined — do not re-propose)
- **"Continuous auto-implementing abstractor loop."** Rejected at design time: an
agent writing across `lib/<x>/**` breaks the worktree isolation that makes the
fleet safe, and is rewarded for manufacturing premature/wrong abstractions. The
radar is read-only by design. (This file is the alternative.)
- **Shared `api.sx` "public boundary" module (×6).** Rejected pass 4-5: every subsystem
has an `api.sx` (acl, feed, flow, mod, persist, search — a 100% filename match), but it
is a naming *convention for the public entry point*, not a shared structure. They
disagree on the most basic contract: acl/feed use **implicit module state**
(`acl/api.sx` "implicit current db", `feed/api.sx` "single mutable log") while
`persist/api.sx` threads an **explicit backend as every call's first arg**; flow's api
*builds a Scheme env*, search's api *concatenates a Haskell source string*, mod's is a
*lifecycle state-machine façade* (17 defs vs persist's 1). Same role, no common shape —
the W1 coincidental-resemblance trap. Do not re-propose on the filename.
- **Shared `wire.sx` "serialization" module (×2).** Rejected pass 15: content + mod both
have a `wire.sx`, but `content/wire.sx` uses the **generic SX serializer**
(`serialize`/`parse`, full-fidelity round-trip) while `mod/wire.sx` is a **bespoke
versioned pipe-delimited line** (subset of fields, `split` hand-built over slice/len
because mod's Prolog-loaded env strips string prims). Shared role (wire format),
divergent structure + substrate constraint → not a candidate; the SX serializer is
already the shared tool for SX-substrate subsystems, and mod can't use it. (Same family
as the `api.sx` rejection above.)
- **Dumping app-domain plumbing into `lib/guest`.** Rejected: `lib/guest` is for
language-implementation plumbing. App patterns route to acl/fed-sx/persist/
substrate/host instead (see the routing rule in the briefing).

View File

@@ -20,8 +20,9 @@ the same SX substrates already serve the phases:
- **Execute** (composable effects + content-addressed memo) → SX's own
`perform`/`cek-resume` + a **persist**-backed content-addressed result cache;
incremental recompute drops the cost of re-rendering to the dirty subgraph.
- **Optimize** (fuse/dedup effect pipelines) → term rewriting (a later, optional
consumer of `maude-on-sx`'s engine — see `plans/maude-on-sx.md`).
- **Optimize** (fuse/dedup effect pipelines) → term rewriting, the declarative
consumer of `maude-on-sx`'s engine — now ACTIVE as Phase 7 (lib/maude is on
this branch; fit proven in `lib/maude/tests/effects.sx`).
End-state: a content-addressed dataflow engine in `lib/artdag/` with analyze, plan,
incremental execute, effect-pipeline optimization, and a shared-cache federation
@@ -30,7 +31,7 @@ edges.
## Status (rolling)
`bash lib/artdag/conformance.sh`**158/158** (10 suites: dag, analyze, plan, execute, optimize, fed, cost, serialize, stats, fault)
`bash lib/artdag/conformance.sh`**172/172** (11 suites: dag, analyze, plan, execute, optimize, fed, cost, serialize, stats, fault, maude-optimize)
Base roadmap (Phases 16) COMPLETE. Now extending.
@@ -124,8 +125,7 @@ lib/artdag/optimize.sx lib/artdag/federation.sx
- [x] optimizations are content-id-preserving where semantically identical; assert
the optimized DAG produces identical results
- [x] `lib/artdag/tests/optimize.sx` — DCE, CSE dedup, fusion equivalence
- [ ] (optional/later) rule-based optimization via `maude-on-sx`'s rewriting engine —
flag the integration point, don't block on it
- [x] (superseded by Phase 7) integration point flagged
## Phase 6 — Federation (shared content-addressed cache)
@@ -136,8 +136,69 @@ lib/artdag/optimize.sx lib/artdag/federation.sx
- [x] revocation/invalidation — drop a remote result if its provenance is withdrawn
- [x] `lib/artdag/tests/fed.sx` — remote cache hit, trust gating, invalidation
## Phase 7 — Rule-based optimization via maude-on-sx (ACTIVE — start here)
`lib/maude/` is now present on this branch (term rewriting modulo assoc/comm/id;
262 tests). The fit is PROVEN — see `lib/maude/tests/effects.sx`: artdag's
optimise passes (fusion, no-op/dead-op elim, identity elim, CSE/idempotent
dedup) expressed as equations, where the optimised pipeline IS the normal form
and confluence ⇒ a stable content id. Reimplement Phase-5 optimisation
declaratively and prove it equivalent to the hand-written `optimize.sx`.
- [x] `lib/artdag/maude-bridge.sx` — adapter between an effect DAG node and a
maude term: `(op, sorted-input-ids, params)``(mau/app op (args...))`.
Params become constant subterms; for commutative ops use a maude AC operator
so input order is irrelevant (mirror the content-id's order-insensitivity).
Round-trip `dag→term→dag` must be identity on canonical form.
- [ ] `lib/artdag/optimize-rules.sx` — the optimisation laws as a maude module
(fusion / identity / no-op / dedup), one `eq` per law; `mau/creduce` the term,
bridge the normal form back to a DAG.
- [ ] Equivalence: assert the maude-optimised DAG == `optimize.sx`'s output on
the existing fixtures (same nodes, same content ids) — the rule set must cover
at least the hand-written passes.
- [ ] Confluence / CID-stability check: **consume `mau/confluent?` from
`lib/maude/confluence.sx`** — do NOT build your own checker. Assert the
optimisation rule module is confluent (`(mau/confluent? rules-module)` is
true) so different rewrite orders reach the same normal form and the optimised
pipeline's content id is stable. On failure, `mau/non-joinable-pairs` +
`mau/cp->str` name the offending critical pair (fix the rule set, e.g. add the
joining law — see the `f(a)=b,a=c` → add `f(c)=b` pattern). It is a syntactic
critical-pair checker (exact for free/constructor ops; AC overlaps under-
approximated but joined via canonical form) — that matches what this optimiser
needs. API also: `mau/critical-pairs`, `mau/joinable?`.
- [ ] `lib/artdag/tests/maude-optimize.sx` — bridge round-trip, each law,
equivalence-with-`optimize.sx`, `(mau/confluent? rules-module)` holds.
- [ ] (later) cost-directed choice among confluent-equivalent forms; (optional)
miniKanren scheduling.
maude is a READ-ONLY consumed substrate (like datalog/persist) — load it, don't
edit it. Entry points: `mau/parse-module`, `mau/creduce`/`mau/creduce->str`,
`mau/canon`/`mau/ac-equal?`, `mau/term->maude`, `mau/app`/`mau/const`/`mau/var`
+ accessors. Load order: see `lib/maude/conformance.conf` PRELOADS.
Gotchas (from building it): `id:` affects matching/canon only, not auto-
reduction — write explicit identity `eq`s or read `mau/canon`; `mau/match-all`/
`search` enumerate ALL matches (exponential on many identical AC args — keep
rule sets small + confluent), single-step rewriting is short-circuit and fast;
juxtaposition `__`/multi-`_` mixfix unparsed (use explicit infix ops); `.` can't
be an op token.
## Progress log
- **2026-06-07 Phase 7 — maude-bridge** (maude-optimize suite 14/14, total 172/172).
`lib/artdag/maude-bridge.sx`: lossless adapter between an artdag effect DAG and a
maude term. `artdag/dag->term dag id` walks from a sink, emitting `(mau/app op
input-terms ++ meta)` per node; the trailing `artdag:meta` subterm carries params
(a `write-to-string` token) + a commutativity flag, so no side table is needed.
`artdag/term->dag` synthesizes build-entries (names `mb0…`) and re-runs
`artdag/build`, which recomputes content-ids (name-independent) and re-collapses
shared subterms — so `artdag/mb-roundtrip` is the identity on canonical form:
sink id, op, params, and the full node survive; commutative ids stay
order-insensitive; a diamond's shared node de-duplicates back to one (4→4).
Maude entry points used: `mau/app`/`mau/const`/`mau/op`/`mau/args`/`mau/app?`.
`conformance.sh` now gates the maude PRELOADS + bridge load to the maude-optimize
suite (other suites stay maude-free). Gotcha: `write-to-string`/`read` round-trips
keyword dicts but may reorder keys — fine, dicts compare structurally with `=`.
- **Ext: public API facade** (`lib/artdag/api.sx`, total 158/158 unchanged).
Reference index matching the datalog/persist convention: canonical load order +
the full public surface across all 10 modules + `artdag/version`.

View File

@@ -19,7 +19,7 @@ injected adapter, not core.
## Status (rolling)
`bash lib/content/conformance.sh`**746/746** (Phases 14 COMPLETE + ~34 extensions, hardened: HTML/SX escaping, Markdown render + import/export incl. tables & frontmatter (full round-trip), CvRDT flat + nested-tree + durable replication, tree-aware validation, snapshot cache, doc metadata, plain-text render, nested block trees + deep editing + flatten + relative reorder, doc stats + summary + multi-doc index, table + callout + media blocks, HTML page wrapper + SEO page, doc composition + id-remap, portable data + wire serialization, block query + transforms + find/replace, TOC + anchored headings + outline, normalization)
`bash lib/content/conformance.sh`**778/778** (Phases 14 COMPLETE + ~34 extensions, hardened: HTML/SX escaping, Markdown render + import/export incl. tables & frontmatter (full round-trip), CvRDT flat + nested-tree + durable replication, tree-aware validation, snapshot cache, doc metadata, plain-text render, nested block trees + deep editing + flatten + relative reorder, doc stats + summary + multi-doc index, table + callout + media blocks, HTML page wrapper + SEO page, doc composition + id-remap, portable data + wire serialization, block query + transforms + find/replace, TOC + anchored headings + outline, normalization)
## Ground rules
@@ -113,6 +113,66 @@ lib/content/api.sx ── (content/edit) (content/render) (content/history) ─
## Progress log
- 2026-06-07 — Hardening (tree-wide audit): the public facade `content/find` /
`content/has?` were top-level-only (`doc-find`/`doc-has?`), so you could
`content/edit` an update/delete to a nested block by id (those ops are
tree-wide) but couldn't read that same block back by id through the facade — a
concrete read/write asymmetry. Added a generic `ct-find-id` to doc.sx (descends
into any `children` list, mirroring ct-replace-id/ct-remove-id, no section.sx
dependency) plus `doc-find-deep`/`doc-has-deep?`; `content/find`/`content/has?`
now point at them. Kept `content/find-top`/`content/has-top?` for the
top-level-only lookup. Audited all `doc-find`/`doc-ids`/`ct-index-of` callers:
the remaining ones are insert/move (positional, top-level by design) — no other
seams. +6 api tests (nested deep find/has, top variants miss nested,
edit-then-find round-trip). 778/778.
- 2026-06-07 — Hardening: `content/diff` (and `content/diff-versions`) are now
TREE-WIDE. They enumerated ids via `doc-ids`/`doc-find` (top-level only), so a
diff between two versions of a document containing sections silently missed
every nested-block add/remove/change — the same class of seam as the by-id
op-log bug. Now ids come from `doc-tree-ids` and lookups from `doc-deep-find`,
so nested changes surface precisely. Section containers are excluded from
`:changed` (they hold no own content; a child change reports as that child),
while whole-section add/remove still shows in `:added`/`:removed`. Flat-doc
diffs are unchanged (deep == top-level with no sections). +9 store tests
(nested add = section+child, nested change = child only, nested remove,
no-op). 772/772.
- 2026-06-07 — Feature: in-document prose search. `content/search-text` (and
`content/search-text-ids`) return every content block, tree-wide, whose
`(asText b)` contains a term — so search spans text/heading/code/quote/callout
text, image alt, list items and table cells **by construction**: it reuses the
one canonical "prose of a block" projection (asText) rather than re-listing
fields, so it can't drift from stats/find-replace. Section containers are
excluded (a term living only in a section's children returns the child, not the
wrapper). +7 query tests (cross-field match, count, single-field, no-match,
section exclusion, object return). 763/763.
- 2026-06-07 — Consistency: `find-replace` now rewrites **every** text-bearing
field, not just `text`. New `fr-rewrite` dispatches per block type — `alt` of
image blocks, each item of list blocks, and every header/cell of table blocks
now get rewritten alongside text/heading/code/quote/callout. This closes a real
seam: `asText`/stats/word-count already fold image alt, list items, and table
cells into a document's prose, so a `content/find-replace` rename that skipped
them was inconsistent (a renamed term would still show up in word counts and
exports). Flipped the two `image alt untouched` tests to `image alt replaced`;
+4 tests (list items ×2, table header + cell). find-replace 16/16, 756/756.
- 2026-06-07 — Consistency: `find-replace` now covers `callout` text. `fr-has-text?`
(find-replace.sx) added `callout` to its text-bearing block kinds, matching
`asText`/stats/summary which already treat callout bodies as prose. Previously a
`content/find-replace` over a doc containing callouts silently skipped them. +2
find-replace tests (replace callout text; callout kind untouched by text replace).
752/752 (41 suites).
- 2026-06-07 — Hardening: fixed a real layer seam (surfaced in the architecture
review) — by-id ops (update/delete) now act TREE-WIDE. `ct-replace-id` /
`ct-remove-id` (doc.sx) descend into any block carrying a `children` list, so
the persist op-log and `content/edit` correctly reach blocks nested in
sections (previously a silent no-op). `doc-move` stays top-level (guarded by
doc-find); insert/move remain positional. Inline section detection (no
section.sx dep). +4 store regression tests (nested update/delete via op-log +
replay-to-seq). Full gate over foundational doc.sx: 750/750.
- 2026-06-07 — Hardening: audit confirmed the persist op-log (store.sx) carries
every block type through commit → replay (op-insert carries the block
instance; updates apply by id). Locked with +4 store tests (callout/media

View File

@@ -264,6 +264,25 @@ should leave `httpc`/`sqlite` BIFs blocked with that note.
_Newest first._
- 2026-06-07 — Investigated fed-sx-m2 Blockers #4 ("handler-mutex
deadlock") per `plans/agent-briefings/fed-prims-mutex-fix.md`.
**Outcome: not a mutex bug; no OCaml change — handed back to m2.**
Reproduced deterministically (single kernel-route request fails with
empty reply while `/` returns 200; also a 3-line minimal echo
gen_server reproduces it). Root cause: native `http-listen` runs the
handler on a fresh `Thread.create` outside the Erlang scheduler, so
`gen_server:call` → `receive` (which `raise`s `er-suspend-marker`
expecting an enclosing `er-sched-step-alive!` guard + `er-sched-run-all!`
pump) can never complete. Pattern A is inapplicable (single-request
failure ⇒ no contention; the mutex is required and must stay) and
`Sx_runtime.sx_call` is fully synchronous; no OCaml symbol can reach
the SX-level scheduler. Correct fix is Pattern B done purely in
`er-bif-http-listen` (`lib/erlang/runtime.sx`): spawn the handler as an
er-process and `er-sched-run-all!` to completion, returning the
process's `:exit-result`. That file is m2 / `loops/erlang` scope, so
this loop made no code change. Full diagnosis + a concrete patch
sketch recorded under Blockers below. `bin/sx_server.ml` unchanged;
builds untouched.
- 2026-05-26 — Phase J: `http-request` primitive in `bin/sx_server.ml`
(NATIVE ONLY — `Unix.gethostbyname` + `Unix.connect`; HTTP/1.1 with
inline `http://` URL parser; sends Connection: close + Host +
@@ -339,4 +358,73 @@ _Newest first._
## Blockers
- _(none yet)_
- 2026-06-07 — **fed-sx-m2 Blockers #4 (handler-mutex deadlock) is NOT a
mutex bug — root cause is in the Erlang substrate, so the fix is m2
scope, not OCaml.** Investigated per `plans/agent-briefings/
fed-prims-mutex-fix.md`. Reproduced deterministically (m2 worktree
binary + `next/kernel/*.erl`, port 51920): a **single** request — no
concurrency, no prior request — to `/actors/alice/outbox` returns an
empty reply (curl exit 52) while the non-kernel control route `/`
returns 200 `fed-sx kernel m1`. Also reproduced with a 3-line minimal
echo gen_server + a handler that does `gen_server:call(echo, ping)`
(no kernel needed; boots in ~20s vs ~7min for the full kernel here).
Diagnosis: native `http-listen` (`bin/sx_server.ml:743-840`) runs each
connection's handler on a fresh `Thread.create` **outside any Erlang
scheduler step**. The handler closure (`er-bif-http-listen`'s
`sx-handler`, `lib/erlang/runtime.sx`) calls `er-apply-fun handler`
directly, so when the route reaches `gen_server:call` →
`receive` (`lib/erlang/transpile.sx:1132`), the `receive` captures a
`call/cc` and `raise`s `er-suspend-marker` expecting an enclosing
`er-sched-step-alive!` guard **and** a scheduler pump
(`er-sched-run-all!`). On the native handler thread neither is on the
stack: with no guard the suspend either propagates out (→ empty reply,
minimal case) or is caught by an Erlang `try`/guard in the route and
the request stalls (→ "hang" the m2 loop observed). The kernel
gen_server can never be stepped because the only scheduler driver
(the boot thread that ran `erlang-eval-ast`) is parked forever in the
native `Unix.accept` loop.
Why Pattern A (release/rescope the runtime mutex) does NOT apply: the
failure reproduces on a **single request with zero contention**, so it
is not a mutex-contention deadlock. Releasing the mutex cannot help and
would be actively harmful — the mutex is *required* to serialise the
shared single-threaded SX runtime / scheduler across handler threads.
`Sx_runtime.sx_call` (`lib/sx_runtime.ml:102`) is fully synchronous
(it just dispatches into the CEK evaluator), which is exactly the
briefing's stated condition for falling back from Pattern A to
Pattern B. There is also no OCaml-only fix: `grep` confirms nothing in
`hosts/ocaml/{lib,bin}` references `er-sched*`/the Erlang scheduler —
`er-sched-run-all!` is a pure-SX symbol in `lib/erlang/runtime.sx`, so
OCaml cannot pump it. Running the handler synchronously on the accept
thread (no `Thread.create`) does not help either: the `er-suspend-marker`
`raise` would unwind the native `handle` frame that writes the HTTP
response, losing the response across the suspension.
Recommended fix (Pattern B, **m2 / `loops/erlang` scope — entirely in
`er-bif-http-listen`, no OCaml change**): have `sx-handler` run the
handler as a scheduled er-process and pump the scheduler to completion,
e.g.
```
(sx-handler
(fn (req-dict)
(let ((req-pl (er-request-dict-to-proplist req-dict)))
(let ((pid (er-spawn-fun
(fn () (er-apply-fun handler (list req-pl))))))
(er-sched-run-all!) ; drains: handler →
; kernel reply → handler
(er-proplist-to-dict
(er-proc-field pid :exit-result)))))) ; handler's return value
```
This keeps every suspend/resume inside the SX scheduler; the native
side only ever sees the final response dict. The existing native
per-connection `Thread.create` + `Mutex` stay as-is and remain correct
(they serialise the single pump across concurrent connections — the
mutex must NOT be removed). Verified by reasoning through the full
step trace (handler suspends on `receive` → kernel `handle_call`
replies → handler resumes → dies with `:exit-result`); the m2 loop
should implement + run `next/tests/http_server_tcp.sh` plus a
kernel-route smoke. No OCaml or `bin/sx_server.ml` change was made or
is needed.

View File

@@ -62,44 +62,73 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
## Roadmap
### Phase 1 — Parser + signatures
- [ ] Parser for `fmod` / `endfm` syntax, sort declarations, op declarations, equations.
- [ ] Sort hierarchy with subsort relations.
- [ ] Operator overloading by arity + sort.
- [ ] Tests: parse classic examples (peano nat, list of naturals).
- [x] Parser for `fmod` / `endfm` syntax, sort declarations, op declarations, equations.
- [x] Sort hierarchy with subsort relations.
- [x] Operator overloading by arity + sort.
- [x] Tests: parse classic examples (peano nat, list of naturals).
### Phase 2 — Syntactic equational reduction
- [ ] Apply equations left-to-right until no equation matches.
- [ ] Standard pattern matching (no equational theories yet — strict syntactic match).
- [ ] Tests: peano arithmetic, list manipulation, propositional logic simplifier.
- [x] Apply equations left-to-right until no equation matches.
- [x] Standard pattern matching (no equational theories yet — strict syntactic match).
- [x] Tests: peano arithmetic, list manipulation, propositional logic simplifier.
### Phase 3 — Equational matching (assoc / comm / id)
- [ ] Extend matching to handle `assoc` operators (flatten then match across permutations of subterm groups).
- [ ] Handle `comm` (try both argument orderings).
- [ ] Handle `id: e` (X * e ≡ X).
- [ ] Combinations: `assoc comm id` together.
- [ ] Returns *all* matches, not just first — caller drives.
- [ ] Tests: classic AC-matching examples (multiset rewriting, set theory, group equations).
- [x] Extend matching to handle `assoc` operators (flatten then match across permutations of subterm groups).
- [x] Handle `comm` (try both argument orderings).
- [x] Handle `id: e` (X * e ≡ X).
- [x] Combinations: `assoc comm id` together.
- [x] Returns *all* matches, not just first — caller drives.
- [x] Tests: classic AC-matching examples (multiset rewriting, set theory, group equations).
### Phase 4 — Conditional equations
- [ ] `ceq L = R if Cond` — apply only when `Cond` reduces to true.
- [ ] Recursion via the same reduce engine (terminating because Cond is shorter).
- [ ] Tests: gcd, sorting, conditional simplifications.
- [x] `ceq L = R if Cond` — apply only when `Cond` reduces to true.
- [x] Recursion via the same reduce engine (terminating because Cond is shorter).
- [x] Tests: gcd, sorting, conditional simplifications.
### Phase 5 — System modules + rewrite rules
- [ ] `mod ... endm` syntax with `rl` rules.
- [ ] Rules apply asymmetrically (`=>` not `=`); fairness across rules.
- [ ] Default strategy: top-down, leftmost-outermost, first applicable rule.
- [ ] Tests: state-transition systems (puzzle solvers, protocol simulators).
- [x] `mod ... endm` syntax with `rl` rules.
- [x] Rules apply asymmetrically (`=>` not `=`); fairness across rules.
- [x] Default strategy: top-down, leftmost-outermost, first applicable rule.
- [x] Tests: state-transition systems (puzzle solvers, protocol simulators).
### Phase 6 — Strategy language
- [ ] Compose strategies: sequential `;`, alternative `|`, iteration `*`, fixed-point.
- [ ] User-named strategies; strategy expressions as values.
- [ ] Tests: programs whose meaning depends on strategy choice.
- [x] Compose strategies: sequential `;`, alternative `|`, iteration `*`, fixed-point.
- [x] User-named strategies; strategy expressions as values.
- [x] Tests: programs whose meaning depends on strategy choice.
### Phase 7 — Reflection (META-LEVEL)
- [ ] Terms-as-data: `META-LEVEL` lets you encode/decode terms as Maude terms.
- [ ] Build proofs / programs that manipulate Maude programs.
- [ ] Tests: meta-circular interpretation, generic theorem helpers.
- [x] Terms-as-data: `META-LEVEL` lets you encode/decode terms as Maude terms.
- [x] Build proofs / programs that manipulate Maude programs.
- [x] Tests: meta-circular interpretation, generic theorem helpers.
### Extensions (post-roadmap, toward the end-state goal)
- [x] Mixfix surface-syntax printer (`lib/maude/pretty.sx`) — `mau/term->maude`
renders the internal prefix form back as Maude mixfix (`((s X) + 0)`),
driven by op forms; `mau/red->maude` / `mau/rew->maude`. 11 tests.
- [x] Program runner (`lib/maude/run.sx`) — `mau/run-program` / `mau/run` parse
a module plus trailing `reduce`/`red`/`rewrite`/`rew TERM .` commands
(`... in MOD : TERM` qualifier accepted) and execute them, rendering results
in surface syntax. Runs an idiomatic `.maude` file end-to-end. Now also:
`search START =>* GOAL .` command (reports the path), least-sort annotated
output via `mau/run-pretty``result SORT: TERM` (Maude-style). 10 tests.
- [x] Witness-path search (`lib/maude/searchpath.sx`) — `mau/search-path` /
`mau/search-length` return the shortest sequence of states start..goal (the
solution moves), not just yes/no. 8 tests.
- [x] Order-sorted least-sort inference (`lib/maude/sorts.sx`) — `mau/term-sort`
computes the least sort of a term: the smallest result sort among the op
declarations whose argument sorts the actual args satisfy (modulo subsorting),
so an overloaded `f(1)` is `NzNat` but `f(s 0)` is `Nat`. `mau/has-sort?`
for membership-style checks. Answers the plan's substrate question — order-
sorted signatures fit cleanly. 14 tests.
- [x] `gather` / parse-time associativity — infix ops parse left (default,
`(E e)`) or right (`(e E)`) per the gather attr, so cons `_:_ [gather (e E)]`
reads `a : b : c` as right-nested. Full insertion sort now runs over BARE cons
lists (no parens). 7 tests.
- [x] `owise` equations — parser now reads trailing eq attributes
(`eq L = R [owise] .`), `mau/split-attrs`; `mau/crewrite-top` is two-pass
(ordinary equations first, owise last), so an owise catch-all fires only when
nothing else applies, regardless of declaration order. Parser also reads
`label`/`prec`/`owise`/`id:` eq+op attrs. 8 tests.
### Phase 8 — Propose `lib/guest/rewriting/`
- [ ] Extract equational matching engine (the most reusable piece).
@@ -107,6 +136,49 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
- [ ] Extract strategy combinators.
- [ ] Wait for second consumer before extracting.
**Status: BLOCKED — no second consumer yet.** The reusable core is identified:
`lib/maude/matching.sx` (AC matching + canon) + `lib/maude/fire.sx`
(short-circuit firing) are the prime extraction candidates; `lib/maude/strategy.sx`
(combinators) is the third. Keep them separable. Do not extract until a Pure/
CafeOBJ/term-rewriting playground consumer appears (or artdag-on-sx's effect
optimiser, per the chisel note).
### SATURATION (post-roadmap)
All 7 roadmap phases + 7 extensions (pretty / run / search-path / owise /
gather / order-sorted least-sort / search-command + result-sort) DONE, **254/254
across 13 suites.** The end-state goal — a faithful Maude 3 functional+system
core that runs idiomatic programs and proves equational identities — is met:
sorts/subsorts/overloading, equational reduction modulo assoc/comm/id,
conditional eqs + owise, system rules (rew + BFS search with witness paths),
a strategy language, and META-LEVEL reflection, with a mixfix surface printer
and an end-to-end `.maude` runner (reduce/rewrite/search commands, sort-annotated
output). **artdag-on-sx fit prototype (lib/maude/tests/effects.sx, 8 tests):** artdag's
optimise passes — adjacent-op fusion, no-op/dead-op elim, identity elim,
CSE/idempotent dedup — expressed as `eq`s; the optimised pipeline IS the normal
form, and confluence ⇒ a stable content id. This is the "second consumer"
spike: it justifies a maude-driven optimiser in `lib/artdag` and the eventual
`lib/guest/rewriting/` extraction. Faithfulness note surfaced: `id:` only
affects matching/canon, NOT auto-reduction — write explicit identity eqs (or
read off the canonical form) if you need `0 + N` to reduce in the term itself.
**Confluence / critical-pair checking (lib/maude/confluence.sx, 12 tests):**
`mau/confluent?` answers the plan's substrate question "can confluence be
checked." Two-sided syntactic unification (`mau/u-unify`, with occurs check) →
critical pairs from LHS overlaps (`mau/critical-pairs`) → joinability via
`mau/ac-equal?` of the normal forms (`mau/non-joinable-pairs` gives the
diagnostics, `mau/cp->str` renders `left <?> right`). Caught `f(a)=b, a=c` as
non-confluent (`b <?> f(c)`); confirmed peano/idempotent/AC examples confluent.
SCOPE: unification is SYNTACTIC — exact for free/constructor ops, an
under-approximation for AC overlaps (full AC-unification is NP/infinitary, out
of scope), but joinability uses the AC-canonical form so AC laws still join
correctly. This is the CID-stability oracle for the artdag optimiser: an
optimisation rule set is content-id-stable iff `mau/confluent?` holds.
Pacing down to hardening. Possible niche future work: membership
axioms (`mb`/`cmb`), critical-pair / confluence checking, meta-search, full
mixfix (multi-`_` ops, juxtaposition `__`).
## lib/guest feedback loop
**Consumes:** `core/lex`, `core/pratt`, `core/ast`, `core/match` (with proposed extension for equational matching).
@@ -125,7 +197,129 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
- Pure language (Albrecht Gräf): https://agraef.github.io/pure-lang/ — practical functional rewriting.
## Progress log
_(awaiting Phase 1 — depends on substrate matching maturity from lib/guest/core/match.sx)_
- **Phase 1 (parser + signatures) — DONE, 65/65.** `lib/maude/term.sx` (term
repr: var/app dicts, equality, vars, `term->str`) + `lib/maude/parser.sx`
(whitespace+bracket tokenizer with `---`/`***` comments; mixfix
classification by splitting op names on `_`; precedence-climbing term parser
over a pratt table built from op decls; `fmod`/`mod` modules with
sorts/subsorts/ops/vars/eqs/rules). Consumes `lib/guest/lex.sx` (ws classes)
and `lib/guest/pratt.sx` (op-table lookup). Verified on Peano (`s X + Y`
parses `_+_(s_(X), Y)` — prefix binds tighter than infix) and NatList
(transitive subsorts NzNat<Nat<List; `_;_` overloaded; `id: nil` / `prec`
attrs). ceq/rl/crl parsed structurally (cond split on `if`, label in `[..]`).
Suite + conformance driver wired (`lib/maude/conformance.{conf,sh}`, MODE=dict).
- Notes for next phases: terms are `{:t :app :op N :args (...)}` /
`{:t :var :name N :sort S}`; module carries a `:grammar` so
`mau/parse-term-in` can parse term strings against its op table. Overloading
is recorded but NOT resolved at parse time (resolve at reduce time).
- **Phase 2 (syntactic reduction) — DONE, 91/91 total.** `lib/maude/reduce.sx`:
one-sided syntactic matching (`mau/match` — pattern vars only, non-linear
patterns checked by bound-var equality), immutable substitutions via `assoc`,
`mau/subst-apply`, top rewrite `mau/rewrite-top` (first unconditional eq whose
LHS matches; conditional eqs skipped until Phase 4), innermost normalisation
to a fixpoint `mau/normalize` (args normalised before the operator; fuel-
guarded). API: `mau/reduce` / `mau/reduce-term` / `mau/reduce->str`. Tested on
Peano (+,*), list ops (append/length/rev), a propositional simplifier, and
non-linear `same(X,X)`. Innermost is fine for confluent terminating eq sets;
Phase 3 will replace the matcher with AC-aware matching (multi-valued).
- **Phase 3 (matching modulo assoc/comm/id) — DONE, 119/119 total. THE CHISEL.**
`lib/maude/matching.sx`. `mau/mm` is the multi-valued matcher (returns the
full list of substitutions): free=positional, comm=both orderings,
assoc=flatten f-spine + ordered sequence match (vars grab contiguous blocks),
assoc+comm=multiset match (vars grab sub-multisets via `mau/all-splits` =
2^n subset/complement pairs). `id: e` lets a var grab the empty block
(contributing e); `mau/var-kmin` gives kmin 0 under id. `mau/canon` is the
AC-canonical printout (flatten, drop identities, sort comm args) and powers
`mau/ac-equal?` (used for bound-var checks too). AC *rewriting* extends each
f-AC equation l=r with rest vars — comm: `f(l,$R)`; assoc: `f($L,l,$R)`
so a rule fires on any sub-multiset/subword (`$`-prefixed rest vars allowed
empty). `mau/first-change` walks candidate matches and only commits a rewrite
that changes the canonical form — this is what makes idempotency (`X U X = X`)
and identity-absorbing matches terminate. API: `mau/ac-reduce` /
`mau/ac-reduce->str` / `mau/ac-canon` / `mau/match-all`. Verified: AC match
counts (X+Y vs a+b+c = 6), bag collapse, set dedup with empty, group
cancellation (assoc non-comm + inverse).
- Notes for next phases: AC matching is multi-valued — Phase 5 rule
application should iterate ALL of `mau/mm`'s results, not just first. The
`mau/ac-rewrite-eq` extension trick (rest vars) is the reusable core for
a future `lib/guest/rewriting/` (Phase 8). Keep `mau/canon` as the equality
oracle. `$EMPTY` is a transient marker for empty rest blocks w/o id; never
leaks past `mau/restv`.
- **Phase 4 (conditional equations) — DONE, 138/138 total.**
`lib/maude/conditional.sx` is a condition-aware superset of the Phase 3
reducer. `mau/eq-candidates` enumerates (subst, result) pairs for an
equation (AC via rest-var extension `mau/ac-candidates`, else `mau/mm`);
`mau/try-candidates` commits the first candidate that both makes progress
(canonical form changes) AND whose guard holds. `mau/cond-holds?` evaluates
`{:kind :eq}` guards (reduce both sides, `ac-equal?`) and `{:kind :bool}`
guards (reduce, `=AC= true`), recursing through `mau/cnormalize` — same
reducer, so guards can mention other (conditional) equations. Public:
`mau/creduce` / `mau/creduce->str` / `mau/ccanon`. Verified on gcd
(subtractive, recursive guard), insertion sort (true/false branches), max,
and even (bool-kind `if pred` guard).
- Notes for next phases: `mau/creduce` is the canonical reducer now; Phase 5
rules reduce to normal form via creduce between rewrite steps. `_:_` cons
parses LEFT-assoc (no `gather` support yet) — write list literals
right-parenthesized, or add a `gather`/parse-assoc attr later if a test
needs bare `a : b : c`.
- **Phase 5 (system modules + rewrite rules) — DONE, 159/159 total.**
`lib/maude/rewrite.sx` + `lib/maude/fire.sx`. Rules (rl/crl) reuse the
equation firing machinery (a rule dict is shaped like an eq). `mau/rewrite`
is the default strategy: normalise with eqs (`creduce`), fire ONE rule
top-down/leftmost-outermost/first-applicable, renormalise, repeat (bounded
by fuel). `mau/rew m src n` = bounded `rew [n]`. `mau/search` is BFS over
ALL one-step successors (`mau/all-successors`) for reachability — solves the
branching `goal` reachable only off the path `rew` takes. Verified: AC
multiset coin-change (rule on a sub-multiset), cyclic traffic light (bounded),
branching nondeterminism (rew vs search), conditional `crl` clock, eq/rule
interleaving.
- **PERF (important):** `lib/maude/fire.sx` is the short-circuiting matcher —
`mau/fire-eq` finds the FIRST productive match via predicate-threaded
`mau/ms-find`/`mau/seq-find` instead of materialising the whole solution
set. Without it, AC rewriting on N identical elements is exponential
(`q;q;q;q;q;q;q;q` went 60s+ → <1s). The eager `mau/match-multiset` /
`mau/eq-candidates` are kept ONLY for `mau/match-all` and `search` (which
truly need every solution). Phase 4 `creduce` and Phase 5 rules both fire
via `mau/fire-eq`. Keep this split: never route single-step rewriting
through the eager enumerator.
- Notes: juxtaposition `__` (empty-token mixfix) and `gather` are NOT parsed —
use an explicit infix op for multisets and right-parenthesise list literals.
`.` can't be an op token (statement terminator). `mau/search` is the prime
Phase 7 reflection / Phase 8 extraction target alongside the matcher.
- **Phase 6 (strategy language) — DONE, 178/178 total.**
`lib/maude/strategy.sx`. Strategies are first-class tagged-dict VALUES and
set-valued: `mau/sapply ctx strat term` → deduped (by canon) list of results.
Combinators: `idle`/`fail`/`all`/`rule LABEL`/`seq`/`alt`/`star`/`plus`/`bang`
/`name`. `seq` = flatmap B over A's results; `alt` = union; `star` = reflexive-
transitive closure (BFS, canon-deduped); `plus` = A then star; `bang` =
normal forms (reachable terms where A yields nothing). Named strategies via a
NAME->strategy env dict passed to `mau/srun`/`mau/srun-canon`. Verified that
the same rule set computes different things under different strategies
(single rule vs all vs seq order vs alt vs star vs bang). Built on Phase 5
`mau/all-successors` (rule label filter = `mau/rules-with-label`).
- Note: `dict-set!` returns the value, not the dict — build a named-strategy
env by binding `(define env {})` then `(dict-set! env ...)`, pass `env`.
`srun-canon` sorts results so expected lists must be sorted.
- **Phase 7 (reflection / META-LEVEL) — DONE, 196/196 total.**
`lib/maude/meta.sx`. `mau/up-term` re-encodes an object term as a term built
from meta-constructors `mt-var`(name,sort) / `mt-app`(op, args...) — a
represented term is itself a first-class object term you can build, inspect,
transform. `mau/down-term` reverses (round-trips). Reflective ops:
`mau/meta-reduce` / `mau/meta-rewrite` / `mau/meta-apply LABEL` take and
return represented terms. `mau/meta-circular?` verifies the law
`down(metaReduce(up t)) =AC= reduce t` (reflection agrees with the object
level). `mau/meta-prove-equal?` is a generic equational theorem helper
(prove an identity by joint reduction). Verified: up/down round-trip,
meta-reduce returns a represented normal form, meta-circular law on Peano,
meta-apply of a single rule, commutativity/associativity instance proofs,
and building a program at the meta level then running it.
## Blockers
_(speculative — equational matching is algorithmically heavy and may surface JIT issues)_
_(none)_

View File

@@ -0,0 +1,170 @@
# Re-implementing rose-ash on SX — migration strategy
Status: **strategy proposal** (drafted by the `radar` loop, 2026-06-07). Not a
unilateral architecture decision — a starting point for the fleet to refine. Radar's
role here is detection: the `*-on-sx` subsystems have converged into a host-agnostic
re-implementation of rose-ash's domain logic, so this doc proposes *when* and *how* to
wire them to production.
---
## 1. Premise: we are ~70% into a re-implementation already
The fleet of `lib/<x>` SX subsystems is not a set of experiments — it is rose-ash's
domain logic, re-expressed substrate-by-substrate, deliberately **host-agnostic**:
| SX subsystem (`lib/`) | rose-ash production domain |
|---|---|
| content-on-sx (CRDT docs, versioning, `page.sx` HTML render) | **blog** |
| commerce-on-sx (catalog, pricing, cart, order + refund sagas) | **market + cart + orders** |
| events-on-sx (calendar, ticketing, booking) | **events** |
| feed-on-sx (activity streams, AP-shaped, threading) | **federation** |
| identity-on-sx (OAuth2, sessions, grants, membership) | **account** |
| acl-on-sx (permissions) | cross-cutting authZ |
| relations / likes | **relations / likes** (internal) |
| persist-on-sx (log / kv / snapshot facets) | per-service Postgres layer |
| flow-on-sx (durable sagas) | order/refund/delivery workflows |
| mod-on-sx, search-on-sx | new capabilities |
**The architectural enabler:** every core was built with *injected seams*`permit?`,
`send-fn`/`fetch-fn`, `transport`, `dispatch`, `backend`. That is ports-and-adapters
(hexagonal) on purpose. Evidence from the radar backlog (`plans/abstractions.md`):
W1 (7/7 federation modules inject the fed-sx transport), W4 (content/commerce/events run
live on `persist/log`), W8 (events+commerce run sagas on `lib/flow`). **The cores do not
depend on how they're hosted, persisted, or federated.**
**Corollary that makes the whole migration tractable:** because logic is separated from
rendering and storage, we can hold the **domain logic to parity** while **freely
redesigning the presentation** — the two are different layers with different rules.
---
## 2. The gating insight: the cores are *ahead of the host*
The domain logic is mature. What is *not* yet production-grade is the **host trio** — and
that is the real critical path:
- **host-on-sx** — HTTP / request-response / session host (briefing exists; the OCaml SX
HTTP server already serves `sx.rose-ash.com`).
- **host-persist** — durable storage adapter (real disk/pg/ipfs) under `persist`'s
facets (content-addressed blob blocker recently closed).
- **fed-sx** — the real ActivityPub transport every core injects (well into m2).
> **So "when do we start?" answers itself: start when the host trio is production-grade,
> not when the cores are done — they mostly already are.** Prioritise the host loops over
> further domain features.
---
## 3. The model: duplicate → cut over → diverge (per slice)
This is the "duplicate first, then change" approach, made precise. Each domain slice goes
through three phases independently:
**Phase A — Duplicate (hold logic to parity).** Stand the SX implementation of the slice
up *in parallel*, behind the existing edge, serving no users yet. Get its **domain/data
behaviour** to match Python (see §4 on how). Presentation can start as a rough port or an
early new design — it doesn't have to match.
**Phase B — Cut over (strangler flip).** Point the edge route for that slice at the SX
host. Python stays as instant rollback. The slice is now live on SX.
**Phase C — Diverge (change freely).** With the slice live and validated, evolve the
look/feel and functionality on the SX side. The validated domain logic underneath is
untouched, so UX/feature changes can't silently corrupt data.
You never rewrite the whole platform at once; you walk slices through A→B→C, oldest tree
strangled last.
---
## 4. The two techniques, and how "we'll change things" reshapes them
### Strangler edge
The edge (Caddy) is the front door every request hits. Add routing rules so **one route
at a time** goes to the SX host while everything else still goes to Python. Properties:
the site is never half-broken; any single route flips back to Python instantly; the old
app is strangled route-by-route. (Opposite of big-bang swap, which is how these die.)
### Shadow diff — split by layer
Run the new version on real traffic in the background, discard its output, and **log how
it differs** from Python. Flip the edge only when diffs are zero/intended.
But because we *intend* to change look/feel + functionality, parity is a tool we apply
**only where we want sameness**, not a straitjacket:
| Layer | Want parity? | Oracle |
|---|---|---|
| **Domain/data** (totals, tax, permissions, what's stored, who-sees-what) | **YES — silent difference = data corruption** | shadow-diff at the *core* boundary; deterministic cores → replay real request logs through the harness and diff |
| **Presentation/UX** (HTML, layout, look, feel, flows) | **NO — this is what we're changing** | manual QA + design review; this is the Phase-C divergence |
Practical shape: shadow-diff hits the **domain core's output** (the computed order, the
visible-activity set, the permission decision) — not the rendered HTML. The deterministic,
harness-replayable cores are the single biggest advantage we have here; it's the same
parity discipline that made the A1 conformance migration safe (one reference slice, hard
parity gate, revert on mismatch).
---
## 5. Readiness gates (start the production migration when ALL hold)
1. **Host trio production-grade** — host-on-sx (HTTP/session), host-persist (durable
adapter), fed-sx (AP transport) — each conformance-green.
2. **Data-migration story exists** — a way to get existing production Postgres state into
`persist` event streams (event-source the current state, or dual-write during overlap).
This is the honest long-pole; it is *not* domain logic and nobody has built it yet.
3. **One vertical slice proven end-to-end** at data-parity in production — the reference
migration, the way the conformance loop migrated one subsystem before the rest.
---
## 6. Sequencing
1. **Host trio first** (critical path — it's behind the cores).
2. **Build the strangler edge + shadow-diff harness** as first-class tooling: edge routing
rules + a dual-run logger that diffs *core outputs* (not HTML) and stores discrepancies.
3. **First slice = lowest risk × highest readiness × cleanest data oracle.**
Recommended: **the blog read path (content-on-sx)** or **the feed read path**
— read-heavy, no money, CRDT/versioning + `page.sx` HTML already exist, and the data
oracle is clean. *Avoid cart/orders/payments first* (transactional + SumUp webhooks =
highest blast radius).
4. **Persistence-first, federation-last.** Land host-persist + migrate per-domain event
stores before any cutover. Do fed-sx federation as a *coordinated* cut near the end —
W1 shows all 7 cores light up federation together once the shared transport ships.
5. **Walk the remaining slices A→B→C**, retiring Python routes as each cuts over.
---
## 7. The honest long tail (mostly host + adapters, not cores)
The cores are pure domain logic; the production *tail* is not in them yet and is most of
the remaining real effort:
- Auth: first-party cookies / Safari-ITP, CSRF, silent SSO, grant caching.
- Cross-cutting: rate limiting, observability/metrics, error pages, caching.
- Integrations: SumUp payment + webhooks, Ghost CMS sync.
- Presentation: the actual HTMX templates + CSS (this is also where the redesign happens).
- **Live data migration** — the single biggest non-core workstream.
---
## 8. Concrete next steps
1. Treat the **host trio** as the fleet's critical path; prioritise over more domain features.
2. Stand up the **strangler edge + core-level shadow-diff harness** as a tool.
3. Prove **one slice** (blog/content read path) end-to-end in production as the reference.
4. **Spec the Postgres → persist data migration** (the long-pole nobody has started).
5. Then walk slices through duplicate → cut over → diverge, redesigning UX in Phase C.
---
## 9. Why this is low-risk despite being a platform rewrite
- It's **wiring host-agnostic cores to a host**, not rewriting domain logic from scratch.
- The **strangler edge** means the site always works and any route reverts in seconds.
- **Deterministic cores** make data-parity *mechanically checkable* (replay + diff), so
correctness isn't a matter of faith.
- **Logic/presentation separation** lets us change look/feel + functionality (Phase C)
*without* re-risking the validated domain logic.
- It's the **same discipline that just shipped A1**: one reference migration, a hard
parity gate, honest exclusions, verify-before-merge.