Idris2Doc : Pack.Core.Types

Pack.Core.Types

(source)
We work a lot with Strings of distinct semantics.
Since I've been bitten by this more than once, we wrap
the in single field record types to drastically increase
type safety.

Reexports

import public Data.FilePath.File

Definitions

quote : Interpolation a => a -> String
  This puts a value in quotes during interpolation.
  
  Note: If the interpolated string contains additional quote
  characters, these will *not* be escaped.

Totality: total
Visibility: export
relativeTo : Path Abs -> Path Abs -> Path Rel
  Returns the second path, relative to the first one
  For instance, `relativeTo /foo/bar/baz /foo/quux` will return
  `../../quux`.

Totality: total
Visibility: export
isIpkgBody : Body -> Bool
  True if the given file path body ends on `.ipkg`

Totality: total
Visibility: export
isTomlBody : Body -> Bool
  True if the given file path body ends on `.toml`

Totality: total
Visibility: export
isHtmlBody : Body -> Bool
  True if the given file path body ends on `.html`

Totality: total
Visibility: export
toAbsPath : Path Abs -> FilePath -> Path Abs
  Converts a `FilePath` - which might hold a relative
  or an absolute path - to an absolute path by interpreting
  a relative path being relative to the given parent directory.

Totality: total
Visibility: export
parse : String -> Path Abs -> Path Abs
  Parses a string, converting it to either a relative
  or absolute path and using `toAbsPath` to convert the result
  to an absolute path.

