Qcert.Compiler.Model.EnhancedModel
Definition check_subtype_pairs
{br:brand_relation}
{fr:foreign_type}
(l:list (rtype×rtype)) : bool
:= forallb (fun τs ⇒ if subtype_dec (fst τs) (snd τs) then true else false) l.
Definition enforce_unary_op_schema
{br:brand_relation}
{fr:foreign_type}
(ts1:rtype×rtype) (tr:rtype)
: option (rtype×rtype)
:= if check_subtype_pairs (ts1::nil)
then Some (tr, (snd ts1))
else None.
Definition enforce_binary_op_schema
{br:brand_relation}
{fr:foreign_type}
(ts1:rtype×rtype) (ts2:rtype×rtype) (tr:rtype)
: option (rtype×rtype×rtype)
:= if check_subtype_pairs (ts1::ts2::nil)
then Some (tr, (snd ts1), (snd ts2))
else None.
Inductive enhanced_data : Set
:=
| enhancedfloat : FLOAT → enhanced_data
| enhancedstring : STRING → enhanced_data
| enhancedtimescale : time_scale → enhanced_data
| enhancedtimeduration : TIME_DURATION → enhanced_data
| enhancedtimepoint : TIME_POINT → enhanced_data
| enhancedsqldate : SQL_DATE → enhanced_data
| enhancedsqldateinterval : SQL_DATE_INTERVAL → enhanced_data
.
Inductive enhanced_type : Set
:=
| enhancedTop : enhanced_type
| enhancedBottom : enhanced_type
| enhancedFloat : enhanced_type
| enhancedString : enhanced_type
| enhancedTimeScale : enhanced_type
| enhancedTimeDuration : enhanced_type
| enhancedTimePoint : enhanced_type
| enhancedSqlDate : enhanced_type
| enhancedSqlDateInterval : enhanced_type
.
Definition enhanced_type_to_string (et:enhanced_type) : string :=
match et with
| enhancedTop ⇒ "ETop"
| enhancedBottom ⇒ "EBottom"
| enhancedFloat ⇒ "EFloat"
| enhancedString ⇒ "EString"
| enhancedTimeScale ⇒ "ETimeScale"
| enhancedTimeDuration ⇒ "ETimeDuration"
| enhancedTimePoint ⇒ "ETimePoint"
| enhancedSqlDate ⇒ "ESqlDate"
| enhancedSqlDateInterval ⇒ "ESqlDateInterval"
end.
Definition string_to_enhanced_type (s:string) : option enhanced_type :=
match s with
| "ETop"%string ⇒ Some enhancedTop
| "EBottom"%string ⇒ Some enhancedBottom
| "EFloat"%string ⇒ Some enhancedFloat
| "EString"%string ⇒ Some enhancedString
| "ETimeScale"%string ⇒ Some enhancedTimeScale
| "ETimeDuration"%string ⇒ Some enhancedTimeDuration
| "ETimePoint"%string ⇒ Some enhancedTimePoint
| "ESqlDate"%string ⇒ Some enhancedSqlDate
| "ESqlDateInterval"%string ⇒ Some enhancedSqlDateInterval
| _ ⇒ None
end.
Program Instance enhanced_foreign_data : foreign_data
:= mk_foreign_data enhanced_data _ _ _ _ _ _.
Definition denhancedfloat f := dforeign (enhancedfloat f).
Definition denhancedstring s := dforeign (enhancedstring s).
Definition denhancedtimescale ts := dforeign (enhancedtimescale ts).
Definition denhancedtimeduration td := dforeign (enhancedtimeduration td).
Definition denhancedtimepoint tp := dforeign (enhancedtimepoint tp).
Definition denhancedsqldate td := dforeign (enhancedsqldate td).
Definition denhancedsqldateinterval td := dforeign (enhancedsqldateinterval td).
Definition jenhancedfloat f := jforeign (enhancedfloat f).
Definition jenhancedstring s := jforeign (enhancedstring s).
Definition jenhancedtimescale ts := jforeign (enhancedtimescale ts).
Definition jenhancedtimeduration td := jforeign (enhancedtimeduration td).
Definition jenhancedtimepoint tp := jforeign (enhancedtimepoint tp).
Definition jenhancedsqldate td := jforeign (enhancedsqldate td).
Definition jenhancedsqldateinterval td := jforeign (enhancedsqldateinterval td).
Inductive enhanced_unary_op
:=
| enhanced_unary_float_op : float_unary_op → enhanced_unary_op
| enhanced_unary_time_op : time_unary_op → enhanced_unary_op
| enhanced_unary_sql_date_op : sql_date_unary_op → enhanced_unary_op.
Definition ondfloat {A} (f : FLOAT → A) (d : data) : option A
:= match d with
| dforeign (enhancedfloat fd) ⇒ Some (f fd)
| _ ⇒ None
end.
Definition ondsqldate {A} (f : SQL_DATE → A) (d : data) : option A
:= match d with
| dforeign (enhancedsqldate fd) ⇒ Some (f fd)
| _ ⇒ None
end.
Definition rondfloat (f: FLOAT → FLOAT) (d:data) : option data
:= lift denhancedfloat (ondfloat f d).
Definition ondcollfloat {A} (f : list FLOAT → A) (d : data) : option A
:= lift_oncoll (fun x ⇒ lift f (rmap (fun z ⇒ ondfloat id z) x)) d.
Definition rondcollfloat (f: list FLOAT → FLOAT) (d:data) : option data
:= lift denhancedfloat (ondcollfloat f d).
Definition float_unary_op_interp (op:float_unary_op) (d:data) : option data
:= match op with
| uop_float_neg ⇒ rondfloat FLOAT_neg d
| uop_float_sqrt ⇒ rondfloat FLOAT_sqrt d
| uop_float_exp ⇒ rondfloat FLOAT_exp d
| uop_float_log ⇒ rondfloat FLOAT_log d
| uop_float_log10 ⇒ rondfloat FLOAT_log10 d
| uop_float_of_int ⇒ lift denhancedfloat (ondnat FLOAT_of_int d)
| uop_float_ceil ⇒ rondfloat FLOAT_ceil d
| uop_float_floor ⇒ rondfloat FLOAT_floor d
| uop_float_truncate ⇒ lift dnat (ondfloat FLOAT_truncate d)
| uop_float_abs ⇒ rondfloat FLOAT_abs d
| uop_float_sum ⇒ rondcollfloat FLOAT_sum d
| uop_float_arithmean ⇒ rondcollfloat FLOAT_arithmean d
| uop_float_listmin ⇒ rondcollfloat FLOAT_listmin d
| uop_float_listmax ⇒ rondcollfloat FLOAT_listmax d
end.
Definition ondstring {A} (f : String.string → A) (d : data) : option A
:= match d with
| dstring s ⇒ Some (f s)
| _ ⇒ None
end.
Definition ondtimepoint {A} (f : TIME_POINT → A) (d : data) : option A
:= match d with
| dforeign (enhancedtimepoint fd) ⇒ Some (f fd)
| _ ⇒ None
end.
Definition time_unary_op_interp (op:time_unary_op) (d:data) : option data
:= match op with
| uop_time_to_scale ⇒ lift denhancedtimescale (ondtimepoint TIME_POINT_to_scale d)
| uop_time_from_string ⇒ lift denhancedtimepoint (ondstring TIME_POINT_from_string d)
| uop_time_duration_from_string ⇒ lift denhancedtimeduration (ondstring TIME_DURATION_from_string d)
end.
Definition sql_date_unary_op_interp (op:sql_date_unary_op) (d:data) : option data
:= match op with
| uop_sql_get_date_component part ⇒
lift dnat (ondsqldate (SQL_DATE_get_component part) d)
| uop_sql_date_from_string ⇒
lift denhancedsqldate (ondstring SQL_DATE_from_string d)
| uop_sql_date_interval_from_string ⇒
lift denhancedsqldateinterval (ondstring SQL_DATE_INTERVAL_from_string d)
end.
Definition enhanced_unary_op_interp
(br:brand_relation_t)
(op:enhanced_unary_op)
(d:data) : option data
:= match op with
| enhanced_unary_float_op f ⇒ float_unary_op_interp f d
| enhanced_unary_time_op f ⇒ time_unary_op_interp f d
| enhanced_unary_sql_date_op f ⇒ sql_date_unary_op_interp f d
end.
Program Instance enhanced_foreign_unary_op : foreign_unary_op
:= { foreign_unary_op_type := enhanced_unary_op
; foreign_unary_op_interp := enhanced_unary_op_interp }.
Definition ondfloat2 {A} (f : FLOAT → FLOAT → A) (d1 d2 : data) : option A
:= match d1, d2 with
| dforeign (enhancedfloat fd1), dforeign (enhancedfloat fd2) ⇒ Some (f fd1 fd2)
| _, _ ⇒ None
end.
Definition rondfloat2 (f: FLOAT → FLOAT → FLOAT) (d1 d2:data) : option data
:= lift denhancedfloat (ondfloat2 f d1 d2).
Definition rondboolfloat2 (f: FLOAT → FLOAT → bool) (d1 d2:data) : option data
:= lift dbool (ondfloat2 f d1 d2).
Inductive enhanced_binary_op
:=
| enhanced_binary_float_op : float_binary_op → enhanced_binary_op
| enhanced_binary_time_op : time_binary_op → enhanced_binary_op
| enhanced_binary_sql_date_op : sql_date_binary_op → enhanced_binary_op
.
Definition float_binary_op_interp
(op:float_binary_op) (d1 d2:data) : option data
:= match op with
| bop_float_plus ⇒ rondfloat2 FLOAT_plus d1 d2
| bop_float_minus ⇒ rondfloat2 FLOAT_minus d1 d2
| bop_float_mult ⇒ rondfloat2 FLOAT_mult d1 d2
| bop_float_div ⇒ rondfloat2 FLOAT_div d1 d2
| bop_float_pow ⇒ rondfloat2 FLOAT_pow d1 d2
| bop_float_min ⇒ rondfloat2 FLOAT_min d1 d2
| bop_float_max ⇒ rondfloat2 FLOAT_max d1 d2
| bop_float_ne ⇒ rondboolfloat2 FLOAT_ne d1 d2
| bop_float_lt ⇒ rondboolfloat2 FLOAT_lt d1 d2
| bop_float_le ⇒ rondboolfloat2 FLOAT_le d1 d2
| bop_float_gt ⇒ rondboolfloat2 FLOAT_gt d1 d2
| bop_float_ge ⇒ rondboolfloat2 FLOAT_ge d1 d2
end.
Definition ondtimepoint2 {A} (f : TIME_POINT → TIME_POINT → A) (d1 d2 : data) : option A
:= match d1, d2 with
| dforeign (enhancedtimepoint fd1), dforeign (enhancedtimepoint fd2) ⇒ Some (f fd1 fd2)
| _, _ ⇒ None
end.
Definition rondbooltimepoint2 (f: TIME_POINT → TIME_POINT → bool) (d1 d2:data) : option data
:= lift dbool (ondtimepoint2 f d1 d2).
Definition rondtimepoint2 (f: TIME_POINT → TIME_POINT → TIME_POINT) (d1 d2:data) : option data
:= lift denhancedtimepoint (ondtimepoint2 f d1 d2).
Definition ondsqldate2 {A} (f : SQL_DATE → SQL_DATE → A) (d1 d2 : data) : option A
:= match d1, d2 with
| dforeign (enhancedsqldate fd1), dforeign (enhancedsqldate fd2) ⇒ Some (f fd1 fd2)
| _, _ ⇒ None
end.
Definition rondboolsqldate2 (f: SQL_DATE → SQL_DATE → bool) (d1 d2:data) : option data
:= lift dbool (ondsqldate2 f d1 d2).
Definition time_binary_op_interp
(op:time_binary_op) (d1 d2:data) : option data
:= match op with
| bop_time_as ⇒
match d1, d2 with
| dforeign (enhancedtimepoint tp), dforeign (enhancedtimescale ts)
⇒ Some (denhancedtimepoint (TIME_POINT_as tp ts))
| _,_ ⇒ None
end
| bop_time_shift ⇒
match d1, d2 with
| dforeign (enhancedtimepoint tp), dforeign (enhancedtimeduration td)
⇒ Some (denhancedtimepoint (TIME_POINT_shift tp td))
| _,_ ⇒ None
end
| bop_time_ne ⇒ rondbooltimepoint2 TIME_POINT_ne d1 d2
| bop_time_lt ⇒ rondbooltimepoint2 TIME_POINT_lt d1 d2
| bop_time_le ⇒ rondbooltimepoint2 TIME_POINT_le d1 d2
| bop_time_gt ⇒ rondbooltimepoint2 TIME_POINT_gt d1 d2
| bop_time_ge ⇒ rondbooltimepoint2 TIME_POINT_ge d1 d2
| bop_time_duration_from_scale ⇒
match d1, d2 with
| dforeign (enhancedtimescale ts), (dnat count)
⇒ Some (denhancedtimeduration (TIME_DURATION_from_scale ts count))
| _,_ ⇒ None
end
| bop_time_duration_between ⇒ lift denhancedtimeduration (ondtimepoint2 TIME_DURATION_between d1 d2)
end.
Definition sql_date_binary_op_interp
(op:sql_date_binary_op) (d1 d2:data) : option data
:= match op with
| bop_sql_date_plus
⇒ match d1, d2 with
| dforeign (enhancedsqldate tp), dforeign (enhancedsqldateinterval td)
⇒ Some (denhancedsqldate (SQL_DATE_plus tp td))
| _,_ ⇒ None
end
| bop_sql_date_minus
⇒ match d1, d2 with
| dforeign (enhancedsqldate tp), dforeign (enhancedsqldateinterval td)
⇒ Some (denhancedsqldate (SQL_DATE_minus tp td))
| _,_ ⇒ None
end
| bop_sql_date_ne ⇒ rondboolsqldate2 SQL_DATE_ne d1 d2
| bop_sql_date_lt ⇒ rondboolsqldate2 SQL_DATE_lt d1 d2
| bop_sql_date_le ⇒ rondboolsqldate2 SQL_DATE_le d1 d2
| bop_sql_date_gt ⇒ rondboolsqldate2 SQL_DATE_gt d1 d2
| bop_sql_date_ge ⇒ rondboolsqldate2 SQL_DATE_ge d1 d2
| bop_sql_date_interval_between ⇒ lift denhancedsqldateinterval (ondsqldate2 SQL_DATE_INTERVAL_between d1 d2)
end.
Definition enhanced_binary_op_interp
(br:brand_relation_t)
(op:enhanced_binary_op)
(d1 d2:data) : option data
:= match op with
| enhanced_binary_float_op f ⇒ float_binary_op_interp f d1 d2
| enhanced_binary_time_op f ⇒ time_binary_op_interp f d1 d2
| enhanced_binary_sql_date_op f ⇒ sql_date_binary_op_interp f d1 d2
end.
Program Instance enhanced_foreign_binary_op : foreign_binary_op
:= { foreign_binary_op_type := enhanced_binary_op
; foreign_binary_op_interp := enhanced_binary_op_interp }.
Instance enhanced_foreign_runtime :
foreign_runtime
:= mk_foreign_runtime
enhanced_foreign_data
enhanced_foreign_unary_op
enhanced_foreign_binary_op.
Definition enhanced_to_java_data
(quotel:String.string) (fd:enhanced_data) : java_json
:= match fd with
| enhancedfloat f ⇒ mk_java_json (FLOAT_tostring f)
| enhancedstring s ⇒ mk_java_json (STRING_tostring s)
| enhancedtimescale ts ⇒ mk_java_json (time_scale_to_java_string ts)
| enhancedtimeduration td ⇒ mk_java_json (@toString _ time_duration_foreign_data.(@foreign_data_tostring ) td)
| enhancedtimepoint tp ⇒ mk_java_json (@toString _ time_point_foreign_data.(@foreign_data_tostring ) tp)
| enhancedsqldate tp ⇒ mk_java_json (@toString _ sql_date_foreign_data.(@foreign_data_tostring ) tp)
| enhancedsqldateinterval tp ⇒ mk_java_json (@toString _ sql_date_interval_foreign_data.(@foreign_data_tostring ) tp)
end.
Definition enhanced_to_java_unary_op
(indent:nat) (eol:String.string)
(quotel:String.string) (fu:enhanced_unary_op)
(d:java_json) : java_json
:= match fu with
| enhanced_unary_float_op op ⇒
float_to_java_unary_op indent eol quotel op d
| enhanced_unary_time_op op ⇒
time_to_java_unary_op indent eol quotel op d
| enhanced_unary_sql_date_op op ⇒
sql_date_to_java_unary_op indent eol quotel op d
end.
Definition enhanced_to_java_binary_op
(indent:nat) (eol:String.string)
(quotel:String.string) (fb:enhanced_binary_op)
(d1 d2:java_json) : java_json
:= match fb with
| enhanced_binary_float_op op ⇒
float_to_java_binary_op indent eol quotel op d1 d2
| enhanced_binary_time_op op ⇒
time_to_java_binary_op indent eol quotel op d1 d2
| enhanced_binary_sql_date_op op ⇒
sql_date_to_java_binary_op indent eol quotel op d1 d2
end.
Instance enhanced_foreign_to_java :
@foreign_to_java enhanced_foreign_runtime
:= mk_foreign_to_java
enhanced_foreign_runtime
enhanced_to_java_data
enhanced_to_java_unary_op
enhanced_to_java_binary_op.
Definition enhanced_to_javascript_data
(quotel:String.string) (fd:enhanced_data) : String.string
:= match fd with
| enhancedfloat f ⇒ FLOAT_tostring f
| enhancedstring s ⇒ STRING_tostring s
| enhancedtimescale ts ⇒ toString ts
| enhancedtimeduration td ⇒ (@toString _ time_duration_foreign_data.(@foreign_data_tostring ) td)
| enhancedtimepoint tp ⇒ (@toString _ time_point_foreign_data.(@foreign_data_tostring ) tp)
| enhancedsqldate tp ⇒ (@toString _ sql_date_foreign_data.(@foreign_data_tostring ) tp)
| enhancedsqldateinterval tp ⇒ (@toString _ sql_date_interval_foreign_data.(@foreign_data_tostring ) tp)
end.
Definition enhanced_to_javascript_unary_op
(indent:nat) (eol:String.string)
(quotel:String.string) (fu:enhanced_unary_op)
(d:String.string) : String.string
:= match fu with
| enhanced_unary_float_op op ⇒
float_to_javascript_unary_op indent eol quotel op d
| enhanced_unary_time_op op ⇒
time_to_javascript_unary_op indent eol quotel op d
| enhanced_unary_sql_date_op op ⇒
sql_date_to_javascript_unary_op indent eol quotel op d
end.
Definition enhanced_to_javascript_binary_op
(indent:nat) (eol:String.string)
(quotel:String.string) (fb:enhanced_binary_op)
(d1 d2:String.string) : String.string
:= match fb with
| enhanced_binary_float_op op ⇒
float_to_javascript_binary_op indent eol quotel op d1 d2
| enhanced_binary_time_op op ⇒
time_to_javascript_binary_op indent eol quotel op d1 d2
| enhanced_binary_sql_date_op op ⇒
sql_date_to_javascript_binary_op indent eol quotel op d1 d2
end.
Instance enhanced_foreign_to_javascript :
@foreign_to_javascript enhanced_foreign_runtime
:= mk_foreign_to_javascript
enhanced_foreign_runtime
enhanced_to_javascript_data
enhanced_to_javascript_unary_op
enhanced_to_javascript_binary_op.
Definition enhanced_to_scala_unary_op (op: enhanced_unary_op) (d: string) : string :=
match op with
| enhanced_unary_float_op op ⇒
float_to_scala_unary_op op d
| enhanced_unary_time_op op ⇒ "EnhancedModel: Time ops not supported for now."
| enhanced_unary_sql_date_op op ⇒ "EnhancedModel: SQL date ops not supported for now."
end.
Definition enhanced_to_scala_spark_datatype {ftype: foreign_type} (ft: foreign_type_type) : string :=
"FloatType".
Instance enhanced_foreign_to_scala {ftype: foreign_type}:
@foreign_to_scala enhanced_foreign_runtime _
:= mk_foreign_to_scala
enhanced_foreign_runtime _
enhanced_to_scala_unary_op
enhanced_to_scala_spark_datatype.
Program Instance enhanced_foreign_to_JSON : foreign_to_JSON
:= mk_foreign_to_JSON enhanced_foreign_data _ _.
Inductive enhanced_numeric_type :=
| enhanced_numeric_int
| enhanced_numeric_float.
Global Instance enhanced_numeric_type_eqdec : EqDec enhanced_numeric_type eq.
Definition enhanced_to_cld_numeric_type
(typ:enhanced_numeric_type) : CldMR.cld_numeric_type
:= match typ with
| enhanced_numeric_int ⇒ CldMR.Cld_int
| enhanced_numeric_float ⇒ CldMR.Cld_float
end.
Inductive enhanced_reduce_op
:= RedOpCount : enhanced_reduce_op
| RedOpSum (typ:enhanced_numeric_type) : enhanced_reduce_op
| RedOpMin (typ:enhanced_numeric_type) : enhanced_reduce_op
| RedOpMax (typ:enhanced_numeric_type) : enhanced_reduce_op
| RedOpArithMean (typ:enhanced_numeric_type) : enhanced_reduce_op
| RedOpStats (typ:enhanced_numeric_type) : enhanced_reduce_op.
Definition enhanced_numeric_type_prefix
(typ:enhanced_numeric_type) : string
:= match typ with
| enhanced_numeric_int ⇒ ""%string
| enhanced_numeric_float ⇒ "F"%string
end.
Definition enhanced_reduce_op_tostring (op:enhanced_reduce_op) : string
:= match op with
| RedOpCount ⇒ "COUNT"%string
| RedOpSum typ ⇒ append (enhanced_numeric_type_prefix typ) "FSUM"%string
| RedOpMin typ ⇒ append (enhanced_numeric_type_prefix typ) "FMIN"%string
| RedOpMax typ ⇒ append (enhanced_numeric_type_prefix typ) "FMAX"%string
| RedOpArithMean typ ⇒ append (enhanced_numeric_type_prefix typ) "FARITHMEAN"%string
| RedOpStats typ ⇒ append (enhanced_numeric_type_prefix typ) "FSTATS"%string
end.
Definition enhanced_numeric_sum (typ:enhanced_numeric_type) : unaryOp
:= match typ with
| enhanced_numeric_int
⇒ ASum
| enhanced_numeric_float
⇒ AForeignUnaryOp (enhanced_unary_float_op uop_float_sum)
end.
Definition enhanced_numeric_min (typ:enhanced_numeric_type) : unaryOp
:= match typ with
| enhanced_numeric_int
⇒ ANumMin
| enhanced_numeric_float
⇒ AForeignUnaryOp (enhanced_unary_float_op uop_float_listmin)
end.
Definition enhanced_numeric_max (typ:enhanced_numeric_type) : unaryOp
:= match typ with
| enhanced_numeric_int
⇒ ANumMax
| enhanced_numeric_float
⇒ AForeignUnaryOp (enhanced_unary_float_op uop_float_listmax)
end.
Definition enhanced_numeric_arith_mean (typ:enhanced_numeric_type) : unaryOp
:= match typ with
| enhanced_numeric_int
⇒ AArithMean
| enhanced_numeric_float
⇒ AForeignUnaryOp (enhanced_unary_float_op uop_float_arithmean)
end.
Definition enhanced_reduce_op_interp
(br:brand_relation_t)
(op:enhanced_reduce_op)
(dl:list data) : option data
:= match op with
| RedOpCount | RedOpSum _ | RedOpMin _ | RedOpMax _ | RedOpArithMean _ ⇒
let uop :=
match op with
| RedOpCount ⇒ ACount
| RedOpSum typ ⇒ enhanced_numeric_sum typ
| RedOpMin typ ⇒ enhanced_numeric_min typ
| RedOpMax typ ⇒ enhanced_numeric_max typ
| RedOpArithMean typ ⇒ enhanced_numeric_arith_mean typ
| RedOpStats _ ⇒ ACount
end
in
fun_of_unaryop br uop (dcoll dl)
| RedOpStats typ ⇒
let coll := dcoll dl in
let count := fun_of_unaryop br ACount coll in
let sum := fun_of_unaryop br (enhanced_numeric_sum typ) coll in
let min := fun_of_unaryop br (enhanced_numeric_min typ) coll in
let max := fun_of_unaryop br (enhanced_numeric_max typ) coll in
let v :=
match (count, sum, min, max) with
| (Some count, Some sum, Some min, Some max) ⇒
Some (drec (("count"%string, count)
::("max"%string, max)
::("min"%string, min)
::("sum"%string, sum)
::nil))
| _ ⇒ None
end
in
v
end.
Program Instance enhanced_foreign_reduce_op : foreign_reduce_op
:= mk_foreign_reduce_op enhanced_foreign_data enhanced_reduce_op _ _ enhanced_reduce_op_interp _.
Definition enhanced_to_reduce_op (uop:unaryOp) : option NNRCMR.reduce_op
:= match uop with
| ACount ⇒ Some (NNRCMR.RedOpForeign RedOpCount)
| ASum ⇒
Some (NNRCMR.RedOpForeign (RedOpSum enhanced_numeric_int))
| AForeignUnaryOp (enhanced_unary_float_op uop_float_sum) ⇒
Some (NNRCMR.RedOpForeign (RedOpSum enhanced_numeric_float))
| ANumMin ⇒
Some (NNRCMR.RedOpForeign (RedOpMin enhanced_numeric_int))
| AForeignUnaryOp (enhanced_unary_float_op uop_float_listmin) ⇒
Some (NNRCMR.RedOpForeign (RedOpMin enhanced_numeric_float))
| ANumMax ⇒
Some (NNRCMR.RedOpForeign (RedOpMax enhanced_numeric_int))
| AForeignUnaryOp (enhanced_unary_float_op uop_float_listmax) ⇒
Some (NNRCMR.RedOpForeign (RedOpMax enhanced_numeric_float))
| AArithMean ⇒
Some (NNRCMR.RedOpForeign (RedOpArithMean enhanced_numeric_int))
| AForeignUnaryOp (enhanced_unary_float_op uop_float_arithmean) ⇒
Some (NNRCMR.RedOpForeign (RedOpArithMean enhanced_numeric_float))
| _ ⇒ None
end.
Definition enhanced_of_reduce_op (rop:NNRCMR.reduce_op) : option unaryOp
:= match rop with
| NNRCMR.RedOpForeign RedOpCount ⇒ Some ACount
| NNRCMR.RedOpForeign (RedOpSum enhanced_numeric_int) ⇒
Some (ASum)
| NNRCMR.RedOpForeign (RedOpSum enhanced_numeric_float) ⇒
Some (AForeignUnaryOp (enhanced_unary_float_op uop_float_sum))
| NNRCMR.RedOpForeign (RedOpMin enhanced_numeric_int) ⇒
Some (ANumMin)
| NNRCMR.RedOpForeign (RedOpMin enhanced_numeric_float) ⇒
Some (AForeignUnaryOp (enhanced_unary_float_op uop_float_listmin))
| NNRCMR.RedOpForeign (RedOpMax enhanced_numeric_int) ⇒
Some (ANumMax)
| NNRCMR.RedOpForeign (RedOpMax enhanced_numeric_float) ⇒
Some (AForeignUnaryOp (enhanced_unary_float_op uop_float_listmax))
| NNRCMR.RedOpForeign (RedOpArithMean enhanced_numeric_int) ⇒
Some (AArithMean)
| NNRCMR.RedOpForeign (RedOpArithMean enhanced_numeric_float) ⇒
Some (AForeignUnaryOp (enhanced_unary_float_op uop_float_arithmean))
| NNRCMR.RedOpForeign (RedOpStats _) ⇒
None
end.
Program Instance enhanced_foreign_to_reduce_op : foreign_to_reduce_op
:= mk_foreign_to_reduce_op enhanced_foreign_runtime enhanced_foreign_reduce_op enhanced_to_reduce_op _ enhanced_of_reduce_op _.
Definition enhanced_to_spark_reduce_op
(rop:enhanced_reduce_op)
(scala_endl quotel:string) : string
:= match rop with
| RedOpCount ⇒ ".count().toString()"
| RedOpSum enhanced_numeric_int ⇒ ".aggregate(0)(_ + _.toInt, _ + _).toString()"
| RedOpSum enhanced_numeric_float ⇒ ".aggregate(0.0)(_ + _.toDouble, _ + _).toString()"
| RedOpMin enhanced_numeric_int ⇒ ".aggregate(Int.MaxValue)(((x, y) => Math.min(x, y.toInt)), Math.min).toString()"
| RedOpMin enhanced_numeric_float ⇒ ".aggregate(Double.MaxValue)(((x, y) => Math.min(x, y.toDouble)), Math.min).toString()"
| RedOpMax enhanced_numeric_int ⇒
".aggregate(Int.MinValue)(((x, y) => Math.max(x, y.toInt)), Math.max).toString()"
| RedOpMax enhanced_numeric_float ⇒
".aggregate(Double.MinValue)(((x, y) => Math.max(x, y.toDouble)), Math.max).toString()"
| RedOpStats _ ⇒
".aggregate("""")(statsReduce, statsRereduce).toString()" ++ scala_endl ++
" sc.parallelize(Array(res))"
| RedOpArithMean _ ⇒
".arithmean /* ArithMean must be removed before code generation */"
end.
Definition min_max_to_stats avoid (mr: mr) :=
match mr.(mr_reduce) with
| RedOp (RedOpForeign op) ⇒
match op with
| RedOpMin typ | RedOpMax typ ⇒
let stats_field :=
match op with
| RedOpMin _ ⇒ "min"%string
| RedOpMax _ ⇒ "max"%string
| _ ⇒ "ERROR"%string
end
in
let (tmp, avoid) := fresh_mr_var "stats$" avoid in
let mr1 :=
mkMR
mr.(mr_input)
tmp
mr.(mr_map)
(RedOp (RedOpForeign (RedOpStats typ)))
in
let x := "stats"%string in
let mr2 :=
mkMR
tmp
mr.(mr_output)
(MapScalar (x, NNRCUnop AColl (NNRCUnop (ADot stats_field) (NNRCVar x))))
RedSingleton
in
Some (mr1::mr2::nil)
| _ ⇒ None
end
| _ ⇒ None
end.
Definition arithmean_to_stats avoid (mr: mr) :=
match mr.(mr_reduce) with
| RedOp (RedOpForeign op) ⇒
match op with
| RedOpArithMean typ ⇒
let (tmp, avoid) := fresh_mr_var "stats$" avoid in
let mr1 :=
mkMR
mr.(mr_input)
tmp
mr.(mr_map)
(RedOp (RedOpForeign (RedOpStats typ)))
in
let map :=
match typ with
| enhanced_numeric_int ⇒
let zero := NNRCConst (dnat 0) in
let x := "stats"%string in
MapScalar (x, NNRCUnop AColl
(NNRCIf (NNRCBinop AEq (NNRCUnop (ADot "count"%string) (NNRCVar x)) zero)
zero
(NNRCBinop (ABArith ArithDivide)
(NNRCUnop (ADot "sum"%string) (NNRCVar x))
(NNRCUnop (ADot "count"%string) (NNRCVar x)))))
| enhanced_numeric_float ⇒
let zero := NNRCConst (dnat 0) in
let zerof := NNRCConst (denhancedfloat FLOAT_CONST0) in
let x := "stats"%string in
MapScalar (x, NNRCUnop AColl
(NNRCIf (NNRCBinop AEq (NNRCUnop (ADot "count"%string) (NNRCVar x)) zero)
zerof
(NNRCBinop (AForeignBinaryOp (enhanced_binary_float_op bop_float_div))
(NNRCUnop (ADot "sum"%string) (NNRCVar x))
(NNRCUnop (AForeignUnaryOp (enhanced_unary_float_op uop_float_of_int))
(NNRCUnop (ADot "count"%string) (NNRCVar x))))))
end
in
let mr2 :=
mkMR
tmp
mr.(mr_output)
map
RedSingleton
in
Some (mr1::mr2::nil)
| _ ⇒ None
end
| _ ⇒ None
end.
Definition min_max_free_reduce (src:reduce_fun)
:= match src with
| RedOp (RedOpForeign (RedOpMin _|RedOpMax _)) ⇒ False
| _ ⇒ True
end.
Definition arithmean_free_reduce (src:reduce_fun)
:= match src with
| RedOp (RedOpForeign (RedOpArithMean _)) ⇒ False
| _ ⇒ True
end.
Definition min_max_free_mr (src:mr)
:= min_max_free_reduce src.(mr_reduce).
Definition arithmean_free_mr (src:mr)
:= arithmean_free_reduce src.(mr_reduce).
Definition min_max_free_mr_chain (src:list mr)
:= Forall min_max_free_mr src.
Definition min_max_free_nnrcmr (src:nnrcmr)
:= min_max_free_mr_chain src.(mr_chain).
Definition arithmean_free_mr_chain (src:list mr)
:= Forall arithmean_free_mr src.
Definition arithmean_free_nnrcmr (src:nnrcmr)
:= arithmean_free_mr_chain src.(mr_chain).
Definition to_spark_nnrcmr (l: nnrcmr) :=
let avoid := get_nnrcmr_vars l in
let l := apply_rewrite (arithmean_to_stats avoid) l in
l.
Definition to_spark_nnrcmr_prepared (src:nnrcmr)
:= arithmean_free_nnrcmr src.
Program Instance enhanced_foreign_to_spark : foreign_to_spark
:= mk_foreign_to_spark
enhanced_foreign_runtime
enhanced_foreign_reduce_op
enhanced_to_spark_reduce_op
to_spark_nnrcmr.
Instance enhanced_foreign_cloudant : foreign_cloudant
:= mk_foreign_cloudant
enhanced_foreign_runtime
(AForeignUnaryOp (enhanced_unary_float_op uop_float_sum))
(AForeignUnaryOp (enhanced_unary_float_op uop_float_listmin))
(AForeignUnaryOp (enhanced_unary_float_op uop_float_listmax)).
Definition enhanced_to_cloudant_reduce_op
(rop:enhanced_reduce_op) : CldMR.cld_reduce_op
:= match rop with
| RedOpCount ⇒ CldMR.CldRedOpCount
| RedOpSum typ ⇒ CldMR.CldRedOpSum (enhanced_to_cld_numeric_type typ)
| RedOpStats typ ⇒ CldMR.CldRedOpStats (enhanced_to_cld_numeric_type typ)
| RedOpMin _ ⇒ CldMR.CldRedOpStats CldMR.Cld_int
| RedOpMax _ ⇒ CldMR.CldRedOpStats CldMR.Cld_int
| RedOpArithMean _ ⇒ CldMR.CldRedOpStats CldMR.Cld_int
end.
Definition to_cloudant_nnrcmr (l: nnrcmr) :=
let avoid := get_nnrcmr_vars l in
let l := apply_rewrite (min_max_to_stats avoid) l in
let l := apply_rewrite (arithmean_to_stats avoid) l in
l.
Definition to_cloudant_nnrcmr_prepared (src:nnrcmr)
:= min_max_free_nnrcmr src ∧ arithmean_free_nnrcmr src.
Program Instance enhanced_foreign_to_cloudant : foreign_to_cloudant
:=
{ foreign_to_cloudant_reduce_op := enhanced_to_cloudant_reduce_op
; foreign_to_cloudant_prepare_nnrcmr := to_cloudant_nnrcmr
; foreign_to_cloudant_nnrcmr_prepared := to_cloudant_nnrcmr_prepared
}.
Axiom OPTIMIZER_LOGGER_nraenv_token_type : Set.
Extract Constant OPTIMIZER_LOGGER_nraenv_token_type ⇒ "Util.nra_logger_token_type".
Axiom OPTIMIZER_LOGGER_nraenv_startPass :
String.string → nraenv → OPTIMIZER_LOGGER_nraenv_token_type.
Extract Constant OPTIMIZER_LOGGER_nraenv_startPass ⇒
"(fun name input -> Logger.nra_log_startPass (Util.string_of_char_list name) input)".
Axiom OPTIMIZER_LOGGER_nraenv_step :
OPTIMIZER_LOGGER_nraenv_token_type → String.string →
nraenv → nraenv →
OPTIMIZER_LOGGER_nraenv_token_type.
Extract Inlined Constant OPTIMIZER_LOGGER_nraenv_step ⇒
"(fun token name input output -> Logger.nra_log_step token (Util.string_of_char_list name) input output)".
Axiom OPTIMIZER_LOGGER_nraenv_endPass :
OPTIMIZER_LOGGER_nraenv_token_type → nraenv → OPTIMIZER_LOGGER_nraenv_token_type.
Extract Inlined Constant OPTIMIZER_LOGGER_nraenv_endPass ⇒
"(fun token output -> Logger.nra_log_endPass token output)".
Instance foreign_nraenv_optimizer_logger :
optimizer_logger string nraenv
:=
{
optimizer_logger_token_type := OPTIMIZER_LOGGER_nraenv_token_type
; logStartPass := OPTIMIZER_LOGGER_nraenv_startPass
; logStep := OPTIMIZER_LOGGER_nraenv_step
; logEndPass := OPTIMIZER_LOGGER_nraenv_endPass
} .
Axiom OPTIMIZER_LOGGER_nnrc_token_type : Set.
Extract Constant OPTIMIZER_LOGGER_nnrc_token_type ⇒ "Util.nrc_logger_token_type".
Axiom OPTIMIZER_LOGGER_nnrc_startPass :
String.string → nnrc → OPTIMIZER_LOGGER_nnrc_token_type.
Extract Inlined Constant OPTIMIZER_LOGGER_nnrc_startPass ⇒
"(fun name input -> Logger.nrc_log_startPass (Util.string_of_char_list name) input)".
Axiom OPTIMIZER_LOGGER_nnrc_step :
OPTIMIZER_LOGGER_nnrc_token_type → String.string →
nnrc → nnrc →
OPTIMIZER_LOGGER_nnrc_token_type.
Extract Inlined Constant OPTIMIZER_LOGGER_nnrc_step ⇒
"(fun token name input output -> Logger.nrc_log_step token (Util.string_of_char_list name) input output)".
Axiom OPTIMIZER_LOGGER_nnrc_endPass :
OPTIMIZER_LOGGER_nnrc_token_type → nnrc → OPTIMIZER_LOGGER_nnrc_token_type.
Extract Inlined Constant OPTIMIZER_LOGGER_nnrc_endPass ⇒
"(fun token output -> Logger.nrc_log_endPass token output)".
Instance foreign_nnrc_optimizer_logger :
optimizer_logger string nnrc
:=
{
optimizer_logger_token_type := OPTIMIZER_LOGGER_nnrc_token_type
; logStartPass := OPTIMIZER_LOGGER_nnrc_startPass
; logStep := OPTIMIZER_LOGGER_nnrc_step
; logEndPass := OPTIMIZER_LOGGER_nnrc_endPass
} .
Foreign typing, used to build the basic_model
Definition enhanced_type_join (t1 t2:enhanced_type)
:= match t1, t2 with
| enhancedBottom, _ ⇒ t2
| _, enhancedBottom ⇒ t1
| enhancedFloat, enhancedFloat ⇒ enhancedFloat
| enhancedString, enhancedString ⇒ enhancedString
| enhancedTimeScale, enhancedTimeScale ⇒ enhancedTimeScale
| enhancedTimeDuration, enhancedTimeDuration ⇒ enhancedTimeDuration
| enhancedTimePoint, enhancedTimePoint ⇒ enhancedTimePoint
| enhancedSqlDate, enhancedSqlDate ⇒ enhancedSqlDate
| enhancedSqlDateInterval, enhancedSqlDateInterval ⇒ enhancedSqlDateInterval
| _, _ ⇒ enhancedTop
end.
Definition enhanced_type_meet (t1 t2:enhanced_type)
:= match t1, t2 with
| enhancedTop, _ ⇒ t2
| _, enhancedTop ⇒ t1
| enhancedFloat, enhancedFloat ⇒ enhancedFloat
| enhancedString, enhancedString ⇒ enhancedString
| enhancedTimeScale, enhancedTimeScale ⇒ enhancedTimeScale
| enhancedTimeDuration, enhancedTimeDuration ⇒ enhancedTimeDuration
| enhancedTimePoint, enhancedTimePoint ⇒ enhancedTimePoint
| enhancedSqlDate, enhancedSqlDate ⇒ enhancedSqlDate
| enhancedSqlDateInterval, enhancedSqlDateInterval ⇒ enhancedSqlDateInterval
| _, _ ⇒ enhancedBottom
end.
Inductive enhanced_subtype : enhanced_type → enhanced_type → Prop :=
| enhanced_subtype_top t : enhanced_subtype t enhancedTop
| enhanced_subtype_bottom t : enhanced_subtype enhancedBottom t
| enhanced_subtype_refl t : enhanced_subtype t t.
Instance enhanced_subtype_pre : PreOrder enhanced_subtype.
Instance enhanced_subtype_post : PartialOrder eq enhanced_subtype.
Instance enhanced_type_lattice : Lattice enhanced_type eq
:= {
join := enhanced_type_join
; meet := enhanced_type_meet
}.
Instance enhanced_type_olattice : OLattice eq enhanced_subtype.
Program Instance enhanced_foreign_type : foreign_type
:= mk_foreign_type enhanced_type _ _ _ _ _ _ _.
Program Instance enhanced_foreign_type_to_JSON : foreign_type_to_JSON
:= mk_foreign_type_to_JSON enhanced_foreign_type _ _.
Inductive enhanced_has_type : enhanced_data → enhanced_type → Prop :=
| enhanced_has_type_top fd : enhanced_has_type fd enhancedTop
| enhanced_has_type_float (f:FLOAT) : enhanced_has_type (enhancedfloat f) enhancedFloat
| enhanced_has_type_string (s:STRING) : enhanced_has_type (enhancedstring s) enhancedString
| enhanced_has_type_timescale (ts:time_scale) : enhanced_has_type (enhancedtimescale ts) enhancedTimeScale
| enhanced_has_type_timepoint (tp:TIME_POINT) : enhanced_has_type (enhancedtimepoint tp) enhancedTimePoint
| enhanced_has_type_timeduration (td:TIME_DURATION) : enhanced_has_type (enhancedtimeduration td) enhancedTimeDuration
| enhanced_has_type_sqldate (tp:SQL_DATE) : enhanced_has_type (enhancedsqldate tp) enhancedSqlDate
| enhanced_has_type_sqldateinterval (tp:SQL_DATE_INTERVAL) : enhanced_has_type (enhancedsqldateinterval tp) enhancedSqlDateInterval
.
Definition enhanced_infer_type (d:enhanced_data) : option enhanced_type
:= match d with
| enhancedfloat _ ⇒ Some enhancedFloat
| enhancedstring _ ⇒ Some enhancedString
| enhancedtimescale _ ⇒ Some enhancedTimeScale
| enhancedtimeduration _ ⇒ Some enhancedTimeDuration
| enhancedtimepoint _ ⇒ Some enhancedTimePoint
| enhancedsqldate _ ⇒ Some enhancedSqlDate
| enhancedsqldateinterval _ ⇒ Some enhancedSqlDateInterval
end.
Program Instance enhanced_foreign_data_typing :
@foreign_data_typing enhanced_foreign_data enhanced_foreign_type
:= mk_foreign_data_typing
enhanced_foreign_data
enhanced_foreign_type
enhanced_has_type _ _ _
enhanced_infer_type _ _ _
.
Definition dnnrc_for_log {br:brand_relation}
:= (@dnnrc enhanced_foreign_runtime (type_annotation unit) dataset).
Axiom OPTIMIZER_LOGGER_dnnrc_token_type : Set.
Extract Constant OPTIMIZER_LOGGER_dnnrc_token_type ⇒ "Util.dnrc_logger_token_type".
Axiom OPTIMIZER_LOGGER_dnnrc_startPass :
∀ {br:brand_relation}, String.string → dnnrc_for_log → OPTIMIZER_LOGGER_dnnrc_token_type.
Extract Inlined Constant OPTIMIZER_LOGGER_dnnrc_startPass ⇒
"(fun br name input -> Logger.dnrc_log_startPass (Util.string_of_char_list name) input)".
Axiom OPTIMIZER_LOGGER_dnnrc_step :
∀ {br:brand_relation},
OPTIMIZER_LOGGER_dnnrc_token_type → String.string →
dnnrc_for_log → dnnrc_for_log →
OPTIMIZER_LOGGER_dnnrc_token_type.
Extract Inlined Constant OPTIMIZER_LOGGER_dnnrc_step ⇒
"(fun br token name input output -> Logger.dnrc_log_step token (Util.string_of_char_list name) input output)".
Axiom OPTIMIZER_LOGGER_dnnrc_endPass :
∀ {br:brand_relation}, OPTIMIZER_LOGGER_dnnrc_token_type → dnnrc_for_log → OPTIMIZER_LOGGER_dnnrc_token_type.
Extract Inlined Constant OPTIMIZER_LOGGER_dnnrc_endPass ⇒
"(fun br token output -> Logger.dnrc_log_endPass token output)".
Instance foreign_dnnrc_optimizer_logger {br:brand_relation} :
optimizer_logger string dnnrc_for_log
:=
{
optimizer_logger_token_type := OPTIMIZER_LOGGER_dnnrc_token_type
; logStartPass := OPTIMIZER_LOGGER_dnnrc_startPass
; logStep := OPTIMIZER_LOGGER_dnnrc_step
; logEndPass := OPTIMIZER_LOGGER_dnnrc_endPass
} .
Module EnhancedRuntime <: CompilerRuntime.
Definition compiler_foreign_type : foreign_type
:= enhanced_foreign_type.
Definition compiler_foreign_runtime : foreign_runtime
:= enhanced_foreign_runtime.
Definition compiler_foreign_to_java : foreign_to_java
:= enhanced_foreign_to_java.
Definition compiler_foreign_to_javascript : foreign_to_javascript
:= enhanced_foreign_to_javascript.
Definition compiler_foreign_to_scala : foreign_to_scala
:= enhanced_foreign_to_scala.
Definition compiler_foreign_to_JSON : foreign_to_JSON
:= enhanced_foreign_to_JSON.
Definition compiler_foreign_type_to_JSON : foreign_type_to_JSON
:= enhanced_foreign_type_to_JSON.
Definition compiler_foreign_reduce_op : foreign_reduce_op
:= enhanced_foreign_reduce_op.
Definition compiler_foreign_to_reduce_op : foreign_to_reduce_op
:= enhanced_foreign_to_reduce_op.
Definition compiler_foreign_to_spark : foreign_to_spark
:= enhanced_foreign_to_spark.
Definition compiler_foreign_cloudant : foreign_cloudant
:= enhanced_foreign_cloudant.
Definition compiler_foreign_to_cloudant : foreign_to_cloudant
:= enhanced_foreign_to_cloudant.
Definition compiler_nraenv_optimizer_logger : optimizer_logger string nraenv
:= foreign_nraenv_optimizer_logger.
Definition compiler_nnrc_optimizer_logger : optimizer_logger string nnrc
:= foreign_nnrc_optimizer_logger.
Definition compiler_dnnrc_optimizer_logger {br:brand_relation}: optimizer_logger string (dnnrc (type_annotation unit) dataset)
:= foreign_dnnrc_optimizer_logger.
Definition compiler_foreign_data_typing : foreign_data_typing
:= enhanced_foreign_data_typing.
End EnhancedRuntime.
Definition Float {br:brand_relation} : rtype := Foreign enhancedFloat.
Definition TimeScale {br:brand_relation} : rtype := Foreign enhancedTimeScale.
Definition TimeDuration {br:brand_relation} : rtype := Foreign enhancedTimeDuration.
Definition TimePoint {br:brand_relation} : rtype := Foreign enhancedTimePoint.
Definition SqlDate {br:brand_relation} : rtype := Foreign enhancedSqlDate.
Definition SqlDateInterval {br:brand_relation} : rtype := Foreign enhancedSqlDateInterval.
Definition isFloat {model : brand_model} (τ:rtype) :=
match proj1_sig τ with
| Foreign₀ enhancedFloat ⇒ true
| _ ⇒ false
end.
Definition isTimePoint {model : brand_model} (τ:rtype) :=
match proj1_sig τ with
| Foreign₀ enhancedTimePoint ⇒ true
| _ ⇒ false
end.
Definition isTimeScale {model : brand_model} (τ:rtype) :=
match proj1_sig τ with
| Foreign₀ enhancedTimeScale ⇒ true
| _ ⇒ false
end.
Definition isTimeDuration {model : brand_model} (τ:rtype) :=
match proj1_sig τ with
| Foreign₀ enhancedTimeDuration ⇒ true
| _ ⇒ false
end.
Definition isSqlDate {model : brand_model} (τ:rtype) :=
match proj1_sig τ with
| Foreign₀ enhancedSqlDate ⇒ true
| _ ⇒ false
end.
Definition isSqlDateInterval {model : brand_model} (τ:rtype) :=
match proj1_sig τ with
| Foreign₀ enhancedSqlDateInterval ⇒ true
| _ ⇒ false
end.
Definition isNat {model : brand_model} (τ:rtype) :=
match proj1_sig τ with
| Nat₀ ⇒ true
| _ ⇒ false
end.
Definition isString {model : brand_model} (τ:rtype) :=
match proj1_sig τ with
| String₀ ⇒ true
| _ ⇒ false
end.
Inductive float_unary_op_has_type {model:brand_model} :
float_unary_op → rtype → rtype → Prop
:=
| tuop_float_neg : float_unary_op_has_type uop_float_neg Float Float
| tuop_float_sqrt : float_unary_op_has_type uop_float_sqrt Float Float
| tuop_float_exp : float_unary_op_has_type uop_float_exp Float Float
| tuop_float_log : float_unary_op_has_type uop_float_log Float Float
| tuop_float_log10 : float_unary_op_has_type uop_float_log10 Float Float
| tuop_float_of_int : float_unary_op_has_type uop_float_of_int Nat Float
| tuop_float_ceil : float_unary_op_has_type uop_float_ceil Float Float
| tuop_float_floor : float_unary_op_has_type uop_float_floor Float Float
| tuop_float_truncate : float_unary_op_has_type uop_float_truncate Float Nat
| tuop_float_abs : float_unary_op_has_type uop_float_abs Float Float
| tuop_float_sum : float_unary_op_has_type uop_float_sum (Coll Float) Float
| tuop_float_arithmean : float_unary_op_has_type uop_float_arithmean (Coll Float) Float
| tuop_float_listmin : float_unary_op_has_type uop_float_listmin (Coll Float) Float
| tuop_float_listmax : float_unary_op_has_type uop_float_listmax (Coll Float) Float
.
Definition tuncoll {model:brand_model} (τ:rtype) : option rtype.
Definition float_unary_op_type_infer {model : brand_model} (op:float_unary_op) (τ₁:rtype) : option rtype :=
match op with
| uop_float_neg
| uop_float_sqrt
| uop_float_exp
| uop_float_log
| uop_float_log10
| uop_float_ceil
| uop_float_floor
| uop_float_abs ⇒
if isFloat τ₁
then Some Float
else None
| uop_float_of_int ⇒
if isNat τ₁
then Some Float
else None
| uop_float_truncate ⇒
if isFloat τ₁
then Some Nat
else None
| uop_float_sum
| uop_float_arithmean
| uop_float_listmin
| uop_float_listmax ⇒
match tuncoll τ₁ return (option rtype) with
| Some τ ⇒
if isFloat τ
then Some Float
else None
| None ⇒ None
end
end.
Definition float_unary_op_type_infer_sub {model : brand_model} (op:float_unary_op) (τ₁:rtype) : option (rtype×rtype) :=
match op with
| uop_float_neg
| uop_float_sqrt
| uop_float_exp
| uop_float_log
| uop_float_log10
| uop_float_ceil
| uop_float_floor
| uop_float_abs ⇒
enforce_unary_op_schema (τ₁,Float) Float
| uop_float_of_int ⇒
enforce_unary_op_schema (τ₁,Nat) Float
| uop_float_truncate ⇒
enforce_unary_op_schema (τ₁,Float) Nat
| uop_float_sum
| uop_float_arithmean
| uop_float_listmin
| uop_float_listmax ⇒
enforce_unary_op_schema (τ₁,Coll Float) Float
end.
Lemma rondcollfloat_typed_some
{model:brand_model}
(f: list FLOAT → FLOAT)
(d:data) :
d ▹ Coll Float →
∃ z,
rondcollfloat f d = Some z
∧ z ▹ Float.
Lemma float_unary_op_typing_sound {model : brand_model}
(fu : float_unary_op) (τin τout : rtype) :
float_unary_op_has_type fu τin τout →
∀ din : data,
din ▹ τin →
∃ dout : data,
float_unary_op_interp fu din = Some dout ∧ dout ▹ τout.
Inductive time_unary_op_has_type {model:brand_model} :
time_unary_op → rtype → rtype → Prop
:=
| tuop_time_to_scale : time_unary_op_has_type uop_time_to_scale TimePoint TimeScale
| tuop_time_from_string : time_unary_op_has_type uop_time_from_string RType.String TimePoint
| tuop_time_duration_from_string : time_unary_op_has_type uop_time_duration_from_string RType.String TimeDuration
.
Definition time_unary_op_type_infer {model : brand_model} (op:time_unary_op) (τ₁:rtype) : option rtype :=
match op with
| uop_time_to_scale ⇒
if isTimePoint τ₁ then Some TimeScale else None
| uop_time_from_string ⇒
if isString τ₁ then Some TimePoint else None
| uop_time_duration_from_string ⇒
if isString τ₁ then Some TimeDuration else None
end.
Definition time_unary_op_type_infer_sub {model : brand_model} (op:time_unary_op) (τ₁:rtype) : option (rtype×rtype) :=
match op with
| uop_time_to_scale ⇒
enforce_unary_op_schema (τ₁,TimePoint) TimeScale
| uop_time_from_string ⇒
enforce_unary_op_schema (τ₁,RType.String) TimePoint
| uop_time_duration_from_string ⇒
enforce_unary_op_schema (τ₁,RType.String) TimeDuration
end.
Lemma time_unary_op_typing_sound {model : brand_model}
(fu : time_unary_op) (τin τout : rtype) :
time_unary_op_has_type fu τin τout →
∀ din : data,
din ▹ τin →
∃ dout : data,
time_unary_op_interp fu din = Some dout ∧ dout ▹ τout.
Inductive sql_date_unary_op_has_type {model:brand_model} :
sql_date_unary_op → rtype → rtype → Prop
:=
| tuop_sql_get_date_component part : sql_date_unary_op_has_type (uop_sql_get_date_component part) SqlDate Nat
| tuop_sql_date_from_string : sql_date_unary_op_has_type uop_sql_date_from_string RType.String SqlDate
| tuop_sql_date_interval_from_string : sql_date_unary_op_has_type uop_sql_date_interval_from_string RType.String SqlDateInterval
.
Definition sql_date_unary_op_type_infer {model : brand_model} (op:sql_date_unary_op) (τ₁:rtype) : option rtype :=
match op with
| uop_sql_get_date_component part ⇒
if isSqlDate τ₁ then Some Nat else None
| uop_sql_date_from_string ⇒
if isString τ₁ then Some SqlDate else None
| uop_sql_date_interval_from_string ⇒
if isString τ₁ then Some SqlDateInterval else None
end.
Definition sql_date_unary_op_type_infer_sub {model : brand_model} (op:sql_date_unary_op) (τ₁:rtype) : option (rtype×rtype) :=
match op with
| uop_sql_get_date_component part ⇒
enforce_unary_op_schema (τ₁,SqlDate) Nat
| uop_sql_date_from_string ⇒
enforce_unary_op_schema (τ₁,RType.String) SqlDate
| uop_sql_date_interval_from_string ⇒
enforce_unary_op_schema (τ₁,RType.String) SqlDateInterval
end.
Lemma sql_date_unary_op_typing_sound {model : brand_model}
(fu : sql_date_unary_op) (τin τout : rtype) :
sql_date_unary_op_has_type fu τin τout →
∀ din : data,
din ▹ τin →
∃ dout : data,
sql_date_unary_op_interp fu din = Some dout ∧ dout ▹ τout.
Inductive enhanced_unary_op_has_type {model:brand_model} : enhanced_unary_op → rtype → rtype → Prop
:=
| tenhanced_unary_float_op fu τin τout:
float_unary_op_has_type fu τin τout →
enhanced_unary_op_has_type (enhanced_unary_float_op fu) τin τout
| tenhanced_unary_time_op fu τin τout:
time_unary_op_has_type fu τin τout →
enhanced_unary_op_has_type (enhanced_unary_time_op fu) τin τout
| tenhanced_unary_sql_date_op fu τin τout:
sql_date_unary_op_has_type fu τin τout →
enhanced_unary_op_has_type (enhanced_unary_sql_date_op fu) τin τout.
Definition enhanced_unary_op_typing_infer {model:brand_model} (fu:enhanced_unary_op) (τ:rtype) : option rtype :=
match fu with
| enhanced_unary_float_op op ⇒ float_unary_op_type_infer op τ
| enhanced_unary_time_op op ⇒ time_unary_op_type_infer op τ
| enhanced_unary_sql_date_op op ⇒ sql_date_unary_op_type_infer op τ
end.
Lemma enhanced_unary_op_typing_infer_correct
{model:brand_model}
(fu:foreign_unary_op_type)
{τ₁ τout} :
enhanced_unary_op_typing_infer fu τ₁ = Some τout →
enhanced_unary_op_has_type fu τ₁ τout.
Lemma enhanced_unary_op_typing_infer_least
{model:brand_model}
(fu:foreign_unary_op_type)
{τ₁ τout₁ τout₂} :
enhanced_unary_op_typing_infer fu τ₁ = Some τout₁ →
enhanced_unary_op_has_type fu τ₁ τout₂ →
τout₁ ≤ τout₂.
Lemma enhanced_unary_op_typing_infer_complete
{model:brand_model}
(fu:foreign_unary_op_type)
{τ₁ τout} :
enhanced_unary_op_typing_infer fu τ₁ = None →
¬ enhanced_unary_op_has_type fu τ₁ τout.
Definition enhanced_unary_op_typing_infer_sub {model:brand_model} (fu:enhanced_unary_op) (τ:rtype) : option (rtype×rtype) :=
match fu with
| enhanced_unary_float_op op ⇒ float_unary_op_type_infer_sub op τ
| enhanced_unary_time_op op ⇒ time_unary_op_type_infer_sub op τ
| enhanced_unary_sql_date_op op ⇒ sql_date_unary_op_type_infer_sub op τ
end.
Lemma enhanced_unary_op_typing_sound {model : brand_model}
(fu : foreign_unary_op_type) (τin τout : rtype) :
enhanced_unary_op_has_type fu τin τout →
∀ din : data,
din ▹ τin →
∃ dout : data,
enhanced_unary_op_interp brand_relation_brands fu din = Some dout ∧ dout ▹ τout.
Instance enhanced_foreign_unary_op_typing
{model:brand_model} :
@foreign_unary_op_typing
enhanced_foreign_data
enhanced_foreign_unary_op
enhanced_foreign_type
enhanced_foreign_data_typing
model
:= { foreign_unary_op_typing_has_type := enhanced_unary_op_has_type
; foreign_unary_op_typing_sound := enhanced_unary_op_typing_sound
; foreign_unary_op_typing_infer := enhanced_unary_op_typing_infer
; foreign_unary_op_typing_infer_correct := enhanced_unary_op_typing_infer_correct
; foreign_unary_op_typing_infer_least := enhanced_unary_op_typing_infer_least
; foreign_unary_op_typing_infer_complete := enhanced_unary_op_typing_infer_complete
; foreign_unary_op_typing_infer_sub := enhanced_unary_op_typing_infer_sub
}.
Inductive float_binary_op_has_type {model:brand_model} :
float_binary_op → rtype → rtype → rtype → Prop
:=
| tbop_float_plus :
float_binary_op_has_type bop_float_plus Float Float Float
| tbop_float_minus :
float_binary_op_has_type bop_float_minus Float Float Float
| tbop_float_mult :
float_binary_op_has_type bop_float_mult Float Float Float
| tbop_float_div :
float_binary_op_has_type bop_float_div Float Float Float
| tbop_float_pow :
float_binary_op_has_type bop_float_pow Float Float Float
| tbop_float_min :
float_binary_op_has_type bop_float_min Float Float Float
| tbop_float_max :
float_binary_op_has_type bop_float_max Float Float Float
| tbop_float_ne :
float_binary_op_has_type bop_float_ne Float Float Bool
| tbop_float_lt :
float_binary_op_has_type bop_float_lt Float Float Bool
| tbop_float_le :
float_binary_op_has_type bop_float_le Float Float Bool
| tbop_float_gt :
float_binary_op_has_type bop_float_gt Float Float Bool
| tbop_float_ge :
float_binary_op_has_type bop_float_ge Float Float Bool
.
Definition float_binary_op_type_infer {model : brand_model} (op:float_binary_op) (τ₁ τ₂:rtype) :=
match op with
| bop_float_plus
| bop_float_minus
| bop_float_mult
| bop_float_div
| bop_float_pow
| bop_float_min
| bop_float_max ⇒
if isFloat τ₁ && isFloat τ₂
then Some Float
else None
| bop_float_ne
| bop_float_lt
| bop_float_le
| bop_float_gt
| bop_float_ge ⇒
if isFloat τ₁ && isFloat τ₂
then Some Bool
else None
end.
Lemma float_binary_op_typing_sound {model : brand_model}
(fb : float_binary_op) (τin₁ τin₂ τout : rtype) :
float_binary_op_has_type fb τin₁ τin₂ τout →
∀ din₁ din₂ : data,
din₁ ▹ τin₁ →
din₂ ▹ τin₂ →
∃ dout : data,
float_binary_op_interp fb din₁ din₂ = Some dout ∧ dout ▹ τout.
Definition float_binary_op_type_infer_sub {model : brand_model} (op:float_binary_op) (τ₁ τ₂:rtype) : option (rtype×rtype×rtype):=
match op with
| bop_float_plus
| bop_float_minus
| bop_float_mult
| bop_float_div
| bop_float_pow
| bop_float_min
| bop_float_max ⇒
enforce_binary_op_schema (τ₁, Float) (τ₂, Float) Float
| bop_float_ne
| bop_float_lt
| bop_float_le
| bop_float_gt
| bop_float_ge ⇒
enforce_binary_op_schema (τ₁, Float) (τ₂, Float) Bool
end.
Inductive time_binary_op_has_type {model:brand_model} :
time_binary_op → rtype → rtype → rtype → Prop
:=
| tbop_time_as :
time_binary_op_has_type bop_time_as TimePoint TimeScale TimePoint
| tbop_time_shift :
time_binary_op_has_type bop_time_shift TimePoint TimeDuration TimePoint
| tbop_time_ne :
time_binary_op_has_type bop_time_ne TimePoint TimePoint Bool
| tbop_time_lt :
time_binary_op_has_type bop_time_lt TimePoint TimePoint Bool
| tbop_time_le :
time_binary_op_has_type bop_time_le TimePoint TimePoint Bool
| tbop_time_gt :
time_binary_op_has_type bop_time_gt TimePoint TimePoint Bool
| tbop_time_ge :
time_binary_op_has_type bop_time_ge TimePoint TimePoint Bool
| tbop_time_duration_from_scale :
time_binary_op_has_type bop_time_duration_from_scale TimeScale Nat TimeDuration
| tbop_time_duration_between :
time_binary_op_has_type bop_time_duration_between TimePoint TimePoint TimeDuration
.
Definition time_binary_op_type_infer {model : brand_model} (op:time_binary_op) (τ₁ τ₂:rtype) :=
match op with
| bop_time_as ⇒
if isTimePoint τ₁ && isTimeScale τ₂ then Some TimePoint else None
| bop_time_shift ⇒
if isTimePoint τ₁ && isTimeDuration τ₂ then Some TimePoint else None
| bop_time_ne ⇒
if isTimePoint τ₁ && isTimePoint τ₂ then Some Bool else None
| bop_time_lt ⇒
if isTimePoint τ₁ && isTimePoint τ₂ then Some Bool else None
| bop_time_le ⇒
if isTimePoint τ₁ && isTimePoint τ₂ then Some Bool else None
| bop_time_gt ⇒
if isTimePoint τ₁ && isTimePoint τ₂ then Some Bool else None
| bop_time_ge ⇒
if isTimePoint τ₁ && isTimePoint τ₂ then Some Bool else None
| bop_time_duration_from_scale ⇒
if isTimeScale τ₁ && isNat τ₂ then Some TimeDuration else None
| bop_time_duration_between ⇒
if isTimePoint τ₁ && isTimePoint τ₂ then Some TimeDuration else None
end.
Lemma time_binary_op_typing_sound {model : brand_model}
(fb : time_binary_op) (τin₁ τin₂ τout : rtype) :
time_binary_op_has_type fb τin₁ τin₂ τout →
∀ din₁ din₂ : data,
din₁ ▹ τin₁ →
din₂ ▹ τin₂ →
∃ dout : data,
time_binary_op_interp fb din₁ din₂ = Some dout ∧ dout ▹ τout.
Definition time_binary_op_type_infer_sub {model : brand_model} (op:time_binary_op) (τ₁ τ₂:rtype) : option (rtype×rtype×rtype) :=
match op with
| bop_time_as ⇒
enforce_binary_op_schema (τ₁,TimePoint) (τ₂,TimeScale) TimePoint
| bop_time_shift ⇒
enforce_binary_op_schema (τ₁,TimePoint) (τ₂,TimeDuration) TimePoint
| bop_time_ne
| bop_time_lt
| bop_time_le
| bop_time_gt
| bop_time_ge ⇒
enforce_binary_op_schema (τ₁,TimePoint) (τ₂,TimePoint) Bool
| bop_time_duration_from_scale ⇒
enforce_binary_op_schema (τ₁,TimeScale) (τ₂,Nat) TimeDuration
| bop_time_duration_between ⇒
enforce_binary_op_schema (τ₁,TimePoint) (τ₂,TimePoint) TimeDuration
end.
Inductive sql_date_binary_op_has_type {model:brand_model} :
sql_date_binary_op → rtype → rtype → rtype → Prop
:=
| tbop_sql_date_plus :
sql_date_binary_op_has_type bop_sql_date_plus SqlDate SqlDateInterval SqlDate
| tbop_sql_date_minus :
sql_date_binary_op_has_type bop_sql_date_minus SqlDate SqlDateInterval SqlDate
| tbop_sql_date_ne :
sql_date_binary_op_has_type bop_sql_date_ne SqlDate SqlDate Bool
| tbop_sql_date_lt :
sql_date_binary_op_has_type bop_sql_date_lt SqlDate SqlDate Bool
| tbop_sql_date_le :
sql_date_binary_op_has_type bop_sql_date_le SqlDate SqlDate Bool
| tbop_sql_date_gt :
sql_date_binary_op_has_type bop_sql_date_gt SqlDate SqlDate Bool
| tbop_sql_date_ge :
sql_date_binary_op_has_type bop_sql_date_ge SqlDate SqlDate Bool
| tbop_sql_date_interval_between :
sql_date_binary_op_has_type bop_sql_date_interval_between SqlDate SqlDate SqlDateInterval
.
Definition sql_date_binary_op_type_infer {model : brand_model} (op:sql_date_binary_op) (τ₁ τ₂:rtype) :=
match op with
| bop_sql_date_plus ⇒
if isSqlDate τ₁ && isSqlDateInterval τ₂ then Some SqlDate else None
| bop_sql_date_minus ⇒
if isSqlDate τ₁ && isSqlDateInterval τ₂ then Some SqlDate else None
| bop_sql_date_ne ⇒
if isSqlDate τ₁ && isSqlDate τ₂ then Some Bool else None
| bop_sql_date_lt ⇒
if isSqlDate τ₁ && isSqlDate τ₂ then Some Bool else None
| bop_sql_date_le ⇒
if isSqlDate τ₁ && isSqlDate τ₂ then Some Bool else None
| bop_sql_date_gt ⇒
if isSqlDate τ₁ && isSqlDate τ₂ then Some Bool else None
| bop_sql_date_ge ⇒
if isSqlDate τ₁ && isSqlDate τ₂ then Some Bool else None
| bop_sql_date_interval_between ⇒
if isSqlDate τ₁ && isSqlDate τ₂ then Some SqlDateInterval else None
end.
Lemma sql_date_binary_op_typing_sound {model : brand_model}
(fb : sql_date_binary_op) (τin₁ τin₂ τout : rtype) :
sql_date_binary_op_has_type fb τin₁ τin₂ τout →
∀ din₁ din₂ : data,
din₁ ▹ τin₁ →
din₂ ▹ τin₂ →
∃ dout : data,
sql_date_binary_op_interp fb din₁ din₂ = Some dout ∧ dout ▹ τout.
Definition sql_date_binary_op_type_infer_sub {model : brand_model} (op:sql_date_binary_op) (τ₁ τ₂:rtype) : option (rtype×rtype×rtype) :=
match op with
| bop_sql_date_plus ⇒
enforce_binary_op_schema (τ₁,SqlDate) (τ₂,SqlDateInterval) SqlDate
| bop_sql_date_minus ⇒
enforce_binary_op_schema (τ₁,SqlDate) (τ₂,SqlDateInterval) SqlDate
| bop_sql_date_ne
| bop_sql_date_lt
| bop_sql_date_le
| bop_sql_date_gt
| bop_sql_date_ge ⇒
enforce_binary_op_schema (τ₁,SqlDate) (τ₂,SqlDate) Bool
| bop_sql_date_interval_between ⇒
enforce_binary_op_schema (τ₁,SqlDate) (τ₂,SqlDate) SqlDateInterval
end.
Inductive enhanced_binary_op_has_type {model:brand_model} :
enhanced_binary_op → rtype → rtype → rtype → Prop
:=
| tenhanced_binary_float_op fb τin₁ τin₂ τout:
float_binary_op_has_type fb τin₁ τin₂ τout →
enhanced_binary_op_has_type (enhanced_binary_float_op fb) τin₁ τin₂ τout
| tenhanced_binary_time_op fb τin₁ τin₂ τout:
time_binary_op_has_type fb τin₁ τin₂ τout →
enhanced_binary_op_has_type (enhanced_binary_time_op fb) τin₁ τin₂ τout
| tenhanced_binary_sql_date_op fb τin₁ τin₂ τout:
sql_date_binary_op_has_type fb τin₁ τin₂ τout →
enhanced_binary_op_has_type (enhanced_binary_sql_date_op fb) τin₁ τin₂ τout.
Definition enhanced_binary_op_typing_infer {model:brand_model} (op:enhanced_binary_op) (τ₁ τ₂:rtype) :=
match op with
| enhanced_binary_float_op fb ⇒ float_binary_op_type_infer fb τ₁ τ₂
| enhanced_binary_time_op fb ⇒ time_binary_op_type_infer fb τ₁ τ₂
| enhanced_binary_sql_date_op fb ⇒ sql_date_binary_op_type_infer fb τ₁ τ₂
end.
Lemma enhanced_binary_op_typing_infer_correct
{model:brand_model}
(fb:foreign_binary_op_type)
{τ₁ τ₂ τout} :
enhanced_binary_op_typing_infer fb τ₁ τ₂ = Some τout →
enhanced_binary_op_has_type fb τ₁ τ₂ τout.
Lemma enhanced_binary_op_typing_infer_least
{model:brand_model}
(fb:foreign_binary_op_type)
{τ₁ τ₂ τout₁ τout₂} :
enhanced_binary_op_typing_infer fb τ₁ τ₂ = Some τout₁ →
enhanced_binary_op_has_type fb τ₁ τ₂ τout₂ →
τout₁ ≤ τout₂.
Lemma enhanced_binary_op_typing_infer_complete
{model:brand_model}
(fb:foreign_binary_op_type)
{τ₁ τ₂ τout} :
enhanced_binary_op_typing_infer fb τ₁ τ₂ = None →
¬ enhanced_binary_op_has_type fb τ₁ τ₂ τout.
Definition enhanced_binary_op_typing_infer_sub {model:brand_model} (op:enhanced_binary_op) (τ₁ τ₂:rtype) :=
match op with
| enhanced_binary_float_op fb ⇒ float_binary_op_type_infer_sub fb τ₁ τ₂
| enhanced_binary_time_op fb ⇒ time_binary_op_type_infer_sub fb τ₁ τ₂
| enhanced_binary_sql_date_op fb ⇒ sql_date_binary_op_type_infer_sub fb τ₁ τ₂
end.
Lemma enhanced_binary_op_typing_sound {model : brand_model}
(fu : foreign_binary_op_type) (τin₁ τin₂ τout : rtype) :
enhanced_binary_op_has_type fu τin₁ τin₂ τout →
∀ din₁ din₂ : data,
din₁ ▹ τin₁ →
din₂ ▹ τin₂ →
∃ dout : data,
enhanced_binary_op_interp brand_relation_brands fu din₁ din₂ = Some dout ∧ dout ▹ τout.
Program Instance enhanced_foreign_binary_op_typing
{model:brand_model} :
@foreign_binary_op_typing
enhanced_foreign_data
enhanced_foreign_binary_op
enhanced_foreign_type
enhanced_foreign_data_typing
model
:= { foreign_binary_op_typing_has_type := enhanced_binary_op_has_type
; foreign_binary_op_typing_sound := enhanced_binary_op_typing_sound
; foreign_binary_op_typing_infer := enhanced_binary_op_typing_infer
; foreign_binary_op_typing_infer_correct := enhanced_binary_op_typing_infer_correct
; foreign_binary_op_typing_infer_least := enhanced_binary_op_typing_infer_least
; foreign_binary_op_typing_infer_complete := enhanced_binary_op_typing_infer_complete
; foreign_binary_op_typing_infer_sub := enhanced_binary_op_typing_infer_sub
}.
Instance enhanced_foreign_typing {model:brand_model}:
@foreign_typing
enhanced_foreign_runtime
enhanced_foreign_type
model
:= mk_foreign_typing
enhanced_foreign_runtime
enhanced_foreign_type
model
enhanced_foreign_data_typing
enhanced_foreign_unary_op_typing
enhanced_foreign_binary_op_typing.
Instance enhanced_basic_model {model:brand_model} :
basic_model
:= mk_basic_model
enhanced_foreign_runtime
enhanced_foreign_type
model
enhanced_foreign_typing.
Module EnhancedForeignType <: CompilerForeignType.
Definition compiler_foreign_type : foreign_type
:= enhanced_foreign_type.
End EnhancedForeignType.
Module EnhancedModel(bm:CompilerBrandModel(EnhancedForeignType)) <: CompilerModel.
Definition compiler_foreign_type : foreign_type
:= enhanced_foreign_type.
Definition compiler_basic_model : @basic_model
:= @enhanced_basic_model bm.compiler_brand_model.
Definition compiler_model_foreign_to_java : foreign_to_java
:= enhanced_foreign_to_java.
Definition compiler_model_foreign_to_javascript : foreign_to_javascript
:= enhanced_foreign_to_javascript.
Definition compiler_model_foreign_to_scala : foreign_to_scala
:= enhanced_foreign_to_scala.
Definition compiler_model_foreign_to_JSON : foreign_to_JSON
:= enhanced_foreign_to_JSON.
Definition compiler_model_foreign_type_to_JSON : foreign_type_to_JSON
:= enhanced_foreign_type_to_JSON.
Definition compiler_model_foreign_reduce_op : foreign_reduce_op
:= enhanced_foreign_reduce_op.
Definition compiler_model_foreign_to_reduce_op : foreign_to_reduce_op
:= enhanced_foreign_to_reduce_op.
Definition compiler_model_foreign_to_spark : foreign_to_spark
:= enhanced_foreign_to_spark.
Definition compiler_model_foreign_cloudant : foreign_cloudant
:= enhanced_foreign_cloudant.
Definition compiler_model_foreign_to_cloudant : foreign_to_cloudant
:= enhanced_foreign_to_cloudant.
Definition compiler_model_nraenv_optimizer_logger : optimizer_logger string nraenv
:= foreign_nraenv_optimizer_logger.
Definition compiler_model_nnrc_optimizer_logger : optimizer_logger string nnrc
:= foreign_nnrc_optimizer_logger.
Definition compiler_model_dnnrc_optimizer_logger {br:brand_relation}: optimizer_logger string (dnnrc (type_annotation unit) dataset)
:= foreign_dnnrc_optimizer_logger.
Definition compiler_model_foreign_data_typing : foreign_data_typing
:= enhanced_foreign_data_typing.
End EnhancedModel.
Module CompEnhanced.
Module Enhanced.
Module Model.
Definition basic_model (bm:brand_model) : basic_model
:= @enhanced_basic_model bm.
Definition foreign_type : foreign_type
:= enhanced_foreign_type.
Definition foreign_typing (bm:brand_model) : foreign_typing
:= @enhanced_foreign_typing bm.
End Model.
Module Data.
Definition dfloat (f : FLOAT) : data
:= dforeign (enhancedfloat f).
Definition dstringblob (s : STRING) : data
:= dforeign (enhancedstring s).
Definition jfloat (f : FLOAT) : json
:= jforeign (enhancedfloat f).
Definition jstringblob (s : STRING) : json
:= jforeign (enhancedstring s).
Definition scale_kind := time_scale.
Definition SECOND : scale_kind
:= ts_second.
Definition MINUTE : scale_kind
:= ts_minute.
Definition HOUR : scale_kind
:= ts_hour.
Definition DAY : scale_kind
:= ts_day.
Definition WEEK : scale_kind
:= ts_week.
Definition MONTH : scale_kind
:= ts_month.
Definition YEAR : scale_kind
:= ts_year.
Definition second : scale_kind
:= ts_second.
Definition minute : scale_kind
:= ts_minute.
Definition hour : scale_kind
:= ts_hour.
Definition day : scale_kind
:= ts_day.
Definition week : scale_kind
:= ts_week.
Definition month : scale_kind
:= ts_month.
Definition year : scale_kind
:= ts_year.
Definition dtime_scale (kind:scale_kind)
:= dforeign (enhancedtimescale kind).
Definition dtime_duration (td:TIME_DURATION)
:= dforeign (enhancedtimeduration td).
Definition dtimepoint (tp:TIME_POINT) : data
:= dforeign (enhancedtimepoint tp).
Definition sql_date_part := sql_date_component.
Definition sql_date_day : sql_date_part := sql_date_DAY.
Definition sql_date_month : sql_date_part := sql_date_MONTH.
Definition sql_date_year : sql_date_part := sql_date_YEAR.
Definition dsql_date (d:SQL_DATE) : data
:= dforeign (enhancedsqldate d).
Definition dsql_date_interval (d:SQL_DATE_INTERVAL) : data
:= dforeign (enhancedsqldateinterval d).
End Data.
Module Ops.
Module Unary.
Definition float_neg
:= AForeignUnaryOp (enhanced_unary_float_op uop_float_neg).
Definition float_sqrt
:= AForeignUnaryOp (enhanced_unary_float_op uop_float_sqrt).
Definition float_exp
:= AForeignUnaryOp (enhanced_unary_float_op uop_float_exp).
Definition float_log
:= AForeignUnaryOp (enhanced_unary_float_op uop_float_log).
Definition float_log10
:= AForeignUnaryOp (enhanced_unary_float_op uop_float_log10).
Definition float_of_int
:= AForeignUnaryOp (enhanced_unary_float_op uop_float_of_int).
Definition float_ceil
:= AForeignUnaryOp (enhanced_unary_float_op uop_float_ceil).
Definition float_floor
:= AForeignUnaryOp (enhanced_unary_float_op uop_float_floor).
Definition float_truncate
:= AForeignUnaryOp (enhanced_unary_float_op uop_float_truncate).
Definition float_abs
:= AForeignUnaryOp (enhanced_unary_float_op uop_float_abs).
Definition float_sum
:= AForeignUnaryOp (enhanced_unary_float_op uop_float_sum).
Definition float_arithmean
:= AForeignUnaryOp (enhanced_unary_float_op uop_float_arithmean).
Definition float_listmin
:= AForeignUnaryOp (enhanced_unary_float_op uop_float_listmin).
Definition float_listmax
:= AForeignUnaryOp (enhanced_unary_float_op uop_float_listmax).
Definition time_to_scale
:= AForeignUnaryOp (enhanced_unary_time_op uop_time_to_scale).
Definition time_from_string
:= AForeignUnaryOp (enhanced_unary_time_op uop_time_from_string).
Definition time_duration_from_string
:= AForeignUnaryOp (enhanced_unary_time_op uop_time_duration_from_string).
Definition sql_get_date_component (component:sql_date_component)
:= AForeignUnaryOp (enhanced_unary_sql_date_op (uop_sql_get_date_component component)).
Definition sql_date_from_string
:= AForeignUnaryOp (enhanced_unary_sql_date_op uop_sql_date_from_string).
Definition sql_date_interval_from_string
:= AForeignUnaryOp (enhanced_unary_sql_date_op uop_sql_date_interval_from_string).
Definition AFloatNeg := float_neg.
Definition AFloatSqrt := float_sqrt.
Definition AFloatExp := float_exp.
Definition AFloatLog := float_log.
Definition AFloatLog10 := float_log10.
Definition AFloatOfInt := float_of_int.
Definition AFloatCeil := float_ceil.
Definition AFloatFloor := float_floor.
Definition AFloatTruncate := float_truncate.
Definition AFloatAbs := float_abs.
Definition AFloatSum := float_sum.
Definition AFloatArithMean := float_arithmean.
Definition AFloatListMin := float_listmin.
Definition AFloatListMax := float_listmax.
Definition ATimeToSscale := time_to_scale.
Definition ATimeFromString := time_from_string.
Definition ATimeDurationFromString := time_duration_from_string.
Definition ASqlGetDateComponent := sql_get_date_component.
Definition ASqlDateFromString := sql_date_from_string.
Definition ASqlDateIntervalFromString := sql_date_interval_from_string.
End Unary.
Module Binary.
Definition float_plus
:= AForeignBinaryOp (enhanced_binary_float_op bop_float_plus).
Definition float_minus
:= AForeignBinaryOp (enhanced_binary_float_op bop_float_minus).
Definition float_mult
:= AForeignBinaryOp (enhanced_binary_float_op bop_float_mult).
Definition float_div
:= AForeignBinaryOp (enhanced_binary_float_op bop_float_div).
Definition float_pow
:= AForeignBinaryOp (enhanced_binary_float_op bop_float_pow).
Definition float_min
:= AForeignBinaryOp (enhanced_binary_float_op bop_float_min).
Definition float_max
:= AForeignBinaryOp (enhanced_binary_float_op bop_float_max).
Definition float_ne
:= AForeignBinaryOp (enhanced_binary_float_op bop_float_ne).
Definition float_lt
:= AForeignBinaryOp (enhanced_binary_float_op bop_float_lt).
Definition float_le
:= AForeignBinaryOp (enhanced_binary_float_op bop_float_le).
Definition float_gt
:= AForeignBinaryOp (enhanced_binary_float_op bop_float_gt).
Definition float_ge
:= AForeignBinaryOp (enhanced_binary_float_op bop_float_ge).
Definition time_as
:= AForeignBinaryOp (enhanced_binary_time_op bop_time_as).
Definition time_shift
:= AForeignBinaryOp (enhanced_binary_time_op bop_time_shift).
Definition time_ne
:= AForeignBinaryOp (enhanced_binary_time_op bop_time_ne).
Definition time_lt
:= AForeignBinaryOp (enhanced_binary_time_op bop_time_lt).
Definition time_le
:= AForeignBinaryOp (enhanced_binary_time_op bop_time_le).
Definition time_gt
:= AForeignBinaryOp (enhanced_binary_time_op bop_time_gt).
Definition time_ge
:= AForeignBinaryOp (enhanced_binary_time_op bop_time_ge).
Definition time_duration_from_scale
:= AForeignBinaryOp (enhanced_binary_time_op (bop_time_duration_from_scale)).
Definition time_duration_between
:= AForeignBinaryOp (enhanced_binary_time_op (bop_time_duration_between)).
Definition sql_date_plus
:= AForeignBinaryOp (enhanced_binary_sql_date_op bop_sql_date_plus).
Definition sql_date_minus
:= AForeignBinaryOp (enhanced_binary_sql_date_op bop_sql_date_minus).
Definition sql_date_ne
:= AForeignBinaryOp (enhanced_binary_sql_date_op bop_sql_date_ne).
Definition sql_date_lt
:= AForeignBinaryOp (enhanced_binary_sql_date_op bop_sql_date_lt).
Definition sql_date_le
:= AForeignBinaryOp (enhanced_binary_sql_date_op bop_sql_date_le).
Definition sql_date_gt
:= AForeignBinaryOp (enhanced_binary_sql_date_op bop_sql_date_gt).
Definition sql_date_ge
:= AForeignBinaryOp (enhanced_binary_sql_date_op bop_sql_date_ge).
Definition sql_date_interval_between
:= AForeignBinaryOp (enhanced_binary_sql_date_op (bop_sql_date_interval_between)).
Definition AFloatPlus := float_plus.
Definition AFloatMinus := float_minus.
Definition AFloatMult := float_mult .
Definition AFloatDiv := float_div .
Definition AFloatPow := float_pow .
Definition AFloatMin := float_min .
Definition AFloatMax := float_max .
Definition AFloatNe := float_ne .
Definition AFloatLt := float_lt .
Definition AFloatLe := float_le .
Definition AFloatGt := float_gt .
Definition AFloatGe := float_ge .
Definition ATimeAs := time_as.
Definition ATimeShift := time_shift.
Definition ATimeNe := time_ne.
Definition ATimeLt := time_lt.
Definition ATimeLe := time_le.
Definition ATimeGt := time_gt.
Definition ATimeGe := time_ge.
Definition ATimeDurationFromScale := time_duration_from_scale.
Definition ATimeDurationBetween := time_duration_between.
Definition ASqlDatePlus := sql_date_plus.
Definition ASqlDateMinus := sql_date_minus.
Definition ASqlDateNe := sql_date_ne.
Definition ASqlDateLt := sql_date_lt.
Definition ASqlDateLe := sql_date_le.
Definition ASqlDateGt := sql_date_gt.
Definition ASqlDateGe := sql_date_ge.
Definition ASqlDateIntervalBetween := sql_date_interval_between.
End Binary.
End Ops.
End Enhanced.
End CompEnhanced.