-- | Generates data used for precise syntax highlighting.

-- {-# OPTIONS_GHC -fwarn-unused-imports #-}  -- Semigroup import obsolete in later ghcs
-- {-# OPTIONS_GHC -fwarn-unused-binds   #-}

module Mikan.Interaction.Highlighting.Generate
  ( Level(..)
  , generateAndPrintSyntaxInfo
  , generateTokenInfo, generateTokenInfoFromSource
  , generateTokenInfoFromString
  , printSyntaxInfo
  , printErrorInfo, errorHighlighting
  , printUnsolvedInfo
  , printHighlightingInfo
  , highlightAsTypeChecked
  , highlightWarning, warningHighlighting
  , computeUnsolvedInfo
  , storeDisambiguatedConstructor, storeDisambiguatedProjection
  , disambiguateRecordFields
  ) where

import Prelude hiding (null)

import Control.Monad

import Data.Foldable qualified as Fold
import Data.Map qualified as Map
import Data.Maybe
import Data.List ((\\))
import Data.List qualified as List
import Data.IntMap qualified as IntMap
import Data.HashMap.Strict (HashMap)
import Data.HashMap.Strict qualified as HMap
import Data.Semigroup (sconcat)
import Data.Sequence (Seq)
import Data.Set qualified as Set
import Data.Text (Text)
import Data.Text qualified as Text

import Mikan.Interaction.Response
  ( RemoveTokenBasedHighlighting( KeepHighlighting ) )
import Mikan.Interaction.Highlighting.Precise as H
import Mikan.Interaction.Highlighting.Range
  (rToR, rangeToRange, overlappings, Ranges)
import Mikan.Interaction.Highlighting.FromAbstract
import Mikan.Interaction.Options.Types (optMdOnlyAgdaBlocks)
import Mikan.Interaction.ReadFile

import Mikan.TypeChecking.Errors qualified as TCM
import Mikan.TypeChecking.MetaVars (isBlockedTerm, hasTwinMeta)
import Mikan.TypeChecking.Monad hiding
  (ModuleInfo, MetaInfo, Primitive, Constructor, Record, Function, Datatype)
import Mikan.TypeChecking.Monad qualified as TCM
import Mikan.TypeChecking.Monad.Base.Warning qualified as W
import Mikan.TypeChecking.Monad.Diagnostic
import Mikan.Syntax.Scope.Errors
import Mikan.TypeChecking.Pretty qualified as TCM
import Mikan.TypeChecking.Positivity.Occurrence (Occurrence(..))
import Mikan.TypeChecking.Positivity.Warnings
import Mikan.TypeChecking.Warnings ( raiseWarningsOnUsage )
import Mikan.TypeChecking.Errors.Deferred

import Mikan.Syntax.Abstract qualified as A
import Mikan.Syntax.Abstract.Name (nameBindingSite)
import Mikan.Syntax.Concrete.Definitions as W ( DeclarationWarning(..), DeclarationWarning'(..) )
import Mikan.Syntax.Common (Induction(..), pattern Ranged)
import Mikan.Syntax.Common.Aspect qualified as Aspect
import Mikan.Syntax.Concrete.Name qualified as C
import Mikan.Syntax.Internal qualified as I
import Mikan.Syntax.Literal qualified as L
import Mikan.Syntax.Parser qualified as Pa
import Mikan.Syntax.Parser.Tokens qualified as T
import Mikan.Syntax.Position qualified as P
import Mikan.Syntax.Position
  (RangeFile, Range, HasRange, getRange, noRange)
import Mikan.Syntax.TopLevelModuleName

import Mikan.Syntax.Scope.Base ( WithKind(..) )
import Mikan.Syntax.Abstract.Views ( KName, declaredNames )

import Mikan.Utils.FileName
import Mikan.Utils.List ( caseList, last1 )
import Mikan.Utils.List1 ( List1 )
import Mikan.Utils.List1 qualified as List1
import Mikan.Utils.List2 ( List2 )
import Mikan.Utils.List2 qualified as List2
import Mikan.Utils.Maybe
import Mikan.Utils.Maybe.Strict qualified as Strict
import Mikan.Utils.Null
import Mikan.Syntax.Common.Pretty
import Mikan.Utils.Singleton

import Mikan.Utils.Impossible

-- | Highlighting levels.

data Level
  = Full
    -- ^ Full highlighting. Should only be used after typechecking has
    --   completed successfully.
  | Partial
    -- ^ Highlighting without disambiguation of overloaded
    --   constructors.

-- | Highlight a warning.
--   We do not generate highlighting for unsolved metas and
--   constraints, as that gets handled in bulk after typechecking.
highlightWarning :: TCWarning -> TCM ()
highlightWarning :: TCWarning -> TCM ()
highlightWarning TCWarning
tcwarn = do
  let h :: HighlightingInfo
h = HighlightingInfoBuilder -> HighlightingInfo
forall a b. Convert a b => a -> b
convert (HighlightingInfoBuilder -> HighlightingInfo)
-> HighlightingInfoBuilder -> HighlightingInfo
forall a b. (a -> b) -> a -> b
$ Bool -> TCWarning -> HighlightingInfoBuilder
warningHighlighting' Bool
False TCWarning
tcwarn
  -- Highlighting for warnings coming from the Happy parser is placed
  -- together with token highlighting.
  case SomeDiagnostic -> Maybe Warning
forall a. Diagnostic a => SomeDiagnostic -> Maybe a
fromSomeDiagnostic (TCWarning -> SomeDiagnostic
forall diag. TCWarning' diag -> diag
tcWarning TCWarning
tcwarn) of
    Just ParseWarning{} -> ASetter' TCState HighlightingInfo
-> (HighlightingInfo -> HighlightingInfo) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ASetter' TCState HighlightingInfo
Lens' TCState HighlightingInfo
stTokens     (HighlightingInfo
h HighlightingInfo -> HighlightingInfo -> HighlightingInfo
forall a. Semigroup a => a -> a -> a
<>)
    Maybe Warning
_                   -> ASetter' TCState HighlightingInfo
-> (HighlightingInfo -> HighlightingInfo) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ASetter' TCState HighlightingInfo
Lens' TCState HighlightingInfo
stSyntaxInfo (HighlightingInfo
h HighlightingInfo -> HighlightingInfo -> HighlightingInfo
forall a. Semigroup a => a -> a -> a
<>)
  HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCEnv tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting HighlightingInfo
h

-- | Generate syntax highlighting information for the given
-- declaration, and (if appropriate) print it. If the boolean is
-- 'True', then the state is additionally updated with the new
-- highlighting info (in case of a conflict new info takes precedence
-- over old info).
--
-- The procedure makes use of some of the highlighting info
-- corresponding to 'stTokens' (that corresponding to the interval
-- covered by the declaration). If the boolean is 'True', then this
-- highlighting info is additionally removed from the data structure
-- that 'stTokens' refers to.

generateAndPrintSyntaxInfo
  :: A.Declaration
       -- ^ Declaration to highlight.
  -> Level
       -- ^ Amount of highlighting.
  -> Bool
       -- ^ Update the state?
  -> TCM ()
generateAndPrintSyntaxInfo :: Declaration -> Level -> Bool -> TCM ()
generateAndPrintSyntaxInfo Declaration
decl Level
_ Bool
_ | Range -> Bool
forall a. Null a => a -> Bool
null (Range -> Bool) -> Range -> Bool
forall a b. (a -> b) -> a -> b
$ Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
decl = () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
generateAndPrintSyntaxInfo Declaration
decl Level
hlLevel Bool
updateState = do
  top <- TopLevelModuleName
-> Maybe TopLevelModuleName -> TopLevelModuleName
forall a. a -> Maybe a -> a
fromMaybe TopLevelModuleName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe TopLevelModuleName -> TopLevelModuleName)
-> TCMT IO (Maybe TopLevelModuleName) -> TCMT IO TopLevelModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe TopLevelModuleName)
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
m (Maybe TopLevelModuleName)
currentTopLevelModule

  reportSDoc "import.iface.create" 15 $
    TCM.fwords
      ("Generating syntax info for the following declaration " ++
       case hlLevel of
         Full   {} -> [Char]
"(final):"
         Partial{} -> [Char]
"(first approximation):")
      TCM.$$
    TCM.prettyA decl

  ignoreAbstractMode $ do
    kinds <- nameKinds hlLevel decl

    -- After the code has been type checked more information may be
    -- available for overloaded constructors, and
    -- @generateConstructorInfo@ takes advantage of this information.
    -- Note, however, that highlighting for overloaded constructors is
    -- included also in @nameInfo@.
    constructorInfo <- case hlLevel of
      Full{} -> TopLevelModuleName
-> NameKinds -> Declaration -> TCM HighlightingInfoBuilder
generateConstructorInfo TopLevelModuleName
top NameKinds
kinds Declaration
decl
      Level
_      -> HighlightingInfoBuilder -> TCM HighlightingInfoBuilder
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return HighlightingInfoBuilder
forall a. Monoid a => a
mempty

    -- Main source of scope-checker generated highlighting:
    let nameInfo = TopLevelModuleName
-> NameKinds -> Declaration -> HighlightingInfoBuilder
forall a.
Hilite a =>
TopLevelModuleName -> NameKinds -> a -> HighlightingInfoBuilder
runHighlighter TopLevelModuleName
top NameKinds
kinds Declaration
decl

    reportSDoc "highlighting.warning" 60 $ TCM.hcat
      [ "current path = "
      , Strict.maybe "(nothing)" (return . pretty) =<< do
          P.rangeFile <$> viewTC eRange
      ]

    -- Highlighting from the lexer and Happy parser:
    (curTokens, otherTokens) <-
      insideAndOutside (rangeToRange (getRange decl)) <$> useTC stTokens

    -- @constructorInfo@ needs
    -- to be placed before @nameInfo@ since, when typechecking is done,
    -- constructors are included in both lists. Finally the token
    -- information is placed last since token highlighting is more
    -- crude than the others.
    let syntaxInfo = HighlightingInfoBuilder -> HighlightingInfo
forall a b. Convert a b => a -> b
convert (HighlightingInfoBuilder
constructorInfo HighlightingInfoBuilder
-> HighlightingInfoBuilder -> HighlightingInfoBuilder
forall a. Semigroup a => a -> a -> a
<> HighlightingInfoBuilder
nameInfo)
                       HighlightingInfo -> HighlightingInfo -> HighlightingInfo
forall a. Semigroup a => a -> a -> a
<>
                     HighlightingInfo
curTokens

    when updateState $ do
      stSyntaxInfo `modifyingTC` mappend syntaxInfo
      stTokens     `setTCLens`   otherTokens

    ifTopLevelAndHighlightingLevelIs NonInteractive $
      printHighlightingInfo KeepHighlighting syntaxInfo

-- | Generate and return the syntax highlighting information for the
-- tokens in the given file.

generateTokenInfo :: AbsolutePath -> TCM HighlightingInfo
generateTokenInfo :: AbsolutePath -> TCMT IO HighlightingInfo
generateTokenInfo AbsolutePath
file = RangeFile -> Text -> TCMT IO HighlightingInfo
generateTokenInfoFromSource RangeFile
rf (Text -> TCMT IO HighlightingInfo)
-> (ReadFile -> Text) -> ReadFile -> TCMT IO HighlightingInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReadFile -> Text
readFileText (ReadFile -> TCMT IO HighlightingInfo)
-> TCMT IO ReadFile -> TCMT IO HighlightingInfo
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AbsolutePath -> TCMT IO ReadFile
readFileTCM AbsolutePath
file
  -- Note the use of Nothing here. The file might not even parse, but
  -- it should still be possible to obtain token-based highlighting
  -- information. The top-level module names seem to be *mostly*
  -- unused, but one cannot use __IMPOSSIBLE__ instead of Nothing,
  -- because the top-level module names are used by interleaveRanges,
  -- which is used by parseLiterateWithComments, which is used by
  -- generateTokenInfoFromSource.
  where rf :: RangeFile
rf = AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
P.mkRangeFile AbsolutePath
file Maybe TopLevelModuleName
forall a. Maybe a
Nothing

-- | Generate and return the syntax highlighting information for the
-- tokens in the given file.

generateTokenInfoFromSource
  :: RangeFile
     -- ^ The module to highlight.
  -> Text
     -- ^ The file contents. Note that the file is /not/ read from
     -- disk.
  -> TCM HighlightingInfo
generateTokenInfoFromSource :: RangeFile -> Text -> TCMT IO HighlightingInfo
generateTokenInfoFromSource RangeFile
file Text
input = do
  mdOnlyAgdaBlocks <- CommandLineOptions -> Bool
optMdOnlyAgdaBlocks (CommandLineOptions -> Bool)
-> TCMT IO CommandLineOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  runPM $ tokenHighlighting . fst . fst <$>
          Pa.parseFile mdOnlyAgdaBlocks Pa.tokensParser file input

-- | Generate and return the syntax highlighting information for the
-- tokens in the given string, which is assumed to correspond to the
-- given range.

generateTokenInfoFromString :: Range -> Text -> TCM HighlightingInfo
generateTokenInfoFromString :: Range -> Text -> TCMT IO HighlightingInfo
generateTokenInfoFromString Range
r Text
_ | Range
r Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Range
forall a. Range' a
noRange = HighlightingInfo -> TCMT IO HighlightingInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return HighlightingInfo
forall a. Monoid a => a
mempty
generateTokenInfoFromString Range
r Text
s = do
  PM HighlightingInfo -> TCMT IO HighlightingInfo
forall a. PM a -> TCM a
runPM (PM HighlightingInfo -> TCMT IO HighlightingInfo)
-> PM HighlightingInfo -> TCMT IO HighlightingInfo
forall a b. (a -> b) -> a -> b
$ [Token] -> HighlightingInfo
tokenHighlighting ([Token] -> HighlightingInfo)
-> (([Token], Attributes) -> [Token])
-> ([Token], Attributes)
-> HighlightingInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Token], Attributes) -> [Token]
forall a b. (a, b) -> a
fst (([Token], Attributes) -> HighlightingInfo)
-> PM ([Token], Attributes) -> PM HighlightingInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          Parser [Token] -> Position -> Text -> PM ([Token], Attributes)
forall a. Parser a -> Position -> Text -> PM (a, Attributes)
Pa.parsePosString Parser [Token]
Pa.tokensParser Position
p Text
s
  where
    Just Position
