git.iko.soy/Idris-dev
on cdff1db help sign in
Idris-dev/contribs/lib/SimpleParser/SimpleParser.idr
190 lines 5.1 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 xs
114 where xs : Parser (List Char)
115 xs = [| letter :: many1 alphanum |]
117nat : Parser Int
118nat = do xs <- many digit
119 pure (cast (cast xs))
121int : Parser Int
122int = neg <|> nat
123 where neg : Parser Int
124 neg = do char '-'
125 n <- nat
126 pure (-n)
128space : Parser ()
129space = do many (sat isSpace)
130 pure ()
133--------------------------------------------------------------------------------
134-- Ignoring spacing
135--------------------------------------------------------------------------------
137token : Parser a -> Parser a
138token p = space $> p <$ space
140identifier : Parser String
141identifier = token ident
143natural : Parser Int
144natural = token nat
146integer : Parser Int
147integer = token int
149symbol : String -> Parser String
150symbol xs = token (string xs)
152strToken : Parser String
153strToken = map pack (token (many1 alphanum))
155--------------------------------------------------------------------------------
156-- combinators
157--------------------------------------------------------------------------------
159optional : Parser a -> Parser (Maybe a)
160optional p = map Just p <|> pure Nothing
162sepBy1 : Parser a -> Parser b -> Parser (List a)
163sepBy1 p s = [| p :: many (s $> p) |]
165sepBy : Parser a -> Parser b -> Parser (List a)
166sepBy p s = sepBy1 p s <|> pure Nil
168manyTil : Parser a -> Parser b -> Parser (List a)
169manyTil p e = (e $> pure Nil) <|> lazy [| p :: manyTil p e |] <|> pure Nil
171--------------------------------------------------------------------------------
172-- Expressions
173--------------------------------------------------------------------------------
175expr : Parser Int
176factor : Parser Int
177term : Parser Int
179expr = do t <- term
180 map (t+) (symbol "+" $> expr) <|> pure t
182factor = (symbol "(" $> expr <$ symbol ")") <|> natural
184term = do f <- factor
185 map (f*) (symbol "*" $> term) <|> pure f
187eval : String -> Maybe Int
188eval xs = case (parse expr xs) of
189 Right (n,rest) => if rest == "" then Just n else Nothing
190 Left msg => Nothing