@@ -1,5 +1,5 @@
11{-
2− Simple monadic parser module, based heavily on that by
2+ Simple monadic parser module, based heavily on that by
33 Graham Hutton.
44-}
55
@@ -13,47 +13,44 @@ import Builtins
1313
1414%access public
1515
16−infixr 5 |||
1716
1817{-
1918The monad of parsers
2019--------------------
2120-}
2221
23−data Parser a = P (String -> Either String (a, String))
22+data Parser a = P (String -> Either String (a, String))
2423
25−parse : Parser a -> String -> Either String (a, String)
26−parse (P p) inp = p inp
24+parse : Parser a -> String -> Either String (a, String)
25+parse (P p) inp = p inp
2726
28−instance Functor Parser where
29− -- fmap : (a -> b) -> f a -> f b
30− -- fmap : (a -> b) -> Parser a -> Parser b
31− -- Given a function (a -> b), and a parser a, make a parser b
32− fmap f p = P (\inp => case parse p inp of
33− (Left err) => Left err
34− -- Apply f to the v that we got from parsing
35− (Right (v, rest)) => Right ((f v), rest))
36−
27+instance Functor Parser where
28+ -- fmap : (a -> b) -> f a -> f b
29+ -- fmap : (a -> b) -> Parser a -> Parser b
30+ -- Given a function (a -> b), and a parser a, make a parser b
31+ fmap f p = P (\inp => case parse p inp of
32+ Left err => Left err
33+ -- Apply f to the v that we got from parsing
34+ Right (v, rest) => Right ((f v), rest))
3735
38−instance Applicative Parser where
39− pure v = P (\inp => Right (v, inp))
40− -- Parse to get the function, then parse to get the first argument
41− a <$> b = P (\inp => do (f, rest) <- parse a inp
42− (x, rest') <- parse b rest
43− pure ((f x), rest'))
36+instance Applicative Parser where
37+ pure v = P (\inp => Right (v, inp))
38+ -- Parse to get the function, then parse to get the first argument
39+ a <$> b = P (\inp => do (f, rest) <- parse a inp
40+ (x, rest') <- parse b rest
41+ pure ((f x), rest'))
4442
4543instance Monad Parser where
46−-- pure v = P (\inp => Right (v,inp))
47− -- m a -> (a -> m b) -> m b
48− p >>= f = P (\inp => case parse p inp of
49− (Left err) => Left err
50− (Right (v,rest)) => parse (f v) rest)
51−
52−--mplus : Monad m => m a -> m a -> m a
53−mplus : Parser a -> Parser a -> Parser a
54−mplus p q = P (\inp => case parse p inp of
55− Left msg => parse q inp
56− Right (v,out) => Right(v,out))
44+ -- m a -> (a -> m b) -> m b
45+ p >>= f = P (\inp => case parse p inp of
46+ Left err => Left err
47+ Right (v,rest) => parse (f v) rest)
48+
49+instance Alternative Parser where
50+ empty = P (const (Left "empty"))
51+ p <|> q = P (\inp => case parse p inp of
52+ Left msg => parse q inp
53+ Right (v,out) => Right (v,out))
5754
5855
5956{-
@@ -61,71 +58,55 @@ Basic parsers
6158-------------
6259-}
6360
64−failure : String -> Parser a
65−failure msg = P (\inp => Left msg)
66−
67−item : Parser Char
68−item = P (\inp => case unpack inp of
69− [] => Left "Error! Parsing empty list."
70− (x::xs) => Right (x, pack xs))
71−
72−
73−{-
74−Choice
75−--------
76−---}
61+failure : String -> Parser a
62+failure msg = P (\inp => Left msg)
7763
78−(|||) : Parser a -> Parser a -> Parser a
79−p ||| q = p `mplus` q
64+item : Parser Char
65+item = P (\inp => case unpack inp of
66+ [] => Left "Error! Parsing empty list."
67+ (x::xs) => Right (x, pack xs))
8068
8169
8270--{-
8371--Derived primitives
8472---}
8573
86−sat : (Char -> Bool) -> Parser Char
87−sat p = item >>= (\x => if p x then pure x else failure "failed")
88−
89−oneof : List Char -> Parser Char
90−oneof xs = sat (\x => elem x xs)
74+sat : (Char -> Bool) -> Parser Char
75+sat p = item >>= (\x => if p x then pure x else failure "failed")
9176
92−digit : Parser Char
93−digit = sat isDigit
77+oneof : List Char -> Parser Char
78+oneof xs = sat (\x => elem x xs)
9479
95−lower : Parser Char
96−lower = sat isLower
80+digit : Parser Char
81+digit = sat isDigit
9782
98−upper : Parser Char
99−upper = sat isUpper
83+lower : Parser Char
84+lower = sat isLower
10085
101−letter : Parser Char
102−letter = sat isAlpha
86+upper : Parser Char
87+upper = sat isUpper
10388
104−alphanum : Parser Char
105−alphanum = sat isAlphaNum
89+letter : Parser Char
90+letter = sat isAlpha
10691
107−char : Char -> Parser Char
108−char x = sat (== x)
92+alphanum : Parser Char
93+alphanum = sat isAlphaNum
10994
110−helper : List Char -> Parser (List Char)
111−string : String -> Parser String
112−string s = do result <- helper (unpack s)
113− pure (pack result)
114−
115−helper [] = pure Prelude.List.Nil
116−helper (x::xs) = do char x
117− string (cast xs)
118− pure (x :: xs)
95+char : Char -> Parser Char
96+char x = sat (== x)
11997
120−many : Parser a -> Parser (List a)
121−many1 : Parser a -> Parser (List a)
122−many1 p = do v <- p
123− vs <- many p
124− pure $ Prelude.List.(::) v vs
98+string : String -> Parser String
99+string s = [| pack (traverse char (unpack s)) |]
125100
101+many1 : Parser a -> Parser (List a)
102+many : Parser a -> Parser (List a)
103+
104+many1 p = [| p :: many p |]
105+
106+many p = many1 p <|> pure []
126107
127108bool : Parser Bool
128−bool = parseTrue ||| parseFalse
109+bool = parseTrue <|> parseFalse
129110 where parseTrue : Parser Bool
130111 parseTrue = do oneof ['T', 't']
131112 string "rue"
@@ -134,54 +115,44 @@ bool = parseTrue ||| parseFalse
134115 string "alse"
135116 pure False
136117
118+ident : Parser String
119+ident = fmap pack [| letter :: many1 alphanum |]
137120
121+nat : Parser Int
122+nat = do xs <- many digit
123+ pure (cast (cast xs))
138124
139−
140−many p = many1 p `mplus` pure Prelude.List.Nil
141−
142−
143−
144−ident : Parser String
145−ident = do x <- letter
146− xs <- many1 alphanum
147− pure (pack(x::xs))
148−
149−nat : Parser Int
150−nat = do xs <- many digit
151− pure (cast (cast xs))
152−
153−
154−int : Parser Int
155−int = neg ||| nat
125+int : Parser Int
126+int = neg <|> nat
156127 where neg : Parser Int
157128 neg = do char '-'
158129 n <- nat
159130 pure (-n)
160131
161−space : Parser ()
162−space = do many (sat isSpace)
163− pure ()
132+space : Parser ()
133+space = do many (sat isSpace)
134+ pure ()
164135--{-
165136--Ignoring spacing
166137---}
167138
168−token : Parser a -> Parser a
169−token p = do space
170− v <- p
171− space
172− pure v
139+token : Parser a -> Parser a
140+token p = do space
141+ v <- p
142+ space
143+ pure v
173144
174−identifier : Parser String
175−identifier = token ident
145+identifier : Parser String
146+identifier = token ident
176147
177−natural : Parser Int
178−natural = token nat
148+natural : Parser Int
149+natural = token nat
179150
180−integer : Parser Int
181−integer = token int
151+integer : Parser Int
152+integer = token int
182153
183−symbol : String -> Parser String
184−symbol xs = token (string xs)
154+symbol : String -> Parser String
155+symbol xs = token (string xs)
185156
186157strToken : Parser String
187158strToken = fmap pack (token (many1 alphanum))
@@ -193,31 +164,19 @@ strToken = fmap pack (token (many1 alphanum))
193164-- Expressions
194165---}
195166
196−factor : Parser Int
197−term : Parser Int
198−expr : Parser Int
199−expr = do t <- term
200− do symbol "+"
201− e <- expr
202− pure $ t + e
203− `mplus` pure t
204−
205−
206−factor = do symbol "("
207− do e <- expr
208− symbol ")"
209− pure e
210− `mplus` natural
211−
212−term = do f <- factor
213− do symbol "*"
214− t <- term
215− pure (f * t)
216− `mplus` pure f
217−
218−
219−
220−eval : String -> Maybe Int
221−eval xs = case (parse expr xs) of
222− Right (n,rest) => if rest == "" then Just n else Nothing
223− Left msg => Nothing
167+expr : Parser Int
168+factor : Parser Int
169+term : Parser Int
170+
171+expr = do t <- term
172+ fmap (t+) (symbol "+" $> expr) <|> pure t
173+
174+factor = (symbol "(" $> expr <$ symbol ")") <|> natural
175+
176+term = do f <- factor
177+ fmap (f*) (symbol "*" $> term) <|> pure f
178+
179+eval : String -> Maybe Int
180+eval xs = case (parse expr xs) of
181+ Right (n,rest) => if rest == "" then Just n else Nothing
182+ Left msg => Nothing