0 | module Pack.Database.TOML
 1 |
 2 | import Data.SortedMap
 3 | import Idris.Package.Types
 4 | import Libraries.Utils.Path
 5 | import Text.TOML
 6 | import Pack.Core.TOML
 7 | import Pack.Core.Types
 8 | import Pack.Database.Types
 9 |
10 | %default total
11 |
12 | export
13 | FromTOML MetaCommit where fromTOML = tmap fromString
14 |
15 | git : FromTOML c => File Abs -> TomlValue -> Either TOMLErr (Package_ I c)
16 | git f v =
17 |   [| Git
18 |        (valAt "url" f v)
19 |        (valAt "commit" f v)
20 |        (valAt "ipkg" f v)
21 |        (optValAt "packagePath" f False v)
22 |        (maybeValAt "test" f v)
23 |        (maybeValAt "notice" f v)
24 |   |]
25 |
26 | local : File Abs -> TomlValue -> Either TOMLErr (Package_ f c)
27 | local f v =
28 |   [| Local
29 |        (valAt "path" f v)
30 |        (valAt "ipkg" f v)
31 |        (optValAt "packagePath" f False v)
32 |        (maybeValAt "test" f v)
33 |   |]
34 |
35 | package : FromTOML c => File Abs -> TomlValue -> Either TOMLErr (Package_ I c)
36 | package f v = valAt {a = String} "type" f v >>=
37 |   \case
38 |     "git"    => git f v
39 |     "github" => git f v -- for compatibility
40 |     "local"  => local f v
41 |     _        => Left $ WrongType ["type"] "Package Type"
42 |
43 | gitM : FromTOML c => File Abs -> TomlValue -> Either TOMLErr (Package_ Maybe c)
44 | gitM f v =
45 |   [| Git
46 |        (maybeValAt "url" f v)
47 |        (maybeValAt "commit" f v)
48 |        (maybeValAt "ipkg" f v)
49 |        (maybeValAt "packagePath" f v)
50 |        (maybeValAt "test" f v)
51 |        (maybeValAt "notice" f v)
52 |   |]
53 |
54 | packageM : FromTOML c => File Abs -> TomlValue -> Either TOMLErr (Package_ Maybe c)
55 | packageM f v = optValAt {a = String} "type" f "git" v >>=
56 |   \case
57 |     "git"    => gitM f v
58 |     "github" => gitM f v -- for compatibility
59 |     "local"  => local f v
60 |     _        => Left $ WrongType ["type"] "Package Type"
61 |
62 | export %inline
63 | FromTOML c => FromTOML (Package_ I c) where fromTOML = package
64 |
65 | export %inline
66 | FromTOML c => FromTOML (Package_ Maybe c) where fromTOML = packageM
67 |
68 | ||| URL of the Idris repository
69 | export
70 | idrisRepo : URL
71 | idrisRepo = "https://github.com/idris-lang/Idris2.git"
72 |
73 | v0 : PkgVersion
74 | v0 = MkPkgVersion (0:::[0,0])
75 |
76 | export
77 | FromTOML MetaDB where
78 |   fromTOML f v =
79 |     [| MkDB
80 |          (optValAt "idris2.url" f idrisRepo v)
81 |          (valAt "idris2.commit" f v)
82 |          (pure v0)
83 |          (optValAt "db" f empty v)
84 |     |]
85 |