読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

シンタクス

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