シンタクス

(*****************************************)
(** 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.