セクション

Coqのセクションという機能を使うとグローバル変数みたいなのを使えます。

Section Hoge.
  Variable x : nat.

  Definition foo := x + 1.
  Definition bar := foo + 2.
  (* Section の中では x はグローバル変数みたいに使える *)
End Hoge.

(* Section を閉じると、foo と bar は x を引数にとるようになる *)
Definition baz := bar 42.

この機能とポインタを一緒に使うと変更できるグローバル変数みたいに使えます。

Section Foo.
  (* 最後にスロット8に置いた、ヒーラー。まだ置いてなければ None *)
  Variable heal_4095_at_8 : ptr (option value).

  (* スロットnにヒーラーが設置されている？ *)
  Definition check_healer n : aicmd bool :=
    v <- myfld n; (* 自分とこのスロットnを読む *)
    v' <- AiRead heal_4095_at_8; (* スロット8に置いたかどうか *)
    match v' with
    | Some v'' => ret (eqvalue v v'')
    | None => ret false
    end.

  Definition make_healer :=
    ifb check_healer 8
    then
      ret tt
    else
      arun 8 (...);; (* がんばってヒーラーを作る *)
      v <- myfld 8;; (* できあがった値を読み出す *)
      AiWrite heal_4095_at_8 (Some v). (* ポインタに覚えておく *)
End Foo.

みたいな感じ。これは未来のプログラム言語に違いない！

cmdexの中ではポインタの操作はできないので、ためしにcmdexを実行してうまくいくか試すなんてことができるはず。でも本当は複数のarunをグループ化してそれをしたいわけなので、ポインタ部分はaicmdから分離すべき。

今の実装は公理の中に

Axiom ptr : Type -> Type.
Axiom make_ptr  : forall {T}, T -> ptr T.
Axiom read_ptr  : forall {T}, ptr T -> T.
Axiom write_ptr : forall {T}, ptr T -> T -> unit.

が入っているので、実はどこからでも操作できたりする。これをちゃんとモナドの中に入れた公理にするのはTODO。