-- | 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. module FreeC.Environment.LookupOrFail where import Data.Composition ( (.:), (.:.) ) import qualified FreeC.Backend.Agda.Syntax as Agda import qualified FreeC.Backend.Coq.Syntax as Coq import FreeC.Environment import FreeC.Environment.Entry import FreeC.Environment.ModuleInterface import FreeC.IR.SrcSpan import qualified FreeC.IR.Syntax as IR import FreeC.Monad.Converter import FreeC.Monad.Reporter import FreeC.Pretty -- | 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. lookupAvailableModuleOrFail :: SrcSpan -> IR.ModName -> Converter ModuleInterface lookupAvailableModuleOrFail srcSpan modName = do maybeInterface <- inEnv $ lookupAvailableModule modName case maybeInterface of Just interface -> return interface Nothing -> reportFatal $ Message srcSpan Error $ "Module '" ++ showPretty modName ++ "' not found." -- | 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. lookupEntryOrFail :: SrcSpan -> IR.Scope -> IR.QName -> Converter EnvEntry lookupEntryOrFail srcSpan scope name = do maybeEntry <- inEnv $ lookupEntry scope name case maybeEntry of Just entry -> return entry Nothing -> reportFatal $ Message srcSpan Error $ "Identifier not in scope '" ++ showPretty name ++ "'" -- | 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. lookupIdentOrFail :: SrcSpan -- ^ The source location where the identifier is requested. -> IR.Scope -- ^ The scope to look the identifier up in. -> IR.QName -- ^ The Haskell identifier to look up. -> Converter Coq.Qualid lookupIdentOrFail srcSpan scope name = entryIdent <$> lookupEntryOrFail srcSpan scope name -- | 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. lookupAgdaIdentOrFail :: SrcSpan -- ^ The source location where the identifier is requested. -> IR.Scope -- ^ The scope to look the identifier up in. -> IR.QName -- ^ The Haskell identifier to look up. -> Converter Agda.QName lookupAgdaIdentOrFail srcSpan scope name = entryAgdaIdent <$> lookupEntryOrFail srcSpan scope name -- | Looks up an Agda identifier from the @IR.ValueScope@. lookupAgdaValIdentOrFail :: SrcSpan -> IR.QName -> Converter Agda.QName lookupAgdaValIdentOrFail = flip lookupAgdaIdentOrFail IR.ValueScope -- | Looks up an Agda identifier from the 'IR.FreshScope'. lookupAgdaFreshIdentOrFail :: SrcSpan -> IR.QName -> Converter Agda.QName lookupAgdaFreshIdentOrFail = flip lookupAgdaIdentOrFail IR.FreshScope -- | Looks up an Agda identifier from the @IR.TypeScope@. lookupAgdaTypeIdentOrFail :: SrcSpan -> IR.QName -> Converter Agda.QName lookupAgdaTypeIdentOrFail = flip lookupAgdaIdentOrFail IR.TypeScope -- | Looks up an Agda identifier and unqualifies the name. lookupUnQualAgdaIdentOrFail :: SrcSpan -> IR.Scope -> IR.QName -> Converter Agda.Name lookupUnQualAgdaIdentOrFail = fmap Agda.unqualify .:. lookupAgdaIdentOrFail -- | 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. lookupSmartIdentOrFail :: SrcSpan -- ^ The source location where the identifier is requested. -> IR.QName -- ^ The Haskell identifier to look up. -> Converter Coq.Qualid lookupSmartIdentOrFail srcSpan name = entrySmartIdent <$> lookupEntryOrFail srcSpan IR.ValueScope name -- | 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. lookupAgdaSmartIdentOrFail :: SrcSpan -- ^ The source location where the identifier is requested. -> IR.QName -- ^ The Haskell identifier to look up. -> Converter Agda.QName lookupAgdaSmartIdentOrFail srcSpan name = entryAgdaSmartIdent <$> lookupEntryOrFail srcSpan IR.ValueScope 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. lookupUnQualAgdaSmartIdentOrFail :: SrcSpan -- ^ The source location where the identifier is requested. -> IR.QName -- ^ The Haskell identifier to look up. -> Converter Agda.Name lookupUnQualAgdaSmartIdentOrFail = fmap Agda.unqualify .: lookupAgdaSmartIdentOrFail