Aspect.hs

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
  | 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