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

Safe Haskell | None
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 (Ranged Expr)
  - | CohesionAttribute Cohesion
  - | PolarityAttribute PolarityModality
  - | LockAttribute Lock
- data Attr = Attr {
  - attrRange :: Range
  - attrName :: String
  - theAttr :: Attribute
  }
- type LensAttribute a = (LensRelevance a, LensQuantity a, LensCohesion a, LensModalPolarity a, LensLock a)
- relevanceAttributeTable :: [(String, Relevance)]
- quantityAttributeTable :: [(String, Quantity)]
- cohesionAttributeTable :: [(String, Cohesion)]
- type Attributes = [Attr]
- polarityAttributeTable :: [(String, PolarityModality)]
- lockAttributeTable :: [(String, Lock)]
- attributesMap :: Map String Attribute
- stringToAttribute :: String -> Maybe Attribute
- exprToAttribute :: Range -> 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
- setPristinePolarity :: LensModalPolarity a => PolarityModality -> 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 -> TacticAttribute
- 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 (Ranged Expr) |
CohesionAttribute Cohesion |
PolarityAttribute PolarityModality |
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 #

data Attr Source #

Parsed attribute.

Constructors

Attr |

Fields

- attrRange :: Range

  Range includes the @.

- attrName :: String

  Concrete, user written attribute for error reporting, not including the "@".

- theAttr :: Attribute

  Parsed attribute.

#### Instances

Instances details

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

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

(Conjunctive constraint.)

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

Modifiers for `Relevance`.

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

Modifiers for `Quantity`.

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

type Attributes = [Attr] Source #

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.

polarityAttributeTable :: [(String, PolarityModality)] Source #

Modifiers for `Polarity`.

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

setPristinePolarity :: LensModalPolarity a => PolarityModality -> a -> Maybe a Source #

Setting `ModalPolarity` 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 -> TacticAttribute Source #

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

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

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