git.iko.soy/Idris-dev
on master help sign in
Text.Parser: add `match` function for easier terminals

In a grammar that accepts `Token k` as its token type, `match` reduces the boilerplate required to parse terminals. Instead of requiring a terminal parsing function per token (or token kind) with a case split, this function requires an `Eq` implementation to compare kinds of tokens.

commitb6f6d4204679683ff26a35cdc9c42b5ef8f51ff1 authorMichael Morgan <morgan.michael@me.com> dateThu 9 Nov 2017, 14:55 (9 years ago) parentbc8da8d
1 file changed+10
compare with master
unifiedsplit
libs/contrib/Text/Parser.idr+10
libs/contrib/Text/Parser.idr+10
@@ -4,10 +4,20 @@ import Data.Bool.Extra
44
55import public Text.Parser.Core
66import public Text.Quantity
7+import public Text.Token
78
89%access export
910%default total
1011
12+||| Parse a terminal based on a kind of token.
13+match : (Eq k, TokenKind k) =>
14+ (kind : k) ->
15+ Grammar (Token k) True (tokType kind)
16+match kind = terminal $
17+ \(Tok kind' text) => if kind' == kind
18+ then Just $ tokValue kind text
19+ else Nothing
20+
1121||| Optionally parse a thing, with a default value if the grammar doesn't
1222||| match. May match the empty input.
1323option : {c : Bool} ->