Kibitとclojure.core.logic

Clojure Advent Calendar 2020 20日目の記事です。(が、大幅におくれ25日になっちゃった。メリークリスプマス!)
以前 静的解析ツールKibitを眺めていたらCore.logicが使われていたのでどのように使われているかという話です。

論理プログラミング言語とは、ルールを宣言的にかいてそれを解かせるということに特化した言語です。
Prologという言語がよく知られていると思います。

そして、core.logicはSchemeの論理プログラミングDSLである、miniKanrenのClojure実装です。

core.logicの実用例を他に眺めていたが、古いものが多かったのであまり深くは追っていません。
言語処理系の例では型を解くのに使われていたり、日付、時間ライブラリのルールをcore.logicで記述してそれで計算を解いているような使われ方をしているようです。

Kibit

KibitはClojureの静的解析ツールです。
入力したソースコードの良くない部分を探し、あればその修正方法を返してくれます。

内部では、ソースコードの悪い例を専用の記法を用いて、パターンとして記述し、良い例も同じように記述し、組みにして持っておきます。
そして、入力したソースコードが記述したパターンにあてはまれば通知するというわけです。

パターンの記法例はこのようになっています。
これは、(+ x 1)のようなコードを、(inc x)にするようにするパターンのコードです。
?xのように?から始まるシンボルはワイルドカードのようになっていて、任意の式がマッチするようになっています。
そして、良いコードのパターンに同じ?から始まるシンボルがあればマッチしたものを挿入するようにしています。

(defrules rules
  [(+ ?x 1) (inc ?x)]
  略)

このマッチさせて展開する部分にcore.logicが使われています。
core.logicでは、前の説明のワイルドカードの部分を論理変数としておこなうと次のようになります。
xが論理変数です。

(run* [x] (== (list '+ x 1) '(+ (* 2 3) 1)));=> ((* 2 3))

kibitのパターン記法の?から始まるシンボルは内部でcore.logicの論理変数(lvar)に変換されてから使われます。この変換は、clojure.core.logic.unifier/prep関数を用いています。sequence中の?からはじまるsymbolをlvarに変換してくれます。

次は展開する部分についてです。
同じように論理変数を良いコードのパターンに埋め込むことで、直前の悪いコードのパターンで拘束された論理変数に対応する部分が挿入されます。あとはそれを結果(ここではres)に対応させるだけです。

(run* [res]
  (fresh [x]
    (== (list '+ x 1) '(+ (* 2 3) 1))
    (== (list 'inc x) res)))
;-> ((inc (* 2 3)))