0 | module Pack.Config.Types

  2 | import Control.Monad.Either

  3 | import Data.Either

  4 | import Data.List

  5 | import Data.IORef

  6 | import public Data.List.Quantifiers

  7 | import Data.Maybe

  8 | import Data.SortedMap as SM

  9 | import Idris.Package.Types

 10 | import Libraries.Data.List.Extra

 11 | import Pack.Core.Git.Consts

 12 | import Pack.Core.Types

 13 | import Pack.Database.Types

 14 | import System.Clock

 16 | %default total

 20 | public export

 21 | data Autoload : Type where

 22 |   ||| Don't load any packages automatically (the default)

 23 |   NoPkgs    : Autoload

 25 |   ||| Load all installed packages of the current scope

 26 |   Installed : Autoload

 28 |   ||| Use the packages from the list of packages to be installed

 30 |   AutoLibs  : Autoload

 32 |   ||| Use the given explicit list of packages

 33 |   AutoPkgs  : List PkgName -> Autoload

 35 |   ||| Use the given explicit list of packages even in the

 37 |   ForcePkgs : List PkgName -> Autoload

 40 | public export

 41 | data QueryType : Type where

 42 |   ||| Display only the matching packages' names

 43 |   NameOnly     : QueryType

 45 |   ||| Display names and short descriptions

 46 |   ShortDesc    : QueryType

 48 |   ||| List direct dependencies

 49 |   Dependencies : QueryType

 51 |   ||| Print the full `.ipkg` file

 52 |   Ipkg         : QueryType

 54 |   ||| List detailed information about a package

 55 |   Details      : QueryType

 57 |   ||| Print dependency tree

 58 |   Tree         : QueryType

 60 |   ||| Print inverse dependency tree

 62 |   ReverseTree  : QueryType

 65 | public export

 66 | data Codegen : Type where

 67 |   Default    : Codegen

 68 |   Chez       : Codegen

 69 |   ChezSep    : Codegen

 70 |   Racket     : Codegen

 71 |   Gambit     : Codegen

 72 |   Node       : Codegen

 73 |   JavaScript : Codegen

 74 |   RefC       : Codegen

 75 |   VMCode     : Codegen

 76 |   Other      : String -> Codegen

 79 | Interpolation Codegen where

 80 |   interpolate Default    = ""

 81 |   interpolate Chez       = "chez"

 82 |   interpolate ChezSep    = "chez-sep"

 83 |   interpolate Racket     = "racket"

 84 |   interpolate Gambit     = "gambit"

 85 |   interpolate Node       = "node"

 86 |   interpolate JavaScript = "javascript"

 87 |   interpolate RefC       = "refc"

 88 |   interpolate VMCode     = "vmcode-interp"

 89 |   interpolate (Other x)  = x

 91 | public export

 92 | fromString : String -> Codegen

 93 | fromString "chez"          = Chez

 94 | fromString "chez-sep"      = ChezSep

 95 | fromString "racket"        = Racket

 96 | fromString "gambit"        = Gambit

 97 | fromString "node"          = Node

 98 | fromString "javascript"    = JavaScript

 99 | fromString "refc"          = RefC

100 | fromString "vmcode-interp" = VMCode

101 | fromString x               = Other x

110 | public export

111 | data WithIpkg : Type where

112 |   ||| Search for an `.ipkg` file in a parent directory.

117 |   Search : (dir : CurDir) -> WithIpkg

119 |   ||| Don't use an `.ipkg` file.

120 |   None   : WithIpkg

122 |   ||| Use the given `.ipkg` file, provided as a command line

124 |   Use    : (ipkg : File Abs) -> WithIpkg

132 | public export

133 | data RlwrapConfig : Type where

134 |   DoNotUseRlwrap : RlwrapConfig

135 |   UseRlwrap      : CmdArgList -> RlwrapConfig

138 | public export

139 | 0 I : Type -> Type

140 | I t = t

152 | public export

153 | record Config_ (f : Type -> Type) (c : Type) where

154 |   constructor MkConfig

155 |   ||| Package collection to use

156 |   collection   : f DBName

158 |   ||| URL to a custom Idris repo

161 |   idrisURL     : Maybe URL

163 |   ||| Custom Idris commit

166 |   idrisCommit  : Maybe c

168 |   ||| All Idris commits mentioned in used configs

169 |   allIdrisCommits : List c

171 |   ||| Custom pack repo

172 |   packURL      : Maybe URL

174 |   ||| Custom pack branch to use (default is `main`)

175 |   packCommit   : Maybe c

177 |   ||| Scheme executable to use

178 |   scheme       : f FilePath

