| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
FreeC.Environment.Renamer
Description
Contains functions for renaming Haskell identifiers such that they can be safely used as Coq and Agda identifiers.
Identifiers must not conflict with Coq keywords and must not shadow types, constructors and functions from the Base library.
Renaming identifiers is also required because in Haskell the scopes for types and functions are separated. Thus it is allowed in Haskell for a data type to have the same name as one of it's constructors. In Coq this would cause a name conflict. Therefore, one of them needs to be renamed.
Synopsis
- mustRenameIdent :: String -> Environment -> Bool
- renameIdent :: String -> Environment -> String
- renameQualid :: String -> Environment -> Qualid
- renameAgdaQualid :: String -> Environment -> QName
- renameEntry :: EnvEntry -> Environment -> EnvEntry
- renameAndAddEntry :: EnvEntry -> Converter EnvEntry
- renameAndDefineTypeVar :: SrcSpan -> String -> Converter Qualid
- renameAndDefineAgdaTypeVar :: SrcSpan -> String -> Converter QName
- renameAndDefineVar :: SrcSpan -> Bool -> String -> Maybe Type -> Converter Qualid
- renameAndDefineAgdaVar :: SrcSpan -> Bool -> String -> Maybe Type -> Converter QName
- renameAndDefineLIRVar :: SrcSpan -> Bool -> String -> Maybe Type -> Converter QName
Predicates
mustRenameIdent :: String -> Environment -> Bool Source #
Tests whether the given Coq identifier must be renamed because it would otherwise conflict with a keyword, reserved or user defined identifier.
Rename Identifiers
renameIdent :: String -> Environment -> String Source #
Renames a Haskell identifier such that it can be safely used in Coq.
If the given identifier is a fresh identifier (i.e. contains an at-sign), the prefix of that identifier is used instead. If the identifier has no name conflict, it is return unchanged. If the identifier would cause a name conflict the smallest natural number is appended such that the resulting identifier does not cause a name conflict anymore. If the identifier already ends with a number, the enumeration will start from that number.
renameQualid :: String -> Environment -> Qualid Source #
Like renameIdent but the Coq identifier is wrapped in a Coq.Qualid.
renameAgdaQualid :: String -> Environment -> QName Source #
Generates a new Agda identifier based on the given String, the used
Agda.QNames from the environment and reserved identifier.
Define and Automatically Rename Identifiers
renameEntry :: EnvEntry -> Environment -> EnvEntry Source #
Renames the identifier of the given entry such that it does not cause any name conflict in the given environment.
Returns the renamed entry.
renameAndAddEntry :: EnvEntry -> Converter EnvEntry Source #
Renames the identifier of the given entry such that it does not cause any name conflict in the current environment and inserts it into the environment.
The entryIdent and entrySmartIdent fields are filled automatically.
The entryName field is used to generate the Coq name.
If it contains a qualified name, the entry is added to the scope both qualified and unqualified.
When the entry is a top-level entry (i.e., not a variable or type variable) the qualified name is also added to the environment.
Returns the renamed entry.
renameAndDefineTypeVar Source #
Arguments
| :: SrcSpan | The location of the type variable declaration. |
| -> String | The name of the type variable. |
| -> Converter Qualid |
Associates the identifier of a user defined Haskell type variable with an automatically generated Coq identifier that does not cause any name conflict in the current environment.
Returns the generated identifier.
renameAndDefineAgdaTypeVar Source #
Arguments
| :: SrcSpan | The location of the type variable declaration. |
| -> String | The name of the type variable. |
| -> Converter QName |
Associates the identifier of a user defined Haskell type variable with an automatically generated Agda identifier that does not cause any name conflict in the current environment.
Returns the generated identifier.
Arguments
| :: SrcSpan | The location of the variable declaration. |
| -> Bool | Whether the variable has not been lifted to the free monad. |
| -> String | The name of the variable. |
| -> Maybe Type | The type of the variable if it is known. |
| -> Converter Qualid |
Associates the identifier of a user defined Haskell variable with an automatically generated Coq identifier that does not cause any name conflict in the current environment.
Returns the generated identifier.
renameAndDefineAgdaVar Source #
Arguments
| :: SrcSpan | The location of the variable declaration. |
| -> Bool | Whether the variable has not been lifted to the free monad. |
| -> String | The name of the variable. |
| -> Maybe Type | The type of the variable if it is known. |
| -> Converter QName |
Associates the identifier of a user defined Haskell variable with an automatically generated Agda identifier that does not cause any name conflict in the current environment.
Returns the generated identifier.