Lvc.IL.ILStateType

Require Import IL.

Inductive isReturn : stmt → Prop :=
| ReturnIsReturn e : isReturn (stmtReturn e).

Class ILStateType X :=
  {
    statetype :> StateType (X × onv val × stmt);
    step_let_op : ∀ L E x e b v (def:op_eval E e = Some v),
        step (L, E, stmtLet x (Operation e) b) EvtTau (L, E[x<-Some v], b);
    step_let_call : ∀ L E x f Y s vl v (def:omap (op_eval E) Y = Some vl),
        step (L, E, stmtLet x (Call f Y) s) (EvtExtern (ExternI f vl v)) (L, E[x <- Some v], s);
    let_op_normal : ∀ L E x e b (def:op_eval E e = None),
        normal2 step (L, E, stmtLet x (Operation e) b);
    let_call_normal : ∀ L E x f Y s (def:omap (op_eval E) Y = None),
        normal2 step (L, E, stmtLet x (Call f Y) s);
    let_call_inversion : ∀ L E x f Y s evt σ,
        step (L, E, stmtLet x (Call f Y) s) evt σ
        → ∃ vl v, omap (op_eval E) Y = Some vl
                ∧ evt = (EvtExtern (ExternI f vl v))
                ∧ σ = (L, E[x <- Some v], s);
    step_cond_true : ∀ L E e b1 b2 v
                  (def:op_eval E e = Some v) (condTrue: val2bool v = true),
        step (L, E, stmtIf e b1 b2) EvtTau (L, E, b1);
    step_cond_false : ∀ L E e b1 b2 v
                   (def:op_eval E e = Some v) (condFalse: val2bool v = false),
        step (L, E, stmtIf e b1 b2) EvtTau (L, E, b2);
    cond_normal : ∀ L E e b1 b2 (def:op_eval E e = None),
        normal2 step (L, E, stmtIf e b1 b2);
    result_none : ∀ L E s, ¬isReturn s → result (L, E, s) = None;
    result_return: ∀ L E e, result(L,E, stmtReturn e) = op_eval E e;
    return_normal: ∀ L E e, normal2 step (L,E, stmtReturn e)
  }.

Instance il_statetype_F : ILStateType F.labenv :=
  {
    statetype := statetype_F;
    step_let_op := F.StepLet;
    step_let_call := F.StepExtern;
    step_cond_true := F.StepIfT;
    step_cond_false := F.StepIfF
  }.
Proof.
  - intros. stuck2.
  - intros. stuck2.
  - intros; inv H; eauto.
  - intros. stuck2.
  - intros; simpl; eauto; destruct s; eauto; exfalso; eauto using isReturn.
  - reflexivity.
  - intros. stuck2.
Defined.

Instance il_statetype_I : ILStateType I.labenv :=
  {
    statetype := statetype_I;
    step_let_op := I.StepLet;
    step_let_call := I.StepExtern;
    step_cond_true := I.StepIfT;
    step_cond_false := I.StepIfF
  }.
Proof.
  - intros. stuck2.
  - intros. stuck2.
  - intros; inv H; eauto.
  - intros; stuck2.
  - intros; simpl; eauto; destruct s; eauto; exfalso; eauto using isReturn.
  - reflexivity.
  - intros. stuck2.
Defined.