module Agda.Syntax.Common.Aspect where

import {-# SOURCE #-} Agda.Syntax.TopLevelModuleName
import Agda.Utils.Maybe
import GHC.Generics

import Data.Set (Set)

import Control.DeepSeq

data Induction = Inductive | CoInductive  -- Keep in this order!
  deriving (Induction -> Induction -> Bool
(Induction -> Induction -> Bool)
-> (Induction -> Induction -> Bool) -> Eq Induction
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Induction -> Induction -> Bool
== :: Induction -> Induction -> Bool
$c/= :: Induction -> Induction -> Bool
/= :: Induction -> Induction -> Bool
Eq, Eq Induction
Eq Induction =>
(Induction -> Induction -> Ordering)
-> (Induction -> Induction -> Bool)
-> (Induction -> Induction -> Bool)
-> (Induction -> Induction -> Bool)
-> (Induction -> Induction -> Bool)
-> (Induction -> Induction -> Induction)
-> (Induction -> Induction -> Induction)
-> Ord 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
$ccompare :: Induction -> Induction -> Ordering
compare :: Induction -> Induction -> Ordering
$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
>= :: Induction -> Induction -> Bool
$cmax :: Induction -> Induction -> Induction
max :: Induction -> Induction -> Induction
$cmin :: Induction -> Induction -> Induction
min :: Induction -> Induction -> Induction
Ord, Int -> Induction -> ShowS
[Induction] -> ShowS
Induction -> String
(Int -> Induction -> ShowS)
-> (Induction -> String)
-> ([Induction] -> ShowS)
-> Show Induction
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Induction -> ShowS
showsPrec :: Int -> Induction -> ShowS
$cshow :: Induction -> String
show :: Induction -> String
$cshowList :: [Induction] -> ShowS
showList :: [Induction] -> ShowS
Show)

data Aspect
  = Comment
  | Keyword
  | String
  | Number
  | Hole
  | Symbol                     -- ^ Symbols like forall, =, ->, etc.
  | PrimitiveType              -- ^ Things like Set and Prop.
  | Name (Maybe NameKind) Bool -- ^ Is the name an operator part?
  | Pragma                     -- ^ Text occurring in pragmas that
                               --   does not have a more specific
                               --   aspect.
  | Background                 -- ^ Non-code contents in literate Agda
  | Markup
    -- ^ Delimiters used to separate the Agda code blocks from the
    -- other contents in literate Agda
    deriving (Aspect -> Aspect -> Bool
(Aspect -> Aspect -> Bool)
-> (Aspect -> Aspect -> Bool) -> Eq Aspect
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Aspect -> Aspect -> Bool
== :: Aspect -> Aspect -> Bool
$c/= :: Aspect -> Aspect -> Bool
/= :: Aspect -> Aspect -> Bool
Eq, Int -> Aspect -> ShowS
[Aspect] -> ShowS
Aspect -> String
(Int -> Aspect -> ShowS)
-> (Aspect -> String) -> ([Aspect] -> ShowS) -> Show Aspect
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Aspect -> ShowS
showsPrec :: Int -> Aspect -> ShowS
$cshow :: Aspect -> String
show :: Aspect -> String
$cshowList :: [Aspect] -> ShowS
showList :: [Aspect] -> ShowS
Show, (forall x. Aspect -> Rep Aspect x)
-> (forall x. Rep Aspect x -> Aspect) -> Generic Aspect
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
$cfrom :: forall x. Aspect -> Rep Aspect x
from :: forall x. Aspect -> Rep Aspect x
$cto :: forall x. Rep Aspect x -> Aspect
to :: forall x. Rep Aspect x -> Aspect
Generic)

-- | @NameKind@s are figured out during scope checking.

data NameKind
  = Bound                         -- ^ Bound variable.
  | Generalizable                 -- ^ Generalizable variable.
                                  --   (This includes generalizable
                                  --   variables that have been
                                  --   generalized).
  | Constructor Induction         -- ^ Inductive or coinductive constructor.
  | Datatype
  | Field                         -- ^ Record field.
  | Function
  | Module                        -- ^ Module name.
  | Postulate
  | Primitive                     -- ^ Primitive.
  | Record                        -- ^ Record type.
  | Argument                      -- ^ Named argument, like x in {x = v}
  | Macro                         -- ^ Macro.
    deriving (NameKind -> NameKind -> Bool
(NameKind -> NameKind -> Bool)
-> (NameKind -> NameKind -> Bool) -> Eq NameKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NameKind -> NameKind -> Bool
== :: NameKind -> NameKind -> Bool
$c/= :: NameKind -> NameKind -> Bool
/= :: NameKind -> NameKind -> Bool
Eq, Int -> NameKind -> ShowS
[NameKind] -> ShowS
NameKind -> String
(Int -> NameKind -> ShowS)
-> (NameKind -> String) -> ([NameKind] -> ShowS) -> Show NameKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NameKind -> ShowS
showsPrec :: Int -> NameKind -> ShowS
$cshow :: NameKind -> String
show :: NameKind -> String
$cshowList :: [NameKind] -> ShowS
showList :: [NameKind] -> ShowS
Show, (forall x. NameKind -> Rep NameKind x)
-> (forall x. Rep NameKind x -> NameKind) -> Generic NameKind
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
$cfrom :: forall x. NameKind -> Rep NameKind x
from :: forall x. NameKind -> Rep NameKind x
$cto :: forall x. Rep NameKind x -> NameKind
to :: forall x. Rep NameKind x -> NameKind
Generic)

-- | Other aspects, generated by type checking.
--   (These can overlap with each other and with 'Aspect's.)

data OtherAspect
  = Error
  | ErrorWarning
    -- ^ A warning that is considered fatal in the end.
  | DottedPattern
  | UnsolvedMeta
  | UnsolvedConstraint
    -- ^ Unsolved constraint not connected to meta-variable. This
    -- could for instance be an emptyness constraint.
  | TerminationProblem
  | PositivityProblem
  | Deadcode
    -- ^ Used for highlighting unreachable clauses, unreachable RHS
    -- (because of an absurd pattern), etc.
  | ShadowingInTelescope
    -- ^ Used for shadowed repeated variable names in telescopes.
  | CoverageProblem
  | IncompletePattern
    -- ^ When this constructor is used it is probably a good idea to
    -- include a 'note' explaining why the pattern is incomplete.
  | TypeChecks
    -- ^ Code which is being type-checked.
  | MissingDefinition
    -- ^ Function declaration without matching definition
  -- NB: We put CatchallClause last so that it is overwritten by other,
  -- more important, aspects in the emacs mode.
  | CatchallClause
  | ConfluenceProblem
    deriving (OtherAspect -> OtherAspect -> Bool
(OtherAspect -> OtherAspect -> Bool)
-> (OtherAspect -> OtherAspect -> Bool) -> Eq OtherAspect
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: OtherAspect -> OtherAspect -> Bool
== :: OtherAspect -> OtherAspect -> Bool
$c/= :: OtherAspect -> OtherAspect -> Bool
/= :: OtherAspect -> OtherAspect -> Bool
Eq, Eq OtherAspect
Eq OtherAspect =>
(OtherAspect -> OtherAspect -> Ordering)
-> (OtherAspect -> OtherAspect -> Bool)
-> (OtherAspect -> OtherAspect -> Bool)
-> (OtherAspect -> OtherAspect -> Bool)
-> (OtherAspect -> OtherAspect -> Bool)
-> (OtherAspect -> OtherAspect -> OtherAspect)
-> (OtherAspect -> OtherAspect -> OtherAspect)
-> Ord 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
$ccompare :: OtherAspect -> OtherAspect -> Ordering
compare :: OtherAspect -> OtherAspect -> Ordering
$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
>= :: OtherAspect -> OtherAspect -> Bool
$cmax :: OtherAspect -> OtherAspect -> OtherAspect
max :: OtherAspect -> OtherAspect -> OtherAspect
$cmin :: OtherAspect -> OtherAspect -> OtherAspect
min :: OtherAspect -> OtherAspect -> OtherAspect
Ord, Int -> OtherAspect -> ShowS
[OtherAspect] -> ShowS
OtherAspect -> String
(Int -> OtherAspect -> ShowS)
-> (OtherAspect -> String)
-> ([OtherAspect] -> ShowS)
-> Show OtherAspect
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> OtherAspect -> ShowS
showsPrec :: Int -> OtherAspect -> ShowS
$cshow :: OtherAspect -> String
show :: OtherAspect -> String
$cshowList :: [OtherAspect] -> ShowS
showList :: [OtherAspect] -> ShowS
Show, Int -> OtherAspect
OtherAspect -> Int
OtherAspect -> [OtherAspect]
OtherAspect -> OtherAspect
OtherAspect -> OtherAspect -> [OtherAspect]
OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect]
(OtherAspect -> OtherAspect)
-> (OtherAspect -> OtherAspect)
-> (Int -> OtherAspect)
-> (OtherAspect -> Int)
-> (OtherAspect -> [OtherAspect])
-> (OtherAspect -> OtherAspect -> [OtherAspect])
-> (OtherAspect -> OtherAspect -> [OtherAspect])
-> (OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect])
-> Enum 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
$csucc :: OtherAspect -> OtherAspect
succ :: OtherAspect -> OtherAspect
$cpred :: OtherAspect -> OtherAspect
pred :: OtherAspect -> OtherAspect
$ctoEnum :: Int -> OtherAspect
toEnum :: Int -> OtherAspect
$cfromEnum :: OtherAspect -> Int
fromEnum :: OtherAspect -> Int
$cenumFrom :: OtherAspect -> [OtherAspect]
enumFrom :: OtherAspect -> [OtherAspect]
$cenumFromThen :: OtherAspect -> OtherAspect -> [OtherAspect]
enumFromThen :: OtherAspect -> OtherAspect -> [OtherAspect]
$cenumFromTo :: OtherAspect -> OtherAspect -> [OtherAspect]
enumFromTo :: OtherAspect -> OtherAspect -> [OtherAspect]
$cenumFromThenTo :: OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect]
enumFromThenTo :: OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect]
Enum, OtherAspect
OtherAspect -> OtherAspect -> Bounded OtherAspect
forall a. a -> a -> Bounded a
$cminBound :: OtherAspect
minBound :: OtherAspect
$cmaxBound :: OtherAspect
maxBound :: OtherAspect
Bounded, (forall x. OtherAspect -> Rep OtherAspect x)
-> (forall x. Rep OtherAspect x -> OtherAspect)
-> Generic OtherAspect
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
$cfrom :: forall x. OtherAspect -> Rep OtherAspect x
from :: forall x. OtherAspect -> Rep OtherAspect x
$cto :: forall x. Rep OtherAspect x -> OtherAspect
to :: forall x. Rep OtherAspect x -> OtherAspect
Generic)

