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

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

- data Fixity' = Fixity' {
  - theFixity :: !Fixity
  - theNotation :: Notation
  - theNameRange :: Range
  }
- data ThingWithFixity x = ThingWithFixity x Fixity'
- data NewNotation = NewNotation {
  - notaName :: QName
  - notaNames :: Set Name
  - notaFixity :: Fixity
  - notation :: Notation
  - notaIsOperator :: Bool
  }
- namesToNotation :: QName -> Name -> NewNotation
- useDefaultFixity :: NewNotation -> NewNotation
- notationNames :: NewNotation -> [QName]
- syntaxOf :: Name -> Notation
- noFixity' :: Fixity'
- mergeNotations :: [NewNotation] -> [NewNotation]
- data NotationSection = NotationSection {
  - sectNotation :: NewNotation
  - sectKind :: NotationKind
  - sectLevel :: Maybe PrecedenceLevel
  - sectIsSection :: Bool
  }
- noSection :: NewNotation -> NotationSection
- data PrecedenceLevel
  - = Unrelated
  - | Related !Integer
- data Associativity
  - = NonAssoc
  - | LeftAssoc
  - | RightAssoc
- data Fixity = Fixity {
  - fixityRange :: Range
  - fixityLevel :: !PrecedenceLevel
  - fixityAssoc :: !Associativity
  }
- noFixity :: Fixity
- defaultFixity :: Fixity
- data ParenPreference
  - = PreferParen
  - | PreferParenless
- preferParen :: ParenPreference -> Bool
- preferParenless :: ParenPreference -> Bool
- data Precedence
  - = TopCtx
  - | FunctionSpaceDomainCtx
  - | LeftOperandCtx Fixity
  - | RightOperandCtx Fixity ParenPreference
  - | FunctionCtx
  - | ArgumentCtx ParenPreference
  - | InsideOperandCtx
  - | WithFunCtx
  - | WithArgCtx
  - | DotPatternCtx
- type PrecedenceStack = [Precedence]
- pushPrecedence :: Precedence -> PrecedenceStack -> PrecedenceStack
- headPrecedence :: PrecedenceStack -> Precedence
- argumentCtx_ :: Precedence
- opBrackets :: Fixity -> PrecedenceStack -> Bool
- opBrackets' :: Bool -> Fixity -> PrecedenceStack -> Bool
- lamBrackets :: PrecedenceStack -> Bool
- appBrackets :: PrecedenceStack -> Bool
- appBrackets' :: Bool -> PrecedenceStack -> Bool
- withAppBrackets :: PrecedenceStack -> Bool
- piBrackets :: PrecedenceStack -> Bool
- roundFixBrackets :: PrecedenceStack -> Bool
- _notaFixity :: Lens' Fixity NewNotation
- _fixityAssoc :: Lens' Associativity Fixity
- _fixityLevel :: Lens' PrecedenceLevel Fixity

# 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 # |
Instance details Defined in Agda.Syntax.Fixity Methods (==) :: Fixity' -> Fixity' -> Bool Source # (/=) :: Fixity' -> Fixity' -> Bool Source #
Data Fixity' Source # |

Instance details

Defined in Agda.Syntax.Fixity

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Fixity' -> c Fixity' Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity' Source #

toConstr :: Fixity' -> Constr Source #

dataTypeOf :: Fixity' -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Fixity') Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity') Source #

gmapT :: (forall b. Data b => b -> b) -> Fixity' -> Fixity' Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Fixity' -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity' -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' Source #

Show Fixity' Source # |
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> Fixity' -> ShowS Source # show :: Fixity' -> String Source # showList :: [Fixity'] -> ShowS Source #
NFData Fixity' Source # |
Instance details Defined in Agda.Syntax.Fixity Methods rnf :: Fixity' -> () Source #
Pretty Fixity' Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Fixity' -> Doc Source # prettyPrec :: Int -> Fixity' -> Doc Source # prettyList :: [Fixity'] -> Doc Source #
KillRange Fixity' Source # |
Instance details Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT Fixity' Source #
EmbPrj Fixity' Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Fixity' -> S Int32 Source # icod_ :: Fixity' -> S Int32 Source # value :: Int32 -> R Fixity' Source #
ToTerm Fixity' Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Fixity' -> Term) Source # toTermR :: TCM (Fixity' -> ReduceM Term) Source #
PrimTerm Fixity' Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Fixity' -> TCM Term Source #

data ThingWithFixity x Source #

Decorating something with `Fixity'`.

