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

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

import Agda.Utils.Impossible

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

data Attribute
  = RelevanceAttribute Relevance
  | QuantityAttribute  Quantity
  | TacticAttribute (Ranged Expr)
  | CohesionAttribute Cohesion
  | LockAttribute      Lock
  deriving (Int -> Attribute -> ShowS
[Attribute] -> ShowS
Attribute -> String
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 -> forall a. HasRange a => a -> Range
getRange Relevance
r
    QuantityAttribute Quantity
q  -> forall a. HasRange a => a -> Range
getRange Quantity
q
    CohesionAttribute Cohesion
c  -> forall a. HasRange a => a -> Range
getRange Cohesion
c
    TacticAttribute Ranged Expr
e    -> forall a. HasRange a => a -> Range
getRange Ranged Expr
e
    LockAttribute Lock
l      -> forall a. Range' a
NoRange

instance SetRange Attribute where
  setRange :: Range -> Attribute -> Attribute
setRange Range
r = \case
    RelevanceAttribute Relevance
a -> Relevance -> Attribute
RelevanceAttribute forall a b. (a -> b) -> a -> b
$ forall a. SetRange a => Range -> a -> a
setRange Range
r Relevance
a
    QuantityAttribute Quantity
q  -> Quantity -> Attribute
QuantityAttribute  forall a b. (a -> b) -> a -> b
$ forall a. SetRange a => Range -> a -> a
setRange Range
r Quantity
q
    CohesionAttribute Cohesion
c  -> Cohesion -> Attribute
CohesionAttribute  forall a b. (a -> b) -> a -> b
$ forall a. SetRange a => Range -> a -> a
setRange Range
r Cohesion
c
    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

instance KillRange Attribute where
  killRange :: Attribute -> Attribute
killRange = \case
    RelevanceAttribute Relevance
a -> Relevance -> Attribute
RelevanceAttribute forall a b. (a -> b) -> a -> b
$ forall a. KillRange a => KillRangeT a
killRange Relevance
a
    QuantityAttribute Quantity
q  -> Quantity -> Attribute
QuantityAttribute  forall a b. (a -> b) -> a -> b
$ forall a. KillRange a => KillRangeT a
killRange Quantity
q
    CohesionAttribute Cohesion
c  -> Cohesion -> Attribute
CohesionAttribute  forall a b. (a -> b) -> a -> b
$ forall a. KillRange a => KillRangeT a
killRange Cohesion
c
    TacticAttribute Ranged Expr
e    -> Ranged Expr -> Attribute
TacticAttribute    forall a b. (a -> b) -> a -> b
$ forall a. KillRange a => KillRangeT a
killRange Ranged 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 = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ forall a b. (a -> b) -> [a] -> [b]
map (, Relevance
Irrelevant)  [ String
"irr", String
"irrelevant" ]
  , forall a b. (a -> b) -> [a] -> [b]
map (, Relevance
NonStrict)   [ String
"shirr", String
"shape-irrelevant" ]
  , 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 forall a b. (a -> b) -> a -> b
$ Range -> Q0Origin
Q0       forall a. Range' a
noRange)
  , (String
"erased" , Q0Origin -> Quantity
Quantity0 forall a b. (a -> b) -> a -> b
$ Range -> Q0Origin
Q0Erased forall a. Range' a
noRange)
  -- TODO: linearity
  -- , ("1"      , Quantity1 $ Q1       noRange)
  -- , ("linear" , Quantity1 $ Q1Linear noRange)
  , (String
"ω"      , QωOrigin -> Quantity
Quantityω forall a b. (a -> b) -> a -> b
$ Range -> QωOrigin
Qω       forall a. Range' a
noRange)
  , (String
"plenty" , QωOrigin -> Quantity
Quantityω forall a b. (a -> b) -> a -> b
$ Range -> QωOrigin
QωPlenty 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)
  ]

-- | 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 = [(Attribute, Range, String)]

-- | Modifiers for 'Quantity'.

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


-- | Concrete syntax for all attributes.

attributesMap :: Map String Attribute
attributesMap :: Map String Attribute
attributesMap = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Relevance -> Attribute
RelevanceAttribute) [(String, Relevance)]
relevanceAttributeTable
  , forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Quantity -> Attribute
QuantityAttribute)  [(String, Quantity)]
quantityAttributeTable
  , forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Cohesion -> Attribute