Totality: total
Visibility: export
(<//>) : Cast a (Path Rel) => Path t -> a -> Path t
  More flexible version of `</>` (path concatenation).

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 5
(//>) : Cast a Body => Path t -> a -> Path t
  More flexible version of `//>`
  (appending a file path body to an absolute path)

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 5
(<->) : Cast a Body => Cast b Body => a -> b -> Body
  Concatenate two file path bodies with a hyphen inbetween.

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 8
toAbsFile : Path Abs -> File Rel -> File Abs
  Convert a relative file path to an absolute one by appending
  it to the given parent directory.

Totality: total
Visibility: export
record PackDirs : Type
  The directory where package collections, global user settings,
  and cached `.ipkg` files are stored.

Totality: total
Visibility: public export
Constructor: 
PD : Path Abs -> Path Abs -> Path Abs -> Path Abs -> PackDirs

Projections:
.bin : PackDirs -> Path Abs
  Directory where executables will be installed.
  
  Depending on what environment variables are set, this defaults to
  (in decreasing order of priority):
  
  * `PACK_BIN_DIR`
  * `$HOME/.local/bin`
.cache : PackDirs -> Path Abs
  Directory with cached data such as cached `.ipkg` files, git repos,
  and temporary files used during installation of libs.
  
  Depending on what environment variables are set, this defaults to
  (in decreasing order of priority):
  
  * `PACK_CACHE_DIR`
  * `$XDG_CACHE_HOME/pack`
  * `$HOME/.cache/pack`
.state : PackDirs -> Path Abs
  Directory with application state (installed compiler and libraries).
  
  Depending on what environment variables are set, this defaults to
  (in decreasing order of priority):
  
  * `PACK_STATE_DIR`
  * `$XDG_STATE_HOME/pack`
  * `$HOME/.local/state/pack`
.user : PackDirs -> Path Abs
  Directory with user settings.
  
  Depending on what environment variables are set, this defaults to
  (in decreasing order of priority):
  
  * `PACK_USER_DIR`
  * `$XDG_CONFIG_HOME/pack`
  * `$HOME/.config/pack`

Hint: 
Env => PackDirs
.user : PackDirs -> Path Abs
  Directory with user settings.
  
  Depending on what environment variables are set, this defaults to
  (in decreasing order of priority):
  
  * `PACK_USER_DIR`
  * `$XDG_CONFIG_HOME/pack`
  * `$HOME/.config/pack`

Totality: total
Visibility: public export
user : PackDirs -> Path Abs
  Directory with user settings.
  
  Depending on what environment variables are set, this defaults to
  (in decreasing order of priority):
  
  * `PACK_USER_DIR`
  * `$XDG_CONFIG_HOME/pack`
  * `$HOME/.config/pack`

Totality: total
Visibility: public export
.state : PackDirs -> Path Abs
  Directory with application state (installed compiler and libraries).
  
  Depending on what environment variables are set, this defaults to
  (in decreasing order of priority):
  
  * `PACK_STATE_DIR`
  * `$XDG_STATE_HOME/pack`
  * `$HOME/.local/state/pack`

Totality: total
Visibility: public export
state : PackDirs -> Path Abs
  Directory with application state (installed compiler and libraries).
  
  Depending on what environment variables are set, this defaults to
  (in decreasing order of priority):
  
  * `PACK_STATE_DIR`
  * `$XDG_STATE_HOME/pack`
  * `$HOME/.local/state/pack`

Totality: total
Visibility: public export
.cache : PackDirs -> Path Abs
  Directory with cached data such as cached `.ipkg` files, git repos,
  and temporary files used during installation of libs.
  
  Depending on what environment variables are set, this defaults to
  (in decreasing order of priority):
  
  * `PACK_CACHE_DIR`
  * `$XDG_CACHE_HOME/pack`
  * `$HOME/.cache/pack`

Totality: total
Visibility: public export
cache : PackDirs -> Path Abs
  Directory with cached data such as cached `.ipkg` files, git repos,
  and temporary files used during installation of libs.
  
  Depending on what environment variables are set, this defaults to
  (in decreasing order of priority):
  
  * `PACK_CACHE_DIR`
  * `$XDG_CACHE_HOME/pack`
  * `$HOME/.cache/pack`

Totality: total
Visibility: public export
.bin : PackDirs -> Path Abs
  Directory where executables will be installed.
  
  Depending on what environment variables are set, this defaults to
  (in decreasing order of priority):
  
  * `PACK_BIN_DIR`
  * `$HOME/.local/bin`

Totality: total
Visibility: public export
bin : PackDirs -> Path Abs
  Directory where executables will be installed.
  
  Depending on what environment variables are set, this defaults to
  (in decreasing order of priority):
  
  * `PACK_BIN_DIR`
  * `$HOME/.local/bin`

Totality: total
Visibility: public export
data CurDir : Type
  The directory from which the pack application was invoked.

Totality: total
Visibility: public export
Constructor: 
CD : Path Abs -> CurDir

Hints:
CurDir => Arg (File Abs)
CurDir => Arg (Path Abs)
CurDir => Arg PkgOrIpkg
Interpolation CurDir
curDir : CurDir => Path Abs
  Use this when you need access to the current directory's path with
  only a value of type `CurDir` in scope.

Totality: total
Visibility: export
data TmpDir : Type
  The directory where temporary files and git repos will be
  kept.

Totality: total
Visibility: public export
Constructor: 
TD : Path Abs -> TmpDir

Hints:
Interpolation TmpDir
Env => TmpDir
tmpDir : TmpDir => Path Abs
  Use this when you need access to the `PACK_DIR` path with
  only a value of type `PackDir` in scope.

Totality: total
Visibility: export
record TTCVersion : Type
  The TTC-Version currently used by the Idris compiler

Totality: total
Visibility: public export
Constructor: 
TTCV : Maybe Body -> TTCVersion

Projection: 
.version : TTCVersion -> Maybe Body

Hint: 
IdrisEnv => TTCVersion
.version : TTCVersion -> Maybe Body
Totality: total
Visibility: public export
version : TTCVersion -> Maybe Body
Totality: total
Visibility: public export
ttcVersion : TTCVersion => Maybe Body
  Use this when you need access to the current TTC version
  only a value of type `TTCVersion` in scope.

Totality: total
Visibility: export
record URL : Type
  URL mostly used to represent Git repositories.

Totality: total
Visibility: public export
Constructor: 
MkURL : String -> URL

Projection: 
.value : URL -> String

Hints:
Cast URL (Path Rel)
Eq URL
FromString URL
FromTOML URL
Interpolation URL
Show URL
Uninhabited (IsCore (Git {_:2796} {_:2797} {_:2798} {_:2799} {_:2801} {_:2800}))
Uninhabited (IsLocal (Git {_:2967} {_:2968} {_:2969} {_:2970} {_:2972} {_:2971}))
.value : URL -> String
Totality: total
Visibility: public export
value : URL -> String
Totality: total
Visibility: public export
record Commit : Type
  A git commit hash or tag.

Totality: total
Visibility: public export
Constructor: 
MkCommit : String -> Commit

Projection: 
.value : Commit -> String

Hints:
Cast Commit (Path Rel)
Eq Commit
FromString Commit
FromTOML Commit
Interpolation Commit
Show Commit
Uninhabited (IsCore (Local {_:2747} {_:2746} {_:2745} {_:2744}))
Uninhabited (IsCore (Git {_:2796} {_:2797} {_:2798} {_:2799} {_:2801} {_:2800}))
Uninhabited (IsLocal (Core {_:2936}))
Uninhabited (IsLocal (Git {_:2967} {_:2968} {_:2969} {_:2970} {_:2972} {_:2971}))
Uninhabited (IsGit (Core {_:3115}))
Uninhabited (IsGit (Local {_:3143} {_:3142} {_:3141} {_:3140}))
.value : Commit -> String
Totality: total
Visibility: public export
value : Commit -> String
Totality: total
Visibility: public export
record Hash : Type
  A hash generated by pack

Totality: total
Visibility: public export
Constructor: 
MkHash : String -> Hash

Projection: 
.value : Hash -> String

Hints:
Cast Hash (Path Rel)
Eq Hash
FromString Hash
Interpolation Hash
Show Hash
.value : Hash -> String
Totality: total
Visibility: public export
value : Hash -> String
Totality: total
Visibility: public export
record Branch : Type
  A branch in a git repo.

Totality: total
Visibility: public export
Constructor: 
MkBranch : String -> Branch

Projection: 
.value : Branch -> String

Hints:
Cast Branch (Path Rel)
Eq Branch
FromString Branch
FromTOML Branch
Interpolation Branch
Show Branch
.value : Branch -> String
Totality: total
Visibility: public export
value : Branch -> String
Totality: total
Visibility: public export
record PkgName : Type
  Name of an Idris package

Totality: total
Visibility: public export
Constructor: 
MkPkgName : String -> PkgName

Projection: 
.value : PkgName -> String

Hints:
Arg PkgName
Arg (List PkgName)
Cast PkgName (Path Rel)
Eq PkgName
FromString PkgName
FromTOML PkgName
Interpolation PkgName
Ord PkgName
Show PkgName
TOMLKey PkgName
.value : PkgName -> String
Totality: total
Visibility: public export
value : PkgName -> String
Totality: total
Visibility: public export
data PkgOrIpkg : Type
  Several pack commands operat either on a pack package or a local
  `.ipkg` file. This data type represents such command line arguments.

Totality: total
Visibility: public export
Constructors:
Pkg : PkgName -> PkgOrIpkg
Ipkg : File Abs -> PkgOrIpkg

Hint: 
CurDir => Arg PkgOrIpkg
data PkgType : Type
  Type of an Idris package (either a library or a binary).

Totality: total
Visibility: public export
Constructors:
PLib : PkgType
PApp : PkgType

Hints:
Arg PkgType
Eq PkgType
Interpolation PkgType
Ord PkgType
data InstallType : Type
  What we want to install: A library, an application to
  run it from within pack, or an application, which should
  be available via the `PATH` variable.

Totality: total
Visibility: public export
Constructors:
Library : InstallType
App : Bool -> InstallType

Hints:
Eq InstallType
Interpolation InstallType
Ord InstallType
record DBName : Type
  Name of a package collection. This must be a valid
  file path body.

Totality: total
Visibility: public export
Constructor: 
MkDBName : Body -> DBName

Projection: 
.value : DBName -> Body

Hints:
Arg DBName
Cast DBName Body
Eq DBName
FromTOML DBName
Interpolation DBName
Ord DBName
TOMLKey DBName
.value : DBName -> Body
Totality: total
Visibility: public export
value : DBName -> Body
Totality: total
Visibility: public export
Head : DBName
Totality: total
Visibility: export
All : DBName
Totality: total
Visibility: export
record Desc : (PkgDesc -> Type) -> Type
  A tagged package desc. We use the tag mainly to make sure that
  the package desc in question has been checked for safety issues.
  Since the tag is parameterized by a `PkgDesc`, we make sure
  we will not inadvertently use a tag for a `PkgDesc` different to
  the one we wrapped.

Totality: total
Visibility: public export
Constructor: 
MkDesc : (desc : PkgDesc) -> String -> File Abs -> (0 _ : t desc) -> Desc t

Projections:
.cont : Desc t -> String
  String content of the `.ipkg` file used when reading the package desc
.desc : Desc t -> PkgDesc
  The parsed package desc
.path : Desc t -> File Abs
  Path to the file use when reading the package desc
0 .tag : ({rec:0} : Desc t) -> t (desc {rec:0})
  Security tag. See `Pack.Runner.Database.check`
.desc : Desc t -> PkgDesc
  The parsed package desc

Totality: total
Visibility: public export
desc : Desc t -> PkgDesc
  The parsed package desc

Totality: total
Visibility: public export
.cont : Desc t -> String
  String content of the `.ipkg` file used when reading the package desc

Totality: total
Visibility: public export
cont : Desc t -> String
  String content of the `.ipkg` file used when reading the package desc

Totality: total
Visibility: public export
.path : Desc t -> File Abs
  Path to the file use when reading the package desc

Totality: total
Visibility: public export
path : Desc t -> File Abs
  Path to the file use when reading the package desc

Totality: total
Visibility: public export
0 .tag : ({rec:0} : Desc t) -> t (desc {rec:0})
  Security tag. See `Pack.Runner.Database.check`

Totality: total
Visibility: public export
0 tag : ({rec:0} : Desc t) -> t (desc {rec:0})
  Security tag. See `Pack.Runner.Database.check`

Totality: total
Visibility: public export
0 U : PkgDesc -> Type
  This is used as a tag for unchecked `Desc`s.

Totality: total
Visibility: public export
dependencies : PkgDesc -> List PkgName
  Lists the dependencies of a package.

Totality: total
Visibility: export
dependencies : Desc t -> List PkgName
  Lists the dependencies of a package.

Totality: total
Visibility: export
data CmdArg : Type
  A command line argument of a call to the system shell.

Totality: total
Visibility: public export
Constructors:
Escapable : String -> CmdArg
  Escapable alternative represents a string that should be understood as a
  single argument disregarding its contents, i.e. the whole string should
  be passed as an argument even if it contains spaces or characters that
  are normally understood specially by shell.
NoEscape : String -> CmdArg
  No escape alternative represents a raw string that is used "as is" at the
  shell call, thus allowing to pass commands to the shell itself.
  Be aware that spaces inside these strings would form several actual
  arguments and quotation marks and backslash symbols may interfere with
  escaping of other arguments.

Hint: 
CmdArgable CmdArg
interface CmdArgable : Type -> Type
  Interface that is used to mark which types can be used as a source for
  command line arguments when building lists of such.
  This allows to be able to pass different literals and expressions without
  explicit wrapping them into the `CmdArg` type.

Parameters: a
Methods:
toCmdArg : a -> CmdArg

Implementations:
CmdArgable CmdArg
Interpolation a => CmdArgable a
toCmdArg : CmdArgable a => a -> CmdArg
Totality: total
Visibility: public export
data CmdArgList : Type
  A list of command line arguments.
  
  This type is meant to look syntacitcally as a simple list, however
  containing possibly values of different types which can form a command
  line argument.
  
  For example, a call to some command with redirection may look like this:
  `sys ["echo", "a", NoEscape ">", file]`,
  when, say, `file` is a value of type `File Abs`.

Totality: total
Visibility: public export
Constructors:
Nil : CmdArgList
(::) : CmdArgable a => a -> CmdArgList -> CmdArgList

Hints:
Arg CmdArgList
FromTOML CmdArgList
Monoid CmdArgList
Semigroup CmdArgList
escapeCmd : CmdArgList -> String
  Converts a list of command line arguments to a single string
  while putting spaces between arguments and escaping appropriate ones.
  
  For example, call `escapeCmd ["echo", "&&", NoEscape "&&", "echo", "yes"]`
  would return a string equivalent to the literal
  `#""echo" "&&" && "echo" "yes""#`.

Totality: total
Visibility: export
(++) : CmdArg -> CmdArg -> CmdArg
  Concatenate two command line arguments into one.
  
  This operation respects meaning of the contents of each argument,
  whether they should be escaped or not.
  This allows, say, to form an argument which partially contains something
  escapable and partially contains a special shell argument, for example
  `sys ["cp", "-r", Escapable "\{dirName}/" ++ NoEscape "*", dest]` would
  list files with shell's `*` even if `dirName` contains spaces.

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7
(++) : CmdArgList -> CmdArgList -> CmdArgList
  Concatenation operation for command line argument lists.

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7
concatMap : Monoid m => (CmdArg -> m) -> CmdArgList -> m
  Specialised version of `concatMap` from `Foldable` for `CmdArgList`,
  since `CmdArgList` cannot implement `Foldable`.

Totality: total
Visibility: export
fromStrList : List String -> CmdArgList
  Function that forms a command line arguments list from a raw list of
  strings, treating each string as a single escapable argument.

Totality: total
Visibility: export
record LineBufferingCmd : Type
  A wrapper for a command list of a shell command which allows to do
  line buffering.

Totality: total
Visibility: public export
Constructor: 
MkLineBufferingCmd : CmdArgList -> LineBufferingCmd

Projection: 
.lineBufferingCmd : LineBufferingCmd -> CmdArgList

Hint: 
Env => LineBufferingCmd
.lineBufferingCmd : LineBufferingCmd -> CmdArgList
Totality: total
Visibility: public export
lineBufferingCmd : LineBufferingCmd -> CmdArgList
Totality: total
Visibility: public export
data LogLevel : Type
  Level used during logging.

Totality: total
Visibility: public export
Constructors:
Debug : LogLevel
Build : LogLevel
Info : LogLevel
Cache : LogLevel
Warning : LogLevel
Silence : LogLevel

Hints:
Eq LogLevel
FromTOML LogLevel
Interpolation LogLevel
Ord LogLevel
logLevels : List (String, LogLevel)
Totality: total
Visibility: export
record LogRef : Type
  Reference `LogLevel` to be used as an auto implicit

Totality: total
Visibility: public export
Constructor: 
MkLogRef : LogLevel -> LogRef

Projection: 
.level : LogRef -> LogLevel

Hints:
Config => LogRef
MetaConfig => LogRef
.level : LogRef -> LogLevel
Totality: total
Visibility: public export
level : LogRef -> LogLevel
Totality: total
Visibility: public export
data TOMLErr : Type
  Error during marshalling from TOML to an Idris type.

Totality: total
Visibility: public export
Constructors:
MissingKey : List String -> TOMLErr
  A mandatory key/value pair in a toml file is
  missing
WrongType : List String -> String -> TOMLErr
  A value in a toml file has the wrong type
prefixKey : String -> Either TOMLErr a -> Either TOMLErr a
  Prefix the given TOML key to an error message. This allows us to
  specify exactly where in a TOML structure things went wrong.

Totality: total
Visibility: export
data PackErr : Type
  Errors that can occur when running pack programs.

Totality: total
Visibility: public export
Constructors:
NoCurDir : PackErr
  Failed to get the path of the current directory.
NoPackDir : PackErr
  Failed to get package directory path
NoTmpDir : PackErr
  Failed to create temporary directory
MkDir : Path Abs -> FileError -> PackErr
  Failed to create the given directory
ReadFile : File Abs -> FileError -> PackErr
  Failed to read the given file
WriteFile : File Abs -> FileError -> PackErr
  Failed to write to the given file
DirEntries : Path Abs -> FileError -> PackErr
  Failed to read the content of a directory
Sys : CmdArgList -> Int -> PackErr
  Error when running the given system command
ChangeDir : Path Abs -> PackErr
  Error when changing into the given directory
UnknownPkg : PkgName -> PackErr
  The given package is not in the package data base
IncompletePkg : PkgName -> PackErr
  Not enough data has been given for this package
NotLocalPkg : PkgName -> PackErr
  The given package is not a local package
NoApp : PkgName -> PackErr
  The given package is not an applicatio
  (No executable name set in the `.ipkg` file)
NoAppIpkg : File Abs -> PackErr
  The given package is not an application
  (No executable name set in the `.ipkg` file)
InvalidPackageDesc : String -> PackErr
  An erroneous package description in a package DB file
EmptyPkgDB : PackErr
  The package database is empty (no header)
InvalidDBHeader : String -> PackErr
  Invalid package database header
InvalidDBName : String -> PackErr
  Invalid package database header
InvalidPkgType : String -> PackErr
  Invalid package type
InvalidPkgVersion : String -> PackErr
  Invalid package version
InvalidLogLevel : String -> PackErr
  Invalid log level
InvalidIpkgFile : File Abs -> PackErr
  Failed to parse an .ipkg file
InvalidBody : String -> PackErr
  Invalid file path body
NoFilePath : String -> PackErr
  Failed to parse a file path
MissingCorePackage : PkgName -> PkgVersion -> Commit -> PackErr
  The given core package (base, contrib, etc.)
  is missing from the Idris installation.
UnknownArg : String -> PackErr
  Unknown command line argument
InvalidArgs : List String -> PackErr
  Invalid command line arguments (in micropack)
ErroneousArg : String -> PackErr
  Erroneous command line argument
BuildMany : List Body -> PackErr
  Trying to run zero or more than one local package
  (or something that isn't a local package).
UnknownCommand : String -> String -> PackErr
  Unknown pack command
InvalidCmdArgs : String -> List String -> String -> PackErr
  Unknown pack command
DirExists : Path Abs -> PackErr
  Trying to clone a repository into an existing
  directory.
TOMLFile : File Abs -> TOMLErr -> PackErr
  Error in a toml file.
TOMLParse : String -> PackErr
  Error in a toml file.
BuildFailures : Nat -> PackErr
  Number of failures when building packages.
ManualInstallPackApp : PackErr
  User tried to manually install the pack application
SafetyAbort : PackErr
  User aborted installation of a lib/app with custom build hooks.
CyclicDeps : List PkgName -> PackErr
printErr : PackErr -> String
  Prints an error that occured during program execution.

Totality: total
Visibility: export
readDBName : String -> Either PackErr DBName
  Tries to convert a string to a `DBName` by first converting
  it to a valid file path body.

Totality: total
Visibility: export
readBody : String -> Either PackErr Body
  Tries to convert a string to a file path body.

Totality: total
Visibility: export
readPkgType : String -> Either PackErr PkgType
  Tries to convert a string to a package type.

Totality: total
Visibility: export
readAbsFile : Path Abs -> String -> Either PackErr (File Abs)
  Tries to convert a string representing a relative or absolute
  file path. This uses `toAbsPath` internally, so it is somewhat
  tolerant w.r.t. to dubious file paths. It fails, however, if the
  given path does not contain at least one file path body.

Totality: total
Visibility: export
readLogLevel : String -> Either PackErr LogLevel
Totality: total
Visibility: export