-- | 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 :: 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 :: [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 :: 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 :: 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 :: 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 :: 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 :: 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 :: [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