-
Notifications
You must be signed in to change notification settings - Fork 5
/
MiniParser.idr
185 lines (139 loc) · 4.43 KB
/
MiniParser.idr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
||| Primitive monadic (non-transformer) parser
module Util.MiniParser
import Data.Vect
%default total
%access public export
data Parser a = P (String -> Either String (a, String))
parse : Parser a -> String -> Either String (a, String)
parse (P f) str = f str
parseAll : Parser a -> String -> Either String a
parseAll p str = do
(xa, rst) <- parse p str
if rst == ""
then Right xa
else Left ("did not parse " ++ rst)
onechar : Parser Char
onechar = P (\inp => case strM inp of
StrNil => Left "Error! Parsing empty list."
StrCons x xs => Right (x, xs))
interface Parsable a where
item : Parser a
Parsable Char where
item = onechar
interface Parsable a => Composite b a where
compose : List a -> b
Composite String Char where
compose = pack
Functor Parser where
map f p = P (\inp => case parse p inp of
Left err => Left err
Right (v, rest) => Right ((f v), rest))
Applicative Parser where
pure v = P (\inp => Right (v, inp))
a <*> b = P (\inp => do (f, rest ) <- parse a inp
(x, rest') <- parse b rest
pure ((f x), rest'))
Monad Parser where
p >>= f = P (\inp => case parse p inp of
Left err => Left err
Right (v,rest) => parse (f v) rest)
||| choice of parsers
Alternative Parser where
empty = P (const (Left "empty"))
p <|> q = P (\inp => case parse p inp of
Left msg => parse q inp
Right (v,out) => Right (v,out))
fail : String -> Parser a
fail msg = P (\_ => Left msg)
infix 0 <?>
||| similar to parsec allows to specify failure message
(<?>) : Parser a -> String -> Parser a
(<?>) p s = p <|> fail s
-- basic char parsers
accept : Parsable a => (a -> Bool) -> Parser a
accept f = do
x <- item
if (f x)
then pure x
else empty
digit : Parser Char
digit = accept isDigit
lower : Parser Char
lower = accept isLower
upper : Parser Char
upper = accept isUpper
letter : Parser Char
letter = accept isAlpha
char : Char -> Parser Char
char c = accept (c ==)
charIngoreCase : Char -> Parser Char
charIngoreCase c = accept ((toUpper c) ==) <|> accept ((toLower c) ==)
string : String -> Parser String
string s = map pack (traverse char (unpack s))
stringIngoreCase : String -> Parser String
stringIngoreCase s = map pack (traverse charIngoreCase (unpack s))
-- combinators
oneof : (Parsable a, Eq a) => List a -> Parser a
oneof xs = accept (\x => elem x xs)
optional : Parser a -> Parser (Maybe a)
optional p = map Just p <|> pure Nothing
notFollowedBy : Parser a -> Parser ()
notFollowedBy p = do
a <- optional p
case a of
Nothing => pure ()
Just x => fail "not empty"
eof : Parser ()
eof = notFollowedBy onechar
||| apply p only if q is not applicable
unless : Parser a -> Parser a -> Parser a
unless q p = P (\inp => case parse q inp of
(Left _) => parse p inp
(Right _) => Left "unless failed"
)
exactly : (n : Nat) -> Parser a -> Parser (Vect n a)
exactly Z _ = pure Nil
exactly (S n) p = [| p :: exactly n p |]
covering
many : Parsable a => Parser a -> Parser (List a)
many p = do
(Just i) <- optional p
| Nothing => pure Nil
[| pure i :: many p |]
covering
many1 : Parsable a => Parser a -> Parser (List a)
many1 p = do
_ <- p
many p
covering
spaces : Parser (List Char)
spaces = many1 (char ' ')
covering
until : Parser a -> Parser a -> Parser (List a)
until to p = map reverse (untilrec to p Nil)
where
partial
untilrec : Parser a -> Parser a -> List a -> Parser (List a)
untilrec to p xa = do
i <- optional to
case i of
Just _ => pure xa
Nothing => do
a <- p
untilrec to p (a :: xa)
covering
between : (Parsable a, Composite b a) => Parser a -> Parser a -> Parser b
between from to = do
fx <- from
as <- until to item
pure (compose as)
covering
stringbetween : Parser Char -> Parser Char -> Parser String
stringbetween = between
-- primitive parsers
covering
decimalInt : Parser Int
decimalInt = many digit >>= pure . cast . pack
covering
decimalInteger : Parser Integer
decimalInteger = many digit >>= pure . cast . pack