So-net無料ブログ作成

Mling: ML処理系のC言語インターフェイスを自動生成する [SML]

SMLの処理系のC言語インターフェイスをCのヘッダから自動生成するツールを作った。

Mling: ML FFI Interface Generator

現在のところMLtonとPoly/MLに対応していて、cursesを使うサンプルが動くようになっている。

先行するものとしてSML/NJとMLtonにはmlnlffigenというツールがあるようなのだけど、使い方がよくわからなかったのだ。 やりたいのはCの関数の型をMLの型に書き換える機械的な作業なので、いいや自分で作ろうということになった。

C言語の構文解析には紆余曲折の後libclangをPythonから使うことにした。 Ubuntuでpython-clang-3.3を導入した環境で動作を確認している。

一般的な構文解析ツールでC言語の構文解析をしようとするとtypedef問題などに突き当たってしまって、かなり面倒なことになる。 libclangは何と言ってもCコンパイラが使う真正のC言語パーサーだからそれを使えるのは理想的なはずだ。 でもlibclang自体の使い方もドキュメントが乏しくてよくわからないところが多い。 だから面倒くささということに関しては結局どっちもどっちかもしれない。


NuSMVを試す [SMV]

モデル検査ツールのNuSMVを試してみた。

例題として基本的な排他制御を書いてみる。

MODULE lock
  VAR
    locked-by : {nobody, 0, 1};
  ASSIGN
    init(locked-by) := nobody;

MODULE proc(id, lock)
  VAR
    status: {normal, trying, critical};
  ASSIGN
    init(status) := normal;
    next(status) :=
      case
        (status = normal) : {trying, normal};
        (status = trying) & (lock.locked-by = nobody) : critical;
        (status = critical) : {critical, normal};
        TRUE : status;
      esac;
    next(lock.locked-by) :=
      case
        (next(status) = critical) : id;
        (status = critical & next(status) = normal) : nobody;
        TRUE : lock.locked-by;
      esac;

MODULE main
  VAR
    lock: process lock;
    proc0: process proc(0, lock);
    proc1: process proc(1, lock);
  -- safety: at most one process can enter ciritcal section.
  LTLSPEC G !((proc0.status = critical) & (proc1.status = critical))

lockモジュールはlocked-byという変数だけを持つ。 これはロックを所有しているプロセスID(誰もロックをとっていない場合はnobody)を示す。

procモジュールはプロセスの現在の状態をstatusという変数で持つ。 normalは何もしていない状態、tryingはロックを取得しようとしている状態、criticalはロックを取得した状態である。

statusの初期状態はnormalで、状態遷移はnext(status) := ...で定義される。 normalの場合は、そのままnormalにとどまるか、非決定的にtryingに遷移する。 tryingで、かつロックが誰にも取得されていなければcriticalに遷移する。 criticalの場合は、そのままcriticalにとどまるか、非決定的にnormalに遷移する。

procモジュールの中でロックの状態の更新も行っている。 statusがcriticalの場合は自身のプロセスIDで置き換える。 criticalからnormalに遷移した場合は所有者をnobodyに戻す。

mainはlockと2つのprocを結びつける。procの引数にはプロセスIDとロックを与える。

LTLSPECはこのモデルが満たすべき仕様(最大1つのプロセスしかクリティカルセクションに入れない)を時相論理式で定義している。

$ NuSMV mutex.smv
*** This is NuSMV 2.5.4 (compiled on Sun Aug 24 14:27:46 UTC 2014)
(中略)
WARNING *** Processes are still supported, but deprecated.      ***
WARNING *** In the future processes may be no longer supported. ***

WARNING *** The model contains PROCESSes or ISAs. ***
WARNING *** The HRC hierarchy will not be usable. ***
-- specification  G !(proc0.status = critical & proc1.status = critical)  is true

最後の行で仕様が満たされたことがわかる。

このようなモデルの書き方がもう廃止候補になっていることが警告されるのだけど、 その背景や代替の書き方などについて知識がないのでとりあえずこのままいくことにする。

次に新たな仕様として、飢餓状態が起こらないことを表現したい。 これはそれぞれのプロセスについて 「どんな場合でも一度tryingになったらいつかはcriticalに入れる」 と宣言することで表現できる。 そこでMODULE procの最後に次の仕様を記述する。

LTLSPEC G ((status = trying) -> F (status = critical))

これで実行してみると仕様が満たされないことが報告され、その反例が示される。

$ NuSMV mutex.smv
*** This is NuSMV 2.5.4 (compiled on Sun Aug 24 14:27:46 UTC 2014)
(中略)
-- specification  G (status = trying ->  F status = critical) IN proc0 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
  lock.locked-by = nobody
  proc0.status = normal
  proc1.status = normal
-> Input: 1.2 <-
  _process_selector_ = proc0
  running = FALSE
  proc1.running = FALSE
  proc0.running = TRUE
  lock.running = FALSE
