tutorial/syntax.tex · Idris-dev

git.iko.soy/Idris-dev

on 2e9fcd4 help sign in

55 lines 2.0 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

37\item \textbf{Symbols} --- included in quotations marks, e.g. \texttt{":="}

38\end{itemize}

40\noindent

41The limitations on the form of a syntax rule are that it must include at least one

42symbol or keyword, and there must be no repeated variables standing for non-terminals.

43Rules can use previously defined rules, but may not be recursive.

44The following syntax extensions would therefore be valid:

46\begin{SaveVerbatim}{syntaxex}

48syntax [var] ":=" [val] = Assign var val;

49syntax [test] "?" [t] ":" [e] = if test then t else e;

50syntax select [x] from [t] where [w] = SelectWhere x t w;

51syntax select [x] from [t] = Select x t;

53\end{SaveVerbatim}

54\useverb{syntaxex}