on 54e4e41 help sign in
Idris-dev/src/Idris/Chaser.hs
152 lines 6.2 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
68-- Strip quotes and the backslash escapes that Haskeline adds
69extractFileName :: String -> String
70extractFileName ('"':xs) = takeWhile (/= '"') xs
71extractFileName ('\'':xs) = takeWhile (/= '\'') xs
72extractFileName x = build x []
73 where
74 build [] acc = reverse $ dropWhile (== ' ') acc
75 build ('\\':' ':xs) acc = build xs (' ':acc)
76 build (x:xs) acc = build xs (x:acc)
78getIModTime (IBC i _) = getModificationTime i
79getIModTime (IDR i) = getModificationTime i
80getIModTime (LIDR i) = getModificationTime i
82buildTree :: [FilePath] -> -- already guaranteed built
83 FilePath -> Idris [ModuleTree]
84buildTree 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
92 let file = extractFileName f
93 logLvl 1 $ "CHASING " ++ show file
94 ibcsd <- valIBCSubDir i
95 ids <- allImportDirs
96 fp <- findImport ids ibcsd file
97 logLvl 1 $ "Found " ++ show fp
98 mt <- runIO $ getIModTime fp
99 if (file `elem` built)
100 then return [MTree fp False mt []]
101 else if file `elem` done
102 then return []
103 else mkChildren fp
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)
113 ms <- if srcexist then
114 do [MTree _ _ _ ms'] <- mkChildren src
115 return ms'
116 else return []
117 mt <- idrisCatch (runIO $ getModificationTime fn)
118 (\c -> runIO $ getIModTime src)
119 -- FIXME: It's also not up to date if anything it imports has
120 -- been modified since its own ibc has.
121 --
122 -- Issue #1592 on the issue tracker.
123 --
124 -- https://github.com/idris-lang/Idris-dev/issues/1592
125 ibcOutdated <- fn `younger` (getSrcFile src)
126 ibcValid <- hasValidIBCVersion fn
127 return [MTree (IBC fn src) (ibcOutdated || not ibcValid) mt ms]
129 getSrcFile (IBC _ src) = getSrcFile src
130 getSrcFile (LIDR src) = src
131 getSrcFile (IDR src) = src
133 younger ibc src = do exist <- runIO $ doesFileExist src
134 if exist then do
135 ibct <- runIO $ getModificationTime ibc
136 srct <- runIO $ getModificationTime src
137 return (srct > ibct)
138 else return False
140 children :: Bool -> FilePath -> [FilePath] -> Idris [ModuleTree]
141 children lit f done = -- idrisCatch
142 do exist <- runIO $ doesFileExist f
143 if exist then do
144 file_in <- runIO $ readSource f
145 file <- if lit then tclift $ unlit f file_in else return file_in
146 (_, _, modules, _) <- parseImports f file
147 -- The chaser should never report warnings from sub-modules
148 clearParserWarnings
149 ms <- mapM (btree done . import_path) modules
150 return (concat ms)
151 else return [] -- IBC with no source available
152-- (\c -> return []) -- error, can't chase modules here