180 |   ||| Whether to bootstrap when building Idris2

181 |   bootstrap    : f Bool

183 |   ||| Whether to rebuild Idris2 with the stage 2 compiler

184 |   bootstrapStage3 : f Bool

186 |   ||| Whether to prompt for a confirmation when

189 |   safetyPrompt : f Bool

191 |   ||| Whether to prompt for a confirmation when

194 |   gcPrompt : f Bool

196 |   ||| Whether to remove not only stuff compiled with outdated version

199 |   gcPurge : f Bool

201 |   ||| Whether to issue a warning in precense of a local `depends` directory

202 |   warnDepends : f Bool

204 |   ||| Whether to skip tests during collection checking

205 |   skipTests : f Bool

207 |   ||| List of package names, for which we will not issue a safety prompt

210 |   whitelist    : f (List PkgName)

212 |   ||| Whether to install the library sources as well

213 |   withSrc      : f Bool

215 |   ||| Whether to install the library docs as well

216 |   withDocs     : f Bool

218 |   ||| Whether to use katla to add semantically highlighted source code

220 |   useKatla     : f Bool

222 |   ||| The `.ipkg` file to use (if any) when starting a REPL session

223 |   withIpkg     : f WithIpkg

225 |   ||| Whether to use `rlwrap` to run a REPL session

226 |   rlwrap       : f RlwrapConfig

228 |   ||| Any extra arguments to pass to Idris2 executable.

229 |   extraArgs    : f CmdArgList

231 |   ||| Libraries to install automatically

232 |   autoLibs     : f (List PkgName)

234 |   ||| Applications to install automatically

235 |   autoApps     : f (List PkgName)

237 |   ||| Libraries to automatically load in a REPL session

238 |   autoLoad     : f Autoload

240 |   ||| Customizations to the package data base

241 |   custom       : f (SortedMap DBName (SortedMap PkgName $ Package_ c))

243 |   ||| Type of query to run

244 |   queryType    : f (QueryType)

246 |   ||| Verbosity of the Log

247 |   logLevel     : f (LogLevel)

249 |   ||| Codegen to use

250 |   codegen      : f (Codegen)

252 |   ||| Name of output file when compiling Idris source files

253 |   output       : f Body

255 |   ||| Default LogLevels for different commands

256 |   levels       : f (SortedMap String LogLevel)

258 |   ||| Whether to initialize git.

259 |   gitInit      : f Bool

262 | public export

263 | 0 IConfig : Type -> Type

264 | IConfig = Config_ I

267 | public export

268 | 0 MConfig : Type -> Type

269 | MConfig = Config_ Maybe

272 | public export

273 | 0 MetaConfig : Type

274 | MetaConfig = IConfig MetaCommit

277 | public export

278 | 0 Config : Type

279 | Config = IConfig Commit

282 | public export

283 | 0 UserConfig : Type

284 | UserConfig = MConfig MetaCommit

290 | traverse :  Applicative f

291 |          => (URL -> a -> f b)

292 |          -> (idrisURL : URL)

293 |          -> Config_ I a

294 |          -> f (Config_ I b)

295 | traverse g idrisURL cfg =

296 |   let iurl = fromMaybe idrisURL cfg.idrisURL

297 |       purl = fromMaybe defaultPackRepo cfg.packURL

298 |       cst = traverse (traverse $ traverse g) cfg.custom

299 |       ic  = traverse (g iurl) cfg.idrisCommit

300 |       ics = traverse (g iurl) cfg.allIdrisCommits

301 |       pc  = traverse (g purl) cfg.packCommit

302 |    in [| adj ic ics pc cst |]

303 |     where adj :  (idrisCommit : Maybe b)

304 |               -> (allidrisCommits : List b)

305 |               -> (packCommit  : Maybe b)

306 |               -> SortedMap DBName (SortedMap PkgName $ Package_ b)

307 |               -> Config_ I b

308 |           adj ic ics pc cb =

309 |             { idrisCommit     := ic

310 |             , allIdrisCommits := ics

311 |             , packCommit      := pc

312 |             , custom          := cb

313 |             } cfg

317 | export %inline %hint

318 | configToLogRef : (c : Config) => LogRef

319 | configToLogRef = MkLogRef c.logLevel

323 | export %inline %hint

324 | metaConfigToLogRef : (c : MetaConfig) => LogRef

325 | metaConfigToLogRef = MkLogRef c.logLevel

331 | export infixl 8 `mergeRight`

334 | mergeRight : SortedMap k v -> SortedMap k v -> SortedMap k v

335 | mergeRight = mergeWith (\_,v => v)

