git.iko.soy/Idris-dev
on master help sign in
Removed need for terminating ;
bd61594Edwin Brady
lib/builtins.idr+123−123
compare with master
unifiedsplit
@@ -1,246 +1,246 @@
1%access public
1%access public
2
2
3data Exists : (a : Set) -> (P : a -> Set) -> Set where
3data 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
5
5
6−getWitness : {P : a -> Set} -> Exists a P -> a;
6+getWitness : {P : a -> Set} -> Exists a P -> a
7−getWitness (a ** v) = a;
7+getWitness (a ** v) = a
8
8
9−getProof : {P : a -> Set} -> (s : Exists a P) -> P (getWitness s);
9+getProof : {P : a -> Set} -> (s : Exists a P) -> P (getWitness s)
10−getProof (a ** v) = v;
10+getProof (a ** v) = v
11
11
12−FalseElim : _|_ -> a;
12+FalseElim : _|_ -> a
13
13
14-- For rewrite tactic
14-- For rewrite tactic
15−replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Set} -> x = y -> P x -> P y;
15+replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Set} -> x = y -> P x -> P y
16−replace refl prf = prf;
16+replace refl prf = prf
17
17
18−sym : {x:a} -> {y:a} -> x = y -> y = x;
18+sym : {x:a} -> {y:a} -> x = y -> y = x
19−sym refl = refl;
19+sym refl = refl
20
20
21−lazy : a -> a;
21+lazy : a -> a
22−lazy x = x; -- compiled specially
22+lazy x = x -- compiled specially
23
23
24−believe_me : a -> b; -- compiled specially as id, use with care!
24+believe_me : a -> b -- compiled specially as id, use with care!
25−believe_me x = prim__believe_me _ _ x;
25+believe_me x = prim__believe_me _ _ x
26
26
27namespace builtins {
27namespace builtins {
28
28
29−id : a -> a;
29+id : a -> a
30−id x = x;
30+id x = x
31
31
32−const : a -> b -> a;
32+const : a -> b -> a
33−const x _ = x;
33+const x _ = x
34
34
35−fst : (s, t) -> s;
35+fst : (s, t) -> s
36−fst (x, y) = x;
36+fst (x, y) = x
37
37
38−snd : (a, b) -> b;
38+snd : (a, b) -> b
39−snd (x, y) = y;
39+snd (x, y) = y
40
40
41−infixl 9 .;
41+infixl 9 .
42
42
43−(.) : (b -> c) -> (a -> b) -> a -> c;
43+(.) : (b -> c) -> (a -> b) -> a -> c
44−(.) f g x = f (g x);
44+(.) f g x = f (g x)
45
45
46−flip : (a -> b -> c) -> b -> a -> c;
46+flip : (a -> b -> c) -> b -> a -> c
47−flip f x y = f y x;
47+flip f x y = f y x
48
48
49−infixr 1 $;
49+infixr 1 $
50
50
51−($) : (a -> b) -> a -> b;
51+($) : (a -> b) -> a -> b
52−f $ a = f a;
52+f $ a = f a
53
53
54−data Bool = False | True;
54+data Bool = False | True
55
55
56−boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a;
56+boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a
57−boolElim True t e = t;
57+boolElim True t e = t
58−boolElim False t e = e;
58+boolElim False t e = e
59
59
60−data so : Bool -> Set where oh : so True;
60+data so : Bool -> Set where oh : so True
61
61
62−syntax if [test] then [t] else [e] = boolElim test t e;
62+syntax if [test] then [t] else [e] = boolElim test t e
63−syntax [test] "?" [t] ":" [e] = if test then t else e;
63+syntax [test] "?" [t] ":" [e] = if test then t else e
64
64
65−infixl 4 &&, ||;
65+infixl 4 &&, ||
66
66
67−(||) : Bool -> Bool -> Bool;
67+(||) : Bool -> Bool -> Bool
68−(||) False x = x;
68+(||) False x = x
69−(||) True _ = True;
69+(||) True _ = True
70
70
71−(&&) : Bool -> Bool -> Bool;
71+(&&) : Bool -> Bool -> Bool
72−(&&) True x = x;
72+(&&) True x = x
73−(&&) False _ = False;
73+(&&) False _ = False
74
74
75−not : Bool -> Bool;
75+not : Bool -> Bool
76−not True = False;
76+not True = False
77−not False = True;
77+not False = True
78
78
79−infixl 5 ==, /=, ==.;
79+infixl 5 ==, /=, ==.
80−infixl 6 <, <=, >, >=, <., <=., >., >=.;
80+infixl 6 <, <=, >, >=, <., <=., >., >=.
81−infixl 7 <<, >>;
81+infixl 7 <<, >>
82−infixl 8 +,-,++,+.,-.;
82+infixl 8 +,-,++,+.,-.
83−infixl 9 *,/,*.,/.;
83+infixl 9 *,/,*.,/.
84
84
85--- Numeric operators
85--- Numeric operators
86
86
87−intToBool : Int -> Bool;
87+intToBool : Int -> Bool
88−intToBool 0 = False;
88+intToBool 0 = False
89−intToBool x = True;
89+intToBool x = True
90
90
91−boolOp : (a -> a -> Int) -> a -> a -> Bool;
91+boolOp : (a -> a -> Int) -> a -> a -> Bool
92−boolOp op x y = intToBool (op x y);
92+boolOp op x y = intToBool (op x y)
93
93
94class Eq a where {
94class Eq a where {
95− (==) : a -> a -> Bool;
95+ (==) : a -> a -> Bool
96− (/=) : a -> a -> Bool;
96+ (/=) : a -> a -> Bool
97
97
98− x /= y = not (x == y);
98+ x /= y = not (x == y)
99− x == y = not (x /= y);
99+ x == y = not (x /= y)
100}
100}
101
101
102instance Eq Int where {
102instance Eq Int where {
103− (==) = boolOp prim__eqInt;
103+ (==) = boolOp prim__eqInt
104}
104}
105
105
106instance Eq Integer where {
106instance Eq Integer where {
107− (==) = boolOp prim__eqBigInt;
107+ (==) = boolOp prim__eqBigInt
108}
108}
109
109
110instance Eq Float where {
110instance Eq Float where {
111− (==) = boolOp prim__eqFloat;
111+ (==) = boolOp prim__eqFloat
112}
112}
113
113
114instance Eq Char where {
114instance Eq Char where {
115− (==) = boolOp prim__eqChar;
115+ (==) = boolOp prim__eqChar
116}
116}
117
117
118instance Eq String where {
118instance Eq String where {
119− (==) = boolOp prim__eqString;
119+ (==) = boolOp prim__eqString
120}
120}
121
121
122−data Ordering = LT | EQ | GT;
122+data Ordering = LT | EQ | GT
123
123
124class Eq a => Ord a where {
124class Eq a => Ord a where {
125− compare : a -> a -> Ordering;
125+ compare : a -> a -> Ordering
126
126
127− (<) : a -> a -> Bool;
127+ (<) : a -> a -> Bool
128− (<) x y with compare x y {
128+ (<) x y with (compare x y) {
129− (<) x y | LT = True;
129+ (<) x y | LT = True
130− (<) x y | _ = False;
130+ (<) x y | _ = False
131 }
131 }
132
132
133− (>) : a -> a -> Bool;
133+ (>) : a -> a -> Bool
134− (>) x y with compare x y {
134+ (>) x y with (compare x y) {
135− (>) x y | GT = True;
135+ (>) x y | GT = True
136− (>) x y | _ = False;
136+ (>) x y | _ = False
137 }
137 }
138
138
139− (<=) : a -> a -> Bool;
139+ (<=) : a -> a -> Bool
140− (<=) x y = x < y || x == y;
140+ (<=) x y = x < y || x == y
141
141
142− (>=) : a -> a -> Bool;
142+ (>=) : a -> a -> Bool
143− (>=) x y = x > y || x == y;
143+ (>=) x y = x > y || x == y
144
144
145− max : a -> a -> a;
145+ max : a -> a -> a
146− max x y = if (x > y) then x else y;
146+ max x y = if (x > y) then x else y
147
147
148− min : a -> a -> a;
148+ min : a -> a -> a
149− min x y = if (x < y) then x else y;
149+ min x y = if (x < y) then x else y
150}
150}
151
151
152
152
153instance Ord Int where {
153instance Ord Int where {
154 compare x y = if (x == y) then EQ else
154 compare x y = if (x == y) then EQ else
155 if (boolOp prim__ltInt x y) then LT else
155 if (boolOp prim__ltInt x y) then LT else
156− GT;
156+ GT
157}
157}
158
158
159instance Ord Integer where {
159instance Ord Integer where {
160 compare x y = if (x == y) then EQ else
160 compare x y = if (x == y) then EQ else
161 if (boolOp prim__ltBigInt x y) then LT else
161 if (boolOp prim__ltBigInt x y) then LT else
162− GT;
162+ GT
163}
163}
164
164
165instance Ord Float where {
165instance Ord Float where {
166 compare x y = if (x == y) then EQ else
166 compare x y = if (x == y) then EQ else
167 if (boolOp prim__ltFloat x y) then LT else
167 if (boolOp prim__ltFloat x y) then LT else
168− GT;
168+ GT
169}
169}
170
170
171instance Ord Char where {
171instance Ord Char where {
172 compare x y = if (x == y) then EQ else
172 compare x y = if (x == y) then EQ else
173 if (boolOp prim__ltChar x y) then LT else
173 if (boolOp prim__ltChar x y) then LT else
174− GT;
174+ GT
175}
175}
176
176
177instance Ord String where {
177instance Ord String where {
178 compare x y = if (x == y) then EQ else
178 compare x y = if (x == y) then EQ else
179 if (boolOp prim__ltString x y) then LT else
179 if (boolOp prim__ltString x y) then LT else
180− GT;
180+ GT
181}
181}
182
182
183class (Eq a, Ord a) => Num a where {
183class (Eq a, Ord a) => Num a where {
184− (+) : a -> a -> a;
184+ (+) : a -> a -> a
185− (-) : a -> a -> a;
185+ (-) : a -> a -> a
186− (*) : a -> a -> a;
186+ (*) : a -> a -> a
187
187
188− abs : a -> a;
188+ abs : a -> a
189− abs x = if (x < 0) then (-x) else x;
189+ abs x = if (x < 0) then (-x) else x
190
190
191− fromInteger : Int -> a;
191+ fromInteger : Int -> a
192}
192}
193
193
194
194
195instance Num Int where {
195instance Num Int where {
196− (+) = prim__addInt;
196+ (+) = prim__addInt
197− (-) = prim__subInt;
197+ (-) = prim__subInt
198− (*) = prim__mulInt;
198+ (*) = prim__mulInt
199
199
200− fromInteger = id;
200+ fromInteger = id
201}
201}
202
202
203instance Num Integer where {
203instance Num Integer where {
204− (+) = prim__addBigInt;
204+ (+) = prim__addBigInt
205− (-) = prim__subBigInt;
205+ (-) = prim__subBigInt
206− (*) = prim__mulBigInt;
206+ (*) = prim__mulBigInt
207
207
208− fromInteger = prim__intToBigInt;
208+ fromInteger = prim__intToBigInt
209}
209}
210
210
211instance Num Float where {
211instance Num Float where {
212− (+) = prim__addFloat;
212+ (+) = prim__addFloat
213− (-) = prim__subFloat;
213+ (-) = prim__subFloat
214− (*) = prim__mulFloat;
214+ (*) = prim__mulFloat
215
215
216− fromInteger = prim__intToFloat;
216+ fromInteger = prim__intToFloat
217}
217}
218
218
219−div : Int -> Int -> Int;
219+div : Int -> Int -> Int
220−div = prim__divInt;
220+div = prim__divInt
221
221
222
222
223−(/) : Float -> Float -> Float;
223+(/) : Float -> Float -> Float
224−(/) = prim__divFloat;
224+(/) = prim__divFloat
225
225
226--- string operators
226--- string operators
227
227
228−(++) : String -> String -> String;
228+(++) : String -> String -> String
229−(++) = prim__concat;
229+(++) = prim__concat
230
230
231−strHead : String -> Char;
231+strHead : String -> Char
232−strHead = prim__strHead;
232+strHead = prim__strHead
233
233
234−strTail : String -> String;
234+strTail : String -> String
235−strTail = prim__strTail;
235+strTail = prim__strTail
236
236
237−strCons : Char -> String -> String;
237+strCons : Char -> String -> String
238−strCons = prim__strCons;
238+strCons = prim__strCons
239
239
240−strIndex : String -> Int -> Char;
240+strIndex : String -> Int -> Char
241−strIndex = prim__strIndex;
241+strIndex = prim__strIndex
242
242
243−rev : String -> String;
243+rev : String -> String
244−rev = prim__strRev;
244+rev = prim__strRev
245
245
246}
246}
lib/network/cgi.idr+87−91
@@ -1,153 +1,149 @@
1−module network.cgi;
1+module network.cgi
2
2
3−import system;
3+import system
4
4
5public
5public
6−Vars : Set;
6+Vars : Set
7−Vars = List (String, String);
7+Vars = List (String, String)
8
8
9data CGIInfo = CGISt Vars -- GET
9data CGIInfo = CGISt Vars -- GET
10 Vars -- POST
10 Vars -- POST
11 Vars -- Cookies
11 Vars -- Cookies
12 String -- User agent
12 String -- User agent
13 String -- headers
13 String -- headers
14− String; -- output
14+ String -- output
15
15
16−get_GET : CGIInfo -> Vars;
16+get_GET : CGIInfo -> Vars
17−get_GET (CGISt g _ _ _ _ _) = g;
17+get_GET (CGISt g _ _ _ _ _) = g
18
18
19−get_POST : CGIInfo -> Vars;
19+get_POST : CGIInfo -> Vars
20−get_POST (CGISt _ p _ _ _ _) = p;
20+get_POST (CGISt _ p _ _ _ _) = p
21
21
22−get_Cookies : CGIInfo -> Vars;
22+get_Cookies : CGIInfo -> Vars
23−get_Cookies (CGISt _ _ c _ _ _) = c;
23+get_Cookies (CGISt _ _ c _ _ _) = c
24
24
25−get_UAgent : CGIInfo -> String;
25+get_UAgent : CGIInfo -> String
26−get_UAgent (CGISt _ _ _ a _ _) = a;
26+get_UAgent (CGISt _ _ _ a _ _) = a
27
27
28−get_Headers : CGIInfo -> String;
28+get_Headers : CGIInfo -> String
29−get_Headers (CGISt _ _ _ _ h _) = h;
29+get_Headers (CGISt _ _ _ _ h _) = h
30
30
31−get_Output : CGIInfo -> String;
31+get_Output : CGIInfo -> String
32−get_Output (CGISt _ _ _ _ _ o) = o;
32+get_Output (CGISt _ _ _ _ _ o) = o
33
33
34−add_Headers : String -> CGIInfo -> CGIInfo;
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;
35+add_Headers str (CGISt g p c a h o) = CGISt g p c a (h ++ str) o
36
36
37−add_Output : String -> CGIInfo -> CGIInfo;
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);
38+add_Output str (CGISt g p c a h o) = CGISt g p c a h (o ++ str)
39
39
40abstract
40abstract
41data CGI : Set -> Set where
41data CGI : Set -> Set where
42− MkCGI : (CGIInfo -> IO (a, CGIInfo)) -> CGI a;
42+ MkCGI : (CGIInfo -> IO (a, CGIInfo)) -> CGI a
43
43
44−getAction : CGI a -> CGIInfo -> IO (a, CGIInfo);
44+getAction : CGI a -> CGIInfo -> IO (a, CGIInfo)
45−getAction (MkCGI act) = act;
45+getAction (MkCGI act) = act
46
46
47instance Monad CGI where {
47instance Monad CGI where {
48− (>>=) (MkCGI f) k = MkCGI (\s => do { v <- f s;
48+ (>>=) (MkCGI f) k = MkCGI (\s => do { v <- f s
49− getAction (k (fst v)) (snd v); });
49+ getAction (k (fst v)) (snd v) })
50
50
51− return v = MkCGI (\s => return (v, s));
51+ return v = MkCGI (\s => return (v, s))
52}
52}
53
53
54−setInfo : CGIInfo -> CGI ();
54+setInfo : CGIInfo -> CGI ()
55−setInfo i = MkCGI (\s => return ((), i));
55+setInfo i = MkCGI (\s => return ((), i))
56
56
57−getInfo : CGI CGIInfo;
57+getInfo : CGI CGIInfo
58−getInfo = MkCGI (\s => return (s, s));
58+getInfo = MkCGI (\s => return (s, s))
59
59
60abstract
60abstract
61−lift : IO a -> CGI a ;
61+lift : IO a -> CGI a
62−lift op = MkCGI (\st => do { x <- op;
62+lift op = MkCGI (\st => do { x <- op
63− return (x, st); } );
63+ return (x, st) } )
64
64
65abstract
65abstract
66−output : String -> CGI ();
66+output : String -> CGI ()
67−output s = do { i <- getInfo;
67+output s = do { i <- getInfo
68− setInfo (add_Output s i); };
68+ setInfo (add_Output s i) }
69
69
70abstract
70abstract
71−queryVars : CGI Vars;
71+queryVars : CGI Vars
72−queryVars = do { i <- getInfo;
72+queryVars = do { i <- getInfo
73− return (get_GET i); };
73+ return (get_GET i) }
74
74
75abstract
75abstract
76−postVars : CGI Vars;
76+postVars : CGI Vars
77−postVars = do { i <- getInfo;
77+postVars = do { i <- getInfo
78− return (get_POST i); };
78+ return (get_POST i) }
79
79
80abstract
80abstract
81−cookieVars : CGI Vars;
81+cookieVars : CGI Vars
82−cookieVars = do { i <- getInfo;
82+cookieVars = do { i <- getInfo
83− return (get_Cookies i); };
83+ return (get_Cookies i) }
84
84
85abstract
85abstract
86−queryVar : String -> CGI (Maybe String);
86+queryVar : String -> CGI (Maybe String)
87−queryVar x = do { vs <- queryVars;
87+queryVar x = do { vs <- queryVars
88− return (lookup x vs); };
88+ return (lookup x vs) }
89
89
90−getOutput : CGI String;
90+getOutput : CGI String
91−getOutput = do { i <- getInfo;
91+getOutput = do { i <- getInfo
92− return (get_Output i); };
92+ return (get_Output i) }
93
93
94−getHeaders : CGI String;
94+getHeaders : CGI String
95−getHeaders = do { i <- getInfo;
95+getHeaders = do { i <- getInfo
96− return (get_Headers i); };
96+ return (get_Headers i) }
97
97
98abstract
98abstract
99−flushHeaders : CGI ();
99+flushHeaders : CGI ()
100−flushHeaders = do { o <- getHeaders;
100+flushHeaders = do { o <- getHeaders
101− lift (putStrLn o);
101+ lift (putStrLn o)
102− };
102+ }
103
103
104abstract
104abstract
105−flush : CGI ();
105+flush : CGI ()
106−flush = do { o <- getOutput;
106+flush = do { o <- getOutput
107− lift (putStr o);
107+ lift (putStr o)
108− };
108+ }
109
109
110−getVars : List Char -> String -> List (String, String);
110+getVars : List Char -> String -> List (String, String)
111getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)
111getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)
112 where {
112 where {
113− readVar : String -> Maybe (String, String);
113+ readVar : String -> Maybe (String, String)
114 readVar xs with split (\x => x == '=') xs {
114 readVar xs with split (\x => x == '=') xs {
115− | [k, v] = Just (trim k, trim v);
115+ | [k, v] = Just (trim k, trim v)
116− | _ = Nothing;
116+ | _ = Nothing
117 }
117 }
118 }
118 }
119
119
120−getContent : Int -> IO String;
120+getContent : Int -> IO String
121getContent x = getC x "" where {
121getContent x = getC x "" where {
122− getC : Int -> String -> IO String;
122+ getC : Int -> String -> IO String
123− getC 0 acc = return $ rev acc;
123+ getC 0 acc = return $ rev acc
124− getC n acc = do { x <- getChar;
124+ getC n acc = do { x <- getChar
125− getC (n-1) (strCons x acc); };
125+ getC (n-1) (strCons x acc) }
126}
126}
127
127
128abstract
128abstract
129−runCGI : CGI a -> IO a;
129+runCGI : CGI a -> IO a
130runCGI prog = do {
130runCGI prog = do {
131− clen_in <- getEnv "CONTENT_LENGTH";
131+ clen_in <- getEnv "CONTENT_LENGTH"
132− let clen = prim__strToInt clen_in;
132+ let clen = prim__strToInt clen_in
133− content <- getContent clen;
133+ content <- getContent clen
134− query <- getEnv "QUERY_STRING";
134+ query <- getEnv "QUERY_STRING"
135− cookie <- getEnv "HTTP_COOKIE";
135+ cookie <- getEnv "HTTP_COOKIE"
136− agent <- getEnv "HTTP_USER_AGENT";
136+ agent <- getEnv "HTTP_USER_AGENT"
137
137
138− let get_vars = getVars ['&',';'] query;
138+ let get_vars = getVars ['&',';'] query
139− let post_vars = getVars ['&'] content;
139+ let post_vars = getVars ['&'] content
140− let cookies = getVars [';'] cookie;
140+ let cookies = getVars [';'] cookie
141
141
142 p <- getAction prog (CGISt get_vars post_vars cookies agent
142 p <- getAction prog (CGISt get_vars post_vars cookies agent
143 "Content-type: text/html\n"
143 "Content-type: text/html\n"
144− "");
144+ "")
145− putStrLn (get_Headers (snd p));
145+ putStrLn (get_Headers (snd p))
146− putStr (get_Output (snd p));
146+ putStr (get_Output (snd p))
147− return (fst p);
147+ return (fst p)
148−};
148+}
149−
150−
151−
152−
153
149
lib/prelude.idr+145−142
@@ -1,153 +1,153 @@
1−module prelude;
1+module prelude
2
2
3−import builtins;
3+import builtins
4−import io;
4+import io
5
5
6−import prelude.nat;
6+import prelude.nat
7−import prelude.list;
7+import prelude.list
8−import prelude.maybe;
8+import prelude.maybe
9−import prelude.either;
9+import prelude.either
10−import prelude.vect;
10+import prelude.vect
11−import prelude.strings;
11+import prelude.strings
12−import prelude.char;
12+import prelude.char
13
13
14-- Show and instances
14-- Show and instances
15
15
16class Show a where {
16class Show a where {
17− show : a -> String;
17+ show : a -> String
18}
18}
19
19
20instance Show Nat where {
20instance Show Nat where {
21− show O = "O";
21+ show O = "O"
22− show (S k) = "s" ++ show k;
22+ show (S k) = "s" ++ show k
23}
23}
24
24
25instance Show Int where {
25instance Show Int where {
26− show = prim__intToStr;
26+ show = prim__intToStr
27}
27}
28
28
29instance Show Integer where {
29instance Show Integer where {
30− show = prim__bigIntToStr;
30+ show = prim__bigIntToStr
31}
31}
32
32
33instance Show Float where {
33instance Show Float where {
34− show = prim__floatToStr;
34+ show = prim__floatToStr
35}
35}
36
36
37instance Show Char where {
37instance Show Char where {
38− show x = strCons x "";
38+ show x = strCons x ""
39}
39}
40
40
41instance Show String where {
41instance Show String where {
42− show = id;
42+ show = id
43}
43}
44
44
45instance Show Bool where {
45instance Show Bool where {
46− show True = "True";
46+ show True = "True"
47− show False = "False";
47+ show False = "False"
48}
48}
49
49
50instance (Show a, Show b) => Show (a, b) where {
50instance (Show a, Show b) => Show (a, b) where {
51− show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")";
51+ show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
52}
52}
53
53
54instance Show a => Show (List a) where {
54instance Show a => Show (List a) where {
55 show xs = "[" ++ show' xs ++ "]" where {
55 show xs = "[" ++ show' xs ++ "]" where {
56− show' : Show a => List a -> String;
56+ show' : Show a => List a -> String
57− show' [] = "";
57+ show' [] = ""
58− show' [x] = show x;
58+ show' [x] = show x
59− show' (x :: xs) = show x ++ ", " ++ show' xs;
59+ show' (x :: xs) = show x ++ ", " ++ show' xs
60 }
60 }
61}
61}
62
62
63instance Show a => Show (Vect a n) where {
63instance Show a => Show (Vect a n) where {
64 show xs = "[" ++ show' xs ++ "]" where {
64 show xs = "[" ++ show' xs ++ "]" where {
65− show' : Show a => Vect a n -> String;
65+ show' : Show a => Vect a n -> String
66− show' [] = "";
66+ show' [] = ""
67− show' [x] = show x;
67+ show' [x] = show x
68− show' (x :: xs) = show x ++ ", " ++ show' xs;
68+ show' (x :: xs) = show x ++ ", " ++ show' xs
69 }
69 }
70}
70}
71
71
72instance Show a => Show (Maybe a) where {
72instance Show a => Show (Maybe a) where {
73− show Nothing = "Nothing";
73+ show Nothing = "Nothing"
74− show (Just x) = "Just " ++ show x;
74+ show (Just x) = "Just " ++ show x
75}
75}
76
76
77---- Monad and instances
77---- Monad and instances
78
78
79−infixl 5 >>= ;
79+infixl 5 >>=
80
80
81class Monad (m : Set -> Set) where {
81class Monad (m : Set -> Set) where {
82− return : a -> m a;
82+ return : a -> m a
83− (>>=) : m a -> (a -> m b) -> m b;
83+ (>>=) : m a -> (a -> m b) -> m b
84}
84}
85
85
86class Monad m => MonadPlus (m : Set -> Set) where {
86class Monad m => MonadPlus (m : Set -> Set) where {
87− mplus : m a -> m a -> m a;
87+ mplus : m a -> m a -> m a
88− mzero : m a;
88+ mzero : m a
89}
89}
90
90
91class Monad m => MonadFail (m : Set -> Set) where {
91class Monad m => MonadFail (m : Set -> Set) where {
92− fail : String -> m ();
92+ fail : String -> m ()
93}
93}
94
94
95instance Monad IO where {
95instance Monad IO where {
96− return t = io_return t;
96+ return t = io_return t
97− b >>= k = io_bind b k;
97+ b >>= k = io_bind b k
98}
98}
99
99
100instance Monad Maybe where {
100instance Monad Maybe where {
101− return = Just;
101+ return = Just
102
102
103− Nothing >>= k = Nothing;
103+ Nothing >>= k = Nothing
104− (Just x) >>= k = k x;
104+ (Just x) >>= k = k x
105}
105}
106
106
107instance MonadPlus Maybe where {
107instance MonadPlus Maybe where {
108− mzero = Nothing;
108+ mzero = Nothing
109
109
110− mplus (Just x) _ = Just x;
110+ mplus (Just x) _ = Just x
111− mplus Nothing (Just y) = Just y;
111+ mplus Nothing (Just y) = Just y
112− mplus Nothing Nothing = Nothing;
112+ mplus Nothing Nothing = Nothing
113}
113}
114
114
115instance Monad List where {
115instance Monad List where {
116− return x = [x];
116+ return x = [x]
117− m >>= f = concatMap f m;
117+ m >>= f = concatMap f m
118}
118}
119
119
120instance MonadPlus List where {
120instance MonadPlus List where {
121− mzero = [];
121+ mzero = []
122− mplus = app;
122+ mplus = app
123}
123}
124
124
125−guard : MonadPlus m => Bool -> m ();
125+guard : MonadPlus m => Bool -> m ()
126−guard True = return ();
126+guard True = return ()
127−guard False = mzero;
127+guard False = mzero
128
128
129---- Functors
129---- Functors
130
130
131class Functor (f : Set -> Set) where {
131class Functor (f : Set -> Set) where {
132− fmap : (a -> b) -> f a -> f b;
132+ fmap : (a -> b) -> f a -> f b
133}
133}
134
134
135instance Functor Maybe where {
135instance Functor Maybe where {
136− fmap f (Just x) = Just (f x);
136+ fmap f (Just x) = Just (f x)
137− fmap f Nothing = Nothing;
137+ fmap f Nothing = Nothing
138}
138}
139
139
140instance Functor List where {
140instance Functor List where {
141− fmap = map;
141+ fmap = map
142}
142}
143
143
144---- Applicative functors/Idioms
144---- Applicative functors/Idioms
145
145
146−infixl 2 <$>;
146+infixl 2 <$>
147
147
148class Functor f => Applicative (f : Set -> Set) where {
148class Functor f => Applicative (f : Set -> Set) where {
149− pure : a -> f a;
149+ pure : a -> f a
150− (<$>) : f (a -> b) -> f a -> f b;
150+ (<$>) : f (a -> b) -> f a -> f b
151}
151}
152
152
153---- some mathematical operations
153---- some mathematical operations
@@ -155,137 +155,140 @@ class Functor f => Applicative (f : Set -> Set) where {
155%include "math.h"
155%include "math.h"
156%lib "m"
156%lib "m"
157
157
158−exp : Float -> Float;
158+exp : Float -> Float
159−exp x = prim__floatExp x;
159+exp x = prim__floatExp x
160
160
161−log : Float -> Float;
161+log : Float -> Float
162−log x = prim__floatLog x;
162+log x = prim__floatLog x
163
163
164−pi : Float;
164+pi : Float
165−pi = 3.141592653589793;
165+pi = 3.141592653589793
166
166
167−sin : Float -> Float;
167+sin : Float -> Float
168−sin x = prim__floatSin x;
168+sin x = prim__floatSin x
169
169
170−cos : Float -> Float;
170+cos : Float -> Float
171−cos x = prim__floatCos x;
171+cos x = prim__floatCos x
172
172
173−tan : Float -> Float;
173+tan : Float -> Float
174−tan x = prim__floatTan x;
174+tan x = prim__floatTan x
175
175
176−asin : Float -> Float;
176+asin : Float -> Float
177−asin x = prim__floatASin x;
177+asin x = prim__floatASin x
178
178
179−acos : Float -> Float;
179+acos : Float -> Float
180−acos x = prim__floatACos x;
180+acos x = prim__floatACos x
181
181
182−atan : Float -> Float;
182+atan : Float -> Float
183−atan x = prim__floatATan x;
183+atan x = prim__floatATan x
184
184
185−sqrt : Float -> Float;
185+sqrt : Float -> Float
186−sqrt x = prim__floatSqrt x;
186+sqrt x = prim__floatSqrt x
187
187
188−floor : Float -> Float;
188+floor : Float -> Float
189−floor x = prim__floatFloor x;
189+floor x = prim__floatFloor x
190
190
191−ceiling : Float -> Float;
191+ceiling : Float -> Float
192−ceiling x = prim__floatCeil x;
192+ceiling x = prim__floatCeil x
193
193
194
194
195-- Ranges
195-- Ranges
196
196
197−count : Num a => a -> a -> a -> List a;
197+count : Num a => a -> a -> a -> List a
198count a inc b = if (a <= b) then (a :: count (a + inc) inc b)
198count a inc b = if (a <= b) then (a :: count (a + inc) inc b)
199− else [];
199+ else []
200
200
201syntax "[" [start] ".." [end] "]"
201syntax "[" [start] ".." [end] "]"
202− = count start 1 end;
202+ = count start 1 end
203syntax "[" [start] "," [next] ".." [end] "]"
203syntax "[" [start] "," [next] ".." [end] "]"
204− = count start (next - start) end;
204+ = count start (next - start) end
205
205
206---- some basic io
206---- some basic io
207
207
208−putStr : String -> IO ();
208+putStr : String -> IO ()
209−putStr x = mkForeign (FFun "putStr" [FString] FUnit) x;
209+putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
210
210
211−putStrLn : String -> IO ();
211+putStrLn : String -> IO ()
212−putStrLn x = putStr (x ++ "\n");
212+putStrLn x = putStr (x ++ "\n")
213
213
214−print : Show a => a -> IO ();
214+print : Show a => a -> IO ()
215−print x = putStrLn (show x);
215+print x = putStrLn (show x)
216
216
217−getLine : IO String;
217+getLine : IO String
218−getLine = mkForeign (FFun "readStr" Nil FString);
218+getLine = mkForeign (FFun "readStr" Nil FString)
219
219
220−putChar : Char -> IO ();
220+putChar : Char -> IO ()
221−putChar c = mkForeign (FFun "putchar" [FChar] FUnit) c;
221+putChar c = mkForeign (FFun "putchar" [FChar] FUnit) c
222
222
223−getChar : IO Char;
223+getChar : IO Char
224−getChar = mkForeign (FFun "getchar" [] FChar);
224+getChar = mkForeign (FFun "getchar" [] FChar)
225
225
226---- some basic file handling
226---- some basic file handling
227
227
228+abstract
228−abstract data File = FHandle Ptr;
229+data File = FHandle Ptr
229
230
230−do_fopen : String -> String -> IO Ptr;
231+do_fopen : String -> String -> IO Ptr
231−do_fopen f m = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m;
232+do_fopen f m = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
232
233
233−fopen : String -> String -> IO File;
234+fopen : String -> String -> IO File
234−fopen f m = do { h <- do_fopen f m;
235+fopen f m = do { h <- do_fopen f m
235− return (FHandle h); };
236+ return (FHandle h) }
236
237
237−data Mode = Read | Write | ReadWrite;
238+data Mode = Read | Write | ReadWrite
238
239
239−openFile : String -> Mode -> IO File;
240+openFile : String -> Mode -> IO File
240openFile f m = fopen f (modeStr m) where {
241openFile f m = fopen f (modeStr m) where {
241− modeStr : Mode -> String;
242+ modeStr : Mode -> String
242− modeStr Read = "r";
243+ modeStr Read = "r"
243− modeStr Write = "w";
244+ modeStr Write = "w"
244− modeStr ReadWrite = "r+";
245+ modeStr ReadWrite = "r+"
245}
246}
246
247
247−do_fclose : Ptr -> IO ();
248+do_fclose : Ptr -> IO ()
248−do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h;
249+do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h
249
250
250−closeFile : File -> IO ();
251+closeFile : File -> IO ()
251−closeFile (FHandle h) = do_fclose h;
252+closeFile (FHandle h) = do_fclose h
252
253
253−do_fread : Ptr -> IO String;
254+do_fread : Ptr -> IO String
254−do_fread h = mkForeign (FFun "freadStr" [FPtr] FString) h;
255+do_fread h = mkForeign (FFun "freadStr" [FPtr] FString) h
255
256
256−fread : File -> IO String;
257+fread : File -> IO String
257−fread (FHandle h) = do_fread h;
258+fread (FHandle h) = do_fread h
258
259
259−do_fwrite : Ptr -> String -> IO ();
260+do_fwrite : Ptr -> String -> IO ()
260−do_fwrite h s = mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s;
261+do_fwrite h s = mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s
261
262
262−fwrite : File -> String -> IO ();
263+fwrite : File -> String -> IO ()
263−fwrite (FHandle h) s = do_fwrite h s;
264+fwrite (FHandle h) s = do_fwrite h s
264
265
265−do_feof : Ptr -> IO Int;
266+do_feof : Ptr -> IO Int
266−do_feof h = mkForeign (FFun "feof" [FPtr] FInt) h;
267+do_feof h = mkForeign (FFun "feof" [FPtr] FInt) h
267
268
268−feof : File -> IO Bool;
269+feof : File -> IO Bool
269−feof (FHandle h) = do { eof <- do_feof h;
270+feof (FHandle h) = do { eof <- do_feof h
270− return (not (eof == 0)); };
271+ return (not (eof == 0)) }
271
272
272−while : |(test : IO Bool) -> |(body : IO ()) -> IO ();
273+while : |(test : IO Bool) -> |(body : IO ()) -> IO ()
273−while t b = do { v <- t;
274+while t b = do { v <- t
274− if v then (do { b; while t b; }) else return (); };
275+ if v then (do { b; while t b }) else return ()
276+ }
275
277
276−readFile : String -> IO String;
278+readFile : String -> IO String
277−readFile fn = do { h <- openFile fn Read;
279+readFile fn = do { h <- openFile fn Read
278− c <- readFile' h "";
280+ c <- readFile' h ""
279− closeFile h;
281+ closeFile h
280− return c;
282+ return c
281 }
283 }
282 where {
284 where {
283− readFile' : File -> String -> IO String;
285+ readFile' : File -> String -> IO String
284 readFile' h contents =
286 readFile' h contents =
285− do { x <- feof h;
287+ do { x <- feof h
286− if (not x) then (do { l <- fread h;
288+ if (not x) then (do { l <- fread h
287− readFile' h (contents ++ l);
289+ readFile' h (contents ++ l)
288 })
290 })
289− else (return contents); };
291+ else (return contents)
292+ }
290 }
293 }
291
294
lib/prelude/char.idr+18−18
@@ -1,34 +1,34 @@
1−module prelude.char;
1+module prelude.char
2
2
3−import builtins;
3+import builtins
4
4
5−isUpper : Char -> Bool;
5+isUpper : Char -> Bool
6−isUpper x = x >= 'A' && x <= 'Z';
6+isUpper x = x >= 'A' && x <= 'Z'
7
7
8−isLower : Char -> Bool;
8+isLower : Char -> Bool
9−isLower x = x >= 'a' && x <= 'z';
9+isLower x = x >= 'a' && x <= 'z'
10
10
11−isAlpha : Char -> Bool;
11+isAlpha : Char -> Bool
12−isAlpha x = isUpper x || isLower x;
12+isAlpha x = isUpper x || isLower x
13
13
14−isDigit : Char -> Bool;
14+isDigit : Char -> Bool
15−isDigit x = (x >= '0' && x <= '9');
15+isDigit x = (x >= '0' && x <= '9')
16
16
17−isAlphaNum : Char -> Bool;
17+isAlphaNum : Char -> Bool
18−isAlphaNum x = isDigit x || isAlpha x;
18+isAlphaNum x = isDigit x || isAlpha x
19
19
20−isSpace : Char -> Bool;
20+isSpace : Char -> Bool
21isSpace x = x == ' ' || x == '\t' || x == '\r' ||
21isSpace x = x == ' ' || x == '\t' || x == '\r' ||
22 x == '\n' || x == '\f' || x == '\v' ||
22 x == '\n' || x == '\f' || x == '\v' ||
23− x == '\xa0';
23+ x == '\xa0'
24
24
25−toUpper : Char -> Char;
25+toUpper : Char -> Char
26toUpper x = if (isLower x)
26toUpper x = if (isLower x)
27 then (prim__intToChar (prim__charToInt x - 32))
27 then (prim__intToChar (prim__charToInt x - 32))
28− else x;
28+ else x
29
29
30−toLower : Char -> Char;
30+toLower : Char -> Char
31toLower x = if (isUpper x)
31toLower x = if (isUpper x)
32 then (prim__intToChar (prim__charToInt x + 32))
32 then (prim__intToChar (prim__charToInt x + 32))
33− else x;
33+ else x
34
34
lib/prelude/either.idr+6−6
@@ -1,10 +1,10 @@
1−module prelude.either;
1+module prelude.either
2
2
3−import builtins;
3+import builtins
4
4
5−data Either a b = Left a | Right b;
5+data Either a b = Left a | Right b
6
6
7−choose : (b : Bool) -> Either (so b) (so (not b));
7+choose : (b : Bool) -> Either (so b) (so (not b))
8−choose True = Left oh;
8+choose True = Left oh
9−choose False = Right oh;
9+choose False = Right oh
10
10
lib/prelude/list.idr+62−62
@@ -1,102 +1,102 @@
1−module prelude.list;
1+module prelude.list
2
2
3−import prelude.maybe;
3+import prelude.maybe
4−import builtins;
4+import builtins
5
5
6%access public
6%access public
7
7
8−infixr 7 :: ;
8+infixr 7 ::
9
9
10−data List a = Nil | (::) a (List a);
10+data List a = Nil | (::) a (List a)
11
11
12−rev : List a -> List a;
12+rev : List a -> List a
13rev xs = revAcc [] xs where {
13rev xs = revAcc [] xs where {
14− revAcc : List a -> List a -> List a;
14+ revAcc : List a -> List a -> List a
15− revAcc acc [] = acc;
15+ revAcc acc [] = acc
16− revAcc acc (x :: xs) = revAcc (x :: acc) xs;
16+ revAcc acc (x :: xs) = revAcc (x :: acc) xs
17}
17}
18
18
19−app : List a -> List a -> List a;
19+app : List a -> List a -> List a
20−app [] xs = xs;
20+app [] xs = xs
21−app (x :: xs) ys = x :: app xs ys;
21+app (x :: xs) ys = x :: app xs ys
22
22
23−length : List a -> Int;
23+length : List a -> Int
24−length [] = 0;
24+length [] = 0
25−length (x :: xs) = 1 + length xs;
25+length (x :: xs) = 1 + length xs
26
26
27−take : Int -> List a -> List a;
27+take : Int -> List a -> List a
28−take 0 xs = [];
28+take 0 xs = []
29−take n [] = [];
29+take n [] = []
30−take n (x :: xs) = x :: take (n-1) xs;
30+take n (x :: xs) = x :: take (n-1) xs
31
31
32−drop : Int -> List a -> List a;
32+drop : Int -> List a -> List a
33−drop 0 xs = xs;
33+drop 0 xs = xs
34−drop n [] = [];
34+drop n [] = []
35−drop n (x :: xs) = drop (n-1) xs;
35+drop n (x :: xs) = drop (n-1) xs
36
36
37−map : (a -> b) -> List a -> List b;
37+map : (a -> b) -> List a -> List b
38−map f [] = [];
38+map f [] = []
39−map f (x :: xs) = f x :: map f xs;
39+map f (x :: xs) = f x :: map f xs
40
40
41−concatMap : (a -> List b) -> List a -> List b;
41+concatMap : (a -> List b) -> List a -> List b
42−concatMap f [] = [];
42+concatMap f [] = []
43−concatMap f (x :: xs) = app (f x) (concatMap f xs);
43+concatMap f (x :: xs) = app (f x) (concatMap f xs)
44
44
45−mapMaybe : (a -> Maybe b) -> List a -> List b;
45+mapMaybe : (a -> Maybe b) -> List a -> List b
46−mapMaybe f [] = [];
46+mapMaybe f [] = []
47mapMaybe f (x :: xs) = case f x of {
47mapMaybe f (x :: xs) = case f x of {
48 Nothing => mapMaybe f xs
48 Nothing => mapMaybe f xs
49 | Just v => v :: mapMaybe f xs
49 | Just v => v :: mapMaybe f xs
50− };
50+ }
51
51
52−filter : (y -> Bool) -> List y -> List y;
52+filter : (y -> Bool) -> List y -> List y
53−filter pred [] = [];
53+filter pred [] = []
54filter pred (x :: xs) = if (pred x) then (x :: filter pred xs)
54filter pred (x :: xs) = if (pred x) then (x :: filter pred xs)
55− else (filter pred xs);
55+ else (filter pred xs)
56
56
57−elem : Eq a => a -> List a -> Bool;
57+elem : Eq a => a -> List a -> Bool
58−elem x [] = False;
58+elem x [] = False
59−elem x (y :: ys) = if (x == y) then True else (elem x ys);
59+elem x (y :: ys) = if (x == y) then True else (elem x ys)
60
60
61−lookup : Eq k => k -> List (k, v) -> Maybe v;
61+lookup : Eq k => k -> List (k, v) -> Maybe v
62−lookup k [] = Nothing;
62+lookup k [] = Nothing
63−lookup k ((x, v) :: xs) = if (x == k) then (Just v) else (lookup k xs);
63+lookup k ((x, v) :: xs) = if (x == k) then (Just v) else (lookup k xs)
64
64
65−sort : Ord a => List a -> List a;
65+sort : Ord a => List a -> List a
66−sort [] = [];
66+sort [] = []
67−sort [x] = [x];
67+sort [x] = [x]
68sort xs = let (x, y) = split xs in
68sort xs = let (x, y) = split xs in
69 merge (sort x) (sort y) where {
69 merge (sort x) (sort y) where {
70− splitrec : List a -> List a -> (List a -> List a) -> (List a, List a);
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));
71+ splitrec (_ :: _ :: xs) (y :: ys) zs = splitrec xs ys (zs . ((::) y))
72− splitrec _ ys zs = (zs [], ys);
72+ splitrec _ ys zs = (zs [], ys)
73
73
74− split : List a -> (List a, List a);
74+ split : List a -> (List a, List a)
75− split xs = splitrec xs xs id;
75+ split xs = splitrec xs xs id
76
76
77− merge : Ord a => List a -> List a -> List a;
77+ merge : Ord a => List a -> List a -> List a
78− merge xs [] = xs;
78+ merge xs [] = xs
79− merge [] ys = ys;
79+ merge [] ys = ys
80 merge (x :: xs) (y :: ys) = if (x < y) then (x :: merge xs (y :: ys))
80 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)
82}
82}
83
83
84−span : (a -> Bool) -> List a -> (List a, List a);
84+span : (a -> Bool) -> List a -> (List a, List a)
85−span p [] = ([], []);
85+span p [] = ([], [])
86span p (x :: xs) with p x {
86span p (x :: xs) with p x {
87 | True with span p xs {
87 | True with span p xs {
88− | (ys, zs) = (x :: ys, zs);
88+ | (ys, zs) = (x :: ys, zs)
89 }
89 }
90− | False = ([], x :: xs);
90+ | False = ([], x :: xs)
91}
91}
92
92
93−break : (a -> Bool) -> List a -> (List a, List a);
93+break : (a -> Bool) -> List a -> (List a, List a)
94−break p = span (not . p);
94+break p = span (not . p)
95
95
96−split : (a -> Bool) -> List a -> List (List a);
96+split : (a -> Bool) -> List a -> List (List a)
97−split p [] = [];
97+split p [] = []
98split p xs = case break p xs of {
98split p xs = case break p xs of {
99 (chunk, []) => [chunk]
99 (chunk, []) => [chunk]
100 | (chunk, (c :: rest)) => chunk :: split p rest
100 | (chunk, (c :: rest)) => chunk :: split p rest
101− };
101+ }
102
102
lib/prelude/maybe.idr+8−8
@@ -1,12 +1,12 @@
1−module prelude.maybe;
1+module prelude.maybe
2
2
3−data Maybe a = Nothing | Just a;
3+data Maybe a = Nothing | Just a
4
4
5−maybe : |(def : b) -> (a -> b) -> Maybe a -> b;
5+maybe : |(def : b) -> (a -> b) -> Maybe a -> b
6−maybe n j Nothing = n;
6+maybe n j Nothing = n
7−maybe n j (Just x) = j x;
7+maybe n j (Just x) = j x
8
8
9−maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b;
9+maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b
10−maybe_bind Nothing k = Nothing;
10+maybe_bind Nothing k = Nothing
11−maybe_bind (Just x) k = k x;
11+maybe_bind (Just x) k = k x
12
12
lib/prelude/nat.idr+40−40
@@ -1,69 +1,69 @@
1−module prelude.nat;
1+module prelude.nat
2
2
3−import builtins;
3+import builtins
4
4
5%access public
5%access public
6
6
7−data Nat = O | S Nat;
7+data Nat = O | S Nat
8
8
9−plus : Nat -> Nat -> Nat;
9+plus : Nat -> Nat -> Nat
10−plus O y = y;
10+plus O y = y
11−plus (S k) y = S (plus k y);
11+plus (S k) y = S (plus k y)
12
12
13−eqRespS : m = n -> S m = S n;
13+eqRespS : m = n -> S m = S n
14−eqRespS refl = refl;
14+eqRespS refl = refl
15
15
16−eqRespS' : S m = S n -> m = n;
16+eqRespS' : S m = S n -> m = n
17−eqRespS' refl = refl;
17+eqRespS' refl = refl
18
18
19−sub : Nat -> Nat -> Nat;
19+sub : Nat -> Nat -> Nat
20−sub O y = O;
20+sub O y = O
21−sub (S k) (S y) = sub k y;
21+sub (S k) (S y) = sub k y
22−sub x O = x;
22+sub x O = x
23
23
24−mult : Nat -> Nat -> Nat;
24+mult : Nat -> Nat -> Nat
25−mult O y = O;
25+mult O y = O
26−mult (S k) y = plus y (mult k y);
26+mult (S k) y = plus y (mult k y)
27
27
28instance Eq Nat where {
28instance Eq Nat where {
29− O == O = True;
29+ O == O = True
30− (S x) == (S y) = x == y;
30+ (S x) == (S y) = x == y
31− O == (S y) = False;
31+ O == (S y) = False
32− (S x) == O = False;
32+ (S x) == O = False
33}
33}
34
34
35instance Ord Nat where {
35instance Ord Nat where {
36− compare O O = EQ;
36+ compare O O = EQ
37− compare O (S k) = LT;
37+ compare O (S k) = LT
38− compare (S k) O = GT;
38+ compare (S k) O = GT
39− compare (S x) (S y) = compare x y;
39+ compare (S x) (S y) = compare x y
40}
40}
41
41
42instance Num Nat where {
42instance Num Nat where {
43− (+) = plus;
43+ (+) = plus
44− (-) = sub;
44+ (-) = sub
45− (*) = mult;
45+ (*) = mult
46
46
47− fromInteger 0 = O;
47+ fromInteger 0 = O
48− fromInteger n = if (n > 0) then (S (fromInteger (n-1))) else O;
48+ fromInteger n = if (n > 0) then (S (fromInteger (n-1))) else O
49}
49}
50
50
51−plusnO : (m : Nat) -> m + O = m;
51+plusnO : (m : Nat) -> m + O = m
52−plusnO O = refl;
52+plusnO O = refl
53−plusnO (S k) = eqRespS (plusnO k);
53+plusnO (S k) = eqRespS (plusnO k)
54
54
55−plusn_Sm : (n : Nat) -> (m : Nat) -> (plus n (S m)) = S (plus n m);
55+plusn_Sm : (n : Nat) -> (m : Nat) -> (plus n (S m)) = S (plus n m)
56−plusn_Sm O m = refl;
56+plusn_Sm O m = refl
57−plusn_Sm (S j) m = eqRespS (plusn_Sm _ _);
57+plusn_Sm (S j) m = eqRespS (plusn_Sm _ _)
58
58
59−plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n;
59+plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
60−plus_commutes O m = sym (plusnO m);
60+plus_commutes O m = sym (plusnO m)
61−plus_commutes (S k) m = let ih = plus_commutes k m in ?plus_commutes_Sk;
61+plus_commutes (S k) m = let ih = plus_commutes k m in ?plus_commutes_Sk
62
62
63plus_commutes_Sk = proof {
63plus_commutes_Sk = proof {
64 intro k,m,ih;
64 intro k,m,ih;
65 refine sym;
65 refine sym;
66 rewrite (sym ih);
66 rewrite (sym ih);
67 refine plusn_Sm;
67 refine plusn_Sm;
68−};
68+}
69
69
lib/prelude/strings.idr+31−31
@@ -1,62 +1,62 @@
1−module prelude.strings;
1+module prelude.strings
2
2
3−import builtins;
3+import builtins
4−import prelude.list;
4+import prelude.list
5−import prelude.char;
5+import prelude.char
6
6
7-- Some more complex string operations
7-- Some more complex string operations
8
8
9data StrM : String -> Set where
9data StrM : String -> Set where
10 StrNil : StrM ""
10 StrNil : StrM ""
11− | StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs);
11+ | StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
12
12
13−strHead' : (x : String) -> so (not (x == "")) -> Char;
13+strHead' : (x : String) -> so (not (x == "")) -> Char
14−strHead' x p = prim__strHead x;
14+strHead' x p = prim__strHead x
15
15
16−strTail' : (x : String) -> so (not (x == "")) -> String;
16+strTail' : (x : String) -> so (not (x == "")) -> String
17−strTail' x p = prim__strTail x;
17+strTail' x p = prim__strTail x
18
18
19-- we need the 'believe_me' because the operations are primitives
19-- we need the 'believe_me' because the operations are primitives
20
20
21−strM : (x : String) -> StrM x;
21+strM : (x : String) -> StrM x
22strM x with choose (not (x == "")) {
22strM x with choose (not (x == "")) {
23− strM x | (Left p) = believe_me (StrCons (strHead' x p) (strTail' x p));
23+ strM x | (Left p) = believe_me (StrCons (strHead' x p) (strTail' x p))
24− strM x | (Right p) = believe_me StrNil;
24+ strM x | (Right p) = believe_me StrNil
25}
25}
26
26
27−unpack : String -> List Char;
27+unpack : String -> List Char
28unpack s with strM s {
28unpack s with strM s {
29− unpack "" | StrNil = [];
29+ unpack "" | StrNil = []
30− unpack (strCons x xs) | (StrCons _ _) = x :: unpack xs;
30+ unpack (strCons x xs) | (StrCons _ _) = x :: unpack xs
31}
31}
32
32
33−pack : List Char -> String;
33+pack : List Char -> String
34−pack [] = "";
34+pack [] = ""
35−pack (x :: xs) = strCons x (pack xs);
35+pack (x :: xs) = strCons x (pack xs)
36
36
37−span : (Char -> Bool) -> String -> (String, String);
37+span : (Char -> Bool) -> String -> (String, String)
38span p xs with strM xs {
38span p xs with strM xs {
39− span p "" | StrNil = ("", "");
39+ span p "" | StrNil = ("", "")
40 span p (strCons x xs) | (StrCons _ _) with p x {
40 span p (strCons x xs) | (StrCons _ _) with p x {
41 | True with span p xs {
41 | True with span p xs {
42− | (ys, zs) = (strCons x ys, zs);
42+ | (ys, zs) = (strCons x ys, zs)
43 }
43 }
44− | False = ("", strCons x xs);
44+ | False = ("", strCons x xs)
45 }
45 }
46}
46}
47
47
48−break : (Char -> Bool) -> String -> (String, String);
48+break : (Char -> Bool) -> String -> (String, String)
49−break p = span (not . p);
49+break p = span (not . p)
50
50
51−split : (Char -> Bool) -> String -> List String;
51+split : (Char -> Bool) -> String -> List String
52−split p xs = map pack (split p (unpack xs));
52+split p xs = map pack (split p (unpack xs))
53
53
54−ltrim : String -> String;
54+ltrim : String -> String
55ltrim xs with strM xs {
55ltrim xs with strM xs {
56− ltrim "" | StrNil = "";
56+ ltrim "" | StrNil = ""
57 ltrim (strCons x xs) | StrCons _ _
57 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)
59}
59}
60
60
61−trim : String -> String;
61+trim : String -> String
62−trim xs = ltrim (rev (ltrim (rev xs)));
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
2
2
3−import prelude.nat;
3+import prelude.nat
4
4
5%access public
5%access public
6
6
7data Fin : Nat -> Set where
7data Fin : Nat -> Set where
8 fO : Fin (S k)
8 fO : Fin (S k)
9− | fS : Fin k -> Fin (S k);
9+ | fS : Fin k -> Fin (S k)
10
10
11instance Eq (Fin n) where {
11instance Eq (Fin n) where {
12− fO == fO = True;
12+ fO == fO = True
13− (fS k) == (fS k') = k == k';
13+ (fS k) == (fS k') = k == k'
14− _ == _ = False;
14+ _ == _ = False
15}
15}
16
16
17−infixr 7 :: ;
17+infixr 7 ::
18
18
19data Vect : Set -> Nat -> Set where
19data Vect : Set -> Nat -> Set where
20 Nil : Vect a O
20 Nil : Vect a O
21− | (::) : a -> Vect a k -> Vect a (S k);
21+ | (::) : a -> Vect a k -> Vect a (S k)
22
22
23−lookup : Fin n -> Vect a n -> a;
23+lookup : Fin n -> Vect a n -> a
24−lookup fO (x :: xs) = x;
24+lookup fO (x :: xs) = x
25−lookup (fS k) (x :: xs) = lookup k xs;
25+lookup (fS k) (x :: xs) = lookup k xs
26−lookup fO [] impossible;
26+lookup fO [] impossible
27−lookup (fS _) [] impossible;
27+lookup (fS _) [] impossible
28
28
29−app : Vect a n -> Vect a m -> Vect a (n + m);
29+app : Vect a n -> Vect a m -> Vect a (n + m)
30−app [] ys = ys;
30+app [] ys = ys
31−app (x :: xs) ys = x :: app xs ys;
31+app (x :: xs) ys = x :: app xs ys
32
32
33−filter : (a -> Bool) -> Vect a n -> (p ** Vect a p);
33+filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
34−filter p [] = ( _ ** [] );
34+filter p [] = ( _ ** [] )
35filter p (x :: xs)
35filter p (x :: xs)
36 = let (_ ** xs') = filter p xs in
36 = 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
38
42
39−map : (a -> b) -> Vect a n -> Vect b n;
40−map f [] = [];
41−map f (x :: xs) = f x :: map f xs;
42
43
lib/system.idr+16−16
@@ -1,28 +1,28 @@
1−module system;
1+module system
2
2
3−import prelude;
3+import prelude
4
4
5%access public
5%access public
6
6
7−getArgs : IO (List String);
7+getArgs : IO (List String)
8−getArgs = do { n <- numArgs;
8+getArgs = do { n <- numArgs
9− ga' [] 0 n; }
9+ ga' [] 0 n }
10 where {
10 where {
11− numArgs : IO Int;
11+ numArgs : IO Int
12− numArgs = mkForeign (FFun "epic_numArgs" [] FInt);
12+ numArgs = mkForeign (FFun "epic_numArgs" [] FInt)
13
13
14− getArg : Int -> IO String;
14+ getArg : Int -> IO String
15− getArg x = mkForeign (FFun "epic_getArg" [FInt] FString) x;
15+ getArg x = mkForeign (FFun "epic_getArg" [FInt] FString) x
16
16
17− ga' : List String -> Int -> Int -> IO (List String);
17+ ga' : List String -> Int -> Int -> IO (List String)
18 ga' acc i n = if (i == n) then (return $ rev acc) else
18 ga' acc i n = if (i == n) then (return $ rev acc) else
19− do { arg <- getArg i;
19+ do { arg <- getArg i
20− ga' (arg :: acc) (i+1) n; };
20+ ga' (arg :: acc) (i+1) n }
21 }
21 }
22
22
23−getEnv : String -> IO String;
23+getEnv : String -> IO String
24−getEnv x = mkForeign (FFun "getenv" [FString] FString) x;
24+getEnv x = mkForeign (FFun "getenv" [FString] FString) x
25
25
26−exit : Int -> IO ();
26+exit : Int -> IO ()
27−exit code = mkForeign (FFun "exit" [FInt] FUnit) code;
27+exit code = mkForeign (FFun "exit" [FInt] FUnit) code
28
28
samples/interp.idr+44−45
@@ -1,25 +1,25 @@
1−module main;
1+module main
2
2
3−data Ty = TyInt | TyBool| TyFun Ty Ty;
3+data Ty = TyInt | TyBool| TyFun Ty Ty
4
4
5−interpTy : Ty -> Set;
5+interpTy : Ty -> Set
6−interpTy TyInt = Int;
6+interpTy TyInt = Int
7−interpTy TyBool = Bool;
7+interpTy TyBool = Bool
8−interpTy (TyFun s t) = interpTy s -> interpTy t;
8+interpTy (TyFun s t) = interpTy s -> interpTy t
9
9
10using (G : Vect Ty n) {
10using (G : Vect Ty n) {
11
11
12 data Env : Vect Ty n -> Set where
12 data Env : Vect Ty n -> Set where
13 Nil : Env Nil
13 Nil : Env Nil
14− | (::) : interpTy a -> Env G -> Env (a :: G);
14+ | (::) : interpTy a -> Env G -> Env (a :: G)
15
15
16 data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
16 data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
17 stop : HasType fO (t :: G) t
17 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
19
19
20− lookup : HasType i G t -> Env G -> interpTy t;
20+ lookup : HasType i G t -> Env G -> interpTy t
21− lookup stop (x :: xs) = x;
21+ lookup stop (x :: xs) = x
22− lookup (pop k) (x :: xs) = lookup k xs;
22+ lookup (pop k) (x :: xs) = lookup k xs
23
23
24 data Expr : Vect Ty n -> Ty -> Set where
24 data Expr : Vect Ty n -> Ty -> Set where
25 Var : HasType i G t -> Expr G t
25 Var : HasType i G t -> Expr G t
@@ -29,58 +29,57 @@ using (G : Vect Ty n) {
29 | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
29 | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
30 Expr G c
30 Expr G c
31 | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
31 | 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
33
33
34− interp : Env G -> {static} Expr G t -> interpTy t;
34+ interp : Env G -> {static} Expr G t -> interpTy t
35− interp env (Var i) = lookup i env;
35+ interp env (Var i) = lookup i env
36− interp env (Val x) = x;
36+ interp env (Val x) = x
37− interp env (Lam sc) = \x => interp (x :: env) sc;
37+ interp env (Lam sc) = \x => interp (x :: env) sc
38− interp env (App f s) = (interp env f) (interp env s);
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);
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);
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));
41+ interp env (Bind v f) = interp env (f (interp env v))
42
42
43− eId : Expr G (TyFun TyInt TyInt);
43+ eId : Expr G (TyFun TyInt TyInt)
44− eId = Lam (Var stop);
44+ eId = Lam (Var stop)
45
45
46− eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt));
46+ eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))
47− eTEST = Lam (Lam (Var (pop stop)));
47+ eTEST = Lam (Lam (Var (pop stop)))
48
48
49− eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));
49+ eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
50− eAdd = Lam (Lam (Op prim__addInt (Var stop) (Var (pop stop))));
50+ eAdd = Lam (Lam (Op prim__addInt (Var stop) (Var (pop stop))))
51
51
52−-- eDouble : Expr G (TyFun TyInt TyInt);
52+-- eDouble : Expr G (TyFun TyInt TyInt)
53−-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));
53+-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO))
54
54
55− eDouble : Expr G (TyFun TyInt TyInt);
55+ eDouble : Expr G (TyFun TyInt TyInt)
56− eDouble = Lam (App (App eAdd (Var stop)) (Var stop));
56+ eDouble = Lam (App (App eAdd (Var stop)) (Var stop))
57
57
58− app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;
58+ app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
59− app = \f, a => App f a;
59+ app = \f, a => App f a
60
60
61− eFac : Expr G (TyFun TyInt TyInt);
61+ eFac : Expr G (TyFun TyInt TyInt)
62 eFac = Lam (If (Op (==) (Var stop) (Val 0))
62 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)))
64
64
65 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
65 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
66
66
67− eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt));
67+ eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt))
68− eProg = Lam (Lam
69− (Bind (App eDouble (Var (pop stop)))
68+ eProg = Lam (Lam (Bind (App eDouble (Var (pop stop)))
70 (\x => Bind (App eDouble (Var stop))
69 (\x => Bind (App eDouble (Var stop))
71 (\y => Bind (App eDouble (Val x))
70 (\y => Bind (App eDouble (Val x))
72− (\z => App (App eAdd (Val y)) (Val z))))));
71+ (\z => App (App eAdd (Val y)) (Val z))))))
73
72
74}
73}
75
74
76−test : Int;
75+test : Int
77−test = interp [] eProg 2 2;
76+test = interp [] eProg 2 2
78
77
79−testFac : Int;
78+testFac : Int
80−testFac = interp [] eFac 4;
79+testFac = interp [] eFac 4
81
80
82−main : IO ();
81+main : IO ()
83−main = do { print testFac;
82+main = do { print testFac
84− print test; };
83+ print test }
85
84
86
85
src/Idris/AbsSyntax.hs+2−1
@@ -50,6 +50,7 @@ data IState = IState { tt_ctxt :: Context,
50 last_proof :: Maybe (Name, [String]),
50 last_proof :: Maybe (Name, [String]),
51 errLine :: Maybe Int,
51 errLine :: Maybe Int,
52 lastParse :: Maybe Name,
52 lastParse :: Maybe Name,
53+ indent_stack :: [Int],
53 hide_list :: [(Name, Maybe Accessibility)],
54 hide_list :: [(Name, Maybe Accessibility)],
54 default_access :: Accessibility,
55 default_access :: Accessibility,
55 ibc_write :: [IBCWrite]
56 ibc_write :: [IBCWrite]
@@ -72,7 +73,7 @@ data IBCWrite = IBCFix FixDecl
72
73
73idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
74idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
74 "" defaultOpts 6 [] [] [] [] [] [] [] []
75 "" defaultOpts 6 [] [] [] [] [] [] [] []
75− Nothing Nothing Nothing [] Hidden []
76+ Nothing Nothing Nothing [] [] Hidden []
76
77
77-- The monad for the main REPL - reading and processing files and updating
78-- The monad for the main REPL - reading and processing files and updating
78-- global state (hence the IO inner monad).
79-- global state (hence the IO inner monad).
src/Idris/Parser.hs+137−59
@@ -140,17 +140,54 @@ parseImports fname input
140 Right (x, i) -> do put i
140 Right (x, i) -> do put i
141 return x
141 return x
142 where ishow err = let ln = sourceLine (errorPos err) in
142 where ishow err = let ln = sourceLine (errorPos err) in
143− fname ++ ":" ++ show ln ++ ":parse error"
143+ fname ++ ":" ++ show ln ++ ":parse error"
144-- show (map messageString (errorMessages err))
144-- show (map messageString (errorMessages err))
145
145
146pHeader :: IParser [String]
146pHeader :: IParser [String]
147−pHeader = try (do reserved "module"; i <- identifier; lchar ';'
147+pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
148 return (parseName i))
148 return (parseName i))
149 <|> return []
149 <|> return []
150 where parseName x = case span (/='.') x of
150 where parseName x = case span (/='.') x of
151 (x, "") -> [x]
151 (x, "") -> [x]
152 (x, '.':y) -> x : parseName y
152 (x, '.':y) -> x : parseName y
153
153
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
154
191
155pfc :: IParser FC
192pfc :: IParser FC
156pfc = do s <- getPosition
193pfc = do s <- getPosition
@@ -163,7 +200,7 @@ pfc = do s <- getPosition
163pImport :: IParser String
200pImport :: IParser String
164pImport = do reserved "import"
201pImport = do reserved "import"
165 f <- identifier
202 f <- identifier
166− lchar ';'
203+ option ';' (lchar ';')
167 return (map dot f)
204 return (map dot f)
168 where dot '.' = '/'
205 where dot '.' = '/'
169 dot c = c
206 dot c = c
@@ -182,6 +219,7 @@ parseProg syn fname input pos
182 return (collect x)
219 return (collect x)
183 where ishow err = let ln = sourceLine (errorPos err) in
220 where ishow err = let ln = sourceLine (errorPos err) in
184 fname ++ ":" ++ show ln ++ ":parse error"
221 fname ++ ":" ++ show ln ++ ":parse error"
222+ ++ " " ++ show (sourceColumn (errorPos err))
185-- show (map messageString (errorMessages err))
223-- show (map messageString (errorMessages err))
186
224
187-- Collect PClauses with the same function name
225-- Collect PClauses with the same function name
@@ -244,7 +282,7 @@ pDecl' syn
244 = try pFixity
282 = try pFixity
245 <|> pFunDecl' syn
283 <|> pFunDecl' syn
246 <|> try (pData syn)
284 <|> try (pData syn)
247− <|> try (pSyntaxDecl syn)
285+ <|> pSyntaxDecl syn
248
286
249pSyntaxDecl :: SyntaxInfo -> IParser PDecl
287pSyntaxDecl :: SyntaxInfo -> IParser PDecl
250pSyntaxDecl syn
288pSyntaxDecl syn
@@ -267,7 +305,8 @@ pSyntaxDecl syn
267
305
268pSyntaxRule :: SyntaxInfo -> IParser Syntax
306pSyntaxRule :: SyntaxInfo -> IParser Syntax
269pSyntaxRule syn
307pSyntaxRule syn
308+ = do push_indent
270− = do sty <- option AnySyntax (do reserved "term"; return TermSyntax
309+ sty <- option AnySyntax (do reserved "term"; return TermSyntax
271 <|> do reserved "pattern"; return PatternSyntax)
310 <|> do reserved "pattern"; return PatternSyntax)
272 reserved "syntax"
311 reserved "syntax"
273 syms <- many1 pSynSym
312 syms <- many1 pSynSym
@@ -277,7 +316,7 @@ pSyntaxRule syn
277 $ fail "Repeated variable in syntax rule"
316 $ fail "Repeated variable in syntax rule"
278 lchar '='
317 lchar '='
279 tm <- pExpr syn
318 tm <- pExpr syn
280− lchar ';'
319+ pTerminator
281 return (Rule syms tm sty)
320 return (Rule syms tm sty)
282 where
321 where
283 expr (Expr _) = True
322 expr (Expr _) = True
@@ -294,12 +333,13 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'
294 return (Symbol sym)
333 return (Symbol sym)
295
334
296pFunDecl' :: SyntaxInfo -> IParser PDecl
335pFunDecl' :: SyntaxInfo -> IParser PDecl
336+pFunDecl' syn = try (do push_indent
297−pFunDecl' syn = try (do acc <- pAccessibility
337+ acc <- pAccessibility
298 n_in <- pfName
338 n_in <- pfName
299 let n = expandNS syn n_in
339 let n = expandNS syn n_in
300 ty <- pTSig syn
340 ty <- pTSig syn
301 fc <- pfc
341 fc <- pfc
302− lchar ';'
342+ pTerminator
303-- ty' <- implicit syn n ty
343-- ty' <- implicit syn n ty
304 addAcc n acc
344 addAcc n acc
305 return (PTy syn fc n ty))
345 return (PTy syn fc n ty))
@@ -348,8 +388,9 @@ expandNS syn n = case syn_namespace syn of
348--------- Fixity ---------
388--------- Fixity ---------
349
389
350pFixity :: IParser PDecl
390pFixity :: IParser PDecl
391+pFixity = do push_indent
351−pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
392+ f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
352− lchar ';'
393+ pTerminator
353 let prec = fromInteger i
394 let prec = fromInteger i
354 istate <- getState
395 istate <- getState
355 let fs = map (Fix (f prec)) ops
396 let fs = map (Fix (f prec)) ops
@@ -428,12 +469,12 @@ pSimpleExtExpr syn = do i <- getState
428
469
429pNoExtExpr syn =
470pNoExtExpr syn =
430 try (pApp syn)
471 try (pApp syn)
431− <|> try (pComprehension syn)
432− <|> pSimpleExpr syn
472+ <|> try (pSimpleExpr syn)
433 <|> pLambda syn
473 <|> pLambda syn
434 <|> pLet syn
474 <|> pLet syn
435 <|> pPi syn
475 <|> pPi syn
436 <|> pDoBlock syn
476 <|> pDoBlock syn
477+ <|> pComprehension syn
437
478
438pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
479pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
439pExtensions syn rules = choice (map (\x -> try (pExt syn x)) (filter valid rules))
480pExtensions syn rules = choice (map (\x -> try (pExt syn x)) (filter valid rules))
@@ -529,19 +570,10 @@ pSimpleExpr syn =
529 lchar '}'
570 lchar '}'
530 return (PCase fc scr opts)
571 return (PCase fc scr opts)
531 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
572 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
532− <|> try (pPair syn)
533 <|> try (pList syn)
573 <|> try (pList syn)
534 <|> try (pAlt syn)
574 <|> try (pAlt syn)
535 <|> try (pIdiom syn)
575 <|> try (pIdiom syn)
536− <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)
576+ <|> try (do lchar '('; bracketed syn)
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"))]))
545 <|> try (do c <- pConstant; fc <- pfc
577 <|> try (do c <- pConstant; fc <- pfc
546 return (modifyConst syn fc (PConstant c)))
578 return (modifyConst syn fc (PConstant c)))
547 <|> do reserved "Set"; return PSet
579 <|> do reserved "Set"; return PSet
@@ -550,6 +582,18 @@ pSimpleExpr syn =
550 <|> do lchar '_'; return Placeholder
582 <|> do lchar '_'; return Placeholder
551 <|> pSimpleExtExpr syn
583 <|> pSimpleExtExpr syn
552
584
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+
553pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
597pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
554pCaseOpt syn = do lhs <- pExpr syn; symbol "=>";
598pCaseOpt syn = do lhs <- pExpr syn; symbol "=>";
555 rhs <- pExpr syn
599 rhs <- pExpr syn
@@ -568,28 +612,37 @@ pList syn = do lchar '['; fc <- pfc
568 mkList fc [] = PRef fc (UN "Nil")
612 mkList fc [] = PRef fc (UN "Nil")
569 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
613 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
570
614
571−pPair syn = try (do lchar '('; l <- pExpr syn; op <- pairOp
615+pPair syn = try (do l <- pExpr syn
572 fc <- pfc
616 fc <- pfc
573− r <- pExpr syn; lchar ')';
617+ rest <- restTuple
618+ case rest of
619+ [] -> return l
620+ [Left r] -> return (PPair fc l r)
574− return (op fc l r))
621+ [Right r] -> return (PDPair fc l Placeholder r))
575− <|> try (do lchar '('; x <- ntuple
622+ <|> try (do x <- ntuple
576 lchar ')'
623 lchar ')'
577 return x)
624 return x)
578− <|> do lchar '('; ln <- pName; lchar ':'; lty <- pExpr syn;
625+ <|> do ln <- pName; lchar ':'; lty <- pExpr syn;
579 reservedOp "**";
626 reservedOp "**";
580 fc <- pfc
627 fc <- pfc
581 r <- pExpr syn; lchar ')';
628 r <- pExpr syn; lchar ')';
582 return (PDPair fc (PRef fc ln) lty r)
629 return (PDPair fc (PRef fc ln) lty r)
583 where
630 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]
584 ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
640 ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
585 rest <- ntuple
641 rest <- ntuple
586 return (PPair fc l rest))
642 return (PPair fc l rest))
587 <|> (do l <- pExpr syn; fc <- pfc; lchar ','
643 <|> (do l <- pExpr syn; fc <- pfc; lchar ','
588 r <- pExpr syn
644 r <- pExpr syn
589 return (PPair fc l r))
645 return (PPair fc l r))
590−
591− pairOp = do lchar ','; return PPair
592− <|> do reservedOp "**"; return (\f x y -> PDPair f x Placeholder y)
593
646
594pAlt syn = do symbol "(|";
647pAlt syn = do symbol "(|";
595 alts <- sepBy1 (pExpr' syn) (lchar ',')
648 alts <- sepBy1 (pExpr' syn) (lchar ',')
@@ -604,9 +657,19 @@ pHSimpleExpr syn
604
657
605pApp syn = do f <- pSimpleExpr syn
658pApp syn = do f <- pSimpleExpr syn
606 fc <- pfc
659 fc <- pfc
660+ args <- many1 (do notEndApp
607− args <- many1 (pArg syn)
661+ pArg syn)
608 return (PApp fc f args)
662 return (PApp fc f args)
609
663
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+
610pArg :: SyntaxInfo -> IParser PArg
673pArg :: SyntaxInfo -> IParser PArg
611pArg syn = try (pImplicitArg syn)
674pArg syn = try (pImplicitArg syn)
612 <|> try (pConstraintArg syn)
675 <|> try (pConstraintArg syn)
@@ -627,18 +690,17 @@ pTSig syn = do lchar ':'
627 sc <- pExpr syn
690 sc <- pExpr syn
628 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
691 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
629
692
630−pLambda syn = try (do lchar '\\';
693+pLambda syn = do lchar '\\'
631− xt <- tyOptDeclList syn
694+ (try (do xt <- tyOptDeclList syn
632− symbol "=>"
695+ symbol "=>"
633− sc <- pExpr syn
696+ sc <- pExpr syn
634− return (bindList PLam xt sc))
697+ return (bindList PLam xt sc))
635− <|> (do lchar '\\'
636− ps <- sepBy (do fc <- pfc
698+ <|> (do ps <- sepBy (do fc <- pfc
637− e <- pSimpleExpr syn
699+ e <- pSimpleExpr syn
638− return (fc, e)) (lchar ',')
700+ return (fc, e)) (lchar ',')
639− symbol "=>"
701+ symbol "=>"
640− sc <- pExpr syn
702+ sc <- pExpr syn
641− return (pmList (zip [0..] ps) sc))
703+ return (pmList (zip [0..] ps) sc)))
642 where pmList [] sc = sc
704 where pmList [] sc = sc
643 pmList ((i, (fc, x)) : xs) sc
705 pmList ((i, (fc, x)) : xs) sc
644 = PLam (MN i "lamp") Placeholder
706 = PLam (MN i "lamp") Placeholder
@@ -713,7 +775,9 @@ pComprehension syn
713
775
714pDoBlock syn
776pDoBlock syn
715 = do reserved "do"; lchar '{'
777 = 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
717 lchar '}'
781 lchar '}'
718 return (PDoBlock ds)
782 return (PDoBlock ds)
719
783
@@ -788,23 +852,25 @@ accData (Just Frozen) n ns = do addAcc n (Just Frozen)
788accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns
852accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns
789
853
790pData :: SyntaxInfo -> IParser PDecl
854pData :: SyntaxInfo -> IParser PDecl
855+pData syn = try (do push_indent
791−pData syn = try (do acc <- pAccessibility
856+ acc <- pAccessibility
792 reserved "data"; fc <- pfc
857 reserved "data"; fc <- pfc
793 tyn_in <- pfName; ty <- pTSig syn
858 tyn_in <- pfName; ty <- pTSig syn
794 let tyn = expandNS syn tyn_in
859 let tyn = expandNS syn tyn_in
795 reserved "where"
860 reserved "where"
796-- ty' <- implicit syn tyn ty
861-- ty' <- implicit syn tyn ty
797 cons <- sepBy (pConstructor syn) (lchar '|')
862 cons <- sepBy (pConstructor syn) (lchar '|')
798− lchar ';'
863+ pTerminator
799 accData acc tyn (map (\ (n, _, _) -> n) cons)
864 accData acc tyn (map (\ (n, _, _) -> n) cons)
800 return $ PData syn fc (PDatadecl tyn ty cons))
865 return $ PData syn fc (PDatadecl tyn ty cons))
866+ <|> do push_indent
801− <|> do acc <- pAccessibility
867+ acc <- pAccessibility
802 reserved "data"; fc <- pfc
868 reserved "data"; fc <- pfc
803 tyn_in <- pfName; args <- many pName
869 tyn_in <- pfName; args <- many pName
804 let tyn = expandNS syn tyn_in
870 let tyn = expandNS syn tyn_in
805 lchar '='
871 lchar '='
806 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
872 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
807− lchar ';'
873+ pTerminator
808 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
874 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
809 let ty = bindArgs (map (\a -> PSet) args) PSet
875 let ty = bindArgs (map (\a -> PSet) args) PSet
810-- ty' <- implicit syn tyn ty
876-- ty' <- implicit syn tyn ty
@@ -835,7 +901,8 @@ pSimpleCon syn
835 = do cn_in <- pfName
901 = do cn_in <- pfName
836 let cn = expandNS syn cn_in
902 let cn = expandNS syn cn_in
837 fc <- pfc
903 fc <- pfc
904+ args <- many (do notEndApp
838− args <- many (pSimpleExpr syn)
905+ pSimpleExpr syn)
839 return (cn, args, fc)
906 return (cn, args, fc)
840
907
841--------- Pattern match clauses ---------
908--------- Pattern match clauses ---------
@@ -859,7 +926,8 @@ pRHS syn n = do lchar '='; pExpr syn
859
926
860pClause :: SyntaxInfo -> IParser PClause
927pClause :: SyntaxInfo -> IParser PClause
861pClause syn
928pClause syn
929+ = try (do push_indent
862− = try (do n_in <- pfName; let n = expandNS syn n_in
930+ n_in <- pfName; let n = expandNS syn n_in
863 cargs <- many (pConstraintArg syn)
931 cargs <- many (pConstraintArg syn)
864 iargs <- many (pImplicitArg syn)
932 iargs <- many (pImplicitArg syn)
865 fc <- pfc
933 fc <- pfc
@@ -869,15 +937,18 @@ pClause syn
869 ist <- getState
937 ist <- getState
870 let ctxt = tt_ctxt ist
938 let ctxt = tt_ctxt ist
871 let wsyn = syn { syn_namespace = [] }
939 let wsyn = syn { syn_namespace = [] }
872− (wheres, nmap) <- choice [pWhereblock n wsyn,
940+ (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
873− do lchar ';'
941+ pop_indent
942+ return x,
943+ do pTerminator
874 return ([], [])]
944 return ([], [])]
875 let capp = PApp fc (PRef fc n)
945 let capp = PApp fc (PRef fc n)
876 (iargs ++ cargs ++ map pexp args)
946 (iargs ++ cargs ++ map pexp args)
877 ist <- getState
947 ist <- getState
878 setState (ist { lastParse = Just n })
948 setState (ist { lastParse = Just n })
879 return $ PClause n capp wargs rhs wheres)
949 return $ PClause n capp wargs rhs wheres)
950+ <|> try (do push_indent
880− <|> try (do wargs <- many1 (pWExpr syn)
951+ wargs <- many1 (pWExpr syn)
881 ist <- getState
952 ist <- getState
882 n <- case lastParse ist of
953 n <- case lastParse ist of
883 Just t -> return t
954 Just t -> return t
@@ -885,12 +956,15 @@ pClause syn
885 rhs <- pRHS syn n
956 rhs <- pRHS syn n
886 let ctxt = tt_ctxt ist
957 let ctxt = tt_ctxt ist
887 let wsyn = syn { syn_namespace = [] }
958 let wsyn = syn { syn_namespace = [] }
888− (wheres, nmap) <- choice [pWhereblock n wsyn,
959+ (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
889− do lchar ';'
960+ pop_indent
961+ return x,
962+ do pTerminator
890 return ([], [])]
963 return ([], [])]
891 return $ PClauseR wargs rhs wheres)
964 return $ PClauseR wargs rhs wheres)
892
965
966+ <|> try (do push_indent
893− <|> try (do n_in <- pfName; let n = expandNS syn n_in
967+ n_in <- pfName; let n = expandNS syn n_in
894 cargs <- many (pConstraintArg syn)
968 cargs <- many (pConstraintArg syn)
895 iargs <- many (pImplicitArg syn)
969 iargs <- many (pImplicitArg syn)
896 fc <- pfc
970 fc <- pfc
@@ -906,6 +980,7 @@ pClause syn
906 lchar '}'
980 lchar '}'
907 ist <- getState
981 ist <- getState
908 setState (ist { lastParse = Just n })
982 setState (ist { lastParse = Just n })
983+ pop_indent
909 return $ PWith n capp wargs wval withs)
984 return $ PWith n capp wargs wval withs)
910
985
911 <|> try (do wargs <- many1 (pWExpr syn)
986 <|> try (do wargs <- many1 (pWExpr syn)
@@ -917,7 +992,8 @@ pClause syn
917 lchar '}'
992 lchar '}'
918 return $ PWithR wargs wval withs)
993 return $ PWithR wargs wval withs)
919
994
995+ <|> do push_indent
920− <|> do l <- pArgExpr syn
996+ l <- pArgExpr syn
921 op <- operator
997 op <- operator
922 let n = expandNS syn (UN op)
998 let n = expandNS syn (UN op)
923 r <- pArgExpr syn
999 r <- pArgExpr syn
@@ -925,8 +1001,10 @@ pClause syn
925 wargs <- many (pWExpr syn)
1001 wargs <- many (pWExpr syn)
926 rhs <- pRHS syn n
1002 rhs <- pRHS syn n
927 let wsyn = syn { syn_namespace = [] }
1003 let wsyn = syn { syn_namespace = [] }
928− (wheres, nmap) <- choice [pWhereblock n wsyn,
1004+ (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
929− do lchar ';'
1005+ pop_indent
1006+ return x,
1007+ do pTerminator
930 return ([], [])]
1008 return ([], [])]
931 ist <- getState
1009 ist <- getState
932 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1010 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)
10
10
11data LineType = Prog | Blank | Comm
11data LineType = Prog | Blank | Comm
12
12
13−ulLine ('>':xs) = case span isSpace xs of
13+ulLine ('>':' ':xs) = (Prog, xs)
14− (_, p) -> (Prog, p)
14+ulLine ('>':xs) = (Prog, xs)
15ulLine xs | all isSpace xs = (Blank, "")
15ulLine xs | all isSpace xs = (Blank, "")
16 | otherwise = (Comm, '-':'-':xs)
16 | otherwise = (Comm, '-':'-':xs)
17
17
test/test001/test001.idr+43−43
@@ -1,25 +1,25 @@
1−module main;
1+module main
2
2
3−data Ty = TyInt | TyBool| TyFun Ty Ty;
3+data Ty = TyInt | TyBool| TyFun Ty Ty
4
4
5−interpTy : Ty -> Set;
5+interpTy : Ty -> Set
6−interpTy TyInt = Int;
6+interpTy TyInt = Int
7−interpTy TyBool = Bool;
7+interpTy TyBool = Bool
8−interpTy (TyFun s t) = interpTy s -> interpTy t;
8+interpTy (TyFun s t) = interpTy s -> interpTy t
9
9
10using (G : Vect Ty n) {
10using (G : Vect Ty n) {
11
11
12 data Env : Vect Ty n -> Set where
12 data Env : Vect Ty n -> Set where
13 Nil : Env Nil
13 Nil : Env Nil
14− | (::) : interpTy a -> Env G -> Env (a :: G);
14+ | (::) : interpTy a -> Env G -> Env (a :: G)
15
15
16 data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
16 data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
17 stop : HasType fO (t :: G) t
17 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
19
19
20− lookup : HasType i G t -> Env G -> interpTy t;
20+ lookup : HasType i G t -> Env G -> interpTy t
21− lookup stop (x :: xs) = x;
21+ lookup stop (x :: xs) = x
22− lookup (pop k) (x :: xs) = lookup k xs;
22+ lookup (pop k) (x :: xs) = lookup k xs
23
23
24 data Expr : Vect Ty n -> Ty -> Set where
24 data Expr : Vect Ty n -> Ty -> Set where
25 Var : HasType i G t -> Expr G t
25 Var : HasType i G t -> Expr G t
@@ -29,59 +29,59 @@ using (G : Vect Ty n) {
29 | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
29 | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
30 Expr G c
30 Expr G c
31 | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
31 | 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
33
33
34− interp : Env G -> {static} Expr G t -> interpTy t;
34+ interp : Env G -> {static} Expr G t -> interpTy t
35− interp env (Var i) = lookup i env;
35+ interp env (Var i) = lookup i env
36− interp env (Val x) = x;
36+ interp env (Val x) = x
37− interp env (Lam sc) = \x => interp (x :: env) sc;
37+ interp env (Lam sc) = \x => interp (x :: env) sc
38− interp env (App f s) = (interp env f) (interp env s);
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);
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);
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));
41+ interp env (Bind v f) = interp env (f (interp env v))
42
42
43− eId : Expr G (TyFun TyInt TyInt);
43+ eId : Expr G (TyFun TyInt TyInt)
44− eId = Lam (Var stop);
44+ eId = Lam (Var stop)
45
45
46− eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt));
46+ eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))
47− eTEST = Lam (Lam (Var (pop stop)));
47+ eTEST = Lam (Lam (Var (pop stop)))
48
48
49− eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));
49+ eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
50− eAdd = Lam (Lam (Op prim__addInt (Var stop) (Var (pop stop))));
50+ eAdd = Lam (Lam (Op prim__addInt (Var stop) (Var (pop stop))))
51
51
52−-- eDouble : Expr G (TyFun TyInt TyInt);
52+-- eDouble : Expr G (TyFun TyInt TyInt)
53−-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));
53+-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO))
54
54
55− eDouble : Expr G (TyFun TyInt TyInt);
55+ eDouble : Expr G (TyFun TyInt TyInt)
56− eDouble = Lam (App (App eAdd (Var stop)) (Var stop));
56+ eDouble = Lam (App (App eAdd (Var stop)) (Var stop))
57
57
58− app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;
58+ app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
59− app = \f, a => App f a;
59+ app = \f, a => App f a
60
60
61− eFac : Expr G (TyFun TyInt TyInt);
61+ eFac : Expr G (TyFun TyInt TyInt)
62 eFac = Lam (If (Op (==) (Var stop) (Val 0))
62 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)))
64
64
65 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
65 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
66
66
67− eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt));
67+ eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt))
68 eProg = Lam (Lam
68 eProg = Lam (Lam
69 (Bind (App eDouble (Var (pop stop)))
69 (Bind (App eDouble (Var (pop stop)))
70 (\x => Bind (App eDouble (Var stop))
70 (\x => Bind (App eDouble (Var stop))
71 (\y => Bind (App eDouble (Val x))
71 (\y => Bind (App eDouble (Val x))
72− (\z => App (App eAdd (Val y)) (Val z))))));
72+ (\z => App (App eAdd (Val y)) (Val z))))))
73
73
74}
74}
75
75
76−test : Int;
76+test : Int
77−test = interp [] eProg 2 2;
77+test = interp [] eProg 2 2
78
78
79−testFac : Int;
79+testFac : Int
80−testFac = interp [] eFac 4;
80+testFac = interp [] eFac 4
81
81
82−main : IO ();
82+main : IO ()
83−main = do { print testFac;
83+main = do { print testFac
84− print test; };
84+ print test }
85
85
86
86
87
87
test/test003/lit.lidr+12−12
@@ -1,19 +1,19 @@
1−> module lit;
1+> module lit
2
2
3Test some string primitives while we're at it
3Test some string primitives while we're at it
4
4
5−> st : String;
5+> st : String
6−> st = "abcdefg";
6+> st = "abcdefg"
7
7
8Literate main program
8Literate main program
9
9
10−> main : IO ();
10+> main : IO ()
11−> main = do { putStrLn (show (strHead st));
11+> main = do { putStrLn (show (strHead st))
12−> putStrLn (show (strIndex st 3));
12+> putStrLn (show (strIndex st 3))
13−> putStrLn (strCons 'z' st);
13+> putStrLn (strCons 'z' st)
14−> putStrLn (rev st);
14+> putStrLn (rev st)
15−> let x = unpack st;
15+> let x = unpack st
16−> putStrLn (show (rev x));
16+> putStrLn (show (rev x))
17−> putStrLn (pack x);
17+> putStrLn (pack x)
18−> };
18+> }
19
19