0 | module Pack.Database.Types

  2 | import Core.Name.Namespace

  3 | import Data.List1

  4 | import Data.List.Elem

  5 | import Data.SortedMap

  6 | import Data.String

  7 | import Derive.Prelude

  8 | import Idris.Package.Types

  9 | import Pack.Core.Types

 11 | %default total

 12 | %language ElabReflection

 19 | public export

 20 | data MetaCommit : Type where

 21 |   MC     : Commit -> MetaCommit

 22 |   Latest : Branch -> MetaCommit

 23 |   Fetch  : Branch -> MetaCommit

 25 | public export

 26 | FromString MetaCommit where

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

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

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

 30 |     _                       => MC $ MkCommit s

 33 | Interpolation MetaCommit where

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

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

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

 39 | toLatest : MetaCommit -> MetaCommit

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

 41 | toLatest x      = x

 44 | public export

 45 | data FetchMethod : Type where

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

 48 |   MissingOnly  : FetchMethod

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

 52 |   All          : FetchMethod

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

 57 |   ClearCommits : FetchMethod

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

 66 | public export

 67 | data CorePkg =

 68 |     Prelude

 69 |   | Base

 70 |   | Contrib

 71 |   | Linear

 72 |   | Network

 73 |   | Test

 74 |   | Papers

 75 |   | IdrisApi

 78 | public export

 79 | corePkgs : List CorePkg

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

 83 | Interpolation CorePkg where

 84 |   interpolate Prelude  = "prelude"

 85 |   interpolate Base     = "base"

 86 |   interpolate Contrib  = "contrib"

 87 |   interpolate Linear   = "linear"

 88 |   interpolate Network  = "network"

 89 |   interpolate Test     = "test"

 90 |   interpolate Papers   = "papers"

 91 |   interpolate IdrisApi = "idris2"

 94 | Cast CorePkg Body where

 95 |   cast Prelude  = "prelude"

 96 |   cast Base     = "base"

 97 |   cast Contrib  = "contrib"

 98 |   cast Linear   = "linear"

 99 |   cast Network  = "network"

100 |   cast Test     = "test"

101 |   cast Papers   = "papers"

102 |   cast IdrisApi = "idris2"

104 | export %inline

105 | Cast CorePkg (Path Rel) where

106 |   cast c = PRel [< cast c]

110 | corePkgName : CorePkg -> PkgName

111 | corePkgName = MkPkgName . interpolate

115 | coreIpkgFile : CorePkg -> Body

116 | coreIpkgFile IdrisApi = "idris2api.ipkg"

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

122 | coreIpkgPath : CorePkg -> File Rel

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

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

128 | readCorePkg : String -> Maybe CorePkg

129 | readCorePkg "prelude" = Just Prelude

130 | readCorePkg "base"    = Just Base

131 | readCorePkg "contrib" = Just Contrib

132 | readCorePkg "linear"  = Just Linear

133 | readCorePkg "network" = Just Network

134 | readCorePkg "test"    = Just Test

135 | readCorePkg "papers"  = Just Papers

136 | readCorePkg "idris2"  = Just IdrisApi

137 | readCorePkg _         = Nothing

141 | isCorePkg : String -> Bool

142 | isCorePkg = isJust . readCorePkg

153 | public export

154 | data Package_ : (c : Type) -> Type where

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

160 |   Git :  (url      : URL)

161 |       -> (commit   : c)

162 |       -> (ipkg     : File Rel)

163 |       -> (pkgPath  : Bool)

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

165 |       -> (notice   : Maybe String)

166 |       -> Package_ c

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

173 |   Local  :  (dir      : Path Abs)

174 |          -> (ipkg     : File Rel)

175 |          -> (pkgPath  : Bool)

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

177 |          -> Package_ c

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

180 |   Core   : (core : CorePkg) -> Package_ c

183 | Functor Package_ where

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

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

186 |   map f (Core c)        = Core c

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

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

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

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

196 | public export

197 | 0 Package : Type

198 | Package = Package_ Commit

202 | public export

203 | 0 UserPackage : Type

204 | UserPackage = Package_ MetaCommit

207 | public export

208 | data IsCore : Package -> Type where

209 |   ItIsCore : IsCore (Core c)

212 | Uninhabited (IsCore $ Local {}) where

213 |   uninhabited _ impossible

216 | Uninhabited (IsCore $ Git {}) where

217 |   uninhabited _ impossible

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

223 | isCore (Core {})  = Yes ItIsCore

224 | isCore (Git {})   = No absurd

225 | isCore (Local {}) = No absurd

228 | public export

229 | data IsLocal : Package -> Type where

230 |   ItIsLocal : IsLocal (Local {})

233 | Uninhabited (IsLocal $ Core {}) where

234 |   uninhabited _ impossible

237 | Uninhabited (IsLocal $ Git {}) where

238 |   uninhabited _ impossible

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

244 | isLocal (Core {})  = No absurd

245 | isLocal (Git {})   = No absurd

246 | isLocal (Local {}) = Yes ItIsLocal

249 | public export

250 | data IsGit : Package -> Type where

251 |   ItIsGit : IsGit (Git {})

254 | Uninhabited (IsGit $ Core {}) where

255 |   uninhabited _ impossible

258 | Uninhabited (IsGit $ Local {}) where

259 |   uninhabited _ impossible

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

265 | isGit (Core {})  = No absurd

266 | isGit (Git {})   = Yes ItIsGit

