Agda.Syntax.Concrete.Attribute

Documentation

data Attribute

An attribute is a modifier for ArgInfo.

Constructors

RelevanceAttribute Relevance

QuantityAttribute Quantity

TacticAttribute (Ranged Expr)

CohesionAttribute Cohesion

LockAttribute Lock

Instances

HasRange Attribute

Defined in Agda.Syntax.Concrete.Attribute

Methods

getRange :: Attribute -> Range

KillRange Attribute

Defined in Agda.Syntax.Concrete.Attribute

Methods

killRange :: KillRangeT Attribute

SetRange Attribute

Defined in Agda.Syntax.Concrete.Attribute

Methods

setRange :: Range -> Attribute -> Attribute

Show Attribute

Defined in Agda.Syntax.Concrete.Attribute

Methods

showsPrec :: Int -> Attribute -> ShowS

show :: Attribute -> String

showList :: [Attribute] -> ShowS

type LensAttribute a = (LensRelevance a, LensQuantity a, LensCohesion a, LensLock a)

(Conjunctive constraint.)

relevanceAttributeTable :: [(String, Relevance)]

Modifiers for Relevance.

quantityAttributeTable :: [(String, Quantity)]

Modifiers for Quantity.

cohesionAttributeTable :: [(String, Cohesion)]

type Attributes = [(Attribute, Range, String)]

Information about attributes (attribute, range, printed representation).

This information is returned by the parser. Code that calls the parser should, if appropriate, complain if support for the given attributes has not been enabled. This can be taken care of by checkAttributes, which should not be called until after pragma options have been set.

lockAttributeTable :: [(String, Lock)]

Modifiers for Quantity.

attributesMap :: Map String Attribute

Concrete syntax for all attributes.

stringToAttribute :: String -> Maybe Attribute

Parsing a string into an attribute.

exprToAttribute :: Expr -> Maybe Attribute

Parsing an expression into an attribute.

setAttribute :: LensAttribute a => Attribute -> a -> a

Setting an attribute (in e.g. an Arg). Overwrites previous value.

setAttributes :: LensAttribute a => [Attribute] -> a -> a

Setting some attributes in left-to-right order. Blindly overwrites previous settings.

Applying attributes only if they have not been set already.

setPristineRelevance :: LensRelevance a => Relevance -> a -> Maybe a

Setting Relevance if unset.

setPristineQuantity :: LensQuantity a => Quantity -> a -> Maybe a

Setting Quantity if unset.

setPristineCohesion :: LensCohesion a => Cohesion -> a -> Maybe a

Setting Cohesion if unset.

setPristineLock :: LensLock a => Lock -> a -> Maybe a

Setting Lock if unset.

setPristineAttribute :: LensAttribute a => Attribute -> a -> Maybe a

Setting an unset attribute (to e.g. an Arg).

setPristineAttributes :: LensAttribute a => [Attribute] -> a -> Maybe a

Setting a list of unset attributes.

Filtering attributes

isRelevanceAttribute :: Attribute -> Maybe Relevance

isQuantityAttribute :: Attribute -> Maybe Quantity

isTacticAttribute :: Attribute -> TacticAttribute

relevanceAttributes :: [Attribute] -> [Attribute]

quantityAttributes :: [Attribute] -> [Attribute]

tacticAttributes :: [Attribute] -> [Attribute]