Lvc.CopyPropagation

Require Import CSet Le.

Require Import Plus Util AllInRel Map.
Require Import Val Var Env EnvTy IL Sim Coherence Fresh Annotation DecSolve SetOperations LabelsDefined.

Require Import Liveness Eqn ValueOpts RenamedApart.

Set Implicit Arguments.

Fixpoint copyPropagate (ϱ:var → var) (s:stmt) : stmt :=
  match s with
   | stmtLet x e s ⇒
     if [ isVar e] then
       stmtLet x e (copyPropagate (ϱ[x <- ϱ (getVar e)]) s)
     else
       stmtLet x (rename_exp ϱ e) (copyPropagate (ϱ[x <- x]) s)
   | stmtIf e s1 s2 ⇒ stmtIf (rename_exp ϱ e)
                             (copyPropagate ϱ s1)
                             (copyPropagate ϱ s2)
   | stmtApp l Y ⇒ stmtApp l (List.map (rename_exp ϱ) Y)
   | stmtReturn e ⇒ stmtReturn (rename_exp ϱ e)
   | stmtExtern x f Y s ⇒ stmtExtern x f (List.map (rename_exp ϱ) Y) (copyPropagate (ϱ[x <- x]) s)
   | stmtFun Z s1 s2 ⇒
     stmtFun Z (copyPropagate (ϱ[Z <-- Z]) s1) (copyPropagate ϱ s2)
   end.

Definition cp_eqn (ϱ:var → var) (x:var) := EqnApx (Var x) (Var (ϱ x)).

Lemma cp_moreDefined ϱ D e
  : Exp.freeVars e[<=]D
    → entails (map (cp_eqn ϱ) D) {EqnApx e (rename_exp ϱ e)}.

Lemma cp_moreDefinedArgs ϱ D Y
  : list_union (List.map Exp.freeVars Y) [<=]D
    → entails (map (cp_eqn ϱ) D) (list_EqnApx Y (List.map (rename_exp ϱ) Y)).

Lemma cp_eqns_agree_incl E E´ lv
: agree_on eq lv E E´
  → map (cp_eqn E) lv ⊆ map (cp_eqn E´) lv.

Lemma cp_eqns_agree E E´ lv
: agree_on eq lv E E´
  → map (cp_eqn E) lv [=] map (cp_eqn E´) lv.

Lemma cp_eqns_add_update ϱ D x y
: x ∉ D
  → map (cp_eqn (ϱ [x <- y])) ({x; D })
            [=] {EqnApx (Var x) (Var y); map (cp_eqn ϱ) D}.

Lemma cp_eqns_freeVars ϱ D
: lookup_set ϱ D ⊆ D
  → eqns_freeVars (map (cp_eqn ϱ) D) ⊆ D.

Lemma single_in_cp_eqns x ϱ D
: x ∈ D
  → {{ EqnApx (Var x) (Var (ϱ x)) }} ⊆ map (cp_eqn ϱ) D.

Lemma entails_cp_eqns_trivial ϱ Z
: entails {} (map (cp_eqn (ϱ [Z <-- Z])) (of_list Z)).

Lemma entails_eqns_trans´ Gamma e e´ e´´
: EqnEq e e´ ∈ Gamma
  → EqnApx e´ e´´ ∈ Gamma
  → entails Gamma {EqnApx e e´´}.

Lemma copyPropagate_sound_eqn s ang Es ϱ
: renamedApart s ang
  → lookup_set ϱ (fst (getAnn ang)) ⊆ (fst (getAnn ang))
  → labelsDefined s (length Es)
  → (∀ n a, get Es n a → snd a [=] ∅)
  → eqn_sound Es
              s (copyPropagate ϱ s)
              (map (cp_eqn ϱ) (fst (getAnn ang)))
              ang.