-- | Some 'NameKind's are more informative than others.
instance Semigroup NameKind where
  -- During scope-checking of record, we build a constructor
  -- whose arguments (@Bound@ variables) are the fields.
  -- Later, we process them as @Field@s proper.
  NameKind
Field    <> :: NameKind -> NameKind -> NameKind
<> NameKind
Bound    = NameKind
Field
  NameKind
Bound    <> NameKind
Field    = NameKind
Field
  -- -- Projections are special functions.
  -- -- TODO necessary?
  -- Field    <> Function = Field
  -- Function <> Field    = Field
  -- TODO: more overwrites?
  NameKind
k1 <> NameKind
k2 | NameKind
k1 NameKind -> NameKind -> Bool
forall a. Eq a => a -> a -> Bool
== NameKind
k2  = NameKind
k1
           | Bool
otherwise = NameKind
k1 -- TODO: __IMPOSSIBLE__

-- | @NameKind@ in @Name@ can get more precise.
instance Semigroup Aspect where
  Name Maybe NameKind
mk1 Bool
op1 <> :: Aspect -> Aspect -> Aspect
<> Name Maybe NameKind
mk2 Bool
op2 = Maybe NameKind -> Bool -> Aspect
Name ((NameKind -> NameKind -> NameKind)
-> Maybe NameKind -> Maybe NameKind -> Maybe NameKind
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionMaybeWith NameKind -> NameKind -> NameKind
forall a. Semigroup a => a -> a -> a
(<>) Maybe NameKind
mk1 Maybe NameKind
mk2) Bool
op1
    -- (op1 || op2) breaks associativity
  Aspect
