Agda

Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Concrete.Fixity

Description

Collecting fixity declarations (and polarity pragmas) for concrete declarations.

Synopsis

type Fixities = Map Name Fixity'
type Polarities = Map Name PragmaPolarities
class Monad m => MonadFixityError (m :: Type -> Type) where
- throwMultipleFixityDecls :: List1 (Name, Pair Fixity') -> m a
- throwMultiplePolarityPragmas :: List1 Name -> m a
- warnUnknownNamesInFixityDecl :: Set1 Name -> m ()
- warnUnknownNamesInPolarityPragmas :: Set1 Name -> m ()
- warnUnknownFixityInMixfixDecl :: Set1 Name -> m ()
- warnPolarityPragmasButNotPostulates :: Set1 Name -> m ()
- warnEmptyPolarityPragma :: Range -> m ()
data DoWarn
- = NoWarn
- | DoWarn
fixitiesAndPolarities :: MonadFixityError m => DoWarn -> [Declaration] -> m (Fixities, Polarities)

Documentation

type Fixities = Map Name Fixity' Source #

type Polarities = Map Name PragmaPolarities Source #

class Monad m => MonadFixityError (m :: Type -> Type) where Source #

Methods

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

throwMultiplePolarityPragmas :: List1 Name -> m a Source #

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

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

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

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

warnEmptyPolarityPragma :: Range -> m () Source #

Instances

Instances details

MonadFixityError ScopeM Source #

Instance details

Defined in Agda.Syntax.Scope.Monad

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 #

data DoWarn Source #

Constructors

NoWarn
DoWarn

Instances

Instances details

Show DoWarn Source #
Instance details Defined in Agda.Syntax.Concrete.Fixity Methods showsPrec :: Int -> DoWarn -> ShowS # show :: DoWarn -> String # showList :: [DoWarn] -> ShowS #
Eq DoWarn Source #
Instance details Defined in Agda.Syntax.Concrete.Fixity Methods (==) :: DoWarn -> DoWarn -> Bool # (/=) :: DoWarn -> DoWarn -> Bool #

fixitiesAndPolarities :: MonadFixityError m => DoWarn -> [Declaration] -> m (Fixities, Polarities) Source #

Get the fixities and polarity pragmas from the current block. Doesn't go inside modules and where blocks. The reason for this is that these declarations have to appear at the same level (or possibly outside an abstract or mutual block) as their target declaration.