
   0 | module Pack.Config.Types
   1 | 
   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
  15 | 
  16 | %default total
  17 | 
  18 | ||| Packages to automatically load in a REPL session
  19 | ||| in absence of an `.ipkg` file in scope.
  20 | public export
  21 | data Autoload : Type where
  22 |   ||| Don't load any packages automatically (the default)
  23 |   NoPkgs    : Autoload
  24 | 
  25 |   ||| Load all installed packages of the current scope
  26 |   Installed : Autoload
  27 | 
  28 |   ||| Use the packages from the list of packages to be installed
  29 |   ||| automatically
  30 |   AutoLibs  : Autoload
  31 | 
  32 |   ||| Use the given explicit list of packages
  33 |   AutoPkgs  : List PkgName -> Autoload
  34 | 
  35 |   ||| Use the given explicit list of packages even in the
  36 |   ||| presence of an `.ipkg` file.
  37 |   ForcePkgs : List PkgName -> Autoload
  38 | 
  39 | ||| What to show when querying the data base
  40 | public export
  41 | data QueryType : Type where
  42 |   ||| Display only the matching packages' names
  43 |   NameOnly     : QueryType
  44 | 
  45 |   ||| Display names and short descriptions
  46 |   ShortDesc    : QueryType
  47 | 
  48 |   ||| List direct dependencies
  49 |   Dependencies : QueryType
  50 | 
  51 |   ||| Print the full `.ipkg` file
  52 |   Ipkg         : QueryType
  53 | 
  54 |   ||| List detailed information about a package
  55 |   Details      : QueryType
  56 | 
  57 |   ||| Print dependency tree
  58 |   Tree         : QueryType
  59 | 
  60 |   ||| Print inverse dependency tree
  61 |   ||| (That is, a tree of packages depending on a given package)
  62 |   ReverseTree  : QueryType
  63 | 
  64 | ||| Code generator to use
  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
  77 | 
  78 | export
  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
  90 | 
  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
 102 | 
 103 | ||| Data type describing whether to search for an `.ipkg`
 104 | ||| file in one of the parent directories (the default), not
 105 | ||| to use an `.ipkg` file at all, or to use the one provided at
 106 | ||| the command line.
 107 | |||
 108 | ||| This is only relevant when working with Idris source files
 109 | ||| directly, for instance when loading them into a REPL session.
 110 | public export
 111 | data WithIpkg : Type where
 112 |   ||| Search for an `.ipkg` file in a parent directory.
 113 |   ||| If an `.idr` file is provided, the parent directories
 114 |   ||| of this file will be searched. If no `.idr` file is
 115 |   ||| given, the current working directory will be search,
 116 |   ||| which is given as an argument to this constructor.
 117 |   Search : (dir : CurDir) -> WithIpkg
 118 | 
 119 |   ||| Don't use an `.ipkg` file.
 120 |   None   : WithIpkg
 121 | 
 122 |   ||| Use the given `.ipkg` file, provided as a command line
 123 |   ||| argument.
 124 |   Use    : (ipkg : File Abs) -> WithIpkg
 125 | 
 126 | ||| Data type describing whether `rlwrap` command should be used
 127 | ||| and which additional arguments should be passed to it.
 128 | |||
 129 | ||| This is basically equivalent to `Maybe CmdArgList`, but
 130 | ||| separate type disallows confusion with `Maybe` from `MConfig`,
 131 | ||| i.e. between not being set and set to not to use `rlwrap`.
 132 | public export
 133 | data RlwrapConfig : Type where
 134 |   DoNotUseRlwrap : RlwrapConfig
 135 |   UseRlwrap      : CmdArgList -> RlwrapConfig
 136 | 
 137 | ||| User-defined configuration
 138 | |||
 139 | ||| @ f : This is used to represent the context of values.
 140 | |||       When we use the config as an environment for running pack
 141 | |||       programs, the context will be set to `I` (the identity function
 142 | |||       for types). This means, all fields will be mandatory.
 143 | |||       For updating the configuration from a `pack.toml` file,
 144 | |||       we use context `Maybe`, because all values will be optional.
 145 | |||
 146 | ||| @ c : This is the type of commit given for custom packages.
 147 | public export
 148 | record Config_ (f : Type -> Type) (c : Type) where
 149 |   constructor MkConfig
 150 |   ||| Package collection to use
 151 |   collection   : f DBName
 152 | 
 153 |   ||| URL to a custom Idris repo
 154 |   ||| This overrides the one from the package collection if not
 155 |   ||| set to `Nothing`.
 156 |   idrisURL     : Maybe URL
 157 | 
 158 |   ||| Custom Idris commit
 159 |   ||| This overrides the one from the package collection if not
 160 |   ||| set to `Nothing`.
 161 |   idrisCommit  : Maybe c
 162 | 
 163 |   ||| All Idris commits mentioned in used configs
 164 |   allIdrisCommits : List c
 165 | 
 166 |   ||| Custom pack repo
 167 |   packURL      : Maybe URL
 168 | 
 169 |   ||| Custom pack branch to use (default is `main`)
 170 |   packCommit   : Maybe c
 171 | 
 172 |   ||| Scheme executable to use
 173 |   scheme       : f FilePath
 174 | 
 175 |   ||| Whether to bootstrap when building Idris2
 176 |   bootstrap    : f Bool
 177 | 
 178 |   ||| Whether to rebuild Idris2 with the stage 2 compiler
 179 |   bootstrapStage3 : f Bool
 180 | 
 181 |   ||| Whether to prompt for a confirmation when
 182 |   ||| building or installing a package with custom
 183 |   ||| build or install hooks.
 184 |   safetyPrompt : f Bool
 185 | 
 186 |   ||| Whether to prompt for a confirmation when
 187 |   ||| running the garbage collector for removing no longer used
 188 |   ||| installation directories.
 189 |   gcPrompt : f Bool
 190 | 
 191 |   ||| Whether to remove not only stuff compiled with outdated version
 192 |   ||| of the compiler but also libs and apps whose install hash does not
 193 |   ||| match the current one.
 194 |   gcPurge : f Bool
 195 | 
 196 |   ||| Whether to issue a warning in presence of a local `depends` directory
 197 |   warnDepends : f Bool
 198 | 
 199 |   ||| Whether to skip tests during collection checking
 200 |   skipTests : f Bool
 201 | 
 202 |   ||| List of package names, for which we will not issue a safety prompt
 203 |   ||| in case of custom `.ipkg` hooks, even if `safetyPrompt` is set
 204 |   ||| to `True`
 205 |   whitelist    : f (List PkgName)
 206 | 
 207 |   ||| Whether to install the library sources as well
 208 |   withSrc      : f Bool
 209 | 
 210 |   ||| Whether to install the library docs as well
 211 |   withDocs     : f Bool
 212 | 
 213 |   ||| Whether to use katla to add semantically highlighted source code
 214 |   ||| to the library docs.
 215 |   useKatla     : f Bool
 216 | 
 217 |   ||| The `.ipkg` file to use (if any) when starting a REPL session
 218 |   withIpkg     : f WithIpkg
 219 | 
 220 |   ||| Whether to use `rlwrap` to run a REPL session
 221 |   rlwrap       : f RlwrapConfig
 222 | 
 223 |   ||| Any extra arguments to pass to Idris2 executable.
 224 |   extraArgs    : f CmdArgList
 225 | 
 226 |   ||| Libraries to install automatically
 227 |   autoLibs     : f (List PkgName)
 228 | 
 229 |   ||| Applications to install automatically
 230 |   autoApps     : f (List PkgName)
 231 | 
 232 |   ||| Libraries to automatically load in a REPL session
 233 |   autoLoad     : f Autoload
 234 | 
 235 |   ||| Customizations to the package data base
 236 |   custom       : f CustomMap
 237 | 
 238 |   ||| Type of query to run
 239 |   queryType    : f (QueryType)
 240 | 
 241 |   ||| Verbosity of the Log
 242 |   logLevel     : f (LogLevel)
 243 | 
 244 |   ||| Codegen to use
 245 |   codegen      : f (Codegen)
 246 | 
 247 |   ||| Name of output file when compiling Idris source files
 248 |   output       : f Body
 249 | 
 250 |   ||| Default LogLevels for different commands
 251 |   levels       : f (SortedMap String LogLevel)
 252 | 
 253 |   ||| Whether to initialize git.
 254 |   gitInit      : f Bool
 255 | 
 256 | ||| Configuration with mandatory fields.
 257 | public export
 258 | 0 IConfig : Type -> Type
 259 | IConfig = Config_ I
 260 | 
 261 | ||| Configuration with optional fields.
 262 | public export
 263 | 0 MConfig : Type -> Type
 264 | MConfig = Config_ Maybe
 265 | 
 266 | ||| Application config with meta commits not yet resolved.
 267 | public export
 268 | 0 MetaConfig : Type
 269 | MetaConfig = IConfig MetaCommit
 270 | 
 271 | ||| Fully resolved application config.
 272 | public export
 273 | 0 Config : Type
 274 | Config = IConfig Commit
 275 | 
 276 | ||| User-defined adjustments to the application config.
 277 | public export
 278 | 0 UserConfig : Type
 279 | UserConfig = MConfig MetaCommit
 280 | 
 281 | ||| Effectfully convert all custom package descriptions
 282 | ||| stored in a configuration. This is mainly used to
 283 | ||| resolve meta commits to mere commits.
 284 | export
 285 | traverse :  Applicative f
 286 |          => (URL -> a -> f b)
 287 |          -> (idrisURL : URL)
 288 |          -> Config_ I a
 289 |          -> f (Config_ I b)
 290 | traverse g idrisURL cfg =
 291 |   let iurl = fromMaybe idrisURL cfg.idrisURL
 292 |       purl = fromMaybe defaultPackRepo cfg.packURL
 293 |       ic  = traverse (g iurl) cfg.idrisCommit
 294 |       ics = traverse (g iurl) cfg.allIdrisCommits
 295 |       pc  = traverse (g purl) cfg.packCommit
 296 |    in [| adj ic ics pc |]
 297 |     where adj :  (idrisCommit : Maybe b)
 298 |               -> (allidrisCommits : List b)
 299 |               -> (packCommit  : Maybe b)
 300 |               -> Config_ I b
 301 |           adj ic ics pc =
 302 |             { idrisCommit     := ic
 303 |             , allIdrisCommits := ics
 304 |             , packCommit      := pc
 305 |             } cfg
 306 | 
 307 | ||| This allows us to use a `Config` in scope when we
 308 | ||| need an auto-implicit `LogLevel` for logging.
 309 | export %inline %hint
 310 | configToLogRef : (c : Config) => LogRef
 311 | configToLogRef = MkLogRef c.logLevel
 312 | 
 313 | ||| This allows us to use a `MetaConfig` in scope when we
 314 | ||| need an auto-implicit `LogLevel` for logging.
 315 | export %inline %hint
 316 | metaConfigToLogRef : (c : MetaConfig) => LogRef
 317 | metaConfigToLogRef = MkLogRef c.logLevel
 318 | 
 319 | --------------------------------------------------------------------------------
 320 | --          Updating the Config
 321 | --------------------------------------------------------------------------------
 322 | 
 323 | export infixl 8 `mergeRight`
 324 | 
 325 | export
 326 | mergeRight : SortedMap k v -> SortedMap k v -> SortedMap k v
 327 | mergeRight = mergeWith (\_,v => v)
 328 | 
 329 | ||| Initial config
 330 | export
 331 | init : (cur : CurDir) => (coll : DBName) -> MetaConfig
 332 | init coll = MkConfig {
 333 |     collection      = coll
 334 |   , idrisURL        = Nothing
 335 |   , idrisCommit     = Nothing
 336 |   , allIdrisCommits = []
 337 |   , packURL         = Nothing
 338 |   , packCommit      = Nothing
 339 |   , scheme          = "scheme"
 340 |   , bootstrap       = False
 341 |   , bootstrapStage3 = True
 342 |   , safetyPrompt    = True
 343 |   , gcPrompt        = True
 344 |   , gcPurge         = False
 345 |   , warnDepends     = True
 346 |   , skipTests       = False
 347 |   , whitelist       = ["pack", "idris2-lsp"]
 348 |   , withSrc         = True
 349 |   , withDocs        = False
 350 |   , useKatla        = False
 351 |   , withIpkg        = Search cur
 352 |   , rlwrap          = DoNotUseRlwrap
 353 |   , extraArgs       = []
 354 |   , autoLibs        = []
 355 |   , autoApps        = []
 356 |   , autoLoad        = NoPkgs
 357 |   , custom          = empty
 358 |   , queryType       = NameOnly
 359 |   , logLevel        = Warning
 360 |   , codegen         = Default
 361 |   , output          = "_tmppack"
 362 |   , levels          = empty
 363 |   , gitInit         = False
 364 |   }
 365 | 
 366 | export infixl 7 `update`
 367 | 
 368 | ||| Update a config with optional settings
 369 | export
 370 | update : IConfig c -> MConfig c -> IConfig c
 371 | update ci cm =
 372 |   MkConfig {
 373 |     collection      = fromMaybe ci.collection cm.collection
 374 |   , idrisURL        = cm.idrisURL <|> ci.idrisURL
 375 |   , idrisCommit     = cm.idrisCommit <|> ci.idrisCommit
 376 |   , allIdrisCommits = cm.allIdrisCommits <+> ci.allIdrisCommits
 377 |   , packURL         = cm.packURL <|> ci.packURL
 378 |   , packCommit      = cm.packCommit <|> ci.packCommit
 379 |   , scheme          = fromMaybe ci.scheme cm.scheme
 380 |   , bootstrap       = fromMaybe ci.bootstrap cm.bootstrap
 381 |   , bootstrapStage3 = fromMaybe ci.bootstrapStage3 cm.bootstrapStage3
 382 |   , safetyPrompt    = fromMaybe ci.safetyPrompt cm.safetyPrompt
 383 |   , gcPrompt        = fromMaybe ci.gcPrompt cm.gcPrompt
 384 |   , gcPurge         = fromMaybe ci.gcPurge cm.gcPurge
 385 |   , warnDepends     = fromMaybe ci.warnDepends cm.warnDepends
 386 |   , skipTests       = fromMaybe ci.skipTests cm.skipTests
 387 |   , withSrc         = fromMaybe ci.withSrc cm.withSrc
 388 |   , withDocs        = fromMaybe ci.withDocs cm.withDocs
 389 |   , useKatla        = fromMaybe ci.useKatla cm.useKatla
 390 |   , withIpkg        = fromMaybe ci.withIpkg cm.withIpkg
 391 |   , rlwrap          = fromMaybe ci.rlwrap cm.rlwrap
 392 |   , extraArgs       = ci.extraArgs <+> fromMaybe [] cm.extraArgs
 393 |   , whitelist       = sortedNub (ci.whitelist ++ concat cm.whitelist)
 394 |   , autoLibs        = sortedNub (ci.autoLibs ++ concat cm.autoLibs)
 395 |   , autoApps        = sortedNub (ci.autoApps ++ concat cm.autoApps)
 396 |   , autoLoad        = fromMaybe ci.autoLoad cm.autoLoad
 397 |   , custom          = mergeWith (mergeWith mergeUP) ci.custom (fromMaybe empty cm.custom)
 398 |   , queryType       = fromMaybe ci.queryType cm.queryType
 399 |   , logLevel        = fromMaybe ci.logLevel cm.logLevel
 400 |   , codegen         = fromMaybe ci.codegen cm.codegen
 401 |   , output          = fromMaybe ci.output cm.output
 402 |   , levels          = mergeWith (\_,v => v) ci.levels (fromMaybe empty cm.levels)
 403 |   , gitInit         = fromMaybe ci.gitInit cm.gitInit
 404 |   }
 405 | 
 406 | --------------------------------------------------------------------------------
 407 | --          HasIdris
 408 | --------------------------------------------------------------------------------
 409 | 
 410 | ||| Proof that we have verified that the required Idris
 411 | ||| compiler has been installed.
 412 | public export
 413 | data HasIdris : Config -> DB -> Type where
 414 |   [noHints]
 415 |   ItHasIdris : {0 c : _} -> {0 db : _} -> HasIdris c db
 416 | 
 417 | --------------------------------------------------------------------------------
 418 | --          Env
 419 | --------------------------------------------------------------------------------
 420 | 
 421 | ||| Cache used during package resolution
 422 | public export
 423 | 0 LibCache : Type
 424 | LibCache = IORef (SortedMap PkgName $ ResolvedLib U)
 425 | 
 426 | ||| Create an empty library cache
 427 | export
 428 | emptyCache : HasIO io => io LibCache
 429 | emptyCache = newIORef SortedMap.empty
 430 | 
 431 | ||| Cache a resolved library
 432 | export
 433 | cacheLib :  HasIO io
 434 |          => (ref : LibCache)
 435 |          => PkgName
 436 |          -> ResolvedLib U
 437 |          -> io (ResolvedLib U)
 438 | cacheLib n lib = modifyIORef ref (insert n lib) $> lib
 439 | 
 440 | ||| Lookup a library in the cache
 441 | export
 442 | lookupLib :  HasIO io
 443 |           => (ref : LibCache)
 444 |           => PkgName
 445 |           -> io (Maybe $ ResolvedLib U)
 446 | lookupLib n = lookup n <$> readIORef ref
 447 | 
 448 | ||| Lookup a library in the cache
 449 | export
 450 | uncacheLib : HasIO io => (ref : LibCache) => PkgName -> io ()
 451 | uncacheLib n = modifyIORef ref (delete n)
 452 | 
 453 | ||| Environment used by most pack methods, consisting of
 454 | ||| the `PACK_DIR` environment variable, the user-defined
 455 | ||| application configuratin, and the data collection to
 456 | ||| use.
 457 | public export
 458 | record Env where
 459 |   constructor MkEnv
 460 |   packDirs : PackDirs
 461 |   tmpDir   : TmpDir
 462 |   config   : Config
 463 |   cache    : LibCache
 464 |   db       : DB -- pack collection
 465 |   all      : SortedMap PkgName Package -- packages merged from config and db
 466 |   linebuf  : LineBufferingCmd
 467 |   clock    : Clock UTC
 468 | 
 469 | ||| Returns the current nanoseconds as a string.
 470 | export
 471 | nanoString : (e : Env) => String
 472 | nanoString = show $ toNano e.clock
 473 | 
 474 | ||| This allows us to use an `Env` in scope when we
 475 | ||| need an auto-implicit `PackDirs`.
 476 | export %inline %hint
 477 | envToPackDirs : (e : Env) => PackDirs
 478 | envToPackDirs = e.packDirs
 479 | 
 480 | ||| This allows us to use an `Env` in scope when we
 481 | ||| need an auto-implicit `TmpDir`.
 482 | export %inline %hint
 483 | envToTmpDir : (e : Env) => TmpDir
 484 | envToTmpDir = e.tmpDir
 485 | 
 486 | ||| This allows us to use an `Env` in scope when we
 487 | ||| need an auto-implicit `LibCache`.
 488 | export %inline %hint
 489 | envToCache : (e : Env) => LibCache
 490 | envToCache = e.cache
 491 | 
 492 | ||| This allows us to use an `Env` in scope when we
 493 | ||| need an auto-implicit `Config`.
 494 | export %inline %hint
 495 | envToConfig : (e : Env) => Config
 496 | envToConfig = e.config
 497 | 
 498 | ||| This allows us to use an `Env` in scope when we
 499 | ||| need an auto-implicit `DB`.
 500 | export %inline %hint
 501 | envToDB : (e : Env) => DB
 502 | envToDB = e.db
 503 | 
 504 | ||| This allows us to use an `Env` in scope when we
 505 | ||| need an auto-implicit `LineBufferingCmd`.
 506 | export %inline %hint
 507 | envToLinebuf : (e : Env) => LineBufferingCmd
 508 | envToLinebuf = e.linebuf
 509 | 
 510 | ||| Like `Pack.Config.Types.Env`, but with an erased proof
 511 | ||| that the Idris compiler installation has been verified.
 512 | public export
 513 | record IdrisEnv where
 514 |   constructor MkIdrisEnv
 515 |   env   : Env
 516 |   ttc   : TTCVersion
 517 |   0 prf : HasIdris env.config env.db
 518 | 
 519 | ||| This allows us to use an `IdrisEnv` in scope when we
 520 | ||| need an auto-implicit `Env`.
 521 | export %inline %hint
 522 | idrisEnvToEnv : (e : IdrisEnv) => Env
 523 | idrisEnvToEnv = e.env
 524 | 
 525 | ||| This allows us to use an `IdrisEnv` in scope when we
 526 | ||| need an auto-implicit `TTCVersion`.
 527 | export %inline %hint
 528 | idrisEnvToTTC : (e : IdrisEnv) => TTCVersion
 529 | idrisEnvToTTC = e.ttc
 530 | 
 531 | --------------------------------------------------------------------------------
 532 | --          Command Arguments
 533 | --------------------------------------------------------------------------------
 534 | 
 535 | ||| An interface for parsing the argument list of a pack command
 536 | public export
 537 | interface Arg (0 a : Type) where
 538 |   argDesc_ : String
 539 |   readArg  : List String -> Maybe (a, List String)
 540 | 
 541 | ||| Utility version of `argDesc_` with an explicit erased type argument.
 542 | public export %inline
 543 | argDesc : (0 a : Type) -> Arg a => String
 544 | argDesc a = argDesc_ {a}
 545 | 
 546 | ||| Utility for implementing `readArg` via a function reading a single string.
 547 | export
 548 | parseSingleMaybe :  (read : String -> Maybe a)
 549 |                  -> List String
 550 |                  -> Maybe (a, List String)
 551 | parseSingleMaybe read []       = Nothing
 552 | parseSingleMaybe read (h :: t) = (,t) <$> read h
 553 | 
 554 | ||| Utility for implementing `readArg` via a function reading a single string.
 555 | export %inline
 556 | parseSingle :  (read : String -> Either e a)
 557 |             -> List String
 558 |             -> Maybe (a, List String)
 559 | parseSingle read = parseSingleMaybe (eitherToMaybe . read)
 560 | 
 561 | ||| Utility for implementing `readArg` via a function reading a single string.
 562 | export %inline
 563 | readSingle :  (read : String -> a) -> List String -> Maybe (a, List String)
 564 | readSingle read = parseSingleMaybe (Just . read)
 565 | 
 566 | export
 567 | Arg a => Arg (Maybe a) where
 568 |   argDesc_ = "[\{argDesc a}]"
 569 | 
 570 |   readArg ss = case readArg {a} ss of
 571 |     Nothing      => Just (Nothing, ss)
 572 |     Just (v,ss') => Just (Just v, ss')
 573 | 
 574 | export
 575 | (cd : CurDir) => Arg (File Abs) where
 576 |   argDesc_ = "<file>"
 577 |   readArg = parseSingle (readAbsFile curDir)
 578 | 
 579 | export
 580 | (cd : CurDir) => Arg (Path Abs) where
 581 |   argDesc_ = "<dir>"
 582 |   readArg = readSingle (\s => parse s curDir)
 583 | 
 584 | export
 585 | (cd : CurDir) => Arg PkgOrIpkg where
 586 |   argDesc_ = "<pkg or .ipkg>"
 587 |   readArg = readSingle $ \s => case readAbsFile curDir s of
 588 |     Left  _ => Pkg $ MkPkgName s
 589 |     Right f =>
 590 |       if isIpkgBody f.file
 591 |            then Ipkg f
 592 |            else Pkg $ MkPkgName s
 593 | 
 594 | export %inline
 595 | Arg PkgName where
 596 |   argDesc_ = "<pkg>"
 597 |   readArg = readSingle MkPkgName
 598 | 
 599 | export %inline
 600 | Arg PkgType where
 601 |   argDesc_ = "<lib | bin>"
 602 |   readArg = parseSingle readPkgType
 603 | 
 604 | export %inline
 605 | Arg CmdArgList where
 606 |   argDesc_ = "[<args>]"
 607 |   readArg ss = Just (fromStrList ss, [])
 608 | 
 609 | export %inline
 610 | Arg (List PkgName) where
 611 |   argDesc_ = "[<pkgs>]"
 612 |   readArg ss = Just (map MkPkgName ss, [])
 613 | 
 614 | export %inline
 615 | Arg Body where
 616 |   argDesc_ = "<file name>"
 617 |   readArg = parseSingle readBody
 618 | 
 619 | export %inline
 620 | Arg DBName where
 621 |   argDesc_ = "<db>"
 622 |   readArg = parseSingle readDBName
 623 | 
 624 | export %inline
 625 | Arg String where
 626 |   argDesc_ = "<str>"
 627 |   readArg = readSingle id
 628 | 
 629 | --------------------------------------------------------------------------------
 630 | --          Command
 631 | --------------------------------------------------------------------------------
 632 | 
 633 | ||| Interface representing pack commands. We abstract over this
 634 | ||| because both pack and pack-admin accept different types of
 635 | ||| commands, but both use the same functionality for reading
 636 | ||| the application config based on the command they use.
 637 | |||
 638 | ||| A command `c` is expected to be an enum type. This interface provides
 639 | ||| a name and detailed description for each command, as well as the types of
 640 | ||| arguments a command takes.
 641 | |||
 642 | ||| This allows us to generate useful error messages when the wrong type
 643 | ||| of argument is passed to a command. It also allows us to implement the
 644 | ||| parsing of commands only once.
 645 | public export
 646 | interface Command c where
 647 |   ||| The command to use if only command line options but
 648 |   ||| not command is given.
 649 |   defaultCommand : c
 650 | 
 651 |   ||| Name of the application in question
 652 |   appName : String
 653 | 
 654 |   ||| Name of command in question
 655 |   cmdName : c -> String
 656 | 
 657 |   ||| The default log level to use.
 658 |   defaultLevel    : c -> LogLevel
 659 | 
 660 |   ||| Detailed usage description of the command
 661 |   desc : c -> String
 662 | 
 663 |   ||| General usage of the application in question
 664 |   usage : Lazy String
 665 | 
 666 |   ||| Types of arguments required by the given command
 667 |   0 ArgTypes : c -> List Type
 668 | 
 669 |   ||| Tries to read a command from a String
 670 |   readCommand_ : String -> Maybe c
 671 | 
 672 |   ||| List of argument readers for the current command
 673 |   readArgs : CurDir => (cmd : c) -> All Arg (ArgTypes cmd)
 674 | 
 675 |   ||| Some commands overwrite certain aspects of the user-defined
 676 |   ||| config. For instance, `pack switch latest` must overwrite the
 677 |   ||| package collection read from the `pack.toml` files with the
 678 |   ||| latest package collection available.
 679 |   adjConfig_ :  HasIO io
 680 |              => PackDirs
 681 |              => TmpDir
 682 |              => (cmd : c)
 683 |              -> All I (ArgTypes cmd)
 684 |              -> MetaConfig
 685 |              -> EitherT PackErr io MetaConfig
 686 | 
 687 | args : All Arg ts -> CurDir => List String -> Maybe (All I ts)
 688 | args [] []       = Just []
 689 | args [] (_ :: _) = Nothing
 690 | args {ts = x :: xs} (p :: ps) ss = do
 691 |   (v,ss') <- readArg {a = x} ss
 692 |   vs      <- args ps ss'
 693 |   pure (v :: vs)
 694 | 
 695 | argsDesc : CurDir => Command c => Maybe c -> String
 696 | argsDesc Nothing  = " [<args>]"
 697 | argsDesc (Just x) = fastConcat $ go (readArgs x)
 698 |   where go : All Arg ts -> List String
 699 |         go = forget . mapProperty (\p => " " ++ argDesc_ @{p})
 700 | 
 701 | ||| Header line for a usage string
 702 | export
 703 | usageHeader : CurDir => Command c => Maybe c -> String
 704 | usageHeader cmd =
 705 |   let nm      := maybe "<cmd>" cmdName cmd
 706 |    in "Usage: \{appName {c}} [options] \{nm}\{argsDesc cmd}"
 707 | 
 708 | ind : String -> String
 709 | ind = unlines . map (indent 2) . lines
 710 | 
 711 | ||| Detailed description how to use the given command.
 712 | |||
 713 | ||| This is a general description of the application
 714 | ||| in case the argument is `Nothing`.
 715 | export
 716 | usageDesc : CurDir => Command c => Maybe c -> String
 717 | usageDesc m = case m of
 718 |   Just cmd =>
 719 |     """
 720 |     \{usageHeader m}
 721 | 
 722 |     \{ind $ desc cmd}
 723 |     """
 724 | 
 725 |   Nothing =>
 726 |     """
 727 |     \{usageHeader m}
 728 | 
 729 |     \{usage {c}}
 730 |     """
 731 | 
 732 | ||| Type of arguments expected by the given command
 733 | public export
 734 | 0 Args : Command c => c -> Type
 735 | Args cmd = All I (ArgTypes cmd)
 736 | 
 737 | ||| A pack command together with its list of arguments
 738 | public export
 739 | 0 CommandWithArgs : (c : Type) -> Command c => Type
 740 | CommandWithArgs c = DPair c Args
 741 | 
 742 | readCWA :  Command c
 743 |         => CurDir
 744 |         => (cmd : c)
 745 |         -> List String
 746 |         -> Either PackErr (CommandWithArgs c)
 747 | readCWA x ss =
 748 |   let readers := readArgs x
 749 |       Just as := args readers ss
 750 |         | Nothing => Left (InvalidCmdArgs (cmdName x) ss $ usageHeader $ Just x)
 751 |    in Right (x ** as)
 752 | 
 753 | ||| Convenience alias for `readCommand_` with an explicit
 754 | ||| erased argument for the command type.
 755 | export
 756 | readCommand :  (0 c : Type)
 757 |             -> Command c
 758 |             => CurDir
 759 |             -> List String
 760 |             -> Either PackErr (CommandWithArgs c)
 761 | readCommand c cd []       = readCWA defaultCommand []
 762 | readCommand c cd (h :: t) = case readCommand_ {c} h of
 763 |   Nothing => Left (UnknownCommand h $ usageDesc {c} Nothing)
 764 |   Just x  => readCWA x t
 765 | 
 766 | ||| Some commands overwrite certain aspects of the user-defined
 767 | ||| config. For instance, `pack switch latest` must overwrite the
 768 | ||| package collection read from the `pack.toml` files with the
 769 | ||| latest package collection available.
 770 | export %inline
 771 | adjConfig :  HasIO io
 772 |           => Command c
 773 |           => PackDirs
 774 |           => TmpDir
 775 |           => CommandWithArgs c
 776 |           -> MetaConfig
 777 |           -> EitherT PackErr io MetaConfig
 778 | adjConfig (command ** args) = adjConfig_ command args
 779 |