-- | 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 Control.Arrow (second)

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 (Semigroup(..))
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 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.Pretty as TCM
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Warnings ( raiseWarningsOnUsage, runPM )

import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Concrete.Definitions as W ( DeclarationWarning(..), DeclarationWarning'(..) )
import Agda.Syntax.Common (pattern Ranged)
import qualified Agda.Syntax.Common as Common
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, initWithDefault, last1 )
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.Utils.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 :: HighlightingInfo
h = forall a b. Convert a b => a -> b
convert forall a b. (a -> b) -> a -> b
$ Bool -> TCWarning -> HighlightingInfoBuilder
warningHighlighting' Bool
False TCWarning
tcwarn
  -- Highlighting for warnings coming from the Happy parser is placed
  -- together with token highlighting.
  case TCWarning -> Warning
tcWarning TCWarning
tcwarn of
    ParseWarning{} -> forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
modifyTCLens Lens' HighlightingInfo TCState
stTokens     (HighlightingInfo
h forall a. Semigroup a => a -> a -> a
<>)
    Warning
_              -> forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
modifyTCLens Lens' HighlightingInfo TCState
stSyntaxInfo (HighlightingInfo
h forall a. Semigroup a => a -> a -> a
<>)
  forall (tcm :: * -> *).
MonadTCEnv tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting HighlightingInfo
h

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

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

  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Key -> TCMT IO Doc -> m ()
reportSDoc [Char]
"import.iface.create" Key
15 forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
TCM.fwords
      ([Char]
"Generating syntax info for the following declaration " forall a. [a] -> [a] -> [a]
++
       case Level
hlLevel of
         Full   {} -> [Char]
"(final):"
         Partial{} -> [Char]
"(first approximation):")
      forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCM.$$
    forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
TCM.prettyA Declaration
decl

  forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode forall a b. (a -> b) -> a -> b
$ do
    NameKinds
kinds <- Level -> Declaration -> TCM NameKinds
nameKinds Level
hlLevel Declaration
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@.
    HighlightingInfoBuilder
constructorInfo <- case Level
hlLevel of
      Full{} -> TopLevelModuleName
-> NameKinds -> Declaration -> TCMT IO HighlightingInfoBuilder
generateConstructorInfo TopLevelModuleName
top NameKinds
kinds Declaration
decl
      Level
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty

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

    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Key -> TCMT IO Doc -> m ()
reportSDoc [Char]
"highlighting.warning" Key
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCM.hcat
      [ TCMT IO Doc
"current path = "
      , forall b a. b -> (a -> b) -> Maybe a -> b
Strict.maybe TCMT IO Doc
"(nothing)" (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
pretty) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
          Range -> SrcFile
P.rangeFile forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Range TCEnv
eRange
      ]

    -- Highlighting from the lexer and Happy parser:
    (HighlightingInfo
curTokens, HighlightingInfo
otherTokens) <-
      forall a. Range -> RangeMap a -> (RangeMap a, RangeMap a)
insideAndOutside (Range -> Range
rangeToRange (forall a. HasRange a => a -> Range
getRange Declaration
decl)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' HighlightingInfo TCState
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 :: HighlightingInfo
syntaxInfo = forall a b. Convert a b => a -> b
convert (HighlightingInfoBuilder
constructorInfo forall a. Semigroup a => a -> a -> a
<> HighlightingInfoBuilder
nameInfo)
                       forall a. Semigroup a => a -> a -> a
<>
                     HighlightingInfo
curTokens

    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
updateState forall a b. (a -> b) -> a -> b
$ do
      Lens' HighlightingInfo TCState
stSyntaxInfo forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` forall a. Monoid a => a -> a -> a
mappend HighlightingInfo
syntaxInfo
      Lens' HighlightingInfo TCState
stTokens     forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens`    HighlightingInfo
otherTokens

    forall (tcm :: * -> *).
MonadTCEnv tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting HighlightingInfo
syntaxInfo

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

generateTokenInfo :: AbsolutePath -> TCM HighlightingInfo
generateTokenInfo :: AbsolutePath -> TCM HighlightingInfo
generateTokenInfo AbsolutePath
file =
  RangeFile -> [Char] -> TCM HighlightingInfo
generateTokenInfoFromSource RangeFile
rf forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Char]
Text.unpack forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
    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 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] -> TCM HighlightingInfo
