0 | module Pack.Core.TOML
  1 |
  2 | import Data.SortedMap as M
  3 | import Idris.Package.Types
  4 | import Pack.Core.IO
  5 | import Pack.Core.Types
  6 | import Text.ILex
  7 | import Text.ParseError
  8 | import Text.TOML
  9 |
 10 | %default total
 11 |
 12 | --------------------------------------------------------------------------------
 13 | --          Interface
 14 | --------------------------------------------------------------------------------
 15 |
 16 | ||| Interface for using a pack data type as a key
 17 | ||| in a TOML table.
 18 | public export
 19 | interface Ord a => TOMLKey a where
 20 |   ||| Tries to convert a key to a value of type `a`
 21 |   fromKey : (k : String) -> Either TOMLErr a
 22 |
 23 | export
 24 | TOMLKey DBName where
 25 |   fromKey s = case Body.parse s of
 26 |     Just b  => Right $ MkDBName b
 27 |     Nothing => Left $ WrongType [] "collection name"
 28 |
 29 | export
 30 | TOMLKey PkgName where fromKey = Right . MkPkgName
 31 |
 32 | export
 33 | TOMLKey String where fromKey = Right
 34 |
 35 | ||| Interface for converting a TOML value to a pack
 36 | ||| data type. We pass the TOML file's absolute path
 37 | ||| as an additional argument, since this allows us to
 38 | ||| convert relative paths listed in the TOML file
 39 | ||| (for instance, the path to a local package) to absolute ones.
 40 | public export
 41 | interface FromTOML a where
 42 |   ||| Tries to convert a `TomlValue` to a value of type `a`.
 43 |   fromTOML : File Abs -> (val  : TomlValue) -> Either TOMLErr a
 44 |
 45 | --------------------------------------------------------------------------------
 46 | --          Utilities
 47 | --------------------------------------------------------------------------------
 48 |
 49 | ||| Read a value of type `b` by reading a value of
 50 | ||| type `a` and converting it with the given function.
 51 | export
 52 | tmap : FromTOML a => (a -> b) -> File Abs -> TomlValue -> Either TOMLErr b
 53 | tmap f p = map f . fromTOML p
 54 |
 55 | ||| Read a value of type `b` by refining a value of
 56 | ||| type `a`.
 57 | export
 58 | trefine :
 59 |      {auto _ : FromTOML a}
 60 |   -> (a -> Either TOMLErr b)
 61 |   -> File Abs
 62 |   -> TomlValue
 63 |   -> Either TOMLErr b
 64 | trefine f p v = fromTOML p v >>= f
 65 |
 66 | ||| Try to extract a value from a toml `TomlValue`.
 67 | |||
 68 | ||| @ get   : Tries to convert the value found at the given `path` to a values of
 69 | |||           the result type.
 70 | ||| @ path  : Dot-separated path to the value we'd like to read.
 71 | ||| @ deflt : Optional default value to use if there is not entry
 72 | |||           at the given `path`. Note: This will not be used if there
 73 | |||           is an entry at `path`. In this case, the value found will
 74 | |||           always be handed over to `get`, resulting in a failure if
 75 | |||           it can't be properly converted.
 76 | ||| @ value : The TOML value we start with.
 77 | export
 78 | valAt' :
 79 |      (get  : TomlValue -> Either TOMLErr a)
 80 |   -> (path : String)
 81 |   -> (dflt : Maybe a)
 82 |   -> (val  : TomlValue)
 83 |   -> Either TOMLErr a
 84 | valAt' get path dflt = go (forget $ split ('.' ==) path)
 85 |
 86 |   where
 87 |     go : List String -> TomlValue -> Either TOMLErr a
 88 |     go []        v        = get v
 89 |     go (x :: xs) (TTbl y) = case lookup x y of
 90 |       Nothing => case dflt of
 91 |         Nothing => Left $ MissingKey [x]
 92 |         Just a  => Right a
 93 |       Just v2 => prefixKey x $ go xs v2
 94 |     go _ _                = Left $ WrongType [] "Table"
 95 |
 96 | ||| Extract and convert a mandatory value from a TOML
 97 | ||| value. The `path` string can contain several dot-separated
 98 | ||| key names. See also `valAt'`.
 99 | export %inline
