Lvc.EAE

Require Import CSet Le.
Require Import Plus Util AllInRel Map SetOperations.

Require Import Val EqDec Computable Var Env EnvTy IL Annotation.
Require Import Bisim Fresh Filter Filter MoreExp.

Set Implicit Arguments.

Function list_to_stmt (xl: list var) (Y : list exp) (s : stmt) : stmt :=
  match xl, Y with
    | x::xl, e :: Y ⇒ stmtLet x e (list_to_stmt xl Y s)
    | _, _ ⇒ s
  end.

Section MapUpdate.
  Open Scope fmap_scope.
  Variable X : Type.
  Context `{OrderedType X}.
  Variable Y : Type.

  Fixpoint update_with_list´ XL YL (m:X → Y) :=
    match XL, YL with
      | x::XL, y::YL ⇒ update_with_list´ XL YL (m[x <- y])
      | _, _ ⇒ m
    end.

  Lemma update_unique_commute (XL:list X) (VL:list Y) E D x y
  : length XL = length VL
    → unique (x::XL)
    → agree_on eq D (E [x <- y] [XL <-- VL]) (E [XL <-- VL] [x <- y]).

  Lemma update_with_list_agree´ (XL:list X) (VL:list Y) E D
  : length XL = length VL
    → unique XL
    → agree_on eq D (E [XL <-- VL]) (update_with_list´ XL VL E).
End MapUpdate.

Lemma list_to_stmt_correct L E s xl Y vl
: length xl = length Y
  → omap (exp_eval E) Y = Some vl
  → unique xl
  → of_list xl ∩ list_union (List.map Exp.freeVars Y) [=] ∅
  → star2 F.step (L, E, list_to_stmt xl Y s) nil (L, update_with_list´ xl (List.map Some vl) E, s).

Lemma list_to_stmt_crash L E s xl Y
: length xl = length Y
  → omap (exp_eval E) Y = None
  → unique xl
  → of_list xl ∩ list_union (List.map Exp.freeVars Y) [=] ∅
  → ∃ σ, star2 F.step (L, E, list_to_stmt xl Y s) nil σ ∧ state_result σ = None ∧ normal2 F.step σ.

Fixpoint compile s
  : stmt :=
  match s with
    | stmtLet x e s ⇒ stmtLet x e (compile s)
    | stmtIf x s t ⇒ stmtIf x (compile s) (compile t)
    | stmtApp l Y ⇒
      if [ ∀ n e, get Y n e → isVar e] then
        stmtApp l Y
      else
        let xl := fresh_list fresh (list_union (List.map Exp.freeVars Y)) (length Y) in
        list_to_stmt xl Y (stmtApp l (List.map Var xl))
    | stmtReturn x ⇒ stmtReturn x
    | stmtExtern x f Y s ⇒ stmtExtern x f Y (compile s)
    | stmtFun Z s t ⇒ stmtFun Z (compile s) (compile t)
  end.

Definition ArgRel (V V:onv val) (G:params) (VL VL´: list val) : Prop :=
  VL = VL´ ∧ length VL = length G.

Definition ParamRel (G:params) (Z Z´ : list var) : Prop :=
  Z = Z´ ∧ length Z = length G.

Instance SR : ProofRelation params := {
   ParamRel := ParamRel;
   ArgRel := ArgRel;
   BlockRel := fun lvZ b b´ ⇒ lvZ = F.block_Z b
}.
Defined.

Lemma omap_lookup_vars V xl vl
  : length xl = length vl
    → unique xl
    → omap (exp_eval (V[xl <-- List.map Some vl])) (List.map Var xl) = Some vl.

Lemma sim_EAE´ r L L´ V s PL
: simL´ bisim_progeq r SR PL L L´
→ bisim´r r (L, V, s) (L´,V, compile s).

Lemma sim_EAE V s
: @bisim _ statetype_F _ statetype_F (nil, V, s) (nil,V, compile s).