git.iko.soy/Idris-dev
on d66da21 help sign in
Idris-dev/contribs/lib/SimpleParser/SimpleParser.idr
188 lines 5.0 kB history raw
1{-
2 Simple monadic parser module, based heavily on that by
3 Graham Hutton.
4-}
6module SimpleParser
8import Prelude
9import Prelude.Monad
10import Prelude.Applicative
11import Prelude.List
12import Builtins
14%access public
17--------------------------------------------------------------------------------
18-- The monad of parsers
19--------------------------------------------------------------------------------
21data Parser a = P (String -> Either String (a, String))
23parse : Parser a -> String -> Either String (a, String)
24parse (P p) inp = p inp
26instance Functor Parser where
27 map f p = P (\inp => case parse p inp of
28 Left err => Left err
29 Right (v, rest) => Right ((f v), rest))
31instance 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'))
37instance Monad Parser where
38 p >>= f = P (\inp => case parse p inp of
39 Left err => Left err
40 Right (v,rest) => parse (f v) rest)
42instance 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))
49--------------------------------------------------------------------------------
50-- Basic parsers
51--------------------------------------------------------------------------------
53failure : String -> Parser a
54failure msg = P (\inp => Left msg)
56item : Parser Char
57item = P (\inp => case choose (inp == "") of
58 Left _ => Left "Error! Parsing empty list."
59 Right p => Right (strHead' inp p, strTail' inp p))
62--------------------------------------------------------------------------------
63-- Derived primitives
64--------------------------------------------------------------------------------
66sat : (Char -> Bool) -> Parser Char
67sat p = do x <- item
68 guard (p x)
69 pure x
71oneof : List Char -> Parser Char
72oneof xs = sat (\x => elem x xs)
74digit : Parser Char
75digit = sat isDigit
77lower : Parser Char
78lower = sat isLower
80upper : Parser Char
81upper = sat isUpper
83letter : Parser Char
84letter = sat isAlpha
86alphanum : Parser Char
87alphanum = sat isAlphaNum
89char : Char -> Parser Char
90char x = sat (== x)
92string : String -> Parser String
93string s = map pack (traverse char (unpack s))
95mutual
96 many1 : Parser a -> Parser (List a)
97 many1 p = [| p :: many p |]
99 many : Parser a -> Parser (List a)
100 many p = lazy (many1 p) <|> pure []
102bool : Parser Bool
103bool = parseTrue <|> parseFalse
104 where parseTrue : Parser Bool
105 parseTrue = do oneof ['T', 't']
106 string "rue"
107 pure True
108 parseFalse = do oneof ['F', 'f']
109 string "alse"
110 pure False
112ident : Parser String
113ident = map pack [| letter :: many1 alphanum |]
115nat : Parser Int
116nat = do xs <- many digit
117 pure (cast (cast xs))
119int : Parser Int
120int = neg <|> nat
121 where neg : Parser Int
122 neg = do char '-'
123 n <- nat
124 pure (-n)
126space : Parser ()
127space = do many (sat isSpace)
128 pure ()
131--------------------------------------------------------------------------------
132-- Ignoring spacing
133--------------------------------------------------------------------------------
135token : Parser a -> Parser a
136token p = space $> p <$ space
138identifier : Parser String
139identifier = token ident
141natural : Parser Int
142natural = token nat
144integer : Parser Int
145integer = token int
147symbol : String -> Parser String
148symbol xs = token (string xs)
150strToken : Parser String
151strToken = map pack (token (many1 alphanum))
153--------------------------------------------------------------------------------
154-- combinators
155--------------------------------------------------------------------------------
157optional : Parser a -> Parser (Maybe a)
158optional p = map Just p <|> pure Nothing
160sepBy1 : Parser a -> Parser b -> Parser (List a)
161sepBy1 p s = [| p :: many (s $> p) |]
163sepBy : Parser a -> Parser b -> Parser (List a)
164sepBy p s = sepBy1 p s <|> pure Nil
166manyTil : Parser a -> Parser b -> Parser (List a)
167manyTil p e = (e $> pure Nil) <|> lazy [| p :: manyTil p e |] <|> pure Nil
169--------------------------------------------------------------------------------
170-- Expressions
171--------------------------------------------------------------------------------
173expr : Parser Int
174factor : Parser Int
175term : Parser Int
177expr = do t <- term
178 map (t+) (symbol "+" $> expr) <|> pure t
180factor = (symbol "(" $> expr <$ symbol ")") <|> natural
182term = do f <- factor
183 map (f*) (symbol "*" $> term) <|> pure f
185eval : String -> Maybe Int
186eval xs = case (parse expr xs) of
187 Right (n,rest) => if rest == "" then Just n else Nothing
188 Left msg => Nothing