-> State: 1.2 <-
  proc0.status = trying
-> Input: 1.3 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-> State: 1.3 <-
  proc1.status = trying
-> Input: 1.4 <-
-- Loop starts here
-> State: 1.4 <-
  lock.locked-by = 1
  proc1.status = critical
-> Input: 1.5 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-> State: 1.5 <-
-- specification  G (status = trying ->  F status = critical) IN proc1 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 2.1 <-
  lock.locked-by = nobody
  proc0.status = normal
  proc1.status = normal
-> Input: 2.2 <-
  _process_selector_ = proc1
  running = FALSE
  proc1.running = TRUE
  proc0.running = FALSE
  lock.running = FALSE
-> State: 2.2 <-
  proc1.status = trying
-> Input: 2.3 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-> State: 2.3 <-
-> Input: 2.4 <-
  _process_selector_ = proc0
  running = FALSE
  proc0.running = TRUE
-- Loop starts here
-> State: 2.4 <-
  proc0.status = trying
-> Input: 2.5 <-
  _process_selector_ = main
  running = TRUE
  proc0.running = FALSE
-- Loop starts here
-> State: 2.5 <-
-> Input: 2.6 <-
  _process_selector_ = lock
  running = FALSE
  lock.running = TRUE
-> State: 2.6 <-
-- specification  G !(proc0.status = critical & proc1.status = critical)  is true

この反例はちょっとつまらない、NuSMVの使い方に関するともいえるものだ。 この反例ではState: 1.2やState: 2.2で各プロセスがtryingになったあと、一度もそのプロセスに実行権が回ってきていないのである。

ここではOSのスケジューラがプロセスに対してある程度公平な扱いをすることを前提にしたい。 このためには、MODULE procに次の行を追加する。

FAIRNESS running

runningはプロセスが実行されていることを示す暗黙の変数で、先ほどの反例のトレース中にも現れていた。 FAIRNESSというのはその式が「いつも『いつかは成立する』」(その式が永遠に成立しないような経路を排除する)ということを条件として与えるものだ。

これで実行してもまだ反例が見つかる。

$ NuSMV mutex.smv
(中略)
-- specification  G (status = trying ->  F status = critical) IN proc0 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
  lock.locked-by = nobody
  proc0.status = normal
  proc1.status = normal
-> Input: 1.2 <-
  _process_selector_ = proc0
  running = FALSE
  proc1.running = FALSE
  proc0.running = TRUE
  lock.running = FALSE
-> State: 1.2 <-
  proc0.status = trying
-> Input: 1.3 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-> State: 1.3 <-
  proc1.status = trying
-> Input: 1.4 <-
-- Loop starts here
-> State: 1.4 <-
  lock.locked-by = 1
  proc1.status = critical
-> Input: 1.5 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-- Loop starts here
-> State: 1.5 <-
-> Input: 1.6 <-
  _process_selector_ = proc0
  running = FALSE
  proc0.running = TRUE
-- Loop starts here
-> State: 1.6 <-
-> Input: 1.7 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-- Loop starts here
-> State: 1.7 <-
-> Input: 1.8 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-> State: 1.8 <-
-- specification  G (status = trying ->  F status = critical) IN proc1 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 2.1 <-
  lock.locked-by = nobody
  proc0.status = normal
  proc1.status = normal
-> Input: 2.2 <-
  _process_selector_ = proc0
  running = FALSE
  proc1.running = FALSE
  proc0.running = TRUE
  lock.running = FALSE
-> State: 2.2 <-
  proc0.status = trying
-> Input: 2.3 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-> State: 2.3 <-
  proc1.status = trying
-> Input: 2.4 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-> State: 2.4 <-
-> Input: 2.5 <-
  _process_selector_ = proc0
  running = FALSE
  proc0.running = TRUE
-- Loop starts here
-> State: 2.5 <-
  lock.locked-by = 0
  proc0.status = critical
-> Input: 2.6 <-
-- Loop starts here
-> State: 2.6 <-
-> Input: 2.7 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-- Loop starts here
-> State: 2.7 <-
-> Input: 2.8 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-> State: 2.8 <-
-- specification  G !(proc0.status = critical & proc1.status = critical)  is true

これは何かというと、自分がtryingのときにもう一方のプロセスがロックを取得し、そのままずっと離さないことを示している。 我々のモデルには「ロックはいつか解放される」とは表現されていなかったのでこのようなことが起こる。

解決方法はおそらく2通りあり、FAIRNESSを使ってロックが永遠に離されない経路を排除するか、 ロックが有限ステップ内で解放されるようにASSIGNの定義を変えることだ。 ここでは後者の方法を選択することにし、プロセスはロックを取得したら次のステップで解放するようにする。

(status = critical) : normal;

また実行するとまた反例が見つかる。

$ NuSMV mutex.smv
(中略)
-- specification  G (status = trying ->  F status = critical) IN proc0 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
  lock.locked-by = nobody
  proc0.status = normal
  proc1.status = normal
