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