content: {-# 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 (Show)
  
  instance HasRange Attribute where
    getRange = \case
      RelevanceAttribute r -> getRange r
      QuantityAttribute q  -> getRange q
      CohesionAttribute c  -> getRange c
      PolarityAttribute p  -> getRange p
      TacticAttribute e    -> getRange e
      LockAttribute _l     -> NoRange
  
  instance SetRange Attribute where
    setRange r = \case
      RelevanceAttribute a -> RelevanceAttribute $ setRange r a
      QuantityAttribute q  -> QuantityAttribute  $ setRange r q
      CohesionAttribute c  -> CohesionAttribute  $ setRange r c
      PolarityAttribute p  -> PolarityAttribute  $ setRange r p
      TacticAttribute e    -> TacticAttribute e  -- -- $ setRange r e -- SetRange Expr not yet implemented
      LockAttribute l      -> LockAttribute l
  
  instance KillRange Attribute where
    killRange = \case
      RelevanceAttribute a -> RelevanceAttribute $ killRange a
      QuantityAttribute q  -> QuantityAttribute  $ killRange q
      CohesionAttribute c  -> CohesionAttribute  $ killRange c
      PolarityAttribute p  -> PolarityAttribute  $ killRange p
      TacticAttribute e    -> TacticAttribute    $ killRange e
      LockAttribute l      -> LockAttribute l
  
  -- | Parsed attribute.
  
  data Attr = Attr
    { attrRange :: Range       -- ^ Range includes the @.
    , attrName  :: String      -- ^ Concrete, user written attribute for error reporting, not including the "@".
    , theAttr   :: Attribute   -- ^ Parsed attribute.
    } deriving (Show)
  
  instance HasRange Attr where
    getRange = attrRange
  
  instance SetRange Attr where
    setRange r (Attr _ x a) = Attr r x a
  
  instance KillRange Attr where
    killRange (Attr _ x a) = Attr noRange x (killRange a)
  
  -- | (Conjunctive constraint.)
  
  type LensAttribute a = (LensRelevance a, LensQuantity a, LensCohesion a, LensModalPolarity a, LensLock a)
  
  -- | Modifiers for 'Relevance'.
  
  relevanceAttributeTable :: [(String, Relevance)]
  relevanceAttributeTable =
    [ ("irr"             , Irrelevant      $ OIrrIrr               noRange)
    , ("irrelevant"      , Irrelevant      $ OIrrIrrelevant        noRange)
    , ("shirr"           , ShapeIrrelevant $ OShIrrShIrr           noRange)
    , ("shape-irrelevant", ShapeIrrelevant $ OShIrrShapeIrrelevant noRange)
    , ("relevant"        , Relevant        $ ORelRelevant          noRange)
    ]
  
  -- | Modifiers for 'Quantity'.
  
  quantityAttributeTable :: [(String, Quantity)]
  quantityAttributeTable =
    [ ("0"      , Quantity0 $ Q0       noRange)
    , ("erased" , Quantity0 $ Q0Erased noRange)
    -- TODO: linearity
    -- , ("1"      , Quantity1 $ Q1       noRange)
    -- , ("linear" , Quantity1 $ Q1Linear noRange)
    , ("ω"      , Quantityω $ Qω       noRange)
    , ("plenty" , Quantityω $ QωPlenty 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 =
    [ ("♭"    , Flat)
    , ("flat" , 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 =
    [ ("unused" , withStandardLock UnusedPolarity)
    , ("++" , withStandardLock StrictlyPositive)
    , ("+" , withStandardLock Positive)
    , ("-" , withStandardLock Negative)
    , ("mixed" , withStandardLock MixedPolarity)]
  
  -- | Modifiers for 'Quantity'.
  
  lockAttributeTable :: [(String, Lock)]
  lockAttributeTable = concat
    [ map (, IsNotLock) [ "notlock" ] -- default, shouldn't be used much
    , map (, IsLock LockOTick) [ "tick" ] -- @tick
    , map (, IsLock LockOLock) [ "lock" ] -- @lock
    ]
  
  
  -- | Concrete syntax for all attributes.
  
  attributesMap :: Map String Attribute
  attributesMap = Map.fromListWith __IMPOSSIBLE__ $ concat
    [ map (second RelevanceAttribute) relevanceAttributeTable
    , map (second QuantityAttribute)  quantityAttributeTable
    , map (second CohesionAttribute)  cohesionAttributeTable
    , map (second PolarityAttribute)  polarityAttributeTable
    , map (second LockAttribute)      lockAttributeTable
    ]
  
  -- | Parsing a string into an attribute.
  
  stringToAttribute :: String -> Maybe Attribute
  stringToAttribute = (`Map.lookup` attributesMap)
  
  -- | Parsing an expression into an attribute.
  
  exprToAttribute :: Range -> Expr -> Maybe Attribute
  exprToAttribute r = \case
    Paren _ (Tactic _ t) -> Just $ TacticAttribute $ Ranged r t
    e -> setRange r $ stringToAttribute $ prettyShow e
  
  -- | Setting an attribute (in e.g. an 'Arg').  Overwrites previous value.
  
  setAttribute :: (LensAttribute a) => Attribute -> a -> a
  setAttribute = \case
    RelevanceAttribute r -> setRelevance r
    QuantityAttribute  q -> setQuantity  q
    CohesionAttribute  c -> setCohesion  c
    PolarityAttribute  p -> setModalPolarity p
    LockAttribute      l -> setLock      l
    TacticAttribute _    -> id
  
  
  -- | Setting some attributes in left-to-right order.
  --   Blindly overwrites previous settings.
  
  setAttributes :: (LensAttribute a) => [Attribute] -> a -> a
  setAttributes attrs arg = foldl' (flip setAttribute) arg 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 r a
    | null (getRelevance a) = Just $ setRelevance r a
    | otherwise = Nothing
  
  -- | Setting 'Quantity' if unset.
  
  setPristineQuantity :: (LensQuantity a) => Quantity -> a -> Maybe a
  setPristineQuantity q a
    | noUserQuantity a = Just $ setQuantity q a
    | otherwise = Nothing
  
  -- | Setting 'Cohesion' if unset.
  
  setPristineCohesion :: (LensCohesion a) => Cohesion -> a -> Maybe a
  setPristineCohesion c a
    | null (getCohesion a) = Just $ setCohesion c a
    | otherwise = Nothing
  
  -- | Setting 'ModalPolarity' if unset.
  
  setPristinePolarity :: (LensModalPolarity a) => PolarityModality -> a -> Maybe a
  setPristinePolarity c a
    | getModalPolarity a == defaultPolarity = Just $ setModalPolarity c a
    | otherwise = Nothing
  
  -- | Setting 'Lock' if unset.
  
  setPristineLock :: (LensLock a) => Lock -> a -> Maybe a
  setPristineLock q a
    | getLock a == defaultLock = Just $ setLock q a
    | otherwise = Nothing
  
  -- | Setting an unset attribute (to e.g. an 'Arg').
  
  setPristineAttribute :: (LensAttribute a) => Attribute -> a -> Maybe a
  setPristineAttribute = \case
    RelevanceAttribute r -> setPristineRelevance r
    QuantityAttribute  q -> setPristineQuantity  q
    CohesionAttribute  c -> setPristineCohesion  c
    PolarityAttribute  p -> setPristinePolarity  p
    LockAttribute      l -> setPristineLock      l
    TacticAttribute{}    -> Just
  
  -- | Setting a list of unset attributes.
  
  setPristineAttributes :: (LensAttribute a) => [Attribute] -> a -> Maybe a
  setPristineAttributes attrs arg = foldM (flip setPristineAttribute) arg attrs
  
  ---------------------------------------------------------------------------
  -- * Filtering attributes
  ---------------------------------------------------------------------------
  
  isRelevanceAttribute :: Attribute -> Maybe Relevance
  isRelevanceAttribute = \case
    RelevanceAttribute q -> Just q
    _ -> Nothing
  
  isQuantityAttribute :: Attribute -> Maybe Quantity
  isQuantityAttribute = \case
    QuantityAttribute q -> Just q
    _ -> Nothing
  
  isTacticAttribute :: Attribute -> TacticAttribute
  isTacticAttribute = C.TacticAttribute . \case
    TacticAttribute t -> Just t
    _ -> Nothing
  
  relevanceAttributes :: [Attribute] -> [Attribute]
  relevanceAttributes = filter $ isJust . isRelevanceAttribute
  
  quantityAttributes :: [Attribute] -> [Attribute]
  quantityAttributes = filter $ isJust . isQuantityAttribute
  
  tacticAttributes :: [Attribute] -> [Attribute]
  tacticAttributes = filter $ isJust . C.theTacticAttribute . isTacticAttribute
  