-- | Generates data used for precise syntax highlighting.

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

module Agda.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 qualified Data.Foldable as Fold
import qualified Data.Map as Map
import Data.Maybe
import Data.List ((\\))
import qualified Data.List as List
import qualified Data.IntMap as IntMap
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HMap
import Data.Semigroup (sconcat)
import Data.Sequence (Seq)
import qualified Data.Set as Set
import qualified Data.Text.Lazy as Text

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

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

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

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

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

import Agda.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 :: RangeMap Aspects
h = DelayedMerge RangePair -> RangeMap Aspects
forall a b. Convert a b => a -> b
convert (DelayedMerge RangePair -> RangeMap Aspects)
-> DelayedMerge RangePair -> RangeMap Aspects
forall a b. (a -> b) -> a -> b
$ Bool -> TCWarning -> DelayedMerge RangePair
warningHighlighting' Bool
False TCWarning
tcwarn
  -- Highlighting for warnings coming from the Happy parser is placed
  -- together with token highlighting.
  case TCWarning -> Warning
tcWarning TCWarning
tcwarn of
    ParseWarning{} -> Lens' TCState (RangeMap Aspects)
-> (RangeMap Aspects -> RangeMap Aspects) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens (RangeMap Aspects -> f (RangeMap Aspects)) -> TCState -> f TCState
Lens' TCState (RangeMap Aspects)
stTokens     (RangeMap Aspects
h RangeMap Aspects -> RangeMap Aspects -> RangeMap Aspects
forall a. Semigroup a => a -> a -> a
<>)
    Warning
_              -> Lens' TCState (RangeMap Aspects)
-> (RangeMap Aspects -> RangeMap Aspects) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens (RangeMap Aspects -> f (RangeMap Aspects)) -> TCState -> f TCState
Lens' TCState (RangeMap Aspects)
stSyntaxInfo (RangeMap Aspects
h RangeMap Aspects -> RangeMap Aspects -> RangeMap Aspects
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 -> RangeMap Aspects -> TCM ()
forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> RangeMap Aspects -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting RangeMap Aspects
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' SrcFile -> Bool
forall a. Null a => a -> Bool
null (Range' SrcFile -> Bool) -> Range' SrcFile -> Bool
forall a b. (a -> b) -> a -> b
$ Declaration -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
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 -> TCMT IO (DelayedMerge RangePair)
generateConstructorInfo TopLevelModuleName
top NameKinds
kinds Declaration
decl
      Level
_      -> DelayedMerge RangePair -> TCMT IO (DelayedMerge RangePair)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return DelayedMerge RangePair
forall a. Monoid a => a
mempty

    -- Main source of scope-checker generated highlighting:
    let nameInfo = TopLevelModuleName
-> NameKinds -> Declaration -> DelayedMerge RangePair
forall a.
Hilite a =>
TopLevelModuleName -> NameKinds -> a -> DelayedMerge RangePair
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 = DelayedMerge RangePair -> RangeMap Aspects
forall a b. Convert a b => a -> b
convert (DelayedMerge RangePair
constructorInfo DelayedMerge RangePair
-> DelayedMerge RangePair -> DelayedMerge RangePair
forall a. Semigroup a => a -> a -> a
<> DelayedMerge RangePair
nameInfo)
                       RangeMap Aspects -> RangeMap Aspects -> RangeMap Aspects
forall a. Semigroup a => a -> a -> a
<>
                     RangeMap Aspects
curTokens

    when updateState $ do
      stSyntaxInfo `modifyTCLens` 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 (RangeMap Aspects)
generateTokenInfo AbsolutePath
file =
  RangeFile -> [Char] -> TCMT IO (RangeMap Aspects)
generateTokenInfoFromSource RangeFile
rf ([Char] -> TCMT IO (RangeMap Aspects))
-> (Text -> [Char]) -> Text -> TCMT IO (RangeMap Aspects)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Char]
Text.unpack (Text -> TCMT IO (RangeMap Aspects))
-> TCMT IO Text -> TCMT IO (RangeMap Aspects)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
    PM Text -> TCMT IO Text
forall a. PM a -> TCM a
runPM (RangeFile -> PM Text
Pa.readFilePM RangeFile
rf)
  where
  -- 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.
  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.
  -> String
     -- ^ The file contents. Note that the file is /not/ read from
     -- disk.
  -> TCM HighlightingInfo
generateTokenInfoFromSource :: RangeFile -> [Char] -> TCMT IO (RangeMap Aspects)
generateTokenInfoFromSource RangeFile
file [Char]
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 -> String -> TCM HighlightingInfo
generateTokenInfoFromString :: Range' SrcFile -> [Char] -> TCMT IO (RangeMap Aspects)
generateTokenInfoFromString Range' SrcFile
r [Char]
_ | Range' SrcFile
r Range' SrcFile -> Range' SrcFile -> Bool
forall a. Eq a => a -> a -> Bool
== Range' SrcFile
forall a. Range' a
noRange = RangeMap Aspects -> TCMT IO (RangeMap Aspects)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return RangeMap Aspects
forall a. Monoid a => a
mempty
generateTokenInfoFromString Range' SrcFile
r [Char]
s = do
  PM (RangeMap Aspects) -> TCMT IO (RangeMap Aspects)
forall a. PM a -> TCM a
runPM (PM (RangeMap Aspects) -> TCMT IO (RangeMap Aspects))
-> PM (RangeMap Aspects) -> TCMT IO (RangeMap Aspects)
forall a b. (a -> b) -> a -> b
$ [Token] -> RangeMap Aspects
tokenHighlighting ([Token] -> RangeMap Aspects)
-> (([Token], Attributes) -> [Token])
-> ([Token], Attributes)
-> RangeMap Aspects
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Token], Attributes) -> [Token]
forall a b. (a, b) -> a
fst (([Token], Attributes) -> RangeMap Aspects)
-> PM ([Token], Attributes) -> PM (RangeMap Aspects)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          Parser [Token] -> Position -> [Char] -> PM ([Token], Attributes)
forall a. Parser a -> Position -> [Char] -> PM (a, Attributes)
Pa.parsePosString Parser [Token]
Pa.tokensParser Position
p [Char]
s
  where
    Just Position
p = Range' SrcFile -> Maybe Position
forall a. Range' a -> Maybe (Position' a)
P.rStart Range' SrcFile
r

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

  tokenToHI :: T.Token -> HighlightingInfoBuilder
  tokenToHI :: Token -> DelayedMerge RangePair
