on master help sign in
Merge pull request #2256 from david-christiansen/name-highlights

Annotate module imports in source code

commit6ecd591bdf1e9bfdf0f64da09e7d1c47ef174dcd authorDavid Christiansen <david@davidchristiansen.dk> dateTue 12 May 2015, 21:10 (11 years ago) parent9b5f7848f9901d
10 files changed+123−52
src/Idris/AbsSyntaxTree.hs+7−5 src/Idris/Chaser.hs+1−1 src/Idris/Core/TT.hs+7 src/Idris/DeepSeq.hs+1−1 src/Idris/ElabDecls.hs+8−5 src/Idris/IBC.hs+6−4 src/Idris/IdeMode.hs+12−2 src/Idris/Output.hs+8−5 src/Idris/ParseHelpers.hs+1−1 src/Idris/Parser.hs+72−28
src/Idris/AbsSyntaxTree.hs+7−5
@@ -600,7 +600,9 @@ data PDecl' t
600600 | PCAF FC Name t -- ^ Top level constant
601601 | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
602602 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
603− | PNamespace String [PDecl' t] -- ^ New namespace
603+ | PNamespace String FC [PDecl' t]
604+ -- ^ New namespace, where FC is accurate location of the
605+ -- namespace in the file
604606 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts
605607 Name -- Record name
606608 FC -- Record name precise location
@@ -742,7 +744,7 @@ declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
742744 where fstt (_, _, a, _, _, _, _) = a
743745declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
744746declared (PParams _ _ ds) = concatMap declared ds
745−declared (PNamespace _ ds) = concatMap declared ds
747+declared (PNamespace _ _ ds) = concatMap declared ds
746748declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
747749declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
748750declared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
@@ -763,7 +765,7 @@ tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
763765 where fstt (_, _, a, _, _, _, _) = a
764766tldeclared (PParams _ _ ds) = []
765767tldeclared (PMutual _ ds) = concatMap tldeclared ds
766−tldeclared (PNamespace _ ds) = concatMap tldeclared ds
768+tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
767769tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
768770tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
769771tldeclared _ = []
@@ -778,7 +780,7 @@ defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
778780 where fstt (_, _, a, _, _, _, _) = a
779781defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
780782defined (PParams _ _ ds) = concatMap defined ds
781−defined (PNamespace _ ds) = concatMap defined ds
783+defined (PNamespace _ _ ds) = concatMap defined ds
782784defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
783785defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
784786defined (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
@@ -1785,7 +1787,7 @@ showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t"
17851787 indent 2 (vsep (map (showCImp o) cs))
17861788showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
17871789showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1788−showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1790+showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
17891791showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
17901792showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
17911793 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
src/Idris/Chaser.hs+1−1
@@ -149,7 +149,7 @@ buildTree built fp = btree [] fp
149149 (_, _, modules, _) <- parseImports f file
150150 -- The chaser should never report warnings from sub-modules
151151 clearParserWarnings
152− ms <- mapM (btree done) [realName | (_, realName, alias, fc) <- modules]
152+ ms <- mapM (btree done . import_path) modules
153153 return (concat ms)
154154 else return [] -- IBC with no source available
155155-- (\c -> return []) -- error, can't chase modules here
src/Idris/Core/TT.hs+7
@@ -163,6 +163,13 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St
163163 | AnnTerm [(Name, Bool)] (TT Name) -- ^ pprint bound vars, original term
164164 | AnnSearchResult Ordering -- ^ more general, isomorphic, or more specific
165165 | AnnErr Err
166+ | AnnNamespace [T.Text] (Maybe FilePath)
167+ -- ^ A namespace (e.g. on an import line or in
168+ -- a namespace declaration). Stored starting
169+ -- at the root, with the hierarchy fully
170+ -- resolved. If a file path is present, then
171+ -- the namespace represents a module imported
172+ -- from that file.
166173 deriving Show
167174
168175-- | Used for error reflection
src/Idris/DeepSeq.hs+1−1
@@ -146,7 +146,7 @@ instance (NFData t) => NFData (PDecl' t) where
146146 rnf x2 `seq`
147147 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
148148 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
149− rnf (PNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
149+ rnf (PNamespace x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
150150 rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
151151 = rnf x1 `seq`
152152 rnf x2 `seq`
src/Idris/ElabDecls.hs+8−5
@@ -18,7 +18,7 @@ import Idris.Primitives
1818import Idris.Inliner
1919import Idris.PartialEval
2020import Idris.DeepSeq
21−import Idris.Output (iputStrLn, pshow, iWarn)
21+import Idris.Output (iputStrLn, pshow, iWarn, sendHighlighting)
2222import IRTS.Lang
2323
2424import Idris.Elab.Utils
@@ -227,11 +227,14 @@ elabDecl' what info (PParams f ns ps)
227227 pblock i = map (expandParamsD False i id ns
228228 (concatMap tldeclared ps)) ps
229229
230−elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps
230+elabDecl' what info (PNamespace n nfc ps) =
231+ do mapM_ (elabDecl' what ninfo) ps
232+ let ns = reverse (map T.pack newNS)
233+ sendHighlighting [(nfc, AnnNamespace ns Nothing)]
231234 where
232− ninfo = case namespace info of
233− Nothing -> info { namespace = Just [n] }
234− Just ns -> info { namespace = Just (n:ns) }
235+ newNS = maybe [n] (n:) (namespace info)
236+ ninfo = info { namespace = Just newNS }
237+
235238elabDecl' what info (PClass doc s f cs n nfc ps pdocs fds ds cn cd)
236239 | what /= EDefns
237240 = do iLOG $ "Elaborating class " ++ show n
src/Idris/IBC.hs+6−4
@@ -1171,9 +1171,10 @@ instance (Binary t) => Binary (PDecl' t) where
11711171 put x1
11721172 put x2
11731173 put x3
1174− PNamespace x1 x2 -> do putWord8 5
1175− put x1
1176− put x2
1174+ PNamespace x1 x2 x3 -> do putWord8 5
1175+ put x1
1176+ put x2
1177+ put x3
11771178 PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ->
11781179 do putWord8 6
11791180 put x1
@@ -1284,7 +1285,8 @@ instance (Binary t) => Binary (PDecl' t) where
12841285 return (PParams x1 x2 x3)
12851286 5 -> do x1 <- get
12861287 x2 <- get
1287− return (PNamespace x1 x2)
1288+ x3 <- get
1289+ return (PNamespace x1 x2 x3)
12881290 6 -> do x1 <- get
12891291 x2 <- get
12901292 x3 <- get
src/Idris/IdeMode.hs+12−2
@@ -7,11 +7,12 @@ module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), s
77import Text.Printf
88import Numeric
99import Data.List
10+import Data.Maybe (isJust)
1011import qualified Data.Binary as Binary
1112import qualified Data.ByteString.Base64 as Base64
1213import qualified Data.ByteString.Lazy as Lazy
1314import qualified Data.ByteString.UTF8 as UTF8
14−-- import qualified Data.Text as T
15+import qualified Data.Text as T
1516import Text.Trifecta hiding (Err)
1617import Text.Trifecta.Delta
1718import System.IO
@@ -115,11 +116,16 @@ constTy (B32 _) = "Bits32"
115116constTy (B64 _) = "Bits64"
116117constTy _ = "Type"
117118
119+namespaceOf :: Name -> Maybe String
120+namespaceOf (NS _ ns) = Just (intercalate "." $ reverse (map T.unpack ns))
121+namespaceOf _ = Nothing
122+
118123instance SExpable OutputAnnotation where
119124 toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)),
120125 (SymbolAtom "implicit", BoolAtom False)] ++
121126 maybeProps [("decor", ty)] ++
122− maybeProps [("doc-overview", d), ("type", t)]
127+ maybeProps [("doc-overview", d), ("type", t)] ++
128+ maybeProps [("namespace", namespaceOf n)]
123129 toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),
124130 (SymbolAtom "decor", SymbolAtom "bound"),
125131 (SymbolAtom "implicit", BoolAtom imp)]
@@ -150,6 +156,10 @@ instance SExpable OutputAnnotation where
150156 LT -> "more general than searched type"
151157 GT -> "more specific than searched type"
152158 toSExp (AnnErr e) = toSExp [(SymbolAtom "error", StringAtom (encodeErr e))]
159+ toSExp (AnnNamespace ns file) =
160+ toSExp $ [(SymbolAtom "namespace", StringAtom (intercalate "." (map T.unpack ns)))] ++
161+ [(SymbolAtom "decor", SymbolAtom $ if isJust file then "module" else "namespace")] ++
162+ maybeProps [("source-file", file)]
153163
154164encodeTerm :: [(Name, Bool)] -> Term -> String
155165encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $
src/Idris/Output.hs+8−5
@@ -195,7 +195,6 @@ prettyDocumentedIst ist (name, ty, docs) =
195195 norm = normaliseAll (tt_ctxt ist) []
196196
197197sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()
198−sendHighlighting [] = return ()
199198sendHighlighting highlights =
200199 do ist <- getIState
201200 case idris_outputmode ist of
@@ -204,10 +203,12 @@ sendHighlighting highlights =
204203 let fancier = [ toSExp (fc, fancifyAnnots ist False annot)
205204 | (fc, annot) <- highlights, fullFC fc
206205 ]
207− in runIO . hPutStrLn h $
208− convSExp "output"
209− (SymbolAtom "ok",
210− (SymbolAtom "highlight-source", fancier)) n
206+ in case fancier of
207+ [] -> return ()
208+ _ -> runIO . hPutStrLn h $
209+ convSExp "output"
210+ (SymbolAtom "ok",
211+ (SymbolAtom "highlight-source", fancier)) n
211212
212213 where fullFC (FC _ _ _) = True
213214 fullFC _ = False
@@ -254,6 +255,7 @@ renderExternal fmt width doc
254255 decorate HTMLOutput (AnnTerm _ _) = id
255256 decorate HTMLOutput (AnnSearchResult _) = id
256257 decorate HTMLOutput (AnnErr _) = id
258+ decorate HTMLOutput (AnnNamespace _ _) = id
257259
258260 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =
259261 latex "IdrisType"
@@ -281,6 +283,7 @@ renderExternal fmt width doc
281283 decorate LaTeXOutput (AnnTerm _ _) = id
282284 decorate LaTeXOutput (AnnSearchResult _) = id
283285 decorate LaTeXOutput (AnnErr _) = id
286+ decorate LaTeXOutput (AnnNamespace _ _) = id
284287
285288 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"
286289 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs
src/Idris/ParseHelpers.hs+1−1
@@ -632,7 +632,7 @@ collect (c@(PClauses _ o _ _) : ds)
632632 fcOf (PClauses fc _ _ _) = fc
633633collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
634634collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
635−collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
635+collect (PNamespace ns fc ps : ds) = PNamespace ns fc (collect ps) : collect ds
636636collect (PClass doc f s cs n nfc ps pdocs fds ds cn cd : ds')
637637 = PClass doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds'
638638collect (PInstance doc argDocs f s cs n nfc ps t en ds : ds')
src/Idris/Parser.hs+72−28
@@ -92,38 +92,52 @@ import System.IO
9292 ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;
9393@
9494-}
95−moduleHeader :: IdrisParser (Maybe (Docstring ()), [String])
95+moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
9696moduleHeader = try (do docs <- optional docComment
9797 noArgs docs
9898 reserved "module"
99− i <- fst <$> identifier
99+ (i, ifc) <- identifier
100100 option ';' (lchar ';')
101− return (fmap fst docs, moduleName i))
101+ let modName = moduleName i
102+ return (fmap fst docs,
103+ modName,
104+ [(ifc, AnnNamespace (map T.pack modName) Nothing)]))
102105 <|> try (do lchar '%'; reserved "unqualified"
103− return (Nothing, []))
104− <|> return (Nothing, moduleName "Main")
106+ return (Nothing, [], []))
107+ <|> return (Nothing, moduleName "Main", [])
105108 where moduleName x = case span (/='.') x of
106109 (x, "") -> [x]
107110 (x, '.':y) -> x : moduleName y
108111 noArgs (Just (_, args)) | not (null args) = fail "Modules do not take arguments"
109112 noArgs _ = return ()
110113
114+data ImportInfo = ImportInfo { import_reexport :: Bool
115+ , import_path :: FilePath
116+ , import_rename :: Maybe (String, FC)
117+ , import_namespace :: [T.Text]
118+ , import_location :: FC
119+ , import_modname_location :: FC
120+ }
121+
111122{- | Parses an import statement
112123
113124@
114125 Import ::= 'import' Identifier_t ';'?;
115126@
116127 -}
117−import_ :: IdrisParser (Bool, String, Maybe String, FC)
128+import_ :: IdrisParser ImportInfo
118129import_ = do fc <- getFC
119130 reserved "import"
120131 reexport <- option False (do reserved "public"; return True)
121− id <- fst <$> identifier
122− newName <- optional (reserved "as" *> (fst <$> identifier))
132+ (id, idfc) <- identifier
133+ newName <- optional (reserved "as" *> identifier)
123134 option ';' (lchar ';')
124− return (reexport, toPath id, toPath <$> newName, fc)
135+ return $ ImportInfo reexport (toPath id)
136+ (fmap (\(n, fc) -> (toPath n, fc)) newName)
137+ (map T.pack $ ns id) fc idfc
125138 <?> "import statement"
126− where toPath = foldl1' (</>) . Spl.splitOn "."
139+ where ns = Spl.splitOn "."
140+ toPath = foldl1' (</>) . ns
127141
128142{- | Parses program source
129143
@@ -594,11 +608,12 @@ Namespace ::=
594608-}
595609namespace :: SyntaxInfo -> IdrisParser [PDecl]
596610namespace syn =
597− do reserved "namespace"; n <- fst <$> identifier
611+ do reserved "namespace"
612+ (n, nfc) <- identifier
598613 openBlock
599614 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
600615 closeBlock
601− return [PNamespace n (concat ds)]
616+ return [PNamespace n nfc (concat ds)]
602617 <?> "namespace declaration"
603618
604619{- | Parses a methods block (for instances)
@@ -1222,16 +1237,21 @@ parseTactic :: IState -> String -> Result PTactic
12221237parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
12231238
12241239-- | Parse module header and imports
1225−parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta)
1240+parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)
12261241parseImports fname input
12271242 = do i <- getIState
12281243 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1229− Failure err -> fail (show err)
1230− Success (x, i) -> do putIState i
1231− return x
1232− where imports :: IdrisParser ((Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState)
1244+ Failure err -> fail (show err)
1245+ Success (x, annots, i) ->
1246+ do putIState i
1247+ sendHighlighting (addPath annots fname)
1248+ return x
1249+ where imports :: IdrisParser ((Maybe (Docstring ()), [String],
1250+ [ImportInfo],
1251+ Maybe Delta),
1252+ [(FC, OutputAnnotation)], IState)
12331253 imports = do whiteSpace
1234− (mdoc, mname) <- moduleHeader
1254+ (mdoc, mname, annots) <- moduleHeader
12351255 ps <- many import_
12361256 mrk <- mark
12371257 isEof <- lookAheadMatches eof
@@ -1239,7 +1259,12 @@ parseImports fname input
12391259 then Nothing
12401260 else Just mrk
12411261 i <- get
1242− return ((mdoc, mname, ps, mrk'), i)
1262+ return ((mdoc, mname, ps, mrk'), annots, i)
1263+ addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]
1264+ addPath [] _ = []
1265+ addPath ((fc, AnnNamespace ns Nothing) : annots) path =
1266+ (fc, AnnNamespace ns (Just path)) : addPath annots path
1267+ addPath (annot:annots) path = annot : addPath annots path
12431268
12441269-- | There should be a better way of doing this...
12451270findFC :: Doc -> (FC, String)
@@ -1351,23 +1376,37 @@ loadSource lidr f toline
13511376 file <- if lidr then tclift $ unlit f file_in else return file_in
13521377 (mdocs, mname, imports_in, pos) <- parseImports f file
13531378 ai <- getAutoImports
1354− let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in
1379+ let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
13551380 ids <- allImportDirs
13561381 ibcsd <- valIBCSubDir i
1357− mapM_ (\(re, f) ->
1382+ mapM_ (\(re, f, ns, nfc) ->
13581383 do fp <- findImport ids ibcsd f
13591384 case fp of
13601385 LIDR fn -> ifail $ "No ibc for " ++ f
13611386 IDR fn -> ifail $ "No ibc for " ++ f
1362− IBC fn src -> loadIBC True fn)
1363− [(re, fn) | (re, fn, _, _) <- imports]
1387+ IBC fn src ->
1388+ do loadIBC True fn
1389+ let srcFn = case src of
1390+ IDR fn -> Just fn
1391+ LIDR fn -> Just fn
1392+ _ -> Nothing
1393+ sendHighlighting [(nfc, AnnNamespace ns srcFn)])
1394+ [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
13641395 reportParserWarnings
13651396
13661397 -- process and check module aliases
13671398 let modAliases = M.fromList
1368− [(prep alias, prep realName) | (reexport, realName, Just alias, fc) <- imports]
1399+ [ (prep alias, prep realName)
1400+ | ImportInfo { import_reexport = reexport
1401+ , import_path = realName
1402+ , import_rename = Just (alias, _)
1403+ , import_location = fc } <- imports
1404+ ]
13691405 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1370− aliasNames = [(alias, fc) | (_, _, Just alias, fc) <- imports]
1406+ aliasNames = [ (alias, fc)
1407+ | ImportInfo { import_rename = Just (alias, _)
1408+ , import_location = fc } <- imports
1409+ ]
13711410 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
13721411 case map head . filter ((/= 1) . length) $ histogram of
13731412 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
@@ -1379,7 +1418,12 @@ loadSource lidr f toline
13791418 -- record package info in .ibc
13801419 imps <- allImportDirs
13811420 mapM_ addIBC (map IBCImportDir imps)
1382− mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
1421+ mapM_ (addIBC . IBCImport)
1422+ [ (reexport, realName)
1423+ | ImportInfo { import_reexport = reexport
1424+ , import_path = realName
1425+ } <- imports
1426+ ]
13831427 let syntax = defaultSyntax{ syn_namespace = reverse mname,
13841428 maxline = toline }
13851429 ist <- getIState
@@ -1463,11 +1507,11 @@ loadSource lidr f toline
14631507 where
14641508 namespaces :: [String] -> [PDecl] -> [PDecl]
14651509 namespaces [] ds = ds
1466− namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1510+ namespaces (x:xs) ds = [PNamespace x NoFC (namespaces xs ds)]
14671511
14681512 toMutual :: PDecl -> PDecl
14691513 toMutual m@(PMutual _ d) = m
1470− toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1514+ toMutual (PNamespace x fc ds) = PNamespace x fc (map toMutual ds)
14711515 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
14721516 case x of
14731517 PClauses{} -> r