From Velus Require Import Common.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Coq Require Import PArith.
From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.
From Velus Require Import CoreExpr.CESyntax.
From Velus Require Import NLustre.NLSyntax.
From Coq Require Import Morphisms.
From Coq Require Import Permutation.
Collecting memory cells
Module Type MEMORIES
(
Ids :
IDS)
(
Op :
OPERATORS)
(
Import CESyn :
CESYNTAX Op)
(
Import Syn :
NLSYNTAX Ids Op CESyn).
Definition memory_eq (
mems:
PS.t) (
eq:
equation) :
PS.t :=
match eq with
|
EqFby x _ _ _ =>
PS.add x mems
|
_ =>
mems
end.
Definition memories (
eqs:
list equation) :
PS.t :=
List.fold_left memory_eq eqs PS.empty.
Properties
Lemma In_fold_left_memory_eq:
forall x eqs m,
PS.In x (
fold_left memory_eq eqs m)
<->
PS.In x (
fold_left memory_eq eqs PS.empty) \/
PS.In x m.
Proof.
induction eqs as [|
eq];
simpl.
-
split;
auto.
intros [
Hin|];
auto.
apply not_In_empty in Hin;
contradiction.
-
setoid_rewrite IHeqs;
split.
+
intros [?|
Hin];
auto.
destruct eq;
simpl;
auto.
apply PS.add_spec in Hin as [|];
auto.
subst;
rewrite PS.add_spec;
auto.
+
intros [[?|
Hin]|?];
auto.
*
destruct eq;
simpl;
try (
apply not_In_empty in Hin;
contradiction).
apply PS.add_spec in Hin as [|
Hin];
try (
apply not_In_empty in Hin;
contradiction).
subst;
rewrite PS.add_spec;
auto.
*
destruct eq;
simpl;
auto.
rewrite PS.add_spec;
auto.
Qed.
Instance List_fold_left_memory_eq_Proper (
eqs:
list equation) :
Proper (
PS.eq ==>
PS.eq) (
fold_left memory_eq eqs).
Proof.
induction eqs as [|[]]; intros * ?? E; simpl; auto.
apply IHeqs; rewrite E; reflexivity.
Qed.
Lemma in_memories_var_defined:
forall x eqs,
PS.In x (
memories eqs) ->
In x (
vars_defined eqs).
Proof.
Lemma in_memories_is_fby:
forall eqs eq,
In eq eqs ->
NoDup (
vars_defined eqs) ->
forall x,
In x (
var_defined eq) ->
PS.mem x (
memories eqs) =
is_fby eq.
Proof.
Lemma in_memories_filter_is_fby:
forall x eqs,
PS.In x (
memories eqs) <->
In x (
vars_defined (
filter is_fby eqs)).
Proof.
Remark filter_mem_fst:
forall A B p (
xs:
list (
ident * (
A *
B))),
map fst (
filter (
fun (
x:
ident*(
A*
B)) =>
PS.mem (
fst x)
p)
xs)
=
filter (
fun x =>
PS.mem x p) (
map fst xs).
Proof.
induction xs as [|
x xs];
auto.
simpl.
destruct (
PS.mem (
fst x)
p);
simpl;
now rewrite IHxs.
Qed.
Lemma notb_filter_mem_fst:
forall A B p (
xs:
list (
ident * (
A *
B))),
map fst (
filter (
notb (
fun (
x:
ident*(
A*
B)) =>
PS.mem (
fst x)
p))
xs)
=
filter (
notb (
fun x =>
PS.mem x p)) (
map fst xs).
Proof.
unfold notb;
simpl.
induction xs as [|
x xs];
auto;
simpl.
destruct (
negb (
PS.mem (
fst x)
p));
simpl;
now rewrite IHxs.
Qed.
Lemma fst_partition_memories_var_defined:
forall n,
Permutation
(
map fst (
fst (
partition
(
fun x =>
PS.mem (
fst x) (
memories n.(
n_eqs)))
n.(
n_vars))))
(
vars_defined (
filter is_fby n.(
n_eqs))).
Proof.
Lemma snd_partition_memories_var_defined:
forall n,
Permutation
(
map fst (
snd (
partition
(
fun x =>
PS.mem (
fst x) (
memories n.(
n_eqs)))
n.(
n_vars)) ++
n.(
n_out)))
(
vars_defined (
filter (
notb is_fby)
n.(
n_eqs))).
Proof.
intro n.
match goal with |-
Permutation (
map fst (
snd (
partition ?
p ?
l) ++
_))
_ =>
assert (
Permutation (
map fst (
snd (
partition p l)))
(
map fst (
filter (
notb p)
n.(
n_vars))))
as Hperm by (
now rewrite snd_partition_filter)
end.
rewrite map_app,
Hperm, <-
map_app;
clear Hperm.
assert (
filter (
notb (
fun x =>
PS.mem (
fst x) (
memories n.(
n_eqs))))
n.(
n_out) =
n.(
n_out))
as Hfout.
{
simpl.
pose proof (
n_vout n)
as Out.
setoid_rewrite <-
in_memories_filter_is_fby in Out.
unfold notb.
induction (
n_out n)
as [|(
x,
t)];
simpl;
auto.
destruct (
PS.mem x (
memories (
n_eqs n)))
eqn:
E;
simpl.
-
apply PSE.MP.Dec.F.mem_iff in E.
exfalso;
eapply Out;
eauto.
simpl;
auto.
-
rewrite IHl;
auto.
intros ???;
eapply Out;
eauto.
simpl;
auto.
}
rewrite <-
Hfout;
clear Hfout.
rewrite filter_app,
notb_filter_mem_fst, <-
n_defd.
remember (
memories n.(
n_eqs))
as mems.
set (
P :=
fun eqs eq =>
In eq eqs ->
forall x,
In x (
var_defined eq) ->
PS.mem x mems =
is_fby eq).
assert (
forall eq,
P n.(
n_eqs)
eq)
as Peq.
{
subst P mems.
intro.
intro Hin.
apply in_memories_is_fby;
auto.
rewrite n_defd.
apply fst_NoDupMembers.
pose proof (
n.(
n_nodup))
as Hnodup.
now apply NoDupMembers_app_r in Hnodup.
}
clear Heqmems.
unfold notb,
vars_defined.
induction n.(
n_eqs)
as [|
eq eqs];
auto.
assert (
forall eq,
P eqs eq)
as Peq'
by (
intros e Hin;
apply Peq;
now constructor 2).
specialize (
IHeqs Peq').
clear Peq'.
destruct eq eqn:
Heq;
simpl;
specialize (
Peq eq);
red in Peq;
subst eq;
simpl in Peq.
+
rewrite Peq;
eauto.
simpl;
auto.
+
assert (
Hmem_in:
forall x,
In x l ->
PS.mem x mems =
false)
by now apply Peq;
eauto.
assert (
Hfilter:
filter (
fun x =>
negb (
PS.mem x mems))
l =
l).
{
clear -
Hmem_in.
induction l as [ |
a i IHi] ;
auto;
simpl.
rewrite Hmem_in;
simpl;
try now constructor.
rewrite IHi;
auto.
intros.
apply Hmem_in.
now constructor 2.
}
rewrite <-
filter_app;
setoid_rewrite Hfilter.
apply Permutation_app_head;
auto.
+
rewrite Peq;
eauto.
Qed.
End MEMORIES.
Module MemoriesFun
(
Ids :
IDS)
(
Op :
OPERATORS)
(
CESyn :
CESYNTAX Op)
(
Syn :
NLSYNTAX Ids Op CESyn)
<:
MEMORIES Ids Op CESyn Syn.
Include MEMORIES Ids Op CESyn Syn.
End MemoriesFun.