Mercurial > urweb

comparison lib/basis.urs @ 559:5d494183ca89

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add SQL arithmetic operators
author Adam Chlipala <adamc@hcoop.net>
date Tue, 09 Dec 2008 14:41:19 -0500
parents 4154b4dc62c6
children 803b2f3bb86b
comparison
equal deleted inserted replaced
558:390cba747188 559:5d494183ca89
200 val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 200 val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
201 -> t ::: Type 201 -> t ::: Type
202 -> sql_exp tables agg exps (option t) 202 -> sql_exp tables agg exps (option t)
203 -> sql_exp tables agg exps bool 203 -> sql_exp tables agg exps bool
204 204
205 class sql_arith
206 val sql_int_arith : sql_arith int
207 val sql_float_arith : sql_arith float
208
205 con sql_unary :: Type -> Type -> Type 209 con sql_unary :: Type -> Type -> Type
206 val sql_not : sql_unary bool bool 210 val sql_not : sql_unary bool bool
207 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 211 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
208 -> arg ::: Type -> res ::: Type 212 -> arg ::: Type -> res ::: Type
209 -> sql_unary arg res -> sql_exp tables agg exps arg 213 -> sql_unary arg res -> sql_exp tables agg exps arg
210 -> sql_exp tables agg exps res 214 -> sql_exp tables agg exps res
215
216 val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t
211 217
212 con sql_binary :: Type -> Type -> Type -> Type 218 con sql_binary :: Type -> Type -> Type -> Type
213 val sql_and : sql_binary bool bool bool 219 val sql_and : sql_binary bool bool bool
214 val sql_or : sql_binary bool bool bool 220 val sql_or : sql_binary bool bool bool
215 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 221 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
216 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type 222 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
217 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1 223 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1
218 -> sql_exp tables agg exps arg2 224 -> sql_exp tables agg exps arg2
219 -> sql_exp tables agg exps res 225 -> sql_exp tables agg exps res
220 226
221 type sql_comparison 227 val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t
222 val sql_eq : sql_comparison 228 val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t
223 val sql_ne : sql_comparison 229 val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t
224 val sql_lt : sql_comparison 230 val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t
225 val sql_le : sql_comparison 231 val sql_mod : sql_binary int int int
226 val sql_gt : sql_comparison 232
227 val sql_ge : sql_comparison 233 val sql_eq : t ::: Type -> sql_binary t t bool
228 val sql_comparison : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 234 val sql_ne : t ::: Type -> sql_binary t t bool
229 -> t ::: Type 235 val sql_lt : t ::: Type -> sql_binary t t bool
230 -> sql_comparison 236 val sql_le : t ::: Type -> sql_binary t t bool
231 -> sql_exp tables agg exps t -> sql_exp tables agg exps t 237 val sql_gt : t ::: Type -> sql_binary t t bool
232 -> sql_exp tables agg exps bool 238 val sql_ge : t ::: Type -> sql_binary t t bool
233 239
234 val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 240 val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
235 -> sql_exp tables agg exps int 241 -> sql_exp tables agg exps int
236 242
237 con sql_aggregate :: Type -> Type 243 con sql_aggregate :: Type -> Type