From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.
From Velus Require Import Common.
From Velus Require Import Operators Environment.
From Velus Require Import Clocks.
From Velus Require Import Fresh.
From Velus Require Import StaticEnv.
From Velus Require Import Lustre.LSyntax Lustre.LClocking.
From Velus Require Import Lustre.Normalization.Normalization.
From Velus Require Import Lustre.SubClock.SCClocking.
Preservation of Typing through Normalization
Module Type NCLOCKING
(
Import Ids :
IDS)
(
Import Op :
OPERATORS)
(
OpAux :
OPERATORS_AUX Ids Op)
(
Import Cks :
CLOCKS Ids Op OpAux)
(
Import Senv :
STATICENV Ids Op OpAux Cks)
(
Import Syn :
LSYNTAX Ids Op OpAux Cks Senv)
(
Import Clo :
LCLOCKING Ids Op OpAux Cks Senv Syn)
(
Import Norm :
NORMALIZATION Ids Op OpAux Cks Senv Syn).
Module Import SCC :=
SCClockingFun Ids Op OpAux Cks Senv Syn Clo SC.
Import SC.
Import Fresh Fresh.Facts Fresh.Tactics.
Rest of clockof preservation (started in Normalization.v)
Fact unnest_reset_clockof :
forall G vars e e'
eqs'
st st',
wc_exp G vars e ->
numstreams e = 1 ->
unnest_reset (
unnest_exp G true)
e st = (
e',
eqs',
st') ->
clockof e' =
clockof e.
Proof.
Corollary mmap2_unnest_exp_clocksof'' :
forall G vars is_control es es'
eqs'
st st',
Forall (
wc_exp G vars)
es ->
mmap2 (
unnest_exp G is_control)
es st = (
es',
eqs',
st') ->
Forall2 (
fun e ck =>
clockof e = [
ck]) (
concat es') (
clocksof es).
Proof.
Corollary mmap2_unnest_exp_clocksof''' :
forall G vars is_control ck es es'
eqs'
st st',
Forall (
wc_exp G vars)
es ->
Forall (
eq ck) (
clocksof es) ->
mmap2 (
unnest_exp G is_control)
es st = (
es',
eqs',
st') ->
Forall (
fun e =>
clockof e = [
ck]) (
concat es').
Proof.
Corollary mmap2_mmap2_unnest_exp_clocksof1 :
forall G vars is_control ck x tx es es'
eqs'
st st',
Forall (
fun es =>
Forall (
wc_exp G vars) (
snd es))
es ->
Forall (
fun '(
i,
es) =>
Forall (
eq (
Con ck x (
tx,
i))) (
clocksof es))
es ->
mmap2 (
fun '(
i,
es) =>
bind2 (
mmap2 (
unnest_exp G is_control)
es) (
fun es'
eqs' =>
ret (
i,
concat es',
concat eqs')))
es st = (
es',
eqs',
st') ->
Forall (
fun '(
i,
es) =>
Forall (
fun e =>
clockof e = [
Con ck x (
tx,
i)])
es)
es'.
Proof.
Corollary mmap2_mmap2_unnest_exp_clocksof2 :
forall G vars is_control ck (
es :
list (
enumtag *
_))
es'
eqs'
st st',
Forall (
fun es =>
Forall (
wc_exp G vars) (
snd es))
es ->
Forall (
fun es =>
Forall (
eq ck) (
clocksof (
snd es)))
es ->
mmap2 (
fun '(
i,
es) =>
bind2 (
mmap2 (
unnest_exp G is_control)
es) (
fun es'
eqs' =>
ret (
i,
concat es',
concat eqs')))
es st = (
es',
eqs',
st') ->
Forall (
fun es =>
Forall (
fun e =>
clockof e = [
ck]) (
snd es))
es'.
Proof.
Corollary mmap2_unnest_exp_clocksof :
forall G vars is_control es es'
eqs'
st st',
Forall (
wc_exp G vars)
es ->
mmap2 (
unnest_exp G is_control)
es st = (
es',
eqs',
st') ->
clocksof (
concat es') =
clocksof es.
Proof.
Local Hint Resolve mmap2_unnest_exp_clocksof :
norm.
Corollary unnest_exps_clocksof :
forall G vars es es'
eqs'
st st',
Forall (
wc_exp G vars)
es ->
unnest_exps G es st = (
es',
eqs',
st') ->
clocksof es' =
clocksof es.
Proof.
Fact fby_iteexp_clockof :
forall e0 e ann es'
eqs'
st st',
fby_iteexp e0 e ann st = (
es',
eqs',
st') ->
clockof es' = [(
snd ann)].
Proof.
intros ?? [
ty cl]
es'
eqs'
st st'
Hfby;
simpl in *.
destruct (
is_constant e0);
repeat inv_bind;
reflexivity.
Qed.
Fact unnest_fby_clocksof :
forall anns e0s es,
length e0s =
length anns ->
length es =
length anns ->
clocksof (
unnest_fby e0s es anns) =
List.map snd anns.
Proof.
Fact unnest_merge_clocksof :
forall tys x tx es nck,
clocksof (
unnest_merge (
x,
tx)
es tys nck) =
List.map (
fun _ =>
nck)
tys.
Proof.
induction tys; intros *; simpl in *; f_equal; eauto.
Qed.
Fact unnest_case_clocksof :
forall tys c es d nck,
clocksof (
unnest_case c es d tys nck) =
List.map (
fun _ =>
nck)
tys.
Proof.
induction tys; intros *; simpl in *; f_equal; eauto.
Qed.
Fact unnest_rhs_clockof:
forall G vars e es'
eqs'
st st',
wc_exp G vars e ->
unnest_rhs G e st = (
es',
eqs',
st') ->
clocksof es' =
clockof e.
Proof.
Corollary unnest_rhss_clocksof:
forall G vars es es'
eqs'
st st',
Forall (
wc_exp G vars)
es ->
unnest_rhss G es st = (
es',
eqs',
st') ->
clocksof es' =
clocksof es.
Proof.
nclockof is also preserved by unnest_exp
Fact unnest_merge_clockof :
forall ckid es tys ck,
Forall (
fun e =>
clockof e = [
ck]) (
unnest_merge ckid es tys ck).
Proof.
Fact unnest_case_clockof :
forall e es d tys ck,
Forall (
fun e =>
clockof e = [
ck]) (
unnest_case e es d tys ck).
Proof.
Fact unnest_when_nclocksof :
forall ckid k es tys ck,
length es =
length tys ->
nclocksof (
unnest_when ckid k es tys ck) =
map (
fun _ => (
ck,
None))
tys.
Proof.
unfold unnest_when.
induction es;
intros *
Hl;
destruct tys;
simpl in *;
try congruence;
auto.
Qed.
Fact unnest_merge_nclocksof :
forall tx tys es ck,
nclocksof (
unnest_merge tx es tys ck) =
map (
fun _ => (
ck,
None))
tys.
Proof.
unfold unnest_merge.
induction tys;
intros;
simpl in *;
auto.
Qed.
Fact unnest_case_nclocksof :
forall e tys es d ck,
nclocksof (
unnest_case e es d tys ck) =
map (
fun _ => (
ck,
None))
tys.
Proof.
unfold unnest_case.
induction tys;
intros;
simpl in *;
auto.
Qed.
Lemma idents_for_anns_nclocksof :
forall anns ids st st',
idents_for_anns anns st = (
ids,
st') ->
nclocksof (
map (
fun '(
x,
ann0) =>
Evar x ann0)
ids) =
map (
fun '(
x, (
_,
ck)) => (
ck,
Some x))
ids.
Proof.
induction anns as [|(?&?)]; intros * Hids; repeat inv_bind; simpl in *; auto.
f_equal; eauto.
Qed.
Fact unnest_exp_nclocksof :
forall G vars e is_control es'
eqs'
st st',
wc_exp G vars e ->
unnest_exp G is_control e st = (
es',
eqs',
st') ->
Forall2 (
fun '(
ck1,
o1) '(
ck2,
o2) =>
ck1 =
ck2 /\
LiftO True (
fun x1 =>
o2 =
Some x1)
o1) (
nclockof e) (
nclocksof es').
Proof with
eauto.
intros *
Hwc Hun.
assert (
length (
nclockof e) =
length (
nclocksof es'))
as Hlen.
{
rewrite length_nclockof_numstreams,
length_nclocksof_annots, <-
length_annot_numstreams.
apply unnest_exp_annot_length in Hun;
eauto with lclocking. }
inv Hwc;
repeat inv_bind;
simpl;
repeat rewrite map_length in Hlen.
-
repeat constructor.
-
repeat constructor.
-
repeat constructor.
-
repeat constructor.
-
repeat constructor.
-
repeat constructor.
-
repeat constructor.
-
erewrite idents_for_anns_nclocksof,
Forall2_map_2;
eauto.
eapply idents_for_anns_values in H5.
rewrite <-
H5, 2
Forall2_map_1.
apply Forall2_same,
Forall_forall;
intros (?&?&?)
_;
simpl;
auto.
-
erewrite idents_for_anns_nclocksof,
Forall2_map_2;
eauto.
eapply idents_for_anns_values in H5.
rewrite <-
H5, 2
Forall2_map_1.
apply Forall2_same,
Forall_forall;
intros (?&?&?)
_;
simpl;
auto.
-
rewrite unnest_when_nclocksof.
2:{
rewrite H2.
apply mmap2_unnest_exp_length in H3;
eauto with lclocking.
rewrite H3,
length_clocksof_annots;
eauto. }
apply Forall2_same,
Forall_map,
Forall_forall.
intros ?
_;
simpl;
auto.
-
destruct is_control;
repeat inv_bind.
+
rewrite unnest_merge_nclocksof.
apply Forall2_same,
Forall_map,
Forall_forall.
intros ?
_;
simpl;
auto.
+
erewrite idents_for_anns_nclocksof,
Forall2_map_2;
eauto.
eapply idents_for_anns_values in H5.
erewrite map_ext, <-
map_map, <-
H5, 2
Forall2_map_1.
2:
instantiate (1:=
fun '(
_,
ck) => (
ck,
None));
auto.
apply Forall2_same,
Forall_forall;
intros (?&?&?)
_;
simpl;
auto.
-
destruct is_control;
repeat inv_bind.
+
rewrite unnest_case_nclocksof.
apply Forall2_same,
Forall_map,
Forall_forall.
intros ?
_;
simpl;
auto.
+
erewrite idents_for_anns_nclocksof,
Forall2_map_2;
eauto.
eapply idents_for_anns_values in H11.
erewrite map_ext, <-
map_map, <-
H11, 2
Forall2_map_1.
2:
instantiate (1:=
fun '(
_,
ck) => (
ck,
None));
auto.
apply Forall2_same,
Forall_forall;
intros (?&?&?)
_;
simpl;
auto.
-
erewrite idents_for_anns_nclocksof,
Forall2_map_2;
eauto.
eapply idents_for_anns_values in H8.
rewrite <-
H8, 2
Forall2_map_1.
apply Forall2_same,
Forall_forall;
intros (?&?&?)
_;
simpl;
auto.
Qed.
Corollary mmap2_unnest_exp_nclocksof :
forall G vars es is_control es'
eqs'
st st',
Forall (
wc_exp G vars)
es ->
mmap2 (
unnest_exp G is_control)
es st = (
es',
eqs',
st') ->
Forall2 (
fun '(
ck1,
o1) '(
ck2,
o2) =>
ck1 =
ck2 /\
LiftO True (
fun x1 =>
o2 =
Some x1)
o1) (
nclocksof es) (
nclocksof (
concat es')).
Proof with
Lemma unnest_noops_exp_nclocksof :
forall ck e e'
eqs'
st st',
normalized_lexp e ->
unnest_noops_exp ck e st = (
e',
eqs',
st') ->
Forall2 (
fun '(
ck1,
o1) '(
ck2,
o2) =>
ck1 =
ck2 /\
LiftO True (
fun x1 =>
o2 =
Some x1)
o1) (
nclockof e) (
nclockof e').
Proof.
unfold unnest_noops_exp.
intros *
Hnormed Hun.
cases_eqn Heq;
repeat inv_bind;
simpl.
-
apply Forall2_same,
Forall_forall.
intros (?&?)
_.
split;
auto.
destruct o;
simpl in *;
auto.
-
inv Hnormed;
simpl in *;
inv Heq.
1-6:
repeat constructor.
destruct ck;
simpl in *;
try congruence.
Qed.
Fact unnest_noops_exps_nclocksof :
forall cks es es'
eqs'
st st',
Forall normalized_lexp es ->
length cks =
length es ->
unnest_noops_exps cks es st = (
es',
eqs',
st') ->
Forall2 (
fun '(
ck1,
o1) '(
ck2,
o2) =>
ck1 =
ck2 /\
LiftO True (
fun x1 =>
o2 =
Some x1)
o1) (
nclocksof es) (
nclocksof es').
Proof.
Fact unnest_noops_exps_nclocksof2 :
forall G vars cks es es2 es'
eqs2 eqs'
st st2 st3 st',
(
forall x, ~
IsLast vars x) ->
Forall (
wc_exp G vars)
es ->
length cks =
length (
annots es) ->
mmap2 (
unnest_exp G false)
es st = (
es2,
eqs2,
st2) ->
unnest_noops_exps cks (
concat es2)
st3 = (
es',
eqs',
st') ->
Forall2 (
fun '(
ck1,
o1) '(
ck2,
o2) =>
ck1 =
ck2 /\
LiftO True (
fun x1 =>
o2 =
Some x1)
o1) (
nclocksof es) (
nclocksof es').
Proof.
A few additional things
Fact idents_for_anns_incl_ck :
forall anns ids st st',
idents_for_anns anns st = (
ids,
st') ->
forall x ty ck,
In (
x, (
ty,
ck))
ids ->
HasClock (
st_senv st')
x ck.
Proof.
intros *
Hids *
Hin.
apply idents_for_anns_incl in Hids.
apply Hids in Hin.
econstructor.
solve_In.
auto.
Qed.
Ltac solve_incl :=
match goal with
|
H :
wc_clock ?
l1 ?
cl |-
wc_clock ?
l2 ?
cl =>
eapply wc_clock_incl; [|
eauto];
intros
|
H :
wc_exp ?
G ?
l1 ?
e |-
wc_exp ?
G ?
l2 ?
e =>
eapply wc_exp_incl; [| |
eauto];
intros
|
H :
wc_equation ?
G ?
l1 ?
eq |-
wc_equation ?
G ?
l2 ?
eq =>
eapply wc_equation_incl; [| |
eauto];
intros
|
H :
wc_block ?
G ?
l1 ?
eq |-
wc_block ?
G ?
l2 ?
eq =>
eapply wc_block_incl; [| |
eauto];
intros
|
H :
In ?
i ?
l1 |-
In ?
i ?
l2 =>
assert (
incl l1 l2)
by repeat solve_incl;
eauto
| |-
incl (
st_anns ?
st1) (
st_anns _) =>
eapply st_follows_incl;
repeat solve_st_follows
| |-
incl ?
l1 ?
l1 =>
reflexivity
| |-
incl ?
l1 (?
l1 ++ ?
l2) =>
eapply incl_appl;
reflexivity
| |-
incl (?
l1 ++ ?
l2) (?
l1 ++ ?
l3) =>
apply incl_appr'
| |-
incl ?
l1 (?
l2 ++ ?
l3) =>
eapply incl_appr
| |-
incl ?
l1 (?
a::?
l2) =>
eapply incl_tl
| |-
incl _ _ =>
apply incl_map
|
H :
HasClock ?
l1 ?
x ?
ty |-
HasClock ?
l2 ?
x ?
ty =>
eapply HasClock_incl; [|
eauto]
|
H :
IsLast ?
l1 ?
x |-
IsLast ?
l2 ?
x =>
eapply IsLast_incl; [|
eauto]
end;
auto.
Preservation of clocking through first pass
Import Permutation.
Fact fresh_ident_wc_env :
forall pref hint vars ty ck id (
st st':
fresh_st pref _),
wc_env (
idck (
vars++
st_senv st)) ->
wc_clock (
idck (
vars++
st_senv st))
ck ->
fresh_ident hint (
ty,
ck)
st = (
id,
st') ->
wc_env (
idck (
vars++
st_senv st')).
Proof.
Fact idents_for_anns_wc_env :
forall vars anns ids st st',
wc_env (
idck (
vars++
st_senv st)) ->
Forall (
wc_clock (
idck (
vars++
st_senv st))) (
map snd anns) ->
idents_for_anns anns st = (
ids,
st') ->
wc_env (
idck (
vars++
st_senv st')).
Proof with
eauto.
induction anns as [|[
ty ck]];
intros ids st st'
Hwenv Hwc Hids;
repeat inv_bind...
inv Hwc.
eapply IHanns in H0... 2:(
solve_forall;
repeat solve_incl).
eapply fresh_ident_wc_env...
Qed.
Fact hd_default_wc_exp {
PSyn prefs} :
forall (
G : @
global PSyn prefs)
vars es,
Forall (
wc_exp G vars)
es ->
wc_exp G vars (
hd_default es).
Proof.
intros G vars es Hf.
destruct es; simpl.
- constructor.
- inv Hf; auto.
Qed.
Local Hint Resolve hd_default_wc_exp :
norm.
Section unnest_node_wc.
Variable G1 : @
global nolocal local_prefs.
Variable G2 : @
global nolocal norm1_prefs.
Fact idents_for_anns_wc :
forall vars anns ids st st',
idents_for_anns anns st = (
ids,
st') ->
Forall (
wc_exp G2 (
vars++
st_senv st')) (
List.map (
fun '(
x,
ann) =>
Evar x ann)
ids).
Proof.
Fact mmap2_wc {
pref A B} :
forall vars (
k :
A ->
Fresh pref (
list exp *
list equation)
B)
a es'
eqs'
st st',
mmap2 k a st = (
es',
eqs',
st') ->
(
forall st st'
a es eqs',
k a st = (
es,
eqs',
st') ->
st_follows st st') ->
Forall (
fun a =>
forall es'
eqs'
st0 st0',
k a st0 = (
es',
eqs',
st0') ->
st_follows st st0 ->
st_follows st0'
st' ->
Forall (
wc_exp G2 vars)
es' /\
Forall (
wc_equation G2 vars)
eqs')
a ->
Forall (
wc_exp G2 vars) (
concat es') /\
Forall (
wc_equation G2 vars) (
concat eqs').
Proof with
eauto.
intros vars k a.
induction a;
intros *
Hmap Hfollows Hforall;
repeat inv_bind;
simpl.
-
repeat constructor.
-
inv Hforall.
assert (
H':=
H).
eapply H3 in H'
as [
Hwc1 Hwc1']... 2,3:
repeat solve_st_follows.
eapply IHa in H0 as [
Hwc2 Hwc2']...
2:{
solve_forall.
eapply H2 in H4...
etransitivity... }
repeat rewrite Forall_app.
repeat split;
eauto.
Qed.
Fact mmap2_wc' {
pref A B} :
forall vars (
k :
A ->
Fresh pref (
enumtag *
list exp *
list equation)
B)
a es'
eqs'
st st',
mmap2 k a st = (
es',
eqs',
st') ->
(
forall st st'
a es eqs',
k a st = (
es,
eqs',
st') ->
st_follows st st') ->
Forall (
fun a =>
forall n es'
eqs'
st0 st0',
k a st0 = (
n,
es',
eqs',
st0') ->
st_follows st st0 ->
st_follows st0'
st' ->
Forall (
wc_exp G2 vars)
es' /\
Forall (
wc_equation G2 vars)
eqs')
a ->
Forall (
wc_exp G2 vars) (
concat (
map snd es')) /\
Forall (
wc_equation G2 vars) (
concat eqs').
Proof with
eauto.
intros vars k a.
induction a;
intros *
Hmap Hfollows Hforall;
repeat inv_bind;
simpl.
-
repeat constructor.
-
inv Hforall.
assert (
H':=
H).
destruct x.
eapply H3 in H'
as [
Hwc1 Hwc1']... 2,3:
repeat solve_st_follows.
eapply IHa in H0 as [
Hwc2 Hwc2']...
2:{
solve_forall.
eapply H2 in H4...
etransitivity... }
repeat rewrite Forall_app.
repeat split;
eauto.
Qed.
Fact unnest_fby_wc_exp :
forall vars e0s es anns,
Forall (
wc_exp G2 vars)
e0s ->
Forall (
wc_exp G2 vars)
es ->
Forall2 (
fun e0 a =>
clockof e0 = [
a])
e0s (
map snd anns) ->
Forall2 (
fun e a =>
clockof e = [
a])
es (
map snd anns) ->
Forall (
wc_exp G2 vars) (
unnest_fby e0s es anns).
Proof.
Fact unnest_arrow_wc_exp :
forall vars e0s es anns,
Forall (
wc_exp G2 vars)
e0s ->
Forall (
wc_exp G2 vars)
es ->
Forall2 (
fun e0 a =>
clockof e0 = [
a])
e0s (
map snd anns) ->
Forall2 (
fun e a =>
clockof e = [
a])
es (
map snd anns) ->
Forall (
wc_exp G2 vars) (
unnest_arrow e0s es anns).
Proof.
Fact unnest_when_wc_exp :
forall vars ckid tx ck b ty es tys,
length es =
length tys ->
HasClock vars ckid ck ->
Forall (
wc_exp G2 vars)
es ->
Forall (
fun e =>
clockof e = [
ck])
es ->
Forall (
wc_exp G2 vars) (
unnest_when (
ckid,
tx)
b es tys (
Con ck ckid (
ty,
b))).
Proof.
intros *
Hlen Hin Hwc Hck.
unfold unnest_when.
solve_forall.
repeat constructor;
auto;
simpl;
rewrite app_nil_r,
H1;
auto.
Qed.
Fact unnest_merge_wc_exp :
forall vars ckid tx ck es tys,
HasClock vars ckid ck ->
es <> [] ->
Forall (
fun es =>
length (
snd es) =
length tys)
es ->
Forall (
fun es =>
Forall (
wc_exp G2 vars) (
snd es))
es ->
Forall (
fun '(
i,
es) =>
Forall (
fun e =>
clockof e = [
Con ck ckid (
tx,
i)])
es)
es ->
Forall (
wc_exp G2 vars) (
unnest_merge (
ckid,
tx)
es tys ck).
Proof.
intros *;
revert es.
induction tys;
intros *
InV Hnnil Hlen Hwc Hcks;
simpl;
constructor.
-
constructor;
auto;
try rewrite Forall_map.
+
contradict Hnnil.
apply map_eq_nil in Hnnil;
auto.
+
clear -
Hwc.
eapply Forall_impl; [|
eauto];
intros (?&?)
Hf;
simpl in *.
inv Hf;
auto with norm.
+
clear -
Hcks Hlen.
rewrite Forall_forall in *;
intros (?&?)
Hin;
simpl.
rewrite app_nil_r.
specialize (
Hlen _ Hin).
specialize (
Hcks _ Hin);
simpl in *.
inv Hcks;
simpl in *;
try congruence.
rewrite H.
auto.
+
clear -
Hcks Hlen.
rewrite Forall_forall in *;
intros (?&?)
Hin;
simpl.
rewrite app_nil_r.
specialize (
Hlen _ Hin).
specialize (
Hcks _ Hin);
simpl in *.
inv Hcks;
simpl in *;
try congruence.
rewrite H.
auto.
-
eapply IHtys;
eauto;
try rewrite Forall_map.
+
contradict Hnnil.
apply map_eq_nil in Hnnil;
auto.
+
clear -
Hlen.
eapply Forall_impl; [|
eauto];
intros.
destruct a0,
l;
simpl;
inv H;
auto.
+
clear -
Hwc.
eapply Forall_impl; [|
eauto];
intros.
destruct a;
simpl in *.
inv H;
simpl;
auto.
+
clear -
Hcks.
eapply Forall_impl; [|
eauto];
intros.
destruct a;
simpl in *.
inv H;
simpl;
auto.
Qed.
Fact unnest_case_wc_exp :
forall vars e ck es d tys,
wc_exp G2 vars e ->
clockof e = [
ck] ->
es <> [] ->
Forall (
fun es =>
length (
snd es) =
length tys)
es ->
Forall (
fun es =>
Forall (
wc_exp G2 vars) (
snd es))
es ->
Forall (
fun es =>
Forall (
fun e =>
clockof e = [
ck]) (
snd es))
es ->
LiftO True (
fun d =>
length (
clocksof d) =
length tys)
d ->
LiftO True (
Forall (
wc_exp G2 vars))
d ->
LiftO True (
Forall (
fun e =>
clockof e = [
ck]))
d ->
Forall (
wc_exp G2 vars) (
unnest_case e es d tys ck).
Proof.
intros *;
revert es d.
induction tys;
intros *
Hwce Hck Hnnil Hlen Hwc Hcks Hlend Hwcd Hckd;
simpl;
constructor.
-
constructor;
auto;
try rewrite Forall_map.
+
contradict Hnnil.
apply map_eq_nil in Hnnil;
auto.
+
clear -
Hwc.
eapply Forall_impl; [|
eauto];
intros (?&?)
Hf;
simpl in *.
inv Hf;
auto with norm.
+
clear -
Hcks Hlen.
rewrite Forall_forall in *;
intros (?&?)
Hin;
simpl.
rewrite app_nil_r.
specialize (
Hlen _ Hin).
specialize (
Hcks _ Hin);
simpl in *.
inv Hcks;
simpl in *;
try congruence.
rewrite H.
auto.
+
clear -
Hcks Hlen.
rewrite Forall_forall in *;
intros (?&?)
Hin;
simpl.
rewrite app_nil_r.
specialize (
Hlen _ Hin).
specialize (
Hcks _ Hin);
simpl in *.
inv Hcks;
simpl in *;
try congruence.
rewrite H.
auto.
+
intros ?
Hopt.
destruct d;
simpl in *;
inv Hopt.
inv Hwcd;
auto with norm.
+
intros ?
Hopt.
destruct d;
simpl in *;
inv Hopt.
inv Hckd;
simpl in *;
try congruence.
rewrite app_nil_r,
H.
auto.
+
intros ?
Hopt.
destruct d;
simpl in *;
inv Hopt.
inv Hckd;
simpl in *;
try congruence.
rewrite app_nil_r,
H.
auto.
-
eapply IHtys;
eauto;
try rewrite Forall_map.
+
contradict Hnnil.
apply map_eq_nil in Hnnil;
auto.
+
clear -
Hlen.
eapply Forall_impl; [|
eauto];
intros.
destruct a0;
simpl;
inv H;
auto.
destruct l;
inv H1;
auto.
+
clear -
Hwc.
eapply Forall_impl; [|
eauto];
intros.
destruct a;
simpl in *;
inv H;
simpl;
auto.
+
clear -
Hcks.
eapply Forall_impl; [|
eauto];
intros.
destruct a;
simpl in *;
inv H;
simpl;
auto.
+
destruct d;
simpl in *;
try congruence.
inv Hckd;
simpl in *;
try congruence.
rewrite H in Hlend;
simpl in *;
inv Hlend;
auto.
+
destruct d;
simpl in *;
auto.
inv Hwcd;
simpl;
auto.
+
destruct d;
simpl in *;
auto.
inv Hckd;
simpl;
auto.
Qed.
Fact unnest_reset_wc :
forall vars e e'
eqs'
st st'
ck,
(
forall x, ~
IsLast vars x) ->
(
forall es'
eqs'
st0',
st_follows st0'
st' ->
unnest_exp G1 true e st = (
es',
eqs',
st0') ->
Forall (
wc_exp G2 (
vars++
st_senv st0'))
es' /\
Forall (
wc_equation G2 (
vars++
st_senv st0'))
eqs') ->
wc_exp G1 (
vars++
st_senv st)
e ->
clockof e = [
ck] ->
unnest_reset (
unnest_exp G1 true)
e st = (
e',
eqs',
st') ->
clockof e' = [
ck] /\
wc_exp G2 (
vars++
st_senv st')
e' /\
Forall (
wc_equation G2 (
vars++
st_senv st'))
eqs'.
Proof.
intros *
Hnl Hkwc Hwc Hck Hunn.
repeat split.
-
eapply unnest_reset_clockof in Hunn;
eauto;
try congruence.
rewrite <-
length_clockof_numstreams,
Hck;
eauto.
-
unnest_reset_spec;
simpl in *;
auto.
+
specialize (
Hkwc _ _ _ (
st_follows_refl _)
eq_refl)
as (
Hwc1&
_).
destruct l;
simpl in H; [
inv H|];
subst.
inv Hwc1;
auto.
+
constructor.
eapply fresh_ident_In in Hfresh.
apply HasClock_app;
right.
econstructor;
solve_In;
auto.
-
unfold unnest_reset in Hunn.
simpl in *;
repeat inv_bind;
auto.
assert (
length x = 1).
{
eapply unnest_exp_length in H;
eauto with lclocking.
rewrite <-
length_clockof_numstreams,
Hck in H;
auto. }
singleton_length.
assert (
Hk:=
H).
eapply unnest_exp_normalized_cexp,
Forall_singl in H. 3:
eauto with lclocking.
2:{
apply NoLast_app;
split;
auto.
apply senv_of_tyck_NoLast. }
assert (
st_follows x1 st')
as Hfollows.
{
inv H; [| |
inv H1];
try destruct cl;
simpl in *;
repeat inv_bind;
repeat solve_st_follows. }
eapply Hkwc in Hk as [
Hwc1 Hwc2];
auto.
inv H; [| |
inv H1];
simpl in *.
1-8:
repeat inv_bind.
1-8:
try constructor.
2,4,6,8,9,11,13,15:
solve_forall;
repeat solve_incl.
1-7:
simpl_Forall.
1-7:
repeat (
constructor;
eauto;
repeat solve_incl);
simpl in *.
1-7:(
take (
fresh_ident _ _ _ = (
_,
_))
and eapply fresh_ident_In in it;
apply HasClock_app,
or_intror;
econstructor;
solve_In;
auto).
Qed.
Fact unnest_resets_wc :
forall vars es es'
eqs'
st st',
(
forall x, ~
IsLast vars x) ->
Forall (
fun e =>
forall es'
eqs'
st0 st0',
unnest_exp G1 true e st0 = (
es',
eqs',
st0') ->
st_follows st st0 ->
st_follows st0'
st' ->
Forall (
wc_exp G2 (
vars++
st_senv st0'))
es' /\
Forall (
wc_equation G2 (
vars++
st_senv st0'))
eqs')
es ->
Forall (
wc_exp G1 (
vars++
st_senv st))
es ->
Forall (
fun e =>
exists ck,
clockof e = [
ck])
es ->
mmap2 (
unnest_reset (
unnest_exp G1 true))
es st = (
es',
eqs',
st') ->
Forall (
fun e =>
exists ck,
clockof e = [
ck])
es' /\
Forall (
wc_exp G2 (
vars++
st_senv st'))
es' /\
Forall (
wc_equation G2 (
vars++
st_senv st')) (
concat eqs').
Proof.
induction es;
intros *
Hnl F Wt Cks Map;
inv F;
inv Wt;
inv Cks;
repeat inv_bind;
simpl in *;
auto.
assert (
Map:=
H0).
eapply IHes in H0 as (
Cks1&
Wt1&
Wt2);
eauto.
3:
solve_forall;
repeat solve_incl.
2:{
eapply Forall_impl; [|
eapply H2].
intros.
eapply H7 in H10;
eauto.
repeat solve_st_follows. }
destruct H5 as (?&?).
eapply unnest_reset_wc in H as (
Cks2&
Wt3&
Wt4);
eauto.
repeat split;
try constructor;
eauto.
-
repeat solve_incl.
-
apply Forall_app;
split;
auto.
solve_forall;
repeat solve_incl.
-
intros *
Follows Un.
eapply H1 in Un;
eauto. 1,2:
repeat solve_st_follows.
Qed.
Lemma unnest_noops_exps_wc :
forall vars cks es es'
eqs'
st st' ,
length es =
length cks ->
Forall normalized_lexp es ->
Forall (
fun e =>
numstreams e = 1)
es ->
Forall (
wc_exp G2 (
vars++
st_senv st))
es ->
unnest_noops_exps cks es st = (
es',
eqs',
st') ->
Forall (
wc_exp G2 (
vars++
st_senv st'))
es' /\
Forall (
wc_equation G2 (
vars++
st_senv st'))
eqs'.
Proof.
unfold unnest_noops_exps.
induction cks;
intros *
Hlen Hnormed Hnums Hwt Hunt;
repeat inv_bind;
simpl;
auto.
destruct es;
simpl in *;
inv Hlen;
repeat inv_bind.
inv Hwt.
inv Hnums.
inv Hnormed.
assert (
Forall (
wc_exp G2 (
vars ++
st_senv x2))
es)
as Hes.
{
solve_forall.
repeat solve_incl;
eauto with norm. }
eapply IHcks in Hes as (
Hes'&
Heqs'). 2-4:
eauto.
2:
repeat inv_bind;
repeat eexists;
eauto;
inv_bind;
eauto.
unfold unnest_noops_exp in H.
rewrite <-
length_annot_numstreams in H6.
singleton_length.
destruct p as (?&?).
split;
simpl;
try constructor;
try (
rewrite Forall_app;
split);
auto.
1,2:
destruct (
is_noops_exp)
eqn:
Hnoops;
repeat inv_bind;
auto.
+
repeat solve_incl.
+
constructor.
eapply fresh_ident_In in H.
eapply HasClock_incl with (
senv1:=
st_senv x2).
repeat solve_incl.
econstructor;
solve_In;
auto.
+
repeat constructor;
auto;
simpl;
try rewrite app_nil_r.
*
repeat solve_incl.
*
rewrite clockof_annot,
Hsingl;
simpl.
constructor;
auto.
eapply fresh_ident_In in H.
apply HasClock_incl with (
senv1:=
st_senv x2).
repeat solve_incl.
econstructor;
solve_In;
auto.
Qed.
Hypothesis Hiface :
global_iface_incl G1 G2.
Fact unnest_exp_wc :
forall vars e is_control es'
eqs'
st st',
(
forall x, ~
IsLast vars x) ->
wc_exp G1 (
vars++
st_senv st)
e ->
unnest_exp G1 is_control e st = (
es',
eqs',
st') ->
Forall (
wc_exp G2 (
vars++
st_senv st'))
es' /\
Forall (
wc_equation G2 (
vars++
st_senv st'))
eqs'.
Proof with
eauto with norm lclocking.
Local Ltac solve_mmap2 :=
solve_forall;
match goal with
|
Hnorm :
unnest_exp _ _ _ _ =
_,
H :
context [
unnest_exp _ _ _ _ =
_ ->
_] |-
_ =>
eapply H in Hnorm as [? ?];
eauto;
try split;
try solve_forall;
repeat solve_incl
end.
intros *
Hnl.
revert is_control es'
eqs'
st st'.
induction e using exp_ind2;
intros is_control es'
eqs'
st st'
Hwc Hnorm;
repeat inv_bind;
inv Hwc.
-
repeat constructor.
-
repeat constructor.
-
repeat constructor...
-
repeat constructor;
auto.
-
assert (
length x =
numstreams e)
as Hlen by eauto with norm lclocking.
rewrite <-
length_clockof_numstreams,
H4 in Hlen;
simpl in Hlen.
singleton_length.
assert (
Hnorm:=
H);
eapply IHe in H as [
Hwc1 Hwc1'];
eauto.
repeat econstructor...
+
inv Hwc1;
eauto.
+
eapply unnest_exp_clockof in Hnorm;
simpl in Hnorm;
eauto with lclocking.
rewrite app_nil_r,
H4 in Hnorm...
-
repeat inv_bind.
assert (
length x =
numstreams e1)
as Hlen1 by eauto with norm lclocking.
rewrite <-
length_clockof_numstreams,
H7 in Hlen1;
simpl in Hlen1.
assert (
length x2 =
numstreams e2)
as Hlen2 by eauto with norm lclocking.
rewrite <-
length_clockof_numstreams,
H8 in Hlen2;
simpl in Hlen2.
repeat singleton_length.
assert (
Hnorm1:=
H);
eapply IHe1 in H as [
Hwc1 Hwc1'];
eauto.
assert (
Hnorm2:=
H0);
eapply IHe2 in H0 as [
Hwc2 Hwc2'];
eauto. 2:
repeat solve_incl.
repeat econstructor...
+
inv Hwc1.
repeat solve_incl.
+
inv Hwc2...
+
eapply unnest_exp_clockof in Hnorm1;
simpl in Hnorm1;
eauto with lclocking.
rewrite app_nil_r,
H7 in Hnorm1...
+
eapply unnest_exp_clockof in Hnorm2;
simpl in Hnorm2;
eauto with lclocking.
rewrite app_nil_r,
H8 in Hnorm2...
+
apply Forall_app;
split;
auto.
solve_forall.
repeat solve_incl.
-
destruct_conjs;
repeat inv_bind.
assert (
Hnorm1:=
H0).
eapply mmap2_wc with (
vars:=
vars++
st_senv x1)
in H0 as [
Hwt1 Hwt1']...
2:
solve_mmap2.
eapply mmap2_unnest_exp_clocksof in Hnorm1;
eauto.
assert (
HasClock (
vars ++
st_senv st')
x2 ck)
as Hck.
{
take (
fresh_ident _ _ _ =
_)
and eapply fresh_ident_In in it.
apply HasClock_app,
or_intror.
econstructor;
solve_In.
auto. }
repeat constructor;
auto.
2,3:
rewrite Hnorm1;
auto.
1,2:
simpl_Forall;
repeat solve_incl.
-
repeat inv_bind.
assert (
Hnorm1:=
H1).
eapply mmap2_wc with (
vars:=
vars++
st_senv x1)
in H1 as [
Hwt1 Hwt1']...
assert (
Hnorm2:=
H2).
eapply mmap2_wc with (
vars:=
vars++
st_senv x4)
in H2 as [
Hwt2 Hwt2']...
2,3:
solve_mmap2.
repeat rewrite Forall_app.
repeat split.
3-4:
solve_forall;
repeat solve_incl.
+
eapply idents_for_anns_wc in H3...
+
assert (
Forall (
wc_exp G2 (
vars++
st_senv st')) (
unnest_fby (
concat x2) (
concat x6)
a))
as Hwcfby.
{
rewrite Forall2_eq in H9,
H10.
eapply unnest_fby_wc_exp...
1-2:
solve_forall;
repeat solve_incl.
+
eapply mmap2_unnest_exp_clocksof''
in Hnorm1...
congruence.
+
eapply mmap2_unnest_exp_clocksof''
in Hnorm2...
congruence. }
remember (
unnest_fby _ _ _)
as fby.
assert (
length (
concat x2) =
length a)
as Hlen1.
{
eapply mmap2_unnest_exp_length in Hnorm1...
apply Forall2_length in H9.
repeat simpl_length;
erewrite <-
map_length, <-
typesof_annots;
solve_length. }
assert (
length (
concat x6) =
length a)
as Hlen2.
{
eapply mmap2_unnest_exp_length in Hnorm2...
apply Forall2_length in H10.
repeat simpl_length.
erewrite <-
map_length, <-
typesof_annots;
solve_length. }
assert (
length fby =
length x5).
{
rewrite Heqfby,
unnest_fby_length...
eapply idents_for_anns_length in H3... }
assert (
Forall2 (
fun '(
_,
ck)
e =>
clockof e = [
ck]) (
map snd x5)
fby)
as Htys.
{
eapply idents_for_anns_values in H3;
subst.
specialize (
unnest_fby_annot'
_ _ _ Hlen1 Hlen2)
as Hanns;
eauto.
clear -
Hanns.
eapply Forall2_swap_args.
solve_forall.
rewrite clockof_annot,
H1;
auto. }
eapply mk_equations_Forall.
solve_forall.
repeat constructor;
eauto;
simpl;
rewrite app_nil_r.
*
rewrite H5.
repeat constructor.
eapply idents_for_anns_incl_ck in H3;
eauto.
apply HasClock_app;
auto.
-
repeat inv_bind.
assert (
Hnorm1:=
H1).
eapply mmap2_wc with (
vars:=
vars++
st_senv x1)
in H1 as [
Hwt1 Hwt1']...
assert (
Hnorm2:=
H2).
eapply mmap2_wc with (
vars:=
vars++
st_senv x4)
in H2 as [
Hwt2 Hwt2']...
2,3:
solve_mmap2.
repeat rewrite Forall_app.
repeat split.
3-4:
solve_forall;
repeat solve_incl.
+
eapply idents_for_anns_wc in H3...
+
assert (
Forall (
wc_exp G2 (
vars++
st_senv st')) (
unnest_arrow (
concat x2) (
concat x6)
a))
as Hwcarrow.
{
rewrite Forall2_eq in H9,
H10.
eapply unnest_arrow_wc_exp...
1-2:
solve_forall;
repeat solve_incl.
+
eapply mmap2_unnest_exp_clocksof''
in Hnorm1...
congruence.
+
eapply mmap2_unnest_exp_clocksof''
in Hnorm2...
congruence. }
remember (
unnest_arrow _ _ _)
as arrow.
assert (
length (
concat x2) =
length a)
as Hlen1.
{
eapply mmap2_unnest_exp_length in Hnorm1...
apply Forall2_length in H9.
repeat simpl_length;
erewrite <-
map_length, <-
typesof_annots;
solve_length. }
assert (
length (
concat x6) =
length a)
as Hlen2.
{
eapply mmap2_unnest_exp_length in Hnorm2...
apply Forall2_length in H10.
repeat simpl_length.
erewrite <-
map_length, <-
typesof_annots;
solve_length. }
assert (
length arrow =
length x5).
{
rewrite Heqarrow,
unnest_arrow_length...
eapply idents_for_anns_length in H3... }
assert (
Forall2 (
fun '(
_,
ck)
e =>
clockof e = [
ck]) (
map snd x5)
arrow)
as Htys.
{
eapply idents_for_anns_values in H3;
subst.
specialize (
unnest_arrow_annot'
_ _ _ Hlen1 Hlen2)
as Hanns;
eauto.
clear -
Hanns.
eapply Forall2_swap_args.
solve_forall.
rewrite clockof_annot,
H1;
auto. }
eapply mk_equations_Forall.
solve_forall.
repeat constructor;
eauto;
simpl;
rewrite app_nil_r.
rewrite H5.
repeat constructor.
eapply idents_for_anns_incl_ck in H3;
eauto.
apply HasClock_app;
auto.
-
repeat inv_bind.
assert (
H0':=
H0).
eapply mmap2_wc with (
vars:=
vars++
st_senv st')
in H0'
as [
Hwc1 Hwc1']...
2:
solve_mmap2.
split;
auto.
apply unnest_when_wc_exp...
+
eapply mmap2_unnest_exp_length in H0...
solve_length.
+
repeat solve_incl.
+
eapply mmap2_unnest_exp_clocksof'''
in H0...
-
repeat inv_bind.
assert (
Hnorm1:=
H0).
eapply mmap2_wc'
in H0 as (?&?).
2:(
intros;
repeat inv_bind;
destruct a;
repeat solve_st_follows).
2:{
solve_forall;
repeat inv_bind.
eapply mmap2_wc with (
vars:=
vars++
st_senv x2)
in H5...
solve_mmap2. }
assert (
Forall (
wc_exp G2 (
vars++
st_senv st')) (
unnest_merge (
x0,
tx)
x tys ck))
as Hwcexp.
{
eapply unnest_merge_wc_exp...
+
destruct is_control;
repeat solve_incl.
+
eapply mmap2_length_1 in Hnorm1.
intro contra;
subst.
destruct es;
simpl in *;
try congruence.
+
apply mmap2_mmap2_unnest_exp_length in Hnorm1. 2:
solve_forall...
clear -
Hnorm1 H7.
induction Hnorm1;
inv H7;
constructor;
auto.
destruct y;
simpl in *.
now rewrite H2,
H,
length_clocksof_annots.
+
eapply Forall_concat in H0.
rewrite Forall_map in H0.
solve_forall.
solve_forall.
destruct is_control;
repeat solve_incl.
+
eapply mmap2_mmap2_unnest_exp_clocksof1;
eauto. }
destruct is_control;
repeat inv_bind;
repeat rewrite Forall_app;
repeat split;
eauto.
3:
solve_forall;
repeat solve_incl.
+
eapply idents_for_anns_wc in H1...
+
assert (
Forall (
fun e :
exp =>
clockof e = [
ck]) (
unnest_merge (
x0,
tx)
x tys ck))
as Hnck.
{
eapply unnest_merge_clockof;
solve_length. }
eapply mk_equations_Forall.
solve_forall.
2:(
rewrite unnest_merge_length;
eapply idents_for_anns_length in H1;
solve_length).
repeat constructor;
simpl. 2:
rewrite app_nil_r.
*
repeat constructor...
*
rewrite H7;
simpl.
repeat constructor.
assert (
H':=
H1).
apply idents_for_anns_values in H'.
eapply idents_for_anns_incl_ck in H1.
apply HasClock_app;
eauto.
assert (
In (
t,
c) (
map snd x3))
by solve_In.
setoid_rewrite H'
in H9.
simpl_In;
eauto.
-
repeat inv_bind.
assert (
st_follows x1 x4)
as Hfollows by repeat solve_st_follows.
assert (
st_follows x7 st')
as Hfollows2 by (
destruct is_control;
repeat solve_st_follows).
assert (
st_follows x4 st')
as Hfollows3 by (
destruct d;
repeat solve_st_follows).
assert (
Hnorm0:=
H1).
eapply IHe in H1 as (
Hwc0&?)...
assert (
Hnorm1:=
H2).
eapply mmap2_wc'
in H2 as (?&?).
2:(
intros;
repeat inv_bind;
destruct a;
repeat solve_st_follows).
2:{
solve_forall;
repeat inv_bind.
eapply mmap2_wc with (
vars:=
vars++
st_senv x4)
in H9...
solve_mmap2. }
assert (
length x = 1);
try singleton_length.
{
eapply unnest_exp_length in Hnorm0...
now rewrite Hnorm0, <-
length_clockof_numstreams,
H6. }
apply Forall_singl in Hwc0.
assert (
Forall (
wc_exp G2 (
vars++
st_senv st')) (
unnest_case e0 x2 x5 tys ck))
as Hwcexp.
{
eapply unnest_case_wc_exp...
+
repeat solve_incl.
+
apply unnest_exp_clockof in Hnorm0;
simpl in *...
rewrite app_nil_r in Hnorm0.
congruence.
+
eapply mmap2_length_1 in Hnorm1.
intro contra;
subst.
destruct es;
simpl in *;
try congruence.
+
apply mmap2_mmap2_unnest_exp_length in Hnorm1. 2:
solve_forall...
clear -
Hnorm1 H10.
induction Hnorm1;
constructor;
inv H10;
eauto with datatypes.
destruct y;
simpl in *;
auto.
now rewrite H,
H2,
length_clocksof_annots.
+
eapply Forall_concat in H2.
rewrite Forall_map in H2.
solve_forall.
solve_forall.
destruct is_control;
repeat solve_incl.
+
eapply mmap2_mmap2_unnest_exp_clocksof2 in Hnorm1;
eauto.
+
destruct d;
repeat inv_bind;
simpl;
auto.
rewrite length_clocksof_annots.
eapply mmap2_unnest_exp_annots_length in H3...
rewrite H3, <-
length_clocksof_annots, <-
H13;
auto.
+
destruct d;
repeat inv_bind;
simpl;
auto.
eapply mmap2_wc in H3 as (?&?)...
solve_forall.
eapply H8 in H9 as (?&?);
eauto. 2:
eapply Forall_forall in H11;
eauto.
split; (
eapply Forall_impl; [|
eauto];
intros). 1-3:
repeat solve_incl.
+
destruct d;
repeat inv_bind;
simpl;
auto.
eapply mmap2_unnest_exp_clocksof'''
in H3;
eauto.
}
assert (
Forall (
wc_equation G2 (
vars ++
st_senv st'))
x6)
as Hwcd'.
{
destruct d;
repeat inv_bind;
simpl;
auto.
eapply mmap2_wc in H3 as (?&?)...
solve_forall.
eapply H8 in H9 as (?&?);
eauto. 2:
eapply Forall_forall in H11;
eauto.
split; (
eapply Forall_impl; [|
eauto];
intros). 1-3:
repeat solve_incl. }
destruct is_control;
repeat inv_bind;
repeat rewrite Forall_app;
repeat split;
eauto.
1,2,5,6:
solve_forall;
repeat solve_incl.
+
eapply idents_for_anns_wc in H4...
+
assert (
Forall (
fun e :
exp =>
clockof e = [
ck]) (
unnest_case e0 x2 x5 tys ck))
as Hnck.
{
eapply unnest_case_clockof;
solve_length. }
eapply mk_equations_Forall.
solve_forall.
2:(
rewrite unnest_case_length;
eapply idents_for_anns_length in H4;
solve_length).
repeat constructor;
simpl. 2:
rewrite app_nil_r.
*
repeat constructor...
*
rewrite H10;
simpl.
repeat constructor.
assert (
H':=
H4).
apply idents_for_anns_values in H'.
eapply idents_for_anns_incl_ck in H4.
apply HasClock_app;
eauto.
assert (
In (
t,
c) (
map snd x))
as Hin'
by solve_In.
setoid_rewrite H'
in Hin'.
simpl_In;
eauto.
-
assert (
st_follows x4 x7)
as Hfollows by repeat solve_st_follows.
eapply unnest_resets_wc in H3 as (
Hck2&
Hwt2&
Hwt2');
eauto.
2:
solve_mmap2. 2:
solve_forall;
repeat solve_incl.
assert (
Hnorm:=
H1).
eapply mmap2_wc with (
vars:=
vars++
st_senv x1)
in H1 as [
Hwc1 Hwc1']...
2:
solve_mmap2.
assert (
length (
find_node_incks G1 f) =
length (
concat x6))
as Hlen1.
{
unfold find_node_incks.
rewrite H11.
eapply Forall2_length in H12.
rewrite map_length.
eapply mmap2_unnest_exp_length in Hnorm...
rewrite length_nclocksof_annots in H12.
rewrite map_length in H12.
congruence. }
assert (
Forall (
fun e :
exp =>
numstreams e = 1) (
concat x6))
as Hnum.
{
eapply mmap2_unnest_exp_numstreams;
eauto. }
apply Hiface in H11 as (?&?&?&?&
Hin&
Hout).
assert (
length (
n_in n) =
length (
nclocksof x2))
as Hlen2.
{
apply Forall2_length in H12.
repeat setoid_rewrite map_length in H12.
rewrite H12.
eapply unnest_noops_exps_nclocksof2 with (
es:=
es),
Forall2_length in H2. 3:
eauto with lclocking. 1-4:
eauto.
2:
rewrite Hlen1...
apply NoLast_app;
split;
auto.
apply senv_of_tyck_NoLast.
}
remember (
Env.from_list (
map_filter (
fun '(
x, (
_,
ox)) =>
option_map (
fun xc => (
x,
xc))
ox)
(
combine (
map fst (
n_in n)) (
nclocksof x2))))
as sub2.
assert (
Forall2 (
fun '(
x,
_) '(
ck,
ox) =>
LiftO (
Env.find x sub2 =
None) (
fun x' =>
Env.MapsTo x x'
sub2)
ox) (
map (
fun '(
x, (
_,
ck,
_)) => (
x,
ck)) (
n_in n)) (
nclocksof x2))
as Hsub2.
{
apply Forall2_forall;
split. 2:
repeat setoid_rewrite map_length;
auto.
intros (?&?) (?&?)
Hin'.
assert (
In (
k, (
c0,
o)) (
combine (
map fst (
n_in n)) (
nclocksof x2)))
as Hin2.
{
repeat setoid_rewrite combine_map_fst in Hin'.
eapply in_map_iff in Hin'
as (((?&(?&?)&?)&?&?)&
Heq&?);
inv Heq.
rewrite combine_map_fst.
eapply in_map_iff.
do 2
esplit;
eauto.
simpl;
auto. }
assert (
NoDupMembers (
combine (
map fst (
n_in n)) (
nclocksof x2)))
as Hnd1.
{
rewrite fst_NoDupMembers,
combine_map_fst', <-
fst_NoDupMembers. 2:
now rewrite map_length.
pose proof (
n_nodup n)
as (
Hnd1&
_).
apply fst_NoDupMembers;
eauto using NoDup_app_l. }
destruct o;
simpl;
subst.
-
eapply Env.find_In_from_list.
2:{
clear -
Hnd1.
remember (
combine _ _)
as comb.
clear -
Hnd1.
induction comb as [|(?&?&?)];
simpl in *;
inv Hnd1.
constructor.
destruct (
option_map _ _)
as [(?&?)|]
eqn:
Hopt;
simpl;
auto.
eapply option_map_inv in Hopt as (?&?&
Heq);
inv Heq.
econstructor;
auto.
intro contra.
apply H1.
apply fst_InMembers,
in_map_iff in contra as ((?&?)&?&
Hin);
subst.
apply map_filter_In'
in Hin as ((?&?&?)&
Hin&
Hopt).
apply option_map_inv in Hopt as (?&?&
Heq);
inv Heq.
apply In_InMembers in Hin;
auto.
}
eapply map_filter_In;
eauto.
-
destruct (
Env.find _ _)
eqn:
Hfind;
auto.
exfalso.
eapply Env.from_list_find_In,
map_filter_In'
in Hfind as ((?&?&?)&
Hin3&
Hopt).
apply option_map_inv in Hopt as (?&?&
Heq);
inv Heq.
eapply NoDupMembers_det in Hin2;
eauto.
inv Hin2.
}
repeat constructor;
simpl in *... 2:
econstructor...
+
eapply idents_for_anns_wc...
+
eapply unnest_noops_exps_wc with (
vars:=
vars)
in H2 as (?&?);
auto.
solve_forall;
repeat solve_incl.
eapply mmap2_normalized_lexp in Hnorm. 1,3:
eauto with lclocking.
apply NoLast_app;
split;
auto.
apply senv_of_tyck_NoLast.
+
solve_forall;
repeat solve_incl.
+
instantiate (1:=
fun x =>
match (
sub x)
with
|
Some y =>
Some y
|
_ =>
Env.find x sub2
end).
eapply unnest_noops_exps_nclocksof2 with (
es:=
es)
in H2. 3,5:
eauto.
2:{
apply NoLast_app;
split;
auto.
apply senv_of_tyck_NoLast. }
2:{
rewrite Hlen1;
eauto... }
eapply Forall2_trans_ex in H2;
eauto.
erewrite map_ext, <-
map_map, <-
Hin.
simpl_Forall.
unfold nclock in *;
destruct_conjs;
subst.
2:
intros;
destruct_conjs;
instantiate (1:=
fun '(
x, (
ty,
ck)) => (
x,
ck));
auto.
destruct o;
simpl in *;
subst.
eapply WellInstantiated_refines2;
eauto.
2:
eapply WellInstantiated_refines1;
eauto.
1,2:
intros ??
Hsub;
rewrite Hsub;
auto.
1:(
take (
WellInstantiated _ _ _ _)
and destruct it as (
Hwi1&
_);
simpl in *;
rewrite Hwi1;
simpl;
eauto;
destruct o0;
simpl in *;
eauto).
+
erewrite map_ext, <-
map_map, <-
Hout,
idents_for_anns_values...
simpl_Forall.
2:
intros;
destruct_conjs;
instantiate (1:=
fun '(
x, (
ty,
ck)) => (
x,
ck));
auto.
eapply WellInstantiated_refines1;
eauto.
*
intros ??
Hsub.
rewrite Hsub;
auto.
*
take (
WellInstantiated _ _ _ _)
and destruct it as (
Hwi1&
_);
simpl in *.
rewrite Hwi1.
subst.
destruct (
Env.find i _)
eqn:
Hfind;
auto.
exfalso.
eapply Env.from_list_find_In,
map_filter_In'
in Hfind as ((?&?&?)&?&
Hopt).
apply option_map_inv in Hopt as (?&?&
Heq);
inv Heq.
simpl_In.
simpl_In.
pose proof (
n_nodup n)
as (
Hnd&
_).
eapply NoDup_app_In in Hnd.
eapply Hnd.
1,2:
solve_In.
+
rewrite app_nil_r,
map_map.
simpl_Forall.
eapply idents_for_anns_incl_ck in H4;
eauto.
apply HasClock_app;
auto.
+
repeat rewrite Forall_app;
repeat split.
2:
eapply unnest_noops_exps_wc in H2 as (?&?);
eauto.
3:{
eapply mmap2_normalized_lexp in Hnorm. 1,3:
eauto with lclocking.
apply NoLast_app;
split;
auto.
apply senv_of_tyck_NoLast. }
1-3:
solve_forall;
repeat solve_incl.
Qed.
Corollary mmap2_unnest_exp_wc :
forall vars is_control es es'
eqs'
st st',
(
forall x, ~
IsLast vars x) ->
Forall (
wc_exp G1 (
vars++
st_senv st))
es ->
mmap2 (
unnest_exp G1 is_control)
es st = (
es',
eqs',
st') ->
Forall (
wc_exp G2 (
vars++
st_senv st')) (
concat es') /\
Forall (
wc_equation G2 (
vars++
st_senv st')) (
concat eqs').
Proof.
intros *
Hnl Hwt Hmap.
eapply mmap2_wc in Hmap;
eauto with norm.
solve_forall.
eapply unnest_exp_wc with (
vars:=
vars)
in H1 as [? ?];
eauto.
split. 1,2:
solve_forall. 1,2,3:
repeat solve_incl.
Qed.
Corollary unnest_exps_wc :
forall vars es es'
eqs'
st st',
(
forall x, ~
IsLast vars x) ->
Forall (
wc_exp G1 (
vars++
st_senv st))
es ->
unnest_exps G1 es st = (
es',
eqs',
st') ->
Forall (
wc_exp G2 (
vars++
st_senv st'))
es' /\
Forall (
wc_equation G2 (
vars++
st_senv st'))
eqs'.
Proof.
Corollary mmap2_mmap2_unnest_exp_wc :
forall vars is_control (
es:
list (
enumtag *
_))
es'
eqs'
st st',
(
forall x, ~
IsLast vars x) ->
Forall (
fun es =>
Forall (
wc_exp G1 (
vars++
st_senv st)) (
snd es))
es ->
mmap2 (
fun '(
i,
es) =>
bind2 (
mmap2 (
unnest_exp G1 is_control)
es) (
fun es'
eqs' =>
ret (
i,
concat es',
concat eqs')))
es st = (
es',
eqs',
st') ->
Forall (
fun es =>
Forall (
wc_exp G2 (
vars++
st_senv st')) (
snd es))
es' /\
Forall (
wc_equation G2 (
vars++
st_senv st')) (
concat eqs').
Proof.
intros *
Hnl Hwt Hmap.
eapply mmap2_wc'
with (
vars:=
vars++
st_senv st')
in Hmap as (
Hwc1&
Hwc2);
eauto.
-
split;
auto.
rewrite <-
Forall_concat,
Forall_map in Hwc1.
eauto.
-
intros ?? (?&?) (?&?) ??.
repeat solve_st_follows.
-
eapply Forall_forall;
intros (?&?)
Hin * ???.
repeat inv_bind.
eapply mmap2_unnest_exp_wc with (
vars:=
vars)
in H as (
Hwc1&
Hwc2);
eauto.
split.
3:
eapply Forall_forall in Hwt;
eauto.
1-3:
eapply Forall_impl; [|
eauto];
intros;
repeat solve_incl.
Qed.
Fact unnest_rhs_wc :
forall vars e es'
eqs'
st st',
(
forall x, ~
IsLast vars x) ->
wc_exp G1 (
vars++
st_senv st)
e ->
unnest_rhs G1 e st = (
es',
eqs',
st') ->
Forall (
wc_exp G2 (
vars++
st_senv st'))
es' /\
Forall (
wc_equation G2 (
vars++
st_senv st'))
eqs'.
Proof with
eauto with norm lclocking.
intros *
Hnl Hwc Hnorm.
destruct e;
unfold unnest_rhs in Hnorm;
try (
solve [
eapply unnest_exp_wc in Hnorm;
eauto]);
repeat inv_bind;
inv Hwc.
-
assert (
Hnorm:=
H).
eapply unnest_exps_wc in H as [
Hwc1 Hwc1']...
eapply unnest_exps_clocksof in Hnorm...
repeat constructor;
auto. 1,2:
congruence.
-
rewrite Forall2_eq in H6,
H7.
repeat inv_bind.
assert (
H':=
H).
eapply unnest_exps_wc in H'
as [
Hwc1 Hwc1']...
assert (
H0':=
H0).
eapply unnest_exps_wc with (
vars:=
vars)
in H0'
as [
Hwc2 Hwc2']...
2:
solve_forall;
repeat solve_incl.
repeat rewrite Forall_app;
repeat split.
2-3:
solve_forall;
repeat solve_incl.
eapply unnest_fby_wc_exp...
+
solve_forall;
repeat solve_incl.
+
unfold unnest_exps in H;
repeat inv_bind.
eapply mmap2_unnest_exp_clocksof''
in H...
congruence.
+
unfold unnest_exps in H0;
repeat inv_bind.
eapply mmap2_unnest_exp_clocksof''
in H0...
congruence.
-
rewrite Forall2_eq in H6,
H7.
repeat inv_bind.
assert (
H':=
H).
eapply unnest_exps_wc in H'
as [
Hwc1 Hwc1']...
assert (
H0':=
H0).
eapply unnest_exps_wc with (
vars:=
vars)
in H0'
as [
Hwc2 Hwc2']...
2:
solve_forall;
repeat solve_incl.
repeat rewrite Forall_app;
repeat split.
2-3:
solve_forall;
repeat solve_incl.
eapply unnest_arrow_wc_exp...
+
solve_forall;
repeat solve_incl.
+
unfold unnest_exps in H;
repeat inv_bind.
eapply mmap2_unnest_exp_clocksof''
in H...
congruence.
+
unfold unnest_exps in H0;
repeat inv_bind.
eapply mmap2_unnest_exp_clocksof''
in H0...
congruence.
-
assert (
Hnorm:=
H).
eapply unnest_exps_wc in H as [
Hwc1 Hwc1']...
assert (
st_follows x4 st')
as Hfollows by repeat solve_st_follows.
eapply unnest_resets_wc with (
vars:=
vars)
in H1 as [
Hwc2 [
Hwc2'
Hwc2'']]...
2,3:
solve_forall. 2:
eapply unnest_exp_wc in H3;
eauto. 2,3:
repeat solve_incl.
assert (
length (
find_node_incks G1 i) =
length x)
as Hlen1.
{
unfold find_node_incks.
rewrite H8.
eapply Forall2_length in H9.
rewrite map_length.
eapply unnest_exps_length in Hnorm;
eauto...
rewrite length_nclocksof_annots,
map_length in H9.
congruence. }
assert (
Forall (
fun e :
exp =>
numstreams e = 1)
x)
as Hnum.
{
eapply unnest_exps_numstreams;
eauto. }
apply Hiface in H8 as (?&?&?&?&
Hin&
Hout).
assert (
length (
n_in n) =
length (
nclocksof x2))
as Hlen2.
{
apply Forall2_length in H9.
repeat setoid_rewrite map_length in H9.
rewrite H9.
unfold unnest_exps in Hnorm;
repeat inv_bind.
eapply unnest_noops_exps_nclocksof2,
Forall2_length in H0. 1,5:
eauto. 2:
eauto with lclocking.
2:
rewrite Hlen1;
eauto...
apply NoLast_app;
split;
auto.
apply senv_of_tyck_NoLast.
}
unfold unnest_exps in *.
repeat inv_bind.
remember (
Env.from_list (
map_filter (
fun '(
x, (
_,
ox)) =>
option_map (
fun xc => (
x,
xc))
ox)
(
combine (
map fst (
n_in n)) (
nclocksof x2))))
as sub2.
assert (
Forall2 (
fun '(
x,
_) '(
ck,
ox) =>
LiftO (
Env.find x sub2 =
None) (
fun x' =>
Env.MapsTo x x'
sub2)
ox) (
map (
fun '(
x, (
_,
ck,
_)) => (
x,
ck)) (
n_in n)) (
nclocksof x2))
as Hsub2.
{
apply Forall2_forall;
split. 2:
repeat setoid_rewrite map_length;
auto.
intros (?&?) (?&?)
Hin'.
assert (
In (
k, (
c0,
o)) (
combine (
map fst (
n_in n)) (
nclocksof x2)))
as Hin2.
{
repeat setoid_rewrite combine_map_fst in Hin'.
eapply in_map_iff in Hin'
as (((?&(?&?)&?)&?&?)&
Heq&?);
inv Heq.
rewrite combine_map_fst.
eapply in_map_iff.
do 2
esplit;
eauto.
simpl;
auto. }
assert (
NoDupMembers (
combine (
map fst (
n_in n)) (
nclocksof x2)))
as Hnd1.
{
rewrite fst_NoDupMembers,
combine_map_fst', <-
fst_NoDupMembers. 2:
now rewrite map_length.
pose proof (
n_nodup n)
as (
Hnd1&
_).
apply fst_NoDupMembers;
eauto using NoDup_app_l. }
destruct o;
simpl;
subst.
-
eapply Env.find_In_from_list.
2:{
clear -
Hnd1.
remember (
combine _ _)
as comb.
clear -
Hnd1.
induction comb as [|(?&?&?)];
simpl in *;
inv Hnd1.
constructor.
destruct (
option_map _ _)
as [(?&?)|]
eqn:
Hopt;
simpl;
auto.
eapply option_map_inv in Hopt as (?&?&
Heq);
inv Heq.
econstructor;
auto.
intro contra.
apply H1.
apply fst_InMembers,
in_map_iff in contra as ((?&?)&?&
Hin);
subst.
apply map_filter_In'
in Hin as ((?&?&?)&
Hin&
Hopt).
apply option_map_inv in Hopt as (?&?&
Heq);
inv Heq.
apply In_InMembers in Hin;
auto.
}
eapply map_filter_In;
eauto.
-
destruct (
Env.find _ _)
eqn:
Hfind;
auto.
exfalso.
eapply Env.from_list_find_In,
map_filter_In'
in Hfind as ((?&?&?)&
Hin3&
Hopt).
apply option_map_inv in Hopt as (?&?&
Heq);
inv Heq.
eapply NoDupMembers_det in Hin2;
eauto.
inv Hin2.
}
repeat constructor;
simpl in *...
econstructor...
+
eapply unnest_noops_exps_wc with (
vars:=
vars)
in H0 as (?&?);
eauto.
solve_forall;
repeat solve_incl.
eapply mmap2_normalized_lexp in H3. 1,3:
eauto with lclocking.
apply NoLast_app;
split;
auto.
apply senv_of_tyck_NoLast.
+
instantiate (1:=
fun x =>
match (
sub x)
with
|
Some y =>
Some y
|
_ =>
Env.find x sub2
end).
eapply unnest_noops_exps_nclocksof2 with (
es:=
l)
in H0. 5,3:
eauto with senv.
2:{
apply NoLast_app;
split;
auto.
apply senv_of_tyck_NoLast. }
2:{
rewrite Hlen1;
eauto... }
eapply Forall2_trans_ex in H0;
eauto.
erewrite map_ext, <-
map_map, <-
Hin.
simpl_Forall.
2:
intros;
destruct_conjs;
instantiate (1:=
fun '(
x, (
_,
ck)) => (
x,
ck));
auto.
unfold nclock in *;
destruct_conjs;
subst.
destruct o;
simpl in *;
subst.
eapply WellInstantiated_refines2;
eauto.
2:
eapply WellInstantiated_refines1;
eauto.
1,2:
intros ??
Hsub;
rewrite Hsub;
auto.
1:(
take (
WellInstantiated _ _ _ _)
and destruct it as (
Hwi1&
_);
simpl in *;
rewrite Hwi1;
simpl;
eauto;
destruct o0;
simpl in *;
auto).
+
erewrite map_ext, <-
map_map, <-
Hout.
simpl_Forall.
2:
intros;
destruct_conjs;
instantiate (1:=
fun '(
x, (
_,
ck)) => (
x,
ck));
auto.
eapply WellInstantiated_refines1;
eauto.
*
intros ??
Hsub.
rewrite Hsub;
auto.
*
take (
WellInstantiated _ _ _ _)
and destruct it as (
Hwi1&
_);
simpl in *.
rewrite Hwi1.
subst.
destruct (
Env.find i0 _)
eqn:
Hfind;
auto.
exfalso.
eapply Env.from_list_find_In in Hfind.
simpl_In.
simpl_In.
pose proof (
n_nodup n)
as (
Hnd&
_).
eapply NoDup_app_In in Hnd.
eapply Hnd.
1,2:
solve_In.
+
repeat rewrite Forall_app;
repeat split.
2:
eapply unnest_noops_exps_wc in H0 as (?&?);
eauto.
3:{
eapply mmap2_normalized_lexp in H3. 1,3:
eauto with lclocking.
apply NoLast_app;
split;
auto.
apply senv_of_tyck_NoLast. }
1-3:
solve_forall;
repeat solve_incl.
Qed.
Corollary unnest_rhss_wc :
forall vars es es'
eqs'
st st',
(
forall x, ~
IsLast vars x) ->
Forall (
wc_exp G1 (
vars++
st_senv st))
es ->
unnest_rhss G1 es st = (
es',
eqs',
st') ->
Forall (
wc_exp G2 (
vars++
st_senv st'))
es' /\
Forall (
wc_equation G2 (
vars++
st_senv st'))
eqs'.
Proof.
intros *
Hnl Hwc Hnorm.
unfold unnest_rhss in Hnorm;
repeat inv_bind.
eapply mmap2_wc in H;
eauto with norm lclocking.
solve_forall.
eapply unnest_rhs_wc with (
vars:=
vars)
in H2 as [? ?];
eauto.
split. 1,2:
solve_forall. 1,2,3:
repeat solve_incl.
Qed.
Fact unnest_equation_wc_eq :
forall vars e eqs'
st st',
(
forall x, ~
IsLast vars x) ->
wc_equation G1 (
vars++
st_senv st)
e ->
unnest_equation G1 e st = (
eqs',
st') ->
Forall (
wc_equation G2 (
vars++
st_senv st'))
eqs'.
Proof with
eauto with norm lclocking.
intros vars [
xs es]
eqs'
st st'
Hnl Hwc Hnorm.
unfold unnest_equation in Hnorm.
repeat inv_bind.
inv Hwc.
-
assert (
length xs =
length anns)
as Hlen.
{
eapply Forall3_length in H6 as (
_&
Hlen).
rewrite map_length in Hlen;
auto. }
unfold unnest_rhss in H;
repeat inv_bind.
rewrite firstn_all2,
skipn_all2. 2,3:
setoid_rewrite Hlen;
reflexivity.
assert (
Hnorm:=
H).
eapply unnest_exps_wc in H as [
Hwc1 Hwc1']...
assert (
st_follows st x6)
as Hfollows by repeat solve_st_follows.
assert (
Hnr:=
H1).
eapply unnest_resets_wc with (
vars:=
vars)
in H1 as [
Hwc2 [
Hwc2'
Hwc2'']]...
2,3:
solve_forall. 2:
eapply unnest_exp_wc in H7;
eauto. 2,3:
repeat solve_incl.
assert (
length (
find_node_incks G1 f) =
length x1)
as Hlen1.
{
unfold find_node_incks.
rewrite H4.
eapply Forall2_length in H5.
rewrite map_length.
eapply unnest_exps_length in Hnorm...
rewrite length_nclocksof_annots,
map_length in H5.
congruence. }
assert (
Forall (
fun e :
exp =>
numstreams e = 1)
x1)
as Hnum.
{
eapply unnest_exps_numstreams;
eauto. }
apply Hiface in H4 as (?&?&?&?&
Hin&
Hout).
assert (
length (
n_in n) =
length (
nclocksof x4))
as Hlen2.
{
apply Forall2_length in H5.
repeat setoid_rewrite map_length in H5.
rewrite H5.
unfold unnest_exps in Hnorm;
repeat inv_bind.
eapply unnest_noops_exps_nclocksof2,
Forall2_length in H0. 1,5:
eauto. 2:
eauto with lclocking.
2:
rewrite Hlen1...
apply NoLast_app;
split;
auto.
apply senv_of_tyck_NoLast.
}
unfold unnest_exps in *.
repeat inv_bind.
remember (
Env.from_list (
map_filter (
fun '(
x, (
_,
ox)) =>
option_map (
fun xc => (
x,
xc))
ox)
(
combine (
map fst (
n_in n)) (
nclocksof x4))))
as sub2.
assert (
Forall2 (
fun '(
x,
_) '(
ck,
ox) =>
LiftO (
Env.find x sub2 =
None) (
fun x' =>
Env.MapsTo x x'
sub2)
ox) (
map (
fun '(
x, (
_,
ck,
_)) => (
x,
ck)) (
n_in n)) (
nclocksof x4))
as Hsub2.
{
apply Forall2_forall;
split. 2:
repeat setoid_rewrite map_length;
auto.
intros (?&?) (?&?)
Hin'.
assert (
In (
k, (
c0,
o)) (
combine (
map fst (
n_in n)) (
nclocksof x4)))
as Hin2.
{
repeat setoid_rewrite combine_map_fst in Hin'.
eapply in_map_iff in Hin'
as (((?&(?&?)&?)&?&?)&
Heq&?);
inv Heq.
rewrite combine_map_fst.
eapply in_map_iff.
do 2
esplit;
eauto.
simpl;
auto. }
assert (
NoDupMembers (
combine (
map fst (
n_in n)) (
nclocksof x4)))
as Hnd1.
{
rewrite fst_NoDupMembers,
combine_map_fst', <-
fst_NoDupMembers. 2:
now rewrite map_length.
pose proof (
n_nodup n)
as (
Hnd1&
_).
apply fst_NoDupMembers;
eauto using NoDup_app_l. }
destruct o;
simpl;
subst.
-
eapply Env.find_In_from_list.
2:{
clear -
Hnd1.
remember (
combine _ _)
as comb.
clear -
Hnd1.
induction comb as [|(?&?&?)];
simpl in *;
inv Hnd1.
constructor.
destruct (
option_map _ _)
as [(?&?)|]
eqn:
Hopt;
simpl;
auto.
eapply option_map_inv in Hopt as (?&?&
Heq);
inv Heq.
econstructor;
auto.
intro contra.
apply H1.
apply fst_InMembers,
in_map_iff in contra as ((?&?)&?&
Hin);
subst.
apply map_filter_In'
in Hin as ((?&?&?)&
Hin&
Hopt).
apply option_map_inv in Hopt as (?&?&
Heq);
inv Heq.
apply In_InMembers in Hin;
auto.
}
eapply map_filter_In;
eauto.
-
destruct (
Env.find _ _)
eqn:
Hfind;
auto.
exfalso.
eapply Env.from_list_find_In,
map_filter_In'
in Hfind as ((?&?&?)&
Hin3&
Hopt).
apply option_map_inv in Hopt as (?&?&
Heq);
inv Heq.
eapply NoDupMembers_det in Hin2;
eauto.
inv Hin2.
}
repeat econstructor;
simpl in *...
+
eapply unnest_noops_exps_wc with (
vars:=
vars)
in H0 as (?&?);
eauto.
solve_forall;
repeat solve_incl.
eapply mmap2_normalized_lexp in H9. 1,3:
eauto with lclocking.
apply NoLast_app;
split;
auto.
apply senv_of_tyck_NoLast.
+
instantiate (1:=
fun x =>
match (
sub x)
with
|
Some y =>
Some y
|
_ =>
Env.find x sub2
end).
eapply unnest_noops_exps_nclocksof2 with (
es:=
es0)
in H0. 5:
eauto. 3:
eauto with lclocking.
2:{
apply NoLast_app;
split;
auto.
apply senv_of_tyck_NoLast. }
2:{
rewrite Hlen1;
eauto... }
eapply Forall2_trans_ex in H0;
eauto.
erewrite map_ext, <-
map_map, <-
Hin.
simpl_Forall.
2:
intros;
destruct_conjs;
instantiate (1:=
fun '(
x, (
_,
ck)) => (
x,
ck));
auto.
unfold nclock in *;
destruct_conjs;
subst.
destruct o;
simpl in *;
subst.
eapply WellInstantiated_refines2;
eauto.
2:
eapply WellInstantiated_refines1;
eauto.
1,2:
intros ??
Hsub;
rewrite Hsub;
auto.
1:(
take (
WellInstantiated _ _ _ _)
and destruct it as (
Hwi1&
_);
simpl in *;
rewrite Hwi1;
simpl;
eauto;
destruct o0;
simpl in *;
auto).
+
erewrite map_ext, <-
map_map, <-
Hout,
map_map.
simpl_Forall.
2:
intros;
destruct_conjs;
instantiate (1:=
fun '(
x, (
_,
ck)) => (
x,
ck));
auto.
erewrite Forall3_map_1 in *.
eapply Forall3_impl_In; [|
eauto];
intros ??? ???
Hwi;
destruct_conjs.
eapply WellInstantiated_refines2;
eauto.
intros ??
Hsub.
rewrite Hsub;
auto.
+
simpl_Forall.
repeat solve_incl.
+
rewrite app_nil_r.
repeat rewrite Forall_app;
repeat split.
2:
eapply unnest_noops_exps_wc in H0 as (?&?);
eauto.
3:{
eapply mmap2_normalized_lexp in H9. 1,3:
eauto with lclocking.
apply NoLast_app;
split;
auto.
apply senv_of_tyck_NoLast. }
1-3:
solve_forall;
repeat solve_incl.
-
assert (
st_follows st st')
as Hfollows by eauto with norm.
assert (
H':=
H).
eapply unnest_rhss_wc in H'
as [
Hwc1'
Hwc1'']...
apply Forall_app;
split...
rename H3 into Hwc2.
replace (
clocksof es)
with (
clocksof x)
in Hwc2.
2: {
eapply unnest_rhss_clocksof in H... }
clear -
H2 Hwc2 Hwc1'
Hfollows.
revert es xs H2 Hwc2 Hwc1'.
induction x;
intros;
simpl in *;
try constructor.
+
inv Hwc2;
simpl;
auto.
+
inv Hwc1'.
assert (
length (
firstn (
numstreams a)
xs) =
length (
clockof a))
as Hlen1.
{
apply Forall2_length in Hwc2.
rewrite app_length in Hwc2.
rewrite firstn_length,
Hwc2,
length_clockof_numstreams.
apply Nat.min_l.
lia. }
rewrite <- (
firstn_skipn (
numstreams a)
xs)
in Hwc2.
apply Forall2_app_split in Hwc2 as [
Hwc2 _]...
repeat constructor...
simpl.
rewrite app_nil_r.
simpl_Forall.
repeat solve_incl.
+
inv Hwc1'.
eapply IHx...
assert (
length (
firstn (
numstreams a)
xs) =
length (
clockof a))
as Hlen1.
{
apply Forall2_length in Hwc2.
rewrite app_length in Hwc2.
rewrite firstn_length,
Hwc2,
length_clockof_numstreams.
apply Nat.min_l.
lia. }
rewrite <- (
firstn_skipn (
numstreams a)
xs)
in Hwc2.
apply Forall2_app_split in Hwc2 as [
_ Hwc2]...
Qed.
Lemma unnest_block_wc :
forall vars d blocks'
st st',
(
forall x, ~
IsLast vars x) ->
wc_block G1 (
vars++
st_senv st)
d ->
unnest_block G1 d st = (
blocks',
st') ->
Forall (
wc_block G2 (
vars++
st_senv st'))
blocks'.
Proof.
induction d using block_ind2;
intros *
Hnl Hwc Hun;
inv Hwc;
repeat inv_bind.
-
eapply unnest_equation_wc_eq in H;
eauto.
rewrite Forall_map.
eapply Forall_impl; [|
eauto];
intros.
constructor;
auto.
-
assert (
st_follows x0 st')
as Hfollows by (
repeat solve_st_follows).
eapply unnest_reset_wc with (
vars:=
vars)
in H1 as (
Hck1&
Hwc1&
Hwc1');
eauto.
2:{
intros.
eapply unnest_exp_wc in H6;
eauto;
repeat solve_incl. }
2:
repeat solve_incl.
apply Forall_app;
split.
+
clear -
Hnl H H2 H0 H5 Hck1 Hwc1 Hfollows.
revert st x x0 Hfollows H H0 H2 H5.
induction blocks;
intros *
Hfollows Hf Hmap Hwc Hwc2;
repeat inv_bind;
simpl;
auto;
inv Hf;
inv Hwc.
rewrite map_app,
Forall_app;
split.
*
eapply H3 in H;
eauto.
rewrite Forall_map.
eapply Forall_impl; [|
eauto];
intros.
econstructor;
eauto.
constructor;
auto.
repeat solve_incl.
*
eapply IHblocks;
eauto.
clear -
H6 H.
solve_forall.
repeat solve_incl.
+
simpl_Forall.
constructor;
auto.
-
constructor;
auto.
eapply iface_incl_wc_block;
eauto.
econstructor;
eauto.
-
constructor;
eauto.
eapply iface_incl_wc_block;
eauto.
econstructor;
eauto.
-
constructor;
eauto.
eapply iface_incl_wc_block;
eauto.
econstructor;
eauto.
Qed.
Corollary unnest_blocks_wc :
forall vars blocks blocks'
st st',
(
forall x, ~
IsLast vars x) ->
Forall (
wc_block G1 (
vars++
st_senv st))
blocks ->
unnest_blocks G1 blocks st = (
blocks',
st') ->
Forall (
wc_block G2 (
vars++
st_senv st'))
blocks'.
Proof with
eauto.
induction blocks;
intros *
Hnl Hwc Hnorm;
unfold unnest_blocks in *;
simpl in *;
repeat inv_bind;
simpl...
assert (
st_follows st x1)
as Hfollows1 by repeat solve_st_follows.
assert (
st_follows x1 st')
as Hfollows2 by repeat solve_st_follows.
inv Hwc.
eapply unnest_block_wc in H...
assert (
unnest_blocks G1 blocks x1 = (
concat x2,
st'))
as Hnorm.
{
unfold unnest_blocks;
repeat inv_bind;
eauto. }
apply IHblocks in Hnorm... 2:
solve_forall;
repeat solve_incl.
apply Forall_app;
split...
solve_forall;
repeat solve_incl.
Qed.
The produced environment is also well-clocked
Hypothesis HwcG1 :
wc_global G1.
Hypothesis HwcG2 :
wc_global G2.
Fact unnest_reset_wc_env :
forall vars e e'
eqs'
st st',
(
forall x, ~
IsLast vars x) ->
wc_env (
idck (
vars++
st_senv st)) ->
(
forall es'
eqs'
st0',
unnest_exp G1 true e st = (
es',
eqs',
st0') ->
st_follows st0'
st' ->
wc_env (
idck (
vars++
st_senv st0'))) ->
wc_exp G1 (
vars ++
st_senv st)
e ->
unnest_reset (
unnest_exp G1 true)
e st = (
e',
eqs',
st') ->
wc_env (
idck (
vars++
st_senv st')).
Proof with
eauto.
intros *
Hnl Hwenv Hun Hwc Hnorm.
unnest_reset_spec;
simpl in *;
eauto.
-
eapply Hun;
eauto;
repeat solve_st_follows.
-
eapply fresh_ident_wc_env in Hfresh;
eauto with fresh.
assert (
Hwc' :=
Hk0).
eapply unnest_exp_wc in Hwc'
as [
Hwc'
_];
eauto.
eapply wc_exp_clocksof in Hwc';
eauto with fresh.
destruct l;
simpl in *;
inv Hhd.
constructor.
apply Forall_app in Hwc'
as [
Hwc'
_].
rewrite clockof_annot in Hwc'.
destruct (
annot e0);
simpl in *.
inv H0;
constructor.
inv Hwc';
auto.
Qed.
Fact mmap2_wc_env {
A A1 A2 :
Type} :
forall vars (
k :
A ->
Unnesting.FreshAnn (
A1 *
A2))
a a1s a2s st st',
wc_env (
idck (
vars++
st_senv st)) ->
mmap2 k a st = (
a1s,
a2s,
st') ->
(
forall st st'
a es a2s,
k a st = (
es,
a2s,
st') ->
st_follows st st') ->
Forall (
fun a =>
forall a1s a2s st0 st0',
wc_env (
idck (
vars++
st_senv st0)) ->
k a st0 = (
a1s,
a2s,
st0') ->
st_follows st st0 ->
st_follows st0'
st' ->
wc_env (
idck (
vars++
st_senv st0')))
a ->
wc_env (
idck (
vars++
st_senv st')).
Proof with
eauto.
induction a;
intros a1s a2s st st'
Hclocks Hmap Hfollows Hf;
simpl in Hmap;
repeat inv_bind...
inv Hf.
specialize (
H3 _ _ _ _ Hclocks H).
eapply IHa in H3...
-
reflexivity.
-
eapply mmap2_st_follows...
solve_forall...
-
solve_forall.
eapply H2 in H5...
etransitivity...
Qed.
Corollary unnest_resets_wc_env :
forall vars es es'
eqs'
st st',
(
forall x, ~
IsLast vars x) ->
wc_env (
idck (
vars++
st_senv st)) ->
Forall (
fun e =>
forall es'
eqs'
st0 st0',
wc_env (
idck (
vars++
st_senv st0)) ->
unnest_exp G1 true e st0 = (
es',
eqs',
st0') ->
st_follows st st0 ->
st_follows st0'
st' ->
wc_env (
idck (
vars++
st_senv st0')))
es ->
Forall (
wc_exp G1 (
vars ++
st_senv st))
es ->
mmap2 (
unnest_reset (
unnest_exp G1 true))
es st = (
es',
eqs',
st') ->
wc_env (
idck (
vars++
st_senv st')).
Proof with
eauto.
induction es;
intros *
Hnl HwcE F Wc Map;
simpl in *;
inv F;
inv Wc;
repeat inv_bind;
eauto.
assert (
Map:=
H0).
eapply IHes in H0;
eauto. 3:
solve_forall;
repeat solve_incl.
2:
solve_forall;
eapply H9;
eauto;
repeat solve_st_follows.
eapply unnest_reset_wc_env in H;
eauto.
intros *
Un Follows.
eapply H1 in Un;
eauto. 1,2:
repeat solve_st_follows.
Qed.
Lemma unnest_noops_exps_wc_env :
forall vars cks es es'
eqs'
st st' ,
length es =
length cks ->
Forall normalized_lexp es ->
Forall (
fun e =>
numstreams e = 1)
es ->
Forall (
wc_exp G2 (
vars++
st_senv st))
es ->
wc_env (
idck (
vars++
st_senv st)) ->
unnest_noops_exps cks es st = (
es',
eqs',
st') ->
wc_env (
idck (
vars++
st_senv st')).
Proof.
Fact unnest_exp_wc_env :
forall vars e is_control es'
eqs'
st st',
(
forall x, ~
IsLast vars x) ->
wc_env (
idck (
vars++
st_senv st)) ->
wc_exp G1 (
vars++
st_senv st)
e ->
unnest_exp G1 is_control e st = (
es',
eqs',
st') ->
wc_env (
idck (
vars++
st_senv st')).
Proof with
Corollary mmap2_unnest_exp_wc_env :
forall vars es is_control es'
eqs'
st st',
(
forall x, ~
IsLast vars x) ->
wc_env (
idck (
vars++
st_senv st)) ->
Forall (
wc_exp G1 (
vars++
st_senv st))
es ->
mmap2 (
unnest_exp G1 is_control)
es st = (
es',
eqs',
st') ->
wc_env (
idck (
vars++
st_senv st')).
Proof.
intros *
Hnl Hwenv Hwc Hmmap.
eapply mmap2_wc_env in Hmmap;
eauto with norm.
simpl_Forall.
eapply unnest_exp_wc_env in H1;
eauto.
repeat solve_incl.
Qed.
Corollary unnest_exps_wc_env :
forall vars es es'
eqs'
st st',
(
forall x, ~
IsLast vars x) ->
wc_env (
idck (
vars++
st_senv st)) ->
Forall (
wc_exp G1 (
vars++
st_senv st))
es ->
unnest_exps G1 es st = (
es',
eqs',
st') ->
wc_env (
idck (
vars++
st_senv st')).
Proof with
Fact unnest_rhs_wc_env :
forall vars e es'
eqs'
st st',
(
forall x, ~
IsLast vars x) ->
wc_env (
idck (
vars++
st_senv st)) ->
wc_exp G1 (
vars++
st_senv st)
e ->
unnest_rhs G1 e st = (
es',
eqs',
st') ->
wc_env (
idck (
vars++
st_senv st')).
Proof with
Corollary unnest_rhss_wc_env :
forall vars es es'
eqs'
st st',
(
forall x, ~
IsLast vars x) ->
wc_env (
idck (
vars++
st_senv st)) ->
Forall (
wc_exp G1 (
vars++
st_senv st))
es ->
unnest_rhss G1 es st = (
es',
eqs',
st') ->
wc_env (
idck (
vars++
st_senv st')).
Proof with
Fact unnest_equation_wc_env :
forall vars e eqs'
st st',
(
forall x, ~
IsLast vars x) ->
wc_env (
idck (
vars++
st_senv st)) ->
wc_equation G1 (
vars++
st_senv st)
e ->
unnest_equation G1 e st = (
eqs',
st') ->
wc_env (
idck (
vars++
st_senv st')).
Proof with
Lemma unnest_block_wc_env :
forall vars d blocks'
st st' ,
(
forall x, ~
IsLast vars x) ->
wc_env (
idck (
vars++
st_senv st)) ->
wc_block G1 (
vars++
st_senv st)
d ->
unnest_block G1 d st = (
blocks',
st') ->
wc_env (
idck (
vars++
st_senv st')).
Proof.
induction d using block_ind2;
intros *
Hnl Hwenv Hwc Hnorm;
inv Hwc;
repeat inv_bind;
auto.
-
eapply unnest_equation_wc_env in H;
eauto.
-
assert (
wc_env (
idck (
vars ++
st_senv x0)))
as Hwenv'.
{
clear -
Hnl H H0 H2 Hwenv.
revert st x0 x H2 Hwenv H0.
induction H;
intros *
Hwc Hwenv Hmap;
inv Hwc;
repeat inv_bind;
auto.
eapply IHForall in H2;
eauto.
solve_forall;
repeat solve_incl. }
eapply unnest_reset_wc_env in H1;
eauto.
intros.
eapply unnest_exp_wc_env in H3;
eauto.
1,2:
repeat solve_incl.
Qed.
Corollary unnest_blocks_wc_env :
forall vars blocks blocks'
st st' ,
(
forall x, ~
IsLast vars x) ->
wc_env (
idck (
vars++
st_senv st)) ->
Forall (
wc_block G1 (
vars++
st_senv st))
blocks ->
unnest_blocks G1 blocks st = (
blocks',
st') ->
wc_env (
idck (
vars++
st_senv st')).
Proof with
eauto.
induction blocks;
intros *
Hnl Hwenv Hwc Hnorm;
unfold unnest_blocks in *;
simpl in *;
repeat inv_bind...
assert (
st_follows st x1)
as Hfollows1 by repeat solve_st_follows.
inv Hwc.
eapply unnest_block_wc_env in H...
assert (
unnest_blocks G1 blocks x1 = (
concat x2,
st'))
as Hnorm.
{
unfold unnest_blocks;
repeat inv_bind;
eauto. }
apply IHblocks in Hnorm as Hwenv2...
solve_forall;
repeat solve_incl.
Qed.
Lemma unnest_node_wc :
forall n,
wc_node G1 n ->
wc_node G2 (
unnest_node G1 n).
Proof with
eauto.
intros *
Wc.
inversion_clear Wc as [???
Hin Hout Hblk];
subst Γ.
unfold unnest_node.
pose proof (
n_syn n)
as Hsyn.
inversion_clear Hsyn as [??
Hsyn1 Hsyn2 _].
inv Hsyn2.
rewrite <-
H0 in *.
inv Hblk.
repeat constructor;
simpl;
auto.
1:{
simpl_Forall.
subst.
auto. }
assert (
forall x, ~
IsLast (
senv_of_ins (
n_in n) ++
senv_of_decls (
n_out n) ++
senv_of_decls locs)
x)
as Hnl.
{
repeat rewrite NoLast_app;
repeat split;
auto using senv_of_ins_NoLast.
-
intros *
Hl.
inv Hl.
simpl_In.
simpl_Forall.
subst;
simpl in *;
congruence.
-
intros *
Hl.
inv Hl.
simpl_In.
simpl_Forall.
subst;
simpl in *;
congruence. }
inv_scope;
subst Γ'.
rewrite <-
H0.
do 2
econstructor;
eauto.
-
destruct (
unnest_blocks _ _ _)
as (
eqs'&
st')
eqn:
Heqres.
eapply unnest_blocks_wc_env in Heqres as Henv'...
2,3:
unfold st_senv;
rewrite init_st_anns,
app_nil_r. 3:
eauto.
+
simpl_app.
unfold wc_env in Henv'.
repeat rewrite Forall_app in Henv'.
destruct Henv'
as (
_&
_&
_&
Henv').
eapply Forall_app.
split;
simpl_Forall;
simpl_app;
solve_incl.
1,2:
repeat rewrite map_map. 2:
erewrite map_ext with (
l:=
st_anns _). 1,2:
eapply incl_appr',
incl_appr'.
apply incl_appl,
incl_refl.
apply incl_refl.
intros;
destruct_conjs;
auto.
+
unfold wc_env in *.
simpl_app.
repeat rewrite Forall_app in *.
destruct Hin as (?&?).
repeat split;
simpl_Forall.
1-3:
eapply wc_clock_incl; [|
eauto]. 3:
reflexivity.
1,2:
repeat rewrite map_map.
erewrite map_ext.
eapply incl_appl,
incl_refl.
2:
erewrite map_ext,
map_ext with (
l:=
n_out n). 2:
eapply incl_appr',
incl_appl,
incl_refl.
all:
unfold decl;
intros;
destruct_conjs;
auto.
+
now rewrite app_assoc.
-
apply Forall_app;
split;
simpl_Forall;
subst;
auto.
-
destruct (
unnest_blocks _ _ _)
as (
eqs'&
st')
eqn:
Heqres.
eapply unnest_blocks_wc in Heqres as Hwc'...
2:
unfold st_senv;
rewrite init_st_anns,
app_nil_r;
now rewrite app_assoc.
simpl_app.
erewrite map_map,
map_ext with (
l:=
st_anns _);
eauto.
intros;
destruct_conjs;
auto.
Qed.
End unnest_node_wc.
Lemma unnest_global_wc :
forall G,
wc_global G ->
wc_global (
unnest_global G).
Proof.
Preservation of clocking through second pass
Section normfby_node_wc.
Variable G1 : @
global nolocal norm1_prefs.
Variable G2 : @
global nolocal norm2_prefs.
Hypothesis Hiface :
global_iface_incl G1 G2.
Local Hint Resolve iface_incl_wc_exp :
norm.
Fact fby_iteexp_wc_exp :
forall vars e0 e ty ck e'
eqs'
st st' ,
wc_exp G1 (
vars++
st_senv st)
e0 ->
wc_exp G1 (
vars++
st_senv st)
e ->
clockof e0 = [
ck] ->
clockof e = [
ck] ->
fby_iteexp e0 e (
ty,
ck)
st = (
e',
eqs',
st') ->
wc_exp G2 (
vars++
st_senv st')
e'.
Proof with
Fact arrow_iteexp_wc_exp :
forall vars e0 e ty ck e'
eqs'
st st' ,
wc_exp G1 (
vars++
st_senv st)
e0 ->
wc_exp G1 (
vars++
st_senv st)
e ->
clockof e0 = [
ck] ->
clockof e = [
ck] ->
arrow_iteexp e0 e (
ty,
ck)
st = (
e',
eqs',
st') ->
wc_exp G2 (
vars++
st_senv st')
e'.
Proof with
Fact init_var_for_clock_wc_env :
forall vars ck id eqs'
st st' ,
wc_env (
idck (
vars++
st_senv st)) ->
wc_clock (
idck (
vars++
st_senv st))
ck ->
init_var_for_clock ck st = (
id,
eqs',
st') ->
wc_env (
idck (
vars++
st_senv st')).
Proof with
Fact fby_iteexp_wc_env :
forall vars e0 e ty ck es'
eqs'
st st' ,
wc_env (
idck (
vars++
st_senv st)) ->
wc_clock (
idck (
vars++
st_senv st))
ck ->
fby_iteexp e0 e (
ty,
ck)
st = (
es',
eqs',
st') ->
wc_env (
idck (
vars++
st_senv st')).
Proof with
Fact init_var_for_clock_wc_eq :
forall vars ck id eqs'
st st' ,
wc_clock (
idck (
vars++
st_senv st))
ck ->
init_var_for_clock ck st = (
id,
eqs',
st') ->
Forall (
wc_equation G2 (
vars++
st_senv st'))
eqs'.
Proof with
Fact normalized_lexp_wc_exp_clockof :
forall vars e,
normalized_lexp e ->
wc_env (
idck vars) ->
wc_exp G2 vars e ->
Forall (
wc_clock (
idck vars)) (
clockof e).
Proof with
eauto.
intros vars e Hnormed Hwenv Hwc.
induction Hnormed;
inv Hwc;
simpl;
repeat constructor...
-
inv H0.
eapply Forall_forall in Hwenv;
eauto. 2:
solve_In.
auto.
-
eapply IHHnormed in H1.
rewrite H4 in H1.
inv H1...
-
eapply IHHnormed1 in H3.
rewrite H6 in H3.
inv H3...
-
apply Forall_singl in H5.
eapply IHHnormed in H5.
simpl in H7.
rewrite app_nil_r in H7.
symmetry in H7.
singleton_length.
inv H6.
inv H5...
-
inv H3.
solve_In.
Qed.
Fact fby_iteexp_wc_eq :
forall vars e0 e ty ck e'
eqs'
st st' ,
normalized_lexp e0 ->
wc_env (
idck (
vars++
st_senv st)) ->
wc_exp G1 (
vars++
st_senv st)
e0 ->
wc_exp G1 (
vars++
st_senv st)
e ->
clockof e0 = [
ck] ->
clockof e = [
ck] ->
fby_iteexp e0 e (
ty,
ck)
st = (
e',
eqs',
st') ->
Forall (
wc_equation G2 (
vars++
st_senv st'))
eqs'.
Proof with
Fact normfby_equation_wc :
forall vars to_cut eq eqs'
st st' ,
unnested_equation G1 eq ->
wc_env (
idck (
vars++
st_senv st)) ->
wc_equation G1 (
vars++
st_senv st)
eq ->
normfby_equation to_cut eq st = (
eqs',
st') ->
(
Forall (
wc_equation G2 (
vars++
st_senv st'))
eqs' /\
wc_env (
idck (
vars++
st_senv st'))).
Proof with
Fact normfby_block_wc :
forall vars to_cut d blocks'
st st' ,
unnested_block G1 d ->
wc_env (
idck (
vars++
st_senv st)) ->
wc_block G1 (
vars++
st_senv st)
d ->
normfby_block to_cut d st = (
blocks',
st') ->
Forall (
wc_block G2 (
vars++
st_senv st'))
blocks' /\
wc_env (
idck (
vars++
st_senv st')).
Proof.
Corollary normfby_blocks_wc :
forall vars to_cut blocks blocks'
st st' ,
Forall (
unnested_block G1)
blocks ->
wc_env (
idck (
vars++
st_senv st)) ->
Forall (
wc_block G1 (
vars++
st_senv st))
blocks ->
normfby_blocks to_cut blocks st = (
blocks',
st') ->
Forall (
wc_block G2 (
vars++
st_senv st'))
blocks' /\
wc_env (
idck (
vars++
st_senv st')).
Proof.
induction blocks;
intros *
Hunt Henv Hwc Hfby;
unfold normfby_blocks in *;
repeat inv_bind;
simpl;
auto.
inv Hunt.
inv Hwc.
assert (
normfby_blocks to_cut blocks x1 = (
concat x2,
st'))
as Hnorm.
{
unfold normfby_blocks.
repeat inv_bind;
eauto. }
assert (
H':=
H).
eapply normfby_block_wc in H as [
Hwc'
Henv'];
auto. 2,3:
eauto.
apply IHblocks in Hnorm as [
Hwc''
Henv''];
auto.
2:
solve_forall;
repeat solve_incl;
eapply normfby_block_st_follows in H';
eauto.
rewrite Forall_app;
repeat split;
eauto.
solve_forall;
repeat solve_incl.
Qed.
Lemma normfby_node_wc :
forall n,
unnested_node G1 n ->
wc_node G1 n ->
wc_node G2 (
normfby_node n).
Proof.
intros *
Hun Wc.
inversion_clear Wc as [???
Hin Hout Hblk];
subst Γ.
unfold unnest_node.
pose proof (
n_syn n)
as Hsyn.
inversion_clear Hsyn as [??
Hsyn1 Hsyn2 _].
inv Hsyn2.
rewrite <-
H0 in *.
inv Hblk.
repeat constructor;
simpl;
auto.
1:{
simpl_Forall.
subst.
auto. }
inv_scope;
subst Γ'.
rewrite <-
H0.
destruct (
normfby_blocks _ _ _)
as (
eqs'&
st')
eqn:
Heqres.
eapply normfby_blocks_wc in Heqres as (
Hres1&
Henv')...
3,4:
unfold st_senv;
rewrite init_st_anns,
app_nil_r. 4:
eauto.
3:{
unfold wc_env in *.
simpl_app.
repeat rewrite Forall_app in *.
destruct Hin as (?&?).
repeat split;
simpl_Forall.
1-3:
eapply wc_clock_incl; [|
eauto]. 3:
reflexivity.
1,2:
repeat rewrite map_map.
erewrite map_ext.
eapply incl_appl,
incl_refl.
2:
erewrite map_ext,
map_ext with (
l:=
n_out n). 2:
eapply incl_appr',
incl_appl,
incl_refl.
all:
unfold decl;
intros;
destruct_conjs;
auto. }
2:{
inv Hun.
rewrite H3 in H0.
now inv H0. }
do 2
econstructor;
eauto.
-
simpl_app.
unfold wc_env in Henv'.
repeat rewrite Forall_app in Henv'.
destruct Henv'
as (
_&
_&
_&
Henv').
eapply Forall_app.
split;
simpl_Forall;
simpl_app;
solve_incl.
1,2:
repeat rewrite map_map. 2:
erewrite map_ext with (
l:=
st_anns _). 1,2:
eapply incl_appr',
incl_appr'.
apply incl_appl,
incl_refl.
apply incl_refl.
intros;
destruct_conjs;
auto.
-
apply Forall_app;
split;
simpl_Forall;
subst;
auto.
-
simpl_Forall.
simpl_app.
erewrite map_map,
map_ext with (
l:=
st_anns _);
eauto.
intros;
destruct_conjs;
auto.
Qed.
End normfby_node_wc.
Lemma normfby_global_wc :
forall G,
unnested_global G ->
wc_global G ->
wc_global (
normfby_global G).
Proof.
Conclusion
Lemma normalize_global_wc :
forall G,
wc_global G ->
wc_global (
normalize_global G).
Proof.
End NCLOCKING.
Module NClockingFun
(
Ids :
IDS)
(
Op :
OPERATORS)
(
OpAux :
OPERATORS_AUX Ids Op)
(
Cks :
CLOCKS Ids Op OpAux)
(
Senv :
STATICENV Ids Op OpAux Cks)
(
Syn :
LSYNTAX Ids Op OpAux Cks Senv)
(
Clo :
LCLOCKING Ids Op OpAux Cks Senv Syn)
(
Norm :
NORMALIZATION Ids Op OpAux Cks Senv Syn)
<:
NCLOCKING Ids Op OpAux Cks Senv Syn Clo Norm.
Include NCLOCKING Ids Op OpAux Cks Senv Syn Clo Norm.
End NClockingFun.