以前紹介したように、AtomにIdris用パッケージをインストールするとキーボードショートカットで様々な機能を利用できます。
これがどのように実装されているのかが気になったので調べてみようと思い、Atomパッケージのソースコードを眺めてみました。
どうやらIdrisにはIDEモードというモードがあり、標準入出力を使用してS式でやり取りを行うIDE向けのプロトコルが存在するようです。ちょっと試してみました。
まずはIDEモードでプロセスを起動。
$ idris --ide-mode 000018(:protocol-version 1 0)
入出力は「メッセージの文字数を6桁の16進数にエンコードしたもの+S式のメッセージ」という形式で行われるようです。
こんな感じの作りかけのファイルを用意しておきます。
module Main main : IO ()
このファイルを読み込みます。メッセージにはユニークなカウンタを含める必要があるようです。
000022((:load-file "/tmp/hello.idr") 1)
出力はこんな感じ。
0000a9(:output (:ok (:highlight-source ((((:filename "/tmp/hello.idr") (:start 1 8) (:end 1 12)) ((:namespace "Main") (:decor :module) (:source-file "/tmp/hello.idr")))))) 1) 00001e(:set-prompt "*/tmp/hello" 1) 000015(:return (:ok ()) 1)
CTRL+ALT+A
相当の:add-clause
というメッセージを送信してみます。
00001B((:add-clause 3 "main") 2)
こんな感じで生成されたコードが返ってきます。
000025(:return (:ok "main = ?main_rhs") 2)
シンプルな手法ではありますが、Idris側でこのような機能を持っているので様々なエディタで同じ機能を簡単に実装できるようです。実際Atom以外にもvimやEmacs、Sublime Text用のプラグインなども用意されています。ショートカットは異なりますが、使い慣れたエディタを使用して型駆動開発を行うことができますね。