git.iko.soy/Idris-dev
on master help sign in
Made braces optional
b0f47e1Edwin Brady
lib/builtins.idr+29−36
compare with master
unifiedsplit
@@ -91,50 +91,42 @@ intToBool x = True
91boolOp : (a -> a -> Int) -> a -> a -> Bool
91boolOp : (a -> a -> Int) -> a -> a -> Bool
92boolOp op x y = intToBool (op x y)
92boolOp op x y = intToBool (op x y)
93
93
94−class Eq a where {
94+class Eq a where
95 (==) : a -> a -> Bool
95 (==) : a -> a -> Bool
96 (/=) : a -> a -> Bool
96 (/=) : a -> a -> Bool
97
97
98 x /= y = not (x == y)
98 x /= y = not (x == y)
99 x == y = not (x /= y)
99 x == y = not (x /= y)
100−}
101
100
102−instance Eq Int where {
101+instance Eq Int where
103 (==) = boolOp prim__eqInt
102 (==) = boolOp prim__eqInt
104−}
105
103
106−instance Eq Integer where {
104+instance Eq Integer where
107 (==) = boolOp prim__eqBigInt
105 (==) = boolOp prim__eqBigInt
108−}
109
106
110−instance Eq Float where {
107+instance Eq Float where
111 (==) = boolOp prim__eqFloat
108 (==) = boolOp prim__eqFloat
112−}
113
109
114−instance Eq Char where {
110+instance Eq Char where
115 (==) = boolOp prim__eqChar
111 (==) = boolOp prim__eqChar
116−}
117
112
118−instance Eq String where {
113+instance Eq String where
119 (==) = boolOp prim__eqString
114 (==) = boolOp prim__eqString
120−}
121
115
122data Ordering = LT | EQ | GT
116data Ordering = LT | EQ | GT
123
117
124−class Eq a => Ord a where {
118+class Eq a => Ord a where
125 compare : a -> a -> Ordering
119 compare : a -> a -> Ordering
126
120
127 (<) : a -> a -> Bool
121 (<) : a -> a -> Bool
128− (<) x y with (compare x y) {
122+ (<) x y with (compare x y)
129 (<) x y | LT = True
123 (<) x y | LT = True
130 (<) x y | _ = False
124 (<) x y | _ = False
131− }
132
125
133 (>) : a -> a -> Bool
126 (>) : a -> a -> Bool
134− (>) x y with (compare x y) {
127+ (>) x y with (compare x y)
135 (>) x y | GT = True
128 (>) x y | GT = True
136 (>) x y | _ = False
129 (>) x y | _ = False
137− }
138
130
139 (<=) : a -> a -> Bool
131 (<=) : a -> a -> Bool
140 (<=) x y = x < y || x == y
132 (<=) x y = x < y || x == y
@@ -147,40 +139,40 @@ class Eq a => Ord a where {
147
139
148 min : a -> a -> a
140 min : a -> a -> a
149 min x y = if (x < y) then x else y
141 min x y = if (x < y) then x else y
150−}
151
142
152
143
144+
153−instance Ord Int where {
145+instance Ord Int where
154 compare x y = if (x == y) then EQ else
146 compare x y = if (x == y) then EQ else
155 if (boolOp prim__ltInt x y) then LT else
147 if (boolOp prim__ltInt x y) then LT else
156 GT
148 GT
157−}
158
149
150+
159−instance Ord Integer where {
151+instance Ord Integer where
160 compare x y = if (x == y) then EQ else
152 compare x y = if (x == y) then EQ else
161 if (boolOp prim__ltBigInt x y) then LT else
153 if (boolOp prim__ltBigInt x y) then LT else
162 GT
154 GT
163−}
164
155
156+
165−instance Ord Float where {
157+instance Ord Float where
166 compare x y = if (x == y) then EQ else
158 compare x y = if (x == y) then EQ else
167 if (boolOp prim__ltFloat x y) then LT else
159 if (boolOp prim__ltFloat x y) then LT else
168 GT
160 GT
169−}
170
161
162+
171−instance Ord Char where {
163+instance Ord Char where
172 compare x y = if (x == y) then EQ else
164 compare x y = if (x == y) then EQ else
173 if (boolOp prim__ltChar x y) then LT else
165 if (boolOp prim__ltChar x y) then LT else
174 GT
166 GT
175−}
176
167
168+
177−instance Ord String where {
169+instance Ord String where
178 compare x y = if (x == y) then EQ else
170 compare x y = if (x == y) then EQ else
179 if (boolOp prim__ltString x y) then LT else
171 if (boolOp prim__ltString x y) then LT else
180 GT
172 GT
181−}
182
173
174+
183−class (Eq a, Ord a) => Num a where {
175+class (Eq a, Ord a) => Num a where
184 (+) : a -> a -> a
176 (+) : a -> a -> a
185 (-) : a -> a -> a
177 (-) : a -> a -> a
186 (*) : a -> a -> a
178 (*) : a -> a -> a
@@ -189,32 +181,32 @@ class (Eq a, Ord a) => Num a where {
189 abs x = if (x < 0) then (-x) else x
181 abs x = if (x < 0) then (-x) else x
190
182
191 fromInteger : Int -> a
183 fromInteger : Int -> a
192−}
193
184
194
185
186+
195−instance Num Int where {
187+instance Num Int where
196 (+) = prim__addInt
188 (+) = prim__addInt
197 (-) = prim__subInt
189 (-) = prim__subInt
198 (*) = prim__mulInt
190 (*) = prim__mulInt
199
191
200 fromInteger = id
192 fromInteger = id
201−}
202
193
194+
203−instance Num Integer where {
195+instance Num Integer where
204 (+) = prim__addBigInt
196 (+) = prim__addBigInt
205 (-) = prim__subBigInt
197 (-) = prim__subBigInt
206 (*) = prim__mulBigInt
198 (*) = prim__mulBigInt
207
199
208 fromInteger = prim__intToBigInt
200 fromInteger = prim__intToBigInt
209−}
210
201
202+
211−instance Num Float where {
203+instance Num Float where
212 (+) = prim__addFloat
204 (+) = prim__addFloat
213 (-) = prim__subFloat
205 (-) = prim__subFloat
214 (*) = prim__mulFloat
206 (*) = prim__mulFloat
215
207
216 fromInteger = prim__intToFloat
208 fromInteger = prim__intToFloat
217−}
209+
218
210
219div : Int -> Int -> Int
211div : Int -> Int -> Int
220div = prim__divInt
212div = prim__divInt
@@ -244,3 +236,4 @@ rev : String -> String
244rev = prim__strRev
236rev = prim__strRev
245
237
246}
238}
239+
lib/io.idr+1−2
@@ -29,11 +29,10 @@ interpFTy FPtr = Ptr
29interpFTy FUnit = ()
29interpFTy FUnit = ()
30
30
31ForeignTy : (xs:List FTy) -> (t:FTy) -> Set
31ForeignTy : (xs:List FTy) -> (t:FTy) -> Set
32−ForeignTy xs t = mkForeign' (rev xs) (IO (interpFTy t)) where {
32+ForeignTy xs t = mkForeign' (rev xs) (IO (interpFTy t)) where
33 mkForeign' : List FTy -> Set -> Set
33 mkForeign' : List FTy -> Set -> Set
34 mkForeign' Nil ty = ty
34 mkForeign' Nil ty = ty
35 mkForeign' (s :: ss) ty = mkForeign' ss (interpFTy s -> ty)
35 mkForeign' (s :: ss) ty = mkForeign' ss (interpFTy s -> ty)
36−}
37
36
38
37
39data Foreign : Set -> Set where
38data Foreign : Set -> Set where
lib/network/cgi.idr+28−32
@@ -45,8 +45,9 @@ getAction : CGI a -> CGIInfo -> IO (a, CGIInfo)
45getAction (MkCGI act) = act
45getAction (MkCGI act) = act
46
46
47instance Monad CGI where {
47instance Monad CGI where {
48− (>>=) (MkCGI f) k = MkCGI (\s => do { v <- f s
48+ (>>=) (MkCGI f) k = MkCGI (\s => do v <- f s
49− getAction (k (fst v)) (snd v) })
49+ getAction (k (fst v)) (snd v)
50+ )
50
51
51 return v = MkCGI (\s => return (v, s))
52 return v = MkCGI (\s => return (v, s))
52}
53}
@@ -64,70 +65,65 @@ lift op = MkCGI (\st => do { x <- op
64
65
65abstract
66abstract
66output : String -> CGI ()
67output : String -> CGI ()
67−output s = do { i <- getInfo
68+output s = do i <- getInfo
68− setInfo (add_Output s i) }
69+ setInfo (add_Output s i)
69
70
70abstract
71abstract
71queryVars : CGI Vars
72queryVars : CGI Vars
72−queryVars = do { i <- getInfo
73+queryVars = do i <- getInfo
73− return (get_GET i) }
74+ return (get_GET i)
74
75
75abstract
76abstract
76postVars : CGI Vars
77postVars : CGI Vars
77−postVars = do { i <- getInfo
78+postVars = do i <- getInfo
78− return (get_POST i) }
79+ return (get_POST i)
79
80
80abstract
81abstract
81cookieVars : CGI Vars
82cookieVars : CGI Vars
82−cookieVars = do { i <- getInfo
83+cookieVars = do i <- getInfo
83− return (get_Cookies i) }
84+ return (get_Cookies i)
84
85
85abstract
86abstract
86queryVar : String -> CGI (Maybe String)
87queryVar : String -> CGI (Maybe String)
87−queryVar x = do { vs <- queryVars
88+queryVar x = do vs <- queryVars
88− return (lookup x vs) }
89+ return (lookup x vs)
89
90
90getOutput : CGI String
91getOutput : CGI String
91−getOutput = do { i <- getInfo
92+getOutput = do i <- getInfo
92− return (get_Output i) }
93+ return (get_Output i)
93
94
94getHeaders : CGI String
95getHeaders : CGI String
95−getHeaders = do { i <- getInfo
96+getHeaders = do i <- getInfo
96− return (get_Headers i) }
97+ return (get_Headers i)
97
98
98abstract
99abstract
99flushHeaders : CGI ()
100flushHeaders : CGI ()
100−flushHeaders = do { o <- getHeaders
101+flushHeaders = do o <- getHeaders
101− lift (putStrLn o)
102+ lift (putStrLn o)
102− }
103
103
104abstract
104abstract
105flush : CGI ()
105flush : CGI ()
106−flush = do { o <- getOutput
106+flush = do o <- getOutput
107− lift (putStr o)
107+ lift (putStr o)
108− }
109
108
110getVars : List Char -> String -> List (String, String)
109getVars : List Char -> String -> List (String, String)
111getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)
110getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)
112− where {
111+ where
113 readVar : String -> Maybe (String, String)
112 readVar : String -> Maybe (String, String)
114− readVar xs with split (\x => x == '=') xs {
113+ readVar xs with (split (\x => x == '=') xs)
115 | [k, v] = Just (trim k, trim v)
114 | [k, v] = Just (trim k, trim v)
116 | _ = Nothing
115 | _ = Nothing
117− }
118− }
119
116
120getContent : Int -> IO String
117getContent : Int -> IO String
121−getContent x = getC x "" where {
118+getContent x = getC x "" where
122 getC : Int -> String -> IO String
119 getC : Int -> String -> IO String
123 getC 0 acc = return $ rev acc
120 getC 0 acc = return $ rev acc
124− getC n acc = do { x <- getChar
121+ getC n acc = do x <- getChar
125− getC (n-1) (strCons x acc) }
122+ getC (n-1) (strCons x acc)
126−}
127
123
128abstract
124abstract
129runCGI : CGI a -> IO a
125runCGI : CGI a -> IO a
130−runCGI prog = do {
126+runCGI prog = do
131 clen_in <- getEnv "CONTENT_LENGTH"
127 clen_in <- getEnv "CONTENT_LENGTH"
132 let clen = prim__strToInt clen_in
128 let clen = prim__strToInt clen_in
133 content <- getContent clen
129 content <- getContent clen
@@ -145,5 +141,5 @@ runCGI prog = do {
145 putStrLn (get_Headers (snd p))
141 putStrLn (get_Headers (snd p))
146 putStr (get_Output (snd p))
142 putStr (get_Output (snd p))
147 return (fst p)
143 return (fst p)
148−}
144+
149
145
lib/prelude.idr+72−73
@@ -13,114 +13,114 @@ import prelude.char
13
13
14-- Show and instances
14-- Show and instances
15
15
16−class Show a where {
16+class Show a where
17 show : a -> String
17 show : a -> String
18−}
19
18
19+
20−instance Show Nat where {
20+instance Show Nat where
21 show O = "O"
21 show O = "O"
22 show (S k) = "s" ++ show k
22 show (S k) = "s" ++ show k
23−}
24
23
24+
25−instance Show Int where {
25+instance Show Int where
26 show = prim__intToStr
26 show = prim__intToStr
27−}
28
27
28+
29−instance Show Integer where {
29+instance Show Integer where
30 show = prim__bigIntToStr
30 show = prim__bigIntToStr
31−}
32
31
32+
33−instance Show Float where {
33+instance Show Float where
34 show = prim__floatToStr
34 show = prim__floatToStr
35−}
36
35
36+
37−instance Show Char where {
37+instance Show Char where
38 show x = strCons x ""
38 show x = strCons x ""
39−}
40
39
40+
41−instance Show String where {
41+instance Show String where
42 show = id
42 show = id
43−}
44
43
44+
45−instance Show Bool where {
45+instance Show Bool where
46 show True = "True"
46 show True = "True"
47 show False = "False"
47 show False = "False"
48−}
49
48
49+
50−instance (Show a, Show b) => Show (a, b) where {
50+instance (Show a, Show b) => Show (a, b) where
51 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
51 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
52−}
53
52
53+
54−instance Show a => Show (List a) where {
54+instance Show a => Show (List a) where
55− show xs = "[" ++ show' xs ++ "]" where {
55+ show xs = "[" ++ show' xs ++ "]" where
56 show' : Show a => List a -> String
56 show' : Show a => List a -> String
57 show' [] = ""
57 show' [] = ""
58 show' [x] = show x
58 show' [x] = show x
59 show' (x :: xs) = show x ++ ", " ++ show' xs
59 show' (x :: xs) = show x ++ ", " ++ show' xs
60− }
60+
61−}
61+
62
62
63−instance Show a => Show (Vect a n) where {
63+instance Show a => Show (Vect a n) where
64− show xs = "[" ++ show' xs ++ "]" where {
64+ show xs = "[" ++ show' xs ++ "]" where
65 show' : Show a => Vect a n -> String
65 show' : Show a => Vect a n -> String
66 show' [] = ""
66 show' [] = ""
67 show' [x] = show x
67 show' [x] = show x
68 show' (x :: xs) = show x ++ ", " ++ show' xs
68 show' (x :: xs) = show x ++ ", " ++ show' xs
69− }
69+
70−}
71
70
71+
72−instance Show a => Show (Maybe a) where {
72+instance Show a => Show (Maybe a) where
73 show Nothing = "Nothing"
73 show Nothing = "Nothing"
74 show (Just x) = "Just " ++ show x
74 show (Just x) = "Just " ++ show x
75−}
75+
76
76
77---- Monad and instances
77---- Monad and instances
78
78
79infixl 5 >>=
79infixl 5 >>=
80
80
81−class Monad (m : Set -> Set) where {
81+class Monad (m : Set -> Set) where
82 return : a -> m a
82 return : a -> m a
83 (>>=) : m a -> (a -> m b) -> m b
83 (>>=) : m a -> (a -> m b) -> m b
84−}
85
84
85+
86−class Monad m => MonadPlus (m : Set -> Set) where {
86+class Monad m => MonadPlus (m : Set -> Set) where
87 mplus : m a -> m a -> m a
87 mplus : m a -> m a -> m a
88 mzero : m a
88 mzero : m a
89−}
90
89
90+
91−class Monad m => MonadFail (m : Set -> Set) where {
91+class Monad m => MonadFail (m : Set -> Set) where
92 fail : String -> m ()
92 fail : String -> m ()
93−}
94
93
94+
95−instance Monad IO where {
95+instance Monad IO where
96 return t = io_return t
96 return t = io_return t
97 b >>= k = io_bind b k
97 b >>= k = io_bind b k
98−}
99
98
99+
100−instance Monad Maybe where {
100+instance Monad Maybe where
101 return t = Just t
101 return t = Just t
102
102
103 Nothing >>= k = Nothing
103 Nothing >>= k = Nothing
104 (Just x) >>= k = k x
104 (Just x) >>= k = k x
105−}
106
105
106+
107−instance MonadPlus Maybe where {
107+instance MonadPlus Maybe where
108 mzero = Nothing
108 mzero = Nothing
109
109
110 mplus (Just x) _ = Just x
110 mplus (Just x) _ = Just x
111 mplus Nothing (Just y) = Just y
111 mplus Nothing (Just y) = Just y
112 mplus Nothing Nothing = Nothing
112 mplus Nothing Nothing = Nothing
113−}
114
113
114+
115−instance Monad List where {
115+instance Monad List where
116 return x = [x]
116 return x = [x]
117 m >>= f = concatMap f m
117 m >>= f = concatMap f m
118−}
119
118
119+
120−instance MonadPlus List where {
120+instance MonadPlus List where
121 mzero = []
121 mzero = []
122 mplus = app
122 mplus = app
123−}
123+
124
124
125guard : MonadPlus m => Bool -> m ()
125guard : MonadPlus m => Bool -> m ()
126guard True = return ()
126guard True = return ()
@@ -128,27 +128,27 @@ guard False = mzero
128
128
129---- Functors
129---- Functors
130
130
131−class Functor (f : Set -> Set) where {
131+class Functor (f : Set -> Set) where
132 fmap : (a -> b) -> f a -> f b
132 fmap : (a -> b) -> f a -> f b
133−}
134
133
134+
135−instance Functor Maybe where {
135+instance Functor Maybe where
136 fmap f (Just x) = Just (f x)
136 fmap f (Just x) = Just (f x)
137 fmap f Nothing = Nothing
137 fmap f Nothing = Nothing
138−}
139
138
139+
140−instance Functor List where {
140+instance Functor List where
141 fmap = map
141 fmap = map
142−}
142+
143
143
144---- Applicative functors/Idioms
144---- Applicative functors/Idioms
145
145
146infixl 2 <$>
146infixl 2 <$>
147
147
148−class Functor f => Applicative (f : Set -> Set) where {
148+class Functor f => Applicative (f : Set -> Set) where
149 pure : a -> f a
149 pure : a -> f a
150 (<$>) : f (a -> b) -> f a -> f b
150 (<$>) : f (a -> b) -> f a -> f b
151−}
151+
152
152
153---- some mathematical operations
153---- some mathematical operations
154
154
@@ -232,18 +232,18 @@ do_fopen : String -> String -> IO Ptr
232do_fopen f m = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
232do_fopen f m = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
233
233
234fopen : String -> String -> IO File
234fopen : String -> String -> IO File
235−fopen f m = do { h <- do_fopen f m
235+fopen f m = do h <- do_fopen f m
236− return (FHandle h) }
236+ return (FHandle h)
237
237
238data Mode = Read | Write | ReadWrite
238data Mode = Read | Write | ReadWrite
239
239
240openFile : String -> Mode -> IO File
240openFile : String -> Mode -> IO File
241−openFile f m = fopen f (modeStr m) where {
241+openFile f m = fopen f (modeStr m) where
242 modeStr : Mode -> String
242 modeStr : Mode -> String
243 modeStr Read = "r"
243 modeStr Read = "r"
244 modeStr Write = "w"
244 modeStr Write = "w"
245 modeStr ReadWrite = "r+"
245 modeStr ReadWrite = "r+"
246−}
246+
247
247
248do_fclose : Ptr -> IO ()
248do_fclose : Ptr -> IO ()
249do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h
249do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h
@@ -267,28 +267,27 @@ do_feof : Ptr -> IO Int
267do_feof h = mkForeign (FFun "feof" [FPtr] FInt) h
267do_feof h = mkForeign (FFun "feof" [FPtr] FInt) h
268
268
269feof : File -> IO Bool
269feof : File -> IO Bool
270−feof (FHandle h) = do { eof <- do_feof h
270+feof (FHandle h) = do eof <- do_feof h
271− return (not (eof == 0)) }
271+ return (not (eof == 0))
272
272
273while : |(test : IO Bool) -> |(body : IO ()) -> IO ()
273while : |(test : IO Bool) -> |(body : IO ()) -> IO ()
274−while t b = do { v <- t
274+while t b = do v <- t
275− if v then (do { b; while t b }) else return ()
275+ if v then (do { b; while t b }) else return ()
276− }
276+
277
277
278readFile : String -> IO String
278readFile : String -> IO String
279−readFile fn = do { h <- openFile fn Read
279+readFile fn = do h <- openFile fn Read
280− c <- readFile' h ""
280+ c <- readFile' h ""
281− closeFile h
281+ closeFile h
282− return c
282+ return c
283− }
284− where {
283+ where
285 readFile' : File -> String -> IO String
284 readFile' : File -> String -> IO String
286 readFile' h contents =
285 readFile' h contents =
287− do { x <- feof h
286+ do x <- feof h
288− if (not x) then (do { l <- fread h
287+ if (not x) then (do l <- fread h
289− readFile' h (contents ++ l)
288+ readFile' h (contents ++ l)
290− })
289+ )
291 else (return contents)
290 else (return contents)
292− }
291+
293− }
292+
294
293
lib/prelude/list.idr+6−12
@@ -10,11 +10,10 @@ infixr 7 ::
10data List a = Nil | (::) a (List a)
10data List a = Nil | (::) a (List a)
11
11
12rev : List a -> List a
12rev : List a -> List a
13−rev xs = revAcc [] xs where {
13+rev xs = revAcc [] xs where
14 revAcc : List a -> List a -> List a
14 revAcc : List a -> List a -> List a
15 revAcc acc [] = acc
15 revAcc acc [] = acc
16 revAcc acc (x :: xs) = revAcc (x :: acc) xs
16 revAcc acc (x :: xs) = revAcc (x :: acc) xs
17−}
18
17
19app : List a -> List a -> List a
18app : List a -> List a -> List a
20app [] xs = xs
19app [] xs = xs
@@ -44,10 +43,9 @@ concatMap f (x :: xs) = app (f x) (concatMap f xs)
44
43
45mapMaybe : (a -> Maybe b) -> List a -> List b
44mapMaybe : (a -> Maybe b) -> List a -> List b
46mapMaybe f [] = []
45mapMaybe f [] = []
47−mapMaybe f (x :: xs) = case f x of {
46+mapMaybe f (x :: xs) = case f x of
48 Nothing => mapMaybe f xs
47 Nothing => mapMaybe f xs
49 | Just v => v :: mapMaybe f xs
48 | Just v => v :: mapMaybe f xs
50− }
51
49
52filter : (y -> Bool) -> List y -> List y
50filter : (y -> Bool) -> List y -> List y
53filter pred [] = []
51filter pred [] = []
@@ -66,7 +64,7 @@ sort : Ord a => List a -> List a
66sort [] = []
64sort [] = []
67sort [x] = [x]
65sort [x] = [x]
68sort xs = let (x, y) = split xs in
66sort xs = let (x, y) = split xs in
69− merge (sort x) (sort y) where {
67+ merge (sort x) (sort y) where
70 splitrec : List a -> List a -> (List a -> List a) -> (List a, List a)
68 splitrec : List a -> List a -> (List a -> List a) -> (List a, List a)
71 splitrec (_ :: _ :: xs) (y :: ys) zs = splitrec xs ys (zs . ((::) y))
69 splitrec (_ :: _ :: xs) (y :: ys) zs = splitrec xs ys (zs . ((::) y))
72 splitrec _ ys zs = (zs [], ys)
70 splitrec _ ys zs = (zs [], ys)
@@ -79,24 +77,20 @@ sort xs = let (x, y) = split xs in
79 merge [] ys = ys
77 merge [] ys = ys
80 merge (x :: xs) (y :: ys) = if (x < y) then (x :: merge xs (y :: ys))
78 merge (x :: xs) (y :: ys) = if (x < y) then (x :: merge xs (y :: ys))
81 else (y :: merge (x :: xs) ys)
79 else (y :: merge (x :: xs) ys)
82−}
83
80
84span : (a -> Bool) -> List a -> (List a, List a)
81span : (a -> Bool) -> List a -> (List a, List a)
85span p [] = ([], [])
82span p [] = ([], [])
86−span p (x :: xs) with p x {
83+span p (x :: xs) with (p x)
87− | True with span p xs {
84+ | True with (span p xs)
88 | (ys, zs) = (x :: ys, zs)
85 | (ys, zs) = (x :: ys, zs)
89− }
90 | False = ([], x :: xs)
86 | False = ([], x :: xs)
91−}
92
87
93break : (a -> Bool) -> List a -> (List a, List a)
88break : (a -> Bool) -> List a -> (List a, List a)
94break p = span (not . p)
89break p = span (not . p)
95
90
96split : (a -> Bool) -> List a -> List (List a)
91split : (a -> Bool) -> List a -> List (List a)
97split p [] = []
92split p [] = []
98−split p xs = case break p xs of {
93+split p xs = case break p xs of
99 (chunk, []) => [chunk]
94 (chunk, []) => [chunk]
100 | (chunk, (c :: rest)) => chunk :: split p rest
95 | (chunk, (c :: rest)) => chunk :: split p rest
101− }
102
96
lib/prelude/nat.idr+3−6
@@ -25,28 +25,25 @@ mult : Nat -> Nat -> Nat
25mult O y = O
25mult O y = O
26mult (S k) y = plus y (mult k y)
26mult (S k) y = plus y (mult k y)
27
27
28−instance Eq Nat where {
28+instance Eq Nat where
29 O == O = True
29 O == O = True
30 (S x) == (S y) = x == y
30 (S x) == (S y) = x == y
31 O == (S y) = False
31 O == (S y) = False
32 (S x) == O = False
32 (S x) == O = False
33−}
34
33
35−instance Ord Nat where {
34+instance Ord Nat where
36 compare O O = EQ
35 compare O O = EQ
37 compare O (S k) = LT
36 compare O (S k) = LT
38 compare (S k) O = GT
37 compare (S k) O = GT
39 compare (S x) (S y) = compare x y
38 compare (S x) (S y) = compare x y
40−}
41
39
42−instance Num Nat where {
40+instance Num Nat where
43 (+) = plus
41 (+) = plus
44 (-) = sub
42 (-) = sub
45 (*) = mult
43 (*) = mult
46
44
47 fromInteger 0 = O
45 fromInteger 0 = O
48 fromInteger n = if (n > 0) then (S (fromInteger (n-1))) else O
46 fromInteger n = if (n > 0) then (S (fromInteger (n-1))) else O
49−}
50
47
51plusnO : (m : Nat) -> m + O = m
48plusnO : (m : Nat) -> m + O = m
52plusnO O = refl
49plusnO O = refl
lib/prelude/strings.idr+7−12
@@ -19,31 +19,26 @@ strTail' x p = prim__strTail x
19-- we need the 'believe_me' because the operations are primitives
19-- we need the 'believe_me' because the operations are primitives
20
20
21strM : (x : String) -> StrM x
21strM : (x : String) -> StrM x
22−strM x with choose (not (x == "")) {
22+strM x with (choose (not (x == "")))
23 strM x | (Left p) = believe_me (StrCons (strHead' x p) (strTail' x p))
23 strM x | (Left p) = believe_me (StrCons (strHead' x p) (strTail' x p))
24 strM x | (Right p) = believe_me StrNil
24 strM x | (Right p) = believe_me StrNil
25−}
26
25
27unpack : String -> List Char
26unpack : String -> List Char
28−unpack s with strM s {
27+unpack s with (strM s)
29 unpack "" | StrNil = []
28 unpack "" | StrNil = []
30 unpack (strCons x xs) | (StrCons _ _) = x :: unpack xs
29 unpack (strCons x xs) | (StrCons _ _) = x :: unpack xs
31−}
32
30
33pack : List Char -> String
31pack : List Char -> String
34pack [] = ""
32pack [] = ""
35pack (x :: xs) = strCons x (pack xs)
33pack (x :: xs) = strCons x (pack xs)
36
34
37span : (Char -> Bool) -> String -> (String, String)
35span : (Char -> Bool) -> String -> (String, String)
38−span p xs with strM xs {
36+span p xs with (strM xs)
39 span p "" | StrNil = ("", "")
37 span p "" | StrNil = ("", "")
40− span p (strCons x xs) | (StrCons _ _) with p x {
38+ span p (strCons x xs) | (StrCons _ _) with (p x)
41− | True with span p xs {
39+ | True with (span p xs)
42 | (ys, zs) = (strCons x ys, zs)
40 | (ys, zs) = (strCons x ys, zs)
43− }
44 | False = ("", strCons x xs)
41 | False = ("", strCons x xs)
45− }
46−}
47
42
48break : (Char -> Bool) -> String -> (String, String)
43break : (Char -> Bool) -> String -> (String, String)
49break p = span (not . p)
44break p = span (not . p)
@@ -52,11 +47,11 @@ split : (Char -> Bool) -> String -> List String
52split p xs = map pack (split p (unpack xs))
47split p xs = map pack (split p (unpack xs))
53
48
54ltrim : String -> String
49ltrim : String -> String
55−ltrim xs with strM xs {
50+ltrim xs with (strM xs)
56 ltrim "" | StrNil = ""
51 ltrim "" | StrNil = ""
57 ltrim (strCons x xs) | StrCons _ _
52 ltrim (strCons x xs) | StrCons _ _
58 = if (isSpace x) then (ltrim xs) else (strCons x xs)
53 = if (isSpace x) then (ltrim xs) else (strCons x xs)
59−}
60
54
61trim : String -> String
55trim : String -> String
62trim xs = ltrim (rev (ltrim (rev xs)))
56trim xs = ltrim (rev (ltrim (rev xs)))
57+
samples/interp.idr+1−3
@@ -7,7 +7,7 @@ interpTy TyInt = Int
7interpTy TyBool = Bool
7interpTy TyBool = Bool
8interpTy (TyFun s t) = interpTy s -> interpTy t
8interpTy (TyFun s t) = interpTy s -> interpTy t
9
9
10−using (G : Vect Ty n) {
10+using (G : Vect Ty n)
11
11
12 data Env : Vect Ty n -> Set where
12 data Env : Vect Ty n -> Set where
13 Nil : Env Nil
13 Nil : Env Nil
@@ -70,8 +70,6 @@ using (G : Vect Ty n) {
70 (\y => Bind (App eDouble (Val x))
70 (\y => Bind (App eDouble (Val x))
71 (\z => App (App eAdd (Val y)) (Val z))))))
71 (\z => App (App eAdd (Val y)) (Val z))))))
72
72
73−}
74−
75test : Int
73test : Int
76test = interp [] eProg 2 2
74test = interp [] eProg 2 2
77
75
src/Idris/AbsSyntax.hs+2−1
@@ -51,6 +51,7 @@ data IState = IState { tt_ctxt :: Context,
51 errLine :: Maybe Int,
51 errLine :: Maybe Int,
52 lastParse :: Maybe Name,
52 lastParse :: Maybe Name,
53 indent_stack :: [Int],
53 indent_stack :: [Int],
54+ brace_stack :: [Maybe Int],
54 hide_list :: [(Name, Maybe Accessibility)],
55 hide_list :: [(Name, Maybe Accessibility)],
55 default_access :: Accessibility,
56 default_access :: Accessibility,
56 ibc_write :: [IBCWrite]
57 ibc_write :: [IBCWrite]
@@ -73,7 +74,7 @@ data IBCWrite = IBCFix FixDecl
73
74
74idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
75idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
75 "" defaultOpts 6 [] [] [] [] [] [] [] []
76 "" defaultOpts 6 [] [] [] [] [] [] [] []
76− Nothing Nothing Nothing [] [] Hidden []
77+ Nothing Nothing Nothing [] [] [] Hidden []
77
78
78-- The monad for the main REPL - reading and processing files and updating
79-- The monad for the main REPL - reading and processing files and updating
79-- global state (hence the IO inner monad).
80-- global state (hence the IO inner monad).
src/Idris/Parser.hs+69−40
@@ -161,7 +161,7 @@ last_indent :: IParser Int
161last_indent = do ist <- getState
161last_indent = do ist <- getState
162 case indent_stack ist of
162 case indent_stack ist of
163 (x : xs) -> return x
163 (x : xs) -> return x
164− _ -> return (-1)
164+ _ -> return 1
165
165
166indent :: IParser Int
166indent :: IParser Int
167indent = do pos <- getPosition
167indent = do pos <- getPosition
@@ -172,11 +172,32 @@ pop_indent = do ist <- getState
172 let (x : xs) = indent_stack ist
172 let (x : xs) = indent_stack ist
173 setState (ist { indent_stack = xs })
173 setState (ist { indent_stack = xs })
174
174
175+open_block :: IParser ()
176+open_block = do lchar '{'
177+ ist <- getState
178+ setState (ist { brace_stack = Nothing : brace_stack ist })
179+ <|> do ist <- getState
180+ lvl <- indent
181+ setState (ist { brace_stack = Just lvl : brace_stack ist })
182+
183+close_block :: IParser ()
184+close_block = do ist <- getState
185+ bs <- case brace_stack ist of
186+ Nothing : xs -> do lchar '}'
187+ return xs
188+ Just lvl : xs -> do i <- indent
189+ inp <- getInput
190+-- trace (show (take 10 inp, i, lvl)) $
191+ if (i >= lvl && take 1 inp /= ")")
192+ then fail "Not end of block"
193+ else return xs
194+ setState (ist { brace_stack = bs })
195+
175pTerminator = do lchar ';'; pop_indent
196pTerminator = do lchar ';'; pop_indent
176 <|> do c <- indent; l <- last_indent
197 <|> do c <- indent; l <- last_indent
177 if (c <= l) then pop_indent
198 if (c <= l) then pop_indent
178 else fail "Not a terminator"
199 else fail "Not a terminator"
179− <|> do i <- getInput; if (take 1 i == "}") then pop_indent
200+ <|> do i <- getInput; if (take 1 i == "}" || take 1 i == ")") then pop_indent
180 else fail "Not a terminator"
201 else fail "Not a terminator"
181 <|> lookAhead eof
202 <|> lookAhead eof
182
203
@@ -189,6 +210,20 @@ pKeepTerminator
189 else fail "Not a terminator"
210 else fail "Not a terminator"
190 <|> lookAhead eof
211 <|> lookAhead eof
191
212
213+notEndApp = do c <- indent; l <- last_indent
214+ i <- getInput
215+ if (c <= l) then fail "Terminator"
216+ else return ()
217+
218+notEndBlock = do ist <- getState
219+ case brace_stack ist of
220+ Just lvl : xs -> do i <- indent
221+ inp <- getInput
222+ if (i < lvl || take 1 inp == ")")
223+ then fail "End of block"
224+ else return ()
225+ _ -> return ()
226+
192pfc :: IParser FC
227pfc :: IParser FC
193pfc = do s <- getPosition
228pfc = do s <- getPosition
194 let (dir, file) = splitFileName (sourceName s)
229 let (dir, file) = splitFileName (sourceName s)
@@ -252,7 +287,9 @@ pFullExpr syn
252 return $ desugar syn i x
287 return $ desugar syn i x
253
288
254pDecl :: SyntaxInfo -> IParser [PDecl]
289pDecl :: SyntaxInfo -> IParser [PDecl]
255−pDecl syn
290+pDecl syn = do notEndBlock
291+ pDeclBody where
292+ pDeclBody
256 = do d <- pDecl' syn
293 = do d <- pDecl' syn
257 i <- getState
294 i <- getState
258 let d' = fmap (desugar syn i) d
295 let d' = fmap (desugar syn i) d
@@ -270,7 +307,8 @@ pDecl syn
270
307
271pFunDecl :: SyntaxInfo -> IParser [PDecl]
308pFunDecl :: SyntaxInfo -> IParser [PDecl]
272pFunDecl syn
309pFunDecl syn
310+ = try (do notEndBlock
273− = try (do d <- pFunDecl' syn
311+ d <- pFunDecl' syn
274 i <- getState
312 i <- getState
275 let d' = fmap (desugar syn i) d
313 let d' = fmap (desugar syn i) d
276 return [d'])
314 return [d'])
@@ -351,10 +389,10 @@ pUsing syn =
351 lchar '('
389 lchar '('
352 ns <- tyDeclList syn
390 ns <- tyDeclList syn
353 lchar ')'
391 lchar ')'
354− lchar '{'
392+ open_block
355 let uvars = using syn
393 let uvars = using syn
356 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
394 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
357− lchar '}'
395+ close_block
358 return (concat ds)
396 return (concat ds)
359
397
360pParams :: SyntaxInfo -> IParser [PDecl]
398pParams :: SyntaxInfo -> IParser [PDecl]
@@ -374,9 +412,9 @@ pNamespace :: SyntaxInfo -> IParser [PDecl]
374pNamespace syn =
412pNamespace syn =
375 do reserved "namespace";
413 do reserved "namespace";
376 n <- identifier
414 n <- identifier
377− lchar '{'
415+ open_block
378 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
416 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
379− lchar '}'
417+ close_block
380 return [PNamespace n (concat ds)]
418 return [PNamespace n (concat ds)]
381
419
382expandNS :: SyntaxInfo -> Name -> Name
420expandNS :: SyntaxInfo -> Name -> Name
@@ -415,9 +453,9 @@ pClass syn = do acc <- pAccessibility
415 cons <- pConstList syn
453 cons <- pConstList syn
416 n_in <- pName; let n = expandNS syn n_in
454 n_in <- pName; let n = expandNS syn n_in
417 cs <- many1 carg
455 cs <- many1 carg
418− reserved "where"; lchar '{'
456+ reserved "where"; open_block
419− ds <- many1 $ pFunDecl syn;
457+ ds <- many1 $ pFunDecl syn
420− lchar '}'
458+ close_block
421 let allDs = concat ds
459 let allDs = concat ds
422 accData acc n (concatMap declared allDs)
460 accData acc n (concatMap declared allDs)
423 return [PClass syn fc cons n cs allDs]
461 return [PClass syn fc cons n cs allDs]
@@ -435,9 +473,9 @@ pInstance syn = do reserved "instance"
435 args <- many1 (pSimpleExpr syn)
473 args <- many1 (pSimpleExpr syn)
436 let sc = PApp fc (PRef fc cn) (map pexp args)
474 let sc = PApp fc (PRef fc cn) (map pexp args)
437 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
475 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
438− reserved "where"; lchar '{'
476+ reserved "where"; open_block
439− ds <- many1 $ pFunDecl syn;
477+ ds <- many1 $ pFunDecl syn
440− lchar '}'
478+ close_block
441 return [PInstance syn fc cs cn args t (concat ds)]
479 return [PInstance syn fc cs cn args t (concat ds)]
442
480
443--------- Expressions ---------
481--------- Expressions ---------
@@ -565,9 +603,9 @@ pSimpleExpr syn =
565 lchar '}'
603 lchar '}'
566 return (PTactics ts)
604 return (PTactics ts)
567 <|> do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
605 <|> do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
568− lchar '{'
606+ open_block
569 opts <- sepBy1 (pCaseOpt syn) (lchar '|')
607 opts <- sepBy1 (pCaseOpt syn) (lchar '|')
570− lchar '}'
608+ close_block
571 return (PCase fc scr opts)
609 return (PCase fc scr opts)
572 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
610 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
573 <|> try (pList syn)
611 <|> try (pList syn)
@@ -661,15 +699,6 @@ pApp syn = do f <- pSimpleExpr syn
661 pArg syn)
699 pArg syn)
662 return (PApp fc f args)
700 return (PApp fc f args)
663
701
664−notEndApp = do c <- indent; l <- last_indent
665− i <- getInput
666− if (c <= l || take 1 i == "}"
667− || take 1 i == ")"
668− || take 1 i == ","
669− || take 2 i == "->"
670− || take 2 i == "=>") then fail "Terminator"
671− else return ()
672−
673pArg :: SyntaxInfo -> IParser PArg
702pArg :: SyntaxInfo -> IParser PArg
674pArg syn = try (pImplicitArg syn)
703pArg syn = try (pImplicitArg syn)
675 <|> try (pConstraintArg syn)
704 <|> try (pConstraintArg syn)
@@ -774,11 +803,11 @@ pComprehension syn
774 addGuard x = x
803 addGuard x = x
775
804
776pDoBlock syn
805pDoBlock syn
777− = do reserved "do"; lchar '{'
806+ = do reserved "do"; open_block
778 push_indent
807 push_indent
779− ds <- many1 (do x <- pDo syn; pKeepTerminator; return x)
808+ ds <- many1 (do notEndBlock; x <- pDo syn; pKeepTerminator; return x)
780 pop_indent
809 pop_indent
781− lchar '}'
810+ close_block
782 return (PDoBlock ds)
811 return (PDoBlock ds)
783
812
784pDo syn
813pDo syn
@@ -973,11 +1002,11 @@ pClause syn
973 let capp = PApp fc (PRef fc n)
1002 let capp = PApp fc (PRef fc n)
974 (iargs ++ cargs ++ map pexp args)
1003 (iargs ++ cargs ++ map pexp args)
975 reserved "with"
1004 reserved "with"
976− wval <- pExpr syn
1005+ wval <- pSimpleExpr syn
977− lchar '{'
1006+ open_block
978 ds <- many1 $ pFunDecl syn
1007 ds <- many1 $ pFunDecl syn
979 let withs = map (fillLHSD n capp wargs) $ concat ds
1008 let withs = map (fillLHSD n capp wargs) $ concat ds
980− lchar '}'
1009+ close_block
981 ist <- getState
1010 ist <- getState
982 setState (ist { lastParse = Just n })
1011 setState (ist { lastParse = Just n })
983 pop_indent
1012 pop_indent
@@ -985,11 +1014,11 @@ pClause syn
985
1014
986 <|> try (do wargs <- many1 (pWExpr syn)
1015 <|> try (do wargs <- many1 (pWExpr syn)
987 reserved "with"
1016 reserved "with"
988− wval <- pExpr syn
1017+ wval <- pSimpleExpr syn
989− lchar '{'
1018+ open_block
990 ds <- many1 $ pFunDecl syn
1019 ds <- many1 $ pFunDecl syn
991 let withs = concat ds
1020 let withs = concat ds
992− lchar '}'
1021+ close_block
993 return $ PWithR wargs wval withs)
1022 return $ PWithR wargs wval withs)
994
1023
995 <|> do push_indent
1024 <|> do push_indent
@@ -1018,10 +1047,10 @@ pClause syn
1018 fc <- pfc
1047 fc <- pfc
1019 wargs <- many (pWExpr syn)
1048 wargs <- many (pWExpr syn)
1020 reserved "with"
1049 reserved "with"
1021− wval <- pExpr syn
1050+ wval <- pSimpleExpr syn
1022− lchar '{'
1051+ open_block
1023 ds <- many1 $ pFunDecl syn
1052 ds <- many1 $ pFunDecl syn
1024− lchar '}'
1053+ close_block
1025 ist <- getState
1054 ist <- getState
1026 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1055 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1027 let withs = map (fillLHSD n capp wargs) $ concat ds
1056 let withs = map (fillLHSD n capp wargs) $ concat ds
@@ -1043,10 +1072,10 @@ pWExpr syn = do lchar '|'; pExpr' syn
1043
1072
1044pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1073pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1045pWhereblock n syn
1074pWhereblock n syn
1046− = do reserved "where"; lchar '{'
1075+ = do reserved "where"; open_block
1047− ds <- many1 $ pFunDecl syn;
1076+ ds <- many1 $ pFunDecl syn
1048 let dns = concatMap (concatMap declared) ds
1077 let dns = concatMap (concatMap declared) ds
1049− lchar '}';
1078+ close_block
1050 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1079 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1051
1080
1052pDirective :: IParser [PDecl]
1081pDirective :: IParser [PDecl]
test/test006/test006.idr+2−5
@@ -7,18 +7,15 @@ data Parity : Nat -> Set where
7parity : (n:Nat) -> Parity n
7parity : (n:Nat) -> Parity n
8parity O = even {n=O}
8parity O = even {n=O}
9parity (S O) = odd {n=O}
9parity (S O) = odd {n=O}
10−parity (S (S k)) with parity k {
10+parity (S (S k)) with (parity k)
11 parity (S (S (j + j))) | even ?= even {n=S j}
11 parity (S (S (j + j))) | even ?= even {n=S j}
12 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
12 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
13−}
14−
15
13
16natToBin : Nat -> List Bool
14natToBin : Nat -> List Bool
17natToBin O = Nil
15natToBin O = Nil
18−natToBin k with parity k {
16+natToBin k with (parity k)
19 natToBin (j + j) | even = False :: natToBin j
17 natToBin (j + j) | even = False :: natToBin j
20 natToBin (S (j + j)) | odd = True :: natToBin j
18 natToBin (S (j + j)) | odd = True :: natToBin j
21−}
22
19
23main : IO ()
20main : IO ()
24main = print (natToBin 42)
21main = print (natToBin 42)
test/test007/test007.idr+11−20
@@ -1,40 +1,34 @@
1module main
1module main
2
2
3−instance Applicative Maybe where {
3+instance Applicative Maybe where
4 (Just f) <$> (Just a) = Just (f a)
4 (Just f) <$> (Just a) = Just (f a)
5 Nothing <$> Nothing = Nothing
5 Nothing <$> Nothing = Nothing
6
6
7 pure x = Just x
7 pure x = Just x
8−}
9
8
10data Expr = Var String
9data Expr = Var String
11 | Val Int
10 | Val Int
12 | Add Expr Expr
11 | Add Expr Expr
13
12
14−
15data Eval : Set -> Set where
13data Eval : Set -> Set where
16 MkEval : (List (String, Int) -> Maybe a) -> Eval a
14 MkEval : (List (String, Int) -> Maybe a) -> Eval a
17
15
18fetch : String -> Eval Int
16fetch : String -> Eval Int
19−fetch x = MkEval (\e => fetchVal e) where {
17+fetch x = MkEval (\e => fetchVal e) where
20 fetchVal : List (String, Int) -> Maybe Int
18 fetchVal : List (String, Int) -> Maybe Int
21 fetchVal [] = Nothing
19 fetchVal [] = Nothing
22 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
20 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
23−}
24
21
25−instance Functor Eval where {
22+instance Functor Eval where
26 fmap f (MkEval g) = MkEval (\e => fmap f (g e))
23 fmap f (MkEval g) = MkEval (\e => fmap f (g e))
27−}
28
24
29−instance Applicative Eval where {
25+instance Applicative Eval where
30 pure x = MkEval (\e => Just x)
26 pure x = MkEval (\e => Just x)
31
27
32− (<$>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where {
28+ (<$>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where
33 appAux : Maybe (a -> b) -> Maybe a -> Maybe b
29 appAux : Maybe (a -> b) -> Maybe a -> Maybe b
34 appAux (Just fx) (Just gx) = Just (fx gx)
30 appAux (Just fx) (Just gx) = Just (fx gx)
35 appAux _ _ = Nothing
31 appAux _ _ = Nothing
36− }
37−}
38
32
39eval : Expr -> Eval Int
33eval : Expr -> Eval Int
40eval (Var x) = fetch x
34eval (Var x) = fetch x
@@ -42,16 +36,13 @@ eval (Val x) = [| x |]
42eval (Add x y) = [| eval x + eval y |]
36eval (Add x y) = [| eval x + eval y |]
43
37
44runEval : List (String, Int) -> Expr -> Maybe Int
38runEval : List (String, Int) -> Expr -> Maybe Int
45−runEval env e with eval e {
39+runEval env e with (eval e) {
46 | MkEval envFn = envFn env
40 | MkEval envFn = envFn env
47}
41}
48
42
49main : IO ()
43main : IO ()
50−main = do { print [| (*2) (Just 4) |]
44+main = do print [| (*2) (Just 4) |]
51− print [| plus (Just 4) (Just 5) |]
45+ print [| plus (Just 4) (Just 5) |]
52− print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))
46+ print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))
53− print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))
47+ print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))
54− }
48+
55−
56−
57−
tutorial/examples/binary.idr+8−11
@@ -5,11 +5,10 @@ data Binary : Nat -> Set where
5 | bO : Binary n -> Binary (n + n)
5 | bO : Binary n -> Binary (n + n)
6 | bI : Binary n -> Binary (S (n + n))
6 | bI : Binary n -> Binary (S (n + n))
7
7
8−instance Show (Binary n) where {
8+instance Show (Binary n) where
9 show (bO x) = show x ++ "0"
9 show (bO x) = show x ++ "0"
10 show (bI x) = show x ++ "1"
10 show (bI x) = show x ++ "1"
11 show bEnd = ""
11 show bEnd = ""
12−}
13
12
14data Parity : Nat -> Set where
13data Parity : Nat -> Set where
15 even : Parity (n + n)
14 even : Parity (n + n)
@@ -18,28 +17,26 @@ data Parity : Nat -> Set where
18parity : (n:Nat) -> Parity n
17parity : (n:Nat) -> Parity n
19parity O = even {n=O}
18parity O = even {n=O}
20parity (S O) = odd {n=O}
19parity (S O) = odd {n=O}
21−parity (S (S k)) with parity k {
20+parity (S (S k)) with (parity k)
22 parity (S (S (j + j))) | even ?= even {n=S j}
21 parity (S (S (j + j))) | even ?= even {n=S j}
23 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
22 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
24−}
25
23
26natToBin : (n:Nat) -> Binary n
24natToBin : (n:Nat) -> Binary n
27natToBin O = bEnd
25natToBin O = bEnd
28−natToBin (S k) with parity k {
26+natToBin (S k) with (parity k)
29 natToBin (S (j + j)) | even = bI (natToBin j)
27 natToBin (S (j + j)) | even = bI (natToBin j)
30 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
28 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
31−}
32
29
33intToNat : Int -> Nat
30intToNat : Int -> Nat
34intToNat 0 = O
31intToNat 0 = O
35intToNat x = if (x>0) then (S (intToNat (x-1))) else O
32intToNat x = if (x>0) then (S (intToNat (x-1))) else O
36
33
37main : IO ()
34main : IO ()
38−main = do { putStr "Enter a number: "
35+main = do putStr "Enter a number: "
39− x <- getLine
36+ x <- getLine
40− let n = prim__strToInt x
37+ let n = prim__strToInt x
41− let b = natToBin (fromInteger n)
38+ let b = natToBin (fromInteger n)
42− print b }
39+ print b
43
40
44---------- Proofs ----------
41---------- Proofs ----------
45
42
tutorial/examples/bmain.idr+2−3
@@ -3,7 +3,6 @@ module main
3import btree
3import btree
4
4
5main : IO ()
5main : IO ()
6−main = do { let t = toTree [1,8,2,7,9,3]
6+main = do let t = toTree [1,8,2,7,9,3]
7− print (toList t)
7+ print (toList t)
8− }
9
8
tutorial/examples/classes.idr+3−4
@@ -1,8 +1,7 @@
1m_add : Maybe Int -> Maybe Int -> Maybe Int
1m_add : Maybe Int -> Maybe Int -> Maybe Int
2−m_add x y = do { x' <- x -- Extract value from x
2+m_add x y = do x' <- x -- Extract value from x
3− y' <- y -- Extract value from y
3+ y' <- y -- Extract value from y
4− return (x' + y') -- Add them
4+ return (x' + y') -- Add them
5− }
6
5
7m_add' : Maybe Int -> Maybe Int -> Maybe Int
6m_add' : Maybe Int -> Maybe Int -> Maybe Int
8m_add' x y = [ x' + y' | x' <- x, y' <- y ]
7m_add' x y = [ x' + y' | x' <- x, y' <- y ]
tutorial/examples/foo.idr+2−4
@@ -1,12 +1,10 @@
1module foo
1module foo
2
2
3−namespace x {
3+namespace x
4 test : Int -> Int
4 test : Int -> Int
5 test x = x * 2
5 test x = x * 2
6−}
7
6
8−namespace y {
7+namespace y
9 test : String -> String
8 test : String -> String
10 test x = x ++ x
9 test x = x ++ x
11−}
12
10
tutorial/examples/interp.idr+4−8
@@ -7,7 +7,7 @@ interpTy TyInt = Int
7interpTy TyBool = Bool
7interpTy TyBool = Bool
8interpTy (TyFun s t) = interpTy s -> interpTy t
8interpTy (TyFun s t) = interpTy s -> interpTy t
9
9
10−using (G : Vect Ty n) {
10+using (G : Vect Ty n)
11
11
12 data Env : Vect Ty n -> Set where
12 data Env : Vect Ty n -> Set where
13 Nil : Env Nil
13 Nil : Env Nil
@@ -54,15 +54,11 @@ using (G : Vect Ty n) {
54 fact = Lam (If (Op (==) (Var stop) (Val 0))
54 fact = Lam (If (Op (==) (Var stop) (Val 0))
55 (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1))) (Var stop)))
55 (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1))) (Var stop)))
56
56
57−}
58−
59testFac : Int
57testFac : Int
60testFac = interp [] fact 4
58testFac = interp [] fact 4
61
59
62main : IO ()
60main : IO ()
63−main = do { putStr "Enter a number: "
61+main = do putStr "Enter a number: "
64− x <- getLine
62+ x <- getLine
65− print (interp [] fact (prim__strToInt x))
63+ print (interp [] fact (prim__strToInt x))
66− }
67−
68
64
tutorial/examples/letbind.idr+1−2
@@ -11,7 +11,6 @@ showPerson p = let MkPerson name age = p in
11 name ++ " is " ++ show age ++ " years old"
11 name ++ " is " ++ show age ++ " years old"
12
12
13splitAt : Char -> String -> (String, String)
13splitAt : Char -> String -> (String, String)
14−splitAt c x = case break (== c) x of {
14+splitAt c x = case break (== c) x of
15 (x, y) => (x, strTail y)
15 (x, y) => (x, strTail y)
16− }
17
16
tutorial/examples/usefultypes.idr+1−2
@@ -14,8 +14,7 @@ list_lookup O (x :: xs) = Just x
14list_lookup (S k) (x :: xs) = list_lookup k xs
14list_lookup (S k) (x :: xs) = list_lookup k xs
15
15
16lookup_default : Nat -> List a -> a -> a
16lookup_default : Nat -> List a -> a -> a
17−lookup_default i xs def = case list_lookup i xs of {
17+lookup_default i xs def = case list_lookup i xs of
18 Nothing => def
18 Nothing => def
19 | Just x => x
19 | Just x => x
20− }
21
20
tutorial/examples/views.idr+2−5
@@ -7,18 +7,15 @@ data Parity : Nat -> Set where
7parity : (n:Nat) -> Parity n
7parity : (n:Nat) -> Parity n
8parity O = even {n=O}
8parity O = even {n=O}
9parity (S O) = odd {n=O}
9parity (S O) = odd {n=O}
10−parity (S (S k)) with parity k {
10+parity (S (S k)) with (parity k)
11 parity (S (S (j + j))) | even ?= even {n=S j}
11 parity (S (S (j + j))) | even ?= even {n=S j}
12 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
12 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
13−}
14−
15
13
16natToBin : Nat -> List Bool
14natToBin : Nat -> List Bool
17natToBin O = Nil
15natToBin O = Nil
18−natToBin k with parity k {
16+natToBin k with (parity k)
19 natToBin (j + j) | even = False :: natToBin j
17 natToBin (j + j) | even = False :: natToBin j
20 natToBin (S (j + j)) | odd = True :: natToBin j
18 natToBin (S (j + j)) | odd = True :: natToBin j
21−}
22
19
23
20
24---------- Proofs ----------
21---------- Proofs ----------