モナド

https://github.com/kik/ICFPC2011/blob/master/src/coq/Ltgmonad.v

二つのモナドを用意しました。cmdexモナドとaicmdモナドです。

cmdexモナドは一つのスロットで実行される命令列を作ります。

putl;; zeror;; succl;; dbll;; getl

こんな感じに書くと、左put右zero左succ左dbl左getを順に実行します。

ExStateの型はcmdex stateiで、現在の状態を返します。stateiにはプレイヤーと盤面と実行中のスロット番号が入っています。よって

Definition p (c : card) : cmdex unit :=
  let v := value_of_card c in
  s <- ExState;
  let v' = getf (sti_board s) (sti_player s) (sti_i s) in
  if eqvalue v v' then
    ret tt
  else 
    clear;; ExRight c   

みたいに書くことで、現在の状態を見て判定するようなスロットの初期化なんてのを書けたりするわけです。

aicmdモナドはAIを作ります。arunはスロット番号を指定してcmdexモナドを実行します。

  arun 0 (putl;; zeror;; succl;; dbll;; getl);;
  arun 1 (putl;; zoerr;; getl)

AiStateはaicmd state型でスロット番号がない以外はExStateと同じです。

STモナドの機能も実装しました。

AiNew : forall T, T -> aicmd (ptr T).
AiRead : forall T, ptr T -> aicmd T.
AiWrite : forall T, ptr T -> T -> aicmd unit.

AiNewでポインタを作成して、AiRead/AiWriteで読み書きします。