{-# LANGUAGE TupleSections #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ConstraintKinds #-}
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.Name
data Attribute
= RelevanceAttribute Relevance
| QuantityAttribute Quantity
deriving (Eq, Ord, Show)
type LensAttribute a = (LensRelevance a, LensQuantity a)
relevanceAttributeTable :: [(String, Relevance)]
relevanceAttributeTable = concat
[ map (, Irrelevant) [ "irr", "irrelevant" ]
, map (, NonStrict) [ "shirr", "shape-irrelevant" ]
, map (, Relevant) [ "relevant" ]
]
quantityAttributeTable :: [(String, Quantity)]
quantityAttributeTable = concat
[ map (, Quantity0) [ "0", "erased" ]
, map (, Quantityω) [ "ω", "plenty" ]
]
attributesMap :: Map String Attribute
attributesMap = Map.fromList $ concat
[ map (second RelevanceAttribute) relevanceAttributeTable
, map (second QuantityAttribute) quantityAttributeTable
]
stringToAttribute :: String -> Maybe Attribute
stringToAttribute = (`Map.lookup` attributesMap)
setAttribute :: (LensAttribute a) => Attribute -> a -> a
setAttribute = \case
RelevanceAttribute r -> setRelevance r
QuantityAttribute q -> setQuantity q
setAttributes :: (LensAttribute a) => [Attribute] -> a -> a
setAttributes attrs arg = foldl' (flip setAttribute) arg attrs
setPristineRelevance :: (LensRelevance a) => Relevance -> a -> Maybe a
setPristineRelevance r a
| getRelevance a == defaultRelevance = Just $ setRelevance r a
| otherwise = Nothing
setPristineQuantity :: (LensQuantity a) => Quantity -> a -> Maybe a
setPristineQuantity q a
| getQuantity a == defaultQuantity = Just $ setQuantity q a
| otherwise = Nothing
setPristineAttribute :: (LensAttribute a) => Attribute -> a -> Maybe a
setPristineAttribute = \case
RelevanceAttribute r -> setPristineRelevance r
QuantityAttribute q -> setPristineQuantity q
setPristineAttributes :: (LensAttribute a) => [Attribute] -> a -> Maybe a
setPristineAttributes attrs arg = foldM (flip setPristineAttribute) arg attrs
isRelevanceAttribute :: Attribute -> Maybe Relevance
isRelevanceAttribute = \case
RelevanceAttribute q -> Just q
_ -> Nothing
isQuantityAttribute :: Attribute -> Maybe Quantity
isQuantityAttribute = \case
QuantityAttribute q -> Just q
_ -> Nothing
relevanceAttributes :: [Attribute] -> [Attribute]
relevanceAttributes = filter $ isJust . isRelevanceAttribute
quantityAttributes :: [Attribute] -> [Attribute]
quantityAttributes = filter $ isJust . isQuantityAttribute