Lvc.Coherence.Delocation

Require Import AllInRel Util Map Env EnvTy Exp IL Annotation Coherence Bisim DecSolve Liveness Restrict MoreExp.


Set Implicit Arguments.

Inductive trs
  : list (option (set var))

    → list (params)

    → stmt

    → ann (set var)

    → ann (list var)

    → Prop :=
 | trsExp DL ZL x e s an an_lv lv
    : trs (restrict DL (lv\{{x}})) ZL s an_lv an
    → trs DL ZL (stmtLet x e s) (ann1 lv an_lv) (ann1 nil an)
  | trsIf DL ZL e s t ans ant ans_lv ant_lv lv
    : trs DL ZL s ans_lv ans
    → trs DL ZL t ant_lv ant
    → trs DL ZL (stmtIf e s t) (ann2 lv ans_lv ant_lv) (ann2 nil ans ant)
  | trsRet e DL ZL lv
    : trs DL ZL (stmtReturn e) (ann0 lv) (ann0 nil)
  | trsGoto DL ZL G´ f Za Y lv
    : get DL (counted f) (Some G´)
    → get ZL (counted f) (Za)


    → trs DL ZL (stmtApp f Y) (ann0 lv) (ann0 nil)
  | trsExtern DL ZL x f Y s lv an_lv an
    : trs (restrict DL (lv\{{x}})) ZL s an_lv an
    → trs DL ZL (stmtExtern x f Y s) (ann1 lv an_lv) (ann1 nil an)
  | trsLet DL ZL s t Z Za ans ant lv ans_lv ant_lv
    :
      
      trs (restrict (Some (getAnn ans_lv \ of_list (Z++Za))::DL) (getAnn ans_lv \ of_list (Z++Za))) (Za::ZL) s ans_lv ans
    → trs (Some (getAnn ans_lv \ of_list (Z++Za))::DL) (Za::ZL) t ant_lv ant
    → trs DL ZL (stmtFun Z s t) (ann2 lv ans_lv ant_lv) (ann2 Za ans ant).

Lemma trs_annotation DL ZL s lv Y
      : trs DL ZL s lv Y → annotation s lv ∧ annotation s Y.

Fixpoint compile (ZL:list (list var)) (s:stmt) (an:ann (list var)) : stmt :=
  match s, an with
    | stmtLet x e s, ann1 _ an ⇒ stmtLet x e (compile ZL s an)
    | stmtIf e s t, ann2 _ ans ant ⇒ stmtIf e (compile ZL s ans) (compile ZL t ant)
    | stmtApp f Y, ann0 _ ⇒ stmtApp f (Y++List.map Var (nth (counted f) ZL nil))
    | stmtReturn e, ann0 _ ⇒ stmtReturn e
    | stmtExtern x f Y s, ann1 _ an ⇒
      stmtExtern x f Y (compile ZL s an)
    | stmtFun Z s t, ann2 Za ans ant ⇒
      stmtFun (Z++Za) (compile (Za::ZL) s ans) (compile (Za::ZL) t ant)
    | s, _ ⇒ s
  end.

Inductive approx
  : list (set var × list var)
    → list (option (set var))
    → list (params) → I.block → I.block → Prop :=
  blk_approxI o (Za Z´:list var) DL ZL Lv s ans ans_lv ans_lv´
              (RD:∀ G, o = Some G →
                       live_sound Imperative ((getAnn ans_lv´,Z´++Za)::Lv) (compile (Za :: ZL) s ans) ans_lv´
                       ∧ trs (restrict (Some G::DL) G) (Za::ZL) s ans_lv ans)
  : approx ((getAnn ans_lv´,Z´++Za)::Lv) (o::DL) (Za::ZL) (I.blockI Z´ s) (I.blockI (Z´++Za) (compile (Za::ZL) s ans)).

Lemma approx_restrict Lv DL ZL L L´ G
: AIR53 approx Lv DL ZL L L´
  → AIR53 approx Lv (restrict DL G) ZL L L´.

Definition appsnd {X} {Y} (s:X × list Y) (t: list Y) := (fst s, snd s ++ t).

