;;; This file was generated by writeminikanren.pl
;;; Generated at 2007-10-25 15:24:42

(define-syntax lambdag@
  (syntax-rules ()
    ((_ (p) e) (lambda (p) e))))

(define-syntax lambdaf@
  (syntax-rules ()
    ((_ () e) (lambda () e))))

(define-syntax run*
  (syntax-rules ()
    ((_ (x) g ...) (run #f (x) g ...))))

(define-syntax rhs
  (syntax-rules ()
    ((_ x) (cdr x))))

(define-syntax lhs
  (syntax-rules ()
    ((_ x) (car x))))

(define-syntax size-s
  (syntax-rules ()
    ((_ x) (length x))))

(define-syntax var
  (syntax-rules ()
    ((_ x) (vector x))))

(define-syntax var?
  (syntax-rules ()
    ((_ x) (vector? x))))


(define empty-s '())

(define walk
  (lambda (v s)
    (cond
      ((var? v)
       (let ((a (assq v s)))
         (cond
           (a (walk (rhs a) s))
           (else v))))
      (else v))))

(define ext-s
  (lambda (x v s)
    (cons `(,x . ,v) s)))

(define unify
  (lambda (v w s)
    (let ((v (walk v s))
          (w (walk w s)))
      (cond
        ((eq? v w) s)
        ((var? v) (ext-s v w s))
        ((var? w) (ext-s w v s))
        ((and (pair? v) (pair? w))
         (let ((s (unify (car v) (car w) s)))
           (and s (unify (cdr v) (cdr w) s))))
        ((equal? v w) s)
        (else #f)))))

(define unify-check
  (lambda (u v s)
    (let ((u (walk u s))
          (v (walk v s)))
      (cond
        ((eq? u v) s)
        ((var? u) (ext-s-check u v s))
        ((var? v) (ext-s-check v u s))
        ((and (pair? u) (pair? v))
         (let ((s (unify-check 
                    (car u) (car v) s)))
           (and s (unify-check 
                    (cdr u) (cdr v) s))))
        ((equal? u v) s)
        (else #f)))))

 
(define ext-s-check
  (lambda (x v s)
    (cond
      ((occurs-check x v s) #f)
      (else (ext-s x v s)))))

(define occurs-check
  (lambda (x v s)
    (let ((v (walk v s)))
      (cond
        ((var? v) (eq? v x))
        ((pair? v) 
         (or 
           (occurs-check x (car v) s)
           (occurs-check x (cdr v) s)))
        (else #f)))))

(define walk*
  (lambda (w s)
    (let ((v (walk w s)))
      (cond
        ((var? v) v)
        ((pair? v)
         (cons
           (walk* (car v) s)
           (walk* (cdr v) s)))
        (else v)))))

(define reify-s
  (lambda (v s)
    (let ((v (walk v s)))
      (cond
        ((var? v)
         (ext-s v (reify-name (size-s s)) s))
        ((pair? v) (reify-s (cdr v)
                     (reify-s (car v) s)))
        (else s)))))

(define reify-name
  (lambda (n)
    (string->symbol
      (string-append "_" "." (number->string n)))))

(define reify
  (lambda (v s)
    (let ((v (walk* v s)))
      (walk* v (reify-s v empty-s)))))

(define == 
  (lambda (u v)
    (lambdag@ (s) (unify u v s))))

(define ==-check
  (lambda (v w)
    (lambdag@ (s)
      (unify-check v w s))))

(define-syntax mzero 
  (syntax-rules () ((_) #f)))

(define-syntax inc 
  (syntax-rules () ((_ e) (lambdaf@ () e))))

(define-syntax unit 
  (syntax-rules () ((_ a) a)))

(define-syntax choice 
  (syntax-rules () ((_ a f) (cons a f))))
 
(define-syntax case-inf
  (syntax-rules ()
    ((_ e (() e0) ((f^) e1) ((a^) e2) ((a f) e3))
     (let ((a-inf e))
       (cond
         ((not a-inf) e0)
         ((procedure? a-inf) (let ((f^ a-inf)) e1))
         ((not (and (pair? a-inf)
                    (procedure? (cdr a-inf))))
          (let ((a^ a-inf)) e2))
         (else (let ((a (car a-inf)) (f (cdr a-inf))) 
                 e3)))))))

(define-syntax run
  (syntax-rules ()
    ((_ n (x) g0 g ...)
     (take n
       (lambdaf@ ()
         ((exist (x) g0 g ... 
            (lambdag@ (s)
              (cons (reify x s) '())))
          empty-s))))))
 
(define take
  (lambda (n f)
    (if (and n (zero? n)) 
      '()
      (case-inf (f)
        (() '())
        ((f) (take n f))
        ((a) a)
        ((a f)
         (cons (car a)
           (take (and n (- n )) f)))))))

 
(define-syntax exist
  (syntax-rules ()
    ((_ (x ...) g0 g ...)
     (lambdag@ (s)
       (inc
         (let ((x (var 'x)) ...)
           (bind* (g0 s) g ...)))))))
 
(define-syntax bind*
  (syntax-rules ()
    ((_ e) e)
    ((_ e g0 g ...) (bind* (bind e g0) g ...))))
 
(define bind
  (lambda (a-inf g)
    (case-inf a-inf
      (() (mzero))
      ((f) (inc (bind (f) g)))
      ((a) (g a))
      ((a f) (mplus (g a) (lambdaf@ () (bind (f) g)))))))

(define-syntax conde
  (syntax-rules ()
    ((_ (g0 g ...) (g1 g^ ...) ...)
     (lambdag@ (s) 
       (inc 
         (mplus* 
           (bind* (g0 s) g ...)
           (bind* (g1 s) g^ ...) ...))))))
 
(define-syntax mplus*
  (syntax-rules ()
    ((_ e) e)
    ((_ e0 e ...) (mplus e0 
                    (lambdaf@ () (mplus* e ...))))))
 
(define mplus
  (lambda (a-inf f)
    (case-inf a-inf
      (() (f))
      ((f^) (inc (mplus (f) f^)))
      ((a) (choice a f))
      ((a f^) (choice a (lambdaf@ () (mplus (f) f^)))))))

(define-syntax conda
  (syntax-rules ()
    ((_ (g0 g ...) (g1 g^ ...) ...)
     (lambdag@ (s)
       (inc
         (ifa ((g0 s) g ...)
              ((g1 s) g^ ...) ...))))))
 
(define-syntax ifa
  (syntax-rules ()
    ((_) (mzero))
    ((_ (e g ...) b ...)
     (let loop ((a-inf e))
       (case-inf a-inf
         (() (ifa b ...))
         ((f) (inc (loop (f))))
         ((a) (bind* a-inf g ...))
         ((a f) (bind* a-inf g ...)))))))

(define-syntax condu
  (syntax-rules ()
    ((_ (g0 g ...) (g1 g^ ...) ...)
     (lambdag@ (s)
       (inc
         (ifu ((g0 s) g ...)
              ((g1 s) g^ ...) ...))))))
 
(define-syntax ifu
  (syntax-rules ()
    ((_) (mzero))
    ((_ (e g ...) b ...)
     (let loop ((a-inf e))
       (case-inf a-inf
         (() (ifu b ...))
         ((f) (inc (loop (f))))
         ((a) (bind* a-inf g ...))
         ((a f) (bind* (unit a) g ...)))))))

(define-syntax project
  (syntax-rules ()
    ((_ (x ...) g g* ...)
     (lambdag@ (s)
       (let ((x (walk* x s)) ...)
         ((exist () g g* ...) s))))))

(define succeed (== #f #f))

(define fail (== #f #t))

(define onceo
  (lambda (g)
    (condu
      (g succeed)
      (else fail))))

;;; This file was generated by writeminikanren.pl
;;; Generated at 2007-10-25 15:24:42

(define *debug-tags* '())
(define debug
  (lambda (tags format . args)
    (let* ((tags (if (not (pair? tags)) (list tags) tags))
           (fs (string-append "[" (symbol->string (car tags)) "] " format "\n")))
      (cond
       [(null? tags)]
       [(pair? tags)
        (if (member (car tags) *debug-tags*)
            (apply printf fs args)
            (void))]
       ))))


;; Stream primitives
(define-syntax lambdag@
  (syntax-rules ()
    ((_ (p ...) e ...) (lambda (p ...) e ...))))

(define-syntax lambdaf@
  (syntax-rules ()
    ((_ () e ...) (lambda () e ...))))

(define-syntax inc
  (syntax-rules () ((_ e) (lambdaf@ () e))))

(define defunc
  (lambda (f)
    (if (procedure? f) (defunc (f)) f)))

(define snull 'snull)

(define snull? 
  (lambda (s)
    (eq? s snull)))

(define-syntax scons
  (syntax-rules ()
    ((_ a d) (cons a (lambda () d)))))

(define scar
  (lambda (s)
    (cond
     [(procedure? s) (scar (s))]
     [else (car s)])))

(define scdr
  (lambda (s)
    (cond
     [(procedure? s) (scdr (s))]
     [else ((cdr s))])))

(define-syntax sunit
  (syntax-rules ()
    ((_ a) (scons a snull))))

(define slift
  (lambda (f)
    (lambda args
      (sunit (apply f args)))))

(define-syntax make-stream
  (syntax-rules ()
    ((_) snull)
    ((_ e1 e2 ...) (scons e1 (make-stream e2 ...)))))

(define take
  (lambda (n s)
    (if (and n (zero? n))
        '()
        (let ([s (defunc s)])
          (cond
           [(snull? s) '()]
           [else (cons (scar s) (take (and n (- n )) (scdr s)))])))))

(define smerge
  (lambda (s1 s2)
    (cond
     [(snull? s1) s2]
     [(procedure? s1)
      (lambda () (smerge s2 (s1)))]
     [else (scons (scar s1) (smerge s2 (scdr s1)))])))

(define stream-merge
  (lambda (ss)
    (cond
     [(snull? ss) snull]
     [(procedure? ss) (lambda () (stream-merge (ss)))]
     [(snull? (scar ss)) (stream-merge (scdr ss))]
     [(procedure? (scar ss)) (lambda () 
                               (smerge (stream-merge (scdr ss))
                                       (scar ss)))]
     [else (scons (scar (scar ss)) (smerge (scdr (scar ss))
                                           (stream-merge (scdr ss))))])))

(define smap
  (lambda (f s)
    (cond
     [(snull? s) snull]
     [(procedure? s) (lambda () (smap f (s)))]
     [else (scons (f (scar s)) (smap f (scdr s)))])))



;; Substitution
(define-syntax rhs
  (syntax-rules ()
    ((_ x) (cdr x))))

(define-syntax lhs
  (syntax-rules ()
    ((_ x) (car x))))

(define-syntax size-s
  (syntax-rules ()
    ((_ x) (length x))))

(define-syntax var
  (syntax-rules ()
    ((_ x) (vector x))))

(define-syntax var?
  (syntax-rules ()
    ((_ x) (vector? x))))

(define empty-s '())

(define walk
  (lambda (v s)
    (cond
      ((var? v)
       (let ((a (assq v s)))
         (cond
           (a (walk (rhs a) s))
           (else v))))
      (else v))))

(define ext-s
  (lambda (x v s)
    (cons `(,x . ,v) s)))

(define unify
  (lambda (v w s env)
    ((env-unify env) v w s env)))

(define unify-good
  (lambda (v w s env)
;    (printf "[unify-good]: ~a <--> ~a :: ~a\n" v w s)
    (let ((v (walk v s))
          (w (walk w s)))
      (cond
        ((eq? v w) s)
        ((var? v) (ext-s v w s))
        ((var? w) (ext-s w v s))
        ((and (pair? v) (pair? w))
         (let ((s (unify-good (car v) (car w) s env)))
           (and s (unify-good (cdr v) (cdr w) s env))))
        ((equal? v w) s)
        (else #f)))))


(define unify-evil
  (lambda (v w s env)
    (debug '(unify-evil unify) 
           "v=~a, w=~a, cvars: ~a\n  subst:~a" v w (env-cvars env) s)
    (let ((vv (walk v s))
          (ww (walk w s)))
      (cond
       ((eq? vv ww) s)
       ((and (var? vv) (memq v (env-cvars env))) #f)
       ((and (var? ww) (memq w (env-cvars env))) #f)
       ((var? vv) (ext-s vv ww s))
       ((var? ww) (ext-s ww vv s))
       ((and (pair? vv) (pair? ww))
        (let ((s (unify-evil (car vv) (car ww) s env)))
          (and s (unify-evil (cdr vv) (cdr ww) s env))))
       ((equal? vv ww) s)
       (else #f)))))


(define switch-unify
  (lambda (env)
    (if (eq? (env-unify env) unify-good)
        (change-unify env unify-evil)
        (change-unify env unify-good))))

(define unify-pred
  (lambda (v pred s env)
    (let ((v (walk v s)))
      (if (var? v)
          (cond 
           [(eq? pred number?) (ext-s v (random 9999999999) s)]
           [(eq? pred string?) (ext-s v "random string..." s)]
           [(eq? pred symbol?) (ext-s v 'randomstring... s)]
           )
          (cond
           [(pred v) s]
           [else #f])))))

(define predo
  (lambda (q pred)
    (lambdag@ (s env)
      (let ((s1 (unify-pred q pred s env)))
        (cond
         [(not s1) snull]
         [else (sunit s1)])))))

(define unify-check
  (lambda (u v s)
    (let ((u (walk u s))
          (v (walk v s)))
      (cond
        ((eq? u v) s)
        ((var? u) (ext-s-check u v s))
        ((var? v) (ext-s-check v u s))
        ((and (pair? u) (pair? v))
         (let ((s (unify-check (car u) (car v) s)))
           (and s (unify-check (cdr u) (cdr v) s))))
        ((equal? u v) s)
        (else #f)))))

 
(define ext-s-check
  (lambda (x v s)
    (cond
      ((occurs-check x v s) #f)
      (else (ext-s x v s)))))

(define occurs-check
  (lambda (x v s)
    (let ((v (walk v s)))
      (cond
        ((var? v) (eq? v x))
        ((pair? v) 
         (or 
           (occurs-check x (car v) s)
           (occurs-check x (cdr v) s)))
        (else #f)))))

(define walk*
  (lambda (w s)
    (let ((v (walk w s)))
      (cond
        ((var? v) v)
        ((pair? v)
         (cons
           (walk* (car v) s)
           (walk* (cdr v) s)))
        (else v)))))

(define reify-s
  (lambda (v s)
    (debug 'reify-s "v: ~a\ns:~a" v s)
    (let ((v (walk v s)))
      (cond
        ((var? v)
         (ext-s v (reify-name (size-s s)) s))
        ((pair? v) (reify-s (cdr v)
                     (reify-s (car v) s)))
        (else s)))))

(define reify-name
  (lambda (n)
    (string->symbol
      (string-append "_" "." (number->string n)))))

(define reify
  (lambda (v s)
    (let ((v (walk* v s)))
      (walk* v (reify-s v empty-s)))))


(define pkg
  (lambda (s c)
    (list s c)))
(define pkg-subst car)                  ; current substitution
(define pkg-constraints cadr)
(define ext-pkg-constraints
  (lambda (p cs ctexts env)
    (let ([newc (map (lambda (g t) 
                       (make-constraint g (env-vars env) t))
                     cs ctexts)])
      (pkg (pkg-subst p) (append newc (pkg-constraints p))))))

;; constraints save the current environment vars
(define make-constraint
  (lambda (g vars text)
    (list g vars text)))
(define constraint-goal car)            ; constraint goal
(define constraint-vars cadr)            ; variables which the constraint care about
(define constraint-text caddr)

;; environment
(define make-env
  (lambda (unify constraints vars cvars)
    (list unify constraints vars cvars)))
(define empty-env (list unify-good '() '() '()))
(define env-unify car)                 ; which unification to use (env)
(define env-constraints cadr)          ; current constraints (env)
(define env-vars caddr)                ; variables at this point (env)
(define env-cvars cadddr)              ; checked variables at this point (env)
(define env-constraint-goals
  (lambda (p)
    (map constraint-goal (env-constraint p))))



(define change-unify
  (lambda (p u)
    (make-env u (env-constraints p) (env-vars p) (env-cvars p))))

(define change-constraints
  (lambda (p c)
    (make-env (env-unify p) c (env-vars p) (env-cvars p))))

(define change-vars
  (lambda (p v)
    (make-env (env-unify p) (env-constraints p) v (env-cvars p))))

(define change-cvars
  (lambda (p cv)
    (env (env-unify p) (env-constraints p) (env-vars p) cv)))

(define ext-constraint
  (lambda (env new-cg)
    (let ([newc (map (lambda (g) (make-constraint g (env-vars env) 'a))
                     new-cg)])
      (change-constraints env newc))))

(define ext-vars
  (lambda (env new-vars)
    (change-vars env (append new-vars (env-vars env)))))

(define ext-cvars
  (lambda (env new-cvars)
    (change-cvars env (append new-cvars (env-cvars env)))))



;;; miniKanren

(define bind
  (lambda (s f env)
    (cond
     [(procedure? s) (lambda () (bind (s) f env))]
     [else
      (stream-merge (smap (lambda (s) (f s env)) s))])))

(define bind*
  (lambda (s goals env)
    (cond
     [(null? goals)
      (stream-merge
       (smap (lambda (s) 
               (bind-constraints (sunit s) (pkg-constraints s) env))
             s))]
     [(snull? s) snull]
     [else (bind* (bind s (car goals) env) (cdr goals) env)])))

(define bind*
  (lambda (s goals env)
    (cond
     [(null? goals) s]
     [(snull? s) snull]
     [else (bind* (bind s (car goals) env) (cdr goals) env)])))

(define bind-constraints
  (lambda (s cs env)
    (cond
     [(null? cs) s]
     [(snull? s) snull]
     [else 
      (debug 'bind-constraints
             "checking constraint: ~a" (constraint-text (car cs)))
      (bind-constraints
            (bind s
                  (constraint-goal (car cs))
                  (make-env (env-unify env)
                            '()                     ; no constraints
                            (env-vars env)
                            (constraint-vars (car cs)))) 
            (cdr cs)
            env)])))

(define ==
  (lambda (u v)
    (lambdag@ (s env)
      (let ((s1 ((env-unify env) u v (pkg-subst s) env)))
        (cond
         [(not s1) snull]
         [else (sunit (pkg s1 (pkg-constraints s)))])))))

(define ==
  (lambda (u v)
    (lambdag@ (s env)
      (let ((s1 ((env-unify env) u v (pkg-subst s) env)))
        (cond
         [(not s1) snull]
         [else
          (let ([cc (bind-constraints (sunit (pkg s1 '()))
                                      (pkg-constraints s) env)])
            (if (snull? cc)
                snull
                (sunit (pkg s1 (filter (lambda (c) 
                                         (not (tautology? c (pkg-subst s))))
                                       (pkg-constraints s))))))])))))

(define ando
  (lambda goals
    (lambdag@ (s env)
      (bind* (sunit s) goals env))))

(define org2
  (lambda (goals)
    (lambdag@ (s env)
      (cond
       [(null? goals) snull]
       [else
        (scons (bind (sunit s) (car goals) env)
               ((org2 (cdr goals)) s env))]))))

(define oro
  (lambda goals
    (lambdag@ (s env)
      (stream-merge ((org2 goals) s env)))))

(define noto
  (lambda (g)
    (lambdag@ (s env)
      (inc
        (let ([ans (g s (switch-unify env))])
          (letrec ((negate (lambda (s)
                             (cond
                              [(procedure? s) (lambda () (negate (s)))]
                              [(snull? ans) (succeed s env)]
                              [else (fail s env)]))))
                  (negate ans)))))))

(define noto
  (lambda (g)
    (lambdag@ (s env)
      (let ([ans (defunc (g s (switch-unify env)))])
        ((if (snull? ans)
             ;;             (begin (printf "###fail###\n") succeed)
             ;;             (begin (printf "###succeed###\n") fail)
             succeed
             fail
             ) s env)))))


(define-syntax exist
  (syntax-rules ()
    ((_ (x ...) g0 g ...)
     (lambdag@ (s env)
       (inc
         (let ((x (var 'x)) ...)
           ((ando g0 g ...) s (ext-vars env (list x ...)))))))))

(define-syntax forall
  (syntax-rules ()
    ((_ (x ...) g0 g ...)
     (lambdag@ (s env)
       (inc
         (let ((x (var 'x)) ...)
           ((ando g0 g ...)
            (let loop ([ss (pkg-subst s)] [vars (list x ...)])
             (cond
              [(null? vars) ss]
              [else (loop (ext-s (car vars) (gensym) ss) (cdr vars))]))
            (ext-vars env (list x ...)))))))))

(define-syntax conde
  (syntax-rules ()
    ((_ (g0 g ...) (g1 g^ ...) ...)
     (lambdag@ (s env)
       (inc
         ((oro (ando g0 g ...)
               (ando g1 g^ ...) ...) s env))))))

(define-syntax condc
  (syntax-rules ()
    ((_ (g0 g ...)) (ando g0 g ...))
    ((_ (g0 g ...) g^ ...)
     (lambdag@ (s env)
       (inc
         ((oro (ando g0 g ...)
               (assert ((noto g0))
                       (condc g^ ...))) s env))))))

(define reify-constraint
  (lambda (s)
    (lambda (c)
      (let ((ct (constraint-text c)))
        (cond
         [(pair? ct)
          (cons (car ct) 
                (map (lambda (v) (walk* v (pkg-subst s))) (cdr ct)))]
         [else ct])))))

(define format-constraints
  (lambda (s)
    (debug 'format-constraints "subst: ~a\nconstraints: ~a\n" 
           (pkg-subst s)
           (pkg-constraints s))
    (map (reify-constraint s)
         (filter (lambda (c) 
                   (not (tautology? c (pkg-subst s))))
                 (pkg-constraints s)))))


(define-syntax run
  (syntax-rules ()
    ((_ n (x) g0 g ...)
     (let ((x (var 'x)))
       (let ([ss ((ando g0 g ...) (pkg empty-s '())
                   (make-env unify-good '() (list x) '()))])
         (take n (smap (lambda (s)
                         (let* ((x (walk* x (pkg-subst s)))
                                (rs (reify-s x empty-s)))
                           (list
                            (walk* x rs)
                            (let ((ctext (walk* (format-constraints s) rs)))
                              (if (null? ctext)
                                  '()
                                  (list 'constraints: ctext))))))
                       ss)))))))

(define tautology?
  (lambda (c s)
    (debug 'tautology?
           "constraint: ~a\nvars: ~a\nsubst:~a\n"
           (constraint-text c)
           (constraint-vars c)
           s)
    (not (snull?
          (defunc ((constraint-goal c)
                   (pkg s '())
                   (make-env unify-evil '() '() (constraint-vars c))))))))


(define-syntax run*
  (syntax-rules ()
    ((_ (x) g ...) (run #f (x) g ...))))

(define-syntax make-text
  (syntax-rules (quote quasiquote)
    ((_ (quote a)) (quote a))
    ((_ (quasiquote a)) (quasiquote a))
    ((_ (g a0 ...)) (list 'g (make-text a0) ...))
    ((_ a) a)))

(define-syntax make-text*
  (syntax-rules (quote quasiquote)
    ((_) '())
    ((_ (quote a)) (quote a))
    ((_ (quasiquote a)) (quasiquote a))
    ((_ (g0 a ...) g ...)
     (list (make-text (g0 a ...)) (make-text g) ...))
    ((_ a) 'a)))


;; (make-text* `b)
;; (make-text* (noto (== `(,a ,d) (cons u v))) (noto (appendo a b c)))
;; (define a 1)
;; (define b 2)
;; (define c 3)
;; (define d 4)
;; (define u 5)
;; (define v 6)
;; (make-text* (a b c) `(,c a))
;; (define q 10)
; (make-text* (noto (== q 3)))

(define-syntax assert
  (syntax-rules ()
    ((_ (c0 c ...) g ...)
     (lambdag@ (s env)
       (inc 
        ((ando g ...)
         (ext-pkg-constraints s (list c0 c ...) (make-text* c0 c ...) env)
         (ext-constraint env (list c0 c ...))))))))

(define-syntax conda
  (syntax-rules ()
    ((_ (g0 g ...) (g1 g^ ...) ...)
     (lambdag@ (s)
       (inc
         (ifa ((g0 s) g ...)
              ((g1 s) g^ ...) ...))))))

(define-syntax ifa
  (syntax-rules ()
    ((_) snull)
    ((_ (e g ...) b ...)
     (cond
      [(snull? (defunc e)) (ifa b ...)]
      [else (bind* e (list g ...))]))))

(define-syntax condu
  (syntax-rules ()
    ((_ (g0 g ...) (g1 g^ ...) ...)
     (lambdag@ (s)
       (inc
         (ifu ((g0 s) g ...)
              ((g1 s) g^ ...) ...))))))
 
(define-syntax ifu
  (syntax-rules ()
    ((_) snull)
    ((_ (e g ...) b ...)
     (cond
      [(snull? (defunc e)) (ifa b ...)]
      [else (bind* (sunit (scar e)) (list g ...))]))))

(define-syntax project
  (syntax-rules ()
    ((_ (x ...) g g* ...)
     (lambdag@ (s env)
       (let ((x (walk* x s)) ...)
         ((exist () g g* ...) s env))))))

(define succeed (lambda (s env) (sunit s)))
(define fail (lambda (s env) snull))

(define prints
  (lambda (s env)
    (begin 
      (printf "#[prints]:: ~s\n" s)
      (succeed s env))))

(define print-env
  (lambdag@ (s env)
    (begin 
      (printf "env: ~s\n" env)
      (succeed s env))))

(define print-var
  (lambda (name v)
    (lambda (s env)
      (begin 
        (printf "#[print-var] ~a = ~s\n" name (walk v s))
        (succeed s env)))))

(define-syntax print-var
  (syntax-rules ()
    ((_ v) (lambda (s env)
             (begin 
               (printf "#[print-var] ~a = ~s\n" 'v (walk* v (pkg-subst s)))
               (succeed s env))))))


(define print-constraintso
  (lambda (s env)
    (printf "#[constraints] \n~a\n" 
            (map (lambda (s) (format "~a\n" s))
                 (map (reify-constraint s) (pkg-constraints s))))
    (succeed s env)))