@@ -0,0 +1,38 @@
6+||| For a type `kind`, specify a way of converting the recognised
7+||| string into a value.
10+||| data SimpleKind = SKString | SKInt | SKComma
12+||| TokenKind SimpleKind where
13+||| tokType SKString = String
14+||| tokType SKInt = Int
15+||| tokType SKComma = ()
17+||| tokValue SKString x = x
18+||| tokValue SKInt x = cast x
19+||| tokValue SKComma x = ()
21+interface TokenKind (k : Type) where
22+ ||| The type that a token of this kind converts to.
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
29+||| A token of a particular kind and the text that was recognised.
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