http://logic.cs.tsukuba.ac.jp/jikken/cam.html を見ながらざっと書いた CAM と計算例。あえてモナディック。

CAM.v

(* Categorical Abstract Machine *)
Set Implicit Arguments.
Unset Strict Implicit.
Set Contextual Implicit.
Require Import Arith.
Require Import List.
Import ListNotations.

(** * Monad *)
Class Monad :=
  {
    t:> Type -> Type;
    bind: forall {X Y: Type}, (X -> t Y) -> t X -> t Y;
    ret: forall {X: Type}, X -> t X
  }.
Notation "m >>= f" := (bind f m) (at level 55, left associativity).
Notation "x : T <- m ; p" := (m >>= (fun (x: T) => p)) (at level 65, T at next level, right associativity).
Notation "x <- m ; p" := (m >>= (fun x => p)) (at level 65, right associativity).
Notation "m >> p" := (m >>= (fun _ => p)) (at level 65, right associativity).
Coercion t: Monad >-> Funclass.

Class Fail (m: Monad):=
  {
    failure (X: Type): m X
  }.

Class St (S: Type)(m: Monad) :=
  {
    get: m S;
    put: S -> m unit
  }.
Definition modify {S: Type}{m: Monad}{ms: St S m}(f: S -> S): m unit :=
  get >>= (fun s => put (f s)).

Class StFail (S: Type)(m: Monad):=
  {
    sf_f:> Fail m;
    sf_s:> St S m
  }.

Fixpoint Nth {m: Monad}{mf: Fail m}(n: nat){A}(l: list A): m A :=
  match n, l with
    | O, x::_ => ret x
    | S n', _::xs => Nth n' xs
    | _, _ => failure
  end.


(** * CAM *)
Module CAM.

  Inductive val :=
  | Int (n: nat)
  | Bool (b: bool)
  | VClos (c: list instr)(e: list val)
  with instr :=
  | Ldi (n: nat)
  | Ldb (b: bool)
  | Access (n: nat)
  | IClos (c: list instr)
  | Apply
  | Return
  | ILet
  | ELet
  | ITest (c1 c2: list instr)
  | Add
  | Eq.

  Definition env := list val.
  Definition code := list instr.

  Definition stack := list val.

  Record State := make_State { stE: env; stS: stack}.
  Notation "[ e -- s ]" := (make_State e s).

  Definition spush (v: val)(st: State): State :=
    match st with
      | [ e -- s ] => [ e -- v::s ]
    end.

  Definition Trans {m: Monad}{mfs: StFail State m}(c: code): m code :=
    st: State <- get;
    match c, st with
      | Ldi n :: c, _ =>
        modify (spush (Int n)) >> ret c
      | Ldb b :: c, _ =>
        modify (spush (Bool b)) >> ret c
      | Access n :: c, _ =>
        v <- Nth n (stE st); modify (spush v) >> ret c
      | IClos c' :: c, _ =>
        modify (spush (VClos c' (stE st))) >> ret c
      | Apply :: c, [ e -- VClos c' e' :: v :: s ] =>
        put [ v:: VClos c' e' :: e' -- VClos c e :: s ] >> ret c'
      | Return :: c, [e -- v :: VClos c' e' :: s ] =>
        put [ e' -- v::s ] >> ret c'
      | ILet :: c, [ e -- v :: s ] =>
        put [ v :: e -- s ] >> ret c
      | ELet :: c, [ v :: e -- s ] =>
        put [ e -- s ] >> ret c
      | ITest c1 c2 :: c, [ e -- Bool b :: s ] =>
        put [ e -- s] >> ret ((if b then c1 else c2) ++ c)
      | Add :: c, [ e -- Int n1 :: Int n2 :: s ] =>
        put [e -- Int (n1 + n2) :: s ] >> ret c
      | Eq :: c, [ e -- Int n1 :: Int n2 :: s ] =>
        put [e -- Bool (beq_nat n1 n2) :: s ] >> ret c
      | _, _ => failure
    end.

  Fixpoint nApp {m: Monad}{mf: Fail m}(n: nat){A}(f: A -> m A)(a: A): m A :=
    match n with
      | O => ret a
      | S n' => f a >>= nApp n' f
    end.

  Fixpoint Evaluate {m: Monad}{mfs: StFail State m}(n: nat)(c: code): m val :=
    st: State <- get;
    match c, st, n with
      | [], [_ -- (v::_)], _ => ret v
      | _, _, S n' => Trans c >>= Evaluate n'
      | _, _, _ => failure
    end.

End CAM.
Import CAM.


(** * Instance *)
Definition State (X: Type) := CAM.State -> option (prod X CAM.State).
Definition Ret (X: Type)(x: X): State X :=
  fun st => Some (x, st).
Definition Bind {X Y: Type}(f: X -> State Y)(m: State X): State Y :=
  fun st => match m st with
              | Some (x, st') => f x st'
              | None => None
            end.

Instance mCAM: Monad :=
  {
    t := State;
    bind := @Bind;
    ret := @Ret
  }.

Instance mfCAM: Fail mCAM :=
  {
    failure X := fun (_: CAM.State) => @None (prod X CAM.State)
  }.

Instance msCAM: St CAM.State mCAM :=
  {
    get := fun st => Some (st,st);
    put s := fun _ => Some (tt,s)
  }.

Instance msfCAM: StFail CAM.State mCAM :=
  {
    sf_f := mfCAM;
    sf_s := msCAM
  }.

Example ex1: code :=
  [Ldi 4; Ldi 3; Ldi 2; Ldi 1; Add; Add; Add].

Compute nApp 3 Trans ex1 [ [] -- []].
     (* = Some ([Ldi 1; Add; Add; Add], [[] -- [Int 2; Int 3; Int 4]]) *)
     (* : option (code * CAM.State) *)

Compute nApp 7 Trans ex1 [ [] -- []].
     (* = Some ([], [[] -- [Int 10]]) *)
     (* : option (code * CAM.State) *)

Compute nApp 9 Trans ex1 [ [] -- []].
     (* = None *)
     (* : option (code * CAM.State) *)

Compute Evaluate 10 ex1 [ [] -- []].
     (* = Some (Int 10, [[] -- [Int 10]]) *)
     (* : option (val * CAM.State) *)