source: LTS/Imp.ma @ 3375

include "arithmetics/nat.ma".
include "basics/types.ma".
include "basics/lists/list.ma".

(*************************)

axiom ltb: nat → nat → bool.

(*************************)

record label: Type[0] ≝ {label_name: nat}.

record ident: Type[0] ≝ {ident_name: nat}.

record fname: Type[0] ≝ {function_name: nat}.

definition label_of_fname: fname → label ≝
 λf. mk_label (function_name f).
 
coercion label_of_fname.

record storeT: Type[1] ≝
 { store:> Type[0]
 ; get: store → option ident → nat
 ; set: store → option ident → nat → store
 ; get_set_hit: ∀s,x,v. get (set s x v) x = v
 ; get_set_miss: ∀s,x,y,v. get (set s x v) y = get s y
 }.

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
| Clabel: label → cmd → 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 (ident × (option label) × continuation)) × S).

definition fetchT ≝ fname → cmd.

inductive step (S: storeT) (fetch: fetchT) : state S → state S → option 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)〉
    (None …)
| step_skip: ∀c,k,K,s.
   step …
    〈Cskip, c::k, K, s〉
    〈c, k, K, s〉
    (None …)
| step_seq: ∀c,c',k,K,s.
   step …
    〈Cseq c c', k, K, s〉
    〈c, c'::k, K, s〉
    (None …)
| 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〉
     (Some … 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〉
     (Some … 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〉
    (Some … 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〉
    (Some … l2)
| step_label: ∀c,l,k,K,s.
   step …
    〈Clabel l c,k,K,s〉
    〈c,k,K,s〉
    (Some … l)
| step_call: ∀x,f,e,l,c,k,K,s. fetch f = c →
   step …
    〈Ccall x f e l, k, K, s〉
    〈c, [], 〈x,l,k〉::K, set ? s (None …) (eval_expr ? s e)〉
    (Some … f)
| step_return: ∀e,k1,x,l,k2,K,s.
   step …
    〈Cret e, k1, 〈x,l,k2〉::K, s〉
    〈Cskip, k2, K, set ? s (Some … x) (eval_expr ? s e)〉
    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.
*)