-> Input: 1.2 <-
  _process_selector_ = proc0
  running = FALSE
  proc1.running = FALSE
  proc0.running = TRUE
  lock.running = FALSE
-> State: 1.2 <-
  proc0.status = trying
-> Input: 1.3 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-> State: 1.3 <-
  proc1.status = trying
-> Input: 1.4 <-
-- Loop starts here
-> State: 1.4 <-
  lock.locked-by = 1
  proc1.status = critical
-> Input: 1.5 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-- Loop starts here
-> State: 1.5 <-
-> Input: 1.6 <-
  _process_selector_ = proc0
  running = FALSE
  proc0.running = TRUE
-- Loop starts here
-> State: 1.6 <-
-> Input: 1.7 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-> State: 1.7 <-
  lock.locked-by = nobody
  proc1.status = normal
-> Input: 1.8 <-
-> State: 1.8 <-
  proc1.status = trying
-> Input: 1.9 <-
-> State: 1.9 <-
  lock.locked-by = 1
  proc1.status = critical
-- specification  G (status = trying ->  F status = critical) IN proc1 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 2.1 <-
  lock.locked-by = nobody
  proc0.status = normal
  proc1.status = normal
-> Input: 2.2 <-
  _process_selector_ = proc0
  running = FALSE
  proc1.running = FALSE
  proc0.running = TRUE
  lock.running = FALSE
-> State: 2.2 <-
  proc0.status = trying
-> Input: 2.3 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-> State: 2.3 <-
  proc1.status = trying
-> Input: 2.4 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-> State: 2.4 <-
-> Input: 2.5 <-
  _process_selector_ = proc0
  running = FALSE
  proc0.running = TRUE
-- Loop starts here
-> State: 2.5 <-
  lock.locked-by = 0
  proc0.status = critical
-> Input: 2.6 <-
-> State: 2.6 <-
  lock.locked-by = nobody
  proc0.status = normal
-> Input: 2.7 <-
-> State: 2.7 <-
  proc0.status = trying
-> Input: 2.8 <-
-- Loop starts here
-> State: 2.8 <-
  lock.locked-by = 0
  proc0.status = critical
-> Input: 2.9 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-- Loop starts here
-> State: 2.9 <-
-> Input: 2.10 <-
-> State: 2.10 <-
-- specification  G !(proc0.status = critical & proc1.status = critical)  is true

これは何かというと、自分がtryingの間もう一方のプロセスがロック取得・解放を延々と繰り返していてずっと割り込めないでいるのだ。

だからOSのスケジューラの公平さとは別に、ロックの動作自体に公平さをもたらす必要があることがわかる。 これはちょっと大仕事になる。

とりあえずtryingからcriticalに遷移していいかどうかの判断をprocから切り離してlockプロセスに移動する。 waitingという配列を導入して、procがtryingになるときにTRUEにする。 procはtrying中にlocked-byが自分自身になったときにcriticalに遷移できるが、locked-byを選ぶのはlockプロセスの仕事にする。 つまり、procはロックに応募するだけで、当選者を決めるのはlockの仕事である。

MODULE lock
  VAR
    locked-by : {nobody, 0, 1};
    waiting : array 0..1 of boolean;
  ASSIGN
    init(locked-by) := nobody;
    next(locked-by) :=
      case
        (locked-by = nobody & waiting[0] = TRUE) : 0;
        (locked-by = nobody & waiting[1] = TRUE) : 1;
        TRUE : locked-by;
      esac;
    next(waiting[0]) :=
      case
        (next(locked-by) = 0) : FALSE;
        TRUE : waiting[0];
      esac;
    next(waiting[1]) :=
      case
        (next(locked-by) = 1) : FALSE;
        TRUE : waiting[1];
      esac;
  FAIRNESS running

MODULE proc(id, lock)
  VAR
    status: {normal, trying, critical};
  ASSIGN
    init(status) := normal;
    init(lock.waiting[id]) := FALSE;
    next(status) :=
      case
        (status = normal) : {trying, normal};
        (status = trying) & (lock.locked-by = id) : critical;
        (status = critical) : normal;
        TRUE : status;
      esac;
    next(lock.waiting[id]) :=
      case
        (status = normal & next(status) = trying) : TRUE;
        TRUE : lock.waiting[id];
      esac;
    next(lock.locked-by) :=
      case
        (status = critical & next(status) = normal) : nobody;
        TRUE : lock.locked-by;
      esac;
  FAIRNESS running
  LTLSPEC G ((status = trying) -> F (status = critical))

MODULE main
  VAR
    lock: process lock;
    proc0: process proc(0, lock);
    proc1: process proc(1, lock);
  -- safety: at most one process can enter ciritcal section.
  LTLSPEC G !((proc0.status = critical) & (proc1.status = critical))

