@@ -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,119 +13,94 @@ import Builtins
1313
1414%access public
1515
16−infixr 5 |||
1716
18−{-
19−The monad of parsers
20−--------------------
21−-}
17+--------------------------------------------------------------------------------
18+-- The monad of parsers
19+--------------------------------------------------------------------------------
2220
23−data Parser a = P (String -> Either String (a, String))
21+data Parser a = P (String -> Either String (a, String))
2422
25−parse : Parser a -> String -> Either String (a, String)
26−parse (P p) inp = p inp
23+parse : Parser a -> String -> Either String (a, String)
24+parse (P p) inp = p inp
2725
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−
26+instance Functor Parser where
27+ fmap f p = P (\inp => case parse p inp of
28+ Left err => Left err
29+ Right (v, rest) => Right ((f v), rest))
3730
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'))
31+instance Applicative Parser where
32+ pure v = P (\inp => Right (v, inp))
33+ a <$> b = P (\inp => do (f, rest) <- parse a inp
34+ (x, rest') <- parse b rest
35+ pure ((f x), rest'))
4436
4537instance 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))
38+ p >>= f = P (\inp => case parse p inp of
39+ Left err => Left err
40+ Right (v,rest) => parse (f v) rest)
5741
42+instance Alternative Parser where
43+ empty = P (const (Left "empty"))
44+ p <|> q = P (\inp => case parse p inp of
45+ Left msg => parse q inp
46+ Right (v,out) => Right (v,out))
5847
59−{-
60−Basic parsers
61−-------------
62−-}
6348
64−failure : String -> Parser a
65−failure msg = P (\inp => Left msg)
49+--------------------------------------------------------------------------------
50+-- Basic parsers
51+--------------------------------------------------------------------------------
6652
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−
53+failure : String -> Parser a
54+failure msg = P (\inp => Left msg)
7255
73−{-
74−Choice
75−--------
76−---}
56+item : Parser Char
57+item = P (\inp => case unpack inp of
58+ [] => Left "Error! Parsing empty list."
59+ (x::xs) => Right (x, pack xs))
7760
78−(|||) : Parser a -> Parser a -> Parser a
79−p ||| q = p `mplus` q
8061
62+--------------------------------------------------------------------------------
63+-- Derived primitives
64+--------------------------------------------------------------------------------
8165
82−--{-
83−--Derived primitives
84−---}
66+sat : (Char -> Bool) -> Parser Char
67+sat p = do x <- item
68+ guard (p x)
69+ pure x
8570
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)
71+oneof : List Char -> Parser Char
72+oneof xs = sat (\x => elem x xs)
9173
92−digit : Parser Char
93−digit = sat isDigit
74+digit : Parser Char
75+digit = sat isDigit
9476
95−lower : Parser Char
96−lower = sat isLower
77+lower : Parser Char
78+lower = sat isLower
9779
98−upper : Parser Char
99−upper = sat isUpper
80+upper : Parser Char
81+upper = sat isUpper
10082
101−letter : Parser Char
102−letter = sat isAlpha
83+letter : Parser Char
84+letter = sat isAlpha
10385
104−alphanum : Parser Char
105−alphanum = sat isAlphaNum
86+alphanum : Parser Char
87+alphanum = sat isAlphaNum
10688
107−char : Char -> Parser Char
108−char x = sat (== x)
89+char : Char -> Parser Char
90+char x = sat (== x)
10991
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)
92+string : String -> Parser String
93+string s = fmap pack (traverse char (unpack s))
11994
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
95+many1 : Parser a -> Parser (List a)
96+many : Parser a -> Parser (List a)
12597
98+many1 p = [| p :: many p |]
99+
100+many p = many1 p <|> pure []
126101
127102bool : Parser Bool
128−bool = parseTrue ||| parseFalse
103+bool = parseTrue <|> parseFalse
129104 where parseTrue : Parser Bool
130105 parseTrue = do oneof ['T', 't']
131106 string "rue"
@@ -134,90 +109,65 @@ bool = parseTrue ||| parseFalse
134109 string "alse"
135110 pure False
136111
112+ident : Parser String
113+ident = fmap pack [| letter :: many1 alphanum |]
137114
115+nat : Parser Int
116+nat = do xs <- many digit
117+ pure (cast (cast xs))
138118
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
119+int : Parser Int
120+int = neg <|> nat
156121 where neg : Parser Int
157122 neg = do char '-'
158123 n <- nat
159124 pure (-n)
160125
161−space : Parser ()
162−space = do many (sat isSpace)
163− pure ()
164−--{-
165−--Ignoring spacing
166−---}
126+space : Parser ()
127+space = do many (sat isSpace)
128+ pure ()
129+
167130
168−token : Parser a -> Parser a
169−token p = do space
170− v <- p
171− space
172− pure v
131+--------------------------------------------------------------------------------
132+-- Ignoring spacing
133+--------------------------------------------------------------------------------
173134
174−identifier : Parser String
175−identifier = token ident
135+token : Parser a -> Parser a
136+token p = space $> p <$ space
176137
177−natural : Parser Int
178−natural = token nat
138+identifier : Parser String
139+identifier = token ident
179140
180−integer : Parser Int
181−integer = token int
141+natural : Parser Int
142+natural = token nat
182143
183−symbol : String -> Parser String
184−symbol xs = token (string xs)
144+integer : Parser Int
145+integer = token int
146+
147+symbol : String -> Parser String
148+symbol xs = token (string xs)
185149
186150strToken : Parser String
187151strToken = fmap pack (token (many1 alphanum))
188152
189−--apply : Parser a -> String -> List (a,String)
190−--apply p = parse (space >>= (\_ => p))
191153
192−--{-
154+--------------------------------------------------------------------------------
193155-- Expressions
194−---}
195−
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
156+--------------------------------------------------------------------------------
157+
158+expr : Parser Int
159+factor : Parser Int
160+term : Parser Int
161+
162+expr = do t <- term
163+ fmap (t+) (symbol "+" $> expr) <|> pure t
164+
165+factor = (symbol "(" $> expr <$ symbol ")") <|> natural
166+
167+term = do f <- factor
168+ fmap (f*) (symbol "*" $> term) <|> pure f
169+
170+eval : String -> Maybe Int
171+eval xs = case (parse expr xs) of
172+ Right (n,rest) => if rest == "" then Just n else Nothing
173+ Left msg => Nothing