git.iko.soy/Idris-dev
on master help sign in
Merge pull request #613 from jfdm/tutorial
cda1274Edwin Brady
.gitignore+2
compare with master
unifiedsplit
@@ -21,3 +21,5 @@ tutorial/*.blg
21tutorial/*.log
21tutorial/*.log
22tutorial/*.out
22tutorial/*.out
23tutorial/*.toc
23tutorial/*.toc
24+tutorial/*.fdb_latexmk
25+tutorial/*.fls
tutorial/Makefile+1−4
@@ -2,9 +2,7 @@ PAPER = idris-tutorial
2
2
3all: ${PAPER}.pdf
3all: ${PAPER}.pdf
4
4
5−TEXFILES = ${PAPER}.tex intro.tex starting.tex miscellany.tex typesfuns.tex \
5+TEXFILES = ${PAPER}.tex content/*.tex
6− classes.tex modules.tex interp.tex views.tex theorems.tex \
7− provisional.tex syntax.tex conclusions.tex miscellany.tex dsl.tex
8
6
9DIAGS =
7DIAGS =
10
8
@@ -13,7 +11,6 @@ SOURCES = ${TEXFILES} ${DIAGS} macros.ltx library.ltx literature.bib
13DITAA = java -jar ~/Downloads/ditaa.jar
11DITAA = java -jar ~/Downloads/ditaa.jar
14
12
15${PAPER}.pdf: ${SOURCES}
13${PAPER}.pdf: ${SOURCES}
16−# dvipdf ${PAPER}.dvi
17 pdflatex ${PAPER}
14 pdflatex ${PAPER}
18 -bibtex ${PAPER}
15 -bibtex ${PAPER}
19 -pdflatex ${PAPER}
16 -pdflatex ${PAPER}
tutorial/conf.ltx+6−1
@@ -1,6 +1,11 @@
1−
2%% This file contains configurations of used packages
1%% This file contains configurations of used packages
3
2
3+\lstset{%
4+ basicstyle=\ttfamily,
5+ xleftmargin=\parindent,
6+ tabsize=2
7+}
8+
4
9
5% Configuration of hyperref (to not use colors):
10% Configuration of hyperref (to not use colors):
6\hypersetup{
11\hypersetup{
tutorial/classes.tex → tutorial/content/classes.texrenamed+66−163
@@ -14,24 +14,18 @@ is the \texttt{Show} type class, which is defined in the prelude and
14provides an interface for converting values to
14provides an interface for converting values to
15\texttt{String}s:
15\texttt{String}s:
16
16
17−\begin{SaveVerbatim}{showclass}
17+\begin{code}
18−
19class Show a where
18class Show a where
20 show : a -> String
19 show : a -> String
21−
20+\end{code}
22−\end{SaveVerbatim}
23−\useverb{showclass}
24
21
25\noindent
22\noindent
26This generates a function of the following type (which we call a \emph{method} of the
23This generates a function of the following type (which we call a \emph{method} of the
27\texttt{Show} class):
24\texttt{Show} class):
28
25
29−\begin{SaveVerbatim}{showty}
26+\begin{code}
30−
31show : Show a => a -> String
27show : Show a => a -> String
32−
28+\end{code}
33−\end{SaveVerbatim}
34−\useverb{showty}
35
29
36\noindent
30\noindent
37We can read this as ``under the constraint that \texttt{a} is an instance of \texttt{Show},
31We can read this as ``under the constraint that \texttt{a} is an instance of \texttt{Show},
@@ -40,17 +34,16 @@ is defined with an \texttt{instance} declaration, which provides implementations
40the function for a specific type. For example, the \texttt{Show} instance for \texttt{Nat}
34the function for a specific type. For example, the \texttt{Show} instance for \texttt{Nat}
41could be defined as:
35could be defined as:
42
36
43−\begin{SaveVerbatim}{shownat}
37+\begin{code}
44−
45instance Show Nat where
38instance Show Nat where
46 show Z = "Z"
39 show Z = "Z"
47 show (S k) = "s" ++ show k
40 show (S k) = "s" ++ show k
41+\end{code}
48
42
43+\begin{lstlisting}
49Idris> show (S (S (S Z)))
44Idris> show (S (S (S Z)))
50"sssO" : String
45"sssO" : String
51−
46+\end{lstlisting}
52−\end{SaveVerbatim}
53−\useverb{shownat}
54
47
55\noindent
48\noindent
56Only one instance of a class can be given for a type --- instances may not overlap.
49Only one instance of a class can be given for a type --- instances may not overlap.
@@ -59,17 +52,14 @@ Instance declarations can themselves have constraints. For example, to define a
59instance for the element type, because we are going to use it to convert each element
52instance for the element type, because we are going to use it to convert each element
60to a \texttt{String}:
53to a \texttt{String}:
61
54
62−\begin{SaveVerbatim}{showvec}
55+\begin{code}
63−
64instance Show a => Show (Vect n a) where
56instance Show a => Show (Vect n a) where
65 show xs = "[" ++ show' xs ++ "]" where
57 show xs = "[" ++ show' xs ++ "]" where
66 show' : Vect n a -> String
58 show' : Vect n a -> String
67 show' Nil = ""
59 show' Nil = ""
68 show' (x :: Nil) = show x
60 show' (x :: Nil) = show x
69 show' (x :: xs) = show x ++ ", " ++ show' xs
61 show' (x :: xs) = show x ++ ", " ++ show' xs
70−
62+\end{code}
71−\end{SaveVerbatim}
72−\useverb{showvec}
73
63
74%\noindent
64%\noindent
75%\textbf{Remark: } The type of the auxiliary function \texttt{show'} is
65%\textbf{Remark: } The type of the auxiliary function \texttt{show'} is
@@ -85,21 +75,17 @@ instance Show a => Show (Vect n a) where
85The library defines an \texttt{Eq} class which provides an interface for comparing
75The library defines an \texttt{Eq} class which provides an interface for comparing
86values for equality or inequality, with instances for all of the built-in types:
76values for equality or inequality, with instances for all of the built-in types:
87
77
88−\begin{SaveVerbatim}{eqbasic}
78+\begin{code}
89−
90class Eq a where
79class Eq a where
91 (==) : a -> a -> Bool
80 (==) : a -> a -> Bool
92 (/=) : a -> a -> Bool
81 (/=) : a -> a -> Bool
93−
82+\end{code}
94−\end{SaveVerbatim}
95−\useverb{eqbasic}
96
83
97\noindent
84\noindent
98To declare an instance of a type, we have to give definitions of all of the methods.
85To declare an instance of a type, we have to give definitions of all of the methods.
99For example, for an instance of \texttt{Eq} for \texttt{Nat}:
86For example, for an instance of \texttt{Eq} for \texttt{Nat}:
100
87
101−\begin{SaveVerbatim}{eqnat}
88+\begin{code}
102−
103instance Eq Nat where
89instance Eq Nat where
104 Z == Z = True
90 Z == Z = True
105 (S x) == (S y) = x == y
91 (S x) == (S y) = x == y
@@ -107,9 +93,7 @@ instance Eq Nat where
107 (S x) == Z = False
93 (S x) == Z = False
108
94
109 x /= y = not (x == y)
95 x /= y = not (x == y)
110−
96+\end{code}
111−\end{SaveVerbatim}
112−\useverb{eqnat}
113
97
114\noindent
98\noindent
115It is hard to imagine many cases where the \texttt{/=} method will be anything other
99It is hard to imagine many cases where the \texttt{/=} method will be anything other
@@ -117,17 +101,14 @@ than the negation of the result of applying the \texttt{==} method. It is theref
117convenient to give a default definition for each method in the class
101convenient to give a default definition for each method in the class
118declaration, in terms of the other method:
102declaration, in terms of the other method:
119
103
120−\begin{SaveVerbatim}{eqdefault}
104+\begin{code}
121−
122class Eq a where
105class Eq a where
123 (==) : a -> a -> Bool
106 (==) : a -> a -> Bool
124 (/=) : a -> a -> Bool
107 (/=) : a -> a -> Bool
125
108
126 x /= y = not (x == y)
109 x /= y = not (x == y)
127 y == y = not (x /= y)
110 y == y = not (x /= y)
128−
111+\end{code}
129−\end{SaveVerbatim}
130−\useverb{eqdefault}
131
112
132\noindent
113\noindent
133A minimal complete definition of an \texttt{Eq} instance requires either \texttt{==}
114A minimal complete definition of an \texttt{Eq} instance requires either \texttt{==}
@@ -140,15 +121,11 @@ Classes can also be extended. A logical next step from an equality relation \tex
140is to define an ordering relation \texttt{Ord}. We can define an \texttt{Ord} class
121is to define an ordering relation \texttt{Ord}. We can define an \texttt{Ord} class
141which inherits methods from \texttt{Eq} as well as defining some of its own:
122which inherits methods from \texttt{Eq} as well as defining some of its own:
142
123
143−\begin{SaveVerbatim}{ord}
124+\begin{code}
144−
145data Ordering = LT | EQ | GT
125data Ordering = LT | EQ | GT
126+\end{code}
146
127
147−\end{SaveVerbatim}
128+\begin{code}
148−\useverb{ord}
149−
150−\begin{SaveVerbatim}{eqord}
151−
152class Eq a => Ord a where
129class Eq a => Ord a where
153 compare : a -> a -> Ordering
130 compare : a -> a -> Ordering
154
131
@@ -158,9 +135,7 @@ class Eq a => Ord a where
158 (>=) : a -> a -> Bool
135 (>=) : a -> a -> Bool
159 max : a -> a -> a
136 max : a -> a -> a
160 min : a -> a -> a
137 min : a -> a -> a
161−
138+\end{code}
162−\end{SaveVerbatim}
163−\useverb{eqord}
164
139
165\noindent
140\noindent
166The \texttt{Ord} class allows us to compare two values and determine their ordering.
141The \texttt{Ord} class allows us to compare two values and determine their ordering.
@@ -171,24 +146,18 @@ increasing order, provided that the element type of the list is in the \texttt{O
171We give the constraints on the type variables left of the fat arrow \texttt{=>}, and the
146We give the constraints on the type variables left of the fat arrow \texttt{=>}, and the
172function type to the right of the fat arrow:
147function type to the right of the fat arrow:
173
148
174−\begin{SaveVerbatim}{sortty}
149+\begin{code}
175−
176sort : Ord a => List a -> List a
150sort : Ord a => List a -> List a
177−
151+\end{code}
178−\end{SaveVerbatim}
179−\useverb{sortty}
180
152
181\noindent
153\noindent
182Functions, classes and instances can have multiple constraints. Multiple constaints are
154Functions, classes and instances can have multiple constraints. Multiple constaints are
183written in brackets in a comma separated list, for example:
155written in brackets in a comma separated list, for example:
184
156
185−\begin{SaveVerbatim}{sortshow}
157+\begin{code}
186−
187sortAndShow : (Ord a, Show a) => List a -> String
158sortAndShow : (Ord a, Show a) => List a -> String
188sortAndShow xs = show (sort xs)
159sortAndShow xs = show (sort xs)
189−
160+\end{code}
190−\end{SaveVerbatim}
191−\useverb{sortshow}
192
161
193\subsection{Monads and \texttt{do}-notation}
162\subsection{Monads and \texttt{do}-notation}
194
163
@@ -200,14 +169,11 @@ and the parameters can have \remph{any} type.
200If the type of the parameter is not \texttt{Type}, we need to give an explicit type
169If the type of the parameter is not \texttt{Type}, we need to give an explicit type
201declaration. For example:
170declaration. For example:
202
171
203−\begin{SaveVerbatim}{monad}
172+\begin{code}
204−
205class Monad (m : Type -> Type) where
173class Monad (m : Type -> Type) where
206 return : a -> m a
174 return : a -> m a
207 (>>=) : m a -> (a -> m b) -> m b
175 (>>=) : m a -> (a -> m b) -> m b
208−
176+\end{code}
209−\end{SaveVerbatim}
210−\useverb{monad}
211
177
212\noindent
178\noindent
213The \texttt{Monad} class allows us to encapsulate binding and computation, and is the
179The \texttt{Monad} class allows us to encapsulate binding and computation, and is the
@@ -224,30 +190,24 @@ basis of \texttt{do}-notation introduced in Section \ref{sect:do}. Inside a
224\texttt{IO} is an instance of \texttt{Monad}, defined using primitive functions.
190\texttt{IO} is an instance of \texttt{Monad}, defined using primitive functions.
225We can also define an instance for \texttt{Maybe}, as follows:
191We can also define an instance for \texttt{Maybe}, as follows:
226
192
227−\begin{SaveVerbatim}{maybemonad}
193+\begin{code}
228−
229instance Monad Maybe where
194instance Monad Maybe where
230 return = Just
195 return = Just
231
196
232 Nothing >>= k = Nothing
197 Nothing >>= k = Nothing
233 (Just x) >>= k = k x
198 (Just x) >>= k = k x
234−
199+\end{code}
235−\end{SaveVerbatim}
236−\useverb{maybemonad}
237
200
238\noindent
201\noindent
239Using this we can, for example, define a function which adds two
202Using this we can, for example, define a function which adds two
240\texttt{Maybe Int}s, using the monad to encapsulate the error handling:
203\texttt{Maybe Int}s, using the monad to encapsulate the error handling:
241
204
242−\begin{SaveVerbatim}{maybeadd}
205+\begin{code}
243−
244m_add : Maybe Int -> Maybe Int -> Maybe Int
206m_add : Maybe Int -> Maybe Int -> Maybe Int
245m_add x y = do x' <- x -- Extract value from x
207m_add x y = do x' <- x -- Extract value from x
246 y' <- y -- Extract value from y
208 y' <- y -- Extract value from y
247 return (x' + y') -- Add them
209 return (x' + y') -- Add them
248−
210+\end{code}
249−\end{SaveVerbatim}
250−\useverb{maybeadd}
251
211
252\noindent
212\noindent
253This function will extract the values from \texttt{x} and \texttt{y}, if they
213This function will extract the values from \texttt{x} and \texttt{y}, if they
@@ -255,29 +215,23 @@ are available, or return \texttt{Nothing} if they are not. Managing the
255\texttt{Nothing} cases is achieved by the \texttt{>>=} operator, hidden by the
215\texttt{Nothing} cases is achieved by the \texttt{>>=} operator, hidden by the
256\texttt{do} notation.
216\texttt{do} notation.
257
217
258−\begin{SaveVerbatim}{maybeaddt}
218+\begin{lstlisting}
259−
260*classes> m_add (Just 20) (Just 22)
219*classes> m_add (Just 20) (Just 22)
261Just 42 : Maybe Int
220Just 42 : Maybe Int
262*classes> m_add (Just 20) Nothing
221*classes> m_add (Just 20) Nothing
263Nothing : Maybe Int
222Nothing : Maybe Int
264−
223+\end{lstlisting}
265−\end{SaveVerbatim}
266−\useverb{maybeaddt}
267
224
268\subsubsection*{Monad comprehensions}
225\subsubsection*{Monad comprehensions}
269
226
270The list comprehension notation we saw in Section \ref{sec:listcomp} is more
227The list comprehension notation we saw in Section \ref{sec:listcomp} is more
271general, and applies to anything which is an instance of \texttt{MonadPlus}:
228general, and applies to anything which is an instance of \texttt{MonadPlus}:
272
229
273−\begin{SaveVerbatim}{monadplus}
230+\begin{code}
274−
275class Monad m => MonadPlus (m : Type -> Type) where
231class Monad m => MonadPlus (m : Type -> Type) where
276 mplus : m a -> m a -> m a
232 mplus : m a -> m a -> m a
277 mzero : m a
233 mzero : m a
278−
234+\end{code}
279−\end{SaveVerbatim}
280−\useverb{monadplus}
281
235
282\noindent
236\noindent
283In general, a comprehension takes the form \texttt{[ exp | qual1, qual2, ..., qualn ]} where
237In general, a comprehension takes the form \texttt{[ exp | qual1, qual2, ..., qualn ]} where
@@ -295,32 +249,24 @@ any qualifier
295\texttt{qual} which is a \emph{guard} is translated to \texttt{guard qual}, using
249\texttt{qual} which is a \emph{guard} is translated to \texttt{guard qual}, using
296the following function:
250the following function:
297
251
298−\begin{SaveVerbatim}{guardq}
252+\begin{code}
299−
300guard : MonadPlus m => Bool -> m ()
253guard : MonadPlus m => Bool -> m ()
301−
254+\end{code}
302−\end{SaveVerbatim}
303−\useverb{guardq}
304
255
305\noindent
256\noindent
306Then the comprehension is converted to \texttt{do} notation:
257Then the comprehension is converted to \texttt{do} notation:
307
258
308−\begin{SaveVerbatim}{comptrans}
259+\begin{code}
309−
310do { qual1; qual2; ...; qualn; return exp; }
260do { qual1; qual2; ...; qualn; return exp; }
311−
261+\end{code}
312−\end{SaveVerbatim}
313−\useverb{comptrans}
314
262
315\noindent
263\noindent
316Using monad comprehensions, an alternative definition for \texttt{m\_add} would be:
264Using monad comprehensions, an alternative definition for \texttt{m\_add} would be:
317
265
318−\begin{SaveVerbatim}{maddb}
266+\begin{code}
319−
320m_add : Maybe Int -> Maybe Int -> Maybe Int
267m_add : Maybe Int -> Maybe Int -> Maybe Int
321m_add x y = [ x' + y' | x' <- x, y' <- y ]
268m_add x y = [ x' + y' | x' <- x, y' <- y ]
322−\end{SaveVerbatim}
269+\end{code}
323−\useverb{maddb}
324
270
325\subsection{Idiom brackets}
271\subsection{Idiom brackets}
326
272
@@ -333,26 +279,20 @@ First, let us revisit \texttt{m\_add} above. All it is really doing is applying
333an operator to two values extracted from Maybe Ints. We could abstract out the
279an operator to two values extracted from Maybe Ints. We could abstract out the
334application:
280application:
335
281
336−\begin{SaveVerbatim}{mapp}
282+\begin{code}
337−
338m_app : Maybe (a -> b) -> Maybe a -> Maybe b
283m_app : Maybe (a -> b) -> Maybe a -> Maybe b
339m_app (Just f) (Just a) = Just (f a)
284m_app (Just f) (Just a) = Just (f a)
340m_app _ _ = Nothing
285m_app _ _ = Nothing
341−
286+\end{code}
342−\end{SaveVerbatim}
343−\useverb{mapp}
344
287
345\noindent
288\noindent
346Using this, we can write an alternative \texttt{m\_add} which uses this alternative
289Using this, we can write an alternative \texttt{m\_add} which uses this alternative
347notion of function application, with explicit calls to \texttt{m\_app}:
290notion of function application, with explicit calls to \texttt{m\_app}:
348
291
349−\begin{SaveVerbatim}{maddb}
292+\begin{code}
350−
351m_add' : Maybe Int -> Maybe Int -> Maybe Int
293m_add' : Maybe Int -> Maybe Int -> Maybe Int
352m_add' x y = m_app (m_app (Just (+)) x) y
294m_add' x y = m_app (m_app (Just (+)) x) y
353−
295+\end{code}
354−\end{SaveVerbatim}
355−\useverb{maddb}
356
296
357\noindent
297\noindent
358Rather than having to insert \texttt{m\_app} everywhere there is an
298Rather than having to insert \texttt{m\_app} everywhere there is an
@@ -360,44 +300,35 @@ application, we can use \remph{idiom brackets} to do the job for us. To do
360this, we use the \texttt{Applicative} class, which captures the notion of
300this, we use the \texttt{Applicative} class, which captures the notion of
361application for a data type:
301application for a data type:
362
302
363−\begin{SaveVerbatim}{applicative}
303+\begin{code}
364−
365infixl 2 <$>
304infixl 2 <$>
366
305
367class Applicative (f : Type -> Type) where
306class Applicative (f : Type -> Type) where
368 pure : a -> f a
307 pure : a -> f a
369 (<$>) : f (a -> b) -> f a -> f b
308 (<$>) : f (a -> b) -> f a -> f b
370−
309+\end{code}
371−\end{SaveVerbatim}
372−\useverb{applicative}
373
310
374\noindent
311\noindent
375\texttt{Maybe} is made an instance of \texttt{Applicative} as follows, where
312\texttt{Maybe} is made an instance of \texttt{Applicative} as follows, where
376\texttt{<\$>} is defined in the same way as \texttt{m\_app} above:
313\texttt{<\$>} is defined in the same way as \texttt{m\_app} above:
377
314
378−\begin{SaveVerbatim}{maybeapp}
315+\begin{code}
379−
380instance Applicative Maybe where
316instance Applicative Maybe where
381 pure = Just
317 pure = Just
382
318
383 (Just f) <$> (Just a) = Just (f a)
319 (Just f) <$> (Just a) = Just (f a)
384 _ <$> _ = Nothing
320 _ <$> _ = Nothing
385−
321+\end{code}
386−\end{SaveVerbatim}
387−\useverb{maybeapp}
388
322
389\noindent
323\noindent
390Using \remph{idiom brackets} we can use this instance as follows, where a function
324Using \remph{idiom brackets} we can use this instance as follows, where a function
391application \texttt{[| f a1 ... an |]}
325application \texttt{[| f a1 ... an |]}
392is translated into \texttt{pure f <\$> a1 <\$> ... <\$> an}:
326is translated into \texttt{pure f <\$> a1 <\$> ... <\$> an}:
393
327
394−\begin{SaveVerbatim}{maddc}
328+\begin{code}
395−
396m_add' : Maybe Int -> Maybe Int -> Maybe Int
329m_add' : Maybe Int -> Maybe Int -> Maybe Int
397m_add' x y = [| x + y |]
330m_add' x y = [| x + y |]
398−
331+\end{code}
399−\end{SaveVerbatim}
400−\useverb{maddc}
401
332
402\subsubsection{An error-handling interpreter}
333\subsubsection{An error-handling interpreter}
403
334
@@ -405,43 +336,34 @@ Idiom notation is commonly useful when defining evaluators. McBride and
405Paterson describe such an evaluator~\cite{idioms}, for a language similar to
336Paterson describe such an evaluator~\cite{idioms}, for a language similar to
406the following:
337the following:
407
338
408−\begin{SaveVerbatim}{idiomexpr}
339+\begin{code}
409−
410data Expr = Var String -- variables
340data Expr = Var String -- variables
411 | Val Int -- values
341 | Val Int -- values
412 | Add Expr Expr -- addition
342 | Add Expr Expr -- addition
413−
343+\end{code}
414−\end{SaveVerbatim}
415−\useverb{idiomexpr}
416
344
417\noindent
345\noindent
418Evaluation will take place relative to a context mapping variables (represented as
346Evaluation will take place relative to a context mapping variables (represented as
419\texttt{String}s) to integer values, and can possibly fail. We define a data type
347\texttt{String}s) to integer values, and can possibly fail. We define a data type
420\texttt{Eval} to wrap an evaluator:
348\texttt{Eval} to wrap an evaluator:
421
349
422−\begin{SaveVerbatim}{evalctxt}
350+\begin{code}
423−
424data Eval : Type -> Type where
351data Eval : Type -> Type where
425 MkEval : (List (String, Int) -> Maybe a) -> Eval a
352 MkEval : (List (String, Int) -> Maybe a) -> Eval a
426−
353+\end{code}
427−\end{SaveVerbatim}
428−\useverb{evalctxt}
429
354
430\noindent
355\noindent
431Wrapping the evaluator in a data type means we will be able to make it an instance
356Wrapping the evaluator in a data type means we will be able to make it an instance
432of a type class later. We begin by defining a function to retrieve values from
357of a type class later. We begin by defining a function to retrieve values from
433the context during evaluation:
358the context during evaluation:
434
359
435−\begin{SaveVerbatim}{fetch}
360+\begin{code}
436−
437fetch : String -> Eval Int
361fetch : String -> Eval Int
438fetch x = MkEval (\e => fetchVal e) where
362fetch x = MkEval (\e => fetchVal e) where
439 fetchVal : List (String, Int) -> Maybe Int
363 fetchVal : List (String, Int) -> Maybe Int
440 fetchVal [] = Nothing
364 fetchVal [] = Nothing
441 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
365 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
442−
366+\end{code}
443−\end{SaveVerbatim}
444−\useverb{fetch}
445
367
446\noindent
368\noindent
447When defining an evaluator for the language, we will be applying functions in
369When defining an evaluator for the language, we will be applying functions in
@@ -451,8 +373,7 @@ Before \texttt{Eval} can be an instance of
451\texttt{Applicative} it is necessary to make \texttt{Eval} an instance of
373\texttt{Applicative} it is necessary to make \texttt{Eval} an instance of
452\texttt{Functor}:
374\texttt{Functor}:
453
375
454−\begin{SaveVerbatim}{}
376+\begin{code}
455−
456instance Functor Eval where
377instance Functor Eval where
457 fmap f (MkEval g) = MkEval (\e => fmap f (g e))
378 fmap f (MkEval g) = MkEval (\e => fmap f (g e))
458
379
@@ -463,20 +384,13 @@ instance Applicative Eval where
463 app : Maybe (a -> b) -> Maybe a -> Maybe b
384 app : Maybe (a -> b) -> Maybe a -> Maybe b
464 app (Just fx) (Just gx) = Just (fx gx)
385 app (Just fx) (Just gx) = Just (fx gx)
465 app _ _ = Nothing
386 app _ _ = Nothing
466−
387+\end{code}
467−\end{SaveVerbatim}
468−\useverb{}
469−
470−\begin{SaveVerbatim}{grr}
471−<$>
472−\end{SaveVerbatim}
473
388
474\noindent
389\noindent
475Evaluating an expression can now make use of the idiomatic application to handle
390Evaluating an expression can now make use of the idiomatic application to handle
476errors:
391errors:
477
392
478−\begin{SaveVerbatim}{evalexpr}
393+\begin{code}
479−
480eval : Expr -> Eval Int
394eval : Expr -> Eval Int
481eval (Var x) = fetch x
395eval (Var x) = fetch x
482eval (Val x) = [| x |]
396eval (Val x) = [| x |]
@@ -485,9 +399,7 @@ eval (Add x y) = [| eval x + eval y |]
485runEval : List (String, Int) -> Expr -> Maybe Int
399runEval : List (String, Int) -> Expr -> Maybe Int
486runEval env e = case eval e of
400runEval env e = case eval e of
487 MkEval envFn => envFn env
401 MkEval envFn => envFn env
488−
402+\end{code}
489−\end{SaveVerbatim}
490−\useverb{evalexpr}
491
403
492\subsection{Named Instances}
404\subsection{Named Instances}
493
405
@@ -495,16 +407,13 @@ It can be desirable to have multiple instances of a type class, for example to p
495alternative methods for sorting or printing values. To achieve this, instances can
407alternative methods for sorting or printing values. To achieve this, instances can
496be \remph{named} as follows:
408be \remph{named} as follows:
497
409
498−\begin{SaveVerbatim}{myord}
410+\begin{code}
499−
500instance [myord] Ord Nat where
411instance [myord] Ord Nat where
501 compare Z (S n) = GT
412 compare Z (S n) = GT
502 compare (S n) Z = LT
413 compare (S n) Z = LT
503 compare Z Z = EQ
414 compare Z Z = EQ
504 compare (S x) (S y) = compare @{myord} x y
415 compare (S x) (S y) = compare @{myord} x y
505−
416+\end{code}
506−\end{SaveVerbatim}
507−\useverb{myord}
508
417
509\noindent
418\noindent
510This declares an instance as normal, but with an explicit name, \texttt{myord}.
419This declares an instance as normal, but with an explicit name, \texttt{myord}.
@@ -513,25 +422,19 @@ The syntax \texttt{compare @\{myord\}} gives an explicit instance to
513We can use this, for example, to sort a list of \texttt{Nat}s in reverse.
422We can use this, for example, to sort a list of \texttt{Nat}s in reverse.
514Given the following list:
423Given the following list:
515
424
516−\begin{SaveVerbatim}{myordlist}
425+\begin{code}
517−
518testList : List Nat
426testList : List Nat
519testList = [3,4,1]
427testList = [3,4,1]
520−
428+\end{code}
521−\end{SaveVerbatim}
522−\useverb{myordlist}
523
429
524\noindent
430\noindent
525\ldots we can sort it using the default \texttt{Ord} instance, then the named
431\ldots we can sort it using the default \texttt{Ord} instance, then the named
526instance \texttt{myord} as follows, at the \Idris{} prompt:
432instance \texttt{myord} as follows, at the \Idris{} prompt:
527
433
528−\begin{SaveVerbatim}{myordlistrun}
434+\begin{lstlisting}
529−
530*named_instance> show (sort testList)
435*named_instance> show (sort testList)
531"[sO, sssO, ssssO]" : String
436"[sO, sssO, ssssO]" : String
532*named_instance> show (sort @{myord} testList)
437*named_instance> show (sort @{myord} testList)
533"[ssssO, sssO, sO]" : String
438"[ssssO, sssO, sO]" : String
534−
439+\end{lstlisting}
535−\end{SaveVerbatim}
536−\useverb{myordlistrun}
537
440
tutorial/conclusions.tex → tutorial/content/conclusions.texrenamed

The content is the same.

tutorial/dsl.tex → tutorial/content/dsl.texrenamed+16−26
@@ -11,23 +11,25 @@ running concurrent processes safely~\cite{cbconc-fi}.
11Unfortunately, the form of object language programs makes it rather hard to program
11Unfortunately, the form of object language programs makes it rather hard to program
12this way in practice. Recall the factorial program in \texttt{Expr} for example:
12this way in practice. Recall the factorial program in \texttt{Expr} for example:
13
13
14−\useverb{facttest}
14+\begin{code}
15+fact : Expr G (TyFun TyInt TyInt)
16+fact = Lam (If (Op (==) (Var stop) (Val 0))
17+ (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1)))
18+ (Var stop)))
19+\end{code}
15
20
16\noindent
21\noindent
17Since this is a particularly useful pattern, \Idris{} provides syntax
22Since this is a particularly useful pattern, \Idris{} provides syntax
18overloading~\cite{res-dsl-padl12} to make it easier to program in such
23overloading~\cite{res-dsl-padl12} to make it easier to program in such
19object languages:
24object languages:
20
25
21−\begin{SaveVerbatim}{exprdsl}
26+\begin{code}
22−
23dsl expr
27dsl expr
24 lambda = Lam
28 lambda = Lam
25 variable = Var
29 variable = Var
26 index_first = stop
30 index_first = stop
27 index_next = pop
31 index_next = pop
28−
32+\end{code}
29−\end{SaveVerbatim}
30−\useverb{exprdsl}
31
33
32\noindent
34\noindent
33A \texttt{dsl} block describes how each syntactic construct is represented in an
35A \texttt{dsl} block describes how each syntactic construct is represented in an
@@ -38,55 +40,43 @@ de Bruijn index (i.e., to count how many bindings since the variable itself was
38It is also possible to overload \texttt{let} in this way. We can now write \texttt{fact}
40It is also possible to overload \texttt{let} in this way. We can now write \texttt{fact}
39as follows:
41as follows:
40
42
41−\begin{SaveVerbatim}{factb}
43+\begin{code}
42−
43fact : Expr G (TyFun TyInt TyInt)
44fact : Expr G (TyFun TyInt TyInt)
44fact = expr (\x => If (Op (==) x (Val 0))
45fact = expr (\x => If (Op (==) x (Val 0))
45 (Val 1) (Op (*) (app fact (Op (-) x (Val 1))) x))
46 (Val 1) (Op (*) (app fact (Op (-) x (Val 1))) x))
46−
47+\end{code}
47−\end{SaveVerbatim}
48−\useverb{factb}
49
48
50\noindent
49\noindent
51In this new version, \texttt{expr} declares that the next expression will be overloaded.
50In this new version, \texttt{expr} declares that the next expression will be overloaded.
52We can take this further, using idiom brackets, by declaring:
51We can take this further, using idiom brackets, by declaring:
53
52
54−\begin{SaveVerbatim}{idiomexpr}
53+\begin{code}
55−
56(<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
54(<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
57(<$>) = \f, a => App f a
55(<$>) = \f, a => App f a
58
56
59pure : Expr G a -> Expr G a
57pure : Expr G a -> Expr G a
60pure = id
58pure = id
61−
59+\end{code}
62−\end{SaveVerbatim}
63−\useverb{idiomexpr}
64
60
65\noindent
61\noindent
66Note that there is no need for these to be part of an instance of \texttt{Applicative},
62Note that there is no need for these to be part of an instance of \texttt{Applicative},
67since idiom bracket notation translates directly to the names \texttt{<\$>} and
63since idiom bracket notation translates directly to the names \texttt{<\$>} and
68\texttt{pure}, and ad-hoc type-directed overloading is allowed. We can now say:
64\texttt{pure}, and ad-hoc type-directed overloading is allowed. We can now say:
69
65
70−\begin{SaveVerbatim}{factc}
66+\begin{code}
71−
72fact : Expr G (TyFun TyInt TyInt)
67fact : Expr G (TyFun TyInt TyInt)
73fact = expr (\x => If (Op (==) x (Val 0))
68fact = expr (\x => If (Op (==) x (Val 0))
74 (Val 1) (Op (*) [| fact (Op (-) x (Val 1)) |] x))
69 (Val 1) (Op (*) [| fact (Op (-) x (Val 1)) |] x))
75−
70+\end{code}
76−\end{SaveVerbatim}
77−\useverb{factc}
78
71
79\noindent
72\noindent
80With some more ad-hoc overloading and type class instances, and a new
73With some more ad-hoc overloading and type class instances, and a new
81syntax rule, we can even go as far as:
74syntax rule, we can even go as far as:
82
75
83−\begin{SaveVerbatim}{factd}
76+\begin{code}
84−
85syntax IF [x] THEN [t] ELSE [e] = If x t e
77syntax IF [x] THEN [t] ELSE [e] = If x t e
86
78
87fact : Expr G (TyFun TyInt TyInt)
79fact : Expr G (TyFun TyInt TyInt)
88fact = expr (\x => IF x == 0 THEN 1 ELSE [| fact (x - 1) |] * x)
80fact = expr (\x => IF x == 0 THEN 1 ELSE [| fact (x - 1) |] * x)
89−
81+\end{code}
90−\end{SaveVerbatim}
91−\useverb{factd}
92
82
tutorial/interp.tex → tutorial/content/interp.texrenamed+61−143
@@ -1,5 +1,4 @@
1\section{Example: The Well-Typed Interpreter}
1\section{Example: The Well-Typed Interpreter}
2−
3\label{sect:interp}
2\label{sect:interp}
4
3
5In this section, we'll use the features we've seen so far to write a larger
4In this section, we'll use the features we've seen so far to write a larger
@@ -9,27 +8,21 @@ construct. We will use the dependent type system to ensure that any programs
9which can be represented are well-typed. First, let us define the types in the
8which can be represented are well-typed. First, let us define the types in the
10language. We have integers, booleans, and functions, represented by \texttt{Ty}:
9language. We have integers, booleans, and functions, represented by \texttt{Ty}:
11
10
12−\begin{SaveVerbatim}{tydecl}
11+\begin{code}
13−
14data Ty = TyInt | TyBool | TyFun Ty Ty
12data Ty = TyInt | TyBool | TyFun Ty Ty
15−
13+\end{code}
16−\end{SaveVerbatim}
17−\useverb{tydecl}
18
14
19\noindent
15\noindent
20We can write a function to translate these representations to a concrete \Idris{}
16We can write a function to translate these representations to a concrete \Idris{}
21type --- remember that types are first class, so can be calculated just like
17type --- remember that types are first class, so can be calculated just like
22any other value:
18any other value:
23
19
24−\begin{SaveVerbatim}{interpty}
20+\begin{code}
25−
26interpTy : Ty -> Type
21interpTy : Ty -> Type
27interpTy TyInt = Int
22interpTy TyInt = Int
28interpTy TyBool = Bool
23interpTy TyBool = Bool
29interpTy (TyFun A T) = interpTy A -> interpTy T
24interpTy (TyFun A T) = interpTy A -> interpTy T
30−
25+\end{code}
31−\end{SaveVerbatim}
32−\useverb{interpty}
33
26
34\noindent
27\noindent
35We're going to define a representation of our language in such a way that only
28We're going to define a representation of our language in such a way that only
@@ -38,31 +31,24 @@ expressions by their type and the types of local variables (the context), which
38we'll be using regularly as an implicit argument, so we define everything
31we'll be using regularly as an implicit argument, so we define everything
39in a \texttt{using} block:
32in a \texttt{using} block:
40
33
41−\begin{SaveVerbatim}{usingg}
34+\begin{code}
42−
43using (G:Vect n Ty)
35using (G:Vect n Ty)
44−
36+\end{code}
45−\end{SaveVerbatim}
46−\useverb{usingg}
47
37
48\noindent
38\noindent
49The full representation of expressions is given in Figure \ref{exprty}. They are
39The full representation of expressions is given in Figure \ref{exprty}. They are
50indexed by the types of the local variables, and the type of the expression itself:
40indexed by the types of the local variables, and the type of the expression itself:
51
41
52−\begin{SaveVerbatim}{exprdecl}
42+\begin{code}
53−
54data Expr : Vect n Ty -> Ty -> Type
43data Expr : Vect n Ty -> Ty -> Type
55−
44+\end{code}
56−\end{SaveVerbatim}
57−\useverb{exprdecl}
58
45
59\noindent
46\noindent
60Since expressions are indexed by their type, we can read the typing rules of
47Since expressions are indexed by their type, we can read the typing rules of
61the language from the definitions of the constructors. Let us look at each
48the language from the definitions of the constructors. Let us look at each
62constructor in turn.
49constructor in turn.
63
50
64−\begin{SaveVerbatim}{exprty}
51+\begin{code}[caption={Expression representation},label=exprty]
65−
66data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
52data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
67 stop : HasType fZ (t :: G) t
53 stop : HasType fZ (t :: G) t
68 pop : HasType k G t -> HasType (fS k) (u :: G) t
54 pop : HasType k G t -> HasType (fS k) (u :: G) t
@@ -75,9 +61,7 @@ data Expr : Vect n Ty -> Ty -> Type where
75 Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
61 Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
76 Expr G c
62 Expr G c
77 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
63 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
78−
64+\end{code}
79−\end{SaveVerbatim}
80−\codefig{exprty}{Expression representation}
81
65
82\noindent
66\noindent
83We use a nameless representation for variables --- they are \emph{de Bruijn indexed}.
67We use a nameless representation for variables --- they are \emph{de Bruijn indexed}.
@@ -85,14 +69,11 @@ Variables are represented by a proof of their membership in the context,
85\texttt{HasType i G T}, which is a proof that variable \texttt{i} in context
69\texttt{HasType i G T}, which is a proof that variable \texttt{i} in context
86\texttt{G} has type \texttt{T}. This is defined as follows:
70\texttt{G} has type \texttt{T}. This is defined as follows:
87
71
88−\begin{SaveVerbatim}{hastype}
72+\begin{code}
89−
90data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
73data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
91 stop : HasType fZ (t :: G) t
74 stop : HasType fZ (t :: G) t
92 pop : HasType k G t -> HasType (fS k) (u :: G) t
75 pop : HasType k G t -> HasType (fS k) (u :: G) t
93−
76+\end{code}
94−\end{SaveVerbatim}
95−\useverb{hastype}
96
77
97\noindent
78\noindent
98We can treat \remph{stop} as a proof that the most recently defined variable is well-typed,
79We can treat \remph{stop} as a proof that the most recently defined variable is well-typed,
@@ -101,12 +82,9 @@ well-typed, so is the \texttt{n+1}th. In practice, this means we use \texttt{sto
101refer to the most recently defined variable, \texttt{pop stop} to refer to the next, and so on,
82refer to the most recently defined variable, \texttt{pop stop} to refer to the next, and so on,
102via the \texttt{Var} constructor:
83via the \texttt{Var} constructor:
103
84
104−\begin{SaveVerbatim}{varcon}
85+\begin{code}
105−
106Var : HasType i G t -> Expr G t
86Var : HasType i G t -> Expr G t
107−
87+\end{code}
108−\end{SaveVerbatim}
109−\useverb{varcon}
110
88
111\noindent
89\noindent
112So, in an expression \texttt{$\backslash$x. $\backslash$y. x y},
90So, in an expression \texttt{$\backslash$x. $\backslash$y. x y},
@@ -118,58 +96,43 @@ definition and the use.
118\noindent
96\noindent
119A value carries a concrete representation of an integer:
97A value carries a concrete representation of an integer:
120
98
121−\begin{SaveVerbatim}{valcon}
99+\begin{code}
122−
123Val : (x : Int) -> Expr G TyInt
100Val : (x : Int) -> Expr G TyInt
124−
101+\end{code}
125−\end{SaveVerbatim}
126−\useverb{valcon}
127
102
128\noindent
103\noindent
129A lambda creates a function. In the scope of a function of type \texttt{a -> t}, there is
104A lambda creates a function. In the scope of a function of type \texttt{a -> t}, there is
130a new local variable of type \texttt{a}, which is expressed by the context index:
105a new local variable of type \texttt{a}, which is expressed by the context index:
131
106
132−\begin{SaveVerbatim}{lamcon}
107+\begin{code}
133−
134Lam : Expr (a :: G) t -> Expr G (TyFun a t)
108Lam : Expr (a :: G) t -> Expr G (TyFun a t)
135−
109+\end{code}
136−\end{SaveVerbatim}
137−\useverb{lamcon}
138
110
139\noindent
111\noindent
140Function application produces a value of type \texttt{t} given a function from
112Function application produces a value of type \texttt{t} given a function from
141\texttt{a} to \texttt{t}
113\texttt{a} to \texttt{t}
142and a value of type \texttt{a}:
114and a value of type \texttt{a}:
143
115
144−\begin{SaveVerbatim}{appcon}
116+\begin{code}
145−
146App : Expr G (TyFun a t) -> Expr G a -> Expr G t
117App : Expr G (TyFun a t) -> Expr G a -> Expr G t
147−
118+\end{code}
148−\end{SaveVerbatim}
149−\useverb{appcon}
150
119
151\noindent
120\noindent
152We allow arbitrary binary operators, where the type of the operator
121We allow arbitrary binary operators, where the type of the operator
153informs what the types of the arguments must be:
122informs what the types of the arguments must be:
154
123
155−\begin{SaveVerbatim}{opcon}
124+\begin{code}
156−
157Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
125Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
158 Expr G c
126 Expr G c
159−
127+\end{code}
160−\end{SaveVerbatim}
161−\useverb{opcon}
162
128
163\noindent
129\noindent
164Finally, if expressions make a choice given a boolean. Each branch must
130Finally, if expressions make a choice given a boolean. Each branch must
165have the same type:
131have the same type:
166
132
167−\begin{SaveVerbatim}{ifcon}
133+\begin{code}
168−
169If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
134If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
170−
135+\end{code}
171−\end{SaveVerbatim}
172−\useverb{ifcon}
173
136
174\noindent
137\noindent
175When we evaluate an \texttt{Expr}, we'll need to know the values in scope, as well as
138When we evaluate an \texttt{Expr}, we'll need to know the values in scope, as well as
@@ -179,8 +142,7 @@ to the vector of local variable types, we use the usual \texttt{::} and \texttt{
179constructors so that we can use the usual list syntax. Given a proof that a variable
142constructors so that we can use the usual list syntax. Given a proof that a variable
180is defined in the context, we can then produce a value from the environment:
143is defined in the context, we can then produce a value from the environment:
181
144
182−\begin{SaveVerbatim}{envtype}
145+\begin{code}
183−
184data Env : Vect n Ty -> Type where
146data Env : Vect n Ty -> Type where
185 Nil : Env Nil
147 Nil : Env Nil
186 (::) : interpTy a -> Env G -> Env (a :: G)
148 (::) : interpTy a -> Env G -> Env (a :: G)
@@ -188,12 +150,9 @@ data Env : Vect n Ty -> Type where
188lookup : HasType i G t -> Env G -> interpTy t
150lookup : HasType i G t -> Env G -> interpTy t
189lookup stop (x :: xs) = x
151lookup stop (x :: xs) = x
190lookup (pop k) (x :: xs) = lookup k xs
152lookup (pop k) (x :: xs) = lookup k xs
153+\end{code}
191
154
192−\end{SaveVerbatim}
155+\begin{code}[caption={Intepreter definition},label=interpdef]
193−\useverb{envtype}
194−
195−\begin{SaveVerbatim}{interpdef}
196−
197interp : Env G -> Expr G t -> interpTy t
156interp : Env G -> Expr G t -> interpTy t
198interp env (Var i) = lookup i env
157interp env (Var i) = lookup i env
199interp env (Val x) = x
158interp env (Val x) = x
@@ -202,65 +161,48 @@ interp env (App f s) = interp env f (interp env s)
202interp env (Op op x y) = op (interp env x) (interp env y)
161interp env (Op op x y) = op (interp env x) (interp env y)
203interp env (If x t e) = if interp env x then interp env t
162interp env (If x t e) = if interp env x then interp env t
204 else interp env e
163 else interp env e
205−
164+\end{code}
206−\end{SaveVerbatim}
207−\codefig{interpdef}{Intepreter definition}
208
165
209\noindent
166\noindent
210Given this, an interpreter (Figure \ref{interpdef})
167Given this, an interpreter (Figure \ref{interpdef})
211is a function which translates an \texttt{Expr} into a
168is a function which translates an \texttt{Expr} into a
212concrete \Idris{} value with respect to a specific environment:
169concrete \Idris{} value with respect to a specific environment:
213
170
214−\begin{SaveVerbatim}{interpty}
171+\begin{code}
215−
216interp : Env G -> Expr G t -> interpTy t
172interp : Env G -> Expr G t -> interpTy t
217−
173+\end{code}
218−\end{SaveVerbatim}
219−\useverb{interpty}
220
174
221\noindent
175\noindent
222To translate a variable, we simply look it up in the environment:
176To translate a variable, we simply look it up in the environment:
223
177
224−\begin{SaveVerbatim}{varinterp}
178+\begin{code}
225−
226interp env (Var i) = lookup i env
179interp env (Var i) = lookup i env
227−
180+\end{code}
228−\end{SaveVerbatim}
229−\useverb{varinterp}
230
181
231\noindent
182\noindent
232To translate a value, we just return the concrete representation of the value:
183To translate a value, we just return the concrete representation of the value:
233
184
234−\begin{SaveVerbatim}{valinterp}
185+\begin{code}
235−
236interp env (Val x) = x
186interp env (Val x) = x
237−
187+\end{code}
238−\end{SaveVerbatim}
239−\useverb{valinterp}
240
188
241\noindent
189\noindent
242Lambdas are more interesting. In this case, we construct a function which
190Lambdas are more interesting. In this case, we construct a function which
243interprets the scope of the lambda with a new value in the environment. So, a
191interprets the scope of the lambda with a new value in the environment. So, a
244function in the object language is translated to an \Idris{} function:
192function in the object language is translated to an \Idris{} function:
245
193
246−\begin{SaveVerbatim}{laminterp}
194+\begin{code}
247−
248interp env (Lam sc) = \x => interp (x :: env) sc
195interp env (Lam sc) = \x => interp (x :: env) sc
249−
196+\end{code}
250−\end{SaveVerbatim}
251−\useverb{laminterp}
252
197
253\noindent
198\noindent
254For an application, we interpret the function and its argument and apply it
199For an application, we interpret the function and its argument and apply it
255directly. We know that interpreting \texttt{f} must produce a function, because of its
200directly. We know that interpreting \texttt{f} must produce a function, because of its
256type:
201type:
257
202
258−\begin{SaveVerbatim}{appinterp}
203+\begin{code}
259−
260interp env (App f s) = interp env f (interp env s)
204interp env (App f s) = interp env f (interp env s)
261−
205+\end{code}
262−\end{SaveVerbatim}
263−\useverb{appinterp}
264
206
265\noindent
207\noindent
266Operators and interpreters are, again, direct translations into the equivalent
208Operators and interpreters are, again, direct translations into the equivalent
@@ -268,39 +210,30 @@ Operators and interpreters are, again, direct translations into the equivalent
268and for \texttt{If}, we apply the \Idris{} \texttt{if...then...else} construct
210and for \texttt{If}, we apply the \Idris{} \texttt{if...then...else} construct
269directly.
211directly.
270
212
271−\begin{SaveVerbatim}{opinterp}
213+\begin{code}
272−
273interp env (Op op x y) = op (interp env x) (interp env y)
214interp env (Op op x y) = op (interp env x) (interp env y)
274interp env (If x t e) = if interp env x then interp env t
215interp env (If x t e) = if interp env x then interp env t
275 else interp env e
216 else interp env e
276−
217+\end{code}
277−\end{SaveVerbatim}
278−\useverb{opinterp}
279
218
280\noindent
219\noindent
281We can make some simple test functions. Firstly, adding two inputs
220We can make some simple test functions. Firstly, adding two inputs
282\texttt{$\backslash$x. $\backslash$y. y + x} is written as follows:
221\texttt{$\backslash$x. $\backslash$y. y + x} is written as follows:
283
222
284−\begin{SaveVerbatim}{addtest}
223+\begin{code}
285−
286add : Expr G (TyFun TyInt (TyFun TyInt TyInt))
224add : Expr G (TyFun TyInt (TyFun TyInt TyInt))
287add = Lam (Lam (Op (+) (Var stop) (Var (pop stop))))
225add = Lam (Lam (Op (+) (Var stop) (Var (pop stop))))
288−
226+\end{code}
289−\end{SaveVerbatim}
290−\useverb{addtest}
291
227
292\noindent
228\noindent
293More interestingly, we can write a factorial function. First, we write a \emph{lazy}
229More interestingly, we can write a factorial function. First, we write a \emph{lazy}
294version of the \texttt{App} constructor, so that the recursive branch will only
230version of the \texttt{App} constructor, so that the recursive branch will only
295be evaluated if necessary:
231be evaluated if necessary:
296
232
297−\begin{SaveVerbatim}{lazyapp}
233+\begin{code}
298−
299app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
234app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
300app = \f, a => App f a
235app = \f, a => App f a
301−
236+\end{code}
302−\end{SaveVerbatim}
303−\useverb{lazyapp}
304
237
305\noindent
238\noindent
306The vertical bar annotation before the \texttt{f} argument indicates that this
239The vertical bar annotation before the \texttt{f} argument indicates that this
@@ -310,28 +243,22 @@ Then \texttt{fact}
310(i.e. \texttt{$\backslash$x. if (x == 0) then 1 else (fact (x-1) * x)})
243(i.e. \texttt{$\backslash$x. if (x == 0) then 1 else (fact (x-1) * x)})
311is written as follows:
244is written as follows:
312
245
313−\begin{SaveVerbatim}{facttest}
246+\begin{code}
314−
315fact : Expr G (TyFun TyInt TyInt)
247fact : Expr G (TyFun TyInt TyInt)
316fact = Lam (If (Op (==) (Var stop) (Val 0))
248fact = Lam (If (Op (==) (Var stop) (Val 0))
317 (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1)))
249 (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1)))
318 (Var stop)))
250 (Var stop)))
319−
251+\end{code}
320−\end{SaveVerbatim}
321−\useverb{facttest}
322
252
323To finish, we write a \texttt{main} program which interprets the factorial function
253To finish, we write a \texttt{main} program which interprets the factorial function
324on user input:
254on user input:
325
255
326−\begin{SaveVerbatim}{factmain}
256+\begin{code}
327−
328main : IO ()
257main : IO ()
329main = do putStr "Enter a number: "
258main = do putStr "Enter a number: "
330 x <- getLine
259 x <- getLine
331 print (interp [] fact (cast x))
260 print (interp [] fact (cast x))
332−
261+\end{code}
333−\end{SaveVerbatim}
334−\useverb{factmain}
335
262
336\noindent
263\noindent
337Here, \texttt{cast} is an overloaded function which converts a value from one
264Here, \texttt{cast} is an overloaded function which converts a value from one
@@ -339,12 +266,11 @@ type to another if possible. Here, it converts a string to
339an integer, giving 0 if the input is invalid. An example run of this program
266an integer, giving 0 if the input is invalid. An example run of this program
340at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
267at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
341
268
342−\begin{SaveVerbatim}[commandchars=^\{\}]{factrun}
269+\begin{lstlisting}[caption={Running the well-typed interpreter}, label=factrun, escapechar=^]
343−
344$ idris interp.idr
270$ idris interp.idr
345 ____ __ _
271 ____ __ _
346 / _/___/ /____(_)____
272 / _/___/ /____(_)____
347− / // __ / ___/ / ___/ Version ^version{}
273+ / // __ / ___/ / ___/ Version ^\version{}^
348 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
274 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
349 /___/\__,_/_/ /_/____/ Type :? for help
275 /___/\__,_/_/ /_/____/ Type :? for help
350
276
@@ -353,22 +279,17 @@ Type checking ./interp.idr
353Enter a number: 6
279Enter a number: 6
354720
280720
355*interp>
281*interp>
356−
282+\end{lstlisting}
357−\end{SaveVerbatim}
358−\codefig{factrun}{Running the well-typed interpreter}
359
283
360\subsubsection*{Aside: \texttt{cast}}
284\subsubsection*{Aside: \texttt{cast}}
361
285
362The prelude defines a type class \texttt{Cast} which allows conversion between
286The prelude defines a type class \texttt{Cast} which allows conversion between
363types:
287types:
364
288
365−\begin{SaveVerbatim}{castclass}
289+\begin{code}
366−
367class Cast from to where
290class Cast from to where
368 cast : from -> to
291 cast : from -> to
369−
292+\end{code}
370−\end{SaveVerbatim}
371−\useverb{castclass}
372
293
373\noindent
294\noindent
374It is a \emph{multi-parameter} type class, defining the source type and object
295It is a \emph{multi-parameter} type class, defining the source type and object
@@ -381,34 +302,31 @@ they make sense.
381
302
382Recall the \texttt{so} data type:
303Recall the \texttt{so} data type:
383
304
384−\useverb{sotype}
305+\begin{code}
306+data so : Bool -> Type where
307+ oh : so True
308+\end{code}
385
309
386\noindent
310\noindent
387This requires its parameter to be a \texttt{True} value. One simple application of this
311This requires its parameter to be a \texttt{True} value. One simple application of this
388is to perform unit testing of functions at compile time. For example, we know that
312is to perform unit testing of functions at compile time. For example, we know that
389\texttt{4! = 24} so we can set up a test case as follows:
313\texttt{4! = 24} so we can set up a test case as follows:
390
314
391−\begin{SaveVerbatim}{unitTestFac}
315+\begin{code}
392−
393unitTestFac : so (interp [] fact 4 == 24)
316unitTestFac : so (interp [] fact 4 == 24)
394unitTestFac = oh
317unitTestFac = oh
395−
318+\end{code}
396−\end{SaveVerbatim}
397−\useverb{unitTestFac}
398
319
399\noindent
320\noindent
400For the program to compile, the test case must pass. If we change \texttt{24} to \texttt{25},
321For the program to compile, the test case must pass. If we change \texttt{24} to \texttt{25},
401say, we will get an error message like the following:
322say, we will get an error message like the following:
402
323
403−\begin{SaveVerbatim}{unitTestErr}
324+\begin{lstlisting}
404−
405Type checking ./interp.idr
325Type checking ./interp.idr
406interp.idr:64:Can't unify so True with so False
326interp.idr:64:Can't unify so True with so False
407
327
408Specifically:
328Specifically:
409 Can't unify True with False
329 Can't unify True with False
410−
330+\end{lstlisting}
411−\end{SaveVerbatim}
412−\useverb{unitTestErr}
413
331
414
332
tutorial/intro.tex → tutorial/content/intro.texrenamed+2−5
@@ -35,12 +35,9 @@ concatenating two lists has the property that the resulting list's length is
35the sum of the lengths of the two input lists. We can therefore give the following type
35the sum of the lengths of the two input lists. We can therefore give the following type
36to the \texttt{app} function, which concatenates vectors:
36to the \texttt{app} function, which concatenates vectors:
37
37
38−\begin{SaveVerbatim}{appendv}
38+\begin{lstlisting}
39−
40app : Vect n a -> Vect m a -> Vect (n + m) a
39app : Vect n a -> Vect m a -> Vect (n + m) a
41−
40+\end{lstlisting}
42−\end{SaveVerbatim}
43−\useverb{appendv}
44
41
45\noindent
42\noindent
46This tutorial introduces \Idris{}, a general purpose functional
43This tutorial introduces \Idris{}, a general purpose functional
tutorial/miscellany.tex → tutorial/content/miscellany.texrenamed+55−130
@@ -10,7 +10,9 @@ foreign function interface, type providers, code generation and the universe hie
10We 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
11they can be inferred by the type checker, e.g.
11they can be inferred by the type checker, e.g.
12
12
13−\useverb{vindeximpty}
13+\begin{code}
14+index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
15+\end{code}
14
16
15\noindent
17\noindent
16In other situations, it may be possible to infer arguments not by type checking but
18In other situations, it may be possible to infer arguments not by type checking but
@@ -18,17 +20,14 @@ by searching the context for an appropriate value, or constructing a proof. For
18the following definition of \texttt{head} which requires a proof that the list is
20the following definition of \texttt{head} which requires a proof that the list is
19non-empty
21non-empty
20
22
21−\begin{SaveVerbatim}{safehead}
23+\begin{code}
22−
23isCons : List a -> Bool
24isCons : List a -> Bool
24isCons [] = False
25isCons [] = False
25isCons (x :: xs) = True
26isCons (x :: xs) = True
26
27
27head : (xs : List a) -> (isCons xs = True) -> a
28head : (xs : List a) -> (isCons xs = True) -> a
28head (x :: xs) _ = x
29head (x :: xs) _ = x
29−
30+\end{code}
30−\end{SaveVerbatim}
31−\useverb{safehead}
32
31
33\noindent
32\noindent
34If the list is statically known to be non-empty, either because its value is known or
33If the list is statically known to be non-empty, either because its value is known or
@@ -36,13 +35,10 @@ because a proof already exists in the context, the proof can be constructed
36automatically. Auto implicit arguments allow this to happen silently. We define
35automatically. Auto implicit arguments allow this to happen silently. We define
37\texttt{head} as follows:
36\texttt{head} as follows:
38
37
39−\begin{SaveVerbatim}{headauto}
38+\begin{code}
40−
41head : (xs : List a) -> {auto p : isCons xs = True} -> a
39head : (xs : List a) -> {auto p : isCons xs = True} -> a
42head (x :: xs) = x
40head (x :: xs) = x
43−
41+\end{code}
44−\end{SaveVerbatim}
45−\useverb{headauto}
46
42
47\noindent
43\noindent
48The \texttt{auto} annotation on the implicit argument means that \Idris{} will
44The \texttt{auto} annotation on the implicit argument means that \Idris{} will
@@ -52,25 +48,19 @@ if a proof is not found.
52Now when \texttt{head} is applied, the proof can be omitted. In the case that a proof
48Now when \texttt{head} is applied, the proof can be omitted. In the case that a proof
53is not found, it can be provided explicitly as normal:
49is not found, it can be provided explicitly as normal:
54
50
55−\begin{SaveVerbatim}{headapp}
51+\begin{code}
56−
57head xs {p = ?headProof}
52head xs {p = ?headProof}
58−
53+\end{code}
59−\end{SaveVerbatim}
60−\useverb{headapp}
61
54
62\noindent
55\noindent
63More generally, we can fill in implicit arguments with a default value by annotating
56More generally, we can fill in implicit arguments with a default value by annotating
64them with \texttt{default}. The definition above is equivalent to:
57them with \texttt{default}. The definition above is equivalent to:
65
58
66−\begin{SaveVerbatim}{defimp}
59+\begin{code}
67−
68head : (xs : List a) ->
60head : (xs : List a) ->
69 {default proof { trivial; } p : isCons xs = True} -> a
61 {default proof { trivial; } p : isCons xs = True} -> a
70head (x :: xs) = x
62head (x :: xs) = x
71−
63+\end{code}
72−\end{SaveVerbatim}
73−\useverb{defimp}
74
64
75\subsection{Implicit conversions}
65\subsection{Implicit conversions}
76
66
@@ -79,16 +69,13 @@ automatic conversion of values from one type to another when required to make
79a term type correct. This is intended to increase convenience and reduce
69a term type correct. This is intended to increase convenience and reduce
80verbosity. A contrived but simple example is the following:
70verbosity. A contrived but simple example is the following:
81
71
82−\begin{SaveVerbatim}{implicit}
72+\begin{code}
83−
84implicit intString : Int -> String
73implicit intString : Int -> String
85intString = show
74intString = show
86
75
87test : Int -> String
76test : Int -> String
88test x = "Number " ++ x
77test x = "Number " ++ x
89−
78+\end{code}
90−\end{SaveVerbatim}
91−\useverb{implicit}
92
79
93\noindent
80\noindent
94In general, we cannot append an \texttt{Int} to a \texttt{String}, but the
81In general, we cannot append an \texttt{Int} to a \texttt{String}, but the
@@ -111,17 +98,14 @@ extension of \texttt{.lidr} then it is assumed to be a literate file. In literat
111programs, everything is assumed to be a comment unless the line begins with a
98programs, everything is assumed to be a comment unless the line begins with a
112greater than sign \texttt{>}, for example:
99greater than sign \texttt{>}, for example:
113
100
114−\begin{SaveVerbatim}{litidr}
101+\begin{lstlisting}
115−
116> module literate
102> module literate
117
103
118This is a comment. The main program is below
104This is a comment. The main program is below
119
105
120> main : IO ()
106> main : IO ()
121> main = putStrLn "Hello literate world!\n"
107> main = putStrLn "Hello literate world!\n"
122−
108+\end{lstlisting}
123−\end{SaveVerbatim}
124−\useverb{litidr}
125
109
126\noindent
110\noindent
127An additional restriction is that there must be a blank line between a program
111An additional restriction is that there must be a blank line between a program
@@ -137,12 +121,9 @@ as part of the prelude. For this, we assume a certain amount of knowledge of
137C and the \texttt{gcc} compiler. First, we define a datatype which describes the external
121C and the \texttt{gcc} compiler. First, we define a datatype which describes the external
138types we can handle:
122types we can handle:
139
123
140−\begin{SaveVerbatim}{foreignty}
124+\begin{code}
141−
142data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit
125data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit
143−
126+\end{code}
144−\end{SaveVerbatim}
145−\useverb{foreignty}
146
127
147\noindent
128\noindent
148Each of these corresponds directly to a C type. Respectively: \texttt{int},
129Each of these corresponds directly to a C type. Respectively: \texttt{int},
@@ -150,8 +131,7 @@ Each of these corresponds directly to a C type. Respectively: \texttt{int},
150There is also a translation to a concrete \Idris{} type, described by the
131There is also a translation to a concrete \Idris{} type, described by the
151following function:
132following function:
152
133
153−\begin{SaveVerbatim}{interpfty}
134+\begin{code}
154−
155interpFTy : FTy -> Type
135interpFTy : FTy -> Type
156interpFTy FInt = Int
136interpFTy FInt = Int
157interpFTy FFloat = Float
137interpFTy FFloat = Float
@@ -159,62 +139,49 @@ interpFTy FChar = Char
159interpFTy FString = String
139interpFTy FString = String
160interpFTy FPtr = Ptr
140interpFTy FPtr = Ptr
161interpFTy FUnit = ()
141interpFTy FUnit = ()
162−
142+\end{code}
163−\end{SaveVerbatim}
164−\useverb{interpfty}
165
143
166\noindent
144\noindent
167A foreign function is described by a list of input types and a return type, which
145A foreign function is described by a list of input types and a return type, which
168can then be converted to an \Idris{} type:
146can then be converted to an \Idris{} type:
169
147
170−\begin{SaveVerbatim}{ffunty}
148+\begin{code}
171−
172ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
149ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
173−
150+\end{code}
174−\end{SaveVerbatim}
175−\useverb{ffunty}
176
151
177\noindent
152\noindent
178A foreign function is assumed to be impure, so \texttt{ForeignTy} builds an
153A foreign function is assumed to be impure, so \texttt{ForeignTy} builds an
179\texttt{IO} type, for example:
154\texttt{IO} type, for example:
180
155
181−\begin{SaveVerbatim}{ftyex}
156+\begin{lstlisting}
182−
183Idris> ForeignTy [FInt, FString] FString
157Idris> ForeignTy [FInt, FString] FString
184Int -> String -> IO String : Type
158Int -> String -> IO String : Type
185
159
186Idris> ForeignTy [FInt, FString] FUnit
160Idris> ForeignTy [FInt, FString] FUnit
187Int -> String -> IO () : Type
161Int -> String -> IO () : Type
188−
162+\end{lstlisting}
189−\end{SaveVerbatim}
190−\useverb{ftyex}
191
163
192\noindent
164\noindent
193We build a call to a foreign function by giving the name of the function, a list of
165We build a call to a foreign function by giving the name of the function, a list of
194argument types and the return type. The built in function \texttt{mkForeign}
166argument types and the return type. The built in function \texttt{mkForeign}
195converts this description to a function callable by \Idris{}
167converts this description to a function callable by \Idris{}
196
168
197−\begin{SaveVerbatim}{mkForeign}
169+\begin{code}
198−
199data Foreign : Type -> Type where
170data Foreign : Type -> Type where
200 FFun : String -> (xs:List FTy) -> (t:FTy) ->
171 FFun : String -> (xs:List FTy) -> (t:FTy) ->
201 Foreign (ForeignTy xs t)
172 Foreign (ForeignTy xs t)
202
173
203mkForeign : Foreign x -> x
174mkForeign : Foreign x -> x
204−
175+\end{code}
205−\end{SaveVerbatim}
206−\useverb{mkForeign}
207
176
208\noindent
177\noindent
209For example, the \texttt{putStr} function is implemented as follows, as a call to
178For example, the \texttt{putStr} function is implemented as follows, as a call to
210an external function \texttt{putStr} defined in the run-time system:
179an external function \texttt{putStr} defined in the run-time system:
211
180
212−\begin{SaveVerbatim}{putStrex}
181+\begin{code}
213−
214putStr : String -> IO ()
182putStr : String -> IO ()
215putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
183putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
216−\end{SaveVerbatim}
184+\end{code}
217−\useverb{putStrex}
218
185
219\subsubsection*{Include and linker directives}
186\subsubsection*{Include and linker directives}
220
187
@@ -241,14 +208,11 @@ tested using the special REPL command \texttt{:x EXPR}, and C libraries can be
241dynamically loaded in the interpreter by using the \texttt{:dynamic} command
208dynamically loaded in the interpreter by using the \texttt{:dynamic} command
242or the \texttt{\%dynamic} directive. For example:
209or the \texttt{\%dynamic} directive. For example:
243
210
244−\begin{SaveVerbatim}{xdynamic}
211+\begin{lstlisting}
245−
246Idris> :dynamic libm.so
212Idris> :dynamic libm.so
247Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
213Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
2480.9995736030415051 : Float
2140.9995736030415051 : Float
249−
215+\end{lstlisting}
250−\end{SaveVerbatim}
251−\useverb{xdynamic}
252
216
253\subsection{Type Providers}
217\subsection{Type Providers}
254Idris type providers, inspired by F\#'s type providers, are a means of making
218Idris type providers, inspired by F\#'s type providers, are a means of making
@@ -265,14 +229,10 @@ including as an index in types.
265
229
266Type providers are still an experimental extension. To enable the extension,
230Type providers are still an experimental extension. To enable the extension,
267use the \texttt{\%language} directive:
231use the \texttt{\%language} directive:
268−\begin{SaveVerbatim}{languageProv}
269
232
233+\begin{code}
270%language TypeProviders
234%language TypeProviders
271−
235+\end{code}
272−\end{SaveVerbatim}
273−
274−\useverb{languageProv}
275−
276
236
277A provider \texttt{p} for some type \texttt{t} is simply an expression of type
237A provider \texttt{p} for some type \texttt{t} is simply an expression of type
278\texttt{IO (Provider t)}. The \texttt{\%provide} directive causes the type
238\texttt{IO (Provider t)}. The \texttt{\%provide} directive causes the type
@@ -282,8 +242,7 @@ reads a text file. If the file consists of the string \texttt{"Int"}, then the
282type \texttt{Int} will be provided. Otherwise, it will provide the type
242type \texttt{Int} will be provided. Otherwise, it will provide the type
283\texttt{Nat}.
243\texttt{Nat}.
284
244
285−\begin{SaveVerbatim}{fromFile}
245+\begin{code}
286−
287strToType : String -> Type
246strToType : String -> Type
288strToType "Int" = Int
247strToType "Int" = Int
289strToType _ = Nat
248strToType _ = Nat
@@ -291,21 +250,16 @@ strToType _ = Nat
291fromFile : String -> IO (Provider Type)
250fromFile : String -> IO (Provider Type)
292fromFile fname = do str <- readFile fname
251fromFile fname = do str <- readFile fname
293 return (Provide (strToType (trim str)))
252 return (Provide (strToType (trim str)))
294−
253+\end{code}
295−\end{SaveVerbatim}
296−\useverb{fromFile}
297
254
298We then use the \texttt{\%provide} directive:
255We then use the \texttt{\%provide} directive:
299
256
300−\begin{SaveVerbatim}{fromFileUse}
257+\begin{code}
301−
302%provide (T1 : Type) with fromFile "theType"
258%provide (T1 : Type) with fromFile "theType"
303
259
304foo : T1
260foo : T1
305foo = 2
261foo = 2
306−
262+\end{code}
307−\end{SaveVerbatim}
308−\useverb{fromFileUse}
309
263
310\noindent
264\noindent
311If the file named \texttt{theType} consists of the word \texttt{Int}, then
265If the file named \texttt{theType} consists of the word \texttt{Int}, then
@@ -317,13 +271,10 @@ then \texttt{T1} is defined as \texttt{t}. Otherwise, the result is an error.
317
271
318Our datatype \texttt{Provider t} has the following definition:
272Our datatype \texttt{Provider t} has the following definition:
319
273
320−\begin{SaveVerbatim}{providerdef}
274+\begin{code}
321−
322data Provider a = Error String
275data Provider a = Error String
323 | Provide a
276 | Provide a
324−
277+\end{code}
325−\end{SaveVerbatim}
326−\useverb{providerdef}
327
278
328\noindent
279\noindent
329We have already seen the \texttt{Provide} constructor. The \texttt{Error}
280We have already seen the \texttt{Provide} constructor. The \texttt{Error}
@@ -344,12 +295,9 @@ communicate with the \emph{JavaScript} ecosystem.
344Code generation is split into two separate targets. To generate code that is
295Code generation is split into two separate targets. To generate code that is
345tailored for running in the browser issue the following command:
296tailored for running in the browser issue the following command:
346
297
347−\begin{SaveVerbatim}{jscodegen}
298+\begin{lstlisting}[language=bash]
348−
349$ idris --codegen javascript hello.idr -o hello.js
299$ idris --codegen javascript hello.idr -o hello.js
350−
300+\end{lstlisting}
351−\end{SaveVerbatim}
352−\useverb{jscodegen}
353
301
354\noindent
302\noindent
355The resulting file can be embedded into your HTML just like any other
303The resulting file can be embedded into your HTML just like any other
@@ -359,14 +307,11 @@ The resulting file can be embedded into your HTML just like any other
359Generating code for \emph{NodeJS} is slightly different. \Idris{} outputs
307Generating code for \emph{NodeJS} is slightly different. \Idris{} outputs
360a \emph{JavaScript} file that can be directly executed via \texttt{node}.
308a \emph{JavaScript} file that can be directly executed via \texttt{node}.
361
309
362−\begin{SaveVerbatim}{nodecodegen}
310+\begin{lstlisting}[language=bash]
363−
364$ idris --codegen node hello.idr -o hello
311$ idris --codegen node hello.idr -o hello
365$ ./hello
312$ ./hello
366Hello world
313Hello world
367−
314+\end{lstlisting}
368−\end{SaveVerbatim}
369−\useverb{nodecodegen}
370
315
371\noindent
316\noindent
372Take into consideration that the \emph{JavaScript} code generator is using
317Take into consideration that the \emph{JavaScript} code generator is using
@@ -390,8 +335,7 @@ of \emph{JavaScript} code.
390\noindent
335\noindent
391One could use the primitive addition of \emph{JavaScript} like so:
336One could use the primitive addition of \emph{JavaScript} like so:
392
337
393−\begin{SaveVerbatim}{jsaddition}
338+\begin{code}
394−
395module Main
339module Main
396
340
397primPlus : Int -> Int -> IO Int
341primPlus : Int -> Int -> IO Int
@@ -402,9 +346,7 @@ main = do
402 a <- primPlus 1 1
346 a <- primPlus 1 1
403 b <- primPlus 1 2
347 b <- primPlus 1 2
404 print (a, b)
348 print (a, b)
405−
349+\end{code}
406−\end{SaveVerbatim}
407−\useverb{jsaddition}
408
350
409\noindent
351\noindent
410Notice that the \texttt{\%n} notation qualifies the position of the
352Notice that the \texttt{\%n} notation qualifies the position of the
@@ -416,14 +358,11 @@ instead.
416Passing functions to a foreign function is very similar. Let's assume that
358Passing functions to a foreign function is very similar. Let's assume that
417we want to call the following function from the \emph{JavaScript} world:
359we want to call the following function from the \emph{JavaScript} world:
418
360
419−\begin{SaveVerbatim}{jstwice}
361+\begin{code}[language=c]
420−
421function twice(f, x) {
362function twice(f, x) {
422 return f(f(x));
363 return f(f(x));
423}
364}
424−
365+\end{code}
425−\end{SaveVerbatim}
426−\useverb{jstwice}
427
366
428\noindent
367\noindent
429We obviously need to pass a function \texttt{f} here (we can infer it from
368We obviously need to pass a function \texttt{f} here (we can infer it from
@@ -436,7 +375,7 @@ you give it something of type \texttt{FFunction}. The following example code
436calls \texttt{twice} in \emph{JavaScript} and returns the result to our
375calls \texttt{twice} in \emph{JavaScript} and returns the result to our
437\Idris{} program:
376\Idris{} program:
438
377
439−\begin{SaveVerbatim}{jshof}
378+\begin{code}
440module Main
379module Main
441
380
442twice : (Int -> Int) -> Int -> IO Int
381twice : (Int -> Int) -> Int -> IO Int
@@ -448,9 +387,7 @@ main : IO ()
448main = do
387main = do
449 a <- twice (+1) 1
388 a <- twice (+1) 1
450 print a
389 print a
451−
390+\end{code}
452−\end{SaveVerbatim}
453−\useverb{jshof}
454
391
455\noindent
392\noindent
456The program outputs \texttt{3}, just like we expected.
393The program outputs \texttt{3}, just like we expected.
@@ -470,38 +407,29 @@ application written in \Idris{}.
470Since values can appear in types and \emph{vice versa}, it is natural that types themselves
407Since values can appear in types and \emph{vice versa}, it is natural that types themselves
471have types. For example:
408have types. For example:
472
409
473−\begin{SaveVerbatim}{typetypes}
410+\begin{lstlisting}
474−
475*universe> :t Nat
411*universe> :t Nat
476Nat : Type
412Nat : Type
477*universe> :t Vect
413*universe> :t Vect
478Vect : Nat -> Type -> Type
414Vect : Nat -> Type -> Type
479−
415+\end{lstlisting}
480−\end{SaveVerbatim}
481−\useverb{typetypes}
482
416
483\noindent
417\noindent
484But what about the type of \texttt{Type}? If we ask \Idris{} it reports
418But what about the type of \texttt{Type}? If we ask \Idris{} it reports
485
419
486−\begin{SaveVerbatim}{setset}
420+\begin{lstlisting}
487−
488*universe> :t Type
421*universe> :t Type
489Type : Type 1
422Type : Type 1
490−
423+\end{lstlisting}
491−\end{SaveVerbatim}
492−\useverb{setset}
493
424
494\noindent
425\noindent
495If \texttt{Type} were its own type, it would lead to an inconsitency
426If \texttt{Type} were its own type, it would lead to an inconsitency
496due to Girard's paradox~\cite{girard-thesis}, so internally there is a \emph{hierarchy}
427due to Girard's paradox~\cite{girard-thesis}, so internally there is a \emph{hierarchy}
497of types (or \emph{universes}):
428of types (or \emph{universes}):
498
429
499−\begin{SaveVerbatim}{sethierarchy}
430+\begin{code}
500−
501Type : Type 1 : Type 2 : Type 3 : ...
431Type : Type 1 : Type 2 : Type 3 : ...
502−
432+\end{code}
503−\end{SaveVerbatim}
504−\useverb{sethierarchy}
505
433
506\noindent
434\noindent
507Universes are \emph{cumulative}, that is, if \texttt{x : Type n} we can also have that
435Universes are \emph{cumulative}, that is, if \texttt{x : Type n} we can also have that
@@ -511,16 +439,13 @@ constraints and reports an error if any inconsistencies are found. Ordinarily, a
511programmer does not need to worry about this, but it does prevent (contrived)
439programmer does not need to worry about this, but it does prevent (contrived)
512programs such as the following:
440programs such as the following:
513
441
514−\begin{SaveVerbatim}{idid}
442+\begin{code}
515−
516myid : (a : Type) -> a -> a
443myid : (a : Type) -> a -> a
517myid _ x = x
444myid _ x = x
518
445
519idid : (a : Type) -> a -> a
446idid : (a : Type) -> a -> a
520idid = myid _ myid
447idid = myid _ myid
521−
448+\end{code}
522−\end{SaveVerbatim}
523−\useverb{idid}
524
449
525\noindent
450\noindent
526The application of \texttt{myid} to itself leads to a cycle in the universe hierarchy
451The application of \texttt{myid} to itself leads to a cycle in the universe hierarchy
tutorial/modules.tex → tutorial/content/modules.texrenamed+20−50
@@ -10,8 +10,7 @@ tree type \texttt{BTree} (in a file \texttt{btree.idr}) and Figure
10\ref{bstmain} gives a main program (in a file \texttt{bmain.idr} which uses the
10\ref{bstmain} gives a main program (in a file \texttt{bmain.idr} which uses the
11\texttt{bst} module to sort a list.
11\texttt{bst} module to sort a list.
12
12
13−\begin{SaveVerbatim}{bstmod}
13+\begin{code}[caption={Binary Tree module}, label=bstmod]
14−
15module btree
14module btree
16
15
17data BTree a = Leaf
16data BTree a = Leaf
@@ -29,12 +28,9 @@ toList (Node l v r) = toList l ++ (v :: toList r)
29toTree : Ord a => List a -> BTree a
28toTree : Ord a => List a -> BTree a
30toTree [] = Leaf
29toTree [] = Leaf
31toTree (x :: xs) = insert x (toTree xs)
30toTree (x :: xs) = insert x (toTree xs)
31+\end{code}
32
32
33−\end{SaveVerbatim}
33+\begin{code}[caption={Binary Tree main program},label=bstmain]
34−\codefig{bstmod}{Binary Tree module}
35−
36−\begin{SaveVerbatim}{bstmain}
37−
38module Main
34module Main
39
35
40import btree
36import btree
@@ -42,9 +38,7 @@ import btree
42main : IO ()
38main : IO ()
43main = do let t = toTree [1,8,2,7,9,3]
39main = do let t = toTree [1,8,2,7,9,3]
44 print (toList t)
40 print (toList t)
45−
41+\end{code}
46−\end{SaveVerbatim}
47−\codefig{bstmain}{Binary Tree main program}
48
42
49\noindent
43\noindent
50The same names can be defined in multiple modules. This is possible because in practice names
44The same names can be defined in multiple modules. This is possible because in practice names
@@ -96,8 +90,7 @@ to be \texttt{private}. For our \texttt{btree} module, it makes sense for the
96tree data type and the functions to be exported as \texttt{abstract}, as we see in
90tree data type and the functions to be exported as \texttt{abstract}, as we see in
97Figure \ref{bstmodp}.
91Figure \ref{bstmodp}.
98
92
99−\begin{SaveVerbatim}{bstmodp}
93+\begin{code}[caption={Binary Tree module, with export modifiers}, label=bstmodp]
100−
101module btree
94module btree
102
95
103abstract data BTree a = Leaf
96abstract data BTree a = Leaf
@@ -118,20 +111,15 @@ abstract
118toTree : Ord a => List a -> BTree a
111toTree : Ord a => List a -> BTree a
119toTree [] = Leaf
112toTree [] = Leaf
120toTree (x :: xs) = insert x (toTree xs)
113toTree (x :: xs) = insert x (toTree xs)
121−
114+\end{code}
122−\end{SaveVerbatim}
123−\codefig{bstmodp}{Binary Tree module, with export modifiers}
124
115
125\noindent
116\noindent
126Finally, the default export mode can be changed with the \texttt{\%access} directive,
117Finally, the default export mode can be changed with the \texttt{\%access} directive,
127for example:
118for example:
128
119
129−\begin{SaveVerbatim}{access}
120+\begin{code}
130−
131%access abstract
121%access abstract
132−
122+\end{code}
133−\end{SaveVerbatim}
134−\useverb{access}
135
123
136\noindent
124\noindent
137In this case, any function with no access modifier will be exported as \texttt{abstract},
125In this case, any function with no access modifier will be exported as \texttt{abstract},
@@ -143,8 +131,7 @@ Defining a module also defines a namespace implicitly. However, namespaces can a
143be given \emph{explicitly}. This is most useful if you wish to overload names within
131be given \emph{explicitly}. This is most useful if you wish to overload names within
144the same module:
132the same module:
145
133
146−\begin{SaveVerbatim}{nsfoo}
134+\begin{code}
147−
148module foo
135module foo
149
136
150namespace x
137namespace x
@@ -154,78 +141,61 @@ namespace x
154namespace y
141namespace y
155 test : String -> String
142 test : String -> String
156 test x = x ++ x
143 test x = x ++ x
157−
144+\end{code}
158−\end{SaveVerbatim}
159−\useverb{nsfoo}
160
145
161\noindent
146\noindent
162This (admittedly contrived) module defines two functions with fully qualified names
147This (admittedly contrived) module defines two functions with fully qualified names
163\texttt{foo.x.test} and \texttt{foo.y.test}, which can be disambiguated by their
148\texttt{foo.x.test} and \texttt{foo.y.test}, which can be disambiguated by their
164types:
149types:
165
150
166−\begin{SaveVerbatim}{usetest}
151+\begin{lstlisting}
167−
168*foo> test 3
152*foo> test 3
1696 : Int
1536 : Int
170*foo> test "foo"
154*foo> test "foo"
171"foofoo" : String
155"foofoo" : String
172−
156+\end{lstlisting}
173−\end{SaveVerbatim}
174−\useverb{usetest}
175
157
176\subsection{Parameterised blocks}
158\subsection{Parameterised blocks}
177
159
178Groups of functions can be parameterised over a number of arguments using a
160Groups of functions can be parameterised over a number of arguments using a
179\texttt{parameters} declaration, for example:
161\texttt{parameters} declaration, for example:
180
162
181−\begin{SaveVerbatim}{paramex}
163+\begin{code}
182−
183parameters (x : Nat, y : Nat)
164parameters (x : Nat, y : Nat)
184 addAll : Nat -> Nat
165 addAll : Nat -> Nat
185 addAll z = x + y + z
166 addAll z = x + y + z
186−
167+\end{code}
187−\end{SaveVerbatim}
188−\useverb{paramex}
189
168
190\noindent
169\noindent
191The effect of a \texttt{parameters} block is to add the declared parameters to every
170The effect of a \texttt{parameters} block is to add the declared parameters to every
192function, type and data constructor within the block. Outside the block, the parameters
171function, type and data constructor within the block. Outside the block, the parameters
193must be given explicitly:
172must be given explicitly:
194
173
195−\begin{SaveVerbatim}{addall}
174+\begin{lstlisting}
196−
197*params> :t addAll
175*params> :t addAll
198addAll : Nat -> Nat -> Nat -> Nat
176addAll : Nat -> Nat -> Nat -> Nat
199−
177+\end{lstlisting}
200−\end{SaveVerbatim}
201−\useverb{addall}
202
178
203\noindent
179\noindent
204Parameters blocks can be nested, and can also include data declarations, in
180Parameters blocks can be nested, and can also include data declarations, in
205which case the parameters are added explicitly to all type and data
181which case the parameters are added explicitly to all type and data
206constructors. They may also be dependent types with implicit arguments:
182constructors. They may also be dependent types with implicit arguments:
207
183
208−\begin{SaveVerbatim}{paramdata}
184+\begin{code}
209−
210parameters (xs : Vect x a, y : Nat)
185parameters (xs : Vect x a, y : Nat)
211 data Vects : Type -> Type where
186 data Vects : Type -> Type where
212 MkVects : Vect a y -> Vects a
187 MkVects : Vect a y -> Vects a
213
188
214 append : Vects a -> Vect (x + y) a
189 append : Vects a -> Vect (x + y) a
215 append (MkVects ys) = xs ++ ys
190 append (MkVects ys) = xs ++ ys
216−
191+\end{code}
217−\end{SaveVerbatim}
218−\useverb{paramdata}
219
192
220\noindent
193\noindent
221To use \texttt{Vects} or \texttt{append} outside the block, we must also
194To use \texttt{Vects} or \texttt{append} outside the block, we must also
222give the \texttt{xs} and \texttt{y} arguments. Here, we can use placeholders for
195give the \texttt{xs} and \texttt{y} arguments. Here, we can use placeholders for
223the values which can be inferred by the type checker:
196the values which can be inferred by the type checker:
224
197
225−\begin{SaveVerbatim}{paramuse}
198+\begin{lstlisting}
226−
227*params> show (append _ _ (MkVects [1,2,3] _ [4,5,6]))
199*params> show (append _ _ (MkVects [1,2,3] _ [4,5,6]))
228"[1, 2, 3, 4, 5, 6]" : String
200"[1, 2, 3, 4, 5, 6]" : String
229−
201+\end{lstlisting}
230−\end{SaveVerbatim}
231−\useverb{paramuse}
tutorial/provisional.tex → tutorial/content/provisional.texrenamed+41−103
@@ -7,31 +7,25 @@ checker and the type of the program we have written will be different (in that
7they do not have the same normal form), but nevertheless provably equal. For
7they do not have the same normal form), but nevertheless provably equal. For
8example, recall the \texttt{parity} function:
8example, recall the \texttt{parity} function:
9
9
10−\begin{SaveVerbatim}{pardecl}
10+\begin{code}
11−
12data Parity : Nat -> Type where
11data Parity : Nat -> Type where
13 even : Parity (n + n)
12 even : Parity (n + n)
14 odd : Parity (S (n + n))
13 odd : Parity (S (n + n))
15
14
16parity : (n:Nat) -> Parity n
15parity : (n:Nat) -> Parity n
17−
16+\end{code}
18−\end{SaveVerbatim}
19−\useverb{pardecl}
20
17
21\noindent
18\noindent
22We'd like to implement this as follows:
19We'd like to implement this as follows:
23
20
24−\begin{SaveVerbatim}{parfail}
21+\begin{code}
25−
26parity : (n:Nat) -> Parity n
22parity : (n:Nat) -> Parity n
27parity Z = even {n=Z}
23parity Z = even {n=Z}
28parity (S Z) = odd {n=Z}
24parity (S Z) = odd {n=Z}
29parity (S (S k)) with (parity k)
25parity (S (S k)) with (parity k)
30 parity (S (S (j + j))) | even = even {n=S j}
26 parity (S (S (j + j))) | even = even {n=S j}
31 parity (S (S (S (j + j)))) | odd = odd {n=S j}
27 parity (S (S (S (j + j)))) | odd = odd {n=S j}
32−
28+\end{code}
33−\end{SaveVerbatim}
34−\useverb{parfail}
35
29
36\noindent
30\noindent
37This simply states that zero is even, one is odd, and recursively, the parity
31This simply states that zero is even, one is odd, and recursively, the parity
@@ -40,13 +34,10 @@ Explicitly marking the value of \texttt{n} in
40even and odd is necessary to help type inference. Unfortunately, the type
34even and odd is necessary to help type inference. Unfortunately, the type
41checker rejects this:
35checker rejects this:
42
36
43−\begin{SaveVerbatim}{parerror}
37+\begin{code}
44−
45views.idr:12:Can't unify Parity (plus (S j) (S j)) with
38views.idr:12:Can't unify Parity (plus (S j) (S j)) with
46Parity (S (S (plus j j)))
39Parity (S (S (plus j j)))
47−
40+\end{code}
48−\end{SaveVerbatim}
49−\useverb{parerror}
50
41
51\noindent
42\noindent
52The type checker
43The type checker
@@ -54,8 +45,7 @@ is telling us that \texttt{(j+1)+(j+1)} and \texttt{2+j+j}
54do not normalise to the same value.
45do not normalise to the same value.
55This is because \texttt{plus} is defined by recursion on its first argument, and in the
46This is because \texttt{plus} is defined by recursion on its first argument, and in the
56second value, there is a successor symbol on the second argument, so this will
47second value, there is a successor symbol on the second argument, so this will
57−not help with reduction. These values are obviously equal --- how can we rewrite
48+not help with reduction. These values are obviously equal --- how can we rewrite the program to fix this problem?
58−the program to fix this problem?
59
49
60\subsection{Provisional definitions}
50\subsection{Provisional definitions}
61
51
@@ -76,17 +66,14 @@ except that they introduce the right hand side with a \texttt{?=} rathar than
76\texttt{=}. We define
66\texttt{=}. We define
77\texttt{parity} as follows:
67\texttt{parity} as follows:
78
68
79−\begin{SaveVerbatim}{paritypro}
69+\begin{code}
80−
81parity : (n:Nat) -> Parity n
70parity : (n:Nat) -> Parity n
82parity Z = even {n=Z}
71parity Z = even {n=Z}
83parity (S Z) = odd {n=Z}
72parity (S Z) = odd {n=Z}
84parity (S (S k)) with (parity k)
73parity (S (S k)) with (parity k)
85 parity (S (S (j + j))) | even ?= even {n=S j}
74 parity (S (S (j + j))) | even ?= even {n=S j}
86 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
75 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
87−
76+\end{code}
88−\end{SaveVerbatim}
89−\useverb{paritypro}
90
77
91\noindent
78\noindent
92When written in this form, instead of reporting a type error, \Idris{} will insert
79When written in this form, instead of reporting a type error, \Idris{} will insert
@@ -94,29 +81,23 @@ a metavariable standing for a theorem which will correct the type error. \Idris{
94tells us we have two proof obligations, with names generated from the module and
81tells us we have two proof obligations, with names generated from the module and
95function names:
82function names:
96
83
97−\begin{SaveVerbatim}{prometas}
84+\begin{lstlisting}
98−
99*views> :m
85*views> :m
100Global metavariables:
86Global metavariables:
101 [views.parity_lemma_2,views.parity_lemma_1]
87 [views.parity_lemma_2,views.parity_lemma_1]
102−
88+\end{lstlisting}
103−\end{SaveVerbatim}
104−\useverb{prometas}
105
89
106\noindent
90\noindent
107The first of these has the following type:
91The first of these has the following type:
108
92
109−\begin{SaveVerbatim}{prolem1}
93+\begin{lstlisting}
110−
111*views> :p views.parity_lemma_1
94*views> :p views.parity_lemma_1
112
95
113---------------------------------- (views.parity_lemma_1) --------
96---------------------------------- (views.parity_lemma_1) --------
114{hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (j + j)))
97{hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (j + j)))
115
98
116-views.parity_lemma_1>
99-views.parity_lemma_1>
117−
100+\end{lstlisting}
118−\end{SaveVerbatim}
119−\useverb{prolem1}
120
101
121\noindent
102\noindent
122The two arguments are \texttt{j}, the variable in scope from the pattern match,
103The two arguments are \texttt{j}, the variable in scope from the pattern match,
@@ -126,71 +107,55 @@ this value.
126We can achieve this using the following theorem from
107We can achieve this using the following theorem from
127the prelude:
108the prelude:
128
109
129−\begin{SaveVerbatim}{plusnsm}
110+\begin{code}
130−
131plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
111plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
132 S (left + right) = left + (S right)
112 S (left + right) = left + (S right)
133−
113+\end{code}
134−
135−\end{SaveVerbatim}
136−\useverb{plusnsm}
137
114
138\noindent
115\noindent
139After applying \texttt{intro} twice, we have:
116After applying \texttt{intro} twice, we have:
140
117
141−\begin{SaveVerbatim}{prolemii}
118+\begin{lstlisting}
142−
143-views.parity_lemma_1> intro
119-views.parity_lemma_1> intro
144
120
145 j : Nat
121 j : Nat
146 value : Parity (S (plus j (S j)))
122 value : Parity (S (plus j (S j)))
147---------------------------------- (views.parity_lemma_1) --------
123---------------------------------- (views.parity_lemma_1) --------
148{hole2} : Parity (S (S (j + j)))
124{hole2} : Parity (S (S (j + j)))
149−
125+\end{lstlisting}
150−\end{SaveVerbatim}
151−\useverb{prolemii}
152
126
153\noindent
127\noindent
154We need to use \texttt{compute} again to unfold the definition of \texttt{(+)}.
128We need to use \texttt{compute} again to unfold the definition of \texttt{(+)}.
155
129
156−\begin{SaveVerbatim}{prolemcomp}
130+\begin{lstlisting}
157−
158-views.parity_lemma_1> intro
131-views.parity_lemma_1> intro
159
132
160 j : Nat
133 j : Nat
161 value : Parity (S (plus j (S j)))
134 value : Parity (S (plus j (S j)))
162---------------------------------- (views.parity_lemma_1) --------
135---------------------------------- (views.parity_lemma_1) --------
163{hole2} : Parity (S (S (plus j j)))
136{hole2} : Parity (S (S (plus j j)))
164−
137+\end{lstlisting}
165−\end{SaveVerbatim}
166−\useverb{prolemcomp}
167
138
168\noindent
139\noindent
169Then we apply the \texttt{plusSuccRightSucc} rewrite rule, symmetrically,
140Then we apply the \texttt{plusSuccRightSucc} rewrite rule, symmetrically,
170to \texttt{j} and \texttt{j}, giving:
141to \texttt{j} and \texttt{j}, giving:
171
142
172−\begin{SaveVerbatim}{prolemr}
143+\begin{lstlisting}
173−
174-views.parity_lemma_1> rewrite sym (plusSuccRightSucc j j)
144-views.parity_lemma_1> rewrite sym (plusSuccRightSucc j j)
175
145
176 j : Nat
146 j : Nat
177 value : Parity (S (plus j (S j)))
147 value : Parity (S (plus j (S j)))
178---------------------------------- (views.parity_lemma_1) --------
148---------------------------------- (views.parity_lemma_1) --------
179{hole3} : Parity (S (plus j (S j)))
149{hole3} : Parity (S (plus j (S j)))
180−
150+\end{lstlisting}
181−\end{SaveVerbatim}
182−\useverb{prolemr}
183
151
184\noindent
152\noindent
185\texttt{sym} is a function, defined in the library, which reverses the order of the rewrite:
153\texttt{sym} is a function, defined in the library, which reverses the order of the rewrite:
186
154
187−\begin{SaveVerbatim}{sym}
155+\begin{lstlisting}
188−
189sym : l = r -> r = l
156sym : l = r -> r = l
190sym refl = refl
157sym refl = refl
191−
158+\end{lstlisting}
192−\end{SaveVerbatim}
193−\useverb{sym}
194
159
195\noindent
160\noindent
196We can complete this proof using the \texttt{trivial} tactic, which finds
161We can complete this proof using the \texttt{trivial} tactic, which finds
@@ -201,13 +166,10 @@ We can now test the \texttt{natToBin} function from Section
201\ref{sect:nattobin} at the prompt. 42 is 101010 in
166\ref{sect:nattobin} at the prompt. 42 is 101010 in
202binary. The binary digits are reversed:
167binary. The binary digits are reversed:
203
168
204−\begin{SaveVerbatim}{ntbtest}
169+\begin{lstlisting}
205−
206*views> show (natToBin 42)
170*views> show (natToBin 42)
207"[False, True, False, True, False, True]" : String
171"[False, True, False, True, False, True]" : String
208−
172+\end{lstlisting}
209−\end{SaveVerbatim}
210−\useverb{ntbtest}
211
173
212
174
213\subsection{Suspension of Disbelief}
175\subsection{Suspension of Disbelief}
@@ -222,28 +184,22 @@ something!
222Therefore, \Idris{} provides a built-in coercion function, which allows you to use
184Therefore, \Idris{} provides a built-in coercion function, which allows you to use
223a value of the incorrect types:
185a value of the incorrect types:
224
186
225−\begin{SaveVerbatim}{believe}
187+\begin{code}
226−
227believe_me : a -> b
188believe_me : a -> b
228−
189+\end{code}
229−\end{SaveVerbatim}
230−\useverb{believe}
231
190
232\noindent
191\noindent
233Obviously, this should be used with extreme caution. It is useful when prototyping, and
192Obviously, this should be used with extreme caution. It is useful when prototyping, and
234can also be appropriate when asserting properties of external code (perhaps in an
193can also be appropriate when asserting properties of external code (perhaps in an
235external C library). The ``proof'' of \texttt{views.parity\_lemma\_1} using this is:
194external C library). The ``proof'' of \texttt{views.parity\_lemma\_1} using this is:
236
195
237−\begin{SaveVerbatim}{pladodgy}
196+\begin{lstlisting}
238−
239views.parity_lemma_2 = proof {
197views.parity_lemma_2 = proof {
240 intro;
198 intro;
241 intro;
199 intro;
242 exact believe_me value;
200 exact believe_me value;
243}
201}
244−
202+\end{lstlisting}
245−\end{SaveVerbatim}
246−\useverb{pladodgy}
247
203
248\noindent
204\noindent
249The \texttt{exact} tactic allows us to provide an exact value for the proof. In this case,
205The \texttt{exact} tactic allows us to provide an exact value for the proof. In this case,
@@ -258,15 +214,12 @@ We begin by indexing binary numbers over their \texttt{Nat} equivalent. This is
258pattern, linking a representation (in this case \texttt{Binary}) with a meaning (in this
214pattern, linking a representation (in this case \texttt{Binary}) with a meaning (in this
259case \texttt{Nat}):
215case \texttt{Nat}):
260
216
261−\begin{SaveVerbatim}{bindef}
217+\begin{code}
262−
263data Binary : Nat -> Type where
218data Binary : Nat -> Type where
264 bEnd : Binary Z
219 bEnd : Binary Z
265 bO : Binary n -> Binary (n + n)
220 bO : Binary n -> Binary (n + n)
266 bI : Binary n -> Binary (S (n + n))
221 bI : Binary n -> Binary (S (n + n))
267−
222+\end{code}
268−\end{SaveVerbatim}
269−\useverb{bindef}
270
223
271\noindent
224\noindent
272\texttt{bO} and \texttt{bI} take a binary number as an argument and effectively shift it one bit
225\texttt{bO} and \texttt{bI} take a binary number as an argument and effectively shift it one bit
@@ -278,69 +231,54 @@ the least significant bit at the front.
278Now a function which converts a Nat to binary will state, in the type, that the
231Now a function which converts a Nat to binary will state, in the type, that the
279resulting binary number is a faithful representation of the original Nat:
232resulting binary number is a faithful representation of the original Nat:
280
233
281−\begin{SaveVerbatim}{ntbty}
234+\begin{code}
282−
283natToBin : (n:Nat) -> Binary n
235natToBin : (n:Nat) -> Binary n
284−
236+\end{code}
285−\end{SaveVerbatim}
286−\useverb{ntbty}
287
237
288\noindent
238\noindent
289The \texttt{Parity} view makes the definition fairly simple --- halving the
239The \texttt{Parity} view makes the definition fairly simple --- halving the
290number is effectively a right shift after all --- although we need to use a
240number is effectively a right shift after all --- although we need to use a
291provisional definition in the odd case:
241provisional definition in the odd case:
292
242
293−\begin{SaveVerbatim}{ntbdef}
243+\begin{code}
294−
295natToBin : (n:Nat) -> Binary n
244natToBin : (n:Nat) -> Binary n
296natToBin Z = bEnd
245natToBin Z = bEnd
297natToBin (S k) with (parity k)
246natToBin (S k) with (parity k)
298 natToBin (S (j + j)) | even = bI (natToBin j)
247 natToBin (S (j + j)) | even = bI (natToBin j)
299 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
248 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
300−
249+\end{code}
301−\end{SaveVerbatim}
302−\useverb{ntbdef}
303
250
304\noindent
251\noindent
305The problem with the odd case is the same as in the definition of \texttt{parity}, and
252The problem with the odd case is the same as in the definition of \texttt{parity}, and
306the proof proceeds in the same way:
253the proof proceeds in the same way:
307
254
308−\begin{SaveVerbatim}{ntboddprf}
255+\begin{code}
309−
310natToBin_lemma_1 = proof {
256natToBin_lemma_1 = proof {
311 intro;
257 intro;
312 intro;
258 intro;
313 rewrite sym (plusSuccRightSucc j j);
259 rewrite sym (plusSuccRightSucc j j);
314 trivial;
260 trivial;
315}
261}
316−
262+\end{code}
317−\end{SaveVerbatim}
318−\useverb{ntboddprf}
319
263
320\noindent
264\noindent
321To finish, we'll implement a main program which reads an integer from the user and
265To finish, we'll implement a main program which reads an integer from the user and
322outputs it in binary.
266outputs it in binary.
323
267
324−\begin{SaveVerbatim}{binmain}
268+\begin{code}
325−
326main : IO ()
269main : IO ()
327main = do putStr "Enter a number: "
270main = do putStr "Enter a number: "
328 x <- getLine
271 x <- getLine
329 print (natToBin (fromInteger (cast x)))
272 print (natToBin (fromInteger (cast x)))
330−
273+\end{code}
331−\end{SaveVerbatim}
332−\useverb{binmain}
333
274
334\noindent
275\noindent
335For this to work, of course, we need a \texttt{Show} instance for \texttt{Binary n}:
276For this to work, of course, we need a \texttt{Show} instance for \texttt{Binary n}:
336
277
337−\begin{SaveVerbatim}{showbin}
278+\begin{code}
338−
339instance Show (Binary n) where
279instance Show (Binary n) where
340 show (bO x) = show x ++ "0"
280 show (bO x) = show x ++ "0"
341 show (bI x) = show x ++ "1"
281 show (bI x) = show x ++ "1"
342 show bEnd = ""
282 show bEnd = ""
343−
283+\end{code}
344−\end{SaveVerbatim}
345−\useverb{showbin}
346
284
tutorial/starting.tex → tutorial/content/starting.texrenamed+15−35
@@ -16,12 +16,9 @@ all major Linux distributions.
16
16
17The easiest way to install \Idris{}, if you have all of the prerequisites, is to type:
17The easiest way to install \Idris{}, if you have all of the prerequisites, is to type:
18
18
19−\begin{SaveVerbatim}{install}
19+\begin{lstlisting}[language=bash]
20−
21cabal update; cabal install idris
20cabal update; cabal install idris
22−
21+\end{lstlisting}
23−\end{SaveVerbatim}
24−\useverb{install}
25
22
26\noindent
23\noindent
27This will install the latest version released on Hackage, along with any dependencies.
24This will install the latest version released on Hackage, along with any dependencies.
@@ -33,15 +30,12 @@ To check that installation has succeeded, and to write your first \Idris{}
33program, create a file called ``\texttt{hello.idr}'' containing the following
30program, create a file called ``\texttt{hello.idr}'' containing the following
34text:
31text:
35
32
36−\begin{SaveVerbatim}{hello}
33+\begin{code}
37−
38module Main
34module Main
39
35
40main : IO ()
36main : IO ()
41main = putStrLn "Hello world"
37main = putStrLn "Hello world"
42−
38+\end{code}
43−\end{SaveVerbatim}
44−\useverb{hello}
45
39
46\noindent
40\noindent
47If you are familiar with Haskell, it should be fairly clear what the program is doing
41If you are familiar with Haskell, it should be fairly clear what the program is doing
@@ -49,14 +43,11 @@ and how it works, but if not, we will explain the details later.
49You can compile the program to an executable by entering \texttt{idris hello.idr -o hello}
43You can compile the program to an executable by entering \texttt{idris hello.idr -o hello}
50at the shell prompt. This will create an executable called \texttt{hello}, which you can run:
44at the shell prompt. This will create an executable called \texttt{hello}, which you can run:
51
45
52−\begin{SaveVerbatim}{hello}
46+\begin{lstlisting}[language=bash]
53−
54$ idris hello.idr -o hello
47$ idris hello.idr -o hello
55$ ./hello
48$ ./hello
56Hello world
49Hello world
57−
50+\end{lstlisting}
58−\end{SaveVerbatim}
59−\useverb{hello}
60
51
61\noindent
52\noindent
62Note that the \texttt{\$} indicates the shell prompt! Some useful options to the
53Note that the \texttt{\$} indicates the shell prompt! Some useful options to the
@@ -74,21 +65,16 @@ interactive environment.
74Entering \texttt{idris} at the shell prompt starts up the interactive
65Entering \texttt{idris} at the shell prompt starts up the interactive
75environment. You should see something like the following:
66environment. You should see something like the following:
76
67
77−\begin{SaveVerbatim}[commandchars=^\{\}]{prompt1}
68+\begin{lstlisting}[escapechar=^]
78−
79$ idris
69$ idris
80 ____ __ _
70 ____ __ _
81 / _/___/ /____(_)____
71 / _/___/ /____(_)____
82− / // __ / ___/ / ___/ Version ^version{}
72+ / // __ / ___/ / ___/ Version ^\version{}^
83 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
73 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
84 /___/\__,_/_/ /_/____/ Type :? for help
74 /___/\__,_/_/ /_/____/ Type :? for help
85
75
86Idris>
76Idris>
87−
77+\end{lstlisting}
88−\end{SaveVerbatim}
89−%$
90−
91−\useverb{prompt1}
92
78
93\noindent
79\noindent
94This gives a \texttt{ghci}-style interface which allows evaluation of expressions,
80This gives a \texttt{ghci}-style interface which allows evaluation of expressions,
@@ -98,8 +84,8 @@ as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
98\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then
84\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then
99the program is compiled to the executable \texttt{hello}.
85the program is compiled to the executable \texttt{hello}.
100
86
101−\begin{SaveVerbatim}[commandchars=\\\{\}]{cmds}
87+\begin{lstlisting}[caption={Interactive environment commands}, label=cmds, escapechar=^]
102−Idris version \version{}
88+Idris version ^\version{}^
103--------------------
89--------------------
104
90
105 Command Arguments Purpose
91 Command Arguments Purpose
@@ -132,16 +118,13 @@ Idris version \version{}
132 :unset <option> Unset an option
118 :unset <option> Unset an option
133 :colour :color <option> Turn REPL colours on or off; set a specific colour
119 :colour :color <option> Turn REPL colours on or off; set a specific colour
134 :q :quit Exit the Idris system
120 :q :quit Exit the Idris system
135−\end{SaveVerbatim}
121+\end{lstlisting}
136−\codefigs{cmds}{Interactive environment commands}
137−
138−
139−\begin{SaveVerbatim}[commandchars=^\{\}]{run1}
140
122
123+\begin{lstlisting}[caption={Sample Interactive Run}, label=run1, escapechar=^]
141$ idris hello.idr
124$ idris hello.idr
142 ____ __ _
125 ____ __ _
143 / _/___/ /____(_)____
126 / _/___/ /____(_)____
144− / // __ / ___/ / ___/ Version ^version{}
127+ / // __ / ___/ / ___/ Version ^\version{}^
145 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
128 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
146 /___/\__,_/_/ /_/____/ Type :? for help
129 /___/\__,_/_/ /_/____/ Type :? for help
147
130
@@ -153,10 +136,7 @@ main : IO ()
153Bye bye
136Bye bye
154$ ./hello
137$ ./hello
155Hello world
138Hello world
156−
139+\end{lstlisting}
157−\end{SaveVerbatim}
158−
159−\codefig{run1}{Sample interactive run}
160
140
161\noindent
141\noindent
162Type checking a file, if successful, creates a bytecode version of the file (in
142Type checking a file, if successful, creates a bytecode version of the file (in
tutorial/syntax.tex → tutorial/content/syntax.texrenamed+13−31
@@ -11,24 +11,18 @@ rules and \texttt{dsl} notation.
11We have seen \texttt{if...then...else} expressions, but these
11We have seen \texttt{if...then...else} expressions, but these
12are 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
13
13
14−\begin{SaveVerbatim}{boolelim}
14+\begin{code}
15−
16boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a;
15boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a;
17boolElim True t e = t;
16boolElim True t e = t;
18boolElim False t e = e;
17boolElim False t e = e;
19−
18+\end{code}
20−\end{SaveVerbatim}
21−\useverb{boolelim}
22
19
23\noindent
20\noindent
24\ldots and extend the core syntax with a \texttt{syntax} declaration:
21\ldots and extend the core syntax with a \texttt{syntax} declaration:
25
22
26−\begin{SaveVerbatim}{syntaxif}
23+\begin{code}
27−
28syntax if [test] then [t] else [e] = boolElim test t e;
24syntax if [test] then [t] else [e] = boolElim test t e;
29−
25+\end{code}
30−\end{SaveVerbatim}
31−\useverb{syntaxif}
32
26
33\noindent
27\noindent
34The left hand side of a \texttt{syntax} declaration describes the syntax rule, and the right
28The left hand side of a \texttt{syntax} declaration describes the syntax rule, and the right
@@ -56,15 +50,12 @@ constants, or bracketed expressions). Rules can use previously defined rules,
56but may not be recursive. The following syntax extensions would therefore be
50but may not be recursive. The following syntax extensions would therefore be
57valid:
51valid:
58
52
59−\begin{SaveVerbatim}{syntaxex}
53+\begin{code}
60−
61syntax [var] ":=" [val] = Assign var val;
54syntax [var] ":=" [val] = Assign var val;
62syntax [test] "?" [t] ":" [e] = if test then t else e;
55syntax [test] "?" [t] ":" [e] = if test then t else e;
63syntax select [x] from [t] where [w] = SelectWhere x t w;
56syntax select [x] from [t] where [w] = SelectWhere x t w;
64syntax select [x] from [t] = Select x t;
57syntax select [x] from [t] = Select x t;
65−
58+\end{code}
66−\end{SaveVerbatim}
67−\useverb{syntaxex}
68
59
69\noindent
60\noindent
70Syntax macros can be further restricted to apply only in patterns (i.e., only on the left
61Syntax macros can be further restricted to apply only in patterns (i.e., only on the left
@@ -73,26 +64,20 @@ of a pattern match clause) by being marked as \texttt{pattern} or \texttt{term}
73rules. For example, we might define an interval as follows, with a static check
64rules. 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}:
65that the lower bound is below the upper bound using \texttt{so}:
75
66
76−\begin{SaveVerbatim}{interval}
67+\begin{code}
77−
78data Interval : Type where
68data Interval : Type where
79 MkInterval : (lower : Float) -> (upper : Float) ->
69 MkInterval : (lower : Float) -> (upper : Float) ->
80 so (lower < upper) -> Interval
70 so (lower < upper) -> Interval
81−
71+\end{code}
82−\end{SaveVerbatim}
83−\useverb{interval}
84
72
85\noindent
73\noindent
86We can define a syntax which, in patterns, always matches \texttt{oh} for the proof
74We 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:
75argument, and in terms requires a proof term to be provided:
88
76
89−\begin{SaveVerbatim}{intervalsyn}
77+\begin{code}
90−
91pattern syntax "[" [x] "..." [y] "]" = MkInterval x y oh
78pattern syntax "[" [x] "..." [y] "]" = MkInterval x y oh
92term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
79term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
93−
80+\end{code}
94−\end{SaveVerbatim}
95−\useverb{intervalsyn}
96
81
97\noindent
82\noindent
98In terms, the syntax \texttt{[x...y]} will generate a proof obligation
83In terms, the syntax \texttt{[x...y]} will generate a proof obligation
@@ -101,22 +86,19 @@ In terms, the syntax \texttt{[x...y]} will generate a proof obligation
101Finally, syntax rules may be used to introduce alternative binding forms. For
86Finally, syntax rules may be used to introduce alternative binding forms. For
102exampe, a \texttt{for} loop binds a variable on each iteration:
87exampe, a \texttt{for} loop binds a variable on each iteration:
103
88
104−\begin{SaveVerbatim}{forloop}
89+\begin{code}
105−
106syntax for {x} "in" [xs] ":" [body] = forLoop xs (\x => body)
90syntax for {x} "in" [xs] ":" [body] = forLoop xs (\x => body)
107
91
108main : IO ()
92main : IO ()
109main = do for x in [1..10]:
93main = do for x in [1..10]:
110 putStrLn ("Number " ++ show x)
94 putStrLn ("Number " ++ show x)
111 putStrLn "Done!"
95 putStrLn "Done!"
112−
96+\end{code}
113−\end{SaveVerbatim}
114−\useverb{forloop}
115
97
116\noindent
98\noindent
117Note that we have used the \texttt{\{x\}} form to state that \texttt{x} represents
99Note 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
100a bound variable, substituted on the right hand side. We have also put \texttt{"in"} in
119quotation marks since it is already a reserved word.
101quotation marks since it is already a reserved word.
120
102
121−\input{dsl}
103+\input{./content/dsl}
122
104
tutorial/theorems.tex → tutorial/content/theorems.texrenamed+53−131
@@ -6,28 +6,22 @@
6programs to be stated and proved. Equality is built in, but conceptually has
6programs to be stated and proved. Equality is built in, but conceptually has
7the following definition:
7the following definition:
8
8
9−\begin{SaveVerbatim}{}
9+\begin{code}
10−
11data (=) : a -> b -> Type where
10data (=) : a -> b -> Type where
12 refl : x = x
11 refl : x = x
13−
12+\end{code}
14−\end{SaveVerbatim}
15−\useverb{}
16
13
17\noindent
14\noindent
18Equalities can be proposed between any values of any types, but the only way to
15Equalities can be proposed between any values of any types, but the only way to
19construct a proof of equality is if values actually are equal. For example:
16construct a proof of equality is if values actually are equal. For example:
20
17
21−\begin{SaveVerbatim}{eqprf}
18+\begin{code}
22−
23fiveIsFive : 5 = 5
19fiveIsFive : 5 = 5
24fiveIsFive = refl
20fiveIsFive = refl
25
21
26twoPlusTwo : 2 + 2 = 4
22twoPlusTwo : 2 + 2 = 4
27twoPlusTwo = refl
23twoPlusTwo = refl
28−
24+\end{code}
29−\end{SaveVerbatim}
30−\useverb{eqprf}
31
25
32\subsection{The Empty Type}
26\subsection{The Empty Type}
33
27
@@ -40,46 +34,36 @@ without using a partially defined or general recursive function (see Section
40to prove that something is impossible, for example zero is never equal
34to prove that something is impossible, for example zero is never equal
41to a successor:
35to a successor:
42
36
43−\begin{SaveVerbatim}{natdisjoint}
37+\begin{code}
44−
45disjoint : (n : Nat) -> Z = S n -> _|_
38disjoint : (n : Nat) -> Z = S n -> _|_
46disjoint n p = replace {P = disjointTy} p ()
39disjoint n p = replace {P = disjointTy} p ()
47 where
40 where
48 disjointTy : Nat -> Type
41 disjointTy : Nat -> Type
49 disjointTy Z = ()
42 disjointTy Z = ()
50 disjointTy (S k) = _|_
43 disjointTy (S k) = _|_
51−
44+\end{code}
52−\end{SaveVerbatim}
53−\useverb{natdisjoint}
54
45
55\noindent
46\noindent
56There is no need to worry too much about how this function works --- essentially,
47There is no need to worry too much about how this function works --- essentially,
57it applies the library function \texttt{replace}, which uses an equality proof to
48it applies the library function \texttt{replace}, which uses an equality proof to
58transform a predicate. Here we use it to transform a value of a type which can exist,
49transform a predicate. Here we use it to transform a value of a type which can exist,
59−the empty tuple, to a value of a type which can't, by using a proof of something
50+the empty tuple, to a value of a type which can't, by using a proof of something which can't exist.
60−which can't exist.
61
51
62Once we have an element of the empty type, we can prove anything. \texttt{FalseElim}
52Once we have an element of the empty type, we can prove anything. \texttt{FalseElim}
63is defined in the library, to assist with proofs by contradiction.
53is defined in the library, to assist with proofs by contradiction.
64
54
65−\begin{SaveVerbatim}{falseelim}
55+\begin{code}
66−
67FalseElim : _|_ -> a
56FalseElim : _|_ -> a
68−
57+\end{code}
69−\end{SaveVerbatim}
70−\useverb{falseelim}
71
58
72\subsection{Simple Theorems}
59\subsection{Simple Theorems}
73
60
74When type checking dependent types, the type itself gets \emph{normalised}. So imagine
61When type checking dependent types, the type itself gets \emph{normalised}. So imagine
75we want to prove the following theorem about the reduction behaviour of \texttt{plus}:
62we want to prove the following theorem about the reduction behaviour of \texttt{plus}:
76
63
77−\begin{SaveVerbatim}{plusred}
64+\begin{code}
78−
79plusReduces : (n:Nat) -> plus Z n = n
65plusReduces : (n:Nat) -> plus Z n = n
80−
66+\end{code}
81−\end{SaveVerbatim}
82−\useverb{plusred}
83
67
84\noindent
68\noindent
85We've written down the statement of the theorem as a type, in just the same way
69We've written down the statement of the theorem as a type, in just the same way
@@ -93,49 +77,37 @@ correspondence~\cite{howard} explains this relationship.
93The proof itself is trivial, because \texttt{plus Z n} normalises to \texttt{n}
77The proof itself is trivial, because \texttt{plus Z n} normalises to \texttt{n}
94by the definition of \texttt{plus}:
78by the definition of \texttt{plus}:
95
79
96−\begin{SaveVerbatim}{plusredp}
80+\begin{code}
97−
98plusReduces n = refl
81plusReduces n = refl
99−
82+\end{code}
100−\end{SaveVerbatim}
101−\useverb{plusredp}
102
83
103\noindent
84\noindent
104It is slightly harder if we try the arguments the other way, because plus is
85It is slightly harder if we try the arguments the other way, because plus is
105defined by recursion on its first argument. The proof also works by recursion
86defined by recursion on its first argument. The proof also works by recursion
106on the first argument to \texttt{plus}, namely \texttt{n}.
87on the first argument to \texttt{plus}, namely \texttt{n}.
107
88
108−\begin{SaveVerbatim}{plusRedO}
89+\begin{code}
109−
110plusReducesZ : (n:Nat) -> n = plus n Z
90plusReducesZ : (n:Nat) -> n = plus n Z
111plusReducesZ Z = refl
91plusReducesZ Z = refl
112plusReducesZ (S k) = cong (plusReducesZ k)
92plusReducesZ (S k) = cong (plusReducesZ k)
113−
93+\end{code}
114−\end{SaveVerbatim}
115−\useverb{plusRedO}
116
94
117\noindent
95\noindent
118\texttt{cong} is a function defined in the library which states that
96\texttt{cong} is a function defined in the library which states that
119equality respects function application:
97equality respects function application:
120
98
121−\begin{SaveVerbatim}{resps}
99+\begin{code}
122−
123cong : {f : t -> u} -> a = b -> f a = f b
100cong : {f : t -> u} -> a = b -> f a = f b
124−
101+\end{code}
125−\end{SaveVerbatim}
126−\useverb{resps}
127
102
128\noindent
103\noindent
129We can do the same for the reduction behaviour of plus on successors:
104We can do the same for the reduction behaviour of plus on successors:
130
105
131−\begin{SaveVerbatim}{plusRedS}
106+\begin{code}
132−
133plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
107plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
134plusReducesS Z m = refl
108plusReducesS Z m = refl
135plusReducesS (S k) m = cong (plusReducesS k m)
109plusReducesS (S k) m = cong (plusReducesS k m)
136−
110+\end{code}
137−\end{SaveVerbatim}
138−\useverb{plusRedS}
139
111
140\noindent
112\noindent
141Even for trival theorems like these, the proofs are a little tricky to
113Even for trival theorems like these, the proofs are a little tricky to
@@ -152,15 +124,12 @@ the proof by \emph{induction}, so we write the cases for \texttt{Z} and
152\texttt{S}, with a recursive call in the \texttt{S} case giving the inductive
124\texttt{S}, with a recursive call in the \texttt{S} case giving the inductive
153hypothesis, and insert \emph{metavariables} for the rest of the definition:
125hypothesis, and insert \emph{metavariables} for the rest of the definition:
154
126
155−\begin{SaveVerbatim}{prOstruct}
127+\begin{code}
156−
157plusReducesZ' : (n:Nat) -> n = plus n Z
128plusReducesZ' : (n:Nat) -> n = plus n Z
158plusReducesZ' Z = ?plusredZ_Z
129plusReducesZ' Z = ?plusredZ_Z
159plusReducesZ' (S k) = let ih = plusReducesZ' k in
130plusReducesZ' (S k) = let ih = plusReducesZ' k in
160 ?plusredZ_S
131 ?plusredZ_S
161−
132+\end{code}
162−\end{SaveVerbatim}
163−\useverb{prOstruct}
164
133
165\noindent
134\noindent
166On running \Idris{}, two global names are created, \texttt{plusredZ\_O} and
135On running \Idris{}, two global names are created, \texttt{plusredZ\_O} and
@@ -169,40 +138,31 @@ at the prompt to find out which metavariables are still to be solved (or, more
169precisely, which functions exist but have no definitions), then the
138precisely, which functions exist but have no definitions), then the
170\texttt{:t} command to see their types:
139\texttt{:t} command to see their types:
171
140
172−\begin{SaveVerbatim}{showmetas}
141+\begin{lstlisting}
173−
174*theorems> :m
142*theorems> :m
175Global metavariables:
143Global metavariables:
176 [plusredZ_S,plusredZ_Z]
144 [plusredZ_S,plusredZ_Z]
177
145
178−\end{SaveVerbatim}
146+\end{lstlisting}
179−
180−\begin{SaveVerbatim}{metatypes}
181
147
148+\begin{lstlisting}
182*theorems> :t plusredZ_Z
149*theorems> :t plusredZ_Z
183plusredZ_Z : Z = plus Z Z
150plusredZ_Z : Z = plus Z Z
184
151
185*theorems> :t plusredZ_S
152*theorems> :t plusredZ_S
186plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
153plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
187−
154+\end{lstlisting}
188−\end{SaveVerbatim}
189−\useverb{showmetas}
190−
191−\useverb{metatypes}
192
155
193\noindent
156\noindent
194The \texttt{:p} command enters interactive proof mode, which can be used to complete
157The \texttt{:p} command enters interactive proof mode, which can be used to complete
195the missing definitions.
158the missing definitions.
196
159
197−\begin{SaveVerbatim}{proveO}
160+\begin{lstlisting}
198−
199*theorems> :p plusredZ_Z
161*theorems> :p plusredZ_Z
200
162
201---------------------------------- (plusredZ_Z) --------
163---------------------------------- (plusredZ_Z) --------
202{hole0} : Z = plus Z Z
164{hole0} : Z = plus Z Z
203−
165+\end{lstlisting}
204−\end{SaveVerbatim}
205−\useverb{proveO}
206
166
207\noindent
167\noindent
208This gives us a list of premisses
168This gives us a list of premisses
@@ -211,15 +171,12 @@ named \texttt{\{hole0\}} here).
211At the prompt we can enter tactics to direct the construction of the proof. In this case,
171At the prompt we can enter tactics to direct the construction of the proof. In this case,
212we can normalise the goal with the \texttt{compute} tactic:
172we can normalise the goal with the \texttt{compute} tactic:
213
173
214−\begin{SaveVerbatim}{compute}
174+\begin{lstlisting}
215−
216-plusredZ_Z> compute
175-plusredZ_Z> compute
217
176
218---------------------------------- (plusredZ_Z) --------
177---------------------------------- (plusredZ_Z) --------
219{hole0} : Z = Z
178{hole0} : Z = Z
220−
179+\end{lstlisting}
221−\end{SaveVerbatim}
222−\useverb{compute}
223
180
224\noindent
181\noindent
225Now we have to prove that \texttt{Z} equals \texttt{Z}, which is easy to prove by
182Now we have to prove that \texttt{Z} equals \texttt{Z}, which is easy to prove by
@@ -227,13 +184,10 @@ Now we have to prove that \texttt{Z} equals \texttt{Z}, which is easy to prove b
227which introduces subgoals for each of the function's explicit arguments (\texttt{refl}
184which introduces subgoals for each of the function's explicit arguments (\texttt{refl}
228has none):
185has none):
229
186
230−\begin{SaveVerbatim}{refrefl}
187+\begin{lstlisting}
231−
232-plusredZ_Z> refine refl
188-plusredZ_Z> refine refl
233plusredZ_Z: no more goals
189plusredZ_Z: no more goals
234−
190+\end{lstlisting}
235−\end{SaveVerbatim}
236−\useverb{refrefl}
237
191
238\noindent
192\noindent
239Here, we could also have used the \texttt{trivial} tactic, which tries to refine by
193Here, we could also have used the \texttt{trivial} tactic, which tries to refine by
@@ -242,40 +196,31 @@ When a proof is complete, we use the \texttt{qed} tactic to add the proof to the
242global context, and remove the metavariable from the unsolved metavariables list.
196global context, and remove the metavariable from the unsolved metavariables list.
243This also outputs a trace of the proof:
197This also outputs a trace of the proof:
244
198
245−\begin{SaveVerbatim}{prOprooftrace}
199+\begin{code}
246−
247-plusredZ_Z> qed
200-plusredZ_Z> qed
248plusredZ_Z = proof {
201plusredZ_Z = proof {
249 compute;
202 compute;
250 refine refl;
203 refine refl;
251}
204}
205+\end{code}
252
206
253−\end{SaveVerbatim}
207+\begin{lstlisting}
254−\useverb{prOprooftrace}
255−
256−\begin{SaveVerbatim}{showmetasO}
257−
258*theorems> :m
208*theorems> :m
259Global metavariables:
209Global metavariables:
260 [plusredZ_S]
210 [plusredZ_S]
261−
211+\end{lstlisting}
262−\end{SaveVerbatim}
263−\useverb{showmetasO}
264
212
265\noindent
213\noindent
266The \texttt{:addproof} command, at the interactive prompt, will add the proof to
214The \texttt{:addproof} command, at the interactive prompt, will add the proof to
267the source file (effectively in an appendix).
215the source file (effectively in an appendix).
268Let us now prove the other required lemma, \texttt{plusredZ\_S}:
216Let us now prove the other required lemma, \texttt{plusredZ\_S}:
269
217
270−\begin{SaveVerbatim}{plusredZSprf}
218+\begin{lstlisting}
271−
272*theorems> :p plusredZ_S
219*theorems> :p plusredZ_S
273
220
274---------------------------------- (plusredZ_S) --------
221---------------------------------- (plusredZ_S) --------
275{hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
222{hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
276−
223+\end{lstlisting}
277−\end{SaveVerbatim}
278−\useverb{plusredZSprf}
279
224
280\noindent
225\noindent
281In this case, the goal is a function type, using \texttt{k} (the argument accessible by
226In this case, the goal is a function type, using \texttt{k} (the argument accessible by
@@ -283,37 +228,31 @@ pattern matching) and \texttt{ih} (the local variable containing the result of
283the recursive call). We can introduce these as premisses using the \texttt{intro} tactic
228the recursive call). We can introduce these as premisses using the \texttt{intro} tactic
284twice (or \texttt{intros}, which introduces all arguments as premisses). This gives:
229twice (or \texttt{intros}, which introduces all arguments as premisses). This gives:
285
230
286−\begin{SaveVerbatim}{prSintros}
231+\begin{lstlisting}
287−
288 k : Nat
232 k : Nat
289 ih : k = plus k Z
233 ih : k = plus k Z
290---------------------------------- (plusredZ_S) --------
234---------------------------------- (plusredZ_S) --------
291{hole2} : S k = plus (S k) Z
235{hole2} : S k = plus (S k) Z
292−
236+\end{lstlisting}
293−\end{SaveVerbatim}
294−\useverb{prSintros}
295
237
296\noindent
238\noindent
297Since plus is defined is defined by recursion on its first argument, the term
239Since plus is defined is defined by recursion on its first argument, the term
298\texttt{plus (S k) Z} in the goal can be simplified, so we use
240\texttt{plus (S k) Z} in the goal can be simplified, so we use
299\texttt{compute}.
241\texttt{compute}.
300
242
301−\begin{SaveVerbatim}{prScompute}
243+\begin{lstlisting}
302 k : Nat
244 k : Nat
303 ih : k = plus k Z
245 ih : k = plus k Z
304---------------------------------- (plusredZ_S) --------
246---------------------------------- (plusredZ_S) --------
305{hole2} : S k = S (plus k Z)
247{hole2} : S k = S (plus k Z)
306−
248+\end{lstlisting}
307−\end{SaveVerbatim}
308−\useverb{prScompute}
309
249
310\noindent
250\noindent
311We know, from the type of \texttt{ih}, that \texttt{k = plus k Z}, so we would like to
251We know, from the type of \texttt{ih}, that \texttt{k = plus k Z}, so we would like to
312use this knowledge to replace \texttt{plus k Z} in the goal with \texttt{k}. We can
252use this knowledge to replace \texttt{plus k Z} in the goal with \texttt{k}. We can
313achieve this with the \texttt{rewrite} tactic:
253achieve this with the \texttt{rewrite} tactic:
314
254
315−\begin{SaveVerbatim}{}
255+\begin{lstlisting}
316−
317-plusredZ_S> rewrite ih
256-plusredZ_S> rewrite ih
318
257
319 k : Nat
258 k : Nat
@@ -322,16 +261,13 @@ achieve this with the \texttt{rewrite} tactic:
322{hole3} : S k = S k
261{hole3} : S k = S k
323
262
324-plusredZ_S>
263-plusredZ_S>
325−
264+\end{lstlisting}
326−\end{SaveVerbatim}
327−\useverb{}
328
265
329\noindent
266\noindent
330The \texttt{rewrite} tactic takes an equality proof as an argument, and tries to rewrite
267The \texttt{rewrite} tactic takes an equality proof as an argument, and tries to rewrite
331the goal using that proof. Here, it results in an equality which is trivially provable:
268the goal using that proof. Here, it results in an equality which is trivially provable:
332
269
333−\begin{SaveVerbatim}{prOStrace}
270+\begin{lstlisting}
334−
335-plusredZ_S> trivial
271-plusredZ_S> trivial
336plusredZ_S: no more goals
272plusredZ_S: no more goals
337-plusredZ_S> qed
273-plusredZ_S> qed
@@ -340,9 +276,7 @@ plusredZ_S = proof {
340 rewrite ih;
276 rewrite ih;
341 trivial;
277 trivial;
342}
278}
343−
279+\end{lstlisting}
344−\end{SaveVerbatim}
345−\useverb{prOStrace}
346
280
347\noindent
281\noindent
348Again, we can add this proof to the end of our source file using the \texttt{:addproof}
282Again, we can add this proof to the end of our source file using the \texttt{:addproof}
@@ -357,8 +291,7 @@ If we really want to trust our proofs, it is important that they are defined by
357possible inputs and is guaranteed to terminate. Otherwise we could construct an
291possible inputs and is guaranteed to terminate. Otherwise we could construct an
358element of the empty type, from which we could prove anything:
292element of the empty type, from which we could prove anything:
359
293
360−\begin{SaveVerbatim}{empties}
294+\begin{code}
361−
362-- making use of 'hd' being partially defined
295-- making use of 'hd' being partially defined
363empty1 : _|_
296empty1 : _|_
364empty1 = hd [] where
297empty1 = hd [] where
@@ -368,25 +301,20 @@ empty1 = hd [] where
368-- not terminating
301-- not terminating
369empty2 : _|_
302empty2 : _|_
370empty2 = empty2
303empty2 = empty2
371−
304+\end{code}
372−\end{SaveVerbatim}
373−\useverb{empties}
374
305
375\noindent
306\noindent
376Internally, \Idris{} checks every definition for totality, and we can check at
307Internally, \Idris{} checks every definition for totality, and we can check at
377the prompt with the \texttt{:total} command. We see that neither of the above
308the prompt with the \texttt{:total} command. We see that neither of the above
378definitions is total:
309definitions is total:
379
310
380−\begin{SaveVerbatim}{totalcheck}
311+\begin{lstlisting}
381−
382*theorems> :total empty1
312*theorems> :total empty1
383possibly not total due to: empty1#hd
313possibly not total due to: empty1#hd
384 not total as there are missing cases
314 not total as there are missing cases
385*theorems> :total empty2
315*theorems> :total empty2
386possibly not total due to recursive path empty2
316possibly not total due to recursive path empty2
387−
317+\end{lstlisting}
388−\end{SaveVerbatim}
389−\useverb{totalcheck}
390
318
391\noindent
319\noindent
392Note the use of the word ``possibly'' --- a totality check can, of course,
320Note the use of the word ``possibly'' --- a totality check can, of course,
@@ -395,28 +323,22 @@ is, therefore, conservative. It is also possible (and indeed advisable, in the
395case of proofs) to mark functions as total so that it will be a compile time
323case of proofs) to mark functions as total so that it will be a compile time
396error for the totality check to fail:
324error for the totality check to fail:
397
325
398−\begin{SaveVerbatim}{emptyfail}
326+\begin{lstlisting}
399−
400total empty2 : _|_
327total empty2 : _|_
401empty2 = empty2
328empty2 = empty2
402
329
403Type checking ./theorems.idr
330Type checking ./theorems.idr
404theorems.idr:25:empty2 is possibly not total due to recursive path empty2
331theorems.idr:25:empty2 is possibly not total due to recursive path empty2
405−
332+\end{lstlisting}
406−\end{SaveVerbatim}
407−\useverb{emptyfail}
408
333
409\noindent
334\noindent
410Reassuringly, our proof in Section \ref{sect:empty} that the zero and successor constructors
335Reassuringly, our proof in Section \ref{sect:empty} that the zero and successor constructors
411are disjoint is total:
336are disjoint is total:
412
337
413−\begin{SaveVerbatim}{totdisjoint}
338+\begin{lstlisting}
414−
415*theorems> :total disjoint
339*theorems> :total disjoint
416Total
340Total
417−
341+\end{lstlisting}
418−\end{SaveVerbatim}
419−\useverb{totdisjoint}
420
342
421\noindent
343\noindent
422The totality check is, necessarily, conservative. To be recorded as total, a
344The totality check is, necessarily, conservative. To be recorded as total, a
tutorial/typesfuns.tex → tutorial/content/typesfuns.texrenamed+142−305
@@ -11,8 +11,7 @@ We can declare some constants with these types. Enter the following
11into a file \texttt{prims.idr} and load it into the \Idris{} interactive
11into a file \texttt{prims.idr} and load it into the \Idris{} interactive
12environment by typing \texttt{idris prims.idr}:
12environment by typing \texttt{idris prims.idr}:
13
13
14−\begin{SaveVerbatim}{constprims}
14+\begin{code}
15−
16module prims
15module prims
17
16
18x : Int
17x : Int
@@ -26,9 +25,7 @@ bar = 'Z'
26
25
27quux : Bool
26quux : Bool
28quux = False
27quux = False
29−
28+\end{code}
30−\end{SaveVerbatim}
31−\useverb{constprims}
32
29
33\noindent
30\noindent
34An \Idris{} file consists of an optional module declaration (here
31An \Idris{} file consists of an optional module declaration (here
@@ -50,15 +47,12 @@ functions. The prelude defines several arithmetic and comparison operators,
50which we can use at the prompt. Evaluating things at the prompt gives an
47which we can use at the prompt. Evaluating things at the prompt gives an
51answer, and the type of the answer. For example:
48answer, and the type of the answer. For example:
52
49
53−\begin{SaveVerbatim}{promptprim}
50+\begin{lstlisting}
54−
55*prims> 6*6+6
51*prims> 6*6+6
5642 : Int
5242 : Int
57*prims> x == 6*6+6
53*prims> x == 6*6+6
58True : Bool
54True : Bool
59−
55+\end{lstlisting}
60−\end{SaveVerbatim}
61−\useverb{promptprim}
62
56
63\noindent
57\noindent
64All of the usual arithmetic and comparison operators are defined for the primitive
58All of the usual arithmetic and comparison operators are defined for the primitive
@@ -66,27 +60,21 @@ types. They are overloaded using type classes, as we will discuss in Section
66\ref{sec:classes} and can be extended to work on user defined types.
60\ref{sec:classes} and can be extended to work on user defined types.
67Boolean expressions can be tested with the \texttt{if...then...else} construct:
61Boolean expressions can be tested with the \texttt{if...then...else} construct:
68
62
69−\begin{SaveVerbatim}{ifthenelse}
63+\begin{lstlisting}
70−
71*prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer"
64*prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer"
72"The answer!" : String
65"The answer!" : String
73−
66+\end{lstlisting}
74−\end{SaveVerbatim}
75−\useverb{ifthenelse}
76
67
77\subsection{Data Types}
68\subsection{Data Types}
78
69
79Data types are declared in a similar way to Haskell data types, with a similar
70Data types are declared in a similar way to Haskell data types, with a similar
80syntax. Natural numbers and lists, for example, can be declared as follows:
71syntax. Natural numbers and lists, for example, can be declared as follows:
81
72
82−\begin{SaveVerbatim}{natlist}
73+\begin{code}
83−
84data Nat = Z | S Nat -- Natural numbers
74data Nat = Z | S Nat -- Natural numbers
85 -- (zero and successor)
75 -- (zero and successor)
86data List a = Nil | (::) a (List a) -- Polymorphic lists
76data List a = Nil | (::) a (List a) -- Polymorphic lists
87−
77+\end{code}
88−\end{SaveVerbatim}
89−\useverb{natlist}
90
78
91\noindent
79\noindent
92The above declarations are taken from the standard library. Unary natural
80The above declarations are taken from the standard library. Unary natural
@@ -97,28 +85,18 @@ or a value added to the front of another list (\texttt{x :: xs}).
97In the declaration for \tTC{List}, we used an infix operator \tDC{::}. New operators
85In the declaration for \tTC{List}, we used an infix operator \tDC{::}. New operators
98such as this can be added using a fixity declaration, as follows:
86such as this can be added using a fixity declaration, as follows:
99
87
100−\begin{SaveVerbatim}{infixcons}
88+\begin{code}
101−
102infixr 10 ::
89infixr 10 ::
103−
90+\end{code}
104−\end{SaveVerbatim}
105−\useverb{infixcons}
106
91
107\noindent
92\noindent
108Functions, data constructors and type constuctors may all be given infix
93Functions, data constructors and type constuctors may all be given infix
109operators as names. They may be used in prefix form if enclosed in brackets,
94operators as names. They may be used in prefix form if enclosed in brackets,
110e.g. \tDC{(::)}. Infix operators can use any of the symbols:
95e.g. \tDC{(::)}. Infix operators can use any of the symbols:
111
96
112−\begin{SaveVerbatim}{infixsyms}
97+\begin{lstlisting}
113−
114:+-*/=_.?|&><!@$%^~.
98:+-*/=_.?|&><!@$%^~.
115−
99+\end{lstlisting}
116−\end{SaveVerbatim}
117−\useverb{infixsyms}
118−
119−\begin{SaveVerbatim}{argh}
120−$
121−\end{SaveVerbatim}
122
100
123\subsection{Functions}
101\subsection{Functions}
124
102
@@ -128,8 +106,7 @@ functions, using a single colon \texttt{:} (rather than
128Haskell's double colon \texttt{::}). Some natural number arithmetic functions can be
106Haskell's double colon \texttt{::}). Some natural number arithmetic functions can be
129defined as follows, again taken from the standard library:
107defined as follows, again taken from the standard library:
130
108
131−\begin{SaveVerbatim}{natfns}
109+\begin{code}
132−
133-- Unary addition
110-- Unary addition
134plus : Nat -> Nat -> Nat
111plus : Nat -> Nat -> Nat
135plus Z y = y
112plus Z y = y
@@ -139,9 +116,7 @@ plus (S k) y = S (plus k y)
139mult : Nat -> Nat -> Nat
116mult : Nat -> Nat -> Nat
140mult Z y = Z
117mult Z y = Z
141mult (S k) y = plus y (mult k y)
118mult (S k) y = plus y (mult k y)
142−
119+\end{code}
143−\end{SaveVerbatim}
144−\useverb{natfns}
145
120
146\noindent
121\noindent
147The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded
122The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded
@@ -154,29 +129,23 @@ all part of the same namespace.
154
129
155We can test these functions at the \Idris{} prompt:
130We can test these functions at the \Idris{} prompt:
156
131
157−\begin{SaveVerbatim}{fntest}
132+\begin{lstlisting}
158−
159Idris> plus (S (S Z)) (S (S Z))
133Idris> plus (S (S Z)) (S (S Z))
160S (S (S (S Z))) : Nat
134S (S (S (S Z))) : Nat
161Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
135Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
162S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : Nat
136S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : Nat
163−
137+\end{lstlisting}
164−\end{SaveVerbatim}
165−\useverb{fntest}
166
138
167\noindent
139\noindent
168Like arithmetic operations, integer literals are also overloaded using type classes,
140Like arithmetic operations, integer literals are also overloaded using type classes,
169meaning that we can also test the functions as follows:
141meaning that we can also test the functions as follows:
170
142
171−\begin{SaveVerbatim}{fntest}
143+\begin{lstlisting}
172−
173Idris> plus 2 2
144Idris> plus 2 2
174S (S (S (S Z))) : Nat
145S (S (S (S Z))) : Nat
175Idris> mult 3 (plus 2 2)
146Idris> mult 3 (plus 2 2)
176S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : Nat
147S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : Nat
177−
148+\end{lstlisting}
178−\end{SaveVerbatim}
179−\useverb{fntest}
180
149
181\noindent
150\noindent
182You may wonder, by the way, why we have unary natural numbers when our
151You may wonder, by the way, why we have unary natural numbers when our
@@ -194,16 +163,13 @@ Functions can also be defined \emph{locally} using \texttt{where} clauses. For e
194to define a function which reverses a list, we can use an auxiliary function which
163to define a function which reverses a list, we can use an auxiliary function which
195accumulates the new, reversed list, and which does not need to be visible globally:
164accumulates the new, reversed list, and which does not need to be visible globally:
196
165
197−\begin{SaveVerbatim}{revwhere}
166+\begin{code}
198−
199reverse : List a -> List a
167reverse : List a -> List a
200reverse xs = revAcc [] xs where
168reverse xs = revAcc [] xs where
201 revAcc : List a -> List a -> List a
169 revAcc : List a -> List a -> List a
202 revAcc acc [] = acc
170 revAcc acc [] = acc
203 revAcc acc (x :: xs) = revAcc (x :: acc) xs
171 revAcc acc (x :: xs) = revAcc (x :: acc) xs
204−
172+\end{code}
205−\end{SaveVerbatim}
206−\useverb{revwhere}
207
173
208\noindent
174\noindent
209Indentation is significant --- functions in the \texttt{where} block must be indented
175Indentation is significant --- functions in the \texttt{where} block must be indented
@@ -220,8 +186,7 @@ As well as functions, \texttt{where} blocks can include local data
220declarations, such as the following where \texttt{MyLT} is not accessible outside
186declarations, such as the following where \texttt{MyLT} is not accessible outside
221the definition of \texttt{foo}:
187the definition of \texttt{foo}:
222
188
223−\begin{SaveVerbatim}{wheredata}
189+\begin{code}
224−
225foo : Int -> Int
190foo : Int -> Int
226foo x = case isLT of
191foo x = case isLT of
227 Yes => x*2
192 Yes => x*2
@@ -231,9 +196,7 @@ foo x = case isLT of
231
196
232 isLT : MyLT
197 isLT : MyLT
233 isLT = if x < 20 then Yes else No
198 isLT = if x < 20 then Yes else No
234−
199+\end{code}
235−\end{SaveVerbatim}
236−\useverb{wheredata}
237
200
238\noindent
201\noindent
239In general, functions defined in a \texttt{where} clause need a type declaration
202In general, functions defined in a \texttt{where} clause need a type declaration
@@ -249,8 +212,7 @@ application
249\noindent
212\noindent
250So, for example, the following definitions are legal:
213So, for example, the following definitions are legal:
251
214
252−\begin{SaveVerbatim}{whereinfer}
215+\begin{code}
253−
254even : Nat -> Bool
216even : Nat -> Bool
255even Z = True
217even Z = True
256even (S k) = odd k where
218even (S k) = odd k where
@@ -262,10 +224,7 @@ test = [c (S 1), c Z, d (S Z)]
262 where c x = 42 + x
224 where c x = 42 + x
263 d y = c (y + 1 + z y)
225 d y = c (y + 1 + z y)
264 where z w = y + w
226 where z w = y + w
265−
227+\end{code}
266−\end{SaveVerbatim}
267−\useverb{whereinfer}
268−
269
228
270\subsection{Dependent Types}
229\subsection{Dependent Types}
271
230
@@ -276,14 +235,11 @@ conventionally called vectors in the dependent type literature. In \Idris{},
276we declare vectors as follows\footnote{Note that prior to \Idris{} 0.9.9,
235we declare vectors as follows\footnote{Note that prior to \Idris{} 0.9.9,
277the order of the arguments to \texttt{Vect} was reversed.}:
236the order of the arguments to \texttt{Vect} was reversed.}:
278
237
279−\begin{SaveVerbatim}{vect}
238+\begin{code}
280−
281data Vect : Nat -> Type -> Type where
239data Vect : Nat -> Type -> Type where
282 Nil : Vect Z a
240 Nil : Vect Z a
283 (::) : a -> Vect k a -> Vect (S k) a
241 (::) : a -> Vect k a -> Vect (S k) a
284−
242+\end{code}
285−\end{SaveVerbatim}
286−\useverb{vect}
287
243
288\noindent
244\noindent
289Note that we have used the same constructor names as for \tTC{List}. Ad-hoc
245Note that we have used the same constructor names as for \tTC{List}. Ad-hoc
@@ -308,42 +264,31 @@ The type of a function over \tTC{Vect} will describe what happens to the
308lengths of the vectors involved. For example, \tFN{++}, defined in the
264lengths of the vectors involved. For example, \tFN{++}, defined in the
309library, appends two \tTC{Vect}s:
265library, appends two \tTC{Vect}s:
310
266
311−\begin{SaveVerbatim}{vapp}
267+\begin{code}
312−
313(++) : Vect n a -> Vect m a -> Vect (n + m) a
268(++) : Vect n a -> Vect m a -> Vect (n + m) a
314(++) Nil ys = ys
269(++) Nil ys = ys
315(++) (x :: xs) ys = x :: xs ++ ys
270(++) (x :: xs) ys = x :: xs ++ ys
316−
271+\end{code}
317−\end{SaveVerbatim}
318−\useverb{vapp}
319
272
320\noindent
273\noindent
321The type of \tFN{(++)} states that the resulting vector's length will be the sum of
274The type of \tFN{(++)} states that the resulting vector's length will be the sum of
322the input lengths. If we get the definition wrong in such a way that this does
275the input lengths. If we get the definition wrong in such a way that this does
323not hold, \Idris{} will not accept the definition. For example:
276not hold, \Idris{} will not accept the definition. For example:
324
277
325−\begin{SaveVerbatim}{vapperr}
278+\begin{code}
326−
327(++) : Vect n a -> Vect m a -> Vect (n + m) a
279(++) : Vect n a -> Vect m a -> Vect (n + m) a
328(++) Nil ys = ys
280(++) Nil ys = ys
329(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
281(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
282+\end{code}
330
283
331−\end{SaveVerbatim}
284+\begin{lstlisting}
332−\useverb{vapperr}
333−
334−\begin{SaveVerbatim}{vapperrmsg}
335−
336$ idris vbroken.idr --check
285$ idris vbroken.idr --check
337vbroken.idr:3:Can't unify Vect n a with Vect m a
286vbroken.idr:3:Can't unify Vect n a with Vect m a
338
287
339Specifically:
288Specifically:
340 Can't unify n with m
289 Can't unify n with m
290+\end{lstlisting}
341
291
342−\end{SaveVerbatim}
343−\begin{SaveVerbatim}{bleh}
344−$
345−\end{SaveVerbatim}
346−\useverb{vapperrmsg}
347
292
348\noindent
293\noindent
349This error message suggests that there is a length mismatch between two vectors
294This error message suggests that there is a length mismatch between two vectors
@@ -357,14 +302,11 @@ of length \texttt{n}.
357Finite sets, as the name suggests, are sets with a finite number of elements.
302Finite sets, as the name suggests, are sets with a finite number of elements.
358They are declared as follows (again, in the prelude):
303They are declared as follows (again, in the prelude):
359
304
360−\begin{SaveVerbatim}{findecl}
305+\begin{code}
361−
362data Fin : Nat -> Type where
306data Fin : Nat -> Type where
363 fZ : Fin (S k)
307 fZ : Fin (S k)
364 fS : Fin k -> Fin (S k)
308 fS : Fin k -> Fin (S k)
365−
309+\end{code}
366−\end{SaveVerbatim}
367−\useverb{findecl}
368
310
369\noindent
311\noindent
370\tDC{fZ} is the zeroth element of a finite set with \texttt{S k} elements;
312\tDC{fZ} is the zeroth element of a finite set with \texttt{S k} elements;
@@ -382,14 +324,11 @@ numbers bounded by \tTC{n}.
382For example, the following function which looks up an element in a \tTC{Vect},
324For example, the following function which looks up an element in a \tTC{Vect},
383by a bounded index given as a \tTC{Fin n}, is defined in the prelude:
325by a bounded index given as a \tTC{Fin n}, is defined in the prelude:
384
326
385−\begin{SaveVerbatim}{vindex}
327+\begin{code}
386−
387index : Fin n -> Vect n a -> a
328index : Fin n -> Vect n a -> a
388index fZ (x :: xs) = x
329index fZ (x :: xs) = x
389index (fS k) (x :: xs) = index k xs
330index (fS k) (x :: xs) = index k xs
390−
331+\end{code}
391−\end{SaveVerbatim}
392−\useverb{vindex}
393
332
394\noindent
333\noindent
395This function looks up a value at a given location in a vector. The location is
334This function looks up a value at a given location in a vector. The location is
@@ -407,12 +346,9 @@ since it would force \texttt{n} to be \tDC{Z}.
407
346
408Let us take a closer look at the type of \texttt{index}:
347Let us take a closer look at the type of \texttt{index}:
409
348
410−\begin{SaveVerbatim}{vindexty}
349+\begin{code}
411−
412index : Fin n -> Vect n a -> a
350index : Fin n -> Vect n a -> a
413−
351+\end{code}
414−\end{SaveVerbatim}
415−\useverb{vindexty}
416
352
417\noindent
353\noindent
418It takes two arguments, an element of the finite set of \texttt{n} elements, and a vector
354It takes two arguments, an element of the finite set of \texttt{n} elements, and a vector
@@ -420,12 +356,9 @@ with \texttt{n} elements of type \texttt{a}. But there are also two names,
420\texttt{n} and \texttt{a}, which are not declared explictly. These are \emph{implicit}
356\texttt{n} and \texttt{a}, which are not declared explictly. These are \emph{implicit}
421arguments to \texttt{index}. We could also write the type of \texttt{index} as:
357arguments to \texttt{index}. We could also write the type of \texttt{index} as:
422
358
423−\begin{SaveVerbatim}{vindeximpty}
359+\begin{code}
424−
425index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
360index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
426−
361+\end{code}
427−\end{SaveVerbatim}
428−\useverb{vindeximpty}
429
362
430\noindent
363\noindent
431Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are
364Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are
@@ -437,23 +370,17 @@ free, will be automatically bound as an implicit argument. Implicit arguments
437can still be given explicitly in applications, using \texttt{\{a=value\}} and
370can still be given explicitly in applications, using \texttt{\{a=value\}} and
438\texttt{\{n=value\}}, for example:
371\texttt{\{n=value\}}, for example:
439
372
440−\begin{SaveVerbatim}{vindexexp}
373+\begin{code}
441−
442index {a=Int} {n=2} fZ (2 :: 3 :: Nil)
374index {a=Int} {n=2} fZ (2 :: 3 :: Nil)
443−
375+\end{code}
444−\end{SaveVerbatim}
445−\useverb{vindexexp}
446
376
447\noindent
377\noindent
448In fact, any argument, implicit or explicit, may be given a name. We could have
378In fact, any argument, implicit or explicit, may be given a name. We could have
449declared the type of \texttt{index} as:
379declared the type of \texttt{index} as:
450
380
451−\begin{SaveVerbatim}{vindexn}
381+\begin{code}
452−
453index : (i:Fin n) -> (xs:Vect n a) -> a
382index : (i:Fin n) -> (xs:Vect n a) -> a
454−
383+\end{code}
455−\end{SaveVerbatim}
456−\useverb{vindexn}
457
384
458\noindent
385\noindent
459It is a matter of taste whether you want to do this --- sometimes it can help
386It is a matter of taste whether you want to do this --- sometimes it can help
@@ -468,14 +395,11 @@ before being used --- or if an implicit argument has a complex type. For example
468we will need to state the types of the implicit arguments in the following
395we will need to state the types of the implicit arguments in the following
469definition, which defines a predicate on vectors:
396definition, which defines a predicate on vectors:
470
397
471−\begin{SaveVerbatim}{elem}
398+\begin{code}
472−
473data Elem : a -> Vect n a -> Type where
399data Elem : a -> Vect n a -> Type where
474 here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
400 here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
475 there : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)
401 there : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)
476−
402+\end{code}
477−\end{SaveVerbatim}
478−\useverb{elem}
479
403
480\noindent
404\noindent
481An instance of \texttt{Elem x xs} states that \texttt{x} is an element of
405An instance of \texttt{Elem x xs} states that \texttt{x} is an element of
@@ -483,31 +407,26 @@ An instance of \texttt{Elem x xs} states that \texttt{x} is an element of
483such a predicate if the required element is \texttt{here}, at the head of the vector,
407such a predicate if the required element is \texttt{here}, at the head of the vector,
484or \texttt{there}, in the tail of the vector. For example:
408or \texttt{there}, in the tail of the vector. For example:
485
409
486−\begin{SaveVerbatim}{testelem}
410+\begin{code}
487−
488testVec : Vect 4 Int
411testVec : Vect 4 Int
489testVec = 3 :: 4 :: 5 :: 6 :: Nil
412testVec = 3 :: 4 :: 5 :: 6 :: Nil
490
413
491inVect : Elem 5 testVec
414inVect : Elem 5 testVec
492inVect = there (there here)
415inVect = there (there here)
493−
416+\end{code}
494−\end{SaveVerbatim}
495−\useverb{testelem}
496
417
497\noindent
418\noindent
498If the same implicit arguments are being used a lot, it can make a definition
419If the same implicit arguments are being used a lot, it can make a definition
499difficult to read. To avoid this problem, a \texttt{using} block gives the types and
420difficult to read. To avoid this problem, a \texttt{using} block gives the types and
500ordering of any implicit arguments which can appear within the block:
421ordering of any implicit arguments which can appear within the block:
501
422
502−\begin{SaveVerbatim}{elemusing}
423+\begin{code}
503−
504using (x:a, y:a, xs:Vect n a)
424using (x:a, y:a, xs:Vect n a)
505 data Elem : a -> Vect n a -> Type where
425 data Elem : a -> Vect n a -> Type where
506 here : Elem x (x :: xs)
426 here : Elem x (x :: xs)
507 there : Elem x xs -> Elem x (y :: xs)
427 there : Elem x xs -> Elem x (y :: xs)
428+\end{code}
508
429
509−\end{SaveVerbatim}
510−\useverb{elemusing}
511
430
512\subsubsection*{Note: Declaration Order and \texttt{mutual} blocks}
431\subsubsection*{Note: Declaration Order and \texttt{mutual} blocks}
513
432
@@ -517,8 +436,7 @@ reduction behaviour to affect type checking. However, this
517restriction can be relaxed by using a \texttt{mutual} block, which allows
436restriction can be relaxed by using a \texttt{mutual} block, which allows
518data types and functions to be defined simultaneously:
437data types and functions to be defined simultaneously:
519
438
520−\begin{SaveVerbatim}{mutual}
439+\begin{code}
521−
522mutual
440mutual
523 even : Nat -> Bool
441 even : Nat -> Bool
524 even Z = True
442 even Z = True
@@ -527,9 +445,8 @@ mutual
527 odd : Nat -> Bool
445 odd : Nat -> Bool
528 odd Z = False
446 odd Z = False
529 odd (S k) = even k
447 odd (S k) = even k
448+\end{code}
530
449
531−\end{SaveVerbatim}
532−\useverb{mutual}
533
450
534\noindent
451\noindent
535In a \texttt{mutual} block, first all of the type declarations are added,
452In a \texttt{mutual} block, first all of the type declarations are added,
@@ -544,12 +461,10 @@ that is, a language where expressions do not have side-effects --- is that I/O
544is inherently side-effecting. Therefore in \Idris{}, such interactions are
461is inherently side-effecting. Therefore in \Idris{}, such interactions are
545encapsulated in the type \texttt{IO}:
462encapsulated in the type \texttt{IO}:
546
463
547−\begin{SaveVerbatim}{ioty}
464+\begin{code}
548−
549data IO a -- IO operation returning a value of type a
465data IO a -- IO operation returning a value of type a
466+\end{code}
550
467
551−\end{SaveVerbatim}
552−\useverb{ioty}
553
468
554\noindent
469\noindent
555We'll leave the definition of \texttt{IO} abstract, but effectively it describes what
470We'll leave the definition of \texttt{IO} abstract, but effectively it describes what
@@ -558,41 +473,34 @@ resulting operations are executed externally,
558by the run-time system. We've already seen one IO
473by the run-time system. We've already seen one IO
559program:
474program:
560
475
561−\begin{SaveVerbatim}{main}
476+\begin{code}
562−
563main : IO ()
477main : IO ()
564main = putStrLn "Hello world"
478main = putStrLn "Hello world"
479+\end{code}
565
480
566−\end{SaveVerbatim}
567−\useverb{main}
568
481
569\noindent
482\noindent
570The type of \texttt{putStrLn} explains that it takes a string, and returns an
483The type of \texttt{putStrLn} explains that it takes a string, and returns an
571element of the unit type () via an I/O action. There is a variant \texttt{putStr} which
484element of the unit type () via an I/O action. There is a variant \texttt{putStr} which
572outputs a string without a newline:
485outputs a string without a newline:
573
486
574−\begin{SaveVerbatim}{putstr}
487+\begin{code}
575−
576putStrLn : String -> IO ()
488putStrLn : String -> IO ()
577putStr : String -> IO ()
489putStr : String -> IO ()
578−
490+\end{code}
579−\end{SaveVerbatim}
580
491
581We can also read strings from user input:
492We can also read strings from user input:
582
493
583−\begin{SaveVerbatim}{getline}
494+\begin{code}
584−
585getLine : IO String
495getLine : IO String
496+\end{code}
586
497
587−\end{SaveVerbatim}
588−\useverb{getline}
589
498
590\noindent
499\noindent
591A number of other I/O operations are defined in the prelude, for example for reading and
500A number of other I/O operations are defined in the prelude, for example for reading and
592writing files, including:
501writing files, including:
593
502
594−\begin{SaveVerbatim}{fileops}
503+\begin{code}
595−
596data File -- abstract
504data File -- abstract
597data Mode = Read | Write | ReadWrite
505data Mode = Read | Write | ReadWrite
598
506
@@ -604,9 +512,8 @@ fwrite : File -> String -> IO ()
604feof : File -> IO Bool
512feof : File -> IO Bool
605
513
606readFile : String -> IO String
514readFile : String -> IO String
515+\end{code}
607
516
608−\end{SaveVerbatim}
609−\useverb{fileops}
610
517
611\subsection{``\texttt{do}'' notation}
518\subsection{``\texttt{do}'' notation}
612
519
@@ -617,15 +524,13 @@ computation into the input of the next. \texttt{IO} is an abstract type, however
617can't access the result of a computation directly. Instead, we sequence
524can't access the result of a computation directly. Instead, we sequence
618operations with \texttt{do} notation:
525operations with \texttt{do} notation:
619
526
620−\begin{SaveVerbatim}{greet}
527+\begin{code}
621−
622greet : IO ()
528greet : IO ()
623greet = do putStr "What is your name? "
529greet = do putStr "What is your name? "
624 name <- getLine
530 name <- getLine
625 putStrLn ("Hello " ++ name)
531 putStrLn ("Hello " ++ name)
532+\end{code}
626
533
627−\end{SaveVerbatim}
628−\useverb{greet}
629
534
630\noindent
535\noindent
631The syntax \texttt{x <- iovalue} executes the I/O operation \texttt{iovalue}, of type
536The syntax \texttt{x <- iovalue} executes the I/O operation \texttt{iovalue}, of type
@@ -637,12 +542,10 @@ statement in the do block must begin in the same column.
637The \texttt{return} operation allows us to inject a value directly into an IO
542The \texttt{return} operation allows us to inject a value directly into an IO
638operation:
543operation:
639
544
640−\begin{SaveVerbatim}{return}
545+\begin{code}
641−
642return : a -> IO a
546return : a -> IO a
547+\end{code}
643
548
644−\end{SaveVerbatim}
645−\useverb{return}
646
549
647\noindent
550\noindent
648As we will see later, \texttt{do} notation is more general than this, and can be
551As we will see later, \texttt{do} notation is more general than this, and can be
@@ -659,16 +562,14 @@ part of \texttt{prelude.idr}.
659
562
660We have already seen the \texttt{List} and \texttt{Vect} data types:
563We have already seen the \texttt{List} and \texttt{Vect} data types:
661
564
662−\begin{SaveVerbatim}{listvec}
565+\begin{code}
663−
664data List a = Nil | (::) a (List a)
566data List a = Nil | (::) a (List a)
665
567
666data Vect : Nat -> Type -> Type where
568data Vect : Nat -> Type -> Type where
667 Nil : Vect Z a
569 Nil : Vect Z a
668 (::) : a -> Vect k a -> Vect (S k) a
570 (::) : a -> Vect k a -> Vect (S k) a
571+\end{code}
669
572
670−\end{SaveVerbatim}
671−\useverb{listvec}
672
573
673\noindent
574\noindent
674Note that the constructor names are the same for each --- constructor names (in
575Note that the constructor names are the same for each --- constructor names (in
@@ -687,8 +588,7 @@ The library also defines a number of functions for manipulating these types.
687\texttt{map} is overloaded both for \texttt{List} and \texttt{Vect}
588\texttt{map} is overloaded both for \texttt{List} and \texttt{Vect}
688and applies a function to every element of the list or vector.
589and applies a function to every element of the list or vector.
689
590
690−\begin{SaveVerbatim}{map}
591+\begin{code}
691−
692map : (a -> b) -> List a -> List b
592map : (a -> b) -> List a -> List b
693map f [] = []
593map f [] = []
694map f (x :: xs) = f x :: map f xs
594map f (x :: xs) = f x :: map f xs
@@ -696,34 +596,29 @@ map f (x :: xs) = f x :: map f xs
696map : (a -> b) -> Vect n a -> Vect n b
596map : (a -> b) -> Vect n a -> Vect n b
697map f [] = []
597map f [] = []
698map f (x :: xs) = f x :: map f xs
598map f (x :: xs) = f x :: map f xs
599+\end{code}
699
600
700−\end{SaveVerbatim}
701−\useverb{map}
702
601
703\noindent
602\noindent
704For example, to double every element in a vector of integers:
603For example, to double every element in a vector of integers:
705
604
706−\begin{SaveVerbatim}{dvect}
605+\begin{code}
707−
708intVec : Vect 5 Int
606intVec : Vect 5 Int
709intVec = [1, 2, 3, 4, 5]
607intVec = [1, 2, 3, 4, 5]
710
608
711double : Int -> Int
609double : Int -> Int
712double x = x * 2
610double x = x * 2
611+\end{code}
713
612
714−\end{SaveVerbatim}
715−\useverb{dvect}
716
613
717\noindent
614\noindent
718You'll find these examples in \texttt{usefultypes.idr} in the \texttt{examples/} directory:
615You'll find these examples in \texttt{usefultypes.idr} in the \texttt{examples/} directory:
719
616
720−\begin{SaveVerbatim}{rundvect}
617+\begin{lstlisting}
721−
722*usefultypes> show (map double intVec)
618*usefultypes> show (map double intVec)
723"[2, 4, 6, 8, 10]" : String
619"[2, 4, 6, 8, 10]" : String
620+\end{lstlisting}
724
621
725−\end{SaveVerbatim}
726−\useverb{rundvect}
727
622
728\noindent
623\noindent
729For more details of the functions available on \texttt{List} and \texttt{Vect},
624For more details of the functions available on \texttt{List} and \texttt{Vect},
@@ -737,13 +632,11 @@ need, please feel free to add it and submit a patch!
737There are actually neater ways to write the above expression. One way would be
632There are actually neater ways to write the above expression. One way would be
738to use an anonymous function:
633to use an anonymous function:
739
634
740−\begin{SaveVerbatim}{lam1}
635+\begin{lstlisting}
741−
742*usefultypes> show (map (\x => x * 2) intVec)
636*usefultypes> show (map (\x => x * 2) intVec)
743"[2, 4, 6, 8, 10]" : String
637"[2, 4, 6, 8, 10]" : String
638+\end{lstlisting}
744
639
745−\end{SaveVerbatim}
746−\useverb{lam1}
747
640
748\noindent
641\noindent
749The notation \texttt{$\backslash$x => val} constructs an anonymous function
642The notation \texttt{$\backslash$x => val} constructs an anonymous function
@@ -754,13 +647,11 @@ types, e.g. \texttt{$\backslash$x : Int => x * 2}, and can pattern match,
754e.g. \texttt{$\backslash$ (x, y) => x + y}.
647e.g. \texttt{$\backslash$ (x, y) => x + y}.
755We could also use an operator section:
648We could also use an operator section:
756
649
757−\begin{SaveVerbatim}{sec1}
650+\begin{code}
758−
759*usefultypes> show (map (* 2) intVec)
651*usefultypes> show (map (* 2) intVec)
760"[2, 4, 6, 8, 10]" : String
652"[2, 4, 6, 8, 10]" : String
653+\end{code}
761
654
762−\end{SaveVerbatim}
763−\useverb{sec1}
764
655
765\noindent
656\noindent
766\texttt{(*2)} is shorthand for a function which multiplies a number by 2. It expands to
657\texttt{(*2)} is shorthand for a function which multiplies a number by 2. It expands to
@@ -772,38 +663,32 @@ Similarly, \texttt{(2*)} would expand to \texttt{$\backslash$x => 2 * x}.
772\texttt{Maybe} describes an optional value. Either there is a value of the given type,
663\texttt{Maybe} describes an optional value. Either there is a value of the given type,
773or there isn't:
664or there isn't:
774
665
775−\begin{SaveVerbatim}{maybe}
666+\begin{code}
776−
777data Maybe a = Just a | Nothing
667data Maybe a = Just a | Nothing
668+\end{code}
778
669
779−\end{SaveVerbatim}
780−\useverb{maybe}
781
670
782\noindent
671\noindent
783\texttt{Maybe} is one way of giving a type to an operation that may fail. For example,
672\texttt{Maybe} is one way of giving a type to an operation that may fail. For example,
784looking something up in a \texttt{List} (rather than a vector) may result in an out of
673looking something up in a \texttt{List} (rather than a vector) may result in an out of
785bounds error:
674bounds error:
786
675
787−\begin{SaveVerbatim}{lookuplist}
676+\begin{code}
788−
789list_lookup : Nat -> List a -> Maybe a
677list_lookup : Nat -> List a -> Maybe a
790list_lookup _ Nil = Nothing
678list_lookup _ Nil = Nothing
791list_lookup Z (x :: xs) = Just x
679list_lookup Z (x :: xs) = Just x
792list_lookup (S k) (x :: xs) = list_lookup k xs
680list_lookup (S k) (x :: xs) = list_lookup k xs
681+\end{code}
793
682
794−\end{SaveVerbatim}
795−\useverb{lookuplist}
796
683
797\noindent
684\noindent
798The \texttt{maybe} function is used to process values of type \texttt{Maybe},
685The \texttt{maybe} function is used to process values of type \texttt{Maybe},
799either by applying a function to the value, if there is one, or by providing a default value:
686either by applying a function to the value, if there is one, or by providing a default value:
800
687
801−\begin{SaveVerbatim}{maybefn}
688+\begin{code}
802−
803maybe : Maybe a -> |(default:b) -> (a -> b) -> b
689maybe : Maybe a -> |(default:b) -> (a -> b) -> b
690+\end{code}
804
691
805−\end{SaveVerbatim}
806−\useverb{maybefn}
807
692
808\noindent
693\noindent
809The vertical bar $\mid$ before the default value is a laziness annotation. Normally
694The vertical bar $\mid$ before the default value is a laziness annotation. Normally
@@ -817,41 +702,35 @@ needed.
817
702
818Values can be paired with the following built-in data type:
703Values can be paired with the following built-in data type:
819
704
820−\begin{SaveVerbatim}{mkpair}
705+\begin{code}
821−
822data Pair a b = MkPair a b
706data Pair a b = MkPair a b
707+\end{code}
823
708
824−\end{SaveVerbatim}
825−\useverb{mkpair}
826
709
827\noindent
710\noindent
828As syntactic sugar, we can write \texttt{(a, b)} which, according to context,
711As syntactic sugar, we can write \texttt{(a, b)} which, according to context,
829means either \texttt{Pair a b} or \texttt{MkPair a b}.
712means either \texttt{Pair a b} or \texttt{MkPair a b}.
830Tuples can contain an arbitrary number of values, represented as nested pairs:
713Tuples can contain an arbitrary number of values, represented as nested pairs:
831
714
832−\begin{SaveVerbatim}{tuple}
715+\begin{code}
833−
834fred : (String, Int)
716fred : (String, Int)
835fred = ("Fred", 42)
717fred = ("Fred", 42)
836
718
837jim : (String, Int, String)
719jim : (String, Int, String)
838jim = ("Jim", 25, "Cambridge")
720jim = ("Jim", 25, "Cambridge")
721+\end{code}
839
722
840−\end{SaveVerbatim}
841−\useverb{tuple}
842
723
843\subsubsection*{Dependent Pairs}
724\subsubsection*{Dependent Pairs}
844
725
845Dependent pairs allow the type of the second element of a pair to depend on
726Dependent pairs allow the type of the second element of a pair to depend on
846the value of the first element:
727the value of the first element:
847
728
848−\begin{SaveVerbatim}{sigma}
729+\begin{code}
849−
850data Exists : (A : Type) -> (P : A -> Type) -> Type where
730data Exists : (A : Type) -> (P : A -> Type) -> Type where
851 Ex_intro : {P : A -> Type} -> (a : A) -> P a -> Exists A P
731 Ex_intro : {P : A -> Type} -> (a : A) -> P a -> Exists A P
732+\end{code}
852
733
853−\end{SaveVerbatim}
854−\useverb{sigma}
855
734
856\noindent
735\noindent
857Again, there is syntactic sugar for this. \texttt{(a : A ** P)} is the type of a pair of
736Again, there is syntactic sugar for this. \texttt{(a : A ** P)} is the type of a pair of
@@ -859,13 +738,11 @@ A and P, where the name \texttt{a} can occur inside P. \texttt{( a ** p )}
859constructs a value of this type. For example, we can pair a number with a
738constructs a value of this type. For example, we can pair a number with a
860\texttt{Vect} of a particular length.
739\texttt{Vect} of a particular length.
861
740
862−\begin{SaveVerbatim}{dvec}
741+\begin{code}
863−
864vec : (n : Nat ** Vect n Int)
742vec : (n : Nat ** Vect n Int)
865vec = (2 ** [3, 4])
743vec = (2 ** [3, 4])
744+\end{code}
866
745
867−\end{SaveVerbatim}
868−\useverb{dvec}
869
746
870\noindent
747\noindent
871The type checker could of course infer the value of the first element from the
748The type checker could of course infer the value of the first element from the
@@ -873,25 +750,21 @@ length of the vector. We can write an underscore \texttt{\_} in place of values
873expect the type checker to fill in, so the above definition could also be
750expect the type checker to fill in, so the above definition could also be
874written as:
751written as:
875
752
876−\begin{SaveVerbatim}{dvec1}
753+\begin{code}
877−
878vec : (n : Nat ** Vect n Int)
754vec : (n : Nat ** Vect n Int)
879vec = (_ ** [3, 4])
755vec = (_ ** [3, 4])
756+\end{code}
880
757
881−\end{SaveVerbatim}
882−\useverb{dvec1}
883
758
884\noindent
759\noindent
885We might also prefer to omit the type of the first element of the pair, since,
760We might also prefer to omit the type of the first element of the pair, since,
886again, it can be inferred:
761again, it can be inferred:
887
762
888−\begin{SaveVerbatim}{dvec2}
763+\begin{code}
889−
890vec : (n ** Vect n Int)
764vec : (n ** Vect n Int)
891vec = (_ ** [3, 4])
765vec = (_ ** [3, 4])
766+\end{code}
892
767
893−\end{SaveVerbatim}
894−\useverb{dvec2}
895
768
896\noindent
769\noindent
897One use for dependent pairs is to return values of dependent types where the
770One use for dependent pairs is to return values of dependent types where the
@@ -899,22 +772,18 @@ index is not necessarily known in advance. For example, if we filter elements
899out of a \texttt{Vect} according to some predicate, we will not know in advance what the
772out of a \texttt{Vect} according to some predicate, we will not know in advance what the
900length of the resulting vector will be:
773length of the resulting vector will be:
901
774
902−\begin{SaveVerbatim}{vfilter}
775+\begin{code}
903−
904filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
776filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
777+\end{code}
905
778
906−\end{SaveVerbatim}
907−\useverb{vfilter}
908
779
909\noindent
780\noindent
910If the \texttt{Vect} is empty, the result is easy:
781If the \texttt{Vect} is empty, the result is easy:
911
782
912−\begin{SaveVerbatim}{vfilternil}
783+\begin{code}
913−
914filter p Nil = (_ ** [])
784filter p Nil = (_ ** [])
785+\end{code}
915
786
916−\end{SaveVerbatim}
917−\useverb{vfilternil}
918
787
919\noindent
788\noindent
920In the \texttt{::} case, we need to inspect the result of a recursive call to
789In the \texttt{::} case, we need to inspect the result of a recursive call to
@@ -922,13 +791,10 @@ In the \texttt{::} case, we need to inspect the result of a recursive call to
922extract the length and the vector from the result. To do this, we use \texttt{with}
791extract the length and the vector from the result. To do this, we use \texttt{with}
923notation, which allows pattern matching on intermediate values:
792notation, which allows pattern matching on intermediate values:
924
793
925−\begin{SaveVerbatim}{vfiltercons}
794+\begin{code}
926−
927filter p (x :: xs) with (filter p xs)
795filter p (x :: xs) with (filter p xs)
928 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
796 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
929−
797+\end{code}
930−\end{SaveVerbatim}
931−\useverb{vfiltercons}
932
798
933\noindent
799\noindent
934We will see more on \texttt{with} notation later.
800We will see more on \texttt{with} notation later.
@@ -938,13 +804,11 @@ We will see more on \texttt{with} notation later.
938The \texttt{so} data type is a predicate on \texttt{Bool} which guarantees that the
804The \texttt{so} data type is a predicate on \texttt{Bool} which guarantees that the
939value is true:
805value is true:
940
806
941−\begin{SaveVerbatim}{sotype}
807+\begin{code}
942−
943data so : Bool -> Type where
808data so : Bool -> Type where
944 oh : so True
809 oh : so True
945−
810+\end{code}
946−\end{SaveVerbatim}
811+
947−\useverb{sotype}
948
812
949\noindent
813\noindent
950This is most useful for providing a static guarantee that a dynamic check has been made.
814This is most useful for providing a static guarantee that a dynamic check has been made.
@@ -952,16 +816,14 @@ For example, we might provide a safe interface to a function which draws a pixel
952on a graphical display as follows, where \texttt{so (inBounds x y)} guarantees that
816on a graphical display as follows, where \texttt{so (inBounds x y)} guarantees that
953the point \texttt{(x,y)} is within the bounds of a 640x480 window:
817the point \texttt{(x,y)} is within the bounds of a 640x480 window:
954
818
955−\begin{SaveVerbatim}{soexample}
819+\begin{code}
956−
957inBounds : Int -> Int -> Bool
820inBounds : Int -> Int -> Bool
958inBounds x y = x >= 0 && x < 640 && y >= 0 && y < 480
821inBounds x y = x >= 0 && x < 640 && y >= 0 && y < 480
959
822
960drawPoint : (x : Int) -> (y : Int) -> so (inBounds x y) -> IO ()
823drawPoint : (x : Int) -> (y : Int) -> so (inBounds x y) -> IO ()
961drawPoint x y p = unsafeDrawPoint x y
824drawPoint x y p = unsafeDrawPoint x y
962−
825+\end{code}
963−\end{SaveVerbatim}
826+
964−\useverb{soexample}
965
827
966\subsection{More Expressions}
828\subsection{More Expressions}
967
829
@@ -969,29 +831,25 @@ drawPoint x y p = unsafeDrawPoint x y
969
831
970Intermediate values can be calculated using \texttt{let} bindings:
832Intermediate values can be calculated using \texttt{let} bindings:
971
833
972−\begin{SaveVerbatim}{letb}
834+\begin{code}
973−
974mirror : List a -> List a
835mirror : List a -> List a
975mirror xs = let xs' = rev xs in
836mirror xs = let xs' = rev xs in
976 xs ++ xs'
837 xs ++ xs'
977−
838+\end{code}
978−\end{SaveVerbatim}
839+
979−\useverb{letb}
980
840
981\noindent
841\noindent
982We can do simple pattern matching in \texttt{let} bindings too. For example, we can extract
842We can do simple pattern matching in \texttt{let} bindings too. For example, we can extract
983fields from a record as follows, as well as by pattern matching at the top level:
843fields from a record as follows, as well as by pattern matching at the top level:
984
844
985−\begin{SaveVerbatim}{letp}
845+\begin{code}
986−
987data Person = MkPerson String Int
846data Person = MkPerson String Int
988
847
989showPerson : Person -> String
848showPerson : Person -> String
990showPerson p = let MkPerson name age = p in
849showPerson p = let MkPerson name age = p in
991 name ++ " is " ++ show age ++ " years old"
850 name ++ " is " ++ show age ++ " years old"
992−
851+\end{code}
993−\end{SaveVerbatim}
852+
994−\useverb{letp}
995
853
996\subsubsection*{List comprehensions}
854\subsubsection*{List comprehensions}
997
855
@@ -1000,12 +858,10 @@ showPerson p = let MkPerson name age = p in
1000\Idris{} provides \emph{comprehension} notation as a convenient shorthand for
858\Idris{} provides \emph{comprehension} notation as a convenient shorthand for
1001building lists. The general form is:
859building lists. The general form is:
1002
860
1003−\begin{SaveVerbatim}{listcomp}
861+\begin{lstlisting}
1004−
1005[ expression | qualifiers ]
862[ expression | qualifiers ]
1006−
863+\end{lstlisting}
1007−\end{SaveVerbatim}
864+
1008−\useverb{listcomp}
1009
865
1010\noindent
866\noindent
1011This generates the list of values produced by evaluating the
867This generates the list of values produced by evaluating the
@@ -1013,14 +869,12 @@ This generates the list of values produced by evaluating the
1013\texttt{qualifiers}. For example, we can build a list of Pythagorean triples as
869\texttt{qualifiers}. For example, we can build a list of Pythagorean triples as
1014follows:
870follows:
1015
871
1016−\begin{SaveVerbatim}{triples}
872+\begin{code}
1017−
1018pythag : Int -> List (Int, Int, Int)
873pythag : Int -> List (Int, Int, Int)
1019pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
874pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
1020 x*x + y*y == z*z ]
875 x*x + y*y == z*z ]
1021−
876+\end{code}
1022−\end{SaveVerbatim}
877+
1023−\useverb{triples}
1024
878
1025\noindent
879\noindent
1026The \texttt{[a..b]} notation is another shorthand which builds a list of
880The \texttt{[a..b]} notation is another shorthand which builds a list of
@@ -1035,14 +889,12 @@ Another way of inspecting intermediate values of \emph{simple} types
1035is to use a \texttt{case} expression.
889is to use a \texttt{case} expression.
1036The following function, for example, splits a string into two at a given character:
890The following function, for example, splits a string into two at a given character:
1037
891
1038−\begin{SaveVerbatim}{split}
892+\begin{code}
1039−
1040splitAt : Char -> String -> (String, String)
893splitAt : Char -> String -> (String, String)
1041splitAt c x = case break (== c) x of
894splitAt c x = case break (== c) x of
1042 (x, y) => (x, strTail y)
895 (x, y) => (x, strTail y)
1043−
896+\end{code}
1044−\end{SaveVerbatim}
897+
1045−\useverb{split}
1046
898
1047\noindent
899\noindent
1048\texttt{break} is a library function which breaks a string into a pair of strings
900\texttt{break} is a library function which breaks a string into a pair of strings
@@ -1055,29 +907,25 @@ looks up an index in a list, returning \texttt{Nothing} if the index is out
1055of bounds. We can use this to write \texttt{lookup\_default}, which
907of bounds. We can use this to write \texttt{lookup\_default}, which
1056looks up an index and returns a default value if the index is out of bounds:
908looks up an index and returns a default value if the index is out of bounds:
1057
909
1058−\begin{SaveVerbatim}{listlookup}
910+\begin{code}
1059−
1060lookup_default : Nat -> List a -> a -> a
911lookup_default : Nat -> List a -> a -> a
1061lookup_default i xs def = case list_lookup i xs of
912lookup_default i xs def = case list_lookup i xs of
1062 Nothing => def
913 Nothing => def
1063 Just x => x
914 Just x => x
1064−
915+\end{code}
1065−\end{SaveVerbatim}
916+
1066−\useverb{listlookup}
1067
917
1068\noindent
918\noindent
1069If the index is in bounds, we get the value at that index, otherwise we get
919If the index is in bounds, we get the value at that index, otherwise we get
1070a default value:
920a default value:
1071
921
1072−\begin{SaveVerbatim}{deftest}
922+\begin{lstlisting}
1073−
1074*usefultypes> lookup_default 2 [3,4,5,6] (-1)
923*usefultypes> lookup_default 2 [3,4,5,6] (-1)
10755 : Int
9245 : Int
1076*usefultypes> lookup_default 4 [3,4,5,6] (-1)
925*usefultypes> lookup_default 4 [3,4,5,6] (-1)
1077-1 : Int
926-1 : Int
1078−
927+\end{lstlisting}
1079−\end{SaveVerbatim}
928+
1080−\useverb{deftest}
1081
929
1082\noindent
930\noindent
1083\textbf{Restrictions:} The \texttt{case} construct is intended for simple analysis
931\textbf{Restrictions:} The \texttt{case} construct is intended for simple analysis
@@ -1099,17 +947,15 @@ determined \emph{without} type checking the \texttt{case}-expression itself.
1099automatically generating field access and update functions. For example, we
947automatically generating field access and update functions. For example, we
1100can represent a person's name and age in a record:
948can represent a person's name and age in a record:
1101
949
1102−\begin{SaveVerbatim}{recsimpl}
950+\begin{code}
1103−
1104record Person : Type where
951record Person : Type where
1105 MkPerson : (name : String) ->
952 MkPerson : (name : String) ->
1106 (age : Int) -> Person
953 (age : Int) -> Person
1107
954
1108fred : Person
955fred : Person
1109fred = MkPerson "Fred" 30
956fred = MkPerson "Fred" 30
1110−
957+\end{code}
1111−\end{SaveVerbatim}
958+
1112−\useverb{recsimpl}
1113
959
1114\noindent
960\noindent
1115Record declarations are like \texttt{data} declarations, except that they are
961Record declarations are like \texttt{data} declarations, except that they are
@@ -1117,31 +963,25 @@ introduced by the \texttt{record} keyword, and can only have one constructor.
1117The names of the binders in the constructor type (\texttt{name} and \texttt{age})
963The names of the binders in the constructor type (\texttt{name} and \texttt{age})
1118here are the field names, which we can use to access the field values:
964here are the field names, which we can use to access the field values:
1119
965
1120−\begin{SaveVerbatim}{recaccess}
966+\begin{lstlisting}
1121−
1122*record> name fred
967*record> name fred
1123"Fred" : String
968"Fred" : String
1124*record> age fred
969*record> age fred
112530 : Int
97030 : Int
1126*record> :t name
971*record> :t name
1127name : Person -> String
972name : Person -> String
1128−
973+\end{lstlisting}
1129−\end{SaveVerbatim}
1130−\useverb{recaccess}
1131
974
1132\noindent
975\noindent
1133We can also use the field names to update a record (or, more precisely, produce a
976We can also use the field names to update a record (or, more precisely, produce a
1134new record with the given fields updates).
977new record with the given fields updates).
1135
978
1136−\begin{SaveVerbatim}{recupdate}
979+\begin{lstlisting}
1137−
1138*record> record { name = "Jim" } fred
980*record> record { name = "Jim" } fred
1139MkPerson "Jim" 30 : Person
981MkPerson "Jim" 30 : Person
1140*record> record { name = "Jim", age = 20 } fred
982*record> record { name = "Jim", age = 20 } fred
1141MkPerson "Jim" 20 : Person
983MkPerson "Jim" 20 : Person
1142−
984+\end{lstlisting}
1143−\end{SaveVerbatim}
1144−\useverb{recupdate}
1145
985
1146\noindent
986\noindent
1147The syntax \texttt{record \{ field = val, ... \}} generates a function which updates
987The syntax \texttt{record \{ field = val, ... \}} generates a function which updates
@@ -1152,29 +992,26 @@ Updates are allowed to change the type of a field,
1152provided that the result is well-typed, and the result does not affect the type of
992provided that the result is well-typed, and the result does not affect the type of
1153the record as a whole. For example:
993the record as a whole. For example:
1154
994
1155−\begin{SaveVerbatim}{deprec}
995+\begin{code}
1156−
1157record Class : Type where
996record Class : Type where
1158 ClassInfo : (students : Vect n Person) ->
997 ClassInfo : (students : Vect n Person) ->
1159 (className : String) ->
998 (className : String) ->
1160 Class
999 Class
1161−
1000+\end{code}
1162−\end{SaveVerbatim}
1163−\useverb{deprec}
1164
1001
1165\noindent
1002\noindent
1166It is safe to update the \texttt{students} field to a vector of a different length
1003It is safe to update the \texttt{students} field to a vector of a different length
1167because it will not affect the type of the record:
1004because it will not affect the type of the record:
1168
1005
1169−\begin{SaveVerbatim}{addstu}
1006+\begin{code}
1170−
1171addStudent : Person -> Class -> Class
1007addStudent : Person -> Class -> Class
1172addStudent p c = record { students = p :: students c } c
1008addStudent p c = record { students = p :: students c } c
1009+\end{code}
1173
1010
1011+\begin{lstlisting}
1174*record> addStudent fred (ClassInfo [] "CS")
1012*record> addStudent fred (ClassInfo [] "CS")
1175ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS"
1013ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS"
1176 : Class
1014 : Class
1015+\end{lstlisting}
1177
1016
1178−\end{SaveVerbatim}
1179−\useverb{addstu}
1180
1017
tutorial/views.tex → tutorial/content/views.texrenamed+10−25
@@ -7,14 +7,11 @@ by the value of others. For example, if we were to write down the implicit
7length arguments to \texttt{(++)}, we'd see that the form of the length argument was
7length arguments to \texttt{(++)}, we'd see that the form of the length argument was
8determined by whether the vector was empty or not:
8determined by whether the vector was empty or not:
9
9
10−\begin{SaveVerbatim}{appdep}
10+\begin{code}
11−
12(++) : Vect n a -> Vect m a -> Vect (n + m) a
11(++) : Vect n a -> Vect m a -> Vect (n + m) a
13(++) {n=Z} [] ys = ys
12(++) {n=Z} [] ys = ys
14(++) {n=S k} (x :: xs) ys = x :: xs ++ ys
13(++) {n=S k} (x :: xs) ys = x :: xs ++ ys
15−
14+\end{code}
16−\end{SaveVerbatim}
17−\useverb{appdep}
18
15
19\noindent
16\noindent
20If \texttt{n} was a successor in the \texttt{[]} case, or zero in the
17If \texttt{n} was a successor in the \texttt{[]} case, or zero in the
@@ -32,15 +29,12 @@ we know about the forms of other values. In its simplest form, the \texttt{with}
32adds another argument to the function being defined, e.g. we have already seen
29adds another argument to the function being defined, e.g. we have already seen
33a vector filter function, defined as follows:
30a vector filter function, defined as follows:
34
31
35−\begin{SaveVerbatim}{vfilterdef}
32+\begin{code}
36−
37filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
33filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
38filter p [] = ( _ ** [] )
34filter p [] = ( _ ** [] )
39filter p (x :: xs) with (filter p xs)
35filter p (x :: xs) with (filter p xs)
40 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
36 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
41−
37+\end{code}
42−\end{SaveVerbatim}
43−\useverb{vfilterdef}
44
38
45\noindent
39\noindent
46Here, the \texttt{with} clause allows us to deconstruct the result of
40Here, the \texttt{with} clause allows us to deconstruct the result of
@@ -54,26 +48,20 @@ testing another. For example, a \texttt{Nat} is either even or odd. If it's even
54be the sum of two equal \texttt{Nat}s. Otherwise, it is the sum of two equal \texttt{Nat}s
48be the sum of two equal \texttt{Nat}s. Otherwise, it is the sum of two equal \texttt{Nat}s
55plus one:
49plus one:
56
50
57−\begin{SaveVerbatim}{parity}
51+\begin{code}
58−
59data Parity : Nat -> Type where
52data Parity : Nat -> Type where
60 even : Parity (n + n)
53 even : Parity (n + n)
61 odd : Parity (S (n + n))
54 odd : Parity (S (n + n))
62−
55+\end{code}
63−\end{SaveVerbatim}
64−\useverb{parity}
65
56
66\noindent
57\noindent
67We say \texttt{Parity} is a \emph{view} of \texttt{Nat}.
58We say \texttt{Parity} is a \emph{view} of \texttt{Nat}.
68It has a \emph{covering function} which tests whether
59It has a \emph{covering function} which tests whether
69it is even or odd and constructs the predicate accordingly.
60it is even or odd and constructs the predicate accordingly.
70
61
71−\begin{SaveVerbatim}{parityty}
62+\begin{code}
72−
73parity : (n:Nat) -> Parity n
63parity : (n:Nat) -> Parity n
74−
64+\end{code}
75−\end{SaveVerbatim}
76−\useverb{parityty}
77
65
78\label{sect:nattobin}
66\label{sect:nattobin}
79
67
@@ -82,16 +70,13 @@ We'll come back to the definition of \texttt{parity} shortly. We can use it
82to write a function which converts a natural number to a list of binary digits
70to write a function which converts a natural number to a list of binary digits
83(least significant first) as follows, using the \texttt{with} rule:
71(least significant first) as follows, using the \texttt{with} rule:
84
72
85−\begin{SaveVerbatim}{natToBin}
73+\begin{code}
86−
87natToBin : Nat -> List Bool
74natToBin : Nat -> List Bool
88natToBin Z = Nil
75natToBin Z = Nil
89natToBin k with (parity k)
76natToBin k with (parity k)
90 natToBin (j + j) | even = False :: natToBin j
77 natToBin (j + j) | even = False :: natToBin j
91 natToBin (S (j + j)) | odd = True :: natToBin j
78 natToBin (S (j + j)) | odd = True :: natToBin j
92−
79+\end{code}
93−\end{SaveVerbatim}
94−\useverb{natToBin}
95
80
96\noindent
81\noindent
97The value of the result of \texttt{parity k} affects the form of \texttt{k},
82The value of the result of \texttt{parity k} affects the form of \texttt{k},
tutorial/macros.ltx → tutorial/fpmacros.styrenamed+41−21
@@ -1,11 +1,25 @@
1−%\usepackage{amstex}
1+%% ------------------------------------------- [ Functional Programming Macros ]
2−\usepackage{amssymb}
2+%% A Package to provide support for functional programming.
3+%%
4+\NeedsTeXFormat{LaTeX2e}[1994/06/01]
5+\ProvidesPackage{fpmacros}[2013/12/17 fpmacros]
6+%% ------------------------------------------------------- [ Required Packages ]
7+\RequirePackage{ifthen}
8+\RequirePackage{amssymb}
3−\usepackage{latexsym}
9+\RequirePackage{latexsym}
4−\usepackage{eepic}
10+\RequirePackage{eepic}
5−
11+\RequirePackage{fancyvrb}
12+%% ----------------------------------------------------- [ Option Delcarations ]
13+\newboolean{useverb}
14+\setboolean{useverb}{true}
15+
16+\DeclareOption{noverb}{%
17+ \setboolean{useverb}{false}
18+}
6
19
7−%%%%%%%%% INFERENCE RULES
20+\ProcessOptions\relax
8
21
22+%% --------------------------------------------------------- [ Inference Rules ]
9\newlength{\rulevgap}
23\newlength{\rulevgap}
10\setlength{\rulevgap}{0.05in}
24\setlength{\rulevgap}{0.05in}
11\newlength{\ruleheight}
25\newlength{\ruleheight}
@@ -78,8 +92,7 @@
78\setlength{\unitlength}{0.0005in}
92\setlength{\unitlength}{0.0005in}
79\begin{picture}(69,180)(0,12)
93\begin{picture}(69,180)(0,12)
80\blacken\path(12,192)(12,12)(57,102)
94\blacken\path(12,192)(12,12)(57,102)
81− (12,192)(12,192)
82−\path(12,192)(12,12)(57,102)
95+ (12,192)(12,192)\path(12,192)(12,12)(57,102)
83 (12,192)(12,192)
96 (12,192)(12,192)
84\end{picture}
97\end{picture}
85}
98}
@@ -305,18 +318,20 @@
305
318
306\newcommand{\DBOX}[2]{\fbox{\parbox{#1}{\textbf{Definition:}#2}}}
319\newcommand{\DBOX}[2]{\fbox{\parbox{#1}{\textbf{Definition:}#2}}}
307
320
321+\ifthenelse{\boolean{useverb}}{%
308−\newcommand{\useverbtb}[1]{\begin{tiny}\BUseVerbatim{#1}\end{tiny}}
322+ \newcommand{\useverbtb}[1]{\begin{tiny}\BUseVerbatim{#1}\end{tiny}}
309−\newcommand{\useverb}[1]{\BUseVerbatim{#1}}
323+ \newcommand{\useverb}[1]{\BUseVerbatim{#1}}
310−\newcommand{\useverbs}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}
324+ \newcommand{\useverbs}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}
311−\newcommand{\useverbb}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}
325+ \newcommand{\useverbb}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}
326+ \newcommand{\codefig}[2]{\begin{figure}[h]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
327+ \newcommand{\codefigs}[2]{\begin{figure}[h]\useverbs{#1}\caption{#2}\label{#1}\end{figure}}
328+ \newcommand{\codefigt}[2]{\begin{figure}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
329+ \newcommand{\codefigb}[2]{\begin{figure}[b]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
330+ \newcommand{\codefigtc}[2]{\begin{figure*}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
331+}{}
312
332
313\newcommand{\diagfig}[3]{\begin{figure}[h]\begin{center}\includegraphics[width=#1]{#2}\end{center}
333\newcommand{\diagfig}[3]{\begin{figure}[h]\begin{center}\includegraphics[width=#1]{#2}\end{center}
314\caption{#3}\label{#2}\end{figure}}
334\caption{#3}\label{#2}\end{figure}}
315−\newcommand{\codefig}[2]{\begin{figure}[h]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
316−\newcommand{\codefigs}[2]{\begin{figure}[h]\useverbs{#1}\caption{#2}\label{#1}\end{figure}}
317−\newcommand{\codefigt}[2]{\begin{figure}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
318−\newcommand{\codefigb}[2]{\begin{figure}[b]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
319−\newcommand{\codefigtc}[2]{\begin{figure*}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
320\newcommand{\diagfigtc}[3]{\begin{figure*}[t]\begin{center}\includegraphics[width=#1]{#2}\end{center}
335\newcommand{\diagfigtc}[3]{\begin{figure*}[t]\begin{center}\includegraphics[width=#1]{#2}\end{center}
321\caption{#3}\label{#2}\end{figure*}}
336\caption{#3}\label{#2}\end{figure*}}
322
337
@@ -324,10 +339,13 @@
324\newcommand{\FFIG}[3]{\begin{figure}\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}
339\newcommand{\FFIG}[3]{\begin{figure}\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}
325\newcommand{\FFIGB}[3]{\begin{figure}[b]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}
340\newcommand{\FFIGB}[3]{\begin{figure}[b]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}
326\newcommand{\FFIGTC}[3]{\begin{figure*}[t]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure*}}
341\newcommand{\FFIGTC}[3]{\begin{figure*}[t]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure*}}
327−\newcommand{\VFIG}[3]{\begin{figure}[h]\begin{boxedverbatim}#1\end{boxedverbatim}\caption{#2}\label{#3}\end{figure}}
328\newcommand{\PFIG}[3]{\begin{figure}[p]\begin{center}\fbox{\DM{#1}}\end{center}\caption{#2}\label{#3}\end{figure}}
342\newcommand{\PFIG}[3]{\begin{figure}[p]\begin{center}\fbox{\DM{#1}}\end{center}\caption{#2}\label{#3}\end{figure}}
329\newcommand{\CFIG}[3]{\begin{figure}[h]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}
343\newcommand{\CFIG}[3]{\begin{figure}[h]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}
330
344
345+\ifthenelse{\boolean{useverb}}{%
346+ \newcommand{\VFIG}[3]{\begin{figure}[h]\begin{boxedverbatim}#1\end{boxedverbatim}\caption{#2}\label{#3}\end{figure}}
347+}{}
348+
331\newcommand{\TFIG}[4]{\begin{figure}[h]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure}}
349\newcommand{\TFIG}[4]{\begin{figure}[h]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure}}
332\newcommand{\TFIGTC}[4]{\begin{figure*}[t]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure*}}
350\newcommand{\TFIGTC}[4]{\begin{figure*}[t]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure*}}
333
351
@@ -676,8 +694,9 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\
676\newcommand{\falsecase}{\Cases{\False}}
694\newcommand{\falsecase}{\Cases{\False}}
677
695
678% Code
696% Code
697+\ifthenelse{\boolean{useverb}}{%
679−\newcommand{\Haskell}[1]{\begin{quotation}\begin{verbatim}#1\end{verbatim}\end{quotation}}
698+ \newcommand{\Haskell}[1]{\begin{quotation}\begin{verbatim}#1\end{verbatim}\end{quotation}}
680−
699+}{}
681% Quicksort
700% Quicksort
682
701
683\newcommand{\QSView}{\TC{QuickSort}}
702\newcommand{\QSView}{\TC{QuickSort}}
@@ -1063,4 +1082,5 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\
1063\newcommand{\direct}[1]{\texttt{\%#1}}
1082\newcommand{\direct}[1]{\texttt{\%#1}}
1064
1083
1065\newcommand{\Feature}[1]{\textbf{Remark:}}
1084\newcommand{\Feature}[1]{\textbf{Remark:}}
1066−%\newcommand{\Remark}[1]{\textbf{Remark:}}
1085+
1086+\endinput
tutorial/idris-tutorial.pdfdeleted

Binary file not shown.

tutorial/idris-tutorial.tex+36−21
@@ -1,39 +1,54 @@
1−\documentclass{article}
1+\documentclass[british, final]{article}
2+
3+\usepackage[l2tabu,orthodox]{nag}
4+\usepackage{fixltx2e}
5+\usepackage{babel}
6+\usepackage[iso]{isodate}
7+\usepackage[utf8]{inputenc}
8+\usepackage[T1]{fontenc}
9+\usepackage[protrusion=true, expansion=true]{microtype}
10+\usepackage[strict=true]{csquotes}
11+\usepackage{xspace}
12+
13+\usepackage{mathpazo}
14+\usepackage[scaled=0.95]{helvet}
15+\usepackage{courier}
2
16
3\usepackage{fullpage}
17\usepackage{fullpage}
4−\usepackage{palatino}
5−\usepackage{url}
6−\usepackage{fancyvrb}
7\usepackage{hyperref}
18\usepackage{hyperref}
19+\usepackage[missing=0.9.10]{gitinfo}
20+
21+\usepackage{fpmacros}
22+\usepackage[numbers]{idrislang}
8
23
9\input{conf.ltx}
24\input{conf.ltx}
10−\input{macros.ltx}
11\input{library.ltx}
25\input{library.ltx}
12
26
13−\newcommand{\Idris}{\textsc{Idris}}
27+\newcommand{\version}{\gitVtagn}
14−\newcommand{\version}{0.9.10}
15
28
16\title{Programming in \Idris{}: a tutorial}
29\title{Programming in \Idris{}: a tutorial}
17−\author{Edwin Brady \\ \url{eb@cs.st-andrews.ac.uk}}
30+\author{The \Idris{} Community}
31+\date{\origdate\today}
18
32
19\begin{document}
33\begin{document}
20
34
21\maketitle
35\maketitle
22
36
23\tableofcontents
37\tableofcontents
24−
38+\newpage
39+
25−\input{intro}
40+\input{./content/intro}
26−\input{starting}
41+\input{./content/starting}
27−\input{typesfuns}
42+\input{./content/typesfuns}
28−\input{classes}
43+\input{./content/classes}
29−\input{modules}
44+\input{./content/modules}
30−\input{interp}
45+\input{./content/interp}
31−\input{views}
46+\input{./content/views}
32−\input{theorems}
47+\input{./content/theorems}
33−\input{provisional}
48+\input{./content/provisional}
34−\input{syntax}
49+\input{./content/syntax}
35−\input{miscellany}
50+\input{./content/miscellany}
36−\input{conclusions}
51+\input{./content/conclusions}
37
52
38\bibliographystyle{abbrv}
53\bibliographystyle{abbrv}
39\bibliography{literature.bib}
54\bibliography{literature.bib}
tutorial/idrislang.stynew file+188
@@ -0,0 +1,188 @@
1+%% --------------------------------------------------- [ Idris Styling Package ]
2+%%
3+%% A set of LaTeX macros and styling for working with Idris in LaTeX
4+%%
5+%% + Provides a listings bindings:
6+%% + idris :: default ascii
7+%% + literateidris :: convert ascii maths to math symbols.
8+%% + Defines a `numbers' and `default' listings style.
9+%% + Defines a `code' environment for typesetting idris.
10+%% + \begin{code}[...] ... \end{code}
11+%% + Defines commands typesetting the name Idris.
12+%% + \Idris{}
13+%% + \idris{}
14+%%
15+%% Options:
16+%% - literate :: turn on literate idris for code environments.
17+%% - numbers :: turn on numbers for code environments.
18+%%
19+%% ----------------------------------------------------------- [ Begin Package ]
20+\ProvidesPackage{idrislang}
21+
22+\RequirePackage{ifthen}
23+\RequirePackage{listings}
24+\RequirePackage{xspace}
25+%% ----------------------------------------------------------------- [ Options ]
26+\newboolean{literate}
27+\setboolean{literate}{false}
28+\newboolean{numbers}
29+\setboolean{numbers}{false}
30+
31+\DeclareOption{literate}{%
32+ \setboolean{literate}{true}
33+}
34+
35+\DeclareOption{numbers}{%
36+ \setboolean{numbers}{true}
37+}
38+
39+\ProcessOptions\relax
40+
41+%% ---------------------------------------------------------------- [ Commands ]
42+\newcommand{\Idris}{\textsc{Idris}\xspace}
43+\newcommand{\idris}{\textsc{Idris}\xspace}
44+
45+%% --------------------------------------------------- [ Define Idris Listings ]
46+\lstdefinelanguage{idris}{%
47+ sensitive,%
48+%% ----------------------------------------------------------- [ Default Style ]
49+ basicstyle=\ttfamily,
50+ flexiblecolumns=false,
51+ commentstyle=\footnotesize\sffamily,
52+%% ---------------------------------------------------------------- [ Keywords ]
53+%% From Idris Parser and idris-mode and vimscript
54+ keywords={%
55+ abstract, attack, case, compute, do, dsl, else, exact, focus, if,
56+ import, in, infix, infixl, infixr, instance, intros, module,
57+ mutual, namespace, of, let, parameters, partial, pattern, prefix,
58+ private, public, refine, rewrite, solve, syntax, term, then,
59+ total, trivial, try, using, where, with
60+},
61+%% ------------------------------------------------------- [ Prelude Functions ]
62+%% Generated using
63+%% find lib/ -name "*.idr" | xargs grep -e "^[a-zA-Z0-9]* :" | awk -F : '{printf $2", "}'
64+ morekeywords={%
65+ class, data, instance, record, dsl, postulate, default, assert_total,
66+ lambda, variable, index_first, index_next
67+ % trace, unsafePerformPrimIO, FInt, FChar, FByte, FShort, FLong,
68+ % FBits8, FBits16, FBits32, FBits64, FBits8x16, FBits16x8,
69+ % FBits32x4, FBits64x2, interpFTy, ForeignTy, mkForeignPrim,
70+ % mkLazyForeignPrim, liftPrimIO, fork, unsafePerformIO, listens,
71+ % censor, Writer, liftReaderT, asks, Reader, modify, gets, State,
72+ % RWS, nGTSm, decideNatLTE, lte, vectInjective1, vectInjective2,
73+ % run, myID, send, msgWaiting, recv, recvWithSender, create,
74+ % sendToThread, checkMsgs, getMsg, viewB8x16, viewB16x8, viewB32x4,
75+ % viewB64x2, pow, exp, log, pi, sin, cos, tan, asin, acos, atan,
76+ % atan2, sinh, cosh, tanh, sqrt, floor, ceiling, count, countFrom,
77+ % curry, uncurry, uniformB8x16, uniformB16x8, uniformB32x4,
78+ % uniformB64x2, putStr, putStrLn, print, getLine, putChar, getChar,
79+ % fopen, openFile, closeFile, fread, fwrite, feof, ferror, nullPtr,
80+ % nullStr, validFile, while, readFile, userSuppliedName, seq, try,
81+ % mkPair, getUName, unApply, mkApp, binderTy, divCeil, nextPow2,
82+ % nextBytes, machineTy, bitsUsed, natToBits, getPad, pad8, pad16,
83+ % pad32, pad64, shiftLeft, shiftRightLogical, shiftRightArithmetic,
84+ % and, or, xor, plus, minus, times, sdiv, udiv, srem, urem, lt, lte,
85+ % eq, gte, gt, complement, zeroExtend, intToBits, bitsToInt, bitAt,
86+ % getBit, setBit, unsetBit, bitsToStr, findElem, replaceElem,
87+ % replaceByElem, mapElem, anyNilAbsurd, anyElim, any, negAnyAll,
88+ % notAllHere, notAllThere, all, length, index, weaken, take, toList,
89+ % fromList, replicate, foldl, foldr, map, pad, zeroBoundIsEmpty,
90+ % empty, insert, delete, contains, fromList, toList, applyKleisli,
91+ % applyMor, applyEndo, absZ, negZ, negNat, minusNatZ, plusZ, subZ,
92+ % multZ, fromInt, natPlusZPlus, natMultZMult, doubleNegElim,
93+ % posInjective, negSInjective, posNotNeg, plusZeroLeftNeutralZ,
94+ % plusZeroRightNeutralZ, plusCommutativeZ, modBin, modComp, div,
95+ % rem, intToMod, modToStr, branch4, branch5, branch6, branch7,
96+ % merge1, merge2, merge3, treeLookup, treeInsert, delType,
97+ % treeDelete, treeToList, empty, lookup, insert, delete, fromList,
98+ % toList, getWitness, getProof, FalseElim, replace, sym, trans,
99+ % lazy, par, malloc, Not, id, the, const, fst, snd, flip, cong,
100+ % boolElim, not, intToBool, boolOp, div, mod, strHead, strTail,
101+ % strCons, strIndex, reverse, null, getArgs, getEnv, setEnv,
102+ % unsetEnv, getEnvironment, exit, usleep, sequence, toHexDigit,
103+ % b8ToString, b16ToString, b32ToString, b64ToString, tail, head,
104+ % last, init, index, deleteAt, replaceAt, take, drop, fromList,
105+ % replicate, zipWith, zip, unzip, concat, elemBy, elem, lookupBy,
106+ % lookup, hasAnyBy, hasAny, find, findIndex, elemIndexBy, elemIndex,
107+ % nubBy, nub, isPrefixOfBy, isPrefixOf, isSuffixOfBy, isSuffixOf,
108+ % catMaybes, diag, range, isLeft, isRight, choose, either, lefts,
109+ % rights, partitionEithers, fromEither, maybeToEither, strM, unpack,
110+ % pack, span, break, split, ltrim, trim, words, lines, foldr1,
111+ % unwords, length, realPart, imagPart, mkPolar, cis, magnitude,
112+ % phase, conjugate, isNothing, isJust, maybe, fromMaybe, toMaybe,
113+ % justInjective, lowerMaybe, raiseToMaybe, isNil, isCons, head,
114+ % tail, last, init, take, drop, takeWhile, dropWhile, list, length,
115+ % repeat, replicate, zipWith, zipWith3, zip, zip3, unzip, unzip3,
116+ % mapMaybe, toList, reverse, intersperse, intercalate, elemBy, elem,
117+ % lookupBy, lookup, hasAnyBy, hasAny, find, findIndex, findIndices,
118+ % elemIndexBy, elemIndex, elemIndicesBy, elemIndices, filter, nubBy,
119+ % nub, span, break, split, partition, isPrefixOfBy, isPrefixOf,
120+ % isSuffixOfBy, isSuffixOf, sorted, mergeBy, merge, sort,
121+ % maybeToList, listToMaybe, catMaybes, appendNilRightNeutral,
122+ % appendAssociative, lengthAppend, mapPreservesLength,
123+ % mapDistributesOverAppend, mapFusion, hasAnyByNilFalse,
124+ % hasAnyNilFalse, fromIntegerNat, toIntegerNat, hyper, log2, gcd,
125+ % liftA, liftA2, liftA3, guard, when, finToNat, finToInt, weaken,
126+ % strengthen, last, natToFin, integerToFin, fromInteger, flatten,
127+ % return, isUpper, isLower, isAlpha, isDigit, isAlphaNum, isSpace,
128+ % isNL, toUpper, toLower, isHexDigit, isValidHeap, merge, insert,
129+ % findMinimum, deleteMinimum, toList, fromList, sort, main, foldl,
130+ % concat, concatMap, and, or, any, all, sum, product, Vars,
131+ % getAction, setInfo, getInfo, lift, output, queryVars, postVars,
132+ % cookieVars, queryVar, getOutput, getHeaders, flushHeaders, flush,
133+ % getVars, getContent, getCgiEnv, runCGI, mult
134+ },
135+%% ---------------------------------------------------------------- [ Comments ]
136+ morecomment=[l]--,%
137+ morecomment=[n]{\{-}{-\}}
138+}[keywords,comments,strings]%
139+
140+%% ---------------------------------------- [ Define Idris with Literate Stuff ]
141+\lstdefinelanguage{literateidris}[]{idris}{
142+ literate= {+}{{$+$}}1
143+ {/}{{$/$}}1
144+ {*}{{$*$}}1
145+ {=}{{$=$}}1
146+ {>}{{$>$}}1
147+ {<}{{$<$}}1
148+ {\\}{{$\lambda$}}1
149+ {\\\\}{{\char`\\\char`\\}}1
150+ {->}{{$\rightarrow$}}2
151+ {>=}{{$\geq$}}2
152+ {<-}{{$\leftarrow$}}2
153+ {<=}{{$\leq$}}2
154+ {=>}{{$\Rightarrow$}}2
155+ {==}{{$\equiv$}}2
156+ {\ .}{{$\circ$}}2
157+ {\ .\ }{{$\circ$}}2
158+ {>>}{{>>}}2
159+ {>>=}{{>>=}}2
160+ {|}{{$\mid$}}1,
161+}
162+%% -------------------------------------------------- [ Default Listings Style ]
163+
164+\lstdefinestyle{default}{%
165+ xleftmargin=\parindent,
166+ tabsize=2
167+}
168+\lstdefinestyle{numbers}{%
169+ numbers=left,
170+ numbersep=10pt,
171+ numberstyle=\footnotesize\sffamily,
172+ frame=leftline
173+}
174+
175+%% ------------------------------------------------------ [ A Code Environment ]
176+%% Replicate the existence of literate haskell code environments,
177+%% option to make pretty with numbers.
178+\lstnewenvironment{code}[1][]
179+ {\ifthenelse{\boolean{literate}}{%
180+ \lstset{language=literateidris}}{%
181+ \lstset{language=idris}}
182+ \ifthenelse{\boolean{numbers}}{%
183+ \lstset{style=numbers, #1}}{%
184+ \lstset{style=default, #1}}
185+ }
186+ {}
187+\endinput
188+%% --------------------------------------------------------------------- [ EOF ]