;;; extKanren.knl --- Extensible Kanren  -*- indent-tabs-mode:nil -*-
;;; Code:

($provide! (var
            empty-state succeed fail
            disj conj $condᵉ $fresh
            $run $run*
            state-data set-state-data
            ≡
            nullᵒ consᵒ
            pairᵒ not-nullᵒ not-pairᵒ)

($import! emacs-global kernel-make-predicate)

($define! barebones? #f)

($define! include-stream-fns? #t)
($define! include-condᵃ? #t)
;; appendᵒ
($define! include-basic-goals? #t)

($when barebones?
  ($define! include-stream-fns? #f)
  ($define! include-condᵃ? #f)
  ($define! include-basic-goals? #f))


;;* Support
;;** Basic utilities
($define! $quote (unwrap identity))
($define! b-> boolean->elisp-boolean)
($define! b<- (inline ($λ (obj) (not? (null? obj)))))
($define! boolean? (inline ($λ (obj) (memq? obj (copy-es-immutable (list #f #t))))))

;; fix/environment
($define! f/e
  (inline ($λ (appv &optional env)
            (delay-inline
             (eval (list $λ ($quote args) (list apply (list wrap ($quote appv)) ($quote args)
                                                ($if (null? env)
                                                     (list make-environment)
                                                     (list $quote env))))
                   ($bindings->environment (appv (unwrap appv))))))))

($define! $let
  (inline
   ($vau (bindings . body) env
     ($import! (make-kernel-standard-environment) $let map)
     ($if (symbol? bindings)
          ($let ((loop-name bindings)
                 (env* (make-environment env))
                 ((bindings . body) body))
            ($let ((loop (eval (cons* $λ (map car bindings) body) env*)))
              (eval (list $define! loop-name loop) env*)
              ($let ((loop (delay-inline loop)))
                (eval (cons loop (map cadr bindings)) env))))
          (eval (cons* $let bindings body) env)))))


;;** List operations
($define! fast-finite-list?
  (inline
   ($λ (ls)
     ($import! emacs-global (length safe-length))
     ($define! drop drop-unsafe)
     (null? (drop (length ls) ls)))))

($define! map-nonnull-reverse
  (inline
   ($λ (f ls)
     ($let ((f (f/e f)))
       ($let loop ((rem ls)
                   (out ()))
         ($let ((rem (cdr rem))
                (out (cons (f (car rem)) out)))
           ($if (null? rem) out
                (loop rem out))))))))

($define! $do-nonempty-list
  (inline
   ($vau (((name expr)) . body) env
     ($let ((body (delay-inline (eval (cons* $λ (list name) body) env))))
       ($let loop ((rem (eval expr env)))
         (apply body (list (car rem)))
         ($let ((rem (cdr rem)))
           ($if (not? (null? rem))
                (loop rem)
                #inert)))))))

($define! map-reverse
  (inline
   ($λ (f ls)
     ($if (null? ls) () (map-nonnull-reverse f ls)))))

($define! map-nonnull
  (inline
   ($λ (f ls)
     (reverse! (map-nonnull-reverse f ls)))))

($define! map
  (inline
   ($λ (f ls)
     ($if (null? ls) () (map-nonnull f ls)))))

($define! reduce-nonnull
  (inline
   ($λ (ls kons &optional (fsingle identity))
     ($let ((kons (f/e kons)))
       ($let loop ((rem (cdr ls))
                   (acc (apply* fsingle (car ls) ())))
         ($if (null? rem) acc
              (loop (cdr rem) (kons (car rem) acc))))))))

($define! fold-nonnull
  (inline
   ($λ (kons knil ls)
     ($let ((kons (f/e kons)))
       ($let loop ((rem ls)
                   (acc knil))
         ($let ((rem (cdr rem))
                (acc (kons (car rem) acc)))
           ($if (null? rem) acc
                (loop rem acc))))))))

($define! fold
  (inline
   ($λ (kons knil ls)
     ($if (null? ls) knil (fold-nonnull kons knil ls)))))

($define! last-pair
  (inline
   ($λ (ls)
     ($define! drop drop-unsafe)
     ($define! length fast-length)
     (drop (- (length ls) 1) ls))))

($define! last
  (inline
   ($λ (ls)
     ($define! drop drop-unsafe)
     (list-ref ls (- (length ls) 1)))))


;;** Value predicates
($define! flonum-zero-eq
  ($λ (a b)
    ($let ((ainf (/ 1.0 a))
           (binf (/ 1.0 b)))
      (b-> (=? ainf binf)))))

($define! nonpair-term-eq?
  (inline
   ($λ (a b)
     ($define! nonpair-term-eq?
       ($λ (a b)
         ($let ((t (vector? a)))
           ($if t (b-> t) (b-> (elisp-equal-safe? a b))))))
     (b<- (nonpair-term-eq? a b)))))

;; FIXME: assumes (in terms of performance) that a is not a kernel
;; pair; it always calls kernel-eq-proper?, which has been terribly
;; written.
($define! value-eq?
  (inline
   ($λ (a b)
     ($let ((t (elisp-eq? a b)))
       (b<- ($if t (b-> t)
                 (elisp-pair? a)
                   (b-> (kernel-eq-proper? a b))
                 (b-> (nonpair-term-eq? a b))))))))

;; Not safe if a and b are a cons or a vector... or elisp byte code.
($define! elisp-equal-safe?
  (inline
   ($λ (a b)
     ($let ((t (elisp-equal? a b)))
       (b<- ($if t ($if (elisp-equal? a 0.0)
                        (flonum-zero-eq a b)
                        (b-> t))
                 (b-> t)))))))

($define! kernel-eq-proper?
  (inline
   ($λ (a b)
     ($import! emacs-global kernel-eq-proper?)
     (b<- (kernel-eq-proper? a b)))))


($define! exact-natural-number?
  (inline
   ($λ (obj)
     (b<- ($let ((x (fixnum? obj)))
            ($if x
                 (b-> (>=? obj 0))
                 (b-> (eq? (elisp-car-safe obj) ($elisp-symbol bigpos)))))))))

($define! nonnegative-fixnum?
  (inline
   ($λ (obj)
     (b<- ($let ((x (fixnum? obj)))
            ($if x
                 (b-> (>=? obj 0))
                 (b-> x)))))))

($define! positive-fixnum?
  (inline
   ($λ (obj)
     (b<- ($let ((x (fixnum? obj)))
            ($if x
                 (b-> (>? obj 0))
                 (b-> x)))))))

($define! exact-rational?
  ($λ (obj)
    (b<- ($let ((x (fixnum? obj)))
           ($if (not? x)
                (b-> (memq? (elisp-car-safe obj)
                            (copy-es-immutable (list ($elisp-symbol frac)
                                                     ($elisp-symbol bigpos)
                                                     ($elisp-symbol bigneg)))))
                (b-> x))))))


;;* Promises
($define! promise-tag (make-uninterned-elisp-symbol "#promise#"))
;; Breaks if e.g. obj is ()...
($define! promise/fast? (inline ($λ (obj) (elisp-symbol? (car obj)))))
($define! promise?   (inline ($λ (obj) (eq? promise-tag (car obj)))))
($define! $lazy      (inline ($vau (expr) env (cons promise-tag (eval (list $elisp-thunk expr) env)))))
($define! force-once (inline ($λ (p) (call-elisp-thunk (cdr p)))))
($define! force      (inline ($λ ($) ($if (promise? $) (force (force-once $)) $))))


($define! lazy-goal-expr cons)

($define! force-goal-expr
  (inline
   ($λ (p)
     ($if (null? (cdr p))
          (car p)
          ($let ((out (unwrap-goal (eval (car p) (cdr p)))))
            (set-car! p out)
            (set-cdr! p ())
            out)))))

($define! goal-expr->g
  (inline
   ($λ (G-expr env)
     ($let ((g (lazy-goal-expr G-expr env)))
       ($λ/g (a)
         (call (force-goal-expr g) a))))))

($define! goal-expr->goal (inline ($λ (G-expr env) (wrap-g (goal-expr->g G-expr env)))))


;;* Errors and checks
($define! kernel-error
  ($λ args
    ($import! emacs-global signal)
    (signal ($elisp-symbol kernel-error) args)))

($define! $range-error
  (inline
   ($vau (name . args) env
     ($import! emacs-global signal)
     (signal ($elisp-symbol kernel-range-error)
             (cons (elisp-symbol (symbol->string name))
                   (eval (cons list args) env))))))

($define! not-a-pair         ($λ (x) ($type-error pair? x)))
($define! not-a-fixnum       ($λ (x) ($type-error fixnum? x)))
($define! not-a-boolean      ($λ (x) ($type-error boolean? x)))
($define! not-a-symbol       ($λ (x) ($type-error symbol? x)))
($define! not-an-applicative ($λ (x) ($type-error applicative? x)))
($define! not-a-finite-list  ($λ (x) ($type-error finite-list? x)))
($define! not-a-var          ($λ (x) ($type-error var? x)))
($define! not-a-goal         ($λ (x) ($type-error goal? x)))
($define! not-a-stream       ($λ (x) ($type-error stream? x)))
($define! not-a-state        ($λ (x) ($type-error state? x)))

(never-returns! not-a-pair not-a-fixnum not-a-boolean not-a-symbol
                not-an-applicative
                not-a-finite-list
                not-a-var not-a-goal not-a-stream not-a-state)

($define! assert-fixnum
  (inline
   ($λ (ls)
     ($unless (fixnum? ls)
       (not-a-fixnum ls))
     ls)))

($define! assert-fx/natnum
  ($λ (obj)
    ($if (fixnum? obj)
         ($unless (>=? obj 0)
           ($type-error exact-natural-number? obj))
         ($type-error fixnum? obj))
    obj))

($define! assert-boolean
  (inline
   ($λ (ls)
     ($unless (boolean? ls)
       (not-a-boolean ls))
     ls)))

($define! assert-symbol
  (inline
   ($λ (obj)
     ($unless (symbol? obj)
       (not-a-symbol obj))
     obj)))

($define! assert-applicative
  (inline
   ($λ (obj)
     ($unless (applicative? obj)
       (not-an-applicative obj))
     obj)))

($define! assert-finite-list
  (inline
   ($λ (ls)
     ($unless (finite-list? ls)
       (not-a-finite-list ls))
     ls)))

($define! assert-var
  (inline
   ($λ ($)
     ($unless (var? $)
       (not-a-var $))
     $)))

($define! assert-pair-term
  (inline
   ($λ ($)
     ($unless (pair-term? $)
       (not-a-pair $))
     $)))

($define! assert-goal
  (inline
   ($λ ($)
     ($unless (goal? $)
       (not-a-goal $))
     $)))

($define! assert-stream
  (inline
   ($λ (ss)
     ($unless (stream? ss)
       (not-a-stream ss))
     ss)))

($define! assert-state
  (inline
   ($λ (ss)
     ($unless (state? ss)
       (not-a-state ss))
     ss)))


;;* Kanren core
;;** Terms
($define! special-term-tag ($elisp-symbol special))
($define! special-term-tag? (inline ($λ (tag) (eq? tag special-term-tag))))

($define! nonpair-term-tag?
  (inline
   ($λ (tag)
     (kernel+-type-tag? (list special-term-tag) tag))))

($define! cons-is-kernel-pair?
  (inline
   ($λ (v)
     (not? (kernel-type-tag? (car v))))))

($define! cons-is-special-term?
  (inline
   ($λ (v)
     (special-term-tag? (car v)))))

($define! cons-is-pair-term?
  (inline
   ($λ (v)
     (not? (nonpair-term-tag? (car v))))))

($define! special-term?
  (inline
   ($λ (v)
     (special-term-tag? (elisp-car-safe v)))))

($define! pair-term?
  (inline
   ($λ (v)
     ($let ((t (elisp-pair? v)))
       (b<- ($if t (b-> (cons-is-pair-term? v)) (b-> t)))))))


;;** Goals and streams: types
($define! goal-tag (make-uninterned-elisp-symbol "#goal#"))
($define! state-tag (make-uninterned-elisp-symbol "#state#"))
($define! stream-tag (make-uninterned-elisp-symbol "#stream#"))
($define! bad-stream-tag (make-uninterned-elisp-symbol "#bad-stream#"))

(list (set! (elisp-variable goal-tag) "goal")
      (set! (elisp-variable state-tag) "state")
      (set! (elisp-variable stream-tag) "stream")
      (set! (elisp-variable bad-stream-tag) "invalid-stream"))

($set! module-environment goal?   (kernel-make-predicate goal-tag))
($set! module-environment state?  (kernel-make-predicate state-tag))
($set! module-environment stream? (kernel-make-predicate stream-tag))

;; This is the 'state' of the monad as a series-parallel state monad.
($define! state?      (inline ($λ (obj) (eq? (elisp-cadr-safe obj) state-tag))))
($define! decap-state (inline ($λ (A) (assert-state A) (decap-a A))))
($define! encap-a     (inline ($λ (a) (cons* ($elisp-symbol encap) state-tag a))))
($define! decap-a     (inline ($λ (A) (elisp-cddr A))))

($define! make-a (inline ($λ (s data) (cons s data))))
($define! a-subst car)
($define! a-data  cdr)
($define! set-a-data  (inline ($λ (a d) (make-a (a-subst a) d))))
($define! set-a-subst (inline ($λ (a s) (make-a s (a-data a)))))

($define! state-data
  ($λ (A)
    (a-data (decap-state A))))

($define! set-state-data
  ($λ (A d)
    (encap-a (set-a-data (decap-state A) d))))

($define! goal?       (inline ($λ (obj) (eq? (elisp-cadr-safe obj) goal-tag))))
($define! unwrap-goal (inline ($λ (G) (assert-goal G) (unwrap-g G))))
($define! wrap-g      (inline ($λ (g) (cons* ($elisp-symbol encap) goal-tag g))))
($define! unwrap-g    (inline ($λ (G) (elisp-cddr G))))

($define! stream?       (inline ($λ (obj) (eq? (elisp-cadr-safe obj) stream-tag))))
($define! encap-stream  (inline ($λ ($) (cons* ($elisp-symbol encap) stream-tag $))))
($define! decap-stream  (inline ($λ ($) (assert-stream $) (decap-$ $))))
($define! decap-$       (inline ($λ ($) (elisp-cddr $))))
($define! make-invalid! (inline ($λ ($) ($unless (null? (cdr (cdr-impure $))) (set-cdr! $ (list bad-stream-tag))))))

($define! choice cons)
($define! empty-$? null?)

($define! empty-s   ())
($define! null-data ())
($define! unit (inline ($λ (a) (choice a mzero))))
($define! mzero ())

($define! empty-a (copy-es-immutable (make-a empty-s null-data)))

($define! empty-state  (copy-es-immutable (encap-a empty-a)))
;; Hack: 'in already set' error
($define! empty-stream (inline ($λ () (copy-es-immutable (encap-stream mzero)))))
($set! module-environment mzero (empty-stream))


;;** Goals: calling and construction
($define! call         (inline ($λ (g a) (call-elisp-λ1 g a))))
($define! call-encap   (inline ($λ (g a) (encap-stream (call g a)))))
($define! call/G       (inline ($λ (G a) (call (unwrap-g G) a))))
($define! call/G-encap (inline ($λ (G a) (encap-stream (call/G G a)))))
($define! call/goal       (inline ($λ (G a) (call (unwrap-goal G) a))))
($define! call/goal-encap (inline ($λ (G a) (encap-stream (call/goal G a)))))

($set! module-environment call/goal
  ($λ (g &optional a)
    (call/G-encap g ($if (null? a)
                         empty-a
                         (decap-state a)))))

($set! module-environment $λ/g
  ($vau ((a-sym) . body) env
    (assert-symbol a-sym)
    ($λ/G (a)
      ($let ((a (encap-a a)))
        (decap-stream
         (eval-runtime-sequence body (list ($elisp-symbol env)
                                           (list env)
                                           (cons a-sym a))))))))

($define! $λ/G
  (inline
   ($vau ((a-sym) . body) env
     (wrap-g (eval (cons* $elisp-λ1 a-sym body) env)))))

($define! $λ/g
  (inline
   ($vau ((a-sym) . body) env
     (eval (cons* $elisp-λ1 a-sym body) env))))


;;** Variables
($define! var-tag     (make-uninterned-elisp-symbol "#var#"))
($define! var-counter (make-uninterned-elisp-symbol "#var-counter#"))

(list (set! (elisp-variable var-tag) "var")
      (set! (elisp-variable var-counter) 0))

($define! var? (inline ($λ (obj) (eq? (elisp-cadr-safe obj) var-tag))))
($define! var-index elisp-cddr)

($define! var<? (inline ($λ (u v) (<? (var-index u) (var-index v)))))

($define! var
  ($λ ()
    (cons* ($elisp-symbol encap) var-tag
           (read-inc-counter var-counter))))


($set! module-environment var? (kernel-make-predicate var-tag))

($set! module-environment var-index
  ($λ (v)
    ($let ((v* (elisp-cdr-safe v)))
      ($unless (eq? var-tag (elisp-car-safe v*))
        (not-a-var v))
      (cdr v*))))

($set! module-environment var<?
  ($λ (u v)
    ($let ((u* (elisp-cdr-safe u)))
      ($let* ((t (eq? var-tag (elisp-car-safe u*)))
              (x ($if t v u)))
        (assert-var x))
      (<? (cdr u*) (var-index v)))))


;; The substitution store...
($define! var-assoc   assq)
($define! var-member? memq?)


;;** walk
($define! walk-var
  ($λ (u s)
    ($let ((pr (var-assoc u s)))
      ($if (null? pr) u
           ($let ((v (cdr pr)))
             ($if (not? (var? v))
                  ($if (special-term? v) u v)
                  (walk-var v s)))))))

($define! walk ($λ (u s) ($if (var? u) (walk-var u s) u)))

($define! walk*
  ($λ (v s &optional out)
    ($define! walk*
      ($λ (v s &optional out)
        ($let* (((a . b) v)
                (a ($inline (walk a s)))
                (out (cons ($if (pair-term? a) (walk* a s) a) out))
                (b ($inline (walk b s))))
          ($if (not? (pair-term? b))
               (append! (reverse! out) b)
               (walk* b s out)))))
    ($let ((v ($inline (walk v s))))
      ($if (pair-term? v)
           (walk* v s)
           v))))

($set! module-environment walk
  ($λ (u a)
    ($inline (walk u (a-subst (decap-state a))))))

($set! module-environment walk*
  ($λ (u a)
    (walk* u (a-subst (decap-state a)))))


;;** Monad helpers: simple
($define! ext-s (inline ($λ (x v s) (cons (cons x v) s))))

($define! succeed-goal (inline ($λ () (copy-es-immutable ($constant-elisp-λ1 a (unit a))))))
($define! fail-goal    (inline ($λ () (copy-es-immutable ($constant-elisp-λ1 a mzero)))))

($define! &succeed (succeed-goal))
($define! &fail    (fail-goal))
($define! succeed  (copy-es-immutable (wrap-g (succeed-goal))))
($define! fail     (copy-es-immutable (wrap-g (fail-goal))))

($define! suspend
  ($λ (G)
    ($let ((g (unwrap-goal G)))
      ($λ/G (a) ($lazy (call g a))))))

($define! $suspend
  ($vau (g) env
    ($λ/G (a) ($lazy (call/goal (eval g env) a)))))

($define! promise-or-stream
  ($λ (strm)
    ($import! emacs-global (knl/force-once kernel-force-once*))
    ($define! knl/promise? (inline ($λ (obj) (eq? (elisp-car-safe obj) ($elisp-symbol promise)))))
    ($if (knl/promise? strm)
         ($lazy ($inline (promise-or-stream (knl/force-once strm))))
         (decap-stream strm))))

($set! module-environment choice
  ($λ (A strm)
    (encap-stream (cons (decap-state A)
                        (promise-or-stream strm)))))

($set! module-environment unit
  ($λ states
    (assert-finite-list states)
    ($if (null? states)
         (empty-stream)
         (encap-stream (map-nonnull decap-state states)))))

($set! module-environment $lazy-choice
  ($vau (state-expr stream-expr) env
    (encap-stream ($lazy (decap-stream (eval stream-expr env))))))


;;** Monad: mplus and bind
($define! mplus
  ($λ ($₁ $₂)
    ($if (empty-$? $₁) $₂
         ;; Temporary check; this is now absolutely compulsory.
         (empty-$? $₂) ($type-error not-empty-$? $₂)
         ($let loop (($₁ $₁) ($₂ $₂))
           ($define! mplus:lazy
             (inline
              ($λ ($₁ $₂)
                ($lazy
                  ($let (($₁ ($if (promise/fast? $₁) (force-once $₁) $₁)))
                    ($if (empty-$? $₁) $₂
                         ($inline (loop $₁ $₂))))))))
           ($if (promise/fast? $₁) (mplus:lazy $₂ $₁)
                ($let* (((a₁ . $₁*) $₁))
                  (choice a₁ ($if (empty-$? $₁*) $₂
                                  ($if (promise/fast? $₂)
                                       (mplus:lazy $₂ $₁*)
                                       (mplus $₂ $₁*))))))))))

($define! bind
  ($λ ($ g)
    ($let loop (($ $))
      ($define! bind:lazy
        (inline
         ($λ ($ g)
           ($lazy ($inline (loop ($if (promise/fast? $) (force-once $) $)))))))
      ($if (empty-$? $) mzero
           (promise/fast? $) (bind:lazy $ g)
           ($let (((a . p) $))
             ($if (empty-$? p)
                  (call g a)
                  (mplus (call g a)
                         ($if (empty-$? (elisp-cdr p))
                              ($let ((a2 (car p)))
                                ($lazy (call g a2)))
                              (bind:lazy p g)))))))))


;;** disj and conj
($define! disj
  ($λ gs
    ($define! disj
      (inline
       ($λ (G₁ g₂)
         ($let ((g₁ (unwrap-g G₁)))
           ($λ/g (a)
             (mplus (call g₁ a)
                    ($lazy (call g₂ a))))))))

    ($if (null? gs) fail
         ($sequence
           (assert-finite-list gs)
           ($do-nonempty-list ((g gs)) (assert-goal g))
           (wrap-g (reduce-nonnull (reverse gs) disj unwrap-g))))))

;; 'gs' must be a non-empty finite list!
($define! conj-impl
  ($λ (gs)
    ($define! conj
      (inline
       ($λ (G₁ g₂)
         ($let ((g₁ (unwrap-g G₁)))
           ($λ/g (a)
             (bind (call g₁ a) g₂))))))

    ($do-nonempty-list ((g gs)) (assert-goal g))
    (reduce-nonnull (reverse gs) conj unwrap-g)))

($define! conj
  ($λ gs
    ($if (null? gs) succeed
         (wrap-g (conj-impl (assert-finite-list gs))))))

($define! conj-exprs
  ($λ (exprs env)
    ($define! force
      (inline
       ($λ (p)
         ($let ((exprs (car p))
                (env (cdr p)))
           ($define! eval-goal ($λ (expr) (assert-goal (eval expr env))))
           ($if (null? env) exprs
                ($let ((g ($if (null? exprs) succeed
                               (null? (cdr exprs))
                                 (unwrap-g (eval-goal (car exprs)))
                               (conj-impl (map-nonnull eval-goal exprs)))))
                  (set-car! p g)
                  (set-cdr! p ())
                  g))))))

    (assert-finite-list exprs)
    ($let ((p (cons exprs env)))
      ($λ/g (a) (call (force p) a)))))

($define! Conj-exprs (inline ($λ (exprs env) (wrap-g (conj-exprs exprs env)))))


;;* Kanren usability
;;** Reification
($define! reify*
  ($λ (v a)
    (reify (walk* v (a-subst a)))))

($define! reify
  (inline
   ($λ (v)
     (walk* v (reify-s v ())))))

($define! reify-s
  ($λ (v s)
    ($let ((v (walk v s)))
      ($if (var? v)       (ext-s v ($inline (reify-var (fast-length s))) s)
           (pair-term? v) (reify-s (cdr v) (reify-s (car v) s))
           s))))

($define! reify-var
  ($λ (n)
    (string->symbol (reify-var-string n))))

($define! reify-var-string
  ($λ (n)
    ;; Bad.
    ($define! list->string string-append)
    ($if (zero? n) "_₀"
         ($let loop ((rem n)
                     (out ()))
           ($let* (((q r) (truncate/ rem 10))
                   (out (cons (string-ref "₀₁₂₃₄₅₆₇₈₉" r) out)))
             ($if (zero? q)
                  (list->string (cons #x5f out))
                  (loop q out)))))))

($set! module-environment reify reify)
($set! module-environment reify*
  ($λ (v a)
    (reify* v (decap-state a))))


;;** Streams
($define! $-take-all
  (inline
   ($λ ($ state-mapper)
     ($let loop ((out ())
                 ($ $))
       ($let (($ (force $)))
         ($if (empty-$? $) (reverse! out)
              (loop (cons (apply state-mapper (list (car $)))
                          out)
                    (cdr $))))))))

($define! $-take
  (inline
   ($λ (n $ state-mapper)
     ($let loop ((out ())
                 ($ $)
                 (n n))
       ($if (zero? n) (reverse! out)
            ($let (($ (force $)))
              ($if (empty-$? $) (reverse! out)
                   (loop (cons (apply state-mapper (list (car $)))
                               out)
                         (cdr $)
                         (- n 1)))))))))


;;* Extensibility
;;** Unify
($define! custom-unifier-key     (make-uninterned-elisp-symbol "#custom-unifier#"))
($define! custom-≡-processor-key (make-uninterned-elisp-symbol "#custom-≡-processor#"))

(list (set! (elisp-variable custom-unifier-key) ())
      (set! (elisp-variable custom-≡-processor-key) ()))

($import! emacs-global kernel-make-dynamic-binder)

($set! module-environment with-custom-unifier
  (kernel-make-dynamic-binder custom-unifier-key))
($set! module-environment with-custom-≡-processor
  (kernel-make-dynamic-binder custom-≡-processor-key))

($define! custom-unifier     (inline ($λ () (elisp-variable custom-unifier-key))))
($define! custom-≡-processor (inline ($λ () (elisp-variable custom-≡-processor-key))))

;; ($define! call-unify
;;   ($λ (u v a)
;;     ($let ((unify-custom (custom-unifier)))
;;       ($let ((s ($if (null? unify-custom)
;;                        (unify-s u v (a-subst a))
;;                      ($let ((a (apply unify-custom (list u v (encap-a a)))))
;;                        ($if (eq? a #f) a
;;                             ;; Assume without checking, that a-data
;;                             ;; is still eq?.
;;                             (a-subst (decap-state a)))))))
;;         ($if (eq? s #f) s
;;              (set-a-subst a s))))))

($define! call-unify
  ($λ (u v a)
    ($import! emacs-global copy-alist)
    ($let ((unify-custom (custom-unifier)))
      ($if (null? unify-custom)
           ($let* ((s-in (a-subst a))
                   (s (unify-s u v s-in)))
             ($if (eq? s #f) s (novel-s! s s-in)))
           ($let ((new-s (apply unify-custom (list u v (encap-a a)))))
             ($if (eq? new-s #f) new-s
                  (copy-alist (check-s-alist new-s))))))))

($define! call-≡-processor
  ($λ (new-s a)
    ($let ((s (a-subst a)))
      ($if (eq? s new-s) a
           ($let ((≡-process-custom (custom-≡-processor)))
             ($if (null? ≡-process-custom)
                  (set-a-subst a (append! new-s s))
                  ($let ((a (apply ≡-process-custom (list new-s (encap-a a)))))
                    ($if (eq? a #f) a
                         (decap-state a)))))))))

($define! unify
  ($λ (u v a)
    ($let ((new-s (call-unify u v a)))
      ($if (eq? new-s #f) new-s
           (call-≡-processor new-s a)))))

($set! module-environment unify
  ($λ (u v A)
    (call-unify u v (decap-state A))))


;;* TODO: sort!
;;** Unify
($define! unify-special
  (inline
   ($λ (U V u v s)
     #f)))

($define! unify-s
  ($λ (u v s)
    ($let ((u ($inline (walk u s)))
           (v ($inline (walk v s))))
      ($if (elisp-eq? u v) s
           (var? u) (ext-s u v s)
           (var? v) (ext-s v u s)
           (not? (elisp-pair? u))
             ($if (vector? u)             #f
                  (elisp-equal-safe? u v) s
                  #f)
           (not? (cons-is-pair-term? u))
             ($if (kernel-eq-proper? u v) s
                  #f)
           (not? (kernel-pair? v)) #f
           ($let ((s (unify-s (car u) (car v) s)))
             ($if (not? (eq? s #f))
                  (unify-s (cdr u) (cdr v) s)
                  s))))))

($define! novel-s!
  ($λ (new-s s)
    ($if (eq? new-s s) ()
         ($let loop ((last new-s)
                     (rem (cdr new-s)))
           ($if (eq? s rem) ($sequence
                              (set-cdr! last ())
                              new-s)
                (loop rem (cdr rem)))))))

($define! novel-s
  ($λ (new-s s)
    ($let loop ((new-s new-s)
                (out ()))
      ($if (eq? s new-s) (reverse! out)
           (loop (cdr new-s)
                 (cons (car new-s) out))))))

($define! check-s-alist
  ($λ (s)
    ($do-list ((pr (assert-finite-list s)))
      ($if (not? (elisp-pair? pr)) (not-a-pair pr)
           ($let ((key (elisp-car pr)))
             ($unless (var? key)
               ($if (kernel-type-tag? key)
                    (not-a-pair pr)
                    (not-a-var key))))))
    s))

;; This does NOT run the user-defined unify extensions; it's exported
;; such that one can build such extensions in the first place.
($set! module-environment unify-triangular
  ($λ (u v A)
    ($let* ((a (decap-state A))
            (s-in (a-subst a))
            (s (unify-s u v s-in)))
      ($if (eq? s #f) s (novel-s! s s-in))
      ;; ($if (eq? s #f) s
      ;;      (eq? s s-in) A
      ;;      (encap-a (set-a-subst a s)))
      )))

($set! module-environment ext-s
  ($λ (x v A)
    ($let ((a (decap-state A)))
      (encap-a
       (set-a-subst a
         (ext-s (assert-var x) v
                (a-subst a)))))))

($set! module-environment ext-s*
  ($λ (A alist)
    ($import! emacs-global copy-alist)
    ($let ((a (decap-state A))
           (new-s (copy-alist (check-s-alist alist))))
      (encap-a (set-a-subst a (append! new-s (a-subst a)))))))

;; FIXME: get this to work again.
($define! unify-cars-s
  ($λ (u v s)
    ($let ((u (walk u s))
           (v (walk v s)))
      ($let ((u-pair? (pair-term? u))
             (v-pair? (pair-term? v)))
        ($if u-pair?
             ($let ((x (car u)))
               ($if v-pair?
                    ($define! y (car v))
                    ($define! (x y) (list (cons x (var)) v)))
               (unify x y s))
             ($if v-pair?
                  (unify u (cons (car v) (var)) s)
                  ($let* ((x (var))
                          (s (unify (cons x (var)) u s)))
                    ($if (eq? s #f) s
                         (unify (cons x (var)) v s)))))))))

($define! unify-cars
  ($λ (u v a)
    ($let ((x (var)) (l (var)) (r (var)))
      ($unify ((a (cons x l) u a)) #f
        (unify (cons x r) v a)))))

($define! $unify
  (inline
   ($vau (((a-sym . unify-args)) fail-expr . body) env
     ($let* ((a (eval (cons unify unify-args) env)))
       ($if (not? (eq? a #f))
            ($let ((env (make-environment env)))
              (eval (list $define! a-sym (list $quote a)) env)
              (eval (cons $sequence body) env))
            ($if (eq? fail-expr #f) a (eval fail-expr env)))))))

($define! $unify-cars
  (inline
   ($vau (((a-sym . unify-args)) fail-expr . body) env
     ($let* ((a (eval (cons unify-cars unify-args) env)))
       ($if (not? (eq? a #f))
            ($let ((env (make-environment env)))
              (eval (list $define! a-sym (list $quote a)) env)
              (eval (cons $sequence body) env))
            ($if (eq? fail-expr #f) a (eval fail-expr env)))))))


;;** Basic goals
($define! ≡
  ($λ (u v)
    ($λ/G (a)
      ($unify ((a u v a)) mzero (unit a)))))

($define! nullᵒ
  ($λ (v)
    ($λ/G (a)
      ($unify ((a () v a)) mzero (unit a)))))

($define! pairᵒ
  ($λ (v)
    ($λ/G (a)
      ($let ((v (walk v (a-subst a))))
        ($if (kernel-pair? v)
             (unit a)
             mzero)))))

($define! not-nullᵒ
  ($λ (v)
    ($λ/G (a)
      ($let ((v (walk v (a-subst a))))
        ($if ($let ((t (null? v)))
               (b<- ($if t (b-> t) (b-> (var? t)))))
             mzero
             (unit a))))))

($define! not-pairᵒ
  ($λ (v)
    ($λ/G (a)
      ($let ((v (walk v (a-subst a))))
        ($if ($let ((t (kernel-pair? v)))
               (b<- ($if t (b-> t) (b-> (var? t)))))
             mzero
             (unit a))))))

($define! consᵒ
  ($λ (car cdr v)
    ($λ/G (a)
      ($unify ((a (cons car cdr) v a)) mzero (unit a)))))


;;** appendᵒ
($define! appendᵒ
  ($λ (l s* out)
    ($λ/G (a)
      ($define! loop
        ($λ (l out a)
          ($let* (($ ($unify-cars ((a l out a)) mzero
                       ;; FIXME: this may still delay the end of the stream.
                       ($let ((s (a-subst a)))
                         ;; The assertions are unfortunately necessary, as
                         ;; unify-cars can fail if we allow arbitrary
                         ;; 'unify' implementations!
                         ($let ((l (walk (cdr (assert-pair-term (walk l s))) s))
                                (out (cdr (assert-pair-term (walk out s)))))
                           ($if (null? l)
                                ($unify ((a s* out a)) mzero (unit a))
                                ($lazy (loop l out a)))))))
                  (a ($unify ((a () l a))   #f
                     ($unify ((a s* out a)) #f a))))
            ($if (eq? a #f)
                 ($if (empty-$? $) $
                      (promise/fast? $) (force-once $)
                      $)
                 (choice a $)))))
      (loop l out a))))


;;* Public API
;;** $run
($define! run-impl
  ($λ (conj xs gs env)
    ($if (null? xs)
         (cons () (apply (wrap conj) gs env))
         ($sequence
           (assert-finite-list xs)
           ($let* ((bindings (map-nonnull (inline ($λ (x)
                                                    (assert-symbol x)
                                                    (cons x (var x))))
                                          xs))
                   (v0 (cdar bindings))
                   (env (cons* ($elisp-symbol env) (list env) bindings))
                   (g (apply (wrap conj) gs env)))
             (cons v0 (call/G g empty-a)))))))

($define! $run*
  ($vau (xs . gs) env
    ($let (((v0 . $) (run-impl conj xs gs env)))
      ($if (null? v0) v0
           ($-take-all $ (inline ($λ (a) (reify* v0 a))))))))

($define! $run
  ($vau (n xs . gs) env
    ($define! n (eval n env))
    (assert-fx/natnum n)
    ($let (((v0 . $) (run-impl conj xs gs env)))
      ($if (null? v0) v0
           ($-take n $ (inline ($λ (a) (reify* v0 a))))))))


;;** $condᵉ
($define! $condᵉ
  ($vau cs env
    (assert-finite-list cs)
    ($define! clause->goal (inline ($λ (gs) (Conj-exprs gs env))))
    (apply disj (map clause->goal cs))))


;;** $condᵃ and $condᵘ
($define! $condᵃ
  ($vau cs env
    (assert-finite-list cs)

    ($define! process-clause
      (inline
       ($λ (exprs)
         (assert-finite-list exprs)
         ($when (null? exprs)
           (kernel-error "$condᵃ: clause must be a non-empty list" exprs))
         ($let (((expr₁ . exprs) exprs))
           (cons (lazy-goal-expr expr₁ env)
                 ($if (null? exprs) exprs (cons exprs env)))))))

    ($define! $condᵃ:finish-clause
      (inline
       ($λ ($ gs)
         ($if (null? gs) $
              (null? (cdr gs))
                (bind $ (car gs))
              ($let ((exprs (car-impure gs))
                     (env (cdr-impure gs)))
                (set-cdr! gs ())
                ($let ((g₂ (conj-exprs exprs env)))
                  (set-car! gs g₂)
                  (bind $ g₂)))))))

    ($define! $condᵃ:loop
      ($λ (a $ gs cs)
        ($if (empty-$? $)
               ($if (null? cs) mzero
                    ($let ((((g₁ . gs) . cs) cs))
                      ($condᵃ:loop a (call (force-goal-expr g₁) a) gs cs)))
             ($let ((t (null? cs)))
               (b<- ($if t (b-> (null? gs)) (b-> t))))
               $
             (promise? $)
               ($lazy ($condᵃ:loop a (force-once $) gs cs))
             ($condᵃ:finish-clause $ gs))))

    ($if (null? cs) fail
         ($let ((cs (map-nonnull process-clause cs)))
           ($λ/G (a)
             ($condᵃ:loop a mzero () cs))))))


;;** $fresh
($define! $fresh
  ($vau (xs . gs) env
    ($if (null? gs) succeed
         (null? xs) (Conj-exprs gs env)
         ($sequence
           (assert-finite-list xs)
           ($let* ((bindings (map-nonnull (inline ($λ (x)
                                                    (assert-symbol x)
                                                    (cons x (var x))))
                                          xs))
                   (env (cons* ($elisp-symbol env) (list env) bindings)))
             (Conj-exprs gs env))))))


;;** Streams
($define! stream-take
  ($λ (n $)
    ($let ((out ($-take (assert-fx/natnum n) (decap-stream $) encap-a)))
      (make-invalid! $)
      out)))

($define! stream-take-all
  ($λ ($)
    ($let ((out ($-take-all (decap-stream $) encap-a)))
      (make-invalid! $)
      out)))

($define! stream-pull
  ($λ ($$)
    ($let (($ (force (decap-stream $$))))
      ($if (empty-$? $)
           (kernel-error "An empty stream was returned")
           ($sequence
             (make-invalid! $$)
             (encap-a (car $)))))))

;; Destructive.
($define! stream-delays
  ($λ (n $)
    (assert-stream $)
    ($let ((content (cdr-impure (cdr $))))
      ($if (empty-$? content) (list 0)
           ($sequence
             (make-invalid! $)
             ($let loop ((out ())
                         (n (assert-fx/natnum n))
                         (d 0)
                         ($ content))
               ($if (empty-$? $) (reverse! (cons d out))
                    (zero? n)    (reverse! out)
                    (not? (promise? $))
                      (loop (cons d out) (- n 1) 0 (cdr $))
                    ($let (($ (force-once $)))
                      (loop out n (+ d 1) $)))))))))


;;* Optional exports
($when include-stream-fns?
  ($set! module-environment stream-take     stream-take)
  ($set! module-environment stream-take-all stream-take-all)
  ($set! module-environment stream-pull     stream-pull)
  ($set! module-environment stream-delays   stream-delays))

($when include-condᵃ?
  ($set! module-environment $condᵃ $condᵃ))

($when include-basic-goals?
  ($set! module-environment appendᵒ appendᵒ))

;;* End
)