git.iko.soy/Idris-dev
on master help sign in
Removed need for terminating ;

A declaration is now considered terminated on encountering a token in the same column as the declaration began - or on encountering a semicolon. Libraries and some tests updated.

commitbd615948689709a3da8c9824fd5d301179d48d15 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 6 Jan 2012, 22:57 (15 years ago) parentc8b0f28
17 files changed+799−721
compare with master
unifiedsplit
lib/builtins.idr+123−123 lib/network/cgi.idr+87−91 lib/prelude.idr+145−142 lib/prelude/char.idr+18−18 lib/prelude/either.idr+6−6 lib/prelude/list.idr+62−62 lib/prelude/maybe.idr+8−8 lib/prelude/nat.idr+40−40 lib/prelude/strings.idr+31−31 lib/prelude/vect.idr+23−22 lib/system.idr+16−16 samples/interp.idr+44−45 src/Idris/AbsSyntax.hs+2−1 src/Idris/Parser.hs+137−59 src/Idris/Unlit.hs+2−2 test/test001/test001.idr+43−43 test/test003/lit.lidr+12−12
lib/builtins.idr+123−123
@@ -1,246 +1,246 @@
11%access public
22
33data Exists : (a : Set) -> (P : a -> Set) -> Set where
4− Ex_intro : {P : a -> Set} -> (x : a) -> P x -> Exists a P;
4+ Ex_intro : {P : a -> Set} -> (x : a) -> P x -> Exists a P
55
6−getWitness : {P : a -> Set} -> Exists a P -> a;
7−getWitness (a ** v) = a;
6+getWitness : {P : a -> Set} -> Exists a P -> a
7+getWitness (a ** v) = a
88
9−getProof : {P : a -> Set} -> (s : Exists a P) -> P (getWitness s);
10−getProof (a ** v) = v;
9+getProof : {P : a -> Set} -> (s : Exists a P) -> P (getWitness s)
10+getProof (a ** v) = v
1111
12−FalseElim : _|_ -> a;
12+FalseElim : _|_ -> a
1313
1414-- For rewrite tactic
15−replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Set} -> x = y -> P x -> P y;
16−replace refl prf = prf;
15+replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Set} -> x = y -> P x -> P y
16+replace refl prf = prf
1717
18−sym : {x:a} -> {y:a} -> x = y -> y = x;
19−sym refl = refl;
18+sym : {x:a} -> {y:a} -> x = y -> y = x
19+sym refl = refl
2020
21−lazy : a -> a;
22−lazy x = x; -- compiled specially
21+lazy : a -> a
22+lazy x = x -- compiled specially
2323
24−believe_me : a -> b; -- compiled specially as id, use with care!
25−believe_me x = prim__believe_me _ _ x;
24+believe_me : a -> b -- compiled specially as id, use with care!
25+believe_me x = prim__believe_me _ _ x
2626
2727namespace builtins {
2828
29−id : a -> a;
30−id x = x;
29+id : a -> a
30+id x = x
3131
32−const : a -> b -> a;
33−const x _ = x;
32+const : a -> b -> a
33+const x _ = x
3434
35−fst : (s, t) -> s;
36−fst (x, y) = x;
35+fst : (s, t) -> s
36+fst (x, y) = x
3737
38−snd : (a, b) -> b;
39−snd (x, y) = y;
38+snd : (a, b) -> b
39+snd (x, y) = y
4040
41−infixl 9 .;
41+infixl 9 .
4242
43−(.) : (b -> c) -> (a -> b) -> a -> c;
44−(.) f g x = f (g x);
43+(.) : (b -> c) -> (a -> b) -> a -> c
44+(.) f g x = f (g x)
4545
46−flip : (a -> b -> c) -> b -> a -> c;
47−flip f x y = f y x;
46+flip : (a -> b -> c) -> b -> a -> c
47+flip f x y = f y x
4848
49−infixr 1 $;
49+infixr 1 $
5050
51−($) : (a -> b) -> a -> b;
52−f $ a = f a;
51+($) : (a -> b) -> a -> b
52+f $ a = f a
5353
54−data Bool = False | True;
54+data Bool = False | True
5555
56−boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a;
57−boolElim True t e = t;
58−boolElim False t e = e;
56+boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a
57+boolElim True t e = t
58+boolElim False t e = e
5959
60−data so : Bool -> Set where oh : so True;
60+data so : Bool -> Set where oh : so True
6161
62−syntax if [test] then [t] else [e] = boolElim test t e;
63−syntax [test] "?" [t] ":" [e] = if test then t else e;
62+syntax if [test] then [t] else [e] = boolElim test t e
63+syntax [test] "?" [t] ":" [e] = if test then t else e
6464
65−infixl 4 &&, ||;
65+infixl 4 &&, ||
6666
67−(||) : Bool -> Bool -> Bool;
68−(||) False x = x;
69−(||) True _ = True;
67+(||) : Bool -> Bool -> Bool
68+(||) False x = x
69+(||) True _ = True
7070
71−(&&) : Bool -> Bool -> Bool;
72−(&&) True x = x;
73−(&&) False _ = False;
71+(&&) : Bool -> Bool -> Bool
72+(&&) True x = x
73+(&&) False _ = False
7474
75−not : Bool -> Bool;
76−not True = False;
77−not False = True;
75+not : Bool -> Bool
76+not True = False
77+not False = True
7878
79−infixl 5 ==, /=, ==.;
80−infixl 6 <, <=, >, >=, <., <=., >., >=.;
81−infixl 7 <<, >>;
82−infixl 8 +,-,++,+.,-.;
83−infixl 9 *,/,*.,/.;
79+infixl 5 ==, /=, ==.
80+infixl 6 <, <=, >, >=, <., <=., >., >=.
81+infixl 7 <<, >>
82+infixl 8 +,-,++,+.,-.
83+infixl 9 *,/,*.,/.
8484
8585--- Numeric operators
8686
87−intToBool : Int -> Bool;
88−intToBool 0 = False;
89−intToBool x = True;
87+intToBool : Int -> Bool
88+intToBool 0 = False
89+intToBool x = True
9090
91−boolOp : (a -> a -> Int) -> a -> a -> Bool;
92−boolOp op x y = intToBool (op x y);
91+boolOp : (a -> a -> Int) -> a -> a -> Bool
92+boolOp op x y = intToBool (op x y)
9393
9494class Eq a where {
95− (==) : a -> a -> Bool;
96− (/=) : a -> a -> Bool;
95+ (==) : a -> a -> Bool
96+ (/=) : a -> a -> Bool
9797
98− x /= y = not (x == y);
99− x == y = not (x /= y);
98+ x /= y = not (x == y)
99+ x == y = not (x /= y)
100100}
101101
102102instance Eq Int where {
103− (==) = boolOp prim__eqInt;
103+ (==) = boolOp prim__eqInt
104104}
105105
106106instance Eq Integer where {
107− (==) = boolOp prim__eqBigInt;
107+ (==) = boolOp prim__eqBigInt
108108}
109109
110110instance Eq Float where {
111− (==) = boolOp prim__eqFloat;
111+ (==) = boolOp prim__eqFloat
112112}
113113
114114instance Eq Char where {
115− (==) = boolOp prim__eqChar;
115+ (==) = boolOp prim__eqChar
116116}
117117
118118instance Eq String where {
119− (==) = boolOp prim__eqString;
119+ (==) = boolOp prim__eqString
120120}
121121
122−data Ordering = LT | EQ | GT;
122+data Ordering = LT | EQ | GT
123123
124124class Eq a => Ord a where {
125− compare : a -> a -> Ordering;
125+ compare : a -> a -> Ordering
126126
127− (<) : a -> a -> Bool;
128− (<) x y with compare x y {
129− (<) x y | LT = True;
130− (<) x y | _ = False;
127+ (<) : a -> a -> Bool
128+ (<) x y with (compare x y) {
129+ (<) x y | LT = True
130+ (<) x y | _ = False
131131 }
132132
133− (>) : a -> a -> Bool;
134− (>) x y with compare x y {
135− (>) x y | GT = True;
136− (>) x y | _ = False;
133+ (>) : a -> a -> Bool
134+ (>) x y with (compare x y) {
135+ (>) x y | GT = True
136+ (>) x y | _ = False
137137 }
138138
139− (<=) : a -> a -> Bool;
140− (<=) x y = x < y || x == y;
139+ (<=) : a -> a -> Bool
140+ (<=) x y = x < y || x == y
141141
142− (>=) : a -> a -> Bool;
143− (>=) x y = x > y || x == y;
142+ (>=) : a -> a -> Bool
143+ (>=) x y = x > y || x == y
144144
145− max : a -> a -> a;
146− max x y = if (x > y) then x else y;
145+ max : a -> a -> a
146+ max x y = if (x > y) then x else y
147147
148− min : a -> a -> a;
149− min x y = if (x < y) then x else y;
148+ min : a -> a -> a
149+ min x y = if (x < y) then x else y
150150}
151151
152152
153153instance Ord Int where {
154154 compare x y = if (x == y) then EQ else
155155 if (boolOp prim__ltInt x y) then LT else
156− GT;
156+ GT
157157}
158158
159159instance Ord Integer where {
160160 compare x y = if (x == y) then EQ else
161161 if (boolOp prim__ltBigInt x y) then LT else
162− GT;
162+ GT
163163}
164164
165165instance Ord Float where {
166166 compare x y = if (x == y) then EQ else
167167 if (boolOp prim__ltFloat x y) then LT else
168− GT;
168+ GT
169169}
170170
171171instance Ord Char where {
172172 compare x y = if (x == y) then EQ else
173173 if (boolOp prim__ltChar x y) then LT else
174− GT;
174+ GT
175175}
176176
177177instance Ord String where {
178178 compare x y = if (x == y) then EQ else
179179 if (boolOp prim__ltString x y) then LT else
180− GT;
180+ GT
181181}
182182
183183class (Eq a, Ord a) => Num a where {
184− (+) : a -> a -> a;
185− (-) : a -> a -> a;
186− (*) : a -> a -> a;
184+ (+) : a -> a -> a
185+ (-) : a -> a -> a
186+ (*) : a -> a -> a
187187
188− abs : a -> a;
189− abs x = if (x < 0) then (-x) else x;
188+ abs : a -> a
189+ abs x = if (x < 0) then (-x) else x
190190
191− fromInteger : Int -> a;
191+ fromInteger : Int -> a
192192}
193193
194194
195195instance Num Int where {
196− (+) = prim__addInt;
197− (-) = prim__subInt;
198− (*) = prim__mulInt;
196+ (+) = prim__addInt
197+ (-) = prim__subInt
198+ (*) = prim__mulInt
199199
200− fromInteger = id;
200+ fromInteger = id
201201}
202202
203203instance Num Integer where {
204− (+) = prim__addBigInt;
205− (-) = prim__subBigInt;
206− (*) = prim__mulBigInt;
204+ (+) = prim__addBigInt
205+ (-) = prim__subBigInt
206+ (*) = prim__mulBigInt
207207
208− fromInteger = prim__intToBigInt;
208+ fromInteger = prim__intToBigInt
209209}
210210
211211instance Num Float where {
212− (+) = prim__addFloat;
213− (-) = prim__subFloat;
214− (*) = prim__mulFloat;
212+ (+) = prim__addFloat
213+ (-) = prim__subFloat
214+ (*) = prim__mulFloat
215215
216− fromInteger = prim__intToFloat;
216+ fromInteger = prim__intToFloat
217217}
218218
219−div : Int -> Int -> Int;
220−div = prim__divInt;
219+div : Int -> Int -> Int
220+div = prim__divInt
221221
222222
223−(/) : Float -> Float -> Float;
224−(/) = prim__divFloat;
223+(/) : Float -> Float -> Float
224+(/) = prim__divFloat
225225
226226--- string operators
227227
228−(++) : String -> String -> String;
229−(++) = prim__concat;
228+(++) : String -> String -> String
229+(++) = prim__concat
230230
231−strHead : String -> Char;
232−strHead = prim__strHead;
231+strHead : String -> Char
232+strHead = prim__strHead
233233
234−strTail : String -> String;
235−strTail = prim__strTail;
234+strTail : String -> String
235+strTail = prim__strTail
236236
237−strCons : Char -> String -> String;
238−strCons = prim__strCons;
237+strCons : Char -> String -> String
238+strCons = prim__strCons
239239
240−strIndex : String -> Int -> Char;
241−strIndex = prim__strIndex;
240+strIndex : String -> Int -> Char
241+strIndex = prim__strIndex
242242
243−rev : String -> String;
244−rev = prim__strRev;
243+rev : String -> String
244+rev = prim__strRev
245245
246246}
lib/network/cgi.idr+87−91
@@ -1,153 +1,149 @@
1−module network.cgi;
1+module network.cgi
22
3−import system;
3+import system
44
55public
6−Vars : Set;
7−Vars = List (String, String);
6+Vars : Set
7+Vars = List (String, String)
88
99data CGIInfo = CGISt Vars -- GET
1010 Vars -- POST
1111 Vars -- Cookies
1212 String -- User agent
1313 String -- headers
14− String; -- output
14+ String -- output
1515
16−get_GET : CGIInfo -> Vars;
17−get_GET (CGISt g _ _ _ _ _) = g;
16+get_GET : CGIInfo -> Vars
17+get_GET (CGISt g _ _ _ _ _) = g
1818
19−get_POST : CGIInfo -> Vars;
20−get_POST (CGISt _ p _ _ _ _) = p;
19+get_POST : CGIInfo -> Vars
20+get_POST (CGISt _ p _ _ _ _) = p
2121
22−get_Cookies : CGIInfo -> Vars;
23−get_Cookies (CGISt _ _ c _ _ _) = c;
22+get_Cookies : CGIInfo -> Vars
23+get_Cookies (CGISt _ _ c _ _ _) = c
2424
25−get_UAgent : CGIInfo -> String;
26−get_UAgent (CGISt _ _ _ a _ _) = a;
25+get_UAgent : CGIInfo -> String
26+get_UAgent (CGISt _ _ _ a _ _) = a
2727
28−get_Headers : CGIInfo -> String;
29−get_Headers (CGISt _ _ _ _ h _) = h;
28+get_Headers : CGIInfo -> String
29+get_Headers (CGISt _ _ _ _ h _) = h
3030
31−get_Output : CGIInfo -> String;
32−get_Output (CGISt _ _ _ _ _ o) = o;
31+get_Output : CGIInfo -> String
32+get_Output (CGISt _ _ _ _ _ o) = o
3333
34−add_Headers : String -> CGIInfo -> CGIInfo;
35−add_Headers str (CGISt g p c a h o) = CGISt g p c a (h ++ str) o;
34+add_Headers : String -> CGIInfo -> CGIInfo
35+add_Headers str (CGISt g p c a h o) = CGISt g p c a (h ++ str) o
3636
37−add_Output : String -> CGIInfo -> CGIInfo;
38−add_Output str (CGISt g p c a h o) = CGISt g p c a h (o ++ str);
37+add_Output : String -> CGIInfo -> CGIInfo
38+add_Output str (CGISt g p c a h o) = CGISt g p c a h (o ++ str)
3939
4040abstract
4141data CGI : Set -> Set where
42− MkCGI : (CGIInfo -> IO (a, CGIInfo)) -> CGI a;
42+ MkCGI : (CGIInfo -> IO (a, CGIInfo)) -> CGI a
4343
44−getAction : CGI a -> CGIInfo -> IO (a, CGIInfo);
45−getAction (MkCGI act) = act;
44+getAction : CGI a -> CGIInfo -> IO (a, CGIInfo)
45+getAction (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) })
5050
51− return v = MkCGI (\s => return (v, s));
51+ return v = MkCGI (\s => return (v, s))
5252}
5353
54−setInfo : CGIInfo -> CGI ();
55−setInfo i = MkCGI (\s => return ((), i));
54+setInfo : CGIInfo -> CGI ()
55+setInfo i = MkCGI (\s => return ((), i))
5656
57−getInfo : CGI CGIInfo;
58−getInfo = MkCGI (\s => return (s, s));
57+getInfo : CGI CGIInfo
58+getInfo = MkCGI (\s => return (s, s))
5959
6060abstract
61−lift : IO a -> CGI a ;
62−lift op = MkCGI (\st => do { x <- op;
63− return (x, st); } );
61+lift : IO a -> CGI a
62+lift op = MkCGI (\st => do { x <- op
63+ return (x, st) } )
6464
6565abstract
66−output : String -> CGI ();
67−output s = do { i <- getInfo;
68− setInfo (add_Output s i); };
66+output : String -> CGI ()
67+output s = do { i <- getInfo
68+ setInfo (add_Output s i) }
6969
7070abstract
71−queryVars : CGI Vars;
72−queryVars = do { i <- getInfo;
73− return (get_GET i); };
71+queryVars : CGI Vars
72+queryVars = do { i <- getInfo
73+ return (get_GET i) }
7474
7575abstract
76−postVars : CGI Vars;
77−postVars = do { i <- getInfo;
78− return (get_POST i); };
76+postVars : CGI Vars
77+postVars = do { i <- getInfo
78+ return (get_POST i) }
7979
8080abstract
81−cookieVars : CGI Vars;
82−cookieVars = do { i <- getInfo;
83− return (get_Cookies i); };
81+cookieVars : CGI Vars
82+cookieVars = do { i <- getInfo
83+ return (get_Cookies i) }
8484
8585abstract
86−queryVar : String -> CGI (Maybe String);
87−queryVar x = do { vs <- queryVars;
88− return (lookup x vs); };
86+queryVar : String -> CGI (Maybe String)
87+queryVar x = do { vs <- queryVars
88+ return (lookup x vs) }
8989
90−getOutput : CGI String;
91−getOutput = do { i <- getInfo;
92− return (get_Output i); };
90+getOutput : CGI String
91+getOutput = do { i <- getInfo
92+ return (get_Output i) }
9393
94−getHeaders : CGI String;
95−getHeaders = do { i <- getInfo;
96− return (get_Headers i); };
94+getHeaders : CGI String
95+getHeaders = do { i <- getInfo
96+ return (get_Headers i) }
9797
9898abstract
99−flushHeaders : CGI ();
100−flushHeaders = do { o <- getHeaders;
101− lift (putStrLn o);
102− };
99+flushHeaders : CGI ()
100+flushHeaders = do { o <- getHeaders
101+ lift (putStrLn o)
102+ }
103103
104104abstract
105−flush : CGI ();
106−flush = do { o <- getOutput;
107− lift (putStr o);
108− };
105+flush : CGI ()
106+flush = do { o <- getOutput
107+ lift (putStr o)
108+ }
109109
110−getVars : List Char -> String -> List (String, String);
110+getVars : List Char -> String -> List (String, String)
111111getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)
112112 where {
113− readVar : String -> Maybe (String, String);
113+ readVar : String -> Maybe (String, String)
114114 readVar xs with split (\x => x == '=') xs {
115− | [k, v] = Just (trim k, trim v);
116− | _ = Nothing;
115+ | [k, v] = Just (trim k, trim v)
116+ | _ = Nothing
117117 }
118118 }
119119
120−getContent : Int -> IO String;
120+getContent : Int -> IO String
121121getContent x = getC x "" where {
122− getC : Int -> String -> IO String;
123− getC 0 acc = return $ rev acc;
124− getC n acc = do { x <- getChar;
125− getC (n-1) (strCons x acc); };
122+ getC : Int -> String -> IO String
123+ getC 0 acc = return $ rev acc
124+ getC n acc = do { x <- getChar
125+ getC (n-1) (strCons x acc) }
126126}
127127
128128abstract
129−runCGI : CGI a -> IO a;
129+runCGI : CGI a -> IO a
130130runCGI prog = do {
131− clen_in <- getEnv "CONTENT_LENGTH";
132− let clen = prim__strToInt clen_in;
133− content <- getContent clen;
134− query <- getEnv "QUERY_STRING";
135− cookie <- getEnv "HTTP_COOKIE";
136− agent <- getEnv "HTTP_USER_AGENT";
131+ clen_in <- getEnv "CONTENT_LENGTH"
132+ let clen = prim__strToInt clen_in
133+ content <- getContent clen
134+ query <- getEnv "QUERY_STRING"
135+ cookie <- getEnv "HTTP_COOKIE"
136+ agent <- getEnv "HTTP_USER_AGENT"
137137
138− let get_vars = getVars ['&',';'] query;
139− let post_vars = getVars ['&'] content;
140− let cookies = getVars [';'] cookie;
138+ let get_vars = getVars ['&',';'] query
139+ let post_vars = getVars ['&'] content
140+ let cookies = getVars [';'] cookie
141141
142142 p <- getAction prog (CGISt get_vars post_vars cookies agent
143143 "Content-type: text/html\n"
144− "");
145− putStrLn (get_Headers (snd p));
146− putStr (get_Output (snd p));
147− return (fst p);
148−};
149−
150−
151−
152−
144+ "")
145+ putStrLn (get_Headers (snd p))
146+ putStr (get_Output (snd p))
147+ return (fst p)
148+}
153149
lib/prelude.idr+145−142
@@ -1,153 +1,153 @@
1−module prelude;
1+module prelude
22
3−import builtins;
4−import io;
3+import builtins
4+import io
55
6−import prelude.nat;
7−import prelude.list;
8−import prelude.maybe;
9−import prelude.either;
10−import prelude.vect;
11−import prelude.strings;
12−import prelude.char;
6+import prelude.nat
7+import prelude.list
8+import prelude.maybe
9+import prelude.either
10+import prelude.vect
11+import prelude.strings
12+import prelude.char
1313
1414-- Show and instances
1515
1616class Show a where {
17− show : a -> String;
17+ show : a -> String
1818}
1919
2020instance Show Nat where {
21− show O = "O";
22− show (S k) = "s" ++ show k;
21+ show O = "O"
22+ show (S k) = "s" ++ show k
2323}
2424
2525instance Show Int where {
26− show = prim__intToStr;
26+ show = prim__intToStr
2727}
2828
2929instance Show Integer where {
30− show = prim__bigIntToStr;
30+ show = prim__bigIntToStr
3131}
3232
3333instance Show Float where {
34− show = prim__floatToStr;
34+ show = prim__floatToStr
3535}
3636
3737instance Show Char where {
38− show x = strCons x "";
38+ show x = strCons x ""
3939}
4040
4141instance Show String where {
42− show = id;
42+ show = id
4343}
4444
4545instance Show Bool where {
46− show True = "True";
47− show False = "False";
46+ show True = "True"
47+ show False = "False"
4848}
4949
5050instance (Show a, Show b) => Show (a, b) where {
51− show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")";
51+ show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
5252}
5353
5454instance Show a => Show (List a) where {
5555 show xs = "[" ++ show' xs ++ "]" where {
56− show' : Show a => List a -> String;
57− show' [] = "";
58− show' [x] = show x;
59− show' (x :: xs) = show x ++ ", " ++ show' xs;
56+ show' : Show a => List a -> String
57+ show' [] = ""
58+ show' [x] = show x
59+ show' (x :: xs) = show x ++ ", " ++ show' xs
6060 }
6161}
6262
6363instance Show a => Show (Vect a n) where {
6464 show xs = "[" ++ show' xs ++ "]" where {
65− show' : Show a => Vect a n -> String;
66− show' [] = "";
67− show' [x] = show x;
68− show' (x :: xs) = show x ++ ", " ++ show' xs;
65+ show' : Show a => Vect a n -> String
66+ show' [] = ""
67+ show' [x] = show x
68+ show' (x :: xs) = show x ++ ", " ++ show' xs
6969 }
7070}
7171
7272instance Show a => Show (Maybe a) where {
73− show Nothing = "Nothing";
74− show (Just x) = "Just " ++ show x;
73+ show Nothing = "Nothing"
74+ show (Just x) = "Just " ++ show x
7575}
7676
7777---- Monad and instances
7878
79−infixl 5 >>= ;
79+infixl 5 >>=
8080
8181class Monad (m : Set -> Set) where {
82− return : a -> m a;
83− (>>=) : m a -> (a -> m b) -> m b;
82+ return : a -> m a
83+ (>>=) : m a -> (a -> m b) -> m b
8484}
8585
8686class Monad m => MonadPlus (m : Set -> Set) where {
87− mplus : m a -> m a -> m a;
88− mzero : m a;
87+ mplus : m a -> m a -> m a
88+ mzero : m a
8989}
9090
9191class Monad m => MonadFail (m : Set -> Set) where {
92− fail : String -> m ();
92+ fail : String -> m ()
9393}
9494
9595instance Monad IO where {
96− return t = io_return t;
97− b >>= k = io_bind b k;
96+ return t = io_return t
97+ b >>= k = io_bind b k
9898}
9999
100100instance Monad Maybe where {
101− return = Just;
101+ return = Just
102102
103− Nothing >>= k = Nothing;
104− (Just x) >>= k = k x;
103+ Nothing >>= k = Nothing
104+ (Just x) >>= k = k x
105105}
106106
107107instance MonadPlus Maybe where {
108− mzero = Nothing;
108+ mzero = Nothing
109109
110− mplus (Just x) _ = Just x;
111− mplus Nothing (Just y) = Just y;
112− mplus Nothing Nothing = Nothing;
110+ mplus (Just x) _ = Just x
111+ mplus Nothing (Just y) = Just y
112+ mplus Nothing Nothing = Nothing
113113}
114114
115115instance Monad List where {
116− return x = [x];
117− m >>= f = concatMap f m;
116+ return x = [x]
117+ m >>= f = concatMap f m
118118}
119119
120120instance MonadPlus List where {
121− mzero = [];
122− mplus = app;
121+ mzero = []
122+ mplus = app
123123}
124124
125−guard : MonadPlus m => Bool -> m ();
126−guard True = return ();
127−guard False = mzero;
125+guard : MonadPlus m => Bool -> m ()
126+guard True = return ()
127+guard False = mzero
128128
129129---- Functors
130130
131131class Functor (f : Set -> Set) where {
132− fmap : (a -> b) -> f a -> f b;
132+ fmap : (a -> b) -> f a -> f b
133133}
134134
135135instance Functor Maybe where {
136− fmap f (Just x) = Just (f x);
137− fmap f Nothing = Nothing;
136+ fmap f (Just x) = Just (f x)
137+ fmap f Nothing = Nothing
138138}
139139
140140instance Functor List where {
141− fmap = map;
141+ fmap = map
142142}
143143
144144---- Applicative functors/Idioms
145145
146−infixl 2 <$>;
146+infixl 2 <$>
147147
148148class Functor f => Applicative (f : Set -> Set) where {
149− pure : a -> f a;
150− (<$>) : f (a -> b) -> f a -> f b;
149+ pure : a -> f a
150+ (<$>) : f (a -> b) -> f a -> f b
151151}
152152
153153---- some mathematical operations
@@ -155,137 +155,140 @@ class Functor f => Applicative (f : Set -> Set) where {
155155%include "math.h"
156156%lib "m"
157157
158−exp : Float -> Float;
159−exp x = prim__floatExp x;
158+exp : Float -> Float
159+exp x = prim__floatExp x
160160
161−log : Float -> Float;
162−log x = prim__floatLog x;
161+log : Float -> Float
162+log x = prim__floatLog x
163163
164−pi : Float;
165−pi = 3.141592653589793;
164+pi : Float
165+pi = 3.141592653589793
166166
167−sin : Float -> Float;
168−sin x = prim__floatSin x;
167+sin : Float -> Float
168+sin x = prim__floatSin x
169169
170−cos : Float -> Float;
171−cos x = prim__floatCos x;
170+cos : Float -> Float
171+cos x = prim__floatCos x
172172
173−tan : Float -> Float;
174−tan x = prim__floatTan x;
173+tan : Float -> Float
174+tan x = prim__floatTan x
175175
176−asin : Float -> Float;
177−asin x = prim__floatASin x;
176+asin : Float -> Float
177+asin x = prim__floatASin x
178178
179−acos : Float -> Float;
180−acos x = prim__floatACos x;
179+acos : Float -> Float
180+acos x = prim__floatACos x
181181
182−atan : Float -> Float;
183−atan x = prim__floatATan x;
182+atan : Float -> Float
183+atan x = prim__floatATan x
184184
185−sqrt : Float -> Float;
186−sqrt x = prim__floatSqrt x;
185+sqrt : Float -> Float
186+sqrt x = prim__floatSqrt x
187187
188−floor : Float -> Float;
189−floor x = prim__floatFloor x;
188+floor : Float -> Float
189+floor x = prim__floatFloor x
190190
191−ceiling : Float -> Float;
192−ceiling x = prim__floatCeil x;
191+ceiling : Float -> Float
192+ceiling x = prim__floatCeil x
193193
194194
195195-- Ranges
196196
197−count : Num a => a -> a -> a -> List a;
197+count : Num a => a -> a -> a -> List a
198198count a inc b = if (a <= b) then (a :: count (a + inc) inc b)
199− else [];
199+ else []
200200
201201syntax "[" [start] ".." [end] "]"
202− = count start 1 end;
202+ = count start 1 end
203203syntax "[" [start] "," [next] ".." [end] "]"
204− = count start (next - start) end;
204+ = count start (next - start) end
205205
206206---- some basic io
207207
208−putStr : String -> IO ();
209−putStr x = mkForeign (FFun "putStr" [FString] FUnit) x;
208+putStr : String -> IO ()
209+putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
210210
211−putStrLn : String -> IO ();
212−putStrLn x = putStr (x ++ "\n");
211+putStrLn : String -> IO ()
212+putStrLn x = putStr (x ++ "\n")
213213
214−print : Show a => a -> IO ();
215−print x = putStrLn (show x);
214+print : Show a => a -> IO ()
215+print x = putStrLn (show x)
216216
217−getLine : IO String;
218−getLine = mkForeign (FFun "readStr" Nil FString);
217+getLine : IO String
218+getLine = mkForeign (FFun "readStr" Nil FString)
219219
220−putChar : Char -> IO ();
221−putChar c = mkForeign (FFun "putchar" [FChar] FUnit) c;
220+putChar : Char -> IO ()
221+putChar c = mkForeign (FFun "putchar" [FChar] FUnit) c
222222
223−getChar : IO Char;
224−getChar = mkForeign (FFun "getchar" [] FChar);
223+getChar : IO Char
224+getChar = mkForeign (FFun "getchar" [] FChar)
225225
226226---- some basic file handling
227227
228−abstract data File = FHandle Ptr;
228+abstract
229+data File = FHandle Ptr
229230
230−do_fopen : String -> String -> IO Ptr;
231−do_fopen f m = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m;
231+do_fopen : String -> String -> IO Ptr
232+do_fopen f m = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
232233
233−fopen : String -> String -> IO File;
234−fopen f m = do { h <- do_fopen f m;
235− return (FHandle h); };
234+fopen : String -> String -> IO File
235+fopen f m = do { h <- do_fopen f m
236+ return (FHandle h) }
236237
237−data Mode = Read | Write | ReadWrite;
238+data Mode = Read | Write | ReadWrite
238239
239−openFile : String -> Mode -> IO File;
240+openFile : String -> Mode -> IO File
240241openFile f m = fopen f (modeStr m) where {
241− modeStr : Mode -> String;
242− modeStr Read = "r";
243− modeStr Write = "w";
244− modeStr ReadWrite = "r+";
242+ modeStr : Mode -> String
243+ modeStr Read = "r"
244+ modeStr Write = "w"
245+ modeStr ReadWrite = "r+"
245246}
246247
247−do_fclose : Ptr -> IO ();
248−do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h;
248+do_fclose : Ptr -> IO ()
249+do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h
249250
250−closeFile : File -> IO ();
251−closeFile (FHandle h) = do_fclose h;
251+closeFile : File -> IO ()
252+closeFile (FHandle h) = do_fclose h
252253
253−do_fread : Ptr -> IO String;
254−do_fread h = mkForeign (FFun "freadStr" [FPtr] FString) h;
254+do_fread : Ptr -> IO String
255+do_fread h = mkForeign (FFun "freadStr" [FPtr] FString) h
255256
256−fread : File -> IO String;
257−fread (FHandle h) = do_fread h;
257+fread : File -> IO String
258+fread (FHandle h) = do_fread h
258259
259−do_fwrite : Ptr -> String -> IO ();
260−do_fwrite h s = mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s;
260+do_fwrite : Ptr -> String -> IO ()
261+do_fwrite h s = mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s
261262
262−fwrite : File -> String -> IO ();
263−fwrite (FHandle h) s = do_fwrite h s;
263+fwrite : File -> String -> IO ()
264+fwrite (FHandle h) s = do_fwrite h s
264265
265−do_feof : Ptr -> IO Int;
266−do_feof h = mkForeign (FFun "feof" [FPtr] FInt) h;
266+do_feof : Ptr -> IO Int
267+do_feof h = mkForeign (FFun "feof" [FPtr] FInt) h
267268
268−feof : File -> IO Bool;
269−feof (FHandle h) = do { eof <- do_feof h;
270− return (not (eof == 0)); };
269+feof : File -> IO Bool
270+feof (FHandle h) = do { eof <- do_feof h
271+ return (not (eof == 0)) }
271272
272−while : |(test : IO Bool) -> |(body : IO ()) -> IO ();
273−while t b = do { v <- t;
274− if v then (do { b; while t b; }) else return (); };
273+while : |(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+ }
275277
276−readFile : String -> IO String;
277−readFile fn = do { h <- openFile fn Read;
278− c <- readFile' h "";
279− closeFile h;
280− return c;
278+readFile : String -> IO String
279+readFile fn = do { h <- openFile fn Read
280+ c <- readFile' h ""
281+ closeFile h
282+ return c
281283 }
282284 where {
283− readFile' : File -> String -> IO String;
285+ readFile' : File -> String -> IO String
284286 readFile' h contents =
285− do { x <- feof h;
286− if (not x) then (do { l <- fread h;
287− readFile' h (contents ++ l);
287+ do { x <- feof h
288+ if (not x) then (do { l <- fread h
289+ readFile' h (contents ++ l)
288290 })
289− else (return contents); };
291+ else (return contents)
292+ }
290293 }
291294
lib/prelude/char.idr+18−18
@@ -1,34 +1,34 @@
1−module prelude.char;
1+module prelude.char
22
3−import builtins;
3+import builtins
44
5−isUpper : Char -> Bool;
6−isUpper x = x >= 'A' && x <= 'Z';
5+isUpper : Char -> Bool
6+isUpper x = x >= 'A' && x <= 'Z'
77
8−isLower : Char -> Bool;
9−isLower x = x >= 'a' && x <= 'z';
8+isLower : Char -> Bool
9+isLower x = x >= 'a' && x <= 'z'
1010
11−isAlpha : Char -> Bool;
12−isAlpha x = isUpper x || isLower x;
11+isAlpha : Char -> Bool
12+isAlpha x = isUpper x || isLower x
1313
14−isDigit : Char -> Bool;
15−isDigit x = (x >= '0' && x <= '9');
14+isDigit : Char -> Bool
15+isDigit x = (x >= '0' && x <= '9')
1616
17−isAlphaNum : Char -> Bool;
18−isAlphaNum x = isDigit x || isAlpha x;
17+isAlphaNum : Char -> Bool
18+isAlphaNum x = isDigit x || isAlpha x
1919
20−isSpace : Char -> Bool;
20+isSpace : Char -> Bool
2121isSpace x = x == ' ' || x == '\t' || x == '\r' ||
2222 x == '\n' || x == '\f' || x == '\v' ||
23− x == '\xa0';
23+ x == '\xa0'
2424
25−toUpper : Char -> Char;
25+toUpper : Char -> Char
2626toUpper x = if (isLower x)
2727 then (prim__intToChar (prim__charToInt x - 32))
28− else x;
28+ else x
2929
30−toLower : Char -> Char;
30+toLower : Char -> Char
3131toLower x = if (isUpper x)
3232 then (prim__intToChar (prim__charToInt x + 32))
33− else x;
33+ else x
3434
lib/prelude/either.idr+6−6
@@ -1,10 +1,10 @@
1−module prelude.either;
1+module prelude.either
22
3−import builtins;
3+import builtins
44
5−data Either a b = Left a | Right b;
5+data Either a b = Left a | Right b
66
7−choose : (b : Bool) -> Either (so b) (so (not b));
8−choose True = Left oh;
9−choose False = Right oh;
7+choose : (b : Bool) -> Either (so b) (so (not b))
8+choose True = Left oh
9+choose False = Right oh
1010
lib/prelude/list.idr+62−62
@@ -1,102 +1,102 @@
1−module prelude.list;
1+module prelude.list
22
3−import prelude.maybe;
4−import builtins;
3+import prelude.maybe
4+import builtins
55
66%access public
77
8−infixr 7 :: ;
8+infixr 7 ::
99
10−data List a = Nil | (::) a (List a);
10+data List a = Nil | (::) a (List a)
1111
12−rev : List a -> List a;
12+rev : List a -> List a
1313rev xs = revAcc [] xs where {
14− revAcc : List a -> List a -> List a;
15− revAcc acc [] = acc;
16− revAcc acc (x :: xs) = revAcc (x :: acc) xs;
14+ revAcc : List a -> List a -> List a
15+ revAcc acc [] = acc
16+ revAcc acc (x :: xs) = revAcc (x :: acc) xs
1717}
1818
19−app : List a -> List a -> List a;
20−app [] xs = xs;
21−app (x :: xs) ys = x :: app xs ys;
19+app : List a -> List a -> List a
20+app [] xs = xs
21+app (x :: xs) ys = x :: app xs ys
2222
23−length : List a -> Int;
24−length [] = 0;
25−length (x :: xs) = 1 + length xs;
23+length : List a -> Int
24+length [] = 0
25+length (x :: xs) = 1 + length xs
2626
27−take : Int -> List a -> List a;
28−take 0 xs = [];
29−take n [] = [];
30−take n (x :: xs) = x :: take (n-1) xs;
27+take : Int -> List a -> List a
28+take 0 xs = []
29+take n [] = []
30+take n (x :: xs) = x :: take (n-1) xs
3131
32−drop : Int -> List a -> List a;
33−drop 0 xs = xs;
34−drop n [] = [];
35−drop n (x :: xs) = drop (n-1) xs;
32+drop : Int -> List a -> List a
33+drop 0 xs = xs
34+drop n [] = []
35+drop n (x :: xs) = drop (n-1) xs
3636
37−map : (a -> b) -> List a -> List b;
38−map f [] = [];
39−map f (x :: xs) = f x :: map f xs;
37+map : (a -> b) -> List a -> List b
38+map f [] = []
39+map f (x :: xs) = f x :: map f xs
4040
41−concatMap : (a -> List b) -> List a -> List b;
42−concatMap f [] = [];
43−concatMap f (x :: xs) = app (f x) (concatMap f xs);
41+concatMap : (a -> List b) -> List a -> List b
42+concatMap f [] = []
43+concatMap f (x :: xs) = app (f x) (concatMap f xs)
4444
45−mapMaybe : (a -> Maybe b) -> List a -> List b;
46−mapMaybe f [] = [];
45+mapMaybe : (a -> Maybe b) -> List a -> List b
46+mapMaybe f [] = []
4747mapMaybe f (x :: xs) = case f x of {
4848 Nothing => mapMaybe f xs
4949 | Just v => v :: mapMaybe f xs
50− };
50+ }
5151
52−filter : (y -> Bool) -> List y -> List y;
53−filter pred [] = [];
52+filter : (y -> Bool) -> List y -> List y
53+filter pred [] = []
5454filter pred (x :: xs) = if (pred x) then (x :: filter pred xs)
55− else (filter pred xs);
55+ else (filter pred xs)
5656
57−elem : Eq a => a -> List a -> Bool;
58−elem x [] = False;
59−elem x (y :: ys) = if (x == y) then True else (elem x ys);
57+elem : Eq a => a -> List a -> Bool
58+elem x [] = False
59+elem x (y :: ys) = if (x == y) then True else (elem x ys)
6060
61−lookup : Eq k => k -> List (k, v) -> Maybe v;
62−lookup k [] = Nothing;
63−lookup k ((x, v) :: xs) = if (x == k) then (Just v) else (lookup k xs);
61+lookup : Eq k => k -> List (k, v) -> Maybe v
62+lookup k [] = Nothing
63+lookup k ((x, v) :: xs) = if (x == k) then (Just v) else (lookup k xs)
6464
65−sort : Ord a => List a -> List a;
66−sort [] = [];
67−sort [x] = [x];
65+sort : Ord a => List a -> List a
66+sort [] = []
67+sort [x] = [x]
6868sort xs = let (x, y) = split xs in
6969 merge (sort x) (sort y) where {
70− splitrec : List a -> List a -> (List a -> List a) -> (List a, List a);
71− splitrec (_ :: _ :: xs) (y :: ys) zs = splitrec xs ys (zs . ((::) y));
72− splitrec _ ys zs = (zs [], ys);
70+ splitrec : List a -> List a -> (List a -> List a) -> (List a, List a)
71+ splitrec (_ :: _ :: xs) (y :: ys) zs = splitrec xs ys (zs . ((::) y))
72+ splitrec _ ys zs = (zs [], ys)
7373
74− split : List a -> (List a, List a);
75− split xs = splitrec xs xs id;
74+ split : List a -> (List a, List a)
75+ split xs = splitrec xs xs id
7676
77− merge : Ord a => List a -> List a -> List a;
78− merge xs [] = xs;
79− merge [] ys = ys;
77+ merge : Ord a => List a -> List a -> List a
78+ merge xs [] = xs
79+ merge [] ys = ys
8080 merge (x :: xs) (y :: ys) = if (x < y) then (x :: merge xs (y :: ys))
81− else (y :: merge (x :: xs) ys);
81+ else (y :: merge (x :: xs) ys)
8282}
8383
84−span : (a -> Bool) -> List a -> (List a, List a);
85−span p [] = ([], []);
84+span : (a -> Bool) -> List a -> (List a, List a)
85+span p [] = ([], [])
8686span p (x :: xs) with p x {
8787 | True with span p xs {
88− | (ys, zs) = (x :: ys, zs);
88+ | (ys, zs) = (x :: ys, zs)
8989 }
90− | False = ([], x :: xs);
90+ | False = ([], x :: xs)
9191}
9292
93−break : (a -> Bool) -> List a -> (List a, List a);
94−break p = span (not . p);
93+break : (a -> Bool) -> List a -> (List a, List a)
94+break p = span (not . p)
9595
96−split : (a -> Bool) -> List a -> List (List a);
97−split p [] = [];
96+split : (a -> Bool) -> List a -> List (List a)
97+split p [] = []
9898split p xs = case break p xs of {
9999 (chunk, []) => [chunk]
100100 | (chunk, (c :: rest)) => chunk :: split p rest
101− };
101+ }
102102
lib/prelude/maybe.idr+8−8
@@ -1,12 +1,12 @@
1−module prelude.maybe;
1+module prelude.maybe
22
3−data Maybe a = Nothing | Just a;
3+data Maybe a = Nothing | Just a
44
5−maybe : |(def : b) -> (a -> b) -> Maybe a -> b;
6−maybe n j Nothing = n;
7−maybe n j (Just x) = j x;
5+maybe : |(def : b) -> (a -> b) -> Maybe a -> b
6+maybe n j Nothing = n
7+maybe n j (Just x) = j x
88
9−maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b;
10−maybe_bind Nothing k = Nothing;
11−maybe_bind (Just x) k = k x;
9+maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b
10+maybe_bind Nothing k = Nothing
11+maybe_bind (Just x) k = k x
1212
lib/prelude/nat.idr+40−40
@@ -1,69 +1,69 @@
1−module prelude.nat;
1+module prelude.nat
22
3−import builtins;
3+import builtins
44
55%access public
66
7−data Nat = O | S Nat;
7+data Nat = O | S Nat
88
9−plus : Nat -> Nat -> Nat;
10−plus O y = y;
11−plus (S k) y = S (plus k y);
9+plus : Nat -> Nat -> Nat
10+plus O y = y
11+plus (S k) y = S (plus k y)
1212
13−eqRespS : m = n -> S m = S n;
14−eqRespS refl = refl;
13+eqRespS : m = n -> S m = S n
14+eqRespS refl = refl
1515
16−eqRespS' : S m = S n -> m = n;
17−eqRespS' refl = refl;
16+eqRespS' : S m = S n -> m = n
17+eqRespS' refl = refl
1818
19−sub : Nat -> Nat -> Nat;
20−sub O y = O;
21−sub (S k) (S y) = sub k y;
22−sub x O = x;
19+sub : Nat -> Nat -> Nat
20+sub O y = O
21+sub (S k) (S y) = sub k y
22+sub x O = x
2323
24−mult : Nat -> Nat -> Nat;
25−mult O y = O;
26−mult (S k) y = plus y (mult k y);
24+mult : Nat -> Nat -> Nat
25+mult O y = O
26+mult (S k) y = plus y (mult k y)
2727
2828instance Eq Nat where {
29− O == O = True;
30− (S x) == (S y) = x == y;
31− O == (S y) = False;
32− (S x) == O = False;
29+ O == O = True
30+ (S x) == (S y) = x == y
31+ O == (S y) = False
32+ (S x) == O = False
3333}
3434
3535instance Ord Nat where {
36− compare O O = EQ;
37− compare O (S k) = LT;
38− compare (S k) O = GT;
39− compare (S x) (S y) = compare x y;
36+ compare O O = EQ
37+ compare O (S k) = LT
38+ compare (S k) O = GT
39+ compare (S x) (S y) = compare x y
4040}
4141
4242instance Num Nat where {
43− (+) = plus;
44− (-) = sub;
45− (*) = mult;
43+ (+) = plus
44+ (-) = sub
45+ (*) = mult
4646
47− fromInteger 0 = O;
48− fromInteger n = if (n > 0) then (S (fromInteger (n-1))) else O;
47+ fromInteger 0 = O
48+ fromInteger n = if (n > 0) then (S (fromInteger (n-1))) else O
4949}
5050
51−plusnO : (m : Nat) -> m + O = m;
52−plusnO O = refl;
53−plusnO (S k) = eqRespS (plusnO k);
51+plusnO : (m : Nat) -> m + O = m
52+plusnO O = refl
53+plusnO (S k) = eqRespS (plusnO k)
5454
55−plusn_Sm : (n : Nat) -> (m : Nat) -> (plus n (S m)) = S (plus n m);
56−plusn_Sm O m = refl;
57−plusn_Sm (S j) m = eqRespS (plusn_Sm _ _);
55+plusn_Sm : (n : Nat) -> (m : Nat) -> (plus n (S m)) = S (plus n m)
56+plusn_Sm O m = refl
57+plusn_Sm (S j) m = eqRespS (plusn_Sm _ _)
5858
59−plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n;
60−plus_commutes O m = sym (plusnO m);
61−plus_commutes (S k) m = let ih = plus_commutes k m in ?plus_commutes_Sk;
59+plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
60+plus_commutes O m = sym (plusnO m)
61+plus_commutes (S k) m = let ih = plus_commutes k m in ?plus_commutes_Sk
6262
6363plus_commutes_Sk = proof {
6464 intro k,m,ih;
6565 refine sym;
6666 rewrite (sym ih);
6767 refine plusn_Sm;
68−};
68+}
6969
lib/prelude/strings.idr+31−31
@@ -1,62 +1,62 @@
1−module prelude.strings;
1+module prelude.strings
22
3−import builtins;
4−import prelude.list;
5−import prelude.char;
3+import builtins
4+import prelude.list
5+import prelude.char
66
77-- Some more complex string operations
88
99data StrM : String -> Set where
1010 StrNil : StrM ""
11− | StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs);
11+ | StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
1212
13−strHead' : (x : String) -> so (not (x == "")) -> Char;
14−strHead' x p = prim__strHead x;
13+strHead' : (x : String) -> so (not (x == "")) -> Char
14+strHead' x p = prim__strHead x
1515
16−strTail' : (x : String) -> so (not (x == "")) -> String;
17−strTail' x p = prim__strTail x;
16+strTail' : (x : String) -> so (not (x == "")) -> String
17+strTail' x p = prim__strTail x
1818
1919-- we need the 'believe_me' because the operations are primitives
2020
21−strM : (x : String) -> StrM x;
21+strM : (x : String) -> StrM x
2222strM x with choose (not (x == "")) {
23− strM x | (Left p) = believe_me (StrCons (strHead' x p) (strTail' x p));
24− strM x | (Right p) = believe_me StrNil;
23+ strM x | (Left p) = believe_me (StrCons (strHead' x p) (strTail' x p))
24+ strM x | (Right p) = believe_me StrNil
2525}
2626
27−unpack : String -> List Char;
27+unpack : String -> List Char
2828unpack s with strM s {
29− unpack "" | StrNil = [];
30− unpack (strCons x xs) | (StrCons _ _) = x :: unpack xs;
29+ unpack "" | StrNil = []
30+ unpack (strCons x xs) | (StrCons _ _) = x :: unpack xs
3131}
3232
33−pack : List Char -> String;
34−pack [] = "";
35−pack (x :: xs) = strCons x (pack xs);
33+pack : List Char -> String
34+pack [] = ""
35+pack (x :: xs) = strCons x (pack xs)
3636
37−span : (Char -> Bool) -> String -> (String, String);
37+span : (Char -> Bool) -> String -> (String, String)
3838span p xs with strM xs {
39− span p "" | StrNil = ("", "");
39+ span p "" | StrNil = ("", "")
4040 span p (strCons x xs) | (StrCons _ _) with p x {
4141 | True with span p xs {
42− | (ys, zs) = (strCons x ys, zs);
42+ | (ys, zs) = (strCons x ys, zs)
4343 }
44− | False = ("", strCons x xs);
44+ | False = ("", strCons x xs)
4545 }
4646}
4747
48−break : (Char -> Bool) -> String -> (String, String);
49−break p = span (not . p);
48+break : (Char -> Bool) -> String -> (String, String)
49+break p = span (not . p)
5050
51−split : (Char -> Bool) -> String -> List String;
52−split p xs = map pack (split p (unpack xs));
51+split : (Char -> Bool) -> String -> List String
52+split p xs = map pack (split p (unpack xs))
5353
54−ltrim : String -> String;
54+ltrim : String -> String
5555ltrim xs with strM xs {
56− ltrim "" | StrNil = "";
56+ ltrim "" | StrNil = ""
5757 ltrim (strCons x xs) | StrCons _ _
58− = if (isSpace x) then (ltrim xs) else (strCons x xs);
58+ = if (isSpace x) then (ltrim xs) else (strCons x xs)
5959}
6060
61−trim : String -> String;
62−trim xs = ltrim (rev (ltrim (rev xs)));
61+trim : String -> String
62+trim xs = ltrim (rev (ltrim (rev xs)))
lib/prelude/vect.idr+23−22
@@ -1,42 +1,43 @@
1−module prelude.vect;
1+module prelude.vect
22
3−import prelude.nat;
3+import prelude.nat
44
55%access public
66
77data Fin : Nat -> Set where
88 fO : Fin (S k)
9− | fS : Fin k -> Fin (S k);
9+ | fS : Fin k -> Fin (S k)
1010
1111instance Eq (Fin n) where {
12− fO == fO = True;
13− (fS k) == (fS k') = k == k';
14− _ == _ = False;
12+ fO == fO = True
13+ (fS k) == (fS k') = k == k'
14+ _ == _ = False
1515}
1616
17−infixr 7 :: ;
17+infixr 7 ::
1818
1919data Vect : Set -> Nat -> Set where
2020 Nil : Vect a O
21− | (::) : a -> Vect a k -> Vect a (S k);
21+ | (::) : a -> Vect a k -> Vect a (S k)
2222
23−lookup : Fin n -> Vect a n -> a;
24−lookup fO (x :: xs) = x;
25−lookup (fS k) (x :: xs) = lookup k xs;
26−lookup fO [] impossible;
27−lookup (fS _) [] impossible;
23+lookup : Fin n -> Vect a n -> a
24+lookup fO (x :: xs) = x
25+lookup (fS k) (x :: xs) = lookup k xs
26+lookup fO [] impossible
27+lookup (fS _) [] impossible
2828
29−app : Vect a n -> Vect a m -> Vect a (n + m);
30−app [] ys = ys;
31−app (x :: xs) ys = x :: app xs ys;
29+app : Vect a n -> Vect a m -> Vect a (n + m)
30+app [] ys = ys
31+app (x :: xs) ys = x :: app xs ys
3232
33−filter : (a -> Bool) -> Vect a n -> (p ** Vect a p);
34−filter p [] = ( _ ** [] );
33+filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
34+filter p [] = ( _ ** [] )
3535filter p (x :: xs)
3636 = let (_ ** xs') = filter p xs in
37− if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );
37+ if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
38+
39+map : (a -> b) -> Vect a n -> Vect b n
40+map f [] = []
41+map f (x :: xs) = f x :: map f xs
3842
39−map : (a -> b) -> Vect a n -> Vect b n;
40−map f [] = [];
41−map f (x :: xs) = f x :: map f xs;
4243
lib/system.idr+16−16
@@ -1,28 +1,28 @@
1−module system;
1+module system
22
3−import prelude;
3+import prelude
44
55%access public
66
7−getArgs : IO (List String);
8−getArgs = do { n <- numArgs;
9− ga' [] 0 n; }
7+getArgs : IO (List String)
8+getArgs = do { n <- numArgs
9+ ga' [] 0 n }
1010 where {
11− numArgs : IO Int;
12− numArgs = mkForeign (FFun "epic_numArgs" [] FInt);
11+ numArgs : IO Int
12+ numArgs = mkForeign (FFun "epic_numArgs" [] FInt)
1313
14− getArg : Int -> IO String;
15− getArg x = mkForeign (FFun "epic_getArg" [FInt] FString) x;
14+ getArg : Int -> IO String
15+ getArg x = mkForeign (FFun "epic_getArg" [FInt] FString) x
1616
17− ga' : List String -> Int -> Int -> IO (List String);
17+ ga' : List String -> Int -> Int -> IO (List String)
1818 ga' acc i n = if (i == n) then (return $ rev acc) else
19− do { arg <- getArg i;
20− ga' (arg :: acc) (i+1) n; };
19+ do { arg <- getArg i
20+ ga' (arg :: acc) (i+1) n }
2121 }
2222
23−getEnv : String -> IO String;
24−getEnv x = mkForeign (FFun "getenv" [FString] FString) x;
23+getEnv : String -> IO String
24+getEnv x = mkForeign (FFun "getenv" [FString] FString) x
2525
26−exit : Int -> IO ();
27−exit code = mkForeign (FFun "exit" [FInt] FUnit) code;
26+exit : Int -> IO ()
27+exit code = mkForeign (FFun "exit" [FInt] FUnit) code
2828
samples/interp.idr+44−45
@@ -1,25 +1,25 @@
1−module main;
1+module main
22
3−data Ty = TyInt | TyBool| TyFun Ty Ty;
3+data Ty = TyInt | TyBool| TyFun Ty Ty
44
5−interpTy : Ty -> Set;
6−interpTy TyInt = Int;
7−interpTy TyBool = Bool;
8−interpTy (TyFun s t) = interpTy s -> interpTy t;
5+interpTy : Ty -> Set
6+interpTy TyInt = Int
7+interpTy TyBool = Bool
8+interpTy (TyFun s t) = interpTy s -> interpTy t
99
1010using (G : Vect Ty n) {
1111
1212 data Env : Vect Ty n -> Set where
1313 Nil : Env Nil
14− | (::) : interpTy a -> Env G -> Env (a :: G);
14+ | (::) : interpTy a -> Env G -> Env (a :: G)
1515
1616 data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
1717 stop : HasType fO (t :: G) t
18− | pop : HasType k G t -> HasType (fS k) (u :: G) t;
18+ | pop : HasType k G t -> HasType (fS k) (u :: G) t
1919
20− lookup : HasType i G t -> Env G -> interpTy t;
21− lookup stop (x :: xs) = x;
22− lookup (pop k) (x :: xs) = lookup k xs;
20+ lookup : HasType i G t -> Env G -> interpTy t
21+ lookup stop (x :: xs) = x
22+ lookup (pop k) (x :: xs) = lookup k xs
2323
2424 data Expr : Vect Ty n -> Ty -> Set where
2525 Var : HasType i G t -> Expr G t
@@ -29,58 +29,57 @@ using (G : Vect Ty n) {
2929 | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
3030 Expr G c
3131 | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
32− | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
32+ | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
3333
34− interp : Env G -> {static} Expr G t -> interpTy t;
35− interp env (Var i) = lookup i env;
36− interp env (Val x) = x;
37− interp env (Lam sc) = \x => interp (x :: env) sc;
38− interp env (App f s) = (interp env f) (interp env s);
39− interp env (Op op x y) = op (interp env x) (interp env y);
40− interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e);
41− interp env (Bind v f) = interp env (f (interp env v));
34+ interp : Env G -> {static} Expr G t -> interpTy t
35+ interp env (Var i) = lookup i env
36+ interp env (Val x) = x
37+ interp env (Lam sc) = \x => interp (x :: env) sc
38+ interp env (App f s) = (interp env f) (interp env s)
39+ interp env (Op op x y) = op (interp env x) (interp env y)
40+ interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e)
41+ interp env (Bind v f) = interp env (f (interp env v))
4242
43− eId : Expr G (TyFun TyInt TyInt);
44− eId = Lam (Var stop);
43+ eId : Expr G (TyFun TyInt TyInt)
44+ eId = Lam (Var stop)
4545
46− eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt));
47− eTEST = Lam (Lam (Var (pop stop)));
46+ eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))
47+ eTEST = Lam (Lam (Var (pop stop)))
4848
49− eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));
50− eAdd = Lam (Lam (Op prim__addInt (Var stop) (Var (pop stop))));
49+ eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
50+ eAdd = Lam (Lam (Op prim__addInt (Var stop) (Var (pop stop))))
5151
52−-- eDouble : Expr G (TyFun TyInt TyInt);
53−-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));
52+-- eDouble : Expr G (TyFun TyInt TyInt)
53+-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO))
5454
55− eDouble : Expr G (TyFun TyInt TyInt);
56− eDouble = Lam (App (App eAdd (Var stop)) (Var stop));
55+ eDouble : Expr G (TyFun TyInt TyInt)
56+ eDouble = Lam (App (App eAdd (Var stop)) (Var stop))
5757
58− app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;
59− app = \f, a => App f a;
58+ app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
59+ app = \f, a => App f a
6060
61− eFac : Expr G (TyFun TyInt TyInt);
61+ eFac : Expr G (TyFun TyInt TyInt)
6262 eFac = Lam (If (Op (==) (Var stop) (Val 0))
63− (Val 1) (Op (*) (app eFac (Op (-) (Var stop) (Val 1))) (Var stop)));
63+ (Val 1) (Op (*) (app eFac (Op (-) (Var stop) (Val 1))) (Var stop)))
6464
6565 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
6666
67− eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt));
68− eProg = Lam (Lam
69− (Bind (App eDouble (Var (pop stop)))
67+ eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt))
68+ eProg = Lam (Lam (Bind (App eDouble (Var (pop stop)))
7069 (\x => Bind (App eDouble (Var stop))
7170 (\y => Bind (App eDouble (Val x))
72− (\z => App (App eAdd (Val y)) (Val z))))));
71+ (\z => App (App eAdd (Val y)) (Val z))))))
7372
7473}
7574
76−test : Int;
77−test = interp [] eProg 2 2;
75+test : Int
76+test = interp [] eProg 2 2
7877
79−testFac : Int;
80−testFac = interp [] eFac 4;
78+testFac : Int
79+testFac = interp [] eFac 4
8180
82−main : IO ();
83−main = do { print testFac;
84− print test; };
81+main : IO ()
82+main = do { print testFac
83+ print test }
8584
8685
src/Idris/AbsSyntax.hs+2−1
@@ -50,6 +50,7 @@ data IState = IState { tt_ctxt :: Context,
5050 last_proof :: Maybe (Name, [String]),
5151 errLine :: Maybe Int,
5252 lastParse :: Maybe Name,
53+ indent_stack :: [Int],
5354 hide_list :: [(Name, Maybe Accessibility)],
5455 default_access :: Accessibility,
5556 ibc_write :: [IBCWrite]
@@ -72,7 +73,7 @@ data IBCWrite = IBCFix FixDecl
7273
7374idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
7475 "" defaultOpts 6 [] [] [] [] [] [] [] []
75− Nothing Nothing Nothing [] Hidden []
76+ Nothing Nothing Nothing [] [] Hidden []
7677
7778-- The monad for the main REPL - reading and processing files and updating
7879-- global state (hence the IO inner monad).
src/Idris/Parser.hs+137−59
@@ -140,17 +140,54 @@ parseImports fname input
140140 Right (x, i) -> do put i
141141 return x
142142 where ishow err = let ln = sourceLine (errorPos err) in
143− fname ++ ":" ++ show ln ++ ":parse error"
143+ fname ++ ":" ++ show ln ++ ":parse error"
144144-- show (map messageString (errorMessages err))
145145
146146pHeader :: IParser [String]
147−pHeader = try (do reserved "module"; i <- identifier; lchar ';'
147+pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
148148 return (parseName i))
149149 <|> return []
150150 where parseName x = case span (/='.') x of
151151 (x, "") -> [x]
152152 (x, '.':y) -> x : parseName y
153153
154+push_indent :: IParser ()
155+push_indent = do pos <- getPosition
156+ ist <- getState
157+ setState (ist { indent_stack = sourceColumn pos :
158+ indent_stack ist })
159+
160+last_indent :: IParser Int
161+last_indent = do ist <- getState
162+ case indent_stack ist of
163+ (x : xs) -> return x
164+ _ -> return (-1)
165+
166+indent :: IParser Int
167+indent = do pos <- getPosition
168+ return (sourceColumn pos)
169+
170+pop_indent :: IParser ()
171+pop_indent = do ist <- getState
172+ let (x : xs) = indent_stack ist
173+ setState (ist { indent_stack = xs })
174+
175+pTerminator = do lchar ';'; pop_indent
176+ <|> do c <- indent; l <- last_indent
177+ if (c <= l) then pop_indent
178+ else fail "Not a terminator"
179+ <|> do i <- getInput; if (take 1 i == "}") then pop_indent
180+ else fail "Not a terminator"
181+ <|> lookAhead eof
182+
183+pKeepTerminator
184+ = do lchar ';'; return ()
185+ <|> do c <- indent; l <- last_indent
186+ if (c <= l) then return ()
187+ else fail "Not a terminator"
188+ <|> do i <- getInput; if (take 1 i == "}") then return ()
189+ else fail "Not a terminator"
190+ <|> lookAhead eof
154191
155192pfc :: IParser FC
156193pfc = do s <- getPosition
@@ -163,7 +200,7 @@ pfc = do s <- getPosition
163200pImport :: IParser String
164201pImport = do reserved "import"
165202 f <- identifier
166− lchar ';'
203+ option ';' (lchar ';')
167204 return (map dot f)
168205 where dot '.' = '/'
169206 dot c = c
@@ -182,6 +219,7 @@ parseProg syn fname input pos
182219 return (collect x)
183220 where ishow err = let ln = sourceLine (errorPos err) in
184221 fname ++ ":" ++ show ln ++ ":parse error"
222+ ++ " " ++ show (sourceColumn (errorPos err))
185223-- show (map messageString (errorMessages err))
186224
187225-- Collect PClauses with the same function name
@@ -244,7 +282,7 @@ pDecl' syn
244282 = try pFixity
245283 <|> pFunDecl' syn
246284 <|> try (pData syn)
247− <|> try (pSyntaxDecl syn)
285+ <|> pSyntaxDecl syn
248286
249287pSyntaxDecl :: SyntaxInfo -> IParser PDecl
250288pSyntaxDecl syn
@@ -267,7 +305,8 @@ pSyntaxDecl syn
267305
268306pSyntaxRule :: SyntaxInfo -> IParser Syntax
269307pSyntaxRule syn
270− = do sty <- option AnySyntax (do reserved "term"; return TermSyntax
308+ = do push_indent
309+ sty <- option AnySyntax (do reserved "term"; return TermSyntax
271310 <|> do reserved "pattern"; return PatternSyntax)
272311 reserved "syntax"
273312 syms <- many1 pSynSym
@@ -277,7 +316,7 @@ pSyntaxRule syn
277316 $ fail "Repeated variable in syntax rule"
278317 lchar '='
279318 tm <- pExpr syn
280− lchar ';'
319+ pTerminator
281320 return (Rule syms tm sty)
282321 where
283322 expr (Expr _) = True
@@ -294,12 +333,13 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'
294333 return (Symbol sym)
295334
296335pFunDecl' :: SyntaxInfo -> IParser PDecl
297−pFunDecl' syn = try (do acc <- pAccessibility
336+pFunDecl' syn = try (do push_indent
337+ acc <- pAccessibility
298338 n_in <- pfName
299339 let n = expandNS syn n_in
300340 ty <- pTSig syn
301341 fc <- pfc
302− lchar ';'
342+ pTerminator
303343-- ty' <- implicit syn n ty
304344 addAcc n acc
305345 return (PTy syn fc n ty))
@@ -348,8 +388,9 @@ expandNS syn n = case syn_namespace syn of
348388--------- Fixity ---------
349389
350390pFixity :: IParser PDecl
351−pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
352− lchar ';'
391+pFixity = do push_indent
392+ f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
393+ pTerminator
353394 let prec = fromInteger i
354395 istate <- getState
355396 let fs = map (Fix (f prec)) ops
@@ -428,12 +469,12 @@ pSimpleExtExpr syn = do i <- getState
428469
429470pNoExtExpr syn =
430471 try (pApp syn)
431− <|> try (pComprehension syn)
432− <|> pSimpleExpr syn
472+ <|> try (pSimpleExpr syn)
433473 <|> pLambda syn
434474 <|> pLet syn
435475 <|> pPi syn
436476 <|> pDoBlock syn
477+ <|> pComprehension syn
437478
438479pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
439480pExtensions syn rules = choice (map (\x -> try (pExt syn x)) (filter valid rules))
@@ -529,19 +570,10 @@ pSimpleExpr syn =
529570 lchar '}'
530571 return (PCase fc scr opts)
531572 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
532− <|> try (pPair syn)
533573 <|> try (pList syn)
534574 <|> try (pAlt syn)
535575 <|> try (pIdiom syn)
536− <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)
537− <|> try (do lchar '('; fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'
538− return $ PLam (MN 0 "x") Placeholder
539− (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 0 "x")),
540− pexp e]))
541− <|> try (do lchar '('; fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'
542− return $ PLam (MN 0 "x") Placeholder
543− (PApp fc (PRef fc (UN o)) [pexp e,
544− pexp (PRef fc (MN 0 "x"))]))
576+ <|> try (do lchar '('; bracketed syn)
545577 <|> try (do c <- pConstant; fc <- pfc
546578 return (modifyConst syn fc (PConstant c)))
547579 <|> do reserved "Set"; return PSet
@@ -550,6 +582,18 @@ pSimpleExpr syn =
550582 <|> do lchar '_'; return Placeholder
551583 <|> pSimpleExtExpr syn
552584
585+bracketed syn =
586+ try (pPair syn)
587+ <|> try (do e <- pExpr syn; lchar ')'; return e)
588+ <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'
589+ return $ PLam (MN 0 "x") Placeholder
590+ (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 0 "x")),
591+ pexp e]))
592+ <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'
593+ return $ PLam (MN 0 "x") Placeholder
594+ (PApp fc (PRef fc (UN o)) [pexp e,
595+ pexp (PRef fc (MN 0 "x"))]))
596+
553597pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
554598pCaseOpt syn = do lhs <- pExpr syn; symbol "=>";
555599 rhs <- pExpr syn
@@ -568,28 +612,37 @@ pList syn = do lchar '['; fc <- pfc
568612 mkList fc [] = PRef fc (UN "Nil")
569613 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
570614
571−pPair syn = try (do lchar '('; l <- pExpr syn; op <- pairOp
615+pPair syn = try (do l <- pExpr syn
572616 fc <- pfc
573− r <- pExpr syn; lchar ')';
574− return (op fc l r))
575− <|> try (do lchar '('; x <- ntuple
617+ rest <- restTuple
618+ case rest of
619+ [] -> return l
620+ [Left r] -> return (PPair fc l r)
621+ [Right r] -> return (PDPair fc l Placeholder r))
622+ <|> try (do x <- ntuple
576623 lchar ')'
577624 return x)
578− <|> do lchar '('; ln <- pName; lchar ':'; lty <- pExpr syn;
625+ <|> do ln <- pName; lchar ':'; lty <- pExpr syn;
579626 reservedOp "**";
580627 fc <- pfc
581628 r <- pExpr syn; lchar ')';
582629 return (PDPair fc (PRef fc ln) lty r)
583630 where
631+ restTuple = do lchar ')'; return []
632+ <|> do lchar ','
633+ r <- pExpr syn
634+ lchar ')'
635+ return [Left r]
636+ <|> do reservedOp "**"
637+ r <- pExpr syn
638+ lchar ')'
639+ return [Right r]
584640 ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
585641 rest <- ntuple
586642 return (PPair fc l rest))
587643 <|> (do l <- pExpr syn; fc <- pfc; lchar ','
588644 r <- pExpr syn
589645 return (PPair fc l r))
590−
591− pairOp = do lchar ','; return PPair
592− <|> do reservedOp "**"; return (\f x y -> PDPair f x Placeholder y)
593646
594647pAlt syn = do symbol "(|";
595648 alts <- sepBy1 (pExpr' syn) (lchar ',')
@@ -604,9 +657,19 @@ pHSimpleExpr syn
604657
605658pApp syn = do f <- pSimpleExpr syn
606659 fc <- pfc
607− args <- many1 (pArg syn)
660+ args <- many1 (do notEndApp
661+ pArg syn)
608662 return (PApp fc f args)
609663
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+
610673pArg :: SyntaxInfo -> IParser PArg
611674pArg syn = try (pImplicitArg syn)
612675 <|> try (pConstraintArg syn)
@@ -627,18 +690,17 @@ pTSig syn = do lchar ':'
627690 sc <- pExpr syn
628691 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
629692
630−pLambda syn = try (do lchar '\\';
631− xt <- tyOptDeclList syn
632− symbol "=>"
633− sc <- pExpr syn
634− return (bindList PLam xt sc))
635− <|> (do lchar '\\'
636− ps <- sepBy (do fc <- pfc
637− e <- pSimpleExpr syn
638− return (fc, e)) (lchar ',')
639− symbol "=>"
640− sc <- pExpr syn
641− return (pmList (zip [0..] ps) sc))
693+pLambda syn = do lchar '\\'
694+ (try (do xt <- tyOptDeclList syn
695+ symbol "=>"
696+ sc <- pExpr syn
697+ return (bindList PLam xt sc))
698+ <|> (do ps <- sepBy (do fc <- pfc
699+ e <- pSimpleExpr syn
700+ return (fc, e)) (lchar ',')
701+ symbol "=>"
702+ sc <- pExpr syn
703+ return (pmList (zip [0..] ps) sc)))
642704 where pmList [] sc = sc
643705 pmList ((i, (fc, x)) : xs) sc
644706 = PLam (MN i "lamp") Placeholder
@@ -713,7 +775,9 @@ pComprehension syn
713775
714776pDoBlock syn
715777 = do reserved "do"; lchar '{'
716− ds <- endBy1 (pDo syn) (lchar ';')
778+ push_indent
779+ ds <- many1 (do x <- pDo syn; pKeepTerminator; return x)
780+ pop_indent
717781 lchar '}'
718782 return (PDoBlock ds)
719783
@@ -788,23 +852,25 @@ accData (Just Frozen) n ns = do addAcc n (Just Frozen)
788852accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns
789853
790854pData :: SyntaxInfo -> IParser PDecl
791−pData syn = try (do acc <- pAccessibility
855+pData syn = try (do push_indent
856+ acc <- pAccessibility
792857 reserved "data"; fc <- pfc
793858 tyn_in <- pfName; ty <- pTSig syn
794859 let tyn = expandNS syn tyn_in
795860 reserved "where"
796861-- ty' <- implicit syn tyn ty
797862 cons <- sepBy (pConstructor syn) (lchar '|')
798− lchar ';'
863+ pTerminator
799864 accData acc tyn (map (\ (n, _, _) -> n) cons)
800865 return $ PData syn fc (PDatadecl tyn ty cons))
801− <|> do acc <- pAccessibility
866+ <|> do push_indent
867+ acc <- pAccessibility
802868 reserved "data"; fc <- pfc
803869 tyn_in <- pfName; args <- many pName
804870 let tyn = expandNS syn tyn_in
805871 lchar '='
806872 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
807− lchar ';'
873+ pTerminator
808874 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
809875 let ty = bindArgs (map (\a -> PSet) args) PSet
810876-- ty' <- implicit syn tyn ty
@@ -835,7 +901,8 @@ pSimpleCon syn
835901 = do cn_in <- pfName
836902 let cn = expandNS syn cn_in
837903 fc <- pfc
838− args <- many (pSimpleExpr syn)
904+ args <- many (do notEndApp
905+ pSimpleExpr syn)
839906 return (cn, args, fc)
840907
841908--------- Pattern match clauses ---------
@@ -859,7 +926,8 @@ pRHS syn n = do lchar '='; pExpr syn
859926
860927pClause :: SyntaxInfo -> IParser PClause
861928pClause syn
862− = try (do n_in <- pfName; let n = expandNS syn n_in
929+ = try (do push_indent
930+ n_in <- pfName; let n = expandNS syn n_in
863931 cargs <- many (pConstraintArg syn)
864932 iargs <- many (pImplicitArg syn)
865933 fc <- pfc
@@ -869,15 +937,18 @@ pClause syn
869937 ist <- getState
870938 let ctxt = tt_ctxt ist
871939 let wsyn = syn { syn_namespace = [] }
872− (wheres, nmap) <- choice [pWhereblock n wsyn,
873− do lchar ';'
940+ (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
941+ pop_indent
942+ return x,
943+ do pTerminator
874944 return ([], [])]
875945 let capp = PApp fc (PRef fc n)
876946 (iargs ++ cargs ++ map pexp args)
877947 ist <- getState
878948 setState (ist { lastParse = Just n })
879949 return $ PClause n capp wargs rhs wheres)
880− <|> try (do wargs <- many1 (pWExpr syn)
950+ <|> try (do push_indent
951+ wargs <- many1 (pWExpr syn)
881952 ist <- getState
882953 n <- case lastParse ist of
883954 Just t -> return t
@@ -885,12 +956,15 @@ pClause syn
885956 rhs <- pRHS syn n
886957 let ctxt = tt_ctxt ist
887958 let wsyn = syn { syn_namespace = [] }
888− (wheres, nmap) <- choice [pWhereblock n wsyn,
889− do lchar ';'
959+ (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
960+ pop_indent
961+ return x,
962+ do pTerminator
890963 return ([], [])]
891964 return $ PClauseR wargs rhs wheres)
892965
893− <|> try (do n_in <- pfName; let n = expandNS syn n_in
966+ <|> try (do push_indent
967+ n_in <- pfName; let n = expandNS syn n_in
894968 cargs <- many (pConstraintArg syn)
895969 iargs <- many (pImplicitArg syn)
896970 fc <- pfc
@@ -906,6 +980,7 @@ pClause syn
906980 lchar '}'
907981 ist <- getState
908982 setState (ist { lastParse = Just n })
983+ pop_indent
909984 return $ PWith n capp wargs wval withs)
910985
911986 <|> try (do wargs <- many1 (pWExpr syn)
@@ -917,7 +992,8 @@ pClause syn
917992 lchar '}'
918993 return $ PWithR wargs wval withs)
919994
920− <|> do l <- pArgExpr syn
995+ <|> do push_indent
996+ l <- pArgExpr syn
921997 op <- operator
922998 let n = expandNS syn (UN op)
923999 r <- pArgExpr syn
@@ -925,8 +1001,10 @@ pClause syn
9251001 wargs <- many (pWExpr syn)
9261002 rhs <- pRHS syn n
9271003 let wsyn = syn { syn_namespace = [] }
928− (wheres, nmap) <- choice [pWhereblock n wsyn,
929− do lchar ';'
1004+ (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1005+ pop_indent
1006+ return x,
1007+ do pTerminator
9301008 return ([], [])]
9311009 ist <- getState
9321010 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
src/Idris/Unlit.hs+2−2
@@ -10,8 +10,8 @@ unlit f s = do let s' = map ulLine (lines s)
1010
1111data LineType = Prog | Blank | Comm
1212
13−ulLine ('>':xs) = case span isSpace xs of
14− (_, p) -> (Prog, p)
13+ulLine ('>':' ':xs) = (Prog, xs)
14+ulLine ('>':xs) = (Prog, xs)
1515ulLine xs | all isSpace xs = (Blank, "")
1616 | otherwise = (Comm, '-':'-':xs)
1717
test/test001/test001.idr+43−43
@@ -1,25 +1,25 @@
1−module main;
1+module main
22
3−data Ty = TyInt | TyBool| TyFun Ty Ty;
3+data Ty = TyInt | TyBool| TyFun Ty Ty
44
5−interpTy : Ty -> Set;
6−interpTy TyInt = Int;
7−interpTy TyBool = Bool;
8−interpTy (TyFun s t) = interpTy s -> interpTy t;
5+interpTy : Ty -> Set
6+interpTy TyInt = Int
7+interpTy TyBool = Bool
8+interpTy (TyFun s t) = interpTy s -> interpTy t
99
1010using (G : Vect Ty n) {
1111
1212 data Env : Vect Ty n -> Set where
1313 Nil : Env Nil
14− | (::) : interpTy a -> Env G -> Env (a :: G);
14+ | (::) : interpTy a -> Env G -> Env (a :: G)
1515
1616 data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
1717 stop : HasType fO (t :: G) t
18− | pop : HasType k G t -> HasType (fS k) (u :: G) t;
18+ | pop : HasType k G t -> HasType (fS k) (u :: G) t
1919
20− lookup : HasType i G t -> Env G -> interpTy t;
21− lookup stop (x :: xs) = x;
22− lookup (pop k) (x :: xs) = lookup k xs;
20+ lookup : HasType i G t -> Env G -> interpTy t
21+ lookup stop (x :: xs) = x
22+ lookup (pop k) (x :: xs) = lookup k xs
2323
2424 data Expr : Vect Ty n -> Ty -> Set where
2525 Var : HasType i G t -> Expr G t
@@ -29,59 +29,59 @@ using (G : Vect Ty n) {
2929 | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
3030 Expr G c
3131 | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
32− | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
32+ | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
3333
34− interp : Env G -> {static} Expr G t -> interpTy t;
35− interp env (Var i) = lookup i env;
36− interp env (Val x) = x;
37− interp env (Lam sc) = \x => interp (x :: env) sc;
38− interp env (App f s) = (interp env f) (interp env s);
39− interp env (Op op x y) = op (interp env x) (interp env y);
40− interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e);
41− interp env (Bind v f) = interp env (f (interp env v));
34+ interp : Env G -> {static} Expr G t -> interpTy t
35+ interp env (Var i) = lookup i env
36+ interp env (Val x) = x
37+ interp env (Lam sc) = \x => interp (x :: env) sc
38+ interp env (App f s) = (interp env f) (interp env s)
39+ interp env (Op op x y) = op (interp env x) (interp env y)
40+ interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e)
41+ interp env (Bind v f) = interp env (f (interp env v))
4242
43− eId : Expr G (TyFun TyInt TyInt);
44− eId = Lam (Var stop);
43+ eId : Expr G (TyFun TyInt TyInt)
44+ eId = Lam (Var stop)
4545
46− eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt));
47− eTEST = Lam (Lam (Var (pop stop)));
46+ eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))
47+ eTEST = Lam (Lam (Var (pop stop)))
4848
49− eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));
50− eAdd = Lam (Lam (Op prim__addInt (Var stop) (Var (pop stop))));
49+ eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
50+ eAdd = Lam (Lam (Op prim__addInt (Var stop) (Var (pop stop))))
5151
52−-- eDouble : Expr G (TyFun TyInt TyInt);
53−-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));
52+-- eDouble : Expr G (TyFun TyInt TyInt)
53+-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO))
5454
55− eDouble : Expr G (TyFun TyInt TyInt);
56− eDouble = Lam (App (App eAdd (Var stop)) (Var stop));
55+ eDouble : Expr G (TyFun TyInt TyInt)
56+ eDouble = Lam (App (App eAdd (Var stop)) (Var stop))
5757
58− app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;
59− app = \f, a => App f a;
58+ app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
59+ app = \f, a => App f a
6060
61− eFac : Expr G (TyFun TyInt TyInt);
61+ eFac : Expr G (TyFun TyInt TyInt)
6262 eFac = Lam (If (Op (==) (Var stop) (Val 0))
63− (Val 1) (Op (*) (app eFac (Op (-) (Var stop) (Val 1))) (Var stop)));
63+ (Val 1) (Op (*) (app eFac (Op (-) (Var stop) (Val 1))) (Var stop)))
6464
6565 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
6666
67− eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt));
67+ eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt))
6868 eProg = Lam (Lam
6969 (Bind (App eDouble (Var (pop stop)))
7070 (\x => Bind (App eDouble (Var stop))
7171 (\y => Bind (App eDouble (Val x))
72− (\z => App (App eAdd (Val y)) (Val z))))));
72+ (\z => App (App eAdd (Val y)) (Val z))))))
7373
7474}
7575
76−test : Int;
77−test = interp [] eProg 2 2;
76+test : Int
77+test = interp [] eProg 2 2
7878
79−testFac : Int;
80−testFac = interp [] eFac 4;
79+testFac : Int
80+testFac = interp [] eFac 4
8181
82−main : IO ();
83−main = do { print testFac;
84− print test; };
82+main : IO ()
83+main = do { print testFac
84+ print test }
8585
8686
8787
test/test003/lit.lidr+12−12
@@ -1,19 +1,19 @@
1−> module lit;
1+> module lit
22
33Test some string primitives while we're at it
44
5−> st : String;
6−> st = "abcdefg";
5+> st : String
6+> st = "abcdefg"
77
88Literate main program
99
10−> main : IO ();
11−> main = do { putStrLn (show (strHead st));
12−> putStrLn (show (strIndex st 3));
13−> putStrLn (strCons 'z' st);
14−> putStrLn (rev st);
15−> let x = unpack st;
16−> putStrLn (show (rev x));
17−> putStrLn (pack x);
18−> };
10+> main : IO ()
11+> main = do { putStrLn (show (strHead st))
12+> putStrLn (show (strIndex st 3))
13+> putStrLn (strCons 'z' st)
14+> putStrLn (rev st)
15+> let x = unpack st
16+> putStrLn (show (rev x))
17+> putStrLn (pack x)
18+> }
1919