Module Qcert.Common.Operators.UnaryOperators
Section
UnaryOperators
.
Require
Import
Ascii
.
Require
Import
String
.
Require
Import
ZArith
.
Require
Import
EquivDec
.
Require
Import
Utils
.
Require
Import
BrandRelation
.
Require
Import
ForeignData
.
Require
Import
DataSort
.
Require
Import
ForeignOperators
.
Require
Import
OperatorsUtils
.
Context
{
fdata
:
foreign_data
}.
Context
{
fuop
:
foreign_unary_op
}.
Inductive
nat_arith_unary_op
:=
NatAbs
(* absolute value *)
|
NatLog2
(* base2 logarithm *)
|
NatSqrt
(* square root *)
.
Inductive
float_arith_unary_op
:=
FloatNeg
(* negative *)
|
FloatSqrt
(* square root *)
|
FloatExp
(* exponent *)
|
FloatLog
(* logarithm base 2 *)
|
FloatLog10
(* logarithm base 10 *)
|
FloatCeil
(* ceiling *)
|
FloatFloor
(* floor *)
|
FloatAbs
(* absolute value *)
.
Inductive
unary_op
:
Set
:=
|
OpIdentity
:
unary_op
(* identity, returns its value *)
|
OpNeg
:
unary_op
(* boolean negation *)
|
OpRec
:
string
->
unary_op
(* create a record with a single field *)
|
OpDot
:
string
->
unary_op
(* record field access *)
|
OpRecRemove
:
string
->
unary_op
(* record remove the given fields *)
|
OpRecProject
:
list
string
->
unary_op
(* record projects on the given fields *)
|
OpBag
:
unary_op
(* create a singleton bag *)
|
OpSingleton
:
unary_op
(* value within a singleton bag *)
|
OpFlatten
:
unary_op
(* flattens a bag of bags *)
|
OpDistinct
:
unary_op
(* distinct values in a bag *)
|
OpOrderBy
:
SortCriterias
->
unary_op
(* sorts a collection of records *)
|
OpCount
:
unary_op
(* bag count *)
|
OpToString
:
unary_op
(* convert any data to a string *)
|
OpSubstring
:
Z
->
option
Z
->
unary_op
(* returns the substring starting with the nth character, for m characters (or the rest of the string) *)
|
OpLike
(
pattern
:
string
)
(
escape
:
option
ascii
) :
unary_op
(* like expression (as in sql) *)
|
OpLeft
:
unary_op
(* create a left value *)
|
OpRight
:
unary_op
(* create a right value *)
|
OpBrand
:
brands
->
unary_op
(* brands a value *)
|
OpUnbrand
:
unary_op
(* content of a branded value *)
|
OpCast
:
brands
->
unary_op
(* coerce a branded value into one of its sub-brands *)
|
OpNatUnary
:
nat_arith_unary_op
->
unary_op
(* arithmetic operations on natural floats *)
|
OpNatSum
:
unary_op
(* sum of natural floats in a bag *)
|
OpNatMin
:
unary_op
(* minimum of natural floats in a bag *)
|
OpNatMax
:
unary_op
(* maximum of natural floats in a bag *)
|
OpNatMean
:
unary_op
(* arithmetic mean of natural floats in a bag *)
|
OpFloatOfNat
:
unary_op
(* coercion from natural float to float *)
|
OpFloatUnary
:
float_arith_unary_op
->
unary_op
(* arithmetic operations on floats *)
|
OpFloatTruncate
:
unary_op
(* truncate *)
|
OpFloatSum
:
unary_op
(* sum *)
|
OpFloatMean
:
unary_op
(* arithmetic mean *)
|
OpFloatBagMin
:
unary_op
(* minimum *)
|
OpFloatBagMax
:
unary_op
(* maximum *)
|
OpForeignUnary
(
fu
:
foreign_unary_op_type
) :
unary_op
(* foreign unary operators *)
.
Global
Instance
nat_arith_unary_op_eqdec
:
EqDec
nat_arith_unary_op
eq
.
Proof.
change
(
forall
x
y
:
nat_arith_unary_op
, {
x
=
y
} + {
x
<>
y
}).
decide
equality
.
Defined.
Global
Instance
float_arith_unary_op_eqdec
:
EqDec
float_arith_unary_op
eq
.
Proof.
change
(
forall
x
y
:
float_arith_unary_op
, {
x
=
y
} + {
x
<>
y
}).
decide
equality
.
Defined.
Global
Instance
SortCriterias_eqdec
:
EqDec
SortCriterias
eq
.
Proof.
change
(
forall
x
y
:
SortCriterias
, {
x
=
y
} + {
x
<>
y
}).
decide
equality
;
try
apply
string_dec
.
decide
equality
;
try
apply
string_dec
.
decide
equality
;
try
apply
string_dec
.
Defined.
Global
Instance
unary_op_eqdec
:
EqDec
unary_op
eq
.
Proof.
change
(
forall
x
y
:
unary_op
, {
x
=
y
} + {
x
<>
y
}).
decide
equality
;
try
apply
string_dec
.
-
induction
l
;
decide
equality
;
apply
string_dec
.
-
apply
SortCriterias_eqdec
.
-
apply
option_eqdec
.
-
apply
Z_eqdec
.
-
apply
equiv_dec
.
-
induction
b
;
decide
equality
;
apply
string_dec
.
-
induction
b
;
decide
equality
;
apply
string_dec
.
-
apply
nat_arith_unary_op_eqdec
.
-
apply
float_arith_unary_op_eqdec
.
-
apply
foreign_unary_op_dec
.
Defined.
Local
Open
Scope
string
.
Global
Instance
ToString_nat_arith_unary_op
:
ToString
nat_arith_unary_op
:= {
toString
:=
fun
(
op
:
nat_arith_unary_op
) =>
match
op
with
|
NatAbs
=> "
NatAbs
"
|
NatLog2
=> "
NatLog2
"
|
NatSqrt
=> "
NatSqrt
"
end
}.
Global
Instance
ToString_float_arith_unary_op
:
ToString
float_arith_unary_op
:= {
toString
:=
fun
(
op
:
float_arith_unary_op
) =>
match
op
with
|
FloatNeg
=> "
FloatNeg
"
|
FloatSqrt
=> "
FloatSqrt
"
|
FloatExp
=> "
FloatExp
"
|
FloatLog
=> "
FloatLog
"
|
FloatLog10
=> "
FloatLog10
"
|
FloatCeil
=> "
FloatCeil
"
|
FloatFloor
=> "
FloatFloor
"
|
FloatAbs
=> "
FloatAbs
"
end
}.
Definition
ToString_SortDesc
sd
:=
match
sd
with
|
Ascending
=> "
asc
"
|
Descending
=> "
desc
"
end
.
Definition
ToString_SortCriteria
(
sc
:
string
*
SortDesc
) :=
let
(
att
,
sd
) :=
sc
in
bracketString
"(" (
att
++ "," ++ (
ToString_SortDesc
sd
)) ")".
Global
Instance
ToString_unary_op
:
ToString
unary_op
:= {
toString
:=
fun
(
op
:
unary_op
) =>
match
op
with
|
OpIdentity
=> "
OpIdentity
"
|
OpNeg
=> "
OpNeg
"
|
OpRec
f
=> "(
OpRec
" ++
f
++ ")"
|
OpDot
s
=> "(
OpDot
" ++
s
++ ")"
|
OpRecRemove
s
=> "(
OpRecRemove
" ++
s
++ ")"
|
OpRecProject
ls
=> "(
OpRecProject
"
++ (
bracketString
"[" (
joinStrings
","
ls
) "]")
++ ")"
|
OpBag
=> "
OpBag
"
|
OpSingleton
=> "
OpSingleton
"
|
OpFlatten
=> "
OpFlatten
"
|
OpDistinct
=> "
OpDistinct
"
|
OpOrderBy
ls
=>
"(
OpOrderBy
"
++ (
bracketString
"[" (
joinStrings
"," (
List.map
ToString_SortCriteria
ls
)) "]")
++ ")"
|
OpCount
=> "
OpCount
"
|
OpToString
=> "
OpToString
"
|
OpSubstring
start
len
=>
"(
OpSubstring
" ++ (
toString
start
)
++ (
match
len
with
|
None
=> ""
|
Some
len
=> " " ++ (
toString
len
)
end
) ++ ")"
|
OpLike
pattern
oescape
=>
"(
OpLike
" ++
pattern
++ (
match
oescape
with
|
None
=> ""
|
Some
escape
=> "
ESCAPE
" ++ (
String
escape
EmptyString
)
end
) ++ ")"
|
OpLeft
=> "
OpLeft
"
|
OpRight
=> "
OpRight
"
|
OpBrand
b
=> "(
OpBrand
" ++ (@
toString
_
ToString_brands
b
)++ ")"
|
OpUnbrand
=> "
OpUnbrand
"
|
OpCast
b
=> "(
OpCast
" ++ (@
toString
_
ToString_brands
b
) ++ ")"
|
OpNatUnary
aop
=> "(
OpNatUnary
" ++
toString
aop
++ ")"
|
OpNatSum
=> "
OpNatSum
"
|
OpNatMin
=> "
OpNatMin
"
|
OpNatMax
=> "
OpNatMax
"
|
OpNatMean
=> "
OpNatMean
"
|
OpFloatOfNat
=> "
OpFloatOfNat
"
|
OpFloatUnary
aop
=> "(
OpFloatUnary
" ++
toString
aop
++ ")"
|
OpFloatTruncate
=> "
OpFloatTruncate
"
|
OpFloatSum
=> "
OpFloatSum
"
|
OpFloatMean
=> "
OpFloatMean
"
|
OpFloatBagMin
=> "
OpFloatBagMin
"
|
OpFloatBagMax
=> "
OpFloatBagMax
"
|
OpForeignUnary
fu
=>
toString
fu
end
}.
End
UnaryOperators
.
Tactic
Notation
"
unary_op_cases
"
tactic
(
first
)
ident
(
c
) :=
first
;
[
Case_aux
c
"
OpIdentity
"%
string
|
Case_aux
c
"
OpNeg
"%
string
|
Case_aux
c
"
OpRec
"%
string
|
Case_aux
c
"
OpDot
"%
string
|
Case_aux
c
"
OpRecRemove
"%
string
|
Case_aux
c
"
OpRecProject
"%
string
|
Case_aux
c
"
OpBag
"%
string
|
Case_aux
c
"
OpSingleton
"%
string
|
Case_aux
c
"
OpFlatten
"%
string
|
Case_aux
c
"
OpDistinct
"%
string
|
Case_aux
c
"
OpOrderBy
"%
string
|
Case_aux
c
"
OpCount
"%
string
|
Case_aux
c
"
OpToString
"%
string
|
Case_aux
c
"
OpSubstring
"%
string
|
Case_aux
c
"
OpLike
"%
string
|
Case_aux
c
"
OpLeft
"%
string
|
Case_aux
c
"
OpRight
"%
string
|
Case_aux
c
"
OpBrand
"%
string
|
Case_aux
c
"
OpUnbrand
"%
string
|
Case_aux
c
"
OpCast
"%
string
|
Case_aux
c
"
OpNatUnary
"%
string
|
Case_aux
c
"
OpNatSum
"%
string
|
Case_aux
c
"
OpNatMin
"%
string
|
Case_aux
c
"
OpNatMax
"%
string
|
Case_aux
c
"
OpNatMean
"%
string
|
Case_aux
c
"
OpFloatOfNat
"%
string
|
Case_aux
c
"
OpFloatUnary
"%
string
|
Case_aux
c
"
OpFloatTruncate
"%
string
|
Case_aux
c
"
OpFloatSum
"%
string
|
Case_aux
c
"
OpFloatMean
"%
string
|
Case_aux
c
"
OpFloatBagMin
"%
string
|
Case_aux
c
"
OpFloatBagMax
"%
string
|
Case_aux
c
"
OpForeignUnary
"%
string
].