git.iko.soy/Idris-dev
on d1663cc help sign in
Idris-dev/tutorial/content/syntax.tex
104 lines 4.1 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{code}
15boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a;
16boolElim True t e = t;
17boolElim False t e = e;
18\end{code}
20\noindent
21\ldots and extend the core syntax with a \texttt{syntax} declaration:
23\begin{code}
24syntax if [test] then [t] else [e] = boolElim test t e;
25\end{code}
27\noindent
28The left hand side of a \texttt{syntax} declaration describes the syntax rule, and the right
29hand side describes its expansion. The syntax rule itself consists of:
31\begin{itemize}
32\item \textbf{Keywords} --- here, \texttt{if}, \texttt{then} and \texttt{else}, which must
33be valid identifiers
34\item \textbf{Non-terminals} --- included in square brackets, \texttt{[test]}, \texttt{[t]}
35and \texttt{[e]} here, which stand for arbitrary expressions. To avoid parsing ambiguities,
36these expressions cannot use syntax extensions at the top level (though they can be used
37in parentheses).
38\item \textbf{Names} --- included in braces, which stand for names which may be bound
39on the right hand side.
40\item \textbf{Symbols} --- included in quotations marks, e.g. \texttt{":="}. This can
41also be used to include reserved words in syntax rules, such as \texttt{"let"} or \texttt{"in"}.
42\end{itemize}
44\noindent
45The limitations on the form of a syntax rule are that it must include at least
46one symbol or keyword, and there must be no repeated variables standing for
47non-terminals. Any expression can be used, but if there are two non-terminals
48in a row in a rule, only simple expressions may be used (that is, variables,
49constants, or bracketed expressions). Rules can use previously defined rules,
50but may not be recursive. The following syntax extensions would therefore be
51valid:
53\begin{code}
54syntax [var] ":=" [val] = Assign var val;
55syntax [test] "?" [t] ":" [e] = if test then t else e;
56syntax select [x] from [t] where [w] = SelectWhere x t w;
57syntax select [x] from [t] = Select x t;
58\end{code}
60\noindent
61Syntax macros can be further restricted to apply only in patterns (i.e., only on the left
62hand side of a pattern match clause) or only in terms (i.e. everywhere but the left hand side
63of a pattern match clause) by being marked as \texttt{pattern} or \texttt{term} syntax
64rules. For example, we might define an interval as follows, with a static check
65that the lower bound is below the upper bound using \texttt{so}:
67\begin{code}
68data Interval : Type where
69 MkInterval : (lower : Float) -> (upper : Float) ->
70 so (lower < upper) -> Interval
71\end{code}
73\noindent
74We can define a syntax which, in patterns, always matches \texttt{oh} for the proof
75argument, and in terms requires a proof term to be provided:
77\begin{code}
78pattern syntax "[" [x] "..." [y] "]" = MkInterval x y oh
79term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
80\end{code}
82\noindent
83In terms, the syntax \texttt{[x...y]} will generate a proof obligation
84\texttt{bounds\_lemma} (possibly renamed).
86Finally, syntax rules may be used to introduce alternative binding forms. For
87exampe, a \texttt{for} loop binds a variable on each iteration:
89\begin{code}
90syntax for {x} "in" [xs] ":" [body] = forLoop xs (\x => body)
92main : IO ()
93main = do for x in [1..10]:
94 putStrLn ("Number " ++ show x)
95 putStrLn "Done!"
96\end{code}
98\noindent
99Note that we have used the \texttt{\{x\}} form to state that \texttt{x} represents
100a bound variable, substituted on the right hand side. We have also put \texttt{"in"} in
101quotation marks since it is already a reserved word.
103\input{./content/dsl}