Pack.Core.TOML

Definitions

interface TOMLKey : Type -> Type

  Interface for using a pack data type as a key
  in a TOML table.

Parameters: a
Constraints: Ord a
Methods:

fromKey : String -> Either TOMLErr a

  Tries to convert a key to a value of type `a`

Implementations:

TOMLKey DBName

TOMLKey PkgName

TOMLKey String

fromKey : TOMLKey a => String -> Either TOMLErr a

  Tries to convert a key to a value of type `a`

Totality: total
Visibility: public export

interface FromTOML : Type -> Type

  Interface for converting a TOML value to a pack
  data type. We pass the TOML file's absolute path
  as an additional argument, since this allows us to
  convert relative paths listed in the TOML file
  (for instance, the path to a local package) to absolute ones.

Parameters: a
Methods:

fromTOML : File Abs -> TomlValue -> Either TOMLErr a

  Tries to convert a `TomlValue` to a value of type `a`.

Implementations:

FromTOML Autoload

FromTOML Codegen

FromTOML RlwrapConfig

FromTOML CmdArgList

FromTOML UserConfig

FromTOML MetaCommit

FromTOML c => FromTOML (Package_ c)

FromTOML MetaDB

FromTOML String

FromTOML PkgName

FromTOML URL

FromTOML Branch

FromTOML Commit

FromTOML FilePath

FromTOML (Path Rel)

FromTOML LogLevel

FromTOML (File Rel)

FromTOML DBName

FromTOML Bool

FromTOML a => FromTOML (List a)

FromTOML PkgVersion

TOMLKey k => FromTOML v => FromTOML (SortedMap k v)

FromTOML (Path Abs)

FromTOML (File Abs)

fromTOML : FromTOML a => File Abs -> TomlValue -> Either TOMLErr a

  Tries to convert a `TomlValue` to a value of type `a`.

Totality: total
Visibility: public export

tmap : FromTOML a => (a -> b) -> File Abs -> TomlValue -> Either TOMLErr b

  Read a value of type `b` by reading a value of
  type `a` and converting it with the given function.

Totality: total
Visibility: export

trefine : FromTOML a => (a -> Either TOMLErr b) -> File Abs -> TomlValue -> Either TOMLErr b

  Read a value of type `b` by refining a value of
  type `a`.

Totality: total
Visibility: export

valAt' : (TomlValue -> Either TOMLErr a) -> String -> Maybe a -> TomlValue -> Either TOMLErr a

  Try to extract a value from a toml `TomlValue`.
  
  @ get   : Tries to convert the value found at the given `path` to a values of
            the result type.
  @ path  : Dot-separated path to the value we'd like to read.
  @ deflt : Optional default value to use if there is not entry
            at the given `path`. Note: This will not be used if there
            is an entry at `path`. In this case, the value found will
            always be handed over to `get`, resulting in a failure if
            it can't be properly converted.
  @ value : The TOML value we start with.

Totality: total
Visibility: export

valAt : FromTOML a => String -> File Abs -> TomlValue -> Either TOMLErr a

  Extract and convert a mandatory value from a TOML
  value. The `path` string can contain several dot-separated
  key names. See also `valAt'`.

Totality: total
Visibility: export

optValAt : FromTOML a => String -> File Abs -> a -> TomlValue -> Either TOMLErr a

  Extract and convert an optional value from a TOML
  value. The `path` string can contain several dot-separated
  key names. See also `valAt'`.

Totality: total
Visibility: export

maybeValAt' : (TomlValue -> Either TOMLErr a) -> String -> TomlValue -> Either TOMLErr (Maybe a)

  Extract and convert an optional value from a TOML
  value. The `path` string can contain several dot-separated
  key names. See also `valAt'`.

Totality: total
Visibility: export

maybeValAt : FromTOML a => String -> File Abs -> TomlValue -> Either TOMLErr (Maybe a)

  Extract and convert an optional value from a TOML
  value. The `path` string can contain several dot-separated
  key names. See also `valAt'`.

Totality: total
Visibility: export

readTOML : HasIO io => File Abs -> EitherT PackErr io TomlValue

  Reads a file and converts its content to a TOML value.

Visibility: export

readFromTOML : HasIO io => (0 a : Type) -> FromTOML a => File Abs -> EitherT PackErr io a

  Reads a file, converts its content to a TOML value, and
  extracts an Idris value from this.

Visibility: export

readOptionalFromTOML : HasIO io => (0 a : Type) -> FromTOML a => File Abs -> EitherT PackErr io a

  Reads a file, converts its content to a TOML value, and
  extracts an Idris value from this.

Visibility: export