;; lib/datalog/tests/negation.sx — stratified negation tests.

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

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

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

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

(define
  dl-nt-set=?
  (fn
    (a b)
    (and
      (= (len a) (len b))
      (dl-nt-subset? a b)
      (dl-nt-subset? b a))))

(define
  dl-nt-subset?
  (fn
    (xs ys)
    (cond
      ((= (len xs) 0) true)
      ((not (dl-nt-contains? ys (first xs))) false)
      (else (dl-nt-subset? (rest xs) ys)))))

(define
  dl-nt-contains?
  (fn
    (xs target)
    (cond
      ((= (len xs) 0) false)
      ((dl-nt-deep=? (first xs) target) true)
      (else (dl-nt-contains? (rest xs) target)))))

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

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

(define
  dl-nt-throws?
  (fn
    (thunk)
    (let
      ((threw false))
      (do
        (guard
          (e (#t (set! threw true)))
          (thunk))
        threw))))

(define
  dl-nt-run-all!
  (fn
    ()
    (do
      ;; Negation against EDB-only relation.
      (dl-nt-test-set! "not against EDB"
        (dl-query
          (dl-program
            "p(1). p(2). p(3). r(2).
             q(X) :- p(X), not(r(X)).")
          (list (quote q) (quote X)))
        (list {:X 1} {:X 3}))

      ;; Negation against derived relation — needs stratification.
      (dl-nt-test-set! "not against derived rel"
        (dl-query
          (dl-program
            "p(1). p(2). p(3). s(2).
             r(X) :- s(X).
             q(X) :- p(X), not(r(X)).")
          (list (quote q) (quote X)))
        (list {:X 1} {:X 3}))

      ;; Two-step strata: r derives via s; q derives via not r.
      (dl-nt-test-set! "two-step strata"
        (dl-query
          (dl-program
            "node(a). node(b). node(c). node(d).
             edge(a, b). edge(b, c). edge(c, a).
             reach(X, Y) :- edge(X, Y).
             reach(X, Z) :- edge(X, Y), reach(Y, Z).
             unreachable(X) :- node(X), not(reach(a, X)).")
          (list (quote unreachable) (quote X)))
        (list {:X (quote d)}))

      ;; Combine negation with arithmetic and comparison.
      (dl-nt-test-set! "negation with arithmetic"
        (dl-query
          (dl-program
            "n(1). n(2). n(3). n(4). n(5). odd(1). odd(3). odd(5).
             even(X) :- n(X), not(odd(X)).")
          (list (quote even) (quote X)))
        (list {:X 2} {:X 4}))

      ;; Empty negation result.
      (dl-nt-test-set! "negation always succeeds"
        (dl-query
          (dl-program
            "p(1). p(2). q(X) :- p(X), not(r(X)).")
          (list (quote q) (quote X)))
        (list {:X 1} {:X 2}))

      ;; Negation always fails.
      (dl-nt-test-set! "negation always fails"
        (dl-query
          (dl-program
            "p(1). p(2). r(1). r(2). q(X) :- p(X), not(r(X)).")
          (list (quote q) (quote X)))
        (list))

      ;; Stratifiability checks.
      (dl-nt-test! "non-stratifiable rejected"
        (dl-nt-throws?
          (fn ()
            (let ((db (dl-make-db)))
              (do
                (dl-add-rule!
                  db
                  {:head (list (quote p) (quote X))
                   :body (list (list (quote q) (quote X))
                               {:neg (list (quote r) (quote X))})})
                (dl-add-rule!
                  db
                  {:head (list (quote r) (quote X))
                   :body (list (list (quote p) (quote X)))})
                (dl-add-fact! db (list (quote q) 1))
                (dl-saturate! db)))))
        true)

      (dl-nt-test! "stratifiable accepted"
        (dl-nt-throws?
          (fn ()
            (dl-program
              "p(1). p(2). r(2).
               q(X) :- p(X), not(r(X)).")))
        false)

      ;; Multi-stratum chain.
      (dl-nt-test-set! "three-level strata"
        (dl-query
          (dl-program
            "a(1). a(2). a(3). a(4).
             b(X) :- a(X), not(c(X)).
             c(X) :- d(X).
             d(2).
             d(4).")
          (list (quote b) (quote X)))
        (list {:X 1} {:X 3}))

      ;; Safety violation: negation refers to unbound var.
      (dl-nt-test! "negation safety violation"
        (dl-nt-throws?
          (fn ()
            (dl-program
              "p(1). q(X) :- p(X), not(r(Y)).")))
        true))))

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