From Coq Require Import String Morphisms.
From Coq Require Import List Permutation.
Import List.ListNotations.
Open Scope list_scope.
From Velus Require Import Common.
From Velus Require Import CommonList.
From Velus Require Import Environment.
From Velus Require Import FunctionalEnvironment.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax Lustre.LTyping Lustre.LCausality Lustre.LSemantics Lustre.LOrdered.
From Velus Require Import Lustre.Denot.Cpo.
Require Import SDfuns SD Restr Infty CommonList2.
Import List.
Module Type LDENOTINF
(
Import Ids :
IDS)
(
Import Op :
OPERATORS)
(
Import 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 Typ :
LTYPING Ids Op OpAux Cks Senv Syn)
(
Import LCA :
LCAUSALITY Ids Op OpAux Cks Senv Syn)
(
Import Lord :
LORDERED Ids Op OpAux Cks Senv Syn)
(
Import Restr :
LRESTR Ids Op OpAux Cks Senv Syn)
(
Import Den :
SD Ids Op OpAux Cks Senv Syn Lord).
Section Top.
Hypothesis HasCausInj :
forall Γ
x cx,
HasCaus Γ
x cx ->
cx =
x.
Lemma HasCausRefl :
forall Γ
x,
IsVar Γ
x ->
HasCaus Γ
x x.
Proof.
First we show that a well-formed node receiving streams of
length n outputs streams of length n.
Section Node_n.
Context {
PSyn :
list decl ->
block ->
Prop}.
Context {
Prefs :
PS.t}.
Variables
(
G : @
global PSyn Prefs)
(
envG :
Dprodi FI).
Fact idcaus_map :
forall l :
list (
ident * (
type *
clock *
ident)),
map snd (
idcaus l) =
map fst l.
Proof.
Fact idcaus_of_decls_map :
forall l :
list (
ident * (
type *
clock *
ident *
option ident)),
Forall (
fun '(
_, (
_,
_,
_,
o)) =>
o =
None)
l ->
map fst l =
map snd (
idcaus_of_decls l).
Proof.
Fact map_fst_idcaus_decls :
forall l,
Forall (
fun '(
_, (
_,
_,
_,
o)) =>
o =
None)
l ->
map fst (
idcaus_of_senv (
senv_of_decls l)) =
map fst l.
Proof.
Invariants pour l'induction causale
Definition P_var (
n :
nat) (
env :
DS_prod SI) (
x :
ident) :
Prop :=
is_ncons n (
PROJ _ x env).
Definition P_vars (
n :
nat) (
env :
DS_prod SI) (
cxs :
list ident) :
Prop :=
forall x,
In x cxs ->
P_var n env x.
Definition P_exp (
n :
nat)
ins envI env (
e :
exp) (
k :
nat) :
Prop :=
let ss :=
denot_exp G ins e envG envI env in
is_ncons n (
get_nth k errTy ss).
Hypothesis Hnode :
forall (
n :
nat) (
f :
ident) (
nd :
node) (
envI :
DS_prod SI),
find_node f G =
Some nd ->
(
P_vars n envI (
map fst (
n_in nd))) ->
(
P_vars n (
envG f envI) (
map fst (
n_out nd))).
Global Add Parametric Morphism n : (
P_var n)
with signature
Oeq (
O :=
DS_prod SI) ==>
eq ==>
iff as P_var_morph.
Proof.
unfold P_var.
intros ??
H ?.
now rewrite H.
Qed.
Global Add Parametric Morphism n : (
P_vars n)
with signature
Oeq (
O :=
DS_prod SI) ==>
eq ==>
iff as P_vars_morph.
Proof.
unfold P_vars.
intros ??
H ?.
now setoid_rewrite H.
Qed.
Lemma P_vars_In :
forall n env xs x,
P_vars n env xs ->
In x xs ->
P_var n env x.
Proof.
auto.
Qed.
Lemma P_var_S :
forall n env x,
P_var (
S n)
env x ->
P_var n env x.
Proof.
Lemma P_vars_S :
forall n env xs,
P_vars (
S n)
env xs ->
P_vars n env xs.
Proof.
Lemma P_vars_O :
forall env xs,
P_vars O env xs.
Proof.
induction xs; constructor; simpl; auto.
Qed.
Lemma P_vars_app_l :
forall n env xs ys,
P_vars n env (
xs ++
ys) ->
P_vars n env ys.
Proof.
Lemma P_vars_app_r :
forall n env xs ys,
P_vars n env (
xs ++
ys) ->
P_vars n env xs.
Proof.
Lemma P_exps_k :
forall n es ins envI env k,
P_exps (
P_exp n ins envI env)
es k ->
is_ncons n (
get_nth k errTy (
denot_exps G ins es envG envI env)).
Proof.
Lemma P_expss_k :
forall n (
ess :
list (
enumtag *
list exp))
ins envI env k m,
Forall (
fun es =>
length (
annots (
snd es)) =
m)
ess ->
Forall (
fun es =>
P_exps (
P_exp n ins envI env)
es k) (
map snd ess) ->
forall_nprod (
fun np =>
is_ncons n (
get_nth k errTy np))
(
denot_expss G ins ess m envG envI env).
Proof.
Lemma P_exps_impl :
forall Q (
P_exp :
exp ->
nat ->
Prop)
es k,
Forall Q es ->
P_exps (
fun e k =>
Q e ->
P_exp e k)
es k ->
P_exps P_exp es k.
Proof.
Lemma Forall_P_exps :
forall (
P_exp :
exp ->
nat ->
Prop)
es k,
Forall (
fun e =>
forall k,
k <
numstreams e ->
P_exp e k)
es ->
k <
list_sum (
map numstreams es) ->
P_exps P_exp es k.
Proof.
induction es as [|
e es];
simpl;
intros *
Hf Hk.
inv Hk.
inv Hf.
destruct (
Nat.lt_ge_cases k (
numstreams e));
auto using P_exps.
constructor 2;
auto.
apply IHes;
auto;
lia.
Qed.
Lemma Forall_P_expss :
forall (
P_exp :
exp ->
nat ->
Prop) (
ess :
list (
enumtag *
list exp))
k m,
Forall (
Forall (
fun e =>
forall k,
k <
numstreams e ->
P_exp e k)) (
map snd ess) ->
Forall (
fun es =>
length (
annots (
snd es)) =
m)
ess ->
k <
m ->
Forall (
fun es =>
P_exps P_exp es k) (
map snd ess).
Proof.
Lemma is_ncons_sbools_of :
forall n m (
np :
nprod m),
forall_nprod (
is_ncons n)
np ->
is_ncons n (
sbools_of np).
Proof.
Ltac solve_err :=
try (
rewrite annots_numstreams in *;
congruence)
;
try (
repeat (
rewrite get_nth_const; [|
simpl;
cases]);
match goal with
| |-
is_cons (
nrem _ (
Cpo_streams_type.map _ _)) =>
apply (
is_ncons_map _ _ _ _ (
S _));
auto 1
|
_ =>
idtac
end;
now (
apply is_ncons_DS_const ||
apply is_consn_DS_const)).
Lemma P_vars_env_of_np :
forall n l m (
mp :
nprod m),
forall_nprod (
is_ncons n)
mp ->
P_vars n (
env_of_np l mp)
l.
Proof.
Lemma P_vars_app :
forall n X Y l,
P_vars 1
X l ->
P_vars n Y l ->
P_vars (
S n) (
APP_env X Y)
l.
Proof.
Lemma P_vars_1 :
forall n X l,
P_vars (
S n)
X l ->
P_vars 1
X l.
Proof.
Lemma is_cons_sreset_aux :
forall (
f:
DS_prod SI -
C->
DS_prod SI)
ins outs R X Y,
(
forall envI,
P_vars 1
envI ins ->
P_vars 1 (
f envI)
outs) ->
is_cons R ->
P_vars 1
X ins ->
P_vars 1
Y outs ->
P_vars 1 (
sreset_aux f R X Y)
outs.
Proof.
Lemma is_ncons_sreset :
forall (
f:
DS_prod SI -
C->
DS_prod SI)
ins outs R X,
(
forall n envI,
P_vars n envI ins ->
P_vars n (
f envI)
outs) ->
forall n,
is_ncons n R ->
P_vars n X ins ->
P_vars n (
sreset f R X)
outs.
Proof.
Lemma is_ncons_bss :
forall n (
env :
DS_prod SI)
l,
P_vars n env l ->
is_ncons n (
bss l env).
Proof.
Lemma exp_n :
forall Γ
n e ins envI env k,
P_vars n envI ins ->
k <
numstreams e ->
restr_exp e ->
wl_exp G e ->
wx_exp Γ
e ->
(
forall x cx,
HasCaus Γ
x cx -> ~
In x ins ->
P_var n env cx) ->
P_exp n ins envI env e k.
Proof.
intros *
Hins.
intros Hk Hr Hwl Hwx Hn.
assert (
forall x,
IsVar Γ
x ->
is_ncons n (
denot_var ins envI env x))
as Hvar.
{
unfold P_vars,
P_var in Hins;
intros.
unfold denot_var.
cases_eqn HH.
*
rewrite mem_ident_spec in HH.
now apply Hins.
*
apply mem_ident_false in HH.
eapply Hn;
eauto using HasCausRefl.
}
revert dependent k.
induction e using exp_ind2;
simpl;
intros.
all:
unfold P_exp;
try now inv Hr.
-
assert (
k =
O)
by lia;
subst.
rewrite denot_exp_eq.
now apply is_ncons_sconst,
is_ncons_bss.
-
assert (
k0 =
O)
by lia;
subst.
rewrite denot_exp_eq.
now apply is_ncons_sconst,
is_ncons_bss.
-
assert (
k =
O)
by lia;
subst.
rewrite denot_exp_eq.
inv Hwx.
now apply Hvar.
-
assert (
k =
O)
by lia;
subst.
revert IHe.
rewrite denot_exp_eq.
unfold P_exp.
gen_sub_exps.
rewrite <-
length_typeof_numstreams.
inv Hr.
inv Hwl.
inv Hwx.
intros.
cases_eqn HH;
solve_err.
apply is_ncons_sunop.
unshelve eapply (
IHe _ _ _ O);
auto.
-
assert (
k =
O)
by lia;
subst.
revert IHe1 IHe2.
rewrite denot_exp_eq.
unfold P_exp.
gen_sub_exps.
rewrite <- 2
length_typeof_numstreams.
inv Hr.
inv Hwl.
inv Hwx.
intros.
cases_eqn HH;
solve_err.
apply is_ncons_sbinop.
unshelve eapply (
IHe1 _ _ _ O);
auto.
unshelve eapply (
IHe2 _ _ _ O);
auto.
-
rewrite denot_exp_eq;
simpl.
unfold eq_rect.
cases;
solve_err.
erewrite lift2_nth;
cases.
inv Hr.
apply Forall_impl_inside with (
P :=
restr_exp)
in H0,
H;
auto.
inv Hwl.
apply Forall_impl_inside with (
P :=
wl_exp _)
in H0,
H;
auto.
inv Hwx.
apply Forall_impl_inside with (
P :=
wx_exp _)
in H0,
H;
auto.
rewrite annots_numstreams in *.
apply is_ncons_fby;
apply P_exps_k,
Forall_P_exps;
auto;
congruence.
-
rewrite denot_exp_eq;
simpl.
unfold eq_rect.
cases;
solve_err.
erewrite llift_nth;
cases.
inv Hr.
apply Forall_impl_inside with (
P :=
restr_exp)
in H;
auto.
inv Hwl.
apply Forall_impl_inside with (
P :=
wl_exp _)
in H;
auto.
inv Hwx.
apply Forall_impl_inside with (
P :=
wx_exp _)
in H;
auto.
apply is_ncons_swhen;
auto.
now apply P_exps_k,
Forall_P_exps.
-
destruct x,
a.
inv Hr.
inv Hwl.
inv Hwx.
rewrite <-
Forall_map in *.
rewrite <-
Forall_concat,
map_map in *.
apply Forall_impl_inside with (
P :=
restr_exp)
in H;
auto.
apply Forall_impl_inside with (
P :=
wl_exp _)
in H;
auto.
apply Forall_impl_inside with (
P :=
wx_exp _)
in H;
auto.
rewrite Forall_concat in H.
eapply Forall_P_expss,
P_expss_k in H;
eauto.
rewrite denot_exp_eq;
simpl.
erewrite lift_nprod_nth;
auto.
apply is_ncons_smerge;
auto.
unfold eq_rect_r,
eq_rect,
eq_sym;
cases.
apply forall_nprod_lift;
eauto.
-
destruct a.
inv Hwl.
inv Hwx.
rewrite <-
Forall_map in *.
rewrite <-
Forall_concat in *.
apply Forall_impl_inside with (
P :=
restr_exp)
in H;
auto.
apply Forall_impl_inside with (
P :=
wl_exp _)
in H;
auto.
apply Forall_impl_inside with (
P :=
wx_exp _)
in H;
auto.
rewrite Forall_concat in H.
eapply Forall_P_expss,
P_expss_k in H;
eauto.
take (
wl_exp G e)
and apply IHe with (
k :=
O)
in it as Hc;
auto;
try lia.
2,3:
inv Hr;
rewrite <-
Forall_concat in *;
auto.
destruct d;
rewrite denot_exp_eq;
simpl.
+
inv Hr.
apply Forall_impl_inside with (
P :=
restr_exp)
in H0;
auto.
apply Forall_impl_inside with (
P :=
wl_exp _)
in H0;
auto.
apply Forall_impl_inside with (
P :=
wx_exp _)
in H0;
auto.
eapply Forall_P_exps with (
k :=
k),
P_exps_k in H0;
auto.
2:{
rewrite <-
annots_numstreams,
H13;
auto. }
revert H0 H Hc.
unfold P_exp.
gen_sub_exps.
unfold eq_rect_r,
eq_sym,
eq_rect.
cases;
try congruence;
intros;
solve_err.
setoid_rewrite lift_nprod_nth with (
F :=
scase_defv _ _);
auto.
rewrite @
lift_cons.
apply is_ncons_scase_def,
forall_nprod_cons,
forall_nprod_lift;
eauto.
+
revert Hc H.
unfold P_exp.
gen_sub_exps.
cases;
try congruence;
intros;
solve_err.
erewrite lift_nprod_nth;
auto.
apply is_ncons_scase;
auto.
unfold eq_rect_r,
eq_rect,
eq_sym;
cases.
apply forall_nprod_lift;
eauto.
-
rewrite denot_exp_eq;
simpl.
unfold eq_rect.
inv Hr.
apply Forall_impl_inside with (
P :=
restr_exp)
in H,
H0;
auto.
inv Hwl.
apply Forall_impl_inside with (
P :=
wl_exp _)
in H,
H0;
auto.
inv Hwx.
apply Forall_impl_inside with (
P :=
wx_exp _)
in H,
H0;
auto.
take (
find_node _ _ =
_)
and rewrite it;
cases;
solve_err.
apply forall_nprod_k;
auto.
apply forall_np_of_env';
setoid_rewrite <-
PROJ_simpl;
rewrite <-
Forall_forall.
eapply Forall_forall,
is_ncons_sreset;
eauto.
+
apply is_ncons_sbools_of.
apply k_forall_nprod_def with (
d :=
errTy);
intros;
solve_err.
now apply P_exps_k,
Forall_P_exps.
+
apply P_vars_env_of_np.
apply k_forall_nprod_def with (
d :=
errTy);
intros;
solve_err.
now apply P_exps_k,
Forall_P_exps.
Qed.
Lemma exps_n :
forall Γ
n es ins envI env k,
P_vars n envI ins ->
k <
list_sum (
map numstreams es) ->
Forall restr_exp es ->
Forall (
wl_exp G)
es ->
Forall (
wx_exp Γ)
es ->
(
forall x cx,
HasCaus Γ
x cx -> ~
In x ins ->
P_var n env cx) ->
P_exps (
P_exp n ins envI env)
es k.
Proof.
induction es as [|
e es];
simpl;
intros *
Hins Hk Hr Hwl Hwx Hn.
inv Hk.
simpl_Forall.
destruct (
Nat.lt_ge_cases k (
numstreams e)).
-
constructor;
eauto using exp_n.
-
constructor 2;
auto.
apply IHes;
auto;
lia.
Qed.
Lemma exp_S :
forall Γ
n e ins envI env k,
P_vars (
S n)
envI ins ->
k <
numstreams e ->
(
forall x,
Is_used_inst Γ
x k e -> ~
In x ins ->
P_var (
S n)
env x) ->
restr_exp e ->
wl_exp G e ->
wx_exp Γ
e ->
(
forall x cx,
HasCaus Γ
x cx -> ~
In x ins ->
P_var n env cx) ->
P_exp (
S n)
ins envI env e k.
Proof.
intros *
Hins Hk Hdep Hr Hwl Hwx Hn.
assert (
Hvar :
forall x cx,
HasCaus Γ
x cx ->
(~
In cx ins ->
P_var (
S n)
env cx) ->
is_ncons (
S n) (
denot_var ins envI env x)).
{
unfold P_vars,
P_var in Hins.
intros x cx Hc Hx.
unfold denot_var;
cases_eqn HH.
+
rewrite mem_ident_spec in HH.
now apply Hins.
+
apply mem_ident_false in HH.
apply HasCausInj in Hc;
subst.
now apply Hx.
}
assert (
Hwl' :=
Hwl).
assert (
Hwx' :=
Hwx).
revert Hwl Hwx Hr.
eapply exp_causal_ind with (16 :=
Hdep);
eauto.
all:
clear dependent e;
clear k;
intros;
unfold P_exp.
all:
try now inv Hr.
-
rewrite denot_exp_eq.
now apply is_ncons_sconst,
is_ncons_bss.
-
rewrite denot_exp_eq.
now apply is_ncons_sconst,
is_ncons_bss.
-
setoid_rewrite denot_exp_eq.
eapply Hvar;
eauto.
-
revert H.
rewrite denot_exp_eq.
unfold P_exp.
gen_sub_exps.
rewrite <-
length_typeof_numstreams.
inv Hr.
inv Hwl.
inv Hwx.
intros.
cases_eqn HH;
solve_err.
apply is_ncons_sunop;
auto.
-
revert H H0.
rewrite denot_exp_eq.
unfold P_exp.
gen_sub_exps.
rewrite <- 2
length_typeof_numstreams.
inv Hr.
inv Hwl.
inv Hwx.
intros.
cases_eqn HH;
solve_err.
apply is_ncons_sbinop;
auto.
-
rewrite denot_exp_eq;
simpl.
unfold eq_rect.
cases;
solve_err.
erewrite lift2_nth;
cases.
inv Hwl.
apply P_exps_impl in H0;
auto.
inv Hwx.
apply P_exps_impl in H0;
auto.
inv Hr.
apply P_exps_impl in H0;
auto.
apply is_ncons_S_fby;
apply P_exps_k;
auto.
eapply exps_n;
eauto using is_ncons_S,
P_vars_S.
-
rewrite denot_exp_eq;
simpl.
unfold eq_rect.
cases;
simpl in H;
solve_err.
inv Hwl.
apply P_exps_impl in H0;
auto.
inv Hwx.
apply P_exps_impl in H0;
auto.
inv Hr.
apply P_exps_impl in H0;
auto.
rewrite annots_numstreams in *.
erewrite llift_nth;
try congruence.
eapply is_ncons_swhen with (
n :=
S n);
eauto using P_exps_k.
-
destruct ann0.
rewrite denot_exp_eq;
simpl.
erewrite lift_nprod_nth;
auto.
eapply is_ncons_smerge with (
n :=
S n);
eauto.
apply forall_nprod_lift.
unfold eq_rect_r,
eq_rect,
eq_sym;
cases.
apply forall_denot_expss.
unfold eq_rect.
inv Hwl.
inv Hwx.
inv Hr.
simpl_Forall;
cases;
solve_err.
apply P_exps_k with (
n :=
S n).
apply P_exps_impl,
P_exps_impl,
P_exps_impl in H2;
auto.
-
destruct ann0.
inv Hwl.
inv Hwx.
take (
Forall (
fun _ =>
length _ =
_)
es)
and
eapply P_expss_k with (
n :=
S n)
in it as Hess;
eauto.
2:{
simpl_Forall.
eapply P_exps_impl in H1;
eauto.
eapply P_exps_impl in H1;
eauto.
eapply P_exps_impl in H1;
eauto.
inv Hr;
simpl_Forall;
auto.
}
destruct d;
rewrite denot_exp_eq;
simpl.
+
inv Hr.
apply P_exps_impl,
P_exps_impl,
P_exps_impl,
P_exps_k in H2;
auto.
revert H0 H2 Hess.
unfold P_exp.
gen_sub_exps.
cases;
intros;
solve_err.
setoid_rewrite lift_nprod_nth with (
F :=
scase_defv _ _);
auto.
unfold eq_rect_r,
eq_sym,
eq_rect;
cases.
rewrite @
lift_cons.
apply is_ncons_scase_def with (
n :=
S n),
forall_nprod_cons,
forall_nprod_lift;
eauto.
+
inv Hr.
revert H0 Hess.
unfold P_exp.
gen_sub_exps.
cases;
intros;
solve_err.
erewrite lift_nprod_nth;
auto.
eapply is_ncons_scase with (
n :=
S n);
auto.
apply forall_nprod_lift.
unfold eq_rect_r,
eq_rect,
eq_sym;
cases;
eauto.
-
rewrite denot_exp_eq;
simpl in *.
unfold eq_rect.
inv Hr;
inv Hwl;
inv Hwx.
destruct (
find_node f G)
eqn:?;
cases;
solve_err.
apply forall_nprod_k;
auto.
apply forall_np_of_env';
setoid_rewrite <-
PROJ_simpl.
eapply is_ncons_sreset with (
n :=
S n);
intros.
+
apply Hnode;
eauto using find_node_name.
+
apply is_ncons_sbools_of.
apply k_forall_nprod_def with (
d :=
errTy);
intros;
solve_err.
rewrite annots_numstreams in *.
apply P_exps_k;
eauto using P_exps_impl.
+
apply P_vars_env_of_np.
apply k_forall_nprod_def with (
d :=
errTy);
intros;
solve_err.
rewrite annots_numstreams in *.
apply P_exps_k;
eauto using P_exps_impl.
Qed.
Corollary exps_S :
forall Γ
n es ins envI env k,
P_vars (
S n)
envI ins ->
k <
list_sum (
map numstreams es) ->
(
forall x,
Is_used_inst_list Γ
x k es -> ~
In x ins ->
P_var (
S n)
env x) ->
Forall restr_exp es ->
Forall (
wl_exp G)
es ->
Forall (
wx_exp Γ)
es ->
(
forall x cx,
HasCaus Γ
x cx -> ~
In x ins ->
P_var n env cx) ->
P_exps (
P_exp (
S n)
ins envI env)
es k.
Proof.
induction es as [|
e es];
simpl;
intros;
try lia;
simpl_Forall.
destruct (
Nat.lt_ge_cases k (
numstreams e)).
-
apply P_exps_now;
auto.
eapply exp_S;
intros;
eauto.
take (
forall x,
_ ->
_)
and apply it;
auto;
left;
auto.
-
apply P_exps_later;
auto.
apply IHes;
auto;
try lia;
intros.
take (
forall x,
_ ->
_)
and apply it;
auto;
right;
auto.
Qed.
Lemma P_var_inside_blocks :
forall Γ
ins envI env blks x n,
Forall restr_block blks ->
Forall (
wl_block G)
blks ->
Forall (
wx_block Γ)
blks ->
P_vars (
S n)
envI ins ->
(
forall x cx :
ident,
HasCaus Γ
x cx -> ~
In x ins ->
P_var n env cx) ->
(
forall y,
Exists (
depends_on Γ
x y)
blks -> ~
In y ins ->
P_var (
S n)
env y) ->
Exists (
Syn.Is_defined_in (
Var x))
blks ->
P_var (
S n) (
denot_blocks G ins blks envG envI env)
x.
Proof.
Lemma HasCaus_In :
forall x cx Γ,
HasCaus Γ
x cx ->
In x (
map fst Γ).
Proof.
intros *
Hc.
inv Hc.
now apply (
in_map fst)
in H.
Qed.
Lemma locals_restr_blocks :
forall (
blks :
list block),
Forall restr_block blks ->
flat_map idcaus_of_locals blks = [].
Proof.
induction 1 as [|?? Hr]; auto; now inv Hr.
Qed.
Lemma get_idcaus_locals :
forall (
nd : @
node PSyn Prefs),
restr_node nd ->
map fst (
get_locals (
n_block nd)) =
map snd (
idcaus_of_locals (
n_block nd)).
Proof.
Lemma nin_defined :
forall (
n : @
node PSyn Prefs),
forall vars blks x,
n_block n =
Blocal (
Scope vars blks) ->
In x (
List.map fst (
senv_of_decls (
n_out n) ++
senv_of_decls vars)) ->
List.Exists (
Syn.Is_defined_in (
Var x))
blks.
Proof.
L'étape d'induction pour P_var sur les nœuds, qui utilise exp_S.
Lemma denot_S :
forall nd envI n,
restr_node nd ->
wl_node G nd ->
wx_node nd ->
node_causal nd ->
P_vars (
S n)
envI (
map fst (
n_in nd)) ->
P_vars n (
FIXP _ (
denot_node G nd envG envI)) (
map fst (
n_out nd) ++
map fst (
get_locals (
n_block nd))) ->
P_vars (
S n) (
FIXP _ (
denot_node G nd envG envI)) (
map fst (
n_out nd) ++
map fst (
get_locals (
n_block nd))).
Proof.
intros *
Hr Hwl Hwx Hcaus Hins.
set (
ins :=
map fst (
n_in nd))
in *.
set (
env :=
FIXP _ _).
intro Hn.
eapply node_causal_ind
with (
P_vars :=
fun l =>
forall x,
In x l -> ~
In x ins ->
P_var (
S n)
env x)
in Hcaus as (
lord &
Perm3 &
Hlord).
-
intros x Hin;
apply Hlord.
+
inversion Hr;
subst.
rewrite Perm3, 2
map_app, <-
idcaus_of_decls_map, <-
get_idcaus_locals;
auto.
rewrite 2
in_app_iff in *;
tauto.
+
pose proof (
Nd :=
NoDup_iol nd).
apply fst_NoDupMembers in Nd.
rewrite 2
map_app,
Permutation_app_comm,
map_fst_senv_of_ins,
map_fst_senv_of_decls in Nd.
eapply NoDup_app_In in Nd;
eauto.
-
inversion 1.
-
intros y ys Hxin Hys Hdep.
intros x []
Hxnins;
subst;
auto.
rewrite <-
in_app_iff,
map_app, <-
app_assoc,
in_app_iff in Hxin.
destruct Hxin as [
Hxin|
Hxin].
+
rewrite idcaus_map in Hxin;
contradiction.
+
inv Hwx;
inv Hwl.
inversion_clear Hr as [??
Hrtb ?].
inversion Hrtb as [????
Hnd].
rewrite <-
Hnd in *;
simpl in Hxin,
Hn.
rewrite locals_restr_blocks,
app_nil_r in Hxin;
auto.
unfold env;
rewrite FIXP_eq;
fold env.
rewrite denot_node_eq,
denot_top_block_eq, <-
Hnd.
take (
wl_block _ _)
and inv it.
take (
wl_scope _ _ _)
and inv it.
take (
wx_block _ _)
and inv it.
take (
wx_scope _ _ _)
and inv it.
eapply P_var_inside_blocks;
eauto.
*
subst Γ' Γ;
intros y cy Hin Hnins.
apply HasCausInj in Hin as ?;
subst.
apply HasCaus_In in Hin.
rewrite 2
map_app, 2
map_fst_senv_of_decls,
map_fst_senv_of_ins, <-
app_assoc in *.
apply in_app_or in Hin as [];
auto;
contradiction.
*
intros y Hex Hnins.
apply Hys in Hnins;
auto;
apply Hdep.
constructor;
rewrite <-
Hnd;
constructor;
econstructor;
eauto.
*
rewrite <- 2
idcaus_of_decls_map in Hxin;
auto.
eapply nin_defined;
eauto.
now rewrite map_app, 2
map_fst_senv_of_decls.
Qed.
Theorem denot_n :
forall nd envI n,
restr_node nd ->
wl_node G nd ->
wx_node nd ->
node_causal nd ->
P_vars n envI (
map fst (
n_in nd)) ->
P_vars n (
FIXP _ (
denot_node G nd envG envI)) (
map fst (
n_out nd) ++
map fst (
get_locals (
n_block nd))).
Proof.
intros *
Hr Hwl Hwx Hcaus Hins.
revert Hr Hwl Hwx Hcaus Hins.
revert nd envI.
induction n;
intros.
-
apply P_vars_O.
-
apply denot_S;
auto.
apply IHn;
auto using P_vars_S.
Qed.
End Node_n.
Using the well-ordered property of programs, show that all nodes
receiving streams of length n outputs streams of length n.
Theorem denot_global_n :
forall {
PSyn Prefs} (
G : @
global PSyn Prefs),
forall n f nd envI,
restr_global G ->
wt_global G ->
Forall node_causal (
nodes G) ->
find_node f G =
Some nd ->
P_vars n envI (
map fst (
n_in nd)) ->
P_vars n (
denot_global G f envI) (
map fst (
n_out nd) ++
map fst (
get_locals (
n_block nd))).
Proof.
intros *
Hr Hwt Hcaus Hfind Hins.
assert (
Ordered_nodes G)
as Hord.
now apply wl_global_Ordered_nodes,
wt_global_wl_global.
unfold denot_global.
rewrite <-
PROJ_simpl,
FIXP_eq,
PROJ_simpl,
denot_global_eq.
rewrite Hfind.
remember (
FIXP (
Dprodi FI) (
denot_global_ G))
as envG eqn:
HF.
assert (
forall f nd envI,
find_node f G =
Some nd ->
envG f envI ==
FIXP _ (
denot_node G nd envG envI))
as HenvG.
{
intros *
Hf;
subst.
now rewrite <-
PROJ_simpl,
FIXP_eq,
PROJ_simpl,
denot_global_eq,
Hf at 1. }
clear HF.
revert Hins HenvG Hfind.
revert envI envG n f nd.
destruct G as [
tys exts nds];
simpl in *.
induction nds as [|
a nds];
simpl;
intros.
inv Hfind.
inv Hcaus.
inv Hr.
destruct (
ident_eq_dec (
n_name a)
f);
subst.
+
rewrite find_node_now in Hfind;
inv Hfind;
auto.
rewrite <-
denot_node_cons;
eauto using find_node_not_Is_node_in,
find_node_now.
apply denot_n;
eauto using wt_global_uncons,
wt_node_wl_node,
wt_node_wx_node.
intros m f nd2 envI2 Hfind2 HI2.
eapply find_node_uncons with (
nd :=
nd)
in Hfind2 as ?;
auto.
rewrite HenvG, <-
denot_node_cons;
eauto using find_node_later_not_Is_node_in.
eapply P_vars_app_r.
apply IHnds with (
f :=
f);
auto.
eauto using wt_global_cons.
eauto using Ordered_nodes_cons.
intros f'
ndf'
envI'
Hfind'.
eapply find_node_uncons with (
nd :=
nd)
in Hfind'
as ?;
auto.
rewrite HenvG, <-
denot_node_cons;
eauto using find_node_later_not_Is_node_in.
+
rewrite find_node_other in Hfind;
auto.
rewrite <-
denot_node_cons;
eauto using find_node_later_not_Is_node_in.
apply IHnds with (
f :=
f);
auto.
eauto using wt_global_cons.
eauto using Ordered_nodes_cons.
intros f'
ndf'
envI'
Hfind'.
eapply find_node_uncons with (
nd :=
a)
in Hfind'
as ?;
auto.
rewrite HenvG, <-
denot_node_cons;
eauto using find_node_later_not_Is_node_in.
Qed.
End Top.
Section MOVE_ME.
Lemma inf_dom_env_of_np :
forall l m (
mp :
nprod m),
forall_nprod (@
infinite _)
mp ->
infinite_dom (
env_of_np l mp)
l.
Proof.
End MOVE_ME.
Maintenant on passe à l'infini
Lemma infinite_P_vars :
forall env l,
infinite_dom env l <-> (
forall n,
P_vars n env l).
Proof.
Theorem denot_inf :
forall (
HasCausInj :
forall Γ
x cx,
HasCaus Γ
x cx ->
cx =
x),
forall {
PSyn Prefs} (
G : @
global PSyn Prefs),
restr_global G ->
wt_global G ->
Forall node_causal (
nodes G) ->
forall f nd envI,
find_node f G =
Some nd ->
infinite_dom envI (
List.map fst (
n_in nd)) ->
infinite_dom (
denot_global G f envI) (
List.map fst (
n_out nd) ++
map fst (
get_locals (
n_block nd))).
Proof.
Lemma sbools_ofs_inf :
forall n (
np :
nprod n),
forall_nprod (@
infinite _)
np ->
infinite (
sbools_of np).
Proof.
Une fois l'infinité des flots obtenue, on peut l'utiliser pour
prouver l'infinité des expressions.
Lemma infinite_exp :
forall {
PSyn Prefs} (
G : @
global PSyn Prefs),
forall ins envI (
envG :
Dprodi FI)
env,
(
forall f nd envI,
find_node f G =
Some nd ->
infinite_dom envI (
List.map fst (
n_in nd)) ->
infinite_dom (
envG f envI) (
List.map fst (
n_out nd))) ->
infinite (
bss ins envI) ->
forall Γ, (
forall x,
IsVar Γ
x ->
infinite (
denot_var ins envI env x)) ->
forall e,
restr_exp e ->
wx_exp Γ
e ->
wl_exp G e ->
forall_nprod (@
infinite _) (
denot_exp G ins e envG envI env).
Proof.
intros *
HG bsi ?
Hvar e Hr Hwx Hwl.
induction e using exp_ind2;
inv Hr;
inv Hwx;
inv Hwl.
all:
simpl;
setoid_rewrite denot_exp_eq;
auto.
-
apply sconst_inf;
auto.
-
apply sconst_inf;
auto.
-
revert IHe.
gen_sub_exps.
intros;
cases;
simpl in *;
eauto using sunop_inf,
DS_const_inf.
-
revert IHe1 IHe2.
gen_sub_exps.
intros;
cases;
simpl in *;
eauto using sbinop_inf,
DS_const_inf.
-
apply Forall_impl_inside with (
P :=
restr_exp)
in H0,
H;
auto.
apply Forall_impl_inside with (
P :=
wx_exp _)
in H0,
H;
auto.
apply Forall_impl_inside with (
P :=
wl_exp _)
in H0,
H;
auto.
apply forall_denot_exps in H,
H0.
unfold eq_rect.
cases;
eauto using forall_nprod_const,
DS_const_inf.
eapply forall_nprod_lift2;
eauto using fby_inf;
cases.
-
apply Forall_impl_inside with (
P :=
restr_exp)
in H;
auto.
apply Forall_impl_inside with (
P :=
wx_exp _)
in H;
auto.
apply Forall_impl_inside with (
P :=
wl_exp _)
in H;
auto.
apply forall_denot_exps in H.
unfold eq_rect.
cases;
eauto using forall_nprod_const,
DS_const_inf.
eapply forall_nprod_llift;
eauto using swhen_inf;
cases.
-
eapply forall_lift_nprod;
eauto using smerge_inf.
unfold eq_rect_r,
eq_rect,
eq_sym;
cases.
apply forall_denot_expss.
unfold eq_rect.
simpl_Forall.
apply Forall_impl_inside with (
P :=
restr_exp)
in H;
auto.
apply Forall_impl_inside with (
P :=
wx_exp _)
in H;
auto.
apply Forall_impl_inside with (
P :=
wl_exp _)
in H;
auto.
cases.
+
now apply forall_denot_exps.
+
rewrite annots_numstreams in *;
congruence.
-
eapply Forall_impl_In in H.
2:{
intros ?
Hin HH.
apply Forall_impl_inside with (
P :=
restr_exp)
in HH;[|
now simpl_Forall].
apply Forall_impl_inside with (
P :=
wx_exp _)
in HH;[|
now simpl_Forall].
apply Forall_impl_inside with (
P :=
wl_exp _)
in HH;[|
now simpl_Forall].
eapply (
proj2 (
forall_denot_exps _ _ _ _ _ _ _ )),
HH. }
eapply forall_forall_denot_expss with (
n :=
length tys)
in H as Hess;
auto.
revert Hess IHe.
gen_sub_exps.
unfold eq_rect_r;
cases;
intros;
eauto using forall_nprod_const,
DS_const_inf.
simpl in *|-.
eapply forall_lift_nprod;
eauto using scase_inf.
unfold eq_rect,
eq_sym;
cases.
-
eapply Forall_impl_In in H.
2:{
intros ?
Hin HH.
apply Forall_impl_inside with (
P :=
restr_exp)
in HH;[|
now simpl_Forall].
apply Forall_impl_inside with (
P :=
wx_exp _)
in HH;[|
now simpl_Forall].
apply Forall_impl_inside with (
P :=
wl_exp _)
in HH;[|
now simpl_Forall].
eapply (
proj2 (
forall_denot_exps _ _ _ _ _ _ _ )),
HH. }
eapply forall_forall_denot_expss with (
n :=
length tys)
in H as Hess;
auto.
apply Forall_impl_inside with (
P :=
restr_exp)
in H0;
auto.
apply Forall_impl_inside with (
P :=
wx_exp _)
in H0;
auto.
apply Forall_impl_inside with (
P :=
wl_exp _)
in H0;
auto.
apply forall_denot_exps in H0 as Hd.
revert Hess IHe Hd.
gen_sub_exps.
unfold eq_rect_r,
eq_rect,
eq_sym;
cases;
intros;
eauto using forall_nprod_const,
DS_const_inf.
simpl in *|-.
eapply forall_lift_nprod;
eauto using scase_def_inf,
forall_nprod_cons.
-
apply Forall_impl_inside with (
P :=
restr_exp)
in H,
H0;
auto.
apply Forall_impl_inside with (
P :=
wx_exp _)
in H,
H0;
auto.
apply Forall_impl_inside with (
P :=
wl_exp _)
in H,
H0;
auto.
apply forall_denot_exps in H,
H0.
unfold eq_rect.
take (
find_node _ _ =
_)
and rewrite it.
cases;
eauto using forall_nprod_const,
DS_const_inf.
apply forall_np_of_env';
intros x Hxout.
eapply sreset_inf_dom;
eauto.
+
apply sbools_ofs_inf;
auto.
+
apply inf_dom_env_of_np;
auto.
Qed.
Corollary infinite_exps :
forall {
PSyn Prefs} (
G : @
global PSyn Prefs),
forall ins (
envG :
Dprodi FI)
envI env,
(
forall f nd envI,
find_node f G =
Some nd ->
infinite_dom envI (
List.map fst (
n_in nd)) ->
infinite_dom (
envG f envI) (
List.map fst (
n_out nd))) ->
infinite (
bss ins envI) ->
forall Γ, (
forall x,
IsVar Γ
x ->
infinite (
denot_var ins envI env x)) ->
forall es,
Forall restr_exp es ->
Forall (
wx_exp Γ)
es ->
Forall (
wl_exp G)
es ->
forall_nprod (@
infinite _) (
denot_exps G ins es envG envI env).
Proof.
Corollary infinite_expss :
forall {
PSyn Prefs} (
G : @
global PSyn Prefs),
forall ins (
envG :
Dprodi FI)
envI env,
(
forall f nd envI,
find_node f G =
Some nd ->
infinite_dom envI (
List.map fst (
n_in nd)) ->
infinite_dom (
envG f envI) (
List.map fst (
n_out nd))) ->
infinite (
bss ins envI) ->
forall Γ, (
forall x,
IsVar Γ
x ->
infinite (
denot_var ins envI env x)) ->
forall I (
ess :
list (
I *
list exp))
n,
Forall (
Forall restr_exp) (
map snd ess) ->
Forall (
fun es =>
Forall (
wx_exp Γ) (
snd es))
ess ->
Forall (
fun es =>
Forall (
wl_exp G) (
snd es))
ess ->
Forall (
fun es =>
length (
annots (
snd es)) =
n)
ess ->
forall_nprod (
forall_nprod (@
infinite _)) (
denot_expss G ins ess n envG envI env).
Proof.
End LDENOTINF.
Module LDenotInfFun
(
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)
(
Typ :
LTYPING Ids Op OpAux Cks Senv Syn)
(
LCA :
LCAUSALITY Ids Op OpAux Cks Senv Syn)
(
Lord :
LORDERED Ids Op OpAux Cks Senv Syn)
(
Restr :
LRESTR Ids Op OpAux Cks Senv Syn)
(
Den :
SD Ids Op OpAux Cks Senv Syn Lord)
<:
LDENOTINF Ids Op OpAux Cks Senv Syn Typ LCA Lord Restr Den.
Include LDENOTINF Ids Op OpAux Cks Senv Syn Typ LCA Lord Restr Den.
End LDenotInfFun.