p = Range -> Maybe Position
forall a. Range' a -> Maybe (Position' a)
P.rStart Range
r

-- | Compute syntax highlighting for the given tokens.
tokenHighlighting :: [T.Token] -> HighlightingInfo
tokenHighlighting :: [Token] -> HighlightingInfo
tokenHighlighting = HighlightingInfoBuilder -> HighlightingInfo
forall a b. Convert a b => a -> b
convert (HighlightingInfoBuilder -> HighlightingInfo)
-> ([Token] -> HighlightingInfoBuilder)
-> [Token]
-> HighlightingInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [HighlightingInfoBuilder] -> HighlightingInfoBuilder
forall a. Monoid a => [a] -> a
mconcat ([HighlightingInfoBuilder] -> HighlightingInfoBuilder)
-> ([Token] -> [HighlightingInfoBuilder])
-> [Token]
-> HighlightingInfoBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Token -> HighlightingInfoBuilder)
-> [Token] -> [HighlightingInfoBuilder]
forall a b. (a -> b) -> [a] -> [b]
map Token -> HighlightingInfoBuilder
tokenToHI
  where
  -- Converts an aspect and a range to a file.
  aToF :: Aspect -> Range -> m
aToF Aspect
a Range
r = Ranges -> Aspects -> m
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR Range
r) (Aspects
forall a. Monoid a => a
mempty { aspect = Just a })

  tokenToHI :: T.Token -> HighlightingInfoBuilder
  tokenToHI :: Token -> HighlightingInfoBuilder
tokenToHI (T.TokKeyword Keyword
T.KwForall Interval
i)       = Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Symbol (Interval -> Range
forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokKeyword Keyword
_ Interval
i)                = Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Keyword (Interval -> Range
forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokSymbol Symbol
T.SymQuestionMark Interval
i) = Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Hole (Interval -> Range
forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokSymbol  Symbol
_ Interval
i)                = Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Symbol (Interval -> Range
forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokComment (Interval
i, Text
_))             = Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Comment (Interval -> Range
forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokTeX (Interval
i, Text
_))                 = Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Background (Interval -> Range
forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokMarkup (Interval
i, Text
_))              = Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Markup (Interval -> Range
forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokId {})                      = HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  tokenToHI (T.TokQId {})                     = HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  tokenToHI (T.TokString (Interval
i,Text
s))               = Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Pragma (Interval -> Range
forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokDummy {})                   = HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  tokenToHI (T.TokEOF {})                     = HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  tokenToHI (T.TokQual QualifiableToken
cls [(Interval, Text)]
_ Interval
i)         = case QualifiableToken
cls of
    QualifiableToken
T.QualDo           -> Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Keyword (Interval -> Range
forall a. HasRange a => a -> Range
getRange Interval
i)
    T.QualOpenIdiom{}  -> Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Symbol  (Interval -> Range
forall a. HasRange a => a -> Range
getRange Interval
i)
    T.QualEmptyIdiom{} -> Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Symbol  (Interval -> Range
forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokLiteral (Ranged Range
r Literal
l)) = case Literal
l of
    L.LitNat{}    -> Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Number Range
r
    L.LitFloat{}  -> Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Number Range
r
    L.LitString{} -> Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
String Range
r
    L.LitChar{}   -> Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
String Range
r
    L.LitQName{}  -> Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
String Range
r
    L.LitMeta{}   -> Aspect -> Range -> HighlightingInfoBuilder
forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
String Range
r

-- | Builds a 'NameKinds' function.

nameKinds :: Level
             -- ^ This should only be @'Full'@ if
             -- type-checking completed successfully (without any
             -- errors).
          -> A.Declaration
          -> TCM NameKinds
nameKinds :: Level -> Declaration -> TCM NameKinds
nameKinds Level
hlLevel Declaration
decl = do
  imported <- Getter TCState (HashMap QName Definition)
-> TCMT IO (HashMap QName Definition)
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (Getter TCState (HashMap QName Definition)
 -> TCMT IO (HashMap QName Definition))
