giles
d2f6bf02b3
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 1m7s
lib/maude/tests/effects.sx — proves artdag's effect-pipeline optimisations (fusion, no-op/dead-op elim, identity elim, CSE/idempotent dedup) are equational rewriting: the optimised pipeline is the normal form, confluence gives a stable content id. The 'second consumer' spike for a maude-driven optimiser in lib/artdag. Surfaced faithfulness note: id: affects matching/canon not auto-reduction. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
80 lines
3.1 KiB
Plaintext
80 lines
3.1 KiB
Plaintext
;; 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}))
|