Control.Monad.Free.Foil.TH.MkFreeFoil

Template Haskell generation for Free Foil (generic scope-safe representation of syntax).

Documentation

data FreeFoilConfig

Config for the Template Haskell generation of data types, pattern synonyms, and conversion functions for the Free Foil representation, based on a raw recursive representation.

Constructors

FreeFoilConfig

Fields

• rawQuantifiedNames :: [Name]

  Names of raw types that may include other binders and terms as components. Some examples of syntax that might be suitable here:

  1. a type scheme in HM-style type system (to explicitly disallow nested forall)
  2. defining equation of a function (which itself is not a term)
  3. data or type synonym declaration (which itself is not a type)
  4. unification constraints (quantified or not)
• freeFoilTermConfigs :: [FreeFoilTermConfig]

  Configurations for each term (e.g. expressions, types) group.

• freeFoilNameModifier :: String -> String

  Name modifier for the Free Foil conterpart of a raw type name. Normally, this is just id.

• freeFoilScopeNameModifier :: String -> String

  Name modifier for the scoped Free Foil conterpart of a raw type name. Normally, this is something like (Scoped ++).

• signatureNameModifier :: String -> String

  Name modifier for the signature conterpart of a raw type name or raw constructor name. Normally, this is something like (++ Sig).

• freeFoilConNameModifier :: String -> String

  Name modifier for the Free Foil conterpart (pattern synonym) of a raw constructor name. Normally, this is just id.

• freeFoilConvertToName :: String -> String

  Name of a conversion function (from raw to scope-safe) for a raw type name. Normally, this is something like ("to" ++).

• freeFoilConvertFromName :: String -> String

  Name of a conversion function (from scope-safe to raw) for a raw type name. Normally, this is something like ("from" ++).

data FreeFoilTermConfig

Config for a single term group, for the Template Haskell generation of data types, pattern synonyms, and conversion functions for the Free Foil representation, based on a raw recursive representation.

Constructors

FreeFoilTermConfig

Fields

• rawIdentName :: Name

  The type name for the identifiers. When identifiers occur in a term, they are converted to Name (with an appropriate type-level scope parameter). When identifiers occur in a pattern, they are converted to NameBinder (with appropriate type-level scope parameters).

• rawTermName :: Name

  The type name for the term. This will be the main recursive type to be converted into an AST.

• rawBindingName :: Name

  The type name for the binders (patterns). This will be the main binder type to used in AST-representation of the terms.

• rawScopeName :: Name

  The type name for the scoped term. This will be replaced with either ScopedAST (with outer scope) or AST (with inner scope) depending on its occurrence in a regular (sub)term or some quantified syntax.

• rawVarConName :: Name

  The constructor name for the variables in a term. This constructor will be replaced with the standard Var. It is expected to have exactly one field of type rawIdentName.

• rawSubTermNames :: [Name]

  Type names for subterm syntax. This will rely on the main term type (rawTermName) for recursive occurrences. Template Haskell will also generate signatures for these.

• rawSubScopeNames :: [Name]

  Type names for scoped subterm syntax. This will rely on the main term type (rawTermName) for recursive occurrences. Template Haskell will also generate signatures for these.

• intToRawIdentName :: Name

  Name of a function that converts Int to a raw identifier. Normally, this is something like (i -> VarIdent ("x" ++ show i)). This is required to generate standard conversions from scope-safe to raw representation.

• rawVarIdentToTermName :: Name

  Name of a function that converts a raw identifier into a raw term. Normally, this is some kind of Var or TypeVar data constructor. This is required to generate standard conversions from scope-safe to raw representation.

• rawTermToScopeName :: Name

  Name of a function that converts a raw term into a raw scoped term. Normally, this is some kind of ScopedTerm or ScopedType data constructor.

• rawScopeToTermName :: Name

  Name of a function that extracts a raw term from a raw scoped term. Normally, this is something like ((ScopedTerm term) -> term).

mkFreeFoil :: FreeFoilConfig -> Q [Dec]

Generate scope-safe types and pattern synonyms for a given raw set of types:

1. Scope-safe quantified types (e.g. type schemas, defining equations of functions, unification constraints, data/type declarations)
2. Scope-safe terms, scoped terms, subterms, scoped subterms.
3. Scope-safe patterns.
4. Signatures for terms, subterms, and scoped subterms.
5. Pattern synonyms for terms, subterms, and scoped subterms.

mkFreeFoilConversions :: FreeFoilConfig -> Q [Dec]

Generate conversions to and from scope-safe representation:

1. Conversions for scope-safe quantified types (e.g. type schemas, defining equations of functions, unification constraints, data/type declarations)
2. Conversions for scope-safe terms, scoped terms, subterms, scoped subterms.
3. CPS-style conversions for scope-safe patterns.
4. Helpers for signatures of terms, subterms, and scoped subterms.