-> Getter TCState (HashMap QName Definition)
-> TCMT IO (HashMap QName Definition)
forall a b. (a -> b) -> a -> b
$ (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stImports ((Signature -> f Signature) -> TCState -> f TCState)
-> ((HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature)
-> (HashMap QName Definition -> f (HashMap QName Definition))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' Signature (HashMap QName Definition)
sigDefinitions
  local    <- case hlLevel of
    Full{} -> Getter TCState (HashMap QName Definition)
-> TCMT IO (HashMap QName Definition)
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (Getter TCState (HashMap QName Definition)
 -> TCMT IO (HashMap QName Definition))
-> Getter TCState (HashMap QName Definition)
-> TCMT IO (HashMap QName Definition)
forall a b. (a -> b) -> a -> b
$ (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature)
-> (HashMap QName Definition -> f (HashMap QName Definition))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' Signature (HashMap QName Definition)
sigDefinitions
    Level
_      -> HashMap QName Definition -> TCMT IO (HashMap QName Definition)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return HashMap QName Definition
forall k v. HashMap k v
HMap.empty
  impPatSyns <- useTC stPatternSynImports
  locPatSyns <- case hlLevel of
    Full{} -> Getter TCState (Map QName PatternSynDefn)
-> TCMT IO (Map QName PatternSynDefn)
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (Map QName PatternSynDefn -> f (Map QName PatternSynDefn))
-> TCState -> f TCState
Lens' TCState (Map QName PatternSynDefn)
Getter TCState (Map QName PatternSynDefn)
stPatternSyns
    Level
_      -> Map QName PatternSynDefn -> TCMT IO (Map QName PatternSynDefn)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Map QName PatternSynDefn
forall a. Null a => a
empty
      -- Traverses the syntax tree and constructs a map from qualified
      -- names to name kinds. TODO: Handle open public.
  let syntax :: NameKindMap
      syntax = NameKindBuilder -> NameKindMap -> NameKindMap
runBuilder (Declaration -> NameKindBuilder
forall m. Collection KName m => Declaration -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames Declaration
decl :: NameKindBuilder) NameKindMap
forall k v. HashMap k v
HMap.empty
  return $ \ QName
n -> (NameKind -> NameKind -> NameKind)
-> [Maybe NameKind] -> Maybe NameKind
forall a. (a -> a -> a) -> [Maybe a] -> Maybe a
unionsMaybeWith NameKind -> NameKind -> NameKind
mergeNameKind
    [ Defn -> NameKind
TCM.defnToNameKind (Defn -> NameKind)
-> (Definition -> Defn) -> Definition -> NameKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> NameKind) -> Maybe Definition -> Maybe NameKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> HashMap QName Definition -> Maybe Definition
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
n HashMap QName Definition
local
    , NameKind
con NameKind -> Maybe PatternSynDefn -> Maybe NameKind
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ QName -> Map QName PatternSynDefn -> Maybe PatternSynDefn
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
n Map QName PatternSynDefn
locPatSyns
    , Defn -> NameKind
TCM.defnToNameKind (Defn -> NameKind)
-> (Definition -> Defn) -> Definition -> NameKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> NameKind) -> Maybe Definition -> Maybe NameKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> HashMap QName Definition -> Maybe Definition
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
n HashMap QName Definition
imported
    , NameKind
con NameKind -> Maybe PatternSynDefn -> Maybe NameKind
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ QName -> Map QName PatternSynDefn -> Maybe PatternSynDefn
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
n Map QName PatternSynDefn
impPatSyns
    , QName -> NameKindMap -> Maybe NameKind
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
n NameKindMap
syntax
    ]
  where

  con :: NameKind
  con :: NameKind
con = Induction -> NameKind
Constructor Induction
Inductive

-- | The 'TCM.Axiom' constructor is used to represent various things
-- which are not really axioms, so when maps are merged 'Postulate's
-- are thrown away whenever possible. The 'declaredNames' function
-- below can return several explanations for one qualified name; the
-- 'Postulate's are bogus.
mergeNameKind :: NameKind -> NameKind -> NameKind
mergeNameKind :: NameKind -> NameKind -> NameKind
mergeNameKind NameKind
Postulate NameKind
k = NameKind
k
mergeNameKind NameKind
_     NameKind
Macro = NameKind
Macro  -- If the abstract syntax says macro, it's a macro.
mergeNameKind NameKind
k         NameKind
_ = NameKind
k

-- Auxiliary types for @nameKinds@ generation

type NameKindMap     = HashMap A.QName NameKind
data NameKindBuilder = NameKindBuilder
  { NameKindBuilder -> NameKindMap -> NameKindMap
runBuilder :: NameKindMap -> NameKindMap
  }

instance Semigroup (NameKindBuilder) where
  NameKindBuilder NameKindMap -> NameKindMap
f <> :: NameKindBuilder -> NameKindBuilder -> NameKindBuilder
<> NameKindBuilder NameKindMap -> NameKindMap
g = (NameKindMap -> NameKindMap) -> NameKindBuilder
NameKindBuilder ((NameKindMap -> NameKindMap) -> NameKindBuilder)
-> (NameKindMap -> NameKindMap) -> NameKindBuilder
forall a b. (a -> b) -> a -> b
$ NameKindMap -> NameKindMap
f (NameKindMap -> NameKindMap)
-> (NameKindMap -> NameKindMap) -> NameKindMap -> NameKindMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameKindMap -> NameKindMap
g

instance Monoid (NameKindBuilder) where
  mempty :: NameKindBuilder
mempty = (NameKindMap -> NameKindMap) -> NameKindBuilder
NameKindBuilder NameKindMap -> NameKindMap
forall a. a -> a
id
  mappend :: NameKindBuilder -> NameKindBuilder -> NameKindBuilder
mappend = NameKindBuilder -> NameKindBuilder -> NameKindBuilder
forall a. Semigroup a => a -> a -> a
(<>)

instance Singleton KName NameKindBuilder where
  singleton :: KName -> NameKindBuilder
singleton (WithKind KindOfName
k QName
q) = (NameKindMap -> NameKindMap) -> NameKindBuilder
NameKindBuilder ((NameKindMap -> NameKindMap) -> NameKindBuilder)
-> (NameKindMap -> NameKindMap) -> NameKindBuilder
forall a b. (a -> b) -> a -> b
$
    (NameKind -> NameKind -> NameKind)
-> QName -> NameKind -> NameKindMap -> NameKindMap
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
HMap.insertWith NameKind -> NameKind -> NameKind
mergeNameKind QName
q (NameKind -> NameKindMap -> NameKindMap)
-> NameKind -> NameKindMap -> NameKindMap
forall a b. (a -> b) -> a -> b
$ KindOfName -> NameKind
kindOfNameToNameKind KindOfName
k

instance Collection KName NameKindBuilder

-- | Generates syntax highlighting information for all constructors
-- occurring in patterns and expressions in the given declaration.
--
-- This function should only be called after type checking.
-- Constructors can be overloaded, and the overloading is resolved by
-- the type checker.

generateConstructorInfo
  :: TopLevelModuleName
     -- ^ The module to highlight.
  -> NameKinds
  -> A.Declaration
  -> TCM HighlightingInfoBuilder
generateConstructorInfo :: TopLevelModuleName
-> NameKinds -> Declaration -> TCM HighlightingInfoBuilder
generateConstructorInfo TopLevelModuleName
top NameKinds
kinds Declaration
decl = do

  -- Get boundaries of current declaration.
  -- @noRange@ should be impossible, but in case of @noRange@
  -- it makes sense to return mempty.
  [IntervalWithoutFile]
-> TCM HighlightingInfoBuilder
-> (IntervalWithoutFile
    -> [IntervalWithoutFile] -> TCM HighlightingInfoBuilder)
-> TCM HighlightingInfoBuilder
forall a b. [a] -> b -> (a -> [a] -> b) -> b
caseList (Range -> [IntervalWithoutFile]
forall a. Range' a -> [IntervalWithoutFile]
P.rangeIntervals (Range -> [IntervalWithoutFile]) -> Range -> [IntervalWithoutFile]
forall a b. (a -> b) -> a -> b
$ Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
decl)
           (HighlightingInfoBuilder -> TCM HighlightingInfoBuilder
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return HighlightingInfoBuilder
forall a. Monoid a => a
mempty) ((IntervalWithoutFile
  -> [IntervalWithoutFile] -> TCM HighlightingInfoBuilder)
 -> TCM HighlightingInfoBuilder)
-> (IntervalWithoutFile
    -> [IntervalWithoutFile] -> TCM HighlightingInfoBuilder)
-> TCM HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$ \ IntervalWithoutFile
i [IntervalWithoutFile]
is -> do
    let start :: Key
