Permalink
Browse files

Debraced tutorial

  • Loading branch information...
1 parent b0f47e1 commit 0b98a9166f6a88291b8afcb211c8972be439621b Edwin Brady committed Jan 7, 2012
View
@@ -4,6 +4,7 @@ Complete rewrite. User visible changes:
* New proof/tactics syntax
* New syntax for pairs/dependent pairs
+* Indentation-significant syntax
* Added type classes
* Added where clauses
* Added case expressions, pattern matching let and lambda
View
@@ -16,9 +16,8 @@ \section{Type Classes}
\begin{SaveVerbatim}{showclass}
-class Show a where {
+class Show a where
show : a -> String
-}
\end{SaveVerbatim}
\useverb{showclass}
@@ -43,10 +42,9 @@ \section{Type Classes}
\begin{SaveVerbatim}{shownat}
-instance Show Nat where {
+instance Show Nat where
show O = "O"
show (S k) = "s" ++ show k
-}
Idris> show (S (S (S O)))
"sssO" : String
@@ -62,14 +60,12 @@ \section{Type Classes}
\begin{SaveVerbatim}{showvec}
-instance Show a => Show (Vect a n) where {
- show xs = "[" ++ show' xs ++ "]" where {
+instance Show a => Show (Vect a n) where
+ show xs = "[" ++ show' xs ++ "]" where
show' : Show a => Vect a n -> String
show' VNil = ""
show' (x :: VNil) = show x
show' (x :: xs) = show x ++ ", " ++ show' xs
- }
-}
\end{SaveVerbatim}
\useverb{showvec}
@@ -81,10 +77,9 @@ \subsection{Default Definitions}
\begin{SaveVerbatim}{eqbasic}
-class Eq a where {
+class Eq a where
(==) : a -> a -> Bool
(/=) : a -> a -> Bool
-}
\end{SaveVerbatim}
\useverb{eqbasic}
@@ -95,14 +90,13 @@ \subsection{Default Definitions}
\begin{SaveVerbatim}{eqnat}
-instance Eq Nat where {
+instance Eq Nat where
O == O = True
(S x) == (S y) = x == y
O == (S y) = False
(S x) == O = False
x /= y = not (x == y)
-}
\end{SaveVerbatim}
\useverb{eqnat}
@@ -115,13 +109,12 @@ \subsection{Default Definitions}
\begin{SaveVerbatim}{eqdefault}
-class Eq a where {
+class Eq a where
(==) : a -> a -> Bool
(/=) : a -> a -> Bool
x /= y = not (x == y)
y == y = not (x /= y)
-}
\end{SaveVerbatim}
\useverb{eqdefault}
@@ -146,7 +139,7 @@ \subsection{Extending Classes}
\begin{SaveVerbatim}{eqord}
-class Eq a => Ord a where {
+class Eq a => Ord a where
compare : a -> a -> Ordering
(<) : a -> a -> Bool
@@ -155,7 +148,6 @@ \subsection{Extending Classes}
(>=) : a -> a -> Bool
max : a -> a -> a
min : a -> a -> a
-}
\end{SaveVerbatim}
\useverb{eqord}
@@ -200,10 +192,9 @@ \subsection{Monads and \texttt{do}-notation}
\begin{SaveVerbatim}{monad}
-class Monad (m : Set -> Set) where {
+class Monad (m : Set -> Set) where
return : a -> m a
(>>=) : m a -> (a -> m b) -> m b
-}
\end{SaveVerbatim}
\useverb{monad}
@@ -225,12 +216,11 @@ \subsection{Monads and \texttt{do}-notation}
\begin{SaveVerbatim}{maybemonad}
-instance Monad Maybe where {
+instance Monad Maybe where
return = Just
Nothing >>= k = Nothing
(Just x) >>= k = k x
-}
\end{SaveVerbatim}
\useverb{maybemonad}
@@ -242,10 +232,9 @@ \subsection{Monads and \texttt{do}-notation}
\begin{SaveVerbatim}{maybeadd}
m_add : Maybe Int -> Maybe Int -> Maybe Int
-m_add x y = do { x' <- x -- Extract value from x
- y' <- y -- Extract value from y
- return (x' + y') -- Add them
- }
+m_add x y = do x' <- x -- Extract value from x
+ y' <- y -- Extract value from y
+ return (x' + y') -- Add them
\end{SaveVerbatim}
\useverb{maybeadd}
@@ -273,10 +262,9 @@ \subsubsection*{Monad comprehensions}
\begin{SaveVerbatim}{monadplus}
-class Monad m => MonadPlus (m : Set -> Set) where {
+class Monad m => MonadPlus (m : Set -> Set) where
mplus : m a -> m a -> m a
mzero : m a
-}
\end{SaveVerbatim}
\useverb{monadplus}
View
Binary file not shown.
View
@@ -320,10 +320,9 @@ \section{Example: The Well-Typed Interpreter}
\begin{SaveVerbatim}{factmain}
main : IO ()
-main = do { putStr "Enter a number: "
- x <- getLine
- print (interp [] fact (prim__strToInt x))
- }
+main = do putStr "Enter a number: "
+ x <- getLine
+ print (interp [] fact (prim__strToInt x))
\end{SaveVerbatim}
\useverb{factmain}
View
@@ -40,9 +40,8 @@ \section{Modules and Namespaces}
import btree
main : IO ()
-main = do { let t = toTree [1,8,2,7,9,3]
- print (toList t)
- }
+main = do let t = toTree [1,8,2,7,9,3]
+ print (toList t)
\end{SaveVerbatim}
\codefig{bstmain}{Binary Tree main program}
@@ -147,15 +146,13 @@ \subsection{Explicit Namespaces}
module foo
-namespace x {
+namespace x
test : Int -> Int
test x = x * 2
-}
-namespace y {
+namespace y
test : String -> String
test x = x ++ x
-}
\end{SaveVerbatim}
\useverb{nsfoo}
View
@@ -252,10 +252,9 @@ \subsection{Example: Binary numbers}
natToBin : (n:Nat) -> Binary n
natToBin O = bEnd
-natToBin (S k) with parity k {
+natToBin (S k) with (parity k)
natToBin (S (j + j)) | even = bI (natToBin j)
natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
-}
\end{SaveVerbatim}
\useverb{ntbdef}
@@ -283,12 +282,11 @@ \subsection{Example: Binary numbers}
\begin{SaveVerbatim}{binmain}
main : IO ()
-main = do { putStr "Enter a number: "
- x <- getLine
- let n = prim__strToInt x
- let b = natToBin (fromInteger n)
- print b
- }
+main = do putStr "Enter a number: "
+ x <- getLine
+ let n = prim__strToInt x
+ let b = natToBin (fromInteger n)
+ print b
\end{SaveVerbatim}
\useverb{binmain}
@@ -298,11 +296,10 @@ \subsection{Example: Binary numbers}
\begin{SaveVerbatim}{showbin}
-instance Show (Binary n) where {
+instance Show (Binary n) where
show (bO x) = show x ++ "0"
show (bI x) = show x ++ "1"
show bEnd = ""
-}
\end{SaveVerbatim}
\useverb{showbin}
View
@@ -196,16 +196,18 @@ \subsubsection*{\texttt{where} clauses}
\begin{SaveVerbatim}{revwhere}
rev : List a -> List a
-rev xs = revAcc [] xs where {
+rev xs = revAcc [] xs where
revAcc : List a -> List a -> List a
revAcc acc [] = acc
revAcc acc (x :: xs) = revAcc (x :: acc) xs
-}
\end{SaveVerbatim}
\useverb{revwhere}
\noindent
+Indentation is significant --- functions in the \texttt{where} block must be indented
+further than the outer function.
+
\textbf{Scope:}
Any names which are visible in the outer scope are also visible in the \texttt{where}
clause (unless they have been redefined, such as \texttt{xs} here).
@@ -450,11 +452,10 @@ \subsubsection{``\texttt{using}'' notation}
\begin{SaveVerbatim}{elemusing}
-using (x:a, y:a, xs:Vect a n) {
+using (x:a, y:a, xs:Vect a n)
data Elem : a -> (Vect a n) -> Set where
here : Elem x (x :: xs)
| there : Elem x xs -> Elem x (y :: xs)
-}
\end{SaveVerbatim}
\useverb{elemusing}
@@ -543,20 +544,20 @@ \subsection{``\texttt{do}'' notation}
\begin{SaveVerbatim}{greet}
greet : IO ()
-greet = do { putStr "What is your name? "
- name <- getLine
- putStrLn ("Hello " ++ name)
- }
+greet = do putStr "What is your name? "
+ name <- getLine
+ putStrLn ("Hello " ++ name)
\end{SaveVerbatim}
\useverb{greet}
\noindent
The syntax \texttt{x <- iovalue} executes the I/O operation iovalue, of type
\texttt{IO a}, and
-puts the result, of type \texttt{a} into the variabel \texttt{x}.
+puts the result, of type \texttt{a} into the variable \texttt{x}.
In this case, \texttt{getLine} returns an \texttt{IO String},
-so \texttt{name} has type \texttt{String}.
+so \texttt{name} has type \texttt{String}. Indentation is significant --- each
+statement in the do block must begin in the same column.
The \texttt{return} operation allows us to inject a value directly into an IO
operation:
@@ -847,9 +848,8 @@ \subsubsection*{Dependent Pairs}
\begin{SaveVerbatim}{vfiltercons}
-filter p (x :: xs) with filter p xs {
+filter p (x :: xs) with (filter p xs)
| (_ , xs') = if (p x) then (_ , x :: xs') else (_ , xs')
-}
\end{SaveVerbatim}
\useverb{vfiltercons}
@@ -932,9 +932,8 @@ \subsubsection*{\texttt{case} expressions}
\begin{SaveVerbatim}{split}
splitAt : Char -> String -> (String, String)
-splitAt c x = case break (== c) x of {
+splitAt c x = case break (== c) x of
(x, y) => (x, strTail y)
- }
\end{SaveVerbatim}
\useverb{split}
@@ -953,10 +952,9 @@ \subsubsection*{\texttt{case} expressions}
\begin{SaveVerbatim}{listlookup}
lookup_default : Nat -> List a -> a -> a
-lookup_default i xs def = case list_lookup i xs of {
+lookup_default i xs def = case list_lookup i xs of
Nothing => def
| Just x => x
- }
\end{SaveVerbatim}
\useverb{listlookup}
View
@@ -36,10 +36,9 @@ \subsection{The \texttt{with} rule --- matching intermediate values}
filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
filter p [] = ( _ ** [] )
-filter p (x :: xs) with filter p xs {
+filter p (x :: xs) with (filter p xs)
| ( _ ** xs' )
= if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
-}
\end{SaveVerbatim}
\useverb{vfilterdef}
@@ -86,10 +85,9 @@ \subsection{The \texttt{with} rule --- matching intermediate values}
natToBin : Nat -> List Bool
natToBin O = Nil
-natToBin k with parity k {
+natToBin k with (parity k)
natToBin (j + j) | even = False :: natToBin j
natToBin (S (j + j)) | odd = True :: natToBin j
-}
\end{SaveVerbatim}
\useverb{natToBin}

0 comments on commit 0b98a91

Please sign in to comment.