Constructors

ThingWithFixity x Fixity' |

Instances

Functor ThingWithFixity Source # |
Instance details Defined in Agda.Syntax.Fixity Methods fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b Source # (<$) :: a -> ThingWithFixity b -> ThingWithFixity a Source #
Foldable ThingWithFixity Source # |

Instance details

Defined in Agda.Syntax.Fixity

Methods

fold :: Monoid m => ThingWithFixity m -> m Source #

foldMap :: Monoid m => (a -> m) -> ThingWithFixity a -> m Source #

foldr :: (a -> b -> b) -> b -> ThingWithFixity a -> b Source #

foldr' :: (a -> b -> b) -> b -> ThingWithFixity a -> b Source #

foldl :: (b -> a -> b) -> b -> ThingWithFixity a -> b Source #

foldl' :: (b -> a -> b) -> b -> ThingWithFixity a -> b Source #

foldr1 :: (a -> a -> a) -> ThingWithFixity a -> a Source #

foldl1 :: (a -> a -> a) -> ThingWithFixity a -> a Source #

toList :: ThingWithFixity a -> [a] Source #

null :: ThingWithFixity a -> Bool Source #

length :: ThingWithFixity a -> Int Source #

elem :: Eq a => a -> ThingWithFixity a -> Bool Source #

maximum :: Ord a => ThingWithFixity a -> a Source #

minimum :: Ord a => ThingWithFixity a -> a Source #

sum :: Num a => ThingWithFixity a -> a Source #

product :: Num a => ThingWithFixity a -> a Source #

Traversable ThingWithFixity Source # |
Instance details Defined in Agda.Syntax.Fixity Methods traverse :: Applicative f => (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b) Source # sequenceA :: Applicative f => ThingWithFixity (f a) -> f (ThingWithFixity a) Source # mapM :: Monad m => (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b) Source # sequence :: Monad m => ThingWithFixity (m a) -> m (ThingWithFixity a) Source #
Data x => Data (ThingWithFixity x) Source # |

Instance details

Defined in Agda.Syntax.Fixity

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ThingWithFixity x -> c (ThingWithFixity x) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ThingWithFixity x) Source #

toConstr :: ThingWithFixity x -> Constr Source #

dataTypeOf :: ThingWithFixity x -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ThingWithFixity x)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ThingWithFixity x)) Source #

gmapT :: (forall b. Data b => b -> b) -> ThingWithFixity x -> ThingWithFixity x Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ThingWithFixity x -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ThingWithFixity x -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) Source #

Show x => Show (ThingWithFixity x) Source # |
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> ThingWithFixity x -> ShowS Source # show :: ThingWithFixity x -> String Source # showList :: [ThingWithFixity x] -> ShowS Source #
Pretty (ThingWithFixity Name) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ThingWithFixity Name -> Doc Source # prettyPrec :: Int -> ThingWithFixity Name -> Doc Source # prettyList :: [ThingWithFixity Name] -> Doc Source #
KillRange x => KillRange (ThingWithFixity x) Source # |
Instance details Defined in Agda.Syntax.Fixity 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 # |
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> NewNotation -> ShowS Source # show :: NewNotation -> String Source # showList :: [NewNotation] -> ShowS Source #

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 `IdPart`s 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: `Hole`s become `NormalHole`s, `Id`s become `IdParts`. If `Name` has no `Hole`s, it returns `noNotation`.

noFixity' :: Fixity' Source #

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

Merges `NewNotation`s 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 `NewNotation`s 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 # |
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> NotationSection -> ShowS Source # show :: NotationSection -> String Source # showList :: [NotationSection] -> ShowS Source #

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 # |
Instance details Defined in Agda.Syntax.Fixity Methods (==) :: PrecedenceLevel -> PrecedenceLevel -> Bool Source # (/=) :: PrecedenceLevel -> PrecedenceLevel -> Bool Source #
Data PrecedenceLevel Source # |

Instance details

Defined in Agda.Syntax.Fixity

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PrecedenceLevel -> c PrecedenceLevel Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PrecedenceLevel Source #

toConstr :: PrecedenceLevel -> Constr Source #

dataTypeOf :: PrecedenceLevel -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PrecedenceLevel) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PrecedenceLevel) Source #

gmapT :: (forall b. Data b => b -> b) -> PrecedenceLevel -> PrecedenceLevel Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PrecedenceLevel -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PrecedenceLevel -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> PrecedenceLevel -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PrecedenceLevel -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PrecedenceLevel -> m PrecedenceLevel Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PrecedenceLevel -> m PrecedenceLevel Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PrecedenceLevel -> m PrecedenceLevel Source #

