Isabelle Tutorial その8 - caeruiro3.3 Case Study: Compiling Expressions 今節では、変数、定数、そして二項演算子からなる式からスタックマシーンへのコンパイラを開発します。これは、2.5.6のブール式を一般化したものです。変数や値の型は特に定めず、型パラメータとして定義します。二項演算子も詳細は定めず、適当な演算子を持っているとします。 types 'v binop = "'v => 'v => 'v" datatype ('a, 'v) expr = Cex 'v | Vex 'a | Bex "'v binop" "('a, 'v) expr" "('a, 'v) expr" 三つの構成子は定数、変数、二項演算子の適用を表わします。式をある環境の下で評価する関数は次のように定義できます。 primrec "value" :: "('a, 'v) expr => ('a => 'v) =
