ソフトウェアの基礎 Imp_J.vの練習問題 stack_compiler

s_execute.v

(*
  スタック言語のプログラムを評価する関数
*)

Fixpoint s_execute (st : state) (stack : list nat)
                   (prog : list sinstr)
                 : list nat :=
  match (prog, stack) with
  | (nil, _) => stack
  | (SPush n :: prog', _) => s_execute st (n::stack) prog'
  | (SLoad X :: prog', _) => s_execute st (st X :: stack) prog'
  | (SPlus :: prog', n::m::stack') => s_execute st (m+n :: stack') prog'
  | (SMinus :: prog', n::m::stack') => s_execute st (m-n :: stack') prog'
  | (SMult :: prog', n::m::stack') => s_execute st (m*n :: stack') prog'
  | (_::prog', _) => s_execute st stack prog'
  end.

(* テストケース 1 *)
Example s_execute1 :
  s_execute empty_state [] [SPush 5, SPush 3, SPush 1, SMinus] = [2, 5].
Proof. reflexivity. Qed.

(* テストケース 2 *)
Example s_execute2 :
  s_execute (update empty_state X 3) [3,4] [SPush 4, SLoad X, SMult, SPlus] = [15, 4].
Proof. reflexivity. Qed.