0 | module Language.JSON.Tokens
 1 |
 2 | import Language.JSON.String
 3 | import Text.Token
 4 | import Text.Bounded
 5 |
 6 | %default total
 7 |
 8 | public export
 9 | strTrue : String
10 | strTrue = "true"
11 |
12 | public export
13 | strFalse : String
14 | strFalse = "false"
15 |
16 | public export
17 | data Bracket = Open | Close
18 |
19 | public export
20 | Eq Bracket where
21 |   (==) Open Open = True
22 |   (==) Close Close = True
23 |   (==) _ _ = False
24 |
25 | public export
26 | data Punctuation
27 |   = Comma
28 |   | Colon
29 |   | Square Bracket
30 |   | Curly Bracket
31 |
32 | public export
33 | Eq Punctuation where
34 |   (==) Comma Comma = True
35 |   (==) Colon Colon = True
36 |   (==) (Square b1) (Square b2) = b1 == b2
37 |   (==) (Curly b1) (Curly b2) = b1 == b2
38 |   (==) _ _ = False
39 |
40 | public export
41 | data JSONTokenKind
42 |   = JTBoolean
43 |   | JTNumber
44 |   | JTString
45 |   | JTNull
46 |   | JTPunct Punctuation
47 |   | JTIgnore
48 |
49 | public export
50 | JSONToken : Type
51 | JSONToken = Token JSONTokenKind
52 |
53 | public export
54 | Eq JSONTokenKind where
55 |   (==) JTBoolean JTBoolean = True
56 |   (==) JTNumber JTNumber = True
57 |   (==) JTString JTString = True
58 |   (==) JTNull JTNull = True
59 |   (==) (JTPunct p1) (JTPunct p2) = p1 == p2
60 |   (==) _ _ = False
61 |
62 | public export
63 | TokenKind JSONTokenKind where
64 |   TokType JTBoolean = Bool
65 |   TokType JTNumber = Double
66 |   TokType JTString = Maybe String
67 |   TokType JTNull = ()
68 |   TokType (JTPunct _) = ()
69 |   TokType JTIgnore = ()
70 |
71 |   tokValue JTBoolean x = x == strTrue
72 |   tokValue JTNumber x = cast x
73 |   tokValue JTString x = stringValue x
74 |   tokValue JTNull _ = ()
75 |   tokValue (JTPunct _) _ = ()
76 |   tokValue JTIgnore _ = ()
77 |
78 | export
79 | ignored : WithBounds JSONToken -> Bool
80 | ignored (MkBounded (Tok JTIgnore _) _ _) = True
81 | ignored _ = False
82 |