git.iko.soy/Idris-dev
on master help sign in
Tutorial updates
d466a82Edwin Brady
tutorial/examples/interp.idr+3
compare with master
unifiedsplit
@@ -58,6 +58,9 @@ using (G : Vect Ty n)
58testFac : Int
58testFac : Int
59testFac = interp [] fact 4
59testFac = interp [] fact 4
60
60
61+unitTestFac : so (interp [] fact 4 == 25)
62+unitTestFac = oh
63+
61main : IO ()
64main : IO ()
62main = do putStr "Enter a number: "
65main = do putStr "Enter a number: "
63 x <- getLine
66 x <- getLine
tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/interp.tex+36−2
@@ -341,12 +341,12 @@ at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
341$ idris interp.idr
341$ idris interp.idr
342 ____ __ _
342 ____ __ _
343 / _/___/ /____(_)____
343 / _/___/ /____(_)____
344− / // __ / ___/ / ___/ Version 0.9.1
344+ / // __ / ___/ / ___/ Version 0.9.2
345 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
345 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
346 /___/\__,_/_/ /_/____/ Type :? for help
346 /___/\__,_/_/ /_/____/ Type :? for help
347
347
348Type checking ./interp.idr
348Type checking ./interp.idr
349−*interp> :exec interp
349+*interp> :exec
350Enter a number: 6
350Enter a number: 6
351720
351720
352*interp>
352*interp>
@@ -374,4 +374,38 @@ parameters at the point where the cast is applied.
374There are casts defined between all of the primitive types, as far as
374There are casts defined between all of the primitive types, as far as
375they make sense.
375they make sense.
376
376
377+\subsection{Unit testing}
378+
379+Recall the \texttt{so} data type:
380+
381+\useverb{sotype}
382+
383+\noindent
384+This requires its parameter to be a \texttt{True} value. One simple application of this
385+is to perform unit testing of functions at compile time. For example, we know that
386+\texttt{4! = 24} so we can set up a test case as follows:
387+
388+\begin{SaveVerbatim}{unitTestFac}
389+
390+unitTestFac : so (interp [] fact 4 == 24)
391+unitTestFac = oh
392+
393+\end{SaveVerbatim}
394+\useverb{unitTestFac}
395+
396+\noindent
397+For the program the compile, the test case must pass. If we change \texttt{24} to \texttt{25},
398+say, we will get an error message like the following:
399+
400+\begin{SaveVerbatim}{unitTestErr}
401+
402+Type checking ./interp.idr
403+interp.idr:64:Can't unify so True with so False
404+
405+Specifically:
406+ Can't unify True with False
407+
408+\end{SaveVerbatim}
409+\useverb{unitTestErr}
410+
377
411
tutorial/intro.tex+1−1
@@ -62,7 +62,7 @@ verifying systems software.
62\subsection{Example Code}
62\subsection{Example Code}
63
63
64This tutorial includes some example code, which has been tested with \Idris{} version
64This tutorial includes some example code, which has been tested with \Idris{} version
65−0.9.1. The files are available in the \Idris{} distribution,
65+0.9.2. The files are available in the \Idris{} distribution,
66so that you can try them out easily,
66so that you can try them out easily,
67under \texttt{tutorial/examples}. However, it is strongly recommended that you
67under \texttt{tutorial/examples}. However, it is strongly recommended that you
68type them in yourself, rather than simply loading and reading them.
68type them in yourself, rather than simply loading and reading them.
tutorial/starting.tex+3−3
@@ -82,7 +82,7 @@ environment. You should see something like the following:
82$ idris
82$ idris
83 ____ __ _
83 ____ __ _
84 / _/___/ /____(_)____
84 / _/___/ /____(_)____
85− / // __ / ___/ / ___/ Version 0.9.1
85+ / // __ / ___/ / ___/ Version 0.9.2
86 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
86 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
87 /___/\__,_/_/ /_/____/ Type :? for help
87 /___/\__,_/_/ /_/____/ Type :? for help
88
88
@@ -102,7 +102,7 @@ as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
102the program is compiled to the executable \texttt{hello}.
102the program is compiled to the executable \texttt{hello}.
103
103
104\begin{SaveVerbatim}{cmds}
104\begin{SaveVerbatim}{cmds}
105−Idris version 0.9.1
105+Idris version 0.9.2
106-------------------
106-------------------
107
107
108 Command Arguments Purpose
108 Command Arguments Purpose
@@ -128,7 +128,7 @@ Idris version 0.9.1
128$ idris hello.idr
128$ idris hello.idr
129 ____ __ _
129 ____ __ _
130 / _/___/ /____(_)____
130 / _/___/ /____(_)____
131− / // __ / ___/ / ___/ Version 0.9.1
131+ / // __ / ___/ / ___/ Version 0.9.2
132 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
132 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
133 /___/\__,_/_/ /_/____/ Type :? for help
133 /___/\__,_/_/ /_/____/ Type :? for help
134
134
tutorial/theorems.tex+1−1
@@ -410,7 +410,7 @@ The totality check is currently very conservative. To be recorded as total, a fu
410\item Be \emph{well-founded} --- i.e. each recursive call must have a decreasing argument
410\item Be \emph{well-founded} --- i.e. each recursive call must have a decreasing argument
411\item Not call any non-total functions
411\item Not call any non-total functions
412\item Not use any data types which are not \emph{strictly positive}
412\item Not use any data types which are not \emph{strictly positive}
413−\item (In version 0.9.1) Not be mutually recursive
413+\item (In version 0.9.2) Not be mutually recursive
414\end{itemize}
414\end{itemize}
415
415
416\noindent
416\noindent