maude: run.sx search command + result-sort output (254 total)

run.sx now handles 'search START =>* GOAL .' (reports the witness path) and
mau/run-pretty prints Maude-style 'result SORT: TERM' using least-sort
inference. searchpath.sx exposes mau/search-path-terms (term-level entry).

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

lib/maude/run.sx

@@ -4,8 +4,13 @@
 ;; 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). Results are rendered in mixfix surface syntax.
+;; 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
@@ -27,7 +32,6 @@
         name
         (mau/take (mau/drop toks 3) (- (len toks) 4))))))
 
-;; strip an optional `in MODNAME :` qualifier from a command's term tokens
 (define
   mau/strip-in
   (fn
@@ -37,18 +41,49 @@
       (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)) (term-toks (mau/strip-in (rest stmt))))
-      (let
-        ((t (mau/parse-term term-toks (mau/module-grammar m))))
-        (cond
-          ((or (= head "reduce") (= head "red")) {:cmd "reduce" :result (mau/term->maude m (mau/creduce m t))})
-          ((or (= head "rewrite") (= head "rew")) {:cmd "rewrite" :result (mau/term->maude m (mau/rewrite m t))})
-          (else {:cmd head :result "?"}))))))
+      ((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
@@ -77,7 +112,21 @@
             (cmd-toks (mau/drop toks (+ eidx 1))))
           (mau/run-commands m (mau/split-statements cmd-toks)))))))
 
-;; convenience: just the rendered result strings
+;; 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

@@ -1,8 +1,8 @@
 {
   "lang": "maude",
-  "total_passed": 250,
+  "total_passed": 254,
   "total_failed": 0,
-  "total": 250,
+  "total": 254,
   "suites": [
     {"name":"parse","passed":65,"failed":0,"total":65},
     {"name":"reduce","passed":26,"failed":0,"total":26},
@@ -16,7 +16,7 @@
     {"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":6,"failed":0,"total":6}
+    {"name":"run","passed":10,"failed":0,"total":10}
   ],
-  "generated": "2026-06-07T15:46:14+00:00"
+  "generated": "2026-06-07T15:49:17+00:00"
 }

lib/maude/scoreboard.md

@@ -1,6 +1,6 @@
 # maude scoreboard
 
-**250 / 250 passing** (0 failure(s)).
+**254 / 254 passing** (0 failure(s)).
 
 | Suite | Passed | Total | Status |
 |-------|--------|-------|--------|
@@ -16,4 +16,4 @@
 | strategy | 19 | 19 | ok |
 | meta | 18 | 18 | ok |
 | pretty | 11 | 11 | ok |
-| run | 6 | 6 | ok |
+| run | 10 | 10 | ok |

lib/maude/searchpath.sx

@@ -61,24 +61,21 @@
               goal
               (- depth 1))))))))
 
+;; term-level: returns the canonical-state path start..goal, or nil
 (define
-  mau/search-path
+  mau/search-path-terms
   (fn
-    (m start-src goal-src max-depth)
+    (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 (mau/parse-term-in m start-src) mau/reduce-fuel))
+        ((start (mau/cnormalize theory eqs start-term mau/reduce-fuel))
           (goal
             (mau/canon
               theory
-              (mau/cnormalize
-                theory
-                eqs
-                (mau/parse-term-in m goal-src)
-                mau/reduce-fuel))))
+              (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
@@ -86,6 +83,16 @@
             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

lib/maude/tests/run.sx

@@ -19,7 +19,7 @@
 
 (define
   mrn-peano
-  "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\nred s 0 + s s 0 .\nred 0 + 0 .\nreduce in PEANO : s s 0 * s s 0 .")
+  "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"
@@ -32,6 +32,15 @@
   (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 .")
@@ -43,6 +52,24 @@
   (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"

plans/maude-on-sx.md

@@ -108,7 +108,9 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
 - [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. 6 tests.
+  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.