1
2-- | Generates data used for precise syntax highlighting.
3
4-- {-# OPTIONS_GHC -fwarn-unused-imports #-}  -- Semigroup import obsolete in later ghcs
5-- {-# OPTIONS_GHC -fwarn-unused-binds   #-}
6
7module Agda.Interaction.Highlighting.Generate
8  ( Level(..)
9  , generateAndPrintSyntaxInfo
10  , generateTokenInfo, generateTokenInfoFromSource
11  , generateTokenInfoFromString
12  , printSyntaxInfo
13  , printErrorInfo, errorHighlighting
14  , printUnsolvedInfo
15  , printHighlightingInfo
16  , highlightAsTypeChecked
17  , highlightWarning, warningHighlighting
18  , computeUnsolvedInfo
19  , storeDisambiguatedConstructor, storeDisambiguatedProjection
20  , disambiguateRecordFields
21  ) where
22
23import Prelude hiding (null)
24
25import Control.Monad
26import Control.Arrow (second)
27
28import qualified Data.Foldable as Fold
29import qualified Data.Map as Map
30import Data.Maybe
31import Data.List ((\\))
32import qualified Data.List as List
33import qualified Data.IntMap as IntMap
34import Data.HashMap.Strict (HashMap)
35import qualified Data.HashMap.Strict as HMap
36import Data.Semigroup (Semigroup(..))
37import Data.Sequence (Seq)
38import qualified Data.Set as Set
39import qualified Data.Text.Lazy as Text
40
41import Agda.Interaction.Response
42  ( RemoveTokenBasedHighlighting( KeepHighlighting ) )
43import Agda.Interaction.Highlighting.Precise as H
44import Agda.Interaction.Highlighting.Range
45  (rToR, rangeToRange, overlappings, Ranges)
46import Agda.Interaction.Highlighting.FromAbstract
47
48import qualified Agda.TypeChecking.Errors as TCM
49import Agda.TypeChecking.MetaVars (isBlockedTerm, hasTwinMeta)
50import Agda.TypeChecking.Monad
51  hiding (ModuleInfo, MetaInfo, Primitive, Constructor, Record, Function, Datatype)
52import qualified Agda.TypeChecking.Monad  as TCM
53import qualified Agda.TypeChecking.Pretty as TCM
54import Agda.TypeChecking.Positivity.Occurrence
55import Agda.TypeChecking.Warnings ( raiseWarningsOnUsage, runPM )
56
57import qualified Agda.Syntax.Abstract as A
58import Agda.Syntax.Concrete.Definitions as W ( DeclarationWarning(..), DeclarationWarning'(..) )
59import Agda.Syntax.Common (pattern Ranged)
60import qualified Agda.Syntax.Common as Common
61import qualified Agda.Syntax.Concrete.Name as C
62import qualified Agda.Syntax.Internal as I
63import qualified Agda.Syntax.Literal as L
64import qualified Agda.Syntax.Parser as Pa
65import qualified Agda.Syntax.Parser.Tokens as T
66import qualified Agda.Syntax.Position as P
67import Agda.Syntax.Position (Range, HasRange, getRange, noRange)
68
69import Agda.Syntax.Scope.Base     ( WithKind(..) )
70import Agda.Syntax.Abstract.Views ( KName, declaredNames )
71
72import Agda.Utils.FileName
73import Agda.Utils.List            ( caseList, initWithDefault, last1 )
74import Agda.Utils.List2           ( List2 )
75import qualified Agda.Utils.List2 as List2
76import Agda.Utils.Maybe
77import qualified Agda.Utils.Maybe.Strict as Strict
78import Agda.Utils.Null
79import Agda.Utils.Pretty
80import Agda.Utils.Singleton
81
82import Agda.Utils.Impossible
83
84-- | Highlighting levels.
85
86data Level
87  = Full
88    -- ^ Full highlighting. Should only be used after typechecking has
89    --   completed successfully.
90  | Partial
91    -- ^ Highlighting without disambiguation of overloaded
92    --   constructors.
93
94-- | Highlight a warning.
95--   We do not generate highlighting for unsolved metas and
96--   constraints, as that gets handled in bulk after typechecking.
97highlightWarning :: TCWarning -> TCM ()
98highlightWarning tcwarn = do
99  let h = convert $ warningHighlighting' False tcwarn
100  -- Highlighting for warnings coming from the Happy parser is placed
101  -- together with token highlighting.
102  case tcWarning tcwarn of
103    ParseWarning{} -> modifyTCLens stTokens     (h <>)
104    _              -> modifyTCLens stSyntaxInfo (h <>)
105  ifTopLevelAndHighlightingLevelIs NonInteractive $
106    printHighlightingInfo KeepHighlighting h
107
108-- | Generate syntax highlighting information for the given
109-- declaration, and (if appropriate) print it. If the boolean is
110-- 'True', then the state is additionally updated with the new
111-- highlighting info (in case of a conflict new info takes precedence
112-- over old info).
113--
114-- The procedure makes use of some of the highlighting info
115-- corresponding to 'stTokens' (that corresponding to the interval
116-- covered by the declaration). If the boolean is 'True', then this
117-- highlighting info is additionally removed from the data structure
118-- that 'stTokens' refers to.
119
120generateAndPrintSyntaxInfo
121  :: A.Declaration
122       -- ^ Declaration to highlight.
123  -> Level
124       -- ^ Amount of highlighting.
125  -> Bool
126       -- ^ Update the state?
127  -> TCM ()
128generateAndPrintSyntaxInfo decl _ _ | null $ getRange decl = return ()
129generateAndPrintSyntaxInfo decl hlLevel updateState = do
130  file <- getCurrentPath
131
132  reportSLn "import.iface.create" 15 $ concat
133    [ "Generating syntax info for "
134    , filePath file
135    , case hlLevel of
136        Full   {} -> " (final)."
137        Partial{} -> " (first approximation)."
138    ]
139
140  ignoreAbstractMode $ do
141    modMap <- sourceToModule
142    kinds  <- nameKinds hlLevel decl
143
144    -- After the code has been type checked more information may be
145    -- available for overloaded constructors, and
146    -- @generateConstructorInfo@ takes advantage of this information.
147    -- Note, however, that highlighting for overloaded constructors is
148    -- included also in @nameInfo@.
149    constructorInfo <- case hlLevel of
150      Full{} -> generateConstructorInfo modMap file kinds decl
151      _      -> return mempty
152
153    -- Main source of scope-checker generated highlighting:
154    let nameInfo = runHighlighter modMap file kinds decl
155
156    reportSDoc "highlighting.warning" 60 $ TCM.hcat
157      [ "current path = "
158      , Strict.maybe "(nothing)" (return . pretty) =<< do
159          P.rangeFile <$> viewTC eRange
160      ]
161
162    -- Highlighting from the lexer and Happy parser:
163    (curTokens, otherTokens) <-
164      insideAndOutside (rangeToRange (getRange decl)) <$> useTC stTokens
165
166    -- @constructorInfo@ needs
167    -- to be placed before @nameInfo@ since, when typechecking is done,
168    -- constructors are included in both lists. Finally the token
169    -- information is placed last since token highlighting is more
170    -- crude than the others.
171    let syntaxInfo = convert (constructorInfo <> nameInfo)
172                       <>
173                     curTokens
174
175    when updateState $ do
176      stSyntaxInfo `modifyTCLens` mappend syntaxInfo
177      stTokens     `setTCLens`    otherTokens
178
179    ifTopLevelAndHighlightingLevelIs NonInteractive $
180      printHighlightingInfo KeepHighlighting syntaxInfo
181
182-- | Generate and return the syntax highlighting information for the
183-- tokens in the given file.
184
185generateTokenInfo :: AbsolutePath -> TCM HighlightingInfo
186generateTokenInfo file =
187  generateTokenInfoFromSource file . Text.unpack =<<
188    runPM (Pa.readFilePM file)
189
190-- | Generate and return the syntax highlighting information for the
191-- tokens in the given file.
192
193generateTokenInfoFromSource
194  :: AbsolutePath
195     -- ^ The module to highlight.
196  -> String
197     -- ^ The file contents. Note that the file is /not/ read from
198     -- disk.
199  -> TCM HighlightingInfo
200generateTokenInfoFromSource file input =
201  runPM $ tokenHighlighting . fst <$> Pa.parseFile Pa.tokensParser file input
202
203-- | Generate and return the syntax highlighting information for the
204-- tokens in the given string, which is assumed to correspond to the
205-- given range.
206
207generateTokenInfoFromString :: Range -> String -> TCM HighlightingInfo
208generateTokenInfoFromString r _ | r == noRange = return mempty
209generateTokenInfoFromString r s = do
210  runPM $ tokenHighlighting <$> Pa.parsePosString Pa.tokensParser p s
211  where
212    Just p = P.rStart r
213
214-- | Compute syntax highlighting for the given tokens.
215tokenHighlighting :: [T.Token] -> HighlightingInfo
216tokenHighlighting = convert . mconcat . map tokenToHI
217  where
218  -- Converts an aspect and a range to a file.
219  aToF a r = H.singleton (rToR r) (mempty { aspect = Just a })
220
221  tokenToHI :: T.Token -> HighlightingInfoBuilder
222  tokenToHI (T.TokKeyword T.KwForall i)  = aToF Symbol (getRange i)
223  tokenToHI (T.TokKeyword T.KwREWRITE _) = mempty  -- #4361, REWRITE is not always a Keyword
224  tokenToHI (T.TokKeyword _ i)           = aToF Keyword (getRange i)
225  tokenToHI (T.TokSymbol T.SymQuestionMark i) = aToF Hole (getRange i)
226  tokenToHI (T.TokSymbol  _ i)                = aToF Symbol (getRange i)
227  tokenToHI (T.TokLiteral (Ranged r (L.LitNat    _))) = aToF Number r
228  tokenToHI (T.TokLiteral (Ranged r (L.LitWord64 _))) = aToF Number r
229  tokenToHI (T.TokLiteral (Ranged r (L.LitFloat  _))) = aToF Number r
230  tokenToHI (T.TokLiteral (Ranged r (L.LitString _))) = aToF String r
231  tokenToHI (T.TokLiteral (Ranged r (L.LitChar   _))) = aToF String r
232  tokenToHI (T.TokLiteral (Ranged r (L.LitQName  _))) = aToF String r
233  tokenToHI (T.TokLiteral (Ranged r (L.LitMeta _ _))) = aToF String r
234  tokenToHI (T.TokComment (i, _))            = aToF Comment (getRange i)
235  tokenToHI (T.TokTeX (i, _))                = aToF Background (getRange i)
236  tokenToHI (T.TokMarkup (i, _))             = aToF Markup (getRange i)
237  tokenToHI (T.TokId {})                     = mempty
238  tokenToHI (T.TokQId {})                    = mempty
239  tokenToHI (T.TokString (i,s))              = aToF Pragma (getRange i)
240  tokenToHI (T.TokDummy {})                  = mempty
241  tokenToHI (T.TokEOF {})                    = mempty
242
243-- | Builds a 'NameKinds' function.
244
245nameKinds :: Level
246             -- ^ This should only be @'Full'@ if
247             -- type-checking completed successfully (without any
248             -- errors).
249          -> A.Declaration
250          -> TCM NameKinds
251nameKinds hlLevel decl = do
252  imported <- useTC $ stImports . sigDefinitions
253  local    <- case hlLevel of
254    Full{} -> useTC $ stSignature . sigDefinitions
255    _      -> return HMap.empty
256  impPatSyns <- useTC stPatternSynImports
257  locPatSyns <- case hlLevel of
258    Full{} -> useTC stPatternSyns
259    _      -> return empty
260      -- Traverses the syntax tree and constructs a map from qualified
261      -- names to name kinds. TODO: Handle open public.
262  let syntax :: NameKindMap
263      syntax = runBuilder (declaredNames decl :: NameKindBuilder) HMap.empty
264  return $ \ n -> unionsMaybeWith mergeNameKind
265    [ defnToKind . theDef <$> HMap.lookup n local
266    , con <$ Map.lookup n locPatSyns
267    , defnToKind . theDef <$> HMap.lookup n imported
268    , con <$ Map.lookup n impPatSyns
269    , HMap.lookup n syntax
270    ]
271  where
272  defnToKind :: TCM.Defn -> NameKind
273  defnToKind   TCM.Axiom{}                           = Postulate
274  defnToKind   TCM.DataOrRecSig{}                    = Postulate
275  defnToKind   TCM.GeneralizableVar{}                = Generalizable
276  defnToKind d@TCM.Function{} | isProperProjection d = Field
277                            | otherwise            = Function
278  defnToKind   TCM.Datatype{}                        = Datatype
279  defnToKind   TCM.Record{}                          = Record
280  defnToKind   TCM.Constructor{ TCM.conInd = i }       = Constructor i
281  defnToKind   TCM.Primitive{}                       = Primitive
282  defnToKind   TCM.PrimitiveSort{}                   = Primitive
283  defnToKind   TCM.AbstractDefn{}                    = __IMPOSSIBLE__
284
285  con :: NameKind
286  con = Constructor Common.Inductive
287
288-- | The 'TCM.Axiom' constructor is used to represent various things
289-- which are not really axioms, so when maps are merged 'Postulate's
290-- are thrown away whenever possible. The 'declaredNames' function
291-- below can return several explanations for one qualified name; the
292-- 'Postulate's are bogus.
293mergeNameKind :: NameKind -> NameKind -> NameKind
294mergeNameKind Postulate k = k
295mergeNameKind _     Macro = Macro  -- If the abstract syntax says macro, it's a macro.
296mergeNameKind k         _ = k
297
298-- Auxiliary types for @nameKinds@ generation
299
300type NameKindMap     = HashMap A.QName NameKind
301data NameKindBuilder = NameKindBuilder
302  { runBuilder :: NameKindMap -> NameKindMap
303  }
304
305instance Semigroup (NameKindBuilder) where
306  NameKindBuilder f <> NameKindBuilder g = NameKindBuilder $ f . g
307
308instance Monoid (NameKindBuilder) where
309  mempty = NameKindBuilder id
310  mappend = (<>)
311
312instance Singleton KName NameKindBuilder where
313  singleton (WithKind k q) = NameKindBuilder $
314    HMap.insertWith mergeNameKind q $ kindOfNameToNameKind k
315
316instance Collection KName NameKindBuilder
317
318-- | Generates syntax highlighting information for all constructors
319-- occurring in patterns and expressions in the given declaration.
320--
321-- This function should only be called after type checking.
322-- Constructors can be overloaded, and the overloading is resolved by
323-- the type checker.
324
325generateConstructorInfo
326  :: SourceToModule  -- ^ Maps source file paths to module names.
327  -> AbsolutePath    -- ^ The module to highlight.
328  -> NameKinds
329  -> A.Declaration
330  -> TCM HighlightingInfoBuilder
331generateConstructorInfo modMap file kinds decl = do
332
333  -- Get boundaries of current declaration.
334  -- @noRange@ should be impossible, but in case of @noRange@
335  -- it makes sense to return mempty.
336  caseList (P.rangeIntervals $ getRange decl)
337           (return mempty) $ \ i is -> do
338    let start = fromIntegral $ P.posPos $ P.iStart i
339        end   = fromIntegral $ P.posPos $ P.iEnd $ last1 i is
340
341    -- Get all disambiguated names that fall within the range of decl.
342    m0 <- useTC stDisambiguatedNames
343    let (_, m1) = IntMap.split (pred start) m0
344        (m2, _) = IntMap.split end m1
345        constrs = IntMap.elems m2
346
347    -- Return suitable syntax highlighting information.
348    return $ foldMap (runHighlighter modMap file kinds) constrs
349
350printSyntaxInfo :: Range -> TCM ()
351printSyntaxInfo r = do
352  syntaxInfo <- useTC stSyntaxInfo
353  ifTopLevelAndHighlightingLevelIs NonInteractive $
354    printHighlightingInfo KeepHighlighting
355      (restrictTo (rangeToRange r) syntaxInfo)
356
357-- | Prints syntax highlighting info for an error.
358
359printErrorInfo :: TCErr -> TCM ()
360printErrorInfo e =
361  printHighlightingInfo KeepHighlighting . convert =<<
362    errorHighlighting e
363
364-- | Generate highlighting for error.
365
366errorHighlighting :: TCErr -> TCM HighlightingInfoBuilder
367errorHighlighting e = errorHighlighting' (getRange e) <$> TCM.prettyError e
368
369errorHighlighting'
370  :: Range     -- ^ Error range.
371  -> String    -- ^ Error message for tooltip.
372  -> HighlightingInfoBuilder
373errorHighlighting' r s = mconcat
374  [ -- Erase previous highlighting.
375    H.singleton (rToR $ P.continuousPerLine r) mempty
376  , -- Print new highlighting.
377    H.singleton (rToR r)
378         $ parserBased { otherAspects = Set.singleton Error
379                       , note         = s
380                       }
381  ]
382
383-- | Highlighting for warnings that are considered fatal.
384
385errorWarningHighlighting :: HasRange a => a -> HighlightingInfoBuilder
386errorWarningHighlighting w =
387  H.singleton (rToR $ P.continuousPerLine $ getRange w) $
388    parserBased { otherAspects = Set.singleton ErrorWarning }
389-- errorWarningHighlighting w = errorHighlighting' (getRange w) ""
390  -- MonadPretty not available here, so, no tooltip.
391  -- errorHighlighting' (getRange w) . render <$> TCM.prettyWarning (tcWarning w)
392
393-- | Generate syntax highlighting for warnings.
394
395warningHighlighting :: TCWarning -> HighlightingInfoBuilder
396warningHighlighting = warningHighlighting' True
397
398warningHighlighting' :: Bool -- ^ should we generate highlighting for unsolved metas and constrains?
399                     -> TCWarning -> HighlightingInfoBuilder
400warningHighlighting' b w = case tcWarning w of
401  TerminationIssue terrs     -> terminationErrorHighlighting terrs
402  NotStrictlyPositive d ocs  -> positivityErrorHighlighting d ocs
403  -- #3965 highlight each unreachable clause independently: they
404  -- may be interleaved with actually reachable clauses!
405  UnreachableClauses _ rs    -> foldMap deadcodeHighlighting rs
406  CoverageIssue{}            -> coverageErrorHighlighting $ getRange w
407  CoverageNoExactSplit{}     -> catchallHighlighting $ getRange w
408  UnsolvedConstraints cs     -> if b then constraintsHighlighting [] cs else mempty
409  UnsolvedMetaVariables rs   -> if b then metasHighlighting rs          else mempty
410  AbsurdPatternRequiresNoRHS{} -> deadcodeHighlighting w
411  ModuleDoesntExport{}         -> deadcodeHighlighting w
412  DuplicateUsing xs            -> foldMap deadcodeHighlighting xs
413  FixityInRenamingModule rs    -> foldMap deadcodeHighlighting rs
414  -- expanded catch-all case to get a warning for new constructors
415  CantGeneralizeOverSorts{}  -> mempty
416  UnsolvedInteractionMetas{} -> mempty
417  OldBuiltin{}               -> mempty
418  EmptyRewritePragma{}       -> deadcodeHighlighting w
419  EmptyWhere{}               -> deadcodeHighlighting w
420  IllformedAsClause{}        -> deadcodeHighlighting w
421  UselessPublic{}            -> deadcodeHighlighting w
422  UselessHiding xs           -> foldMap deadcodeHighlighting xs
423  UselessInline{}            -> mempty
424  UselessPatternDeclarationForRecord{} -> deadcodeHighlighting w
425  ClashesViaRenaming _ xs    -> foldMap deadcodeHighlighting xs
426    -- #4154, TODO: clashing renamings are not dead code, but introduce problems.
427    -- Should we have a different color?
428  WrongInstanceDeclaration{} -> mempty
429  InstanceWithExplicitArg{}  -> deadcodeHighlighting w
430  InstanceNoOutputTypeName{} -> mempty
431  InstanceArgWithExplicitArg{} -> mempty
432  InversionDepthReached{}    -> mempty
433  NoGuardednessFlag{}        -> mempty
434  GenericWarning{}           -> mempty
435  GenericUseless r _         -> deadcodeHighlighting r
436  -- Andreas, 2020-03-21, issue #4456:
437  -- Error warnings that do not have dedicated highlighting
438  -- are highlighted as errors.
439  GenericNonFatalError{}                -> errorWarningHighlighting w
440  SafeFlagPostulate{}                   -> errorWarningHighlighting w
441  SafeFlagPragma{}                      -> errorWarningHighlighting w
442  SafeFlagNonTerminating                -> errorWarningHighlighting w
443  SafeFlagTerminating                   -> errorWarningHighlighting w
444  SafeFlagWithoutKFlagPrimEraseEquality -> errorWarningHighlighting w
445  SafeFlagEta                           -> errorWarningHighlighting w
446  SafeFlagInjective                     -> errorWarningHighlighting w
447  SafeFlagNoCoverageCheck               -> errorWarningHighlighting w
448  SafeFlagNoPositivityCheck             -> errorWarningHighlighting w
449  SafeFlagPolarity                      -> errorWarningHighlighting w
450  SafeFlagNoUniverseCheck               -> errorWarningHighlighting w
451  InfectiveImport{}                     -> errorWarningHighlighting w
452  CoInfectiveImport{}                   -> errorWarningHighlighting w
453  WithoutKFlagPrimEraseEquality -> mempty
454  DeprecationWarning{}       -> mempty
455  UserWarning{}              -> mempty
456  LibraryWarning{}           -> mempty
457  RewriteNonConfluent{}      -> confluenceErrorHighlighting w
458  RewriteMaybeNonConfluent{} -> confluenceErrorHighlighting w
459  RewriteAmbiguousRules{}    -> confluenceErrorHighlighting w
460  RewriteMissingRule{}       -> confluenceErrorHighlighting w
461  PragmaCompileErased{}      -> deadcodeHighlighting w
462  NotInScopeW{}              -> deadcodeHighlighting w
463  AsPatternShadowsConstructorOrPatternSynonym{}
464                             -> deadcodeHighlighting w
465  RecordFieldWarning w       -> recordFieldWarningHighlighting w
466  ParseWarning w             -> case w of
467    Pa.UnsupportedAttribute{}     -> deadcodeHighlighting w
468    Pa.MultipleAttributes{}       -> deadcodeHighlighting w
469    Pa.OverlappingTokensWarning{} -> mempty
470  NicifierIssue (DeclarationWarning _ w) -> case w of
471    -- we intentionally override the binding of `w` here so that our pattern of
472    -- using `getRange w` still yields the most precise range information we
473    -- can get.
474    NotAllowedInMutual{}             -> deadcodeHighlighting w
475    EmptyAbstract{}                  -> deadcodeHighlighting w
476    EmptyConstructor{}               -> deadcodeHighlighting w
477    EmptyInstance{}                  -> deadcodeHighlighting w
478    EmptyMacro{}                     -> deadcodeHighlighting w
479    EmptyMutual{}                    -> deadcodeHighlighting w
480    EmptyPostulate{}                 -> deadcodeHighlighting w
481    EmptyPrimitive{}                 -> deadcodeHighlighting w
482    EmptyPrivate{}                   -> deadcodeHighlighting w
483    EmptyGeneralize{}                -> deadcodeHighlighting w
484    EmptyField{}                     -> deadcodeHighlighting w
485    UselessAbstract{}                -> deadcodeHighlighting w
486    UselessInstance{}                -> deadcodeHighlighting w
487    UselessPrivate{}                 -> deadcodeHighlighting w
488    InvalidNoPositivityCheckPragma{} -> deadcodeHighlighting w
489    InvalidNoUniverseCheckPragma{}   -> deadcodeHighlighting w
490    InvalidTerminationCheckPragma{}  -> deadcodeHighlighting w
491    InvalidCoverageCheckPragma{}     -> deadcodeHighlighting w
492    InvalidConstructor{}             -> deadcodeHighlighting w
493    InvalidConstructorBlock{}        -> deadcodeHighlighting w
494    InvalidRecordDirective{}         -> deadcodeHighlighting w
495    OpenPublicAbstract{}             -> deadcodeHighlighting w
496    OpenPublicPrivate{}              -> deadcodeHighlighting w
497    W.ShadowingInTelescope nrs       -> foldMap
498                                          (shadowingTelHighlighting . snd)
499                                          nrs
500    MissingDefinitions{}             -> missingDefinitionHighlighting w
501    -- TODO: explore highlighting opportunities here!
502    InvalidCatchallPragma{}           -> mempty
503    PolarityPragmasButNotPostulates{} -> mempty
504    PragmaNoTerminationCheck{}        -> mempty
505    PragmaCompiled{}                  -> errorWarningHighlighting w
506    UnknownFixityInMixfixDecl{}       -> mempty
507    UnknownNamesInFixityDecl{}        -> mempty
508    UnknownNamesInPolarityPragmas{}   -> mempty
509
510recordFieldWarningHighlighting ::
511  RecordFieldWarning -> HighlightingInfoBuilder
512recordFieldWarningHighlighting = \case
513  DuplicateFieldsWarning xrs      -> dead xrs
514  TooManyFieldsWarning _q _ys xrs -> dead xrs
515  where
516  dead :: [(C.Name, Range)] -> HighlightingInfoBuilder
517  dead = mconcat . map deadcodeHighlighting
518  -- Andreas, 2020-03-27 #3684: This variant seems to only highlight @x@:
519  -- dead = mconcat . map f
520  -- f (x, r) = deadcodeHighlighting (getRange x) `mappend` deadcodeHighlighting r
521
522-- | Generate syntax highlighting for termination errors.
523
524terminationErrorHighlighting ::
525  [TerminationError] -> HighlightingInfoBuilder
526terminationErrorHighlighting termErrs = functionDefs `mappend` callSites
527  where
528    m            = parserBased { otherAspects = Set.singleton TerminationProblem }
529    functionDefs = foldMap (\x -> H.singleton (rToR $ bindingSite x) m) $
530                   concatMap termErrFunctions termErrs
531    callSites    = foldMap (\r -> H.singleton (rToR r) m) $
532                   concatMap (map callInfoRange . termErrCalls) termErrs
533    bindingSite  = A.nameBindingSite . A.qnameName
534
535-- | Generate syntax highlighting for not-strictly-positive inductive
536-- definitions.
537
538positivityErrorHighlighting ::
539  I.QName -> Seq OccursWhere -> HighlightingInfoBuilder
540positivityErrorHighlighting q os =
541  several (rToR <$> getRange q : rs) m
542  where
543    rs = map (\(OccursWhere r _ _) -> r) (Fold.toList os)
544    m  = parserBased { otherAspects = Set.singleton PositivityProblem }
545
546deadcodeHighlighting :: HasRange a => a -> HighlightingInfoBuilder
547deadcodeHighlighting a = H.singleton (rToR $ P.continuous $ getRange a) m
548  where m = parserBased { otherAspects = Set.singleton Deadcode }
549
550coverageErrorHighlighting :: Range -> HighlightingInfoBuilder
551coverageErrorHighlighting r = H.singleton (rToR $ P.continuousPerLine r) m
552  where m = parserBased { otherAspects = Set.singleton CoverageProblem }
553
554shadowingTelHighlighting :: List2 Range -> HighlightingInfoBuilder
555shadowingTelHighlighting =
556  -- we do not want to highlight the one variable in scope so we take
557  -- the @init@ segment of the ranges in question
558  foldMap (\r -> H.singleton (rToR $ P.continuous r) m) . List2.init
559  where
560  m = parserBased { otherAspects =
561                      Set.singleton H.ShadowingInTelescope }
562
563catchallHighlighting :: Range -> HighlightingInfoBuilder
564catchallHighlighting r = H.singleton (rToR $ P.continuousPerLine r) m
565  where m = parserBased { otherAspects = Set.singleton CatchallClause }
566
567confluenceErrorHighlighting ::
568  HasRange a => a -> HighlightingInfoBuilder
569confluenceErrorHighlighting a = H.singleton (rToR $ P.continuousPerLine $ getRange a) m
570  where m = parserBased { otherAspects = Set.singleton ConfluenceProblem }
571
572missingDefinitionHighlighting ::
573  HasRange a => a -> HighlightingInfoBuilder
574missingDefinitionHighlighting a = H.singleton (rToR $ P.continuousPerLine $ getRange a) m
575  where m = parserBased { otherAspects = Set.singleton MissingDefinition }
576
577-- | Generates and prints syntax highlighting information for unsolved
578-- meta-variables and certain unsolved constraints.
579
580printUnsolvedInfo :: TCM ()
581printUnsolvedInfo = do
582  info <- computeUnsolvedInfo
583
584  printHighlightingInfo KeepHighlighting (convert info)
585
586computeUnsolvedInfo :: TCM HighlightingInfoBuilder
587computeUnsolvedInfo = do
588  (rs, metaInfo) <- computeUnsolvedMetaWarnings
589  constraintInfo <- computeUnsolvedConstraints rs
590
591  return $ metaInfo `mappend` constraintInfo
592
593-- | Generates syntax highlighting information for unsolved meta
594-- variables.
595--   Also returns ranges of unsolved or interaction metas.
596computeUnsolvedMetaWarnings :: TCM ([Ranges], HighlightingInfoBuilder)
597computeUnsolvedMetaWarnings = do
598  is <- getInteractionMetas
599
600  -- We don't want to highlight blocked terms, since
601  --   * there is always at least one proper meta responsible for the blocking
602  --   * in many cases the blocked term covers the highlighting for this meta
603  --   * for the same reason we skip metas with a twin, since the twin will be blocked.
604  let notBlocked m = not <$> isBlockedTerm m
605  let notHasTwin m = not <$> hasTwinMeta m
606  ms <- filterM notHasTwin =<< filterM notBlocked =<< getOpenMetas
607
608  let extend = map (rToR . P.continuousPerLine)
609
610  rs <- extend <$> mapM getMetaRange (ms \\ is)
611
612  rs' <- extend <$> mapM getMetaRange is
613  return $ (rs ++ rs', metasHighlighting' rs)
614
615metasHighlighting :: [Range] -> HighlightingInfoBuilder
616metasHighlighting rs = metasHighlighting' (map (rToR . P.continuousPerLine) rs)
617
618metasHighlighting' :: [Ranges] -> HighlightingInfoBuilder
619metasHighlighting' rs = several rs
620                     $ parserBased { otherAspects = Set.singleton UnsolvedMeta }
621
622-- | Generates syntax highlighting information for unsolved constraints
623--   (ideally: that are not connected to a meta variable).
624
625computeUnsolvedConstraints :: [Ranges] -- ^ does not add ranges that would overlap with these.
626                           -> TCM HighlightingInfoBuilder
627computeUnsolvedConstraints ms = constraintsHighlighting ms <$> getAllConstraints
628
629constraintsHighlighting ::
630  [Ranges] -> Constraints -> HighlightingInfoBuilder
631constraintsHighlighting ms cs =
632  several (filter noOverlap $ map (rToR . P.continuousPerLine) rs)
633          (parserBased { otherAspects = Set.singleton UnsolvedConstraint })
634  where
635  noOverlap r = not $ any (overlappings $ r) $ ms
636  -- get ranges of interesting unsolved constraints
637  rs = (`mapMaybe` (map theConstraint cs)) $ \case
638    Closure{ clValue = IsEmpty r t           } -> Just r
639    Closure{ clEnv = e, clValue = ValueCmp{} } -> Just $ getRange (envRange e)
640    Closure{ clEnv = e, clValue = ElimCmp{}  } -> Just $ getRange (envRange e)
641    Closure{ clEnv = e, clValue = SortCmp{}  } -> Just $ getRange (envRange e)
642    Closure{ clEnv = e, clValue = LevelCmp{} } -> Just $ getRange (envRange e)
643    Closure{ clEnv = e, clValue = CheckSizeLtSat{} } -> Just $ getRange (envRange e)
644    _ -> Nothing
645
646
647-- * Disambiguation of constructors and projections.
648
649storeDisambiguatedField :: A.QName -> TCM ()
650storeDisambiguatedField = storeDisambiguatedName Field
651
652storeDisambiguatedProjection :: A.QName -> TCM ()
653storeDisambiguatedProjection = storeDisambiguatedField
654
655storeDisambiguatedConstructor :: Common.Induction -> A.QName -> TCM ()
656storeDisambiguatedConstructor i = storeDisambiguatedName $ Constructor i
657
658-- TODO: move the following function to a new module TypeChecking.Overloading
659-- that gathers functions concerning disambiguation of overloading.
660
661-- | Remember a name disambiguation (during type checking).
662--   To be used later during syntax highlighting.
663--   Also: raise user warnings associated with the name.
664storeDisambiguatedName :: NameKind -> A.QName -> TCM ()
665storeDisambiguatedName k q = do
666  raiseWarningsOnUsage q
667  whenJust (start $ getRange q) $ \ i ->
668    modifyTCLens stDisambiguatedNames $ IntMap.insert i $ DisambiguatedName k q
669  where
670  start r = fromIntegral . P.posPos <$> P.rStart' r
671
672-- | Store a disambiguation of record field tags for the purpose of highlighting.
673disambiguateRecordFields
674  :: [C.Name]   -- ^ Record field names in a record expression.
675  -> [A.QName]  -- ^ Record field names in the corresponding record type definition
676  -> TCM ()
677disambiguateRecordFields cxs axs = forM_ cxs $ \ cx -> do
678  caseMaybe (List.find ((cx ==) . A.nameConcrete . A.qnameName) axs) (return ()) $ \ ax -> do
679    storeDisambiguatedField ax{ A.qnameName = (A.qnameName ax) { A.nameConcrete = cx } }
680