0 | module Pack.Database.Types

  2 | import Core.Name.Namespace

  3 | import Data.Either

  4 | import Data.List1

  5 | import Data.List.Elem

  6 | import Data.SortedMap

  7 | import Data.String

  8 | import Derive.Prelude

  9 | import Idris.Package.Types

 10 | import Pack.Core.Types

 12 | %default total

 13 | %language ElabReflection

 20 | public export

 21 | 0 I : Type -> Type

 22 | I t = t

 25 | public export

 26 | data MetaCommit : Type where

 27 |   MC     : Commit -> MetaCommit

 28 |   Latest : Branch -> MetaCommit

 29 |   Fetch  : Branch -> MetaCommit

 31 | %runElab derive "MetaCommit" [Show,Eq]

 33 | public export

 34 | FromString MetaCommit where

 35 |   fromString s = case forget $ split (':' ==) s of

 36 |     ["latest",branch]       => Latest $ MkBranch branch

 37 |     ["fetch-latest",branch] => Fetch $ MkBranch branch

 38 |     _                       => MC $ MkCommit s

 41 | Interpolation MetaCommit where

 42 |   interpolate (Latest b) = "latest:\{b}"

 43 |   interpolate (Fetch b)  = "fetch-latest:\{b}"

 44 |   interpolate (MC c)     = "\{c}"

 47 | toLatest : MetaCommit -> MetaCommit

 48 | toLatest (MC x) = Latest (MkBranch x.value)

 49 | toLatest x      = x

 52 | public export

 53 | data FetchMethod : Type where

 54 |   ||| Update only meta commits, which don't have a cached entry in the

 56 |   MissingOnly  : FetchMethod

 58 |   ||| Update all custom commits. This is the strategy used with the `fetch`

 60 |   All          : FetchMethod

 62 |   ||| Remove the "commits" directory, thus forcing all meta commits to

 65 |   ClearCommits : FetchMethod

 67 | %runElab derive "FetchMethod" [Show,Eq,Ord]

 74 | public export

 75 | data CorePkg =

 76 |     Prelude

 77 |   | Base

 78 |   | Contrib

 79 |   | Linear

 80 |   | Network

 81 |   | Test

 82 |   | Papers

 83 |   | IdrisApi

 86 | public export

 87 | corePkgs : List CorePkg

 88 | corePkgs = [Prelude, Base, Contrib, Linear, Network, Test, Papers, IdrisApi]

 91 | Interpolation CorePkg where

 92 |   interpolate Prelude  = "prelude"

 93 |   interpolate Base     = "base"

 94 |   interpolate Contrib  = "contrib"

 95 |   interpolate Linear   = "linear"

 96 |   interpolate Network  = "network"

 97 |   interpolate Test     = "test"

 98 |   interpolate Papers   = "papers"

 99 |   interpolate IdrisApi = "idris2"

102 | Cast CorePkg Body where

103 |   cast Prelude  = "prelude"

104 |   cast Base     = "base"

105 |   cast Contrib  = "contrib"

106 |   cast Linear   = "linear"

107 |   cast Network  = "network"

108 |   cast Test     = "test"

109 |   cast Papers   = "papers"

110 |   cast IdrisApi = "idris2"

112 | export %inline

113 | Cast CorePkg (Path Rel) where

114 |   cast c = PRel [< cast c]

118 | corePkgName : CorePkg -> PkgName

119 | corePkgName = MkPkgName . interpolate

123 | coreIpkgFile : CorePkg -> Body

124 | coreIpkgFile IdrisApi = "idris2api.ipkg"

125 | coreIpkgFile c        = cast c <+> ".ipkg"

130 | coreIpkgPath : CorePkg -> File Rel

131 | coreIpkgPath IdrisApi = MkF neutral "idris2api.ipkg"

