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  -- Keep in this order!
  deriving (Eq, Ord, 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 (Eq, Show, 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 (Eq, Show, 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 (Eq, Ord, Show, Enum, Bounded, 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.
  Field    <> Bound    = Field
  Bound    <> Field    = Field
  -- -- Projections are special functions.
  -- -- TODO necessary?
  -- Field    <> Function = Field
  -- Function <> Field    = Field
  -- TODO: more overwrites?
  k1 <> k2 | k1 == k2  = k1
           | otherwise = k1 -- TODO: __IMPOSSIBLE__

-- | @NameKind@ in @Name@ can get more precise.
instance Semigroup Aspect where
  Name mk1 op1 <> Name mk2 op2 = Name (unionMaybeWith (<>) mk1 mk2) op1
    -- (op1 || op2) breaks associativity
  a1 <> a2 | a1 == a2  = a1
           | otherwise = 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
  { aspect       :: Maybe Aspect
  , otherAspects :: Set OtherAspect
  , 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).
  , definitionSite :: Maybe DefinitionSite
    -- ^ The definition site of the annotated thing, if applicable and
    --   known.
  , tokenBased :: !TokenBased
    -- ^ Is this entry token-based?
  }
  deriving (Show, Generic)

data DefinitionSite = DefinitionSite
  { defSiteModule :: (TopLevelModuleName' Range)
      -- ^ The defining module.
  , defSitePos    :: Int
      -- ^ The file position in that module. File positions are
      -- counted from 1.
  , defSiteHere   :: Bool
      -- ^ Has this @DefinitionSite@ been created at the defining site of the name?
  , defSiteAnchor :: Maybe String
      -- ^ A pretty name for the HTML linking.
  }
  deriving (Show, Generic)

instance Eq DefinitionSite where
  DefinitionSite m p _ _ == DefinitionSite m' p' _ _ = m == m' && p == p'

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

data TokenBased = TokenBased | NotOnlyTokenBased
  deriving (Eq, Show)

instance Eq Aspects where
  Aspects a o _ d t == Aspects a' o' _ d' t' =
    (a, o, d, t) == (a', o', d', t')

instance NFData Induction where
  rnf Inductive   = ()
  rnf CoInductive = ()

instance NFData NameKind where
  rnf = \case
    Bound         -> ()
    Generalizable -> ()
    Constructor c -> rnf c
    Datatype      -> ()
    Field         -> ()
    Function      -> ()
    Module        -> ()
    Postulate     -> ()
    Primitive     -> ()
    Record        -> ()
    Argument      -> ()
    Macro         -> ()