;; lib/maude/confluence.sx — critical-pair / local-confluence checking.
;;
;; A terminating equation set is confluent iff every critical pair is joinable
;; (Knuth-Bendix / Newman). A critical pair arises when two oriented equations
;; overlap: a non-variable subterm of one LHS unifies with the other LHS, giving
;; two ways to rewrite the overlap; they must reduce to the same normal form.
;;
;; This needs TWO-SIDED unification (variables on both sides), not the one-sided
;; matching the reducer uses — so this file carries its own syntactic unifier.
;;
;; SCOPE / honesty: the unifier is SYNTACTIC. For free/constructor operators the
;; check is exact. For assoc/comm (AC) operators it sees only syntactic overlaps
;; (full AC-unification is NP/infinitary — out of scope), but joinability is
;; tested with `mau/ac-equal?` (canonical form modulo the theory), so AC laws are
;; joined correctly even though their overlaps are under-approximated. Conditional
;; and `owise` equations are not oriented (skipped).

;; ---------- syntactic unification (vars on both sides) ----------

(define
  mau/u-walk
  (fn
    (t s)
    (if
      (mau/var? t)
      (let
        ((b (get s (mau/vname t))))
        (if (= b nil) t (mau/u-walk b s)))
      t)))

(define
  mau/u-occurs?
  (fn
    (name t s)
    (let
      ((w (mau/u-walk t s)))
      (cond
        ((mau/var? w) (= (mau/vname w) name))
        ((mau/app? w) (mau/u-occurs-any? name (mau/args w) s))
        (else false)))))

(define
  mau/u-occurs-any?
  (fn
    (name args s)
    (cond
      ((empty? args) false)
      ((mau/u-occurs? name (first args) s) true)
      (else (mau/u-occurs-any? name (rest args) s)))))

(define
  mau/u-unify-args
  (fn
    (as bs s)
    (cond
      ((= s nil) nil)
      ((and (empty? as) (empty? bs)) s)
      ((or (empty? as) (empty? bs)) nil)
      (else
        (mau/u-unify-args
          (rest as)
          (rest bs)
          (mau/u-unify (first as) (first bs) s))))))

(define
  mau/u-unify
  (fn
    (t1 t2 s)
    (if
      (= s nil)
      nil
      (let
        ((a (mau/u-walk t1 s)) (b (mau/u-walk t2 s)))
        (cond
          ((and (mau/var? a) (mau/var? b) (= (mau/vname a) (mau/vname b)))
            s)
          ((mau/var? a)
            (if
              (mau/u-occurs? (mau/vname a) b s)
              nil
              (assoc s (mau/vname a) b)))
          ((mau/var? b)
            (if
              (mau/u-occurs? (mau/vname b) a s)
              nil
              (assoc s (mau/vname b) a)))
          ((and (mau/app? a) (mau/app? b))
            (if
              (and
                (= (mau/op a) (mau/op b))
                (= (mau/arity a) (mau/arity b)))
              (mau/u-unify-args (mau/args a) (mau/args b) s)
              nil))
          (else nil))))))

(define
  mau/u-apply
  (fn
    (t s)
    (let
      ((w (mau/u-walk t s)))
      (if
        (mau/app? w)
        (mau/app
          (mau/op w)
          (map (fn (a) (mau/u-apply a s)) (mau/args w)))
        w))))

(define
  mau/u-rename
  (fn
    (t suffix)
    (cond
      ((mau/var? t) (mau/var (str (mau/vname t) suffix) (mau/vsort t)))
      ((mau/app? t)
        (mau/app
          (mau/op t)
          (map (fn (a) (mau/u-rename a suffix)) (mau/args t))))
      (else t))))

;; ---------- positions ----------

(define
  mau/positions-args
  (fn
    (args i)
    (if
      (empty? args)
      (list)
      (mau/append2
        (map (fn (p) (cons i p)) (mau/nv-positions (first args)))
        (mau/positions-args (rest args) (+ i 1))))))

