@@ -16,49 +16,38 @@ import prelude.char
1616class Show a where
1717 show : a -> String
1818
19−
2019instance Show Nat where
2120 show O = "O"
2221 show (S k) = "s" ++ show k
2322
24−
2523instance Show Int where
2624 show = prim__intToStr
2725
28−
2926instance Show Integer where
3027 show = prim__bigIntToStr
3128
32−
3329instance Show Float where
3430 show = prim__floatToStr
3531
36−
3732instance Show Char where
3833 show x = strCons x ""
3934
40−
4135instance Show String where
4236 show = id
4337
44−
4538instance Show Bool where
4639 show True = "True"
4740 show False = "False"
4841
49−
5042instance (Show a, Show b) => Show (a, b) where
5143 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
5244
53−
5445instance Show a => Show (List a) where
5546 show xs = "[" ++ show' xs ++ "]" where
5647 show' : Show a => List a -> String
5748 show' [] = ""
5849 show' [x] = show x
5950 show' (x :: xs) = show x ++ ", " ++ show' xs
60−
61−
6251
6352instance Show a => Show (Vect a n) where
6453 show xs = "[" ++ show' xs ++ "]" where
@@ -66,14 +55,11 @@ instance Show a => Show (Vect a n) where
6655 show' [] = ""
6756 show' [x] = show x
6857 show' (x :: xs) = show x ++ ", " ++ show' xs
69−
70−
7158
7259instance Show a => Show (Maybe a) where
7360 show Nothing = "Nothing"
7461 show (Just x) = "Just " ++ show x
7562
76−
7763---- Monad and instances
7864
7965infixl 5 >>=
@@ -82,28 +68,20 @@ class Monad (m : Set -> Set) where
8268 return : a -> m a
8369 (>>=) : m a -> (a -> m b) -> m b
8470
85−
8671class Monad m => MonadPlus (m : Set -> Set) where
8772 mplus : m a -> m a -> m a
8873 mzero : m a
8974
90−
91−class Monad m => MonadFail (m : Set -> Set) where
92− fail : String -> m ()
93−
94−
9575instance Monad IO where
9676 return t = io_return t
9777 b >>= k = io_bind b k
9878
99−
10079instance Monad Maybe where
10180 return t = Just t
10281
10382 Nothing >>= k = Nothing
10483 (Just x) >>= k = k x
10584
106−
10785instance MonadPlus Maybe where
10886 mzero = Nothing
10987
@@ -111,17 +89,14 @@ instance MonadPlus Maybe where
11189 mplus Nothing (Just y) = Just y
11290 mplus Nothing Nothing = Nothing
11391
114−
11592instance Monad List where
11693 return x = [x]
11794 m >>= f = concatMap f m
11895
119−
12096instance MonadPlus List where
12197 mzero = []
12298 mplus = app
12399
124−
125100guard : MonadPlus m => Bool -> m ()
126101guard True = return ()
127102guard False = mzero
@@ -131,16 +106,13 @@ guard False = mzero
131106class Functor (f : Set -> Set) where
132107 fmap : (a -> b) -> f a -> f b
133108
134−
135109instance Functor Maybe where
136110 fmap f (Just x) = Just (f x)
137111 fmap f Nothing = Nothing
138112
139−
140113instance Functor List where
141114 fmap = map
142115
143−
144116---- Applicative functors/Idioms
145117
146118infixl 2 <$>
@@ -149,7 +121,6 @@ class Functor f => Applicative (f : Set -> Set) where
149121 pure : a -> f a
150122 (<$>) : f (a -> b) -> f a -> f b
151123
152−
153124---- some mathematical operations
154125
155126%include "math.h"
@@ -191,7 +162,6 @@ floor x = prim__floatFloor x
191162ceiling : Float -> Float
192163ceiling x = prim__floatCeil x
193164
194−
195165-- Ranges
196166
197167count : Num a => a -> a -> a -> List a
@@ -244,7 +214,6 @@ openFile f m = fopen f (modeStr m) where
244214 modeStr Write = "w"
245215 modeStr ReadWrite = "r+"
246216
247−
248217do_fclose : Ptr -> IO ()
249218do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h
250219
@@ -288,6 +257,4 @@ readFile fn = do h <- openFile fn Read
288257 readFile' h (contents ++ l)
289258 )
290259 else (return contents)
291−
292−
293260