diff doc/manual.tex @ 1573:34364e383bed

For new IF, fix Monoize typing and add to manual
author Adam Chlipala <adam@chlipala.net>
date Sat, 15 Oct 2011 09:04:41 -0400
parents 0fab80567fa3
children 644558d9c756
line wrap: on
line diff
--- a/doc/manual.tex	Fri Oct 14 02:33:03 2011 -0430
+++ b/doc/manual.tex	Sat Oct 15 09:04:41 2011 -0400
@@ -1783,6 +1783,15 @@
 \hspace{.1in} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_query} \; \mt{tables} \; \mt{agg} \; [\mt{nm} = \mt{t}] \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{nt}
 \end{array}$$
 
+There is also an \cd{IF..THEN..ELSE..} construct that is compiled into standard SQL \cd{CASE} expressions.
+$$\begin{array}{l}
+\mt{val} \; \mt{sql\_if\_then\_else} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
+\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{bool} \\
+\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\
+\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\
+\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t}
+\end{array}$$
+
 \texttt{FROM} clauses are specified using a type family, whose arguments are the free table variables and the table variables bound by this clause.
 $$\begin{array}{l}
   \mt{con} \; \mt{sql\_from\_items} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\
@@ -2133,6 +2142,7 @@
   &&& E \; b \; E & \textrm{binary operators} \\
   &&& \mt{COUNT}(\ast) & \textrm{count number of rows} \\
   &&& a(E) & \textrm{other aggregate function} \\
+  &&& \mt{IF} \; E \; \mt{THEN} \; E \; \mt{ELSE} \; E & \textrm{conditional} \\
   &&& (Q) & \textrm{subquery (must return a single expression column)} \\
   &&& (E) & \textrm{explicit precedence} \\
   \textrm{Nullary operators} & n &::=& \mt{CURRENT\_TIMESTAMP} \\