git.iko.soy/Idris-dev
on 76ec3fe help sign in
Idris-dev/src/Idris/Chaser.hs
145 lines 5.7 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
18import Util.System (readSource, writeSource)
20data ModuleTree = MTree { mod_path :: IFileType,
21 mod_needsRecheck :: Bool,
22 mod_time :: UTCTime,
23 mod_deps :: [ModuleTree] }
24 deriving Show
26latest :: UTCTime -> [ModuleTree] -> UTCTime
27latest tm [] = tm
28latest tm (m : ms) = latest (max tm (mod_time m)) (ms ++ mod_deps m)
30-- Given a module tree, return the list of files to be loaded. If any
31-- module has a descendent which needs reloading, return its source, otherwise
32-- return the IBC
34getModuleFiles :: [ModuleTree] -> [IFileType]
35getModuleFiles ts = nub $ execState (modList ts) [] where
36 modList :: [ModuleTree] -> State [IFileType] ()
37 modList [] = return ()
38 modList (m : ms) = do modTree [] m; modList ms
40 modTree path (MTree p rechk tm deps)
41 = do let file = chkReload rechk p
42 -- Needs rechecking if 'rechk' is true, or if any of the
43 -- modification times in 'deps' are later than tm
44 let depMod = latest tm deps
45 let needsRechk = rechk || depMod > tm
47 st <- get
48 if needsRechk then put $ nub (getSrc file : updateToSrc path st)
49 else put $ nub (file : st)
50-- when (not (ibc p) || rechk) $
51 mapM_ (modTree (getSrc p : path)) deps
53 ibc (IBC _ _) = True
54 ibc _ = False
56 chkReload False p = p
57 chkReload True (IBC fn src) = chkReload True src
58 chkReload True p = p
60 getSrc (IBC fn src) = getSrc src
61 getSrc f = f
63 updateToSrc path [] = []
64 updateToSrc path (x : xs) = if getSrc x `elem` path
65 then getSrc x : updateToSrc path xs
66 else x : updateToSrc path xs
68getIModTime (IBC i _) = getModificationTime i
69getIModTime (IDR i) = getModificationTime i
70getIModTime (LIDR i) = getModificationTime i
72buildTree :: [FilePath] -> -- already guaranteed built
73 FilePath -> Idris [ModuleTree]
74buildTree built fp = btree [] fp
75-- = idrisCatch (btree [] fp)
76-- (\e -> do now <- runIO $ getCurrentTime
77-- iputStrLn (show e)
78-- return [MTree (IDR fp) True now []])
79 where
80 btree done f =
81 do i <- getIState
82 let file = takeWhile (/= ' ') f
83 iLOG $ "CHASING " ++ show file
84 ibcsd <- valIBCSubDir i
85 ids <- allImportDirs
86 fp <- findImport ids ibcsd file
87 iLOG $ "Found " ++ show fp
88 mt <- runIO $ getIModTime fp
89 if (file `elem` built)
90 then return [MTree fp False mt []]
91 else if file `elem` done
92 then return []
93 else mkChildren fp
95 where mkChildren (LIDR fn) = do ms <- children True fn (f:done)
96 mt <- runIO $ getModificationTime fn
97 return [MTree (LIDR fn) True mt ms]
98 mkChildren (IDR fn) = do ms <- children False fn (f:done)
99 mt <- runIO $ getModificationTime fn
100 return [MTree (IDR fn) True mt ms]
101 mkChildren (IBC fn src)
102 = do srcexist <- runIO $ doesFileExist (getSrcFile src)
103 ms <- if srcexist then
104 do [MTree _ _ _ ms'] <- mkChildren src
105 return ms'
106 else return []
107 mt <- idrisCatch (runIO $ getModificationTime fn)
108 (\c -> runIO $ getIModTime src)
109 ok <- checkIBCUpToDate fn src
110 return [MTree (IBC fn src) ok mt ms]
112 getSrcFile (IBC _ src) = getSrcFile src
113 getSrcFile (LIDR src) = src
114 getSrcFile (IDR src) = src
116 -- FIXME: It's also not up to date if anything it imports has
117 -- been modified since its own ibc has.
118 --
119 -- Issue #1592 on the issue tracker.
120 --
121 -- https://github.com/idris-lang/Idris-dev/issues/1592
123 checkIBCUpToDate fn (LIDR src) = older fn src
124 checkIBCUpToDate fn (IDR src) = older fn src
126 older ibc src = do exist <- runIO $ doesFileExist src
127 if exist then do
128 ibct <- runIO $ getModificationTime ibc
129 srct <- runIO $ getModificationTime src
130 return (srct >= ibct)
131 else return False
133 children :: Bool -> FilePath -> [FilePath] -> Idris [ModuleTree]
134 children lit f done = -- idrisCatch
135 do exist <- runIO $ doesFileExist f
136 if exist then do
137 file_in <- runIO $ readSource f
138 file <- if lit then tclift $ unlit f file_in else return file_in
139 (_, _, modules, _) <- parseImports f file
140 -- The chaser should never report warnings from sub-modules
141 clearParserWarnings
142 ms <- mapM (btree done) [realName | (_, realName, alias, fc) <- modules]
143 return (concat ms)
144 else return [] -- IBC with no source available
145-- (\c -> return []) -- error, can't chase modules here