summaryrefslogtreecommitdiff
path: root/lib/basis.urs
diff options
context:
space:
mode:
Diffstat (limited to 'lib/basis.urs')
-rw-r--r--lib/basis.urs30
1 files changed, 18 insertions, 12 deletions
diff --git a/lib/basis.urs b/lib/basis.urs
index 9681328f..eb2a6d29 100644
--- a/lib/basis.urs
+++ b/lib/basis.urs
@@ -202,6 +202,10 @@ val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-> 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 @@ val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-> 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 @@ val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-> 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