;; lib/datalog/tests/eval.sx — naive evaluation + safety analysis tests.

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

;; Same deep-equal helper used in other suites.
(define
  dl-et-deep=?
  (fn
    (a b)
    (cond
      ((and (list? a) (list? b))
        (and (= (len a) (len b)) (dl-et-deq-l? a b 0)))
      ((and (dict? a) (dict? b))
        (let
          ((ka (keys a)) (kb (keys b)))
          (and (= (len ka) (len kb)) (dl-et-deq-d? a b ka 0))))
      ((and (number? a) (number? b)) (= a b))
      (else (equal? a b)))))

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

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

;; Set-equality on lists (order-independent, uses dl-et-deep=?).
(define
  dl-et-set=?
  (fn
    (a b)
    (and (= (len a) (len b)) (dl-et-subset? a b) (dl-et-subset? b a))))

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

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

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

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

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

(define
  dl-et-run-all!
  (fn
    ()
    (do
      (dl-et-test-set!
        "fact lookup any"
        (dl-query
          (dl-program "parent(tom, bob). parent(bob, ann).")
          (list (quote parent) (quote X) (quote Y)))
        (list {:X (quote tom) :Y (quote bob)} {:X (quote bob) :Y (quote ann)}))
      (dl-et-test-set!
        "fact lookup constant arg"
        (dl-query
          (dl-program "parent(tom, bob). parent(tom, liz). parent(bob, ann).")
          (list (quote parent) (quote tom) (quote Y)))
        (list {:Y (quote bob)} {:Y (quote liz)}))
      (dl-et-test-set!
        "no match"
        (dl-query
          (dl-program "parent(tom, bob).")
          (list (quote parent) (quote nobody) (quote X)))
        (list))
      (dl-et-test-set!
        "ancestor closure"
        (dl-query
          (dl-program
            "parent(tom, bob). parent(bob, ann). parent(ann, pat).\n             ancestor(X, Y) :- parent(X, Y).\n             ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z).")
          (list (quote ancestor) (quote tom) (quote X)))
        (list {:X (quote bob)} {:X (quote ann)} {:X (quote pat)}))
      (dl-et-test-set!
        "sibling"
        (dl-query
          (dl-program
            "parent(tom, bob). parent(tom, liz). parent(jane, bob). parent(jane, liz).\n             sibling(X, Y) :- parent(P, X), parent(P, Y).")
          (list (quote sibling) (quote bob) (quote Y)))
        (list {:Y (quote bob)} {:Y (quote liz)}))
      (dl-et-test-set!
        "same-generation"
        (dl-query
          (dl-program
            "parent(tom, bob). parent(tom, liz). parent(bob, ann). parent(liz, joe).\n             person(tom). person(bob). person(liz). person(ann). person(joe).\n             sg(X, X) :- person(X).\n             sg(X, Y) :- parent(P1, X), sg(P1, P2), parent(P2, Y).")
          (list (quote sg) (quote ann) (quote X)))
        (list {:X (quote ann)} {:X (quote joe)}))
      (dl-et-test!
        "ancestor count"
        (let
          ((db (dl-program "parent(a, b). parent(b, c). parent(c, d).\n                  ancestor(X, Y) :- parent(X, Y).\n                  ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z).")))
          (do (dl-saturate! db) (len (dl-relation db "ancestor"))))
        6)
      (dl-et-test-set!
        "grandparent"
        (dl-query
          (dl-program
            "parent(a, b). parent(b, c). parent(c, d).\n             grandparent(X, Z) :- parent(X, Y), parent(Y, Z).")
          (list (quote grandparent) (quote X) (quote Y)))
        (list {:X (quote a) :Y (quote c)} {:X (quote b) :Y (quote d)}))
      (dl-et-test!
        "no recursion infinite loop"
        (let
          ((db (dl-program "edge(1, 2). edge(2, 3). edge(3, 1).\n                  reach(X, Y) :- edge(X, Y).\n                  reach(X, Z) :- edge(X, Y), reach(Y, Z).")))
          (do (dl-saturate! db) (len (dl-relation db "reach"))))
        9)
      ;; Rule-shape sanity: empty-list head and non-list body raise
      ;; clear errors rather than crashing inside the saturator.
      (dl-et-test! "empty head rejected"
        (dl-et-throws?
          (fn ()
            (dl-add-rule! (dl-make-db)
              {:head (list) :body (list)})))
        true)

      (dl-et-test! "non-list body rejected"
        (dl-et-throws?
          (fn ()
            (dl-add-rule! (dl-make-db)
              {:head (list (quote p) (quote X)) :body 42})))
        true)

      ;; Reserved relation names rejected as rule/fact heads.
      (dl-et-test!
        "reserved name `not` as head rejected"
        (dl-et-throws? (fn () (dl-program "not(X) :- p(X).")))
        true)

      (dl-et-test!
        "reserved name `count` as head rejected"
        (dl-et-throws?
          (fn () (dl-program "count(N, X, p(X)) :- p(X).")))
        true)

      (dl-et-test!
        "reserved name `<` as head rejected"
        (dl-et-throws? (fn () (dl-program "<(X, 5) :- p(X).")))
        true)

      (dl-et-test!
        "reserved name `is` as head rejected"
        (dl-et-throws? (fn () (dl-program "is(N, +(1, 2)) :- p(N).")))
        true)

      ;; Body literal with a reserved-name positive head is rejected.
      ;; The parser only treats outer-level `not(P)` as negation; nested
      ;; `not(not(P))` would otherwise silently parse as a positive call
      ;; to a relation named `not` and succeed vacuously. The safety
      ;; checker now flags this so the user gets a clear error.
      ;; Body literal with a reserved-name positive head is rejected.
      ;; The parser only treats outer-level `not(P)` as negation; nested
      ;; `not(not(P))` would otherwise silently parse as a positive call
      ;; to a relation named `not` and succeed vacuously — so the safety
      ;; checker now flags this to give the user a clear error.
      (dl-et-test!
        "nested not(not(...)) rejected"
        (dl-et-throws?
          (fn ()
            (dl-program
              "banned(a). u(a). vip(X) :- u(X), not(not(banned(X))).")))
        true)

      ;; A dict body literal that isn't `{:neg ...}` is almost always a
      ;; typo — it would otherwise silently fall through to a confusing
      ;; head-var-unbound safety error. Now caught with a clear message.
      (dl-et-test!
        "dict body lit without :neg rejected"
        (dl-et-throws?
          (fn ()
            (let ((db (dl-make-db)))
              (dl-add-rule! db
                {:head (list (quote p) (quote X))
                 :body (list {:weird "stuff"})}))))
        true)

      ;; Facts may only have simple-term args (number / string / symbol).
      ;; A compound arg like `+(1, 2)` would otherwise be silently
      ;; stored as the unreduced expression `(+ 1 2)` because dl-ground?
      ;; sees no free variables.
      (dl-et-test!
        "compound arg in fact rejected"
        (dl-et-throws? (fn () (dl-program "p(+(1, 2)).")))
        true)

      ;; Rule heads may only have variable or constant args — no
      ;; compounds. Compound heads would be saturated as unreduced
      ;; tuples rather than the arithmetic result the user expected.
      (dl-et-test!
        "compound arg in rule head rejected"
        (dl-et-throws?
          (fn () (dl-program "n(3). double(*(X, 2)) :- n(X).")))
        true)

      ;; The anonymous-variable renamer used to start at `_anon1`
      ;; unconditionally; a rule that wrote `q(_anon1) :- p(_anon1, _)`
      ;; (the user picking the same name the renamer would generate)
      ;; would see the `_` renamed to `_anon1` too, collapsing the
      ;; two positions in `p(_anon1, _)` to a single var. Now the
      ;; renamer scans the rule for the max `_anon<N>` and starts past
      ;; it, so user-written names of that form are preserved.
      (dl-et-test-set! "anonymous-rename avoids user `_anon` collision"
        (dl-query
          (dl-program
            "p(a, b). p(c, d). q(_anon1) :- p(_anon1, _).")
          (quote (q X)))
        (list {:X (quote a)} {:X (quote c)}))

      (dl-et-test!
        "unsafe head var"
        (dl-et-throws? (fn () (dl-program "p(X, Y) :- q(X).")))
        true)
      (dl-et-test!
        "unsafe — empty body"
        (dl-et-throws? (fn () (dl-program "p(X) :- .")))
        true)
      ;; Underscore in head is unsafe — it's a fresh existential per
      ;; occurrence after Phase 5d's anonymous-var renaming, and there's
      ;; nothing in the body to bind it. (Old behavior accepted this by
      ;; treating '_' as a literal name to skip; the renaming made it an
      ;; ordinary unbound variable.)
      (dl-et-test!
        "underscore in head — unsafe"
        (dl-et-throws? (fn () (dl-program "p(X, _) :- q(X).")))
        true)
      (dl-et-test!
        "underscore in body only — safe"
        (dl-et-throws? (fn () (dl-program "p(X) :- q(X, _).")))
        false)
      (dl-et-test!
        "var only in head — unsafe"
        (dl-et-throws? (fn () (dl-program "p(X, Y) :- q(Z).")))
        true)
      (dl-et-test!
        "head var bound by body"
        (dl-et-throws? (fn () (dl-program "p(X) :- q(X).")))
        false)
      (dl-et-test!
        "head subset of body"
        (dl-et-throws?
          (fn
            ()
            (dl-program
              "edge(a,b). edge(b,c). reach(X, Z) :- edge(X, Y), edge(Y, Z).")))
        false)

      ;; Anonymous variables: each occurrence must be independent.
      (dl-et-test-set! "anon vars in rule are independent"
        (dl-query
          (dl-program
            "p(a, b). p(c, d). q(X) :- p(X, _), p(_, Y).")
          (list (quote q) (quote X)))
        (list {:X (quote a)} {:X (quote c)}))

      (dl-et-test-set! "anon vars in goal are independent"
        (dl-query
          (dl-program "p(1, 2, 3). p(4, 5, 6).")
          (list (quote p) (quote _) (quote X) (quote _)))
        (list {:X 2} {:X 5}))

      ;; dl-summary: relation -> tuple-count for inspection.
      (dl-et-test! "dl-summary basic"
        (dl-summary
          (let
            ((db (dl-program "p(1). p(2). q(3).")))
            (do (dl-saturate! db) db)))
        {:p 2 :q 1})

      (dl-et-test! "dl-summary empty IDB shown"
        (dl-summary
          (let
            ((db (dl-program "r(X) :- s(X).")))
            (do (dl-saturate! db) db)))
        {:r 0})

      (dl-et-test! "dl-summary mixed EDB and IDB"
        (dl-summary
          (let
            ((db (dl-program
                   "parent(a, b).
                    ancestor(X, Y) :- parent(X, Y).
                    ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z).")))
            (do (dl-saturate! db) db)))
        {:parent 1 :ancestor 1})

      (dl-et-test! "dl-summary empty db"
        (dl-summary (dl-make-db))
        {})

      ;; Strategy hook: default semi-naive; :magic accepted but
      ;; falls back to semi-naive (the transformation itself is
      ;; deferred — Phase 6 in plan).
      (dl-et-test! "default strategy"
        (dl-get-strategy (dl-make-db))
        :semi-naive)

      (dl-et-test! "set strategy"
        (let ((db (dl-make-db)))
          (do (dl-set-strategy! db :magic) (dl-get-strategy db)))
        :magic)

      ;; Unknown strategy values are rejected so typos don't silently
      ;; fall back to the default.
      (dl-et-test!
        "unknown strategy rejected"
        (dl-et-throws?
          (fn ()
            (let ((db (dl-make-db)))
              (dl-set-strategy! db :semi_naive))))
        true)

      ;; dl-saturated?: no-work-left predicate.
      (dl-et-test! "saturated? after saturation"
        (let ((db (dl-program
                    "parent(a, b).
                     ancestor(X, Y) :- parent(X, Y).")))
          (do (dl-saturate! db) (dl-saturated? db)))
        true)

      (dl-et-test! "saturated? before saturation"
        (let ((db (dl-program
                    "parent(a, b).
                     ancestor(X, Y) :- parent(X, Y).")))
          (dl-saturated? db))
        false)

      ;; Disjunction via multiple rules — Datalog has no `;` in
      ;; body, so disjunction is expressed as separate rules with
      ;; the same head. Here plant_based(X) is satisfied by either
      ;; vegan(X) or vegetarian(X).
      (dl-et-test-set! "disjunction via multiple rules"
        (dl-query
          (dl-program
            "vegan(alice). vegetarian(bob). meat_eater(carol).
             plant_based(X) :- vegan(X).
             plant_based(X) :- vegetarian(X).")
          (list (quote plant_based) (quote X)))
        (list {:X (quote alice)} {:X (quote bob)}))

      ;; Bipartite-style join: pair-of-friends who share a hobby.
      ;; Three-relation join exercising the planner's join order.
      (dl-et-test-set! "bipartite friends-with-hobby"
        (dl-query
          (dl-program
            "hobby(alice, climb). hobby(bob, paint).
             hobby(carol, climb).
             friend(alice, carol). friend(bob, alice).
             match(A, B, H) :- friend(A, B), hobby(A, H), hobby(B, H).")
          (list (quote match) (quote A) (quote B) (quote H)))
        (list {:A (quote alice) :B (quote carol) :H (quote climb)}))

      ;; Repeated variable (diagonal): p(X, X) only matches tuples
      ;; whose two args are equal. The unifier handles this via the
      ;; subst chain — first occurrence binds X, second occurrence
      ;; checks against the binding.
      (dl-et-test-set! "diagonal query"
        (dl-query
          (dl-program "p(1, 1). p(2, 3). p(4, 4). p(5, 5).")
          (list (quote p) (quote X) (quote X)))
        (list {:X 1} {:X 4} {:X 5}))

      ;; A relation can be both EDB-seeded and rule-derived;
      ;; saturate combines facts + derivations.
      (dl-et-test-set! "mixed EDB + IDB same relation"
        (dl-query
          (dl-program
            "link(a, b). link(c, d). link(e, c).
             via(a, e).
             link(X, Y) :- via(X, M), link(M, Y).")
          (list (quote link) (quote a) (quote X)))
        (list {:X (quote b)} {:X (quote c)}))

      (dl-et-test! "saturated? after assert"
        (let ((db (dl-program
                    "parent(a, b).
                     ancestor(X, Y) :- parent(X, Y).")))
          (do
            (dl-saturate! db)
            (dl-add-fact! db (list (quote parent) (quote b) (quote c)))
            (dl-saturated? db)))
        false)

      (dl-et-test-set! "magic-set still derives correctly"
        (let
          ((db (dl-program
                 "parent(a, b). parent(b, c).
                  ancestor(X, Y) :- parent(X, Y).
                  ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z).")))
          (do
            (dl-set-strategy! db :magic)
            (dl-query db (list (quote ancestor) (quote a) (quote X)))))
        (list {:X (quote b)} {:X (quote c)})))))

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