git.iko.soy/Idris-dev
on master help sign in
Debraced rest of lib
c5e3aa7Edwin Brady
lib/prelude.idr−33
compare with master
unifiedsplit
@@ -16,49 +16,38 @@ import prelude.char
16class Show a where
16class Show a where
17 show : a -> String
17 show : a -> String
18
18
19−
20instance Show Nat where
19instance Show Nat where
21 show O = "O"
20 show O = "O"
22 show (S k) = "s" ++ show k
21 show (S k) = "s" ++ show k
23
22
24−
25instance Show Int where
23instance Show Int where
26 show = prim__intToStr
24 show = prim__intToStr
27
25
28−
29instance Show Integer where
26instance Show Integer where
30 show = prim__bigIntToStr
27 show = prim__bigIntToStr
31
28
32−
33instance Show Float where
29instance Show Float where
34 show = prim__floatToStr
30 show = prim__floatToStr
35
31
36−
37instance Show Char where
32instance Show Char where
38 show x = strCons x ""
33 show x = strCons x ""
39
34
40−
41instance Show String where
35instance Show String where
42 show = id
36 show = id
43
37
44−
45instance Show Bool where
38instance Show Bool where
46 show True = "True"
39 show True = "True"
47 show False = "False"
40 show False = "False"
48
41
49−
50instance (Show a, Show b) => Show (a, b) where
42instance (Show a, Show b) => Show (a, b) where
51 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
43 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
52
44
53−
54instance Show a => Show (List a) where
45instance Show a => Show (List a) where
55 show xs = "[" ++ show' xs ++ "]" where
46 show xs = "[" ++ show' xs ++ "]" where
56 show' : Show a => List a -> String
47 show' : Show a => List a -> String
57 show' [] = ""
48 show' [] = ""
58 show' [x] = show x
49 show' [x] = show x
59 show' (x :: xs) = show x ++ ", " ++ show' xs
50 show' (x :: xs) = show x ++ ", " ++ show' xs
60−
61−
62
51
63instance Show a => Show (Vect a n) where
52instance Show a => Show (Vect a n) where
64 show xs = "[" ++ show' xs ++ "]" where
53 show xs = "[" ++ show' xs ++ "]" where
@@ -66,14 +55,11 @@ instance Show a => Show (Vect a n) where
66 show' [] = ""
55 show' [] = ""
67 show' [x] = show x
56 show' [x] = show x
68 show' (x :: xs) = show x ++ ", " ++ show' xs
57 show' (x :: xs) = show x ++ ", " ++ show' xs
69−
70−
71
58
72instance Show a => Show (Maybe a) where
59instance Show a => Show (Maybe a) where
73 show Nothing = "Nothing"
60 show Nothing = "Nothing"
74 show (Just x) = "Just " ++ show x
61 show (Just x) = "Just " ++ show x
75
62
76−
77---- Monad and instances
63---- Monad and instances
78
64
79infixl 5 >>=
65infixl 5 >>=
@@ -82,28 +68,20 @@ class Monad (m : Set -> Set) where
82 return : a -> m a
68 return : a -> m a
83 (>>=) : m a -> (a -> m b) -> m b
69 (>>=) : m a -> (a -> m b) -> m b
84
70
85−
86class Monad m => MonadPlus (m : Set -> Set) where
71class Monad m => MonadPlus (m : Set -> Set) where
87 mplus : m a -> m a -> m a
72 mplus : m a -> m a -> m a
88 mzero : m a
73 mzero : m a
89
74
90−
91−class Monad m => MonadFail (m : Set -> Set) where
92− fail : String -> m ()
93−
94−
95instance Monad IO where
75instance Monad IO where
96 return t = io_return t
76 return t = io_return t
97 b >>= k = io_bind b k
77 b >>= k = io_bind b k
98
78
99−
100instance Monad Maybe where
79instance Monad Maybe where
101 return t = Just t
80 return t = Just t
102
81
103 Nothing >>= k = Nothing
82 Nothing >>= k = Nothing
104 (Just x) >>= k = k x
83 (Just x) >>= k = k x
105
84
106−
107instance MonadPlus Maybe where
85instance MonadPlus Maybe where
108 mzero = Nothing
86 mzero = Nothing
109
87
@@ -111,17 +89,14 @@ instance MonadPlus Maybe where
111 mplus Nothing (Just y) = Just y
89 mplus Nothing (Just y) = Just y
112 mplus Nothing Nothing = Nothing
90 mplus Nothing Nothing = Nothing
113
91
114−
115instance Monad List where
92instance Monad List where
116 return x = [x]
93 return x = [x]
117 m >>= f = concatMap f m
94 m >>= f = concatMap f m
118
95
119−
120instance MonadPlus List where
96instance MonadPlus List where
121 mzero = []
97 mzero = []
122 mplus = app
98 mplus = app
123
99
124−
125guard : MonadPlus m => Bool -> m ()
100guard : MonadPlus m => Bool -> m ()
126guard True = return ()
101guard True = return ()
127guard False = mzero
102guard False = mzero
@@ -131,16 +106,13 @@ guard False = mzero
131class Functor (f : Set -> Set) where
106class Functor (f : Set -> Set) where
132 fmap : (a -> b) -> f a -> f b
107 fmap : (a -> b) -> f a -> f b
133
108
134−
135instance Functor Maybe where
109instance Functor Maybe where
136 fmap f (Just x) = Just (f x)
110 fmap f (Just x) = Just (f x)
137 fmap f Nothing = Nothing
111 fmap f Nothing = Nothing
138
112
139−
140instance Functor List where
113instance Functor List where
141 fmap = map
114 fmap = map
142
115
143−
144---- Applicative functors/Idioms
116---- Applicative functors/Idioms
145
117
146infixl 2 <$>
118infixl 2 <$>
@@ -149,7 +121,6 @@ class Functor f => Applicative (f : Set -> Set) where
149 pure : a -> f a
121 pure : a -> f a
150 (<$>) : f (a -> b) -> f a -> f b
122 (<$>) : f (a -> b) -> f a -> f b
151
123
152−
153---- some mathematical operations
124---- some mathematical operations
154
125
155%include "math.h"
126%include "math.h"
@@ -191,7 +162,6 @@ floor x = prim__floatFloor x
191ceiling : Float -> Float
162ceiling : Float -> Float
192ceiling x = prim__floatCeil x
163ceiling x = prim__floatCeil x
193
164
194−
195-- Ranges
165-- Ranges
196
166
197count : Num a => a -> a -> a -> List a
167count : Num a => a -> a -> a -> List a
@@ -244,7 +214,6 @@ openFile f m = fopen f (modeStr m) where
244 modeStr Write = "w"
214 modeStr Write = "w"
245 modeStr ReadWrite = "r+"
215 modeStr ReadWrite = "r+"
246
216
247−
248do_fclose : Ptr -> IO ()
217do_fclose : Ptr -> IO ()
249do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h
218do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h
250
219
@@ -288,6 +257,4 @@ readFile fn = do h <- openFile fn Read
288 readFile' h (contents ++ l)
257 readFile' h (contents ++ l)
289 )
258 )
290 else (return contents)
259 else (return contents)
291−
292−
293
260
lib/prelude/vect.idr+1−2
@@ -8,11 +8,10 @@ data Fin : Nat -> Set where
8 fO : Fin (S k)
8 fO : Fin (S k)
9 | fS : Fin k -> Fin (S k)
9 | fS : Fin k -> Fin (S k)
10
10
11−instance Eq (Fin n) where {
11+instance Eq (Fin n) where
12 fO == fO = True
12 fO == fO = True
13 (fS k) == (fS k') = k == k'
13 (fS k) == (fS k') = k == k'
14 _ == _ = False
14 _ == _ = False
15−}
16
15
17infixr 7 ::
16infixr 7 ::
18
17
lib/system.idr+5−7
@@ -5,10 +5,9 @@ import prelude
5%access public
5%access public
6
6
7getArgs : IO (List String)
7getArgs : IO (List String)
8−getArgs = do { n <- numArgs
8+getArgs = do n <- numArgs
9− ga' [] 0 n
9+ ga' [] 0 n
10− }
11− where {
10+ where
12 numArgs : IO Int
11 numArgs : IO Int
13 numArgs = mkForeign (FFun "epic_numArgs" [] FInt)
12 numArgs = mkForeign (FFun "epic_numArgs" [] FInt)
14
13
@@ -17,9 +16,8 @@ getArgs = do { n <- numArgs
17
16
18 ga' : List String -> Int -> Int -> IO (List String)
17 ga' : List String -> Int -> Int -> IO (List String)
19 ga' acc i n = if (i == n) then (return $ rev acc) else
18 ga' acc i n = if (i == n) then (return $ rev acc) else
20− do { arg <- getArg i
19+ do arg <- getArg i
21− ga' (arg :: acc) (i+1) n }
20+ ga' (arg :: acc) (i+1) n
22−}
23
21
24getEnv : String -> IO String
22getEnv : String -> IO String
25getEnv x = mkForeign (FFun "getenv" [FString] FString) x
23getEnv x = mkForeign (FFun "getenv" [FString] FString) x