Safe Haskell	None
Language	Haskell98

Agda.Syntax.Fixity

Contents

Notation coupled with Fixity
Sections
Fixity
Precendence
Some lenses
Printing
NFData instances

Description

Definitions for fixity, precedence levels, and declared syntax.

Synopsis

Notation coupled with `Fixity`

data Fixity' Source #

The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.

Constructors

Fixity'
Fields theFixity :: !Fixity theNotation :: Notation

Instances

Eq Fixity' Source #
Methods (==) :: Fixity' -> Fixity' -> Bool # (/=) :: Fixity' -> Fixity' -> Bool #
Show Fixity' Source #
Methods showsPrec :: Int -> Fixity' -> ShowS # show :: Fixity' -> String # showList :: [Fixity'] -> ShowS #
NFData Fixity' Source #
Methods rnf :: Fixity' -> () #
KillRange Fixity' Source #
Methods killRange :: KillRangeT Fixity' Source #

data ThingWithFixity x Source #

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity'

Instances

Functor ThingWithFixity Source #
Methods fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b # (<$) :: a -> ThingWithFixity b -> ThingWithFixity a #
Foldable ThingWithFixity Source #
Methods fold :: Monoid m => ThingWithFixity m -> m # foldMap :: Monoid m => (a -> m) -> ThingWithFixity a -> m # foldr :: (a -> b -> b) -> b -> ThingWithFixity a -> b # foldr' :: (a -> b -> b) -> b -> ThingWithFixity a -> b # foldl :: (b -> a -> b) -> b -> ThingWithFixity a -> b # foldl' :: (b -> a -> b) -> b -> ThingWithFixity a -> b # foldr1 :: (a -> a -> a) -> ThingWithFixity a -> a # foldl1 :: (a -> a -> a) -> ThingWithFixity a -> a # toList :: ThingWithFixity a -> [a] # null :: ThingWithFixity a -> Bool # length :: ThingWithFixity a -> Int # elem :: Eq a => a -> ThingWithFixity a -> Bool # maximum :: Ord a => ThingWithFixity a -> a # minimum :: Ord a => ThingWithFixity a -> a # sum :: Num a => ThingWithFixity a -> a # product :: Num a => ThingWithFixity a -> a #
Traversable ThingWithFixity Source #
Methods traverse :: Applicative f => (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b) # sequenceA :: Applicative f => ThingWithFixity (f a) -> f (ThingWithFixity a) # mapM :: Monad m => (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b) # sequence :: Monad m => ThingWithFixity (m a) -> m (ThingWithFixity a) #
Show x => Show (ThingWithFixity x) Source #
Methods showsPrec :: Int -> ThingWithFixity x -> ShowS # show :: ThingWithFixity x -> String # showList :: [ThingWithFixity x] -> ShowS #
KillRange x => KillRange (ThingWithFixity x) Source #
Methods killRange :: KillRangeT (ThingWithFixity x) Source #

data NewNotation Source #

All the notation information related to a name.

Constructors

NewNotation

Fields

notaName :: QName
notaNames :: Set Name
The names the syntax and/or fixity belong to.
Invariant: The set is non-empty. Every name in the list matches notaName.
notaFixity :: Fixity
Associativity and precedence (fixity) of the names.
notation :: Notation
Syntax associated with the names.
notaIsOperator :: Bool
True if the notation comes from an operator (rather than a syntax declaration).

Instances

Show NewNotation Source #
Methods showsPrec :: Int -> NewNotation -> ShowS # show :: NewNotation -> String # showList :: [NewNotation] -> ShowS #

namesToNotation :: QName -> Name -> NewNotation Source #

If an operator has no specific notation, then it is computed from its name.

useDefaultFixity :: NewNotation -> NewNotation Source #

Replace noFixity by defaultFixity.

notationNames :: NewNotation -> [QName] Source #

Return the IdParts of a notation, the first part qualified, the other parts unqualified. This allows for qualified use of operators, e.g., M.for x ∈ xs return e, or x ℕ.+ y.

syntaxOf :: Name -> Notation Source #

Create a Notation (without binders) from a concrete Name. Does the obvious thing: Holes become NormalHoles, Ids become IdParts. If Name has no Holes, it returns noNotation.

noFixity' :: Fixity' Source #

mergeNotations :: [NewNotation] -> [NewNotation] Source #

Merges NewNotations that have the same precedence level and notation, with two exceptions:

Operators and notations coming from syntax declarations are kept separate.
If all instances of a given NewNotation have the same precedence level or are "unrelated", then they are merged. They get the given precedence level, if any, and otherwise they become unrelated (but related to each other).

If NewNotations that are merged have distinct associativities, then they get NonAssoc as their associativity.

Precondition: No Name may occur in more than one list element. Every NewNotation must have the same notaName.

Postcondition: No Name occurs in more than one list element.

Sections

data NotationSection Source #

Sections, as well as non-sectioned operators.

Constructors

