idris-mode for Vim/Emacs
最近巷で話題の Idris (依存型を持つ純粋関数型言語)ですが、この Idris にも vim と emacs のプラグインがあります。
idris-vim
vim の idris-mode です。Idris のメイン開発者である Edwin Brady さんも開発に加わっています。
※ 2013-11-1現在では Hackage にある idris-0.9.9.3 では動きません。 idris-0.9.10 を待つか、 idris の HEAD で試してください。
インストール
neobundle を使っている人は NeoBundle 'idris-hackers/idris-vim' で入ります。Vundle でも同じかんじで入ると思います。
確認していませんが、もしかすると syntastic と vimshell がないと正常に動かないかもしれません。
使い方
<leader> は Vim の leader-key というやつです。デフォルトでは \ です。
<leader>t- カーソル下にあるシンボルの型を表示
<leader>e- 入力された式を評価するプロンプトが表示される
<leader>r- カレントバッファの型チェックを行う
<leader>c- カーソルが場合分けを行う変数の上にあるときは、パターンが網羅されるように場合分けが展開される
<leader>w-
f x y z = ?rhsの形をしているとき、with-パターンを挿入する
-
<leader>d- カーソルがトップレベルにある関数の型シグネチャの上(
:の右側)にあるときは、関数の定義のフォーマットを挿入する
- カーソルがトップレベルにある関数の型シグネチャの上(
というキーバインドになっています。
以下のようにすると、(たぶん) vim が開くので、これで上のコマンドが使えるようになります。
% idris test.idr ____ __ _ / _/___/ /____(_)____ / // __ / ___/ / ___/ Version 0.9.9.3 _/ // /_/ / / / (__ ) http://www.idris-lang.org/ /___/\__,_/_/ /_/____/ Type :? for help Type checking test.idr *test> :e
なぜ一旦 idris の REPL を起動しないといけないかというと、 REPL を起動すると repl-server というのがポート4294で起動して、そこに向けてコマンド(idris --client :l <idris-file> など)を投げるという実装になっているからです。
正直 REPL を経由するのは面倒なのでしないでもよくなってほしいです。
[追記] https://github.com/amutake/idris-vim いちいち REPL を起動しなくてよくしてみました。 vimproc が必要です。vim 歴一週間くらいなのでこれでいいのかよくわかっていません。
vim-mode
emacs の idris-mode です。
インストール
el-get を使っている人は、公式のレシピの中に既に入っているので、(el-get 'sync 'idris-mode) でインストールできます。
それ以外の人は、ロードパスを通して(require 'idris-mode) をすると、*.idr ファイルを開いた時に自動的に idris-mode になります。
使い方
C-c C-l とタイプすると、そのファイルがロードされた Idris の REPL が開きます。ロードできなかったときはエラーの場所をハイライトしてくれます。
......のはずですが、CUI 版の emacs だと、エラーの場合はいいのですが REPL を開いてコマンドを打ったとき、応答がなくなってしまいます。
また、GUI 版の emacs だと、REPL からの応答はあるのですが、文字化けしているようになってしまいます(おそらく Idris の REPL は色を付けて表示する機能が付いているからだと思います)。
動いたらまた追記したいと思います。
まとめ
- idris も Vim/Emacs のモードがあるよ。
- idris-vim のほうが多機能。
- ちゃんと動かすのは難しいかもしれない。シンタックスハイライトとインデントをしてくれるだけでもいいなら。
- この idris-hackers というグループこわい。
