maude: owise (otherwise) equations (8 tests, 229 total)

Parser reads trailing eq attributes (eq L = R [owise] .) via mau/split-attrs.
mau/crewrite-top is two-pass: ordinary equations first, owise last — an owise
catch-all fires only when no ordinary equation applies, regardless of
declaration order. Verified a catch-all declared first still defers.

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

lib/maude/conditional.sx

@@ -1,4 +1,4 @@
-;; lib/maude/conditional.sx — conditional equations (Phase 4).
+;; 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
@@ -10,10 +10,13 @@
 ;; — 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) so reduction is not quadratic/exponential in AC argument size.
+;; (mau/fire-eq). The eager candidate enumeration (mau/eq-candidates) is
-;; The eager candidate enumeration (mau/eq-candidates) is retained for `search`
+;; retained for `search` (rewrite.sx), which genuinely needs every successor.
-;; (rewrite.sx), which genuinely needs every successor.
 
 (define
   mau/ac-candidates
@@ -86,6 +89,14 @@
           (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
@@ -99,7 +110,14 @@
 
 (define
   mau/crewrite-top
-  (fn (theory eqs term) (mau/crewrite-loop theory eqs eqs term)))
+  (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

lib/maude/conformance.conf

@@ -25,6 +25,7 @@ SUITES=(
   "reduce:lib/maude/tests/reduce.sx:(mau-reduce-tests-run!)"
   "matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)"
   "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)"
+  "owise:lib/maude/tests/owise.sx:(mau-owise-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!)"

lib/maude/parser.sx

@@ -13,8 +13,8 @@
 ;;   subsort/subsorts A B < C < D .
 ;;   op/ops NAMES : ARITY -> RESULT [ATTRS] .
 ;;   var/vars NAMES : SORT .
-;;   eq LHS = RHS .            ceq LHS = RHS if COND .
+;;   eq LHS = RHS [ATTRS] .       ceq LHS = RHS if COND [ATTRS] .
-;;   rl [L] : LHS => RHS .     crl [L] : LHS => RHS if COND .
+;;   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
@@ -384,6 +384,8 @@
               (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))
@@ -392,6 +394,10 @@
               (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))))
             (else (loop (rest ts))))))
       (do (loop toks) acc))))
 
@@ -404,6 +410,9 @@
       {}
       (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
@@ -514,9 +523,9 @@
         conditional?
         (let
           ((rhs-toks (mau/take-until after "if"))
-            (cond-toks (rest (mau/drop-until after "if"))))
+            (cond-raw (rest (mau/drop-until after "if"))))
-          {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond (mau/parse-cond cond-toks grammar) :rhs (mau/parse-term rhs-toks grammar)})
+          (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)}))
-        {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond nil :rhs (mau/parse-term after grammar)}))))
+        (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
@@ -548,8 +557,8 @@
             (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 cond-toks grammar) :rhs (mau/parse-term rhs-toks grammar)})
+              {: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 after 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!

lib/maude/scoreboard.json

@@ -1,13 +1,14 @@
 {
   "lang": "maude",
-  "total_passed": 221,
+  "total_passed": 229,
   "total_failed": 0,
-  "total": 221,
+  "total": 229,
   "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":"owise","passed":8,"failed":0,"total":8},
     {"name":"rewrite","passed":21,"failed":0,"total":21},
     {"name":"searchpath","passed":8,"failed":0,"total":8},
     {"name":"strategy","passed":19,"failed":0,"total":19},
@@ -15,5 +16,5 @@
     {"name":"pretty","passed":11,"failed":0,"total":11},
     {"name":"run","passed":6,"failed":0,"total":6}
   ],
-  "generated": "2026-06-07T15:36:28+00:00"
+  "generated": "2026-06-07T15:39:50+00:00"
 }

lib/maude/scoreboard.md

@@ -1,6 +1,6 @@
 # maude scoreboard
 
-**221 / 221 passing** (0 failure(s)).
+**229 / 229 passing** (0 failure(s)).
 
 | Suite | Passed | Total | Status |
 |-------|--------|-------|--------|
@@ -8,6 +8,7 @@
 | reduce | 26 | 26 | ok |
 | matching | 28 | 28 | ok |
 | conditional | 19 | 19 | ok |
+| owise | 8 | 8 | ok |
 | rewrite | 21 | 21 | ok |
 | searchpath | 8 | 8 | ok |
 | strategy | 19 | 19 | ok |

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

plans/maude-on-sx.md

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