generateTokenInfoFromSource RangeFile
file [Char]
input =
  forall a. PM a -> TCM a
runPM forall a b. (a -> b) -> a -> b
$ [Token] -> HighlightingInfo
tokenHighlighting forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          forall a.
Show a =>
Parser a
-> RangeFile -> [Char] -> PM ((a, CohesionAttributes), FileType)
Pa.parseFile Parser [Token]
Pa.tokensParser RangeFile
file [Char]
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 -> [Char] -> TCM HighlightingInfo
generateTokenInfoFromString Range
r [Char]
_ | Range
r forall a. Eq a => a -> a -> Bool
== forall a. Range' a
noRange = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
generateTokenInfoFromString Range
r [Char]
s = do
  forall a. PM a -> TCM a
runPM forall a b. (a -> b) -> a -> b
$ [Token] -> HighlightingInfo
tokenHighlighting forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          forall a.
Parser a -> Position -> [Char] -> PM (a, CohesionAttributes)
Pa.parsePosString Parser [Token]
Pa.tokensParser Position
p [Char]
s
  where
    Just Position
p = forall a. Range' a -> Maybe (Position' a)
P.rStart Range
r

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

  tokenToHI :: T.Token -> HighlightingInfoBuilder
  tokenToHI :: Token -> HighlightingInfoBuilder
tokenToHI (T.TokKeyword Keyword
T.KwForall Interval
i)  = forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Symbol (forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokKeyword Keyword
T.KwREWRITE Interval
_) = forall a. Monoid a => a
mempty  -- #4361, REWRITE is not always a Keyword
  tokenToHI (T.TokKeyword Keyword
_ Interval
i)           = forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Keyword (forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokSymbol Symbol
T.SymQuestionMark Interval
i) = forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Hole (forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokSymbol  Symbol
_ Interval
i)                = forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Symbol (forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokLiteral (Ranged Range
r (L.LitNat    Integer
_))) = forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Number Range
r
  tokenToHI (T.TokLiteral (Ranged Range
r (L.LitWord64 Word64
_))) = forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Number Range
r
  tokenToHI (T.TokLiteral (Ranged Range
r (L.LitFloat  Double
_))) = forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Number Range
r
  tokenToHI (T.TokLiteral (Ranged Range
r (L.LitString Text
_))) = forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
String Range
r
  tokenToHI (T.TokLiteral (Ranged Range
r (L.LitChar   Char
_))) = forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
String Range
r
  tokenToHI (T.TokLiteral (Ranged Range
r (L.LitQName  QName
_))) = forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
String Range
r
  tokenToHI (T.TokLiteral (Ranged Range
r (L.LitMeta TopLevelModuleName
_ MetaId
_))) = forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
String Range
r
  tokenToHI (T.TokComment (Interval
i, [Char]
_))            = forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Comment (forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokTeX (Interval
i, [Char]
_))                = forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Background (forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokMarkup (Interval
i, [Char]
_))             = forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Markup (forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokId {})                     = forall a. Monoid a => a
mempty
  tokenToHI (T.TokQId {})                    = forall a. Monoid a => a
mempty
  tokenToHI (T.TokString (Interval
i,[Char]
s))              = forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
aToF Aspect
Pragma (forall a. HasRange a => a -> Range
getRange Interval
i)
  tokenToHI (T.TokDummy {})                  = forall a. Monoid a => a
mempty
  tokenToHI (T.TokEOF {})                    = forall a. Monoid a => a
mempty

-- | 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
  HashMap QName Definition
imported <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC forall a b. (a -> b) -> a -> b
$ Lens' Signature TCState
stImports forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' (HashMap QName Definition) Signature
sigDefinitions
  HashMap QName Definition
