(*****************************************)
(** SYNTAX *)
(*****************************************)
(** 基本データ構造を二分木構造で定める *)
Inductive DATA:Type :=
| DNIL : DATA
| DCONS : DATA -> DATA -> DATA.
Inductive VAR : Type :=
| X_IN : VAR (*入力用の変数*)
| X_OUT : VAR (*出力用の変数*)
| X : nat -> VAR.
Inductive EXPRESSION : Type :=
| V : VAR -> EXPRESSION
| D : DATA -> EXPRESSION
| CONS : EXPRESSION -> EXPRESSION -> EXPRESSION
| LEFT : EXPRESSION -> EXPRESSION
| RIGHT : EXPRESSION -> EXPRESSION
| ISEQ : EXPRESSION -> EXPRESSION -> EXPRESSION.
Inductive COMMAND : Type :=
| ASSIGN : VAR -> EXPRESSION -> COMMAND
| SEMI : COMMAND -> COMMAND -> COMMAND
| WHILE : EXPRESSION -> COMMAND -> COMMAND.
Inductive PROGRAM : Type :=
| MAIN : COMMAND -> PROGRAM.