267 | isGit (Local {}) = No absurd

272 | usePackagePath : Package_ c -> Bool

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

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

275 | usePackagePath (Core _)         = False

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

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

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

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

289 | public export

290 | data PkgStatus : Package -> Type where

291 |   Missing     : Hash -> PkgStatus p

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

295 | hash : PkgStatus p -> Hash

296 | hash (Missing h)     = h

297 | hash (Installed h _) = h

302 | public export

303 | record ResolvedLib t where

304 |   constructor RL

305 |   pkg     : Package

306 |   hash    : Hash

307 |   name    : PkgName

308 |   desc    : Desc t

309 |   status  : PkgStatus pkg

310 |   deps    : List (DPair Package PkgStatus)

312 | namespace ResolvedLib

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

314 |   export %inline

315 |   nameStr : ResolvedLib t -> String

316 |   nameStr = value . name

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

319 |   export %inline

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

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

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

324 |   export

325 |   dependencies : ResolvedLib t -> List PkgName

326 |   dependencies rp = dependencies rp.desc

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

329 |   export

330 |   isInstalled : ResolvedLib t -> Bool

331 |   isInstalled rl = case rl.status of

332 |     Missing _ => False

333 |     _         => True

335 | namespace AppStatus

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

337 |   public export

338 |   data AppStatus : Package -> Type where

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

340 |     Missing      :  Hash -> AppStatus p

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

343 |     Installed    :  Hash -> AppStatus p

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

347 |     BinInstalled :  Hash -> AppStatus p

352 | public export

353 | record ResolvedApp t where

354 |   constructor RA

355 |   pkg     : Package

356 |   hash    : Hash

357 |   name    : PkgName

358 |   desc    : Desc t

359 |   status  : AppStatus pkg

360 |   exec    : Body

361 |   deps    : List (DPair Package PkgStatus)

363 | namespace ResolveApp

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

365 |   export %inline

366 |   nameStr : ResolvedApp t -> String

367 |   nameStr = value . name

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

370 |   export

371 |   dependencies : ResolvedApp t -> List PkgName

372 |   dependencies rp = dependencies rp.desc

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

375 |   export %inline

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

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

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

381 |   export %inline

382 |   usePackagePath : ResolvedApp t -> Bool

383 |   usePackagePath = usePackagePath . pkg

388 | public export

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

390 |   Lib : ResolvedLib t -> LibOrApp t s

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

393 | namespace LibOrApp

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

395 |   export

396 |   dependencies : LibOrApp t s -> List PkgName

397 |   dependencies (Lib x)   = dependencies x

398 |   dependencies (App _ x) = dependencies x

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

401 |   export

402 |   pkg : LibOrApp t s -> Package

403 |   pkg (Lib x)   = x.pkg

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

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

407 |   export

408 |   desc : LibOrApp t t -> Desc t

409 |   desc (Lib x)   = x.desc

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

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

413 |   export

414 |   name : LibOrApp t s -> PkgName

415 |   name (Lib x)   = x.name

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

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

419 |   export

420 |   libName : LibOrApp t s -> Maybe PkgName

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

422 |   libName (App _ _) = Nothing

431 | public export

432 | record DB_ c where

433 |   constructor MkDB

434 |   idrisURL     : URL

435 |   idrisCommit  : c

436 |   idrisVersion : PkgVersion

437 |   packages     : SortedMap PkgName (Package_ c)

440 | Functor DB_ where

441 |   map f db = {

442 |       idrisCommit $= f

443 |     , packages    $= map (map f)

444 |     } db

446 | public export

447 | 0 DB : Type

448 | DB = DB_ Commit

450 | public export

451 | 0 MetaDB : Type

452 | MetaDB = DB_ MetaCommit

455 | export %inline

456 | setVersion : PkgVersion -> DB -> DB

457 | setVersion v = {idrisVersion := v}

461 | traverseDB :

462 |      {auto _ : Applicative f}

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

464 |   -> DB_ a

465 |   -> f (DB_ b)

466 | traverseDB g db =

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

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

469 |    in [| adj ic pkgs |]

470 |     where

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

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

474 | tomlBool : Bool -> String

475 | tomlBool True  = "true"

476 | tomlBool False = "false"

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

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

481 | notice : Maybe String -> Maybe String

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

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

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

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

489 |   , "type        = \"github\""

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

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

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

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

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

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

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

498 |   , "type        = \"local\""

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

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

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

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

504 | printPair (x, Core c) =

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

506 |   , "type        = \"core\""

507 |   ]

511 | printDB : DB -> String

512 | printDB (MkDB u c v db) =

513 |   let header := """

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

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

527 | corePkgsTest Prelude  = %search

528 | corePkgsTest Base     = %search

529 | corePkgsTest Contrib  = %search

530 | corePkgsTest Linear   = %search

531 | corePkgsTest Network  = %search

532 | corePkgsTest Test     = %search

533 | corePkgsTest Papers   = %search

534 | corePkgsTest IdrisApi = %search

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

539 | corePkgRoundTrip Prelude  = Refl

540 | corePkgRoundTrip Base     = Refl

541 | corePkgRoundTrip Contrib  = Refl

542 | corePkgRoundTrip Linear   = Refl

543 | corePkgRoundTrip Network  = Refl

544 | corePkgRoundTrip Test     = Refl

545 | corePkgRoundTrip Papers   = Refl

546 | corePkgRoundTrip IdrisApi = Refl