@@ -0,0 +1,38 @@
1+module Text.Token
2+
3+%access public export
4+%default total
5+
6+||| For a type `kind`, specify a way of converting the recognised
7+||| string into a value.
8+|||
9+||| ```idris example
10+||| data SimpleKind = SKString | SKInt | SKComma
11+|||
12+||| TokenKind SimpleKind where
13+||| TokType SKString = String
14+||| TokType SKInt = Int
15+||| TokType SKComma = ()
16+|||
17+||| tokValue SKString x = x
18+||| tokValue SKInt x = cast x
19+||| tokValue SKComma x = ()
20+||| ```
21+interface TokenKind (k : Type) where
22+ ||| The type that a token of this kind converts to.
23+ TokType : k -> Type
24+
25+ ||| Convert a recognised string into a value. The type is determined
26+ ||| by the kind of token.
27+ tokValue : (kind : k) -> String -> TokType kind
28+
29+||| A token of a particular kind and the text that was recognised.
30+record Token k where
31+ constructor Tok
32+ kind : k
33+ text : String
34+
35+||| Get the value of a `Token k`. The resulting type depends upon
36+||| the kind of token.
37+value : TokenKind k => (t : Token k) -> TokType (kind t)
38+value (Tok k x) = tokValue k x