    -- | Attributes: concrete syntax for ArgInfo, esp. modalities.

    module Agda.Syntax.Concrete.Attribute where

    import Prelude hiding (null)

    import Control.Arrow (second)
    import Control.Monad (foldM)

    import Data.List (foldl')
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Maybe

    import Agda.Syntax.Common
    import Agda.Syntax.Concrete (Expr(..), TacticAttribute)
    import qualified Agda.Syntax.Concrete as C
    import Agda.Syntax.Concrete.Pretty () --instance only
    import Agda.Syntax.Common.Pretty (prettyShow)
    import Agda.Syntax.Position

    import Agda.Utils.List1 (List1, pattern (:|))
    import Agda.Utils.Null

    import Agda.Utils.Impossible

    -- | An attribute is a modifier for `ArgInfo`.

    data Attribute
      = RelevanceAttribute Relevance
      | QuantityAttribute  Quantity
      | TacticAttribute (Ranged Expr)
      | CohesionAttribute Cohesion
      | PolarityAttribute PolarityModality
      | LockAttribute      Lock
      deriving (Int -> Attribute -> ShowS
    [Attribute] -> ShowS
    Attribute -> String
    (Int -> Attribute -> ShowS)
    -> (Attribute -> String)
    -> ([Attribute] -> ShowS)
    -> Show Attribute
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Attribute -> ShowS
    showsPrec :: Int -> Attribute -> ShowS
    $cshow :: Attribute -> String
    show :: Attribute -> String
    $cshowList :: [Attribute] -> ShowS
    showList :: [Attribute] -> ShowS
    Show)

    instance HasRange Attribute where
      getRange :: Attribute -> Range
    getRange = \case
        RelevanceAttribute Relevance
    r -> Relevance -> Range
    forall a. HasRange a => a -> Range
    getRange Relevance
    r
        QuantityAttribute Quantity
    q  -> Quantity -> Range
    forall a. HasRange a => a -> Range
    getRange Quantity
    q
        CohesionAttribute Cohesion
    c  -> Cohesion -> Range
    forall a. HasRange a => a -> Range
    getRange Cohesion
    c
        PolarityAttribute PolarityModality
    p  -> PolarityModality -> Range
    forall a. HasRange a => a -> Range
    getRange PolarityModality
    p
        TacticAttribute Ranged Expr
    e    -> Ranged Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Ranged Expr
    e
        LockAttribute Lock
    l      -> Range
    forall a. Range' a
    NoRange

    instance SetRange Attribute where
      setRange :: Range -> Attribute -> Attribute
    setRange Range
    r = \case
        RelevanceAttribute Relevance
    a -> Relevance -> Attribute
    RelevanceAttribute (Relevance -> Attribute) -> Relevance -> Attribute
    forall a b. (a -> b) -> a -> b
    $ Range -> Relevance -> Relevance
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r Relevance
    a
        QuantityAttribute Quantity
    q  -> Quantity -> Attribute
    QuantityAttribute  (Quantity -> Attribute) -> Quantity -> Attribute
    forall a b. (a -> b) -> a -> b
    $ Range -> Quantity -> Quantity
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r Quantity
    q
        CohesionAttribute Cohesion
    c  -> Cohesion -> Attribute
    CohesionAttribute  (Cohesion -> Attribute) -> Cohesion -> Attribute
    forall a b. (a -> b) -> a -> b
    $ Range -> Cohesion -> Cohesion
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r Cohesion
    c
        PolarityAttribute PolarityModality
    p  -> PolarityModality -> Attribute
    PolarityAttribute  (PolarityModality -> Attribute) -> PolarityModality -> Attribute
    forall a b. (a -> b) -> a -> b
    $ Range -> PolarityModality -> PolarityModality
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r PolarityModality
    p
        TacticAttribute Ranged Expr
    e    -> Ranged Expr -> Attribute
    TacticAttribute Ranged Expr
    e  -- -- $ setRange r e -- SetRange Expr not yet implemented
        LockAttribute Lock
    l      -> Lock -> Attribute
    LockAttribute Lock
    l

    instance KillRange Attribute where
      killRange :: Attribute -> Attribute
    killRange = \case
        RelevanceAttribute Relevance
    a -> Relevance -> Attribute
    RelevanceAttribute (Relevance -> Attribute) -> Relevance -> Attribute
    forall a b. (a -> b) -> a -> b
    $ Relevance -> Relevance
    forall a. KillRange a => KillRangeT a
    killRange Relevance
    a
        QuantityAttribute Quantity
    q  -> Quantity -> Attribute
    QuantityAttribute  (Quantity -> Attribute) -> Quantity -> Attribute
    forall a b. (a -> b) -> a -> b
    $ Quantity -> Quantity
    forall a. KillRange a => KillRangeT a
    killRange Quantity
    q
        CohesionAttribute Cohesion
    c  -> Cohesion -> Attribute
    CohesionAttribute  (Cohesion -> Attribute) -> Cohesion -> Attribute
    forall a b. (a -> b) -> a -> b
    $ Cohesion -> Cohesion
    forall a. KillRange a => KillRangeT a
    killRange Cohesion
    c
        PolarityAttribute PolarityModality
    p  -> PolarityModality -> Attribute
    PolarityAttribute  (PolarityModality -> Attribute) -> PolarityModality -> Attribute
    forall a b. (a -> b) -> a -> b
    $ PolarityModality -> PolarityModality
    forall a. KillRange a => KillRangeT a
    killRange PolarityModality
    p
        TacticAttribute Ranged Expr
    e    -> Ranged Expr -> Attribute
    TacticAttribute    (Ranged Expr -> Attribute) -> Ranged Expr -> Attribute
    forall a b. (a -> b) -> a -> b
    $ KillRangeT (Ranged Expr)
    forall a. KillRange a => KillRangeT a
    killRange Ranged Expr
    e
        LockAttribute Lock
    l      -> Lock -> Attribute
    LockAttribute Lock
    l

    -- | Parsed attribute.

    data Attr = Attr
      { Attr -> Range
    attrRange :: Range       -- ^ Range includes the @.
      , Attr -> String
    attrName  :: String      -- ^ Concrete, user written attribute for error reporting, not including the "@".
      , Attr -> Attribute
    theAttr   :: Attribute   -- ^ Parsed attribute.
      } deriving (Int -> Attr -> ShowS
    [Attr] -> ShowS
    Attr -> String
    (Int -> Attr -> ShowS)
    -> (Attr -> String) -> ([Attr] -> ShowS) -> Show Attr
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Attr -> ShowS
    showsPrec :: Int -> Attr -> ShowS
    $cshow :: Attr -> String
    show :: Attr -> String
    $cshowList :: [Attr] -> ShowS
    showList :: [Attr] -> ShowS
    Show)

    instance HasRange Attr where
      getRange :: Attr -> Range
    getRange = Attr -> Range
    attrRange

    instance SetRange Attr where
      setRange :: Range -> Attr -> Attr
    setRange Range
    r (Attr Range
    _ String
    x Attribute
    a) = Range -> String -> Attribute -> Attr
    Attr Range
    r String
    x Attribute
    a

    instance KillRange Attr where
      killRange :: Attr -> Attr
    killRange (Attr Range
    _ String
    x Attribute
    a) = Range -> String -> Attribute -> Attr
    Attr Range
    forall a. Range' a
    noRange String
    x (Attribute -> Attribute
    forall a. KillRange a => KillRangeT a
    killRange Attribute
    a)

    -- | (Conjunctive constraint.)

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

    -- | Modifiers for 'Relevance'.

    relevanceAttributeTable :: [(String, Relevance)]
    relevanceAttributeTable :: [(String, Relevance)]
    relevanceAttributeTable =
      [ (String
    "irr"             , OriginIrrelevant -> Relevance
    Irrelevant      (OriginIrrelevant -> Relevance) -> OriginIrrelevant -> Relevance
    forall a b. (a -> b) -> a -> b
    $ Range -> OriginIrrelevant
    OIrrIrr               Range
    forall a. Range' a
    noRange)
      , (String
    "irrelevant"      , OriginIrrelevant -> Relevance
    Irrelevant      (OriginIrrelevant -> Relevance) -> OriginIrrelevant -> Relevance
    forall a b. (a -> b) -> a -> b
    $ Range -> OriginIrrelevant
    OIrrIrrelevant        Range
    forall a. Range' a
    noRange)
      , (String
    "shirr"           , OriginShapeIrrelevant -> Relevance
    ShapeIrrelevant (OriginShapeIrrelevant -> Relevance)
    -> OriginShapeIrrelevant -> Relevance
    forall a b. (a -> b) -> a -> b
    $ Range -> OriginShapeIrrelevant
    OShIrrShIrr           Range
    forall a. Range' a
    noRange)
      , (String
    "shape-irrelevant", OriginShapeIrrelevant -> Relevance
    ShapeIrrelevant (OriginShapeIrrelevant -> Relevance)
    -> OriginShapeIrrelevant -> Relevance
    forall a b. (a -> b) -> a -> b
    $ Range -> OriginShapeIrrelevant
    OShIrrShapeIrrelevant Range
    forall a. Range' a
    noRange)
      , (String
    "relevant"        , OriginRelevant -> Relevance
    Relevant        (OriginRelevant -> Relevance) -> OriginRelevant -> Relevance
    forall a b. (a -> b) -> a -> b
    $ Range -> OriginRelevant
    ORelRelevant          Range
    forall a. Range' a
    noRange)
      ]

    -- | Modifiers for 'Quantity'.

    quantityAttributeTable :: [(String, Quantity)]
    quantityAttributeTable :: [(String, Quantity)]
    quantityAttributeTable =
      [ (String
    "0"      , Q0Origin -> Quantity
    Quantity0 (Q0Origin -> Quantity) -> Q0Origin -> Quantity
    forall a b. (a -> b) -> a -> b
    $ Range -> Q0Origin
    Q0       Range
    forall a. Range' a
    noRange)
      , (String
    "erased" , Q0Origin -> Quantity
    Quantity0 (Q0Origin -> Quantity) -> Q0Origin -> Quantity
    forall a b. (a -> b) -> a -> b
    $ Range -> Q0Origin
    Q0Erased Range
    forall a. Range' a
    noRange)
      -- TODO: linearity
      -- , ("1"      , Quantity1 $ Q1       noRange)
      -- , ("linear" , Quantity1 $ Q1Linear noRange)
      , (String
    "ω"      , QωOrigin -> Quantity
    Quantityω (QωOrigin -> Quantity) -> QωOrigin -> Quantity
    forall a b. (a -> b) -> a -> b
    $ Range -> QωOrigin
    Qω       Range
    forall a. Range' a
    noRange)
      , (String
    "plenty" , QωOrigin -> Quantity
    Quantityω (QωOrigin -> Quantity) -> QωOrigin -> Quantity
    forall a b. (a -> b) -> a -> b
    $ Range -> QωOrigin
    QωPlenty Range
    forall a. Range' a
    noRange)
      ]
    -- quantityAttributeTable = concat
    --   [ map (, Quantity0) [ "0", "erased" ] -- , "static", "compile-time" ]
    --   , map (, Quantityω) [ "ω", "plenty" ] -- , "dynamic", "runtime", "unrestricted", "abundant" ]
    --   -- , map (, Quantity1)  [ "1", "linear" ]
    --   -- , map (, Quantity01) [ "01", "affine" ]
    --   ]

    cohesionAttributeTable :: [(String, Cohesion)]
    cohesionAttributeTable :: [(String, Cohesion)]
    cohesionAttributeTable =
      [ (String
    "♭"    , Cohesion
    Flat)
      , (String
    "flat" , Cohesion
    Flat)
      ]

    -- | 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
    -- 'Agda.Syntax.Translation.ConcreteToAbstract.checkAttributes', which
    -- should not be called until after pragma options have been set.

    type Attributes = [Attr]

    -- | Modifiers for 'Polarity'.

    polarityAttributeTable :: [(String, PolarityModality)]
    polarityAttributeTable :: [(String, PolarityModality)]
    polarityAttributeTable =
      [ (String
    "unused" , ModalPolarity -> PolarityModality
    withStandardLock ModalPolarity
    UnusedPolarity)
      , (String
    "++" , ModalPolarity -> PolarityModality
    withStandardLock ModalPolarity
    StrictlyPositive)
      , (String
    "+" , ModalPolarity -> PolarityModality
    withStandardLock ModalPolarity
    Positive)
      , (String
    "-" , ModalPolarity -> PolarityModality
    withStandardLock ModalPolarity
    Negative)
      , (String
    "mixed" , ModalPolarity -> PolarityModality
    withStandardLock ModalPolarity
    MixedPolarity)]

    -- | Modifiers for 'Quantity'.

    lockAttributeTable :: [(String, Lock)]
    lockAttributeTable :: [(String, Lock)]
    lockAttributeTable = [[(String, Lock)]] -> [(String, Lock)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
      [ (String -> (String, Lock)) -> [String] -> [(String, Lock)]
    forall a b. (a -> b) -> [a] -> [b]
    map (, Lock
    IsNotLock) [ String
    "notlock" ] -- default, shouldn't be used much
      , (String -> (String, Lock)) -> [String] -> [(String, Lock)]
    forall a b. (a -> b) -> [a] -> [b]
    map (, LockOrigin -> Lock
    IsLock LockOrigin
    LockOTick) [ String
    "tick" ] -- @tick
      , (String -> (String, Lock)) -> [String] -> [(String, Lock)]
    forall a b. (a -> b) -> [a] -> [b]
    map (, LockOrigin -> Lock
    IsLock LockOrigin
    LockOLock) [ String
    "lock" ] -- @lock
      ]

    -- | Concrete syntax for all attributes.

    attributesMap :: Map String Attribute
    attributesMap :: Map String Attribute
    attributesMap = (Attribute -> Attribute -> Attribute)
    -> [(String, Attribute)] -> Map String Attribute
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith Attribute -> Attribute -> Attribute
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([(String, Attribute)] -> Map String Attribute)
    -> [(String, Attribute)] -> Map String Attribute
    forall a b. (a -> b) -> a -> b
    $ [[(String, Attribute)]] -> [(String, Attribute)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
      [ ((String, Relevance) -> (String, Attribute))
    -> [(String, Relevance)] -> [(String, Attribute)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Relevance -> Attribute)
    -> (String, Relevance) -> (String, Attribute)
    forall b c d. (b -> c) -> (d, b) -> (d, c)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second Relevance -> Attribute
    RelevanceAttribute) [(String, Relevance)]
    relevanceAttributeTable
      , ((String, Quantity) -> (String, Attribute))
    -> [(String, Quantity)] -> [(String, Attribute)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Quantity -> Attribute)
    -> (String, Quantity) -> (String, Attribute)
    forall b c d. (b -> c) -> (d, b) -> (d, c)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second Quantity -> Attribute
    QuantityAttribute)  [(String, Quantity)]
    quantityAttributeTable
      , ((String, Cohesion) -> (String, Attribute))
    -> [(String, Cohesion)] -> [(String, Attribute)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Cohesion -> Attribute)
    -> (String, Cohesion) -> (String, Attribute)
    forall b c d. (b -> c) -> (d, b) -> (d, c)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second Cohesion -> Attribute
    CohesionAttribute)  [(String, Cohesion)]
    cohesionAttributeTable
      , ((String, PolarityModality) -> (String, Attribute))
    -> [(String, PolarityModality)] -> [(String, Attribute)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((PolarityModality -> Attribute)
    -> (String, PolarityModality) -> (String, Attribute)
    forall b c d. (b -> c) -> (d, b) -> (d, c)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second PolarityModality -> Attribute
    PolarityAttribute)  [(String, PolarityModality)]
    polarityAttributeTable
      , ((String, Lock) -> (String, Attribute))
    -> [(String, Lock)] -> [(String, Attribute)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Lock -> Attribute) -> (String, Lock) -> (String, Attribute)
    forall b c d. (b -> c) -> (d, b) -> (d, c)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second Lock -> Attribute
    LockAttribute)      [(String, Lock)]
    lockAttributeTable
      ]

    -- | Parsing a string into an attribute.

    stringToAttribute :: String -> Maybe Attribute
    stringToAttribute :: String -> Maybe Attribute
    stringToAttribute = (String -> Map String Attribute -> Maybe Attribute
    forall k a. Ord k => k -> Map k a -> Maybe a
    `Map.lookup` Map String Attribute
    attributesMap)

    -- | Parsing an expression into an attribute.

    exprToAttribute :: Range -> Expr -> Maybe Attribute
    exprToAttribute :: Range -> Expr -> Maybe Attribute
    exprToAttribute Range
    r = \case
      e :: Expr
    e@(Paren Range
    _ (Tactic Range
    _ Expr
    t)) -> Attribute -> Maybe Attribute
    forall a. a -> Maybe a
    Just (Attribute -> Maybe Attribute) -> Attribute -> Maybe Attribute
    forall a b. (a -> b) -> a -> b
    $ Ranged Expr -> Attribute
    TacticAttribute (Ranged Expr -> Attribute) -> Ranged Expr -> Attribute
    forall a b. (a -> b) -> a -> b
    $ Range -> Expr -> Ranged Expr
    forall a. Range -> a -> Ranged a
    Ranged Range
    r Expr
    t
      Expr
    e -> Range -> Maybe Attribute -> Maybe Attribute
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r (Maybe Attribute -> Maybe Attribute)
    -> Maybe Attribute -> Maybe Attribute
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe Attribute
    stringToAttribute (String -> Maybe Attribute) -> String -> Maybe Attribute
    forall a b. (a -> b) -> a -> b
    $ Expr -> String
    forall a. Pretty a => a -> String
    prettyShow Expr
    e

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

    setAttribute :: (LensAttribute a) => Attribute -> a -> a
    setAttribute :: forall a. LensAttribute a => Attribute -> a -> a
    setAttribute = \case
      RelevanceAttribute Relevance
    r -> Relevance -> a -> a
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance Relevance
    r
      QuantityAttribute  Quantity
    q -> Quantity -> a -> a
    forall a. LensQuantity a => Quantity -> a -> a
    setQuantity  Quantity
    q
      CohesionAttribute  Cohesion
    c -> Cohesion -> a -> a
    forall a. LensCohesion a => Cohesion -> a -> a
    setCohesion  Cohesion
    c
      PolarityAttribute  PolarityModality
    p -> PolarityModality -> a -> a
    forall a. LensModalPolarity a => PolarityModality -> a -> a
    setModalPolarity PolarityModality
    p
      LockAttribute      Lock
    l -> Lock -> a -> a
    forall a. LensLock a => Lock -> a -> a
    setLock      Lock
    l
      TacticAttribute Ranged Expr
    t    -> a -> a
    forall a. a -> a
    id

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

    setAttributes :: (LensAttribute a) => [Attribute] -> a -> a
    setAttributes :: forall a. LensAttribute a => [Attribute] -> a -> a
    setAttributes [Attribute]
    attrs a
    arg = (a -> Attribute -> a) -> a -> [Attribute] -> a
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl' ((Attribute -> a -> a) -> a -> Attribute -> a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Attribute -> a -> a
    forall a. LensAttribute a => Attribute -> a -> a
    setAttribute) a
    arg [Attribute]
    attrs

    ---------------------------------------------------------------------------
    -- * Applying attributes only if they have not been set already.
    --   No overwriting.
    ---------------------------------------------------------------------------

    -- | Setting 'Relevance' if unset.

    setPristineRelevance :: (LensRelevance a) => Relevance -> a -> Maybe a
    setPristineRelevance :: forall a. LensRelevance a => Relevance -> a -> Maybe a
    setPristineRelevance Relevance
    r a
    a
      | Relevance -> Bool
    forall a. Null a => a -> Bool
    null (a -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance a
    a) = a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ Relevance -> a -> a
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance Relevance
    r a
    a
      | Bool
    otherwise = Maybe a
    forall a. Maybe a
    Nothing

    -- | Setting 'Quantity' if unset.

    setPristineQuantity :: (LensQuantity a) => Quantity -> a -> Maybe a
    setPristineQuantity :: forall a. LensQuantity a => Quantity -> a -> Maybe a
    setPristineQuantity Quantity
    q a
    a
      | a -> Bool
    forall a. LensQuantity a => a -> Bool
    noUserQuantity a
    a = a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ Quantity -> a -> a
    forall a. LensQuantity a => Quantity -> a -> a
    setQuantity Quantity
    q a
    a
      | Bool
    otherwise = Maybe a
    forall a. Maybe a
    Nothing

    -- | Setting 'Cohesion' if unset.

    setPristineCohesion :: (LensCohesion a) => Cohesion -> a -> Maybe a
    setPristineCohesion :: forall a. LensCohesion a => Cohesion -> a -> Maybe a
    setPristineCohesion Cohesion
    c a
    a
      | Cohesion -> Bool
    forall a. Null a => a -> Bool
    null (a -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion a
    a) = a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ Cohesion -> a -> a
    forall a. LensCohesion a => Cohesion -> a -> a
    setCohesion Cohesion
    c a
    a
      | Bool
    otherwise = Maybe a
    forall a. Maybe a
    Nothing

    -- | Setting 'ModalPolarity' if unset.

    setPristinePolarity :: (LensModalPolarity a) => PolarityModality -> a -> Maybe a
    setPristinePolarity :: forall a. LensModalPolarity a => PolarityModality -> a -> Maybe a
    setPristinePolarity PolarityModality
    c a
    a
      | a -> PolarityModality
    forall a. LensModalPolarity a => a -> PolarityModality
    getModalPolarity a
    a PolarityModality -> PolarityModality -> Bool
    forall a. Eq a => a -> a -> Bool
    == PolarityModality
    defaultPolarity = a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ PolarityModality -> a -> a
    forall a. LensModalPolarity a => PolarityModality -> a -> a
    setModalPolarity PolarityModality
    c a
    a
      | Bool
    otherwise = Maybe a
    forall a. Maybe a
    Nothing

    -- | Setting 'Lock' if unset.

    setPristineLock :: (LensLock a) => Lock -> a -> Maybe a
    setPristineLock :: forall a. LensLock a => Lock -> a -> Maybe a
    setPristineLock Lock
    q a
    a
      | a -> Lock
    forall a. LensLock a => a -> Lock
    getLock a
    a Lock -> Lock -> Bool
    forall a. Eq a => a -> a -> Bool
    == Lock
    defaultLock = a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ Lock -> a -> a
    forall a. LensLock a => Lock -> a -> a
    setLock Lock
    q a
    a
      | Bool
    otherwise = Maybe a
    forall a. Maybe a
    Nothing

    -- | Setting an unset attribute (to e.g. an 'Arg').

    setPristineAttribute :: (LensAttribute a) => Attribute -> a -> Maybe a
    setPristineAttribute :: forall a. LensAttribute a => Attribute -> a -> Maybe a
    setPristineAttribute = \case
      RelevanceAttribute Relevance
    r -> Relevance -> a -> Maybe a
    forall a. LensRelevance a => Relevance -> a -> Maybe a
    setPristineRelevance Relevance
    r
      QuantityAttribute  Quantity
    q -> Quantity -> a -> Maybe a
    forall a. LensQuantity a => Quantity -> a -> Maybe a
    setPristineQuantity  Quantity
    q
      CohesionAttribute  Cohesion
    c -> Cohesion -> a -> Maybe a
    forall a. LensCohesion a => Cohesion -> a -> Maybe a
    setPristineCohesion  Cohesion
    c
      PolarityAttribute  PolarityModality
    p -> PolarityModality -> a -> Maybe a
    forall a. LensModalPolarity a => PolarityModality -> a -> Maybe a
    setPristinePolarity  PolarityModality
    p
      LockAttribute      Lock
    l -> Lock -> a -> Maybe a
    forall a. LensLock a => Lock -> a -> Maybe a
    setPristineLock      Lock
    l
      TacticAttribute{}    -> a -> Maybe a
    forall a. a -> Maybe a
    Just

    -- | Setting a list of unset attributes.

    setPristineAttributes :: (LensAttribute a) => [Attribute] -> a -> Maybe a
    setPristineAttributes :: forall a. LensAttribute a => [Attribute] -> a -> Maybe a
    setPristineAttributes [Attribute]
    attrs a
    arg = (a -> Attribute -> Maybe a) -> a -> [Attribute] -> Maybe a
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM ((Attribute -> a -> Maybe a) -> a -> Attribute -> Maybe a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Attribute -> a -> Maybe a
    forall a. LensAttribute a => Attribute -> a -> Maybe a
    setPristineAttribute) a
    arg [Attribute]
    attrs

    ---------------------------------------------------------------------------
    -- * Filtering attributes
    ---------------------------------------------------------------------------

    isRelevanceAttribute :: Attribute -> Maybe Relevance
    isRelevanceAttribute :: Attribute -> Maybe Relevance
    isRelevanceAttribute = \case
      RelevanceAttribute Relevance
    q -> Relevance -> Maybe Relevance
    forall a. a -> Maybe a
    Just Relevance
    q
      Attribute
    _ -> Maybe Relevance
    forall a. Maybe a
    Nothing

    isQuantityAttribute :: Attribute -> Maybe Quantity
    isQuantityAttribute :: Attribute -> Maybe Quantity
    isQuantityAttribute = \case
      QuantityAttribute Quantity
    q -> Quantity -> Maybe Quantity
    forall a. a -> Maybe a
    Just Quantity
    q
      Attribute
    _ -> Maybe Quantity
    forall a. Maybe a
    Nothing

    isTacticAttribute :: Attribute -> TacticAttribute
    isTacticAttribute :: Attribute -> TacticAttribute
    isTacticAttribute = Maybe (Ranged Expr) -> TacticAttribute
    forall a. Maybe (Ranged a) -> TacticAttribute' a
    C.TacticAttribute (Maybe (Ranged Expr) -> TacticAttribute)
    -> (Attribute -> Maybe (Ranged Expr))
    -> Attribute
    -> TacticAttribute
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . \case
      TacticAttribute Ranged Expr
    t -> Ranged Expr -> Maybe (Ranged Expr)
    forall a. a -> Maybe a
    Just Ranged Expr
    t
      Attribute
    _ -> Maybe (Ranged Expr)
    forall a. Maybe a
    Nothing

    relevanceAttributes :: [Attribute] -> [Attribute]
    relevanceAttributes :: [Attribute] -> [Attribute]
    relevanceAttributes = (Attribute -> Bool) -> [Attribute] -> [Attribute]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((Attribute -> Bool) -> [Attribute] -> [Attribute])
    -> (Attribute -> Bool) -> [Attribute] -> [Attribute]
    forall a b. (a -> b) -> a -> b
    $ Maybe Relevance -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Relevance -> Bool)
    -> (Attribute -> Maybe Relevance) -> Attribute -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Attribute -> Maybe Relevance
    isRelevanceAttribute

    quantityAttributes :: [Attribute] -> [Attribute]
    quantityAttributes :: [Attribute] -> [Attribute]
    quantityAttributes = (Attribute -> Bool) -> [Attribute] -> [Attribute]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((Attribute -> Bool) -> [Attribute] -> [Attribute])
    -> (Attribute -> Bool) -> [Attribute] -> [Attribute]
    forall a b. (a -> b) -> a -> b
    $ Maybe Quantity -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Quantity -> Bool)
    -> (Attribute -> Maybe Quantity) -> Attribute -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Attribute -> Maybe Quantity
    isQuantityAttribute

    tacticAttributes :: [Attribute] -> [Attribute]
    tacticAttributes :: [Attribute] -> [Attribute]
    tacticAttributes = (Attribute -> Bool) -> [Attribute] -> [Attribute]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((Attribute -> Bool) -> [Attribute] -> [Attribute])
    -> (Attribute -> Bool) -> [Attribute] -> [Attribute]
    forall a b. (a -> b) -> a -> b
    $ Maybe (Ranged Expr) -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe (Ranged Expr) -> Bool)
    -> (Attribute -> Maybe (Ranged Expr)) -> Attribute -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TacticAttribute -> Maybe (Ranged Expr)
    forall a. TacticAttribute' a -> Maybe (Ranged a)
    C.theTacticAttribute (TacticAttribute -> Maybe (Ranged Expr))
    -> (Attribute -> TacticAttribute)
    -> Attribute
    -> Maybe (Ranged Expr)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Attribute -> TacticAttribute
    isTacticAttribute