;; lib/prolog/tests/solve.sx — DFS solver unit tests

(define pl-s-test-count 0)
(define pl-s-test-pass 0)
(define pl-s-test-fail 0)
(define pl-s-test-failures (list))

(define
  pl-s-test!
  (fn
    (name got expected)
    (begin
      (set! pl-s-test-count (+ pl-s-test-count 1))
      (if
        (= got expected)
        (set! pl-s-test-pass (+ pl-s-test-pass 1))
        (begin
          (set! pl-s-test-fail (+ pl-s-test-fail 1))
          (append!
            pl-s-test-failures
            (str name "\n    expected: " expected "\n    got:      " got)))))))

(define
  pl-s-goal
  (fn
    (src env)
    (pl-instantiate (nth (first (pl-parse (str "g :- " src "."))) 2) env)))

(define pl-s-empty-db (pl-mk-db))

(pl-s-test!
  "true succeeds"
  (pl-solve-once! pl-s-empty-db (pl-s-goal "true" {}) (pl-mk-trail))
  true)

(pl-s-test!
  "fail fails"
  (pl-solve-once! pl-s-empty-db (pl-s-goal "fail" {}) (pl-mk-trail))
  false)

(pl-s-test!
  "= identical atoms"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal "=(a, a)" {})
    (pl-mk-trail))
  true)

(pl-s-test!
  "= different atoms"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal "=(a, b)" {})
    (pl-mk-trail))
  false)

(pl-s-test!
  "= var to atom"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal "=(X, foo)" {})
    (pl-mk-trail))
  true)

(define pl-s-env-bind {})
(define pl-s-trail-bind (pl-mk-trail))
(define pl-s-goal-bind (pl-s-goal "=(X, foo)" pl-s-env-bind))
(pl-solve-once! pl-s-empty-db pl-s-goal-bind pl-s-trail-bind)

(pl-s-test!
  "X bound to foo after =(X, foo)"
  (pl-atom-name (pl-walk-deep (dict-get pl-s-env-bind "X")))
  "foo")

(pl-s-test!
  "true , true succeeds"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal "true, true" {})
    (pl-mk-trail))
  true)

(pl-s-test!
  "true , fail fails"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal "true, fail" {})
    (pl-mk-trail))
  false)

(pl-s-test!
  "consistent X bindings succeed"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal "=(X, a), =(X, a)" {})
    (pl-mk-trail))
  true)

(pl-s-test!
  "conflicting X bindings fail"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal "=(X, a), =(X, b)" {})
    (pl-mk-trail))
  false)

(define pl-s-db1 (pl-mk-db))
(pl-db-load!
  pl-s-db1
  (pl-parse "parent(tom, bob). parent(bob, liz). parent(bob, ann)."))

(pl-s-test!
  "fact lookup hit"
  (pl-solve-once!
    pl-s-db1
    (pl-s-goal "parent(tom, bob)" {})
    (pl-mk-trail))
  true)

(pl-s-test!
  "fact lookup miss"
  (pl-solve-once!
    pl-s-db1
    (pl-s-goal "parent(tom, liz)" {})
    (pl-mk-trail))
  false)

(pl-s-test!
  "all parent solutions"
  (pl-solve-count!
    pl-s-db1
    (pl-s-goal "parent(X, Y)" {})
    (pl-mk-trail))
  3)

(pl-s-test!
  "fixed first arg solutions"
  (pl-solve-count!
    pl-s-db1
    (pl-s-goal "parent(bob, Y)" {})
    (pl-mk-trail))
  2)

(define pl-s-db2 (pl-mk-db))
(pl-db-load!
  pl-s-db2
  (pl-parse
    "parent(tom, bob). parent(bob, ann). ancestor(X, Y) :- parent(X, Y). ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z)."))

(pl-s-test!
  "rule direct ancestor"
  (pl-solve-once!
    pl-s-db2
    (pl-s-goal "ancestor(tom, bob)" {})
    (pl-mk-trail))
  true)

(pl-s-test!
  "rule transitive ancestor"
  (pl-solve-once!
    pl-s-db2
    (pl-s-goal "ancestor(tom, ann)" {})
    (pl-mk-trail))
  true)

(pl-s-test!
  "rule no path"
  (pl-solve-once!
    pl-s-db2
    (pl-s-goal "ancestor(ann, tom)" {})
    (pl-mk-trail))
  false)

