; lib/artdag/optimize-rules.sx — Phase 7: optimisation laws as a confluent maude module.
; The optimised effect pipeline IS the normal form of the rule set, so confluence
; (mau/confluent?) is exactly content-id stability: every rewrite order reaches the
; same normal form. Media ops (blur/bright/id/over) are the opaque-op model from
; lib/maude/tests/effects.sx — the engine reasons about the pipeline algebra, never
; pixels. The radius algebra is an AC operator with identity 0 (unary 1s): Peano
; successor rules (s M + N = s(M+N), 0 + N = N) are NOT confluent here (the symbolic
; critical pairs M + 0 and (A+B)+C vs A+(B+C) stick), whereas [assoc comm id: 0]
; joins them via canonical form. maude (lib/maude) is a READ-ONLY consumed substrate:
; mau/parse-module, mau/creduce-term, mau/creduce->str, mau/ccanon, mau/confluent?,
; mau/non-joinable-pairs, mau/cp->str.

(define
  artdag/opt-module-src
  (str
    "fmod ARTDAGOPT is\n"
    "  sorts Img Num .\n"
    "  op 0 : -> Num .\n"
    "  op 1 : -> Num .\n"
    "  op _+_ : Num Num -> Num [assoc comm id: 0] .\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 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 .\n"
    "endfm"))

(define artdag/opt-module (mau/parse-module artdag/opt-module-src))

; ---- reduce a surface pipeline to its optimised normal form ----

(define
  artdag/opt-reduce-term
  (fn (src) (mau/creduce-term artdag/opt-module src)))

(define
  artdag/opt-normal-form
  (fn (src) (mau/creduce->str artdag/opt-module src)))

(define artdag/opt-canon (fn (src) (mau/ccanon artdag/opt-module src)))

; two surface pipelines optimise to the same pipeline (=> same content id) iff
; their normal forms coincide.
(define
  artdag/opt-same-form?
  (fn (a b) (= (artdag/opt-normal-form a) (artdag/opt-normal-form b))))

; ---- confluence / content-id stability (consume lib/maude/confluence.sx) ----

(define artdag/opt-confluent? (fn () (mau/confluent? artdag/opt-module)))

(define
  artdag/opt-non-joinable
  (fn () (mau/non-joinable-pairs artdag/opt-module)))

(define
  artdag/opt-non-joinable->strs
  (fn
    ()
    (map
      (fn (cp) (mau/cp->str artdag/opt-module cp))
      (artdag/opt-non-joinable))))