Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Scope.Operator

Description

Computing scopes of names that are relevant to parsing some raw expression.

Synopsis

data OperatorScope = OpScope {
- osHasOps :: !Bool
- osScope :: Map QName (List1 AbstractName)
- osLocals :: !(AssocList Name Name)
}
getOperatorScope :: Set QName -> ScopeInfo -> OperatorScope
getDefinedNames :: KindsOfNames -> OperatorScope -> [List1 NewNotation]
localNames :: ExprKind -> Maybe QName -> OperatorScope -> ScopeM ([QName], [NewNotation])

Documentation

data OperatorScope Source #

Names that are relevant to operator parsing.

Constructors

OpScope
Fields osHasOps :: !Bool Are there any operators or notations in scope? osScope :: Map QName (List1 AbstractName) All relevant names in global scope. osLocals :: !(AssocList Name Name) Relevant names in local scope.

Instances

Instances details

Pretty OperatorScope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: OperatorScope -> Doc Source #

prettyPrec :: Int -> OperatorScope -> Doc Source #

prettyList :: [OperatorScope] -> Doc Source #

Null OperatorScope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

empty :: OperatorScope Source #

null :: OperatorScope -> Bool Source #

NFData OperatorScope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: OperatorScope -> () #

Generic OperatorScope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep OperatorScope

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep OperatorScope = D1 ('MetaData "OperatorScope" "Agda.Syntax.Scope.Base" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "OpScope" 'PrefixI 'True) (S1 ('MetaSel ('Just "osHasOps") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "osScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName (List1 AbstractName))) :*: S1 ('MetaSel ('Just "osLocals") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (AssocList Name Name)))))

Methods

from :: OperatorScope -> Rep OperatorScope x #

to :: Rep OperatorScope x -> OperatorScope #

Show OperatorScope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> OperatorScope -> ShowS #

show :: OperatorScope -> String #

showList :: [OperatorScope] -> ShowS #

Eq OperatorScope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

(==) :: OperatorScope -> OperatorScope -> Bool #

(/=) :: OperatorScope -> OperatorScope -> Bool #

type Rep OperatorScope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep OperatorScope = D1 ('MetaData "OperatorScope" "Agda.Syntax.Scope.Base" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "OpScope" 'PrefixI 'True) (S1 ('MetaSel ('Just "osHasOps") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "osScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName (List1 AbstractName))) :*: S1 ('MetaSel ('Just "osLocals") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (AssocList Name Name)))))

getOperatorScope :: Set QName -> ScopeInfo -> OperatorScope Source #

getDefinedNames :: KindsOfNames -> OperatorScope -> [List1 NewNotation] Source #

localNames :: ExprKind -> Maybe QName -> OperatorScope -> ScopeM ([QName], [NewNotation]) Source #

Compute all names (first component) and operators/notations (second component) in scope.

For IsPattern, only constructor-like names are returned.