Safe Haskell	None
Language	Haskell2010

FreeC.Environment

Contents

Environment
Module Information
Inserting Entries into the Environment
Modifying Entries in the Environment
Looking up Entries from the Environment

Description

This module contains a data type that encapsulates the state of the compiler. There are also utility functions to modify the state and retrieve information stored in the state.

Synopsis

data Environment = Environment {
- envAvailableModules :: Map ModName ModuleInterface
- envEntries :: Map ScopedName EnvEntry
- envDecArgs :: Map QName (Int, String)
- envFreshIdentCount :: Map String Int
}
emptyEnv :: Environment
makeModuleAvailable :: ModuleInterface -> Environment -> Environment
isModuleAvailable :: ModName -> Environment -> Bool
lookupAvailableModule :: ModName -> Environment -> Maybe ModuleInterface
addEntry :: EnvEntry -> Environment -> Environment
defineDecArg :: QName -> Int -> String -> Environment -> Environment
removeDecArg :: QName -> Environment -> Environment
modifyEntryIdent :: Scope -> QName -> Qualid -> Environment -> Environment
addEffectsToEntry :: QName -> [Effect] -> Environment -> Environment
lookupEntry :: Scope -> QName -> Environment -> Maybe EnvEntry
encapsulatesEffects :: QName -> Environment -> Bool
isFunction :: QName -> Environment -> Bool
isVariable :: QName -> Environment -> Bool
isPureVar :: QName -> Environment -> Bool
lookupModName :: Scope -> QName -> Environment -> Maybe ModName
lookupIdent :: Scope -> QName -> Environment -> Maybe Qualid
lookupSmartIdent :: QName -> Environment -> Maybe Qualid
usedIdents :: Environment -> [Qualid]
usedAgdaIdents :: Environment -> [QName]
lookupSrcSpan :: Scope -> QName -> Environment -> Maybe SrcSpan
lookupTypeArgs :: Scope -> QName -> Environment -> Maybe [TypeVarIdent]
lookupTypeArgArity :: Scope -> QName -> Environment -> Maybe Int
lookupArgTypes :: Scope -> QName -> Environment -> Maybe [Type]
lookupStrictArgs :: QName -> Environment -> Maybe [Bool]
lookupReturnType :: Scope -> QName -> Environment -> Maybe Type
lookupTypeScheme :: Scope -> QName -> Environment -> Maybe TypeScheme
lookupArity :: Scope -> QName -> Environment -> Maybe Int
lookupTypeSynonym :: QName -> Environment -> Maybe ([TypeVarIdent], Type)
needsFreeArgs :: QName -> Environment -> Bool
hasEffect :: Effect -> QName -> Environment -> Bool
lookupEffects :: QName -> Environment -> [Effect]
lookupDecArg :: QName -> Environment -> Maybe (Int, String)
lookupDecArgIndex :: QName -> Environment -> Maybe Int
lookupDecArgIdent :: QName -> Environment -> Maybe String

Environment

data Environment Source #

Data type that encapsulates the state of the converter.

Constructors

Environment

Fields

envAvailableModules :: Map ModName ModuleInterface
Maps names of modules that can be imported to their interface.
envEntries :: Map ScopedName EnvEntry
Maps original names of entries for declarations to the entries.
envDecArgs :: Map QName (Int, String)
Maps Haskell function names to the index and name of their decreasing argument. Contains no entry for non-recursive functions, but there are also entries for functions that are shadowed by local variables.
envFreshIdentCount :: Map String Int
The number of fresh identifiers that were used in the environment with a certain prefix.

Instances

Show Environment Source #
Instance details Defined in FreeC.Environment Methods showsPrec :: Int -> Environment -> ShowS Source # show :: Environment -> String Source # showList :: [Environment] -> ShowS Source #
Monad m => MonadState Environment (ConverterT m) Source #
Instance details Defined in FreeC.Monad.Converter Methods get :: ConverterT m Environment Source # put :: Environment -> ConverterT m () Source # state :: (Environment -> (a, Environment)) -> ConverterT m a Source #

emptyEnv :: Environment Source #

An environment that does not even contain any predefined types and functions.

Module Information

makeModuleAvailable :: ModuleInterface -> Environment -> Environment Source #

Inserts the interface of a module name into the environment such that it can be imported.

isModuleAvailable :: ModName -> Environment -> Bool Source #

Tests whether the module with the given name can be imported.

lookupAvailableModule :: ModName -> Environment -> Maybe ModuleInterface Source #

Looks up the environment of another module that can be imported.

Inserting Entries into the Environment

addEntry :: EnvEntry -> Environment -> Environment Source #

Inserts an entry into the given environment and associates it with its original name.

defineDecArg :: QName -> Int -> String -> Environment -> Environment Source #

Stores the index and name of the decreasing argument of a recursive function in the environment.

removeDecArg :: QName -> Environment -> Environment Source #

Removes the index of the decreasing argument of a recursive function from the environment (e.g., because the function has been transformed into a non-recursive function).