tokenToHI (T.TokKeyword Keyword
T.KwForall Interval' SrcFile
i)       = Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
Symbol (Interval' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Interval' SrcFile
i)
  tokenToHI (T.TokKeyword Keyword
T.KwREWRITE Interval' SrcFile
_)      = DelayedMerge RangePair
forall a. Monoid a => a
mempty  -- #4361, REWRITE is not always a Keyword
  tokenToHI (T.TokKeyword Keyword
_ Interval' SrcFile
i)                = Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
Keyword (Interval' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Interval' SrcFile
i)
  tokenToHI (T.TokSymbol Symbol
T.SymQuestionMark Interval' SrcFile
i) = Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
Hole (Interval' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Interval' SrcFile
i)
  tokenToHI (T.TokSymbol  Symbol
_ Interval' SrcFile
i)                = Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
Symbol (Interval' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Interval' SrcFile
i)
  tokenToHI (T.TokComment (Interval' SrcFile
i, [Char]
_))             = Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
Comment (Interval' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Interval' SrcFile
i)
  tokenToHI (T.TokTeX (Interval' SrcFile
i, [Char]
_))                 = Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
Background (Interval' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Interval' SrcFile
i)
  tokenToHI (T.TokMarkup (Interval' SrcFile
i, [Char]
_))              = Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
Markup (Interval' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Interval' SrcFile
i)
  tokenToHI (T.TokId {})                      = DelayedMerge RangePair
forall a. Monoid a => a
mempty
  tokenToHI (T.TokQId {})                     = DelayedMerge RangePair
forall a. Monoid a => a
mempty
  tokenToHI (T.TokString (Interval' SrcFile
i,[Char]
s))               = Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
Pragma (Interval' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Interval' SrcFile
i)
  tokenToHI (T.TokDummy {})                   = DelayedMerge RangePair
forall a. Monoid a => a
mempty
  tokenToHI (T.TokEOF {})                     = DelayedMerge RangePair
forall a. Monoid a => a
mempty
  tokenToHI (T.TokQual QualifiableToken
cls [(Interval' SrcFile, [Char])]
_ Interval' SrcFile
i)         = case QualifiableToken
cls of
    QualifiableToken
T.QualDo           -> Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
Keyword (Interval' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Interval' SrcFile
i)
    T.QualOpenIdiom{}  -> Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
Symbol  (Interval' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Interval' SrcFile
i)
    T.QualEmptyIdiom{} -> Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
Symbol  (Interval' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Interval' SrcFile
i)
  tokenToHI (T.TokLiteral (Ranged Range' SrcFile
r Literal
l)) = case Literal
l of
    L.LitNat{}    -> Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
Number Range' SrcFile
r
    L.LitWord64{} -> Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
Number Range' SrcFile
r
    L.LitFloat{}  -> Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
Number Range' SrcFile
r
    L.LitString{} -> Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
String Range' SrcFile
r
    L.LitChar{}   -> Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
String Range' SrcFile
r
    L.LitQName{}  -> Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
String Range' SrcFile
r
    L.LitMeta{}   -> Aspect -> Range' SrcFile -> DelayedMerge RangePair
forall {m}.
IsBasicRangeMap Aspects m =>
Aspect -> Range' SrcFile -> m
aToF Aspect
String Range' SrcFile
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 <- Lens' TCState (HashMap QName Definition)
-> TCMT IO (HashMap QName Definition)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Lens' TCState (HashMap QName Definition)
 -> TCMT IO (HashMap QName Definition))
-> Lens' 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{} -> Lens' TCState (HashMap QName Definition)
-> TCMT IO (HashMap QName Definition)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Lens' TCState (HashMap QName Definition)
 -> TCMT IO (HashMap QName Definition))
-> Lens' 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{} -> Lens' TCState (Map QName PatternSynDefn)
-> TCMT IO (Map QName PatternSynDefn)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map QName PatternSynDefn -> f (Map QName PatternSynDefn))
-> TCState -> f TCState
Lens' 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. 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. 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. 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.
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 -> TCMT IO (DelayedMerge RangePair)
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]
-> TCMT IO (DelayedMerge RangePair)
-> (IntervalWithoutFile
    -> [IntervalWithoutFile] -> TCMT IO (DelayedMerge RangePair))
-> TCMT IO (DelayedMerge RangePair)
forall a b. [a] -> b -> (a -> [a] -> b) -> b
caseList (Range' SrcFile -> [IntervalWithoutFile]
forall a. Range' a -> [IntervalWithoutFile]
P.rangeIntervals (Range' SrcFile -> [IntervalWithoutFile])
-> Range' SrcFile -> [IntervalWithoutFile]
forall a b. (a -> b) -> a -> b
$ Declaration -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Declaration
decl)
           (DelayedMerge RangePair -> TCMT IO (DelayedMerge RangePair)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return DelayedMerge RangePair
forall a. Monoid a => a
mempty) ((IntervalWithoutFile
  -> [IntervalWithoutFile] -> TCMT IO (DelayedMerge RangePair))
 -> TCMT IO (DelayedMerge RangePair))
-> (IntervalWithoutFile
    -> [IntervalWithoutFile] -> TCMT IO (DelayedMerge RangePair))
-> TCMT IO (DelayedMerge RangePair)
forall a b. (a -> b) -> a -> b
$ \ IntervalWithoutFile
i [IntervalWithoutFile]
is -> do
    let start :: Int
start = Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> Int) -> Word32 -> Int
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 :: Int
end   = Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> Int) -> Word32 -> Int
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 <- Lens' TCState (IntMap DisambiguatedName)
-> TCMT IO (IntMap DisambiguatedName)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (IntMap DisambiguatedName -> f (IntMap DisambiguatedName))
-> TCState -> f TCState
Lens' 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' SrcFile -> TCM ()
printSyntaxInfo Range' SrcFile
r = do
  syntaxInfo <- Lens' TCState (RangeMap Aspects) -> TCMT IO (RangeMap Aspects)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (RangeMap Aspects -> f (RangeMap Aspects)) -> TCState -> f TCState
Lens' TCState (RangeMap Aspects)
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 -> RangeMap Aspects -> TCM ()
forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> RangeMap Aspects -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (RangeMap Aspects -> TCM ())
-> (DelayedMerge RangePair -> RangeMap Aspects)
-> DelayedMerge RangePair
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DelayedMerge RangePair -> RangeMap Aspects
forall a b. Convert a b => a -> b
convert (DelayedMerge RangePair -> TCM ())
-> TCMT IO (DelayedMerge RangePair) -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
    TCErr -> TCMT IO (DelayedMerge RangePair)
errorHighlighting TCErr
e

-- | Generate highlighting for error.

