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