module Agda.Interaction.Highlighting.Generate
( Level(..)
, generateAndPrintSyntaxInfo
, generateTokenInfo, generateTokenInfoFromString
, printErrorInfo, errorHighlighting
, printUnsolvedInfo
, printHighlightingInfo
, highlightAsTypeChecked
, computeUnsolvedMetaWarnings
, computeUnsolvedConstraints
, Agda.Interaction.Highlighting.Generate.tests
) where
import Agda.Interaction.FindFile
import Agda.Interaction.Response (Response(Resp_HighlightingInfo))
import Agda.Interaction.Highlighting.Precise hiding (tests)
import Agda.Interaction.Highlighting.Range hiding (tests)
import qualified Agda.TypeChecking.Errors as E
import Agda.TypeChecking.MetaVars (isBlockedTerm)
import Agda.TypeChecking.Monad
hiding (MetaInfo, Primitive, Constructor, Record, Function, Datatype)
import qualified Agda.TypeChecking.Monad as M
import Agda.TypeChecking.Pretty
import qualified Agda.TypeChecking.Reduce as R
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common (Delayed(..))
import qualified Agda.Syntax.Common as SC
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Info as SI
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.Utils.List
import Agda.Utils.TestHelpers
import Agda.Utils.HashMap (HashMap)
import qualified Agda.Utils.HashMap as HMap
import Control.Monad
import Control.Monad.Trans
import Control.Monad.State
import Control.Monad.Reader
import Control.Applicative
import Control.Arrow ((***))
import Data.Monoid
import Data.Generics.Geniplate
import Agda.Utils.FileName
import Data.HashSet (HashSet)
import qualified Data.HashSet as HSet
import qualified Data.Map as Map
import Data.Maybe
import Data.List ((\\), isPrefixOf)
import qualified Data.Foldable as Fold (toList, fold, foldMap)
#include "../../undefined.h"
import Agda.Utils.Impossible
highlightAsTypeChecked
:: MonadTCM tcm
=> P.Range
-> P.Range
-> tcm a
-> tcm a
highlightAsTypeChecked rPre r m
| r /= P.noRange && delta == rPre' = wrap r' highlight clear
| otherwise = wrap delta clear highlight
where
rPre' = rToR (P.continuousPerLine rPre)
r' = rToR (P.continuousPerLine r)
delta = rPre' `minus` r'
clear = mempty
highlight = mempty { otherAspects = [TypeChecks] }
wrap rs x y = do
p rs x
v <- m
p rs y
return v
where
p rs x = printHighlightingInfo (singletonC rs x)
printHighlightingInfo :: MonadTCM tcm => HighlightingInfo -> tcm ()
printHighlightingInfo x = do
modToSrc <- gets stModuleToSource
liftTCM $ reportSLn "highlighting" 50 $
"Printing highlighting info:\n" ++ show x ++ "\n" ++
" modToSrc = " ++ show modToSrc
unless (null $ ranges x) $ do
liftTCM $ appInteractionOutputCallback $
Resp_HighlightingInfo x modToSrc
data Level
= Full [TerminationError]
| Partial
generateAndPrintSyntaxInfo :: A.Declaration -> Level -> TCM ()
generateAndPrintSyntaxInfo decl _ | P.noRange == P.getRange decl = return ()
generateAndPrintSyntaxInfo decl hlLevel = do
file <- envCurrentPath <$> ask
reportSLn "import.iface.create" 15 $
"Generating syntax info for " ++ filePath file ++ ' ' :
case hlLevel of
Full {} -> "(final)"
Partial {} -> "(first approximation)"
++ "."
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
let (from, to) = case P.rangeToInterval (P.getRange decl) of
Nothing -> __IMPOSSIBLE__
Just i -> let conv = toInteger . P.posPos in
(conv $ P.iStart i, conv $ P.iEnd i)
(prevTokens, (curTokens, postTokens)) <-
(id *** splitAtC to) . splitAtC from . stTokens <$> get
let syntaxInfo = compress (mconcat [ constructorInfo
, theRest modMap file
, nameInfo
, termInfo
])
`mappend`
curTokens
case hlLevel of
Full _ -> modify (\st ->
st { stSyntaxInfo = syntaxInfo `mappend` stSyntaxInfo st
, stTokens = prevTokens `mappend` postTokens
})
_ -> return ()
ifTopLevelAndHighlightingLevelIs NonInteractive $
printHighlightingInfo syntaxInfo
where
termInfo = case hlLevel of
Full termErrs -> functionDefs `mappend` callSites
where
m = mempty { otherAspects = [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
_ -> mempty
names :: [A.AmbiguousQName]
names =
(map (A.AmbQ . (:[])) $
filter (not . extendedLambda) $
universeBi decl) ++
universeBi decl
where
extendedLambda :: A.QName -> Bool
extendedLambda n = extendlambdaname `isPrefixOf` show (A.qnameName n)
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 getExpr $ universeBi decl
, Fold.foldMap getPatSynArgs $ universeBi decl
, Fold.foldMap getModuleName $ universeBi decl
, Fold.foldMap getModuleInfo $ universeBi decl
, Fold.foldMap getNamedArg $ universeBi decl
]
where
bound n = nameToFile modMap file [] (A.nameConcrete n)
(\isOp -> mempty { aspect = Just $ Name (Just Bound) isOp })
(Just $ A.nameBindingSite n)
patsyn n = nameToFileA modMap file n True $ \isOp ->
mempty { aspect = Just $ Name (Just $ Constructor SC.Inductive) isOp }
field m n = nameToFile modMap file m n
(\isOp -> mempty { aspect = Just $ Name (Just Field) isOp })
Nothing
asName n = nameToFile modMap file []
n
(\isOp -> mempty { aspect = Just $ Name (Just Module) isOp })
Nothing
mod isTopLevelModule n =
nameToFile modMap file []
(A.nameConcrete n)
(\isOp -> mempty { aspect = Just $ Name (Just Module) isOp })
(Just $ (if isTopLevelModule then P.beginningOfFile else id)
(A.nameBindingSite n))
getVarAndField :: A.Expr -> File
getVarAndField (A.Var x) = bound x
getVarAndField (A.Rec _ fs) = mconcat $ map (field [] . fst) fs
getVarAndField _ = mempty
getNamedArg :: SC.RString -> File
getNamedArg x = singleton (rToR $ P.getRange x) mempty{ aspect = Just $ Name (Just Argument) False }
getLet :: A.LetBinding -> File
getLet (A.LetBind _ _ x _ _) = bound x
getLet A.LetPatBind{} = mempty
getLet A.LetApply{} = mempty
getLet A.LetOpen{} = mempty
getLam :: A.LamBinding -> File
getLam (A.DomainFree _ x) = bound x
getLam (A.DomainFull {}) = mempty
getTyped :: A.TypedBinding -> File
getTyped (A.TBind _ xs _) = mconcat $ map bound xs
getTyped A.TLet{} = mempty
getPatSynArgs :: A.Declaration -> File
getPatSynArgs (A.PatternSynDef _ xs _) = mconcat $ map (bound . SC.unArg) xs
getPatSynArgs _ = mempty
getPattern :: A.Pattern -> File
getPattern (A.VarP x) = bound x
getPattern (A.AsP _ x _) = bound x
getPattern (A.DotP pi _) =
singleton (rToR $ P.getRange pi)
(mempty { otherAspects = [DottedPattern] })
getPattern (A.PatternSynP _ q _) = patsyn q
getPattern _ = mempty
getExpr :: A.Expr -> File
getExpr (A.PatternSyn q) = patsyn 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 catMaybes $
map (join .
fmap P.srcFile .
P.rStart .
A.nameBindingSite) xs of
f : _ -> Map.lookup f modMap ==
Just (C.toTopLevelModuleName $ A.mnameToConcrete m)
[] -> False
getModuleInfo :: SI.ModuleInfo -> File
getModuleInfo (SI.ModuleInfo { SI.minfoAsTo = asTo
, SI.minfoAsName = name }) =
singleton (rToR asTo) (mempty { aspect = Just Symbol })
`mappend`
maybe mempty asName name
generateTokenInfo
:: AbsolutePath
-> TCM CompressedFile
generateTokenInfo file =
liftIO $ tokenHighlighting <$> Pa.parseFile' Pa.tokensParser file
generateTokenInfoFromString :: P.Range -> String -> TCM CompressedFile
generateTokenInfoFromString r _ | r == P.noRange = return mempty
generateTokenInfoFromString r s = do
liftIO $ 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 (P.getRange i)
tokenToCFile (T.TokKeyword T.KwSet i) = aToF PrimitiveType (P.getRange i)
tokenToCFile (T.TokKeyword T.KwProp i) = aToF PrimitiveType (P.getRange i)
tokenToCFile (T.TokKeyword T.KwForall i) = aToF Symbol (P.getRange i)
tokenToCFile (T.TokKeyword _ i) = aToF Keyword (P.getRange i)
tokenToCFile (T.TokSymbol _ i) = aToF Symbol (P.getRange i)
tokenToCFile (T.TokLiteral (L.LitInt 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.TokComment (i, _)) = aToF Comment (P.getRange i)
tokenToCFile (T.TokTeX (i, _)) = aToF Comment (P.getRange i)
tokenToCFile (T.TokId {}) = mempty
tokenToCFile (T.TokQId {}) = mempty
tokenToCFile (T.TokString {}) = mempty
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 <- fix . stImports <$> get
local <- case hlLevel of
Full _ -> fix . stSignature <$> get
_ -> return HMap.empty
let syntax = foldr ($) HMap.empty $ map declToKind $ universeBi decl
let merged = HMap.unions [local, imported, syntax]
return (\n -> HMap.lookup n merged)
where
fix = HMap.map (defnToKind . theDef) . sigDefinitions
insert = HMap.insertWith dropPostulates
where
dropPostulates Postulate k = k
dropPostulates k _ = k
defnToKind :: Defn -> NameKind
defnToKind M.Axiom{} = Postulate
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
declToKind :: A.Declaration ->
HashMap A.QName NameKind -> HashMap A.QName NameKind
declToKind (A.Axiom _ _ _ q _) = 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 (Constructor SC.Inductive)
declToKind (A.FunDef _ q _ _) = insert q Function
declToKind (A.DataSig _ q _ _) = insert q Datatype
declToKind (A.DataDef _ q _ cs) = \m ->
insert q Datatype $
foldr (\d -> insert (A.axiomName d)
(Constructor SC.Inductive))
m cs
declToKind (A.RecSig _ q _ _) = insert q Record
declToKind (A.RecDef _ q _ c _ _ _) = insert q Record .
case c of
Nothing -> id
Just q -> insert q (Constructor SC.Inductive)
generateConstructorInfo
:: SourceToModule
-> AbsolutePath
-> NameKinds
-> A.Declaration
-> TCM File
generateConstructorInfo modMap file kinds decl = do
let names = Fold.toList (A.allNames decl)
defMap <- M.sigDefinitions <$> M.getSignature
let defs = catMaybes $ map (flip HMap.lookup defMap) names
clauses <- R.instantiateFull $ concatMap M.defClauses defs
types <- R.instantiateFull $ map defType defs
let
patterns = universeBi (types, clauses)
terms = universeBi (types, clauses)
constrs = filter ((/= P.noRange) . P.getRange) $
concatMap getConstructorP patterns ++
concatMap getConstructor terms
delayed <- evalStateT (getDelayed terms) HSet.empty
return $ Fold.fold $ fmap (generate modMap file kinds . mkAmb)
(delayed ++ constrs)
where
mkAmb q = A.AmbQ [q]
getDelayed :: [I.Term] -> StateT (HashSet A.QName) TCM [A.QName]
getDelayed ts = concat <$> mapM getT ts
where
getT t = do
lift $ reportSDoc "highlighting.delayed" 50 $
text "Inspecting sub-term:" <+> prettyTCM t
seen <- get
case t of
I.Def q _ | not (q `HSet.member` seen)
&&
fmap P.srcFile (P.rStart (P.getRange q)) ==
Just (Just file)
-> getQ q
_ -> return []
getQ q = do
lift $ reportSDoc "highlighting.delayed" 30 $
text "Inspecting name:" <+> prettyTCM q
def <- lift $ getConstInfo q
case defDelayed def of
NotDelayed -> return []
Delayed -> do
lift $ reportSDoc "highlighting.delayed" 10 $
text "Found delayed definition:" <+> prettyTCM q
modify (HSet.insert q)
terms <- universeBi . concat . map (getRHS . I.clauseBody) <$>
lift (R.instantiateFull $ defClauses def)
(concatMap getConstructor terms ++) <$> getDelayed terms
getRHS (I.Body v) = [v]
getRHS I.NoBody = []
getRHS (I.Bind b) = getRHS (I.unAbs b)
getConstructorP :: I.Pattern -> [A.QName]
getConstructorP (I.ConP c _ _) = [I.conName c]
getConstructorP _ = []
getConstructor :: I.Term -> [A.QName]
getConstructor (I.Con q _) = [I.conName q]
getConstructor _ = []
printErrorInfo :: TCErr -> TCM ()
printErrorInfo e = do
printHighlightingInfo $ singletonC (rToR $ P.continuousPerLine $ P.getRange e) mempty
printHighlightingInfo . compress =<< errorHighlighting e
errorHighlighting :: TCErr -> TCM File
errorHighlighting e = do
s <- E.prettyError e
return $ singleton (rToR r)
$ mempty { otherAspects = [Error]
, note = Just s
}
where
r = P.getRange e
printUnsolvedInfo :: TCM ()
printUnsolvedInfo = do
metaInfo <- computeUnsolvedMetaWarnings
constraintInfo <- computeUnsolvedConstraints
printHighlightingInfo
(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 $ several (map (rToR . P.continuousPerLine) rs)
(mempty { otherAspects = [UnsolvedMeta] })
computeUnsolvedConstraints :: TCM File
computeUnsolvedConstraints = do
cs <- getAllConstraints
let rs = [ r | PConstr{ theConstraint = Closure{ clValue = IsEmpty r t }} <- cs ]
return $ several (map (rToR . P.continuousPerLine) rs)
(mempty { otherAspects = [UnsolvedConstraint] })
generate :: SourceToModule
-> AbsolutePath
-> NameKinds
-> A.AmbiguousQName
-> File
generate modMap file kinds (A.AmbQ qs) =
mconcat $ map (\q -> nameToFileA modMap file q include m) qs
where
ks = map kinds qs
kind = case [ k | Just k <- ks ] of
k : _ -> Just k
[] -> Nothing
m isOp = mempty { aspect = Just $ Name kind isOp }
include = allEqual (map bindingSite qs)
nameToFile :: SourceToModule
-> AbsolutePath
-> [C.Name]
-> C.Name
-> (Bool -> MetaInfo)
-> Maybe P.Range
-> File
nameToFile modMap file xs x m mR =
if all (== Just file) fileNames then
several (map rToR rs)
((m $ C.isOperator x) { definitionSite = mFilePos })
else
mempty
where
fileNames = catMaybes $ map (fmap P.srcFile . P.rStart . P.getRange) (x : xs)
rs = map P.getRange (x : xs)
mFilePos = do
r <- mR
P.Pn { P.srcFile = Just f, P.posPos = p } <- P.rStart r
mod <- Map.lookup f modMap
return (mod, toInteger p)
nameToFileA :: SourceToModule
-> AbsolutePath
-> A.QName
-> Bool
-> (Bool -> MetaInfo)
-> File
nameToFileA modMap file x include m =
nameToFile modMap
file
(concreteQualifier x)
(concreteBase x)
m
(if include then Just $ bindingSite x else Nothing)
concreteBase = A.nameConcrete . A.qnameName
concreteQualifier = map A.nameConcrete . A.mnameToList . A.qnameModule
bindingSite = A.nameBindingSite . A.qnameName
tests :: IO Bool
tests = runTests "Agda.Interaction.Highlighting.Generate" []