Safe Haskell	None
Language	Haskell2010

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 theNameRange :: Range Range of the name in the fixity declaration (used for correct highlighting, see issue #2140).

Instances

Eq Fixity' Source #
Methods (==) :: Fixity' -> Fixity' -> Bool # (/=) :: Fixity' -> Fixity' -> Bool #
Data Fixity' Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Fixity' -> c Fixity' # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity' # toConstr :: Fixity' -> Constr # dataTypeOf :: Fixity' -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Fixity') # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity') # gmapT :: (forall b. Data b => b -> b) -> Fixity' -> Fixity' # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r # gmapQ :: (forall d. Data d => d -> u) -> Fixity' -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity' -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' #
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 #
ToTerm Fixity' Source #
Methods toTerm :: TCM (Fixity' -> Term) Source # toTermR :: TCM (Fixity' -> ReduceM Term) Source #
PrimTerm Fixity' Source #
Methods primTerm :: Fixity' -> TCM Term 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) #
Data x => Data (ThingWithFixity x) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ThingWithFixity x -> c (ThingWithFixity x) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ThingWithFixity x) # toConstr :: ThingWithFixity x -> Constr # dataTypeOf :: ThingWithFixity x -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (ThingWithFixity x)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ThingWithFixity x)) # gmapT :: (forall b. Data b => b -> b) -> ThingWithFixity x -> ThingWithFixity x # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r # gmapQ :: (forall d. Data d => d -> u) -> ThingWithFixity x -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ThingWithFixity x -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) #
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	No fixity declared.
Related !Integer	Fixity level declared as the `Integer`.

Instances

Eq PrecedenceLevel Source #
Methods (==) :: PrecedenceLevel -> PrecedenceLevel -> Bool # (/=) :: PrecedenceLevel -> PrecedenceLevel -> Bool #
Data PrecedenceLevel Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PrecedenceLevel -> c PrecedenceLevel # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PrecedenceLevel # toConstr :: PrecedenceLevel -> Constr # dataTypeOf :: PrecedenceLevel -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c PrecedenceLevel) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PrecedenceLevel) # gmapT :: (forall b. Data b => b -> b) -> PrecedenceLevel -> PrecedenceLevel # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PrecedenceLevel -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PrecedenceLevel -> r # gmapQ :: (forall d. Data d => d -> u) -> PrecedenceLevel -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PrecedenceLevel -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PrecedenceLevel -> m PrecedenceLevel # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PrecedenceLevel -> m PrecedenceLevel # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PrecedenceLevel -> m PrecedenceLevel #
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 #
ToTerm PrecedenceLevel Source #
Methods toTerm :: TCM (PrecedenceLevel -> Term) Source # toTermR :: TCM (PrecedenceLevel -> ReduceM Term) Source #

data Associativity Source #

Associativity.

Constructors

NonAssoc
LeftAssoc
RightAssoc

Instances

Eq Associativity Source #
Methods (==) :: Associativity -> Associativity -> Bool # (/=) :: Associativity -> Associativity -> Bool #
Data Associativity Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Associativity -> c Associativity # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Associativity # toConstr :: Associativity -> Constr # dataTypeOf :: Associativity -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Associativity) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Associativity) # gmapT :: (forall b. Data b => b -> b) -> Associativity -> Associativity # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r # gmapQ :: (forall d. Data d => d -> u) -> Associativity -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Associativity -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity #
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 #
ToTerm Associativity Source #
Methods toTerm :: TCM (Associativity -> Term) Source # toTermR :: TCM (Associativity -> ReduceM Term) Source #

data Fixity Source #

Fixity of operators.

Constructors

Fixity
Fields fixityRange :: Range Range of the whole fixity declaration. fixityLevel :: !PrecedenceLevel fixityAssoc :: !Associativity

Instances

Eq Fixity Source #
Methods (==) :: Fixity -> Fixity -> Bool # (/=) :: Fixity -> Fixity -> Bool #
Data Fixity Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Fixity -> c Fixity # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity # toConstr :: Fixity -> Constr # dataTypeOf :: Fixity -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Fixity) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity) # gmapT :: (forall b. Data b => b -> b) -> Fixity -> Fixity # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r # gmapQ :: (forall d. Data d => d -> u) -> Fixity -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity #
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 #
ToTerm Fixity Source #
Methods toTerm :: TCM (Fixity -> Term) Source # toTermR :: TCM (Fixity -> ReduceM Term) 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 #
Data Precedence Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Precedence -> c Precedence # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Precedence # toConstr :: Precedence -> Constr # dataTypeOf :: Precedence -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Precedence) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Precedence) # gmapT :: (forall b. Data b => b -> b) -> Precedence -> Precedence # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Precedence -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Precedence -> r # gmapQ :: (forall d. Data d => d -> u) -> Precedence -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Precedence -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Precedence -> m Precedence # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Precedence -> m Precedence # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Precedence -> m Precedence #
Show Precedence Source #
Methods showsPrec :: Int -> Precedence -> ShowS # show :: Precedence -> String # showList :: [Precedence] -> ShowS #
Pretty Precedence Source #
Methods pretty :: Precedence -> Doc Source # prettyPrec :: Int -> Precedence -> Doc Source # prettyList :: [Precedence] -> Doc Source #

type PrecedenceStack = [Precedence] Source #

When printing we keep track of a stack of precedences in order to be able to decide whether it's safe to leave out parens around lambdas. An empty stack is equivalent to TopCtx. Invariant: `notElem TopCtx`.

pushPrecedence :: Precedence -> PrecedenceStack -> PrecedenceStack Source #

headPrecedence :: PrecedenceStack -> Precedence Source #

hiddenArgumentCtx :: Hiding -> Precedence Source #

The precedence corresponding to a possibly hidden argument.

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

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

opBrackets' :: Bool -> Fixity -> PrecedenceStack -> Bool Source #

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

lamBrackets' :: Bool -> PrecedenceStack -> 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. To decide we need to look at the stack of precedences and not just the current precedence. Example: m₁ >>= (λ x → x) >>= m₂ (for _>>=_ left associative). The first argument is the parenthesis preference. If True, we add parentheses also in right operand contexts where they aren't strictly needed.

lamBrackets :: PrecedenceStack -> Bool Source #

Preference for adding parentheses.

appBrackets :: PrecedenceStack -> Bool Source #

Does a function application need brackets?

appBrackets' :: Bool -> PrecedenceStack -> Bool Source #

Does a function application need brackets?

withAppBrackets :: PrecedenceStack -> Bool Source #

Does a with application need brackets?

piBrackets :: PrecedenceStack -> Bool Source #

Does a function space need brackets?

roundFixBrackets :: PrecedenceStack -> Bool Source #