a1 <> Aspect
a2 | Aspect
a1 Aspect -> Aspect -> Bool
forall a. Eq a => a -> a -> Bool
== Aspect
a2  = Aspect
a1
           | Bool
otherwise = Aspect
a1 -- TODO: __IMPOSSIBLE__

------------------------------------------------------------------------
-- Highlighting information

-- | Syntactic aspects of the code. (These cannot overlap.)

-- | Meta information which can be associated with a
-- character\/character range.

data Aspects = Aspects
  { Aspects -> Maybe Aspect
aspect       :: Maybe Aspect
  , Aspects -> Set OtherAspect
otherAspects :: Set OtherAspect
  , Aspects -> String
note         :: String
    -- ^ This note, if not null, can be displayed as a tool-tip or
    -- something like that. It should contain useful information about
    -- the range (like the module containing a certain identifier, or
    -- the fixity of an operator).
  , Aspects -> Maybe DefinitionSite
definitionSite :: Maybe DefinitionSite
    -- ^ The definition site of the annotated thing, if applicable and
    --   known.
  , Aspects -> TokenBased
tokenBased :: !TokenBased
    -- ^ Is this entry token-based?
  }
  deriving (Int -> Aspects -> ShowS
[Aspects] -> ShowS
Aspects -> String
(Int -> Aspects -> ShowS)
-> (Aspects -> String) -> ([Aspects] -> ShowS) -> Show Aspects
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Aspects -> ShowS
showsPrec :: Int -> Aspects -> ShowS
$cshow :: Aspects -> String
show :: Aspects -> String
$cshowList :: [Aspects] -> ShowS
showList :: [Aspects] -> ShowS
Show, (forall x. Aspects -> Rep Aspects x)
-> (forall x. Rep Aspects x -> Aspects) -> Generic Aspects
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
$cfrom :: forall x. Aspects -> Rep Aspects x
from :: forall x. Aspects -> Rep Aspects x
$cto :: forall x. Rep Aspects x -> Aspects
to :: forall x. Rep Aspects x -> Aspects
Generic)