CohesionAttribute)  [(String, Cohesion)]
cohesionAttributeTable
  , forall a b. (a -> b) -> [a] -> [b]
map (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 = (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 = \case
  e :: Expr
e@(Paren Range
_ (Tactic Range
_ Expr
t)) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Ranged Expr -> Attribute
TacticAttribute forall a b. (a -> b) -> a -> b
$ forall a. Range -> a -> Ranged a
Ranged (forall a. HasRange a => a -> Range
getRange Expr
e) Expr
t
  Expr
e -> forall a. SetRange a => Range -> a -> a
setRange (forall a. HasRange a => a -> Range
getRange Expr
e) forall a b. (a -> b) -> a -> b
$ String -> Maybe Attribute
stringToAttribute forall a b. (a -> b) -> a -> b
$ 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 -> forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
r
  QuantityAttribute  Quantity
q -> forall a. LensQuantity a => Quantity -> a -> a
setQuantity  Quantity
q
  CohesionAttribute  Cohesion
c -> forall a. LensCohesion a => Cohesion -> a -> a
setCohesion  Cohesion
c
  LockAttribute      Lock
l -> forall a. LensLock a => Lock -> a -> a
setLock      Lock
l
  TacticAttribute Ranged Expr
t    -> 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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip 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
  | forall a. LensRelevance a => a -> Relevance
getRelevance a
a forall a. Eq a => a -> a -> Bool
== Relevance
defaultRelevance = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
r a
a
  | Bool
otherwise = 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
  | forall a. LensQuantity a => a -> Bool
noUserQuantity a
a = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
q a
a
  | Bool
otherwise = 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
  | forall a. LensCohesion a => a -> Cohesion
getCohesion a
a forall a. Eq a => a -> a -> Bool
== Cohesion
defaultCohesion = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. LensCohesion a => Cohesion -> a -> a
setCohesion Cohesion
c a
a
  | Bool
otherwise = 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
  | forall a. LensLock a => a -> Lock
getLock a
a forall a. Eq a => a -> a -> Bool
== Lock
defaultLock = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. LensLock a => Lock -> a -> a
setLock Lock
q a
a
  | Bool
otherwise = 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 -> forall a. LensRelevance a => Relevance -> a -> Maybe a
setPristineRelevance Relevance
r
  QuantityAttribute  Quantity
q -> forall a. LensQuantity a => Quantity -> a -> Maybe a
setPristineQuantity  Quantity
q
  CohesionAttribute  Cohesion
c -> forall a. LensCohesion a => Cohesion -> a -> Maybe a
setPristineCohesion  Cohesion
c
  LockAttribute      Lock
l -> forall a. LensLock a => Lock -> a -> Maybe a
setPristineLock      Lock
l
  TacticAttribute{}    -> 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 = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 -> forall a. a -> Maybe a
Just Relevance
q
  Attribute
_ -> forall a. Maybe a
Nothing

isQuantityAttribute :: Attribute -> Maybe Quantity
isQuantityAttribute :: Attribute -> Maybe Quantity
isQuantityAttribute = \case
  QuantityAttribute Quantity
q -> forall a. a -> Maybe a
Just Quantity
q
  Attribute
_ -> forall a. Maybe a
Nothing

isTacticAttribute :: Attribute -> TacticAttribute
isTacticAttribute :: Attribute -> TacticAttribute
isTacticAttribute (TacticAttribute Ranged Expr
t) = forall a. a -> Maybe a
Just Ranged Expr
t
isTacticAttribute Attribute
_                   = forall a. Maybe a
Nothing

relevanceAttributes :: [Attribute] -> [Attribute]
relevanceAttributes :: [Attribute] -> [Attribute]
relevanceAttributes = forall a. (a -> Bool) -> [a] -> [a]
filter forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attribute -> Maybe Relevance
isRelevanceAttribute

quantityAttributes :: [Attribute] -> [Attribute]
quantityAttributes :: [Attribute] -> [Attribute]
quantityAttributes = forall a. (a -> Bool) -> [a] -> [a]
filter forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attribute -> Maybe Quantity
isQuantityAttribute

tacticAttributes :: [Attribute] -> [Attribute]
tacticAttributes :: [Attribute] -> [Attribute]
tacticAttributes = forall a. (a -> Bool) -> [a] -> [a]
filter forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attribute -> TacticAttribute
isTacticAttribute