@@ -109,6 +109,20 @@ export
109109 Grammar tok (c1 || c2) b
110110(*>) x y = map (const id) x <*> y
111111
112+||| Produce a grammar that can parse a different type of token by providing a
113+||| function converting the new token type into the original one.
114+export
115+mapToken : (a -> b) -> Grammar b c ty -> Grammar a c ty
116+mapToken f (Empty val) = Empty val
117+mapToken f (Terminal g) = Terminal (g . f)
118+mapToken f (NextIs g) = SeqEmpty (NextIs (g . f)) (Empty . f)
119+mapToken f EOF = EOF
120+mapToken f (Fail msg) = Fail msg
121+mapToken f Commit = Commit
122+mapToken f (SeqEat act next) = SeqEat (mapToken f act) (\x => mapToken f (next x))
123+mapToken f (SeqEmpty act next) = SeqEmpty (mapToken f act) (\x => mapToken f (next x))
124+mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y)
125+
112126||| Always succeed with the given value.
113127export
114128pure : (val : ty) -> Grammar tok False ty