local    <- case Level
hlLevel of
    Full{} -> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC forall a b. (a -> b) -> a -> b
$ Lens' Signature TCState
stSignature forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' (HashMap QName Definition) Signature
sigDefinitions
    Level
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall k v. HashMap k v
HMap.empty
  Map QName PatternSynDefn
impPatSyns <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map QName PatternSynDefn) TCState
stPatternSynImports
  Map QName PatternSynDefn
locPatSyns <- case Level
hlLevel of
    Full{} -> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map QName PatternSynDefn) TCState
stPatternSyns
    Level
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 :: NameKindMap
syntax = NameKindBuilder -> NameKindMap -> NameKindMap
runBuilder (forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames Declaration
decl :: NameKindBuilder) forall k v. HashMap k v
HMap.empty
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \ QName
n -> forall a. (a -> a -> a) -> [Maybe a] -> Maybe a
unionsMaybeWith NameKind -> NameKind -> NameKind
mergeNameKind
    [ Defn -> NameKind
defnToKind forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
n HashMap QName Definition
local
    , NameKind
con forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
n Map QName PatternSynDefn
locPatSyns
    , Defn -> NameKind
defnToKind forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
n HashMap QName Definition
imported
    , NameKind
con forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
n Map QName PatternSynDefn
impPatSyns
    , forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
n NameKindMap
syntax
    ]
  where
  defnToKind :: TCM.Defn -> NameKind
  defnToKind :: Defn -> NameKind
defnToKind   TCM.Axiom{}                           = NameKind
Postulate
  defnToKind   TCM.DataOrRecSig{}                    = NameKind
Postulate
  defnToKind   TCM.GeneralizableVar{}                = NameKind
Generalizable
  defnToKind d :: Defn
d@TCM.Function{} | Defn -> Bool
isProperProjection Defn
d = NameKind
Field
                            | Bool
otherwise            = NameKind
Function
  defnToKind   TCM.Datatype{}                        = NameKind
Datatype
  defnToKind   TCM.Record{}                          = NameKind
Record
  defnToKind   TCM.Constructor{ conInd :: Defn -> Induction
TCM.conInd = Induction
i }       = Induction -> NameKind
Constructor Induction
i
  defnToKind   TCM.Primitive{}                       = NameKind
Primitive
  defnToKind   TCM.PrimitiveSort{}                   = NameKind
Primitive
  defnToKind   TCM.AbstractDefn{}                    = forall a. HasCallStack => a
__IMPOSSIBLE__

  con :: NameKind
  con :: NameKind
con = Induction -> NameKind
Constructor Induction
Common.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 forall a b. (a -> b) -> a -> b
$ NameKindMap -> NameKindMap
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameKindMap -> NameKindMap
g

instance Monoid (NameKindBuilder) where
  mempty :: NameKindBuilder
mempty = (NameKindMap -> NameKindMap) -> NameKindBuilder
NameKindBuilder forall a. a -> a
id
  mappend :: NameKindBuilder -> NameKindBuilder -> NameKindBuilder
mappend = 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 forall a b. (a -> b) -> a -> b
$
    forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
HMap.insertWith NameKind -> NameKind -> NameKind
mergeNameKind QName
q 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 HighlightingInfoBuilder
generateConstructorInfo TopLevelModuleName
top NameKinds
kinds Declaration
decl = do

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

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

    -- Return suitable syntax highlighting information.
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a.
Hilite a =>
TopLevelModuleName -> NameKinds -> a -> HighlightingInfoBuilder
runHighlighter TopLevelModuleName
top NameKinds
kinds) [DisambiguatedName]
constrs

printSyntaxInfo :: Range -> TCM ()
printSyntaxInfo :: Range -> TCM ()
printSyntaxInfo Range
r = do
  HighlightingInfo
syntaxInfo <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' HighlightingInfo TCState
stSyntaxInfo
  forall (tcm :: * -> *).
