@@ -1,81 +1,81 @@
11module Text.Parser
22
3+import Data.Bool.Extra
4+
35import public Text.Parser.Core
46
57%access export
68%default total
79
8−||| Parse one or more things
9−some : Grammar tok True a ->
10− Grammar tok True (List a)
11−some p = do x <- p
12− (do xs <- some p
13− pure (x :: xs)) <|> pure [x]
10+||| Optionally parse a thing, with a default value if the grammar doesn't
11+||| match. May match the empty input.
12+option : {c : Bool} ->
13+ (def : a) -> (p : Grammar tok c a) ->
14+ Grammar tok False a
15+option {c} def p = rewrite sym (andFalseFalse c) in
16+ p <|> pure def
1417
15−||| Parse zero or more things (may match the empty input)
16−many : Grammar tok True a ->
17− Grammar tok False (List a)
18−many p = some p
19− <|> pure []
18+||| Optionally parse a thing.
19+||| To provide a default value, use `option` instead.
20+optional : (p : Grammar tok c a) ->
21+ Grammar tok False (Maybe a)
22+optional p = option Nothing (map Just p)
2023
21−||| Parse one or more things, separated by another thing
22−sepBy1 : Grammar tok True () -> Grammar tok True a ->
23− Grammar tok True (List a)
24−sepBy1 sep p = do x <- p
25− (do sep
26− xs <- sepBy1 sep p
27− pure (x :: xs)) <|> pure [x]
28−
29−||| Parse zero or more things, separated by another thing. May
30−||| match the empty input.
31−sepBy : Grammar tok True () -> Grammar tok True a ->
32− Grammar tok False (List a)
33−sepBy sep p = sepBy1 sep p <|> pure []
24+||| Try each grammar in a container until the first one succeeds.
25+||| Fails if the container is empty.
26+choice : {c : Bool} ->
27+ Foldable t => t (Grammar tok c a) ->
28+ Grammar tok c a
29+choice {c} xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in
30+ x <|> acc)
31+ (fail "No more options") xs
3432
35−||| Optionally parse a thing, with a default value if the grammar doesn't
36−||| match. May match the empty input.
37−optional : Grammar tok True a -> (ifNothing : a) ->
38− Grammar tok False a
39−optional p def = p <|> pure def
33+mutual
34+ ||| Parse one or more things
35+ some : Grammar tok True a ->
36+ Grammar tok True (List a)
37+ some p = pure (!p :: !(many p))
4038
41−||| Fold over a list of grammars until the first one succeeds.
42−choice : Foldable t => t (Grammar tok True a) -> Grammar tok True a
43−choice xs = foldr (<|>) (fail "No more options") xs
39+ ||| Parse zero or more things (may match the empty input)
40+ many : Grammar tok True a ->
41+ Grammar tok False (List a)
42+ many p = option [] (some p)
4443
45−||| Parse an instance of `p` that is between `left` and `right`.
46−between : (left : Grammar tok True ())
47− -> (right : Grammar tok True ())
48− -> (p : Grammar tok True a)
49− -> Grammar tok True a
50−between left right contents = do
51− left
52− res <- contents
53− right
54− pure res
44+||| Parse one or more instances of `p`, returning the parsed items and proof
45+||| that the resulting list is non-empty.
46+some' : (p : Grammar tok True a) ->
47+ Grammar tok True (xs : List a ** NonEmpty xs)
48+some' p = pure (!p :: !(many p) ** IsNonEmpty)
5549
56−||| Parse one or more instances of `p` separated by `s`, returning the
57−||| parsed items and proof the resulting list is non-empty.
58−sepBy1' : (sep : Grammar tok True ())
59− -> (p : Grammar tok True a)
60− -> Grammar tok True (xs : List a ** NonEmpty xs)
61−sepBy1' sep p
62− = do x <- p
63− (do sep
64− xs <- sepBy1 sep p
65− pure (x :: xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)
50+||| Parse one or more things, each separated by another thing.
51+sepBy1 : {c : Bool} ->
52+ (sep : Grammar tok True s) ->
53+ (p : Grammar tok c a) ->
54+ Grammar tok c (List a)
55+sepBy1 {c} sep p = rewrite sym (orFalseNeutral c) in
56+ [| p :: many (sep *> p) |]
6657
67−||| Parse one or more instances of `p`, returning the parsed items and proof the resulting list is non-empty.
68−some' : (p : Grammar tok True a)
69− -> Grammar tok True (xs : List a ** NonEmpty xs)
70−some' p = do
71− x <- p
72− (do xs <- some p
73− pure (x::xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)
58+||| Parse zero or more things, each separated by another thing. May
59+||| match the empty input.
60+sepBy : (sep : Grammar tok True s) ->
61+ (p : Grammar tok c a) ->
62+ Grammar tok False (List a)
63+sepBy sep p = option [] $ sepBy1 sep p
7464
65+||| Parse one or more instances of `p` separated by `sep`, returning the
66+||| parsed items and proof that the resulting list is non-empty.
67+sepBy1' : {c : Bool} ->
68+ (sep : Grammar tok True s) ->
69+ (p : Grammar tok c a) ->
70+ Grammar tok c (xs : List a ** NonEmpty xs)
71+sepBy1' {c} sep p
72+ = rewrite sym (orFalseNeutral c) in
73+ seq p (\x => do xs <- many (sep *> p)
74+ pure (x :: xs ** IsNonEmpty))
7575
76−||| Optionally parse a thing. If the grammar provides a default use `optional` instead.
77−maybe : Grammar tok True a
78− -> Grammar tok False (Maybe a)
79−maybe p =
80− (do res <- p; pure $ Just res)
81− <|> pure Nothing
76+||| Parse an instance of `p` that is between `left` and `right`.
77+between : (left : Grammar tok True l) ->
78+ (right : Grammar tok True r) ->
79+ (p : Grammar tok c a) ->
80+ Grammar tok True a
81+between left right contents = left *> contents <* right