Emacs の why-mode のためのあれこれ
これは、Theorem Proving Advent Calendar の11日目の記事になります。
Why の Emacs 上での開発環境について紹介します。
ちっとも証明してないですが、凄い方々の凄い記事の間の箸休めということで一つ。
why-mode
tmiya さんによる3日目の記事で紹介されてた Why3 には、Emacs 向けの開発環境になるwhy.el が付属しています。Emacs の load-path が指しているディレクトリにこれを置き、
(require 'why-mode "why.el")
とすれば読み込めます。なお require の第二引数はオプションで、省略した場合には第一引数に .el を付けたファイル名を探すようです。
しかしこの why.el は、コメントを見るに2002年に作られたものらしく、現在の Why3 では使えない機能も一部あります。この記事では、why.el を前提に3つの拡張を提案します。
コメント
Emacs のデフォルトのキーバインドでは M-; でコメントの挿入ができます。ところが why-mode にはこのコメントとしてどんな記号を入力してやるかという設定がありません。
以下でコメントを認識させてやることができます。
(defun why-comment-setting () (make-local-variable 'comment-start) (setq comment-start "(* ") (make-local-variable 'comment-end) (setq comment-end " *)") (make-local-variable 'comment-multi-line) (setq comment-multi-line t) ) (add-hook 'why-mode-hook 'why-comment-setting)
なおせっかくの複数行コメントなのに、複数行の範囲をコメントアウトするときも一行づつコメントアウトされてしまいますが、仕様です :-)
flymake
Emacs の標準機能として、プログラムのエラー箇所を表示する flymake というものがあります。構文や型システムに慣れないうちは特に助かります。これを WhyML 向けに設定してやります。
flymake は処理系のエラーメッセージに対して、一つのエラーにつき一行のメッセージという仮定を置いています。一方 why3ml は複数行のエラーメッセージを出力することがあるため、そのままでは利用できません。
幸か不幸か、why3ml はエラーを発見したら直ちに停止するため、一度の変換で最大一つのエラーしか報告できません。そこで flymake がエラーメッセージを読み込む直前に一行に纏めてやります。
(defvar flymake-read-multiple-lines nil)
(make-variable-buffer-local 'flymake-read-multiple-lines)
(set-default 'flymake-read-multiple-lines nil)
(defun fold-lines (list)
(if list
(concat (car list) " " (fold-lines (cdr list)))
""))
(defadvice flymake-split-output (after flymake-output-split-multilines)
(when flymake-read-multiple-lines
(let ((lines (car ad-return-value))
(residual (cadr ad-return-value)))
(setq ad-return-value
(list (list (fold-lines lines))
residual)))))
(ad-activate 'flymake-split-output)flymake-read-multiple-lines を t にすると全てのエラーメッセージを一行に纏めるようになります。あとは why-mode でのこの変数の設定をしつつ他の言語と同じように設定してやります。
(defun flymake-why-init ()
(let* ((temp-file (flymake-init-create-temp-buffer-copy
'flymake-create-temp-inplace))
(local-file (file-relative-name
temp-file
(file-name-directory buffer-file-name))))
(list "why3ml" (append '("--type-only") (list local-file)))))
(defconst flymake-allowed-why-file-name-masks '("\\.mlw" flymake-why-init))
(defvar flymake-whyml-err-line-patterns '("^File \"\\(.+\\)\", line \\([0-9]+\\), characters \\([0-9]+-[0-9]+\\)\\(.*\\)" 1 2 3 4))
(defun flymake-whyml-start ()
(interactive)
(setq flymake-read-multiple-lines t)
(defadvice flymake-post-syntax-check (before flymake-force-check-was-interrupted)
(setq flymake-check-was-interrupted t))
(ad-activate 'flymake-post-syntax-check)
(add-to-list 'flymake-allowed-file-name-masks flymake-allowed-why-file-name-masks)
(add-to-list 'flymake-err-line-patterns flymake-whyml-err-line-patterns)
(flymake-mode t))
(add-hook 'why-mode-hook 'flymake-whyml-start) 図では Why3 付属のサンプルプログラムを変更し、 型エラーを起こさせています。赤くなっている行では int 型を引数に取る関数に int 型でない変数を適用しています。
またエラーメッセージが下部のミニバッファに表示されています。flymake でのエラーメッセージの表示方法はいくつか考案されていて、これはそのうちの一つです(標準の表示方法である flymake-display-err-menu-for-current-line はエラー箇所が見えなくなることがあるので、今回は使いませんでした)。
compile
端末に戻らず、Emacs から証明器を動かした方が便利な場合もあるかと思います。
compile コマンドは、外部コマンドを非同期に実行してくれます。
私は smart-compile を利用して、以下のように設定しています。
(add-to-list 'smart-compile-alist
'("\\.mlw$" . "why3ml -P alt-ergo %f --timelimit 1")) 図は Why3 付属のサンプルプログラムを実行してみたものです。ファイル中の命題をそれぞれ証明した結果が出力されています。証明結果については色を付けられると良さそうですね。
