module Agda.Interaction.Highlighting.Generate
( generateSyntaxInfo
, generateErrorInfo
, Agda.Interaction.Highlighting.Generate.tests
)
where
import Agda.Interaction.FindFile
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.Options (reportSLn)
import Agda.TypeChecking.Monad
hiding (MetaInfo, Primitive, Constructor, Record, Function, Datatype)
import qualified Agda.TypeChecking.Monad as M
import qualified Agda.TypeChecking.Reduce as R
import qualified Agda.Syntax.Abstract as A
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 qualified Agda.Syntax.Scope.Base as S
import qualified Agda.Syntax.Translation.ConcreteToAbstract as CA
import Agda.Utils.List
import Agda.Utils.TestHelpers
import Control.Monad
import Control.Monad.Trans
import Control.Monad.State
import Control.Applicative
import Data.Monoid
import Data.Function
import Agda.Utils.Generics
import Agda.Utils.FileName
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Sequence (Seq, (><))
import Data.List ((\\), isPrefixOf)
import qualified Data.Sequence as Seq
import qualified Data.Foldable as Fold (toList, fold, foldMap)
import Agda.Utils.Impossible
#include "../../undefined.h"
generateErrorInfo :: P.Range -> Maybe String -> Maybe HighlightingInfo
generateErrorInfo r s =
case P.rStart r of
Nothing -> Nothing
Just (P.Pn { P.srcFile = Nothing }) -> Nothing
Just (P.Pn { P.srcFile = Just f, P.posPos = p }) ->
Just $ compress $ generateErrorFile r s
generateErrorFile :: P.Range -> Maybe String -> File
generateErrorFile r s =
several (rToR $ P.continuousPerLine r)
(mempty { otherAspects = [Error]
, note = s
})
generateSyntaxInfo
:: AbsolutePath
-> Maybe TCErr
-> CA.TopLevelInfo
-> [M.TerminationError]
-> TCM HighlightingInfo
generateSyntaxInfo file mErr top termErrs = do
reportSLn "import.iface.create" 15 $
"Generating syntax info for " ++ filePath file ++ ' ' : maybe "(No TCErr)" (const "(with TCErr)") mErr ++ "."
M.withScope_ (CA.insideScope top) $ M.ignoreAbstractMode $ do
modMap <- sourceToModule
tokens <- liftIO $ Pa.parseFile' Pa.tokensParser file
kinds <- nameKinds mErr decls
let nameInfo = mconcat $ map (generate modMap file kinds)
(Fold.toList names)
constructorInfo <- case mErr of
Nothing -> generateConstructorInfo modMap file kinds decls
Just _ -> return mempty
metaInfo <- case mErr of
Nothing -> computeUnsolvedMetaWarnings
Just _ -> return mempty
errorInfo <- case mErr of
Nothing -> return mempty
Just e -> let r = P.getRange e in
case P.rStart r of
Just p | P.srcFile p == Just file ->
generateErrorFile r . Just <$> E.prettyError e
_ -> __IMPOSSIBLE__
return $ compress $ mconcat
[ errorInfo
, constructorInfo
, theRest modMap
, nameInfo
, metaInfo
, termInfo
, tokInfo tokens
]
where
decls = CA.topLevelDecls top
aToF a r = several (rToR r) (mempty { aspect = Just a })
tokInfo = Fold.foldMap tokenToFile
where
tokenToFile :: T.Token -> File
tokenToFile (T.TokSetN (i, _)) = aToF PrimitiveType (P.getRange i)
tokenToFile (T.TokKeyword T.KwSet i) = aToF PrimitiveType (P.getRange i)
tokenToFile (T.TokKeyword T.KwProp i) = aToF PrimitiveType (P.getRange i)
tokenToFile (T.TokKeyword T.KwForall i) = aToF Symbol (P.getRange i)
tokenToFile (T.TokKeyword _ i) = aToF Keyword (P.getRange i)
tokenToFile (T.TokSymbol _ i) = aToF Symbol (P.getRange i)
tokenToFile (T.TokLiteral (L.LitInt r _)) = aToF Number r
tokenToFile (T.TokLiteral (L.LitFloat r _)) = aToF Number r
tokenToFile (T.TokLiteral (L.LitString r _)) = aToF String r
tokenToFile (T.TokLiteral (L.LitChar r _)) = aToF String r
tokenToFile (T.TokLiteral (L.LitQName r _)) = aToF String r
tokenToFile (T.TokComment (i, _)) = aToF Comment (P.getRange i)
tokenToFile (T.TokTeX (i, _)) = aToF Comment (P.getRange i)
tokenToFile (T.TokId {}) = mempty
tokenToFile (T.TokQId {}) = mempty
tokenToFile (T.TokString {}) = mempty
tokenToFile (T.TokDummy {}) = mempty
tokenToFile (T.TokEOF {}) = mempty
termInfo = functionDefs `mappend` callSites
where
m = mempty { otherAspects = [TerminationProblem] }
functionDefs = Fold.foldMap (\x -> several (rToR $ bindingSite x) m) $
concatMap M.termErrFunctions termErrs
callSites = Fold.foldMap (\r -> several (rToR r) m) $
concatMap (map M.callInfoRange . M.termErrCalls) termErrs
names = everything' (><) (Seq.empty `mkQ` getName
`extQ` getAmbiguous)
decls
where
getName :: A.QName -> Seq A.AmbiguousQName
getName n | isPrefixOf extendlambdaname $ show $ A.qnameName n = mempty
| otherwise = Seq.singleton (A.AmbQ [n])
getAmbiguous :: A.AmbiguousQName -> Seq A.AmbiguousQName
getAmbiguous = Seq.singleton
theRest modMap = everything' mappend query decls
where
query :: GenericQ File
query = mempty `mkQ`
getFieldDecl `extQ`
getVarAndField `extQ`
getLet `extQ`
getLam `extQ`
getTyped `extQ`
getPattern `extQ`
getModuleName `extQ`
getModuleInfo
bound n = nameToFile modMap file []
(A.nameConcrete n)
(\isOp -> mempty { aspect = Just $ Name (Just Bound) isOp })
(Just $ A.nameBindingSite n)
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
getLet :: A.LetBinding -> File
getLet (A.LetBind _ _ x _ _) = bound x
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.TNoBind {}) = mempty
getPattern :: A.Pattern -> File
getPattern (A.VarP x) = bound x
getPattern (A.AsP _ x _) = bound x
getPattern (A.DotP pi _) =
several (rToR $ P.getRange pi)
(mempty { otherAspects = [DottedPattern] })
getPattern _ = 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 }) =
aToF Symbol asTo `mappend` maybe mempty asName name
type NameKinds = A.QName -> Maybe NameKind
nameKinds :: Maybe TCErr
-> [A.Declaration]
-> TCM NameKinds
nameKinds mErr decls = do
imported <- fix . stImports <$> get
local <- case mErr of
Nothing -> fix . stSignature <$> get
Just _ -> return $
everything' union (Map.empty `mkQ` getDecl) decls
let merged = Map.union local imported
return (\n -> Map.lookup n merged)
where
fix = Map.map (defnToNameKind . theDef) . sigDefinitions
union = Map.unionWith dropPostulates
where
dropPostulates Postulate k = k
dropPostulates k _ = k
defnToNameKind :: Defn -> NameKind
defnToNameKind (M.Axiom {}) = Postulate
defnToNameKind (M.Function {}) = Function
defnToNameKind (M.Datatype {}) = Datatype
defnToNameKind (M.Record {}) = Record
defnToNameKind (M.Constructor { M.conInd = i }) = Constructor i
defnToNameKind (M.Primitive {}) = Primitive
getAxiomName :: A.Declaration -> A.QName
getAxiomName (A.Axiom _ _ q _) = q
getAxiomName _ = __IMPOSSIBLE__
getDecl :: A.Declaration -> Map A.QName NameKind
getDecl (A.Axiom _ _ q _) = Map.singleton q Postulate
getDecl (A.Field _ q _) = Map.singleton q Function
getDecl (A.Primitive _ q _) = Map.singleton q Primitive
getDecl (A.Mutual {}) = Map.empty
getDecl (A.Section {}) = Map.empty
getDecl (A.Apply {}) = Map.empty
getDecl (A.Import {}) = Map.empty
getDecl (A.Pragma {}) = Map.empty
getDecl (A.ScopedDecl {}) = Map.empty
getDecl (A.Open {}) = Map.empty
getDecl (A.FunDef _ q _) = Map.singleton q Function
getDecl (A.DataSig _ q _ _) = Map.singleton q Datatype
getDecl (A.DataDef _ q _ cs) = Map.singleton q Datatype `union`
(Map.unions $
map (\q -> Map.singleton q (Constructor SC.Inductive)) $
map getAxiomName cs)
getDecl (A.RecSig _ q _ _) = Map.singleton q Record
getDecl (A.RecDef _ q c _ _ _) = Map.singleton q Record `union`
case c of
Nothing -> Map.empty
Just q ->
Map.singleton q (Constructor SC.Inductive)
generateConstructorInfo
:: SourceToModule
-> AbsolutePath
-> NameKinds
-> [A.Declaration]
-> TCM File
generateConstructorInfo modMap file kinds decls = do
let names = Fold.toList $ Fold.foldMap A.allNames decls
defMap <- M.sigDefinitions <$> M.getSignature
let defs = catMaybes $ map (flip Map.lookup defMap) names
clauses <- R.instantiateFull $ concatMap M.defClauses defs
types <- R.instantiateFull $ map defType defs
constrs <- everything' (liftM2 (><)) query (types, clauses)
return $ Fold.fold $ fmap (generate modMap file kinds . mkAmb) constrs
where
mkAmb q = A.AmbQ [q]
query :: GenericQ (TCM (Seq A.QName))
query = return mempty `mkQ`
getConstructor `extQ`
getConstructorP
getConstructor :: I.Term -> TCM (Seq A.QName)
getConstructor (I.Con q _) = return $ Seq.singleton q
getConstructor (I.Def c _)
| fmap P.srcFile (P.rStart (P.getRange c)) == Just (Just file)
= retrieveCoconstructor c
getConstructor _ = return Seq.empty
getConstructorP :: I.Pattern -> TCM (Seq A.QName)
getConstructorP (I.ConP q _ _) = return $ Seq.singleton q
getConstructorP _ = return Seq.empty
retrieveCoconstructor :: A.QName -> TCM (Seq A.QName)
retrieveCoconstructor c = do
def <- getConstInfo c
case defDelayed def of
NotDelayed -> return Seq.empty
Delayed -> do
clauses <- R.instantiateFull $ defClauses def
case clauses of
[I.Clause{ I.clauseBody = body }] -> case getRHS body of
Just (I.Con c args) -> do
s <- everything' (liftM2 (><)) query args
return $ Seq.singleton c >< s
Just (I.MetaV {}) -> return Seq.empty
_ -> __IMPOSSIBLE__
_ -> __IMPOSSIBLE__
where
getRHS (I.Body v) = Just v
getRHS I.NoBody = Nothing
getRHS (I.Bind b) = getRHS (I.unAbs b)
computeUnsolvedMetaWarnings :: TCM File
computeUnsolvedMetaWarnings = do
is <- getInteractionMetas
let notBlocked m = not <$> isBlockedTerm m
ms <- filterM notBlocked =<< getOpenMetas
rs <- mapM getMetaRange (ms \\ is)
return $ several (concatMap (rToR . P.continuousPerLine) rs)
$ mempty { otherAspects = [UnsolvedMeta] }
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 (allEqual ks, ks) of
(True, Just 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 rs' ((m isOp) { definitionSite = mFilePos })
else
mempty
where
fileNames = catMaybes $ map (fmap P.srcFile . P.rStart . P.getRange) (x : xs)
(rs, isOp) = getRanges x
rs' = rs ++ concatMap (fst . getRanges) 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
everything' :: (r -> r -> r) -> GenericQ r -> GenericQ r
everything' (+) = everythingBut
(+)
(False `mkQ` isString
`extQ` isAQName `extQ` isAName `extQ` isCName
`extQ` isScope `extQ` isMap1 `extQ` isMap2
`extQ` isAmbiguous)
where
isString :: String -> Bool
isAQName :: A.QName -> Bool
isAName :: A.Name -> Bool
isCName :: C.Name -> Bool
isScope :: S.ScopeInfo -> Bool
isMap1 :: Map A.QName A.QName -> Bool
isMap2 :: Map A.ModuleName A.ModuleName -> Bool
isAmbiguous :: A.AmbiguousQName -> Bool
isString = const True
isAQName = const True
isAName = const True
isCName = const True
isScope = const True
isMap1 = const True
isMap2 = const True
isAmbiguous = const True
tests :: IO Bool
tests = runTests "Agda.Interaction.Highlighting.Generate" []