on master help sign in
Cache information when module chasing

In particular - don't parse import lists more than once for each file, and once a part of the import tree is built, don't build it again. Fixes #2730

commitfe38aac9c9699f061bf9dc5f5e2e741d7a9bdb69 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 13 Oct 2015, 23:50 (11 years ago) parent4249691
3 files changed+74−39
src/Idris/Chaser.hs+68−38 src/Idris/Elab/Utils.hs+1 src/Idris/REPL.hs+5−1
src/Idris/Chaser.hs+68−38
@@ -1,4 +1,4 @@
1−module Idris.Chaser(buildTree, getModuleFiles, ModuleTree(..)) where
1+module Idris.Chaser(buildTree, getImports, getModuleFiles, ModuleTree(..)) where
22
33import Idris.Parser
44import Idris.AbsSyntax
@@ -79,42 +79,74 @@ getIModTime (IBC i _) = getModificationTime i
7979getIModTime (IDR i) = getModificationTime i
8080getIModTime (LIDR i) = getModificationTime i
8181
82−buildTree :: [FilePath] -> -- already guaranteed built
83− FilePath -> Idris [ModuleTree]
84−buildTree built fp = btree [] fp
85−-- = idrisCatch (btree [] fp)
86−-- (\e -> do now <- runIO $ getCurrentTime
87−-- iputStrLn (show e)
88−-- return [MTree (IDR fp) True now []])
89− where
90− btree done f =
91− do i <- getIState
82+getImports :: FilePath -> Idris (FilePath, [ImportInfo])
83+getImports f = do
84+ i <- getIState
9285 let file = extractFileName f
93− logLvl 1 $ "CHASING " ++ show file
9486 ibcsd <- valIBCSubDir i
9587 ids <- allImportDirs
9688 fp <- findImport ids ibcsd file
97− logLvl 1 $ "Found " ++ show fp
98− mt <- runIO $ getIModTime fp
89+ let parsef = fname fp
90+ exist <- runIO $ doesFileExist parsef
91+ if exist then do
92+ src_in <- runIO $ readSource parsef
93+ src <- if lit fp then tclift $ unlit parsef src_in else return src_in
94+ (_, _, modules, _) <- parseImports parsef src
95+ clearParserWarnings
96+ return (parsef, modules)
97+ else return (parsef, [])
98+ where
99+ lit (LIDR _) = True
100+ lit _ = False
101+
102+ fname (IDR fn) = fn
103+ fname (LIDR fn) = fn
104+ fname (IBC _ src) = fname src
105+
106+buildTree :: [FilePath] -> -- already guaranteed built
107+ [(FilePath, [ImportInfo])] -> -- import lists (don't reparse)
108+ FilePath -> Idris [ModuleTree]
109+buildTree built importlists fp = evalStateT (btree [] fp) []
110+ where
111+ addFile :: FilePath -> [ModuleTree] ->
112+ StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]
113+ addFile f m = do fs <- get
114+ put ((f, m) : fs)
115+ return m
116+
117+ btree :: [FilePath] -> FilePath ->
118+ StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]
119+ btree stk f =
120+ do i <- lift getIState
121+ let file = extractFileName f
122+ lift $ logLvl 1 $ "CHASING " ++ show file ++ " (" ++ show fp ++ ")"
123+ ibcsd <- lift $ valIBCSubDir i
124+ ids <- lift $ allImportDirs
125+ fp <- lift $ findImport ids ibcsd file
126+ lift $ logLvl 1 $ "Found " ++ show fp
127+ mt <- lift $ runIO $ getIModTime fp
99128 if (file `elem` built)
100129 then return [MTree fp False mt []]
101− else if file `elem` done
102− then return []
103− else mkChildren fp
104−
105− where mkChildren (LIDR fn) = do ms <- children True fn (f:done)
106− mt <- runIO $ getModificationTime fn
107− return [MTree (LIDR fn) True mt ms]
108− mkChildren (IDR fn) = do ms <- children False fn (f:done)
109− mt <- runIO $ getModificationTime fn
110− return [MTree (IDR fn) True mt ms]
111− mkChildren (IBC fn src)
112− = do srcexist <- runIO $ doesFileExist (getSrcFile src)
130+ else if file `elem` stk then return []
131+ else do donetree <- get
132+ case lookup file donetree of
133+ Just t -> return t
134+ _ -> do ms <- mkChildren file fp
135+ addFile file ms
136+
137+ where mkChildren file (LIDR fn) = do ms <- children True fn (file : stk)
138+ mt <- lift $ runIO $ getModificationTime fn
139+ return [MTree (LIDR fn) True mt ms]
140+ mkChildren file (IDR fn) = do ms <- children False fn (file : stk)
141+ mt <- lift $ runIO $ getModificationTime fn
142+ return [MTree (IDR fn) True mt ms]
143+ mkChildren file (IBC fn src)
144+ = do srcexist <- lift $ runIO $ doesFileExist (getSrcFile src)
113145 ms <- if srcexist then
114− do [MTree _ _ _ ms'] <- mkChildren src
146+ do [MTree _ _ _ ms'] <- mkChildren file src
115147 return ms'
116148 else return []
117− mt <- idrisCatch (runIO $ getModificationTime fn)
149+ mt <- lift $ idrisCatch (runIO $ getModificationTime fn)
118150 (\c -> runIO $ getIModTime src)
119151 -- FIXME: It's also not up to date if anything it imports has
120152 -- been modified since its own ibc has.
@@ -122,7 +154,7 @@ buildTree built fp = btree [] fp
122154 -- Issue #1592 on the issue tracker.
123155 --
124156 -- https://github.com/idris-lang/Idris-dev/issues/1592
125− ibcOutdated <- fn `younger` (getSrcFile src)
157+ ibcOutdated <- lift $ fn `younger` (getSrcFile src)
126158 -- FIXME (EB): The below 'hasValidIBCVersion' that's
127159 -- commented out appears to be breaking reloading in vim
128160 -- mode. Until we know why, I've commented it out.
@@ -140,16 +172,14 @@ buildTree built fp = btree [] fp
140172 return (srct > ibct)
141173 else return False
142174
143− children :: Bool -> FilePath -> [FilePath] -> Idris [ModuleTree]
144− children lit f done = -- idrisCatch
145− do exist <- runIO $ doesFileExist f
175+ children :: Bool -> FilePath -> [FilePath] ->
176+ StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]
177+ children lit f stk = -- idrisCatch
178+ do exist <- lift $ runIO $ doesFileExist f
146179 if exist then do
147− file_in <- runIO $ readSource f
148− file <- if lit then tclift $ unlit f file_in else return file_in
149− (_, _, modules, _) <- parseImports f file
150− -- The chaser should never report warnings from sub-modules
151− clearParserWarnings
152− ms <- mapM (btree done . import_path) modules
180+ lift $ logLvl 1 $ "Reading source " ++ show f
181+ let modules = maybe [] id (lookup f importlists)
182+ ms <- mapM (btree stk . import_path) modules
153183 return (concat ms)
154184 else return [] -- IBC with no source available
155185-- (\c -> return []) -- error, can't chase modules here
src/Idris/Elab/Utils.hs+1
@@ -51,6 +51,7 @@ checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)
5151checkAddDef add toplvl fc mkerr [] = return []
5252checkAddDef add toplvl fc mkerr ((n, (i, top, t, psns)) : ns)
5353 = do ctxt <- getContext
54+ logLvl 5 $ "Rechecking deferred name " ++ show (n, t)
5455 (t', _) <- recheckC fc (mkerr n) [] t
5556 when add $ do addDeferred [(n, (i, top, t, psns, toplvl))]
5657 addIBC (IBCDef n)
src/Idris/REPL.hs+5−1
@@ -1513,11 +1513,15 @@ loadInputs inputs toline -- furthest line to read in input source files
15131513 -- For each ifile list, check it and build ibcs in the same clean IState
15141514 -- so that they don't interfere with each other when checking
15151515
1516+ importlists <- mapM getImports inputs
1517+ logLvl 5 (show (map (\(i,m) -> (i, map import_path m)) importlists))
1518+
15161519 let ninputs = zip [1..] inputs
15171520 ifiles <- mapWhileOK (\(num, input) ->
15181521 do putIState ist
1519− modTree <- buildTree
1522+ modTree <- buildTree
15201523 (map snd (take (num-1) ninputs))
1524+ importlists
15211525 input
15221526 let ifiles = getModuleFiles modTree
15231527 logLvl 1 ("MODULE TREE : " ++ show modTree)