;; lib/prolog/tests/iso_predicates.sx — succ/2, plus/3, between/3, length/2, last/2, nth0/3, nth1/3, max/min arith

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

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

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

(define pl-ip-db (pl-mk-db))

;; ── succ/2 ──

(define pl-ip-env-s1 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "succ(3, X)" pl-ip-env-s1)
  (pl-mk-trail))
(pl-ip-test!
  "succ(3, X) → X=4"
  (pl-num-val (pl-walk-deep (dict-get pl-ip-env-s1 "X")))
  4)

(define pl-ip-env-s2 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "succ(0, X)" pl-ip-env-s2)
  (pl-mk-trail))
(pl-ip-test!
  "succ(0, X) → X=1"
  (pl-num-val (pl-walk-deep (dict-get pl-ip-env-s2 "X")))
  1)

(define pl-ip-env-s3 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "succ(X, 5)" pl-ip-env-s3)
  (pl-mk-trail))
(pl-ip-test!
  "succ(X, 5) → X=4"
  (pl-num-val (pl-walk-deep (dict-get pl-ip-env-s3 "X")))
  4)

(pl-ip-test!
  "succ(X, 0) fails"
  (pl-solve-once!
    pl-ip-db
    (pl-ip-goal "succ(X, 0)" {})
    (pl-mk-trail))
  false)

;; ── plus/3 ──

(define pl-ip-env-p1 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "plus(2, 3, X)" pl-ip-env-p1)
  (pl-mk-trail))
(pl-ip-test!
  "plus(2, 3, X) → X=5"
  (pl-num-val (pl-walk-deep (dict-get pl-ip-env-p1 "X")))
  5)

(define pl-ip-env-p2 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "plus(2, X, 7)" pl-ip-env-p2)
  (pl-mk-trail))
(pl-ip-test!
  "plus(2, X, 7) → X=5"
  (pl-num-val (pl-walk-deep (dict-get pl-ip-env-p2 "X")))
  5)

(define pl-ip-env-p3 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "plus(X, 3, 7)" pl-ip-env-p3)
  (pl-mk-trail))
(pl-ip-test!
  "plus(X, 3, 7) → X=4"
  (pl-num-val (pl-walk-deep (dict-get pl-ip-env-p3 "X")))
  4)

(pl-ip-test!
  "plus(0, 0, 0) succeeds"
  (pl-solve-once!
    pl-ip-db
    (pl-ip-goal "plus(0, 0, 0)" {})
    (pl-mk-trail))
  true)

;; ── between/3 ──

(pl-ip-test!
  "between(1, 3, X): 3 solutions"
  (pl-solve-count!
    pl-ip-db
    (pl-ip-goal "between(1, 3, X)" {})
    (pl-mk-trail))
  3)

(pl-ip-test!
  "between(1, 3, 2) succeeds"
  (pl-solve-once!
    pl-ip-db
    (pl-ip-goal "between(1, 3, 2)" {})
    (pl-mk-trail))
  true)

(pl-ip-test!
  "between(1, 3, 5) fails"
  (pl-solve-once!
    pl-ip-db
    (pl-ip-goal "between(1, 3, 5)" {})
    (pl-mk-trail))
  false)

(pl-ip-test!
  "between(5, 3, X): 0 solutions (empty range)"
  (pl-solve-count!
    pl-ip-db
    (pl-ip-goal "between(5, 3, X)" {})
    (pl-mk-trail))
  0)

(define pl-ip-env-b1 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "between(1, 5, X)" pl-ip-env-b1)
  (pl-mk-trail))
(pl-ip-test!
  "between(1, 5, X): first solution X=1"
  (pl-num-val (pl-walk-deep (dict-get pl-ip-env-b1 "X")))
  1)

(pl-ip-test!
  "between + condition: between(1,5,X), X > 3 → 2 solutions"
  (pl-solve-count!
    pl-ip-db
    (pl-ip-goal "between(1, 5, X), X > 3" {})
    (pl-mk-trail))
  2)

;; ── length/2 ──

(define pl-ip-env-l1 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "length([1,2,3], N)" pl-ip-env-l1)
  (pl-mk-trail))
(pl-ip-test!
  "length([1,2,3], N) → N=3"
  (pl-num-val (pl-walk-deep (dict-get pl-ip-env-l1 "N")))
  3)

