Reasoned Schemer (61) run, run*

runとrun*

(define-syntax run
  (syntax-rules ()
    ((run n (x0 x ...) g ...)
     (run n q (fresh (x0 x ...) (== `(,x0 ,x ...) q) g ...)))
    ((run n q g ...)
     (let ((q (var 'q)))
       (map (reify q) (run-goal n (conj g ...)))))))

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

freshはあとで定義されるのでここではfreshのまま扱うか

(run n (x0 x ...) g ...)という形は
qという変数を導入してqに(x0 x ...)を割り当てるようにして
(run n q g ...)の形に変換する
(run n q g ...)の形はただの書き替えなんだけど
qが決め打ちでいいのかなあ
gの中にqがあったらよろしくなくない？
いや、マクロ展開のときqは別の変数に置き換えられるのか
いやいや、1行目のqは決め打ちになるんじゃないか

Macro Stepper使って展開されたものを確認してみよう
まず問題なさげなほうから

  (run* (x y) (conj2 (== 'split x) (== 'pea y)))
= (run #f (x y) (conj2 (== 'split x) (== 'pea y)))
= (run #f q (fresh (x y) (== `(,x ,y) q) (conj2 (== 'split x) (== 'pea y))))

qっていう変数を使ってたら？

  (run* (q y) (conj2 (== 'split q) (== 'pea y)))
= (run #f (q y) (conj2 (== 'split q) (== 'pea y)))
= (run #f q (fresh (q y) (== `(,q ,y) q) (conj2 (== 'split q) (== 'pea y))))

なんかあやしくない？
実行すると？

> (run* (x y) (conj2 (== 'split x) (== 'pea y)))
((split pea))
> (run* (q y) (conj2 (== 'split q) (== 'pea y)))
((split pea))

うーん
普通に結果が出てる
いいのかなあ

もう１回展開

(let ((q (var 'q)))
  (map
   (reify q)
   (run-goal
    #f
    (conj (fresh (q y) (== `(,q ,y) q) (conj2 (== 'split q) (== 'pea y)))))))

varで導入される変数とfreshで導入される変数は別ってことかな
考えてみると別物だけど
上の式でどのqが何なのかというとまだ理解が足りない