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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Scope.Monad

Contents

- The scope checking monad
- General operations
- Names
- Resolving names
- Binding names
- Operations to do with record constructor names
- Module manipulation operations
- Import directives
- Opening a module
- Orphan instances

Description

The scope monad with operations.

Synopsis

- type ScopeM = TCM
- printLocals :: Int -> String -> ScopeM ()
- scopeWarning' :: CallStack -> DeclarationWarning' -> ScopeM ()
- scopeWarning :: HasCallStack => DeclarationWarning' -> ScopeM ()
- isDatatypeModule :: ReadTCState m => ModuleName -> m (Maybe DataOrRecordModule)
- getCurrentModule :: ReadTCState m => m ModuleName
- setCurrentModule :: MonadTCState m => ModuleName -> m ()
- withCurrentModule :: (ReadTCState m, MonadTCState m) => ModuleName -> m a -> m a
- withCurrentModule' :: (MonadTrans t, Monad (t ScopeM)) => ModuleName -> t ScopeM a -> t ScopeM a
- getNamedScope :: ModuleName -> ScopeM Scope
- getCurrentScope :: ScopeM Scope
- createModule :: Maybe DataOrRecordModule -> 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 ()
- setContextPrecedence :: PrecedenceStack -> ScopeM ()
- withContextPrecedence :: ReadTCState m => Precedence -> m a -> m a
- getLocalVars :: ReadTCState m => m LocalVars
- modifyLocalVars :: (LocalVars -> LocalVars) -> ScopeM ()
- setLocalVars :: LocalVars -> ScopeM ()
- withLocalVars :: ScopeM a -> ScopeM a
- outsideLocalVars :: Int -> ScopeM a -> ScopeM a
- withCheckNoShadowing :: ScopeM a -> ScopeM a
- checkNoShadowing :: LocalVars -> LocalVars -> ScopeM ()
- getVarsToBind :: ScopeM LocalVars
- addVarToBind :: Name -> LocalVar -> ScopeM ()
- bindVarsToBind :: ScopeM ()
- annotateDecls :: ReadTCState m => m [Declaration] -> m Declaration
- annotateExpr :: ReadTCState m => m Expr -> m Expr
- freshAbstractName :: Fixity' -> Name -> ScopeM Name
- freshAbstractName_ :: Name -> ScopeM Name
- freshAbstractQName :: Fixity' -> Name -> ScopeM QName
- freshAbstractQName' :: Name -> ScopeM QName
- freshConcreteName :: Range -> Int -> String -> ScopeM Name
- resolveName :: QName -> ScopeM ResolvedName
- resolveName' :: KindsOfNames -> Maybe (Set1 Name) -> QName -> ScopeM ResolvedName
- tryResolveName :: (ReadTCState m, HasBuiltins m, MonadError NameResolutionError m) => KindsOfNames -> Maybe (Set1 Name) -> QName -> m ResolvedName
- canHaveSuffixTest :: HasBuiltins m => m (QName -> Bool)
- resolveModule :: QName -> ScopeM AbstractModule
- getConcreteFixity :: Name -> ScopeM Fixity'
- getConcretePolarity :: Name -> ScopeM (Maybe PragmaPolarities)
- computeFixitiesAndPolarities :: DoWarn -> [Declaration] -> ScopeM a -> ScopeM a
- getNotation :: QName -> Set1 Name -> ScopeM NewNotation
- bindVariable :: BindingSource -> Name -> Name -> ScopeM ()
- unbindVariable :: Name -> ScopeM a -> ScopeM a
- bindName :: Access -> KindOfName -> Name -> QName -> ScopeM ()
- bindName' :: Access -> KindOfName -> NameMetadata -> Name -> QName -> ScopeM ()
- bindName'' :: Access -> KindOfName -> NameMetadata -> Name -> QName -> ScopeM (Maybe TypeError)
- rebindName :: Access -> KindOfName -> Name -> QName -> ScopeM ()
- bindModule :: Access -> Name -> ModuleName -> ScopeM ()
- bindQModule :: Access -> QName -> ModuleName -> ScopeM ()
- setRecordConstructor :: QName -> (QName, Maybe Induction) -> ScopeM ()
- getRecordConstructor :: ReadTCState m => QName -> m (Maybe (QName, Maybe Induction))
- isRecordConstructor :: QName -> Maybe QName
- stripNoNames :: ScopeM ()
- type WSM = StateT ScopeMemo ScopeM
- data ScopeMemo = ScopeMemo {
  - memoNames :: Ren QName
  - memoModules :: Map ModuleName (ModuleName, Bool)
  }
