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

    module Agda.Syntax.Concrete.Attribute where

    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(..))
    import Agda.Syntax.Concrete.Pretty () --instance only
    import Agda.Syntax.Position

    import Agda.Utils.List1 (List1, pattern (:|))
    import Agda.Utils.Pretty (prettyShow)

    import Agda.Utils.Impossible

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

    data Attribute
      = RelevanceAttribute Relevance
      | QuantityAttribute  Quantity
      | TacticAttribute Expr
      | CohesionAttribute Cohesion
      | 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
    showList :: [Attribute] -> ShowS
    $cshowList :: [Attribute] -> ShowS
    show :: Attribute -> String
    $cshow :: Attribute -> String
    showsPrec :: Int -> Attribute -> ShowS
    $cshowsPrec :: Int -> 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
        TacticAttribute Expr
    e    -> Expr -> Range
    forall a. HasRange a => a -> Range
    getRange 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
        TacticAttribute Expr
    e    -> Expr -> Attribute
    TacticAttribute 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
        TacticAttribute Expr
    e    -> Expr -> Attribute
    TacticAttribute    (Expr -> Attribute) -> Expr -> Attribute
    forall a b. (a -> b) -> a -> b
    $ KillRangeT Expr
    forall a. KillRange a => KillRangeT a
    killRange Expr
    e
        LockAttribute Lock
    l      -> Lock -> Attribute
    LockAttribute Lock
    l

    -- | (Conjunctive constraint.)

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

    -- | Modifiers for 'Relevance'.

    relevanceAttributeTable :: [(String, Relevance)]
    relevanceAttributeTable :: [(String, Relevance)]
    relevanceAttributeTable = [[(String, Relevance)]] -> [(String, Relevance)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
      [ (String -> (String, Relevance))
    -> [String] -> [(String, Relevance)]
    forall a b. (a -> b) -> [a] -> [b]
    map (, Relevance
    Irrelevant)  [ String
    "irr", String
    "irrelevant" ]
      , (String -> (String, Relevance))
    -> [String] -> [(String, Relevance)]
    forall a b. (a -> b) -> [a] -> [b]
    map (, Relevance
    NonStrict)   [ String
    "shirr", String
    "shape-irrelevant" ]
      , (String -> (String, Relevance))
    -> [String] -> [(String, Relevance)]
    forall a b. (a -> b) -> [a] -> [b]
    map (, Relevance
    Relevant)    [ String
    "relevant" ]
      ]

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

    -- | 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 (, Lock
    IsLock) [ String
    "lock", String
    "tick" ] -- 🔓
      ]

    -- | 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 (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 (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 (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second Cohesion -> Attribute
    CohesionAttribute)  [(String, Cohesion)]
    cohesionAttributeTable
      , ((String, Lock) -> (String, Attribute))
    -> [(String, Lock)] -> [(String, Attribute)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Lock -> Attribute) -> (String, Lock) -> (String, Attribute)
    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 :: Expr -> Maybe Attribute
    exprToAttribute :: Expr -> Maybe Attribute
    exprToAttribute (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
    $ Expr -> Attribute
    TacticAttribute Expr
    t
    exprToAttribute Expr
    e = Range -> Maybe Attribute -> Maybe Attribute
    forall a. SetRange a => Range -> a -> a
    setRange (Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e) (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
      LockAttribute      Lock
    l -> Lock -> a -> a
    forall a. LensLock a => Lock -> a -> a
    setLock      Lock
    l
      TacticAttribute 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 (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
      | a -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance a
    a Relevance -> Relevance -> Bool
    forall a. Eq a => a -> a -> Bool
    == Relevance
    defaultRelevance = 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
      | a -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion a
    a Cohesion -> Cohesion -> Bool
    forall a. Eq a => a -> a -> Bool
    == Cohesion
    defaultCohesion = 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 '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
      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 -> Maybe Expr
    isTacticAttribute :: Attribute -> Maybe Expr
    isTacticAttribute (TacticAttribute Expr
    t) = Expr -> Maybe Expr
    forall a. a -> Maybe a
    Just Expr
    t
    isTacticAttribute Attribute
    _                   = Maybe 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 Expr -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Expr -> Bool)
    -> (Attribute -> Maybe Expr) -> Attribute -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Attribute -> Maybe Expr
    isTacticAttribute