Ord PrecedenceLevel Source # |

Instance details

Defined in Agda.Syntax.Fixity

Methods

compare :: PrecedenceLevel -> PrecedenceLevel -> Ordering Source #

(<) :: PrecedenceLevel -> PrecedenceLevel -> Bool Source #

(<=) :: PrecedenceLevel -> PrecedenceLevel -> Bool Source #

(>) :: PrecedenceLevel -> PrecedenceLevel -> Bool Source #

(>=) :: PrecedenceLevel -> PrecedenceLevel -> Bool Source #

max :: PrecedenceLevel -> PrecedenceLevel -> PrecedenceLevel Source #

min :: PrecedenceLevel -> PrecedenceLevel -> PrecedenceLevel Source #

Show PrecedenceLevel Source # |
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> PrecedenceLevel -> ShowS Source # show :: PrecedenceLevel -> String Source # showList :: [PrecedenceLevel] -> ShowS Source #
EmbPrj PrecedenceLevel Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: PrecedenceLevel -> S Int32 Source # icod_ :: PrecedenceLevel -> S Int32 Source # value :: Int32 -> R PrecedenceLevel Source #
ToTerm PrecedenceLevel Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (PrecedenceLevel -> Term) Source # toTermR :: TCM (PrecedenceLevel -> ReduceM Term) Source #

data Associativity Source #

Associativity.

Constructors

NonAssoc |
LeftAssoc |
RightAssoc |

Instances

Eq Associativity Source # |
Instance details Defined in Agda.Syntax.Fixity Methods (==) :: Associativity -> Associativity -> Bool Source # (/=) :: Associativity -> Associativity -> Bool Source #
Data Associativity Source # |

Instance details

Defined in Agda.Syntax.Fixity

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Associativity -> c Associativity Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Associativity Source #

toConstr :: Associativity -> Constr Source #

dataTypeOf :: Associativity -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Associativity) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Associativity) Source #

gmapT :: (forall b. Data b => b -> b) -> Associativity -> Associativity Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Associativity -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Associativity -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity Source #

Ord Associativity Source # |

Instance details

Defined in Agda.Syntax.Fixity

Methods

compare :: Associativity -> Associativity -> Ordering Source #

(<) :: Associativity -> Associativity -> Bool Source #

(<=) :: Associativity -> Associativity -> Bool Source #

(>) :: Associativity -> Associativity -> Bool Source #

(>=) :: Associativity -> Associativity -> Bool Source #

max :: Associativity -> Associativity -> Associativity Source #

min :: Associativity -> Associativity -> Associativity Source #

Show Associativity Source # |
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> Associativity -> ShowS Source # show :: Associativity -> String Source # showList :: [Associativity] -> ShowS Source #
EmbPrj Associativity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Associativity -> S Int32 Source # icod_ :: Associativity -> S Int32 Source # value :: Int32 -> R Associativity Source #
ToTerm Associativity Source # |
Instance details Defined in Agda.TypeChecking.Primitive 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 # |
Instance details Defined in Agda.Syntax.Fixity Methods (==) :: Fixity -> Fixity -> Bool Source # (/=) :: Fixity -> Fixity -> Bool Source #
Data Fixity Source # |

Instance details

Defined in Agda.Syntax.Fixity

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Fixity -> c Fixity Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity Source #

toConstr :: Fixity -> Constr Source #

dataTypeOf :: Fixity -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Fixity) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity) Source #

gmapT :: (forall b. Data b => b -> b) -> Fixity -> Fixity Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Fixity -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity Source #

Ord Fixity Source # |
Instance details Defined in Agda.Syntax.Fixity Methods compare :: Fixity -> Fixity -> Ordering Source # (<) :: Fixity -> Fixity -> Bool Source # (<=) :: Fixity -> Fixity -> Bool Source # (>) :: Fixity -> Fixity -> Bool Source # (>=) :: Fixity -> Fixity -> Bool Source # max :: Fixity -> Fixity -> Fixity Source # min :: Fixity -> Fixity -> Fixity Source #
Show Fixity Source # |
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> Fixity -> ShowS Source # show :: Fixity -> String Source # showList :: [Fixity] -> ShowS Source #
NFData Fixity Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Fixity Methods rnf :: Fixity -> () Source #
Pretty Fixity Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Fixity -> Doc Source # prettyPrec :: Int -> Fixity -> Doc Source # prettyList :: [Fixity] -> Doc Source #
KillRange Fixity Source # |
Instance details Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT Fixity Source #
HasRange Fixity Source # |
Instance details Defined in Agda.Syntax.Fixity Methods getRange :: Fixity -> Range Source #
EmbPrj Fixity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Fixity -> S Int32 Source # icod_ :: Fixity -> S Int32 Source # value :: Int32 -> R Fixity Source #
ToTerm Fixity Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Fixity -> Term) Source # toTermR :: TCM (Fixity -> ReduceM Term) Source #

