0 | module Text.TOML.Types
  1 |
  2 | import public Data.Time.Time
  3 | import public Data.SortedMap
  4 | import Derive.Prelude
  5 | import Text.Bounds
  6 | import Text.ParseError
  7 |
  8 | %default total
  9 | %language ElabReflection
 10 |
 11 | --------------------------------------------------------------------------------
 12 | --          Floating Point Literals
 13 | --------------------------------------------------------------------------------
 14 |
 15 | public export
 16 | data TomlFloat : Type where
 17 |   NaN   : TomlFloat
 18 |   Infty : Sign -> TomlFloat
 19 |   Float : Double -> TomlFloat
 20 |
 21 | %runElab derive "TomlFloat" [Eq,Show]
 22 |
 23 | export
 24 | Interpolation TomlFloat where
 25 |   interpolate NaN          = "nan"
 26 |   interpolate (Infty Plus) = "inf"
 27 |   interpolate (Infty _)    = "-inf"
 28 |   interpolate (Float dbl) = show dbl
 29 |
 30 | --------------------------------------------------------------------------------
 31 | --          TomlValue and Table
 32 | --------------------------------------------------------------------------------
 33 |
 34 | ||| Data type for trees of TOML data.
 35 | public export
 36 | data TomlValue : Type where
 37 |   ||| A string literal
 38 |   TStr  : String -> TomlValue
 39 |
 40 |   ||| A boolean literal
 41 |   TBool : Bool -> TomlValue
 42 |
 43 |   ||| A date-time literal
 44 |   TTime : AnyTime -> TomlValue
 45 |
 46 |   ||| An integer
 47 |   TInt  : Integer -> TomlValue
 48 |
 49 |   ||| A floating point number
 50 |   TDbl  : TomlFloat  -> TomlValue
 51 |
 52 |   ||| An array of values
 53 |   TArr  : List TomlValue -> TomlValue
 54 |
 55 |   ||| A table of key-value pairs
 56 |   TTbl  : SortedMap String TomlValue -> TomlValue
 57 |
 58 | %name TomlValue v,v1,v2
 59 | %runElab derive "TomlValue" [Eq,Show]
 60 |
 61 | ||| Currently, a TOML table is a list of pairs. This might be later
 62 | ||| changed to some kind of dictionary.
 63 | public export
 64 | 0 TomlTable : Type
 65 | TomlTable = SortedMap String TomlValue
 66 |
 67 | %name TomlTable t,t1,t2
 68 |
 69 | --------------------------------------------------------------------------------
 70 | --          Keys
 71 | --------------------------------------------------------------------------------
 72 |
 73 | public export
 74 | data KeyType = Plain | Quoted | Literal
 75 |
 76 | %runElab derive "KeyType" [Eq,Show]
 77 |
 78 | public export
 79 | record Key where
 80 |   constructor KT
 81 |   key    : String
 82 |   tpe    : KeyType
 83 |   bounds : Bounds
 84 |
 85 | %name Key k,k2,k3
 86 | %runElab derive "Key" [Eq,Show]
 87 |
 88 | export
 89 | Interpolation Key where
 90 |   interpolate (KT k t _) = case t of
 91 |     Plain   => k
 92 |     Quoted  => show k
 93 |     Literal => "'\{k}'"
 94 |
 95 | Interpolation (List Key) where
 96 |   interpolate = fastConcat . intersperse "." . map interpolate
 97 |
 98 | --------------------------------------------------------------------------------
 99 | --          Errors
100 | --------------------------------------------------------------------------------
101 |
102 | public export
103 | data TomlParseError : Type where
104 |   ValueExists       : List Key -> TomlParseError
105 |   InlineTableExists : List Key -> TomlParseError
106 |   TableExists       : List Key -> TomlParseError
107 |   StaticArray       : List Key -> TomlParseError
108 |   TableArray        : List Key -> TomlParseError
109 |   InvalidLeapDay    : LocalDate -> TomlParseError
110 |
111 | %runElab derive "TomlParseError" [Eq,Show]
112 |
113 | export
114 | Interpolation TomlParseError where
115 |   interpolate (ValueExists k) =
116 |     "Trying to overwrite an existing value: \{k}"
117 |   interpolate (InlineTableExists k) =
118 |     "Trying to overwrite an existing inline table: \{k}"
119 |   interpolate (TableExists k) =
120 |     "Trying to overwrite an existing table: \{k}"
121 |   interpolate (StaticArray k) =
122 |     "Trying to overwrite an existing array: \{k}"
123 |   interpolate (TableArray k) =
124 |     "Trying to overwrite an existing array of tables: \{k}"
125 |   interpolate (InvalidLeapDay d) = "Invalid leap day: \{d}"
126 |
127 | ||| Error type when lexing and parsing TOML files
128 | public export
129 | 0 TErr : Type
130 | TErr = BoundedErr TomlParseError
131 |