git.iko.soy/Idris-dev
on master help sign in
Text.Parser: use `%access export`
3287187Michael Morgan
libs/contrib/Text/Parser.idr+4−10
compare with master
unifiedsplit
@@ -1,9 +1,11 @@
1module Text.Parser
1module Text.Parser
2
2
3+import public Text.Parser.Core
4+
5+%access export
3%default total
6%default total
4
7
5||| Parse one or more things
8||| Parse one or more things
6−export
7some : Grammar tok True a ->
9some : Grammar tok True a ->
8 Grammar tok True (List a)
10 Grammar tok True (List a)
9some p = do x <- p
11some p = do x <- p
@@ -11,14 +13,12 @@ some p = do x <- p
11 pure (x :: xs)) <|> pure [x]
13 pure (x :: xs)) <|> pure [x]
12
14
13||| Parse zero or more things (may match the empty input)
15||| Parse zero or more things (may match the empty input)
14−export
15many : Grammar tok True a ->
16many : Grammar tok True a ->
16 Grammar tok False (List a)
17 Grammar tok False (List a)
17many p = some p
18many p = some p
18 <|> pure []
19 <|> pure []
19
20
20||| Parse one or more things, separated by another thing
21||| Parse one or more things, separated by another thing
21−export
22sepBy1 : Grammar tok True () -> Grammar tok True a ->
22sepBy1 : Grammar tok True () -> Grammar tok True a ->
23 Grammar tok True (List a)
23 Grammar tok True (List a)
24sepBy1 sep p = do x <- p
24sepBy1 sep p = do x <- p
@@ -28,24 +28,21 @@ sepBy1 sep p = do x <- p
28
28
29||| Parse zero or more things, separated by another thing. May
29||| Parse zero or more things, separated by another thing. May
30||| match the empty input.
30||| match the empty input.
31−export
32sepBy : Grammar tok True () -> Grammar tok True a ->
31sepBy : Grammar tok True () -> Grammar tok True a ->
33 Grammar tok False (List a)
32 Grammar tok False (List a)
34sepBy sep p = sepBy1 sep p <|> pure []
33sepBy sep p = sepBy1 sep p <|> pure []
35
34
36||| Optionally parse a thing, with a default value if the grammar doesn't
35||| Optionally parse a thing, with a default value if the grammar doesn't
37||| match. May match the empty input.
36||| match. May match the empty input.
38−export
39optional : Grammar tok True a -> (ifNothing : a) ->
37optional : Grammar tok True a -> (ifNothing : a) ->
40 Grammar tok False a
38 Grammar tok False a
41optional p def = p <|> pure def
39optional p def = p <|> pure def
42
40
43||| Fold over a list of grammars until the first one succeeds.
41||| Fold over a list of grammars until the first one succeeds.
44choice : Foldable t => t (Grammar tok True a) -> Grammar tok True a
42choice : 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
46
44
47||| Parse an instance of `p` that is between `left` and `right`.
45||| Parse an instance of `p` that is between `left` and `right`.
48−export
49between : (left : Grammar tok True ())
46between : (left : Grammar tok True ())
50 -> (right : Grammar tok True ())
47 -> (right : Grammar tok True ())
51 -> (p : Grammar tok True a)
48 -> (p : Grammar tok True a)
@@ -58,7 +55,6 @@ between left right contents = do
58
55
59||| Parse one or more instances of `p` separated by `s`, returning the
56||| Parse one or more instances of `p` separated by `s`, returning the
60||| parsed items and proof the resulting list is non-empty.
57||| parsed items and proof the resulting list is non-empty.
61−export
62sepBy1' : (sep : Grammar tok True ())
58sepBy1' : (sep : Grammar tok True ())
63 -> (p : Grammar tok True a)
59 -> (p : Grammar tok True a)
64 -> Grammar tok True (xs : List a ** NonEmpty xs)
60 -> Grammar tok True (xs : List a ** NonEmpty xs)
@@ -69,7 +65,6 @@ sepBy1' sep p
69 pure (x :: xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)
65 pure (x :: xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)
70
66
71||| Parse one or more instances of `p`, returning the parsed items and proof the resulting list is non-empty.
67||| Parse one or more instances of `p`, returning the parsed items and proof the resulting list is non-empty.
72−export
73some' : (p : Grammar tok True a)
68some' : (p : Grammar tok True a)
74 -> Grammar tok True (xs : List a ** NonEmpty xs)
69 -> Grammar tok True (xs : List a ** NonEmpty xs)
75some' p = do
70some' p = do
@@ -79,7 +74,6 @@ some' p = do
79
74
80
75
81||| Optionally parse a thing. If the grammar provides a default use `optional` instead.
76||| Optionally parse a thing. If the grammar provides a default use `optional` instead.
82−export
83maybe : Grammar tok True a
77maybe : Grammar tok True a
84 -> Grammar tok False (Maybe a)
78 -> Grammar tok False (Maybe a)
85maybe p =
79maybe p =