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