This module contains functions for loading and decoding ModuleInterfaces from TOML configuration files.

The module interface file contains the entries of a ModuleInterface. The file format is TOML (see https://github.com/toml-lang/toml). JSON files can be decoded as well. The TOML format is preferred for configuration files maintained by humans and JSON should be used to read automatically generated (serialized) interfaces.

File contents

The TOML document is expected to contain four arrays of tables types, type-synonyms, constructors and functions. Each table in these arrays defines a data type, type synonym, constructor or function respectively. The expected contents of each table is described below. In addition, the module interface file contains meta information in the top-level table.

Top-Level

The top-level table must contain the following key/value pairs:

• version (Integer) the version of the configuration file format. The current version is moduleInterfaceFileFormatVersion. If there is a breaking change in the future, the module interface file format version should be updated. The parser accepts module interface files that use the most recent version only.
• module-name (String) the name of the module that is described by the module interface file.
• library-name (String) the name of the Coq library that contains the module.
• exported-types (Array of String) the names (haskell-name) of the type-level entries exported by the module. All other entries in the types and type-synonyms tables are "hidden" (i.e. cannot be used by an importing module directly).
• exported-values (Array of String) the names (haskell-name) of the value-level entries exported by the module. All other entries in the constructors and functions tables are "hidden" (i.e. cannot be used by an importing module directly).

Data types

The tables in the types array must contain the following key/value pairs:

• haskell-name (String) the qualified Haskell name of the type constructor in the module it has been defined in.
• coq-name (String) the identifier of the corresponding Coq type constructor.
• arity (Integer) the number of type arguments expected by the type constructor.
• cons-names (Array of String) the names of the constructors of the defined data type.

Type synonyms

The tables in the type-synonyms array must contain the following key/value pairs:

• haskell-name (String) the qualified Haskell name of the type synonym in the module it has been defined in.
• coq-name (String) the identifier of the corresponding Coq definition.
• arity (Integer) the number of type arguments expected by the type synonym.
• haskell-type (String) the Haskell type that is abbreviated by the type synonym.
• type-arguments (Array of String) the Haskell identifiers of the type arguments. Must be of length arity.

Constructors

The tables in the constructors array must contain the following key/value pairs:

• haskell-type (String) the Haskell type of the data constructor.
• haskell-name (String) the qualified Haskell name of the data constructor in the module it has been defined in.
• coq-name (String) the identifier of the corresponding Coq data constructor.
• coq-smart-name (String) the identifier of the corresponding Coq smart constructor.
• arity (Integer) the number of arguments expected by the data constructor.

Functions

The tables in the functions array must contain the following key/value pairs:

• haskell-type (String) the Haskell type of the function.
• haskell-name (String) the qualified Haskell name of the function in the module it has been defined in.
• coq-name (String) the identifier of the corresponding Coq function.
• arity (Integer) the number of arguments expected by the function.
• strict-args (Array of Boolean) whether the function is strict in in its arguments.
• effects (Array of String) the effects contained in the function, i.e. which type classes need to be passed.
• needs-free-args (Boolean) whether the arguments of the Free monad need to be passed to the function.

Additionally, the following optional key/value pairs are allowed.

• encapsulates-effects (Boolean, defaults to false) whether the function encapsulates effects. This property should only be set to true for selected functions from the base library. For example, the flag is set for functions from the QuickCheck extension.