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 qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Syntax.Position
import Agda.Utils.List1 (List1, pattern (:|))
import Agda.Utils.Impossible
data Attribute
= RelevanceAttribute Relevance
| QuantityAttribute Quantity
| TacticAttribute (Ranged 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
$cshowsPrec :: Int -> Attribute -> ShowS
showsPrec :: Int -> Attribute -> ShowS
$cshow :: Attribute -> String
show :: Attribute -> String
$cshowList :: [Attribute] -> ShowS
showList :: [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 Ranged Expr
e -> Ranged Expr -> Range
forall a. HasRange a => a -> Range
getRange Ranged 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 Ranged Expr
e -> Ranged Expr -> Attribute
TacticAttribute Ranged Expr
e
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 Ranged Expr
e -> Ranged Expr -> Attribute
TacticAttribute (Ranged Expr -> Attribute) -> Ranged Expr -> Attribute
forall a b. (a -> b) -> a -> b
$ KillRangeT (Ranged Expr)
forall a. KillRange a => KillRangeT a
killRange Ranged Expr
e
LockAttribute Lock
l -> Lock -> Attribute
LockAttribute Lock
l
type LensAttribute a = (LensRelevance a, LensQuantity a, LensCohesion a, LensLock a)
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" ]
]
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)
, (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)
]
cohesionAttributeTable :: [(String, Cohesion)]
cohesionAttributeTable :: [(String, Cohesion)]
cohesionAttributeTable =
[ (String
"♭" , Cohesion
Flat)
, (String
"flat" , Cohesion
Flat)
]
type Attributes = [(Attribute, Range, String)]
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" ]
, (String -> (String, Lock)) -> [String] -> [(String, Lock)]
forall a b. (a -> b) -> [a] -> [b]
map (, LockOrigin -> Lock
IsLock LockOrigin
LockOTick) [ String
"tick" ]
, (String -> (String, Lock)) -> [String] -> [(String, Lock)]
forall a b. (a -> b) -> [a] -> [b]
map (, LockOrigin -> Lock
IsLock LockOrigin
LockOLock) [ String
"lock" ]
]
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 b c d. (b -> c) -> (d, b) -> (d, c)
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 b c d. (b -> c) -> (d, b) -> (d, c)
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 b c d. (b -> c) -> (d, b) -> (d, c)
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 b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Lock -> Attribute
LockAttribute) [(String, Lock)]
lockAttributeTable
]
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)
exprToAttribute :: Expr -> Maybe Attribute
exprToAttribute :: Expr -> Maybe Attribute
exprToAttribute = \case
e :: Expr
e@(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
$ Ranged Expr -> Attribute
TacticAttribute (Ranged Expr -> Attribute) -> Ranged Expr -> Attribute
forall a b. (a -> b) -> a -> b
$ Range -> Expr -> Ranged Expr
forall a. Range -> a -> Ranged a
Ranged (Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e) Expr
t
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
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 Ranged Expr
t -> a -> a
forall a. a -> a
id
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 b a. (b -> a -> b) -> b -> [a] -> b
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
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
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
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
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
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
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
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 -> TacticAttribute
isTacticAttribute :: Attribute -> TacticAttribute
isTacticAttribute = Maybe (Ranged Expr) -> TacticAttribute
forall a. Maybe (Ranged a) -> TacticAttribute' a
C.TacticAttribute (Maybe (Ranged Expr) -> TacticAttribute)
-> (Attribute -> Maybe (Ranged Expr))
-> Attribute
-> TacticAttribute
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
TacticAttribute Ranged Expr
t -> Ranged Expr -> Maybe (Ranged Expr)
forall a. a -> Maybe a
Just Ranged Expr
t
Attribute
_ -> Maybe (Ranged 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 (Ranged Expr) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Ranged Expr) -> Bool)
-> (Attribute -> Maybe (Ranged Expr)) -> Attribute -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticAttribute -> Maybe (Ranged Expr)
forall a. TacticAttribute' a -> Maybe (Ranged a)
C.theTacticAttribute (TacticAttribute -> Maybe (Ranged Expr))
-> (Attribute -> TacticAttribute)
-> Attribute
-> Maybe (Ranged Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attribute -> TacticAttribute
isTacticAttribute