Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Unused.Types.Context

Contents

Definitions
Interface
Construction
Conversion

Description

Definitions and interface for the Context and AccessContext types, which represent namespaces of definitions.

Synopsis

data Item
data Module = Module !(Set Range) !Context
data AccessModule = AccessModule !Access !(Set Range) !Context
data Context
data AccessContext
accessContextUnion :: AccessContext -> AccessContext -> AccessContext
data LookupError where
- LookupNotFound :: LookupError
- LookupAmbiguous :: LookupError
contextLookupItem :: QName -> Context -> Maybe Item
contextLookupModule :: QName -> Context -> Maybe Module
accessContextLookup :: QName -> AccessContext -> Either LookupError (Set Range)
accessContextLookupModule :: QName -> AccessContext -> Either LookupError Module
accessContextLookupDefining :: QName -> AccessContext -> Either LookupError (Bool, Set Range)
accessContextLookupSpecial :: QName -> AccessContext -> Maybe Bool
contextInsertRangeAll :: Range -> Context -> Context
accessContextInsertRangeAll :: Range -> AccessContext -> AccessContext
contextDelete :: Name -> Context -> Context
contextDeleteModule :: Name -> Context -> Context
accessContextDefine :: Name -> AccessContext -> AccessContext
accessContextDefineFields :: AccessContext -> AccessContext
moduleRanges :: Module -> Set Range
contextRanges :: Context -> Set Range
accessContextRanges :: AccessContext -> Set Range
accessContextMatch :: [String] -> AccessContext -> [Name]
contextItem :: Name -> Item -> Context
contextModule :: Name -> Module -> Context
accessContextConstructor :: Name -> Access -> Set Range -> Maybe Name -> AccessContext
accessContextPattern :: Name -> Access -> Set Range -> Maybe Name -> AccessContext
accessContextField :: Name -> Access -> Set Range -> Maybe Name -> AccessContext
accessContextItem :: Name -> Access -> Set Range -> Maybe Name -> AccessContext
accessContextModule :: Name -> AccessModule -> AccessContext
accessContextModule' :: Name -> Access -> Set Range -> AccessContext -> AccessContext
accessContextImport :: QName -> Context -> AccessContext
fromContext :: Access -> Context -> AccessContext
toContext :: AccessContext -> Context

Definitions

data Item Source #

The data associated with a name in context. This includes:

Whether the name is a constructor, pattern synonym, or ordinary definition.
A list of ranges associated with the name, which includes the site of the original definition, as well as any relevant import or open statements.
Alternative syntax for the name, if any.

Instances

Instances details

Show Item Source #
Instance details Defined in Agda.Unused.Types.Context Methods showsPrec :: Int -> Item -> ShowS # show :: Item -> String # showList :: [Item] -> ShowS #

data Module Source #

The data associated with a module in context. This includes:

A list of ranges associated with the module, which includes the site of the original definition, as well as any relevant import or open statements.
The inner context of the module.

Constructors

Module !(Set Range) !Context

Instances

Instances details

Show Module Source #
Instance details Defined in Agda.Unused.Types.Context Methods showsPrec :: Int -> Module -> ShowS # show :: Module -> String # showList :: [Module] -> ShowS #

data AccessModule Source #

Like Module, but also recording whether the module is public or private.

Constructors

AccessModule !Access !(Set Range) !Context

Instances

Instances details

Show AccessModule Source #
Instance details Defined in Agda.Unused.Types.Context Methods showsPrec :: Int -> AccessModule -> ShowS # show :: AccessModule -> String # showList :: [AccessModule] -> ShowS #

data Context Source #

A namespace of definitions. Any Agda module produces a Context.

Instances

Instances details

Monoid Context Source #
Instance details Defined in Agda.Unused.Types.Context Methods mempty :: Context # mappend :: Context -> Context -> Context # mconcat :: [Context] -> Context #
Semigroup Context Source #	Prefer values from second context.
Instance details Defined in Agda.Unused.Types.Context Methods (<>) :: Context -> Context -> Context # sconcat :: NonEmpty Context -> Context # stimes :: Integral b => b -> Context -> Context #
Show Context Source #
Instance details Defined in Agda.Unused.Types.Context Methods showsPrec :: Int -> Context -> ShowS # show :: Context -> String # showList :: [Context] -> ShowS #

data AccessContext Source #

A namespace of definitions, which may be public or private. Any collection of Agda declarations produces an AccessContext, for example.

Instances

Instances details

