{-# 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.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.Tuple (second)

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
  | RewriteAttribute RewriteAnn
  deriving (Int -> Attribute -> ShowS
[Attribute] -> ShowS
Attribute -> [Char]
(Int -> Attribute -> ShowS)
-> (Attribute -> [Char])
-> ([Attribute] -> ShowS)
-> Show Attribute
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Attribute -> ShowS
showsPrec :: Int -> Attribute -> ShowS
$cshow :: Attribute -> [Char]
show :: Attribute -> [Char]
$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
    RewriteAttribute RewriteAnn
_r  -> 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
    RewriteAttribute RewriteAnn
r   -> RewriteAnn -> Attribute
RewriteAttribute RewriteAnn
r

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
    RewriteAttribute RewriteAnn
r   -> RewriteAnn -> Attribute
RewriteAttribute RewriteAnn
r

-- | Parsed attribute.

data Attr = Attr
  { Attr -> Range
attrRange :: Range       -- ^ Range includes the @.
  , Attr -> [Char]
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 -> [Char]
(Int -> Attr -> ShowS)
-> (Attr -> [Char]) -> ([Attr] -> ShowS) -> Show Attr
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Attr -> ShowS
showsPrec :: Int -> Attr -> ShowS
$cshow :: Attr -> [Char]
show :: Attr -> [Char]
$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
_ [Char]
x Attribute
a) = Range -> [Char] -> Attribute -> Attr
Attr Range
r [Char]
x Attribute
a

instance KillRange Attr where
  killRange :: Attr -> Attr
killRange (Attr Range
_ [Char]
x Attribute
a) = Range -> [Char] -> Attribute -> Attr
Attr Range
forall a. Range' a
noRange [Char]
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, LensRewriteAnn a)

-- | Modifiers for 'Relevance'.

relevanceAttributeTable :: [(String, Relevance)]
relevanceAttributeTable :: [([Char], Relevance)]
relevanceAttributeTable =
  [ ([Char]
"irr"             , OriginIrrelevant -> Relevance
Irrelevant      (OriginIrrelevant -> Relevance) -> OriginIrrelevant -> Relevance
forall a b. (a -> b) -> a -> b
$ Range -> OriginIrrelevant
OIrrIrr               Range
forall a. Range' a
noRange)
  , ([Char]
"irrelevant"      , OriginIrrelevant -> Relevance
Irrelevant      (OriginIrrelevant -> Relevance) -> OriginIrrelevant -> Relevance
forall a b. (a -> b) -> a -> b
$ Range -> OriginIrrelevant
OIrrIrrelevant        Range
forall a. Range' a
noRange)
  , ([Char]
"shirr"           , OriginShapeIrrelevant -> Relevance
ShapeIrrelevant (OriginShapeIrrelevant -> Relevance)
-> OriginShapeIrrelevant -> Relevance
forall a b. (a -> b) -> a -> b
$ Range -> OriginShapeIrrelevant
OShIrrShIrr           Range
forall a. Range' a
noRange)
  , ([Char]
"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)
  , ([Char]
"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 :: [([Char], Quantity)]
quantityAttributeTable =
  [ ([Char]
"0"      , Q0Origin -> Quantity
Quantity0 (Q0Origin -> Quantity) -> Q0Origin -> Quantity
forall a b. (a -> b) -> a -> b
$ Range -> Q0Origin
Q0       Range
forall a. Range' a
noRange)
  , ([Char]
"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)
  , ([Char]
"ω"      , 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)
  , ([Char]
"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 :: [([Char], Cohesion)]
cohesionAttributeTable =
  [ ([Char]
"♭"    , Cohesion
Flat)
  , ([Char]
"flat" , Cohesion
Flat)
  , ([Char]
"♯"    , Cohesion
Sharp)
  , ([Char]
"sharp", Cohesion
Sharp)
  ]

-- | 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 :: [([Char], PolarityModality)]
polarityAttributeTable =
  [ ([Char]
"unused" , ModalPolarity -> PolarityModality
withStandardLock ModalPolarity
UnusedPolarity)
  , ([Char]
"++" , ModalPolarity -> PolarityModality
withStandardLock ModalPolarity
StrictlyPositive)
  , ([Char]
"+" , ModalPolarity -> PolarityModality
withStandardLock ModalPolarity
Positive)
  , ([Char]
"-" , ModalPolarity -> PolarityModality
withStandardLock ModalPolarity
Negative)
  , ([Char]
"mixed" , ModalPolarity -> PolarityModality
withStandardLock ModalPolarity
MixedPolarity)]

-- | Modifiers for 'Lock'.

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

-- | Modifiers for @RewriteAnn@
--   I don't think we ever actually hit this because 'rewrite' is a keyword
--   Of course, we might want to add aliases
rewriteAttributeTable :: [(String, RewriteAnn)]
rewriteAttributeTable :: [([Char], RewriteAnn)]
rewriteAttributeTable =
  [ ([Char]
"rewrite" , Range -> RewriteAnn
IsRewrite Range
forall a. Range' a
noRange)
  ]

-- | Concrete syntax for all attributes.

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

-- | Parsing a string into an attribute.

stringToAttribute :: String -> Maybe Attribute
stringToAttribute :: [Char] -> Maybe Attribute
stringToAttribute = ([Char] -> Map [Char] Attribute -> Maybe Attribute
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map [Char] 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
$ [Char] -> Maybe Attribute
stringToAttribute ([Char] -> Maybe Attribute) -> [Char] -> Maybe Attribute
forall a b. (a -> b) -> a -> b
$ Expr -> [Char]
forall a. Pretty a => a -> [Char]
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
  RewriteAttribute   RewriteAnn
r -> RewriteAnn -> a -> a
forall a. LensRewriteAnn a => RewriteAnn -> a -> a
setRewriteAnn RewriteAnn
r
  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 'RewriteAnn' if unset.

setPristineRewriteAnn :: (LensRewriteAnn a) => RewriteAnn -> a -> Maybe a
setPristineRewriteAnn :: forall a. LensRewriteAnn a => RewriteAnn -> a -> Maybe a
setPristineRewriteAnn RewriteAnn
q a
a
  | a -> RewriteAnn
forall a. LensRewriteAnn a => a -> RewriteAnn
getRewriteAnn a
a RewriteAnn -> RewriteAnn -> Bool
forall a. Eq a => a -> a -> Bool
== RewriteAnn
defaultRewrite = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ RewriteAnn -> a -> a
forall a. LensRewriteAnn a => RewriteAnn -> a -> a
setRewriteAnn RewriteAnn
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
  RewriteAttribute   RewriteAnn
r -> RewriteAnn -> a -> Maybe a
forall a. LensRewriteAnn a => RewriteAnn -> a -> Maybe a
setPristineRewriteAnn RewriteAnn
r
  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

isRewriteAttribute :: Attribute -> Maybe RewriteAnn
isRewriteAttribute :: Attribute -> Maybe RewriteAnn
isRewriteAttribute = \case
  RewriteAttribute RewriteAnn
q -> RewriteAnn -> Maybe RewriteAnn
forall a. a -> Maybe a
Just RewriteAnn
q
  Attribute
_                  -> Maybe RewriteAnn
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

rewAttributes :: [Attribute] -> [Attribute]
rewAttributes :: [Attribute] -> [Attribute]
rewAttributes = (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 RewriteAnn -> Bool
forall a. Maybe a -> Bool
isJust (Maybe RewriteAnn -> Bool)
-> (Attribute -> Maybe RewriteAnn) -> Attribute -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attribute -> Maybe RewriteAnn
isRewriteAttribute