;; lib/minikanren/tests/laziness.sx — verify Zzz wrapping (in conde)
;; lets infinitely-recursive relations produce finite prefixes via run-n.

;; --- a relation that has no base case but conde-protects via Zzz ---

(define
  listo-aux
  (fn
    (l)
    (conde ((nullo l)) ((fresh (a d) (conso a d l) (listo-aux d))))))

(mk-test
  "infinite-relation-truncates-via-run-n"
  (run 4 q (listo-aux q))
  (list
    (list)
    (list (make-symbol "_.0"))
    (list (make-symbol "_.0") (make-symbol "_.1"))
    (list (make-symbol "_.0") (make-symbol "_.1") (make-symbol "_.2"))))

;; --- two infinite generators interleaved via mk-disj must both produce
;;     answers (no starvation) — the fairness test ---

(define
  ones-gen
  (fn
    (l)
    (conde
      ((== l (list)))
      ((fresh (d) (conso 1 d l) (ones-gen d))))))

(define
  twos-gen
  (fn
    (l)
    (conde
      ((== l (list)))
      ((fresh (d) (conso 2 d l) (twos-gen d))))))

(mk-test
  "interleaving-keeps-both-streams-alive"
  (let
    ((res (run 4 q (mk-disj (ones-gen q) (twos-gen q)))))
    (and
      (= (len res) 4)
      (and
        (some
          (fn
            (x)
            (and
              (list? x)
              (and (not (empty? x)) (= (first x) 1))))
          res)
        (some
          (fn
            (x)
            (and
              (list? x)
              (and (not (empty? x)) (= (first x) 2))))
          res))))
  true)

;; --- run* terminates on a relation whose conde has finite base case
;;     reached from any starting point ---

(mk-test
  "run-star-terminates-on-bounded-relation"
  (run*
    q
    (fresh
      (l)
      (== l (list 1 2 3))
      (listo l)
      (== q :ok)))
  (list :ok))

(mk-tests-run!)