(define pl-s-env-undo {})
(define pl-s-trail-undo (pl-mk-trail))
(define pl-s-goal-undo (pl-s-goal "=(X, a), fail" pl-s-env-undo))
(pl-solve-once! pl-s-empty-db pl-s-goal-undo pl-s-trail-undo)

(pl-s-test!
  "trail undone after failure leaves X unbound"
  (pl-var-bound? (dict-get pl-s-env-undo "X"))
  false)

(define pl-s-db-cut1 (pl-mk-db))

(pl-db-load! pl-s-db-cut1 (pl-parse "g :- !. g :- true."))

(pl-s-test!
  "bare cut succeeds"
  (pl-solve-once! pl-s-db-cut1 (pl-s-goal "g" {}) (pl-mk-trail))
  true)

(pl-s-test!
  "cut commits to first matching clause"
  (pl-solve-count! pl-s-db-cut1 (pl-s-goal "g" {}) (pl-mk-trail))
  1)

(define pl-s-db-cut2 (pl-mk-db))

(pl-db-load! pl-s-db-cut2 (pl-parse "a(1). a(2). g(X) :- a(X), !."))

(pl-s-test!
  "cut commits to first a solution"
  (pl-solve-count! pl-s-db-cut2 (pl-s-goal "g(X)" {}) (pl-mk-trail))
  1)

(define pl-s-db-cut3 (pl-mk-db))

(pl-db-load!
  pl-s-db-cut3
  (pl-parse "a(1). a(2). g(X) :- a(X), !, fail. g(99)."))

(pl-s-test!
  "cut then fail blocks alt clauses"
  (pl-solve-count! pl-s-db-cut3 (pl-s-goal "g(X)" {}) (pl-mk-trail))
  0)

(define pl-s-db-cut4 (pl-mk-db))

(pl-db-load!
  pl-s-db-cut4
  (pl-parse "a(1). b(10). b(20). g(X, Y) :- a(X), !, b(Y)."))

(pl-s-test!
  "post-cut goal backtracks freely"
  (pl-solve-count!
    pl-s-db-cut4
    (pl-s-goal "g(X, Y)" {})
    (pl-mk-trail))
  2)

(define pl-s-db-cut5 (pl-mk-db))

(pl-db-load!
  pl-s-db-cut5
  (pl-parse "r(1). r(2). q :- r(X), !. p :- q. p :- true."))

(pl-s-test!
  "inner cut does not commit outer predicate"
  (pl-solve-count! pl-s-db-cut5 (pl-s-goal "p" {}) (pl-mk-trail))
  2)

(pl-s-test!
  "\\= different atoms succeeds"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal "\\=(a, b)" {})
    (pl-mk-trail))
  true)

(pl-s-test!
  "\\= same atoms fails"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal "\\=(a, a)" {})
    (pl-mk-trail))
  false)

(pl-s-test!
  "\\= var-vs-atom would unify so fails"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal "\\=(X, a)" {})
    (pl-mk-trail))
  false)

(define pl-s-env-ne {})

(define pl-s-trail-ne (pl-mk-trail))

(define pl-s-goal-ne (pl-s-goal "\\=(X, a)" pl-s-env-ne))

(pl-solve-once! pl-s-empty-db pl-s-goal-ne pl-s-trail-ne)

(pl-s-test!
  "\\= leaves no bindings"
  (pl-var-bound? (dict-get pl-s-env-ne "X"))
  false)

(pl-s-test!
  "; left succeeds"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal ";(true, fail)" {})
    (pl-mk-trail))
  true)

(pl-s-test!
  "; right succeeds when left fails"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal ";(fail, true)" {})
    (pl-mk-trail))
  true)

(pl-s-test!
  "; both fail"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal ";(fail, fail)" {})
    (pl-mk-trail))
  false)

(pl-s-test!
  "; both branches counted"
  (pl-solve-count!
    pl-s-empty-db
    (pl-s-goal ";(true, true)" {})
    (pl-mk-trail))
  2)

(define pl-s-db-call (pl-mk-db))

(pl-db-load! pl-s-db-call (pl-parse "p(1). p(2)."))

