git.iko.soy/Idris-dev
on aa42f71 help sign in
Idris-dev/contribs/lib/SimpleParser/SimpleParser.idr
173 lines 4.4 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 fmap 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 unpack inp of
58 [] => Left "Error! Parsing empty list."
59 (x::xs) => Right (x, pack xs))
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 = fmap pack (traverse char (unpack s))
95many1 : Parser a -> Parser (List a)
96many : Parser a -> Parser (List a)
98many1 p = [| p :: many p |]
100many p = 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 = fmap 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 = fmap pack (token (many1 alphanum))
154--------------------------------------------------------------------------------
155-- Expressions
156--------------------------------------------------------------------------------
158expr : Parser Int
159factor : Parser Int
160term : Parser Int
162expr = do t <- term
163 fmap (t+) (symbol "+" $> expr) <|> pure t
165factor = (symbol "(" $> expr <$ symbol ")") <|> natural
167term = do f <- factor
168 fmap (f*) (symbol "*" $> term) <|> pure f
170eval : String -> Maybe Int
171eval xs = case (parse expr xs) of
172 Right (n,rest) => if rest == "" then Just n else Nothing
173 Left msg => Nothing