module Agda.Syntax.Common.Aspect where
import Agda.Syntax.TopLevelModuleName.Boot (TopLevelModuleName')
import Agda.Syntax.Position (Range)
import Agda.Utils.Maybe
import GHC.Generics
import Data.Set (Set)
import Control.DeepSeq
data Induction = Inductive | CoInductive
deriving (Induction -> Induction -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Induction -> Induction -> Bool
$c/= :: Induction -> Induction -> Bool
== :: Induction -> Induction -> Bool
$c== :: Induction -> Induction -> Bool
Eq, Eq Induction
Induction -> Induction -> Bool
Induction -> Induction -> Ordering
Induction -> Induction -> Induction
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Induction -> Induction -> Induction
$cmin :: Induction -> Induction -> Induction
max :: Induction -> Induction -> Induction
$cmax :: Induction -> Induction -> Induction
>= :: Induction -> Induction -> Bool
$c>= :: Induction -> Induction -> Bool
> :: Induction -> Induction -> Bool
$c> :: Induction -> Induction -> Bool
<= :: Induction -> Induction -> Bool
$c<= :: Induction -> Induction -> Bool
< :: Induction -> Induction -> Bool
$c< :: Induction -> Induction -> Bool
compare :: Induction -> Induction -> Ordering
$ccompare :: Induction -> Induction -> Ordering
Ord, Int -> Induction -> ShowS
[Induction] -> ShowS
Induction -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Induction] -> ShowS
$cshowList :: [Induction] -> ShowS
show :: Induction -> String
$cshow :: Induction -> String
showsPrec :: Int -> Induction -> ShowS
$cshowsPrec :: Int -> Induction -> ShowS
Show)
data Aspect
=
| Keyword
| String
| Number
| Hole
| Symbol
| PrimitiveType
| Name (Maybe NameKind) Bool
| Pragma
| Background
| Markup
deriving (Aspect -> Aspect -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Aspect -> Aspect -> Bool
$c/= :: Aspect -> Aspect -> Bool
== :: Aspect -> Aspect -> Bool
$c== :: Aspect -> Aspect -> Bool
Eq, Int -> Aspect -> ShowS
[Aspect] -> ShowS
Aspect -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Aspect] -> ShowS
$cshowList :: [Aspect] -> ShowS
show :: Aspect -> String
$cshow :: Aspect -> String
showsPrec :: Int -> Aspect -> ShowS
$cshowsPrec :: Int -> Aspect -> ShowS
Show, forall x. Rep Aspect x -> Aspect
forall x. Aspect -> Rep Aspect x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Aspect x -> Aspect
$cfrom :: forall x. Aspect -> Rep Aspect x
Generic)
data NameKind
= Bound
| Generalizable
| Constructor Induction
| Datatype
| Field
| Function
| Module
| Postulate
| Primitive
| Record
| Argument
| Macro
deriving (NameKind -> NameKind -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NameKind -> NameKind -> Bool
$c/= :: NameKind -> NameKind -> Bool
== :: NameKind -> NameKind -> Bool
$c== :: NameKind -> NameKind -> Bool
Eq, Int -> NameKind -> ShowS
[NameKind] -> ShowS
NameKind -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NameKind] -> ShowS
$cshowList :: [NameKind] -> ShowS
show :: NameKind -> String
$cshow :: NameKind -> String
showsPrec :: Int -> NameKind -> ShowS
$cshowsPrec :: Int -> NameKind -> ShowS
Show, forall x. Rep NameKind x -> NameKind
forall x. NameKind -> Rep NameKind x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NameKind x -> NameKind
$cfrom :: forall x. NameKind -> Rep NameKind x
Generic)
data OtherAspect
= Error
| ErrorWarning
| DottedPattern
| UnsolvedMeta
| UnsolvedConstraint
| TerminationProblem
| PositivityProblem
| Deadcode
| ShadowingInTelescope
| CoverageProblem
| IncompletePattern
| TypeChecks
| MissingDefinition
| CatchallClause
| ConfluenceProblem
deriving (OtherAspect -> OtherAspect -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OtherAspect -> OtherAspect -> Bool
$c/= :: OtherAspect -> OtherAspect -> Bool
== :: OtherAspect -> OtherAspect -> Bool
$c== :: OtherAspect -> OtherAspect -> Bool
Eq, Eq OtherAspect
OtherAspect -> OtherAspect -> Bool
OtherAspect -> OtherAspect -> Ordering
OtherAspect -> OtherAspect -> OtherAspect
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: OtherAspect -> OtherAspect -> OtherAspect
$cmin :: OtherAspect -> OtherAspect -> OtherAspect
max :: OtherAspect -> OtherAspect -> OtherAspect
$cmax :: OtherAspect -> OtherAspect -> OtherAspect
>= :: OtherAspect -> OtherAspect -> Bool
$c>= :: OtherAspect -> OtherAspect -> Bool
> :: OtherAspect -> OtherAspect -> Bool
$c> :: OtherAspect -> OtherAspect -> Bool
<= :: OtherAspect -> OtherAspect -> Bool
$c<= :: OtherAspect -> OtherAspect -> Bool
< :: OtherAspect -> OtherAspect -> Bool
$c< :: OtherAspect -> OtherAspect -> Bool
compare :: OtherAspect -> OtherAspect -> Ordering
$ccompare :: OtherAspect -> OtherAspect -> Ordering
Ord, Int -> OtherAspect -> ShowS
[OtherAspect] -> ShowS
OtherAspect -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OtherAspect] -> ShowS
$cshowList :: [OtherAspect] -> ShowS
show :: OtherAspect -> String
$cshow :: OtherAspect -> String
showsPrec :: Int -> OtherAspect -> ShowS
$cshowsPrec :: Int -> OtherAspect -> ShowS
Show, Int -> OtherAspect
OtherAspect -> Int
OtherAspect -> [OtherAspect]
OtherAspect -> OtherAspect
OtherAspect -> OtherAspect -> [OtherAspect]
OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect]
$cenumFromThenTo :: OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect]
enumFromTo :: OtherAspect -> OtherAspect -> [OtherAspect]
$cenumFromTo :: OtherAspect -> OtherAspect -> [OtherAspect]
enumFromThen :: OtherAspect -> OtherAspect -> [OtherAspect]
$cenumFromThen :: OtherAspect -> OtherAspect -> [OtherAspect]
enumFrom :: OtherAspect -> [OtherAspect]
$cenumFrom :: OtherAspect -> [OtherAspect]
fromEnum :: OtherAspect -> Int
$cfromEnum :: OtherAspect -> Int
toEnum :: Int -> OtherAspect
$ctoEnum :: Int -> OtherAspect
pred :: OtherAspect -> OtherAspect
$cpred :: OtherAspect -> OtherAspect
succ :: OtherAspect -> OtherAspect
$csucc :: OtherAspect -> OtherAspect
Enum, OtherAspect
forall a. a -> a -> Bounded a
maxBound :: OtherAspect
$cmaxBound :: OtherAspect
minBound :: OtherAspect
$cminBound :: OtherAspect
Bounded, forall x. Rep OtherAspect x -> OtherAspect
forall x. OtherAspect -> Rep OtherAspect x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep OtherAspect x -> OtherAspect
$cfrom :: forall x. OtherAspect -> Rep OtherAspect x
Generic)
instance Semigroup NameKind where
NameKind
Field <> :: NameKind -> NameKind -> NameKind
<> NameKind
Bound = NameKind
Field
NameKind
Bound <> NameKind
Field = NameKind
Field
NameKind
k1 <> NameKind
k2 | NameKind
k1 forall a. Eq a => a -> a -> Bool
== NameKind
k2 = NameKind
k1
| Bool
otherwise = NameKind
k1
instance Semigroup Aspect where
Name Maybe NameKind
mk1 Bool
op1 <> :: Aspect -> Aspect -> Aspect
<> Name Maybe NameKind
mk2 Bool
op2 = Maybe NameKind -> Bool -> Aspect
Name (forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionMaybeWith forall a. Semigroup a => a -> a -> a
(<>) Maybe NameKind
mk1 Maybe NameKind
mk2) Bool
op1
Aspect
a1 <> Aspect
a2 | Aspect
a1 forall a. Eq a => a -> a -> Bool
== Aspect
a2 = Aspect
a1
| Bool
otherwise = Aspect
a1
data Aspects = Aspects
{ Aspects -> Maybe Aspect
aspect :: Maybe Aspect
, Aspects -> Set OtherAspect
otherAspects :: Set OtherAspect
, Aspects -> String
note :: String
, Aspects -> Maybe DefinitionSite
definitionSite :: Maybe DefinitionSite
, Aspects -> TokenBased
tokenBased :: !TokenBased
}
deriving (Int -> Aspects -> ShowS
[Aspects] -> ShowS
Aspects -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Aspects] -> ShowS
$cshowList :: [Aspects] -> ShowS
show :: Aspects -> String
$cshow :: Aspects -> String
showsPrec :: Int -> Aspects -> ShowS
$cshowsPrec :: Int -> Aspects -> ShowS
Show, forall x. Rep Aspects x -> Aspects
forall x. Aspects -> Rep Aspects x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Aspects x -> Aspects
$cfrom :: forall x. Aspects -> Rep Aspects x
Generic)
data DefinitionSite = DefinitionSite
{ DefinitionSite -> TopLevelModuleName' Range
defSiteModule :: (TopLevelModuleName' Range)
, DefinitionSite -> Int
defSitePos :: Int
, DefinitionSite -> Bool
defSiteHere :: Bool
, DefinitionSite -> Maybe String
defSiteAnchor :: Maybe String
}
deriving (Int -> DefinitionSite -> ShowS
[DefinitionSite] -> ShowS
DefinitionSite -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DefinitionSite] -> ShowS
$cshowList :: [DefinitionSite] -> ShowS
show :: DefinitionSite -> String
$cshow :: DefinitionSite -> String
showsPrec :: Int -> DefinitionSite -> ShowS
$cshowsPrec :: Int -> DefinitionSite -> ShowS
Show, forall x. Rep DefinitionSite x -> DefinitionSite
forall x. DefinitionSite -> Rep DefinitionSite x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DefinitionSite x -> DefinitionSite
$cfrom :: forall x. DefinitionSite -> Rep DefinitionSite x
Generic)
instance Eq DefinitionSite where
DefinitionSite TopLevelModuleName' Range
m Int
p Bool
_ Maybe String
_ == :: DefinitionSite -> DefinitionSite -> Bool
== DefinitionSite TopLevelModuleName' Range
m' Int
p' Bool
_ Maybe String
_ = TopLevelModuleName' Range
m forall a. Eq a => a -> a -> Bool
== TopLevelModuleName' Range
m' Bool -> Bool -> Bool
&& Int
p forall a. Eq a => a -> a -> Bool
== Int
p'
data TokenBased = TokenBased | NotOnlyTokenBased
deriving (TokenBased -> TokenBased -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TokenBased -> TokenBased -> Bool
$c/= :: TokenBased -> TokenBased -> Bool
== :: TokenBased -> TokenBased -> Bool
$c== :: TokenBased -> TokenBased -> Bool
Eq, Int -> TokenBased -> ShowS
[TokenBased] -> ShowS
TokenBased -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TokenBased] -> ShowS
$cshowList :: [TokenBased] -> ShowS
show :: TokenBased -> String
$cshow :: TokenBased -> String
showsPrec :: Int -> TokenBased -> ShowS
$cshowsPrec :: Int -> TokenBased -> ShowS
Show)
instance Eq Aspects where
Aspects Maybe Aspect
a Set OtherAspect
o String
_ Maybe DefinitionSite
d TokenBased
t == :: Aspects -> Aspects -> Bool
== Aspects Maybe Aspect
a' Set OtherAspect
o' String
_ Maybe DefinitionSite
d' TokenBased
t' =
(Maybe Aspect
a, Set OtherAspect
o, Maybe DefinitionSite
d, TokenBased
t) forall a. Eq a => a -> a -> Bool
== (Maybe Aspect
a', Set OtherAspect
o', Maybe DefinitionSite
d', TokenBased
t')
instance NFData Induction where
rnf :: Induction -> ()
rnf Induction
Inductive = ()
rnf Induction
CoInductive = ()
instance NFData NameKind where
rnf :: NameKind -> ()
rnf = \case
NameKind
Bound -> ()
NameKind
Generalizable -> ()
Constructor Induction
c -> forall a. NFData a => a -> ()
rnf Induction
c
NameKind
Datatype -> ()
NameKind
Field -> ()
NameKind
Function -> ()
NameKind
Module -> ()
NameKind
Postulate -> ()
NameKind
Primitive -> ()
NameKind
Record -> ()
NameKind
Argument -> ()
NameKind
Macro -> ()