339 | init : (cur : CurDir) => (coll : DBName) -> MetaConfig

340 | init coll = MkConfig {

341 |     collection      = coll

342 |   , idrisURL        = Nothing

343 |   , idrisCommit     = Nothing

344 |   , allIdrisCommits = []

345 |   , packURL         = Nothing

346 |   , packCommit      = Nothing

347 |   , scheme          = "scheme"

348 |   , bootstrap       = False

349 |   , bootstrapStage3 = True

350 |   , safetyPrompt    = True

351 |   , gcPrompt        = True

352 |   , gcPurge         = False

353 |   , warnDepends     = True

354 |   , skipTests       = False

355 |   , whitelist       = ["pack", "idris2-lsp"]

356 |   , withSrc         = True

357 |   , withDocs        = False

358 |   , useKatla        = False

359 |   , withIpkg        = Search cur

360 |   , rlwrap          = DoNotUseRlwrap

361 |   , extraArgs       = []

362 |   , autoLibs        = []

363 |   , autoApps        = []

364 |   , autoLoad        = NoPkgs

365 |   , custom          = empty

366 |   , queryType       = NameOnly

367 |   , logLevel        = Warning

368 |   , codegen         = Default

369 |   , output          = "_tmppack"

370 |   , levels          = empty

371 |   , gitInit         = False

372 |   }

374 | export infixl 7 `update`

378 | update : IConfig c -> MConfig c -> IConfig c

379 | update ci cm = MkConfig {

380 |     collection      = fromMaybe ci.collection cm.collection

381 |   , idrisURL        = cm.idrisURL <|> ci.idrisURL

382 |   , idrisCommit     = cm.idrisCommit <|> ci.idrisCommit

383 |   , allIdrisCommits = cm.allIdrisCommits <+> ci.allIdrisCommits

384 |   , packURL         = cm.packURL <|> ci.packURL

385 |   , packCommit      = cm.packCommit <|> ci.packCommit

386 |   , scheme          = fromMaybe ci.scheme cm.scheme

387 |   , bootstrap       = fromMaybe ci.bootstrap cm.bootstrap

388 |   , bootstrapStage3 = fromMaybe ci.bootstrapStage3 cm.bootstrapStage3

389 |   , safetyPrompt    = fromMaybe ci.safetyPrompt cm.safetyPrompt

390 |   , gcPrompt        = fromMaybe ci.gcPrompt cm.gcPrompt

391 |   , gcPurge         = fromMaybe ci.gcPurge cm.gcPurge

392 |   , warnDepends     = fromMaybe ci.warnDepends cm.warnDepends

393 |   , skipTests       = fromMaybe ci.skipTests cm.skipTests

394 |   , withSrc         = fromMaybe ci.withSrc cm.withSrc

395 |   , withDocs        = fromMaybe ci.withDocs cm.withDocs

396 |   , useKatla        = fromMaybe ci.useKatla cm.useKatla

397 |   , withIpkg        = fromMaybe ci.withIpkg cm.withIpkg

398 |   , rlwrap          = fromMaybe ci.rlwrap cm.rlwrap

399 |   , extraArgs       = ci.extraArgs <+> fromMaybe [] cm.extraArgs

400 |   , whitelist       = sortedNub (ci.whitelist ++ concat cm.whitelist)

401 |   , autoLibs        = sortedNub (ci.autoLibs ++ concat cm.autoLibs)

402 |   , autoApps        = sortedNub (ci.autoApps ++ concat cm.autoApps)

403 |   , autoLoad        = fromMaybe ci.autoLoad cm.autoLoad

404 |   , custom          = mergeWith mergeRight ci.custom (fromMaybe empty cm.custom)

405 |   , queryType       = fromMaybe ci.queryType cm.queryType

406 |   , logLevel        = fromMaybe ci.logLevel cm.logLevel

407 |   , codegen         = fromMaybe ci.codegen cm.codegen

408 |   , output          = fromMaybe ci.output cm.output

409 |   , levels          = mergeWith (\_,v => v) ci.levels (fromMaybe empty cm.levels)

410 |   , gitInit         = fromMaybe ci.gitInit cm.gitInit

411 |   }

419 | public export

420 | data HasIdris : Config -> DB -> Type where

421 |   [noHints]

422 |   ItHasIdris : {0 c : _} -> {0 db : _} -> HasIdris c db

429 | public export

430 | 0 LibCache : Type

431 | LibCache = IORef (SortedMap PkgName $ ResolvedLib U)

435 | emptyCache : HasIO io => io LibCache

436 | emptyCache = newIORef SortedMap.empty

440 | cacheLib :  HasIO io

