intros ?????? [
xs [|? []]]
e' Hg Htr Hlasts Henvs Hxr Hnorm Hwt Hwcenv Hwc;
try (
inv Htr;
cases;
discriminate).
Opaque to_cexp.
destruct e;
inv Hwt;
simpl in *;
simpl_Foralls;
cases_eqn Eq;
try monadInv Htr.
all:
try (
inv Hwc;
simpl_Foralls;
eapply envs_eq_find in Henvs;
eauto;
rewrite Henvs in EQ;
inv EQ;
try rewrite app_nil_r in *;
take (
Senv.HasClock _ _ _)
and inv it;
econstructor;
eauto; [
eapply in_map_iff;
do 2
esplit;
eauto;
simpl;
auto;
take (
Senv.clo _ = _)
and rewrite it;
eauto|];
assert (
Hwce:=
EQ1);
eapply wc_cexp in Hwce as (?&?&?);
eauto;
simpl in *;
econstructor;
eauto;
congruence).
Transparent to_cexp.
3:
inv Hwc.
-
inv Hwc.
simpl_Forall.
take (
LC.wc_exp _ _ _)
and inv it.
take (
Senv.HasClock _ _ _)
and inv it.
solve_In.
repeat econstructor.
+
solve_In.
+
simpl_Forall.
eapply mmap_inversion,
Coqlib.list_forall2_in_right in EQ;
eauto;
destruct_conjs;
simpl_Forall.
eapply wc_lexp in H5 as (?&?&?);
eauto.
apply Forall_flat_map in H7.
simpl_Forall.
rewrite H5 in H7.
simpl_Forall;
auto.
-
inv Hnorm; [|
inv H1;
inv H].
inv Hwc.
simpl_Forall.
erewrite envs_eq_find in EQ0;
eauto.
inv EQ0.
take (
Senv.HasClock _ _ _)
and inv it.
assert (
Senv.causl_last e1 =
None)
as Nlast.
{
destruct (
Senv.causl_last e1)
eqn:
Causl;
auto.
exfalso.
take (~
In _
lasts)
and apply it,
Hlasts.
econstructor;
eauto.
congruence. }
constructor;
eauto.
+
solve_In.
rewrite Nlast.
auto.
+
take (
LC.wc_exp _ _ _)
and inv it.
simpl_Forall.
eapply wc_lexp in EQ2 as (?&
Heq &?);
eauto.
rewrite app_nil_r in *.
congruence.
+
simpl_Forall.
simpl_In.
esplit.
solve_In.
-
rename Eq into Vars.
eapply vars_of_spec in Vars.
clear H0 H3.
rename H9 into WIi.
rename H10 into WIo.
rename H12 into Hf2.
eapply find_node_global in Hg as (
n' &
Hfind &
Hton);
eauto.
assert (
find_base_clock (
L.clocksof l) =
bck)
as ->.
{
take (
L.find_node _ _ =
Some n)
and apply LC.wc_find_node in it as (?&
Wcn);
eauto.
inversion_clear Wcn as [?
Wcin _ _].
apply find_base_clock_bck.
-
rewrite L.clocksof_nclocksof;
eapply LC.WellInstantiated_bck;
eauto.
rewrite length_map;
exact (
L.n_ingt0 n).
-
apply LC.WellInstantiated_parent in WIi.
rewrite L.clocksof_nclocksof.
simpl_Forall;
eauto. }
eapply NLC.CEqApp;
eauto;
try discriminate.
+
eapply wc_equation_app_inputs with (
es:=
l) (
xs:=
xs);
eauto.
apply Forall2_length in Hf2.
apply Forall3_length in WIo as (
WIo&?).
unfold idfst,
idsnd in *.
repeat rewrite length_map in *.
setoid_rewrite WIo;
auto.
unfold idsnd,
idfst.
simpl_Forall.
eauto.
+
unfold idsnd in *.
erewrite <- (
to_node_out n n');
eauto.
unfold idfst in *.
simpl_Forall.
rewrite Forall3_map_1,
Forall3_map_2 in WIo.
eapply Forall2_swap_args,
Forall3_ignore1',
Forall3_Forall3 in Hf2. 2:
eapply WIo.
2:
apply Forall3_length in WIo as (?&?);
auto.
eapply Forall3_ignore2 in Hf2.
simpl_Forall.
inversion_clear H1 as [
Sub Inst].
simpl in *.
rewrite Sub.
split;
auto.
inv H2.
do 2
esplit.
split.
solve_In.
erewrite instck_sub_ext;
eauto.
+
eapply Forall_app;
split;
eauto.
2:
eapply Forall2_ignore1 in Vars. 1,2:
simpl_Forall.
*
simpl_In.
esplit.
solve_In.
*
subst.
inv H7.
take (
Senv.HasClock _ _ _)
and inv it.
esplit.
solve_In.
-
rename Eq into Vars.
eapply vars_of_spec in Vars.
clear H0 H3.
rename H4 into Hf2.
simpl in Hf2;
rewrite app_nil_r in Hf2.
simpl_Forall.
take (
LC.wc_exp _ _ _)
and inversion_clear it
as [| | | | | | | | | | | |?????
bck sub Wce Wcer ?
WIi WIo Ckr].
eapply find_node_global in Hg as (
n' &
Hfind &
Hton);
eauto.
assert (
find_base_clock (
L.clocksof l) =
bck)
as ->.
{
take (
L.find_node _ _ =
Some n)
and apply LC.wc_find_node in it as (?&
Wcn);
eauto.
inversion_clear Wcn as [?
Wcin _ _].
apply find_base_clock_bck.
-
rewrite L.clocksof_nclocksof;
eapply LC.WellInstantiated_bck;
eauto.
rewrite length_map;
exact (
L.n_ingt0 n).
-
apply LC.WellInstantiated_parent in WIi.
rewrite L.clocksof_nclocksof.
simpl_Forall;
eauto. }
eapply NLC.CEqApp;
eauto;
try discriminate.
+
eapply wc_equation_app_inputs with (
es:=
l) (
xs:=
xs);
eauto.
apply Forall2_length in Hf2.
apply Forall2_length in WIo.
1,2:
unfold idfst,
idsnd in *.
repeat rewrite length_map in *.
setoid_rewrite WIo;
auto.
simpl_Forall.
eauto.
+
unfold idsnd in *.
erewrite <- (
to_node_out n n');
eauto.
clear -
Hf2 WIo.
replace (
map _ (
L.n_out n))
with (
idsnd (
idfst (
idfst (
L.n_out n))))
in WIo.
2:{
unfold idfst,
idsnd.
erewrite 2
map_map,
map_ext;
eauto.
intros;
destruct_conjs;
auto. }
rewrite Forall2_map_2 in WIo.
eapply Forall3_ignore1' in Hf2.
eapply Forall3_ignore2' in WIo.
eapply Forall3_Forall3 in WIo;
eauto.
clear Hf2.
2:{
apply Forall3_length in Hf2 as (?&?).
repeat rewrite length_map in *;
auto. }
2:{
apply Forall2_length in Hf2.
apply Forall2_length in WIo.
congruence. }
apply Forall2_forall.
split.
2:{
apply Forall3_length in WIo as (?&?).
unfold idsnd,
idfst in *.
repeat rewrite length_map in *.
congruence. }
intros (?&(?&?)) ?
Hin.
split.
*
destruct (
sub i)
eqn:
Hsub.
--
eapply Forall3_ignore3,
Forall2_map_1,
Forall2_combine,
Forall_forall in WIo;
eauto;
simpl in *.
destruct WIo as ((?&?)&?&
Hsub'&?);
simpl in *.
rewrite Hsub in Hsub';
auto.
inv Hsub'.
--
unfold L.idents.
apply assoc_ident_true.
2:{
rewrite <-2
map_fst_idfst,
combine_map_fst,
in_map_iff.
esplit;
split;
eauto.
now simpl. }
apply NoDup_NoDupMembers_combine.
pose proof (
L.n_nodup n)
as (
Hdup&_);
eauto using NoDup_app_r.
*
eapply Forall3_ignore3,
Forall2_map_1,
Forall2_combine,
Forall_forall in WIo;
eauto.
destruct WIo as ((?&?)&?&?&?);
simpl in *.
take (
Senv.HasClock _ _ _)
and inv it.
do 2
esplit;
split;
eauto using instck_sub_ext.
solve_In.
+
eapply Forall_app;
split;
eauto.
2:
eapply Forall2_ignore1 in Vars. 1,2:
simpl_Forall.
*
simpl_In.
esplit.
solve_In.
*
subst.
inv Wcer.
take (
Senv.HasClock _ _ _)
and inv it.
esplit.
solve_In.
Qed.