100 | valAt :
101 |      {auto _ : FromTOML a}
102 |   -> (path : String)
103 |   -> File Abs
104 |   -> (val : TomlValue)
105 |   -> Either TOMLErr a
106 | valAt path f = valAt' (fromTOML f) path Nothing
107 |
108 | ||| Extract and convert an optional value from a TOML
109 | ||| value. The `path` string can contain several dot-separated
110 | ||| key names. See also `valAt'`.
111 | export %inline
112 | optValAt :
113 |      {auto _ : FromTOML a}
114 |   -> (path : String)
115 |   -> File Abs
116 |   -> (dflt : a)
117 |   -> (val  : TomlValue)
118 |   -> Either TOMLErr a
119 | optValAt path f = valAt' (fromTOML f) path . Just
120 |
121 | ||| Extract and convert an optional value from a TOML
122 | ||| value. The `path` string can contain several dot-separated
123 | ||| key names. See also `valAt'`.
124 | export
125 | maybeValAt' :
126 |      (f    : TomlValue -> Either TOMLErr a)
127 |   -> (path : String)
128 |   -> (val  : TomlValue)
129 |   -> Either TOMLErr (Maybe a)
130 | maybeValAt' f path = valAt' (map Just . f) path (Just Nothing)
131 |
132 | ||| Extract and convert an optional value from a TOML
133 | ||| value. The `path` string can contain several dot-separated
134 | ||| key names. See also `valAt'`.
135 | export %inline
136 | maybeValAt :
137 |      {auto _ : FromTOML a}
138 |   -> (path : String)
139 |   -> File Abs
140 |   -> (val  : TomlValue)
141 |   -> Either TOMLErr (Maybe a)
142 | maybeValAt p f = maybeValAt' (fromTOML f) p
143 |
144 | --------------------------------------------------------------------------------
145 | --          Implementations
146 | --------------------------------------------------------------------------------
147 |
148 | export
149 | FromTOML String where
150 |   fromTOML _ (TStr s) = Right s
151 |   fromTOML _ _        = Left $ WrongType [] "String"
152 |
153 | export
154 | FromTOML PkgName where fromTOML = tmap MkPkgName
155 |
156 | export
157 | FromTOML URL where fromTOML = tmap MkURL
158 |
159 | export
160 | FromTOML Branch where fromTOML = tmap MkBranch
161 |
162 | export
163 | FromTOML Commit where fromTOML = tmap MkCommit
164 |
165 | export
166 | FromTOML FilePath where fromTOML = tmap fromString
167 |
168 | toRelPath : FilePath -> Either TOMLErr (Path Rel)
169 | toRelPath (FP $ PRel sx)  = Right (PRel sx)
170 | toRelPath (FP $ PAbs _ _) = Left (WrongType [] "Relative Path")
171 |
172 | toRelFile : FilePath -> Either TOMLErr (File Rel)
173 | toRelFile (FP $ PRel (sx :< x)) = Right (MkF (PRel sx) x)
174 | toRelFile _                     = Left (WrongType [] "relative file path")
175 |
176 | export %inline
177 | FromTOML (Path Rel) where fromTOML = trefine toRelPath
178 |
179 | toLogLevel : String -> Either TOMLErr LogLevel
180 | toLogLevel s = case lookup s logLevels of
181 |   Just lvl => Right lvl
182 |   Nothing  => Left (WrongType [] "log level")
183 |
184 | export %inline
185 | FromTOML LogLevel where fromTOML = trefine toLogLevel
186 |
187 | export %inline
188 | FromTOML (File Rel) where fromTOML = trefine toRelFile
189 |
190 | export %inline
191 | FromTOML DBName where fromTOML = trefine fromKey
192 |
193 | export
194 | FromTOML Bool where
195 |   fromTOML _ (TBool b) = Right b
196 |   fromTOML _ _         = Left $ WrongType [] "Bool"
197 |
198 | export
199 | FromTOML a => FromTOML (List a) where
200 |   fromTOML f (TArr vs) = traverse (fromTOML f) vs
201 |   fromTOML _ _         = Left $ WrongType [] "Array"
202 |
203 | readVersion : String -> Either TOMLErr PkgVersion
204 | readVersion s = case traverse parsePositive $ split ('.' ==) s of
205 |   Just ns => Right $ MkPkgVersion ns
206 |   Nothing => Left $ WrongType [] "Package Version"
207 |
208 | export
209 | FromTOML PkgVersion where
210 |   fromTOML = trefine readVersion
211 |
212 | keyVal :
213 |      {auto _ : TOMLKey k}
214 |   -> (TomlValue -> Either TOMLErr v)
215 |   -> (String,TomlValue)
216 |   -> Either TOMLErr (k,v)
217 | keyVal f (x,y) = prefixKey x [| MkPair (fromKey x) (f y) |]
218 |
219 | export
220 | TOMLKey k => FromTOML v => FromTOML (SortedMap k v) where
221 |   fromTOML f (TTbl m) =
222 |     M.fromList <$> traverse (keyVal $ fromTOML f) (M.toList m)
223 |   fromTOML _ _        = Left $ WrongType [] "Table"
224 |
225 | export
226 | FromTOML (Path Abs) where
227 |   fromTOML f v = toAbsPath f.parent <$> fromTOML f v
228 |
229 | export
230 | FromTOML (File Abs) where
231 |   fromTOML f v = toAbsFile f.parent <$> fromTOML f v
232 |
233 | --------------------------------------------------------------------------------
234 | --          Reading a TOML File
235 | --------------------------------------------------------------------------------
236 |
237 | ||| Reads a file and converts its content to a TOML value.
238 | export covering
239 | readTOML :  HasIO io => File Abs -> EitherT PackErr io TomlValue
240 | readTOML file = do
241 |   str <- read file
242 |   case parseString toml (FileSrc "\{file}") str of
243 |     Right v => pure (TTbl v)
244 |     Left x  => throwE $ TOMLParse "\{x}"
245 |
246 | ||| Reads a file, converts its content to a TOML value, and
247 | ||| extracts an Idris value from this.
248 | export covering
249 | readFromTOML :
250 |      {auto _ : HasIO io}
251 |   -> (0 a : Type)
252 |   -> {auto _ : FromTOML a}
253 |   -> File Abs
254 |   -> EitherT PackErr io a
255 | readFromTOML _ file = do
256 |   v <- readTOML file
257 |   liftEither $ mapFst (TOMLFile file) (fromTOML file v)
258 |
259 | ||| Reads a file, converts its content to a TOML value, and
260 | ||| extracts an Idris value from this.
261 | export covering
262 | readOptionalFromTOML :
263 |      {auto _ : HasIO io}
264 |   -> (0 a : Type)
265 |   -> {auto _ : FromTOML a}
266 |   -> File Abs
267 |   -> EitherT PackErr io a
268 | readOptionalFromTOML a f = do
269 |   True <- fileExists f
270 |     | False => liftEither (mapFst (TOMLFile f) $ fromTOML f (TTbl empty))
271 |   readFromTOML a f
272 |