132 | coreIpkgPath c        = MkF (neutral /> "libs" //> c) (coreIpkgFile c)

136 | readCorePkg : String -> Maybe CorePkg

137 | readCorePkg "prelude" = Just Prelude

138 | readCorePkg "base"    = Just Base

139 | readCorePkg "contrib" = Just Contrib

140 | readCorePkg "linear"  = Just Linear

141 | readCorePkg "network" = Just Network

142 | readCorePkg "test"    = Just Test

143 | readCorePkg "papers"  = Just Papers

144 | readCorePkg "idris2"  = Just IdrisApi

145 | readCorePkg _         = Nothing

149 | isCorePkg : String -> Bool

150 | isCorePkg = isJust . readCorePkg

161 | public export

162 | data Package_ : (f : Type -> Type) -> (c : Type) -> Type where

163 |   ||| A Git repository, given as the package's URL,

168 |   Git :  (url      : f URL)

169 |       -> (commit   : f c)

170 |       -> (ipkg     : f $ File Rel)

171 |       -> (pkgPath  : f $ Bool)

172 |       -> (testIpkg : Maybe (File Rel))

173 |       -> (notice   : Maybe String)

174 |       -> Package_ f c

176 |   ||| A local Idris project given as an absolute path to a local

181 |   Local  :  (dir      : Path Abs)

182 |          -> (ipkg     : File Rel)

183 |          -> (pkgPath  : Bool)

184 |          -> (testIpkg : Maybe (File Rel))

185 |          -> Package_ f c

187 |   ||| A core package of the Idris2 project

188 |   Core   : (core : CorePkg) -> Package_ f c

191 | Functor (Package_ I) where

192 |   map f (Git u c i p t n) = Git u (f c) i p t n

193 |   map f (Local d i p t) = Local d i p t

194 |   map f (Core c)        = Core c

197 | traverse : Applicative f => (URL -> a -> f b) -> Package_ I a -> f (Package_ I b)

198 | traverse g (Git u c i p t n) = (\c' => Git u c' i p t n) <$> g u c

199 | traverse _ (Local d i p t)    = pure $ Local d i p t

200 | traverse _ (Core c)           = pure $ Core c

204 | public export

205 | 0 Package : Type

206 | Package = Package_ I Commit

210 | public export

211 | 0 UserPackage : Type

212 | UserPackage = Package_ Maybe MetaCommit

214 | public export

215 | 0 PackageMap : Type

216 | PackageMap = SortedMap PkgName Package

218 | public export

219 | 0 CustomMap : Type

220 | CustomMap = SortedMap DBName (SortedMap PkgName UserPackage)

223 | public export

224 | data IsCore : Package -> Type where

225 |   ItIsCore : IsCore (Core c)

228 | Uninhabited (IsCore $ Local {}) where

229 |   uninhabited _ impossible

232 | Uninhabited (IsCore $ Git {}) where

233 |   uninhabited _ impossible

238 | isCore : (p : Package) -> Dec (IsCore p)

239 | isCore (Core {})  = Yes ItIsCore

240 | isCore (Git {})   = No absurd

241 | isCore (Local {}) = No absurd

244 | public export

245 | data IsLocal : Package -> Type where

246 |   ItIsLocal : IsLocal (Local {})

249 | Uninhabited (IsLocal $ Core {}) where

250 |   uninhabited _ impossible

253 | Uninhabited (IsLocal $ Git {}) where

254 |   uninhabited _ impossible

259 | isLocal : (p : Package) -> Dec (IsLocal p)

260 | isLocal (Core {})  = No absurd

261 | isLocal (Git {})   = No absurd

262 | isLocal (Local {}) = Yes ItIsLocal

265 | public export

266 | data IsGit : Package -> Type where

267 |   ItIsGit : IsGit (Git {})

270 | Uninhabited (IsGit $ Core {}) where

271 |   uninhabited _ impossible

274 | Uninhabited (IsGit $ Local {}) where

275 |   uninhabited _ impossible

280 | isGit : (p : Package) -> Dec (IsGit p)

281 | isGit (Core {})  = No absurd

282 | isGit (Git {})   = Yes ItIsGit

283 | isGit (Local {}) = No absurd

288 | usePackagePath : Package_ I c -> Bool

289 | usePackagePath (Git _ _ _ pp _ _) = pp

290 | usePackagePath (Local _ _ pp _) = pp

291 | usePackagePath (Core _)         = False

295 | ipkg : (dir : Path Abs) -> Package -> File Abs

296 | ipkg dir (Git _ _ i _ _ _) = toAbsFile dir i

297 | ipkg dir (Local _ i _ _) = toAbsFile dir i

298 | ipkg dir (Core c)        = toAbsFile dir (coreIpkgPath c)

305 | public export

306 | data PkgStatus : Package -> Type where

307 |   Missing     : Hash -> PkgStatus p

308 |   Installed   : Hash -> (withDocs : Bool) -> PkgStatus p

311 | hash : PkgStatus p -> Hash

312 | hash (Missing h)     = h

313 | hash (Installed h _) = h

318 | public export

319 | record ResolvedLib t where

320 |   constructor RL

321 |   pkg     : Package

322 |   hash    : Hash

323 |   name    : PkgName

324 |   desc    : Desc t

325 |   status  : PkgStatus pkg

326 |   deps    : List (DPair Package PkgStatus)

328 | namespace ResolvedLib

329 |   ||| Extracts the package name from a resolved library.

330 |   export %inline

331 |   nameStr : ResolvedLib t -> String

332 |   nameStr = value . name

334 |   ||| Change the type-level tag of a resolved library.

335 |   export %inline

336 |   reTag : ResolvedLib s -> Desc t -> ResolvedLib t

337 |   reTag rl d = {desc := d} rl

339 |   ||| Extracts the dependencies of a resolved library.

340 |   export

341 |   dependencies : ResolvedLib t -> List PkgName

342 |   dependencies rp = dependencies rp.desc

344 |   ||| Check if the given library is installed

345 |   export

346 |   isInstalled : ResolvedLib t -> Bool

347 |   isInstalled rl = case rl.status of

348 |     Missing _ => False

349 |     _         => True

351 | namespace AppStatus

352 |   ||| Installation status of an Idris app.

353 |   public export

354 |   data AppStatus : Package -> Type where

355 |     ||| The app has not been compiled and is therfore missing

356 |     Missing      :  Hash -> AppStatus p

358 |     ||| The app has been built but is not on the `PATH`.

359 |     Installed    :  Hash -> AppStatus p

361 |     ||| The app has been built and a wrapper script has been added

363 |     BinInstalled :  Hash -> AppStatus p

368 | public export

369 | record ResolvedApp t where

370 |   constructor RA

371 |   pkg     : Package

372 |   hash    : Hash

373 |   name    : PkgName

374 |   desc    : Desc t

375 |   status  : AppStatus pkg

376 |   exec    : Body

377 |   deps    : List (DPair Package PkgStatus)

379 | namespace ResolveApp

380 |   ||| Extracts the package name from a resolved application.

381 |   export %inline

382 |   nameStr : ResolvedApp t -> String

383 |   nameStr = value . name

385 |   ||| Extracts the dependencies of a resolved application.

386 |   export

387 |   dependencies : ResolvedApp t -> List PkgName

388 |   dependencies rp = dependencies rp.desc

390 |   ||| Change the type-level tag of a resolved application.

391 |   export %inline

392 |   reTag : ResolvedApp s -> Desc t -> ResolvedApp t

393 |   reTag rl d = {desc := d} rl

395 |   ||| True, if the given application needs access to the

397 |   export %inline

398 |   usePackagePath : ResolvedApp t -> Bool

399 |   usePackagePath = usePackagePath . pkg

404 | public export

405 | data LibOrApp : (t,s : PkgDesc -> Type) -> Type where

406 |   Lib : ResolvedLib t -> LibOrApp t s

407 |   App : (withWrapperScript : Bool) -> ResolvedApp s -> LibOrApp t s

409 | namespace LibOrApp

410 |   ||| Extract the dependencies of a resolved library or application.

411 |   export

412 |   dependencies : LibOrApp t s -> List PkgName

413 |   dependencies (Lib x)   = dependencies x

414 |   dependencies (App _ x) = dependencies x

416 |   ||| Extract the package of a resolved library or application.

417 |   export

418 |   pkg : LibOrApp t s -> Package

419 |   pkg (Lib x)   = x.pkg

420 |   pkg (App _ x) = x.pkg

422 |   ||| Extract the description of a resolved library or application.

423 |   export

424 |   desc : LibOrApp t t -> Desc t

425 |   desc (Lib x)   = x.desc

426 |   desc (App _ x) = x.desc

428 |   ||| Extract the package name of a resolved library or application.

429 |   export

430 |   name : LibOrApp t s -> PkgName

431 |   name (Lib x)   = x.name

432 |   name (App _ x) = x.name

434 |   ||| Try to extract the package name of a resolved library.

435 |   export

436 |   libName : LibOrApp t s -> Maybe PkgName

437 |   libName (Lib x)   = Just x.name

438 |   libName (App _ _) = Nothing

447 | public export

448 | record DB_ c where

449 |   constructor MkDB

450 |   idrisURL     : URL

451 |   idrisCommit  : c

452 |   idrisVersion : PkgVersion

453 |   packages     : SortedMap PkgName (Package_ I c)

456 | Functor DB_ where

457 |   map f db = {

458 |       idrisCommit $= f

459 |     , packages    $= map (map f)

460 |     } db

462 | public export

463 | 0 DB : Type

464 | DB = DB_ Commit

466 | public export

467 | 0 MetaDB : Type

468 | MetaDB = DB_ MetaCommit

471 | export %inline

472 | setVersion : PkgVersion -> DB -> DB

473 | setVersion v = {idrisVersion := v}

477 | traverseDB :

478 |      {auto _ : Applicative f}

479 |   -> (URL -> a -> f b)

480 |   -> DB_ a

481 |   -> f (DB_ b)

482 | traverseDB g db =

483 |   let ic   := g db.idrisURL db.idrisCommit

484 |       pkgs := traverse (traverse g) db.packages

485 |    in [| adj ic pkgs |]

486 |     where

487 |       adj : b -> SortedMap PkgName (Package_ I b) -> DB_ b

488 |       adj ic cb = {idrisCommit := ic, packages := cb} db

490 | tomlBool : Bool -> String

491 | tomlBool True  = "true"

492 | tomlBool False = "false"

494 | testPath : Maybe (File Rel) -> Maybe String

495 | testPath = map (\x => "test        = \{quote x}")

497 | notice : Maybe String -> Maybe String

498 | notice = map (\x =>   "notice      = \{quote x}")

502 | printPair : (PkgName,Package) -> List String

503 | printPair (x, Git url commit ipkg pp t n) =

504 |   [ "[db.\{x}]"

505 |   , "type        = \"github\""

506 |   , "url         = \{quote url}"

507 |   , "commit      = \{quote commit}"

508 |   , "ipkg        = \{quote ipkg}"

509 |   , "packagePath = \{tomlBool pp}"

510 |   ] ++ (catMaybes [testPath t, notice n])

512 | printPair (x, Local dir ipkg pp t) =

513 |   [ "[db.\{x}]"

514 |   , "type        = \"local\""

515 |   , "path        = \{quote dir}"

516 |   , "ipkg        = \{quote ipkg}"

517 |   , "packagePath = \{tomlBool pp}"

518 |   ] ++ (catMaybes [testPath t])

520 | printPair (x, Core c) =

521 |   [ "[db.\{x}]"

522 |   , "type        = \"core\""

523 |   ]

527 | printDB : DB -> String

528 | printDB (MkDB u c v db) =

529 |   let header := """

535 |    in unlines $ header :: (SortedMap.toList db >>= \p => "" :: printPair p)

542 | mergeUP : UserPackage -> UserPackage -> UserPackage

543 | mergeUP (Git u1 c1 i1 p1 t1 n1) (Git u2 c2 i2 p2 t2 n2) =

544 |   Git (u1<|>u2)(c1<|>c2)(i1<|>i2)(p1<|>p2)(t1<|>t2)(n1<|>n2)

545 | mergeUP _ y = y

552 | 0 corePkgsTest : (c : CorePkg) -> Elem c Types.corePkgs

553 | corePkgsTest Prelude  = %search

554 | corePkgsTest Base     = %search

555 | corePkgsTest Contrib  = %search

556 | corePkgsTest Linear   = %search

557 | corePkgsTest Network  = %search

558 | corePkgsTest Test     = %search

559 | corePkgsTest Papers   = %search

560 | corePkgsTest IdrisApi = %search

564 | 0 corePkgRoundTrip : (c : CorePkg) -> readCorePkg (interpolate c) === Just c

565 | corePkgRoundTrip Prelude  = Refl

566 | corePkgRoundTrip Base     = Refl

567 | corePkgRoundTrip Contrib  = Refl

568 | corePkgRoundTrip Linear   = Refl

569 | corePkgRoundTrip Network  = Refl

570 | corePkgRoundTrip Test     = Refl

571 | corePkgRoundTrip Papers   = Refl

572 | corePkgRoundTrip IdrisApi = Refl