git.iko.soy/Idris-dev
on master help sign in
so type and pattern/term syntax extensions in tutorial
401e9a0Edwin Brady
tutorial/idris-tutorial.pdf
compare with master
unifiedsplit

Binary file not shown.

tutorial/syntax.tex+32
@@ -55,3 +55,35 @@ syntax select [x] from [t] = Select x t;
55\end{SaveVerbatim}
55\end{SaveVerbatim}
56\useverb{syntaxex}
56\useverb{syntaxex}
57
57
58+\noindent
59+Syntax macros can be further restricted to apply only in patterns (i.e., only on the left
60+hand side of a pattern match clause) or only in terms (i.e. everywhere but the left hand side
61+of a pattern match clause) by being marked as \texttt{pattern} or \texttt{term} syntax
62+rules. For example, we might define an interval as follows, with a static check
63+that the lower bound is below the upper bound using \texttt{so}:
64+
65+\begin{SaveVerbatim}{interval}
66+
67+data Interval : Set where
68+ MkInterval : (lower : Float) -> (upper : Float) ->
69+ so (lower < upper) -> Interval
70+
71+\end{SaveVerbatim}
72+\useverb{interval}
73+
74+\noindent
75+We can define a syntax which, in patterns, always matches \texttt{oh} for the proof
76+argument, and in terms requires a proof term to be provided:
77+
78+\begin{SaveVerbatim}{intervalsyn}
79+
80+pattern syntax "[" [x] "..." [y] "]" = MkInterval x y oh
81+term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
82+
83+\end{SaveVerbatim}
84+\useverb{intervalsyn}
85+
86+\noindent
87+In terms, the syntax \texttt{[x...y]} will generate a proof obligation
88+\texttt{bounds\_lemma} (possibly renamed).
89+
tutorial/typesfuns.tex+30
@@ -855,6 +855,36 @@ filter p (x :: xs) with (filter p xs)
855\noindent
855\noindent
856We will see more on \texttt{with} notation later.
856We will see more on \texttt{with} notation later.
857
857
858+\subsection{\texttt{so}}
859+
860+The \texttt{so} data type is a predicate on \texttt{Bool} which guarantees that the
861+value is true:
862+
863+\begin{SaveVerbatim}{sotype}
864+
865+data so : Bool where
866+ oh : so True
867+
868+\end{SaveVerbatim}
869+\useverb{sotype}
870+
871+\noindent
872+This is most useful for providing a static guarantee that a dynamic check has been made.
873+For example, we might provide a safe interface to a function which draws a pixel
874+on a graphical display as follows, where \texttt{so (inBounds x y)} guarantees that
875+the point \texttt{(x,y)} is within the bounds of a 640x480 window:
876+
877+\begin{SaveVerbatim}{soexample}
878+
879+inBounds : Int -> Int -> Bool
880+inBounds x y = x >= 0 && x < 640 && y >= 0 && y < 480
881+
882+drawPoint : (x : Int) -> (y : Int) -> so (inBounds x y) -> IO ()
883+drawPoint x y oh = unsafeDrawPoint x y
884+
885+\end{SaveVerbatim}
886+\useverb{soexample}
887+
858\subsection{More Expressions}
888\subsection{More Expressions}
859
889
860\subsubsection*{\texttt{let} bindings}
890\subsubsection*{\texttt{let} bindings}