Module Qcert.Imp.Lang.ImpData
Imp with the Q*cert data model
Require
Import
String
.
Require
Import
EquivDec
.
Require
Import
Decidable
.
Require
Import
Utils
.
Require
Import
DataRuntime
.
Require
Import
Imp
.
Section
ImpData
.
Context
{
fruntime
:
foreign_runtime
}.
Section
Syntax
.
Definition
imp_data_model
:=
data
.
Definition
imp_data_constant
:
Set
:=
data
.
Inductive
imp_data_op
:
Set
:=
|
DataOpUnary
:
unary_op
->
imp_data_op
|
DataOpBinary
:
binary_op
->
imp_data_op
.
Inductive
imp_data_runtime_op
:
Set
:=
|
DataRuntimeGroupby
:
string
->
list
string
->
imp_data_runtime_op
|
DataRuntimeEither
:
imp_data_runtime_op
|
DataRuntimeToLeft
:
imp_data_runtime_op
|
DataRuntimeToRight
:
imp_data_runtime_op
.
Definition
imp_data_expr
:= @
imp_expr
imp_data_constant
imp_data_op
imp_data_runtime_op
.
Definition
imp_data_stmt
:= @
imp_stmt
imp_data_constant
imp_data_op
imp_data_runtime_op
.
Definition
imp_data_function
:= @
imp_function
imp_data_constant
imp_data_op
imp_data_runtime_op
.
Definition
imp_data
:= @
imp
imp_data_constant
imp_data_op
imp_data_runtime_op
.
End
Syntax
.
Section
dec
.
Global
Instance
imp_data_constant_eqdec
:
EqDec
imp_data_constant
eq
.
Proof.
apply
data_eqdec
.
Qed.
Global
Instance
imp_data_op_eqdec
:
EqDec
imp_data_op
eq
.
Proof.
change
(
forall
x
y
:
imp_data_op
, {
x
=
y
} + {
x
<>
y
}).
decide
equality
.
apply
unary_op_eqdec
.
apply
binary_op_eqdec
.
Qed.
Global
Instance
imp_data_runtime_op_eqdec
:
EqDec
imp_data_runtime_op
eq
.
Proof.
change
(
forall
x
y
:
imp_data_runtime_op
, {
x
=
y
} + {
x
<>
y
}).
decide
equality
.
-
clear
a
.
revert
l0
;
induction
l
;
intros
;
destruct
l0
;
simpl
in
*;
try
solve
[
right
;
inversion
1].
left
;
reflexivity
.
elim
(
IHl
l0
);
intros
;
clear
IHl
.
+
subst
;
destruct
(
string_dec
a
s1
);
subst
; [
left
;
reflexivity
|
right
;
congruence
].
+
right
;
congruence
.
-
apply
string_eqdec
.
Qed.
Global
Instance
imp_data_expr_eqdec
:
EqDec
imp_data_expr
eq
.
Proof.
apply
(@
imp_expr_eqdec
imp_data_constant
imp_data_op
imp_data_runtime_op
).
apply
imp_data_constant_eqdec
.
apply
imp_data_op_eqdec
.
apply
imp_data_runtime_op_eqdec
.
Qed.
End
dec
.
End
ImpData
.
Tactic
Notation
"
imp_data_runtime_op_cases
"
tactic
(
first
)
ident
(
c
) :=
first
;
[
Case_aux
c
"
DataRuntimeGroupby
"%
string
|
Case_aux
c
"
DataRuntimeEither
"%
string
|
Case_aux
c
"
DataRuntimeLeft
"%
string
|
Case_aux
c
"
DataRuntimeRight
"%
string
].