start = Word32 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> Key) -> Word32 -> Key
forall a b. (a -> b) -> a -> b
$ Position' () -> Word32
forall a. Position' a -> Word32
P.posPos (Position' () -> Word32) -> Position' () -> Word32
forall a b. (a -> b) -> a -> b
$ IntervalWithoutFile -> Position' ()
forall a. Interval' a -> Position' a
P.iStart IntervalWithoutFile
i
        end :: Key
end   = Word32 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> Key) -> Word32 -> Key
forall a b. (a -> b) -> a -> b
$ Position' () -> Word32
forall a. Position' a -> Word32
P.posPos (Position' () -> Word32) -> Position' () -> Word32
forall a b. (a -> b) -> a -> b
$ IntervalWithoutFile -> Position' ()
forall a. Interval' a -> Position' a
P.iEnd (IntervalWithoutFile -> Position' ())
-> IntervalWithoutFile -> Position' ()
forall a b. (a -> b) -> a -> b
$ IntervalWithoutFile -> [IntervalWithoutFile] -> IntervalWithoutFile
forall a. a -> [a] -> a
last1 IntervalWithoutFile
i [IntervalWithoutFile]
is

    -- Get all disambiguated names that fall within the range of decl.
    m0 <- Getter TCState (IntMap DisambiguatedName)
-> TCMT IO (IntMap DisambiguatedName)
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (IntMap DisambiguatedName -> f (IntMap DisambiguatedName))
-> TCState -> f TCState
Lens' TCState (IntMap DisambiguatedName)
Getter TCState (IntMap DisambiguatedName)
stDisambiguatedNames
    let (_, m1) = IntMap.split (pred start) m0
        (m2, _) = IntMap.split end m1
        constrs = IntMap DisambiguatedName -> [DisambiguatedName]
forall a. IntMap a -> [a]
IntMap.elems IntMap DisambiguatedName
m2

    -- Return suitable syntax highlighting information.
    return $ foldMap (runHighlighter top kinds) constrs

printSyntaxInfo :: Range -> TCM ()
printSyntaxInfo :: Range -> TCM ()
printSyntaxInfo Range
r = do
  syntaxInfo <- Getter TCState HighlightingInfo -> TCMT IO HighlightingInfo
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (HighlightingInfo -> f HighlightingInfo) -> TCState -> f TCState
Lens' TCState HighlightingInfo
Getter TCState HighlightingInfo
stSyntaxInfo
  ifTopLevelAndHighlightingLevelIs NonInteractive $
    printHighlightingInfo KeepHighlighting
      (restrictTo (rangeToRange r) syntaxInfo)

-- | Prints syntax highlighting info for an error.

printErrorInfo :: TCErr -> TCM ()
printErrorInfo :: TCErr -> TCM ()
printErrorInfo TCErr
e =
  RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (HighlightingInfo -> TCM ())
-> (HighlightingInfoBuilder -> HighlightingInfo)
-> HighlightingInfoBuilder
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HighlightingInfoBuilder -> HighlightingInfo
forall a b. Convert a b => a -> b
convert (HighlightingInfoBuilder -> TCM ())
-> TCM HighlightingInfoBuilder -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
    TCErr -> TCM HighlightingInfoBuilder
errorHighlighting TCErr
e

-- | Generate highlighting for error.

errorHighlighting :: TCErr -> TCM HighlightingInfoBuilder
errorHighlighting :: TCErr -> TCM HighlightingInfoBuilder
errorHighlighting TCErr
e = [TCM HighlightingInfoBuilder] -> TCM HighlightingInfoBuilder
forall a. Monoid a => [a] -> a
mconcat
  [ TCErr -> TCM HighlightingInfoBuilder
extraErrorHighlighting TCErr
e
  , Range -> [Char] -> HighlightingInfoBuilder
errorHighlighting' (TCErr -> Range
forall a. HasRange a => a -> Range
getRange TCErr
e) ([Char] -> HighlightingInfoBuilder)
-> TCMT IO [Char] -> TCM HighlightingInfoBuilder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCErr -> TCMT IO [Char]
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm [Char]
TCM.renderError TCErr
e
  ]

errorHighlighting'
  :: Range     -- ^ Error range.
  -> String    -- ^ Error message for tooltip.
  -> HighlightingInfoBuilder
errorHighlighting' :: Range -> [Char] -> HighlightingInfoBuilder
errorHighlighting' Range
r [Char]
s = [HighlightingInfoBuilder] -> HighlightingInfoBuilder
forall a. Monoid a => [a] -> a
mconcat
  [ -- Erase previous highlighting.
    Ranges -> Aspects -> HighlightingInfoBuilder
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Range' a -> Range' a
P.continuousPerLine Range
r) Aspects
forall a. Monoid a => a
mempty
  , -- Print new highlighting.
    Ranges -> Aspects -> HighlightingInfoBuilder
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR Range
r)
         (Aspects -> HighlightingInfoBuilder)
-> Aspects -> HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$ Aspects
parserBased { otherAspects = Set.singleton Error
                       , note         = s
                       }
  ]

-- | Some errors point to things out of the errorneous expression/declaration,
--   so we might to highlight these things as well.
extraErrorHighlighting :: TCErr -> TCM HighlightingInfoBuilder
extraErrorHighlighting :: TCErr -> TCM HighlightingInfoBuilder
extraErrorHighlighting = \case
  TypeError CallStack
_ TCState
_ Closure SomeDiagnostic
cl ->
    case SomeDiagnostic -> Maybe TypeError
forall a. Diagnostic a => SomeDiagnostic -> Maybe a
fromSomeDiagnostic (Closure SomeDiagnostic -> SomeDiagnostic
forall a. Closure a -> a
clValue Closure SomeDiagnostic
cl) of
      -- Andreas, 2025-09-15.
      -- The identifier that would be shadowed by the clashing definition
      -- is highlighted as dead code.
      -- (Not sure how good this is.)
      Just (ClashingDefinition QName
_ ClashingName
y Maybe NiceDeclaration
_) -> HighlightingInfoBuilder -> TCM HighlightingInfoBuilder
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (HighlightingInfoBuilder -> TCM HighlightingInfoBuilder)
-> HighlightingInfoBuilder -> TCM HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$ Range -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting (Range -> HighlightingInfoBuilder)
-> Range -> HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$ QName -> Range
forall a. HasNameBindingSite a => a -> Range
I.nameBindingSite (QName -> Range) -> QName -> Range
forall a b. (a -> b) -> a -> b
$ ClashingName -> QName
clashingQName ClashingName
y
      Just (ShadowedModule Name
x List1 ModuleName
ms)      -> Range -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting (Range -> HighlightingInfoBuilder)
-> ((TCMT IO Doc, Range) -> Range)
-> (TCMT IO Doc, Range)
-> HighlightingInfoBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TCMT IO Doc, Range) -> Range
forall a b. (a, b) -> b
snd ((TCMT IO Doc, Range) -> HighlightingInfoBuilder)
-> TCMT IO (TCMT IO Doc, Range) -> TCM HighlightingInfoBuilder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> List1 ModuleName -> TCMT IO (TCMT IO Doc, Range)
forall (m :: * -> *).
MonadPretty m =>
Name -> List1 ModuleName -> m (m Doc, Range)
TCM.prettyShadowedModule Name
x List1 ModuleName
ms
        -- 'prettyShadowedModule' mostly duplicates the work done by @'renderError' ('ShadowedModule' x ms)@
        -- in 'errorHighlighting',
        -- but since throwing an error is a once-in-a-run thing we need not worry.
      Maybe TypeError
_ -> TCM HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  TCErr
_ -> TCM HighlightingInfoBuilder
forall a. Monoid a => a
mempty

-- | Highlighting for warnings that are considered fatal.

errorWarningHighlighting :: HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting a
w =
  Ranges -> Aspects -> HighlightingInfoBuilder
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Range' a -> Range' a
P.continuousPerLine (Range -> Range) -> Range -> Range
forall a b. (a -> b) -> a -> b
$ a -> Range
forall a. HasRange a => a -> Range
getRange a
w) (Aspects -> HighlightingInfoBuilder)
-> Aspects -> HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$
    Aspects
parserBased { otherAspects = Set.singleton ErrorWarning }

-- | Generate syntax highlighting for warnings.

warningHighlighting :: TCWarning -> HighlightingInfoBuilder
warningHighlighting :: TCWarning -> HighlightingInfoBuilder
warningHighlighting = Bool -> TCWarning -> HighlightingInfoBuilder
warningHighlighting' Bool
True

warningHighlighting'
  :: Bool       -- ^ should we generate highlighting for unsolved metas and constrains?
  -> TCWarning  -- ^ the boxed diagnostic to generate highlighting information from
  -> HighlightingInfoBuilder

-- TODO: This function currently works by attempting to upcast to all of
-- the warning types that we know about. This means in particular that
-- it only works for the module currently being checked (but this isn't
-- a problem because we don't *re*highlight warnings when they're loaded
-- from an interface file).
-- It should probably be refactored so that either the Diagnostic class
-- directly handles highlighting generation *or* more specifically the
-- DiagWarning DiagnosticReason includes a "warning highlighting class"
-- that can be used.

warningHighlighting' :: Bool -> TCWarning -> HighlightingInfoBuilder
warningHighlighting' Bool
b TCWarning
w | Just UnsolvedWarning
warn <- SomeDiagnostic -> Maybe UnsolvedWarning
forall a. Diagnostic a => SomeDiagnostic -> Maybe a
fromSomeDiagnostic (TCWarning -> SomeDiagnostic
forall diag. TCWarning' diag -> diag
tcWarning TCWarning
w) = case UnsolvedWarning
warn of
  UnsolvedInteractionMetas{} -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  UnsolvedConstraints List1 ProblemConstraint
