git.iko.soy/Idris-dev
on master help sign in
Some re-ordering of the tutorial
486b176Edwin Brady
CHANGELOG+2−1
compare with master
unifiedsplit
@@ -6,7 +6,8 @@ User visible changes:
6* dsl notation
6* dsl notation
7* record projection and update
7* record projection and update
8* auto implicits and default argument values {auto n : T}, {default val n : T}
8* auto implicits and default argument values {auto n : T}, {default val n : T}
9−* Additions to prelude
9+* Additions to prelude, including Nat and List theorems
10+* New libs: control.monad.identity, control.monad.state
10
11
11Internal changes:
12Internal changes:
12
13
tutorial/dsl.tex+1−1
@@ -1,4 +1,4 @@
1−\section{More on overloading: \texttt{dsl} notation}
1+\subsection{\texttt{dsl} notation}
2
2
3The well-typed interpreter in Section \ref{sect:interp} is a simple example of
3The well-typed interpreter in Section \ref{sect:interp} is a simple example of
4a common programming pattern with dependent types, namely: describe an
4a common programming pattern with dependent types, namely: describe an
tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/idris-tutorial.tex+1−1
@@ -28,8 +28,8 @@
28\input{views}
28\input{views}
29\input{theorems}
29\input{theorems}
30\input{provisional}
30\input{provisional}
31+\input{syntax}
31\input{miscellany}
32\input{miscellany}
32−\input{dsl}
33\input{conclusions}
33\input{conclusions}
34
34
35\bibliographystyle{abbrv}
35\bibliographystyle{abbrv}
tutorial/miscellany.tex+1−3
@@ -1,12 +1,10 @@
1\section{Miscellany}
1\section{Miscellany}
2
2
3−In this section we discuss a variety of additional features: extensible syntax,
3+In this section we discuss a variety of additional features:
4auto implicit and default
4auto implicit and default
5arguments, literate programming, interfacing with external libraries through the
5arguments, literate programming, interfacing with external libraries through the
6foriegn function interface, and the universe hierarchy.
6foriegn function interface, and the universe hierarchy.
7
7
8−\input{syntax}
9−
10\subsection{Auto implicit arguments}
8\subsection{Auto implicit arguments}
11
9
12We have already seen implicit arguments, which allows arguments to be omitted when
10We have already seen implicit arguments, which allows arguments to be omitted when
tutorial/syntax.tex+9−2
@@ -1,9 +1,14 @@
1−\subsection{Syntax Extensions}
1+\section{Syntax Extensions}
2
2
3\Idris{} supports the implementation of Embedded Domain Specific Languages (EDSLs) in
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
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
5extending \texttt{do} notation. Another important way is to allow extension of the core
6+syntax. In this section we describe two ways of extending the syntax: \texttt{syntax}
7+rules and \texttt{dsl} notation.
8+
9+\subsection{\texttt{syntax} rules}
10+
6−syntax. For example, we have seen \texttt{if...then...else} expressions, but these
11+We have seen \texttt{if...then...else} expressions, but these
7are not built in --- instead, we define a function in the prelude\ldots
12are not built in --- instead, we define a function in the prelude\ldots
8
13
9\begin{SaveVerbatim}{boolelim}
14\begin{SaveVerbatim}{boolelim}
@@ -87,3 +92,5 @@ term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
87In terms, the syntax \texttt{[x...y]} will generate a proof obligation
92In terms, the syntax \texttt{[x...y]} will generate a proof obligation
88\texttt{bounds\_lemma} (possibly renamed).
93\texttt{bounds\_lemma} (possibly renamed).
89
94
95+\input{dsl}
96+