;; non-variable positions (paths) of a term; root = empty path
(define
  mau/nv-positions
  (fn
    (t)
    (if
      (mau/app? t)
      (cons (list) (mau/positions-args (mau/args t) 0))
      (list))))

(define
  mau/at-path
  (fn
    (t path)
    (if
      (empty? path)
      t
      (mau/at-path (nth (mau/args t) (first path)) (rest path)))))

(define
  mau/replace-nth
  (fn
    (xs i v)
    (if
      (= i 0)
      (cons v (rest xs))
      (cons (first xs) (mau/replace-nth (rest xs) (- i 1) v)))))

(define
  mau/replace-at
  (fn
    (t path new)
    (if
      (empty? path)
      new
      (mau/app
        (mau/op t)
        (mau/replace-nth
          (mau/args t)
          (first path)
          (mau/replace-at (nth (mau/args t) (first path)) (rest path) new))))))

;; ---------- critical pairs ----------

(define
  mau/eq-same?
  (fn
    (e1 e2)
    (and
      (mau/term=? (get e1 :lhs) (get e2 :lhs))
      (mau/term=? (get e1 :rhs) (get e2 :rhs)))))

(define
  mau/cps-at
  (fn
    (l1 r1 l2 r2 same? paths)
    (if
      (empty? paths)
      (list)
      (let
        ((p (first paths)))
        (if
          (and same? (empty? p))
          (mau/cps-at l1 r1 l2 r2 same? (rest paths))
          (let
            ((s (mau/u-unify (mau/at-path l1 p) l2 {})))
            (if
              (= s nil)
              (mau/cps-at l1 r1 l2 r2 same? (rest paths))
              (cons {:right (mau/u-apply (mau/replace-at l1 p r2) s) :left (mau/u-apply r1 s)} (mau/cps-at l1 r1 l2 r2 same? (rest paths))))))))))

(define
  mau/cps-of
  (fn
    (e1 e2)
    (let
      ((l1 (mau/u-rename (get e1 :lhs) "#1"))
        (r1 (mau/u-rename (get e1 :rhs) "#1"))
        (l2 (mau/u-rename (get e2 :lhs) "#2"))
        (r2 (mau/u-rename (get e2 :rhs) "#2")))
      (mau/cps-at l1 r1 l2 r2 (mau/eq-same? e1 e2) (mau/nv-positions l1)))))

(define
  mau/all-cps
  (fn
    (eqs)
    (mau/concat-map
      (fn (e1) (mau/concat-map (fn (e2) (mau/cps-of e1 e2)) eqs))
      eqs)))

;; ---------- public API ----------

(define
  mau/orientable-eqs
  (fn
    (m)
    (filter
      (fn (e) (and (= (get e :cond) nil) (not (= (get e :owise) true))))
      (mau/module-eqs m))))

(define
  mau/joinable?
  (fn
    (theory eqs t1 t2)
    (mau/ac-equal?
      theory
      (mau/cnormalize theory eqs t1 mau/reduce-fuel)
      (mau/cnormalize theory eqs t2 mau/reduce-fuel))))

(define mau/critical-pairs (fn (m) (mau/all-cps (mau/orientable-eqs m))))

(define
  mau/non-joinable-pairs
  (fn
    (m)
    (let
      ((theory (mau/build-theory m)) (eqs (mau/module-eqs m)))
      (filter
        (fn
          (cp)
          (not (mau/joinable? theory eqs (get cp :left) (get cp :right))))
        (mau/all-cps (mau/orientable-eqs m))))))

(define mau/confluent? (fn (m) (empty? (mau/non-joinable-pairs m))))

(define
  mau/cp->str
  (fn
    (m cp)
    (let
      ((theory (mau/build-theory m)))
      (str
        (mau/canon theory (get cp :left))
        " <?> "
        (mau/canon theory (get cp :right))))))