\section{Syntax Extensions}

\Idris{} supports the implementation of Embedded Domain Specific Languages (EDSLs) in
several ways~\cite{res-dsl-padl12}. One way, as we have already seen, is through
extending \texttt{do} notation. Another important way is to allow extension of the core
syntax. In this section we describe two ways of extending the syntax: \texttt{syntax}
rules and \texttt{dsl} notation.

\subsection{\texttt{syntax} rules}

We have seen \texttt{if...then...else} expressions, but these
are not built in --- instead, we define a function in the prelude\ldots

\begin{SaveVerbatim}{boolelim}

boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a; 
boolElim True  t e = t;
boolElim False t e = e;

\end{SaveVerbatim}
\useverb{boolelim}

\noindent
\ldots and extend the core syntax with a \texttt{syntax} declaration:

\begin{SaveVerbatim}{syntaxif}

syntax if [test] then [t] else [e] = boolElim test t e;

\end{SaveVerbatim}
\useverb{syntaxif}

\noindent
The left hand side of a \texttt{syntax} declaration describes the syntax rule, and the right
hand side describes its expansion. The syntax rule itself consists of:

\begin{itemize}
\item \textbf{Keywords} --- here, \texttt{if}, \texttt{then} and \texttt{else}, which must
be valid identifiers
\item \textbf{Non-terminals} --- included in square brackets, \texttt{[test]}, \texttt{[t]}
and \texttt{[e]} here, which stand for arbitrary expressions. To avoid parsing ambiguities, 
these expressions cannot use syntax extensions at the top level (though they can be used
in parentheses).
\item \textbf{Names} --- included in braces, which stand for names which may be bound
on the right hand side.
\item \textbf{Symbols} --- included in quotations marks, e.g. \texttt{":="}. This can
also be used to include reserved words in syntax rules, such as \texttt{"let"} or \texttt{"in"}.
\end{itemize}

\noindent
The limitations on the form of a syntax rule are that it must include at least
one symbol or keyword, and there must be no repeated variables standing for
non-terminals. Any expression can be used, but if there are two non-terminals
in a row in a rule, only simple expressions may be used (that is, variables,
constants, or bracketed expressions). Rules can use previously defined rules,
but may not be recursive.  The following syntax extensions would therefore be
valid:

\begin{SaveVerbatim}{syntaxex}

syntax [var] ":=" [val]              = Assign var val;
syntax [test] "?" [t] ":" [e]        = if test then t else e;
syntax select [x] from [t] where [w] = SelectWhere x t w;
syntax select [x] from [t]           = Select x t;

\end{SaveVerbatim}
\useverb{syntaxex}

\noindent
Syntax macros can be further restricted to apply only in patterns (i.e., only on the left
hand side of a pattern match clause) or only in terms (i.e. everywhere but the left hand side
of a pattern match clause) by being marked as \texttt{pattern} or \texttt{term} syntax
rules. For example, we might define an interval as follows, with a static check
that the lower bound is below the upper bound using \texttt{so}:

\begin{SaveVerbatim}{interval}

data Interval : Type where
   MkInterval : (lower : Float) -> (upper : Float) -> 
                so (lower < upper) -> Interval

\end{SaveVerbatim}
\useverb{interval}

\noindent
We can define a syntax which, in patterns, always matches \texttt{oh} for the proof 
argument, and in terms requires a proof term to be provided:

\begin{SaveVerbatim}{intervalsyn}

pattern syntax "[" [x] "..." [y] "]" = MkInterval x y oh
term    syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma

\end{SaveVerbatim}
\useverb{intervalsyn} 

\noindent
In terms, the syntax \texttt{[x...y]} will generate a proof obligation
\texttt{bounds\_lemma} (possibly renamed).

Finally, syntax rules may be used to introduce alternative binding forms. For
exampe, a \texttt{for} loop binds a variable on each iteration:

\begin{SaveVerbatim}{forloop}

syntax for {x} "in" [xs] ":" [body] = forLoop xs (\x => body)
  
main : IO ()
main = do for x in [1..10]:
              putStrLn ("Number " ++ show x)
          putStrLn "Done!"

\end{SaveVerbatim}
\useverb{forloop} 

\noindent
Note that we have used the \texttt{\{x\}} form to state that \texttt{x} represents
a bound variable, substituted on the right hand side. We have also put \texttt{"in"} in
quotation marks since it is already a reserved word.

\input{dsl}