Module SCClocking
From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.
From Velus Require Import Common.
From Velus Require Import CommonTyping.
From Velus Require Import Environment.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import Fresh.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax.
From Velus Require Import Lustre.LClocking.
From Velus Require Import Lustre.SubClock.SubClock.
Module Type SCCLOCKING
(
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 SC :
SUBCLOCK Ids Op OpAux Cks Senv Syn).
Section subclock.
Variable bck :
clock.
Variable sub :
Env.t ident.
Variable Γ Γ' :
static_env.
Hypothesis NoLast :
forall x, ~
IsLast Γ
x.
Hypothesis Hsub :
forall x y ck,
Env.find x sub =
Some y ->
HasClock Γ
x ck ->
HasClock Γ'
y (
subclock_clock bck sub ck).
Hypothesis Hnsub :
forall x ck,
Env.find x sub =
None ->
HasClock Γ
x ck ->
HasClock Γ'
x (
subclock_clock bck sub ck).
Lemma rename_var_wc :
forall x ck,
HasClock Γ
x ck ->
HasClock Γ' (
rename_var sub x) (
subclock_clock bck sub ck).
Proof.
unfold rename_var.
intros *
Hin.
destruct (
Env.find _ _)
eqn:
Hfind;
simpl in *;
eauto.
Qed.
Context {
PSyn :
list decl ->
block ->
Prop} {
prefs :
PS.t}.
Variable G : @
global PSyn prefs.
Hypothesis Hwbck :
wc_clock (
idck Γ')
bck.
Lemma subclock_clock_wc :
forall ck,
wc_clock (
idck Γ)
ck ->
wc_clock (
idck Γ') (
subclock_clock bck sub ck).
Proof.
induction ck;
intros *
Hwc;
inv Hwc;
simpl;
auto.
constructor;
eauto.
simpl_In.
assert (
HasClock Γ
i a.(
clo))
as Hck by eauto with senv.
eapply rename_var_wc in Hck.
inv Hck.
solve_In.
congruence.
Qed.
Lemma add_whens_wc :
forall e ty,
clockof e = [
Cbase] ->
wc_exp G Γ'
e ->
wc_exp G Γ' (
add_whens e ty bck).
Proof.
Lemma subclock_clock_instck :
forall sub1 sub0 bck'
ck ck',
instck bck'
sub0 ck =
Some ck' ->
instck (
subclock_clock bck sub1 bck') (
fun x0 =>
option_map (
rename_var sub1) (
sub0 x0))
ck =
Some (
subclock_clock bck sub1 ck').
Proof.
induction ck;
intros *
Hinst;
simpl in *.
-
inv Hinst;
auto.
-
cases_eqn Heq;
inv Hinst;
simpl in *.
+
inv Heq2;
simpl.
specialize (
IHck _ eq_refl).
now inv IHck.
+
congruence.
+
specialize (
IHck _ eq_refl).
congruence.
Qed.
Lemma subclock_nclock_WellInstantiated1 :
forall bck'
sub0 sub xck nck,
WellInstantiated bck'
sub0 xck nck ->
WellInstantiated (
subclock_clock bck sub bck') (
fun x =>
option_map (
rename_var sub) (
sub0 x))
xck (
subclock_nclock bck sub nck).
Proof.
intros ??? (
x&
ck) (
ck'&
name) (
Hw1&
Hw2).
split;
simpl in *.
-
rewrite Hw1.
destruct name;
simpl;
auto.
-
apply subclock_clock_instck;
auto.
Qed.
Lemma subclock_nclock_WellInstantiated2 :
forall bck'
sub0 sub xck ck,
WellInstantiated bck'
sub0 xck (
ck,
None) ->
WellInstantiated (
subclock_clock bck sub bck') (
fun x =>
option_map (
rename_var sub) (
sub0 x))
xck (
subclock_clock bck sub ck,
None).
Proof.
intros ??? (
x&
ck)
ck' (
Hw1&
Hw2).
split;
simpl in *.
-
rewrite Hw1.
reflexivity.
-
apply subclock_clock_instck;
auto.
Qed.
Lemma subclock_exp_wc :
forall e,
wc_exp G Γ
e ->
wc_exp G Γ' (
subclock_exp bck sub e).
Proof with
Lemma subclock_equation_wc :
forall eq,
wc_equation G Γ
eq ->
wc_equation G Γ' (
subclock_equation bck sub eq).
Proof.
End subclock.
End SCCLOCKING.
Module SCClockingFun
(
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)
(
SC :
SUBCLOCK Ids Op OpAux Cks Senv Syn)
<:
SCCLOCKING Ids Op OpAux Cks Senv Syn Clo SC.
Include SCCLOCKING Ids Op OpAux Cks Senv Syn Clo SC.
End SCClockingFun.