Lvc.DVE
Require Import CSet Le.
Require Import Plus Util AllInRel Map.
Require Import Val EqDec Computable Var Env EnvTy IL Annotation.
Require Import Sim Fresh Filter Liveness TrueLiveness Filter MoreExp.
Set Implicit Arguments.
Fixpoint compile (LV:list (set var × params)) (s:stmt) (a:ann (set var)) :=
match s, a with
| stmtLet x e s, ann1 lv an ⇒
if [x ∈ getAnn an] then stmtLet x e (compile LV s an)
else compile LV s an
| stmtIf e s t, ann2 _ ans ant ⇒
if [exp2bool e = Some true] then
(compile LV s ans)
else if [ exp2bool e = Some false ] then
(compile LV t ant)
else
stmtIf e (compile LV s ans) (compile LV t ant)
| stmtApp f Y, ann0 lv ⇒
let lvZ := nth (counted f) LV (∅,nil) in
stmtApp f (filter_by (fun y ⇒ B[y ∈ fst lvZ]) (snd lvZ) Y)
| stmtReturn x, ann0 _ ⇒ stmtReturn x
| stmtExtern x f e s, ann1 lv an ⇒
stmtExtern x f e (compile LV s an)
| stmtFun Z s t, ann2 lv ans ant ⇒
let LV´ := (getAnn ans,Z)::LV in
stmtFun (List.filter (fun x ⇒ B[x ∈ getAnn ans]) Z)
(compile LV´ s ans) (compile LV´ t ant)
| s, _ ⇒ s
end.
Definition ArgRel (V V:onv val) (G:(set var × params)) (VL VL´: list val) : Prop :=
VL´ = (filter_by (fun x ⇒ B[x ∈ (fst G)]) (snd G) VL) ∧
length (snd G) = length VL.
Definition ParamRel (G:(set var × params)) (Z Z´ : list var) : Prop :=
Z´ = (List.filter (fun x ⇒ B[x ∈ (fst G)]) Z) ∧ snd G = Z.
Instance SR : ProofRelation (set var × params) := {
ParamRel := ParamRel;
ArgRel := ArgRel;
BlockRel := fun lvZ b b´ ⇒ True
}.
Defined.
Lemma agree_on_update_filter X `{OrderedType X} Y `{Equivalence (option Y)}
(lv:set X) (V: X → option Y) Z VL
: length Z = length VL
→ agree_on R lv
(V [Z <-- List.map Some VL])
(V [List.filter (fun x ⇒ B[x ∈ lv]) Z <--
List.map Some (filter_by (fun x ⇒ B[x ∈ lv]) Z VL)]).
Lemma agree_on_update_filter´ X `{OrderedType X} Y `{Equivalence (option Y)} (lv:set X) (V V´:X → option Y) Z VL
: length Z = length VL
→ agree_on R (lv \ of_list Z) V V´
→ agree_on R lv
(V [Z <-- List.map Some VL])
(V´ [(List.filter (fun x ⇒ B[x ∈ lv]) Z) <-- (List.map Some
(filter_by (fun x ⇒ B[x ∈ lv]) Z VL))]).
Lemma sim_DVE´ r L L´ V V´ s LV lv
: agree_on eq (getAnn lv) V V´
→ true_live_sound Functional LV s lv
→ simL´ sim_progeq r SR LV L L´
→ sim´r r (L,V, s) (L´,V´, compile LV s lv).
Lemma sim_DVE V V´ s lv
: agree_on eq (getAnn lv) V V´
→ true_live_sound Functional nil s lv
→ @sim F.state _ F.state _ (nil,V, s) (nil,V´, compile nil s lv).
Module I.
Import Sim.I.
Definition ArgRel (V V´:onv val) (G:(set var × params)) (VL VL´: list val) : Prop :=
VL´ = (filter_by (fun x ⇒ B[x ∈ (fst G)]) (snd G) VL) ∧
length (snd G) = length VL ∧
agree_on eq (fst G \ of_list (snd G)) V V´.
Definition ParamRel (G:(set var × params)) (Z Z´ : list var) : Prop :=
Z´ = (List.filter (fun x ⇒ B[x ∈ (fst G)]) Z) ∧ snd G = Z.
Instance SR : SimRelation (set var × params) := {
ParamRel := ParamRel;
ArgRel := ArgRel;
BlockRel := fun lvZ b b´ ⇒ I.block_Z b = snd lvZ
}.
Defined.
Lemma sim_I r L L´ V V´ s LV lv
: agree_on eq (getAnn lv) V V´
→ true_live_sound Imperative LV s lv
→ simL´ r SR LV L L´
→ sim´r r (L,V, s) (L´,V´, compile LV s lv).
Lemma sim_DVE V V´ s lv
: agree_on eq (getAnn lv) V V´
→ true_live_sound Imperative nil s lv
→ @sim I.state _ I.state _ (nil,V, s) (nil,V´, compile nil s lv).
End I.
Fixpoint compile_live (s:stmt) (a:ann (set var)) (G:set var) : ann (set var) :=
match s, a with
| stmtLet x e s, ann1 lv an as a ⇒
if [x ∈ getAnn an] then ann1 (G ∪ lv) (compile_live s an {x})
else compile_live s an G
| stmtIf e s t, ann2 lv ans ant ⇒
if [exp2bool e = Some true] then
compile_live s ans G
else if [exp2bool e = Some false ] then
compile_live t ant G
else
ann2 (G ∪ lv) (compile_live s ans ∅) (compile_live t ant ∅)
| stmtApp f Y, ann0 lv ⇒ ann0 (G ∪ lv)
| stmtReturn x, ann0 lv ⇒ ann0 (G ∪ lv)
| stmtExtern x f Y s, ann1 lv an as a ⇒
ann1 (G ∪ lv) (compile_live s an {x})
| stmtFun Z s t, ann2 lv ans ant ⇒
let ans´ := compile_live s ans ∅ in
ann2 (G ∪ lv) (setTopAnn (ans´)
(getAnn ans´ ∪
of_list (List.filter (fun x ⇒ B[x ∈ getAnn ans]) Z)))
(compile_live t ant ∅)
| _, a ⇒ a
end.
Lemma compile_live_incl G i LV s lv
: true_live_sound i LV s lv
→ getAnn (compile_live s lv G) ⊆ G ∪ getAnn lv.
Lemma compile_live_incl_empty i LV s lv
: true_live_sound i LV s lv
→ getAnn (compile_live s lv ∅) ⊆ getAnn lv.
Lemma incl_compile_live G i LV s lv
: true_live_sound i LV s lv
→ G ⊆ getAnn (compile_live s lv G).
Definition compile_LV (LV:list (set var ×params)) :=
List.map (fun lvZ ⇒ let Z´ := List.filter (fun x ⇒ B[x ∈ fst lvZ]) (snd lvZ) in
(fst lvZ, Z´)) LV.
Lemma dve_live i LV s lv G
: true_live_sound i LV s lv
→ live_sound i (compile_LV LV) (compile LV s lv) (compile_live s lv G).
Require Import Plus Util AllInRel Map.
Require Import Val EqDec Computable Var Env EnvTy IL Annotation.
Require Import Sim Fresh Filter Liveness TrueLiveness Filter MoreExp.
Set Implicit Arguments.
Fixpoint compile (LV:list (set var × params)) (s:stmt) (a:ann (set var)) :=
match s, a with
| stmtLet x e s, ann1 lv an ⇒
if [x ∈ getAnn an] then stmtLet x e (compile LV s an)
else compile LV s an
| stmtIf e s t, ann2 _ ans ant ⇒
if [exp2bool e = Some true] then
(compile LV s ans)
else if [ exp2bool e = Some false ] then
(compile LV t ant)
else
stmtIf e (compile LV s ans) (compile LV t ant)
| stmtApp f Y, ann0 lv ⇒
let lvZ := nth (counted f) LV (∅,nil) in
stmtApp f (filter_by (fun y ⇒ B[y ∈ fst lvZ]) (snd lvZ) Y)
| stmtReturn x, ann0 _ ⇒ stmtReturn x
| stmtExtern x f e s, ann1 lv an ⇒
stmtExtern x f e (compile LV s an)
| stmtFun Z s t, ann2 lv ans ant ⇒
let LV´ := (getAnn ans,Z)::LV in
stmtFun (List.filter (fun x ⇒ B[x ∈ getAnn ans]) Z)
(compile LV´ s ans) (compile LV´ t ant)
| s, _ ⇒ s
end.
Definition ArgRel (V V:onv val) (G:(set var × params)) (VL VL´: list val) : Prop :=
VL´ = (filter_by (fun x ⇒ B[x ∈ (fst G)]) (snd G) VL) ∧
length (snd G) = length VL.
Definition ParamRel (G:(set var × params)) (Z Z´ : list var) : Prop :=
Z´ = (List.filter (fun x ⇒ B[x ∈ (fst G)]) Z) ∧ snd G = Z.
Instance SR : ProofRelation (set var × params) := {
ParamRel := ParamRel;
ArgRel := ArgRel;
BlockRel := fun lvZ b b´ ⇒ True
}.
Defined.
Lemma agree_on_update_filter X `{OrderedType X} Y `{Equivalence (option Y)}
(lv:set X) (V: X → option Y) Z VL
: length Z = length VL
→ agree_on R lv
(V [Z <-- List.map Some VL])
(V [List.filter (fun x ⇒ B[x ∈ lv]) Z <--
List.map Some (filter_by (fun x ⇒ B[x ∈ lv]) Z VL)]).
Lemma agree_on_update_filter´ X `{OrderedType X} Y `{Equivalence (option Y)} (lv:set X) (V V´:X → option Y) Z VL
: length Z = length VL
→ agree_on R (lv \ of_list Z) V V´
→ agree_on R lv
(V [Z <-- List.map Some VL])
(V´ [(List.filter (fun x ⇒ B[x ∈ lv]) Z) <-- (List.map Some
(filter_by (fun x ⇒ B[x ∈ lv]) Z VL))]).
Lemma sim_DVE´ r L L´ V V´ s LV lv
: agree_on eq (getAnn lv) V V´
→ true_live_sound Functional LV s lv
→ simL´ sim_progeq r SR LV L L´
→ sim´r r (L,V, s) (L´,V´, compile LV s lv).
Lemma sim_DVE V V´ s lv
: agree_on eq (getAnn lv) V V´
→ true_live_sound Functional nil s lv
→ @sim F.state _ F.state _ (nil,V, s) (nil,V´, compile nil s lv).
Module I.
Import Sim.I.
Definition ArgRel (V V´:onv val) (G:(set var × params)) (VL VL´: list val) : Prop :=
VL´ = (filter_by (fun x ⇒ B[x ∈ (fst G)]) (snd G) VL) ∧
length (snd G) = length VL ∧
agree_on eq (fst G \ of_list (snd G)) V V´.
Definition ParamRel (G:(set var × params)) (Z Z´ : list var) : Prop :=
Z´ = (List.filter (fun x ⇒ B[x ∈ (fst G)]) Z) ∧ snd G = Z.
Instance SR : SimRelation (set var × params) := {
ParamRel := ParamRel;
ArgRel := ArgRel;
BlockRel := fun lvZ b b´ ⇒ I.block_Z b = snd lvZ
}.
Defined.
Lemma sim_I r L L´ V V´ s LV lv
: agree_on eq (getAnn lv) V V´
→ true_live_sound Imperative LV s lv
→ simL´ r SR LV L L´
→ sim´r r (L,V, s) (L´,V´, compile LV s lv).
Lemma sim_DVE V V´ s lv
: agree_on eq (getAnn lv) V V´
→ true_live_sound Imperative nil s lv
→ @sim I.state _ I.state _ (nil,V, s) (nil,V´, compile nil s lv).
End I.
Fixpoint compile_live (s:stmt) (a:ann (set var)) (G:set var) : ann (set var) :=
match s, a with
| stmtLet x e s, ann1 lv an as a ⇒
if [x ∈ getAnn an] then ann1 (G ∪ lv) (compile_live s an {x})
else compile_live s an G
| stmtIf e s t, ann2 lv ans ant ⇒
if [exp2bool e = Some true] then
compile_live s ans G
else if [exp2bool e = Some false ] then
compile_live t ant G
else
ann2 (G ∪ lv) (compile_live s ans ∅) (compile_live t ant ∅)
| stmtApp f Y, ann0 lv ⇒ ann0 (G ∪ lv)
| stmtReturn x, ann0 lv ⇒ ann0 (G ∪ lv)
| stmtExtern x f Y s, ann1 lv an as a ⇒
ann1 (G ∪ lv) (compile_live s an {x})
| stmtFun Z s t, ann2 lv ans ant ⇒
let ans´ := compile_live s ans ∅ in
ann2 (G ∪ lv) (setTopAnn (ans´)
(getAnn ans´ ∪
of_list (List.filter (fun x ⇒ B[x ∈ getAnn ans]) Z)))
(compile_live t ant ∅)
| _, a ⇒ a
end.
Lemma compile_live_incl G i LV s lv
: true_live_sound i LV s lv
→ getAnn (compile_live s lv G) ⊆ G ∪ getAnn lv.
Lemma compile_live_incl_empty i LV s lv
: true_live_sound i LV s lv
→ getAnn (compile_live s lv ∅) ⊆ getAnn lv.
Lemma incl_compile_live G i LV s lv
: true_live_sound i LV s lv
→ G ⊆ getAnn (compile_live s lv G).
Definition compile_LV (LV:list (set var ×params)) :=
List.map (fun lvZ ⇒ let Z´ := List.filter (fun x ⇒ B[x ∈ fst lvZ]) (snd lvZ) in
(fst lvZ, Z´)) LV.
Lemma dve_live i LV s lv G
: true_live_sound i LV s lv
→ live_sound i (compile_LV LV) (compile LV s lv) (compile_live s lv G).