MonadTCEnv tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting
      (forall a. Range -> RangeMap a -> RangeMap a
restrictTo (Range -> Range
rangeToRange Range
r) HighlightingInfo
syntaxInfo)

-- | Prints syntax highlighting info for an error.

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

-- | Generate highlighting for error.

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

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

-- | Highlighting for warnings that are considered fatal.

errorWarningHighlighting :: HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting a
w =
  forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Range' a -> Range' a
P.continuousPerLine forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange a
w) forall a b. (a -> b) -> a -> b
$
    Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = forall a. a -> Set a
Set.singleton OtherAspect
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 -> HighlightingInfoBuilder
warningHighlighting = Bool -> TCWarning -> HighlightingInfoBuilder
warningHighlighting' Bool
True

warningHighlighting' :: Bool -- ^ should we generate highlighting for unsolved metas and constrains?
                     -> TCWarning -> HighlightingInfoBuilder
warningHighlighting' :: Bool -> TCWarning -> HighlightingInfoBuilder
warningHighlighting' Bool
b TCWarning
w = case TCWarning -> Warning
tcWarning TCWarning
w of
  TerminationIssue [TerminationError]
terrs     -> [TerminationError] -> HighlightingInfoBuilder
terminationErrorHighlighting [TerminationError]
terrs
  NotStrictlyPositive QName
d Seq OccursWhere
ocs  -> QName -> Seq OccursWhere -> HighlightingInfoBuilder
positivityErrorHighlighting QName
d Seq OccursWhere
ocs
  -- #3965 highlight each unreachable clause independently: they
  -- may be interleaved with actually reachable clauses!
  UnreachableClauses QName
_ [Range]
rs    -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting [Range]
rs
  CoverageIssue{}            -> Range -> HighlightingInfoBuilder
coverageErrorHighlighting forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange TCWarning
w
  CoverageNoExactSplit{}     -> Range -> HighlightingInfoBuilder
catchallHighlighting forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange TCWarning
w
  UnsolvedConstraints Constraints
cs     -> if Bool
b then [Ranges] -> Constraints -> HighlightingInfoBuilder
constraintsHighlighting [] Constraints
cs else forall a. Monoid a => a
mempty
  UnsolvedMetaVariables [Range]
rs   -> if Bool
b then [Range] -> HighlightingInfoBuilder
metasHighlighting [Range]
rs          else forall a. Monoid a => a
mempty
  AbsurdPatternRequiresNoRHS{} -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  ModuleDoesntExport{}         -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  DuplicateUsing List1 ImportedName
xs            -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting List1 ImportedName
xs
  FixityInRenamingModule List1 Range
rs    -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting List1 Range
rs
  -- expanded catch-all case to get a warning for new constructors
  CantGeneralizeOverSorts{}  -> forall a. Monoid a => a
mempty
  UnsolvedInteractionMetas{} -> forall a. Monoid a => a
mempty
  OldBuiltin{}               -> forall a. Monoid a => a
mempty
  EmptyRewritePragma{}       -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  EmptyWhere{}               -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  IllformedAsClause{}        -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  UselessPublic{}            -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  UselessHiding [ImportedName]
xs           -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting [ImportedName]
xs
  UselessInline{}            -> forall a. Monoid a => a
mempty
  UselessPatternDeclarationForRecord{} -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  ClashesViaRenaming NameOrModule
_ [Name]
xs    -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting [Name]
xs
    -- #4154, TODO: clashing renamings are not dead code, but introduce problems.
    -- Should we have a different color?
  WrongInstanceDeclaration{} -> forall a. Monoid a => a
mempty
  InstanceWithExplicitArg{}  -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  InstanceNoOutputTypeName{} -> forall a. Monoid a => a
mempty
  InstanceArgWithExplicitArg{} -> forall a. Monoid a => a
mempty
  InversionDepthReached{}    -> forall a. Monoid a => a
mempty
  NoGuardednessFlag{}        -> forall a. Monoid a => a
mempty
  GenericWarning{}           -> forall a. Monoid a => a
