git.iko.soy/Idris-dev
on bdf07be help sign in
Idris-dev/tutorial/syntax.tex
119 lines 4.2 kB history raw
1\section{Syntax Extensions}
3\Idris{} supports the implementation of Embedded Domain Specific Languages (EDSLs) in
4several ways~\cite{res-dsl-padl12}. One way, as we have already seen, is through
5extending \texttt{do} notation. Another important way is to allow extension of the core
6syntax. In this section we describe two ways of extending the syntax: \texttt{syntax}
7rules and \texttt{dsl} notation.
9\subsection{\texttt{syntax} rules}
11We have seen \texttt{if...then...else} expressions, but these
12are not built in --- instead, we define a function in the prelude\ldots
14\begin{SaveVerbatim}{boolelim}
16boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a;
17boolElim True t e = t;
18boolElim False t e = e;
20\end{SaveVerbatim}
21\useverb{boolelim}
23\noindent
24\ldots and extend the core syntax with a \texttt{syntax} declaration:
26\begin{SaveVerbatim}{syntaxif}
28syntax if [test] then [t] else [e] = boolElim test t e;
30\end{SaveVerbatim}
31\useverb{syntaxif}
33\noindent
34The left hand side of a \texttt{syntax} declaration describes the syntax rule, and the right
35hand side describes its expansion. The syntax rule itself consists of:
37\begin{itemize}
38\item \textbf{Keywords} --- here, \texttt{if}, \texttt{then} and \texttt{else}, which must
39be valid identifiers
40\item \textbf{Non-terminals} --- included in square brackets, \texttt{[test]}, \texttt{[t]}
41and \texttt{[e]} here, which stand for arbitrary expressions. To avoid parsing ambiguities,
42these expressions cannot use syntax extensions at the top level (though they can be used
43in parentheses).
44\item \textbf{Names} --- included in braces, which stand for names which may be bound
45on the right hand side.
46\item \textbf{Symbols} --- included in quotations marks, e.g. \texttt{":="}. This can
47also be used to include reserved words in syntax rules, such as \texttt{"let"} or \texttt{"in"}.
48\end{itemize}
50\noindent
51The limitations on the form of a syntax rule are that it must include at least one
52symbol or keyword, and there must be no repeated variables standing for non-terminals.
53Rules can use previously defined rules, but may not be recursive.
54The following syntax extensions would therefore be valid:
56\begin{SaveVerbatim}{syntaxex}
58syntax [var] ":=" [val] = Assign var val;
59syntax [test] "?" [t] ":" [e] = if test then t else e;
60syntax select [x] from [t] where [w] = SelectWhere x t w;
61syntax select [x] from [t] = Select x t;
63\end{SaveVerbatim}
64\useverb{syntaxex}
66\noindent
67Syntax macros can be further restricted to apply only in patterns (i.e., only on the left
68hand side of a pattern match clause) or only in terms (i.e. everywhere but the left hand side
69of a pattern match clause) by being marked as \texttt{pattern} or \texttt{term} syntax
70rules. For example, we might define an interval as follows, with a static check
71that the lower bound is below the upper bound using \texttt{so}:
73\begin{SaveVerbatim}{interval}
75data Interval : Type where
76 MkInterval : (lower : Float) -> (upper : Float) ->
77 so (lower < upper) -> Interval
79\end{SaveVerbatim}
80\useverb{interval}
82\noindent
83We can define a syntax which, in patterns, always matches \texttt{oh} for the proof
84argument, and in terms requires a proof term to be provided:
86\begin{SaveVerbatim}{intervalsyn}
88pattern syntax "[" [x] "..." [y] "]" = MkInterval x y oh
89term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
91\end{SaveVerbatim}
92\useverb{intervalsyn}
94\noindent
95In terms, the syntax \texttt{[x...y]} will generate a proof obligation
96\texttt{bounds\_lemma} (possibly renamed).
98Finally, syntax rules may be used to introduce alternative binding forms. For
99exampe, a \texttt{for} loop binds a variable on each iteration:
101\begin{SaveVerbatim}{forloop}
103syntax for {x} "in" [xs] [body] = forLoop xs (\x => body)
105main : IO ()
106main = do for x in [1..10] do
107 putStrLn ("Number " ++ show x)
108 putStrLn "Done!"
110\end{SaveVerbatim}
111\useverb{forloop}
113\noindent
114Note that we have used the \texttt{\{x\}} form to state that \texttt{x} represents
115a bound variable, substituted on the right hand side. We have also put \texttt{"in"} in
116quotation marks since it is already a reserved word.
118\input{dsl}