ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Fixity

Definitions for fixity, precedence levels, and declared syntax.

Contents

Precendence

Synopsis

data ThingWithFixity
data ParenPreference
value preferParen
value preferParenless
data Precedence
type PrecedenceStack
value pushPrecedence
value headPrecedence
value argumentCtx_
value opBrackets
value opBrackets'
value lamBrackets
value appBrackets
value appBrackets'
value withAppBrackets
value piBrackets
value roundFixBrackets

PackageAgda-2.8.0.2
Exports17
LanguageHaskell2010
LicenceMIT
SourceFixity.hs

datadata ThingWithFixity x

Source#

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity'

Instances8Functor, Foldable, Traversable, Show, Pretty, KillRange, …

Functor ThingWithFixityDefined in Agda-2.8.0.2 · Agda.Syntax.Fixity
Foldable ThingWithFixityDefined in Agda-2.8.0.2 · Agda.Syntax.Fixity
Traversable ThingWithFixityDefined in Agda-2.8.0.2 · Agda.Syntax.Fixity
Show x => Show (ThingWithFixity x)Defined in Agda-2.8.0.2 · Agda.Syntax.Fixity
Pretty (ThingWithFixity Name)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Pretty · orphan
KillRange x => KillRange (ThingWithFixity x)Defined in Agda-2.8.0.2 · Agda.Syntax.Fixity
LensFixity' (ThingWithFixity a)Defined in Agda-2.8.0.2 · Agda.Syntax.Fixity
LensFixity (ThingWithFixity a)Defined in Agda-2.8.0.2 · Agda.Syntax.Fixity

datadata ParenPreference

Source#

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

PreferParen PreferParenless

Instances7Eq, Ord, Show, Generic, NFData, EmbPrj, …

Eq ParenPreferenceDefined in Agda-2.8.0.2 · Agda.Syntax.Fixity
Ord ParenPreferenceDefined in Agda-2.8.0.2 · Agda.Syntax.Fixity
Show ParenPreferenceDefined in Agda-2.8.0.2 · Agda.Syntax.Fixity
Generic ParenPreferenceDefined in Agda-2.8.0.2 · Agda.Syntax.Fixity
NFData ParenPreferenceDefined in Agda-2.8.0.2 · Agda.Syntax.Fixity
EmbPrj ParenPreferenceDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Abstract · orphan
type Rep ParenPreference = D1 ('MetaData "ParenPreference" "Agda.Syntax.Fixity" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "PreferParen" 'PrefixI 'False) U1 :+: C1 ('MetaCons "PreferParenless" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Fixity

valuepreferParen :: ParenPreference -> Bool

valuepreferParenless :: ParenPreference -> Bool

Precendence

datadata Precedence

Source#

Precedence is associated with a context.

Instances7Eq, Show, Generic, NFData, Pretty, EmbPrj, …

Eq PrecedenceDefined in Agda-2.8.0.2 · Agda.Syntax.Fixity
Show PrecedenceDefined in Agda-2.8.0.2 · Agda.Syntax.Fixity
Generic PrecedenceDefined in Agda-2.8.0.2 · Agda.Syntax.Fixity
NFData PrecedenceDefined in Agda-2.8.0.2 · Agda.Syntax.Fixity
Pretty PrecedenceDefined in Agda-2.8.0.2 · Agda.Syntax.Fixity
EmbPrj PrecedenceDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Abstract · orphan
type Rep Precedence = D1 ('MetaData "Precedence" "Agda.Syntax.Fixity" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (((C1 ('MetaCons "TopCtx" 'PrefixI 'False) U1 :+: C1 ('MetaCons "FunctionSpaceDomainCtx" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "LeftOperandCtx" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity)) :+: (C1 ('MetaCons "RightOperandCtx" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ParenPreference)) :+: C1 ('MetaCons "FunctionCtx" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "ArgumentCtx" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ParenPreference)) :+: C1 ('MetaCons "InsideOperandCtx" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "WithFunCtx" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "WithArgCtx" 'PrefixI 'False) U1 :+: C1 ('MetaCons "DotPatternCtx" 'PrefixI 'False) U1))))Defined in Agda-2.8.0.2 · Agda.Syntax.Fixity

typetype 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`.

valuepushPrecedence :: Precedence -> PrecedenceStack -> PrecedenceStack

valueheadPrecedence :: PrecedenceStack -> Precedence

valueargumentCtx_ :: Precedence

Source#

Argument context preferring parens.

valueopBrackets :: Fixity -> PrecedenceStack -> Bool

Source#

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

valueopBrackets' :: Bool -> Fixity -> PrecedenceStack -> Bool

Source#

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

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

valueappBrackets :: PrecedenceStack -> Bool

Source#

Does a function application need brackets?

valueappBrackets' :: Bool -> PrecedenceStack -> Bool

Source#

Does a function application need brackets?

valuewithAppBrackets :: PrecedenceStack -> Bool

Source#

Does a with application need brackets?

valuepiBrackets :: PrecedenceStack -> Bool

Source#

Does a function space need brackets?

valueroundFixBrackets :: PrecedenceStack -> Bool