{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wunused-matches #-}
{-# OPTIONS_GHC -Wunused-binds #-}

{-# LANGUAGE CPP #-}

-- | 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)

#if !MIN_VERSION_base(4,20,0)
import Data.List (foldl')
#endif

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.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
  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
_    -> 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