(pl-s-test!
  "call(true) succeeds"
  (pl-solve-once!
    pl-s-db-call
    (pl-s-goal "call(true)" {})
    (pl-mk-trail))
  true)

(pl-s-test!
  "call(p(X)) yields all solutions"
  (pl-solve-count!
    pl-s-db-call
    (pl-s-goal "call(p(X))" {})
    (pl-mk-trail))
  2)

(pl-s-test!
  "call of bound goal var resolves"
  (pl-solve-once!
    pl-s-db-call
    (pl-s-goal "=(G, true), call(G)" {})
    (pl-mk-trail))
  true)

(define pl-s-db-ite (pl-mk-db))

(pl-db-load! pl-s-db-ite (pl-parse "p(1). p(2). q(yes). q(no)."))

(pl-s-test!
  "if-then-else: cond true → then runs"
  (pl-solve-once!
    pl-s-db-ite
    (pl-s-goal ";(->(true, =(X, ok)), =(X, fallback))" {})
    (pl-mk-trail))
  true)

(define pl-s-env-ite1 {})

(pl-solve-once!
  pl-s-db-ite
  (pl-s-goal ";(->(true, =(X, ok)), =(X, fallback))" pl-s-env-ite1)
  (pl-mk-trail))

(pl-s-test!
  "if-then-else: cond true binds via then"
  (pl-atom-name (pl-walk-deep (dict-get pl-s-env-ite1 "X")))
  "ok")

(pl-s-test!
  "if-then-else: cond false → else"
  (pl-solve-once!
    pl-s-db-ite
    (pl-s-goal ";(->(fail, =(X, ok)), =(X, fallback))" {})
    (pl-mk-trail))
  true)

(define pl-s-env-ite2 {})

(pl-solve-once!
  pl-s-db-ite
  (pl-s-goal ";(->(fail, =(X, ok)), =(X, fallback))" pl-s-env-ite2)
  (pl-mk-trail))

(pl-s-test!
  "if-then-else: cond false binds via else"
  (pl-atom-name (pl-walk-deep (dict-get pl-s-env-ite2 "X")))
  "fallback")

(pl-s-test!
  "if-then-else: cond commits to first solution (count = 1)"
  (pl-solve-count!
    pl-s-db-ite
    (pl-s-goal ";(->(p(X), =(Y, found)), =(Y, none))" {})
    (pl-mk-trail))
  1)

(pl-s-test!
  "if-then-else: then can backtrack"
  (pl-solve-count!
    pl-s-db-ite
    (pl-s-goal ";(->(true, p(X)), =(X, none))" {})
    (pl-mk-trail))
  2)

(pl-s-test!
  "if-then-else: else can backtrack"
  (pl-solve-count!
    pl-s-db-ite
    (pl-s-goal ";(->(fail, =(X, ignored)), p(X))" {})
    (pl-mk-trail))
  2)

(pl-s-test!
  "standalone -> with true cond succeeds"
  (pl-solve-once!
    pl-s-db-ite
    (pl-s-goal "->(true, =(X, hi))" {})
    (pl-mk-trail))
  true)

(pl-s-test!
  "standalone -> with false cond fails"
  (pl-solve-once!
    pl-s-db-ite
    (pl-s-goal "->(fail, =(X, hi))" {})
    (pl-mk-trail))
  false)

(pl-s-test!
  "write(hello)"
  (begin
    (pl-output-clear!)
    (pl-solve-once!
      pl-s-empty-db
      (pl-s-goal "write(hello)" {})
      (pl-mk-trail))
    pl-output-buffer)
  "hello")

(pl-s-test!
  "nl outputs newline"
  (begin
    (pl-output-clear!)
    (pl-solve-once! pl-s-empty-db (pl-s-goal "nl" {}) (pl-mk-trail))
    pl-output-buffer)
  "\n")

(pl-s-test!
  "write(42) outputs digits"
  (begin
    (pl-output-clear!)
    (pl-solve-once!
      pl-s-empty-db
      (pl-s-goal "write(42)" {})
      (pl-mk-trail))
    pl-output-buffer)
  "42")

(pl-s-test!
  "write(foo(a, b)) formats compound"
  (begin
    (pl-output-clear!)
    (pl-solve-once!
      pl-s-empty-db
      (pl-s-goal "write(foo(a, b))" {})
      (pl-mk-trail))
    pl-output-buffer)
  "foo(a, b)")

