Safe Haskell | None |
---|---|
Language | Haskell2010 |
The scope monad with operations.
- type ScopeM = TCM
- isDatatypeModule :: ModuleName -> ScopeM (Maybe DataOrRecord)
- getCurrentModule :: ScopeM ModuleName
- setCurrentModule :: ModuleName -> ScopeM ()
- withCurrentModule :: ModuleName -> ScopeM a -> ScopeM a
- withCurrentModule' :: (MonadTrans t, Monad (t ScopeM)) => ModuleName -> t ScopeM a -> t ScopeM a
- getNamedScope :: ModuleName -> ScopeM Scope
- getCurrentScope :: ScopeM Scope
- createModule :: Maybe DataOrRecord -> ModuleName -> ScopeM ()
- modifyScopes :: (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
- modifyNamedScope :: ModuleName -> (Scope -> Scope) -> ScopeM ()
- setNamedScope :: ModuleName -> Scope -> ScopeM ()
- modifyNamedScopeM :: ModuleName -> (Scope -> ScopeM (a, Scope)) -> ScopeM a
- modifyCurrentScope :: (Scope -> Scope) -> ScopeM ()
- modifyCurrentScopeM :: (Scope -> ScopeM (a, Scope)) -> ScopeM a
- modifyCurrentNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> ScopeM ()
- pushContextPrecedence :: Precedence -> ScopeM ()
- popContextPrecedence :: ScopeM ()
- withContextPrecedence :: Precedence -> ScopeM a -> ScopeM a
- getLocalVars :: ScopeM LocalVars
- modifyLocalVars :: (LocalVars -> LocalVars) -> ScopeM ()
- setLocalVars :: LocalVars -> ScopeM ()
- withLocalVars :: ScopeM a -> ScopeM a
- freshAbstractName :: Fixity' -> Name -> ScopeM Name
- freshAbstractName_ :: Name -> ScopeM Name
- freshAbstractQName :: Fixity' -> Name -> ScopeM QName
- data ResolvedName
- resolveName :: QName -> ScopeM ResolvedName
- resolveName' :: [KindOfName] -> Maybe (Set Name) -> QName -> ScopeM ResolvedName
- resolveModule :: QName -> ScopeM AbstractModule
- getNotation :: QName -> Set Name -> ScopeM NewNotation
- bindVariable :: Bool -> Name -> Name -> ScopeM ()
- bindName :: Access -> KindOfName -> Name -> QName -> ScopeM ()
- rebindName :: Access -> KindOfName -> Name -> QName -> ScopeM ()
- bindModule :: Access -> Name -> ModuleName -> ScopeM ()
- bindQModule :: Access -> QName -> ModuleName -> ScopeM ()
- stripNoNames :: ScopeM ()
- type WSM = StateT ScopeMemo ScopeM
- data ScopeMemo = ScopeMemo {
- memoNames :: Ren QName
- memoModules :: [(ModuleName, (ModuleName, Bool))]
- memoToScopeInfo :: ScopeMemo -> ScopeCopyInfo
- copyScope :: QName -> ModuleName -> Scope -> ScopeM (Scope, ScopeCopyInfo)
- applyImportDirectiveM :: QName -> ImportDirective -> Scope -> ScopeM (ImportDirective, Scope)
- lookupImportedName :: (Eq a, Eq b) => ImportedName' a b -> [ImportedName' (a, c) (b, d)] -> ImportedName' c d
- mapImportDir :: (Eq a, Eq b) => [ImportedName' (a, c) (b, d)] -> [ImportedName' (a, c) (b, d)] -> ImportDirective' a b -> ImportDirective' c d
- mapUsing :: (Eq a, Eq b) => [ImportedName' (a, c) (b, d)] -> Using' a b -> Using' c d
- mapRenaming :: (Eq a, Eq b) => [ImportedName' (a, c) (b, d)] -> [ImportedName' (a, c) (b, d)] -> Renaming' a b -> Renaming' c d
- openModule_ :: QName -> ImportDirective -> ScopeM ImportDirective
The scope checking monad
To simplify interaction between scope checking and type checking (in particular when chasing imports), we use the same monad.
Errors
isDatatypeModule :: ModuleName -> ScopeM (Maybe DataOrRecord) Source #
General operations
setCurrentModule :: ModuleName -> ScopeM () Source #
withCurrentModule :: ModuleName -> ScopeM a -> ScopeM a Source #
withCurrentModule' :: (MonadTrans t, Monad (t ScopeM)) => ModuleName -> t ScopeM a -> t ScopeM a Source #
getNamedScope :: ModuleName -> ScopeM Scope Source #
createModule :: Maybe DataOrRecord -> ModuleName -> ScopeM () Source #
Create a new module with an empty scope.
(Just
if it is a datatype or record module.)
modifyScopes :: (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM () Source #
Apply a function to the scope map.
modifyNamedScope :: ModuleName -> (Scope -> Scope) -> ScopeM () Source #
Apply a function to the given scope.
setNamedScope :: ModuleName -> Scope -> ScopeM () Source #
modifyNamedScopeM :: ModuleName -> (Scope -> ScopeM (a, Scope)) -> ScopeM a Source #
Apply a monadic function to the top scope.
modifyCurrentNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> ScopeM () Source #
Apply a function to the public or private name space.
pushContextPrecedence :: Precedence -> ScopeM () Source #
popContextPrecedence :: ScopeM () Source #
withContextPrecedence :: Precedence -> ScopeM a -> ScopeM a Source #
setLocalVars :: LocalVars -> ScopeM () Source #
withLocalVars :: ScopeM a -> ScopeM a Source #
Run a computation without changing the local variables.
Names
freshAbstractName :: Fixity' -> Name -> ScopeM Name Source #
Create a fresh abstract name from a concrete name.
This function is used when we translate a concrete name
in a binder. The Range
of the concrete name is
saved as the nameBindingSite
of the abstract name.
freshAbstractQName :: Fixity' -> Name -> ScopeM QName Source #
Create a fresh abstract qualified name.
Resolving names
data ResolvedName Source #
VarName | Local variable bound by λ, Π, module telescope, pattern, |
| |
DefinedName Access AbstractName | Function, data/record type, postulate. |
FieldName [AbstractName] | Record field name. Needs to be distinguished to parse copatterns. |
ConstructorName [AbstractName] | Data or record constructor name. |
PatternSynResName AbstractName | Name of pattern synonym. |
UnknownName | Unbound name. |
resolveName :: QName -> ScopeM ResolvedName Source #
Look up the abstract name referred to by a given concrete name.
resolveName' :: [KindOfName] -> Maybe (Set Name) -> QName -> ScopeM ResolvedName Source #
Look up the abstract name corresponding to a concrete name of a certain kind and/or from a given set of names. Sometimes we know already that we are dealing with a constructor or pattern synonym (e.g. when we have parsed a pattern). Then, we can ignore conflicting definitions of that name of a different kind. (See issue 822.)
resolveModule :: QName -> ScopeM AbstractModule Source #
Look up a module in the scope.
:: QName | |
-> Set Name | The name must correspond to one of the names in this set. |
-> ScopeM NewNotation |
Get the notation of a name. The name is assumed to be in scope.
Binding names
Bind a variable.
bindName :: Access -> KindOfName -> Name -> QName -> ScopeM () Source #
Bind a defined name. Must not shadow anything.
rebindName :: Access -> KindOfName -> Name -> QName -> ScopeM () Source #
Rebind a name. Use with care!
Ulf, 2014-06-29: Currently used to rebind the name defined by an
unquoteDecl, which is a QuotableName
in the body, but a DefinedName
later on.
bindModule :: Access -> Name -> ModuleName -> ScopeM () Source #
Bind a module name.
bindQModule :: Access -> QName -> ModuleName -> ScopeM () Source #
Bind a qualified module name. Adds it to the imports field of the scope.
Module manipulation operations
stripNoNames :: ScopeM () Source #
Clear the scope of any no names.
ScopeMemo | |
|
copyScope :: QName -> ModuleName -> Scope -> ScopeM (Scope, ScopeCopyInfo) Source #
Create a new scope with the given name from an old scope. Renames public names in the old scope to match the new name and returns the renamings.
applyImportDirectiveM :: QName -> ImportDirective -> Scope -> ScopeM (ImportDirective, Scope) Source #
Apply an import directive and check that all the names mentioned actually exist.
lookupImportedName :: (Eq a, Eq b) => ImportedName' a b -> [ImportedName' (a, c) (b, d)] -> ImportedName' c d Source #
A finite map for ImportedName
s.
:: (Eq a, Eq b) | |
=> [ImportedName' (a, c) (b, d)] | Translation of imported names. |
-> [ImportedName' (a, c) (b, d)] | Translation of names defined by this import. |
-> ImportDirective' a b | |
-> ImportDirective' c d |
Translation of ImportDirective
.
:: (Eq a, Eq b) | |
=> [ImportedName' (a, c) (b, d)] | Translation of names in |
-> Using' a b | |
-> Using' c d |
Translation of Using or Hiding
.
:: (Eq a, Eq b) | |
=> [ImportedName' (a, c) (b, d)] | Translation of |
-> [ImportedName' (a, c) (b, d)] | Translation of |
-> Renaming' a b | |
-> Renaming' c d |
Translation of Renaming
.
openModule_ :: QName -> ImportDirective -> ScopeM ImportDirective Source #
Open a module.