{-# LANGUAGE FlexibleContexts #-}
module Idris.Chaser(
buildTree, getImports
, getModuleFiles
, ModuleTree(..)
) where
import Idris.AbsSyntax
import Idris.Core.TT
import Idris.Error
import Idris.Imports
import Idris.Parser
import Idris.Unlit
import Control.Monad.State
import Data.List
import qualified Data.Map as M
import qualified Data.Set as S
import Data.Time.Clock
import System.Directory
import Util.System (readSource)
data ModuleTree = MTree { ModuleTree -> IFileType
mod_path :: IFileType,
ModuleTree -> Bool
mod_needsRecheck :: Bool,
ModuleTree -> UTCTime
mod_time :: UTCTime,
ModuleTree -> [ModuleTree]
mod_deps :: [ModuleTree] }
deriving Int -> ModuleTree -> ShowS
[ModuleTree] -> ShowS
ModuleTree -> String
(Int -> ModuleTree -> ShowS)
-> (ModuleTree -> String)
-> ([ModuleTree] -> ShowS)
-> Show ModuleTree
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModuleTree] -> ShowS
$cshowList :: [ModuleTree] -> ShowS
show :: ModuleTree -> String
$cshow :: ModuleTree -> String
showsPrec :: Int -> ModuleTree -> ShowS
$cshowsPrec :: Int -> ModuleTree -> ShowS
Show
latest :: UTCTime -> [IFileType] -> [ModuleTree] -> UTCTime
latest :: UTCTime -> [IFileType] -> [ModuleTree] -> UTCTime
latest UTCTime
tm [IFileType]
done [] = UTCTime
tm
latest UTCTime
tm [IFileType]
done (ModuleTree
m : [ModuleTree]
ms)
| ModuleTree -> IFileType
mod_path ModuleTree
m IFileType -> [IFileType] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [IFileType]
done = UTCTime -> [IFileType] -> [ModuleTree] -> UTCTime
latest UTCTime
tm [IFileType]
done [ModuleTree]
ms
| Bool
otherwise = UTCTime -> [IFileType] -> [ModuleTree] -> UTCTime
latest (UTCTime -> UTCTime -> UTCTime
forall a. Ord a => a -> a -> a
max UTCTime
tm (ModuleTree -> UTCTime
mod_time ModuleTree
m)) (ModuleTree -> IFileType
mod_path ModuleTree
m IFileType -> [IFileType] -> [IFileType]
forall a. a -> [a] -> [a]
: [IFileType]
done) [ModuleTree]
ms
modName :: IFileType -> String
modName :: IFileType -> String
modName (IDR String
fp) = String
fp
modName (LIDR String
fp) = String
fp
modName (IBC String
fp IFileType
src) = IFileType -> String
modName IFileType
src
getModuleFiles :: [ModuleTree] -> [IFileType]
getModuleFiles :: [ModuleTree] -> [IFileType]
getModuleFiles [ModuleTree]
ts
= let ([IFileType]
files, (Set IFileType
rebuild, Map IFileType (Bool, [IFileType])
_)) = State
(Set IFileType, Map IFileType (Bool, [IFileType])) [IFileType]
-> (Set IFileType, Map IFileType (Bool, [IFileType]))
-> ([IFileType],
(Set IFileType, Map IFileType (Bool, [IFileType])))
forall s a. State s a -> s -> (a, s)
runState ([ModuleTree]
-> State
(Set IFileType, Map IFileType (Bool, [IFileType])) [IFileType]
modList [ModuleTree]
ts) (Set IFileType
forall a. Set a
S.empty, Map IFileType (Bool, [IFileType])
forall k a. Map k a
M.empty) in
Set IFileType -> [IFileType] -> [IFileType]
updateToSrc Set IFileType
rebuild ([IFileType] -> [IFileType]
forall a. [a] -> [a]
reverse [IFileType]
files)
where
modList :: [ModuleTree] ->
State (S.Set IFileType,
M.Map IFileType (Bool, [IFileType])) [IFileType]
modList :: [ModuleTree]
-> State
(Set IFileType, Map IFileType (Bool, [IFileType])) [IFileType]
modList [] = [IFileType]
-> State
(Set IFileType, Map IFileType (Bool, [IFileType])) [IFileType]
forall (m :: * -> *) a. Monad m => a -> m a
return []
modList (ModuleTree
m : [ModuleTree]
ms) = do (Bool
_, [IFileType]
fs) <- Set IFileType
-> ModuleTree
-> StateT
(Set IFileType, Map IFileType (Bool, [IFileType]))
Identity
(Bool, [IFileType])
forall (m :: * -> *).
MonadState (Set IFileType, Map IFileType (Bool, [IFileType])) m =>
Set IFileType -> ModuleTree -> m (Bool, [IFileType])
modTree Set IFileType
forall a. Set a
S.empty ModuleTree
m
[IFileType]
fs' <- [ModuleTree]
-> State
(Set IFileType, Map IFileType (Bool, [IFileType])) [IFileType]
modList [ModuleTree]
ms
[IFileType]
-> State
(Set IFileType, Map IFileType (Bool, [IFileType])) [IFileType]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([IFileType]
fs [IFileType] -> [IFileType] -> [IFileType]
forall a. [a] -> [a] -> [a]
++ [IFileType]
fs')
modTree :: Set IFileType -> ModuleTree -> m (Bool, [IFileType])
modTree Set IFileType
path m :: ModuleTree
m@(MTree IFileType
p Bool
rechk UTCTime
tm [ModuleTree]
deps)
= do let file :: IFileType
file = Bool -> IFileType -> IFileType
chkReload Bool
rechk IFileType
p
(Set IFileType
rebuild, Map IFileType (Bool, [IFileType])
res) <- m (Set IFileType, Map IFileType (Bool, [IFileType]))
forall s (m :: * -> *). MonadState s m => m s
get
case IFileType
-> Map IFileType (Bool, [IFileType]) -> Maybe (Bool, [IFileType])
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup IFileType
file Map IFileType (Bool, [IFileType])
res of
Just (Bool, [IFileType])
ms -> (Bool, [IFileType]) -> m (Bool, [IFileType])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool, [IFileType])
ms
Maybe (Bool, [IFileType])
Nothing -> do
[(Bool, [IFileType])]
toBuildsAll <- (ModuleTree -> m (Bool, [IFileType]))
-> [ModuleTree] -> m [(Bool, [IFileType])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Set IFileType -> ModuleTree -> m (Bool, [IFileType])
modTree (IFileType -> Set IFileType -> Set IFileType
forall a. Ord a => a -> Set a -> Set a
S.insert (IFileType -> IFileType
getSrc IFileType
p) Set IFileType
path)) [ModuleTree]
deps
let ([Bool]
rechkDep_in, [[IFileType]]
toBuilds) = [(Bool, [IFileType])] -> ([Bool], [[IFileType]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Bool, [IFileType])]
toBuildsAll
let rechkDep :: Bool
rechkDep = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
rechkDep_in
(Set IFileType
rebuild, Map IFileType (Bool, [IFileType])
res) <- m (Set IFileType, Map IFileType (Bool, [IFileType]))
forall s (m :: * -> *). MonadState s m => m s
get
let depMod :: UTCTime
depMod = UTCTime -> [IFileType] -> [ModuleTree] -> UTCTime
latest UTCTime
tm [] [ModuleTree]
deps
let needsRechk :: Bool
needsRechk = Bool
rechkDep Bool -> Bool -> Bool
|| Bool
rechk Bool -> Bool -> Bool
|| UTCTime
depMod UTCTime -> UTCTime -> Bool
forall a. Ord a => a -> a -> Bool
> UTCTime
tm
let rnub :: [IFileType] -> [IFileType]
rnub = [IFileType] -> [IFileType]
forall a. [a] -> [a]
reverse ([IFileType] -> [IFileType])
-> ([IFileType] -> [IFileType]) -> [IFileType] -> [IFileType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [IFileType] -> [IFileType]
forall a. Eq a => [a] -> [a]
nub ([IFileType] -> [IFileType])
-> ([IFileType] -> [IFileType]) -> [IFileType] -> [IFileType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [IFileType] -> [IFileType]
forall a. [a] -> [a]
reverse
let ret :: (Bool, [IFileType])
ret = if Bool
needsRechk
then (Bool
needsRechk, [IFileType] -> [IFileType]
rnub (IFileType -> IFileType
getSrc IFileType
file IFileType -> [IFileType] -> [IFileType]
forall a. a -> [a] -> [a]
: [[IFileType]] -> [IFileType]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[IFileType]]
toBuilds))
else (Bool
needsRechk, [IFileType] -> [IFileType]
rnub (IFileType
file IFileType -> [IFileType] -> [IFileType]
forall a. a -> [a] -> [a]
: [[IFileType]] -> [IFileType]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[IFileType]]
toBuilds))
(Set IFileType, Map IFileType (Bool, [IFileType])) -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (if Bool
needsRechk
then Set IFileType -> Set IFileType -> Set IFileType
forall a. Ord a => Set a -> Set a -> Set a
S.union Set IFileType
path Set IFileType
rebuild
else Set IFileType
rebuild, IFileType
-> (Bool, [IFileType])
-> Map IFileType (Bool, [IFileType])
-> Map IFileType (Bool, [IFileType])
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert IFileType
file (Bool, [IFileType])
ret Map IFileType (Bool, [IFileType])
res)
(Bool, [IFileType]) -> m (Bool, [IFileType])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool, [IFileType])
ret
chkReload :: Bool -> IFileType -> IFileType
chkReload Bool
False IFileType
p = IFileType
p
chkReload Bool
True (IBC String
fn IFileType
src) = Bool -> IFileType -> IFileType
chkReload Bool
True IFileType
src
chkReload Bool
True IFileType
p = IFileType
p
getSrc :: IFileType -> IFileType
getSrc (IBC String
fn IFileType
src) = IFileType -> IFileType
getSrc IFileType
src
getSrc IFileType
f = IFileType
f
updateToSrc :: Set IFileType -> [IFileType] -> [IFileType]
updateToSrc Set IFileType
rebuilds [] = []
updateToSrc Set IFileType
rebuilds (IFileType
x : [IFileType]
xs)
= if IFileType -> IFileType
getSrc IFileType
x IFileType -> Set IFileType -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set IFileType
rebuilds
then IFileType -> IFileType
getSrc IFileType
x IFileType -> [IFileType] -> [IFileType]
forall a. a -> [a] -> [a]
: Set IFileType -> [IFileType] -> [IFileType]
updateToSrc Set IFileType
rebuilds [IFileType]
xs
else IFileType
x IFileType -> [IFileType] -> [IFileType]
forall a. a -> [a] -> [a]
: Set IFileType -> [IFileType] -> [IFileType]
updateToSrc Set IFileType
rebuilds [IFileType]
xs
extractFileName :: String -> String
(Char
'"':String
xs) = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'"') String
xs
extractFileName (Char
'\'':String
xs) = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'\'') String
xs
extractFileName String
x = String -> ShowS
build String
x []
where
build :: String -> ShowS
build [] String
acc = ShowS
forall a. [a] -> [a]
reverse ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
' ') String
acc
build (Char
'\\':Char
' ':String
xs) String
acc = String -> ShowS
build String
xs (Char
' 'Char -> ShowS
forall a. a -> [a] -> [a]
:String
acc)
build (Char
x:String
xs) String
acc = String -> ShowS
build String
xs (Char
xChar -> ShowS
forall a. a -> [a] -> [a]
:String
acc)
getIModTime :: IFileType -> IO UTCTime
getIModTime (IBC String
i IFileType
_) = String -> IO UTCTime
getModificationTime String
i
getIModTime (IDR String
i) = String -> IO UTCTime
getModificationTime String
i
getIModTime (LIDR String
i) = String -> IO UTCTime
getModificationTime String
i
getImports :: [(FilePath, [ImportInfo])]
-> [FilePath]
-> Idris [(FilePath, [ImportInfo])]
getImports :: [(String, [ImportInfo])]
-> [String] -> Idris [(String, [ImportInfo])]
getImports [(String, [ImportInfo])]
acc [] = [(String, [ImportInfo])] -> Idris [(String, [ImportInfo])]
forall (m :: * -> *) a. Monad m => a -> m a
return [(String, [ImportInfo])]
acc
getImports [(String, [ImportInfo])]
acc (String
f : [String]
fs) = do
IState
i <- Idris IState
getIState
let file :: String
file = ShowS
extractFileName String
f
String
ibcsd <- IState -> Idris String
valIBCSubDir IState
i
Idris [(String, [ImportInfo])]
-> (Err -> Idris [(String, [ImportInfo])])
-> Idris [(String, [ImportInfo])]
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do
[String]
srcds <- Idris [String]
allSourceDirs
IFileType
fp <- [String] -> String -> String -> Idris IFileType
findImport [String]
srcds String
ibcsd String
file
let parsef :: String
parsef = IFileType -> String
fname IFileType
fp
case String -> [(String, [ImportInfo])] -> Maybe [ImportInfo]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
parsef [(String, [ImportInfo])]
acc of
Just [ImportInfo]
_ -> [(String, [ImportInfo])]
-> [String] -> Idris [(String, [ImportInfo])]
getImports [(String, [ImportInfo])]
acc [String]
fs
Maybe [ImportInfo]
_ -> do
Bool
exist <- IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO (IO Bool -> Idris Bool) -> IO Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ String -> IO Bool
doesFileExist String
parsef
if Bool
exist then do
String
src_in <- IO String -> Idris String
forall a. IO a -> Idris a
runIO (IO String -> Idris String) -> IO String -> Idris String
forall a b. (a -> b) -> a -> b
$ String -> IO String
readSource String
parsef
String
src <- if IFileType -> Bool
lit IFileType
fp then TC String -> Idris String
forall a. TC a -> Idris a
tclift (TC String -> Idris String) -> TC String -> Idris String
forall a b. (a -> b) -> a -> b
$ String -> String -> TC String
unlit String
parsef String
src_in
else String -> Idris String
forall (m :: * -> *) a. Monad m => a -> m a
return String
src_in
(Maybe (Docstring ())
_, [String]
_, [ImportInfo]
modules, Maybe Mark
_) <- String
-> String
-> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark)
parseImports String
parsef String
src
Idris ()
clearParserWarnings
[(String, [ImportInfo])]
-> [String] -> Idris [(String, [ImportInfo])]
getImports ((String
parsef, [ImportInfo]
modules) (String, [ImportInfo])
-> [(String, [ImportInfo])] -> [(String, [ImportInfo])]
forall a. a -> [a] -> [a]
: [(String, [ImportInfo])]
acc)
([String]
fs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (ImportInfo -> String) -> [ImportInfo] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ImportInfo -> String
import_path [ImportInfo]
modules)
else [(String, [ImportInfo])]
-> [String] -> Idris [(String, [ImportInfo])]
getImports ((String
parsef, []) (String, [ImportInfo])
-> [(String, [ImportInfo])] -> [(String, [ImportInfo])]
forall a. a -> [a] -> [a]
: [(String, [ImportInfo])]
acc) [String]
fs)
(\Err
_ -> [(String, [ImportInfo])]
-> [String] -> Idris [(String, [ImportInfo])]
getImports [(String, [ImportInfo])]
acc [String]
fs)
where
lit :: IFileType -> Bool
lit (LIDR String
_) = Bool
True
lit IFileType
_ = Bool
False
fname :: IFileType -> String
fname (IDR String
fn) = String
fn
fname (LIDR String
fn) = String
fn
fname (IBC String
_ IFileType
src) = IFileType -> String
fname IFileType
src
buildTree :: [FilePath]
-> [(FilePath, [ImportInfo])]
-> FilePath
-> Idris [ModuleTree]
buildTree :: [String]
-> [(String, [ImportInfo])] -> String -> Idris [ModuleTree]
buildTree [String]
built [(String, [ImportInfo])]
importlists String
fp = StateT [(String, [ModuleTree])] Idris [ModuleTree]
-> [(String, [ModuleTree])] -> Idris [ModuleTree]
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ([String]
-> String -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
btree [] String
fp) []
where
addFile :: FilePath -> [ModuleTree] ->
StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]
addFile :: String
-> [ModuleTree]
-> StateT [(String, [ModuleTree])] Idris [ModuleTree]
addFile String
f [ModuleTree]
m = do [(String, [ModuleTree])]
fs <- StateT [(String, [ModuleTree])] Idris [(String, [ModuleTree])]
forall s (m :: * -> *). MonadState s m => m s
get
[(String, [ModuleTree])]
-> StateT [(String, [ModuleTree])] Idris ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((String
f, [ModuleTree]
m) (String, [ModuleTree])
-> [(String, [ModuleTree])] -> [(String, [ModuleTree])]
forall a. a -> [a] -> [a]
: [(String, [ModuleTree])]
fs)
[ModuleTree] -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
forall (m :: * -> *) a. Monad m => a -> m a
return [ModuleTree]
m
btree :: [FilePath] -> FilePath ->
StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]
btree :: [String]
-> String -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
btree [String]
stk String
f =
do IState
i <- Idris IState -> StateT [(String, [ModuleTree])] Idris IState
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Idris IState
getIState
let file :: String
file = ShowS
extractFileName String
f
Idris () -> StateT [(String, [ModuleTree])] Idris ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris () -> StateT [(String, [ModuleTree])] Idris ())
-> Idris () -> StateT [(String, [ModuleTree])] Idris ()
forall a b. (a -> b) -> a -> b
$ Int -> String -> Idris ()
logLvl Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"CHASING " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
file String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
fp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
String
ibcsd <- Idris String -> StateT [(String, [ModuleTree])] Idris String
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris String -> StateT [(String, [ModuleTree])] Idris String)
-> Idris String -> StateT [(String, [ModuleTree])] Idris String
forall a b. (a -> b) -> a -> b
$ IState -> Idris String
valIBCSubDir IState
i
[String]
ids <- Idris [String] -> StateT [(String, [ModuleTree])] Idris [String]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Idris [String]
allImportDirs
IFileType
fp <- Idris IFileType -> StateT [(String, [ModuleTree])] Idris IFileType
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris IFileType
-> StateT [(String, [ModuleTree])] Idris IFileType)
-> Idris IFileType
-> StateT [(String, [ModuleTree])] Idris IFileType
forall a b. (a -> b) -> a -> b
$ [String] -> String -> String -> Idris IFileType
findImport [String]
ids String
ibcsd String
file
Idris () -> StateT [(String, [ModuleTree])] Idris ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris () -> StateT [(String, [ModuleTree])] Idris ())
-> Idris () -> StateT [(String, [ModuleTree])] Idris ()
forall a b. (a -> b) -> a -> b
$ Int -> String -> Idris ()
logLvl Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Found " String -> ShowS
forall a. [a] -> [a] -> [a]
++ IFileType -> String
forall a. Show a => a -> String
show IFileType
fp
UTCTime
mt <- StateT IState (ExceptT Err IO) UTCTime
-> StateT [(String, [ModuleTree])] Idris UTCTime
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT IState (ExceptT Err IO) UTCTime
-> StateT [(String, [ModuleTree])] Idris UTCTime)
-> StateT IState (ExceptT Err IO) UTCTime
-> StateT [(String, [ModuleTree])] Idris UTCTime
forall a b. (a -> b) -> a -> b
$ IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a. IO a -> Idris a
runIO (IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime)
-> IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a b. (a -> b) -> a -> b
$ IFileType -> IO UTCTime
getIModTime IFileType
fp
if (String
file String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
built)
then [ModuleTree] -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
forall (m :: * -> *) a. Monad m => a -> m a
return [IFileType -> Bool -> UTCTime -> [ModuleTree] -> ModuleTree
MTree IFileType
fp Bool
False UTCTime
mt []]
else if String
file String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
stk then
do Idris [ModuleTree]
-> StateT [(String, [ModuleTree])] Idris [ModuleTree]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris [ModuleTree]
-> StateT [(String, [ModuleTree])] Idris [ModuleTree])
-> Idris [ModuleTree]
-> StateT [(String, [ModuleTree])] Idris [ModuleTree]
forall a b. (a -> b) -> a -> b
$ TC [ModuleTree] -> Idris [ModuleTree]
forall a. TC a -> Idris a
tclift (TC [ModuleTree] -> Idris [ModuleTree])
-> TC [ModuleTree] -> Idris [ModuleTree]
forall a b. (a -> b) -> a -> b
$ Err -> TC [ModuleTree]
forall a. Err -> TC a
tfail
(String -> Err
forall t. String -> Err' t
Msg (String -> Err) -> String -> Err
forall a b. (a -> b) -> a -> b
$ String
"Cycle detected in imports: "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
" -> " ([String] -> [String]
forall a. [a] -> [a]
reverse (String
file String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
stk)))
else do [(String, [ModuleTree])]
donetree <- StateT [(String, [ModuleTree])] Idris [(String, [ModuleTree])]
forall s (m :: * -> *). MonadState s m => m s
get
case String -> [(String, [ModuleTree])] -> Maybe [ModuleTree]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
file [(String, [ModuleTree])]
donetree of
Just [ModuleTree]
t -> [ModuleTree] -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
forall (m :: * -> *) a. Monad m => a -> m a
return [ModuleTree]
t
Maybe [ModuleTree]
_ -> do [ModuleTree]
ms <- String
-> IFileType -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
mkChildren String
file IFileType
fp
String
-> [ModuleTree]
-> StateT [(String, [ModuleTree])] Idris [ModuleTree]
addFile String
file [ModuleTree]
ms
where mkChildren :: String
-> IFileType -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
mkChildren String
file (LIDR String
fn) = do [ModuleTree]
ms <- Bool
-> String
-> [String]
-> StateT [(String, [ModuleTree])] Idris [ModuleTree]
children Bool
True String
fn (String
file String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
stk)
UTCTime
mt <- StateT IState (ExceptT Err IO) UTCTime
-> StateT [(String, [ModuleTree])] Idris UTCTime
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT IState (ExceptT Err IO) UTCTime
-> StateT [(String, [ModuleTree])] Idris UTCTime)
-> StateT IState (ExceptT Err IO) UTCTime
-> StateT [(String, [ModuleTree])] Idris UTCTime
forall a b. (a -> b) -> a -> b
$ IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a. IO a -> Idris a
runIO (IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime)
-> IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a b. (a -> b) -> a -> b
$ String -> IO UTCTime
getModificationTime String
fn
[ModuleTree] -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
forall (m :: * -> *) a. Monad m => a -> m a
return [IFileType -> Bool -> UTCTime -> [ModuleTree] -> ModuleTree
MTree (String -> IFileType
LIDR String
fn) Bool
True UTCTime
mt [ModuleTree]
ms]
mkChildren String
file (IDR String
fn) = do [ModuleTree]
ms <- Bool
-> String
-> [String]
-> StateT [(String, [ModuleTree])] Idris [ModuleTree]
children Bool
False String
fn (String
file String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
stk)
UTCTime
mt <- StateT IState (ExceptT Err IO) UTCTime
-> StateT [(String, [ModuleTree])] Idris UTCTime
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT IState (ExceptT Err IO) UTCTime
-> StateT [(String, [ModuleTree])] Idris UTCTime)
-> StateT IState (ExceptT Err IO) UTCTime
-> StateT [(String, [ModuleTree])] Idris UTCTime
forall a b. (a -> b) -> a -> b
$ IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a. IO a -> Idris a
runIO (IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime)
-> IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a b. (a -> b) -> a -> b
$ String -> IO UTCTime
getModificationTime String
fn
[ModuleTree] -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
forall (m :: * -> *) a. Monad m => a -> m a
return [IFileType -> Bool -> UTCTime -> [ModuleTree] -> ModuleTree
MTree (String -> IFileType
IDR String
fn) Bool
True UTCTime
mt [ModuleTree]
ms]
mkChildren String
file (IBC String
fn IFileType
src)
= do Bool
srcexist <- Idris Bool -> StateT [(String, [ModuleTree])] Idris Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris Bool -> StateT [(String, [ModuleTree])] Idris Bool)
-> Idris Bool -> StateT [(String, [ModuleTree])] Idris Bool
forall a b. (a -> b) -> a -> b
$ IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO (IO Bool -> Idris Bool) -> IO Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ String -> IO Bool
doesFileExist (IFileType -> String
getSrcFile IFileType
src)
[ModuleTree]
ms <- if Bool
srcexist then
do [MTree IFileType
_ Bool
_ UTCTime
_ [ModuleTree]
ms'] <- String
-> IFileType -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
mkChildren String
file IFileType
src
[ModuleTree] -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
forall (m :: * -> *) a. Monad m => a -> m a
return [ModuleTree]
ms'
else [ModuleTree] -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
forall (m :: * -> *) a. Monad m => a -> m a
return []
UTCTime
smt <- StateT IState (ExceptT Err IO) UTCTime
-> StateT [(String, [ModuleTree])] Idris UTCTime
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT IState (ExceptT Err IO) UTCTime
-> StateT [(String, [ModuleTree])] Idris UTCTime)
-> StateT IState (ExceptT Err IO) UTCTime
-> StateT [(String, [ModuleTree])] Idris UTCTime
forall a b. (a -> b) -> a -> b
$ StateT IState (ExceptT Err IO) UTCTime
-> (Err -> StateT IState (ExceptT Err IO) UTCTime)
-> StateT IState (ExceptT Err IO) UTCTime
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a. IO a -> Idris a
runIO (IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime)
-> IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a b. (a -> b) -> a -> b
$ IFileType -> IO UTCTime
getIModTime IFileType
src)
(\Err
c -> IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a. IO a -> Idris a
runIO (IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime)
-> IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a b. (a -> b) -> a -> b
$ String -> IO UTCTime
getModificationTime String
fn)
UTCTime
mt <- StateT IState (ExceptT Err IO) UTCTime
-> StateT [(String, [ModuleTree])] Idris UTCTime
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT IState (ExceptT Err IO) UTCTime
-> StateT [(String, [ModuleTree])] Idris UTCTime)
-> StateT IState (ExceptT Err IO) UTCTime
-> StateT [(String, [ModuleTree])] Idris UTCTime
forall a b. (a -> b) -> a -> b
$ StateT IState (ExceptT Err IO) UTCTime
-> (Err -> StateT IState (ExceptT Err IO) UTCTime)
-> StateT IState (ExceptT Err IO) UTCTime
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do UTCTime
t <- IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a. IO a -> Idris a
runIO (IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime)
-> IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a b. (a -> b) -> a -> b
$ String -> IO UTCTime
getModificationTime String
fn
UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall (m :: * -> *) a. Monad m => a -> m a
return (UTCTime -> UTCTime -> UTCTime
forall a. Ord a => a -> a -> a
max UTCTime
smt UTCTime
t))
(\Err
c -> UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall (m :: * -> *) a. Monad m => a -> m a
return UTCTime
smt)
Bool
ibcOutdated <- Idris Bool -> StateT [(String, [ModuleTree])] Idris Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris Bool -> StateT [(String, [ModuleTree])] Idris Bool)
-> Idris Bool -> StateT [(String, [ModuleTree])] Idris Bool
forall a b. (a -> b) -> a -> b
$ String
fn String -> String -> Idris Bool
`younger` (IFileType -> String
getSrcFile IFileType
src)
Bool
ibcValid <- Bool -> StateT [(String, [ModuleTree])] Idris Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
[ModuleTree] -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
forall (m :: * -> *) a. Monad m => a -> m a
return [IFileType -> Bool -> UTCTime -> [ModuleTree] -> ModuleTree
MTree (String -> IFileType -> IFileType
IBC String
fn IFileType
src) (Bool
ibcOutdated Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
ibcValid) UTCTime
mt [ModuleTree]
ms]
getSrcFile :: IFileType -> String
getSrcFile (IBC String
_ IFileType
src) = IFileType -> String
getSrcFile IFileType
src
getSrcFile (LIDR String
src) = String
src
getSrcFile (IDR String
src) = String
src
younger :: String -> String -> Idris Bool
younger String
ibc String
src = do Bool
exist <- IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO (IO Bool -> Idris Bool) -> IO Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ String -> IO Bool
doesFileExist String
src
if Bool
exist then do
UTCTime
ibct <- IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a. IO a -> Idris a
runIO (IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime)
-> IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a b. (a -> b) -> a -> b
$ String -> IO UTCTime
getModificationTime String
ibc
UTCTime
srct <- IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a. IO a -> Idris a
runIO (IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime)
-> IO UTCTime -> StateT IState (ExceptT Err IO) UTCTime
forall a b. (a -> b) -> a -> b
$ String -> IO UTCTime
getModificationTime String
src
Bool -> Idris Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (UTCTime
srct UTCTime -> UTCTime -> Bool
forall a. Ord a => a -> a -> Bool
> UTCTime
ibct)
else Bool -> Idris Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
children :: Bool -> FilePath -> [FilePath] ->
StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]
children :: Bool
-> String
-> [String]
-> StateT [(String, [ModuleTree])] Idris [ModuleTree]
children Bool
lit String
f [String]
stk =
do Bool
exist <- Idris Bool -> StateT [(String, [ModuleTree])] Idris Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris Bool -> StateT [(String, [ModuleTree])] Idris Bool)
-> Idris Bool -> StateT [(String, [ModuleTree])] Idris Bool
forall a b. (a -> b) -> a -> b
$ IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO (IO Bool -> Idris Bool) -> IO Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ String -> IO Bool
doesFileExist String
f
if Bool
exist then do
Idris () -> StateT [(String, [ModuleTree])] Idris ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris () -> StateT [(String, [ModuleTree])] Idris ())
-> Idris () -> StateT [(String, [ModuleTree])] Idris ()
forall a b. (a -> b) -> a -> b
$ Int -> String -> Idris ()
logLvl Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Reading source " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
f
let modules :: [ImportInfo]
modules = [ImportInfo]
-> ([ImportInfo] -> [ImportInfo])
-> Maybe [ImportInfo]
-> [ImportInfo]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] [ImportInfo] -> [ImportInfo]
forall a. a -> a
id (String -> [(String, [ImportInfo])] -> Maybe [ImportInfo]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
f [(String, [ImportInfo])]
importlists)
[[ModuleTree]]
ms <- (ImportInfo -> StateT [(String, [ModuleTree])] Idris [ModuleTree])
-> [ImportInfo]
-> StateT [(String, [ModuleTree])] Idris [[ModuleTree]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([String]
-> String -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
btree [String]
stk (String -> StateT [(String, [ModuleTree])] Idris [ModuleTree])
-> (ImportInfo -> String)
-> ImportInfo
-> StateT [(String, [ModuleTree])] Idris [ModuleTree]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ImportInfo -> String
import_path) [ImportInfo]
modules
[ModuleTree] -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
forall (m :: * -> *) a. Monad m => a -> m a
return ([[ModuleTree]] -> [ModuleTree]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[ModuleTree]]
ms)
else [ModuleTree] -> StateT [(String, [ModuleTree])] Idris [ModuleTree]
forall (m :: * -> *) a. Monad m => a -> m a
return []