cs     -> if Bool
b then [Ranges] -> Constraints -> HighlightingInfoBuilder
constraintsHighlighting [] (Constraints -> HighlightingInfoBuilder)
-> Constraints -> HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$ List1 ProblemConstraint -> Constraints
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList List1 ProblemConstraint
cs else HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  UnsolvedMetaVariables Set1 Range
rs   -> if Bool
b then [Range] -> HighlightingInfoBuilder
metasHighlighting          ([Range] -> HighlightingInfoBuilder)
-> [Range] -> HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$ Set1 Range -> [Range]
forall a. NESet a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Set1 Range
rs else HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  InteractionMetaBoundaries{} -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty

warningHighlighting' Bool
b TCWarning
w | Just (IgnoredRecordDeclaration
warn :: IgnoredRecordDeclaration) <- SomeDiagnostic -> Maybe IgnoredRecordDeclaration
forall a. Diagnostic a => SomeDiagnostic -> Maybe a
fromSomeDiagnostic (TCWarning -> SomeDiagnostic
forall diag. TCWarning' diag -> diag
tcWarning TCWarning
w) =
  case IgnoredRecordDeclaration
warn of
    PrivateRecordField KwRange
kw Name
_ -> KwRange -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting KwRange
kw
    IgnoredRecordDeclaration
_                       -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w

warningHighlighting' Bool
b TCWarning
w | Just (DeclarationWarning CallStack
_ DeclarationWarning'
w) <- SomeDiagnostic -> Maybe DeclarationWarning
forall a. Diagnostic a => SomeDiagnostic -> Maybe a
fromSomeDiagnostic (TCWarning -> SomeDiagnostic
forall diag. TCWarning' diag -> diag
tcWarning TCWarning
w) = case DeclarationWarning'
w of
  -- we intentionally override the binding of `w` here so that our pattern of
  -- using `getRange w` still yields the most precise range information we
  -- can get.
  NotAllowedInMutual{}             -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  EmptyAbstract{}                  -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  EmptyConstructor{}               -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  EmptyInstance{}                  -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  EmptyMacro{}                     -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  EmptyMutual{}                    -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  EmptyPostulate{}                 -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  EmptyPrimitive{}                 -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  EmptyPrivate{}                   -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  EmptyGeneralize{}                -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  EmptyField{}                     -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  EmptyPolarityPragma{}            -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  HiddenGeneralize{}               -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
    -- Andreas, 2022-03-25, issue #5850
    -- We would like @deadcodeHighlighting w@ for the braces in
    -- @variable {x} : A@, but these have no range, so we cannot highlight them.
    -- Highlighting the variable instead might be misleading,
    -- suggesting that it is not generalized over.
  UselessAbstract{}                -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  UselessImport{}                  -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  UselessInstance{}                -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  UselessMacro{}                   -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  UselessPrivate{}                 -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  InvalidCatchallPragma{}          -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  InvalidNoPositivityCheckPragma{} -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  InvalidNoUniverseCheckPragma{}   -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  InvalidTerminationCheckPragma{}  -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  InvalidCoverageCheckPragma{}     -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  InvalidConstructorBlock{}        -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  InvalidDataOrRecDefParameter{}   -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  InvalidTacticAttribute{}         -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
  OpenImportAbstract{}             -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
cosmeticProblemHighlighting DeclarationWarning'
w
  OpenImportPrivate{}              -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
cosmeticProblemHighlighting DeclarationWarning'
w
  SafeFlagEta                   {} -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting DeclarationWarning'
w
  SafeFlagInjective             {} -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting DeclarationWarning'
w
  SafeFlagNoCoverageCheck       {} -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting DeclarationWarning'
w
  SafeFlagNoPositivityCheck     {} -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting DeclarationWarning'
w
  SafeFlagNoUniverseCheck       {} -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting DeclarationWarning'
w
  SafeFlagNonTerminating        {} -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting DeclarationWarning'
w
  SafeFlagPolarity              {} -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting DeclarationWarning'
w
  SafeFlagTerminating           {} -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting DeclarationWarning'
w
  W.ShadowingInTelescope List1 (Name, List2 Range)
nrs       -> ((Name, List2 Range) -> HighlightingInfoBuilder)
-> List1 (Name, List2 Range) -> HighlightingInfoBuilder
forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap
                                        (List2 Range -> HighlightingInfoBuilder
shadowingTelHighlighting (List2 Range -> HighlightingInfoBuilder)
-> ((Name, List2 Range) -> List2 Range)
-> (Name, List2 Range)
-> HighlightingInfoBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, List2 Range) -> List2 Range
forall a b. (a, b) -> b
snd)
                                        List1 (Name, List2 Range)
nrs
  MissingDataDeclaration{}         -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
missingDefinitionHighlighting DeclarationWarning'
w
  MissingDefinitions{}             -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
missingDefinitionHighlighting DeclarationWarning'
w
  -- TODO: explore highlighting opportunities here!
  PolarityPragmasButNotPostulates{} -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  PragmaNoTerminationCheck{}        -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  PragmaCompiled{}                  -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting DeclarationWarning'
w
  UnknownFixityInMixfixDecl{}       -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  UnknownNamesInFixityDecl{}        -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting DeclarationWarning'
w
  UnknownNamesInPolarityPragmas{}   -> DeclarationWarning' -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting DeclarationWarning'
w


warningHighlighting' Bool
b TCWarning
w | Just Warning
warn <- SomeDiagnostic -> Maybe Warning
forall a. Diagnostic a => SomeDiagnostic -> Maybe a
fromSomeDiagnostic (TCWarning -> SomeDiagnostic
forall diag. TCWarning' diag -> diag
tcWarning TCWarning
w) = case Warning
warn of
  TerminationIssue List1 TerminationError
terrs     -> List1 TerminationError -> HighlightingInfoBuilder
terminationErrorHighlighting List1 TerminationError
terrs
  NotStrictlyPositive QName
d Seq OccursWhere
ocs  -> QName -> Seq OccursWhere -> HighlightingInfoBuilder
positivityErrorHighlighting QName
d Seq OccursWhere
ocs
  ConstructorDoesNotFitInData DataOrRecord_
_dataOrRecord QName
c Sort
_s1 Sort
_s2 TCErr
_err -> Range -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting (Range -> HighlightingInfoBuilder)
-> Range -> HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$
     QName -> Range
forall a. HasRange a => a -> Range
getRange QName
c Range -> Range -> Range
forall a. Null a => a -> a -> a
`catchNull` TCWarning -> Range
forall a. HasRange a => a -> Range
getRange TCWarning
w
  CoinductiveEtaRecord QName
_x    -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  -- #3965 highlight each unreachable clause independently: they
  -- may be interleaved with actually reachable clauses!
  UnreachableClauses QName
_ List1 Range
rs    -> (Range -> HighlightingInfoBuilder)
-> List1 Range -> HighlightingInfoBuilder
forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Range -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting List1 Range
rs
  CoverageIssue{}            -> Range -> HighlightingInfoBuilder
coverageErrorHighlighting (Range -> HighlightingInfoBuilder)
-> Range -> HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall a. HasRange a => a -> Range
getRange TCWarning
w
  CoverageNoExactSplit{}     -> Range -> HighlightingInfoBuilder
catchallHighlighting (Range -> HighlightingInfoBuilder)
-> Range -> HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall a. HasRange a => a -> Range
getRange TCWarning
w
  InlineNoExactSplit{}       -> Range -> HighlightingInfoBuilder
catchallHighlighting (Range -> HighlightingInfoBuilder)
-> Range -> HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall a. HasRange a => a -> Range
getRange TCWarning
w
  AbsurdPatternRequiresAbsentRHS{} -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  DuplicateRecordDirective{}   -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  ModuleDoesntExport QName
_ [Name]
_ [Name]
_ List1 ImportedName
xs  -> (ImportedName -> HighlightingInfoBuilder)
-> List1 ImportedName -> HighlightingInfoBuilder
forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ImportedName -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting List1 ImportedName
xs
  DuplicateUsing List1 ImportedName
xs            -> (ImportedName -> HighlightingInfoBuilder)
-> List1 ImportedName -> HighlightingInfoBuilder
forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ImportedName -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting List1 ImportedName
xs
  FixityInRenamingModule List1 Range
rs    -> (Range -> HighlightingInfoBuilder)
-> List1 Range -> HighlightingInfoBuilder
forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Range -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting List1 Range
rs
  -- expanded catch-all case to get a warning for new constructors
  CantGeneralizeOverSorts{}  -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  OldBuiltin{}                -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  BuiltinDeclaresIdentifier{} -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  EmptyWhere{}               -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  IllformedAsClause{}        -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  UnusedImports ModuleName
m Maybe (List1 AbstractName)
Nothing    -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  UnusedImports ModuleName
m Maybe (List1 AbstractName)
xs         -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
cosmeticProblemHighlighting TCWarning
w HighlightingInfoBuilder
-> HighlightingInfoBuilder -> HighlightingInfoBuilder
forall a. Semigroup a => a -> a -> a
<> (List1 AbstractName -> HighlightingInfoBuilder)
-> Maybe (List1 AbstractName) -> HighlightingInfoBuilder
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap List1 AbstractName -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting Maybe (List1 AbstractName)
xs
  UselessPragma Range
