Agda-2.6.4.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Fixity

Contents

Description

Definitions for fixity, precedence levels, and declared syntax.

Synopsis

Documentation

data ThingWithFixity x Source #

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity' 

Instances

Instances details
Foldable ThingWithFixity Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

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

foldMap :: Monoid m => (a -> m) -> ThingWithFixity a -> 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 # 
Instance details

Defined in Agda.Syntax.Fixity

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) #

Functor ThingWithFixity Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b #

(<$) :: a -> ThingWithFixity b -> ThingWithFixity a #

LensFixity (ThingWithFixity a) Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

lensFixity :: Lens' (ThingWithFixity a) Fixity Source #

LensFixity' (ThingWithFixity a) Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

lensFixity' :: Lens' (ThingWithFixity a) Fixity' 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 #

Show x => Show (ThingWithFixity x) Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> ThingWithFixity x -> ShowS #

show :: ThingWithFixity x -> String #

showList :: [ThingWithFixity x] -> ShowS #

data ParenPreference Source #

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

Constructors

PreferParen 
PreferParenless 

Instances

Instances details
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 #

Generic ParenPreference Source # 
Instance details

Defined in Agda.Syntax.Fixity

Associated Types

type Rep ParenPreference 
Instance details

Defined in Agda.Syntax.Fixity

type Rep ParenPreference = D1 ('MetaData "ParenPreference" "Agda.Syntax.Fixity" "Agda-2.6.4.1-inplace" 'False) (C1 ('MetaCons "PreferParen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PreferParenless" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: ParenPreference -> Rep ParenPreference x #

to :: Rep ParenPreference x -> ParenPreference #

Show ParenPreference Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> ParenPreference -> ShowS #

show :: ParenPreference -> String #

showList :: [ParenPreference] -> ShowS #

NFData ParenPreference Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

rnf :: ParenPreference -> () #

Eq ParenPreference Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

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

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

Ord ParenPreference Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

compare :: ParenPreference -> ParenPreference -> Ordering #

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

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

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

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

max :: ParenPreference -> ParenPreference -> ParenPreference #

min :: ParenPreference -> ParenPreference -> ParenPreference #

type Rep ParenPreference Source # 
Instance details

Defined in Agda.Syntax.Fixity

type Rep ParenPreference = D1 ('MetaData "ParenPreference" "Agda.Syntax.Fixity" "Agda-2.6.4.1-inplace" 'False) (C1 ('MetaCons "PreferParen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PreferParenless" 'PrefixI 'False) (U1 :: Type -> Type))

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

Instances details
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 #

Generic Precedence Source # 
Instance details

Defined in Agda.Syntax.Fixity

Associated Types

type Rep Precedence 
Instance details

Defined in Agda.Syntax.Fixity

type Rep Precedence = D1 ('MetaData "Precedence" "Agda.Syntax.Fixity" "Agda-2.6.4.1-inplace" 'False) (((C1 ('MetaCons "TopCtx" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FunctionSpaceDomainCtx" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LeftOperandCtx" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity)) :+: (C1 ('MetaCons "RightOperandCtx" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ParenPreference)) :+: C1 ('MetaCons "FunctionCtx" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "ArgumentCtx" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ParenPreference)) :+: C1 ('MetaCons "InsideOperandCtx" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WithFunCtx" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WithArgCtx" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DotPatternCtx" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: Precedence -> Rep Precedence x #

to :: Rep Precedence x -> Precedence #

Show Precedence Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> Precedence -> ShowS #

show :: Precedence -> String #

showList :: [Precedence] -> ShowS #

NFData Precedence Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

rnf :: Precedence -> () #

Eq Precedence Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

(==) :: Precedence -> Precedence -> Bool #

(/=) :: Precedence -> Precedence -> Bool #

type Rep Precedence Source # 
Instance details

Defined in Agda.Syntax.Fixity

type Rep Precedence = D1 ('MetaData "Precedence" "Agda.Syntax.Fixity" "Agda-2.6.4.1-inplace" 'False) (((C1 ('MetaCons "TopCtx" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FunctionSpaceDomainCtx" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LeftOperandCtx" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity)) :+: (C1 ('MetaCons "RightOperandCtx" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ParenPreference)) :+: C1 ('MetaCons "FunctionCtx" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "ArgumentCtx" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ParenPreference)) :+: C1 ('MetaCons "InsideOperandCtx" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WithFunCtx" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WithArgCtx" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DotPatternCtx" 'PrefixI 'False) (U1 :: Type -> Type)))))

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 #