Monoid AccessContext Source #
Instance details Defined in Agda.Unused.Types.Context Methods mempty :: AccessContext # mappend :: AccessContext -> AccessContext -> AccessContext # mconcat :: [AccessContext] -> AccessContext #
Semigroup AccessContext Source #	Prefer values from second access context.
Instance details Defined in Agda.Unused.Types.Context Methods (<>) :: AccessContext -> AccessContext -> AccessContext # sconcat :: NonEmpty AccessContext -> AccessContext # stimes :: Integral b => b -> AccessContext -> AccessContext #
Show AccessContext Source #
Instance details Defined in Agda.Unused.Types.Context Methods showsPrec :: Int -> AccessContext -> ShowS # show :: AccessContext -> String # showList :: [AccessContext] -> ShowS #

accessContextUnion :: AccessContext -> AccessContext -> AccessContext Source #

Like (<>), but public items take precedence over private items. This is important when combining contexts from successive declarations; for example:

module M where

  postulate
    A : Set

module N where

  postulate
    A : Set

  open M

x : N.A
x = ?

This code type-checks, and the identifier N.A refers to the postulate declared in the definition of N, not the definition opened from M.

Interface

Lookup

data LookupError where Source #

A description of failure for an AccessContext lookup.

Constructors

LookupNotFound :: LookupError
LookupAmbiguous :: LookupError

Instances

Instances details

Show LookupError Source #
Instance details Defined in Agda.Unused.Types.Context Methods showsPrec :: Int -> LookupError -> ShowS # show :: LookupError -> String # showList :: [LookupError] -> ShowS #

contextLookupItem :: QName -> Context -> Maybe Item Source #

Get the item for the given name, or Nothing if not in context.

contextLookupModule :: QName -> Context -> Maybe Module Source #

Get the inner module for the given name, or Nothing if not in context.

accessContextLookup :: QName -> AccessContext -> Either LookupError (Set Range) Source #

Get the ranges for the given name, or produce a LookupError.

accessContextLookupModule :: QName -> AccessContext -> Either LookupError Module Source #

Get the inner module for the given name, or produce a LookupError.

accessContextLookupDefining :: QName -> AccessContext -> Either LookupError (Bool, Set Range) Source #

Like accessContextLookup, but also return a boolean indicating whether we are currently defining the referenced item.

accessContextLookupSpecial :: QName -> AccessContext -> Maybe Bool Source #

Determine whether a name represents a constructor or pattern synonym. Return Nothing if the name is not in context.

Insert

contextInsertRangeAll :: Range -> Context -> Context Source #

Insert a range for all names in a context.

accessContextInsertRangeAll :: Range -> AccessContext -> AccessContext Source #

Insert a range for all names in an access context.

Delete

contextDelete :: Name -> Context -> Context Source #

Delete an item from the context.

contextDeleteModule :: Name -> Context -> Context Source #

Delete a module from the context.

Define

accessContextDefine :: Name -> AccessContext -> AccessContext Source #

Mark an existing name as in process of being defined.

accessContextDefineFields :: AccessContext -> AccessContext Source #

Mark all fields as in process of being defined.

Ranges

moduleRanges :: Module -> Set Range Source #

Get all ranges associated with names in the given module, including ranges associated with the module itself.

contextRanges :: Context -> Set Range Source #

Get all ranges associated with names in the given context.

accessContextRanges :: AccessContext -> Set Range Source #

Get all ranges associated with names in the given access context.

Match

accessContextMatch :: [String] -> AccessContext -> [Name] Source #

Find all operators matching the given list of tokens.

Construction

contextItem :: Name -> Item -> Context Source #

Construct a Context with a single item.

contextModule :: Name -> Module -> Context Source #

Construct a Context with a single module.

accessContextConstructor :: Name -> Access -> Set Range -> Maybe Name -> AccessContext Source #

Construct an AccessContext with a single constructor.

accessContextPattern :: Name -> Access -> Set Range -> Maybe Name -> AccessContext Source #

Construct an AccessContext with a single pattern synonym.

accessContextField :: Name -> Access -> Set Range -> Maybe Name -> AccessContext Source #

Construct an AccessContext with a single field.

accessContextItem :: Name -> Access -> Set Range -> Maybe Name -> AccessContext Source #

Construct an AccessContext with a single ordinary definition.

accessContextModule :: Name -> AccessModule -> AccessContext Source #

Construct an AccessContext with a single access module.

accessContextModule' :: Name -> Access -> Set Range -> AccessContext -> AccessContext Source #

Like accessContextModule, but taking an access context. We convert the given access context to an ordinary context using toContext:

accessContextModule' n a rs c
  = accessContextModule n (AccessModule a rs (toContext c))

accessContextImport :: QName -> Context -> AccessContext Source #

Construct an access context with a single import.

Conversion

fromContext :: Access -> Context -> AccessContext Source #

Convert a Context to AccessContext. Give all items the given access.

toContext :: AccessContext -> Context Source #

Convert an AccessContext to Context. Discard private items and imports.