Agda.Unused.Types.Context

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

Definitions

data Item

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

Show Item

Defined in Agda.Unused.Types.Context

Methods

showsPrec :: Int -> Item -> ShowS

show :: Item -> String

showList :: [Item] -> ShowS

data Module

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 ![Range] !Context

Instances

Show Module

Defined in Agda.Unused.Types.Context

Methods

showsPrec :: Int -> Module -> ShowS

show :: Module -> String

showList :: [Module] -> ShowS

data AccessModule

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

Constructors

AccessModule !Access ![Range] !Context

Instances

Show AccessModule

Defined in Agda.Unused.Types.Context

Methods

showsPrec :: Int -> AccessModule -> ShowS

show :: AccessModule -> String

showList :: [AccessModule] -> ShowS

data Context

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

Instances

Show Context

Defined in Agda.Unused.Types.Context

Methods

showsPrec :: Int -> Context -> ShowS

show :: Context -> String

showList :: [Context] -> ShowS

Semigroup Context

Prefer values from second context.

Defined in Agda.Unused.Types.Context

Methods

(<>) :: Context -> Context -> Context

sconcat :: NonEmpty Context -> Context

stimes :: Integral b => b -> Context -> Context

Monoid Context

Defined in Agda.Unused.Types.Context

Methods

mempty :: Context

mappend :: Context -> Context -> Context

mconcat :: [Context] -> Context

data AccessContext

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

Instances

Show AccessContext

Defined in Agda.Unused.Types.Context

Methods

showsPrec :: Int -> AccessContext -> ShowS

show :: AccessContext -> String

showList :: [AccessContext] -> ShowS

Semigroup AccessContext

Prefer values from second access context.

Defined in Agda.Unused.Types.Context

Methods

(<>) :: AccessContext -> AccessContext -> AccessContext

sconcat :: NonEmpty AccessContext -> AccessContext

stimes :: Integral b => b -> AccessContext -> AccessContext

Monoid AccessContext

Defined in Agda.Unused.Types.Context

Methods

mempty :: AccessContext

mappend :: AccessContext -> AccessContext -> AccessContext

mconcat :: [AccessContext] -> AccessContext

accessContextUnion :: AccessContext -> AccessContext -> AccessContext

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

A description of failure for an AccessContext lookup.

Constructors

LookupNotFound :: LookupError

LookupAmbiguous :: LookupError

Instances

Show LookupError

Defined in Agda.Unused.Types.Context

Methods

showsPrec :: Int -> LookupError -> ShowS

show :: LookupError -> String

showList :: [LookupError] -> ShowS

contextLookup :: QName -> Context -> Maybe [Range]

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

contextLookupItem :: QName -> Context -> Maybe Item

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

contextLookupModule :: QName -> Context -> Maybe Module

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

accessContextLookup :: QName -> AccessContext -> Either LookupError [Range]

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

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

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

accessContextLookupDefining :: QName -> AccessContext -> Either LookupError (Bool, [Range])

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

accessContextLookupSpecial :: QName -> AccessContext -> Maybe Bool

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

Insert

contextInsertRange :: Name -> Range -> Context -> Context

Insert a range for the given name, if present.

contextInsertRangeModule :: Name -> Range -> Context -> Context

Insert a range for all names in the given module, if present.

contextInsertRangeAll :: Range -> Context -> Context

Insert a range for all names in a context.

accessContextInsertRangeAll :: Range -> AccessContext -> AccessContext

Insert a range for all names in an access context.

Delete

contextDelete :: Name -> Context -> Context

Delete an item from the context.

contextDeleteModule :: Name -> Context -> Context

Delete a module from the context.

Rename

contextRename :: Name -> Name -> Context -> Context

Rename an item, if present.

contextRenameModule :: Name -> Name -> Context -> Context

Rename a module, if present.

Define

accessContextDefine :: Name -> AccessContext -> AccessContext

Mark an existing name as in process of being defined.

Ranges

moduleRanges :: Module -> [Range]

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

contextRanges :: Context -> [Range]

Get all ranges associated with names in the given context.

Match

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

Find all operators matching the given list of tokens.

Construction

item :: [Range] -> Maybe Name -> Item

Construct an Item representing an ordinary definition.

itemPattern :: [Range] -> Maybe Name -> Item

Construct an Item representing a pattern synonym.

itemConstructor :: [Range] -> Maybe Name -> Item

Construct an Item representing a constructor.

contextItem :: Name -> Item -> Context

Construct a Context with a single item.

contextModule :: Name -> Module -> Context

Construct a Context with a single module.

accessContextItem :: Name -> Access -> Item -> AccessContext

Construct an AccessContext with a single item, along with the relevant syntax item if applicable.

accessContextModule :: Name -> AccessModule -> AccessContext

Construct an AccessContext with a single access module.

accessContextModule' :: Name -> Access -> [Range] -> AccessContext -> AccessContext

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

Construct an access context with a single import.

Conversion

fromContext :: Access -> Context -> AccessContext

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

toContext :: AccessContext -> Context

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