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

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

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

セマンティクス

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