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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Syntax.Concrete.Attribute

Contents

- Applying attributes only if they have not been set already.
- Filtering attributes

Description

Synopsis

- data Attribute
  - = RelevanceAttribute Relevance
  - | QuantityAttribute Quantity
  - | TacticAttribute Expr
  - | CohesionAttribute Cohesion
  - | LockAttribute Lock
- type LensAttribute a = (LensRelevance a, LensQuantity a, LensCohesion a, LensLock a)
- relevanceAttributeTable :: [(String, Relevance)]
- quantityAttributeTable :: [(String, Quantity)]
- cohesionAttributeTable :: [(String, Cohesion)]
- lockAttributeTable :: [(String, Lock)]
- attributesMap :: Map String Attribute
- stringToAttribute :: String -> Maybe Attribute
- exprToAttribute :: Expr -> Maybe Attribute
- setAttribute :: LensAttribute a => Attribute -> a -> a
- setAttributes :: LensAttribute a => [Attribute] -> a -> a
- setPristineRelevance :: LensRelevance a => Relevance -> a -> Maybe a
- setPristineQuantity :: LensQuantity a => Quantity -> a -> Maybe a
- setPristineCohesion :: LensCohesion a => Cohesion -> a -> Maybe a
- setPristineLock :: LensLock a => Lock -> a -> Maybe a
- setPristineAttribute :: LensAttribute a => Attribute -> a -> Maybe a
- setPristineAttributes :: LensAttribute a => [Attribute] -> a -> Maybe a
- isRelevanceAttribute :: Attribute -> Maybe Relevance
- isQuantityAttribute :: Attribute -> Maybe Quantity
- isTacticAttribute :: Attribute -> Maybe Expr
- relevanceAttributes :: [Attribute] -> [Attribute]
- quantityAttributes :: [Attribute] -> [Attribute]
- tacticAttributes :: [Attribute] -> [Attribute]

# Documentation

data Attribute Source #

An attribute is a modifier for `ArgInfo`.

Constructors

RelevanceAttribute Relevance |
QuantityAttribute Quantity |
TacticAttribute Expr |
CohesionAttribute Cohesion |
LockAttribute Lock |

#### Instances

Instances details

HasRange Attribute Source # |
Instance details Defined in Agda.Syntax.Concrete.Attribute Methods getRange :: Attribute -> Range Source #
KillRange Attribute Source # |
Instance details Defined in Agda.Syntax.Concrete.Attribute Methods killRange :: KillRangeT Attribute Source #
SetRange Attribute Source # |
Instance details Defined in Agda.Syntax.Concrete.Attribute Methods setRange :: Range -> Attribute -> Attribute Source #
Show Attribute Source # |
Instance details Defined in Agda.Syntax.Concrete.Attribute Methods showsPrec :: Int -> Attribute -> ShowS Source # show :: Attribute -> String Source # showList :: [Attribute] -> ShowS Source #

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

(Conjunctive constraint.)

relevanceAttributeTable :: [(String, Relevance)] Source #

Modifiers for `Relevance`.

quantityAttributeTable :: [(String, Quantity)] Source #

Modifiers for `Quantity`.

cohesionAttributeTable :: [(String, Cohesion)] Source #

lockAttributeTable :: [(String, Lock)] Source #

Modifiers for `Quantity`.

attributesMap :: Map String Attribute Source #

Concrete syntax for all attributes.

stringToAttribute :: String -> Maybe Attribute Source #

Parsing a string into an attribute.

exprToAttribute :: Expr -> Maybe Attribute Source #

Parsing an expression into an attribute.

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

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

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

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

Setting `Relevance` if unset.

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

Setting `Quantity` if unset.

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

Setting `Cohesion` if unset.

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

Setting `Lock` if unset.

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

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

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

Setting a list of unset attributes.

# Filtering attributes

isRelevanceAttribute :: Attribute -> Maybe Relevance Source #

isQuantityAttribute :: Attribute -> Maybe Quantity Source #

isTacticAttribute :: Attribute -> Maybe Expr Source #

relevanceAttributes :: [Attribute] -> [Attribute] Source #

quantityAttributes :: [Attribute] -> [Attribute] Source #

tacticAttributes :: [Attribute] -> [Attribute] Source #