git.iko.soy/Idris-dev
on master help sign in
Made braces optional

(at the expense of 'with' now needing the expression to be tested in brackets) do notation doesn't quite behave right - the first token after the do block must be at a lower level of indentation, which means putting it in brackets is awkward.

commitb0f47e176969104cf4213e47f287cfb4e8d50c32 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 7 Jan 2012, 14:19 (15 years ago) parent4804676
20 files changed+254−281
compare with master
unifiedsplit
lib/builtins.idr+29−36 lib/io.idr+1−2 lib/network/cgi.idr+28−32 lib/prelude.idr+72−73 lib/prelude/list.idr+6−12 lib/prelude/nat.idr+3−6 lib/prelude/strings.idr+7−12 samples/interp.idr+1−3 src/Idris/AbsSyntax.hs+2−1 src/Idris/Parser.hs+69−40 test/test006/test006.idr+2−5 test/test007/test007.idr+11−20 tutorial/examples/binary.idr+8−11 tutorial/examples/bmain.idr+2−3 tutorial/examples/classes.idr+3−4 tutorial/examples/foo.idr+2−4 tutorial/examples/interp.idr+4−8 tutorial/examples/letbind.idr+1−2 tutorial/examples/usefultypes.idr+1−2 tutorial/examples/views.idr+2−5
lib/builtins.idr+29−36
@@ -91,50 +91,42 @@ intToBool x = True
9191boolOp : (a -> a -> Int) -> a -> a -> Bool
9292boolOp op x y = intToBool (op x y)
9393
94−class Eq a where {
94+class Eq a where
9595 (==) : a -> a -> Bool
9696 (/=) : a -> a -> Bool
9797
9898 x /= y = not (x == y)
9999 x == y = not (x /= y)
100−}
101100
102−instance Eq Int where {
101+instance Eq Int where
103102 (==) = boolOp prim__eqInt
104−}
105103
106−instance Eq Integer where {
104+instance Eq Integer where
107105 (==) = boolOp prim__eqBigInt
108−}
109106
110−instance Eq Float where {
107+instance Eq Float where
111108 (==) = boolOp prim__eqFloat
112−}
113109
114−instance Eq Char where {
110+instance Eq Char where
115111 (==) = boolOp prim__eqChar
116−}
117112
118−instance Eq String where {
113+instance Eq String where
119114 (==) = boolOp prim__eqString
120−}
121115
122116data Ordering = LT | EQ | GT
123117
124−class Eq a => Ord a where {
118+class Eq a => Ord a where
125119 compare : a -> a -> Ordering
126120
127121 (<) : a -> a -> Bool
128− (<) x y with (compare x y) {
122+ (<) x y with (compare x y)
129123 (<) x y | LT = True
130124 (<) x y | _ = False
131− }
132125
133126 (>) : a -> a -> Bool
134− (>) x y with (compare x y) {
127+ (>) x y with (compare x y)
135128 (>) x y | GT = True
136129 (>) x y | _ = False
137− }
138130
139131 (<=) : a -> a -> Bool
140132 (<=) x y = x < y || x == y
@@ -147,40 +139,40 @@ class Eq a => Ord a where {
147139
148140 min : a -> a -> a
149141 min x y = if (x < y) then x else y
150−}
151142
152143
153−instance Ord Int where {
144+
145+instance Ord Int where
154146 compare x y = if (x == y) then EQ else
155147 if (boolOp prim__ltInt x y) then LT else
156148 GT
157−}
158149
159−instance Ord Integer where {
150+
151+instance Ord Integer where
160152 compare x y = if (x == y) then EQ else
161153 if (boolOp prim__ltBigInt x y) then LT else
162154 GT
163−}
164155
165−instance Ord Float where {
156+
157+instance Ord Float where
166158 compare x y = if (x == y) then EQ else
167159 if (boolOp prim__ltFloat x y) then LT else
168160 GT
169−}
170161
171−instance Ord Char where {
162+
163+instance Ord Char where
172164 compare x y = if (x == y) then EQ else
173165 if (boolOp prim__ltChar x y) then LT else
174166 GT
175−}
176167
177−instance Ord String where {
168+
169+instance Ord String where
178170 compare x y = if (x == y) then EQ else
179171 if (boolOp prim__ltString x y) then LT else
180172 GT
181−}
182173
183−class (Eq a, Ord a) => Num a where {
174+
175+class (Eq a, Ord a) => Num a where
184176 (+) : a -> a -> a
185177 (-) : a -> a -> a
186178 (*) : a -> a -> a
@@ -189,32 +181,32 @@ class (Eq a, Ord a) => Num a where {
189181 abs x = if (x < 0) then (-x) else x
190182
191183 fromInteger : Int -> a
192−}
193184
194185
195−instance Num Int where {
186+
187+instance Num Int where
196188 (+) = prim__addInt
197189 (-) = prim__subInt
198190 (*) = prim__mulInt
199191
200192 fromInteger = id
201−}
202193
203−instance Num Integer where {
194+
195+instance Num Integer where
204196 (+) = prim__addBigInt
205197 (-) = prim__subBigInt
206198 (*) = prim__mulBigInt
207199
208200 fromInteger = prim__intToBigInt
209−}
210201
211−instance Num Float where {
202+
203+instance Num Float where
212204 (+) = prim__addFloat
213205 (-) = prim__subFloat
214206 (*) = prim__mulFloat
215207
216208 fromInteger = prim__intToFloat
217−}
209+
218210
219211div : Int -> Int -> Int
220212div = prim__divInt
@@ -244,3 +236,4 @@ rev : String -> String
244236rev = prim__strRev
245237
246238}
239+
lib/io.idr+1−2
@@ -29,11 +29,10 @@ interpFTy FPtr = Ptr
2929interpFTy FUnit = ()
3030
3131ForeignTy : (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
3333 mkForeign' : List FTy -> Set -> Set
3434 mkForeign' Nil ty = ty
3535 mkForeign' (s :: ss) ty = mkForeign' ss (interpFTy s -> ty)
36−}
3736
3837
3938data Foreign : Set -> Set where
lib/network/cgi.idr+28−32
@@ -45,8 +45,9 @@ getAction : CGI a -> CGIInfo -> IO (a, CGIInfo)
4545getAction (MkCGI act) = act
4646
4747instance Monad CGI where {
48− (>>=) (MkCGI f) k = MkCGI (\s => do { v <- f s
49− getAction (k (fst v)) (snd v) })
48+ (>>=) (MkCGI f) k = MkCGI (\s => do v <- f s
49+ getAction (k (fst v)) (snd v)
50+ )
5051
5152 return v = MkCGI (\s => return (v, s))
5253}
@@ -64,70 +65,65 @@ lift op = MkCGI (\st => do { x <- op
6465
6566abstract
6667output : String -> CGI ()
67−output s = do { i <- getInfo
68− setInfo (add_Output s i) }
68+output s = do i <- getInfo
69+ setInfo (add_Output s i)
6970
7071abstract
7172queryVars : CGI Vars
72−queryVars = do { i <- getInfo
73− return (get_GET i) }
73+queryVars = do i <- getInfo
74+ return (get_GET i)
7475
7576abstract
7677postVars : CGI Vars
77−postVars = do { i <- getInfo
78− return (get_POST i) }
78+postVars = do i <- getInfo
79+ return (get_POST i)
7980
8081abstract
8182cookieVars : CGI Vars
82−cookieVars = do { i <- getInfo
83− return (get_Cookies i) }
83+cookieVars = do i <- getInfo
84+ return (get_Cookies i)
8485
8586abstract
8687queryVar : String -> CGI (Maybe String)
87−queryVar x = do { vs <- queryVars
88− return (lookup x vs) }
88+queryVar x = do vs <- queryVars
89+ return (lookup x vs)
8990
9091getOutput : CGI String
91−getOutput = do { i <- getInfo
92− return (get_Output i) }
92+getOutput = do i <- getInfo
93+ return (get_Output i)
9394
9495getHeaders : CGI String
95−getHeaders = do { i <- getInfo
96− return (get_Headers i) }
96+getHeaders = do i <- getInfo
97+ return (get_Headers i)
9798
9899abstract
99100flushHeaders : CGI ()
100−flushHeaders = do { o <- getHeaders
101− lift (putStrLn o)
102− }
101+flushHeaders = do o <- getHeaders
102+ lift (putStrLn o)
103103
104104abstract
105105flush : CGI ()
106−flush = do { o <- getOutput
107− lift (putStr o)
108− }
106+flush = do o <- getOutput
107+ lift (putStr o)
109108
110109getVars : List Char -> String -> List (String, String)
111110getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)
112− where {
111+ where
113112 readVar : String -> Maybe (String, String)
114− readVar xs with split (\x => x == '=') xs {
113+ readVar xs with (split (\x => x == '=') xs)
115114 | [k, v] = Just (trim k, trim v)
116115 | _ = Nothing
117− }
118− }
119116
120117getContent : Int -> IO String
121−getContent x = getC x "" where {
118+getContent x = getC x "" where
122119 getC : Int -> String -> IO String
123120 getC 0 acc = return $ rev acc
124− getC n acc = do { x <- getChar
125− getC (n-1) (strCons x acc) }
126−}
121+ getC n acc = do x <- getChar
122+ getC (n-1) (strCons x acc)
127123
128124abstract
129125runCGI : CGI a -> IO a
130−runCGI prog = do {
126+runCGI prog = do
131127 clen_in <- getEnv "CONTENT_LENGTH"
132128 let clen = prim__strToInt clen_in
133129 content <- getContent clen
@@ -145,5 +141,5 @@ runCGI prog = do {
145141 putStrLn (get_Headers (snd p))
146142 putStr (get_Output (snd p))
147143 return (fst p)
148−}
144+
149145
lib/prelude.idr+72−73
@@ -13,114 +13,114 @@ import prelude.char
1313
1414-- Show and instances
1515
16−class Show a where {
16+class Show a where
1717 show : a -> String
18−}
1918
20−instance Show Nat where {
19+
20+instance Show Nat where
2121 show O = "O"
2222 show (S k) = "s" ++ show k
23−}
2423
25−instance Show Int where {
24+
25+instance Show Int where
2626 show = prim__intToStr
27−}
2827
29−instance Show Integer where {
28+
29+instance Show Integer where
3030 show = prim__bigIntToStr
31−}
3231
33−instance Show Float where {
32+
33+instance Show Float where
3434 show = prim__floatToStr
35−}
3635
37−instance Show Char where {
36+
37+instance Show Char where
3838 show x = strCons x ""
39−}
4039
41−instance Show String where {
40+
41+instance Show String where
4242 show = id
43−}
4443
45−instance Show Bool where {
44+
45+instance Show Bool where
4646 show True = "True"
4747 show False = "False"
48−}
4948
50−instance (Show a, Show b) => Show (a, b) where {
49+
50+instance (Show a, Show b) => Show (a, b) where
5151 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
52−}
5352
54−instance Show a => Show (List a) where {
55− show xs = "[" ++ show' xs ++ "]" where {
53+
54+instance Show a => Show (List a) where
55+ show xs = "[" ++ show' xs ++ "]" where
5656 show' : Show a => List a -> String
5757 show' [] = ""
5858 show' [x] = show x
5959 show' (x :: xs) = show x ++ ", " ++ show' xs
60− }
61−}
60+
61+
6262
63−instance Show a => Show (Vect a n) where {
64− show xs = "[" ++ show' xs ++ "]" where {
63+instance Show a => Show (Vect a n) where
64+ show xs = "[" ++ show' xs ++ "]" where
6565 show' : Show a => Vect a n -> String
6666 show' [] = ""
6767 show' [x] = show x
6868 show' (x :: xs) = show x ++ ", " ++ show' xs
69− }
70−}
69+
7170
72−instance Show a => Show (Maybe a) where {
71+
72+instance Show a => Show (Maybe a) where
7373 show Nothing = "Nothing"
7474 show (Just x) = "Just " ++ show x
75−}
75+
7676
7777---- Monad and instances
7878
7979infixl 5 >>=
8080
81−class Monad (m : Set -> Set) where {
81+class Monad (m : Set -> Set) where
8282 return : a -> m a
8383 (>>=) : m a -> (a -> m b) -> m b
84−}
8584
86−class Monad m => MonadPlus (m : Set -> Set) where {
85+
86+class Monad m => MonadPlus (m : Set -> Set) where
8787 mplus : m a -> m a -> m a
8888 mzero : m a
89−}
9089
91−class Monad m => MonadFail (m : Set -> Set) where {
90+
91+class Monad m => MonadFail (m : Set -> Set) where
9292 fail : String -> m ()
93−}
9493
95−instance Monad IO where {
94+
95+instance Monad IO where
9696 return t = io_return t
9797 b >>= k = io_bind b k
98−}
9998
100−instance Monad Maybe where {
99+
100+instance Monad Maybe where
101101 return t = Just t
102102
103103 Nothing >>= k = Nothing
104104 (Just x) >>= k = k x
105−}
106105
107−instance MonadPlus Maybe where {
106+
107+instance MonadPlus Maybe where
108108 mzero = Nothing
109109
110110 mplus (Just x) _ = Just x
111111 mplus Nothing (Just y) = Just y
112112 mplus Nothing Nothing = Nothing
113−}
114113
115−instance Monad List where {
114+
115+instance Monad List where
116116 return x = [x]
117117 m >>= f = concatMap f m
118−}
119118
120−instance MonadPlus List where {
119+
120+instance MonadPlus List where
121121 mzero = []
122122 mplus = app
123−}
123+
124124
125125guard : MonadPlus m => Bool -> m ()
126126guard True = return ()
@@ -128,27 +128,27 @@ guard False = mzero
128128
129129---- Functors
130130
131−class Functor (f : Set -> Set) where {
131+class Functor (f : Set -> Set) where
132132 fmap : (a -> b) -> f a -> f b
133−}
134133
135−instance Functor Maybe where {
134+
135+instance Functor Maybe where
136136 fmap f (Just x) = Just (f x)
137137 fmap f Nothing = Nothing
138−}
139138
140−instance Functor List where {
139+
140+instance Functor List where
141141 fmap = map
142−}
142+
143143
144144---- Applicative functors/Idioms
145145
146146infixl 2 <$>
147147
148−class Functor f => Applicative (f : Set -> Set) where {
148+class Functor f => Applicative (f : Set -> Set) where
149149 pure : a -> f a
150150 (<$>) : f (a -> b) -> f a -> f b
151−}
151+
152152
153153---- some mathematical operations
154154
@@ -232,18 +232,18 @@ do_fopen : String -> String -> IO Ptr
232232do_fopen f m = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
233233
234234fopen : String -> String -> IO File
235−fopen f m = do { h <- do_fopen f m
236− return (FHandle h) }
235+fopen f m = do h <- do_fopen f m
236+ return (FHandle h)
237237
238238data Mode = Read | Write | ReadWrite
239239
240240openFile : String -> Mode -> IO File
241−openFile f m = fopen f (modeStr m) where {
241+openFile f m = fopen f (modeStr m) where
242242 modeStr : Mode -> String
243243 modeStr Read = "r"
244244 modeStr Write = "w"
245245 modeStr ReadWrite = "r+"
246−}
246+
247247
248248do_fclose : Ptr -> IO ()
249249do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h
@@ -267,28 +267,27 @@ do_feof : Ptr -> IO Int
267267do_feof h = mkForeign (FFun "feof" [FPtr] FInt) h
268268
269269feof : File -> IO Bool
270−feof (FHandle h) = do { eof <- do_feof h
271− return (not (eof == 0)) }
270+feof (FHandle h) = do eof <- do_feof h
271+ return (not (eof == 0))
272272
273273while : |(test : IO Bool) -> |(body : IO ()) -> IO ()
274−while t b = do { v <- t
275− if v then (do { b; while t b }) else return ()
276− }
274+while t b = do v <- t
275+ if v then (do { b; while t b }) else return ()
276+
277277
278278readFile : String -> IO String
279−readFile fn = do { h <- openFile fn Read
280− c <- readFile' h ""
281− closeFile h
282− return c
283− }
284− where {
279+readFile fn = do h <- openFile fn Read
280+ c <- readFile' h ""
281+ closeFile h
282+ return c
283+ where
285284 readFile' : File -> String -> IO String
286285 readFile' h contents =
287− do { x <- feof h
288− if (not x) then (do { l <- fread h
289− readFile' h (contents ++ l)
290− })
286+ do x <- feof h
287+ if (not x) then (do l <- fread h
288+ readFile' h (contents ++ l)
289+ )
291290 else (return contents)
292− }
293− }
291+
292+
294293
lib/prelude/list.idr+6−12
@@ -10,11 +10,10 @@ infixr 7 ::
1010data List a = Nil | (::) a (List a)
1111
1212rev : List a -> List a
13−rev xs = revAcc [] xs where {
13+rev xs = revAcc [] xs where
1414 revAcc : List a -> List a -> List a
1515 revAcc acc [] = acc
1616 revAcc acc (x :: xs) = revAcc (x :: acc) xs
17−}
1817
1918app : List a -> List a -> List a
2019app [] xs = xs
@@ -44,10 +43,9 @@ concatMap f (x :: xs) = app (f x) (concatMap f xs)
4443
4544mapMaybe : (a -> Maybe b) -> List a -> List b
4645mapMaybe f [] = []
47−mapMaybe f (x :: xs) = case f x of {
46+mapMaybe f (x :: xs) = case f x of
4847 Nothing => mapMaybe f xs
4948 | Just v => v :: mapMaybe f xs
50− }
5149
5250filter : (y -> Bool) -> List y -> List y
5351filter pred [] = []
@@ -66,7 +64,7 @@ sort : Ord a => List a -> List a
6664sort [] = []
6765sort [x] = [x]
6866sort xs = let (x, y) = split xs in
69− merge (sort x) (sort y) where {
67+ merge (sort x) (sort y) where
7068 splitrec : List a -> List a -> (List a -> List a) -> (List a, List a)
7169 splitrec (_ :: _ :: xs) (y :: ys) zs = splitrec xs ys (zs . ((::) y))
7270 splitrec _ ys zs = (zs [], ys)
@@ -79,24 +77,20 @@ sort xs = let (x, y) = split xs in
7977 merge [] ys = ys
8078 merge (x :: xs) (y :: ys) = if (x < y) then (x :: merge xs (y :: ys))
8179 else (y :: merge (x :: xs) ys)
82−}
8380
8481span : (a -> Bool) -> List a -> (List a, List a)
8582span p [] = ([], [])
86−span p (x :: xs) with p x {
87− | True with span p xs {
83+span p (x :: xs) with (p x)
84+ | True with (span p xs)
8885 | (ys, zs) = (x :: ys, zs)
89− }
9086 | False = ([], x :: xs)
91−}
9287
9388break : (a -> Bool) -> List a -> (List a, List a)
9489break p = span (not . p)
9590
9691split : (a -> Bool) -> List a -> List (List a)
9792split p [] = []
98−split p xs = case break p xs of {
93+split p xs = case break p xs of
9994 (chunk, []) => [chunk]
10095 | (chunk, (c :: rest)) => chunk :: split p rest
101− }
10296
lib/prelude/nat.idr+3−6
@@ -25,28 +25,25 @@ mult : Nat -> Nat -> Nat
2525mult O y = O
2626mult (S k) y = plus y (mult k y)
2727
28−instance Eq Nat where {
28+instance Eq Nat where
2929 O == O = True
3030 (S x) == (S y) = x == y
3131 O == (S y) = False
3232 (S x) == O = False
33−}
3433
35−instance Ord Nat where {
34+instance Ord Nat where
3635 compare O O = EQ
3736 compare O (S k) = LT
3837 compare (S k) O = GT
3938 compare (S x) (S y) = compare x y
40−}
4139
42−instance Num Nat where {
40+instance Num Nat where
4341 (+) = plus
4442 (-) = sub
4543 (*) = mult
4644
4745 fromInteger 0 = O
4846 fromInteger n = if (n > 0) then (S (fromInteger (n-1))) else O
49−}
5047
5148plusnO : (m : Nat) -> m + O = m
5249plusnO O = refl
lib/prelude/strings.idr+7−12
@@ -19,31 +19,26 @@ strTail' x p = prim__strTail x
1919-- we need the 'believe_me' because the operations are primitives
2020
2121strM : (x : String) -> StrM x
22−strM x with choose (not (x == "")) {
22+strM x with (choose (not (x == "")))
2323 strM x | (Left p) = believe_me (StrCons (strHead' x p) (strTail' x p))
2424 strM x | (Right p) = believe_me StrNil
25−}
2625
2726unpack : String -> List Char
28−unpack s with strM s {
27+unpack s with (strM s)
2928 unpack "" | StrNil = []
3029 unpack (strCons x xs) | (StrCons _ _) = x :: unpack xs
31−}
3230
3331pack : List Char -> String
3432pack [] = ""
3533pack (x :: xs) = strCons x (pack xs)
3634
3735span : (Char -> Bool) -> String -> (String, String)
38−span p xs with strM xs {
36+span p xs with (strM xs)
3937 span p "" | StrNil = ("", "")
40− span p (strCons x xs) | (StrCons _ _) with p x {
41− | True with span p xs {
38+ span p (strCons x xs) | (StrCons _ _) with (p x)
39+ | True with (span p xs)
4240 | (ys, zs) = (strCons x ys, zs)
43− }
4441 | False = ("", strCons x xs)
45− }
46−}
4742
4843break : (Char -> Bool) -> String -> (String, String)
4944break p = span (not . p)
@@ -52,11 +47,11 @@ split : (Char -> Bool) -> String -> List String
5247split p xs = map pack (split p (unpack xs))
5348
5449ltrim : String -> String
55−ltrim xs with strM xs {
50+ltrim xs with (strM xs)
5651 ltrim "" | StrNil = ""
5752 ltrim (strCons x xs) | StrCons _ _
5853 = if (isSpace x) then (ltrim xs) else (strCons x xs)
59−}
6054
6155trim : String -> String
6256trim xs = ltrim (rev (ltrim (rev xs)))
57+
samples/interp.idr+1−3
@@ -7,7 +7,7 @@ interpTy TyInt = Int
77interpTy TyBool = Bool
88interpTy (TyFun s t) = interpTy s -> interpTy t
99
10−using (G : Vect Ty n) {
10+using (G : Vect Ty n)
1111
1212 data Env : Vect Ty n -> Set where
1313 Nil : Env Nil
@@ -70,8 +70,6 @@ using (G : Vect Ty n) {
7070 (\y => Bind (App eDouble (Val x))
7171 (\z => App (App eAdd (Val y)) (Val z))))))
7272
73−}
74−
7573test : Int
7674test = interp [] eProg 2 2
7775
src/Idris/AbsSyntax.hs+2−1
@@ -51,6 +51,7 @@ data IState = IState { tt_ctxt :: Context,
5151 errLine :: Maybe Int,
5252 lastParse :: Maybe Name,
5353 indent_stack :: [Int],
54+ brace_stack :: [Maybe Int],
5455 hide_list :: [(Name, Maybe Accessibility)],
5556 default_access :: Accessibility,
5657 ibc_write :: [IBCWrite]
@@ -73,7 +74,7 @@ data IBCWrite = IBCFix FixDecl
7374
7475idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
7576 "" defaultOpts 6 [] [] [] [] [] [] [] []
76− Nothing Nothing Nothing [] [] Hidden []
77+ Nothing Nothing Nothing [] [] [] Hidden []
7778
7879-- The monad for the main REPL - reading and processing files and updating
7980-- global state (hence the IO inner monad).
src/Idris/Parser.hs+69−40
@@ -161,7 +161,7 @@ last_indent :: IParser Int
161161last_indent = do ist <- getState
162162 case indent_stack ist of
163163 (x : xs) -> return x
164− _ -> return (-1)
164+ _ -> return 1
165165
166166indent :: IParser Int
167167indent = do pos <- getPosition
@@ -172,11 +172,32 @@ pop_indent = do ist <- getState
172172 let (x : xs) = indent_stack ist
173173 setState (ist { indent_stack = xs })
174174
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+
175196pTerminator = do lchar ';'; pop_indent
176197 <|> do c <- indent; l <- last_indent
177198 if (c <= l) then pop_indent
178199 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
180201 else fail "Not a terminator"
181202 <|> lookAhead eof
182203
@@ -189,6 +210,20 @@ pKeepTerminator
189210 else fail "Not a terminator"
190211 <|> lookAhead eof
191212
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+
192227pfc :: IParser FC
193228pfc = do s <- getPosition
194229 let (dir, file) = splitFileName (sourceName s)
@@ -252,7 +287,9 @@ pFullExpr syn
252287 return $ desugar syn i x
253288
254289pDecl :: SyntaxInfo -> IParser [PDecl]
255−pDecl syn
290+pDecl syn = do notEndBlock
291+ pDeclBody where
292+ pDeclBody
256293 = do d <- pDecl' syn
257294 i <- getState
258295 let d' = fmap (desugar syn i) d
@@ -270,7 +307,8 @@ pDecl syn
270307
271308pFunDecl :: SyntaxInfo -> IParser [PDecl]
272309pFunDecl syn
273− = try (do d <- pFunDecl' syn
310+ = try (do notEndBlock
311+ d <- pFunDecl' syn
274312 i <- getState
275313 let d' = fmap (desugar syn i) d
276314 return [d'])
@@ -351,10 +389,10 @@ pUsing syn =
351389 lchar '('
352390 ns <- tyDeclList syn
353391 lchar ')'
354− lchar '{'
392+ open_block
355393 let uvars = using syn
356394 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
357− lchar '}'
395+ close_block
358396 return (concat ds)
359397
360398pParams :: SyntaxInfo -> IParser [PDecl]
@@ -374,9 +412,9 @@ pNamespace :: SyntaxInfo -> IParser [PDecl]
374412pNamespace syn =
375413 do reserved "namespace";
376414 n <- identifier
377− lchar '{'
415+ open_block
378416 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
379− lchar '}'
417+ close_block
380418 return [PNamespace n (concat ds)]
381419
382420expandNS :: SyntaxInfo -> Name -> Name
@@ -415,9 +453,9 @@ pClass syn = do acc <- pAccessibility
415453 cons <- pConstList syn
416454 n_in <- pName; let n = expandNS syn n_in
417455 cs <- many1 carg
418− reserved "where"; lchar '{'
419− ds <- many1 $ pFunDecl syn;
420− lchar '}'
456+ reserved "where"; open_block
457+ ds <- many1 $ pFunDecl syn
458+ close_block
421459 let allDs = concat ds
422460 accData acc n (concatMap declared allDs)
423461 return [PClass syn fc cons n cs allDs]
@@ -435,9 +473,9 @@ pInstance syn = do reserved "instance"
435473 args <- many1 (pSimpleExpr syn)
436474 let sc = PApp fc (PRef fc cn) (map pexp args)
437475 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
438− reserved "where"; lchar '{'
439− ds <- many1 $ pFunDecl syn;
440− lchar '}'
476+ reserved "where"; open_block
477+ ds <- many1 $ pFunDecl syn
478+ close_block
441479 return [PInstance syn fc cs cn args t (concat ds)]
442480
443481--------- Expressions ---------
@@ -565,9 +603,9 @@ pSimpleExpr syn =
565603 lchar '}'
566604 return (PTactics ts)
567605 <|> do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
568− lchar '{'
606+ open_block
569607 opts <- sepBy1 (pCaseOpt syn) (lchar '|')
570− lchar '}'
608+ close_block
571609 return (PCase fc scr opts)
572610 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
573611 <|> try (pList syn)
@@ -661,15 +699,6 @@ pApp syn = do f <- pSimpleExpr syn
661699 pArg syn)
662700 return (PApp fc f args)
663701
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−
673702pArg :: SyntaxInfo -> IParser PArg
674703pArg syn = try (pImplicitArg syn)
675704 <|> try (pConstraintArg syn)
@@ -774,11 +803,11 @@ pComprehension syn
774803 addGuard x = x
775804
776805pDoBlock syn
777− = do reserved "do"; lchar '{'
806+ = do reserved "do"; open_block
778807 push_indent
779− ds <- many1 (do x <- pDo syn; pKeepTerminator; return x)
808+ ds <- many1 (do notEndBlock; x <- pDo syn; pKeepTerminator; return x)
780809 pop_indent
781− lchar '}'
810+ close_block
782811 return (PDoBlock ds)
783812
784813pDo syn
@@ -973,11 +1002,11 @@ pClause syn
9731002 let capp = PApp fc (PRef fc n)
9741003 (iargs ++ cargs ++ map pexp args)
9751004 reserved "with"
976− wval <- pExpr syn
977− lchar '{'
1005+ wval <- pSimpleExpr syn
1006+ open_block
9781007 ds <- many1 $ pFunDecl syn
9791008 let withs = map (fillLHSD n capp wargs) $ concat ds
980− lchar '}'
1009+ close_block
9811010 ist <- getState
9821011 setState (ist { lastParse = Just n })
9831012 pop_indent
@@ -985,11 +1014,11 @@ pClause syn
9851014
9861015 <|> try (do wargs <- many1 (pWExpr syn)
9871016 reserved "with"
988− wval <- pExpr syn
989− lchar '{'
1017+ wval <- pSimpleExpr syn
1018+ open_block
9901019 ds <- many1 $ pFunDecl syn
9911020 let withs = concat ds
992− lchar '}'
1021+ close_block
9931022 return $ PWithR wargs wval withs)
9941023
9951024 <|> do push_indent
@@ -1018,10 +1047,10 @@ pClause syn
10181047 fc <- pfc
10191048 wargs <- many (pWExpr syn)
10201049 reserved "with"
1021− wval <- pExpr syn
1022− lchar '{'
1050+ wval <- pSimpleExpr syn
1051+ open_block
10231052 ds <- many1 $ pFunDecl syn
1024− lchar '}'
1053+ close_block
10251054 ist <- getState
10261055 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
10271056 let withs = map (fillLHSD n capp wargs) $ concat ds
@@ -1043,10 +1072,10 @@ pWExpr syn = do lchar '|'; pExpr' syn
10431072
10441073pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
10451074pWhereblock n syn
1046− = do reserved "where"; lchar '{'
1047− ds <- many1 $ pFunDecl syn;
1075+ = do reserved "where"; open_block
1076+ ds <- many1 $ pFunDecl syn
10481077 let dns = concatMap (concatMap declared) ds
1049− lchar '}';
1078+ close_block
10501079 return (concat ds, map (\x -> (x, decoration syn x)) dns)
10511080
10521081pDirective :: IParser [PDecl]
test/test006/test006.idr+2−5
@@ -7,18 +7,15 @@ data Parity : Nat -> Set where
77parity : (n:Nat) -> Parity n
88parity O = even {n=O}
99parity (S O) = odd {n=O}
10−parity (S (S k)) with parity k {
10+parity (S (S k)) with (parity k)
1111 parity (S (S (j + j))) | even ?= even {n=S j}
1212 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
13−}
14−
1513
1614natToBin : Nat -> List Bool
1715natToBin O = Nil
18−natToBin k with parity k {
16+natToBin k with (parity k)
1917 natToBin (j + j) | even = False :: natToBin j
2018 natToBin (S (j + j)) | odd = True :: natToBin j
21−}
2219
2320main : IO ()
2421main = print (natToBin 42)
test/test007/test007.idr+11−20
@@ -1,40 +1,34 @@
11module main
22
3−instance Applicative Maybe where {
3+instance Applicative Maybe where
44 (Just f) <$> (Just a) = Just (f a)
55 Nothing <$> Nothing = Nothing
66
77 pure x = Just x
8−}
98
109data Expr = Var String
1110 | Val Int
1211 | Add Expr Expr
1312
14−
1513data Eval : Set -> Set where
1614 MkEval : (List (String, Int) -> Maybe a) -> Eval a
1715
1816fetch : String -> Eval Int
19−fetch x = MkEval (\e => fetchVal e) where {
17+fetch x = MkEval (\e => fetchVal e) where
2018 fetchVal : List (String, Int) -> Maybe Int
2119 fetchVal [] = Nothing
2220 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
23−}
2421
25−instance Functor Eval where {
22+instance Functor Eval where
2623 fmap f (MkEval g) = MkEval (\e => fmap f (g e))
27−}
2824
29−instance Applicative Eval where {
25+instance Applicative Eval where
3026 pure x = MkEval (\e => Just x)
3127
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
3329 appAux : Maybe (a -> b) -> Maybe a -> Maybe b
3430 appAux (Just fx) (Just gx) = Just (fx gx)
3531 appAux _ _ = Nothing
36− }
37−}
3832
3933eval : Expr -> Eval Int
4034eval (Var x) = fetch x
@@ -42,16 +36,13 @@ eval (Val x) = [| x |]
4236eval (Add x y) = [| eval x + eval y |]
4337
4438runEval : List (String, Int) -> Expr -> Maybe Int
45−runEval env e with eval e {
39+runEval env e with (eval e) {
4640 | MkEval envFn = envFn env
4741}
4842
4943main : IO ()
50−main = do { print [| (*2) (Just 4) |]
51− print [| plus (Just 4) (Just 5) |]
52− 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"))))
54− }
55−
56−
57−
44+main = do print [| (*2) (Just 4) |]
45+ print [| plus (Just 4) (Just 5) |]
46+ print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))
47+ print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))
48+
tutorial/examples/binary.idr+8−11
@@ -5,11 +5,10 @@ data Binary : Nat -> Set where
55 | bO : Binary n -> Binary (n + n)
66 | bI : Binary n -> Binary (S (n + n))
77
8−instance Show (Binary n) where {
8+instance Show (Binary n) where
99 show (bO x) = show x ++ "0"
1010 show (bI x) = show x ++ "1"
1111 show bEnd = ""
12−}
1312
1413data Parity : Nat -> Set where
1514 even : Parity (n + n)
@@ -18,28 +17,26 @@ data Parity : Nat -> Set where
1817parity : (n:Nat) -> Parity n
1918parity O = even {n=O}
2019parity (S O) = odd {n=O}
21−parity (S (S k)) with parity k {
20+parity (S (S k)) with (parity k)
2221 parity (S (S (j + j))) | even ?= even {n=S j}
2322 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
24−}
2523
2624natToBin : (n:Nat) -> Binary n
2725natToBin O = bEnd
28−natToBin (S k) with parity k {
26+natToBin (S k) with (parity k)
2927 natToBin (S (j + j)) | even = bI (natToBin j)
3028 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
31−}
3229
3330intToNat : Int -> Nat
3431intToNat 0 = O
3532intToNat x = if (x>0) then (S (intToNat (x-1))) else O
3633
3734main : IO ()
38−main = do { putStr "Enter a number: "
39− x <- getLine
40− let n = prim__strToInt x
41− let b = natToBin (fromInteger n)
42− print b }
35+main = do putStr "Enter a number: "
36+ x <- getLine
37+ let n = prim__strToInt x
38+ let b = natToBin (fromInteger n)
39+ print b
4340
4441---------- Proofs ----------
4542
tutorial/examples/bmain.idr+2−3
@@ -3,7 +3,6 @@ module main
33import btree
44
55main : IO ()
6−main = do { let t = toTree [1,8,2,7,9,3]
7− print (toList t)
8− }
6+main = do let t = toTree [1,8,2,7,9,3]
7+ print (toList t)
98
tutorial/examples/classes.idr+3−4
@@ -1,8 +1,7 @@
11m_add : Maybe Int -> Maybe Int -> Maybe Int
2−m_add x y = do { x' <- x -- Extract value from x
3− y' <- y -- Extract value from y
4− return (x' + y') -- Add them
5− }
2+m_add x y = do x' <- x -- Extract value from x
3+ y' <- y -- Extract value from y
4+ return (x' + y') -- Add them
65
76m_add' : Maybe Int -> Maybe Int -> Maybe Int
87m_add' x y = [ x' + y' | x' <- x, y' <- y ]
tutorial/examples/foo.idr+2−4
@@ -1,12 +1,10 @@
11module foo
22
3−namespace x {
3+namespace x
44 test : Int -> Int
55 test x = x * 2
6−}
76
8−namespace y {
7+namespace y
98 test : String -> String
109 test x = x ++ x
11−}
1210
tutorial/examples/interp.idr+4−8
@@ -7,7 +7,7 @@ interpTy TyInt = Int
77interpTy TyBool = Bool
88interpTy (TyFun s t) = interpTy s -> interpTy t
99
10−using (G : Vect Ty n) {
10+using (G : Vect Ty n)
1111
1212 data Env : Vect Ty n -> Set where
1313 Nil : Env Nil
@@ -54,15 +54,11 @@ using (G : Vect Ty n) {
5454 fact = Lam (If (Op (==) (Var stop) (Val 0))
5555 (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1))) (Var stop)))
5656
57−}
58−
5957testFac : Int
6058testFac = interp [] fact 4
6159
6260main : IO ()
63−main = do { putStr "Enter a number: "
64− x <- getLine
65− print (interp [] fact (prim__strToInt x))
66− }
67−
61+main = do putStr "Enter a number: "
62+ x <- getLine
63+ print (interp [] fact (prim__strToInt x))
6864
tutorial/examples/letbind.idr+1−2
@@ -11,7 +11,6 @@ showPerson p = let MkPerson name age = p in
1111 name ++ " is " ++ show age ++ " years old"
1212
1313splitAt : Char -> String -> (String, String)
14−splitAt c x = case break (== c) x of {
14+splitAt c x = case break (== c) x of
1515 (x, y) => (x, strTail y)
16− }
1716
tutorial/examples/usefultypes.idr+1−2
@@ -14,8 +14,7 @@ list_lookup O (x :: xs) = Just x
1414list_lookup (S k) (x :: xs) = list_lookup k xs
1515
1616lookup_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
1818 Nothing => def
1919 | Just x => x
20− }
2120
tutorial/examples/views.idr+2−5
@@ -7,18 +7,15 @@ data Parity : Nat -> Set where
77parity : (n:Nat) -> Parity n
88parity O = even {n=O}
99parity (S O) = odd {n=O}
10−parity (S (S k)) with parity k {
10+parity (S (S k)) with (parity k)
1111 parity (S (S (j + j))) | even ?= even {n=S j}
1212 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
13−}
14−
1513
1614natToBin : Nat -> List Bool
1715natToBin O = Nil
18−natToBin k with parity k {
16+natToBin k with (parity k)
1917 natToBin (j + j) | even = False :: natToBin j
2018 natToBin (S (j + j)) | odd = True :: natToBin j
21−}
2219
2320
2421---------- Proofs ----------