;; lib/datalog/tests/unify.sx — unification + substitution tests.

(define dl-ut-pass 0)
(define dl-ut-fail 0)
(define dl-ut-failures (list))

(define
  dl-ut-deep-equal?
  (fn
    (a b)
    (cond
      ((and (list? a) (list? b))
        (and (= (len a) (len b)) (dl-ut-deq-list? a b 0)))
      ((and (dict? a) (dict? b))
        (let
          ((ka (keys a)) (kb (keys b)))
          (and (= (len ka) (len kb)) (dl-ut-deq-dict? a b ka 0))))
      ((and (number? a) (number? b)) (= a b))
      (else (equal? a b)))))

(define
  dl-ut-deq-list?
  (fn
    (a b i)
    (cond
      ((>= i (len a)) true)
      ((not (dl-ut-deep-equal? (nth a i) (nth b i))) false)
      (else (dl-ut-deq-list? a b (+ i 1))))))

(define
  dl-ut-deq-dict?
  (fn
    (a b ka i)
    (cond
      ((>= i (len ka)) true)
      ((let ((k (nth ka i))) (not (dl-ut-deep-equal? (get a k) (get b k))))
        false)
      (else (dl-ut-deq-dict? a b ka (+ i 1))))))

(define
  dl-ut-test!
  (fn
    (name got expected)
    (if
      (dl-ut-deep-equal? got expected)
      (set! dl-ut-pass (+ dl-ut-pass 1))
      (do
        (set! dl-ut-fail (+ dl-ut-fail 1))
        (append!
          dl-ut-failures
          (str name "\n    expected: " expected "\n    got:      " got))))))

(define
  dl-ut-run-all!
  (fn
    ()
    (do
      (dl-ut-test! "var? uppercase" (dl-var? (quote X)) true)
      (dl-ut-test! "var? underscore" (dl-var? (quote _foo)) true)
      (dl-ut-test! "var? lowercase" (dl-var? (quote tom)) false)
      (dl-ut-test! "var? number" (dl-var? 5) false)
      (dl-ut-test! "var? string" (dl-var? "hi") false)
      (dl-ut-test! "var? list" (dl-var? (list 1)) false)
      (dl-ut-test!
        "atom-atom match"
        (dl-unify (quote tom) (quote tom) (dl-empty-subst))
        {})
      (dl-ut-test!
        "atom-atom fail"
        (dl-unify (quote tom) (quote bob) (dl-empty-subst))
        nil)
      (dl-ut-test!
        "num-num match"
        (dl-unify 5 5 (dl-empty-subst))
        {})
      (dl-ut-test!
        "num-num fail"
        (dl-unify 5 6 (dl-empty-subst))
        nil)
      (dl-ut-test!
        "string match"
        (dl-unify "hi" "hi" (dl-empty-subst))
        {})
      (dl-ut-test! "string fail" (dl-unify "hi" "bye" (dl-empty-subst)) nil)
      (dl-ut-test!
        "var-atom binds"
        (dl-unify (quote X) (quote tom) (dl-empty-subst))
        {:X (quote tom)})
      (dl-ut-test!
        "atom-var binds"
        (dl-unify (quote tom) (quote X) (dl-empty-subst))
        {:X (quote tom)})
      (dl-ut-test!
        "var-var same"
        (dl-unify (quote X) (quote X) (dl-empty-subst))
        {})
      (dl-ut-test!
        "var-var bind"
        (let
          ((s (dl-unify (quote X) (quote Y) (dl-empty-subst))))
          (dl-walk (quote X) s))
        (quote Y))
      (dl-ut-test!
        "tuple match"
        (dl-unify
          (list (quote parent) (quote X) (quote bob))
          (list (quote parent) (quote tom) (quote Y))
          (dl-empty-subst))
        {:X (quote tom) :Y (quote bob)})
      (dl-ut-test!
        "tuple arity mismatch"
        (dl-unify
          (list (quote p) (quote X))
          (list (quote p) (quote a) (quote b))
          (dl-empty-subst))
        nil)
      (dl-ut-test!
        "tuple head mismatch"
        (dl-unify
          (list (quote p) (quote X))
          (list (quote q) (quote X))
          (dl-empty-subst))
        nil)
      (dl-ut-test!
        "walk chain"
        (let
          ((s1 (dl-unify (quote X) (quote Y) (dl-empty-subst))))
          (let
            ((s2 (dl-unify (quote Y) (quote tom) s1)))
            (dl-walk (quote X) s2)))
        (quote tom))
      (dl-ut-test!
        "apply subst on tuple"
        (let
          ((s (dl-bind (quote X) (quote tom) (dl-empty-subst))))
          (dl-apply-subst (list (quote parent) (quote X) (quote Y)) s))
        (list (quote parent) (quote tom) (quote Y)))
      (dl-ut-test!
        "ground? all const"
        (dl-ground?
          (list (quote p) (quote tom) 5)
          (dl-empty-subst))
        true)
      (dl-ut-test!
        "ground? unbound var"
        (dl-ground? (list (quote p) (quote X)) (dl-empty-subst))
        false)
      (dl-ut-test!
        "ground? bound var"
        (let
          ((s (dl-bind (quote X) (quote tom) (dl-empty-subst))))
          (dl-ground? (list (quote p) (quote X)) s))
        true)
      (dl-ut-test!
        "ground? bare var"
        (dl-ground? (quote X) (dl-empty-subst))
        false)
      (dl-ut-test!
        "vars-of basic"
        (dl-vars-of
          (list (quote p) (quote X) (quote tom) (quote Y) (quote X)))
        (list "X" "Y"))
      (dl-ut-test!
        "vars-of ground"
        (dl-vars-of (list (quote p) (quote tom) (quote bob)))
        (list))
      (dl-ut-test!
        "vars-of nested compound"
        (dl-vars-of
          (list
            (quote is)
            (quote Z)
            (list (string->symbol "+") (quote X) 1)))
        (list "Z" "X")))))

(define
  dl-unify-tests-run!
  (fn
    ()
    (do
      (set! dl-ut-pass 0)
      (set! dl-ut-fail 0)
      (set! dl-ut-failures (list))
      (dl-ut-run-all!)
      {:failures dl-ut-failures :total (+ dl-ut-pass dl-ut-fail) :passed dl-ut-pass :failed dl-ut-fail})))