errorHighlighting :: TCErr -> TCM HighlightingInfoBuilder
errorHighlighting :: TCErr -> TCMT IO (DelayedMerge RangePair)
errorHighlighting TCErr
e = [TCMT IO (DelayedMerge RangePair)]
-> TCMT IO (DelayedMerge RangePair)
forall a. Monoid a => [a] -> a
mconcat
  [ TCErr -> TCMT IO (DelayedMerge RangePair)
extraErrorHighlighting TCErr
e
  , Range' SrcFile -> [Char] -> DelayedMerge RangePair
errorHighlighting' (TCErr -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange TCErr
e) ([Char] -> DelayedMerge RangePair)
-> TCMT IO [Char] -> TCMT IO (DelayedMerge RangePair)
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' SrcFile -> [Char] -> DelayedMerge RangePair
errorHighlighting' Range' SrcFile
r [Char]
s = [DelayedMerge RangePair] -> DelayedMerge RangePair
forall a. Monoid a => [a] -> a
mconcat
  [ -- Erase previous highlighting.
    Ranges -> Aspects -> DelayedMerge RangePair
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range' SrcFile -> Ranges
rToR (Range' SrcFile -> Ranges) -> Range' SrcFile -> Ranges
forall a b. (a -> b) -> a -> b
$ Range' SrcFile -> Range' SrcFile
forall a. Range' a -> Range' a
P.continuousPerLine Range' SrcFile
r) Aspects
forall a. Monoid a => a
mempty
  , -- Print new highlighting.
    Ranges -> Aspects -> DelayedMerge RangePair
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range' SrcFile -> Ranges
rToR Range' SrcFile
r)
         (Aspects -> DelayedMerge RangePair)
-> Aspects -> DelayedMerge RangePair
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 -> TCMT IO (DelayedMerge RangePair)
extraErrorHighlighting = \case
  TypeError CallStack
_ TCState
_ Closure TypeError
cl ->
    case Closure TypeError -> TypeError
forall a. Closure a -> a
clValue Closure TypeError
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.)
      ClashingDefinition QName
