git.iko.soy/Idris-dev
on f593dcc help sign in
Idris-dev/tutorial/syntax.tex
122 lines 4.4 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
52one symbol or keyword, and there must be no repeated variables standing for
53non-terminals. Any expression can be used, but if there are two non-terminals
54in a row in a rule, only simple expressions may be used (that is, variables,
55constants, or bracketed expressions). Rules can use previously defined rules,
56but may not be recursive. The following syntax extensions would therefore be
57valid:
59\begin{SaveVerbatim}{syntaxex}
61syntax [var] ":=" [val] = Assign var val;
62syntax [test] "?" [t] ":" [e] = if test then t else e;
63syntax select [x] from [t] where [w] = SelectWhere x t w;
64syntax select [x] from [t] = Select x t;
66\end{SaveVerbatim}
67\useverb{syntaxex}
69\noindent
70Syntax macros can be further restricted to apply only in patterns (i.e., only on the left
71hand side of a pattern match clause) or only in terms (i.e. everywhere but the left hand side
72of a pattern match clause) by being marked as \texttt{pattern} or \texttt{term} syntax
73rules. For example, we might define an interval as follows, with a static check
74that the lower bound is below the upper bound using \texttt{so}:
76\begin{SaveVerbatim}{interval}
78data Interval : Type where
79 MkInterval : (lower : Float) -> (upper : Float) ->
80 so (lower < upper) -> Interval
82\end{SaveVerbatim}
83\useverb{interval}
85\noindent
86We can define a syntax which, in patterns, always matches \texttt{oh} for the proof
87argument, and in terms requires a proof term to be provided:
89\begin{SaveVerbatim}{intervalsyn}
91pattern syntax "[" [x] "..." [y] "]" = MkInterval x y oh
92term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
94\end{SaveVerbatim}
95\useverb{intervalsyn}
97\noindent
98In terms, the syntax \texttt{[x...y]} will generate a proof obligation
99\texttt{bounds\_lemma} (possibly renamed).
101Finally, syntax rules may be used to introduce alternative binding forms. For
102exampe, a \texttt{for} loop binds a variable on each iteration:
104\begin{SaveVerbatim}{forloop}
106syntax for {x} "in" [xs] ":" [body] = forLoop xs (\x => body)
108main : IO ()
109main = do for x in [1..10]:
110 putStrLn ("Number " ++ show x)
111 putStrLn "Done!"
113\end{SaveVerbatim}
114\useverb{forloop}
116\noindent
117Note that we have used the \texttt{\{x\}} form to state that \texttt{x} represents
118a bound variable, substituted on the right hand side. We have also put \texttt{"in"} in
119quotation marks since it is already a reserved word.
121\input{dsl}