Lvc.ConstantPropagation
Require Import CSet Le.
Require Import Plus Util AllInRel Map.
Require Import CSet Val Var Env EnvTy IL Sim Fresh Annotation MoreExp Coherence LabelsDefined DecSolve.
Require Import RenamedApart Filter SetOperations Eqn ValueOpts Lattice.
Set Implicit Arguments.
Definition aval := withTop val.
Fixpoint exp_eval (E:onv aval) (e:exp) : aval :=
match e with
| Con v ⇒ wTA v
| Var x ⇒ match E x with
| Some v ⇒ v
| None ⇒ Top
end
| UnOp o e ⇒ match exp_eval E e with
| Top ⇒ Top
| wTA v ⇒ match Exp.unop_eval o v with
| Some v ⇒ wTA v
| None ⇒ Top
end
end
| BinOp o e1 e2 ⇒
match exp_eval E e1 with
| Top ⇒ Top
| wTA v1 ⇒
match exp_eval E e2 with
| Top ⇒ Top
| wTA v2 ⇒
match Exp.binop_eval o v1 v2 with
| Some v ⇒ wTA v
| None ⇒ Top
end
end
end
end.
Inductive le_precise : option aval → option aval → Prop :=
| leTop x : le_precise (Some Top) x
| leValVal y : le_precise (Some (wTA y)) (Some (wTA y))
| leBot : le_precise None None.
Instance le_precise_computable a b : Computable (le_precise a b).
Defined.
Inductive isEqCmp : exp → Prop :=
IisEqCmp x c : isEqCmp (BinOp 3 (Var x) (Con c)).
Instance isEqCmp_dec e : Computable (isEqCmp e).
Definition getEqCmpVar (e:exp) :=
match e with
| BinOp 3 (Var x) (Con c) ⇒ x
| _ ⇒ 0
end.
Definition getEqCmpCon (e:exp) :=
match e with
| BinOp 3 (Var x) (Con c) ⇒ c
| _ ⇒ 0
end.
Definition update_cond (AE:onv aval) (e:exp) (v:bool) :=
match v with
| false ⇒
if [ isVar e ] then
AE [getVar e <- Some (wTA 0)]
else
AE
| true ⇒
if [ isEqCmp e ] then
AE [getEqCmpVar e <- Some (wTA (getEqCmpCon e))]
else
AE
end.
Definition aval2bool (v:aval) :=
match v with
| wTA v ⇒ Some (val2bool v)
| Top ⇒ None
end.
Lemma oval2bool_some v b
: aval2bool v = Some b →
∃ v´, v = wTA v´ ∧ val2bool v´ = b.
Inductive cp_sound : onv aval
→ list (params×list (option aval))
→ stmt
→ Prop :=
| CPOpr AE (x:var) Cp b e
: cp_sound AE Cp b
→ Some (exp_eval AE e) = AE x
→ cp_sound AE Cp (stmtLet x e b)
| CPIf AE Cp e b1 b2
:
(aval2bool (exp_eval AE e) ≠ (Some false) → cp_sound (update_cond AE e true) Cp b1)
→ (aval2bool (exp_eval AE e) ≠ (Some true) → cp_sound (update_cond AE e false) Cp b2)
→ cp_sound AE Cp (stmtIf e b1 b2)
| CPGoto AE l Y Cp Z aY
: get Cp (counted l) (Z,aY)
→ length Z = length Y
→ PIR2 le_precise aY (List.map (exp_eval AE ∘ Some) Y)
→ cp_sound AE Cp (stmtApp l Y)
| CPReturn AE Cp e
: cp_sound AE Cp (stmtReturn e)
| CPLet AE Cp s Z b
: cp_sound AE ((Z,lookup_list AE Z)::Cp) s
→ cp_sound AE ((Z,lookup_list AE Z)::Cp) b
→ cp_sound AE Cp (stmtFun Z s b).
Instance cp_sound_dec AE ZL s : Computable (cp_sound AE ZL s).
Definition cp_eqn (E:onv aval) x :=
match E x with
| Some (wTA c) ⇒ singleton (EqnEq (Var x) (Con c))
| _ ⇒ ∅
end.
Definition cp_eqns (E:onv aval) (lv:set var) : eqns :=
fold union (map (cp_eqn E) lv) ∅.
Instance cp_eqns_morphism_equal E
: Proper (Equal ==> Equal) (cp_eqns E).
Instance cp_eqns_morphism_subset E
: Proper (Subset ==> Subset) (cp_eqns E).
Instance cp_eqns_morphism_flip_subset E
: Proper (flip Subset ==> flip Subset) (cp_eqns E).
Lemma cp_eqns_add E x lv
: cp_eqns E ({x; lv}) [=] cp_eqn E x ∪ cp_eqns E lv.
Lemma cp_eqns_union E lv lv´
: cp_eqns E (lv ∪ lv´) [=] cp_eqns E lv ∪ cp_eqns E lv´.
Lemma cp_eqn_agree lv E E´
: agree_on eq lv E E´
→ agree_on _eq lv (cp_eqn E) (cp_eqn E´).
Lemma cp_eqns_agree lv E E´
: agree_on eq lv E E´
→ cp_eqns E lv [=] cp_eqns E´ lv.
Inductive same_shape (A B:Type) : ann B → ann A → Prop :=
| SameShape0 a b
: same_shape (ann0 a) (ann0 b)
| SameShape1 a b an bn
: same_shape an bn
→ same_shape (ann1 a an) (ann1 b bn)
| SameShape2 a b an bn an´ bn´
: same_shape an bn
→ same_shape an´ bn´
→ same_shape (ann2 a an an´) (ann2 b bn bn´).
Fixpoint zip2Ann X Y Z (f:X→Y→Z) (a:ann X) (b:ann Y) z : ann Z :=
match a, b with
| ann1 a an, ann1 a´ an´ ⇒ ann1 (f a a´) (zip2Ann f an an´ z)
| ann2 a an1 an2, ann2 a´ an1´ an2´ ⇒ ann2 (f a a´)
(zip2Ann f an1 an1´ z)
(zip2Ann f an2 an2´ z)
| ann0 a, ann0 b ⇒ ann0 (f a b)
| _, _ ⇒ z
end.
Definition cp_eqns_ann (a:ann (onv aval)) (b:ann (set var)) : ann eqns :=
zip2Ann cp_eqns a b (ann0 ∅).
Definition cp_choose_exp E e :=
match exp_eval E e with
| wTA c ⇒ Con c
| _ ⇒ e
end.
Fixpoint constantPropagate (AE:onv aval) s : stmt :=
match s with
| stmtLet x e s ⇒
stmtLet x (cp_choose_exp AE e) (constantPropagate AE s)
| stmtIf e s t ⇒
stmtIf (cp_choose_exp AE e)
(constantPropagate (update_cond AE e true) s)
(constantPropagate (update_cond AE e false) t)
| stmtApp f Y ⇒
stmtApp f (List.map (cp_choose_exp AE) Y)
| stmtReturn e ⇒ stmtReturn (cp_choose_exp AE e)
| stmtExtern x f Y s ⇒
stmtExtern x f (List.map (cp_choose_exp AE) Y)
(constantPropagate AE s)
| stmtFun Z s t ⇒
stmtFun Z (constantPropagate AE s) (constantPropagate AE t)
end.
Lemma zip2Ann_get X Y Z (f:X→Y→Z) a b z
:
same_shape a b
→ getAnn (zip2Ann f a b z) = f (getAnn a) (getAnn b).
Lemma in_or_not X `{OrderedType X} x s
: { x ∈ s ∧ s [=] s \ {{x}} ∪ {{x}} }
+ { x ∉ s ∧ s [=] s \ {{x}} }.
Lemma in_cp_eqns AE x lv v
: x \In lv
→ AE x = ⎣wTA v ⎦
→ EqnEq (Var x) (Con v) ∈ cp_eqns AE lv.
Lemma cp_eqns_satisfies_env AE E x v lv
: x ∈ lv
→ AE x = ⎣wTA v ⎦
→ satisfiesAll E (cp_eqns AE lv)
→ E x = ⎣v ⎦.
Ltac smatch :=
match goal with
| [ H : match ?x with
_ ⇒ _
end = ?y,
H´ : ?x = _ |- _ ] ⇒ rewrite H´ in H; simpl in H
end.
Ltac dmatch :=
match goal with
| [ H : match ?x with
_ ⇒ _
end = ?y |- _ ] ⇒ case_eq x; intros
end.
Ltac imatch := dmatch; smatch; isabsurd.
Lemma exp_eval_same e lv AE E v
: Exp.freeVars e ⊆ lv
→ exp_eval AE e = wTA v
→ satisfiesAll E (cp_eqns AE lv)
→ ∃ v´, Exp.exp_eval E e = Some v´ ∧ option_eq eq ⎣v´ ⎦ ⎣v ⎦.
Lemma exp_eval_entails AE e v x lv
: Exp.freeVars e ⊆ lv
→ exp_eval AE e = wTA v
→ entails ({EqnEq (Var x) e ; { EqnEq (Var x) (cp_choose_exp AE e) ;
cp_eqns AE lv } }) (singleton (EqnEq (Var x) (Con v))).
Lemma cp_eqns_single AE x
: cp_eqns AE {{ x }} [=] cp_eqn AE x.
Lemma cp_choose_approx AE e lv
: Exp.freeVars e ⊆ lv
→ entails (cp_eqns AE lv) {EqnApx e (cp_choose_exp AE e)}.
Lemma cp_choose_approx_list AE Y lv
: list_union (List.map Exp.freeVars Y) ⊆ lv
→ entails (cp_eqns AE lv) (list_EqnApx Y (List.map (cp_choose_exp AE) Y)).
Lemma cp_choose_exp_freeVars AE e D
: Exp.freeVars e ⊆ D
→ Exp.freeVars (cp_choose_exp AE e) ⊆ D.
Lemma cp_choose_exp_live_sound_exp AE e lv
: Exp.freeVars e ⊆ lv
→ Exp.freeVars (cp_choose_exp AE e) ⊆ lv.
Lemma cp_choose_exp_eval_exp AE e v
: exp_eval AE e = wTA v
→ exp_eval AE (cp_choose_exp AE e) = wTA v.
Lemma subst_eqns_in gamma ϱ Gamma
: gamma \In subst_eqns ϱ Gamma
→ ∃ γ´, γ´ ∈ Gamma ∧ gamma = subst_eqn ϱ γ´.
Lemma cp_eqns_in gamma AE lv
: gamma \In cp_eqns AE lv
→ ∃ x, x ∈ lv ∧ gamma ∈ cp_eqn AE x.
Lemma lookup_list_get (AE:onv aval) Z n x z
: get (lookup_list AE Z) n x
→ get Z n z
→ x = AE z.
Lemma cp_eqns_freeVars AE lv
: eqns_freeVars (cp_eqns AE lv) ⊆ lv.
Lemma in_subst_eqns gamma Z Y AE
: length Z = length Y
→ gamma \In subst_eqns (sid [Z <-- Y]) (cp_eqns AE (of_list Z))
→ ∃ n x c,
gamma = subst_eqn (sid [Z <-- Y]) (EqnEq (Var x) (Con c))
∧ AE x = Some (wTA c)
∧ get Z n x
∧ get Y n ((sid [Z <-- Y]) x).
Lemma entails_cp_eqns_subst AE D Z Y
: length Z = length Y
→ PIR2 le_precise (lookup_list AE Z) (List.map (exp_eval AE ∘ Some) Y)
→ list_union (List.map Exp.freeVars Y)[<=]D
→ entails (cp_eqns AE D)
(subst_eqns (sid [Z <-- Y]) (cp_eqns AE (of_list Z))).
Lemma entails_cp_eqns_subst_choose AE AE´ D Z Y
: length Z = length Y
→ PIR2 le_precise (lookup_list AE´ Z) (List.map (exp_eval AE ∘ Some) Y)
→ list_union (List.map Exp.freeVars Y)[<=]D
→ entails (cp_eqns AE D)
(subst_eqns (sid [Z <-- List.map (cp_choose_exp AE) Y]) (cp_eqns AE´ (of_list Z))).
Lemma cp_eqns_update D x c AE
: x ∈ D
→ cp_eqns (AE [x <- ⎣ wTA c ⎦]) D [=] singleton (EqnEq (Var x) (Con c)) ∪ cp_eqns AE (D \ {{x}}).
Lemma cp_sound_eqn AE Cp Es s (ang:ann (set var × set var))
: let Gamma := (cp_eqns AE (fst (getAnn ang))) in
cp_sound AE Cp s
→ renamedApart s ang
→ labelsDefined s (length Es)
→ (∀ n a aY Z, get Es n a
→ get Cp n (Z,aY)
→ (∃ AE´, aY = lookup_list AE´ Z
∧ snd a [=] cp_eqns AE´ (of_list Z))
∧ (fst (fst (fst a))) = Z)
→ eqn_sound Es s (constantPropagate AE s) Gamma ang.
Require Import CMap.
Lemma cp_eqns_no_assumption d G
: (∀ x : var,
x \In G → MapInterface.find x d = ⎣⎦)
→ cp_eqns (fun x0 : var ⇒ MapInterface.find x0 d) G [=] ∅.
Require Import Plus Util AllInRel Map.
Require Import CSet Val Var Env EnvTy IL Sim Fresh Annotation MoreExp Coherence LabelsDefined DecSolve.
Require Import RenamedApart Filter SetOperations Eqn ValueOpts Lattice.
Set Implicit Arguments.
Definition aval := withTop val.
Fixpoint exp_eval (E:onv aval) (e:exp) : aval :=
match e with
| Con v ⇒ wTA v
| Var x ⇒ match E x with
| Some v ⇒ v
| None ⇒ Top
end
| UnOp o e ⇒ match exp_eval E e with
| Top ⇒ Top
| wTA v ⇒ match Exp.unop_eval o v with
| Some v ⇒ wTA v
| None ⇒ Top
end
end
| BinOp o e1 e2 ⇒
match exp_eval E e1 with
| Top ⇒ Top
| wTA v1 ⇒
match exp_eval E e2 with
| Top ⇒ Top
| wTA v2 ⇒
match Exp.binop_eval o v1 v2 with
| Some v ⇒ wTA v
| None ⇒ Top
end
end
end
end.
Inductive le_precise : option aval → option aval → Prop :=
| leTop x : le_precise (Some Top) x
| leValVal y : le_precise (Some (wTA y)) (Some (wTA y))
| leBot : le_precise None None.
Instance le_precise_computable a b : Computable (le_precise a b).
Defined.
Inductive isEqCmp : exp → Prop :=
IisEqCmp x c : isEqCmp (BinOp 3 (Var x) (Con c)).
Instance isEqCmp_dec e : Computable (isEqCmp e).
Definition getEqCmpVar (e:exp) :=
match e with
| BinOp 3 (Var x) (Con c) ⇒ x
| _ ⇒ 0
end.
Definition getEqCmpCon (e:exp) :=
match e with
| BinOp 3 (Var x) (Con c) ⇒ c
| _ ⇒ 0
end.
Definition update_cond (AE:onv aval) (e:exp) (v:bool) :=
match v with
| false ⇒
if [ isVar e ] then
AE [getVar e <- Some (wTA 0)]
else
AE
| true ⇒
if [ isEqCmp e ] then
AE [getEqCmpVar e <- Some (wTA (getEqCmpCon e))]
else
AE
end.
Definition aval2bool (v:aval) :=
match v with
| wTA v ⇒ Some (val2bool v)
| Top ⇒ None
end.
Lemma oval2bool_some v b
: aval2bool v = Some b →
∃ v´, v = wTA v´ ∧ val2bool v´ = b.
Inductive cp_sound : onv aval
→ list (params×list (option aval))
→ stmt
→ Prop :=
| CPOpr AE (x:var) Cp b e
: cp_sound AE Cp b
→ Some (exp_eval AE e) = AE x
→ cp_sound AE Cp (stmtLet x e b)
| CPIf AE Cp e b1 b2
:
(aval2bool (exp_eval AE e) ≠ (Some false) → cp_sound (update_cond AE e true) Cp b1)
→ (aval2bool (exp_eval AE e) ≠ (Some true) → cp_sound (update_cond AE e false) Cp b2)
→ cp_sound AE Cp (stmtIf e b1 b2)
| CPGoto AE l Y Cp Z aY
: get Cp (counted l) (Z,aY)
→ length Z = length Y
→ PIR2 le_precise aY (List.map (exp_eval AE ∘ Some) Y)
→ cp_sound AE Cp (stmtApp l Y)
| CPReturn AE Cp e
: cp_sound AE Cp (stmtReturn e)
| CPLet AE Cp s Z b
: cp_sound AE ((Z,lookup_list AE Z)::Cp) s
→ cp_sound AE ((Z,lookup_list AE Z)::Cp) b
→ cp_sound AE Cp (stmtFun Z s b).
Instance cp_sound_dec AE ZL s : Computable (cp_sound AE ZL s).
Definition cp_eqn (E:onv aval) x :=
match E x with
| Some (wTA c) ⇒ singleton (EqnEq (Var x) (Con c))
| _ ⇒ ∅
end.
Definition cp_eqns (E:onv aval) (lv:set var) : eqns :=
fold union (map (cp_eqn E) lv) ∅.
Instance cp_eqns_morphism_equal E
: Proper (Equal ==> Equal) (cp_eqns E).
Instance cp_eqns_morphism_subset E
: Proper (Subset ==> Subset) (cp_eqns E).
Instance cp_eqns_morphism_flip_subset E
: Proper (flip Subset ==> flip Subset) (cp_eqns E).
Lemma cp_eqns_add E x lv
: cp_eqns E ({x; lv}) [=] cp_eqn E x ∪ cp_eqns E lv.
Lemma cp_eqns_union E lv lv´
: cp_eqns E (lv ∪ lv´) [=] cp_eqns E lv ∪ cp_eqns E lv´.
Lemma cp_eqn_agree lv E E´
: agree_on eq lv E E´
→ agree_on _eq lv (cp_eqn E) (cp_eqn E´).
Lemma cp_eqns_agree lv E E´
: agree_on eq lv E E´
→ cp_eqns E lv [=] cp_eqns E´ lv.
Inductive same_shape (A B:Type) : ann B → ann A → Prop :=
| SameShape0 a b
: same_shape (ann0 a) (ann0 b)
| SameShape1 a b an bn
: same_shape an bn
→ same_shape (ann1 a an) (ann1 b bn)
| SameShape2 a b an bn an´ bn´
: same_shape an bn
→ same_shape an´ bn´
→ same_shape (ann2 a an an´) (ann2 b bn bn´).
Fixpoint zip2Ann X Y Z (f:X→Y→Z) (a:ann X) (b:ann Y) z : ann Z :=
match a, b with
| ann1 a an, ann1 a´ an´ ⇒ ann1 (f a a´) (zip2Ann f an an´ z)
| ann2 a an1 an2, ann2 a´ an1´ an2´ ⇒ ann2 (f a a´)
(zip2Ann f an1 an1´ z)
(zip2Ann f an2 an2´ z)
| ann0 a, ann0 b ⇒ ann0 (f a b)
| _, _ ⇒ z
end.
Definition cp_eqns_ann (a:ann (onv aval)) (b:ann (set var)) : ann eqns :=
zip2Ann cp_eqns a b (ann0 ∅).
Definition cp_choose_exp E e :=
match exp_eval E e with
| wTA c ⇒ Con c
| _ ⇒ e
end.
Fixpoint constantPropagate (AE:onv aval) s : stmt :=
match s with
| stmtLet x e s ⇒
stmtLet x (cp_choose_exp AE e) (constantPropagate AE s)
| stmtIf e s t ⇒
stmtIf (cp_choose_exp AE e)
(constantPropagate (update_cond AE e true) s)
(constantPropagate (update_cond AE e false) t)
| stmtApp f Y ⇒
stmtApp f (List.map (cp_choose_exp AE) Y)
| stmtReturn e ⇒ stmtReturn (cp_choose_exp AE e)
| stmtExtern x f Y s ⇒
stmtExtern x f (List.map (cp_choose_exp AE) Y)
(constantPropagate AE s)
| stmtFun Z s t ⇒
stmtFun Z (constantPropagate AE s) (constantPropagate AE t)
end.
Lemma zip2Ann_get X Y Z (f:X→Y→Z) a b z
:
same_shape a b
→ getAnn (zip2Ann f a b z) = f (getAnn a) (getAnn b).
Lemma in_or_not X `{OrderedType X} x s
: { x ∈ s ∧ s [=] s \ {{x}} ∪ {{x}} }
+ { x ∉ s ∧ s [=] s \ {{x}} }.
Lemma in_cp_eqns AE x lv v
: x \In lv
→ AE x = ⎣wTA v ⎦
→ EqnEq (Var x) (Con v) ∈ cp_eqns AE lv.
Lemma cp_eqns_satisfies_env AE E x v lv
: x ∈ lv
→ AE x = ⎣wTA v ⎦
→ satisfiesAll E (cp_eqns AE lv)
→ E x = ⎣v ⎦.
Ltac smatch :=
match goal with
| [ H : match ?x with
_ ⇒ _
end = ?y,
H´ : ?x = _ |- _ ] ⇒ rewrite H´ in H; simpl in H
end.
Ltac dmatch :=
match goal with
| [ H : match ?x with
_ ⇒ _
end = ?y |- _ ] ⇒ case_eq x; intros
end.
Ltac imatch := dmatch; smatch; isabsurd.
Lemma exp_eval_same e lv AE E v
: Exp.freeVars e ⊆ lv
→ exp_eval AE e = wTA v
→ satisfiesAll E (cp_eqns AE lv)
→ ∃ v´, Exp.exp_eval E e = Some v´ ∧ option_eq eq ⎣v´ ⎦ ⎣v ⎦.
Lemma exp_eval_entails AE e v x lv
: Exp.freeVars e ⊆ lv
→ exp_eval AE e = wTA v
→ entails ({EqnEq (Var x) e ; { EqnEq (Var x) (cp_choose_exp AE e) ;
cp_eqns AE lv } }) (singleton (EqnEq (Var x) (Con v))).
Lemma cp_eqns_single AE x
: cp_eqns AE {{ x }} [=] cp_eqn AE x.
Lemma cp_choose_approx AE e lv
: Exp.freeVars e ⊆ lv
→ entails (cp_eqns AE lv) {EqnApx e (cp_choose_exp AE e)}.
Lemma cp_choose_approx_list AE Y lv
: list_union (List.map Exp.freeVars Y) ⊆ lv
→ entails (cp_eqns AE lv) (list_EqnApx Y (List.map (cp_choose_exp AE) Y)).
Lemma cp_choose_exp_freeVars AE e D
: Exp.freeVars e ⊆ D
→ Exp.freeVars (cp_choose_exp AE e) ⊆ D.
Lemma cp_choose_exp_live_sound_exp AE e lv
: Exp.freeVars e ⊆ lv
→ Exp.freeVars (cp_choose_exp AE e) ⊆ lv.
Lemma cp_choose_exp_eval_exp AE e v
: exp_eval AE e = wTA v
→ exp_eval AE (cp_choose_exp AE e) = wTA v.
Lemma subst_eqns_in gamma ϱ Gamma
: gamma \In subst_eqns ϱ Gamma
→ ∃ γ´, γ´ ∈ Gamma ∧ gamma = subst_eqn ϱ γ´.
Lemma cp_eqns_in gamma AE lv
: gamma \In cp_eqns AE lv
→ ∃ x, x ∈ lv ∧ gamma ∈ cp_eqn AE x.
Lemma lookup_list_get (AE:onv aval) Z n x z
: get (lookup_list AE Z) n x
→ get Z n z
→ x = AE z.
Lemma cp_eqns_freeVars AE lv
: eqns_freeVars (cp_eqns AE lv) ⊆ lv.
Lemma in_subst_eqns gamma Z Y AE
: length Z = length Y
→ gamma \In subst_eqns (sid [Z <-- Y]) (cp_eqns AE (of_list Z))
→ ∃ n x c,
gamma = subst_eqn (sid [Z <-- Y]) (EqnEq (Var x) (Con c))
∧ AE x = Some (wTA c)
∧ get Z n x
∧ get Y n ((sid [Z <-- Y]) x).
Lemma entails_cp_eqns_subst AE D Z Y
: length Z = length Y
→ PIR2 le_precise (lookup_list AE Z) (List.map (exp_eval AE ∘ Some) Y)
→ list_union (List.map Exp.freeVars Y)[<=]D
→ entails (cp_eqns AE D)
(subst_eqns (sid [Z <-- Y]) (cp_eqns AE (of_list Z))).
Lemma entails_cp_eqns_subst_choose AE AE´ D Z Y
: length Z = length Y
→ PIR2 le_precise (lookup_list AE´ Z) (List.map (exp_eval AE ∘ Some) Y)
→ list_union (List.map Exp.freeVars Y)[<=]D
→ entails (cp_eqns AE D)
(subst_eqns (sid [Z <-- List.map (cp_choose_exp AE) Y]) (cp_eqns AE´ (of_list Z))).
Lemma cp_eqns_update D x c AE
: x ∈ D
→ cp_eqns (AE [x <- ⎣ wTA c ⎦]) D [=] singleton (EqnEq (Var x) (Con c)) ∪ cp_eqns AE (D \ {{x}}).
Lemma cp_sound_eqn AE Cp Es s (ang:ann (set var × set var))
: let Gamma := (cp_eqns AE (fst (getAnn ang))) in
cp_sound AE Cp s
→ renamedApart s ang
→ labelsDefined s (length Es)
→ (∀ n a aY Z, get Es n a
→ get Cp n (Z,aY)
→ (∃ AE´, aY = lookup_list AE´ Z
∧ snd a [=] cp_eqns AE´ (of_list Z))
∧ (fst (fst (fst a))) = Z)
→ eqn_sound Es s (constantPropagate AE s) Gamma ang.
Require Import CMap.
Lemma cp_eqns_no_assumption d G
: (∀ x : var,
x \In G → MapInterface.find x d = ⎣⎦)
→ cp_eqns (fun x0 : var ⇒ MapInterface.find x0 d) G [=] ∅.