diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index c9aa1d3e..5286e343 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -35,4 +35,5 @@ SUITES=( "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!)" ) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index 65d16819..886b34b1 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,8 +1,8 @@ { "lang": "maude", - "total_passed": 254, + "total_passed": 262, "total_failed": 0, - "total": 254, + "total": 262, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, {"name":"reduce","passed":26,"failed":0,"total":26}, @@ -16,7 +16,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":"run","passed":10,"failed":0,"total":10}, + {"name":"effects","passed":8,"failed":0,"total":8} ], - "generated": "2026-06-07T15:51:45+00:00" + "generated": "2026-06-07T19:38:27+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index cf8fd781..cfb8c57d 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,6 +1,6 @@ # maude scoreboard -**254 / 254 passing** (0 failure(s)). +**262 / 262 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -17,3 +17,4 @@ | meta | 18 | 18 | ok | | pretty | 11 | 11 | ok | | run | 10 | 10 | ok | +| effects | 8 | 8 | ok | diff --git a/lib/maude/tests/effects.sx b/lib/maude/tests/effects.sx new file mode 100644 index 00000000..a22a18d9 --- /dev/null +++ b/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})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index adaf76ea..447049f9 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -153,7 +153,16 @@ 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). Pacing down to hardening. Possible niche future work: membership +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. + +Pacing down to hardening. Possible niche future work: membership axioms (`mb`/`cmb`), critical-pair / confluence checking, meta-search, full mixfix (multi-`_` ops, juxtaposition `__`).