From Coq Require Import BinPos List.
From Velus Require Import Common Ident Operators Clocks CoindStreams.
From Velus Require Import Lustre.StaticEnv Lustre.LSyntax Lustre.LSemantics Lustre.LOrdered.
From Velus Require Import Lustre.Denot.Cpo.
Close Scope equiv_scope.
Import ListNotations.
Require Import CommonList2.
Require Import SDfuns.
Module Type SD
(
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 Lord :
LORDERED Ids Op OpAux Cks Senv Syn).
Section LSyntax_facts.
Definition get_locals (
blk :
block) :
static_env :=
match blk with
|
Blocal (
Scope vars _) =>
senv_of_decls vars
| _ => []
end.
Lemma NoDup_senv_loc :
forall {
PSyn Prefs},
forall (
nd : @
node PSyn Prefs)
vars blks,
n_block nd =
Blocal (
Scope vars blks) ->
NoDupMembers (
senv_of_ins (
n_in nd) ++
senv_of_decls (
n_out nd) ++
senv_of_decls vars).
Proof.
Corollary NoDup_iol :
forall {
PSyn Prefs},
forall (
n : @
node PSyn Prefs),
NoDupMembers (
senv_of_ins (
n_in n) ++
senv_of_decls (
n_out n) ++
get_locals (
n_block n)).
Proof.
Chercher les variables à gauche des équations dans les blocks
Definition get_defined (
blk :
block) :
list ident :=
match blk with
|
Beq (
xs,
es) =>
xs
| _ => []
end.
Et dans les nœuds
Definition get_defined_node {
PSyn Prefs} (
n : @
node PSyn Prefs) :
list ident :=
match n_block n with
|
Blocal (
Scope _
blks) =>
flat_map get_defined blks
| _ => []
end.
Lemma NoDup_get_defined :
forall {
PSyn Prefs},
forall (
nd : @
node PSyn Prefs)
vars blks,
n_block nd =
Blocal (
Scope vars blks) ->
NoDup (
flat_map get_defined blks ++
List.map fst (
n_in nd)).
Proof.
Corollary NoDup_get_defined_node :
forall {
PSyn Prefs},
forall (
nd : @
node PSyn Prefs),
NoDup (
get_defined_node nd ++
List.map fst (
n_in nd)).
Proof.
Lemma get_defined_node_incl :
forall {
PSyn Prefs},
forall (
n : @
node PSyn Prefs),
incl (
get_defined_node n)
(
List.map fst (
n_out n) ++
List.map fst (
get_locals (
n_block n))).
Proof.
intros ??.
unfold get_defined_node.
intro n.
pose proof (
n_defd n)
as (
xs &
Vd &
Perm).
cases_eqn Hn;
subst;
simpl;
try now (
intros ? []).
inv Vd.
take (
VarsDefinedScope _ _ _)
and inversion_clear it as [??? (
xs' &
Vd' &
Perm')].
clear Hn.
rewrite Perm in Perm'.
clear -
Vd' Perm'.
apply (
Permutation.Permutation_map fst)
in Perm'.
revert Perm'.
rewrite map_app, 2
map_fst_senv_of_decls.
generalize (
List.map fst (
n_out n) ++
List.map fst l).
intros l' ?;
clear l n.
assert (
Hincl :
incl (
List.map fst (
concat xs'))
l').
{
intros x Hin;
rewrite Perm' in Hin;
auto. }
clear Perm';
revert Hincl;
revert l'.
induction Vd';
simpl;
intros l1. {
now intros ? []. }
unfold incl in *.
rewrite map_app.
setoid_rewrite in_app_iff.
intros Hincl a [
Hin|
Hin];
eauto.
destruct x;
simpl in *;
try now inv Hin.
destruct e as (
xs,
es).
inv H;
simpl in *;
subst;
auto.
Qed.
End LSyntax_facts.
We always use this specialized version of mem_nth
Definition mem_nth :=
mem_nth ident ident_eq_dec.
Definition errTy :
DS (
sampl value) :=
DS_const (
err error_Ty).
Denotational environments (local & program-wide)
Section Denot_env.
Definition SI :=
fun _ :
ident =>
sampl value.
Definition FI :=
fun _ :
ident => (
DS_prod SI -
C->
DS_prod SI).
Definition err_env :
DS_prod SI :=
fun _ =>
errTy.
build an environment from a tuple of streams, with names given in l
Definition env_of_np (
l :
list ident) {
n} :
nprod n -
C->
DS_prod SI :=
Dprodi_DISTR _ _ _
(
fun x =>
match mem_nth l x with
|
Some n =>
get_nth n errTy
|
None => 0
end).
Lemma env_of_np_eq :
forall l n (
ss :
nprod n)
x,
env_of_np l ss x =
match mem_nth l x with
|
Some n =>
get_nth n errTy ss
|
None => 0
end.
Proof.
Lemma env_of_np_tl :
forall l n (
np :
nprod (
S n))
x y,
x <>
y ->
env_of_np (
y ::
l)
np x ==
env_of_np l (
nprod_tl np)
x.
Proof.
Lemma env_of_np_nth :
forall l n (
np :
nprod n)
k x,
mem_nth l x =
Some k ->
env_of_np l np x =
get_nth k errTy np.
Proof.
Lemma forall_env_of_np :
forall (
P :
DS (
sampl value) ->
Prop)
l {
n} (
ss :
nprod n),
P errTy ->
P 0 ->
forall_nprod P ss ->
forall x,
P (
env_of_np l ss x).
Proof.
extract a tuple from an environment
Definition np_of_env (
l :
list ident) :
DS_prod SI -
C-> @
nprod (
DS (
sampl value)) (
length l).
induction l as [|
x l].
-
apply CTE, 0.
-
exact ((
nprod_cons @2_
PROJ _
x)
IHl).
Defined.
Lemma nth_np_of_env :
forall d d' l env k,
k <
length l ->
get_nth k d' (
np_of_env l env) =
env (
nth k l d).
Proof.
induction l as [|? []]; intros * Hl.
- inv Hl.
- destruct k; auto. simpl in *; lia.
- destruct k; simpl; auto.
setoid_rewrite IHl; now auto with arith.
Qed.
Lemma np_of_env_eq :
forall l env,
np_of_env l env
=
match l with
| [] => 0
|
i ::
l =>
nprod_cons (
env i) (
np_of_env l env)
end.
Proof.
induction l; auto.
Qed.
Lemma np_of_env_cons :
forall i l env,
np_of_env (
i ::
l)
env
=
nprod_cons (
env i) (
np_of_env l env).
Proof.
trivial.
Qed.
Lemma np_of_env_le_eq :
forall l env1 env2,
env1 <=
env2 ->
infinite_dom env1 l ->
np_of_env l env1 ==
np_of_env l env2.
Proof.
Lemma np_of_env_ext :
forall l env1 env2,
(
forall x,
In x l ->
env1 x ==
env2 x) ->
np_of_env l env1 ==
np_of_env l env2.
Proof.
induction l as [|
i l];
intros *
Hin;
auto;
simpl in Hin.
rewrite 2 (
np_of_env_eq (
i ::
l)).
apply nprod_cons_Oeq_compat.
-
apply Hin;
auto.
-
apply IHl;
auto.
intros;
apply Hin;
auto.
Qed.
Lemma forall_np_of_env :
forall (
P :
DS (
sampl value) ->
Prop)
l env,
(
forall x,
P (
env x)) ->
forall_nprod P (
np_of_env l env).
Proof.
induction l as [|? []]; intros * Hp; eauto.
- now simpl.
- apply Hp.
- constructor.
+ apply Hp.
+ apply IHl, Hp.
Qed.
Lemma forall_np_of_env' :
forall (
P :
DS (
sampl value) ->
Prop)
l env,
(
forall x,
In x l ->
P (
env x)) ->
forall_nprod P (
np_of_env l env).
Proof.
induction l as [|? []]; intros * Hp; eauto.
- now simpl.
- apply Hp; now constructor.
- constructor.
+ apply Hp. now constructor.
+ apply IHl. clear - Hp. firstorder.
Qed.
Lemma inf_dom_np_of_env :
forall l env,
infinite_dom env l ->
forall_nprod (@
infinite _) (
np_of_env l env).
Proof.
Lemma np_of_env_of_np :
forall l np,
0 <
length l ->
NoDup l ->
np_of_env l (
env_of_np l np) ==
np.
Proof.
Lemma env_of_np_of_env_proj :
forall (
env:
DS_prod SI)
l i,
In i l ->
env_of_np l (
np_of_env l env)
i =
env i.
Proof.
End Denot_env.
Section Denot_node.
Context {
PSyn :
list decl ->
block ->
Prop}.
Context {
Prefs :
PS.t}.
Variable (
G : @
global PSyn Prefs).
Definition sbool_of :
DS (
sampl value) -
C->
DS bool :=
MAP (
fun v =>
match v with
|
pres (
Venum 1) =>
true
| _ =>
false
end).
Definition sbools_of {
n} : @
nprod (
DS (
sampl value))
n -
C->
DS bool :=
nprod_Fold (
ZIP orb) (
DS_const false) @_
lift sbool_of.
Definition swhenv :=
let get_tag :=
fun v =>
match v with Venum t =>
Some t | _ =>
None end in
@
swhen value value enumtag get_tag Nat.eqb.
Definition smergev :=
let get_tag :=
fun v =>
match v with Venum t =>
Some t | _ =>
None end in
@
smerge value value enumtag get_tag Nat.eqb.
Definition scasev :=
let get_tag :=
fun v =>
match v with Venum t =>
Some t | _ =>
None end in
@
scase value value enumtag get_tag Nat.eqb.
Definition scase_defv :=
let get_tag :=
fun v =>
match v with Venum t =>
Some t | _ =>
None end in
@
scase_def value value enumtag get_tag Nat.eqb.
On définit tout de suite denot_exps_ en fonction de denot_exp_
pour simplifier le raisonnement dans denot_exp_eq
Section Denot_exps.
Hypothesis denot_exp_ :
forall e :
exp,
Dprod (
Dprod (
Dprodi FI) (
DS_prod SI)) (
DS_prod SI) -
C->
@
nprod (
DS (
sampl value)) (
numstreams e).
Definition denot_exps_ (
es :
list exp) :
Dprod (
Dprod (
Dprodi FI) (
DS_prod SI)) (
DS_prod SI) -
C->
@
nprod (
DS (
sampl value)) (
list_sum (
List.map numstreams es)).
induction es as [|
a].
+
exact 0.
+
exact ((
nprod_app @2_ (
denot_exp_ a))
IHes).
Defined.
Definition denot_expss_ {
A} (
ess :
list (
A *
list exp)) (
n :
nat) :
Dprod (
Dprod (
Dprodi FI) (
DS_prod SI)) (
DS_prod SI) -
C->
@
nprod (@
nprod (
DS (
sampl value))
n) (
length ess).
induction ess as [|[?
es]].
+
exact 0.
+
destruct (
Nat.eq_dec (
list_sum (
List.map numstreams es))
n)
as [<-|].
*
exact ((
nprod_cons @2_ (
denot_exps_ es))
IHess).
*
exact 0.
Defined.
End Denot_exps.
Definition denot_exp_ (
ins :
list ident)
(
e :
exp) :
Dprod (
Dprod (
Dprodi FI) (
DS_prod SI)) (
DS_prod SI) -
C->
@
nprod (
DS (
sampl value)) (
numstreams e).
set (
ctx :=
Dprod _ _).
epose (
denot_var :=
fun x =>
if mem_ident x ins
then PROJ (
DS_fam SI)
x @_
SND _ _ @_
FST _ _
else PROJ (
DS_fam SI)
x @_
SND _ _).
revert e.
fix denot_exp_ 1.
intro e.
destruct e eqn:
He;
simpl (
nprod _).
-
apply (
sconst (
Vscalar (
sem_cconst c)) @_
bss ins @_
SND _ _ @_
FST _ _).
-
apply (
sconst (
Venum e0) @_
bss ins @_
SND _ _ @_
FST _ _).
-
exact (
denot_var i).
-
apply CTE, 0.
-
eapply fcont_comp. 2:
apply (
denot_exp_ e0).
destruct (
numstreams e0)
as [|[]].
1,3:
apply CTE,
errTy.
destruct (
typeof e0)
as [|
ty []].
1,3:
apply CTE,
errTy.
exact (
sunop (
fun v =>
sem_unop u v ty)).
-
eapply fcont_comp2.
3:
apply (
denot_exp_ e0_2).
2:
apply (
denot_exp_ e0_1).
destruct (
numstreams e0_1)
as [|[]], (
numstreams e0_2)
as [|[]].
1-4,6-9:
apply curry,
CTE,
errTy.
destruct (
typeof e0_1)
as [|
ty1 []], (
typeof e0_2)
as [|
ty2 []].
1-4,6-9:
apply curry,
CTE,
errTy.
exact (
sbinop (
fun v1 v2 =>
sem_binop b v1 ty1 v2 ty2)).
-
apply CTE, 0.
-
rename l into e0s,
l0 into es,
l1 into anns.
clear He.
pose (
s0s :=
denot_exps_ denot_exp_ e0s).
pose (
ss :=
denot_exps_ denot_exp_ es).
destruct (
Nat.eq_dec
(
list_sum (
List.map numstreams es))
(
list_sum (
List.map numstreams e0s))
)
as [
Heq1|].
destruct (
Nat.eq_dec
(
list_sum (
List.map numstreams e0s))
(
length anns)
)
as [
Heq2|].
2,3:
apply CTE, (
nprod_const _
errTy).
rewrite Heq1 in ss.
rewrite <-
Heq2.
exact ((
lift2 (
SDfuns.fby) @2_
s0s)
ss).
-
apply CTE, 0.
-
rename l into es.
destruct l0 as (
tys,
ck).
destruct p as (
i,
ty).
clear He.
destruct (
Nat.eq_dec
(
list_sum (
List.map numstreams es))
(
length tys)
)
as [<-|].
2:
apply CTE, (
nprod_const _
errTy).
pose (
ss :=
denot_exps_ denot_exp_ es).
exact ((
llift (
swhenv e0) @2_
ss) (
denot_var i)).
-
rename l into ies.
destruct l0 as (
tys,
ck).
destruct p as [
i ty].
pose (
ses :=
denot_expss_ denot_exp_ ies (
length tys)).
rewrite <- (
length_map fst)
in ses.
exact ((
lift_nprod @_ (
smergev (
List.map fst ies)) @2_
denot_var i)
ses).
-
rename l into ies.
destruct l0 as (
tys,
ck).
pose (
ses :=
denot_expss_ denot_exp_ ies (
length tys)).
rewrite <- (
length_map fst)
in ses.
destruct o as [
d_es|].
+
revert ses.
destruct (
Nat.eq_dec
(
list_sum (
List.map numstreams d_es))
(
length tys)
)
as [<-|].
2:
apply CTE,
CTE, (
nprod_const _
errTy).
intro ses.
refine ((_ @2_ (
denot_exp_ e0)) ((
nprod_cons @2_
denot_exps_ denot_exp_ d_es)
ses)).
destruct (
numstreams e0)
as [|[]].
1,3:
apply CTE,
CTE, (
nprod_const _
errTy).
exact (
lift_nprod @_
scase_defv (
List.map fst ies)).
+
refine ((_ @2_ (
denot_exp_ e0))
ses).
destruct (
numstreams e0)
as [|[]].
1,3:
apply CTE,
CTE, (
nprod_const _
errTy).
exact (
lift_nprod @_ (
scasev (
List.map fst ies))).
-
rename l into es,
l0 into er,
l1 into anns.
clear He.
destruct (
find_node i G)
as [
n|].
destruct (
Nat.eq_dec (
length (
List.map fst n.(
n_out))) (
length anns))
as [<-|].
2,3:
apply CTE, (
nprod_const _
errTy).
pose (
f :=
PROJ _
i @_
FST _ _ @_
FST _ _ :
ctx -
C->
FI i).
pose (
ss :=
denot_exps_ denot_exp_ es).
pose (
rs :=
denot_exps_ denot_exp_ er).
refine
(
np_of_env (
List.map fst (
n_out n)) @_
(
sreset @3_
f) (
sbools_of @_
rs) (
env_of_np (
idents (
n_in n)) @_
ss)).
Defined.
Definition denot_exp (
ins :
list ident) (
e :
exp) :
Dprodi FI -
C->
DS_prod SI -
C->
DS_prod SI -
C->
nprod (
numstreams e) :=
curry (
curry (
denot_exp_ ins e)).
Definition denot_exps (
ins :
list ident) (
es :
list exp) :
Dprodi FI -
C->
DS_prod SI -
C->
DS_prod SI -
C->
nprod (
list_sum (
List.map numstreams es)) :=
curry (
curry (
denot_exps_ (
denot_exp_ ins)
es)).
Lemma denot_exps_eq :
forall ins e es envG envI env,
denot_exps ins (
e ::
es)
envG envI env
=
nprod_app (
denot_exp ins e envG envI env) (
denot_exps ins es envG envI env).
Proof.
reflexivity.
Qed.
Lemma forall_denot_exps :
forall (
P :
DS (
sampl value) ->
Prop)
ins es envG envI env,
forall_nprod P (
denot_exps ins es envG envI env)
<->
Forall (
fun e =>
forall_nprod P (
denot_exp ins e envG envI env))
es.
Proof.
Definition denot_expss {
A} (
ins :
list ident) (
ess :
list (
A *
list exp)) (
n :
nat) :
Dprodi FI -
C->
DS_prod SI -
C->
DS_prod SI -
C->
@
nprod (@
nprod (
DS (
sampl value))
n) (
length ess) :=
curry (
curry (
denot_expss_ (
denot_exp_ ins)
ess n)).
Lemma denot_expss_eq :
forall A ins (
x :
A)
es ess envG envI env n,
denot_expss ins ((
x,
es) ::
ess)
n envG envI env
=
match Nat.eq_dec (
list_sum (
List.map numstreams es))
n with
|
left eqn =>
nprod_cons
(
eq_rect _
nprod (
denot_exps ins es envG envI env) _
eqn)
(
denot_expss ins ess n envG envI env)
| _ => 0
end.
Proof.
Lemma denot_expss_nil :
forall A ins n envG envI env,
@
denot_expss A ins []
n envG envI env == 0.
Proof.
reflexivity.
Qed.
Lemma forall_denot_expss :
forall A ins (
ess :
list (
A *
list exp))
n envG envI env (
P :
nprod n ->
Prop),
Forall (
fun es =>
match Nat.eq_dec (
list_sum (
List.map numstreams es))
n with
|
left eqn =>
P (
eq_rect _
nprod (
denot_exps ins es envG envI env)
n eqn)
| _ =>
P 0
end) (
List.map snd ess) ->
forall_nprod P (
denot_expss ins ess n envG envI env).
Proof.
Lemma forall_forall_denot_expss_ :
forall A ins (
ess :
list (
A *
list exp))
n envG envI env (
P :
DS (
sampl value) ->
Prop),
P 0 ->
Forall (
fun es =>
forall_nprod P (
denot_exps ins (
snd es)
envG envI env))
ess ->
forall_nprod (
forall_nprod P) (
denot_expss ins ess n envG envI env).
Proof.
Lemma forall_forall_denot_expss :
forall A ins (
ess :
list (
A *
list exp))
n envG envI env (
P :
DS (
sampl value) ->
Prop),
Forall (
fun es =>
length (
annots (
snd es)) =
n)
ess ->
Forall (
fun es =>
forall_nprod P (
denot_exps ins (
snd es)
envG envI env))
ess ->
forall_nprod (
forall_nprod P) (
denot_expss ins ess n envG envI env).
Proof.
Lemma Forall_denot_expss :
forall A P ins (
es :
list (
A *
list exp))
n envG envI env,
Forall (
fun es =>
length (
annots (
snd es)) =
n)
es ->
forall_nprod (
forall_nprod P) (
denot_expss ins es n envG envI env)
<->
Forall (
fun l =>
Forall (
fun e =>
forall_nprod P (
denot_exp ins e envG envI env))
l) (
List.map snd es).
Proof.
Lemma denot_exps_nil :
forall ins envG envI env,
denot_exps ins []
envG envI env = 0.
Proof.
reflexivity.
Qed.
Lemma denot_exps_1 :
forall ins e envG envI env,
list_of_nprod (
denot_exps ins [
e]
envG envI env)
=
list_of_nprod (
denot_exp ins e envG envI env).
Proof.
Definition denot_var ins envI env x :
DS (
sampl value) :=
if mem_ident x ins then envI x else env x.
Lemma denot_exp_eq :
forall ins e envG envI env,
denot_exp ins e envG envI env =
match e return nprod (
numstreams e)
with
|
Econst c =>
sconst (
Vscalar (
sem_cconst c)) (
bss ins envI)
|
Eenum c _ =>
sconst (
Venum c) (
bss ins envI)
|
Evar x _ =>
denot_var ins envI env x
|
Eunop op e an =>
let se :=
denot_exp ins e envG envI env in
match numstreams e as n return nprod n ->
nprod 1
with
| 1 =>
fun se =>
match typeof e with
| [
ty] =>
sunop (
fun v =>
sem_unop op v ty)
se
| _ =>
errTy
end
| _ =>
fun _ =>
errTy
end se
|
Ebinop op e1 e2 an =>
let se1 :=
denot_exp ins e1 envG envI env in
let se2 :=
denot_exp ins e2 envG envI env in
match numstreams e1 as n1,
numstreams e2 as n2
return nprod n1 ->
nprod n2 ->
nprod 1
with
| 1,1 =>
fun se1 se2 =>
match typeof e1,
typeof e2 with
| [
ty1],[
ty2] =>
sbinop (
fun v1 v2 =>
sem_binop op v1 ty1 v2 ty2)
se1 se2
| _,_ =>
errTy
end
| _,_ =>
fun _ _ =>
errTy
end se1 se2
|
Efby e0s es an =>
let s0s :=
denot_exps ins e0s envG envI env in
let ss :=
denot_exps ins es envG envI env in
let n := (
list_sum (
List.map numstreams e0s))
in
let m := (
list_sum (
List.map numstreams es))
in
match Nat.eq_dec m n,
Nat.eq_dec n (
length an)
with
|
left eqm,
left eqan =>
eq_rect _
nprod (
lift2 (
SDfuns.fby)
s0s (
eq_rect _
nprod ss _
eqm)) _
eqan
| _, _ =>
nprod_const _
errTy
end
|
Ewhen es (
x,_)
k (
tys,_) =>
let ss :=
denot_exps ins es envG envI env in
match Nat.eq_dec (
list_sum (
List.map numstreams es)) (
length tys)
with
|
left eqn =>
eq_rect _
nprod (
llift (
swhenv k)
ss (
denot_var ins envI env x)) _
eqn
| _ =>
nprod_const _
errTy
end
|
Emerge (
x,_)
ies (
tys,_) =>
let ss :=
denot_expss ins ies (
length tys)
envG envI env in
let ss :=
eq_rect_r nprod ss (
length_map _ _)
in
lift_nprod (
smergev (
List.map fst ies) (
denot_var ins envI env x))
ss
|
Ecase ec ies None (
tys,_) =>
let ss :=
denot_expss ins ies (
length tys)
envG envI env in
let ss :=
eq_rect_r nprod ss (
length_map _ _)
in
let cs :=
denot_exp ins ec envG envI env in
match numstreams ec as n return nprod n -> _
with
| 1 =>
fun cs =>
lift_nprod (
scasev (
List.map fst ies)
cs)
ss
| _ =>
fun _ =>
nprod_const _
errTy
end cs
|
Ecase ec ies (
Some eds) (
tys,_) =>
let ss :=
denot_expss ins ies (
length tys)
envG envI env in
let ss :=
eq_rect_r nprod ss (
length_map _ _)
in
let cs :=
denot_exp ins ec envG envI env in
let ds :=
denot_exps ins eds envG envI env in
match numstreams ec as n,
Nat.eq_dec (
list_sum (
List.map numstreams eds)) (
length tys)
return nprod n -> _
with
| 1,
left eqm =>
fun cs =>
lift_nprod (
scase_defv (
List.map fst ies)
cs)
(
nprod_cons (
eq_rect _
nprod ds _
eqm)
ss)
| _,_ =>
fun _ =>
nprod_const _
errTy
end cs
|
Eapp f es er an =>
let ss :=
denot_exps ins es envG envI env in
let rs :=
denot_exps ins er envG envI env in
match find_node f G with
|
Some n =>
match Nat.eq_dec (
length (
List.map fst n.(
n_out))) (
length an)
with
|
left eqan =>
eq_rect _
nprod
(
np_of_env (
List.map fst n.(
n_out)) (
sreset (
envG f) (
sbools_of rs) (
env_of_np (
idents n.(
n_in))
ss)))
_
eqan
| _ =>
nprod_const _
errTy
end
| _ =>
nprod_const _
errTy
end
| _ => 0
end.
Proof.
Ltac fold_denot_exps_ ins :=
repeat
match goal with
| |-
context [
denot_exps_ ?
A ] =>
change A with (
denot_exp_ ins)
| |-
context [
denot_expss_ ?
A ] =>
change A with (
denot_exp_ ins)
end.
Ltac gen_denot_sub_exps :=
repeat
match goal with
| |-
context [
denot_exp_ ?
A ?
B ] =>
generalize (
denot_exp_ A B);
intro
| |-
context [
denot_exps_ ?
A ?
B ] =>
generalize (
denot_exps_ A B);
intro
| |-
context [
denot_expss_ ?
A ?
B ] =>
generalize (
denot_expss_ A B);
intro
end.
destruct e;
auto;
intros envG envI env.
-
unfold denot_exp,
denot_exp_,
denot_var at 1.
cases.
-
unfold denot_exp,
denot_exp_ at 1.
fold (
denot_exp_ ins e).
generalize (
denot_exp_ ins e)
as ss.
generalize (
numstreams e)
as ne.
destruct ne as [|[]];
intros;
auto.
destruct (
typeof e)
as [|? []];
auto.
-
unfold denot_exp,
denot_exp_ at 1.
fold (
denot_exp_ ins e1) (
denot_exp_ ins e2).
generalize (
denot_exp_ ins e1)
as ss1.
generalize (
denot_exp_ ins e2)
as ss2.
generalize (
numstreams e1)
as ne1.
generalize (
numstreams e2)
as ne2.
destruct ne1 as [|[]],
ne2 as [|[]];
intros;
auto.
destruct (
typeof e1)
as [|?[]], (
typeof e2)
as [|?[]];
auto.
-
unfold denot_exp,
denot_exps,
denot_exp_ at 1.
fold_denot_exps_ ins.
unfold eq_rect.
gen_denot_sub_exps.
cases;
simpl;
cases.
-
destruct l0 as (
tys,?).
destruct p as (
i,?).
unfold denot_exp,
denot_exps,
denot_exp_ at 1.
fold_denot_exps_ ins.
gen_denot_sub_exps.
unfold denot_var,
eq_rect.
cases;
simpl;
cases.
-
destruct l0 as (
tys,?).
destruct p as (
i,
ty).
unfold denot_exp,
denot_exp_,
denot_exps,
denot_expss at 1.
fold_denot_exps_ ins.
gen_denot_sub_exps.
unfold denot_var,
eq_rect_r,
eq_rect,
eq_sym.
cases.
-
destruct l0 as (
tys,?).
destruct o.
+
unfold denot_exp,
denot_exp_,
denot_exps,
denot_expss at 1.
fold_denot_exps_ ins.
gen_denot_sub_exps.
unfold eq_rect_r,
eq_rect,
eq_sym.
cases;
simpl;
cases.
+
unfold denot_exp,
denot_exp_,
denot_exps,
denot_expss at 1.
fold_denot_exps_ ins.
gen_denot_sub_exps.
unfold eq_rect_r,
eq_rect,
eq_sym.
cases.
-
rename l into es,
l0 into er,
l1 into anns,
i into f.
unfold denot_exp,
denot_exps,
denot_exp_ at 1.
fold_denot_exps_ ins.
gen_denot_sub_exps.
cases.
generalize (
np_of_env (
List.map fst (
n_out n)));
intro.
unfold eq_rect.
simpl;
destruct e.
rewrite 3
curry_Curry, 3
Curry_simpl,
fcont_comp_simpl.
reflexivity.
Qed.
Global Opaque denot_exp.
Global Add Parametric Morphism ins : (
denot_var ins)
with signature @
Oeq (
DS_prod SI) ==> @
eq (
DS_prod SI) ==> @
eq ident ==> @
Oeq (
DS (
sampl value))
as denot_var_morph1.
Proof.
Global Add Parametric Morphism ins : (
denot_var ins)
with signature @
eq (
DS_prod SI) ==> @
Oeq (
DS_prod SI) ==> @
eq ident ==> @
Oeq (
DS (
sampl value))
as denot_var_morph2.
Proof.
Lemma denot_var_inf :
forall ins envI env x,
all_infinite envI ->
all_infinite env ->
infinite (
denot_var ins envI env x).
Proof.
Lemma denot_var_nins :
forall ins envI env x,
~
In x ins ->
denot_var ins envI env x =
env x.
Proof.
env_of_np_ext xs ss env binds xs to ss in env
Definition env_of_np_ext (
l :
list ident) {
n} :
nprod n -
C->
DS_prod SI -
C->
DS_prod SI :=
curry (
Dprodi_DISTR _ _ _
(
fun x =>
match mem_nth l x with
|
Some n =>
get_nth n errTy @_
FST _ _
|
None =>
PROJ _
x @_
SND _ _
end)).
Lemma env_of_np_ext_eq :
forall l n (
np :
nprod n)
env x,
env_of_np_ext l np env x
=
match mem_nth l x with
|
Some n =>
get_nth n errTy np
|
None =>
env x
end.
Proof.
unfold env_of_np_ext.
intros.
autorewrite with cpodb.
cases.
Qed.
Definition denot_block (
ins :
list ident) (
b :
block) :
Dprodi FI -
C->
DS_prod SI -
C->
DS_prod SI -
C->
DS_prod SI -
C->
DS_prod SI :=
curry (
curry (
curry
match b with
|
Beq (
xs,
es) => ((
env_of_np_ext xs @2_
uncurry (
uncurry (
denot_exps ins es)) @_
FST _ _)
(
SND _ _))
| _ =>
SND _ _
end)).
Lemma denot_block_eq :
forall ins b envG envI env env_acc,
denot_block ins b envG envI env env_acc
=
match b with
|
Beq (
xs,
es) =>
env_of_np_ext xs (
denot_exps ins es envG envI env)
env_acc
| _ =>
env_acc
end.
Proof.
Definition denot_blocks (
ins :
list ident) (
blks :
list block) :
Dprodi FI -
C->
DS_prod SI -
C->
DS_prod SI -
C->
DS_prod SI.
apply curry,
curry.
revert blks;
fix denot_blocks 1.
intros [|
blk blks].
-
apply CTE, 0.
-
refine ((
ID _ @2_
uncurry (
uncurry (
denot_block ins blk))) (
denot_blocks blks)).
Defined.
Lemma denot_blocks_eq :
forall ins envG envI env blks,
denot_blocks ins blks envG envI env
=
fold_right (
fun blk =>
denot_block ins blk envG envI env) 0
blks.
Proof.
induction blks;
simpl;
auto.
unfold denot_blocks at 1.
setoid_rewrite <-
IHblks.
reflexivity.
Qed.
Corollary denot_blocks_eq_cons :
forall ins envG envI env blk blks,
denot_blocks ins (
blk ::
blks)
envG envI env
=
denot_block ins blk envG envI env
(
denot_blocks ins blks envG envI env).
Proof.
reflexivity.
Qed.
Definition denot_top_block (
ins :
list ident) (
b :
block) :
Dprodi FI -
C->
DS_prod SI -
C->
DS_prod SI -
C->
DS_prod SI :=
match b with
|
Blocal (
Scope _
blks) =>
denot_blocks ins blks
| _ => 0
end.
Lemma denot_top_block_eq :
forall ins blk envG envI env,
denot_top_block ins blk envG envI env
=
match blk with
|
Blocal (
Scope _
blks) =>
denot_blocks ins blks envG envI env
| _ => 0
end.
Proof.
Definition denot_node (
n : @
node PSyn Prefs) :
Dprodi FI -
C->
DS_prod SI -
C->
DS_prod SI -
C->
DS_prod SI.
apply curry.
refine ((
denot_top_block (
List.map fst n.(
n_in))
n.(
n_block) @2_ _) _).
-
exact (
FST _ _).
-
exact (
SND _ _).
Defined.
Lemma denot_node_eq :
forall n envG envI,
let ins :=
List.map fst n.(
n_in)
in
denot_node n envG envI =
denot_top_block ins n.(
n_block)
envG envI.
Proof.
reflexivity.
Qed.
End Denot_node.
After rewriting denot_exp_eq we often need to destruct numstreams _
or Nat.eq_dec _ _. It does not work directly in general because
the type of the denotation of subterms depends on these values.
One way solve the problem is to revert the hypotheses and
generalize the results of denot_exp, denot_exps, denot_expss on subterms
with the following tactic.
Ltac gen_sub_exps :=
repeat match goal with
| |-
context [ ?
f1 (?
f2 (?
f3 (
denot_expss ?
e1 ?
e2 ?
e3 ?
e4) ?
e5) ?
e6) ?
e7 ] =>
generalize (
f1 (
f2 (
f3 (
denot_expss e1 e2 e3 e4)
e5)
e6)
e7)
| |-
context [ ?
f1 (?
f2 (?
f3 (
denot_exps ?
e1 ?
e2 ?
e3) ?
e4) ?
e5) ?
e6 ] =>
generalize (
f1 (
f2 (
f3 (
denot_exps e1 e2 e3)
e4)
e5)
e6)
| |-
context [ ?
f1 (?
f2 (?
f3 (
denot_exp ?
e1 ?
e2 ?
e3) ?
e4) ?
e5) ?
e6 ] =>
generalize (
f1 (
f2 (
f3 (
denot_exp e1 e2 e3)
e4)
e5)
e6)
end.
Section Global.
Definition denot_global_ {
PSyn Prefs} (
G : @
global PSyn Prefs) :
Dprodi FI -
C->
Dprodi FI.
apply Dprodi_DISTR;
intro f.
destruct (
find_node f G).
-
exact (
curry (
FIXP _ @_ (
denot_node G n @2_
FST _ _) (
SND _ _))).
-
apply CTE,
CTE, 0.
Defined.
Lemma denot_global_eq :
forall {
PSyn Prefs},
forall (
G : @
global PSyn Prefs)
envG f envI,
denot_global_ G envG f envI =
match find_node f G with
|
Some n =>
FIXP _ (
denot_node G n envG envI)
|
None => 0
end.
Proof.
intros.
unfold denot_global_.
autorewrite with cpodb.
cases.
Qed.
Definition denot_global {
PSyn Prefs} (
G: @
global PSyn Prefs) :
Dprodi FI :=
FIXP _ (
denot_global_ G).
End Global.
Lemma denot_in :
forall {
PSyn Prefs} (
G : @
global PSyn Prefs),
forall f n,
find_node f G =
Some n ->
forall envI x,
In x (
List.map fst (
n_in n)) ->
denot_global G f envI x == 0.
Proof.
intros *
Hfind *
Hin.
pose proof (
Hnin :=
NoDup_get_defined_node n).
unfold denot_global,
get_defined_node in *.
rewrite <-
PROJ_simpl, <-
PROJ_simpl,
FIXP_eq,
PROJ_simpl,
PROJ_simpl.
rewrite denot_global_eq,
Hfind.
rewrite <-
PROJ_simpl,
FIXP_eq,
denot_node_eq,
denot_top_block_eq,
PROJ_simpl at 1.
cases.
remember (
FIXP _ _)
as envG eqn:
HH;
clear HH.
remember (
FIXP _ _)
as env eqn:
HH;
clear HH.
induction l0 as [|
blk blks];
auto.
simpl in Hnin;
rewrite <-
app_assoc in Hnin.
rewrite denot_blocks_eq_cons,
denot_block_eq.
cases;
simpl in Hnin.
rewrite env_of_np_ext_eq.
cases_eqn Hmem;
eauto 3
using NoDup_app_r;
exfalso.
eapply NoDup_app_In;
eauto using mem_nth_In,
in_or_app.
Qed.
Lemma not_out_bot :
forall {
PSyn Prefs} (
G : @
global PSyn Prefs),
forall f n,
find_node f G =
Some n ->
forall envI x,
~
In x (
List.map fst (
n_out n)) ->
~
In x (
List.map fst (
get_locals (
n_block n))) ->
denot_global G f envI x == 0.
Proof.
intros *
Hfind *
Nout Nloc.
assert (
Hnin: ~
In x (
get_defined_node n)).
{
intros Hin%
get_defined_node_incl%
in_app_iff;
tauto. }
clear Nout Nloc.
unfold get_defined_node,
denot_global,
get_locals in *.
rewrite <-
PROJ_simpl, <-
PROJ_simpl,
FIXP_eq,
PROJ_simpl,
PROJ_simpl.
rewrite denot_global_eq,
Hfind.
rewrite <-
PROJ_simpl,
FIXP_eq,
PROJ_simpl.
rewrite denot_node_eq,
denot_top_block_eq.
cases.
remember (
FIXP _ _)
as envG eqn:
HH;
clear HH.
remember (
FIXP _ _)
as env eqn:
HH;
clear HH.
induction l0 as [|
blk blks'];
auto.
simpl in Hnin;
rewrite in_app_iff in Hnin.
rewrite denot_blocks_eq_cons,
denot_block_eq.
cases_eqn HH;
subst.
rewrite env_of_np_ext_eq.
cases_eqn Hmem;
exfalso.
apply mem_nth_In in Hmem;
auto.
Qed.
Here we show that a node can be removed from the environment
if it is not evaluated during the computations.
Section Denot_cons.
Lemma denot_exps_hyp :
forall {
PSyn Prefs} (
G G' : @
global PSyn Prefs),
forall ins es envG envI env,
Forall (
fun e =>
denot_exp G ins e envG envI env ==
denot_exp G' ins e envG envI env)
es ->
denot_exps G ins es envG envI env ==
denot_exps G' ins es envG envI env.
Proof.
Lemma denot_exp_cons :
forall {
PSyn Prefs} (
nd : @
node PSyn Prefs),
forall nds tys exts
ins envG envI env e,
~
Is_node_in_exp nd.(
n_name)
e ->
denot_exp (
Global tys exts nds)
ins e envG envI env
==
denot_exp (
Global tys exts (
nd ::
nds))
ins e envG envI env.
Proof.
induction e using exp_ind2;
intro Hnin.
all:
setoid_rewrite denot_exp_eq;
auto 1.
-
revert IHe.
gen_sub_exps.
cases;
simpl;
intros.
rewrite IHe;
auto.
intro H;
apply Hnin;
constructor;
auto.
-
revert IHe1 IHe2.
gen_sub_exps.
cases;
simpl;
intros.
rewrite IHe1,
IHe2;
auto.
all:
intro H;
apply Hnin;
constructor;
auto.
-
assert (
denot_exps (
Global tys exts nds)
ins e0s envG envI env
==
denot_exps (
Global tys exts (
nd::
nds))
ins e0s envG envI env)
as He0s.
{
apply denot_exps_hyp.
simpl_Forall.
apply H;
contradict Hnin.
constructor;
left;
solve_Exists. }
assert (
denot_exps (
Global tys exts nds)
ins es envG envI env
==
denot_exps (
Global tys exts (
nd::
nds))
ins es envG envI env)
as Hes.
{
apply denot_exps_hyp.
simpl_Forall.
apply H0;
contradict Hnin.
constructor;
right;
solve_Exists. }
revert He0s Hes;
simpl;
unfold eq_rect.
gen_sub_exps;
cases.
-
assert (
denot_exps (
Global tys exts nds)
ins es envG envI env
==
denot_exps (
Global tys exts (
nd::
nds))
ins es envG envI env)
as Hes.
{
apply denot_exps_hyp.
simpl_Forall.
apply H;
contradict Hnin.
constructor;
solve_Exists. }
revert Hes;
simpl;
unfold eq_rect.
gen_sub_exps;
cases.
-
destruct a as [
tyss c].
assert (
denot_expss (
Global tys exts nds)
ins es (
length tyss)
envG envI env
==
denot_expss (
Global tys exts (
nd::
nds))
ins es (
length tyss)
envG envI env)
as Hess.
{
induction es as [| [
i es]
ies].
trivial.
inv H.
assert (
denot_exps (
Global tys exts nds)
ins es envG envI env
==
denot_exps (
Global tys exts (
nd::
nds))
ins es envG envI env)
as Hes.
{
apply denot_exps_hyp.
simpl_Forall.
apply H2;
contradict Hnin.
constructor;
solve_Exists. }
rewrite 2
denot_expss_eq.
revert Hes;
unfold eq_rect.
destruct (
Nat.eq_dec _ _);
try trivial.
rewrite IHies;
cases;
auto.
contradict Hnin;
inv Hnin.
constructor;
now right. }
revert Hess;
simpl;
unfold eq_rect_r,
eq_rect,
eq_sym.
gen_sub_exps;
cases.
-
destruct a as [
tyss c].
assert (
denot_expss (
Global tys exts nds)
ins es (
length tyss)
envG envI env
==
denot_expss (
Global tys exts (
nd::
nds))
ins es (
length tyss)
envG envI env)
as Hess.
{
induction es as [| [
i es]
ies].
trivial.
inv H.
assert (
denot_exps (
Global tys exts nds)
ins es envG envI env
==
denot_exps (
Global tys exts (
nd::
nds))
ins es envG envI env)
as Hes.
{
apply denot_exps_hyp.
simpl_Forall.
apply H3;
contradict Hnin.
constructor;
right;
left;
solve_Exists. }
rewrite 2
denot_expss_eq.
revert Hes;
unfold eq_rect.
destruct (
Nat.eq_dec _ _);
try trivial.
rewrite IHies;
cases;
auto.
contradict Hnin;
inv Hnin.
destruct H2 as [|[]];
constructor;
auto. }
revert Hess;
simpl;
unfold eq_rect_r,
eq_rect,
eq_sym.
revert IHe.
gen_sub_exps.
intros;
destruct d as [
esd|];
cases.
+
assert (
denot_exps (
Global tys exts nds)
ins esd envG envI env
==
denot_exps (
Global tys exts (
nd::
nds))
ins esd envG envI env)
as Hesd.
{
apply denot_exps_hyp.
simpl_Forall.
apply H0;
contradict Hnin.
constructor;
right;
right;
esplit;
split;
eauto;
solve_Exists. }
rewrite Hesd,
IHe;
auto.
contradict Hnin.
constructor;
auto.
+
rewrite IHe;
auto.
contradict Hnin.
constructor;
auto.
-
simpl.
destruct (
ident_eq_dec nd.(
n_name)
f)
as [|
Hf];
subst.
{
contradict Hnin.
apply INEapp2. }
rewrite (
find_node_other _ _ _ _ _
Hf).
assert (
denot_exps (
Global tys exts nds)
ins es envG envI env
==
denot_exps (
Global tys exts (
nd::
nds))
ins es envG envI env)
as Hes.
{
apply denot_exps_hyp.
simpl_Forall.
apply H;
contradict Hnin.
constructor;
left;
solve_Exists. }
assert (
denot_exps (
Global tys exts nds)
ins er envG envI env
==
denot_exps (
Global tys exts (
nd::
nds))
ins er envG envI env)
as Her.
{
apply denot_exps_hyp.
simpl_Forall.
apply H0;
contradict Hnin.
constructor;
right;
solve_Exists. }
revert Hes Her;
simpl;
unfold eq_rect.
gen_sub_exps;
cases.
now intros ???? -> ->.
Qed.
Corollary denot_exps_cons :
forall {
PSyn Prefs} (
nd : @
node PSyn Prefs),
forall nds tys exts
ins envG envI env es,
~ (
List.Exists (
Is_node_in_exp nd.(
n_name))
es) ->
denot_exps (
Global tys exts nds)
ins es envG envI env
==
denot_exps (
Global tys exts (
nd ::
nds))
ins es envG envI env.
Proof.
Lemma denot_block_cons :
forall {
PSyn Prefs} (
nd : @
node PSyn Prefs),
forall nds tys exts
ins envG envI env env_acc blk,
~
Is_node_in_block (
n_name nd)
blk ->
denot_block (
Global tys exts nds)
ins blk envG envI env env_acc
==
denot_block (
Global tys exts (
nd ::
nds))
ins blk envG envI env env_acc.
Proof.
Corollary denot_blocks_cons :
forall {
PSyn Prefs} (
nd : @
node PSyn Prefs),
forall nds tys exts
ins envG envI env blks,
~ (
List.Exists (
Is_node_in_block (
n_name nd))
blks) ->
denot_blocks (
Global tys exts nds)
ins blks envG envI env
==
denot_blocks (
Global tys exts (
nd ::
nds))
ins blks envG envI env.
Proof.
Lemma denot_node_cons :
forall {
PSyn Prefs} (
n : @
node PSyn Prefs),
forall nd nds tys exts,
~
Is_node_in_block nd.(
n_name)
n.(
n_block) ->
denot_node (
Global tys exts nds)
n
==
denot_node (
Global tys exts (
nd ::
nds))
n.
Proof.
End Denot_cons.
End SD.
Module SdFun
(
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)
(
Lord :
LORDERED Ids Op OpAux Cks Senv Syn)
<:
SD Ids Op OpAux Cks Senv Syn Lord.
Include SD Ids Op OpAux Cks Senv Syn Lord.
End SdFun.