From cc0f3f1ff7323a87845ec5cec7aa31136d396cb5 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:40:11 +0000 Subject: [PATCH] maude: owise (otherwise) equations (8 tests, 229 total) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- lib/maude/conditional.sx | 28 +++++++++++++---- lib/maude/conformance.conf | 1 + lib/maude/parser.sx | 23 +++++++++----- lib/maude/scoreboard.json | 7 +++-- lib/maude/scoreboard.md | 3 +- lib/maude/tests/owise.sx | 61 ++++++++++++++++++++++++++++++++++++++ plans/maude-on-sx.md | 5 ++++ 7 files changed, 112 insertions(+), 16 deletions(-) create mode 100644 lib/maude/tests/owise.sx diff --git a/lib/maude/conditional.sx b/lib/maude/conditional.sx index 31c76965..5411f2b7 100644 --- a/lib/maude/conditional.sx +++ b/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. -;; The eager candidate enumeration (mau/eq-candidates) is retained for `search` -;; (rewrite.sx), which genuinely needs every successor. +;; (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 @@ -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 diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index e8ca5d13..51249a66 100644 --- a/lib/maude/conformance.conf +++ b/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!)" diff --git a/lib/maude/parser.sx b/lib/maude/parser.sx index 0196e9fc..13cf03bf 100644 --- a/lib/maude/parser.sx +++ b/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 . -;; rl [L] : LHS => RHS . crl [L] : LHS => RHS if COND . +;; 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 @@ -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")))) - {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond (mau/parse-cond cond-toks grammar) :rhs (mau/parse-term rhs-toks grammar)}) - {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond nil :rhs (mau/parse-term after grammar)})))) + (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 @@ -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 nil :rhs (mau/parse-term after 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 (get (mau/split-attrs after) :term) grammar)})))))) (define mau/collect-rules! diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index ac74ee99..7cd864a9 100644 --- a/lib/maude/scoreboard.json +++ b/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" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index 66199e2a..c092d674 100644 --- a/lib/maude/scoreboard.md +++ b/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 | diff --git a/lib/maude/tests/owise.sx b/lib/maude/tests/owise.sx new file mode 100644 index 00000000..ba8f003c --- /dev/null +++ b/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})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index d5dda65d..8c69c575 100644 --- a/plans/maude-on-sx.md +++ b/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).