@@ -1,9 +1,11 @@
11module Text.Parser
22
3+import public Text.Parser.Core
4+
5+%access export
36%default total
47
58||| Parse one or more things
6−export
79some : Grammar tok True a ->
810 Grammar tok True (List a)
911some p = do x <- p
@@ -11,14 +13,12 @@ some p = do x <- p
1113 pure (x :: xs)) <|> pure [x]
1214
1315||| Parse zero or more things (may match the empty input)
14−export
1516many : Grammar tok True a ->
1617 Grammar tok False (List a)
1718many p = some p
1819 <|> pure []
1920
2021||| Parse one or more things, separated by another thing
21−export
2222sepBy1 : Grammar tok True () -> Grammar tok True a ->
2323 Grammar tok True (List a)
2424sepBy1 sep p = do x <- p
@@ -28,24 +28,21 @@ sepBy1 sep p = do x <- p
2828
2929||| Parse zero or more things, separated by another thing. May
3030||| match the empty input.
31−export
3231sepBy : Grammar tok True () -> Grammar tok True a ->
3332 Grammar tok False (List a)
3433sepBy sep p = sepBy1 sep p <|> pure []
3534
3635||| Optionally parse a thing, with a default value if the grammar doesn't
3736||| match. May match the empty input.
38−export
3937optional : Grammar tok True a -> (ifNothing : a) ->
4038 Grammar tok False a
4139optional p def = p <|> pure def
4240
4341||| Fold over a list of grammars until the first one succeeds.
4442choice : Foldable t => t (Grammar tok True a) -> Grammar tok True a
45−choice xs = foldr Alt (Fail "No more options") xs
43+choice xs = foldr (<|>) (fail "No more options") xs
4644
4745||| Parse an instance of `p` that is between `left` and `right`.
48−export
4946between : (left : Grammar tok True ())
5047 -> (right : Grammar tok True ())
5148 -> (p : Grammar tok True a)
@@ -58,7 +55,6 @@ between left right contents = do
5855
5956||| Parse one or more instances of `p` separated by `s`, returning the
6057||| parsed items and proof the resulting list is non-empty.
61−export
6258sepBy1' : (sep : Grammar tok True ())
6359 -> (p : Grammar tok True a)
6460 -> Grammar tok True (xs : List a ** NonEmpty xs)
@@ -69,7 +65,6 @@ sepBy1' sep p
6965 pure (x :: xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)
7066
7167||| Parse one or more instances of `p`, returning the parsed items and proof the resulting list is non-empty.
72−export
7368some' : (p : Grammar tok True a)
7469 -> Grammar tok True (xs : List a ** NonEmpty xs)
7570some' p = do
@@ -79,7 +74,6 @@ some' p = do
7974
8075
8176||| Optionally parse a thing. If the grammar provides a default use `optional` instead.
82−export
8377maybe : Grammar tok True a
8478 -> Grammar tok False (Maybe a)
8579maybe p =