441 |          => (ref : LibCache)

442 |          => PkgName

443 |          -> ResolvedLib U

444 |          -> io (ResolvedLib U)

445 | cacheLib n lib = modifyIORef ref (insert n lib) $> lib

449 | lookupLib :  HasIO io

450 |           => (ref : LibCache)

451 |           => PkgName

452 |           -> io (Maybe $ ResolvedLib U)

453 | lookupLib n = lookup n <$> readIORef ref

457 | uncacheLib : HasIO io => (ref : LibCache) => PkgName -> io ()

458 | uncacheLib n = modifyIORef ref (delete n)

464 | public export

465 | record Env where

466 |   constructor MkEnv

467 |   packDirs : PackDirs

468 |   tmpDir   : TmpDir

469 |   config   : Config

470 |   cache    : LibCache

471 |   db       : DB -- pack collection

472 |   all      : SortedMap PkgName Package -- packages merged from config and db

473 |   linebuf  : LineBufferingCmd

474 |   clock    : Clock UTC

478 | nanoString : (e : Env) => String

479 | nanoString = show $ toNano e.clock

483 | export %inline %hint

484 | envToPackDirs : (e : Env) => PackDirs

485 | envToPackDirs = e.packDirs

489 | export %inline %hint

490 | envToTmpDir : (e : Env) => TmpDir

491 | envToTmpDir = e.tmpDir

495 | export %inline %hint

496 | envToCache : (e : Env) => LibCache

497 | envToCache = e.cache

501 | export %inline %hint

502 | envToConfig : (e : Env) => Config

503 | envToConfig = e.config

507 | export %inline %hint

508 | envToDB : (e : Env) => DB

509 | envToDB = e.db

513 | export %inline %hint

514 | envToLinebuf : (e : Env) => LineBufferingCmd

515 | envToLinebuf = e.linebuf

519 | public export

520 | record IdrisEnv where

521 |   constructor MkIdrisEnv

522 |   env   : Env

523 |   ttc   : TTCVersion

524 |   0 prf : HasIdris env.config env.db

528 | export %inline %hint

529 | idrisEnvToEnv : (e : IdrisEnv) => Env

530 | idrisEnvToEnv = e.env

534 | export %inline %hint

535 | idrisEnvToTTC : (e : IdrisEnv) => TTCVersion

536 | idrisEnvToTTC = e.ttc

543 | public export

544 | interface Arg (0 a : Type) where

545 |   argDesc_ : String

546 |   readArg  : List String -> Maybe (a, List String)

549 | public export %inline

550 | argDesc : (0 a : Type) -> Arg a => String

551 | argDesc a = argDesc_ {a}

555 | parseSingleMaybe :  (read : String -> Maybe a)

556 |                  -> List String

557 |                  -> Maybe (a, List String)

558 | parseSingleMaybe read []       = Nothing

559 | parseSingleMaybe read (h :: t) = (,t) <$> read h

562 | export %inline

563 | parseSingle :  (read : String -> Either e a)

564 |             -> List String

565 |             -> Maybe (a, List String)

566 | parseSingle read = parseSingleMaybe (eitherToMaybe . read)

569 | export %inline

570 | readSingle :  (read : String -> a) -> List String -> Maybe (a, List String)

571 | readSingle read = parseSingleMaybe (Just . read)

574 | Arg a => Arg (Maybe a) where

575 |   argDesc_ = "[\{argDesc a}]"

577 |   readArg ss = case readArg {a} ss of

578 |     Nothing      => Just (Nothing, ss)

579 |     Just (v,ss') => Just (Just v, ss')

582 | (cd : CurDir) => Arg (File Abs) where

583 |   argDesc_ = "<file>"

584 |   readArg = parseSingle (readAbsFile curDir)

587 | (cd : CurDir) => Arg (Path Abs) where

588 |   argDesc_ = "<dir>"

589 |   readArg = readSingle (\s => parse s curDir)

592 | (cd : CurDir) => Arg PkgOrIpkg where

593 |   argDesc_ = "<pkg or .ipkg>"

594 |   readArg = readSingle $ \s => case readAbsFile curDir s of

595 |     Left  _ => Pkg $ MkPkgName s

596 |     Right f =>

597 |       if isIpkgBody f.file

598 |            then Ipkg f

599 |            else Pkg $ MkPkgName s

601 | export %inline

602 | Arg PkgName where

603 |   argDesc_ = "<pkg>"

604 |   readArg = readSingle MkPkgName

606 | export %inline

607 | Arg PkgType where

608 |   argDesc_ = "<lib | bin>"

609 |   readArg = parseSingle readPkgType

