@@ -1,331 +1,216 @@
11module Text.Parser
22
3−%default total
4−
5−-- TODO: Add some primitives for helping with error messages.
6−-- e.g. perhaps set a string to state what we're currently trying to
7−-- parse, or to say what the next expected token is in words
8−
9−||| Description of a language's grammar. The `tok` parameter is the type
10−||| of tokens, and the `consumes` flag is True if the language is guaranteed
11−||| to be non-empty - that is, successfully parsing the language is guaranteed
12−||| to consume some input.
13−export
14−data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
15− Empty : (val : ty) -> Grammar tok False ty
16− Terminal : (tok -> Maybe a) -> Grammar tok True a
17− NextIs : (tok -> Bool) -> Grammar tok False tok
18− EOF : Grammar tok False ()
19−
20− Fail : String -> Grammar tok c ty
21− Commit : Grammar tok False ()
22−
23− SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->
24− Grammar tok True b
25− SeqEmpty : {c1, c2 : Bool} ->
26− Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
27− Grammar tok (c1 || c2) b
28− Alt : {c1, c2 : Bool} ->
29− Grammar tok c1 ty -> Grammar tok c2 ty ->
30− Grammar tok (c1 && c2) ty
31−
32−public export
33−inf : Bool -> Type -> Type
34−inf True t = Inf t
35−inf False t = t
36−
37−||| Sequence two grammars. If either consumes some input, the sequence is
38−||| guaranteed to consume some input. If the first one consumes input, the
39−||| second is allowed to be recursive (because it means some input has been
40−||| consumed and therefore the input is smaller)
41−export %inline
42−(>>=) : {c1 : Bool} ->
43− Grammar tok c1 a ->
44− inf c1 (a -> Grammar tok c2 b) ->
45− Grammar tok (c1 || c2) b
46−(>>=) {c1 = False} = SeqEmpty
47−(>>=) {c1 = True} = SeqEat
48−
49−||| Sequence a grammar followed by the grammar it returns.
50−export
51−join : {c1 : Bool} ->
52− Grammar tok c1 (Grammar tok c2 a) ->
53− Grammar tok (c1 || c2) a
54−join {c1 = False} p = SeqEmpty p id
55−join {c1 = True} p = SeqEat p id
56−
57−||| Give two alternative grammars. If both consume, the combination is
58−||| guaranteed to consume.
59−export
60−(<|>) : Grammar tok c1 ty ->
61− Grammar tok c2 ty ->
62− Grammar tok (c1 && c2) ty
63−(<|>) = Alt
64−
65−||| Allows the result of a grammar to be mapped to a different value.
66−export
67−Functor (Grammar tok c) where
68− map f (Empty val) = Empty (f val)
69− map f (Fail msg) = Fail msg
70− map f (Terminal g) = Terminal (\t => map f (g t))
71− map f (Alt x y) = Alt (map f x) (map f y)
72− map f (SeqEat act next)
73− = SeqEat act (\val => map f (next val))
74− map f (SeqEmpty act next)
75− = SeqEmpty act (\val => map f (next val))
76− -- The remaining constructors (NextIs, EOF, Commit) have a fixed type,
77− -- so a sequence must be used.
78− map {c = False} f p = SeqEmpty p (Empty . f)
79−
80−||| Sequence a grammar with value type `a -> b` and a grammar
81−||| with value type `a`. If both succeed, apply the function
82−||| from the first grammar to the value from the second grammar.
83−||| Guaranteed to consume if either grammar consumes.
84−export
85−(<*>) : {c1 : Bool} ->
86− Grammar tok c1 (a -> b) ->
87− inf c1 (Grammar tok c2 a) ->
88− Grammar tok (c1 || c2) b
89−(<*>) {c1 = False} x y = SeqEmpty x (\f => map f y)
90−(<*>) {c1 = True} x y = SeqEat x (\f => map f y)
91−
92−||| Sequence two grammars. If both succeed, use the value of the first one.
93−||| Guaranteed to consume if either grammar consumes.
94−export
95−(<*) : Grammar tok c1 a ->
96− inf c1 (Grammar tok c2 b) ->
97− Grammar tok (c1 || c2) a
98−(<*) x y = map const x <*> y
99−
100−||| Sequence two grammars. If both succeed, use the value of the second one.
101−||| Guaranteed to consume if either grammar consumes.
102−export
103−(*>) : Grammar tok c1 a ->
104− inf c1 (Grammar tok c2 b) ->
105− Grammar tok (c1 || c2) b
106−(*>) x y = map (const id) x <*> y
107−
108−||| Always succeed with the given value.
109−export
110−pure : (val : ty) -> Grammar tok False ty
111−pure = Empty
112−
113−||| Check whether the next token satisfies a predicate
114−export
115−nextIs : (tok -> Bool) -> Grammar tok False tok
116−nextIs = NextIs
117−
118−||| Look at the next token in the input
119−export
120−peek : Grammar tok False tok
121−peek = nextIs (const True)
122−
123−||| Succeeds if running the predicate on the next token returns Just x,
124−||| returning x. Otherwise fails.
125−export
126−terminal : (tok -> Maybe a) -> Grammar tok True a
127−terminal = Terminal
128−
129−||| Always fail with a message
130−export
131−fail : String -> Grammar tok c ty
132−fail = Fail
133−
134−||| Succeed if the input is empty
135−export
136−eof : Grammar tok False ()
137−eof = EOF
138−
139−||| Commit to an alternative; if the current branch of an alternative
140−||| fails to parse, no more branches will be tried
141−export
142−commit : Grammar tok False ()
143−commit = Commit
3+import Data.Bool.Extra
1444
145−data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
146− Failure : {xs : List tok} ->
147− (committed : Bool) ->
148− (err : String) -> (rest : List tok) -> ParseResult xs c ty
149− EmptyRes : (committed : Bool) ->
150− (val : ty) -> (more : List tok) -> ParseResult more False ty
151− NonEmptyRes : (committed : Bool) ->
152− (val : ty) -> (more : List tok) ->
153− ParseResult (x :: xs ++ more) c ty
5+import public Text.Parser.Core
6+import public Text.Quantity
1547
155−-- Take the result of an alternative branch, reset the commit flag to
156−-- the commit flag from the outer alternative, and weaken the 'consumes'
157−-- flag to take both alternatives into account
158−weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
159− (com' : Bool) ->
160− ParseResult xs c ty -> ParseResult xs (whatever && c) ty
161−weakenRes com' (Failure com msg ts) = Failure com' msg ts
162−weakenRes {whatever=True} com' (EmptyRes com val xs) = EmptyRes com' val xs
163−weakenRes {whatever=False} com' (EmptyRes com val xs) = EmptyRes com' val xs
164−weakenRes com' (NonEmptyRes com val more) = NonEmptyRes com' val more
165−
166−shorter : (more : List tok) -> .(ys : List tok) ->
167− LTE (S (length more)) (S (length (ys ++ more)))
168−shorter more [] = lteRefl
169−shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))
170−
171−doParse : {c : Bool} ->
172− (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
173− ParseResult xs c ty
174−doParse com xs act with (sizeAccessible xs)
175− doParse com xs (Empty val) | sml = EmptyRes com val xs
176− doParse com [] (Fail str) | sml = Failure com str []
177− doParse com (x :: xs) (Fail str) | sml = Failure com str (x :: xs)
178− doParse com xs Commit | sml = EmptyRes True () xs
179−
180− doParse com [] (Terminal f) | sml = Failure com "End of input" []
181− doParse com (x :: xs) (Terminal f) | sml
182− = maybe
183− (Failure com "Unrecognised token" (x :: xs))
184− (\a => NonEmptyRes com {xs=[]} a xs)
185− (f x)
186− doParse com [] EOF | sml = EmptyRes com () []
187− doParse com (x :: xs) EOF | sml
188− = Failure com "Expected end of input" (x :: xs)
189− doParse com [] (NextIs f) | sml = Failure com "End of input" []
190− doParse com (x :: xs) (NextIs f) | sml
191− = if f x
192− then EmptyRes com x (x :: xs)
193− else Failure com "Unrecognised token" (x :: xs)
194− doParse com xs (Alt x y) | sml with (doParse False xs x | sml)
195− doParse com xs (Alt x y) | sml | Failure com' msg ts
196− = if com' -- If the alternative had committed, don't try the
197− -- other branch (and reset commit flag)
198− then Failure com msg ts
199− else weakenRes com (doParse False xs y | sml)
200− -- Successfully parsed the first option, so use the outer commit flag
201− doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
202− = EmptyRes com val xs
203− doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)
204− = NonEmptyRes com val more
205− doParse com xs (SeqEmpty act next) | (Access morerec)
206− = case doParse com xs act | Access morerec of
207− Failure com msg ts => Failure com msg ts
208− EmptyRes com val xs =>
209− case doParse com xs (next val) | (Access morerec) of
210− Failure com' msg ts => Failure com' msg ts
211− EmptyRes com' val xs => EmptyRes com' val xs
212− NonEmptyRes com' val more => NonEmptyRes com' val more
213− NonEmptyRes {x} {xs=ys} com val more =>
214− case (doParse com more (next val) | morerec _ (shorter more ys)) of
215− Failure com' msg ts => Failure com' msg ts
216− EmptyRes com' val _ => NonEmptyRes com' val more
217− NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
218− rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
219− NonEmptyRes com' val more'
220− doParse com xs (SeqEat act next) | sml with (doParse com xs act | sml)
221− doParse com xs (SeqEat act next) | sml | Failure com' msg ts
222− = Failure com' msg ts
223− doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)
224− = case doParse com' more (next val) | morerec _ (shorter more ys) of
225− Failure com' msg ts => Failure com' msg ts
226− EmptyRes com' val _ => NonEmptyRes com' val more
227− NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
228− rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
229− NonEmptyRes com' val more'
230− -- This next line is not strictly necessary, but it stops the coverage
231− -- checker taking a really long time and eating lots of memory...
232− doParse _ _ _ | sml = Failure True "Help the coverage checker!" []
233−
234−public export
235−data ParseError tok = Error String (List tok)
236−
237−||| Parse a list of tokens according to the given grammar. If successful,
238−||| returns a pair of the parse result and the unparsed tokens (the remaining
239−||| input).
240−export
241−parse : (xs : List tok) -> (act : Grammar tok c ty) ->
242− Either (ParseError tok) (ty, List tok)
243−parse xs act
244− = case doParse False xs act of
245− Failure _ msg ts => Left (Error msg ts)
246− EmptyRes _ val rest => pure (val, rest)
247− NonEmptyRes _ val rest => pure (val, rest)
248−
249−||| Parse one or more things
250−export
251−some : Grammar tok True a ->
252− Grammar tok True (List a)
253−some p = do x <- p
254− (do xs <- some p
255− pure (x :: xs)) <|> pure [x]
256−
257−||| Parse zero or more things (may match the empty input)
258−export
259−many : Grammar tok True a ->
260− Grammar tok False (List a)
261−many p = some p
262− <|> pure []
8+%access export
9+%default total
26310
264−||| Parse one or more things, separated by another thing
265−export
266−sepBy1 : Grammar tok True () -> Grammar tok True a ->
11+||| Optionally parse a thing, with a default value if the grammar doesn't
12+||| match. May match the empty input.
13+option : {c : Bool} ->
14+ (def : a) -> (p : Grammar tok c a) ->
15+ Grammar tok False a
16+option {c = False} def p = p <|> pure def
17+option {c = True} def p = p <|> pure def
18+
19+||| Optionally parse a thing.
20+||| To provide a default value, use `option` instead.
21+optional : (p : Grammar tok c a) ->
22+ Grammar tok False (Maybe a)
23+optional p = option Nothing (map Just p)
24+
25+||| Try to parse one thing or the other, producing a value that indicates
26+||| which option succeeded. If both would succeed, the left option
27+||| takes priority.
28+choose : (l : Grammar tok c1 a) ->
29+ (r : Grammar tok c2 b) ->
30+ Grammar tok (c1 && c2) (Either a b)
31+choose l r = map Left l <|> map Right r
32+
33+||| Produce a grammar by applying a function to each element of a container,
34+||| then try each resulting grammar until the first one succeeds. Fails if the
35+||| container is empty.
36+choiceMap : {c : Bool} ->
37+ (a -> Grammar tok c b) ->
38+ Foldable t => t a ->
39+ Grammar tok c b
40+choiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in
41+ f x <|> acc)
42+ (fail "No more options") xs
43+
44+||| Try each grammar in a container until the first one succeeds.
45+||| Fails if the container is empty.
46+choice : Foldable t => t (Grammar tok c a) ->
47+ Grammar tok c a
48+choice = choiceMap id
49+
50+mutual
51+ ||| Parse one or more things
52+ some : Grammar tok True a ->
26753 Grammar tok True (List a)
268−sepBy1 sep p = do x <- p
269− (do sep
270− xs <- sepBy1 sep p
271− pure (x :: xs)) <|> pure [x]
272−
273−||| Parse zero or more things, separated by another thing. May
54+ some p = pure (!p :: !(many p))
55+
56+ ||| Parse zero or more things (may match the empty input)
57+ many : Grammar tok True a ->
58+ Grammar tok False (List a)
59+ many p = option [] (some p)
60+
61+||| Parse one or more instances of `p`, returning the parsed items and proof
62+||| that the resulting list is non-empty.
63+some' : (p : Grammar tok True a) ->
64+ Grammar tok True (xs : List a ** NonEmpty xs)
65+some' p = pure (!p :: !(many p) ** IsNonEmpty)
66+
67+mutual
68+ private
69+ count1 : (q : Quantity) ->
70+ (p : Grammar tok True a) ->
71+ Grammar tok True (List a)
72+ count1 q p = do x <- p
73+ seq (count q p)
74+ (\xs => pure (x :: xs))
75+
76+ ||| Parse `p`, repeated as specified by `q`, returning the list of values.
77+ count : (q : Quantity) ->
78+ (p : Grammar tok True a) ->
79+ Grammar tok (isSucc (min q)) (List a)
80+ count (Qty Z Nothing) p = many p
81+ count (Qty Z (Just Z)) _ = pure []
82+ count (Qty Z (Just (S max))) p = option [] $ count1 (atMost max) p
83+ count (Qty (S min) Nothing) p = count1 (atLeast min) p
84+ count (Qty (S min) (Just Z)) _ = fail "Quantity out of order"
85+ count (Qty (S min) (Just (S max))) p = count1 (between (S min) max) p
86+
87+mutual
88+ ||| Parse one or more instances of `p` until `end` succeeds, returning the
89+ ||| list of values from `p`. Guaranteed to consume input.
90+ someTill : {c : Bool} ->
91+ (end : Grammar tok c e) ->
92+ (p : Grammar tok True a) ->
93+ Grammar tok True (List a)
94+ someTill {c} end p = do x <- p
95+ seq (manyTill end p)
96+ (\xs => pure (x :: xs))
97+
98+ ||| Parse zero or more instances of `p` until `end` succeeds, returning the
99+ ||| list of values from `p`. Guaranteed to consume input if `end` consumes.
100+ manyTill : {c : Bool} ->
101+ (end : Grammar tok c e) ->
102+ (p : Grammar tok True a) ->
103+ Grammar tok c (List a)
104+ manyTill {c} end p = rewrite sym (andTrueNeutral c) in
105+ map (const []) end <|> someTill end p
106+
107+||| Parse one or more instances of `p` until `end` succeeds, returning the
108+||| list of values from `p`, along with a proof that the resulting list is
109+||| non-empty.
110+someTill' : {c : Bool} ->
111+ (end : Grammar tok c a) ->
112+ (p : Grammar tok True a) ->
113+ Grammar tok True (xs : List a ** NonEmpty xs)
114+someTill' end p
115+ = do x <- p
116+ seq (manyTill end p)
117+ (\xs => pure (x :: xs ** IsNonEmpty))
118+
119+mutual
120+ ||| Parse one or more instance of `skip` until `p` is encountered,
121+ ||| returning its value.
122+ afterSome : (skip : Grammar tok True s) ->
123+ (p : Grammar tok c a) ->
124+ Grammar tok True a
125+ afterSome skip p = do skip
126+ afterMany skip p
127+
128+ ||| Parse zero or more instance of `skip` until `p` is encountered,
129+ ||| returning its value.
130+ afterMany : {c : Bool} ->
131+ (skip : Grammar tok True s) ->
132+ (p : Grammar tok c a) ->
133+ Grammar tok c a
134+ afterMany {c} skip p = rewrite sym (andTrueNeutral c) in
135+ p <|> afterSome skip p
136+
137+||| Parse one or more things, each separated by another thing.
138+sepBy1 : {c : Bool} ->
139+ (sep : Grammar tok True s) ->
140+ (p : Grammar tok c a) ->
141+ Grammar tok c (List a)
142+sepBy1 {c} sep p = rewrite sym (orFalseNeutral c) in
143+ [| p :: many (sep *> p) |]
144+
145+||| Parse zero or more things, each separated by another thing. May
274146||| match the empty input.
275−export
276−sepBy : Grammar tok True () -> Grammar tok True a ->
147+sepBy : (sep : Grammar tok True s) ->
148+ (p : Grammar tok c a) ->
277149 Grammar tok False (List a)
278−sepBy sep p = sepBy1 sep p <|> pure []
150+sepBy sep p = option [] $ sepBy1 sep p
151+
152+||| Parse one or more instances of `p` separated by `sep`, returning the
153+||| parsed items and proof that the resulting list is non-empty.
154+sepBy1' : {c : Bool} ->
155+ (sep : Grammar tok True s) ->
156+ (p : Grammar tok c a) ->
157+ Grammar tok c (xs : List a ** NonEmpty xs)
158+sepBy1' {c} sep p
159+ = rewrite sym (orFalseNeutral c) in
160+ seq p (\x => do xs <- many (sep *> p)
161+ pure (x :: xs ** IsNonEmpty))
162+
163+||| Parse one or more instances of `p` separated by and optionally terminated by
164+||| `sep`.
165+sepEndBy1 : {c : Bool} ->
166+ (sep : Grammar tok True s) ->
167+ (p : Grammar tok c a) ->
168+ Grammar tok c (List a)
169+sepEndBy1 {c} sep p = rewrite sym (orFalseNeutral c) in
170+ sepBy1 sep p <* optional sep
171+
172+||| Parse zero or more instances of `p`, separated by and optionally terminated
173+||| by `sep`. Will not match a separator by itself.
174+sepEndBy : (sep : Grammar tok True s) ->
175+ (p : Grammar tok c a) ->
176+ Grammar tok False (List a)
177+sepEndBy sep p = option [] $ sepEndBy1 sep p
178+
179+||| Parse zero or more instances of `p`, separated by and optionally terminated
180+||| by `sep`, returning the parsed items and a proof that the resulting list
181+||| is non-empty.
182+sepEndBy1' : {c : Bool} ->
183+ (sep : Grammar tok True s) ->
184+ (p : Grammar tok c a) ->
185+ Grammar tok c (xs : List a ** NonEmpty xs)
186+sepEndBy1' {c} sep p = rewrite sym (orFalseNeutral c) in
187+ sepBy1' sep p <* optional sep
188+
189+||| Parse one or more instances of `p`, separated and terminated by `sep`.
190+endBy1 : {c : Bool} ->
191+ (sep : Grammar tok True s) ->
192+ (p : Grammar tok c a) ->
193+ Grammar tok True (List a)
194+endBy1 {c} sep p = some $ rewrite sym (orTrueTrue c) in
195+ p <* sep
279196
280−||| Optionally parse a thing, with a default value if the grammar doesn't
281−||| match. May match the empty input.
282−export
283−optional : Grammar tok True a -> (ifNothing : a) ->
284− Grammar tok False a
285−optional p def = p <|> pure def
197+endBy : (sep : Grammar tok True s) ->
198+ (p : Grammar tok c a) ->
199+ Grammar tok False (List a)
200+endBy sep p = option [] $ endBy1 sep p
286201
287−||| Fold over a list of grammars until the first one succeeds.
288−choice : Foldable t => t (Grammar tok True a) -> Grammar tok True a
289−choice xs = foldr Alt (Fail "No more options") xs
202+||| Parse zero or more instances of `p`, separated and terminated by `sep`,
203+||| returning the parsed items and a proof that the resulting list is non-empty.
204+endBy1' : {c : Bool} ->
205+ (sep : Grammar tok True s) ->
206+ (p : Grammar tok c a) ->
207+ Grammar tok True (xs : List a ** NonEmpty xs)
208+endBy1' {c} sep p = some' $ rewrite sym (orTrueTrue c) in
209+ p <* sep
290210
291211||| Parse an instance of `p` that is between `left` and `right`.
292−export
293−between : (left : Grammar tok True ())
294− -> (right : Grammar tok True ())
295− -> (p : Grammar tok True a)
296− -> Grammar tok True a
297−between left right contents = do
298− left
299− res <- contents
300− right
301− pure res
302−
303−||| Parse one or more instances of `p` separated by `s`, returning the
304−||| parsed items and proof the resulting list is non-empty.
305−export
306−sepBy1' : (sep : Grammar tok True ())
307− -> (p : Grammar tok True a)
308− -> Grammar tok True (xs : List a ** NonEmpty xs)
309−sepBy1' sep p
310− = do x <- p
311− (do sep
312− xs <- sepBy1 sep p
313− pure (x :: xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)
314−
315−||| Parse one or more instances of `p`, returning the parsed items and proof the resulting list is non-empty.
316−export
317−some' : (p : Grammar tok True a)
318− -> Grammar tok True (xs : List a ** NonEmpty xs)
319−some' p = do
320− x <- p
321− (do xs <- some p
322− pure (x::xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)
323−
324−
325−||| Optionally parse a thing. If the grammar provides a default use `optional` instead.
326−export
327−maybe : Grammar tok True a
328− -> Grammar tok False (Maybe a)
329−maybe p =
330− (do res <- p; pure $ Just res)
331− <|> pure Nothing
212+between : (left : Grammar tok True l) ->
213+ (right : Grammar tok True r) ->
214+ (p : Grammar tok c a) ->
215+ Grammar tok True a
216+between left right contents = left *> contents <* right