lockプロセスはwaitingがTRUEになっているプロセスのなかからlocked-byにするプロセスを選択するとともに、そのプロセスのwaitingをFALSEに戻す。 ここで next(waiting[0]) := ... と添え字ごとに書いている箇所は添え字部分を変数にしてforeachみたいな構文で書きたいのだが、まだ調査不足でやりかたがわからない。

これを実行するとproc0については仕様が成立し、proc1については成立しない結果となるが、 lockプロセスのプロセス選択が不公平だからだ。このモデルでは両方がtryingのとき必ずproc0を優先することになっている。

ここでturnという変数を導入する。turnはプロセス数を範囲とするカウンタであり、ロックが取得されていないときは1ずつ上がっていく。 waitingからロックを与えるプロセスを決めるときはturnと一致するプロセスがtryingであるかどうかを見る。 つまりプロセスを順番に見て行って一番最初にtryingとして見つかったものにロックを与える。

MODULE lock
  VAR
    locked-by : {nobody, 0, 1};
    waiting : array 0..1 of boolean;
    turn : 0..1;
  ASSIGN
    init(locked-by) := nobody;
    next(locked-by) :=
      case
        (locked-by = nobody & waiting[turn] = TRUE) : turn;
        TRUE : locked-by;
      esac;
    next(waiting[0]) :=
      case
        (next(locked-by) = 0) : FALSE;
        TRUE : waiting[0];
      esac;
    next(waiting[1]) :=
      case
        (next(locked-by) = 1) : FALSE;
        TRUE : waiting[1];
      esac;
    next(turn) :=
      case
        (locked-by = nobody) : (turn + 1) mod 2;
        TRUE : turn;
      esac;
  FAIRNESS running

このモデルを検証するとようやくすべての仕様が満たされた。

$ NuSMV mutex2.smv
(中略)
-- specification  G (status = trying ->  F status = critical) IN proc0 is true
-- specification  G (status = trying ->  F status = critical) IN proc1 is true
-- specification  G !(proc0.status = critical & proc1.status = critical)  is true

調査不足かつ情報もあまり多くないので、まだよくわかっていない部分も多い。 こうかけたらいいのに、という部分はところどころあるが、NuSMV自体の制約かもしれないし知らないだけかもしれない。


チルダ置換のbash, ksh93, zshの違い [sh]

シェルではコマンドや引数がチルダで始まるときに置換が行われる。

チルダの後に続く(スラッシュまでの)文字がユーザー名である場合、 そのユーザーのログインディレクトリに置換される。 たとえばrootのログインディレクトリが/rootのとき、次のようになる。

$ echo ~root
/root

この置換はクォートの内部では働かない。

$ echo "~root"
~root

ここまでの動作はbash, ksh93, zshで共通だ。

チルダに続くのが変数置換のとき、 bashではチルダ置換が行われないが、ksh93とzshでは行われる。

$ sudo bash -c 'echo ~$USER'
~root
$ sudo ksh -c 'echo ~$USER'
/root
$ sudo zsh -c 'echo ~$USER'
/root

チルダに続くのがクォートされた文字列のとき、 bashではチルダ置換が行われないが、ksh93とzshでは行われる。

$ bash -c 'echo ~"root"'
~root
$ ksh -c 'echo ~"root"'
/root
$ zsh -c 'echo ~"root"'
/root
$ bash -c 'echo ~"ro""ot"'
~root
$ ksh -c 'echo ~"ro""ot"'
/root
$ zsh -c 'echo ~"ro""ot"'
/root

チルダに続く文字列がエスケープされているとき、 bashではチルダ置換が行われないが、ksh93とzshでは行われる。

$ bash -c 'echo ~\r\o\o\t'
~root
$ ksh -c 'echo ~\r\o\o\t'
/root
$ zsh -c 'echo ~\r\o\o\t'
/root

チルダに続くのがコマンド置換のとき、3つのシェルのいずれでもチルダ置換が行われる。

$ bash -c "echo ~`echo root`"
/root
$ ksh -c "echo ~`echo root`"
/root
$ zsh -c "echo ~`echo root`"
/root
$ bash -c "echo ~$(echo root)"
/root
$ ksh -c "echo ~$(echo root)"
/root
$ zsh -c "echo ~$(echo root)"
/root

チルダ置換はコマンド、引数の先頭以外にも、変数代入の文脈で値をコロン区切りにした先頭部分でも行われる。

$ PATH=~root:~root
$ echo $PATH
/root:/root

しかし、どこが変数代入の文脈とみなされるかはbashとksh93, zshで異なるようだ。 ksh93とzshではコマンド前のA=Bやexportの文脈のみだが、bashではそれ以外でも変数代入の形をしていればチルダ置換をする。

$ bash -c 'echo PATH=~root:~root'
PATH=/root:/root
$ ksh -c 'echo PATH=~root:~root'
PATH=~root:~root
$ zsh -c 'echo PATH=~root:~root'
PATH=~root:~root