Definition defined_on {X} `{OrderedType X} {Y} (G:set X) (E:X → option Y)
  := ∀ x, x ∈ G → ∃ y, E x = Some y.

Lemma defined_on_update_some X `{OrderedType X} Y (G:set X) (E:X → option Y) x v
  : defined_on (G \ {{x}}) E
    → defined_on G (E [x <- Some v]).

Lemma defined_on_incl X `{OrderedType X} Y (G G´:set X) (E:X → option Y)
  : defined_on G E
    → G´ ⊆ G
    → defined_on G´ E.

Inductive trsR : I.state → I.state → Prop :=
  trsRI (E E´:onv val) L L´ s ans Lv´ ans_lv ans_lv´ DL ZL
  (RD: trs DL ZL s ans_lv ans)
  (EA: AIR53 approx Lv´ DL ZL L L´)
  (EQ: (@feq _ _ eq) E E´)
  (LV´: live_sound Imperative Lv´ (compile ZL s ans) ans_lv´)
  (EDEF: defined_on (getAnn ans_lv´) E´)
  : trsR (L, E, s) (L´, E´, compile ZL s ans).

Lemma omap_var_defined_on Za lv E
: of_list Za ⊆ lv
  → defined_on lv E
  → ∃ l, omap (exp_eval E) (List.map Var Za) = Some l.

Lemma defined_on_update_list lv (E:onv val) Z vl
: length vl = length Z
  → defined_on (lv \ of_list Z) E
  → defined_on lv (E [Z <-- List.map Some vl]).

Lemma trsR_sim σ1 σ2
  : trsR σ1 σ2 → bisim σ1 σ2.

Lemma trs_srd AL ZL s ans_lv ans
  (RD:trs AL ZL s ans_lv ans)
  : srd AL (compile ZL s ans) ans_lv.

Inductive additionalParameters_live : list (set var)
                                      → stmt
                                      → ann (set var)
                                      → ann (list var)
                                      → Prop :=
| additionalParameters_liveExp ZL x e s an an_lv lv
  : additionalParameters_live ZL s an_lv an
    → additionalParameters_live ZL (stmtLet x e s) (ann1 lv an_lv) (ann1 nil an)
| additionalParameters_liveIf ZL e s t ans ant ans_lv ant_lv lv
  : additionalParameters_live ZL s ans_lv ans
    → additionalParameters_live ZL t ant_lv ant
    → additionalParameters_live ZL (stmtIf e s t) (ann2 lv ans_lv ant_lv) (ann2 nil ans ant)
| additionalParameters_liveRet ZL e lv
    : additionalParameters_live ZL (stmtReturn e) (ann0 lv) (ann0 nil)
| additionalParameters_liveGoto ZL Za f Y lv
  : get ZL (counted f) Za
    → Za ⊆ lv
    → additionalParameters_live ZL (stmtApp f Y) (ann0 lv) (ann0 nil)
| additionalParameters_liveExtern ZL x f Y s an an_lv lv
  : additionalParameters_live ZL s an_lv an
    → additionalParameters_live ZL
                                (stmtExtern x f Y s)
                                (ann1 lv an_lv)
                                (ann1 nil an)
| additionalParameters_liveLet ZL s t Z Za ans ant lv ans_lv ant_lv
  : of_list Za ⊆ getAnn ans_lv \ of_list Z
    → additionalParameters_live (of_list Za::ZL) s ans_lv ans
    → additionalParameters_live (of_list Za::ZL) t ant_lv ant
    → additionalParameters_live ZL (stmtFun Z s t) (ann2 lv ans_lv ant_lv) (ann2 Za ans ant).

Lemma live_sound_compile DL ZL AL s ans_lv ans o
  (RD:trs AL ZL s ans_lv ans)
  (LV:live_sound o DL s ans_lv)
  (APL: additionalParameters_live (List.map of_list ZL) s ans_lv ans)
  : live_sound o (zip (fun s t ⇒ (fst s, snd s ++ t)) DL ZL) (compile ZL s ans) ans_lv.