instaparseで遊ぶ

この記事はClojure Advent Calendar 2013 - Qiita [キータ]１９日目の記事です。

instaparse

本記事ではinstaparseというライブラリを使って遊んでみます。

instaparseはEBNFやABNFで記述された文脈自由文法から自動的にパーサを生成してくれます。 左再帰、右再帰、曖昧性など、いかなる文脈自由文法でも動作します。 生成されたパーサは文字列からenliveまたはhiccup風の木構造を生成します。

今回は型なしラムダ計算を題材にします。

型なしラムダ計算

型なしラムダ計算は、型がない（または型がひとつしかない）ラムダ計算です。

ラムダ計算はとてもシンプルで、すべての計算が関数定義と関数適用だけで実現可能です。

ラムダ計算の構文は以下の３つからなります。

t ::=        項
    x        変数
  | \x . t   ラムダ抽象
  | t t      関数適用

定義くらいはほしいだろう、ということで、今回作るパーサは以下のような拡張をした構文にします。

lang ::= (expr | def)+
def  ::= var '=' expr ';'*
expr ::= (var | app | abs)
     |  '(' app | abs ')' ';'*
var  ::= [a-zA-Z-]+
app  ::= expr expr
abs  ::= '\\' var '->' expr

さて、上の構文を用いてパーサを作ってみます。

(ns lambda.core
  (:require [instaparse.core :as insta]
            [clojure.core.match :as match]))

(def parser
  (insta/parser
    "lang = (expr | def)+
    def = <w> var <'='> expr <';'*> <w>
    <expr> = <w>
    (var | app | abs
         | <'('> (app | abs) <')'>) <w> <';'*>
    var = <w> #'[a-zA-Z-]+' <w>
    app = expr expr
    abs = <'\\\\'> var <arrow> expr
    w = #'[\\n\\s]*'
    arrow = '->'
    "))

簡単に書けました。

実行すると以下のような結果が得られます。

(parser "true = \\x -> \\y -> x;")
; => [:lang [:def [:var "true"] [:abs [:var "x"] [:abs [:var "y"] [:var "x"]]]]]

驚きのお手軽感です。

お分かりかとは思いますが、langやdefなどがキーとなった木（ベクタ）ができています。そして< >で囲まれたexprやwは出力結果にはありません。 < >はパース結果を隠す役割があります。他にも正規表現が使えたりと大変便利なライブラリです。

またパース結果をグラフ化することもできます。

(insta/visualize (parser (slurp "sample.lambda")))

せっかくパーサができたので評価できるようにします。

実装にあたってはこの辺とかこの辺を参考にしました。

α変換．．．本来だと条件によって置換しなくてもいいこともある。ﾌﾑﾌﾑ〜〜〜。

面倒だし、全部置き換えたところで一緒なので全部置換することにします。

(gensym)でユニークな変数が降ってくるので、\x -> \y -> x yのような形のものを、\unique_symbol -> \y -> \unique_symbol yのように変換します。 そのようにすれば適用する式の中身と変数名がかぶりませんね。

HaskellやOCamlみたいなパターンマッチがClojureにもあったらなーと思っていたら、clojure.core.matchがなかなか良さそうなので使ってみました。

(def env (atom {}))

(defn evaluate [expr]
  (match/match
    expr
    [:def v e]
    (do (swap! env conj {v e}) v)

    [:var v]
    (get @env [:var v] [:var v])

    [:app [:var v] n]
    [:app (get @env [:var v] [:var v]) n]

    [:app [:app m n'] n]
    [:app (evaluate [:app m n']) n]

    [:app [:abs [:var v] body] n]
    (clojure.walk/postwalk
      (fn [z] (if (= z [:var v]) n z))
      (evaluate body))

    [:abs [:var v] body]
    (let [v' (str (gensym))]
      [:abs [:var v']
            (clojure.walk/postwalk 
              (fn [z] (if (= z [:var v]) [:var v'] z))
              (evaluate body))])))

(defn show [expr]
  (match/match
    expr
    [:lang & n]
    (reduce str (map show n))
    [:def v e]
    (str (show v) " = " (show e))
    [:var v]
    v
    [:app f x]
    (str "(" (show f) " " (show x) ")")
    [:abs arg e]
    (str "^" (show arg) "." (show e))))

(defn evaluate-all [expr]
  (match/match
    expr
    [:app m n]
    (evaluate-all (evaluate expr))
    :else expr))

(let [code
      (str
        "true = \\x -> \\y -> x;"                ;; "true = ^x.^y.x"
        "false = \\x -> \\y -> y;"               ;; "false = ^x.^y.y"
        "if = \\p -> \\t -> \\f -> ((p t) f);"   ;; "if = ^p.^t.^f.((p t) f)"
        "cons = \\x -> \\y -> \\f -> ((f x) y);" ;; "cons = ^x.^y.^f.((f x) y)"
        "car = \\p -> p true;"                   ;; "car = ^p.(p true)"
        "cdr = \\p -> p false;"                  ;; "cdr = ^p.(p false)"
        "(car ((cons true) false))"              ;; "^x.^y.x"
        "(((if true) false) true)")              ;; "^x.^y.y"
      parsed (parser code)
      results (map evaluate-all (rest parsed))]
 (map show results))

Clojureすごい！instaparseすごい！

というわけで、１９日目はこれでおしまいです。