bashは上記のような無関係(?)な箇所でチルダ展開が起こることに注意しなければならない。 一方ksh93やzshでも PATH=... commandenv PATH=... command でチルダ展開の有無が異なることに注意しなければならない。 (前者の...の箇所では起こるが、後者の...の箇所では起こらない)

ここまでの例ではksh93とzshの動作は同じだったが、存在しないユーザーが指定された場合の動作はbash, ksh93とzshで異なる。 zshの場合はエラーとなり、ほかの2つではチルダがそのまま残される。

$ bash -c 'echo ~nosuchuser'
~nosuchuser
$ ksh -c 'echo ~nosuchuser'
~nosuchuser
$ zsh -c 'echo ~nosuchuser'
zsh:1: no such user or named directory: nosuchuser

もう一つ変なものを見つけてしまった。 チルダプレフィクス(チルダからスラッシュが来るまで、またはコマンドや引数が終わるまで)がチルダ単体の場合は自身の$HOMEで置換されるが、 bashとksh93ではコロンでもよい。zshはそうではない。

# bash -c 'echo ~:~'
/root:~
# ksh -c 'echo ~:~'
/root:~
# zsh -c 'echo ~:~'
~:~

初めて再帰モジュールが必要になった話 [OCaml]

入力ストリームの実装から独立したパーサーを定義したい。 そこでまずは入力ストリームのデータ型を定義する。

module type INSTREAM = sig
  type instream
  (* 本当はinstreamに対する色々な操作を含むつもり *)
end

実際の入力元はチャネルだったりメモリ上の文字列だったりする。

module ChanIns = struct
  type instream = in_channel
end

module StringIns = struct
  type instream = string
end

パーサーのシグニチャと実装はこんな感じになる。

module type PARSE = sig
  type instream
  type result
  val parse : instream -> result
end

module Parse(I: INSTREAM): PARSE with type instream = I.instream
  = struct
  type instream = I.instream
  type result = unit
  let parse ins = ()
end

module StringParse = Parse(StringIns)
module ChanParse = Parse(ChanIns)

ここでparse関数の中で、 「ストリームから読み込んだデータをいったん文字列にしてparse関数自身でパースする」 という処理がしたい。 文字列が変数sだとして、その内部のparse関数の呼び出しはどのように書けばよいか。

単にlet rec parse ins = ...としてparse (s : string)では駄目そうだ。 parseの型はinstream -> resultなのだがinstreamI.instreamであって、 stringであるとは限らない。

じゃあ StringParse.parse (s : string) では?というとこれもだめだ。 Parseの実装の中ではまだStringParseは定義されていない。 もちろんStringParseはParseに依存するのでParseより前に移動するわけにもいかない。

ということは…あ、再帰か。 ということで初めて実際に再帰モジュールというものが必要になる場面に出くわしたのだった。

結論から書くと、次のように書くことでコンパイルが通るようになる。

module Parse(I: INSTREAM)(S: PARSE with type instream = StringIns.instream)
  : PARSE with type instream = I.instream
  = struct
  type instream = I.instream
  type result = unit
  let parse ins = (ignore (S.parse ""); ())
end

module rec StringParse : PARSE with type instream = StringIns.instream =
        Parse(StringIns)(StringParse)
module ChanParse = Parse(ChanIns)(StringParse)

ファンクターは新しい引数Sをとる。 Sのモジュール型から、S.instreamはStringIns.instreamであるという想定がおけるので、 問題のparseの呼び出しはこのSに定義されたparseを呼ぶことでよくなる。

S.parseは結果的にはStringParse.parseを呼んでいることにしたい、 つまりS = StringParseであるということにしたいので、 ファンクターを適用するときに第2引数をStringParseにする必要がある。

これはChanParseのときは簡単な話で、普通に適用すればよい。 しかしStringParseを作るときは自分自身を使って自分自身を作るということになる。 これは再帰だ。ということでrecが付く。 再帰モジュール定義の場合はStringParseのモジュール型を明示する必要があるようだ。

後書き

実際にはSMLを書いていてこの問題に遭遇したのでこのように解決することはできませんでしたが、 そういえばOCamlには再帰モジュールって有ったと思い出して問題を翻訳しました。


シェルのコマンド置換の内部でのコメント [sh]

シェルのパーサーを書こうとしていていたのだけどマニュアルから読み取れないところはどうしても動かして実地調査するしかない。 シェルのコマンド置換の内部にコメントを書いて、そのコメントの中にコマンド置換の終端記号が来た場合、終端記号が勝つのかコメントが勝つのかという問題を調べた。

つまりこういうのを試す。

