git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/Chaser.hs
144 lines 5.6 kB history raw
1module Idris.Chaser(buildTree, getModuleFiles, ModuleTree(..)) where
3import Idris.Parser
4import Idris.AbsSyntax
5import Idris.Imports
6import Idris.Unlit
7import Idris.Error
8import Idris.IBC
10import System.FilePath
11import System.Directory
12import Data.Time.Clock
13import Control.Monad.Trans
14import Control.Monad.State
15import Data.List
17import Debug.Trace
19data ModuleTree = MTree { mod_path :: IFileType,
20 mod_needsRecheck :: Bool,
21 mod_time :: UTCTime,
22 mod_deps :: [ModuleTree] }
23 deriving Show
25latest :: UTCTime -> [ModuleTree] -> UTCTime
26latest tm [] = tm
27latest tm (m : ms) = latest (max tm (mod_time m)) (ms ++ mod_deps m)
29-- Given a module tree, return the list of files to be loaded. If any
30-- module has a descendent which needs reloading, return its source, otherwise
31-- return the IBC
33getModuleFiles :: [ModuleTree] -> [IFileType]
34getModuleFiles ts = nub $ execState (modList ts) [] where
35 modList :: [ModuleTree] -> State [IFileType] ()
36 modList [] = return ()
37 modList (m : ms) = do modTree [] m; modList ms
39 modTree path (MTree p rechk tm deps)
40 = do let file = chkReload rechk p
41 -- Needs rechecking if 'rechk' is true, or if any of the
42 -- modification times in 'deps' are later than tm
43 let depMod = latest tm deps
44 let needsRechk = rechk || depMod > tm
46 st <- get
47 if needsRechk then put $ nub (getSrc file : updateToSrc path st)
48 else put $ nub (file : st)
49-- when (not (ibc p) || rechk) $
50 mapM_ (modTree (getSrc p : path)) deps
52 ibc (IBC _ _) = True
53 ibc _ = False
55 chkReload False p = p
56 chkReload True (IBC fn src) = chkReload True src
57 chkReload True p = p
59 getSrc (IBC fn src) = getSrc src
60 getSrc f = f
62 updateToSrc path [] = []
63 updateToSrc path (x : xs) = if getSrc x `elem` path
64 then getSrc x : updateToSrc path xs
65 else x : updateToSrc path xs
67getIModTime (IBC i _) = getModificationTime i
68getIModTime (IDR i) = getModificationTime i
69getIModTime (LIDR i) = getModificationTime i
71buildTree :: [FilePath] -> -- already guaranteed built
72 FilePath -> Idris [ModuleTree]
73buildTree built fp = btree [] fp
74-- = idrisCatch (btree [] fp)
75-- (\e -> do now <- runIO $ getCurrentTime
76-- iputStrLn (show e)
77-- return [MTree (IDR fp) True now []])
78 where
79 btree done f =
80 do i <- getIState
81 let file = takeWhile (/= ' ') f
82 iLOG $ "CHASING " ++ show file
83 ibcsd <- valIBCSubDir i
84 ids <- allImportDirs
85 fp <- findImport ids ibcsd file
86 iLOG $ "Found " ++ show fp
87 mt <- runIO $ getIModTime fp
88 if (file `elem` built)
89 then return [MTree fp False mt []]
90 else if file `elem` done
91 then return []
92 else mkChildren fp
94 where mkChildren (LIDR fn) = do ms <- children True fn (f:done)
95 mt <- runIO $ getModificationTime fn
96 return [MTree (LIDR fn) True mt ms]
97 mkChildren (IDR fn) = do ms <- children False fn (f:done)
98 mt <- runIO $ getModificationTime fn
99 return [MTree (IDR fn) True mt ms]
100 mkChildren (IBC fn src)
101 = do srcexist <- runIO $ doesFileExist (getSrcFile src)
102 ms <- if srcexist then
103 do [MTree _ _ _ ms'] <- mkChildren src
104 return ms'
105 else return []
106 mt <- idrisCatch (runIO $ getModificationTime fn)
107 (\c -> runIO $ getIModTime src)
108 ok <- checkIBCUpToDate fn src
109 return [MTree (IBC fn src) ok mt ms]
111 getSrcFile (IBC _ src) = getSrcFile src
112 getSrcFile (LIDR src) = src
113 getSrcFile (IDR src) = src
115 -- FIXME: It's also not up to date if anything it imports has
116 -- been modified since its own ibc has.
117 --
118 -- Issue #1592 on the issue tracker.
119 --
120 -- https://github.com/idris-lang/Idris-dev/issues/1592
122 checkIBCUpToDate fn (LIDR src) = older fn src
123 checkIBCUpToDate fn (IDR src) = older fn src
125 older ibc src = do exist <- runIO $ doesFileExist src
126 if exist then do
127 ibct <- runIO $ getModificationTime ibc
128 srct <- runIO $ getModificationTime src
129 return (srct > ibct)
130 else return False
132 children :: Bool -> FilePath -> [FilePath] -> Idris [ModuleTree]
133 children lit f done = -- idrisCatch
134 do exist <- runIO $ doesFileExist f
135 if exist then do
136 file_in <- runIO $ readFile f
137 file <- if lit then tclift $ unlit f file_in else return file_in
138 (_, modules, _) <- parseImports f file
139 -- The chaser should never report warnings from sub-modules
140 clearParserWarnings
141 ms <- mapM (btree done) [realName | (realName, alias, fc) <- modules]
142 return (concat ms)
143 else return [] -- IBC with no source available
144-- (\c -> return []) -- error, can't chase modules here