モナドを実行するインタープリタを書かないといけません。必要なのは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…

https://github.com/kik/ICFPC2011 インタープリタ ゲーム中に存在する全ての値を type value = | ValNum of int | ValI | ValSucc | ValDbl | ValGet | ValPut | ValS | ValSf of value | ValSfg of value * value | ValK | ValKx of value | ValInc | ValD…

例年のごとく一人で参加。時刻は全てUTCで 17日 00:00 問題が公開されたので読む。予想通り殴り合いゲーだ。 01:00 大体問題を理解したので、インタープリタを書き始めてみる。言語はOCamlを選択。というかこれ以外に選択肢がない 03:00 電車で会社に移動し…