Agda-2.5.3.20180526: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Scope.Monad

Contents

Description

The scope monad with operations.

Synopsis

The scope checking monad

type ScopeM = TCM Source #

To simplify interaction between scope checking and type checking (in particular when chasing imports), we use the same monad.

Errors

General operations

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.

modifyNamedScopeM :: ModuleName -> (Scope -> ScopeM (a, Scope)) -> ScopeM a Source #

Apply a monadic function to the top scope.

modifyCurrentScope :: (Scope -> Scope) -> ScopeM () Source #

Apply a function to the current scope.

modifyCurrentNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> ScopeM () Source #

Apply a function to the public or private name space.

withLocalVars :: ScopeM a -> ScopeM a Source #

Run a computation without changing the local variables.

bindVarsToBind :: ScopeM () Source #

After collecting some variable names in the scopeVarsToBind, bind them all simultaneously.

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.

freshAbstractName_ :: Name -> ScopeM Name Source #

freshAbstractName_ = freshAbstractName noFixity'

freshAbstractQName :: Fixity' -> Name -> ScopeM QName Source #

Create a fresh abstract qualified name.

Resolving names

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.

getNotation Source #

Arguments

:: 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

bindVariable Source #

Arguments

:: Binder

λ, Π, let, ...?

-> Name

Concrete name.

-> Name

Abstract name.

-> ScopeM () 

Bind a variable.

unbindVariable :: Name -> ScopeM a -> ScopeM a Source #

Temporarily unbind a variable. Used for non-recursive lets.

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.

data ScopeMemo Source #

Constructors

ScopeMemo 

Fields

  • memoNames :: Ren QName
     
  • memoModules :: [(ModuleName, (ModuleName, Bool))]

    Bool: did we copy recursively? We need to track this because we don't copy recursively when creating new modules for reexported functions (issue1985), but we might need to copy recursively later.

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 ImportedNames.

mapImportDir Source #

Arguments

:: (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.

mapUsing Source #

Arguments

:: (Eq a, Eq b) 
=> [ImportedName' (a, c) (b, d)]

Translation of names in using or hiding list.

-> Using' a b 
-> Using' c d 

Translation of Using or Hiding.

mapRenaming Source #

Arguments

:: (Eq a, Eq b) 
=> [ImportedName' (a, c) (b, d)]

Translation of renFrom names.

-> [ImportedName' (a, c) (b, d)]

Translation of rento names.

-> Renaming' a b 
-> Renaming' c d 

Translation of Renaming.