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