(define pl-ip-env-l2 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "length([], N)" pl-ip-env-l2)
  (pl-mk-trail))
(pl-ip-test!
  "length([], N) → N=0"
  (pl-num-val (pl-walk-deep (dict-get pl-ip-env-l2 "N")))
  0)

(pl-ip-test!
  "length([a,b], 2) check succeeds"
  (pl-solve-once!
    pl-ip-db
    (pl-ip-goal "length([a,b], 2)" {})
    (pl-mk-trail))
  true)

(define pl-ip-env-l3 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "length(L, 3)" pl-ip-env-l3)
  (pl-mk-trail))
(pl-ip-test!
  "length(L, 3): L is a list of length 3"
  (pl-solve-once!
    pl-ip-db
    (pl-ip-goal "length(L, 3), is_list(L)" pl-ip-env-l3)
    (pl-mk-trail))
  true)

;; ── last/2 ──

(define pl-ip-env-la1 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "last([1,2,3], X)" pl-ip-env-la1)
  (pl-mk-trail))
(pl-ip-test!
  "last([1,2,3], X) → X=3"
  (pl-num-val (pl-walk-deep (dict-get pl-ip-env-la1 "X")))
  3)

(define pl-ip-env-la2 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "last([a], X)" pl-ip-env-la2)
  (pl-mk-trail))
(pl-ip-test!
  "last([a], X) → X=a"
  (pl-atom-name (pl-walk-deep (dict-get pl-ip-env-la2 "X")))
  "a")

(pl-ip-test!
  "last([], X) fails"
  (pl-solve-once!
    pl-ip-db
    (pl-ip-goal "last([], X)" {})
    (pl-mk-trail))
  false)

;; ── nth0/3 ──

(define pl-ip-env-n0 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "nth0(0, [a,b,c], X)" pl-ip-env-n0)
  (pl-mk-trail))
(pl-ip-test!
  "nth0(0, [a,b,c], X) → X=a"
  (pl-atom-name (pl-walk-deep (dict-get pl-ip-env-n0 "X")))
  "a")

(define pl-ip-env-n1 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "nth0(2, [a,b,c], X)" pl-ip-env-n1)
  (pl-mk-trail))
(pl-ip-test!
  "nth0(2, [a,b,c], X) → X=c"
  (pl-atom-name (pl-walk-deep (dict-get pl-ip-env-n1 "X")))
  "c")

(pl-ip-test!
  "nth0(5, [a,b,c], X) fails"
  (pl-solve-once!
    pl-ip-db
    (pl-ip-goal "nth0(5, [a,b,c], X)" {})
    (pl-mk-trail))
  false)

;; ── nth1/3 ──

(define pl-ip-env-n1a {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "nth1(1, [a,b,c], X)" pl-ip-env-n1a)
  (pl-mk-trail))
(pl-ip-test!
  "nth1(1, [a,b,c], X) → X=a"
  (pl-atom-name (pl-walk-deep (dict-get pl-ip-env-n1a "X")))
  "a")

(define pl-ip-env-n1b {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "nth1(3, [a,b,c], X)" pl-ip-env-n1b)
  (pl-mk-trail))
(pl-ip-test!
  "nth1(3, [a,b,c], X) → X=c"
  (pl-atom-name (pl-walk-deep (dict-get pl-ip-env-n1b "X")))
  "c")

;; ── max/min in arithmetic ──

(define pl-ip-env-m1 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "X is max(3, 5)" pl-ip-env-m1)
  (pl-mk-trail))
(pl-ip-test!
  "X is max(3, 5) → X=5"
  (pl-num-val (pl-walk-deep (dict-get pl-ip-env-m1 "X")))
  5)

(define pl-ip-env-m2 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "X is min(3, 5)" pl-ip-env-m2)
  (pl-mk-trail))
(pl-ip-test!
  "X is min(3, 5) → X=3"
  (pl-num-val (pl-walk-deep (dict-get pl-ip-env-m2 "X")))
  3)

(define pl-ip-env-m3 {})
(pl-solve-once!
  pl-ip-db
  (pl-ip-goal "X is max(7, 2) + min(1, 4)" pl-ip-env-m3)
  (pl-mk-trail))
(pl-ip-test!
  "X is max(7,2) + min(1,4) → X=8"
  (pl-num-val (pl-walk-deep (dict-get pl-ip-env-m3 "X")))
  8)

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