モナドを実行するインタープリタを書かないといけません。必要なのはaicmdを受け取って、次に実行するコマンドと残りのaicmdを返す関数です。OCaml側がその関数を順に呼び出します。とりあえずの実装なので、動くんだけど効率とかよくないし直したい。継続を…

Coqのセクションという機能を使うとグローバル変数みたいなのを使えます。 Section Hoge. Variable x : nat. Definition foo := x + 1. Definition bar := foo + 2. (* Section の中では x はグローバル変数みたいに使える *) End Hoge. (* Section を閉じる…

https://github.com/kik/ICFPC2011/blob/master/src/coq/Ltgmonad.v二つのモナドを用意しました。cmdexモナドとaicmdモナドです。cmdexモナドは一つのスロットで実行される命令列を作ります。 putl;; zeror;; succl;; dbll;; getlこんな感じに書くと、左put…

インタープリタ https://github.com/kik/ICFPC2011/blob/master/src/coq/Ltg.vここは急いで書いたのでバグがあるかもしれない。ただ、ここはデバッグするよりも証明したほうが早いと思う。 Inductive evalue : Set := | EValue : value -> evalue | EApp : e…