include "Common.ma".

inductive expr : Type[0] :=
| Evar: option ident → expr
| Econst: nat → expr
| Eadd: expr → expr → expr
| Esub: expr → expr → expr.

inductive bool_expr : Type[0] :=
| Bequal: expr → expr → bool_expr
| Bless: expr → expr → bool_expr.

inductive cmd : Type[0] :=
| Cskip: cmd
| Cassign: ident → expr → cmd
| Cseq: cmd → cmd → cmd
| Cifthenelse: bool_expr → label → cmd → label → cmd → cmd
| Cwhile: bool_expr → label → cmd → label → cmd
| Cio: label → label → cmd
| Ccall: ident → fname → expr → option label → cmd
| Cret: expr → cmd.

let rec eval_expr (S: storeT) (s: S) (e: expr) on e : nat :=
 match e with
 [ Evar x ⇒ get S s x
 | Econst n ⇒ n
 | Eadd e1 e2 ⇒ eval_expr S s e1 + eval_expr S s e2
 | Esub e1 e2 ⇒ eval_expr S s e1 - eval_expr S s e2
 ].

definition eval_bool_expr: ∀S:storeT. ∀s:S. ∀b:bool_expr. bool ≝
 λS,s,b.
  match b with
  [ Bequal e1 e2 => eqb (eval_expr S s e1) (eval_expr S s e2)
  | Bless e1 e2 => ltb (eval_expr S s e1) (eval_expr S s e2)
  ].
  
definition continuation: Type[0] ≝ list cmd.

definition state: storeT → Type[0] ≝ λS.
 cmd × continuation × ((list (nat × ident × ((option label) × continuation))) × S).

definition fetchT ≝ fname → cmd.

inductive step (S: storeT) (fetch: fetchT) : state S → state S → list label → Prop :=
| step_assign: ∀x,e,k,K,s.
   step …
    〈Cassign x e, k, K, s〉
    〈Cskip, k, K, set … s (Some … x) (eval_expr … s e)〉
    []
| step_skip: ∀c,k,K,s.
   step …
    〈Cskip, c::k, K, s〉
    〈c,        k, K, s〉
    []
| step_seq: ∀c,c',k,K,s.
   step …
    〈Cseq c c',     k, K, s〉
    〈        c, c'::k, K, s〉
    []
| step_if_true:
   ∀b,l1,c1,l2,c2,k,K,s. eval_bool_expr ? s b = true →
    step …
     〈Cifthenelse b l1 c1 l2 c2, k, K, s〉
     〈                       c1, k, K, s〉
     [l1]
| step_if_false:
   ∀b,l1,c1,l2,c2,k,K,s. eval_bool_expr ? s b = false →
    step …
     〈Cifthenelse b l1 c1 l2 c2, k, K, s〉
     〈                       c2, k, K, s〉
     [l2]
| step_while_true: ∀b,l1,c,l2,k,K,s. eval_bool_expr ? s b = true →
   step …
    〈Cwhile b l1 c l2,                     k, K,s〉
    〈               c, (Cwhile b l1 c l2)::k, K, s〉
    [l1]
| step_while_false: ∀b,l1,c,l2,k,K,s. eval_bool_expr ? s b = false →
   step …
    〈Cwhile b l1 c l2, k, K, s〉
    〈           Cskip, k, K, s〉
    [l2]
| step_label: ∀l1,l2,k,K,s.
   step …
    〈Cio l1 l2, k, K, s〉
    〈    Cskip, k, K, s〉
    [l1;l2]
| step_call: ∀x,f,e,l,c,k,K,s. fetch f = c →
   step …
    〈Ccall x f e l,  k, K,                                                            s〉
    〈            c, [], 〈get ? s (None …),x,l,k〉::K, set ? s (None …) (eval_expr ? s e)〉
    [f]
| step_return: ∀e,k1,v,x,l,k2,K,s.
   step …
    〈Cret e, k1, 〈v,x,l,k2〉::K,                                                       s〉
    〈 Cskip, k2,             K, set ? (set ? s (Some … x) (eval_expr ? s e)) (None …) v〉
    (match l with [ None ⇒ [] | Some l ⇒ [l]]).

(*
definition steps: ∀S: storeT) : state S → state S → option label → Prop := star (trans_imp lbl).

Definition term_imp_lbl (lbl: Type) (c: cmd lbl) (s s': store) (trace: list lbl): Prop :=
        star_imp lbl (c, Chalt lbl, s) (Cskip lbl, Chalt lbl, s') trace.

Lemma induction_on_code_imp:
forall (P : code_imp -> Prop),
  P (Cskip False) ->
  (forall x e, P (Cassign False x e)) ->
  (forall S1 S2, P S1 -> P S2 -> P (Cseq False S1 S2)) ->
  (forall S1 S2 b, P S1 -> P S2 -> P (Cifthenelse False b S1 S2)) ->
  (forall S b, P S -> P (Cwhile False b S)) ->
  forall S : code_imp, P S.
Proof.
 unfold code_imp; intros.
 induction S as [ | | | | | Hfalse ]; auto.
 destruct Hfalse.
Qed.
*)