rose-ash/lib/prolog/tests/solve.sx

;; 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-solve-tests-run! (fn () {:failed pl-s-test-fail :passed pl-s-test-pass :total pl-s-test-count :failures pl-s-test-failures}))