maude: confluence / critical-pair checking (12 tests, 274 total)

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>

lib/maude/conditional.sx

@@ -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))))

lib/maude/confluence.sx

@@ -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))))))

lib/maude/conformance.conf

@@ -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!)"
+)

lib/maude/conformance.sh

@@ -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" "$@"

lib/maude/fire.sx

@@ -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 {}))))))

lib/maude/matching.sx

@@ -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))))

lib/maude/meta.sx

@@ -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))))

lib/maude/parser.sx

@@ -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)))

lib/maude/pretty.sx

@@ -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))))

lib/maude/reduce.sx

@@ -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))))

lib/maude/rewrite.sx

@@ -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)))))

lib/maude/run.sx

@@ -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))))

lib/maude/scoreboard.json

@@ -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"
+}

lib/maude/scoreboard.md

@@ -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 |

lib/maude/searchpath.sx

@@ -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)))))

lib/maude/sorts.sx

@@ -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)))

lib/maude/strategy.sx

@@ -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))))))

lib/maude/term.sx

@@ -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))))))

lib/maude/tests/conditional.sx

@@ -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}))

lib/maude/tests/confluence.sx

@@ -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}))

lib/maude/tests/effects.sx

@@ -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}))

lib/maude/tests/gather.sx

@@ -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}))

lib/maude/tests/matching.sx

@@ -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}))

lib/maude/tests/meta.sx

@@ -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}))

lib/maude/tests/owise.sx

@@ -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}))

lib/maude/tests/parse.sx

@@ -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}))

lib/maude/tests/pretty.sx

@@ -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}))

lib/maude/tests/reduce.sx

@@ -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}))

lib/maude/tests/rewrite.sx

@@ -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}))

lib/maude/tests/run.sx

@@ -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}))

lib/maude/tests/searchpath.sx

@@ -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}))

lib/maude/tests/sorts.sx

@@ -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}))

lib/maude/tests/strategy.sx

@@ -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}))

plans/maude-on-sx.md

@@ -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)_