Mercurial > urweb
diff lib/basis.urs @ 559:5d494183ca89
Add SQL arithmetic operators
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 09 Dec 2008 14:41:19 -0500 |
parents | 4154b4dc62c6 |
children | 803b2f3bb86b |
line wrap: on
line diff
--- a/lib/basis.urs Tue Dec 09 14:06:51 2008 -0500 +++ b/lib/basis.urs Tue Dec 09 14:41:19 2008 -0500 @@ -202,6 +202,10 @@ -> sql_exp tables agg exps (option t) -> sql_exp tables agg exps bool +class sql_arith +val sql_int_arith : sql_arith int +val sql_float_arith : sql_arith float + con sql_unary :: Type -> Type -> Type val sql_not : sql_unary bool bool val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} @@ -209,6 +213,8 @@ -> sql_unary arg res -> sql_exp tables agg exps arg -> sql_exp tables agg exps res +val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t + con sql_binary :: Type -> Type -> Type -> Type val sql_and : sql_binary bool bool bool val sql_or : sql_binary bool bool bool @@ -218,18 +224,18 @@ -> sql_exp tables agg exps arg2 -> sql_exp tables agg exps res -type sql_comparison -val sql_eq : sql_comparison -val sql_ne : sql_comparison -val sql_lt : sql_comparison -val sql_le : sql_comparison -val sql_gt : sql_comparison -val sql_ge : sql_comparison -val sql_comparison : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type - -> sql_comparison - -> sql_exp tables agg exps t -> sql_exp tables agg exps t - -> sql_exp tables agg exps bool +val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t +val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t +val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t +val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t +val sql_mod : sql_binary int int int + +val sql_eq : t ::: Type -> sql_binary t t bool +val sql_ne : t ::: Type -> sql_binary t t bool +val sql_lt : t ::: Type -> sql_binary t t bool +val sql_le : t ::: Type -> sql_binary t t bool +val sql_gt : t ::: Type -> sql_binary t t bool +val sql_ge : t ::: Type -> sql_binary t t bool val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> sql_exp tables agg exps int