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