summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-12-09 14:41:19 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-12-09 14:41:19 -0500
commit5108a7e86734b335b65b9efd60a7f2f2797b602b (patch)
tree1bdcd341e3e43df6833972a5384b8552f8343039
parent55fefa6122803e9739e9e71f1d50eae671665df4 (diff)
Add SQL arithmetic operators
-rw-r--r--doc/manual.tex24
-rw-r--r--lib/basis.urs30
-rw-r--r--lib/top.ur2
-rw-r--r--src/monoize.sml63
-rw-r--r--src/urweb.grm29
-rw-r--r--tests/sql_ops.ur8
-rw-r--r--tests/sql_ops.urp6
7 files changed, 89 insertions, 73 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 3c97b720..21092735 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -1198,7 +1198,7 @@ $$\begin{array}{l}
\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; (\mt{option} \; \mt{t}) \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{bool}
\end{array}$$
-We have generic nullary, unary, and binary operators, as well as comparison operators.
+We have generic nullary, unary, and binary operators.
$$\begin{array}{l}
\mt{con} \; \mt{sql\_nfunc} :: \mt{Type} \to \mt{Type} \\
\mt{val} \; \mt{sql\_current\_timestamp} : \mt{sql\_nfunc} \; \mt{time} \\
@@ -1221,16 +1221,16 @@ $$\begin{array}{l}
\end{array}$$
$$\begin{array}{l}
- \mt{type} \; \mt{sql\_comparison} \\
- \mt{val} \; \mt{sql\_eq} : \mt{sql\_comparison} \\
- \mt{val} \; \mt{sql\_ne} : \mt{sql\_comparison} \\
- \mt{val} \; \mt{sql\_lt} : \mt{sql\_comparison} \\
- \mt{val} \; \mt{sql\_le} : \mt{sql\_comparison} \\
- \mt{val} \; \mt{sql\_gt} : \mt{sql\_comparison} \\
- \mt{val} \; \mt{sql\_ge} : \mt{sql\_comparison} \\
- \mt{val} \; \mt{sql\_comparison} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
- \hspace{.1in} \to \mt{sql\_comparison} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{bool}
- \end{array}$$
+ \mt{class} \; \mt{sql\_arith} \\
+ \mt{val} \; \mt{sql\_int\_arith} : \mt{sql\_arith} \; \mt{int} \\
+ \mt{val} \; \mt{sql\_float\_arith} : \mt{sql\_arith} \; \mt{float} \\
+ \mt{val} \; \mt{sql\_neg} : \mt{t} ::: \mt{Type} \to \mt{sql\_arith} \; \mt{t} \to \mt{sql\_unary} \; \mt{t} \; \mt{t} \\
+ \mt{val} \; \mt{sql\_plus} : \mt{t} ::: \mt{Type} \to \mt{sql\_arith} \; \mt{t} \to \mt{sql\_binary} \; \mt{t} \; \mt{t} \; \mt{t} \\
+ \mt{val} \; \mt{sql\_minus} : \mt{t} ::: \mt{Type} \to \mt{sql\_arith} \; \mt{t} \to \mt{sql\_binary} \; \mt{t} \; \mt{t} \; \mt{t} \\
+ \mt{val} \; \mt{sql\_times} : \mt{t} ::: \mt{Type} \to \mt{sql\_arith} \; \mt{t} \to \mt{sql\_binary} \; \mt{t} \; \mt{t} \; \mt{t} \\
+ \mt{val} \; \mt{sql\_div} : \mt{t} ::: \mt{Type} \to \mt{sql\_arith} \; \mt{t} \to \mt{sql\_binary} \; \mt{t} \; \mt{t} \; \mt{t} \\
+ \mt{val} \; \mt{sql\_mod} : \mt{sql\_binary} \; \mt{int} \; \mt{int} \; \mt{int}
+\end{array}$$
Finally, we have aggregate functions. The $\mt{COUNT(\ast)}$ syntax is handled specially, since it takes no real argument. The other aggregate functions are placed into a general type family, using type classes to restrict usage to properly-typed arguments. The key aspect of the $\mt{sql\_aggregate}$ function's type is the shift of aggregate-function-only fields into unrestricted fields.
@@ -1445,6 +1445,8 @@ $$\begin{array}{rrcll}
\textrm{XML pieces} & l &::=& \textrm{text} & \textrm{cdata} \\
&&& \texttt{<}g\texttt{/>} & \textrm{tag with no children} \\
&&& \texttt{<}g\texttt{>}l^*\texttt{</}x\texttt{>} & \textrm{tag with children} \\
+ &&& \{e\} & \textrm{computed XML fragment} \\
+ &&& \{[e]\} & \textrm{injection of an Ur expression, via the $\mt{Top}.\mt{txt}$ function} \\
\textrm{Tag} & g &::=& h \; (x = v)^* \\
\textrm{Tag head} & h &::=& x & \textrm{tag name} \\
&&& h\{c\} & \textrm{constructor parameter} \\
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
diff --git a/lib/top.ur b/lib/top.ur
index 76fe73c1..fd7676a3 100644
--- a/lib/top.ur
+++ b/lib/top.ur
@@ -238,4 +238,4 @@ fun eqNullable' (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type})
(e2 : option t) =
case e2 of
None => (SQL {e1} IS NULL)
- | Some _ => sql_comparison sql_eq e1 (@sql_inject inj e2)
+ | Some _ => sql_binary sql_eq e1 (@sql_inject inj e2)
diff --git a/src/monoize.sml b/src/monoize.sml
index cd20e366..1880c57d 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -165,14 +165,14 @@ fun monoType env =
(L'.TFfi ("Basis", "string"), loc)
| L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_binary"), _), _), _), _), _), _) =>
(L'.TFfi ("Basis", "string"), loc)
- | L.CFfi ("Basis", "sql_comparison") =>
- (L'.TFfi ("Basis", "string"), loc)
| L.CApp ((L.CFfi ("Basis", "sql_aggregate"), _), t) =>
(L'.TFfi ("Basis", "string"), loc)
| L.CApp ((L.CFfi ("Basis", "sql_summable"), _), _) =>
(L'.TRecord [], loc)
| L.CApp ((L.CFfi ("Basis", "sql_maxable"), _), _) =>
(L'.TRecord [], loc)
+ | L.CApp ((L.CFfi ("Basis", "sql_arith"), _), _) =>
+ (L'.TRecord [], loc)
| L.CApp ((L.CFfi ("Basis", "sql_nfunc"), _), _) =>
(L'.TFfi ("Basis", "string"), loc)
@@ -1369,19 +1369,34 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
fm)
end
- | L.EFfi ("Basis", "sql_eq") =>
+ | L.ECApp ((L.EFfi ("Basis", "sql_eq"), _), _) =>
((L'.EPrim (Prim.String "="), loc), fm)
- | L.EFfi ("Basis", "sql_ne") =>
+ | L.ECApp ((L.EFfi ("Basis", "sql_ne"), _), _) =>
((L'.EPrim (Prim.String "<>"), loc), fm)
- | L.EFfi ("Basis", "sql_lt") =>
+ | L.ECApp ((L.EFfi ("Basis", "sql_lt"), _), _) =>
((L'.EPrim (Prim.String "<"), loc), fm)
- | L.EFfi ("Basis", "sql_le") =>
+ | L.ECApp ((L.EFfi ("Basis", "sql_le"), _), _) =>
((L'.EPrim (Prim.String "<="), loc), fm)
- | L.EFfi ("Basis", "sql_gt") =>
+ | L.ECApp ((L.EFfi ("Basis", "sql_gt"), _), _) =>
((L'.EPrim (Prim.String ">"), loc), fm)
- | L.EFfi ("Basis", "sql_ge") =>
+ | L.ECApp ((L.EFfi ("Basis", "sql_ge"), _), _) =>
((L'.EPrim (Prim.String ">="), loc), fm)
+ | L.ECApp ((L.EFfi ("Basis", "sql_plus"), _), _) =>
+ ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc),
+ (L'.EPrim (Prim.String "+"), loc)), loc), fm)
+ | L.ECApp ((L.EFfi ("Basis", "sql_minus"), _), _) =>
+ ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc),
+ (L'.EPrim (Prim.String "-"), loc)), loc), fm)
+ | L.ECApp ((L.EFfi ("Basis", "sql_times"), _), _) =>
+ ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc),
+ (L'.EPrim (Prim.String "*"), loc)), loc), fm)
+ | L.ECApp ((L.EFfi ("Basis", "sql_div"), _), _) =>
+ ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc),
+ (L'.EPrim (Prim.String "/"), loc)), loc), fm)
+ | L.EFfi ("Basis", "sql_mod") =>
+ ((L'.EPrim (Prim.String "%"), loc), fm)
+
| L.ECApp (
(L.ECApp (
(L.ECApp (
@@ -1407,6 +1422,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
fm)
end
| L.EFfi ("Basis", "sql_not") => ((L'.EPrim (Prim.String "NOT"), loc), fm)
+ | L.ECApp ((L.EFfi ("Basis", "sql_neg"), _), _) =>
+ ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc),
+ (L'.EPrim (Prim.String "-"), loc)), loc), fm)
| L.ECApp (
(L.ECApp (
@@ -1444,32 +1462,6 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
(L.ECApp (
(L.ECApp (
(L.ECApp (
- (L.EFfi ("Basis", "sql_comparison"), _),
- _), _),
- _), _),
- _), _),
- _) =>
- let
- val s = (L'.TFfi ("Basis", "string"), loc)
- fun sc s = (L'.EPrim (Prim.String s), loc)
- in
- ((L'.EAbs ("c", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc),
- (L'.EAbs ("e1", s, (L'.TFun (s, s), loc),
- (L'.EAbs ("e2", s, s,
- strcat loc [sc "(",
- (L'.ERel 1, loc),
- sc " ",
- (L'.ERel 2, loc),
- sc " ",
- (L'.ERel 0, loc),
- sc ")"]), loc)), loc)), loc),
- fm)
- end
-
- | L.ECApp (
- (L.ECApp (
- (L.ECApp (
- (L.ECApp (
(L.ECApp (
(L.ECApp (
(L.ECApp (
@@ -1566,6 +1558,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
(L'.EPrim (Prim.String "SUM"), loc)), loc),
fm)
+ | L.EFfi ("Basis", "sql_arith_int") => ((L'.ERecord [], loc), fm)
+ | L.EFfi ("Basis", "sql_arith_float") => ((L'.ERecord [], loc), fm)
+
| L.EFfi ("Basis", "sql_maxable_int") => ((L'.ERecord [], loc), fm)
| L.EFfi ("Basis", "sql_maxable_float") => ((L'.ERecord [], loc), fm)
| L.EFfi ("Basis", "sql_maxable_string") => ((L'.ERecord [], loc), fm)
diff --git a/src/urweb.grm b/src/urweb.grm
index 3d77905e..7798b018 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -119,15 +119,6 @@ fun amend_group loc (gi, tabs) =
fun sql_inject (v, loc) =
(EApp ((EVar (["Basis"], "sql_inject", Infer), loc), (v, loc)), loc)
-fun sql_compare (oper, sqlexp1, sqlexp2, loc) =
- let
- val e = (EVar (["Basis"], "sql_comparison", Infer), loc)
- val e = (EApp (e, (EVar (["Basis"], "sql_" ^ oper, Infer), loc)), loc)
- val e = (EApp (e, sqlexp1), loc)
- in
- (EApp (e, sqlexp2), loc)
- end
-
fun sql_binary (oper, sqlexp1, sqlexp2, loc) =
let
val e = (EVar (["Basis"], "sql_binary", Infer), loc)
@@ -1239,16 +1230,24 @@ sqlexp : TRUE (sql_inject (EVar (["Basis"], "True", In
| LBRACE eexp RBRACE (eexp)
- | sqlexp EQ sqlexp (sql_compare ("eq", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
- | sqlexp NE sqlexp (sql_compare ("ne", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
- | sqlexp LT sqlexp (sql_compare ("lt", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
- | sqlexp LE sqlexp (sql_compare ("le", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
- | sqlexp GT sqlexp (sql_compare ("gt", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
- | sqlexp GE sqlexp (sql_compare ("ge", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
+ | sqlexp EQ sqlexp (sql_binary ("eq", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
+ | sqlexp NE sqlexp (sql_binary ("ne", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
+ | sqlexp LT sqlexp (sql_binary ("lt", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
+ | sqlexp LE sqlexp (sql_binary ("le", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
+ | sqlexp GT sqlexp (sql_binary ("gt", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
+ | sqlexp GE sqlexp (sql_binary ("ge", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
+
+ | sqlexp PLUS sqlexp (sql_binary ("plus", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
+ | sqlexp MINUS sqlexp (sql_binary ("minus", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
+ | sqlexp STAR sqlexp (sql_binary ("times", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
+ | sqlexp DIVIDE sqlexp (sql_binary ("div", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
+ | sqlexp MOD sqlexp (sql_binary ("mod", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
| sqlexp CAND sqlexp (sql_binary ("and", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
| sqlexp OR sqlexp (sql_binary ("or", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
+
| NOT sqlexp (sql_unary ("not", sqlexp, s (NOTleft, sqlexpright)))
+ | MINUS sqlexp (sql_unary ("neg", sqlexp, s (MINUSleft, sqlexpright)))
| sqlexp IS NULL (let
val loc = s (sqlexpleft, NULLright)
diff --git a/tests/sql_ops.ur b/tests/sql_ops.ur
new file mode 100644
index 00000000..34e78775
--- /dev/null
+++ b/tests/sql_ops.ur
@@ -0,0 +1,8 @@
+table t : { A : int, B : float }
+
+val q = (SELECT t.A + t.A AS X, t.B * t.B AS Y FROM t)
+
+fun main () : transaction page =
+ xml <- queryX q (fn r => <xml>{[r.X]}, {[r.Y]}<br/></xml>);
+ return <xml><body>{xml}</body></xml>
+
diff --git a/tests/sql_ops.urp b/tests/sql_ops.urp
new file mode 100644
index 00000000..90e47b77
--- /dev/null
+++ b/tests/sql_ops.urp
@@ -0,0 +1,6 @@
+debug
+database dbname=sql_ops
+sql sql_ops.sql
+exe /tmp/webapp
+
+sql_ops