mempty
  GenericUseless Range
r Doc
_         -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting Range
r
  -- Andreas, 2020-03-21, issue #4456:
  -- Error warnings that do not have dedicated highlighting
  -- are highlighted as errors.
  GenericNonFatalError{}                -> forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  SafeFlagPostulate{}                   -> forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  SafeFlagPragma{}                      -> forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  Warning
SafeFlagNonTerminating                -> forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  Warning
SafeFlagTerminating                   -> forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  Warning
SafeFlagWithoutKFlagPrimEraseEquality -> forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  Warning
SafeFlagEta                           -> forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  Warning
SafeFlagInjective                     -> forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  Warning
SafeFlagNoCoverageCheck               -> forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  Warning
SafeFlagNoPositivityCheck             -> forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  Warning
SafeFlagPolarity                      -> forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  Warning
SafeFlagNoUniverseCheck               -> forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  InfectiveImport{}                     -> forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  CoInfectiveImport{}                   -> forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting TCWarning
w
  Warning
WithoutKFlagPrimEraseEquality -> forall a. Monoid a => a
mempty
  DeprecationWarning{}       -> forall a. Monoid a => a
mempty
  UserWarning{}              -> forall a. Monoid a => a
mempty
  LibraryWarning{}           -> forall a. Monoid a => a
mempty
  RewriteNonConfluent{}      -> forall a. HasRange a => a -> HighlightingInfoBuilder
confluenceErrorHighlighting TCWarning
w
  RewriteMaybeNonConfluent{} -> forall a. HasRange a => a -> HighlightingInfoBuilder
confluenceErrorHighlighting TCWarning
w
  RewriteAmbiguousRules{}    -> forall a. HasRange a => a -> HighlightingInfoBuilder
confluenceErrorHighlighting TCWarning
w
  RewriteMissingRule{}       -> forall a. HasRange a => a -> HighlightingInfoBuilder
confluenceErrorHighlighting TCWarning
w
  PragmaCompileErased{}      -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  NotInScopeW{}              -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  UnsupportedIndexedMatch{}  -> forall a. Monoid a => a
mempty
  AsPatternShadowsConstructorOrPatternSynonym{}
                             -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting TCWarning
w
  RecordFieldWarning RecordFieldWarning
w       -> RecordFieldWarning -> HighlightingInfoBuilder
recordFieldWarningHighlighting RecordFieldWarning
w
  ParseWarning ParseWarning
w             -> case ParseWarning
w of
    Pa.UnsupportedAttribute{}     -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting ParseWarning
w
    Pa.MultipleAttributes{}       -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting ParseWarning
w
    Pa.OverlappingTokensWarning{} -> forall a. Monoid a => a
mempty
  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{}             -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    EmptyAbstract{}                  -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    EmptyConstructor{}               -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    EmptyInstance{}                  -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    EmptyMacro{}                     -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    EmptyMutual{}                    -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    EmptyPostulate{}                 -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    EmptyPrimitive{}                 -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    EmptyPrivate{}                   -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    EmptyGeneralize{}                -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    EmptyField{}                     -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    HiddenGeneralize{}               -> 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{}                -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    UselessInstance{}                -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    UselessPrivate{}                 -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    InvalidNoPositivityCheckPragma{} -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    InvalidNoUniverseCheckPragma{}   -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    InvalidTerminationCheckPragma{}  -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    InvalidCoverageCheckPragma{}     -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    InvalidConstructor{}             -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    InvalidConstructorBlock{}        -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    InvalidRecordDirective{}         -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    OpenPublicAbstract{}             -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    OpenPublicPrivate{}              -> forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting DeclarationWarning'
w
    W.ShadowingInTelescope List1 (Name, List2 Range)
nrs       -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap
                                          (List2 Range -> HighlightingInfoBuilder
shadowingTelHighlighting forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)
                                          List1 (Name, List2 Range)
nrs
    MissingDeclarations{}            -> forall a. HasRange a => a -> HighlightingInfoBuilder
