git.iko.soy/Idris-dev
on master help sign in
Merge pull request #373 from SimonJF/simpleparser
c244c71Edwin Brady
contribs/lib/SimpleParser/SimpleParser.idrnew file+223
compare with master
unifiedsplit
@@ -0,0 +1,223 @@
1+{-
2+ Simple monadic parser module, based heavily on that by
3+ Graham Hutton.
4+-}
5+
6+module SimpleParser
7+
8+import Prelude
9+import Prelude.Monad
10+import Prelude.Applicative
11+import Prelude.List
12+import Builtins
13+
14+%access public
15+
16+infixr 5 |||
17+
18+{-
19+The monad of parsers
20+--------------------
21+-}
22+
23+data Parser a = P (String -> Either String (a, String))
24+
25+parse : Parser a -> String -> Either String (a, String)
26+parse (P p) inp = p inp
27+
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+
37+
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'))
44+
45+instance 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))
57+
58+
59+{-
60+Basic parsers
61+-------------
62+-}
63+
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+---}
77+
78+(|||) : Parser a -> Parser a -> Parser a
79+p ||| q = p `mplus` q
80+
81+
82+--{-
83+--Derived primitives
84+---}
85+
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)
91+
92+digit : Parser Char
93+digit = sat isDigit
94+
95+lower : Parser Char
96+lower = sat isLower
97+
98+upper : Parser Char
99+upper = sat isUpper
100+
101+letter : Parser Char
102+letter = sat isAlpha
103+
104+alphanum : Parser Char
105+alphanum = sat isAlphaNum
106+
107+char : Char -> Parser Char
108+char x = sat (== x)
109+
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)
119+
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
125+
126+
127+bool : Parser Bool
128+bool = parseTrue ||| parseFalse
129+ where parseTrue : Parser Bool
130+ parseTrue = do oneof ['T', 't']
131+ string "rue"
132+ pure True
133+ parseFalse = do oneof ['F', 'f']
134+ string "alse"
135+ pure False
136+
137+
138+
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
156+ where neg : Parser Int
157+ neg = do char '-'
158+ n <- nat
159+ pure (-n)
160+
161+space : Parser ()
162+space = do many (sat isSpace)
163+ pure ()
164+--{-
165+--Ignoring spacing
166+---}
167+
168+token : Parser a -> Parser a
169+token p = do space
170+ v <- p
171+ space
172+ pure v
173+
174+identifier : Parser String
175+identifier = token ident
176+
177+natural : Parser Int
178+natural = token nat
179+
180+integer : Parser Int
181+integer = token int
182+
183+symbol : String -> Parser String
184+symbol xs = token (string xs)
185+
186+strToken : Parser String
187+strToken = fmap pack (token (many1 alphanum))
188+
189+--apply : Parser a -> String -> List (a,String)
190+--apply p = parse (space >>= (\_ => p))
191+
192+--{-
193+-- 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
contribs/lib/simpleparser.idrdeleted−183
@@ -1,183 +0,0 @@
1−module Parsing
2−
3−import prelude
4−import builtins
5−
6−infixr 5 |||
7−
8−{-
9−The monad of parsers
10−--------------------
11−-}
12−
13−data Parser a = P (String -> Either String (a,String))
14−
15−parse : Parser a -> String ->Either String (a,String)
16−parse (P p) inp = p inp
17−
18−instance Monad Parser where
19− return v = P (\inp => Right (v,inp))
20− p >>= f = P (\inp => case parse p inp of
21− Left err => Left err
22− Right (v,rest) => parse (f v) rest)
23−
24−
25−instance MonadPlus Parser where
26− mzero = P (\inp => Left "Parse Error")
27− mplus p q = P (\inp => case parse p inp of
28− Left msg => parse q inp
29− Right (v,out) => Right(v,out))
30−
31−
32−{-
33−Basic parsers
34−-------------
35−-}
36−
37−failure : String -> Parser a
38−failure msg = P (\inp => Left msg)
39−
40−item : Parser Char
41−item = P (\inp => case unpack inp of
42− [] => Left "Error! Parsing empty list."
43− (x::xs) => Right (x, pack xs))
44−
45−
46−{-
47−Choice
48−--------
49−---}
50−
51−(|||) : Parser a -> Parser a -> Parser a
52−p ||| q = p `mplus` q
53−
54−
55−--{-
56−--Derived primitives
57−---}
58−
59−sat : (Char -> Bool) -> Parser Char
60−sat p = item >>= (\x => if p x then return x else failure "failed")
61−
62−oneof : List Char -> Parser Char
63−oneof xs = sat (\x => elem x xs)
64−
65−digit : Parser Char
66−digit = sat isDigit
67−
68−lower : Parser Char
69−lower = sat isLower
70−
71−upper : Parser Char
72−upper = sat isUpper
73−
74−letter : Parser Char
75−letter = sat isAlpha
76−
77−alphanum : Parser Char
78−alphanum = sat isAlphaNum
79−
80−char : Char -> Parser Char
81−char x = sat (== x)
82−
83−string : String -> Parser String
84−helper : List Char -> Parser (List Char)
85−string s = do result <- helper (unpack s)
86− return (pack result)
87−
88−helper [] = return []
89−helper (x::xs) = do char x
90− string (cast xs)
91− return (x :: xs)
92−
93−many1 : Parser a -> Parser (List a)
94−many : Parser a -> Parser (List a)
95−many1 p = do v <- p
96− vs <- many p
97− return (v::vs)
98−
99−
100−many p = many1 p `mplus` return []
101−
102−
103−
104−ident : Parser String
105−ident = do x <- letter
106− xs <- many1 alphanum
107− return (pack(x::xs))
108−
109−
110−nat : Parser Int
111−nat = do xs <- many digit
112− return (cast (cast xs))
113−
114−
115−int : Parser Int
116−int = do char '-'
117− n <- nat
118− return (-n)
119− `mplus` nat
120−
121−space : Parser ()
122−space = do many (sat isSpace)
123− return ()
124−--{-
125−--Ignoring spacing
126−---}
127−
128−token : Parser a -> Parser a
129−token p = do space
130− v <- p
131− space
132− return v
133−
134−identifier : Parser String
135−identifier = token ident
136−
137−natural : Parser Int
138−natural = token nat
139−
140−integer : Parser Int
141−integer = token int
142−
143−symbol : String -> Parser String
144−symbol xs = token (string xs)
145−
146−--apply : Parser a -> String -> List (a,String)
147−--apply p = parse (space >>= (\_ => p))
148−
149−--{-
150−-- Expressions
151−---}
152−
153−factor : Parser Int
154−term : Parser Int
155−expr : Parser Int
156−expr = do t <- term
157− do symbol "+"
158− e <- expr
159− Right (t+e)
160− ||| Right t
161−
162−
163−factor = do symbol "("
164− do e <- expr
165− symbol ")"
166− return e
167− ||| natural
168−
169−term = do f <- factor
170− do symbol "*"
171− t <- term
172− return (f * t)
173− ||| return f
174−
175−
176−
177−eval : String -> Maybe Int
178−eval xs = case (parse expr xs) of
179− Right (n,rest) => if rest == "" then Just n else Nothing
180− Left msg => Nothing
181−
182−
183−