r Doc
_          -> Range -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting Range
r
  UselessPublic{}            -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  UselessHiding List1 ImportedName
xs           -> (ImportedName -> HighlightingInfoBuilder)
-> List1 ImportedName -> HighlightingInfoBuilder
forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ImportedName -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting List1 ImportedName
xs
  UselessInline{}            -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  UselessPatternDeclarationForRecord{} -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  UselessTactic{}            -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  ClashesViaRenaming NameOrModule
_ Set1 Name
xs    -> (Name -> HighlightingInfoBuilder)
-> Set1 Name -> HighlightingInfoBuilder
forall m a. Monoid m => (a -> m) -> NESet a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Name -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting Set1 Name
xs
    -- #4154, TODO: clashing renamings are not dead code, but introduce problems.
    -- Should we have a different color?
  WrongInstanceDeclaration KwRange
kwr  -> KwRange -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
instanceProblemHighlighting KwRange
kwr HighlightingInfoBuilder
-> HighlightingInfoBuilder -> HighlightingInfoBuilder
forall a. Semigroup a => a -> a -> a
<> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
instanceProblemHighlighting TCWarning
w
  InstanceWithExplicitArg KwRange
kwr QName
_ -> KwRange -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
instanceProblemHighlighting KwRange
kwr HighlightingInfoBuilder
-> HighlightingInfoBuilder -> HighlightingInfoBuilder
forall a. Semigroup a => a -> a -> a
<> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
instanceProblemHighlighting TCWarning
w
  InstanceNoOutputTypeName{}   -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
instanceProblemHighlighting TCWarning
w
  InstanceArgWithExplicitArg{} -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
instanceProblemHighlighting TCWarning
w
  InversionDepthReached{}    -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  -- Andreas, 2020-03-21, issue #4456:
  -- Error warnings that do not have dedicated highlighting
  -- are highlighted as errors.
  InvalidCharacterLiteral{}             -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  SafeFlagPostulate{}                   -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  SafeFlagPragma{}                      -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  InfectiveImport{}                     -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  CoInfectiveImport{}                   -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  InvalidDisplayForm{}                  -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  UnusedVariablesInDisplayForm List1 Name
xs       -> (Name -> HighlightingInfoBuilder)
-> List1 Name -> HighlightingInfoBuilder
forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Name -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting List1 Name
xs
  Warning
ShouldBeEtaRecordPattern              -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  TooManyArgumentsToSort QName
_ List1 (NamedArg Expr)
args         -> List1 (NamedArg Expr) -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting List1 (NamedArg Expr)
args
  Warning
RewritesNothing                       -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
cosmeticProblemHighlighting TCWarning
w
  RecursiveRecordNeedsInductivity QName
_x    -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  WithClauseProjectionFixityMismatch NamedArg Pattern
p ProjOrigin
_ NamedArg DeBruijnPattern
_ ProjOrigin
_ -> NamedArg Pattern -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
cosmeticProblemHighlighting NamedArg Pattern
p
  ConflictingPragmaOptions{} -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  DeprecationWarning{}       -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  UserWarning{}              -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  LibraryWarning{}           -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  PragmaCompileWrongName{}   -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  PragmaExpectsDefinedSymbol{}
                             -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  PragmaExpectsUnambiguousConstructorOrFunction{}
                             -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  PragmaExpectsUnambiguousProjectionOrFunction{}
                             -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  NoMain{}                   -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  NotInScopeW{}              -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  UnsupportedIndexedMatch{}  -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  AsPatternShadowsConstructorOrPatternSynonym{}
                             -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  PatternShadowsConstructor{}-> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w  -- or mempty ?
  RecordFieldWarning RecordFieldWarning
w       -> RecordFieldWarning -> HighlightingInfoBuilder
recordFieldWarningHighlighting RecordFieldWarning
w
  OptionWarning OptionWarning
w            -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  ParseWarning ParseWarning
w             -> case ParseWarning
w of
    Pa.MisplacedAttributes{}      -> ParseWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting ParseWarning
w
    Pa.UnknownPolarity{}          -> ParseWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting ParseWarning
w
    Pa.UnknownAttribute{}         -> ParseWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting ParseWarning
w
    Pa.UnsupportedAttribute{}     -> ParseWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting ParseWarning
w
    Pa.MismatchedBrackets{}       -> ParseWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting ParseWarning
w
    Pa.OverlappingTokensWarning{} -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty
  MissingTypeSignatureForOpaque{} -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  NotAffectedByOpaque{}           -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  UselessOpaque{}                 -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  UnfoldingWrongName QName
x            -> QName -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting QName
x
  UnfoldTransparentName QName
r         -> QName -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting QName
r
  FaceConstraintCannotBeHidden{}  -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  FaceConstraintCannotBeNamed{}   -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w

  HiddenNotInArgumentPosition{}   -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  InstanceNotInArgumentPosition{} -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  MacroInLetBindings{}            -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  AbstractInLetBindings{}         -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  IllegalDeclarationInDataDefinition{} -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  DefinitionBeforeDeclaration AbstractName
x   -> TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
cosmeticProblemHighlighting TCWarning
w HighlightingInfoBuilder
-> HighlightingInfoBuilder -> HighlightingInfoBuilder
forall a. Semigroup a => a -> a -> a
<> Range -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
cosmeticProblemHighlighting (AbstractName -> Range
forall a. HasNameBindingSite a => a -> Range
nameBindingSite AbstractName
x)

  -- Backends
  CustomBackendWarning{} -> HighlightingInfoBuilder
forall a. Monoid a => a
mempty

  -- Polarities
  TooManyPolarities QName
_x PragmaPolarities
occs -> PragmaPolarities -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting PragmaPolarities
occs

warningHighlighting' Bool
b TCWarning
w | Just (DeferredError
_ :: DeferredError) <- SomeDiagnostic -> Maybe DeferredError
forall a. Diagnostic a => SomeDiagnostic -> Maybe a
fromSomeDiagnostic (TCWarning -> SomeDiagnostic
forall diag. TCWarning' diag -> diag
tcWarning TCWarning
w) =
  -- TODO: proper errorHighlighting gets overridden by semantic
  -- highlighted of overloaded definitions after the type checker
  -- finishes
  -- errorHighlighting' (clEnv cl ^. eRange) (tcWarningString w)
  TCWarning -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w

warningHighlighting' Bool
b TCWarning
w = HighlightingInfoBuilder
forall a. Monoid a => a
mempty

recordFieldWarningHighlighting ::
  RecordFieldWarning -> HighlightingInfoBuilder
recordFieldWarningHighlighting :: RecordFieldWarning -> HighlightingInfoBuilder
recordFieldWarningHighlighting = \case
  W.DuplicateFields List1 (Name, List1 Range)
xrs      -> NonEmpty HighlightingInfoBuilder -> HighlightingInfoBuilder
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty HighlightingInfoBuilder -> HighlightingInfoBuilder)
-> NonEmpty HighlightingInfoBuilder -> HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$ ((Name, List1 Range) -> HighlightingInfoBuilder)
-> List1 (Name, List1 Range) -> NonEmpty HighlightingInfoBuilder
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (List1 Range -> HighlightingInfoBuilder
dead (List1 Range -> HighlightingInfoBuilder)
-> ((Name, List1 Range) -> List1 Range)
-> (Name, List1 Range)
-> HighlightingInfoBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, List1 Range) -> List1 Range
forall a b. (a, b) -> b
snd) List1 (Name, List1 Range)
xrs
  W.TooManyFields QName
_q [Name]
_ys List1 (Name, Range)
xrs -> List1 Range -> HighlightingInfoBuilder
dead (List1 Range -> HighlightingInfoBuilder)
-> List1 Range -> HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$ ((Name, Range) -> Range) -> List1 (Name, Range) -> List1 Range
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, Range) -> Range
forall a b. (a, b) -> b
snd List1 (Name, Range)
xrs
  where
  dead :: List1 Range -> HighlightingInfoBuilder
  dead :: List1 Range -> HighlightingInfoBuilder
dead = NonEmpty HighlightingInfoBuilder -> HighlightingInfoBuilder
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty HighlightingInfoBuilder -> HighlightingInfoBuilder)
-> (List1 Range -> NonEmpty HighlightingInfoBuilder)
-> List1 Range
-> HighlightingInfoBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Range -> HighlightingInfoBuilder)
-> List1 Range -> NonEmpty HighlightingInfoBuilder
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Range -> HighlightingInfoBuilder
forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting
  -- Andreas, 2020-03-27 #3684: This variant seems to only highlight @x@:
  -- dead = mconcat . map f
  -- f (x, r) = deadcodeHighlighting (getRange x) `mappend` deadcodeHighlighting r

-- | Generate syntax highlighting for termination errors.

terminationErrorHighlighting ::
  List1 TerminationError -> HighlightingInfoBuilder
