Coqでつくる手続き型プログラミング言語
とってもシンプルな言語をCoq内で定義してみた。
次のような感じでプログラムは表現される。
(* プログラムの例 入力された2数を足し算するプログラム *) Definition plus_program := MAIN ( X O <- LEFT (!X_IN); (*変数X_INの左値を変数X0に代入*) X_OUT <- RIGHT (!X_IN); (*変数X_INの右値を変数X_OUTに代入*) WHILE (!X O) ( (*変数X0がnilになるまでループ*) X_OUT <- CONS (D DNIL) (!X_OUT); (*X_OUTに(nil, X_OUTの値)を代入*) X O <- RIGHT (!X O) (*X0にX0の右値を代入*) ) ).
詳細は以下
シンタクス
(*****************************************) (** 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.
セマンティクス
(*****************************************) (** SEMANTICS *) (*****************************************) Require Import List. Section ListAssoc. Variable A B:Set. Variable A_beq : A -> A -> bool. Fixpoint List_assoc (l:list (A*B))(a:A){struct l} := match l with | List.nil => None | List.cons (l_hd_left,l_hd_right) l_tl => if A_beq l_hd_left a then Some l_hd_right else List_assoc l_tl a end. End ListAssoc. Definition store:Type := list (VAR * DATA). Fixpoint nat_beq (m n:nat) {struct m} : bool := match m, n with | O, O => true | S m', S n' => nat_beq m' n' | _, _ => false end. Definition VAR_beq (v1 v2:VAR) : bool := match v1, v2 with | X_IN, X_IN => true | X_OUT, X_OUT => true | X m, X n => nat_beq m n | _, _ => false end. Fixpoint DATA_beq (d1 d2:DATA){struct d1} : bool := match d1, d2 with | DNIL, DNIL => true | DCONS hd1 tl1, DCONS hd2 tl2 => match DATA_beq hd1 hd2, DATA_beq tl1 tl2 with | true, true => true | _, _ => false end | _, _ => false end. (* var -> store -> option DATA *) Definition eval_VAR (v:VAR) (s:store) := List_assoc VAR DATA VAR_beq s v. Definition try_DCONS (d_opt1 d_opt2:option DATA) := match d_opt1, d_opt2 with | Some d1, Some d2 => Some (DCONS d1 d2) | _,_ => None end. Fixpoint eval_DATA_EQ_aux (d1 d2:DATA) {struct d1} := match d1, d2 with | DCONS hd1 tl1, DCONS hd2 tl2 => match eval_DATA_EQ_aux hd1 hd2, eval_DATA_EQ_aux tl1 tl2 with | true, true => true | _,_ => false end | DCONS _ _, DNIL => false | DNIL, DCONS _ _ => false | DNIL, DNIL => true end. (* DATA -> DATA -> option bool *) Definition eval_DATA_EQ d_opt1 d_opt2 := match d_opt1, d_opt2 with | Some d1, Some d2 => Some (eval_DATA_EQ_aux d1 d2) | _,_ => None end. (* EXPRESSION -> store -> option DATA *) Fixpoint eval_EXPR (e:EXPRESSION) := (fun s:store => match e with | V v => eval_VAR v s | D d => Some d | CONS E F => try_DCONS (eval_EXPR E s)(eval_EXPR F s) | LEFT E => match eval_EXPR E s with | Some (DCONS head _) => Some head | Some _ => Some DNIL | None => None end | RIGHT E => match eval_EXPR E s with | Some (DCONS _ tail) => Some tail | Some _ => Some DNIL | None => None end | ISEQ E F => match eval_DATA_EQ (eval_EXPR E s) (eval_EXPR F s) with | Some true => Some (DCONS DNIL DNIL) | Some false => Some DNIL | None => None end end). Fixpoint do_1CMD (C:COMMAND)(s:store) : option (option COMMAND * store) := match C with | ASSIGN v E => match eval_EXPR E s with | Some d => Some (None, List.cons (v,d) s) | None => None end | SEMI C1 C2 => match do_1CMD C1 s with | Some (Some C1', s') => Some (Some (SEMI C1' C2), s') | Some (None, s') => Some (Some C2, s') | None => None end | WHILE E C' => match eval_EXPR E s with | Some DNIL => Some (None, s) | Some _ => match do_1CMD C' s with | Some (Some C'', s') => Some (Some (SEMI C'' (WHILE E C')), s') | Some (None, s') => Some (Some (WHILE E C'), s') | None => None end | None => None end end. Fixpoint do_CMD (count:nat)(c:COMMAND)(s:store){struct count} : option store := match count with | O => None | S count' => match do_1CMD c s with | Some (Some c', s') => do_CMD count' c' s' | Some (None, s') => Some s' | None => None end end. Definition COUNT_MAX := 100. Definition eval (p:PROGRAM)(input:DATA) : option DATA := match p with | MAIN cmds => match do_CMD COUNT_MAX cmds ((X_IN, input)::nil) with | Some s' => eval_EXPR (!X_OUT) s' | None => None end end. Definition eval_debug (p:PROGRAM)(input:DATA) : option (store * option DATA) := match p with | MAIN cmds => match do_CMD COUNT_MAX cmds ((X_IN, input)::nil) with | Some s => Some (s, eval_EXPR (!X_OUT) s) | None => None end end.