\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{Symbols} --- included in quotations marks, e.g. \texttt{":="}
\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.
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 : Set 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).

\input{dsl}