data DefinitionSite = DefinitionSite
  { DefinitionSite -> TopLevelModuleName
defSiteModule :: TopLevelModuleName
      -- ^ The defining module.
  , DefinitionSite -> Int
defSitePos    :: Int
      -- ^ The file position in that module. File positions are
      -- counted from 1.
  , DefinitionSite -> Bool
defSiteHere   :: Bool
      -- ^ Has this @DefinitionSite@ been created at the defining site of the name?
  , DefinitionSite -> Maybe String
defSiteAnchor :: Maybe String
      -- ^ A pretty name for the HTML linking.
  }
  deriving (Int -> DefinitionSite -> ShowS
[DefinitionSite] -> ShowS
DefinitionSite -> String
(Int -> DefinitionSite -> ShowS)
-> (DefinitionSite -> String)
-> ([DefinitionSite] -> ShowS)
-> Show DefinitionSite
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DefinitionSite -> ShowS
showsPrec :: Int -> DefinitionSite -> ShowS
$cshow :: DefinitionSite -> String
show :: DefinitionSite -> String
$cshowList :: [DefinitionSite] -> ShowS
showList :: [DefinitionSite] -> ShowS
Show, (forall x. DefinitionSite -> Rep DefinitionSite x)
-> (forall x. Rep DefinitionSite x -> DefinitionSite)
-> Generic DefinitionSite
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
$cfrom :: forall x. DefinitionSite -> Rep DefinitionSite x
from :: forall x. DefinitionSite -> Rep DefinitionSite x
$cto :: forall x. Rep DefinitionSite x -> DefinitionSite
to :: forall x. Rep DefinitionSite x -> DefinitionSite
Generic)

instance Eq DefinitionSite where
  DefinitionSite TopLevelModuleName
m Int
p Bool
_ Maybe String
_ == :: DefinitionSite -> DefinitionSite -> Bool
== DefinitionSite TopLevelModuleName
m' Int
p' Bool
_ Maybe String
_ = TopLevelModuleName
m TopLevelModuleName -> TopLevelModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== TopLevelModuleName
m' Bool -> Bool -> Bool
&& Int
p Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
p'

-- | Is the highlighting \"token-based\", i.e. based only on
-- information from the lexer?

data TokenBased = TokenBased | NotOnlyTokenBased
  deriving (TokenBased -> TokenBased -> Bool
(TokenBased -> TokenBased -> Bool)
-> (TokenBased -> TokenBased -> Bool) -> Eq TokenBased
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TokenBased -> TokenBased -> Bool
== :: TokenBased -> TokenBased -> Bool
$c/= :: TokenBased -> TokenBased -> Bool
/= :: TokenBased -> TokenBased -> Bool
Eq, Int -> TokenBased -> ShowS
[TokenBased] -> ShowS
TokenBased -> String
(Int -> TokenBased -> ShowS)
-> (TokenBased -> String)
-> ([TokenBased] -> ShowS)
-> Show TokenBased
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TokenBased -> ShowS
showsPrec :: Int -> TokenBased -> ShowS
$cshow :: TokenBased -> String
show :: TokenBased -> String
$cshowList :: [TokenBased] -> ShowS
showList :: [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) (Maybe Aspect, Set OtherAspect, Maybe DefinitionSite, TokenBased)
-> (Maybe Aspect, Set OtherAspect, Maybe DefinitionSite,
    TokenBased)
-> Bool
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 -> Induction -> ()
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         -> ()