「プログラミング言語の基礎概念」の演習問題を解くためのEmacs拡張を作ったので紹介します。
動機
関数型言語MLの一種Objective Camlを題材としてプログラミング言語の意味論，型システム，プログラミング言語の基礎概念，これらの概念間の数学的な関連を学ぶ．オンライン演習システムを用いて，「証明」を解答とする演習問題の正誤をWeb上で自動判定することもできる．
とあるとおり、この本にはオンライン演習システムが用意されていて、演習問題の採点をしてもらえます。
採点によって自分の理解度を確認できてとても便利なのですが、長い導出をエディタの補助なしに完成させるのは大変です。
なのでEmacsの
- major-mode
- Flycheck拡張
を作りました。
major-mode
シンタックスハイライトを実装しました。
一応、波括弧 {} のインデントに対応していますが実装は超手抜きです。
Flycheck拡張
Flycheckで導出が正しいかチェックできるようにしました。
導出のチェックは著者の五十嵐先生が公開されているcopl-toolsをdockerで動かしています。(igjit/docker-copl-tools)
所感
Emacsで割と快適に演習問題を解くことができるようになりました。
得られた知見:
CoPLの演習問題、詳細の導出は "?" で後回しにして幅優先で解いたほうが良さそう。
— igjit (@igjit) 2018年11月12日
深さ優先で導出すると最後の方で間違いに気付いたりする…… pic.twitter.com/D8lz8u8zkE