git.iko.soy/Idris-dev
on master help sign in
Some re-ordering of the tutorial
commit486b176e574d433e08f5c39c494a46328ef43439 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 31 Jan 2012, 12:48 (15 years ago) parent141694f
6 files changed+14−8
compare with master
unifiedsplit
CHANGELOG+2−1 tutorial/dsl.tex+1−1 tutorial/idris-tutorial.pdf tutorial/idris-tutorial.tex+1−1 tutorial/miscellany.tex+1−3 tutorial/syntax.tex+9−2
CHANGELOG+2−1
@@ -6,7 +6,8 @@ User visible changes:
66* dsl notation
77* record projection and update
88* 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
1011
1112Internal changes:
1213
tutorial/dsl.tex+1−1
@@ -1,4 +1,4 @@
1−\section{More on overloading: \texttt{dsl} notation}
1+\subsection{\texttt{dsl} notation}
22
33The well-typed interpreter in Section \ref{sect:interp} is a simple example of
44a 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 @@
2828\input{views}
2929\input{theorems}
3030\input{provisional}
31+\input{syntax}
3132\input{miscellany}
32−\input{dsl}
3333\input{conclusions}
3434
3535\bibliographystyle{abbrv}
tutorial/miscellany.tex+1−3
@@ -1,12 +1,10 @@
11\section{Miscellany}
22
3−In this section we discuss a variety of additional features: extensible syntax,
3+In this section we discuss a variety of additional features:
44auto implicit and default
55arguments, literate programming, interfacing with external libraries through the
66foriegn function interface, and the universe hierarchy.
77
8−\input{syntax}
9−
108\subsection{Auto implicit arguments}
119
1210We 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}
22
33\Idris{} supports the implementation of Embedded Domain Specific Languages (EDSLs) in
44several ways~\cite{res-dsl-padl12}. One way, as we have already seen, is through
55extending \texttt{do} notation. Another important way is to allow extension of the core
6−syntax. For example, we have seen \texttt{if...then...else} expressions, but these
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+
11+We have seen \texttt{if...then...else} expressions, but these
712are not built in --- instead, we define a function in the prelude\ldots
813
914\begin{SaveVerbatim}{boolelim}
@@ -87,3 +92,5 @@ term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
8792In terms, the syntax \texttt{[x...y]} will generate a proof obligation
8893\texttt{bounds\_lemma} (possibly renamed).
8994
95+\input{dsl}
96+