_ ClashingName
y Maybe NiceDeclaration
_ -> DelayedMerge RangePair -> TCMT IO (DelayedMerge RangePair)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DelayedMerge RangePair -> TCMT IO (DelayedMerge RangePair))
-> DelayedMerge RangePair -> TCMT IO (DelayedMerge RangePair)
forall a b. (a -> b) -> a -> b
$ Range' SrcFile -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting (Range' SrcFile -> DelayedMerge RangePair)
-> Range' SrcFile -> DelayedMerge RangePair
forall a b. (a -> b) -> a -> b
$ QName -> Range' SrcFile
forall a. HasNameBindingSite a => a -> Range' SrcFile
I.nameBindingSite (QName -> Range' SrcFile) -> QName -> Range' SrcFile
forall a b. (a -> b) -> a -> b
$ ClashingName -> QName
clashingQName ClashingName
y
      ShadowedModule Name
x List1 ModuleName
ms      -> Range' SrcFile -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting (Range' SrcFile -> DelayedMerge RangePair)
-> ((TCMT IO Doc, Range' SrcFile) -> Range' SrcFile)
-> (TCMT IO Doc, Range' SrcFile)
-> DelayedMerge RangePair
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TCMT IO Doc, Range' SrcFile) -> Range' SrcFile
forall a b. (a, b) -> b
snd ((TCMT IO Doc, Range' SrcFile) -> DelayedMerge RangePair)
-> TCMT IO (TCMT IO Doc, Range' SrcFile)
-> TCMT IO (DelayedMerge RangePair)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> List1 ModuleName -> TCMT IO (TCMT IO Doc, Range' SrcFile)
forall (m :: * -> *).
MonadPretty m =>
Name -> List1 ModuleName -> m (m Doc, Range' SrcFile)
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.
      TypeError
_ -> TCMT IO (DelayedMerge RangePair)
forall a. Monoid a => a
mempty
  TCErr
_ -> TCMT IO (DelayedMerge RangePair)
forall a. Monoid a => a
mempty

-- | Highlighting for warnings that are considered fatal.

errorWarningHighlighting :: HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting :: forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting a
w =
  Ranges -> Aspects -> DelayedMerge RangePair
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range' SrcFile -> Ranges
rToR (Range' SrcFile -> Ranges) -> Range' SrcFile -> Ranges
forall a b. (a -> b) -> a -> b
$ Range' SrcFile -> Range' SrcFile
forall a. Range' a -> Range' a
P.continuousPerLine (Range' SrcFile -> Range' SrcFile)
-> Range' SrcFile -> Range' SrcFile
forall a b. (a -> b) -> a -> b
$ a -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange a
w) (Aspects -> DelayedMerge RangePair)
-> Aspects -> DelayedMerge RangePair
forall a b. (a -> b) -> a -> b
$
    Aspects
parserBased { otherAspects = Set.singleton ErrorWarning }
-- errorWarningHighlighting w = errorHighlighting' (getRange w) ""
  -- MonadPretty not available here, so, no tooltip.
  -- errorHighlighting' (getRange w) . render <$> TCM.prettyWarning (tcWarning w)

-- | Generate syntax highlighting for warnings.

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

warningHighlighting' :: Bool -- ^ should we generate highlighting for unsolved metas and constrains?
                     -> TCWarning -> HighlightingInfoBuilder
warningHighlighting' :: Bool -> TCWarning -> DelayedMerge RangePair
warningHighlighting' Bool
b TCWarning
w = case TCWarning -> Warning
tcWarning TCWarning
w of
  TerminationIssue List1 TerminationError
terrs     -> List1 TerminationError -> DelayedMerge RangePair
terminationErrorHighlighting List1 TerminationError
terrs
  NotStrictlyPositive QName
d Seq OccursWhere
ocs  -> QName -> Seq OccursWhere -> DelayedMerge RangePair
positivityErrorHighlighting QName
d Seq OccursWhere
ocs
  ConstructorDoesNotFitInData DataOrRecord_
_dataOrRecord QName
c Sort
_s1 Sort
_s2 TCErr
_err -> Range' SrcFile -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting (Range' SrcFile -> DelayedMerge RangePair)
-> Range' SrcFile -> DelayedMerge RangePair
forall a b. (a -> b) -> a -> b
$
     QName -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange QName
c Range' SrcFile -> Range' SrcFile -> Range' SrcFile
forall a. Null a => a -> a -> a
`catchNull` TCWarning -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange TCWarning
w
  CoinductiveEtaRecord QName
_x    -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  UnguardedEtaRecordW QName
_x      -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting TCWarning
w
  -- #3965 highlight each unreachable clause independently: they
  -- may be interleaved with actually reachable clauses!
  UnreachableClauses QName
_ List1 (Range' SrcFile)
rs    -> (Range' SrcFile -> DelayedMerge RangePair)
-> List1 (Range' SrcFile) -> DelayedMerge RangePair
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' SrcFile -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting List1 (Range' SrcFile)
rs
  CoverageIssue{}            -> Range' SrcFile -> DelayedMerge RangePair
coverageErrorHighlighting (Range' SrcFile -> DelayedMerge RangePair)
-> Range' SrcFile -> DelayedMerge RangePair
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange TCWarning
w
  CoverageNoExactSplit{}     -> Range' SrcFile -> DelayedMerge RangePair
catchallHighlighting (Range' SrcFile -> DelayedMerge RangePair)
-> Range' SrcFile -> DelayedMerge RangePair
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange TCWarning
w
  InlineNoExactSplit{}       -> Range' SrcFile -> DelayedMerge RangePair
catchallHighlighting (Range' SrcFile -> DelayedMerge RangePair)
-> Range' SrcFile -> DelayedMerge RangePair
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange TCWarning
w
  UnsolvedConstraints List1 ProblemConstraint
cs     -> if Bool
b then [Ranges] -> Constraints -> DelayedMerge RangePair
constraintsHighlighting [] (Constraints -> DelayedMerge RangePair)
-> Constraints -> DelayedMerge RangePair
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 DelayedMerge RangePair
forall a. Monoid a => a
mempty
  UnsolvedMetaVariables Set1 (Range' SrcFile)
rs   -> if Bool
b then [Range' SrcFile] -> DelayedMerge RangePair
metasHighlighting          ([Range' SrcFile] -> DelayedMerge RangePair)
-> [Range' SrcFile] -> DelayedMerge RangePair
forall a b. (a -> b) -> a -> b
$ Set1 (Range' SrcFile) -> [Range' SrcFile]
forall a. NESet a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Set1 (Range' SrcFile)
rs else DelayedMerge RangePair
forall a. Monoid a => a
mempty
  AbsurdPatternRequiresAbsentRHS{} -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  DuplicateRecordDirective{}   -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  ModuleDoesntExport QName
_ [Name]
_ [Name]
_ List1 ImportedName
xs  -> (ImportedName -> DelayedMerge RangePair)
-> List1 ImportedName -> DelayedMerge RangePair
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 -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting List1 ImportedName
xs
  DuplicateUsing List1 ImportedName
xs            -> (ImportedName -> DelayedMerge RangePair)
-> List1 ImportedName -> DelayedMerge RangePair
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 -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting List1 ImportedName
xs
  FixityInRenamingModule List1 (Range' SrcFile)
rs    -> (Range' SrcFile -> DelayedMerge RangePair)
-> List1 (Range' SrcFile) -> DelayedMerge RangePair
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' SrcFile -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting List1 (Range' SrcFile)
rs
  -- expanded catch-all case to get a warning for new constructors
  CantGeneralizeOverSorts{}  -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  UnsolvedInteractionMetas{} -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  InteractionMetaBoundaries{} -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  OldBuiltin{}                -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  BuiltinDeclaresIdentifier{} -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  EmptyRewritePragma{}       -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  EmptyWhere{}               -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  -- TODO: linearity
  -- FixingQuantity _ q _       -> if null r then cosmeticHighlighting w else deadcodeHighlighting r
  --   where r = getRange q
  FixingRelevance [Char]
_ Relevance
q Relevance
_      -> if Range' SrcFile -> Bool
forall a. Null a => a -> Bool
null Range' SrcFile
r then TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
cosmeticProblemHighlighting TCWarning
w else Range' SrcFile -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting Range' SrcFile
r
    where r :: Range' SrcFile
r = Relevance -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Relevance
q
  FixingCohesion [Char]
_ Cohesion
q Cohesion
_       -> if Range' SrcFile -> Bool
forall a. Null a => a -> Bool
null Range' SrcFile
r then TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
cosmeticProblemHighlighting TCWarning
w else Range' SrcFile -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting Range' SrcFile
r
    where r :: Range' SrcFile
r = Cohesion -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Cohesion
q
  FixingPolarity [Char]
_ PolarityModality
q PolarityModality
_       -> if Range' SrcFile -> Bool
forall a. Null a => a -> Bool
null Range' SrcFile
r then TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
cosmeticProblemHighlighting TCWarning
w else Range' SrcFile -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting Range' SrcFile
r
    where r :: Range' SrcFile
r = PolarityModality -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange PolarityModality
q
  IgnoringRew [Char]
_ RewriteAnn
q            -> if Range' SrcFile -> Bool
forall a. Null a => a -> Bool
null Range' SrcFile
r then TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
cosmeticProblemHighlighting TCWarning
w else Range' SrcFile -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting Range' SrcFile
r
    where r :: Range' SrcFile
r = RewriteAnn -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange RewriteAnn
q
  IllformedAsClause{}        -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  UnusedImports ModuleName
m Maybe (List1 AbstractName)
Nothing    -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  UnusedImports ModuleName
m Maybe (List1 AbstractName)
xs         -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
cosmeticProblemHighlighting TCWarning
w DelayedMerge RangePair
-> DelayedMerge RangePair -> DelayedMerge RangePair
forall a. Semigroup a => a -> a -> a
<> (List1 AbstractName -> DelayedMerge RangePair)
-> Maybe (List1 AbstractName) -> DelayedMerge RangePair
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 -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting Maybe (List1 AbstractName)
xs
  UselessPragma Range' SrcFile
r Doc
_          -> Range' SrcFile -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting Range' SrcFile
r
  UselessPublic{}            -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  UselessHiding List1 ImportedName
xs           -> (ImportedName -> DelayedMerge RangePair)
-> List1 ImportedName -> DelayedMerge RangePair
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 -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting List1 ImportedName
xs
  UselessInline{}            -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  UselessPatternDeclarationForRecord{} -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  UselessTactic{}            -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  ClashesViaRenaming NameOrModule
_ Set1 Name
xs    -> (Name -> DelayedMerge RangePair)
-> Set1 Name -> DelayedMerge RangePair
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 -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
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 -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
instanceProblemHighlighting KwRange
kwr DelayedMerge RangePair
-> DelayedMerge RangePair -> DelayedMerge RangePair
forall a. Semigroup a => a -> a -> a
<> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
instanceProblemHighlighting TCWarning
w
  InstanceWithExplicitArg KwRange
kwr QName
_ -> KwRange -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
instanceProblemHighlighting KwRange
kwr DelayedMerge RangePair
-> DelayedMerge RangePair -> DelayedMerge RangePair
forall a. Semigroup a => a -> a -> a
<> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
instanceProblemHighlighting TCWarning
w
  InstanceNoOutputTypeName{}   -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
instanceProblemHighlighting TCWarning
w
  InstanceArgWithExplicitArg{} -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
instanceProblemHighlighting TCWarning
w
  InversionDepthReached{}    -> DelayedMerge RangePair
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 -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting TCWarning
w
  SafeFlagPostulate{}                   -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting TCWarning
w
  SafeFlagPragma{}                      -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting TCWarning
w
  Warning
SafeFlagWithoutKFlagPrimEraseEquality -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting TCWarning
w
  InfectiveImport{}                     -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting TCWarning
w
  CoInfectiveImport{}                   -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting TCWarning
w
  InvalidDisplayForm{}                  -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  UnusedVariablesInDisplayForm List1 Name
xs       -> (Name -> DelayedMerge RangePair)
-> List1 Name -> DelayedMerge RangePair
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 -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting List1 Name
xs
  Warning
ShouldBeEtaRecordPattern              -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting TCWarning
w
  TooManyArgumentsToSort QName
_ NonEmpty (NamedArg Expr)
args         -> NonEmpty (NamedArg Expr) -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting NonEmpty (NamedArg Expr)
args
  Warning
RewritesNothing                       -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
cosmeticProblemHighlighting TCWarning
w
  RecursiveRecordNeedsInductivity QName
_x    -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting TCWarning
w
  WithClauseProjectionFixityMismatch Arg (Named_ Pattern)
p ProjOrigin
_ NamedArg DeBruijnPattern
_ ProjOrigin
_ -> Arg (Named_ Pattern) -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
cosmeticProblemHighlighting Arg (Named_ Pattern)
p
  Warning
WithoutKFlagPrimEraseEquality -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  ConflictingPragmaOptions{} -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  DeprecationWarning{}       -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  UserWarning{}              -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  LibraryWarning{}           -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  ConfluenceCheckingIncompleteBecauseOfMeta{} -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
confluenceErrorHighlighting TCWarning
w
  ConfluenceForCubicalNotSupported{} -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  RewriteNonConfluent{}      -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
confluenceErrorHighlighting TCWarning
w
  RewriteMaybeNonConfluent{} -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
confluenceErrorHighlighting TCWarning
w
  RewriteAmbiguousRules{}    -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
confluenceErrorHighlighting TCWarning
w
  RewriteMissingRule{}       -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
confluenceErrorHighlighting TCWarning
w
  IllegalRewriteRule (GlobalRewrite Definition
x)  IllegalRewriteRuleReason
_ -> QName -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting (Definition -> QName
defName Definition
x)
  IllegalRewriteRule (LocalRewrite Context
_ Maybe Name
x Type
_) IllegalRewriteRuleReason
_ -> Maybe Name -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting Maybe Name
x
  NotARewriteRule QName
x IsAmbiguous
_        -> QName -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting QName
x
  InferredLocalRewrite MetaId
_ Term
_   -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  PragmaCompileErased{}      -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  PragmaCompileList{}        -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  PragmaCompileMaybe{}       -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  PragmaCompileWrong{}       -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  PragmaCompileWrongName{}   -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  PragmaCompileUnparsable{}  -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  PragmaExpectsDefinedSymbol{}
                             -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  PragmaExpectsUnambiguousConstructorOrFunction{}
                             -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  PragmaExpectsUnambiguousProjectionOrFunction{}
                             -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  UnknownJSPrimitive{}       -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  NoMain{}                   -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  NotInScopeW{}              -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  UnsupportedIndexedMatch{}  -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  AsPatternShadowsConstructorOrPatternSynonym{}
                             -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  PatternShadowsConstructor{}-> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting TCWarning
w  -- or mempty ?
  PlentyInHardCompileTimeMode QωOrigin
o
                             -> QωOrigin -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting QωOrigin
o
  RecordFieldWarning RecordFieldWarning
w       -> RecordFieldWarning -> DelayedMerge RangePair
recordFieldWarningHighlighting RecordFieldWarning
w
  OptionWarning OptionWarning
w            -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  ParseWarning ParseWarning
w             -> case ParseWarning
w of
    Pa.MisplacedAttributes{}      -> ParseWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting ParseWarning
w
    Pa.UnknownPolarity{}          -> ParseWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting ParseWarning
w
    Pa.UnknownAttribute{}         -> ParseWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting ParseWarning
w
    Pa.UnsupportedAttribute{}     -> ParseWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting ParseWarning
w
    Pa.MultipleAttributes{}       -> ParseWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting ParseWarning
w
    Pa.MismatchedBrackets{}       -> ParseWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting ParseWarning
w
    Pa.OverlappingTokensWarning{} -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
  MissingTypeSignatureForOpaque{} -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting TCWarning
w
  NotAffectedByOpaque{}           -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  UselessOpaque{}                 -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  UnfoldingWrongName QName
x            -> QName -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting QName
x
  UnfoldTransparentName QName
r         -> QName -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting QName
r
  FaceConstraintCannotBeHidden{}  -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w
  FaceConstraintCannotBeNamed{}   -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting TCWarning
w

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

  NicifierIssue (DeclarationWarning CallStack
_ DeclarationWarning'
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' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    DivergentModalityInClause{}      -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    EmptyAbstract{}                  -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    EmptyConstructor{}               -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    EmptyInstance{}                  -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    EmptyMacro{}                     -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    EmptyMutual{}                    -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    EmptyPostulate{}                 -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    EmptyPrimitive{}                 -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    EmptyPrivate{}                   -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    EmptyGeneralize{}                -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    EmptyField{}                     -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    EmptyPolarityPragma{}            -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    HiddenGeneralize{}               -> DelayedMerge RangePair
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' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    UselessImport{}                  -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    UselessInstance{}                -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    UselessMacro{}                   -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    UselessPrivate{}                 -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    InvalidCatchallPragma{}          -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    InvalidEtaEqualityPragma{}       -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    InvalidNoPositivityCheckPragma{} -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    InvalidNoUniverseCheckPragma{}   -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    InvalidTerminationCheckPragma{}  -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    InvalidCoverageCheckPragma{}     -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    InvalidConstructorBlock{}        -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    InvalidDataOrRecDefParameter{}   -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    InvalidTacticAttribute{}         -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    InvalidRewriteAttribute{}        -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting DeclarationWarning'
w
    OpenImportAbstract{}             -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
cosmeticProblemHighlighting DeclarationWarning'
w
    OpenImportPrivate{}              -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
cosmeticProblemHighlighting DeclarationWarning'
w
    SafeFlagInjective             {} -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting DeclarationWarning'
w
    SafeFlagNoCoverageCheck       {} -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting DeclarationWarning'
w
    SafeFlagNoPositivityCheck     {} -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting DeclarationWarning'
w
    SafeFlagNoUniverseCheck       {} -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting DeclarationWarning'
w
    SafeFlagNonTerminating        {} -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting DeclarationWarning'
w
    SafeFlagPolarity              {} -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting DeclarationWarning'
w
    SafeFlagTerminating           {} -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting DeclarationWarning'
w
    W.ShadowingInTelescope List1 (Name, List2 (Range' SrcFile))
nrs       -> ((Name, List2 (Range' SrcFile)) -> DelayedMerge RangePair)
-> List1 (Name, List2 (Range' SrcFile)) -> DelayedMerge RangePair
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' SrcFile) -> DelayedMerge RangePair
shadowingTelHighlighting (List2 (Range' SrcFile) -> DelayedMerge RangePair)
-> ((Name, List2 (Range' SrcFile)) -> List2 (Range' SrcFile))
-> (Name, List2 (Range' SrcFile))
-> DelayedMerge RangePair
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, List2 (Range' SrcFile)) -> List2 (Range' SrcFile)
forall a b. (a, b) -> b
snd)
                                          List1 (Name, List2 (Range' SrcFile))
nrs
    MissingDataDeclaration{}         -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
missingDefinitionHighlighting DeclarationWarning'
w
    MissingDefinitions{}             -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
missingDefinitionHighlighting DeclarationWarning'
w
    -- TODO: explore highlighting opportunities here!
    PolarityPragmasButNotPostulates{} -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
    PragmaNoTerminationCheck{}        -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
    PragmaCompiled{}                  -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting DeclarationWarning'
w
    UnknownFixityInMixfixDecl{}       -> DelayedMerge RangePair
forall a. Monoid a => a
mempty
    UnknownNamesInFixityDecl{}        -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting DeclarationWarning'
w
    UnknownNamesInPolarityPragmas{}   -> DeclarationWarning' -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting DeclarationWarning'
w

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

  -- Polarities
  TooManyPolarities QName
_x NonEmpty (Ranged Occurrence)
occs -> NonEmpty (Ranged Occurrence) -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
deadcodeHighlighting NonEmpty (Ranged Occurrence)
occs
  TopLevelPolarity{} -> TCWarning -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
errorWarningHighlighting TCWarning
w

recordFieldWarningHighlighting ::
  RecordFieldWarning -> HighlightingInfoBuilder
recordFieldWarningHighlighting :: RecordFieldWarning -> DelayedMerge RangePair
recordFieldWarningHighlighting = \case
  W.DuplicateFields List1 (Name, List1 (Range' SrcFile))
xrs      -> NonEmpty (DelayedMerge RangePair) -> DelayedMerge RangePair
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty (DelayedMerge RangePair) -> DelayedMerge RangePair)
-> NonEmpty (DelayedMerge RangePair) -> DelayedMerge RangePair
forall a b. (a -> b) -> a -> b
$ ((Name, List1 (Range' SrcFile)) -> DelayedMerge RangePair)
-> List1 (Name, List1 (Range' SrcFile))
-> NonEmpty (DelayedMerge RangePair)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (List1 (Range' SrcFile) -> DelayedMerge RangePair
dead (List1 (Range' SrcFile) -> DelayedMerge RangePair)
-> ((Name, List1 (Range' SrcFile)) -> List1 (Range' SrcFile))
-> (Name, List1 (Range' SrcFile))
-> DelayedMerge RangePair
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, List1 (Range' SrcFile)) -> List1 (Range' SrcFile)
forall a b. (a, b) -> b
snd) List1 (Name, List1 (Range' SrcFile))
xrs
  W.TooManyFields QName
_q [Name]
_ys List1 (Name, Range' SrcFile)
xrs -> List1 (Range' SrcFile) -> DelayedMerge RangePair
dead (List1 (Range' SrcFile) -> DelayedMerge RangePair)
-> List1 (Range' SrcFile) -> DelayedMerge RangePair
forall a b. (a -> b) -> a -> b
$ ((Name, Range' SrcFile) -> Range' SrcFile)
-> List1 (Name, Range' SrcFile) -> List1 (Range' SrcFile)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, Range' SrcFile) -> Range' SrcFile
forall a b. (a, b) -> b
snd List1 (Name, Range' SrcFile)
xrs
  where
  dead :: List1 Range -> HighlightingInfoBuilder
  dead :: List1 (Range' SrcFile) -> DelayedMerge RangePair
dead = NonEmpty (DelayedMerge RangePair) -> DelayedMerge RangePair
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty (DelayedMerge RangePair) -> DelayedMerge RangePair)
-> (List1 (Range' SrcFile) -> NonEmpty (DelayedMerge RangePair))
-> List1 (Range' SrcFile)
-> DelayedMerge RangePair
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Range' SrcFile -> DelayedMerge RangePair)
-> List1 (Range' SrcFile) -> NonEmpty (DelayedMerge RangePair)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Range' SrcFile -> DelayedMerge RangePair
forall a. HasRange a => a -> DelayedMerge RangePair
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 -> DelayedMerge RangePair
terminationErrorHighlighting List1 TerminationError
termErrs = DelayedMerge RangePair
functionDefs DelayedMerge RangePair
-> DelayedMerge RangePair -> DelayedMerge RangePair
forall a. Monoid a => a -> a -> a
`mappend` DelayedMerge RangePair
callSites
  where
    m :: Aspects
m            = Aspects
parserBased { otherAspects = Set.singleton TerminationProblem }
    functionDefs :: DelayedMerge RangePair
functionDefs = (QName -> DelayedMerge RangePair)
-> [QName] -> DelayedMerge RangePair
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 -> DelayedMerge RangePair
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range' SrcFile -> Ranges
rToR (Range' SrcFile -> Ranges) -> Range' SrcFile -> Ranges
forall a b. (a -> b) -> a -> b
$ QName -> Range' SrcFile
forall a. HasNameBindingSite a => a -> Range' SrcFile
nameBindingSite QName
x) Aspects
m) ([QName] -> DelayedMerge RangePair)
-> [QName] -> DelayedMerge RangePair
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 :: DelayedMerge RangePair
callSites    = (Range' SrcFile -> DelayedMerge RangePair)
-> [Range' SrcFile] -> DelayedMerge RangePair
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\Range' SrcFile
r -> Ranges -> Aspects -> DelayedMerge RangePair
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range' SrcFile -> Ranges
rToR Range' SrcFile
r) Aspects
m) ([Range' SrcFile] -> DelayedMerge RangePair)
-> [Range' SrcFile] -> DelayedMerge RangePair
forall a b. (a -> b) -> a -> b
$
                   (TerminationError -> [Range' SrcFile])
-> List1 TerminationError -> [Range' SrcFile]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((CallInfo -> Range' SrcFile) -> [CallInfo] -> [Range' SrcFile]
forall a b. (a -> b) -> [a] -> [b]
map CallInfo -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange ([CallInfo] -> [Range' SrcFile])
-> (TerminationError -> [CallInfo])
-> TerminationError
-> [Range' SrcFile]
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 -> DelayedMerge RangePair
positivityErrorHighlighting QName
q Seq OccursWhere
os =
  [Ranges] -> Aspects -> DelayedMerge RangePair
forall a hl.
(IsBasicRangeMap a hl, Monoid hl) =>
[Ranges] -> a -> hl
several (Range' SrcFile -> Ranges
rToR (Range' SrcFile -> Ranges) -> [Range' SrcFile] -> [Ranges]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange QName
q Range' SrcFile -> [Range' SrcFile] -> [Range' SrcFile]
forall a. a -> [a] -> [a]
: [Range' SrcFile]
rs) Aspects
m
  where
    rs :: [Range' SrcFile]
rs = (OccursWhere -> Range' SrcFile)
-> [OccursWhere] -> [Range' SrcFile]
forall a b. (a -> b) -> [a] -> [b]
map (\(OccursWhere Range' SrcFile
r Seq Where
_ Seq Where
_) -> Range' SrcFile
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 -> DelayedMerge RangePair
deadcodeHighlighting a
a = Ranges -> Aspects -> DelayedMerge RangePair
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range' SrcFile -> Ranges
rToR (Range' SrcFile -> Ranges) -> Range' SrcFile -> Ranges
forall a b. (a -> b) -> a -> b
$ Range' SrcFile -> Range' SrcFile
forall a. Range' a -> Range' a
P.continuous (Range' SrcFile -> Range' SrcFile)
-> Range' SrcFile -> Range' SrcFile
forall a b. (a -> b) -> a -> b
$ a -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange a
a) Aspects
m
  where m :: Aspects
m = Aspects
parserBased { otherAspects = Set.singleton Deadcode }

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

shadowingTelHighlighting :: List2 Range -> HighlightingInfoBuilder
shadowingTelHighlighting :: List2 (Range' SrcFile) -> DelayedMerge RangePair
shadowingTelHighlighting =
  -- we do not want to highlight the one variable in scope so we take
  -- the @init@ segment of the ranges in question
  (Range' SrcFile -> DelayedMerge RangePair)
-> List1 (Range' SrcFile) -> DelayedMerge RangePair
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' SrcFile
r -> Ranges -> Aspects -> DelayedMerge RangePair
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range' SrcFile -> Ranges
rToR (Range' SrcFile -> Ranges) -> Range' SrcFile -> Ranges
forall a b. (a -> b) -> a -> b
$ Range' SrcFile -> Range' SrcFile
forall a. Range' a -> Range' a
P.continuous Range' SrcFile
r) Aspects
m) (List1 (Range' SrcFile) -> DelayedMerge RangePair)
-> (List2 (Range' SrcFile) -> List1 (Range' SrcFile))
-> List2 (Range' SrcFile)
-> DelayedMerge RangePair
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List2 (Range' SrcFile) -> List1 (Range' SrcFile)
forall a. List2 a -> List1 a
List2.init
  where
  m :: Aspects
m = Aspects
parserBased { otherAspects =
                      Set.singleton H.ShadowingInTelescope }

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

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

confluenceErrorHighlighting ::
  HasRange a => a -> HighlightingInfoBuilder
confluenceErrorHighlighting :: forall a. HasRange a => a -> DelayedMerge RangePair
confluenceErrorHighlighting a
a = Ranges -> Aspects -> DelayedMerge RangePair
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range' SrcFile -> Ranges
rToR (Range' SrcFile -> Ranges) -> Range' SrcFile -> Ranges
forall a b. (a -> b) -> a -> b
$ Range' SrcFile -> Range' SrcFile
forall a. Range' a -> Range' a
P.continuousPerLine (Range' SrcFile -> Range' SrcFile)
-> Range' SrcFile -> Range' SrcFile
forall a b. (a -> b) -> a -> b
$ a -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange a
a) Aspects
m
  where m :: Aspects
m = Aspects
parserBased { otherAspects = Set.singleton ConfluenceProblem }

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

missingDefinitionHighlighting ::
  HasRange a => a -> HighlightingInfoBuilder
missingDefinitionHighlighting :: forall a. HasRange a => a -> DelayedMerge RangePair
missingDefinitionHighlighting a
a = Ranges -> Aspects -> DelayedMerge RangePair
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range' SrcFile -> Ranges
rToR (Range' SrcFile -> Ranges) -> Range' SrcFile -> Ranges
forall a b. (a -> b) -> a -> b
$ Range' SrcFile -> Range' SrcFile
forall a. Range' a -> Range' a
P.continuousPerLine (Range' SrcFile -> Range' SrcFile)
-> Range' SrcFile -> Range' SrcFile
forall a b. (a -> b) -> a -> b
$ a -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
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 <- TCMT IO (DelayedMerge RangePair)
computeUnsolvedInfo

  printHighlightingInfo KeepHighlighting (convert info)

computeUnsolvedInfo :: TCM HighlightingInfoBuilder
computeUnsolvedInfo :: TCMT IO (DelayedMerge RangePair)
computeUnsolvedInfo = do
  (rs, metaInfo) <- TCM ([Ranges], DelayedMerge RangePair)
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], DelayedMerge RangePair)
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' SrcFile -> Ranges) -> [Range' SrcFile] -> [Ranges]
forall a b. (a -> b) -> [a] -> [b]
map (Range' SrcFile -> Ranges
rToR (Range' SrcFile -> Ranges)
-> (Range' SrcFile -> Range' SrcFile) -> Range' SrcFile -> Ranges
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range' SrcFile -> Range' SrcFile
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' SrcFile] -> DelayedMerge RangePair
metasHighlighting = [Ranges] -> DelayedMerge RangePair
metasHighlighting' ([Ranges] -> DelayedMerge RangePair)
-> ([Range' SrcFile] -> [Ranges])
-> [Range' SrcFile]
-> DelayedMerge RangePair
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Range' SrcFile -> Ranges) -> [Range' SrcFile] -> [Ranges]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Range' SrcFile -> Ranges
rToR (Range' SrcFile -> Ranges)
-> (Range' SrcFile -> Range' SrcFile) -> Range' SrcFile -> Ranges
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range' SrcFile -> Range' SrcFile
forall a. Range' a -> Range' a
P.continuousPerLine)

metasHighlighting' :: [Ranges] -> HighlightingInfoBuilder
metasHighlighting' :: [Ranges] -> DelayedMerge RangePair
metasHighlighting' [Ranges]
rs =
  [Ranges] -> Aspects -> DelayedMerge RangePair
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] -> TCMT IO (DelayedMerge RangePair)
computeUnsolvedConstraints [Ranges]
ms = [Ranges] -> Constraints -> DelayedMerge RangePair
constraintsHighlighting [Ranges]
ms (Constraints -> DelayedMerge RangePair)
-> TCMT IO Constraints -> TCMT IO (DelayedMerge RangePair)
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 -> DelayedMerge RangePair
constraintsHighlighting [Ranges]
ms Constraints
cs =
  [Ranges] -> Aspects -> DelayedMerge RangePair
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' SrcFile -> Ranges) -> [Range' SrcFile] -> [Ranges]
forall a b. (a -> b) -> [a] -> [b]
map (Range' SrcFile -> Ranges
rToR (Range' SrcFile -> Ranges)
-> (Range' SrcFile -> Range' SrcFile) -> Range' SrcFile -> Ranges
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range' SrcFile -> Range' SrcFile
forall a. Range' a -> Range' a
P.continuousPerLine) [Range' SrcFile]
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' SrcFile]
rs = ((Closure Constraint -> Maybe (Range' SrcFile))
-> [Closure Constraint] -> [Range' SrcFile]
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' SrcFile))
 -> [Range' SrcFile])
-> (Closure Constraint -> Maybe (Range' SrcFile))
-> [Range' SrcFile]
forall a b. (a -> b) -> a -> b
$ \case
    Closure{ clValue :: forall a. Closure a -> a
clValue = IsEmpty Range' SrcFile
r Type
t           } -> Range' SrcFile -> Maybe (Range' SrcFile)
forall a. a -> Maybe a
Just Range' SrcFile
r
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = ValueCmp{} } -> Range' SrcFile -> Maybe (Range' SrcFile)
forall a. a -> Maybe a
Just (Range' SrcFile -> Maybe (Range' SrcFile))
-> Range' SrcFile -> Maybe (Range' SrcFile)
forall a b. (a -> b) -> a -> b
$! Range' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange (Getting (Range' SrcFile) TCEnv (Range' SrcFile)
-> TCEnv -> Range' SrcFile
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Range' SrcFile) TCEnv (Range' SrcFile)
Lens' TCEnv (Range' SrcFile)
eRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = ElimCmp{}  } -> Range' SrcFile -> Maybe (Range' SrcFile)
forall a. a -> Maybe a
Just (Range' SrcFile -> Maybe (Range' SrcFile))
-> Range' SrcFile -> Maybe (Range' SrcFile)
forall a b. (a -> b) -> a -> b
$! Range' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange (Getting (Range' SrcFile) TCEnv (Range' SrcFile)
-> TCEnv -> Range' SrcFile
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Range' SrcFile) TCEnv (Range' SrcFile)
Lens' TCEnv (Range' SrcFile)
eRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = SortCmp{}  } -> Range' SrcFile -> Maybe (Range' SrcFile)
forall a. a -> Maybe a
Just (Range' SrcFile -> Maybe (Range' SrcFile))
-> Range' SrcFile -> Maybe (Range' SrcFile)
forall a b. (a -> b) -> a -> b
$! Range' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange (Getting (Range' SrcFile) TCEnv (Range' SrcFile)
-> TCEnv -> Range' SrcFile
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Range' SrcFile) TCEnv (Range' SrcFile)
Lens' TCEnv (Range' SrcFile)
eRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = LevelCmp{} } -> Range' SrcFile -> Maybe (Range' SrcFile)
forall a. a -> Maybe a
Just (Range' SrcFile -> Maybe (Range' SrcFile))
-> Range' SrcFile -> Maybe (Range' SrcFile)
forall a b. (a -> b) -> a -> b
$! Range' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange (Getting (Range' SrcFile) TCEnv (Range' SrcFile)
-> TCEnv -> Range' SrcFile
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Range' SrcFile) TCEnv (Range' SrcFile)
Lens' TCEnv (Range' SrcFile)
eRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = CheckSizeLtSat{} } -> Range' SrcFile -> Maybe (Range' SrcFile)
forall a. a -> Maybe a
Just (Range' SrcFile -> Maybe (Range' SrcFile))
-> Range' SrcFile -> Maybe (Range' SrcFile)
forall a b. (a -> b) -> a -> b
$! Range' SrcFile -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange (Getting (Range' SrcFile) TCEnv (Range' SrcFile)
-> TCEnv -> Range' SrcFile
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Range' SrcFile) TCEnv (Range' SrcFile)
Lens' TCEnv (Range' SrcFile)
eRange TCEnv
e)
    Closure Constraint
_ -> Maybe (Range' SrcFile)
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 Int -> (Int -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (Range' SrcFile -> Maybe Int
forall {b} {a}. Num b => Range' a -> Maybe b
start (Range' SrcFile -> Maybe Int) -> Range' SrcFile -> Maybe Int
forall a b. (a -> b) -> a -> b
$ QName -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange QName
q) ((Int -> TCM ()) -> TCM ()) -> (Int -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Int
i ->
    Lens' TCState (IntMap DisambiguatedName)
-> (IntMap DisambiguatedName -> IntMap DisambiguatedName) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens (IntMap DisambiguatedName -> f (IntMap DisambiguatedName))
-> TCState -> f TCState
Lens' TCState (IntMap DisambiguatedName)
stDisambiguatedNames ((IntMap DisambiguatedName -> IntMap DisambiguatedName) -> TCM ())
-> (IntMap DisambiguatedName -> IntMap DisambiguatedName) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Int
-> DisambiguatedName
-> IntMap DisambiguatedName
-> IntMap DisambiguatedName
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
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 } }