terminationErrorHighlighting :: List1 TerminationError -> HighlightingInfoBuilder
terminationErrorHighlighting List1 TerminationError
termErrs = HighlightingInfoBuilder
functionDefs HighlightingInfoBuilder
-> HighlightingInfoBuilder -> HighlightingInfoBuilder
forall a. Monoid a => a -> a -> a
`mappend` HighlightingInfoBuilder
callSites
  where
    m :: Aspects
m            = Aspects
parserBased { otherAspects = Set.singleton TerminationProblem }
    functionDefs :: HighlightingInfoBuilder
functionDefs = (QName -> HighlightingInfoBuilder)
-> [QName] -> HighlightingInfoBuilder
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\QName
x -> Ranges -> Aspects -> HighlightingInfoBuilder
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ QName -> Range
forall a. HasNameBindingSite a => a -> Range
nameBindingSite QName
x) Aspects
m) ([QName] -> HighlightingInfoBuilder)
-> [QName] -> HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$
                   (TerminationError -> [QName]) -> List1 TerminationError -> [QName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TerminationError -> [QName]
termErrFunctions List1 TerminationError
termErrs
    callSites :: HighlightingInfoBuilder
callSites    = (Range -> HighlightingInfoBuilder)
-> [Range] -> HighlightingInfoBuilder
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\Range
r -> Ranges -> Aspects -> HighlightingInfoBuilder
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR Range
r) Aspects
m) ([Range] -> HighlightingInfoBuilder)
-> [Range] -> HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$
                   (TerminationError -> [Range]) -> List1 TerminationError -> [Range]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((CallInfo -> Range) -> [CallInfo] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map CallInfo -> Range
forall a. HasRange a => a -> Range
getRange ([CallInfo] -> [Range])
-> (TerminationError -> [CallInfo]) -> TerminationError -> [Range]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TerminationError -> [CallInfo]
termErrCalls) List1 TerminationError
termErrs

-- | Generate syntax highlighting for not-strictly-positive inductive
-- definitions.

positivityErrorHighlighting ::
  I.QName -> Seq OccursWhere -> HighlightingInfoBuilder
positivityErrorHighlighting :: QName -> Seq OccursWhere -> HighlightingInfoBuilder
positivityErrorHighlighting QName
q Seq OccursWhere
os =
  [Ranges] -> Aspects -> HighlightingInfoBuilder
forall a hl.
(IsBasicRangeMap a hl, Monoid hl) =>
[Ranges] -> a -> hl
several (Range -> Ranges
rToR (Range -> Ranges) -> [Range] -> [Ranges]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Range
forall a. HasRange a => a -> Range
getRange QName
q Range -> [Range] -> [Range]
forall a. a -> [a] -> [a]
: [Range]
rs) Aspects
m
  where
    rs :: [Range]
rs = (OccursWhere -> Range) -> [OccursWhere] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map (\(OccursWhere Range
r Seq Where
_ Seq Where
_) -> Range
r) (Seq OccursWhere -> [OccursWhere]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Seq OccursWhere
os)
    m :: Aspects
m  = Aspects
parserBased { otherAspects = Set.singleton PositivityProblem }

deadcodeHighlighting :: HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting a
a = Ranges -> Aspects -> HighlightingInfoBuilder
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Range' a -> Range' a
P.continuous (Range -> Range) -> Range -> Range
forall a b. (a -> b) -> a -> b
$ a -> Range
forall a. HasRange a => a -> Range
getRange a
a) Aspects
m
  where m :: Aspects
m = Aspects
parserBased { otherAspects = Set.singleton Deadcode }

coverageErrorHighlighting :: Range -> HighlightingInfoBuilder
coverageErrorHighlighting :: Range -> HighlightingInfoBuilder
coverageErrorHighlighting Range
r = Ranges -> Aspects -> HighlightingInfoBuilder
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Range' a -> Range' a
P.continuousPerLine Range
r) Aspects
m
  where m :: Aspects
m = Aspects
parserBased { otherAspects = Set.singleton CoverageProblem }

shadowingTelHighlighting :: List2 Range -> HighlightingInfoBuilder
shadowingTelHighlighting :: List2 Range -> HighlightingInfoBuilder
shadowingTelHighlighting =
  -- we do not want to highlight the one variable in scope so we take
  -- the @init@ segment of the ranges in question
  (Range -> HighlightingInfoBuilder)
-> List1 Range -> HighlightingInfoBuilder
forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\Range
r -> Ranges -> Aspects -> HighlightingInfoBuilder
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Range' a -> Range' a
P.continuous Range
r) Aspects
m) (List1 Range -> HighlightingInfoBuilder)
-> (List2 Range -> List1 Range)
-> List2 Range
-> HighlightingInfoBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List2 Range -> List1 Range
forall a. List2 a -> List1 a
List2.init
  where
  m :: Aspects
m = Aspects
parserBased { otherAspects =
                      Set.singleton H.ShadowingInTelescope }

catchallHighlighting :: Range -> HighlightingInfoBuilder
catchallHighlighting :: Range -> HighlightingInfoBuilder
catchallHighlighting Range
r = Ranges -> Aspects -> HighlightingInfoBuilder
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Range' a -> Range' a
P.continuousPerLine Range
r) Aspects
m
  where m :: Aspects
m = Aspects
parserBased { otherAspects = Set.singleton CatchallClause }

cosmeticProblemHighlighting :: HasRange a => a -> HighlightingInfoBuilder
cosmeticProblemHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
cosmeticProblemHighlighting a
a = Ranges -> Aspects -> HighlightingInfoBuilder
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Range' a -> Range' a
P.continuousPerLine Range
r) Aspects
m
  where
    r :: Range
r = a -> Range
forall a. HasRange a => a -> Range
getRange a
a
    m :: Aspects
m = Aspects
parserBased { otherAspects = Set.singleton CosmeticProblem }

instanceProblemHighlighting :: HasRange a => a -> HighlightingInfoBuilder
instanceProblemHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
instanceProblemHighlighting a
a = Ranges -> Aspects -> HighlightingInfoBuilder
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Range' a -> Range' a
P.continuousPerLine Range
r) Aspects
m
  where
    r :: Range
r = a -> Range
forall a. HasRange a => a -> Range
getRange a
a
    m :: Aspects
m = Aspects
parserBased { otherAspects = Set.singleton InstanceProblem }

missingDefinitionHighlighting ::
  HasRange a => a -> HighlightingInfoBuilder
missingDefinitionHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
missingDefinitionHighlighting a
a = Ranges -> Aspects -> HighlightingInfoBuilder
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Range' a -> Range' a
P.continuousPerLine (Range -> Range) -> Range -> Range
forall a b. (a -> b) -> a -> b
$ a -> Range
forall a. HasRange a => a -> Range
getRange a
a) Aspects
m
  where m :: Aspects
m = Aspects
parserBased { otherAspects = Set.singleton Aspect.MissingDefinition }

-- | Generates and prints syntax highlighting information for unsolved
-- meta-variables and certain unsolved constraints.

printUnsolvedInfo :: TCM ()
printUnsolvedInfo :: TCM ()
printUnsolvedInfo = do
  info <- TCM HighlightingInfoBuilder
computeUnsolvedInfo

  printHighlightingInfo KeepHighlighting (convert info)

computeUnsolvedInfo :: TCM HighlightingInfoBuilder
computeUnsolvedInfo :: TCM HighlightingInfoBuilder
computeUnsolvedInfo = do
  (rs, metaInfo) <- TCM ([Ranges], HighlightingInfoBuilder)
computeUnsolvedMetaWarnings
  constraintInfo <- computeUnsolvedConstraints rs

  return $ metaInfo `mappend` constraintInfo

-- | Generates syntax highlighting information for unsolved meta
-- variables.
--   Also returns ranges of unsolved or interaction metas.
computeUnsolvedMetaWarnings :: TCM ([Ranges], HighlightingInfoBuilder)
computeUnsolvedMetaWarnings :: TCM ([Ranges], HighlightingInfoBuilder)
computeUnsolvedMetaWarnings = do
  is <- TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas

  -- We don't want to highlight blocked terms, since
  --   * there is always at least one proper meta responsible for the blocking
  --   * in many cases the blocked term covers the highlighting for this meta
  --   * for the same reason we skip metas with a twin, since the twin will be blocked.
  let notBlocked MetaId
m = Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Bool
isBlockedTerm MetaId
m
  let notHasTwin MetaId
m = Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Bool
hasTwinMeta MetaId
m
  ms <- filterM notHasTwin =<< filterM notBlocked =<< getOpenMetas

  let extend = (Range -> Ranges) -> [Range] -> [Ranges]
forall a b. (a -> b) -> [a] -> [b]
map (Range -> Ranges
rToR (Range -> Ranges) -> (Range -> Range) -> Range -> Ranges
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Range
forall a. Range' a -> Range' a
P.continuousPerLine)

  rs <- extend <$> mapM getMetaRange (ms \\ is)

  rs' <- extend <$> mapM getMetaRange is
  return $ (rs ++ rs', metasHighlighting' rs)

metasHighlighting :: [Range] -> HighlightingInfoBuilder
metasHighlighting :: [Range] -> HighlightingInfoBuilder
metasHighlighting = [Ranges] -> HighlightingInfoBuilder
metasHighlighting' ([Ranges] -> HighlightingInfoBuilder)
-> ([Range] -> [Ranges]) -> [Range] -> HighlightingInfoBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Range -> Ranges) -> [Range] -> [Ranges]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Range -> Ranges
rToR (Range -> Ranges) -> (Range -> Range) -> Range -> Ranges
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Range
forall a. Range' a -> Range' a
P.continuousPerLine)