missingDefinitionHighlighting DeclarationWarning'
w
    MissingDefinitions{}             -> forall a. HasRange a => a -> HighlightingInfoBuilder
missingDefinitionHighlighting DeclarationWarning'
w
    -- TODO: explore highlighting opportunities here!
    InvalidCatchallPragma{}           -> forall a. Monoid a => a
mempty
    PolarityPragmasButNotPostulates{} -> forall a. Monoid a => a
mempty
    PragmaNoTerminationCheck{}        -> forall a. Monoid a => a
mempty
    PragmaCompiled{}                  -> forall a. HasRange a => a -> HighlightingInfoBuilder
errorWarningHighlighting DeclarationWarning'
w
    UnknownFixityInMixfixDecl{}       -> forall a. Monoid a => a
mempty
    UnknownNamesInFixityDecl{}        -> forall a. Monoid a => a
mempty
    UnknownNamesInPolarityPragmas{}   -> forall a. Monoid a => a
mempty

recordFieldWarningHighlighting ::
  RecordFieldWarning -> HighlightingInfoBuilder
recordFieldWarningHighlighting :: RecordFieldWarning -> HighlightingInfoBuilder
recordFieldWarningHighlighting = \case
  DuplicateFieldsWarning [(Name, Range)]
xrs      -> [(Name, Range)] -> HighlightingInfoBuilder
dead [(Name, Range)]
xrs
  TooManyFieldsWarning QName
_q [Name]
_ys [(Name, Range)]
xrs -> [(Name, Range)] -> HighlightingInfoBuilder
dead [(Name, Range)]
xrs
  where
  dead :: [(C.Name, Range)] -> HighlightingInfoBuilder
  dead :: [(Name, Range)] -> HighlightingInfoBuilder
dead = forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. HasRange a => a -> HighlightingInfoBuilder
deadcodeHighlighting
  -- Andreas, 2020-03-27 #3684: This variant seems to only highlight @x@:
  -- dead = mconcat . map f
  -- f (x, r) = deadcodeHighlighting (getRange x) `mappend` deadcodeHighlighting r

-- | Generate syntax highlighting for termination errors.

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

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

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

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

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

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

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

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

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

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

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

  forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (forall a b. Convert a b => a -> b
convert HighlightingInfoBuilder
info)

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

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ HighlightingInfoBuilder
metaInfo forall a. Monoid a => a -> a -> a
`mappend` HighlightingInfoBuilder
constraintInfo

-- | Generates syntax highlighting information for unsolved meta
-- variables.
--   Also returns ranges of unsolved or interaction metas.
computeUnsolvedMetaWarnings :: TCM ([Ranges], HighlightingInfoBuilder)
computeUnsolvedMetaWarnings :: TCM ([Ranges], HighlightingInfoBuilder)
computeUnsolvedMetaWarnings = do
  [MetaId]
is <- 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 -> TCMT IO Bool
notBlocked MetaId
m = Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Bool
isBlockedTerm MetaId
m
  let notHasTwin :: MetaId -> TCMT IO Bool
notHasTwin MetaId
m = Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Bool
hasTwinMeta MetaId
m
  [MetaId]
ms <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM MetaId -> TCMT IO Bool
notHasTwin forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM MetaId -> TCMT IO Bool
notBlocked forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas

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

  [Ranges]
rs <- [Range] -> [Ranges]
extend forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange ([MetaId]
ms forall a. Eq a => [a] -> [a] -> [a]
\\ [MetaId]
is)

  [Ranges]
rs' <- [Range] -> [Ranges]
extend forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange [MetaId]
is
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ([Ranges]
rs forall a. [a] -> [a] -> [a]
++ [Ranges]
rs', [Ranges] -> HighlightingInfoBuilder
metasHighlighting' [Ranges]
rs)