- memoToScopeInfo :: ScopeMemo -> ScopeCopyInfo
- copyName :: QName -> QName -> ScopeM ()
- copyScope :: QName -> ModuleName -> Scope -> ScopeM (Scope, ScopeCopyInfo)
- checkNoFixityInRenamingModule :: [Renaming] -> ScopeM ()
- verifyImportDirective :: [ImportedName] -> HidingDirective -> RenamingDirective -> ScopeM ()
- applyImportDirectiveM :: QName -> ImportDirective -> Scope -> ScopeM (ImportDirective, Scope)
- mapImportDir :: (Ord n1, Ord m1) => [ImportedName' (n1, n2) (m1, m2)] -> [ImportedName' (n1, n2) (m1, m2)] -> ImportDirective' n1 m1 -> ImportDirective' n2 m2
- data ImportedNameMap n1 n2 m1 m2 = ImportedNameMap {
  - inameMap :: Map n1 n2
  - imoduleMap :: Map m1 m2
  }
- importedNameMapFromList :: (Ord n1, Ord m1) => [ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
- lookupImportedName :: (Ord n1, Ord m1) => ImportedNameMap n1 n2 m1 m2 -> ImportedName' n1 m1 -> ImportedName' n2 m2
- mapRenaming :: (Ord n1, Ord m1) => ImportedNameMap n1 n2 m1 m2 -> ImportedNameMap n1 n2 m1 m2 -> Renaming' n1 m1 -> Renaming' n2 m2
- data OpenKind
  - = LetOpenModule
  - | TopOpenModule
- noGeneralizedVarsIfLetOpen :: OpenKind -> Scope -> Scope
- openModule_ :: OpenKind -> QName -> ImportDirective -> ScopeM ImportDirective
- openModule :: OpenKind -> Maybe ModuleName -> QName -> ImportDirective -> ScopeM ImportDirective

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

printLocals :: Int -> String -> ScopeM () Source #

scopeWarning' :: CallStack -> DeclarationWarning' -> ScopeM () Source #

scopeWarning :: HasCallStack => DeclarationWarning' -> ScopeM () Source #

# General operations

isDatatypeModule :: ReadTCState m => ModuleName -> m (Maybe DataOrRecordModule) Source #

getCurrentModule :: ReadTCState m => m ModuleName Source #

setCurrentModule :: MonadTCState m => ModuleName -> m () Source #

withCurrentModule :: (ReadTCState m, MonadTCState m) => ModuleName -> m a -> m a Source #

withCurrentModule' :: (MonadTrans t, Monad (t ScopeM)) => ModuleName -> t ScopeM a -> t ScopeM a Source #

getNamedScope :: ModuleName -> ScopeM Scope Source #

getCurrentScope :: ScopeM Scope Source #

createModule :: Maybe DataOrRecordModule -> ModuleName -> ScopeM () Source #

Create a new module with an empty scope. If the module is not new (e.g. duplicate `import`), don't erase its contents. (`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.

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

Apply a function to the current scope.

modifyCurrentScopeM :: (Scope -> ScopeM (a, Scope)) -> ScopeM a Source #

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

Apply a function to the public or private name space.

setContextPrecedence :: PrecedenceStack -> ScopeM () Source #

withContextPrecedence :: ReadTCState m => Precedence -> m a -> m a Source #

getLocalVars :: ReadTCState m => m LocalVars Source #

modifyLocalVars :: (LocalVars -> LocalVars) -> ScopeM () Source #

setLocalVars :: LocalVars -> ScopeM () Source #

withLocalVars :: ScopeM a -> ScopeM a Source #

Run a computation without changing the local variables.

outsideLocalVars :: Int -> ScopeM a -> ScopeM a Source #

Run a computation outside some number of local variables and add them back afterwards. This lets you bind variables in the middle of the context and is used when binding generalizable variables (#3735).

withCheckNoShadowing :: ScopeM a -> ScopeM a Source #

Check that the newly added variable have unique names.

checkNoShadowing Source #

Arguments

:: LocalVars | Old local scope
-> LocalVars | New local scope
-> ScopeM () |

getVarsToBind :: ScopeM LocalVars Source #

addVarToBind :: Name -> LocalVar -> ScopeM () Source #

bindVarsToBind :: ScopeM () Source #

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

annotateDecls :: ReadTCState m => m [Declaration] -> m Declaration Source #

annotateExpr :: ReadTCState m => m Expr -> m Expr Source #

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

freshAbstractQName' :: Name -> ScopeM QName Source #

freshConcreteName :: Range -> Int -> String -> ScopeM Name Source #

Create a concrete name that is not yet in scope. | NOTE: See `chooseName` in `Agda.Syntax.Translation.AbstractToConcrete` for similar logic. | NOTE: See `withName` in `Agda.Syntax.Translation.ReflectedToAbstract` for similar logic.

# Resolving names

resolveName :: QName -> ScopeM ResolvedName Source #

Look up the abstract name referred to by a given concrete name.

resolveName' :: KindsOfNames -> Maybe (Set1 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.)

tryResolveName Source #

Arguments

:: (ReadTCState m, HasBuiltins m, MonadError NameResolutionError m) |
=> KindsOfNames | Restrict search to these kinds of names.
-> Maybe (Set1 Name) | Unless `Nothing`, restrict search to match any of these names.
-> QName | Name to be resolved
-> m ResolvedName | If illegally ambiguous, throw error with the ambiguous name.

canHaveSuffixTest :: HasBuiltins m => m (QName -> Bool) Source #

Test if a given abstract name can appear with a suffix. Currently only true for the names of builtin sorts.

resolveModule :: QName -> ScopeM AbstractModule Source #

Look up a module in the scope.

getConcreteFixity :: Name -> ScopeM Fixity' Source #

Get the fixity of a not yet bound name.

getConcretePolarity :: Name -> ScopeM (Maybe PragmaPolarities) Source #

Get the polarities of a not yet bound name.

computeFixitiesAndPolarities :: DoWarn -> [Declaration] -> ScopeM a -> ScopeM a Source #

Collect the fixity/syntax declarations and polarity pragmas from the list of declarations and store them in the scope.

getNotation Source #

Arguments

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

:: BindingSource | `λ`, `Π`, `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.

bindName' :: Access -> KindOfName -> NameMetadata -> Name -> QName -> ScopeM () Source #

bindName'' :: Access -> KindOfName -> NameMetadata -> Name -> QName -> ScopeM (Maybe TypeError) Source #

Bind a name. Returns the `TypeError` if exists, but does not throw it.

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.

# Operations to do with record constructor names

setRecordConstructor :: QName -> (QName, Maybe Induction) -> ScopeM () Source #

Record (ha) that a given record has the specified constructor name.

getRecordConstructor :: ReadTCState m => QName -> m (Maybe (QName, Maybe Induction)) Source #

Get the internal `QName` for the name of a record constructor. If the name does not refer to a record type, `Nothing` is returned.

isRecordConstructor :: QName -> Maybe QName Source #

Is this the qualified name which refers to the constructor of an anonymous record (like `Foo.constructor`)?

If so, return the part of the name referring to the record (`Foo`).

# Module manipulation operations

stripNoNames :: ScopeM () Source #

Clear the scope of any no names.

type WSM = StateT ScopeMemo ScopeM Source #

data ScopeMemo Source #

Constructors

ScopeMemo |

Fields

- memoNames :: Ren QName
- memoModules :: Map 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.

memoToScopeInfo :: ScopeMemo -> ScopeCopyInfo Source #

copyName :: QName -> QName -> ScopeM () Source #

Mark a name as being a copy in the TC state.

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.

# Import directives

checkNoFixityInRenamingModule :: [Renaming] -> ScopeM () Source #

Warn about useless fixity declarations in `renaming` directives. Monadic for the sake of error reporting.

verifyImportDirective :: [ImportedName] -> HidingDirective -> RenamingDirective -> ScopeM () Source #

Check that an import directive doesn't contain repeated names.

applyImportDirectiveM Source #

Arguments

:: QName | Name of the scope, only for error reporting.
-> ImportDirective | Description of how scope is to be modified.
-> Scope | Input scope.
-> ScopeM (ImportDirective, Scope) | Scope-checked description, output scope.

Apply an import directive and check that all the names mentioned actually exist.

Monadic for the sake of error reporting.

mapImportDir Source #

Arguments

:: (Ord n1, Ord m1) |
=> [ImportedName' (n1, n2) (m1, m2)] | Translation of imported names.
-> [ImportedName' (n1, n2) (m1, m2)] | Translation of names defined by this import.
-> ImportDirective' n1 m1 |
-> ImportDirective' n2 m2 |

Translation of `ImportDirective`.

data ImportedNameMap n1 n2 m1 m2 Source #

A finite map for `ImportedName`s.

Constructors

ImportedNameMap |

Fields

- inameMap :: Map n1 n2
- imoduleMap :: Map m1 m2

importedNameMapFromList :: (Ord n1, Ord m1) => [ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2 Source #

Create a `ImportedNameMap`.

lookupImportedName :: (Ord n1, Ord m1) => ImportedNameMap n1 n2 m1 m2 -> ImportedName' n1 m1 -> ImportedName' n2 m2 Source #

Apply a `ImportedNameMap`.

mapRenaming Source #

Arguments

:: (Ord n1, Ord m1) |
=> ImportedNameMap n1 n2 m1 m2 | Translation of `renFrom` names and module names.
-> ImportedNameMap n1 n2 m1 m2 | Translation of `rento` names and module names.
-> Renaming' n1 m1 | Renaming before translation (1).
-> Renaming' n2 m2 | Renaming after translation (2).

Translation of `Renaming`.

# Opening a module

data OpenKind Source #

Constructors

LetOpenModule |
TopOpenModule |

noGeneralizedVarsIfLetOpen :: OpenKind -> Scope -> Scope Source #

openModule_ :: OpenKind -> QName -> ImportDirective -> ScopeM ImportDirective Source #

Open a module.

openModule :: OpenKind -> Maybe ModuleName -> QName -> ImportDirective -> ScopeM ImportDirective Source #

Open a module, possibly given an already resolved module name.

# Orphan instances

MonadFixityError ScopeM Source # |

Instance details

Methods

throwMultipleFixityDecls :: List1 (Name, Pair Fixity') -> ScopeM a Source #

throwMultiplePolarityPragmas :: List1 Name -> ScopeM a Source #

warnUnknownNamesInFixityDecl :: Set1 Name -> ScopeM () Source #

warnUnknownNamesInPolarityPragmas :: Set1 Name -> ScopeM () Source #

warnUnknownFixityInMixfixDecl :: Set1 Name -> ScopeM () Source #

warnPolarityPragmasButNotPostulates :: Set1 Name -> ScopeM () Source #

warnEmptyPolarityPragma :: Range -> ScopeM () Source #