@@ -3,7 +3,7 @@ module Text.Parser
33%default total
44
55-- TODO: Add some primitives for helping with error messages.
6−-- e.g. perhaps set a string to state what we're currently trying to
6+-- e.g. perhaps set a string to state what we're currently trying to
77-- parse, or to say what the next expected token is in words
88
99||| Description of a language's grammar. The `tok` parameter is the type
@@ -26,14 +26,14 @@ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
2626 Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
2727 Grammar tok (c1 || c2) b
2828 Alt : {c1, c2 : Bool} ->
29− Grammar tok c1 ty -> Grammar tok c2 ty ->
29+ Grammar tok c1 ty -> Grammar tok c2 ty ->
3030 Grammar tok (c1 && c2) ty
3131
3232public export
3333inf : Bool -> Type -> Type
3434inf True t = Inf t
3535inf False t = t
36−
36+
3737||| Sequence two grammars. If either consumes some input, the sequence is
3838||| guaranteed to consume some input. If the first one consumes input, the
3939||| second is allowed to be recursive (because it means some input has been
@@ -44,11 +44,11 @@ export %inline
4444 Grammar tok (c1 || c2) b
4545(>>=) {c1 = False} = SeqEmpty
4646(>>=) {c1 = True} = SeqEat
47−
47+
4848||| Give two alternative grammars. If both consume, the combination is
4949||| guaranteed to consume.
5050export
51−(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->
51+(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->
5252 Grammar tok (c1 && c2) ty
5353(<|>) = Alt
5454
@@ -82,21 +82,21 @@ export
8282eof : Grammar tok False ()
8383eof = EOF
8484
85−||| Commit to an alternative; if the current branch of an alternative
85+||| Commit to an alternative; if the current branch of an alternative
8686||| fails to parse, no more branches will be tried
8787export
8888commit : Grammar tok False ()
8989commit = Commit
9090
9191data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
92− Failure : {xs : List tok} ->
92+ Failure : {xs : List tok} ->
9393 (committed : Bool) ->
9494 (err : String) -> (rest : List tok) -> ParseResult xs c ty
9595 EmptyRes : (committed : Bool) ->
9696 (val : ty) -> (more : List tok) -> ParseResult more False ty
9797 NonEmptyRes : (committed : Bool) ->
9898 (val : ty) -> (more : List tok) ->
99− ParseResult (x :: xs ++ more) c ty
99+ ParseResult (x :: xs ++ more) c ty
100100
101101weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
102102 ParseResult xs c ty -> ParseResult xs (whatever && c) ty
@@ -105,13 +105,13 @@ weakenRes {whatever=True} (EmptyRes com val xs) = EmptyRes com val xs
105105weakenRes {whatever=False} (EmptyRes com val xs) = EmptyRes com val xs
106106weakenRes (NonEmptyRes com val more) = NonEmptyRes com val more
107107
108−shorter : (more : List tok) -> .(ys : List tok) ->
108+shorter : (more : List tok) -> .(ys : List tok) ->
109109 LTE (S (length more)) (S (length (ys ++ more)))
110110shorter more [] = lteRefl
111111shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))
112112
113113doParse : {c : Bool} ->
114− (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
114+ (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
115115 ParseResult xs c ty
116116doParse com xs act with (sizeAccessible xs)
117117 doParse com xs (Empty val) | sml = EmptyRes com val xs
@@ -120,17 +120,17 @@ doParse com xs act with (sizeAccessible xs)
120120 doParse com xs Commit | sml = EmptyRes True () xs
121121
122122 doParse com [] (Terminal f) | sml = Failure com "End of input" []
123− doParse com (x :: xs) (Terminal f) | sml
123+ doParse com (x :: xs) (Terminal f) | sml
124124 = maybe
125125 (Failure com "Unrecognised token" (x :: xs))
126126 (\a => NonEmptyRes com {xs=[]} a xs)
127127 (f x)
128128 doParse com [] EOF | sml = EmptyRes com () []
129− doParse com (x :: xs) EOF | sml
129+ doParse com (x :: xs) EOF | sml
130130 = Failure com "Expected end of input" (x :: xs)
131131 doParse com [] (NextIs f) | sml = Failure com "End of input" []
132− doParse com (x :: xs) (NextIs f) | sml
133− = if f x
132+ doParse com (x :: xs) (NextIs f) | sml
133+ = if f x
134134 then EmptyRes com x (x :: xs)
135135 else Failure com "Unrecognised token" (x :: xs)
136136 doParse com xs (Alt x y) | sml with (doParse False xs x | sml)
@@ -140,19 +140,19 @@ doParse com xs act with (sizeAccessible xs)
140140 then Failure com msg ts
141141 else weakenRes (doParse False xs y | sml)
142142 -- Successfully parsed the first option, so use the outer commit flag
143− doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
143+ doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
144144 = EmptyRes com val xs
145− doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)
145+ doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)
146146 = NonEmptyRes com val more
147147 doParse com xs (SeqEmpty act next) | (Access morerec)
148148 = case doParse com xs act | Access morerec of
149149 Failure com msg ts => Failure com msg ts
150− EmptyRes com val xs =>
150+ EmptyRes com val xs =>
151151 case doParse com xs (next val) | (Access morerec) of
152152 Failure com' msg ts => Failure com' msg ts
153153 EmptyRes com' val xs => EmptyRes com' val xs
154154 NonEmptyRes com' val more => NonEmptyRes com' val more
155− NonEmptyRes {x} {xs=ys} com val more =>
155+ NonEmptyRes {x} {xs=ys} com val more =>
156156 case (doParse com more (next val) | morerec _ (shorter more ys)) of
157157 Failure com' msg ts => Failure com' msg ts
158158 EmptyRes com' val _ => NonEmptyRes com' val more
@@ -160,13 +160,13 @@ doParse com xs act with (sizeAccessible xs)
160160 rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
161161 NonEmptyRes com' val more'
162162 doParse com xs (SeqEat act next) | sml with (doParse com xs act | sml)
163− doParse com xs (SeqEat act next) | sml | Failure com' msg ts
163+ doParse com xs (SeqEat act next) | sml | Failure com' msg ts
164164 = Failure com' msg ts
165− doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)
165+ doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)
166166 = case doParse com' more (next val) | morerec _ (shorter more ys) of
167167 Failure com' msg ts => Failure com' msg ts
168168 EmptyRes com' val _ => NonEmptyRes com' val more
169− NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
169+ NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
170170 rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
171171 NonEmptyRes com' val more'
172172 -- This next line is not strictly necessary, but it stops the coverage
@@ -180,7 +180,7 @@ data ParseError tok = Error String (List tok)
180180||| returns a pair of the parse result and the unparsed tokens (the remaining
181181||| input).
182182export
183−parse : (xs : List tok) -> (act : Grammar tok c ty) ->
183+parse : (xs : List tok) -> (act : Grammar tok c ty) ->
184184 Either (ParseError tok) (ty, List tok)
185185parse xs act
186186 = case doParse False xs act of
@@ -190,7 +190,7 @@ parse xs act
190190
191191||| Parse one or more things
192192export
193−some : Grammar tok True a ->
193+some : Grammar tok True a ->
194194 Grammar tok True (List a)
195195some p = do x <- p
196196 (do xs <- some p
@@ -198,14 +198,14 @@ some p = do x <- p
198198
199199||| Parse zero or more things (may match the empty input)
200200export
201−many : Grammar tok True a ->
201+many : Grammar tok True a ->
202202 Grammar tok False (List a)
203203many p = some p
204204 <|> pure []
205205
206206||| Parse one or more things, separated by another thing
207207export
208−sepBy1 : Grammar tok True () -> Grammar tok True a ->
208+sepBy1 : Grammar tok True () -> Grammar tok True a ->
209209 Grammar tok True (List a)
210210sepBy1 sep p = do x <- p
211211 (do sep
@@ -215,7 +215,7 @@ sepBy1 sep p = do x <- p
215215||| Parse zero or more things, separated by another thing. May
216216||| match the empty input.
217217export
218−sepBy : Grammar tok True () -> Grammar tok True a ->
218+sepBy : Grammar tok True () -> Grammar tok True a ->
219219 Grammar tok False (List a)
220220sepBy sep p = sepBy1 sep p <|> pure []
221221
@@ -227,3 +227,44 @@ optional : Grammar tok True a -> (ifNothing : a) ->
227227optional p def = p <|> pure def
228228
229229
230+||| Parse an instance of `p` that is between `left` and `right`.
231+export
232+between : (left : Grammar tok True ())
233+ -> (right : Grammar tok True ())
234+ -> (p : Grammar tok True a)
235+ -> Grammar tok True a
236+between left right contents = do
237+ left
238+ res <- contents
239+ right
240+ pure res
241+
242+||| Parse one or more instances of `p` separated by `s`, returning the
243+||| parsed items and proof the resulting list is non-empty.
244+export
245+sepBy1' : (sep : Grammar tok True ())
246+ -> (p : Grammar tok True a)
247+ -> Grammar tok True (xs : List a ** NonEmpty xs)
248+sepBy1' sep p
249+ = do x <- p
250+ (do sep
251+ xs <- sepBy1 sep p
252+ pure (x :: xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)
253+
254+||| Parse one or more instances of `p`, returning the parsed items and proof the resulting list is non-empty.
255+export
256+some' : (p : Grammar tok True a)
257+ -> Grammar tok True (xs : List a ** NonEmpty xs)
258+some' p = do
259+ x <- p
260+ (do xs <- some p
261+ pure (x::xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)
262+
263+
264+||| Optionally parse a thing. If the grammar provides a default use `optional` instead.
265+export
266+maybe : Grammar tok True a
267+ -> Grammar tok False (Maybe a)
268+maybe p =
269+ (do res <- p; pure $ Just res)
270+ <|> pure Nothing