Module StcIsVariable
From
Velus
Require
Import
Common
.
From
Velus
Require
Import
Operators
.
From
Velus
Require
Import
CoreExpr.CESyntax
.
From
Velus
Require
Import
Stc.StcSyntax
.
From
Velus
Require
Import
Clocks
.
From
Coq
Require
Import
List
.
Import
List.ListNotations
.
Open
Scope
list_scope
.
Module
Type
STCISVARIABLE
(
Import
Ids
:
IDS
)
(
Import
Op
:
OPERATORS
)
(
Import
CESyn
:
CESYNTAX
Op
)
(
Import
Syn
:
STCSYNTAX
Ids
Op
CESyn
).
Inductive
Is_variable_in_tc
:
ident
->
trconstr
->
Prop
:=
|
VarTcDef
:
forall
x
ck
e
,
Is_variable_in_tc
x
(
TcDef
x
ck
e
)
|
VarTcCall
:
forall
x
i
xs
ck
rst
f
es
,
In
x
xs
->
Is_variable_in_tc
x
(
TcCall
i
xs
ck
rst
f
es
).
Definition
Is_variable_in
(
x
:
ident
) (
tcs
:
list
trconstr
) :
Prop
:=
Exists
(
Is_variable_in_tc
x
)
tcs
.
Lemma
Is_variable_in_variables
:
forall
tcs
x
,
Is_variable_in
x
tcs
<->
In
x
(
variables
tcs
).
Proof.
unfold
variables
.
induction
tcs
as
[|[]];
simpl
.
-
split
;
try
contradiction
;
inversion
1.
-
split
.
+
inversion_clear
1
as
[??
Var
|];
try
inv
Var
;
auto
.
right
;
apply
IHtcs
;
auto
.
+
intros
[
E
|].
*
subst
;
left
;
constructor
.
*
right
;
apply
IHtcs
;
auto
.
-
setoid_rewrite
<-
IHtcs
;
split
.
+
inversion_clear
1
as
[??
Var
|];
auto
;
inv
Var
.
+
right
;
auto
.
-
setoid_rewrite
<-
IHtcs
;
split
.
+
inversion_clear
1
as
[??
Var
|];
auto
;
inv
Var
.
+
right
;
auto
.
-
split
.
+
inversion_clear
1
as
[??
Var
|];
try
inv
Var
.
*
apply
in_app
;
auto
.
*
apply
in_app
;
right
;
apply
IHtcs
;
auto
.
+
rewrite
in_app
;
intros
[?|?].
*
left
;
constructor
;
auto
.
*
right
;
apply
IHtcs
;
auto
.
Qed.
Definition
is_variable_in_tc_b
(
x
:
ident
) (
tc
:
trconstr
) :
bool
:=
match
tc
with
|
TcDef
x
'
_
_
=>
ident_eqb
x
x
'
|
TcCall
_
xs
_
_
_
_
=>
existsb
(
ident_eqb
x
)
xs
|
_
=>
false
end
.
Fact
Is_variable_in_tc_reflect
:
forall
x
tc
,
Is_variable_in_tc
x
tc
<->
is_variable_in_tc_b
x
tc
=
true
.
Proof.
destruct
tc
;
simpl
;
split
;
try
discriminate
;
try
now
inversion
1.
-
inversion_clear
1;
apply
ident_eqb_refl
.
-
rewrite
ident_eqb_eq
;
intro
;
subst
;
constructor
.
-
inversion_clear
1.
apply
existsb_exists
;
eexists
;
split
;
eauto
.
apply
ident_eqb_refl
.
-
rewrite
existsb_exists
;
intros
(?&?&
E
).
apply
ident_eqb_eq
in
E
;
subst
.
constructor
;
auto
.
Qed.
Lemma
Is_variable_in_tc_dec
:
forall
x
tc
,
{
Is_variable_in_tc
x
tc
} + { ~
Is_variable_in_tc
x
tc
}.
Proof.
intros
;
eapply
Bool.reflect_dec
,
Bool.iff_reflect
,
Is_variable_in_tc_reflect
.
Qed.
End
STCISVARIABLE
.
Module
StcIsVariableFun
(
Ids
:
IDS
)
(
Op
:
OPERATORS
)
(
CESyn
:
CESYNTAX
Op
)
(
Syn
:
STCSYNTAX
Ids
Op
CESyn
)
<:
STCISVARIABLE
Ids
Op
CESyn
Syn
.
Include
STCISVARIABLE
Ids
Op
CESyn
Syn
.
End
StcIsVariableFun
.