;; lib/datalog/unify.sx — unification + substitution for Datalog terms.
;;
;; Term taxonomy (after parsing):
;;   variable  — SX symbol whose first char is uppercase A–Z or '_'.
;;   constant  — SX symbol whose first char is lowercase a–z (atom name).
;;   number    — numeric literal.
;;   string    — string literal.
;;   compound  — SX list (functor arg ... arg). In core Datalog these
;;               only appear as arithmetic expressions (see Phase 4
;;               safety analysis); compound-against-compound unification
;;               is supported anyway for completeness.
;;
;; Substitutions are immutable dicts keyed by variable name (string).
;; A failed unification returns nil; success returns the extended subst.

(define dl-empty-subst (fn () {}))

(define
  dl-var?
  (fn
    (term)
    (and
      (symbol? term)
      (let
        ((name (symbol->string term)))
        (and
          (> (len name) 0)
          (let
            ((c (slice name 0 1)))
            (or (and (>= c "A") (<= c "Z")) (= c "_"))))))))

;; Walk: chase variable bindings until we hit a non-variable or an unbound
;; variable. The result is either a non-variable term or an unbound var.
(define
  dl-walk
  (fn
    (term subst)
    (if
      (dl-var? term)
      (let
        ((name (symbol->string term)))
        (if
          (and (dict? subst) (has-key? subst name))
          (dl-walk (get subst name) subst)
          term))
      term)))

;; Bind a variable symbol to a value in subst, returning a new subst.
(define
  dl-bind
  (fn (var-sym value subst) (assoc subst (symbol->string var-sym) value)))

(define
  dl-unify
  (fn
    (t1 t2 subst)
    (if
      (nil? subst)
      nil
      (let
        ((u1 (dl-walk t1 subst)) (u2 (dl-walk t2 subst)))
        (cond
          ((dl-var? u1)
            (cond
              ((and (dl-var? u2) (= (symbol->string u1) (symbol->string u2)))
                subst)
              (else (dl-bind u1 u2 subst))))
          ((dl-var? u2) (dl-bind u2 u1 subst))
          ((and (list? u1) (list? u2))
            (if
              (= (len u1) (len u2))
              (dl-unify-list u1 u2 subst 0)
              nil))
          ((and (number? u1) (number? u2)) (if (= u1 u2) subst nil))
          ((and (string? u1) (string? u2)) (if (= u1 u2) subst nil))
          ((and (symbol? u1) (symbol? u2))
            (if (= (symbol->string u1) (symbol->string u2)) subst nil))
          (else nil))))))

(define
  dl-unify-list
  (fn
    (a b subst i)
    (cond
      ((nil? subst) nil)
      ((>= i (len a)) subst)
      (else
        (dl-unify-list
          a
          b
          (dl-unify (nth a i) (nth b i) subst)
          (+ i 1))))))

;; Apply substitution: walk the term and recurse into lists.
(define
  dl-apply-subst
  (fn
    (term subst)
    (let
      ((w (dl-walk term subst)))
      (if (list? w) (map (fn (x) (dl-apply-subst x subst)) w) w))))

;; Ground? — true iff no free variables remain after walking.
(define
  dl-ground?
  (fn
    (term subst)
    (let
      ((w (dl-walk term subst)))
      (cond
        ((dl-var? w) false)
        ((list? w) (dl-ground-list? w subst 0))
        (else true)))))

(define
  dl-ground-list?
  (fn
    (xs subst i)
    (cond
      ((>= i (len xs)) true)
      ((not (dl-ground? (nth xs i) subst)) false)
      (else (dl-ground-list? xs subst (+ i 1))))))

;; Return the list of variable names appearing in a term (deduped, in
;; left-to-right order). Useful for safety analysis later.
(define
  dl-vars-of
  (fn (term) (let ((seen (list))) (do (dl-vars-of-aux term seen) seen))))

(define
  dl-vars-of-aux
  (fn
    (term acc)
    (cond
      ((dl-var? term)
        (let
          ((name (symbol->string term)))
          (when (not (dl-member? name acc)) (append! acc name))))
      ((list? term) (dl-vars-of-list term acc 0))
      (else nil))))

(define
  dl-vars-of-list
  (fn
    (xs acc i)
    (when
      (< i (len xs))
      (do
        (dl-vars-of-aux (nth xs i) acc)
        (dl-vars-of-list xs acc (+ i 1))))))

(define
  dl-member?
  (fn
    (x xs)
    (cond
      ((= (len xs) 0) false)
      ((= (first xs) x) true)
      (else (dl-member? x (rest xs))))))