NotationSection
Fields sectNotation :: NewNotation sectKind :: NotationKind For non-sectioned operators this should match the notation's `notationKind`. sectLevel :: Maybe PrecedenceLevel Effective precedence level. `Nothing` for closed notations. sectIsSection :: Bool `False` for non-sectioned operators.

Instances

Show NotationSection Source #
Methods showsPrec :: Int -> NotationSection -> ShowS # show :: NotationSection -> String # showList :: [NotationSection] -> ShowS #

noSection :: NewNotation -> NotationSection Source #

Converts a notation to a (non-)section.

Fixity

data PrecedenceLevel Source #

Precedence levels for operators.

Constructors

Unrelated
Related !Integer

Instances

Eq PrecedenceLevel Source #
Methods (==) :: PrecedenceLevel -> PrecedenceLevel -> Bool # (/=) :: PrecedenceLevel -> PrecedenceLevel -> Bool #
Ord PrecedenceLevel Source #
Methods compare :: PrecedenceLevel -> PrecedenceLevel -> Ordering # (<) :: PrecedenceLevel -> PrecedenceLevel -> Bool # (<=) :: PrecedenceLevel -> PrecedenceLevel -> Bool # (>) :: PrecedenceLevel -> PrecedenceLevel -> Bool # (>=) :: PrecedenceLevel -> PrecedenceLevel -> Bool # max :: PrecedenceLevel -> PrecedenceLevel -> PrecedenceLevel # min :: PrecedenceLevel -> PrecedenceLevel -> PrecedenceLevel #
Show PrecedenceLevel Source #
Methods showsPrec :: Int -> PrecedenceLevel -> ShowS # show :: PrecedenceLevel -> String # showList :: [PrecedenceLevel] -> ShowS #

data Associativity Source #

Associativity.

Constructors

NonAssoc
LeftAssoc
RightAssoc

Instances

Eq Associativity Source #
Methods (==) :: Associativity -> Associativity -> Bool # (/=) :: Associativity -> Associativity -> Bool #
Ord Associativity Source #
Methods compare :: Associativity -> Associativity -> Ordering # (<) :: Associativity -> Associativity -> Bool # (<=) :: Associativity -> Associativity -> Bool # (>) :: Associativity -> Associativity -> Bool # (>=) :: Associativity -> Associativity -> Bool # max :: Associativity -> Associativity -> Associativity # min :: Associativity -> Associativity -> Associativity #
Show Associativity Source #
Methods showsPrec :: Int -> Associativity -> ShowS # show :: Associativity -> String # showList :: [Associativity] -> ShowS #

data Fixity Source #

Fixity of operators.

Constructors

Fixity
Fields fixityRange :: Range fixityLevel :: !PrecedenceLevel fixityAssoc :: !Associativity

Instances

Eq Fixity Source #
Methods (==) :: Fixity -> Fixity -> Bool # (/=) :: Fixity -> Fixity -> Bool #
Ord Fixity Source #
Methods compare :: Fixity -> Fixity -> Ordering # (<) :: Fixity -> Fixity -> Bool # (<=) :: Fixity -> Fixity -> Bool # (>) :: Fixity -> Fixity -> Bool # (>=) :: Fixity -> Fixity -> Bool # max :: Fixity -> Fixity -> Fixity # min :: Fixity -> Fixity -> Fixity #
Show Fixity Source #
Methods showsPrec :: Int -> Fixity -> ShowS # show :: Fixity -> String # showList :: [Fixity] -> ShowS #
NFData Fixity Source #	Ranges are not forced.
Methods rnf :: Fixity -> () #
KillRange Fixity Source #
Methods killRange :: KillRangeT Fixity Source #
HasRange Fixity Source #
Methods getRange :: Fixity -> Range Source #

noFixity :: Fixity Source #

defaultFixity :: Fixity Source #

Precendence

data Precedence Source #

Precedence is associated with a context.

Constructors

TopCtx
FunctionSpaceDomainCtx
LeftOperandCtx Fixity
RightOperandCtx Fixity
FunctionCtx
ArgumentCtx
InsideOperandCtx
WithFunCtx
WithArgCtx
DotPatternCtx

Instances

Eq Precedence Source #
Methods (==) :: Precedence -> Precedence -> Bool # (/=) :: Precedence -> Precedence -> Bool #
Show Precedence Source #
Methods showsPrec :: Int -> Precedence -> ShowS # show :: Precedence -> String # showList :: [Precedence] -> ShowS #

hiddenArgumentCtx :: Hiding -> Precedence Source #

The precedence corresponding to a possibly hidden argument.

opBrackets :: Fixity -> Precedence -> Bool Source #

Do we need to bracket an operator application of the given fixity in a context with the given precedence.

lamBrackets :: Precedence -> Bool Source #

Does a lambda-like thing (lambda, let or pi) need brackets in the given context? A peculiar thing with lambdas is that they don't need brackets in certain right operand contexts. However, we insert brackets anyway, for the following reasons: