;; lib/maude/tests/confluence.sx — critical-pair / local-confluence checking.

(define mcf-pass 0)
(define mcf-fail 0)
(define mcf-failures (list))

(define
  mcf-check!
  (fn
    (name got expected)
    (if
      (= got expected)
      (set! mcf-pass (+ mcf-pass 1))
      (do
        (set! mcf-fail (+ mcf-fail 1))
        (append!
          mcf-failures
          (str name "  expected: " expected "  got: " got))))))

;; peano addition: no LHS overlaps -> confluent
(define
  mcf-peano
  (mau/parse-module
    "fmod P is\n  sort Nat .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op _+_ : Nat Nat -> Nat .\n  vars X Y : Nat .\n  eq 0 + Y = Y .\n  eq s X + Y = s (X + Y) .\nendfm"))

(mcf-check! "peano-confluent" (mau/confluent? mcf-peano) true)
(mcf-check!
  "peano-no-bad-pairs"
  (len (mau/non-joinable-pairs mcf-peano))
  0)

;; f(a)=b, a=c : the inner `a` overlaps -> critical pair b vs f(c), NOT joinable
(define
  mcf-bad
  (mau/parse-module
    "fmod B is\n  sort T .\n  op a : -> T .\n  op b : -> T .\n  op c : -> T .\n  op f : T -> T .\n  eq f(a) = b .\n  eq a = c .\nendfm"))

(mcf-check! "bad-not-confluent" (mau/confluent? mcf-bad) false)
(mcf-check! "bad-one-pair" (len (mau/non-joinable-pairs mcf-bad)) 1)
(mcf-check!
  "bad-pair-shape"
  (mau/cp->str mcf-bad (first (mau/non-joinable-pairs mcf-bad)))
  "b <?> f(c)")
(mcf-check!
  "bad-has-cps"
  (> (len (mau/critical-pairs mcf-bad)) 0)
  true)

;; adding f(c)=b joins the pair -> confluent
(define
  mcf-fixed
  (mau/parse-module
    "fmod F is\n  sort T .\n  op a : -> T .\n  op b : -> T .\n  op c : -> T .\n  op f : T -> T .\n  eq f(a) = b .\n  eq a = c .\n  eq f(c) = b .\nendfm"))

(mcf-check! "fixed-confluent" (mau/confluent? mcf-fixed) true)

;; self-overlap that is joinable: idempotent d(d(X)) = d(X)
(define
  mcf-idem
  (mau/parse-module
    "fmod I is\n  sort T .\n  op d : T -> T .\n  op x : -> T .\n  var X : T .\n  eq d(d(X)) = d(X) .\nendfm"))

(mcf-check! "idem-confluent" (mau/confluent? mcf-idem) true)

;; a free-op overlap that joins: g(h(X)) over h(a)
(define
  mcf-join
  (mau/parse-module
    "fmod J is\n  sort T .\n  op a : -> T .\n  op k : -> T .\n  op h : T -> T .\n  op g : T -> T .\n  op r : T -> T .\n  var X : T .\n  eq g(h(X)) = r(X) .\n  eq h(a) = k .\nendfm"))

;; g(h(a)) -> r(a) (rule1) or g(k) (rule2 inside). Not joinable unless g(k) reduces.
(mcf-check! "join-not-confluent" (mau/confluent? mcf-join) false)

;; AC operator, genuinely confluent; joinability uses canonical form
(define
  mcf-ac
  (mau/parse-module
    "fmod AC is\n  sort S .\n  op a : -> S .\n  op b : -> S .\n  op _+_ : S S -> S [assoc comm] .\n  eq a + a = b .\nendfm"))

(mcf-check! "ac-confluent" (mau/confluent? mcf-ac) true)

;; unifier sanity (two-sided): f(X, b) unifies with f(a, Y)
(mcf-check!
  "unify-twosided"
  (=
    nil
    (mau/u-unify
      (mau/app "f" (list (mau/var "X" "T") (mau/const "b")))
      (mau/app "f" (list (mau/const "a") (mau/var "Y" "T")))
      {}))
  false)
;; occurs check: X vs f(X) fails
(mcf-check!
  "unify-occurs"
  (mau/u-unify
    (mau/var "X" "T")
    (mau/app "f" (list (mau/var "X" "T")))
    {})
  nil)

(define mau-confluence-tests-run! (fn () {:failures mcf-failures :total (+ mcf-pass mcf-fail) :passed mcf-pass :failed mcf-fail}))