giles
7fb4c52159
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Has been cancelled
619 lines
12 KiB
Plaintext
619 lines
12 KiB
Plaintext
;; 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}))
|