Modifying Entries in the Environment

modifyEntryIdent :: Scope -> QName -> Qualid -> Environment -> Environment Source #

Changes the Coq identifier of the entry with the given name in the given scope to the given identifier.

If such an entry does not exist, the environment is not changed.

addEffectsToEntry :: QName -> [Effect] -> Environment -> Environment Source #

Adds the given effects to the effects of the function with the given name.

If such a function does not exist, the environment is not changed.

Looking up Entries from the Environment

lookupEntry :: Scope -> QName -> Environment -> Maybe EnvEntry Source #

Looks up the entry with the given original name in the given scope of the given environment.

encapsulatesEffects :: QName -> Environment -> Bool Source #

Tests whether the function with the given name encapsulates effects.

Returns False if there is no such function.

isFunction :: QName -> Environment -> Bool Source #

Tests whether the given name identifies a function in the given environment.

Returns False if there is no such function.

isVariable :: QName -> Environment -> Bool Source #

Tests whether the given name identifies a local variable in the given environment.

Returns False if there is no such variable.

isPureVar :: QName -> Environment -> Bool Source #

Test whether the variable with the given name is not monadic.

lookupModName :: Scope -> QName -> Environment -> Maybe ModName Source #

Looks up the IR module name for a Haskell function, (type) constructor or (type) variable with the given name.

Returns Nothing if there is no such function, (type/smart) constructor, constructor or (type) variable with the given name or no module name is specified for that entry.

lookupIdent :: Scope -> QName -> Environment -> Maybe Qualid Source #

Looks up the Coq identifier for a Haskell function, (type) constructor or (type) variable with the given name.

Returns Nothing if there is no such function, (type/smart) constructor, constructor or (type) variable with the given name.

lookupSmartIdent :: QName -> Environment -> Maybe Qualid Source #

Looks up the Coq identifier for the smart constructor of the Haskell constructor with the given name.

Returns Nothing if there is no such constructor.

usedIdents :: Environment -> [Qualid] Source #

Gets a list of Coq identifiers for functions, (type/smart) constructors, (type/fresh) variables that were used in the given environment already.

usedAgdaIdents :: Environment -> [QName] Source #

Gets a list of Agda identifiers for functions, (type/smart) constructors, (type/fresh) variables that were used in the given environment already.

lookupSrcSpan :: Scope -> QName -> Environment -> Maybe SrcSpan Source #

Looks up the location of the declaration with the given name.

lookupTypeArgs :: Scope -> QName -> Environment -> Maybe [TypeVarIdent] Source #

Looks up the type variables used by the type synonym, (smart) constructor or type signature of the function with the given name.

Returns Nothing if there is no such type synonym, function or (smart) constructor with the given name.

lookupTypeArgArity :: Scope -> QName -> Environment -> Maybe Int Source #

Returns the length of the list returned by lookupTypeArgs.

lookupArgTypes :: Scope -> QName -> Environment -> Maybe [Type] Source #

Looks up the argument and return types of the function or (smart) constructor with the given name.

Returns Nothing if there is no such function or (smart) constructor with the given name.

lookupStrictArgs :: QName -> Environment -> Maybe [Bool] Source #

Looks up the strict arguments of the function with the given name.

Returns Nothing if there is no such function.

lookupReturnType :: Scope -> QName -> Environment -> Maybe Type Source #

Looks up the return type of the function or (smart) constructor with the given name.

Returns Nothing if there is no such function or (smart) constructor with the given name or the return type is not known.

lookupTypeScheme :: Scope -> QName -> Environment -> Maybe TypeScheme Source #

Gets the type scheme of the variable, function or constructor with the given name.

lookupArity :: Scope -> QName -> Environment -> Maybe Int Source #

Looks up the number of arguments expected by the Haskell function or smart constructor with the given name.

Returns Nothing if there is no such function or (smart) constructor with the given name.

lookupTypeSynonym :: QName -> Environment -> Maybe ([TypeVarIdent], Type) Source #

Looks up the type the type synonym with the given name is associated with.

Returns Nothing if there is no such type synonym.

needsFreeArgs :: QName -> Environment -> Bool Source #

Tests whether the function with the given name needs the arguments of the Free monad.

Returns False if there is no such function.

hasEffect :: Effect -> QName -> Environment -> Bool Source #

Tests whether the function with the given name has the given effect.

Returns False if there is no such function.

lookupEffects :: QName -> Environment -> [Effect] Source #

Looks up the effects of the function with the given name.

Returns [] if such a function does not exist.

lookupDecArg :: QName -> Environment -> Maybe (Int, String) Source #

Looks up the index and name of the decreasing argument of the recursive function with the given name.

Returns Nothing if there is no such recursive function.

lookupDecArgIndex :: QName -> Environment -> Maybe Int Source #

Like lookupDecArg but returns the decreasing argument's index only.

lookupDecArgIdent :: QName -> Environment -> Maybe String Source #

Like lookupDecArg but returns the decreasing argument's name only.