content: module Agda.Syntax.Common.Aspect where
  
  import Prelude hiding (null)
  
  import GHC.Generics ( Generic )
  import Control.DeepSeq ( NFData(..) )
  import Data.Set (Set)
  import Data.Text (Text)
  
  import Agda.Syntax.TopLevelModuleName.Boot (TopLevelModuleName')
  import Agda.Syntax.Position (Range, rangeModule, rStart, Position'(posPos), HasRange(..))
  import Agda.Utils.Maybe ( unionMaybeWith )
  import Agda.Utils.Null ( Null(..) )
  
  data Induction = Inductive | CoInductive  -- Keep in this order!
    deriving (Eq, Ord, Generic, Show)
  
  data Aspect
    = Comment
    | Keyword
    | String
    | Number
    | Hole
    | Symbol
        -- ^ Symbols like @forall@, @=@, @->@, etc.
    | PrimitiveType
        -- ^ Things like @Set@ and @Prop@.
    | Name (Maybe NameKind) Bool
        -- ^ '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.
    | URL Text
        -- ^ Uniform Resource Locator aka clickable link.
    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.
    | InstanceProblem
        -- ^ Unusable instance etc.
  
    -- NB: We put CatchallClause and CosmeticProblem last
    -- so that they are overwritten by other,
    -- more important, aspects in the emacs mode.
    | CosmeticProblem
        -- ^ Nothing serious, just a beauty flaw.
    | 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, Generic, Show)
  
  instance Null TokenBased where
    empty = TokenBased
  
  instance Null Aspects where
    empty = Aspects Nothing mempty "" Nothing TokenBased
    null (Aspects a o s d t) = null a && null o && null s && null d && null t
  
  instance Eq Aspects where
    Aspects a o _ d t == Aspects a' o' _ d' t' =
      (a, o, d, t) == (a', o', d', t')
  
  -- | Compute the 'Aspects' which (possibly) contain a 'DefinitionSite'
  -- for the given thing-with-range.
  rangeDefinitionSite :: HasRange a => a -> Aspects
  rangeDefinitionSite thing = do
    let
      r = getRange thing
  
      defs :: Maybe DefinitionSite
      defs = do
        mod <- rangeModule r
        pos <- posPos <$> rStart r
        pure DefinitionSite
          { defSiteModule = mod
          , defSitePos    = fromIntegral pos
          , defSiteHere   = False
          , defSiteAnchor = Nothing
          }
    empty{ definitionSite = defs }
  
  ------------------------------------------------------------------------
  -- NFData instances
  
  instance NFData DefinitionSite
  instance NFData OtherAspect
  instance NFData TokenBased
  instance NFData Induction
  instance NFData NameKind
  instance NFData Aspects
  instance NFData Aspect
  