metasHighlighting' :: [Ranges] -> HighlightingInfoBuilder
metasHighlighting' :: [Ranges] -> HighlightingInfoBuilder
metasHighlighting' [Ranges]
rs =
  [Ranges] -> Aspects -> HighlightingInfoBuilder
forall a hl.
(IsBasicRangeMap a hl, Monoid hl) =>
[Ranges] -> a -> hl
several ([Ranges] -> [Item [Ranges]]
forall l. IsList l => l -> [Item l]
List1.toList [Ranges]
rs) Aspects
parserBased{ otherAspects = Set.singleton UnsolvedMeta }

-- | Generates syntax highlighting information for unsolved constraints
--   (ideally: that are not connected to a meta variable).

computeUnsolvedConstraints :: [Ranges] -- ^ does not add ranges that would overlap with these.
                           -> TCM HighlightingInfoBuilder
computeUnsolvedConstraints :: [Ranges] -> TCM HighlightingInfoBuilder
computeUnsolvedConstraints [Ranges]
ms = [Ranges] -> Constraints -> HighlightingInfoBuilder
constraintsHighlighting [Ranges]
ms (Constraints -> HighlightingInfoBuilder)
-> TCMT IO Constraints -> TCM HighlightingInfoBuilder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
getAllConstraints

constraintsHighlighting ::
  [Ranges] -> Constraints -> HighlightingInfoBuilder
constraintsHighlighting :: [Ranges] -> Constraints -> HighlightingInfoBuilder
constraintsHighlighting [Ranges]
ms Constraints
cs =
  [Ranges] -> Aspects -> HighlightingInfoBuilder
forall a hl.
(IsBasicRangeMap a hl, Monoid hl) =>
[Ranges] -> a -> hl
several ((Ranges -> Bool) -> [Ranges] -> [Ranges]
forall a. (a -> Bool) -> [a] -> [a]
filter Ranges -> Bool
noOverlap ([Ranges] -> [Ranges]) -> [Ranges] -> [Ranges]
forall a b. (a -> b) -> a -> b
$ (Range -> Ranges) -> [Range] -> [Ranges]
forall a b. (a -> b) -> [a] -> [b]
map (Range -> Ranges
rToR (Range -> Ranges) -> (Range -> Range) -> Range -> Ranges
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Range
forall a. Range' a -> Range' a
P.continuousPerLine) [Range]
rs)
          (Aspects
parserBased { otherAspects = Set.singleton UnsolvedConstraint })
  where
  noOverlap :: Ranges -> Bool
noOverlap Ranges
r = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Ranges -> Bool) -> [Ranges] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Ranges -> Ranges -> Bool
overlappings (Ranges -> Ranges -> Bool) -> Ranges -> Ranges -> Bool
forall a b. (a -> b) -> a -> b
$ Ranges
r) ([Ranges] -> Bool) -> [Ranges] -> Bool
forall a b. (a -> b) -> a -> b
$ [Ranges]
ms
  -- get ranges of interesting unsolved constraints
  rs :: [Range]
rs = ((Closure Constraint -> Maybe Range)
-> [Closure Constraint] -> [Range]
forall a b. (a -> Maybe b) -> [a] -> [b]
`mapMaybe` ((ProblemConstraint -> Closure Constraint)
-> Constraints -> [Closure Constraint]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> Closure Constraint
theConstraint Constraints
cs)) ((Closure Constraint -> Maybe Range) -> [Range])
-> (Closure Constraint -> Maybe Range) -> [Range]
forall a b. (a -> b) -> a -> b
$ \case
    Closure{ clValue :: forall a. Closure a -> a
clValue = IsEmpty Range
r Type
t           } -> Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = ValueCmp{} } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$! Range -> Range
forall a. HasRange a => a -> Range
getRange (Getting Range TCEnv Range -> TCEnv -> Range
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Range TCEnv Range
Lens' TCEnv Range
eRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = ElimCmp{}  } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$! Range -> Range
forall a. HasRange a => a -> Range
getRange (Getting Range TCEnv Range -> TCEnv -> Range
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Range TCEnv Range
Lens' TCEnv Range
eRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = SortCmp{}  } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$! Range -> Range
forall a. HasRange a => a -> Range
getRange (Getting Range TCEnv Range -> TCEnv -> Range
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Range TCEnv Range
Lens' TCEnv Range
eRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = LevelCmp{} } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$! Range -> Range
forall a. HasRange a => a -> Range
getRange (Getting Range TCEnv Range -> TCEnv -> Range
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Range TCEnv Range
Lens' TCEnv Range
eRange TCEnv
e)
    Closure Constraint
_ -> Maybe Range
forall a. Maybe a
Nothing


-- * Disambiguation of constructors and projections.

storeDisambiguatedField :: A.QName -> TCM ()
storeDisambiguatedField :: QName -> TCM ()
storeDisambiguatedField = NameKind -> QName -> TCM ()
storeDisambiguatedName NameKind
Field

storeDisambiguatedProjection :: A.QName -> TCM ()
storeDisambiguatedProjection :: QName -> TCM ()
storeDisambiguatedProjection = QName -> TCM ()
storeDisambiguatedField

storeDisambiguatedConstructor :: Induction -> A.QName -> TCM ()
storeDisambiguatedConstructor :: Induction -> QName -> TCM ()
storeDisambiguatedConstructor Induction
i = NameKind -> QName -> TCM ()
storeDisambiguatedName (NameKind -> QName -> TCM ()) -> NameKind -> QName -> TCM ()
forall a b. (a -> b) -> a -> b
$ Induction -> NameKind
Constructor Induction
i

-- TODO: move the following function to a new module TypeChecking.Overloading
-- that gathers functions concerning disambiguation of overloading.

-- | Remember a name disambiguation (during type checking).
--   To be used later during syntax highlighting.
--   Also: raise user warnings associated with the name.
storeDisambiguatedName :: NameKind -> A.QName -> TCM ()
storeDisambiguatedName :: NameKind -> QName -> TCM ()
storeDisambiguatedName NameKind
k QName
q = do
  QName -> TCM ()
forall (m :: * -> *). MonadWarning m => QName -> m ()
raiseWarningsOnUsage QName
q
  Maybe Key -> (Key -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (Range -> Maybe Key
forall {b} {a}. Num b => Range' a -> Maybe b
start (Range -> Maybe Key) -> Range -> Maybe Key
forall a b. (a -> b) -> a -> b
$ QName -> Range
forall a. HasRange a => a -> Range
getRange QName
q) ((Key -> TCM ()) -> TCM ()) -> (Key -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Key
i ->
    ASetter' TCState (IntMap DisambiguatedName)
-> (IntMap DisambiguatedName -> IntMap DisambiguatedName) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ASetter' TCState (IntMap DisambiguatedName)
Lens' TCState (IntMap DisambiguatedName)
stDisambiguatedNames ((IntMap DisambiguatedName -> IntMap DisambiguatedName) -> TCM ())
-> (IntMap DisambiguatedName -> IntMap DisambiguatedName) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Key
-> DisambiguatedName
-> IntMap DisambiguatedName
-> IntMap DisambiguatedName
forall a. Key -> a -> IntMap a -> IntMap a
IntMap.insert Key
i (DisambiguatedName
 -> IntMap DisambiguatedName -> IntMap DisambiguatedName)
-> DisambiguatedName
-> IntMap DisambiguatedName
-> IntMap DisambiguatedName
forall a b. (a -> b) -> a -> b
$ NameKind -> QName -> DisambiguatedName
DisambiguatedName NameKind
k QName
q
  where
  start :: Range' a -> Maybe b
start Range' a
r = Word32 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> b) -> (Position' () -> Word32) -> Position' () -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Position' () -> Word32
forall a. Position' a -> Word32
P.posPos (Position' () -> b) -> Maybe (Position' ()) -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range' a -> Maybe (Position' ())
forall a. Range' a -> Maybe (Position' ())
P.rStart' Range' a
r

-- | Store a disambiguation of record field tags for the purpose of highlighting.
disambiguateRecordFields
  :: [C.Name]   -- ^ Record field names in a record expression.
  -> [A.QName]  -- ^ Record field names in the corresponding record type definition
  -> TCM ()
disambiguateRecordFields :: [Name] -> [QName] -> TCM ()
disambiguateRecordFields [Name]
cxs [QName]
axs = [Name] -> (Name -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Name]
cxs ((Name -> TCM ()) -> TCM ()) -> (Name -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Name
cx -> do
  Maybe QName -> TCM () -> (QName -> TCM ()) -> TCM ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe ((QName -> Bool) -> [QName] -> Maybe QName
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((Name
cx Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==) (Name -> Bool) -> (QName -> Name) -> QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
A.nameConcrete (Name -> Name) -> (QName -> Name) -> QName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
A.qnameName) [QName]
axs) (() -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
ax -> do
    QName -> TCM ()
storeDisambiguatedField QName
ax{ A.qnameName = (A.qnameName ax) { A.nameConcrete = cx } }