611 | export %inline

612 | Arg CmdArgList where

613 |   argDesc_ = "[<args>]"

614 |   readArg ss = Just (fromStrList ss, [])

616 | export %inline

617 | Arg (List PkgName) where

618 |   argDesc_ = "[<pkgs>]"

619 |   readArg ss = Just (map MkPkgName ss, [])

621 | export %inline

622 | Arg Body where

623 |   argDesc_ = "<file name>"

624 |   readArg = parseSingle readBody

626 | export %inline

627 | Arg DBName where

628 |   argDesc_ = "<db>"

629 |   readArg = parseSingle readDBName

631 | export %inline

632 | Arg String where

633 |   argDesc_ = "<str>"

634 |   readArg = readSingle id

652 | public export

653 | interface Command c where

654 |   ||| The command to use if only command line options but

656 |   defaultCommand : c

658 |   ||| Name of the application in question

659 |   appName : String

661 |   ||| Name of command in question

662 |   cmdName : c -> String

664 |   ||| The default log level to use.

665 |   defaultLevel    : c -> LogLevel

667 |   ||| Detailed usage description of the command

668 |   desc : c -> String

670 |   ||| General usage of the application in question

671 |   usage : Lazy String

673 |   ||| Types of arguments required by the given command

674 |   0 ArgTypes : c -> List Type

676 |   ||| Tries to read a command from a String

677 |   readCommand_ : String -> Maybe c

679 |   ||| List of argument readers for the current command

680 |   readArgs : CurDir => (cmd : c) -> All Arg (ArgTypes cmd)

682 |   ||| Some commands overwrite certain aspects of the user-defined

686 |   adjConfig_ :  HasIO io

687 |              => PackDirs

688 |              => TmpDir

689 |              => (cmd : c)

690 |              -> All I (ArgTypes cmd)

691 |              -> MetaConfig

692 |              -> EitherT PackErr io MetaConfig

694 | args : All Arg ts -> CurDir => List String -> Maybe (All I ts)

695 | args [] []       = Just []

696 | args [] (_ :: _) = Nothing

697 | args {ts = x :: xs} (p :: ps) ss = do

698 |   (v,ss') <- readArg {a = x} ss

699 |   vs      <- args ps ss'

700 |   pure (v :: vs)

702 | argsDesc : CurDir => Command c => Maybe c -> String

703 | argsDesc Nothing  = " [<args>]"

704 | argsDesc (Just x) = fastConcat $ go (readArgs x)

705 |   where go : All Arg ts -> List String

706 |         go = forget . mapProperty (\p => " " ++ argDesc_ @{p})

710 | usageHeader : CurDir => Command c => Maybe c -> String

711 | usageHeader cmd =

712 |   let nm      := maybe "<cmd>" cmdName cmd

713 |    in "Usage: \{appName {c}} [options] \{nm}\{argsDesc cmd}"

715 | ind : String -> String

716 | ind = unlines . map (indent 2) . lines

723 | usageDesc : CurDir => Command c => Maybe c -> String

724 | usageDesc m = case m of

725 |   Just cmd =>

726 |     """

732 |   Nothing =>

733 |     """

740 | public export

741 | 0 Args : Command c => c -> Type

742 | Args cmd = All I (ArgTypes cmd)

745 | public export

746 | 0 CommandWithArgs : (c : Type) -> Command c => Type

747 | CommandWithArgs c = DPair c Args

749 | readCWA :  Command c

750 |         => CurDir

751 |         => (cmd : c)

752 |         -> List String

753 |         -> Either PackErr (CommandWithArgs c)

754 | readCWA x ss =

755 |   let readers := readArgs x

756 |       Just as := args readers ss

757 |         | Nothing => Left (InvalidCmdArgs (cmdName x) ss $ usageHeader $ Just x)

758 |    in Right (x ** as)

763 | readCommand :  (0 c : Type)

764 |             -> Command c

765 |             => CurDir

766 |             -> List String

767 |             -> Either PackErr (CommandWithArgs c)

768 | readCommand c cd []       = readCWA defaultCommand []

769 | readCommand c cd (h :: t) = case readCommand_ {c} h of

770 |   Nothing => Left (UnknownCommand h $ usageDesc {c} Nothing)

771 |   Just x  => readCWA x t

777 | export %inline

778 | adjConfig :  HasIO io

779 |           => Command c

780 |           => PackDirs

781 |           => TmpDir

782 |           => CommandWithArgs c

783 |           -> MetaConfig

784 |           -> EitherT PackErr io MetaConfig

785 | adjConfig (command ** args) = adjConfig_ command args