transparent.scm

(define-syntax let*/and
  (syntax-rules ()
    ((_ () rest ...) (and rest ...))
    ((_ ((name expr) ne* ...) rest ...)
     (let ((name expr))
       (and name (let*/and (ne* ...) rest ...))))))

(define-syntax defrecord
  (syntax-rules ()
    ((_ name name?)
     (begin
       (define name (vector 'name))
       (define (name? datum) (eq? name datum))))
    ((_ name name? (field set-field) ...)
     (begin
       (define (name field ...) (vector 'name field ...))
       (define (name? datum)
         (and (vector? datum) (eq? 'name (vector-ref datum 0))))
       (let ()
         (define (range-assoc start xs)
           (let loop ((xs xs) (idx start))
             (if (null? xs)
               '()
               (cons (cons (car xs) idx) (loop (cdr xs) (+ idx 1))))))
         (define (define-field-getter name rassc)
           (define idx (cdr (assoc name rassc)))
           (eval `(define (,name datum) (vector-ref datum ,idx))))
         (define (define-field-setter name rassc)
           (define idx (cdr (assoc name rassc)))
           (eval `(define (,name datum value)
                    (let ((new (vector-copy datum)))
                      (vector-set! new ,idx value)
                      new))))
         (let ((fns (range-assoc 1 '(field ...))))
           (begin (define-field-getter 'field fns) ...))
         (let ((set-fns (range-assoc 1 '(set-field ...))))
           (begin (define-field-setter 'set-field set-fns) ...)))))
    ((_ name name? field ...)
     (begin
       (define (name field ...) (vector 'name field ...))
       (define (name? datum)
         (and (vector? datum) (eq? 'name (vector-ref datum 0))))
       (let ()
         (define (range-assoc start xs)
           (let loop ((xs xs) (idx start))
             (if (null? xs)
               '()
               (cons (cons (car xs) idx) (loop (cdr xs) (+ idx 1))))))
         (define (define-field-getter name rassc)
           (define idx (cdr (assoc name rassc)))
           (eval `(define (,name datum) (vector-ref datum ,idx))))
         (let ((fns (range-assoc 1 '(field ...))))
           (begin (define-field-getter 'field fns) ...)))))))

(define store-empty '())
(define (store-ref store key . default)
  (let ((binding (assoc key store)))
    (if binding
      (cdr binding)
      (if (null? default)
        (error 'store-ref (format "missing key ~s in ~s" key store))
        (car default)))))
(define (store-set store key value) `((,key . ,value) . ,store))

(defrecord var var? var-index)
(define var/fresh
  (let ((index -1))
    (lambda ()
      (set! index (+ 1 index))
      (var index))))
;(define var=? eq?)
(define (var=? t1 t2)
  (and (var? t1) (var? t2) (eqv? (var-index t1) (var-index t2))))
(define (var<? v1 v2) (< (var-index v1) (var-index v2)))
(define var-initial (var/fresh))

(define (vattrs-get vs vr) (store-ref vs vr vr))
(define (vattrs-set vs vr value) (store-set vs vr value))
(define (walk-vs vs tm)
  (if (var? tm)
    (let ((va (vattrs-get vs tm)))
      (if (var=? tm va)
        tm
        (walk-vs vs va)))
    tm))

(defrecord state state? (state-vs set-state-vs))
(define state-empty (state store-empty))
(define (state-var-get st vr) (vattrs-get (state-vs st) vr))
(define (state-var-set st vr value)
  (set-state-vs st (vattrs-set (state-vs st) vr value)))
(define (state-var-== st vr value)
  (let*/and ((st (not-occurs? st vr value)))
    (state-var-set st vr value)))
(define (state-var-==-var st v1 v2)
  (if (var<? v1 v2)  ;; Pointing new to old may yield flatter substitutions.
    (state-var-set st v2 v1)
    (state-var-set st v1 v2)))

(define (walk st tm) (walk-vs (state-vs st) tm))

(define (not-occurs? st vr tm)
  (if (pair? tm)
    (let*/and ((st (not-occurs? st vr (walk st (car tm)))))
      (not-occurs? st vr (walk st (cdr tm))))
    (and (not (var=? vr tm)) st)))

(define (unify st t1 t2)
  (and st (let ((t1 (walk st t1)) (t2 (walk st t2)))
            (cond
              ((eqv? t1 t2) st)
              ((var? t1)
               (if (var? t2)
                 (state-var-==-var st t1 t2)
                 (state-var-== st t1 t2)))
              ((var? t2) (state-var-== st t2 t1))
              ((and (pair? t1) (pair? t2))
               (let*/and ((st (unify st (car t1) (car t2))))
                 (unify st (cdr t1) (cdr t2))))
              (else #f)))))

(defrecord conj conj? conj-c1 conj-c2)
(defrecord disj disj? disj-c1 disj-c2)
(defrecord zzz zzz? zzz-metadata zzz-wake)
(defrecord pause pause? pause-state pause-goal)
(defrecord == ==? ==-t1 ==-t2)

(define-syntax define-relation
  (syntax-rules ()
    ((_ (name param ...) body ...)
     (define (name param ...)
       (zzz `(name ,param ...) (lambda () body ...))))))

(define solution-info '())
(define (solution-clear!) (set! solution-info '()))
(define (solution-step! ss)
  (set! solution-info (cons (cons '() ss) solution-info)))
(define (solution-describe! desc)
  (set! solution-info
    (cons (cons (cons desc (caar solution-info)) (cdar solution-info))
          (cdr solution-info))))

(define (rappend xs ys)
  (if (null? xs) ys (rappend (cdr xs) (cons (car xs) ys))))

(define (solution->path sol)
  (let loop-sol ((sol sol) (done '()) (path '()))
    (if (null? sol)
      (append path done)
      (let loop-desc ((ds (caar sol)) (done done) (prefix '()) (suffix path))
        (if (null? ds)
          (begin
            (loop-sol (cdr sol) done (rappend prefix suffix)))
          (let ((desc (car ds)) (rds (cdr ds)))
            (cond
              ((eq? 'swap desc)
               (if (car suffix)
                 (loop-desc '() done prefix (cons #f (cdr suffix)))
                 (loop-desc rds done (cons #t prefix) (cdr suffix))))
              ((eq? 'fail desc) (loop-desc '() done prefix (cons #f suffix)))
              ((eq? 'ascend desc)
               (if (and (pair? suffix) (not (car suffix)))
                 (let loop-ascend
                   ((rds rds) (prefix prefix) (suffix (cdr suffix)))
                   (cond
                     ((car suffix)
                      (loop-desc '() done (cons #f prefix) (cdr suffix)))
                     ((eq? 'succeed (car rds))
                      (loop-desc '() done (cons #t prefix) (cons #f (cdr suffix))))
                     (else (loop-ascend (cdr rds)
                                        (cons (not (car suffix)) prefix)
                                        (cdr suffix)))))
                 (loop-desc rds done (cons #t prefix) suffix)))
              ((eq? 'succeed desc)
               (if (and (pair? suffix) (car suffix))
                 (loop-desc '() (append (cdr suffix) done) prefix '(#t))
                 (loop-desc '() done prefix suffix)))
              (else (error 'solution->path
                           (format "bad description ~s" desc))))))))))

(define (labeled-solution ss)
  (define answer1
    (begin (solution-clear!) (reify-initial (car (stream-take 1 ss)))))
  (define path (solution->path solution-info))
  (define follow (follow-path '() path ss))
  (define leftover (car follow))
  (define answer2 (reify-initial (car (stream-take 1 (cadr follow)))))
  (define choices (caddr follow))
  (cond
    ((pair? leftover)
     (error 'labeled-solution (format "unused path: ~s" leftover)))
    ((not (equal? answer1 answer2))
     (error 'labeled-solution
            (format "mismatching answers:\nexpected:~s\ncomputed:~s"
                    answer1 answer2)))
    (else choices)))

(define (labeled-solution* ss)
  (define answer1
    (begin (solution-clear!) (reify-initial (car (stream-take 1 ss)))))
  (define path (solution->path solution-info))
  (define follow (follow-path* follow-ctx0 '() path ss))
  (define leftover (car follow))
  (define answer2 (reify-initial (car (stream-take 1 (cadr follow)))))
  (define choices (cadddr follow))
  (cond
    ((pair? leftover)
     (error 'labeled-solution* (format "unused path: ~s" leftover)) )
    ((not (equal? answer1 answer2))
     (error 'labeled-solution*
            (format "mismatching answers:\nexpected:~s\ncomputed:~s"
                    answer1 answer2)))
    (else choices)))

(define (labeled-solution*-hint ss-hint ss)
  (define answer1
    (begin (solution-clear!) (reify-initial (car (stream-take 1 ss-hint)))))
  (define path (solution->path solution-info))
  (define follow (follow-path* follow-ctx0 '() path ss))
  (define leftover (car follow))
  (define answer2 (reify-initial (car (stream-take 1 (cadr follow)))))
  (define choices (cadddr follow))
  (cond
    ((pair? leftover)
     (error 'labeled-solution*-hint (format "unused path: ~s" leftover)))
    ((not (equal? answer1 answer2))
     (error 'labeled-solution*-hint
            (format "mismatching answers:\nexpected:~s\ncomputed:~s"
                    answer1 answer2)))
    (else choices)))

(define (labeled-pretty choices)
  (map (lambda (choice) (list (car choice)
                              (cadr (stream-pretty (cadr choice)))))
       choices))

(define (fbind/no-fail ss goal)
  (cond
    ((or (not ss) (state? ss)) (fstart/no-fail ss goal))
    ((pair? ss) (disj (pause (car ss) goal) (conj (cdr ss) goal)))
    (else (conj ss goal))))
(define (fstart/no-fail st goal)
  (cond
    ((conj? goal) (fbind/no-fail (fstart/no-fail st (conj-c1 goal))
                                 (conj-c2 goal)))
    ((disj? goal) (disj (pause st (disj-c1 goal)) (pause st (disj-c2 goal))))
    ((zzz? goal) (fstart/no-fail st ((zzz-wake goal))))
    ((==? goal) (and st (unify st (==-t1 goal) (==-t2 goal))))))

(define (fbind ss goal)
  (cond
    ((not ss) #f)
    ((state? ss) (fstart ss goal))
    ((pair? ss) (disj (pause (car ss) goal) (conj (cdr ss) goal)))
    (else (conj ss goal))))
(define (fstart st goal)
  (cond
    ((conj? goal) (fbind (fstart st (conj-c1 goal)) (conj-c2 goal)))
    ((disj? goal) (disj (pause st (disj-c1 goal)) (pause st (disj-c2 goal))))
    ((zzz? goal) (fstart st ((zzz-wake goal))))
    ((==? goal) (unify st (==-t1 goal) (==-t2 goal)))))

(define (follow-path choices path ss)
  (cond
    ((pair? ss) (list path (car ss) choices))
    ((state? ss) (list path ss choices))
    ((null? path) (list '() ss choices))
    ((not ss) (list path #f choices))
    ((conj? ss)
     (let* ((result (follow-path choices path (conj-c1 ss)))
            (path (car result))
            (ss1 (cadr result))
            (choices (caddr result)))
       (follow-path choices path (fbind ss1 (conj-c2 ss)))))
    ((disj? ss)
     (follow-path (cons (list (car path) ss) choices) (cdr path)
                  (if (car path) (disj-c1 ss) (disj-c2 ss))))
    ((pause? ss)
     (follow-path choices path (fstart (pause-state ss) (pause-goal ss))))
    (else (error 'follow-path (format "bad stream following ~s ~s" path ss)))))

(define (leaf? ss)
  (cond
    ((disj? ss) #f)
    ((conj? ss) (and (leaf? (conj-c1 ss)) (leaf? (conj-c2 ss))))
    ((pause? ss) (leaf? (pause-goal ss)))
    (else #t)))

(define (follow-ctx0 subpath ss) (list subpath ss))

(define (follow-path* ctx choices path ss)
  (define (choice-shift k)
    (lambda (choice) (ctx (car choice) (conj (cadr choice) k))))
  (define (ctx-disj direction alt-branch)
    (lambda (subpath ss)
      (ctx (cons direction subpath)
           (if ss
             (if direction (disj ss alt-branch) (disj alt-branch ss))
             alt-branch))))
  (define (ctx-fill alt) (cadr (ctx '() alt)))
  (cond
    ((pair? ss) (list path (car ss) (ctx-fill (cdr ss)) choices))
    ((state? ss) (list path ss (ctx-fill #f) choices))
    ((null? path) (list '() ss (ctx-fill #f) choices))
    ((not ss) (list path #f (ctx-fill #f) choices))
    ((conj? ss)
     (let* ((result (follow-path* follow-ctx0 '() path (conj-c1 ss)))
            (path (car result))
            (ss1 (cadr result))
            (alt-ss (caddr result))
            (alt-ss (and alt-ss (conj alt-ss (conj-c2 ss))))
            (choices (append (map (choice-shift (conj-c2 ss)) (cadddr result))
                             choices))
            (ctx (if alt-ss (ctx-disj #t alt-ss) ctx)))
       (follow-path* ctx choices path (fbind ss1 (conj-c2 ss)))))
    ((disj? ss)
     (let* ((dir (car path))
            (branch (if dir (disj-c1 ss) (disj-c2 ss)))
            (alt-branch (if dir (disj-c2 ss) (disj-c1 ss))))
       (follow-path* (ctx-disj dir alt-branch)
                     (if (leaf? branch) (cons (ctx (list dir) ss) choices)
                       choices)
                     (cdr path) branch)))
    ((pause? ss)
     (follow-path* ctx choices path (fstart (pause-state ss) (pause-goal ss))))
    (else (error 'follow-path* (format "bad stream following ~s ~s" path ss)))))

(define (wake-path path ss)
  (cond
    ((conj? ss) (conj (wake-path path (conj-c1 ss)) (conj-c2 ss)))
    ((disj? ss)
     (cond ((null? path) (error 'wake-path (format "path is too short ~s" ss)))
           ((car path) (disj (wake-path (cdr path) (disj-c1 ss)) (disj-c2 ss)))
           (else (disj (disj-c1 ss) (wake-path (cdr path) (disj-c2 ss))))))
    ((pause? ss)
     (cond ((not (zzz? (pause-goal ss)))
            (error 'wake-path (format "expected zzz ~s ~s" path ss)))
           ((pair? path)
            (error 'wake-path (format "path is too long ~s ~s" path ss)))
           (else (prune-goal
                   50 (pause-state ss) ((zzz-wake (pause-goal ss)))))))
    (else (error 'wake-path (format "cannot wake ~s ~s" path ss)))))

(define (prune force? ss)
  (cond
    ((conj? ss) (prune-bind force? (prune force? (conj-c1 ss)) (conj-c2 ss)))
    ((disj? ss) (prune-mplus force? (prune #f (disj-c1 ss)) (disj-c2 ss)))
    ((pause? ss) (prune-goal force? (pause-state ss) (pause-goal ss)))
    ((not ss) #f)
    (else ss)))
(define (prune-goal force? st goal)
  (cond
    ((conj? goal)
     (prune-bind force? (prune-goal force? st (conj-c1 goal)) (conj-c2 goal)))
    ((disj? goal)
     (prune force? (disj (pause st (disj-c1 goal)) (pause st (disj-c2 goal)))))
    ((zzz? goal)
     (if force?
       (prune-goal (or (eq? #t force?) (and (< 1 force?) (- force? 1)))
                   st ((zzz-wake goal)))
       (pause st goal)))
    ((==? goal) (unify st (==-t1 goal) (==-t2 goal)))
    (else (error 'prune-goal (format "unexpected goal: ~s" ss)))))
(define (prune-mplus force? c1 c2)
  (define (build c1 c2)
    (cond ((pair? c1) (cons (car c1) (build (cdr c1) c2)))
          ((state? c1) (cons c1 c2))
          ((pair? c2) (cons (car c2) (build (cdr c2) c1)))
          ((state? c2) (cons c2 c1))
          (else (disj c1 c2))))
  (if c1 (let ((c2 (prune #f c2)))
           (cond (c2 (build c1 c2))
                 (force? (prune force? c1))
                 (else c1)))
    (prune force? c2)))
(define (prune-bind force? ss goal)
  (cond ((not ss) #f)
        ((state? ss) (prune-goal force? ss goal))
        ((pair? ss) (prune-mplus force? (prune-goal #f (car ss) goal)
                                 (conj (cdr ss) goal)))
        (else (conj ss goal))))

(define (expand-path path path-expected ss0)
  (define ss (prune #t (wake-path path ss0)))
  (list (cond ((not ss) (error 'expand-path (format "no solution ~s" ss0)))
              ((or (state? ss) (pair? ss)) 'solved)
              ((equal? path path-expected) 'good)
              (else 'unknown))
        ss))

(define (good-path hint ss g*)
  (define (use-hint st) (unify st (==-t1 hint) (==-t2 hint)))
  (define (good-path-goal st g g*)
    (cond ((conj? g) (good-path-goal st (conj-c1 g) (cons (conj-c2 g) g*)))
          ((disj? g) (let ((p1 (good-path-goal st (disj-c1 g) g*)))
                       (if p1 (cons #t p1)
                         (let ((p2 (good-path-goal st (disj-c2 g) g*)))
                           (and p2 (cons #f p2))))))
          ((zzz? g) (and (good-path-goal st ((zzz-wake g)) g*) '()))
          ((==? g)
           (let ((st (unify st (==-t1 g) (==-t2 g))))
             (and st (or (null? g*) (good-path-goal st (car g*) (cdr g*)))
                  '())))
          (else (error 'good-path-goal (format "unexpected goal ~s" g)))))
  (cond ((conj? ss) (good-path hint (conj-c1 ss) (cons (conj-c2 ss) g*)))
        ((disj? ss) (let* ((p1 (good-path hint (disj-c1 ss) g*)))
                      (if p1 (cons #t p1)
                        (let ((p2 (good-path hint (disj-c2 ss) g*)))
                          (and p2 (cons #f p2))))))
        ((pause? ss) (let ((st (use-hint (pause-state ss))))
                       (and st (good-path-goal st (pause-goal ss) g*))))
        (else (error 'good-path (format "unexpected stream ~s" ss)))))

(define (good-paths hint ss)
  (define path (good-path hint ss '()))
  (define next (expand-path path path ss))
  (define flag (car next))
  (define ss-next (cadr next))
  (cons (cons path ss) (if (eq? 'solved flag) '() (good-paths hint ss-next))))

(define (interact in show out hint ss gpath show?)
  (define (valid-path? path)
    (or (null? path)
        (and (pair? path) (or (eqv? #t (car path)) (eqv? #f (car path)))
             (valid-path? (cdr path)))))
  (define good (if gpath gpath (good-path hint ss '())))
  (when show? (show ss))
  (let ((request (in)))
    (when (not (eof-object? request))
      (cond
        ((eq? 'good-path request)
         (out (list 'good-path good))
         (interact in show out hint ss good #f))
        ((eq? 'steps-remaining request)
         (out (list 'steps-remaining (map car (good-paths hint ss))))
         (interact in show out hint ss good #f))
        ((and (pair? request) (eq? 'jump-to-steps-remaining (car request)))
         (let* ((remaining (good-paths hint ss))
                (remaining-count (length remaining))
                (drop-count (- remaining-count (cadr request)))
                (chosen (and (<= 0 drop-count)
                             (> remaining-count drop-count)
                             (list-ref remaining drop-count))))
           (when (> 0 drop-count)
             (error 'interact (format "only ~s steps remain: ~s"
                                      remaining-count (cadr request))))
           (when (<= remaining-count drop-count)
             (error 'interact "cannot jump to steps-remaining lower than 1"))
           (interact in show out hint (cdr chosen) (car chosen) #t)))
        ((and (pair? request) (valid-path? request))
         (let* ((result (expand-path request good ss))
                (flag (car result))
                (ss2 (cadr result)))
           (out (list 'follow-path flag))
           (when (not (or (eq? 'solved flag) (eq? 'fail-solved flag)))
             (interact in show out hint ss2 #f #t))))
        (else (error 'interact (format "invalid request: ~s" request)))))))

(define (bind ss goal)
  (cond
    ((not ss) #f)
    ((state? ss) (start ss goal))
    ((pair? ss) (disj (pause (car ss) goal) (conj (cdr ss) goal)))
    ;; Immediate restart confuses solution->path, so disable this for now.
    ;((pair? ss) (mplus (start (car ss) goal) (conj (cdr ss) goal)))
    (else (conj ss goal))))
(define (mplus s1 s2)
  (cond
    ((not s1)
     (solution-describe! 'fail)
     s2)
    ((state? s1)
     (solution-describe! 'succeed)
     (cons s1 s2))
    ((pair? s1)
     (solution-describe! 'ascend)
     (cons (car s1) (disj s2 (cdr s1))))
    (else
      (solution-describe! 'swap)
      (disj s2 s1))))

(define (start st goal)
  (cond
    ((conj? goal) (bind (start st (conj-c1 goal)) (conj-c2 goal)))
    ((disj? goal) (disj (pause st (disj-c1 goal)) (pause st (disj-c2 goal))))
    ((zzz? goal) (start st ((zzz-wake goal))))
    ((==? goal) (unify st (==-t1 goal) (==-t2 goal)))
    (else (error 'start (format "invalid goal to start: ~s" goal)))))

(define (continue ss)
  (cond
    ((conj? ss) (bind (continue (conj-c1 ss)) (conj-c2 ss)))
    ((disj? ss) (mplus (continue (disj-c1 ss)) (disj-c2 ss)))
    ((pause? ss) (start (pause-state ss) (pause-goal ss)))
    ((not ss) #f)
    ((state? ss) (cons ss #f))
    (else (error 'start (format "invalid stream to continue: ~s" ss)))))

(define (stream-next ps)
  (define ss (begin (solution-step! ps) (continue ps)))
  (cond
    ((not ss) '())
    ((state? ss) (cons ss #f))
    ((pair? ss)
     (solution-describe! 'ascend)
     ss)
    (else (stream-next ss))))

(define (stream-take n ps)
  (if (and n (= 0 n))
    '()
    (let ((ss (stream-next ps)))
      (if (pair? ss)
        (cons (car ss) (stream-take (and n (- n 1)) (cdr ss)))
        '()))))

(define (goal-pretty goal)
  (cond
    ((conj? goal) `(conj ,(goal-pretty (conj-c1 goal)) ,(goal-pretty (conj-c2 goal))))
    ((disj? goal) `(disj ,(goal-pretty (disj-c1 goal)) ,(goal-pretty (disj-c2 goal))))
    ((zzz? goal) (zzz-metadata goal))
    ((==? goal) `(== ,(==-t1 goal) ,(==-t2 goal)))))
(define (stream-pretty ss)
  (define (pretty ss)
    (cond
      ((conj? ss) `(conj ,(pretty (conj-c1 ss))
                         ,(reify #f state-empty (goal-pretty (conj-c2 ss)))))
      ((disj? ss) `(disj ,(pretty (disj-c1 ss)) ,(pretty (disj-c2 ss))))
      ((pause? ss)
       (reify #f (pause-state ss)
              `(pause (state ,var-initial) ,(goal-pretty (pause-goal ss)))))
      (else ss)))
  (let loop ((ss ss) (states '()))
    (cond
      ((state? ss) (loop #f (cons ss states)))
      ((pair? ss) (loop (cdr ss) (cons (car ss) states)))
      (else (list (map reify-initial (reverse states)) (pretty ss))))))

(define (step n ss)
  (cond
    ((= 0 n) ss)
    ((not ss) #f)
    ((pair? ss) (cons (car ss) (step n (cdr ss))))
    (else (solution-step! ss) (step (- n 1) (continue ss)))))

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

(define-syntax conj*
  (syntax-rules ()
    ((_) succeed)
    ((_ g) g)
    ((_ gs ... g-final) (conj (conj* gs ...) g-final))))
(define-syntax disj*
  (syntax-rules ()
    ((_) fail)
    ((_ g) g)
    ((_ g0 gs ...) (disj g0 (disj* gs ...)))))

(define-syntax fresh
  (syntax-rules ()
    ((_ (vr ...) g0 gs ...) (let ((vr (var/fresh)) ...) (conj* g0 gs ...)))))
(define-syntax conde
  (syntax-rules ()
    ((_ (g0 gs ...)) (conj* g0 gs ...))
    ((_ c0 cs ...) (disj (conde c0) (conde cs ...)))))

(define (run-goal n st goal) (stream-take n (pause st goal)))

(define (walk* st tm)
  (let ((tm (walk st tm)))
    (if (pair? tm)
      `(,(walk* st (car tm)) . ,(walk* st (cdr tm)))
      tm)))

(define (reify index st tm)
  (let loop
    ((rvs store-empty) (index index) (tm tm) (k (lambda (rvs i tm) tm)))
    (let ((tm (walk st tm)))
      (cond
        ((var? tm)
         (let* ((idx (store-ref rvs tm (or index (var-index tm))))
                (n (string->symbol (string-append "_." (number->string idx)))))
           (if (eqv? index idx)
             (k (store-set rvs tm index) (+ 1 index) n)
             (k rvs index n))))
        ((pair? tm) (loop rvs index (car tm)
                          (lambda (r i a)
                            (loop r i (cdr tm)
                                  (lambda (r i d) (k r i `(,a . ,d)))))))
        (else (k rvs index tm))))))
(define (reify-initial st) (reify 0 st var-initial))

(define-syntax query
  (syntax-rules ()
    ((_ (vr ...) g0 gs ...)
     (let ((goal (fresh (vr ...) (== (list vr ...) var-initial) g0 gs ...)))
       (pause state-empty goal)))))
(define-syntax run
  (syntax-rules ()
    ((_ n body ...) (map reify-initial (stream-take n (query body ...))))))
(define-syntax run*
  (syntax-rules ()
    ((_ body ...) (run #f body ...))))