(pl-s-test!
  "write conjunction"
  (begin
    (pl-output-clear!)
    (pl-solve-once!
      pl-s-empty-db
      (pl-s-goal "write(a), write(b)" {})
      (pl-mk-trail))
    pl-output-buffer)
  "ab")

(pl-s-test!
  "write of bound var walks binding"
  (begin
    (pl-output-clear!)
    (pl-solve-once!
      pl-s-empty-db
      (pl-s-goal "=(X, hello), write(X)" {})
      (pl-mk-trail))
    pl-output-buffer)
  "hello")

(pl-s-test!
  "write then nl"
  (begin
    (pl-output-clear!)
    (pl-solve-once!
      pl-s-empty-db
      (pl-s-goal "write(hi), nl" {})
      (pl-mk-trail))
    pl-output-buffer)
  "hi\n")

(define pl-s-env-arith1 {})

(pl-solve-once!
  pl-s-empty-db
  (pl-s-goal "is(X, 42)" pl-s-env-arith1)
  (pl-mk-trail))

(pl-s-test!
  "is(X, 42) binds X to 42"
  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith1 "X")))
  42)

(define pl-s-env-arith2 {})

(pl-solve-once!
  pl-s-empty-db
  (pl-s-goal "is(X, +(2, 3))" pl-s-env-arith2)
  (pl-mk-trail))

(pl-s-test!
  "is(X, +(2, 3)) binds X to 5"
  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith2 "X")))
  5)

(define pl-s-env-arith3 {})

(pl-solve-once!
  pl-s-empty-db
  (pl-s-goal "is(X, *(2, 3))" pl-s-env-arith3)
  (pl-mk-trail))

(pl-s-test!
  "is(X, *(2, 3)) binds X to 6"
  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith3 "X")))
  6)

(define pl-s-env-arith4 {})

(pl-solve-once!
  pl-s-empty-db
  (pl-s-goal "is(X, -(10, 3))" pl-s-env-arith4)
  (pl-mk-trail))

(pl-s-test!
  "is(X, -(10, 3)) binds X to 7"
  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith4 "X")))
  7)

(define pl-s-env-arith5 {})

(pl-solve-once!
  pl-s-empty-db
  (pl-s-goal "is(X, /(10, 2))" pl-s-env-arith5)
  (pl-mk-trail))

(pl-s-test!
  "is(X, /(10, 2)) binds X to 5"
  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith5 "X")))
  5)

(define pl-s-env-arith6 {})

(pl-solve-once!
  pl-s-empty-db
  (pl-s-goal "is(X, mod(10, 3))" pl-s-env-arith6)
  (pl-mk-trail))

(pl-s-test!
  "is(X, mod(10, 3)) binds X to 1"
  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith6 "X")))
  1)

(define pl-s-env-arith7 {})

(pl-solve-once!
  pl-s-empty-db
  (pl-s-goal "is(X, abs(-(0, 5)))" pl-s-env-arith7)
  (pl-mk-trail))

(pl-s-test!
  "is(X, abs(-(0, 5))) binds X to 5"
  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith7 "X")))
  5)

(define pl-s-env-arith8 {})

(pl-solve-once!
  pl-s-empty-db
  (pl-s-goal "is(X, +(2, *(3, 4)))" pl-s-env-arith8)
  (pl-mk-trail))

(pl-s-test!
  "is(X, +(2, *(3, 4))) binds X to 14 (nested)"
  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith8 "X")))
  14)

(pl-s-test!
  "is(5, +(2, 3)) succeeds (LHS num matches)"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal "is(5, +(2, 3))" {})
    (pl-mk-trail))
  true)

(pl-s-test!
  "is(6, +(2, 3)) fails (LHS num mismatch)"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal "is(6, +(2, 3))" {})
    (pl-mk-trail))
  false)

(pl-s-test!
  "is propagates bound vars on RHS"
  (pl-solve-once!
    pl-s-empty-db
    (pl-s-goal "=(Y, 4), is(X, +(Y, 1)), =(X, 5)" {})
    (pl-mk-trail))
  true)

(define pl-solve-tests-run! (fn () {:failed pl-s-test-fail :passed pl-s-test-pass :total pl-s-test-count :failures pl-s-test-failures}))