metasHighlighting :: [Range] -> HighlightingInfoBuilder
metasHighlighting :: [Range] -> HighlightingInfoBuilder
metasHighlighting [Range]
rs = [Ranges] -> HighlightingInfoBuilder
metasHighlighting' (forall a b. (a -> b) -> [a] -> [b]
map (Range -> Ranges
rToR forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => Range' a -> Range' a
P.continuousPerLine) [Range]
rs)

metasHighlighting' :: [Ranges] -> HighlightingInfoBuilder
metasHighlighting' :: [Ranges] -> HighlightingInfoBuilder
metasHighlighting' [Ranges]
rs = forall a hl.
(IsBasicRangeMap a hl, Monoid hl) =>
[Ranges] -> a -> hl
several [Ranges]
rs
                     forall a b. (a -> b) -> a -> b
$ Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = forall a. a -> Set a
Set.singleton OtherAspect
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 HighlightingInfoBuilder
computeUnsolvedConstraints [Ranges]
ms = [Ranges] -> Constraints -> HighlightingInfoBuilder
constraintsHighlighting [Ranges]
ms forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m Constraints
getAllConstraints

constraintsHighlighting ::
  [Ranges] -> Constraints -> HighlightingInfoBuilder
constraintsHighlighting :: [Ranges] -> Constraints -> HighlightingInfoBuilder
constraintsHighlighting [Ranges]
ms Constraints
cs =
  forall a hl.
(IsBasicRangeMap a hl, Monoid hl) =>
[Ranges] -> a -> hl
several (forall a. (a -> Bool) -> [a] -> [a]
filter Ranges -> Bool
noOverlap forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Range -> Ranges
rToR forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => Range' a -> Range' a
P.continuousPerLine) [Range]
rs)
          (Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = forall a. a -> Set a
Set.singleton OtherAspect
UnsolvedConstraint })
  where
  noOverlap :: Ranges -> Bool
noOverlap Ranges
r = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Ranges -> Ranges -> Bool
overlappings forall a b. (a -> b) -> a -> b
$ Ranges
r) forall a b. (a -> b) -> a -> b
$ [Ranges]
ms
  -- get ranges of interesting unsolved constraints
  rs :: [Range]
rs = (forall a b. (a -> Maybe b) -> [a] -> [b]
`mapMaybe` (forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> Closure Constraint
theConstraint Constraints
cs)) forall a b. (a -> b) -> a -> b
$ \case
    Closure{ clValue :: forall a. Closure a -> a
clValue = IsEmpty Range
r Type
t           } -> forall a. a -> Maybe a
Just Range
r
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = ValueCmp{} } -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = ElimCmp{}  } -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = SortCmp{}  } -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = LevelCmp{} } -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = CheckSizeLtSat{} } -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
    Closure Constraint
_ -> 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 :: Common.Induction -> A.QName -> TCM ()
storeDisambiguatedConstructor :: Induction -> QName -> TCM ()
storeDisambiguatedConstructor Induction
i = NameKind -> QName -> TCM ()
storeDisambiguatedName 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
  forall (m :: * -> *).
(MonadWarning m, ReadTCState m) =>
QName -> m ()
raiseWarningsOnUsage QName
q
  forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (forall {b} {a}. Num b => Range' a -> Maybe b
start forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange QName
q) forall a b. (a -> b) -> a -> b
$ \ Key
i ->
    forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
modifyTCLens Lens' (IntMap DisambiguatedName) TCState
stDisambiguatedNames forall a b. (a -> b) -> a -> b
$ forall a. Key -> a -> IntMap a -> IntMap a
IntMap.insert Key
i 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 = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Position' a -> Int32
P.posPos forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Name]
cxs forall a b. (a -> b) -> a -> b
$ \ Name
cx -> do
  forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((Name
cx forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
A.nameConcrete forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
A.qnameName) [QName]
axs) (forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall a b. (a -> b) -> a -> b
$ \ QName
ax -> do
    QName -> TCM ()
storeDisambiguatedField QName
ax{ qnameName :: Name
A.qnameName = (QName -> Name
A.qnameName QName
ax) { nameConcrete :: Name
A.nameConcrete = Name
cx } }