noFixity :: Fixity Source #

defaultFixity :: Fixity Source #

data ParenPreference Source #

Do we prefer parens around arguments like `λ x → x` or not? See `lamBrackets`.

Constructors

PreferParen |
PreferParenless |

Instances

Eq ParenPreference Source # |
Instance details Defined in Agda.Syntax.Fixity Methods (==) :: ParenPreference -> ParenPreference -> Bool Source # (/=) :: ParenPreference -> ParenPreference -> Bool Source #
Data ParenPreference Source # |

Instance details

Defined in Agda.Syntax.Fixity

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ParenPreference -> c ParenPreference Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ParenPreference Source #

toConstr :: ParenPreference -> Constr Source #

dataTypeOf :: ParenPreference -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ParenPreference) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ParenPreference) Source #

gmapT :: (forall b. Data b => b -> b) -> ParenPreference -> ParenPreference Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ParenPreference -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ParenPreference -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ParenPreference -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ParenPreference -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ParenPreference -> m ParenPreference Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ParenPreference -> m ParenPreference Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ParenPreference -> m ParenPreference Source #

Ord ParenPreference Source # |

Instance details

Defined in Agda.Syntax.Fixity

Methods

compare :: ParenPreference -> ParenPreference -> Ordering Source #

(<) :: ParenPreference -> ParenPreference -> Bool Source #

(<=) :: ParenPreference -> ParenPreference -> Bool Source #

(>) :: ParenPreference -> ParenPreference -> Bool Source #

(>=) :: ParenPreference -> ParenPreference -> Bool Source #

max :: ParenPreference -> ParenPreference -> ParenPreference Source #

min :: ParenPreference -> ParenPreference -> ParenPreference Source #

Show ParenPreference Source # |
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> ParenPreference -> ShowS Source # show :: ParenPreference -> String Source # showList :: [ParenPreference] -> ShowS Source #
EmbPrj ParenPreference Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ParenPreference -> S Int32 Source # icod_ :: ParenPreference -> S Int32 Source # value :: Int32 -> R ParenPreference Source #

preferParen :: ParenPreference -> Bool Source #

preferParenless :: ParenPreference -> Bool Source #

# Precendence

data Precedence Source #

Precedence is associated with a context.

Constructors

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

Instances

Eq Precedence Source # |
Instance details Defined in Agda.Syntax.Fixity Methods (==) :: Precedence -> Precedence -> Bool Source # (/=) :: Precedence -> Precedence -> Bool Source #
Data Precedence Source # |

Instance details

Defined in Agda.Syntax.Fixity

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Precedence -> c Precedence Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Precedence Source #

toConstr :: Precedence -> Constr Source #

dataTypeOf :: Precedence -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Precedence) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Precedence) Source #

gmapT :: (forall b. Data b => b -> b) -> Precedence -> Precedence Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Precedence -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Precedence -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Precedence -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Precedence -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Precedence -> m Precedence Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Precedence -> m Precedence Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Precedence -> m Precedence Source #

Show Precedence Source # |
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> Precedence -> ShowS Source # show :: Precedence -> String Source # showList :: [Precedence] -> ShowS Source #
Pretty Precedence Source # |
Instance details Defined in Agda.Syntax.Fixity Methods pretty :: Precedence -> Doc Source # prettyPrec :: Int -> Precedence -> Doc Source # prettyList :: [Precedence] -> Doc Source #
EmbPrj Precedence Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Precedence -> S Int32 Source # icod_ :: Precedence -> S Int32 Source # value :: Int32 -> R Precedence 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 #

argumentCtx_ :: Precedence Source #

Argument context preferring parens.

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 :: 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).

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 #

# Some lenses

_notaFixity :: Lens' Fixity NewNotation Source #

_fixityAssoc :: Lens' Associativity Fixity Source #

_fixityLevel :: Lens' PrecedenceLevel Fixity Source #

# Printing

# NFData instances