From 5108a7e86734b335b65b9efd60a7f2f2797b602b Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 9 Dec 2008 14:41:19 -0500 Subject: Add SQL arithmetic operators --- doc/manual.tex | 24 +++++++++++---------- lib/basis.urs | 30 +++++++++++++++----------- lib/top.ur | 2 +- src/monoize.sml | 63 +++++++++++++++++++++++++------------------------------ src/urweb.grm | 29 +++++++++++++------------ tests/sql_ops.ur | 8 +++++++ tests/sql_ops.urp | 6 ++++++ 7 files changed, 89 insertions(+), 73 deletions(-) create mode 100644 tests/sql_ops.ur create mode 100644 tests/sql_ops.urp 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{} & \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 ( @@ -1440,32 +1458,6 @@ fun monoExp (env, st, fm) (all as (e, loc)) = | L.EFfi ("Basis", "sql_and") => ((L'.EPrim (Prim.String "AND"), loc), fm) | L.EFfi ("Basis", "sql_or") => ((L'.EPrim (Prim.String "OR"), loc), fm) - | L.ECApp ( - (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 ( @@ -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 => {[r.X]}, {[r.Y]}
); + return {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 -- cgit v1.2.3