;; lib/minikanren/conde.sx — Phase 2 piece C: `conde`, the canonical
;; miniKanren and-or form, with implicit Zzz inverse-eta delay so recursive
;; relations like appendo terminate.
;;
;;   (conde (g1a g1b ...) (g2a g2b ...) ...)
;;     ≡ (mk-disj (Zzz (mk-conj g1a g1b ...))
;;                (Zzz (mk-conj g2a g2b ...)) ...)
;;
;; `Zzz g` wraps a goal expression in (fn (S) (fn () (g S))) so that
;; `g`'s body isn't constructed until the surrounding fn is applied to a
;; substitution AND the returned thunk is forced. This is what gives
;; miniKanren its laziness — recursive goal definitions can be `(conde
;; ... (... (recur ...)))` without infinite descent at construction time.
;;
;; Hygiene: the substitution parameter is gensym'd so that user goal
;; expressions which themselves bind `s` (e.g. `(appendo l s ls)`) keep
;; their lexical `s` and don't accidentally reference the wrapper's
;; substitution. Without gensym, miniKanren relations that follow the
;; common (l s ls) parameter convention are silently miscompiled.

(defmacro
  Zzz
  (g)
  (let
    ((s-sym (gensym "zzz-s-")))
    (quasiquote
      (fn ((unquote s-sym)) (fn () ((unquote g) (unquote s-sym)))))))

(defmacro
  conde
  (&rest clauses)
  (quasiquote
    (mk-disj
      (splice-unquote
        (map
          (fn
            (clause)
            (quasiquote (Zzz (mk-conj (splice-unquote clause)))))
          clauses)))))