module Agda.Interaction.Highlighting.Generate
( Level(..)
, generateAndPrintSyntaxInfo
, generateTokenInfo, generateTokenInfoFromSource
, generateTokenInfoFromString
, printSyntaxInfo
, printErrorInfo, errorHighlighting
, printUnsolvedInfo
, printHighlightingInfo
, highlightAsTypeChecked
, highlightWarning, warningHighlighting
, computeUnsolvedMetaWarnings
, computeUnsolvedConstraints
, storeDisambiguatedName, disambiguateRecordFields
) where
import Prelude hiding (null)
import Control.Monad
import Control.Arrow (second)
import Data.Generics.Geniplate
import qualified Data.Map as Map
import Data.Maybe
import Data.List ((\\))
import qualified Data.List as List
import qualified Data.Foldable as Fold (fold, foldMap, toList)
import qualified Data.IntMap as IntMap
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HMap
import Data.Sequence (Seq)
import qualified Data.Set as Set
import qualified Data.Text.Lazy as T
import Data.Void
import Agda.Interaction.Response
( Response( Resp_HighlightingInfo )
, RemoveTokenBasedHighlighting( KeepHighlighting )
)
import Agda.Interaction.Highlighting.Precise as P
import Agda.Interaction.Highlighting.Range (rToR, minus)
import qualified Agda.TypeChecking.Errors as E
import Agda.TypeChecking.MetaVars (isBlockedTerm)
import Agda.TypeChecking.Monad
hiding (ModuleInfo, MetaInfo, Primitive, Constructor, Record, Function, Datatype)
import qualified Agda.TypeChecking.Monad as M
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Warnings (runPM)
import Agda.Syntax.Abstract (IsProjP(..))
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Concrete (FieldAssignment'(..))
import Agda.Syntax.Concrete.Definitions as W ( DeclarationWarning(..) )
import qualified Agda.Syntax.Common as Common
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Info ( ModuleInfo(..), defMacro )
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 (Range, HasRange, getRange, noRange)
import Agda.Utils.FileName
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.Impossible
data Level
= Full
| Partial
highlightWarning :: TCWarning -> TCM ()
highlightWarning tcwarn = do
let h = compress $ warningHighlighting tcwarn
modifyTCLens stSyntaxInfo (h <>)
ifTopLevelAndHighlightingLevelIs NonInteractive $
printHighlightingInfo KeepHighlighting h
generateAndPrintSyntaxInfo
:: A.Declaration
-> Level
-> Bool
-> TCM ()
generateAndPrintSyntaxInfo decl _ _ | null $ getRange decl = return ()
generateAndPrintSyntaxInfo decl hlLevel updateState = do
file <- getCurrentPath
reportSLn "import.iface.create" 15 $
"Generating syntax info for " ++ filePath file ++ ' ' :
case hlLevel of
Full {} -> "(final)"
Partial {} -> "(first approximation)"
++ "."
reportSLn "highlighting.names" 60 $ "highlighting names = " ++ prettyShow names
M.ignoreAbstractMode $ do
modMap <- sourceToModule
kinds <- nameKinds hlLevel decl
let nameInfo = mconcat $ map (generate modMap file kinds) names
constructorInfo <- case hlLevel of
Full{} -> generateConstructorInfo modMap file kinds decl
_ -> return mempty
cm <- P.rangeFile <$> viewTC eRange
reportSLn "highlighting.warning" 60 $ "current path = " ++ show cm
let (from, to) = case P.rangeToInterval (getRange decl) of
Nothing -> __IMPOSSIBLE__
Just i -> ( fromIntegral $ P.posPos $ P.iStart i
, fromIntegral $ P.posPos $ P.iEnd i)
(prevTokens, (curTokens, postTokens)) <-
second (splitAtC to) . splitAtC from <$> useTC stTokens
let syntaxInfo = compress (mconcat [ constructorInfo
, theRest modMap file
, nameInfo
])
`mappend`
curTokens
when updateState $ do
stSyntaxInfo `modifyTCLens` mappend syntaxInfo
stTokens `setTCLens` (prevTokens `mappend` postTokens)
ifTopLevelAndHighlightingLevelIs NonInteractive $
printHighlightingInfo KeepHighlighting syntaxInfo
where
names :: [A.AmbiguousQName]
names =
(map I.unambiguous $
filter (not . isExtendedLambdaName) $
universeBi decl) ++
universeBi decl
theRest :: SourceToModule -> AbsolutePath -> File
theRest modMap file = mconcat
[ Fold.foldMap getFieldDecl $ universeBi decl
, Fold.foldMap getVarAndField $ universeBi decl
, Fold.foldMap getLet $ universeBi decl
, Fold.foldMap getLam $ universeBi decl
, Fold.foldMap getTyped $ universeBi decl
, Fold.foldMap getPattern $ universeBi decl
, Fold.foldMap getPatternSyn $ universeBi decl
, Fold.foldMap getExpr $ universeBi decl
, Fold.foldMap getPatSynArgs $ universeBi decl
, Fold.foldMap getModuleName $ universeBi decl
, Fold.foldMap getModuleInfo $ universeBi decl
, Fold.foldMap getNamedArgE $ universeBi decl
, Fold.foldMap getNamedArgP $ universeBi decl
, Fold.foldMap getNamedArgB $ universeBi decl
, Fold.foldMap getNamedArgL $ universeBi decl
, Fold.foldMap getQuantityAttr$ universeBi decl
, Fold.foldMap getPragma $ universeBi decl
]
where
bound A.BindName{ unBind = n } =
nameToFile modMap file [] (A.nameConcrete n) noRange
(\isOp -> parserBased { aspect =
Just $ Name (Just Bound) isOp })
(Just $ A.nameBindingSite n)
patsyn n =
nameToFileA modMap file (I.headAmbQ n) True $ \isOp ->
parserBased { aspect =
Just $ Name (Just $ Constructor Common.Inductive) isOp }
macro n = nameToFileA modMap file n True $ \isOp ->
parserBased { aspect = Just $ Name (Just Macro) isOp }
field :: [C.Name] -> C.Name -> File
field m n = nameToFile modMap file m n noRange
(\isOp -> parserBased { aspect =
Just $ Name (Just Field) isOp })
Nothing
asName :: C.Name -> File
asName n = nameToFile modMap file []
n noRange
(\isOp -> parserBased { aspect =
Just $ Name (Just Module) isOp })
Nothing
mod isTopLevelModule n =
nameToFile modMap file []
(A.nameConcrete n) noRange
(\isOp -> parserBased { aspect =
Just $ Name (Just Module) isOp })
(Just $ applyWhen isTopLevelModule P.beginningOfFile $
A.nameBindingSite n)
getVarAndField :: A.Expr -> File
getVarAndField (A.Var x) = bound $ A.mkBindName x
getVarAndField (A.Rec _ fs) = mconcat [ field [] x | Left (FieldAssignment x _) <- fs ]
getVarAndField (A.RecUpdate _ _ fs) = mconcat [ field [] x | (FieldAssignment x _) <- fs ]
getVarAndField _ = mempty
getNamedArgE :: Common.NamedArg A.Expr -> File
getNamedArgE = getNamedArg
getNamedArgP :: Common.NamedArg A.Pattern -> File
getNamedArgP = getNamedArg
getNamedArgB :: Common.NamedArg A.BindName -> File
getNamedArgB = getNamedArg
getNamedArgL :: Common.NamedArg A.LHSCore -> File
getNamedArgL = getNamedArg
getNamedArg :: Common.NamedArg a -> File
getNamedArg x = caseMaybe (Common.nameOf $ Common.unArg x) mempty $ \ s ->
singleton (rToR $ getRange s) $
parserBased { aspect = Just $ Name (Just Argument) False }
getBinder :: A.Binder -> File
getBinder (A.Binder _ n) = bound n
getLet :: A.LetBinding -> File
getLet (A.LetBind _ _ x _ _) = bound x
getLet A.LetPatBind{} = mempty
getLet A.LetApply{} = mempty
getLet A.LetOpen{} = mempty
getLet (A.LetDeclaredVariable x) = bound x
getLam :: A.LamBinding -> File
getLam (A.DomainFree _ xs) = getBinder (Common.namedArg xs)
getLam (A.DomainFull {}) = mempty
getTyped :: A.TypedBinding -> File
getTyped (A.TBind _ _ xs _) = Fold.foldMap (getBinder . Common.namedArg) xs
getTyped A.TLet{} = mempty
getPatSynArgs :: A.Declaration -> File
getPatSynArgs (A.PatternSynDef _ xs _) = mconcat $ map (bound . A.mkBindName . Common.unArg) xs
getPatSynArgs _ = mempty
getPragma :: A.Declaration -> File
getPragma = \case
A.Pragma _ p ->
case p of
A.BuiltinPragma b _ -> keyword b
A.BuiltinNoDefPragma b _ -> keyword b
A.CompilePragma b _ _ -> keyword b
A.RewritePragma r _ -> keyword r
A.OptionsPragma{} -> mempty
A.StaticPragma{} -> mempty
A.EtaPragma{} -> mempty
A.InjectivePragma{} -> mempty
A.InlinePragma{} -> mempty
A.DisplayPragma{} -> mempty
_ -> mempty
keyword :: HasRange a => a -> File
keyword x = singleton (rToR $ getRange x) $ parserBased { aspect = Just Keyword }
getPattern' :: IsProjP e => A.Pattern' e -> File
getPattern' (A.VarP x) = bound x
getPattern' (A.AsP _ x _) = bound x
getPattern' (A.DotP pi e)
| Just _ <- isProjP e = mempty
| otherwise =
singleton (rToR $ getRange pi)
(parserBased { otherAspects = Set.singleton DottedPattern })
getPattern' (A.PatternSynP _ q _) = patsyn q
getPattern' (A.RecP _ fs) = mconcat [ field [] x | FieldAssignment x _ <- fs ]
getPattern' _ = mempty
getPattern :: A.Pattern -> File
getPattern = getPattern'
getPatternSyn :: A.Pattern' Void -> File
getPatternSyn = getPattern'
getExpr :: A.Expr -> File
getExpr (A.PatternSyn q) = patsyn q
getExpr (A.Macro q) = macro q
getExpr _ = mempty
getFieldDecl :: A.Declaration -> File
getFieldDecl (A.RecDef _ _ _ _ _ _ _ _ fs) = Fold.foldMap extractField fs
where
extractField (A.ScopedDecl _ ds) = Fold.foldMap extractField ds
extractField (A.Field _ x _) = field (concreteQualifier x)
(concreteBase x)
extractField _ = mempty
getFieldDecl _ = mempty
getModuleName :: A.ModuleName -> File
getModuleName m@(A.MName { A.mnameToList = xs }) =
mconcat $ map (mod isTopLevelModule) xs
where
isTopLevelModule =
case mapMaybe (join .
fmap (Strict.toLazy . P.srcFile) .
P.rStart .
A.nameBindingSite) xs of
f : _ -> Map.lookup f modMap ==
Just (C.toTopLevelModuleName $ A.mnameToConcrete m)
[] -> False
getModuleInfo :: ModuleInfo -> File
getModuleInfo (ModuleInfo{ minfoAsTo, minfoAsName }) =
singleton (rToR minfoAsTo) (parserBased { aspect = Just Symbol })
`mappend`
maybe mempty asName minfoAsName
getQuantityAttr :: Common.Quantity -> File
getQuantityAttr q = singleton (rToR $ getRange q) (parserBased { aspect = Just Symbol })
generateTokenInfo :: AbsolutePath -> TCM CompressedFile
generateTokenInfo file =
generateTokenInfoFromSource file . T.unpack =<<
runPM (Pa.readFilePM file)
generateTokenInfoFromSource
:: AbsolutePath
-> String
-> TCM CompressedFile
generateTokenInfoFromSource file input =
runPM $ tokenHighlighting <$> fst <$> Pa.parseFile Pa.tokensParser file input
generateTokenInfoFromString :: Range -> String -> TCM CompressedFile
generateTokenInfoFromString r _ | r == noRange = return mempty
generateTokenInfoFromString r s = do
runPM $ tokenHighlighting <$> Pa.parsePosString Pa.tokensParser p s
where
Just p = P.rStart r
tokenHighlighting :: [T.Token] -> CompressedFile
tokenHighlighting = merge . map tokenToCFile
where
aToF a r = singletonC (rToR r) (mempty { aspect = Just a })
merge = CompressedFile . concat . map ranges
tokenToCFile :: T.Token -> CompressedFile
tokenToCFile (T.TokSetN (i, _)) = aToF PrimitiveType (getRange i)
tokenToCFile (T.TokPropN (i, _)) = aToF PrimitiveType (getRange i)
tokenToCFile (T.TokKeyword T.KwSet i) = aToF PrimitiveType (getRange i)
tokenToCFile (T.TokKeyword T.KwProp i) = aToF PrimitiveType (getRange i)
tokenToCFile (T.TokKeyword T.KwForall i) = aToF Symbol (getRange i)
tokenToCFile (T.TokKeyword T.KwREWRITE _) = mempty
tokenToCFile (T.TokKeyword _ i) = aToF Keyword (getRange i)
tokenToCFile (T.TokSymbol _ i) = aToF Symbol (getRange i)
tokenToCFile (T.TokLiteral (L.LitNat r _)) = aToF Number r
tokenToCFile (T.TokLiteral (L.LitWord64 r _)) = aToF Number r
tokenToCFile (T.TokLiteral (L.LitFloat r _)) = aToF Number r
tokenToCFile (T.TokLiteral (L.LitString r _)) = aToF String r
tokenToCFile (T.TokLiteral (L.LitChar r _)) = aToF String r
tokenToCFile (T.TokLiteral (L.LitQName r _)) = aToF String r
tokenToCFile (T.TokLiteral (L.LitMeta r _ _)) = aToF String r
tokenToCFile (T.TokComment (i, _)) = aToF Comment (getRange i)
tokenToCFile (T.TokTeX (i, _)) = aToF Background (getRange i)
tokenToCFile (T.TokMarkup (i, _)) = aToF Markup (getRange i)
tokenToCFile (T.TokId {}) = mempty
tokenToCFile (T.TokQId {}) = mempty
tokenToCFile (T.TokString (i,s)) = aToF Pragma (getRange i)
tokenToCFile (T.TokDummy {}) = mempty
tokenToCFile (T.TokEOF {}) = mempty
type NameKinds = A.QName -> Maybe NameKind
nameKinds :: Level
-> A.Declaration
-> TCM NameKinds
nameKinds hlLevel decl = do
imported <- useTC $ stImports . sigDefinitions
local <- case hlLevel of
Full{} -> useTC $ stSignature . sigDefinitions
_ -> return HMap.empty
impPatSyns <- useTC stPatternSynImports
locPatSyns <- case hlLevel of
Full{} -> useTC stPatternSyns
_ -> return empty
let syntax = foldr ($) HMap.empty $ map declToKind $ universeBi decl
return $ \ n -> unionsMaybeWith merge
[ defnToKind . theDef <$> HMap.lookup n local
, con <$ Map.lookup n locPatSyns
, defnToKind . theDef <$> HMap.lookup n imported
, con <$ Map.lookup n impPatSyns
, HMap.lookup n syntax
]
where
merge Postulate k = k
merge _ Macro = Macro
merge k _ = k
insert = HMap.insertWith merge
defnToKind :: Defn -> NameKind
defnToKind M.Axiom{} = Postulate
defnToKind M.DataOrRecSig{} = Postulate
defnToKind M.GeneralizableVar{} = Generalizable
defnToKind d@M.Function{} | isProperProjection d = Field
| otherwise = Function
defnToKind M.Datatype{} = Datatype
defnToKind M.Record{} = Record
defnToKind M.Constructor{ M.conInd = i } = Constructor i
defnToKind M.Primitive{} = Primitive
defnToKind M.AbstractDefn{} = __IMPOSSIBLE__
declToKind :: A.Declaration ->
HashMap A.QName NameKind -> HashMap A.QName NameKind
declToKind (A.Axiom _ i _ _ q _)
| defMacro i == Common.MacroDef = insert q Macro
| otherwise = insert q Postulate
declToKind (A.Field _ q _) = insert q Field
declToKind (A.Primitive _ q _) = insert q Primitive
declToKind (A.Mutual {}) = id
declToKind (A.Section {}) = id
declToKind (A.Apply {}) = id
declToKind (A.Import {}) = id
declToKind (A.Pragma {}) = id
declToKind (A.ScopedDecl {}) = id
declToKind (A.Open {}) = id
declToKind (A.PatternSynDef q _ _) = insert q con
declToKind (A.Generalize _ _ _ q _) = insert q Generalizable
declToKind (A.FunDef _ q _ _) = insert q Function
declToKind (A.UnquoteDecl _ _ qs _) = foldr (\ q f -> insert q Function . f) id qs
declToKind (A.UnquoteDef _ qs _) = foldr (\ q f -> insert q Function . f) id qs
declToKind (A.DataSig _ q _ _) = insert q Datatype
declToKind (A.DataDef _ q _ _ cs) = \m ->
insert q Datatype $
foldr (\d -> insert (A.axiomName d) con)
m cs
declToKind (A.RecSig _ q _ _) = insert q Record
declToKind (A.RecDef _ q _ _ _ c _ _ _) = insert q Record . maybe id (`insert` con) c
con :: NameKind
con = Constructor Common.Inductive
generateConstructorInfo
:: SourceToModule
-> AbsolutePath
-> NameKinds
-> A.Declaration
-> TCM File
generateConstructorInfo modMap file kinds decl = do
ifNull (P.rangeIntervals $ getRange decl)
(return mempty) $ \is -> do
let start = fromIntegral $ P.posPos $ P.iStart $ head is
end = fromIntegral $ P.posPos $ P.iEnd $ last is
m0 <- useTC stDisambiguatedNames
let (_, m1) = IntMap.split (pred start) m0
(m2, _) = IntMap.split end m1
constrs = IntMap.elems m2
let files = for constrs $ \ q -> generate modMap file kinds $ I.unambiguous q
return $ Fold.fold files
printSyntaxInfo :: Range -> TCM ()
printSyntaxInfo r = do
syntaxInfo <- useTC stSyntaxInfo
ifTopLevelAndHighlightingLevelIs NonInteractive $
printHighlightingInfo KeepHighlighting (selectC r syntaxInfo)
printErrorInfo :: TCErr -> TCM ()
printErrorInfo e =
printHighlightingInfo KeepHighlighting . compress =<<
errorHighlighting e
errorHighlighting :: TCErr -> TCM File
errorHighlighting e = do
let r = getRange e
erase = singleton (rToR $ P.continuousPerLine r) mempty
s <- E.prettyError e
let error = singleton (rToR r)
$ parserBased { otherAspects = Set.singleton Error
, note = Just s
}
return $ mconcat [ erase, error ]
warningHighlighting :: TCWarning -> File
warningHighlighting w = case tcWarning w of
TerminationIssue terrs -> terminationErrorHighlighting terrs
NotStrictlyPositive d ocs -> positivityErrorHighlighting d ocs
UnreachableClauses _ rs -> Fold.foldMap deadcodeHighlighting rs
CoverageIssue{} -> coverageErrorHighlighting $ getRange w
CoverageNoExactSplit{} -> catchallHighlighting $ getRange w
UnsolvedConstraints cs -> constraintsHighlighting cs
UnsolvedMetaVariables rs -> metasHighlighting rs
AbsurdPatternRequiresNoRHS{} -> deadcodeHighlighting $ getRange w
ModuleDoesntExport{} -> deadcodeHighlighting $ getRange w
FixityInRenamingModule rs -> Fold.foldMap deadcodeHighlighting rs
CantGeneralizeOverSorts{} -> mempty
UnsolvedInteractionMetas{} -> mempty
OldBuiltin{} -> mempty
EmptyRewritePragma{} -> deadcodeHighlighting $ getRange w
IllformedAsClause{} -> deadcodeHighlighting $ getRange w
UselessPublic{} -> deadcodeHighlighting $ getRange w
UselessInline{} -> mempty
ClashesViaRenaming _ xs -> Fold.foldMap (deadcodeHighlighting . getRange) xs
WrongInstanceDeclaration{} -> mempty
InstanceWithExplicitArg{} -> deadcodeHighlighting $ getRange w
InstanceNoOutputTypeName{} -> mempty
InstanceArgWithExplicitArg{} -> mempty
ParseWarning{} -> mempty
InversionDepthReached{} -> mempty
GenericWarning{} -> mempty
GenericNonFatalError{} -> mempty
SafeFlagPostulate{} -> mempty
SafeFlagPragma{} -> mempty
SafeFlagNonTerminating -> mempty
SafeFlagTerminating -> mempty
SafeFlagWithoutKFlagPrimEraseEquality -> mempty
SafeFlagEta -> mempty
SafeFlagInjective -> mempty
SafeFlagNoCoverageCheck -> mempty
WithoutKFlagPrimEraseEquality -> mempty
SafeFlagNoPositivityCheck -> mempty
SafeFlagPolarity -> mempty
SafeFlagNoUniverseCheck -> mempty
DeprecationWarning{} -> mempty
UserWarning{} -> mempty
LibraryWarning{} -> mempty
InfectiveImport{} -> mempty
CoInfectiveImport{} -> mempty
RewriteNonConfluent{} -> confluenceErrorHighlighting $ getRange w
RewriteMaybeNonConfluent{} -> confluenceErrorHighlighting $ getRange w
PragmaCompileErased{} -> deadcodeHighlighting $ getRange w
NotInScopeW{} -> deadcodeHighlighting $ getRange w
NicifierIssue w -> case w of
NotAllowedInMutual{} -> deadcodeHighlighting $ getRange w
EmptyAbstract{} -> deadcodeHighlighting $ getRange w
EmptyInstance{} -> deadcodeHighlighting $ getRange w
EmptyMacro{} -> deadcodeHighlighting $ getRange w
EmptyMutual{} -> deadcodeHighlighting $ getRange w
EmptyPostulate{} -> deadcodeHighlighting $ getRange w
EmptyPrimitive{} -> deadcodeHighlighting $ getRange w
EmptyPrivate{} -> deadcodeHighlighting $ getRange w
EmptyGeneralize{} -> deadcodeHighlighting $ getRange w
EmptyField{} -> deadcodeHighlighting $ getRange w
UselessAbstract{} -> deadcodeHighlighting $ getRange w
UselessInstance{} -> deadcodeHighlighting $ getRange w
UselessPrivate{} -> deadcodeHighlighting $ getRange w
InvalidNoPositivityCheckPragma{} -> deadcodeHighlighting $ getRange w
InvalidNoUniverseCheckPragma{} -> deadcodeHighlighting $ getRange w
InvalidTerminationCheckPragma{} -> deadcodeHighlighting $ getRange w
InvalidCoverageCheckPragma{} -> deadcodeHighlighting $ getRange w
OpenPublicAbstract{} -> deadcodeHighlighting $ getRange w
OpenPublicPrivate{} -> deadcodeHighlighting $ getRange w
W.ShadowingInTelescope nrs -> Fold.foldMap
(shadowingTelHighlighting . snd)
nrs
MissingDefinitions{} -> missingDefinitionHighlighting $ getRange w
InvalidCatchallPragma{} -> mempty
PolarityPragmasButNotPostulates{} -> mempty
PragmaNoTerminationCheck{} -> mempty
PragmaCompiled{} -> mempty
UnknownFixityInMixfixDecl{} -> mempty
UnknownNamesInFixityDecl{} -> mempty
UnknownNamesInPolarityPragmas{} -> mempty
terminationErrorHighlighting :: [TerminationError] -> File
terminationErrorHighlighting termErrs = functionDefs `mappend` callSites
where
m = parserBased { otherAspects = Set.singleton TerminationProblem }
functionDefs = Fold.foldMap (\x -> singleton (rToR $ bindingSite x) m) $
concatMap M.termErrFunctions termErrs
callSites = Fold.foldMap (\r -> singleton (rToR r) m) $
concatMap (map M.callInfoRange . M.termErrCalls) termErrs
positivityErrorHighlighting :: I.QName -> Seq OccursWhere -> File
positivityErrorHighlighting q os =
several (rToR <$> getRange q : rs) m
where
rs = map (\(OccursWhere r _ _) -> r) (Fold.toList os)
m = parserBased { otherAspects = Set.singleton PositivityProblem }
deadcodeHighlighting :: Range -> File
deadcodeHighlighting r = singleton (rToR $ P.continuous r) m
where m = parserBased { otherAspects = Set.singleton Deadcode }
coverageErrorHighlighting :: Range -> File
coverageErrorHighlighting r = singleton (rToR $ P.continuousPerLine r) m
where m = parserBased { otherAspects = Set.singleton CoverageProblem }
shadowingTelHighlighting :: [Range] -> File
shadowingTelHighlighting =
Fold.foldMap (\r -> singleton (rToR $ P.continuous r) m) . init
where
m = parserBased { otherAspects =
Set.singleton P.ShadowingInTelescope }
catchallHighlighting :: Range -> File
catchallHighlighting r = singleton (rToR $ P.continuousPerLine r) m
where m = parserBased { otherAspects = Set.singleton CatchallClause }
confluenceErrorHighlighting :: Range -> File
confluenceErrorHighlighting r = singleton (rToR $ P.continuousPerLine r) m
where m = parserBased { otherAspects = Set.singleton ConfluenceProblem }
missingDefinitionHighlighting :: Range -> File
missingDefinitionHighlighting r = singleton (rToR $ P.continuousPerLine r) m
where m = parserBased { otherAspects = Set.singleton MissingDefinition }
printUnsolvedInfo :: TCM ()
printUnsolvedInfo = do
metaInfo <- computeUnsolvedMetaWarnings
constraintInfo <- computeUnsolvedConstraints
printHighlightingInfo KeepHighlighting
(compress $ metaInfo `mappend` constraintInfo)
computeUnsolvedMetaWarnings :: TCM File
computeUnsolvedMetaWarnings = do
is <- getInteractionMetas
let notBlocked m = not <$> isBlockedTerm m
ms <- filterM notBlocked =<< getOpenMetas
rs <- mapM getMetaRange (ms \\ is)
return $ metasHighlighting rs
metasHighlighting :: [Range] -> File
metasHighlighting rs = several (map (rToR . P.continuousPerLine) rs)
$ parserBased { otherAspects = Set.singleton UnsolvedMeta }
computeUnsolvedConstraints :: TCM File
computeUnsolvedConstraints = constraintsHighlighting <$> getAllConstraints
constraintsHighlighting :: Constraints -> File
constraintsHighlighting cs =
several (map (rToR . P.continuousPerLine) rs)
(parserBased { otherAspects = Set.singleton UnsolvedConstraint })
where
rs = (`mapMaybe` (map theConstraint cs)) $ \case
Closure{ clValue = IsEmpty r t } -> Just r
Closure{ clEnv = e, clValue = ValueCmp{} } -> Just $ getRange (envRange e)
Closure{ clEnv = e, clValue = ElimCmp{} } -> Just $ getRange (envRange e)
Closure{ clEnv = e, clValue = TelCmp{} } -> Just $ getRange (envRange e)
Closure{ clEnv = e, clValue = SortCmp{} } -> Just $ getRange (envRange e)
Closure{ clEnv = e, clValue = LevelCmp{} } -> Just $ getRange (envRange e)
Closure{ clEnv = e, clValue = CheckSizeLtSat{} } -> Just $ getRange (envRange e)
_ -> Nothing
generate :: SourceToModule
-> AbsolutePath
-> NameKinds
-> A.AmbiguousQName
-> File
generate modMap file kinds (A.AmbQ qs) =
Fold.foldMap (\ q -> nameToFileA modMap file q include m) qs
where
ks = map kinds (Fold.toList qs)
kind = case [ k | Just k <- ks ] of
k : _ -> Just k
[] -> Nothing
m isOp = parserBased { aspect = Just $ Name kind isOp }
include = allEqual (map bindingSite $ Fold.toList qs)
nameToFile :: SourceToModule
-> AbsolutePath
-> [C.Name]
-> C.Name
-> Range
-> (Bool -> Aspects)
-> Maybe Range
-> File
nameToFile modMap file xs x fr m mR =
if all (== Strict.Just file) fileNames then
frFile `mappend`
several (map rToR rs)
(aspects { definitionSite = mFilePos })
else
mempty
where
aspects = m $ C.isOperator x
fileNames = mapMaybe (fmap P.srcFile . P.rStart . getRange) (x : xs)
frFile = singleton (rToR fr) (aspects { definitionSite = notHere <$> mFilePos })
rs = map getRange (x : xs)
notHere d = d { defSiteHere = False }
mFilePos :: Maybe DefinitionSite
mFilePos = do
r <- mR
P.Pn { P.srcFile = Strict.Just f, P.posPos = p } <- P.rStart r
mod <- Map.lookup f modMap
let qualifiers = drop (length $ C.moduleNameParts mod) xs
local = maybe True isLocalAspect $ aspect aspects
return $ DefinitionSite
{ defSiteModule = mod
, defSitePos = fromIntegral p
, defSiteHere = r == getRange x
, defSiteAnchor = if local || C.isNoName x || any Common.isUnderscore qualifiers
then Nothing
else Just $ prettyShow $ foldr C.Qual (C.QName x) qualifiers
}
isLocalAspect :: Aspect -> Bool
isLocalAspect = \case
Name mkind _ -> maybe True isLocal mkind
_ -> True
isLocal :: NameKind -> Bool
isLocal = \case
Bound -> True
Generalizable -> True
Argument -> True
Constructor{} -> False
Datatype -> False
Field -> False
Function -> False
Module -> False
Postulate -> False
Primitive -> False
Record -> False
Macro -> False
nameToFileA
:: SourceToModule
-> AbsolutePath
-> A.QName
-> Bool
-> (Bool -> Aspects)
-> File
nameToFileA modMap file x include m =
nameToFile modMap
file
(concreteQualifier x)
(concreteBase x)
rangeOfFixityDeclaration
m
(if include then Just $ bindingSite x else Nothing)
`mappend` notationFile
where
rangeOfFixityDeclaration =
if P.rangeFile r == Strict.Just file
then r else noRange
where
r = Common.theNameRange $ A.nameFixity $ A.qnameName x
notationFile =
if P.rangeFile (getRange notation) == Strict.Just file
then mconcat $ map genPartFile notation
else mempty
where
notation = Common.theNotation $ A.nameFixity $ A.qnameName x
boundAspect = parserBased{ aspect = Just $ Name (Just Bound) False }
genPartFile (Common.BindHole r i) = several [rToR r, rToR $ getRange i] boundAspect
genPartFile (Common.NormalHole r i) = several [rToR r, rToR $ getRange i] boundAspect
genPartFile Common.WildHole{} = mempty
genPartFile (Common.IdPart x) = singleton (rToR $ getRange x) (m False)
concreteBase :: I.QName -> C.Name
concreteBase = A.nameConcrete . A.qnameName
concreteQualifier :: I.QName -> [C.Name]
concreteQualifier = map A.nameConcrete . A.mnameToList . A.qnameModule
bindingSite :: I.QName -> Range
bindingSite = A.nameBindingSite . A.qnameName
storeDisambiguatedName :: A.QName -> TCM ()
storeDisambiguatedName q = whenJust (start $ getRange q) $ \ i ->
stDisambiguatedNames `modifyTCLens` IntMap.insert i q
where
start r = fromIntegral . P.posPos <$> P.rStart' r
disambiguateRecordFields
:: [C.Name]
-> [A.QName]
-> TCM ()
disambiguateRecordFields cxs axs = forM_ cxs $ \ cx -> do
caseMaybe (List.find ((cx ==) . A.nameConcrete . A.qnameName) axs) (return ()) $ \ ax -> do
storeDisambiguatedName ax { A.qnameName = (A.qnameName ax) { A.nameConcrete = cx } }