git.iko.soy/Idris-dev
on bb3e629 help sign in
Idris-dev/tutorial/syntax.tex
89 lines 3.2 kB history raw
1\subsection{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. For example, we have seen \texttt{if...then...else} expressions, but these
7are not built in --- instead, we define a function in the prelude\ldots
9\begin{SaveVerbatim}{boolelim}
11boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a;
12boolElim True t e = t;
13boolElim False t e = e;
15\end{SaveVerbatim}
16\useverb{boolelim}
18\noindent
19\ldots and extend the core syntax with a \texttt{syntax} declaration:
21\begin{SaveVerbatim}{syntaxif}
23syntax if [test] then [t] else [e] = boolElim test t e;
25\end{SaveVerbatim}
26\useverb{syntaxif}
28\noindent
29The left hand side of a \texttt{syntax} declaration describes the syntax rule, and the right
30hand side describes its expansion. The syntax rule itself consists of:
32\begin{itemize}
33\item \textbf{Keywords} --- here, \texttt{if}, \texttt{then} and \texttt{else}, which must
34be valid identifiers
35\item \textbf{Non-terminals} --- included in square brackets, \texttt{[test]}, \texttt{[t]}
36and \texttt{[e]} here, which stand for arbitrary expressions. To avoid parsing ambiguities,
37these expressions cannot use syntax extensions at the top level (though they can be used
38in parentheses).
39\item \textbf{Symbols} --- included in quotations marks, e.g. \texttt{":="}
40\end{itemize}
42\noindent
43The limitations on the form of a syntax rule are that it must include at least one
44symbol or keyword, and there must be no repeated variables standing for non-terminals.
45Rules can use previously defined rules, but may not be recursive.
46The following syntax extensions would therefore be valid:
48\begin{SaveVerbatim}{syntaxex}
50syntax [var] ":=" [val] = Assign var val;
51syntax [test] "?" [t] ":" [e] = if test then t else e;
52syntax select [x] from [t] where [w] = SelectWhere x t w;
53syntax select [x] from [t] = Select x t;
55\end{SaveVerbatim}
56\useverb{syntaxex}
58\noindent
59Syntax macros can be further restricted to apply only in patterns (i.e., only on the left
60hand side of a pattern match clause) or only in terms (i.e. everywhere but the left hand side
61of a pattern match clause) by being marked as \texttt{pattern} or \texttt{term} syntax
62rules. For example, we might define an interval as follows, with a static check
63that the lower bound is below the upper bound using \texttt{so}:
65\begin{SaveVerbatim}{interval}
67data Interval : Set where
68 MkInterval : (lower : Float) -> (upper : Float) ->
69 so (lower < upper) -> Interval
71\end{SaveVerbatim}
72\useverb{interval}
74\noindent
75We can define a syntax which, in patterns, always matches \texttt{oh} for the proof
76argument, and in terms requires a proof term to be provided:
78\begin{SaveVerbatim}{intervalsyn}
80pattern syntax "[" [x] "..." [y] "]" = MkInterval x y oh
81term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
83\end{SaveVerbatim}
84\useverb{intervalsyn}
86\noindent
87In terms, the syntax \texttt{[x...y]} will generate a proof obligation
88\texttt{bounds\_lemma} (possibly renamed).