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
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
|
-- https://github.com/ziman/lightyear/raw/master/Lightyear/Combinators.idr
-- --------------------------------------------------------- [ Combinators.idr ]
-- Module : Lightyear.Combinators
-- Description : Generic Combinators
--
-- This code is distributed under the BSD 2-clause license.
-- See the file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Lightyear.Combinators
import Data.Vect
import Lightyear.Core
%access export
-- --------------------------------------------------------------- [ Operators ]
infixr 3 :::
private
(:::) : a -> List a -> List a
(:::) x xs = x :: xs
infixr 3 ::.
private
(::.) : a -> Vect n a -> Vect (S n) a
(::.) x xs = x :: xs
-- -------------------------------------------------- [ Any Token and No Token ]
||| Parse a single arbitrary token. Returns the parsed token.
|||
||| This parser will fail if and only if the input stream is empty.
anyToken : (Monad m, Stream tok str) => ParserT str m tok
anyToken = satisfy (const True) <?> "any token"
||| Parse the end of input.
|||
||| This parser will succeed if and only if the input stream is empty.
eof : (Monad m, Stream tok str) => ParserT str m ()
eof = requireFailure anyToken <?> "end of input"
-- ---------------------------------------------------- [ Multiple Expressions ]
||| Run some parser as many times as possible, collecting a list of
||| successes.
many : Monad m => ParserT str m a -> ParserT str m (List a)
many p = (pure (:::) <*> p <*>| many p) <|> pure List.Nil
||| Run the specified parser precisely `n` times, returning a vector
||| of successes.
ntimes : Monad m => (n : Nat)
-> ParserT str m a
-> ParserT str m (Vect n a)
ntimes Z p = pure Vect.Nil
ntimes (S n) p = [| p ::. ntimes n p |]
||| Like `many`, but the parser must succeed at least once
some : Monad m => ParserT str m a -> ParserT str m (List a)
some p = [| p ::: many p |]
-- --------------------------------------------------- [ Separated Expressions ]
||| Parse repeated instances of at least one `p`, separated by `s`,
||| returning a list of successes.
|||
||| @ p the parser for items
||| @ s the parser for separators
sepBy1 : Monad m => (p : ParserT str m a)
-> (s : ParserT str m b)
-> ParserT str m (List a)
sepBy1 p s = [| p ::: many (s *> p) |]
||| Parse zero or more `p`s, separated by `s`s, returning a list of
||| successes.
|||
||| @ p the parser for items
||| @ s the parser for separators
sepBy : Monad m => (p : ParserT str m a)
-> (s : ParserT str m b)
-> ParserT str m (List a)
sepBy p s = (p `sepBy1` s) <|> pure List.Nil
||| Parse precisely `n` `p`s, separated by `s`s, returning a vect of
||| successes.
|||
||| @ n how many to parse
||| @ p the parser for items
||| @ s the parser for separators
sepByN : Monad m => (n : Nat)
-> (p : ParserT str m a)
-> (s : ParserT str m b)
-> ParserT str m (Vect n a)
sepByN Z p s = pure Vect.Nil
sepByN (S n) p s = [| p ::. ntimes n (s *> p) |]
||| Parse one or more `p`s, separated by `op`s. Return a value that is
||| the left associative application of the functions returned by `op`.
|||
||| @ p the parser
||| @ op the parser for operators
chainl1 : Monad m => (p : ParserT str m a)
-> (op: ParserT str m (a -> a -> a))
-> ParserT str m a
chainl1 p op = p >>= rest
where rest a1 = (do f <- op
a2 <- p
rest (f a1 a2)) <|> pure a1
||| Parse zero or more `p`s, separated by `op`s. Return a value that is
||| the left associative application of the functions returned by `op`.
||| Return `a` when there are zero occurences of `p`.
|||
||| @ p the parser
||| @ op the parser for operators
chainl : Monad m => (p : ParserT str m a)
-> (op : ParserT str m (a -> a -> a))
-> a
-> ParserT str m a
chainl p op a = (p `chainl1` op) <|> pure a
||| Parse one or more `p`s, separated by `op`s. Return a value that is
||| the right associative application of the functions returned by `op`.
|||
||| @ p the parser
||| @ op the parser for operators
chainr1 : Monad m => (p : ParserT str m a)
-> (op: ParserT str m (a -> a -> a))
-> ParserT str m a
chainr1 p op = p >>= rest
where rest a1 = (do f <- op
a2 <- p >>= rest
rest (f a1 a2)) <|> pure a1
||| Parse zero or more `p`s, separated by `op`s. Return a value that is
||| the right associative application of the functions returned by `op`.
||| Return `a` when there are zero occurences of `p`.
|||
||| @ p the parser
||| @ op the parser for operators
chainr : Monad m => (p : ParserT str m a)
-> (op : ParserT str m (a -> a -> a))
-> a
-> ParserT str m a
chainr p op a = (p `chainr1` op) <|> pure a
||| Alternate between matches of `p` and `s`, starting with `p`,
||| returning a list of successes from both.
alternating : Monad m => (p : ParserT str m a)
-> (s : ParserT str m a)
-> ParserT str m (List a)
alternating p s = (pure (:::) <*> p <*>| alternating s p) <|> pure List.Nil
||| Throw away the result from a parser
skip : Monad m => ParserT str m a -> ParserT str m ()
skip = map (const ())
||| Attempt to parse `p`. If it succeeds, then return the value. If it
||| fails, continue parsing.
opt : Monad m => (p : ParserT str m a) -> ParserT str m (Maybe a)
opt p = map Just p <|> pure Nothing
||| Parse open, then p, then close. Returns the result of `p`.
|||
||| @open The opening parser.
||| @close The closing parser.
||| @p The parser for the middle part.
between : Monad m => (open : ParserT str m a)
-> (close : ParserT str m a)
-> (p : ParserT str m b)
-> ParserT str m b
between open close p = open *> p <* close
-- The following names are inspired by the cut operator from Prolog
-- ---------------------------------------------------- [ Monad-like Operators ]
infixr 5 >!=
||| Committing bind
(>!=) : Monad m => ParserT str m a
-> (a -> ParserT str m b)
-> ParserT str m b
x >!= f = x >>= commitTo . f
infixr 5 >!
||| Committing sequencing
(>!) : Monad m => ParserT str m a
-> ParserT str m b
-> ParserT str m b
x >! y = x >>= \_ => commitTo y
-- ---------------------------------------------- [ Applicative-like Operators ]
infixl 2 <*!>
||| Committing application
(<*!>) : Monad m => ParserT str m (a -> b)
-> ParserT str m a
-> ParserT str m b
f <*!> x = f <*> commitTo x
infixl 2 <*!
(<*!) : Monad m => ParserT str m a
-> ParserT str m b
-> ParserT str m a
x <*! y = x <* commitTo y
infixl 2 *!>
(*!>) : Monad m => ParserT str m a
-> ParserT str m b
-> ParserT str m b
x *!> y = x *> commitTo y
-- ---------------------------------------------------------- [ Lazy Operators ]
infixl 2 <*|
(<*|) : Monad m => ParserT str m a
-> Lazy (ParserT str m b)
-> ParserT str m a
x <*| y = pure const <*> x <*>| y
infixl 2 *>|
(*>|) : Monad m => ParserT str m a
-> Lazy (ParserT str m b)
-> ParserT str m b
x *>| y = pure (const id) <*> x <*>| y
-- ---------------------------------------------------------------------- [ EF ]
|
