| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
FreeC.Environment.Fresh
Contents
Description
This module contains functions for generating fresh identifiers.
Fresh identifiers are identifiers that have been introduced artificially into the Haskell or Coq AST. They are guaranteed not to conflict with any other valid identifier.
Synopsis
- freshArgPrefix :: String
- freshNormalformArgPrefix :: String
- freshSharingArgPrefix :: String
- freshFuncPrefix :: String
- freshBoolPrefix :: String
- freshTypeVarPrefix :: String
- freshTypeArgPrefix :: String
- freshHaskellIdent :: String -> Converter String
- freshHaskellName :: Name -> Converter Name
- freshHaskellQName :: QName -> Converter QName
- freshTypeVar :: Converter Type
- freshCoqIdent :: String -> Converter String
- freshCoqQualid :: String -> Converter Qualid
- freshAgdaVar :: String -> Converter QName
- freshIRQName :: String -> Converter QName
Prefixes
freshArgPrefix :: String Source #
The prefix to use for artificially introduced variables of type a.
freshNormalformArgPrefix :: String Source #
The prefix to use for variables artificially introduced by normalization.
freshSharingArgPrefix :: String Source #
The prefix to use for variables artificially introduced by sharing.
freshFuncPrefix :: String Source #
The prefix to use for artificially introduced variables of type a -> b.
freshBoolPrefix :: String Source #
The prefix to use for artificially introduced variables of type Bool.
freshTypeVarPrefix :: String Source #
The prefix to use for artificially introduced type variables of kind *.
freshTypeArgPrefix :: String Source #
The prefix to use for artificially introduced type variables of kind *
that are passed as a type argument to a function.
Generating Fresh Haskell Identifiers
freshHaskellIdent :: String -> Converter String Source #
Gets the next fresh Haskell identifier from the current environment.
All fresh identifiers contain an at-sign (See internalIdentChar).
This ensures that they cannot be confused with actual Haskell identifiers.
The corresponding Coq identifier contains an underscore instead (see
FreeC.Environment.Renamer). The at-sign (or underscore) is preceded
by the given prefix and followed by an incrementing number (staring at
0).
If the given prefix is a fresh identifier itself (i.e. contains an at-sign), the prefix of that identifier is used instead.
The freshly generated identifier is not inserted into the environment, i.e. it can still be used to create a declaration.
freshHaskellName :: Name -> Converter Name Source #
Applies freshHaskellIdent to the given name.
Fails if the given name is a symbol.
freshHaskellQName :: QName -> Converter QName Source #
Like freshHaskellName but preserves the module name of qualified names.
freshTypeVar :: Converter Type Source #
Generates a fresh Haskell type variable.
Generating Fresh Coq Identifiers
freshCoqIdent :: String -> Converter String Source #
Gets the next fresh Haskell identifier from the current environment and renames it such that it can be used in Coq.
A VarEntry is added to the environment for the Haskell identifier in the
FreshScope name space. Since the fresh Haskell identifier is not
visible from the outside, the environment entry cannot be accessed
directly. Its main purpose is to prevent the the same fresh Coq identifier
to be issued twice.
freshCoqQualid :: String -> Converter Qualid Source #
Like freshCoqIdent but the resulting Coq identifier is wrapped in a
Term.
Generating Fresh Agda Identifiers
freshAgdaVar :: String -> Converter QName Source #
Generates a new Agda identifier based on the given name.