echo $(echo hello # comment)

echo $(echo hello
# comment)

echo `echo hello # comment`

echo `echo hello
comment`

結果

$ echo $(echo hello # comment)
> )
hello
$ echo $(echo hello
> # comment)
> )
hello
$ echo `echo hello # comment`
hello
$ echo `echo hello
> # comment`
hello

つまりダラーの場合はコメントのほうが勝って、バッククォートの場合はバッククォートのほうが勝つ。 bashでもksh93でもzshでも同様の動き。

めんどくさい… 忘れないようにメモしておく。


ブログをもう1つ始めた

ブログをもう1つ始めました。

wonderful cool something -- http://wcs.hatenablog.com/

使い分けはあまり考えていませんが、向こうではとりあえずProcessingで遊んだことなどを書き記していこうと思います。

SML の long identifier のドットについて [SML]

Standard MLの文法について調べていて気付いたこと。

SMLでは Int.toString みたいなドットで区切られた識別子のことを long identifier というんだけど、これは The Definition of Standard ML では longx ::= x | strid1.・・・.stridn.x というBNFで定義している(2.4 Identifiers)。 また、2.5 Lexical analysis では "Each item of lexical analysis is ... or a long identifier." と書いていて、long identifier が(syntacticなカテゴリではなく)lexicalなitemであるとしている。

そうするとこのドットの前後にホワイトスペースは許容されるのかという疑問が生じてくる。 通常の lexical analysis ではホワイトスペースをトークン中に含まない。とはいえそういうことができないわけではない。 一方でプログラミング言語一般的にはドットの前後で改行できるのが普通だと思う。

各種のSML実装で比較してみると、なんと!許容しないほうが多数派だった。

  • 許容しない: MLton, MLKit, Poly/ML, Moscow ML, Hamlet
  • 許容する: SML/NJ, SML#, Alice ML

検証ソース

$ cat longvid-split.sml
val _ = print (Int
.toString (Array.
maxLen))

実行結果

$ mlton longvid-split.sml
Error: longvid-split.sml 2.1.
  Illegal token.
Error: longvid-split.sml 2.17.
  Illegal token.
Error: longvid-split.sml 1.16.
  Undefined variable Int.
Error: longvid-split.sml 2.2.
  Undefined variable toString.
Error: longvid-split.sml 2.12.
  Undefined variable Array.
Error: longvid-split.sml 3.1.
  Undefined variable maxLen.
compilation aborted: parseAndElaborate reported errors
$ mlkit longvid-split.sml
[reading source file:   longvid-split.sml]
longvid-split.sml, line 2, column 2:
  .toString (Array.
    ^
cannot lex "."
[[ERR in sub process:
  PARSE_ELAB_ERROR]]
Stopping compilation of MLB-file due to error (code 1).
$ polyc longvid-split.sml
Error- in 'longvid-split.sml', line 2.
unknown symbol .t
Error- in 'longvid-split.sml', line 2.
invalid identifer - Array.
Exception- Fail "Static Errors" raised
$ sml
Standard ML of New Jersey v110.76 [built: Tue Oct 22 14:04:11 2013]
- use "longvid-split.sml";
[opening longvid-split.sml]
[autoloading]
[library $SMLNJ-BASIS/basis.cm is stable]
[autoloading done]
16777215val it = () : unit
$ mosml -P full
Moscow ML version 2.10
Enter `quit();' to quit.
- use "longvid-split.sml";
[opening file "longvid-split.sml"]
File "longvid-split.sml", line 2, characters 0-1:
! .toString (Array.
! ^
! Lexical error: ill-formed token.
[closing file "longvid-split.sml"]
$ alice
Alice 1.4 ("Kraftwerk 'Equaliser' Album") mastered 2013/11/08
### loaded signature from x-alice:/lib/system/Print
### loaded signature from x-alice:/lib/tools/Inspector
### loaded signature from x-alice:/lib/distribution/Remote
- use "longvid-split.sml";
val it : unit = ()
### evaluating file /home/ether/longvid-split.sml
16777199-
SML# 2.0.0 (2014-04-04 11:47:08 JST) for i686-unknown-linux-gnu with LLVM 3.4
# use "longvid-split.sml";
8388607#
$ ./hamlet
HaMLet 2.0.0 - To Be Or Not To Be Standard ML
[loading standard basis library]
- use "longvid-split.sml";
val it = () : unit
[processing /home/ether/longvid-split.sml]
../longvid-split.sml:2.0-2.1: invalid character `.'

ちなみにこの実験中に MLKit では Array.maxLen が 123456789 と定義されていることにも気づいてしまった。たぶん嘘だと思う。

$ cat longvid.sml
val _ = print (Int.toString (Array.maxLen))
$ mlkit longvid.sml
[wrote X86 code file:   MLB/RI_GC/base-link_objects.s]
[wrote executable file: run]
$ ./run
123456789

Proglr: SML用のGLRパーサージェネレーター [SML]

ちまちま作っていたSML用のパーサージェネレーターが結構形になってきたので紹介します。

https://github.com/tkob/proglr

先日の記事ではML-BNFCという名前で、パーサーはLR(0)の状態だった。当初のもくろみとしては一度SLR(1)にした後でBermudez and Logothetisの方法なるものを使ってLALR(1)にするということを考えていたんだけど、面倒に思えてきたのと、そのわりに得られる結果がLALR(1)で独自性がない気がしたので結局GLRにした。 そうするとこのパーサージェネレーターの独自性はどちらかというとGLRになるのでML-BNFCという名前もやめてML-GLRという名前にした。[追記参照] いまでは文法定義ファイルからSMLソースを生成するようになっていて、文法定義ファイルの解析自体もML-GLR自身が生成したものになっている。

[追記]: ML-GLRっていう名前のパーサージェネレーターが既にあった!http://www.cis.uni-muenchen.de/~leiss/relationaleGrammatik-09-10/ml-glr.pdf

ということでさらに名称変更してProglrという名前にした。 [追記終わり]

ビルド

git clone --recursive https://github.com/tkob/proglr
cd proglr
make -f Makefile.mlton

パターンマッチに関する警告がたくさん出ますが無視してください。 proglrという実行ファイルができます。 なお、MLtonのほかに一応MLKitとPoly/MLでもビルドできるようになっています。[追記]SML#2.0.0でもコンパイルできるようになりました。

使用例

文法定義は次のように書く。BNFCにおおむね似ている。

token Add "+" ;
token Sub "-" ;
token Mul "*" ;
token Div "/" ;
token LParen "(" ;
token RParen ")" ;
token Integer of int;

EAdd. Exp ::= Exp "+" Exp1 ;
_.    Exp ::= Exp1 ;
ESub. Exp ::= Exp "-" Exp1 ;
EMul. Exp1 ::= Exp1 "*" Exp2 ;
EDiv. Exp1 ::= Exp1 "/" Exp2 ;
_.    Exp1 ::= Exp2 ;
EInt. Exp2 ::= Integer ;
_.    Exp2 ::= "(" Exp ")" ;

この文法定義からは次のようなAST型が生成される。

  structure Ast = struct
    datatype exp =
      EAdd of Lex.span * exp * exp
    | ESub of Lex.span * exp * exp
    | EMul of Lex.span * exp * exp
    | EDiv of Lex.span * exp * exp
    | EInt of Lex.span * int
  end

スキャナーの定義はml-ulexを使う。

%defs (
  open Token
  type lex_result = Token.token
  val eof = fn () => Token.EOF
);

%name Lexer;

%let digit = [0-9];
%let space = [ \t\r\n];

<INITIAL> "+" => (Add);
<INITIAL> "-" => (Sub);
<INITIAL> "*" => (Mul);
<INITIAL> "/" => (Div);
<INITIAL> "(" => (LParen);
<INITIAL> ")" => (RParen);
<INITIAL> {digit}+ => (Integer (Option.valOf (Int.fromString (yytext))));
<INITIAL> {space}+ => (continue ());

ドライバとなるプログラムは次のような感じで書く。

structure Parse = ParseFun(Lexer)

open Parse.Ast

fun calc (EAdd (_, e1, e2)) = (calc e1) + (calc e2)
  | calc (ESub (_, e1, e2)) = (calc e1) - (calc e2)
  | calc (EMul  (_, e1, e2)) = (calc e1) * (calc e2)
  | calc (EDiv  (_, e1, e2)) = Int.div (calc e1, calc e2)
  | calc (EInt (_, e)) = e

fun main () =
  let
    val strm = Lexer.streamifyInstream TextIO.stdIn
    val sourcemap = AntlrStreamPos.mkSourcemap ()
    val ast = Parse.parse sourcemap strm
    val result = calc (hd ast)
  in
    print (Int.toString result);
    print "\n"
  end

val _ = main ()

ビルドするときはランタイムとしてsmlnj-libとmllpt-libをリンクする。

(* calc.mlb *)
$(SML_LIB)/basis/basis.mlb
$(SML_LIB)/smlnj-lib/smlnj-lib.mlb
$(SML_LIB)/mllpt-lib/mllpt-lib.mlb

calc-parse.sml
scan.ulex.sml
calc.sml

スキャナーとパーサーを生成するためのMakefile

mlglr: calc-parse.sml scan.ulex.sml
        mlton -output calc calc.mlb

calc-parse.sml: calc.cf
        proglr < calc.cf > calc-parse.sml

scan.ulex.sml: scan.ulex
        ml-ulex scan.ulex

clean:
        rm -f calc calc-parse.sml scan.ulex.sml

実行例

$ ./calc
(1 - 2) + 3 * 4 + 5
16

Generalized LRについて

構文解析について調べたりしながら思ったこと。

BNFCみたいに文法定義からASTのデータ型を自動生成するということを考えると、文法定義自体が「もともと表現したい構造」から離れていないほうがよい。BNFCのターゲットとなるパーサージェネレーターが全部LR系なのはそれなりに理由があることなんだろう。

ところでよく使われているLALR(1)では多義性のない文法に対してもconflictが生じることがあって、そういう場合はやっぱり文法のほうを変えなければならない。どんな文法に対してもきれいなASTデータ型を自動で出したければ理想的にはすべてのCFGを扱えるパーサーが望ましい。しかし文脈自由言語一般を扱えるパーサーはどれも最悪でO(n^3)の実行時間がかかってしまうそうだ。

Generalized LRもCFG一般を取り扱える手法だが、これはLR(0)やLALR(1)などの決定的なLR法に一手間加えて実現できる。普通の決定的なLR法ではconflictは起こってはいけない、あるいは起こったらどちらかを選ぶように決めておく。GLRではconflictが起きたら両方の選択肢をキープして構文解析を続ける。途中で選択肢の1つがエラーで死ぬかもしれないし、最終的に複数残るかもしれない。これは概念的に理解しやすい。

GLRは任意の文法に対してはO(n^(k+1)) (kは文法の最長の右辺)[1]だそうだけど、いま書いたことを考えるとconflictが起きなければO(n)になりそうじゃないか、という気がしてくる。その場合はベースとなるLR(0)やLALR(1)での解析と同じことしか起こっていないことになるわけだから。Wikipedia [2] にもそのようなことが書いてある。

ちょっとだけconflictのある文法はO(n)よりちょっとだけ遅くて、かなりconflictのある文法はかなり遅くなる、ということなら、プログラミング言語の構文解析も全部GLRでよくはないのだろうか。現実のプログラミング言語の文法はおおよそLALR(1)の範囲であるということが経験的にいえるのだし、そのうえでconflictが起こる少量のケースに関して決定的にするのかペナルティを受け入れて残すかの選択肢が設計者に残せるのだとしたら特に悪いことはなさそうだ。

でもプログラミング言語の処理系でGLRを採用して構文解析しているというのはあまり聞いたことがないような…そうだとしたらやっぱり何か使わない理由があるのだろうか。

[1] 文法をチョムスキー標準形にすると右辺は最大2にできるのでO(n^3)になるということだと思う。
[2] http://en.wikipedia.org/wiki/GLR_parser

SML用のLRパーサージェネレーターを作る [SML]

SMLのためのLRパーサージェネレーターを新しく自分で作っている。 まだ限定的なことしかできないしコードが汚い部分も残っているのだけど、公開された場所に置くことがモチベーションになるかもしれないと思ってGithubにアップロードした。

ML-BNFC: BNF Converter for Standard ML

SML処理系のためのパーサージェネレーターは各SML処理系に付属している場合が多いから、 新しくパーサージェネレーターを作るということ―車輪の再発明―を正当化するのはなかなか難しい。 私の場合は、自分で好きなように手を入れられるものが欲しいと思った、という程度ものだ。 でも新しく作るからには既存のものと少しは違う。 とりあえず作るにあたっての方針と、今後の目標を次に記そうと思う。

方針

  • ml-ulexと組み合わせて使える

SML/NJには歴史のあるml-yacc/ml-lexに加えて、ml-lptという言語処理系作成向けのツール群がある。 ml-ulexはml-lptに付属するスキャナージェネレーターである。 これはml-lexに比べると非常に進化していて、どうしてもこれを使いたかった。 もちろんml-lptを使えば使えるのだが、基本的にはml-antlrというLL(k)のパーサージェネレーターと組み合わせるしかなかった。

  • 構文木のデータ型を自動生成する

パーサージェネレーターには普通セマンティックアクションを付与した文法定義を与え、そのセマンティックアクションの中で構文木の生成を行うという形をとることが多い。 多いというか、パーサージェネレーターを使う殆どのケースでまずは構文木を作ると思う。 だとしたらパーサージェネレーターが構文木のデータ型も構文木を構築するコードも自動生成してくれればいい。 以前紹介したBNFCがそのような機能を提供していてとても便利だと思っていたのでそれを取り入れた。 また、ツールの名前もそこからとってML-BNFCとした。

  • 移植性

生成されるコードはできるだけ多くのSML処理系で動くようにする。

現状

現時点でコミットしてあるコードはブートストラップしていなくて、文法定義はSMLのデータとして直接与えて一緒にコンパイルするしかない。 ビルドするとmlbnfcというバイナリができ、ファイル名を与えて実行するとパーサーおよび構文木のデータ型のコードを出力する。 このコードはml-ulexで書いたスキャナーを組み合わせて使えるようになっていて、パースすると構文木が作られる。

今後の目標

  • 文法定義を外部ファイルから読み込むようにする
  • 雛形となるようなドライバのコードも自動生成するようにしたい
  • 現在LR(0)の文法しかサポートされていない。いずれLALR(1)まで持っていきたい
  • コードをきれいにする

[追記] この記事の続きはこちら http://rainyday.blog.so-net.ne.jp/2014-06-18


この広告は前回の更新から一定期間経過したブログに表示されています。更新すると自動で解除されます。