CPS変換風のやり方で NNF(否定標準形) を DNF(選言標準形) に変換する

NNF: 否定(¬) が葉ノードにだけついている、∧ と ∨ で表現された論理式。
DNF: NNFのうち、root ノードが ∨ であり、それぞれの節が ∧ だけで出来ている論理式。

例: 以下のNNFを

(and (or (and x (not z)) y)
     c
     (or a b))

DNFに変換したい。

(or (and x (not z) c a)
    (and x (not z) c b)
    (and y c a)
    (and y c b))

べつにこれを実装するのにCPS変換の知識が必須というわけではない。
しかし、イテレータみたいなものを実装しようとすると、必然的にCPS変換っぽくなるのだ。

(ql:quickload '(:trivia :trivia.quasiquote))
(use-package :trivia) ; パターンマッチ用マクロ
(named-readtables:in-readtable :fare-quasiquote) ; パターンにquasiquote ` を使える

(defun NNF-DNF (condition)
  ;; 論理式をとって、継続渡しスタイル(cps)の関数を返す。
  ;; OR 節はイテレータになる。
  (ematch condition
    (`(or ,@rest)                             ; list の 最初の要素がorのとき
      (let ((restk (mapcar #'NNF-DNF rest)))  ; 要素ごとにcps関数を作って
        (lambda (k)                    ; 関数自体もcps関数を返す
          ;; calls k for each element
          (dolist (nowk restk)         ; イテレータ
            (funcall nowk k)))))       ; それぞれのcps関数に継続(残りの計算)を渡す

    (`(,first ,@rest)                 ; or 以外の場合
     (let ((firstk (NNF-DNF first))   ; first と rest のcps関数を作って
           (restk  (NNF-DNF rest)))
       (lambda (k)
         (funcall firstk              ; first を評価
                  (lambda (result)    ; 結果が継続に渡されて
                    (funcall restk    ; rest も評価
                             (lambda (result2) ; 結果が帰ってきて
                               ;; 2つをconsで渡して 継続(残りの計算) に渡す
                               (funcall k (cons result result2)))))))))

    (_ ; list じゃない場合は そのまま現在の値を継続に渡す
     (lambda (k) (funcall k condition)))))

これだけだと結果を取り出す方法を書いてないので

(defun use-expander (condition)
  (let (acc)
    (funcall (NNF-DNF condition)
             (lambda (result)      ; 最後のコールバックとしてaccに貯める関数を指定
               (push result acc)))
    (print acc)))

結果確認。

(use-expander 'a)
(use-expander '(or a b))
(use-expander '(or a b c (or d e)))
(use-expander '(and x (or a b)))
(use-expander '(and (or x y) (or a b)))
(use-expander '(and (or x y) c (or a b)))
(use-expander '(and (or (and x z) y) c (or a b)))
(use-expander '(or (and x (or w z)) y))

(A) 
(B A) 
(E D C B A) 
((AND X B) (AND X A)) 
((AND Y B) (AND Y A) (AND X B) (AND X A)) 
((AND Y C B) (AND Y C A) (AND X C B) (AND X C A)) 
((AND Y C B) (AND Y C A) (AND (AND X Z) C B) (AND (AND X Z) C A)) 
(Y (AND X Z) (AND X W)) 

動いてるっぽい。