maude: Phase 6 strategy language (19 tests, 178 total)

lib/maude/strategy.sx — first-class set-valued strategies: idle/fail/all/
rule/seq/alt/star/plus/bang/name combinators, named-strategy env. Same
rule set computes different things under different strategies; verified
with single-rule vs all vs seq-order vs alt vs star vs bang.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

lib/maude/conformance.conf

@@ -13,6 +13,7 @@ PRELOADS=(
   lib/maude/conditional.sx
   lib/maude/fire.sx
   lib/maude/rewrite.sx
+  lib/maude/strategy.sx
 )
 
 SUITES=(
@@ -21,4 +22,5 @@ SUITES=(
   "matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)"
   "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)"
   "rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-tests-run!)"
+  "strategy:lib/maude/tests/strategy.sx:(mau-strategy-tests-run!)"
 )

lib/maude/scoreboard.json

@@ -1,14 +1,15 @@
 {
   "lang": "maude",
-  "total_passed": 159,
+  "total_passed": 178,
   "total_failed": 0,
-  "total": 159,
+  "total": 178,
   "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":"conditional","passed":19,"failed":0,"total":19},
-    {"name":"rewrite","passed":21,"failed":0,"total":21}
+    {"name":"rewrite","passed":21,"failed":0,"total":21},
+    {"name":"strategy","passed":19,"failed":0,"total":19}
   ],
-  "generated": "2026-06-07T15:22:28+00:00"
+  "generated": "2026-06-07T15:26:26+00:00"
 }

lib/maude/scoreboard.md

@@ -1,6 +1,6 @@
 # maude scoreboard
 
-**159 / 159 passing** (0 failure(s)).
+**178 / 178 passing** (0 failure(s)).
 
 | Suite | Passed | Total | Status |
 |-------|--------|-------|--------|
@@ -9,3 +9,4 @@
 | matching | 28 | 28 | ok |
 | conditional | 19 | 19 | ok |
 | rewrite | 21 | 21 | ok |
+| strategy | 19 | 19 | ok |

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

@@ -92,9 +92,9 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
 - [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.
@@ -220,5 +220,20 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
     `.` 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.
+
 ## Blockers
 _(none)_