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

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 [Occurrence]
- class Monad m => MonadFixityError m where
  - throwMultipleFixityDecls :: [(Name, [Fixity'])] -> m a
  - throwMultiplePolarityPragmas :: [Name] -> m a
  - warnUnknownNamesInFixityDecl :: [Name] -> m ()
  - warnUnknownNamesInPolarityPragmas :: [Name] -> m ()
  - warnUnknownFixityInMixfixDecl :: [Name] -> m ()
  - warnPolarityPragmasButNotPostulates :: [Name] -> m ()
- data DoWarn
  - = NoWarn
  - | DoWarn
- fixitiesAndPolarities :: MonadFixityError m => DoWarn -> [Declaration] -> m (Fixities, Polarities)

# Documentation

type Fixities = Map Name Fixity' Source #

type Polarities = Map Name [Occurrence] Source #

class Monad m => MonadFixityError m where Source #

Methods

throwMultipleFixityDecls :: [(Name, [Fixity'])] -> m a Source #

throwMultiplePolarityPragmas :: [Name] -> m a Source #

warnUnknownNamesInFixityDecl :: [Name] -> m () Source #

warnUnknownNamesInPolarityPragmas :: [Name] -> m () Source #

warnUnknownFixityInMixfixDecl :: [Name] -> m () Source #

warnPolarityPragmasButNotPostulates :: [Name] -> m () Source #

Instances

MonadFixityError ScopeM Source # |

Instance details

Defined in Agda.Syntax.Scope.Monad

Methods

throwMultipleFixityDecls :: [(Name, [Fixity'])] -> ScopeM a Source #

throwMultiplePolarityPragmas :: [Name] -> ScopeM a Source #

warnUnknownNamesInFixityDecl :: [Name] -> ScopeM () Source #

warnUnknownNamesInPolarityPragmas :: [Name] -> ScopeM () Source #

warnUnknownFixityInMixfixDecl :: [Name] -> ScopeM () Source #

warnPolarityPragmasButNotPostulates :: [Name] -> ScopeM () Source #

data DoWarn Source #

Constructors

NoWarn |
DoWarn |

Instances

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

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.