| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
FreeC.Environment.LookupOrFail
Description
This module contains functions to lookup entries of the Environment
that (in contrast to the functions defined in FreeC.Environment)
report a fatal error message when there is no such entry.
Synopsis
- lookupAvailableModuleOrFail :: SrcSpan -> ModName -> Converter ModuleInterface
- lookupEntryOrFail :: SrcSpan -> Scope -> QName -> Converter EnvEntry
- lookupIdentOrFail :: SrcSpan -> Scope -> QName -> Converter Qualid
- lookupAgdaIdentOrFail :: SrcSpan -> Scope -> QName -> Converter QName
- lookupAgdaValIdentOrFail :: SrcSpan -> QName -> Converter QName
- lookupAgdaFreshIdentOrFail :: SrcSpan -> QName -> Converter QName
- lookupAgdaTypeIdentOrFail :: SrcSpan -> QName -> Converter QName
- lookupUnQualAgdaIdentOrFail :: SrcSpan -> Scope -> QName -> Converter Name
- lookupSmartIdentOrFail :: SrcSpan -> QName -> Converter Qualid
- lookupAgdaSmartIdentOrFail :: SrcSpan -> QName -> Converter QName
- lookupUnQualAgdaSmartIdentOrFail :: SrcSpan -> QName -> Converter Name
Documentation
lookupAvailableModuleOrFail :: SrcSpan -> ModName -> Converter ModuleInterface Source #
Looks up the module interface for the module with the given name in the current environment or reports a fatal error message if no such module interface is available.
If an error is reported, it points to the given source span.
lookupEntryOrFail :: SrcSpan -> Scope -> QName -> Converter EnvEntry Source #
Looks up an entry of the environment with the given name or reports a fatal error message if the identifier has not been defined or the name is ambiguous.
If an error is reported, it points to the given source span.
Arguments
| :: SrcSpan | The source location where the identifier is requested. |
| -> Scope | The scope to look the identifier up in. |
| -> QName | The Haskell identifier to look up. |
| -> Converter Qualid |
Looks up the Coq identifier for a Haskell function, (type) constructor or (type) variable with the given name or reports a fatal error message if the identifier has not been defined.
If an error is reported, it points to the given source span.
lookupAgdaIdentOrFail Source #
Arguments
| :: SrcSpan | The source location where the identifier is requested. |
| -> Scope | The scope to look the identifier up in. |
| -> QName | The Haskell identifier to look up. |
| -> Converter QName |
Looks up the Agda identifier for a Haskell function, (type) constructor or (type) variable with the given name or reports a fatal error message if the identifier has not been defined.
If an error is reported, it points to the given source span.
lookupAgdaValIdentOrFail :: SrcSpan -> QName -> Converter QName Source #
Looks up an Agda identifier from the IR.ValueScope.
lookupAgdaFreshIdentOrFail :: SrcSpan -> QName -> Converter QName Source #
Looks up an Agda identifier from the FreshScope.
lookupAgdaTypeIdentOrFail :: SrcSpan -> QName -> Converter QName Source #
Looks up an Agda identifier from the IR.TypeScope.
lookupUnQualAgdaIdentOrFail :: SrcSpan -> Scope -> QName -> Converter Name Source #
Looks up an Agda identifier and unqualifies the name.
lookupSmartIdentOrFail Source #
Arguments
| :: SrcSpan | The source location where the identifier is requested. |
| -> QName | The Haskell identifier to look up. |
| -> Converter Qualid |
Looks up the Coq identifier of a smart constructor of the Haskell data constructor with the given name or reports a fatal error message if there is no such constructor.
If an error is reported, it points to the given source span.
lookupAgdaSmartIdentOrFail Source #
Arguments
| :: SrcSpan | The source location where the identifier is requested. |
| -> QName | The Haskell identifier to look up. |
| -> Converter QName |
Looks up the Agda identifier of a smart constructor of the Haskell data constructor with the given name or reports a fatal error message if there is no such constructor.
If an error is reported, it points to the given source span.
lookupUnQualAgdaSmartIdentOrFail Source #
Arguments
| :: SrcSpan | The source location where the identifier is requested. |
| -> QName | The Haskell identifier to look up. |
| -> Converter Name |
Looks up the Agda identifier of a smart constructor of the Haskell data constructor with the given name and unqualifies it or reports a fatal error message if there is no such constructor.
If an error is reported, it points to the given source span.