{-|
Module      : Idris.Chaser
Description : Module chaser to determine cycles and import modules.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# 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 -> FilePath
(Int -> ModuleTree -> ShowS)
-> (ModuleTree -> FilePath)
-> ([ModuleTree] -> ShowS)
-> Show ModuleTree
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ModuleTree -> ShowS
showsPrec :: Int -> ModuleTree -> ShowS
$cshow :: ModuleTree -> FilePath
show :: ModuleTree -> FilePath
$cshowList :: [ModuleTree] -> ShowS
showList :: [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 a. Eq a => a -> [a] -> 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 -> FilePath
modName (IDR FilePath
fp) = FilePath
fp
modName (LIDR FilePath
fp) = FilePath
fp
modName (IBC FilePath
fp IFileType
src) = IFileType -> FilePath
modName IFileType
src

-- | Given a module tree, return the list of files to be loaded. If
-- any module has a descendent which needs reloading, return its
-- source, otherwise return the IBC
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
   -- Get the order of building modules. As we go we'll find things that
   -- need rebuilding, which we keep track of in the Set.
   -- The order of the list matters - things which get built first appear
   -- in the list first. We'll remove any repetition later.
   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 a.
a
-> StateT
     (Set IFileType, Map IFileType (Bool, [IFileType])) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
   modList (ModuleTree
m : [ModuleTree]
ms) = do (_, 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
                         fs' <- modList ms
                         pure (fs ++ 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
            (rebuild, res) <- m (Set IFileType, Map IFileType (Bool, [IFileType]))
forall s (m :: * -> *). MonadState s m => m s
get
            case M.lookup file res of
                 Just (Bool, [IFileType])
ms -> (Bool, [IFileType]) -> m (Bool, [IFileType])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool, [IFileType])
ms
                 Maybe (Bool, [IFileType])
Nothing -> do
                    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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 (rechkDep_in, toBuilds) = unzip toBuildsAll
                    let rechkDep = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
rechkDep_in

                    (rebuild, res) <- get

                    -- Needs rechecking if 'rechk' is true, or if any of the
                    -- modification times in 'deps' are later than tm, or
                    -- if any dependency needed rechecking
                    let depMod = UTCTime -> [IFileType] -> [ModuleTree] -> UTCTime
latest UTCTime
tm [] [ModuleTree]
deps
                    let 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

                    -- Remove duplicates, but keep the last...
                    let 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 = 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))

                    -- Cache the result
                    put (if needsRechk
                            then S.union path rebuild
                            else rebuild, M.insert file ret res)
                    pure ret

   chkReload :: Bool -> IFileType -> IFileType
chkReload Bool
False IFileType
p = IFileType
p
   chkReload Bool
True (IBC FilePath
fn IFileType
src) = Bool -> IFileType -> IFileType
chkReload Bool
True IFileType
src
   chkReload Bool
True IFileType
p = IFileType
p

   getSrc :: IFileType -> IFileType
getSrc (IBC FilePath
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

-- | Strip quotes and the backslash escapes that Haskeline adds
extractFileName :: String -> String
extractFileName :: ShowS
extractFileName (Char
'"':FilePath
xs) = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'"') FilePath
xs
extractFileName (Char
'\'':FilePath
xs) = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'\'') FilePath
xs
extractFileName FilePath
x = FilePath -> ShowS
build FilePath
x []
                        where
                            build :: FilePath -> ShowS
build [] FilePath
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
' ') FilePath
acc
                            build (Char
'\\':Char
' ':FilePath
xs) FilePath
acc = FilePath -> ShowS
build FilePath
xs (Char
' 'Char -> ShowS
forall a. a -> [a] -> [a]
:FilePath
acc)
                            build (Char
x:FilePath
xs) FilePath
acc = FilePath -> ShowS
build FilePath
xs (Char
xChar -> ShowS
forall a. a -> [a] -> [a]
:FilePath
acc)

getIModTime :: IFileType -> IO UTCTime
getIModTime (IBC FilePath
i IFileType
_) = FilePath -> IO UTCTime
getModificationTime FilePath
i
getIModTime (IDR FilePath
i) = FilePath -> IO UTCTime
getModificationTime FilePath
i
getIModTime (LIDR FilePath
i) = FilePath -> IO UTCTime
getModificationTime FilePath
i

getImports :: [(FilePath, [ImportInfo])]
           -> [FilePath]
           -> Idris [(FilePath, [ImportInfo])]
getImports :: [(FilePath, [ImportInfo])]
-> [FilePath] -> Idris [(FilePath, [ImportInfo])]
getImports [(FilePath, [ImportInfo])]
acc [] = [(FilePath, [ImportInfo])] -> Idris [(FilePath, [ImportInfo])]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(FilePath, [ImportInfo])]
acc
getImports [(FilePath, [ImportInfo])]
acc (FilePath
f : [FilePath]
fs) = do
   i <- Idris IState
getIState
   let file = ShowS
extractFileName FilePath
f
   ibcsd <- valIBCSubDir i
   idrisCatch (do
       srcds <- allSourceDirs
       fp <- findImport srcds ibcsd file
       let parsef = IFileType -> FilePath
fname IFileType
fp
       case lookup parsef acc of
            Just [ImportInfo]
_ -> [(FilePath, [ImportInfo])]
-> [FilePath] -> Idris [(FilePath, [ImportInfo])]
getImports [(FilePath, [ImportInfo])]
acc [FilePath]
fs
            Maybe [ImportInfo]
_ -> do
               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
$ FilePath -> IO Bool
doesFileExist FilePath
parsef
               if exist then do
                   src_in <- runIO $ readSource parsef
                   src <- if lit fp then tclift $ unlit parsef src_in
                                    else return src_in
                   (_, _, modules, _) <- parseImports parsef src
                   clearParserWarnings
                   getImports ((parsef, modules) : acc)
                              (fs ++ map import_path modules)
                     else getImports ((parsef, []) : acc) fs)
        (\Err
_ -> [(FilePath, [ImportInfo])]
-> [FilePath] -> Idris [(FilePath, [ImportInfo])]
getImports [(FilePath, [ImportInfo])]
acc [FilePath]
fs) -- not in current soure tree, ignore
  where
    lit :: IFileType -> Bool
lit (LIDR FilePath
_) = Bool
True
    lit IFileType
_ = Bool
False

    fname :: IFileType -> FilePath
fname (IDR FilePath
fn) = FilePath
fn
    fname (LIDR FilePath
fn) = FilePath
fn
    fname (IBC FilePath
_ IFileType
src) = IFileType -> FilePath
fname IFileType
src

buildTree :: [FilePath]                 -- ^ already guaranteed built
          -> [(FilePath, [ImportInfo])] -- ^ import lists (don't reparse)
          -> FilePath
          -> Idris [ModuleTree]
buildTree :: [FilePath]
-> [(FilePath, [ImportInfo])] -> FilePath -> Idris [ModuleTree]
buildTree [FilePath]
built [(FilePath, [ImportInfo])]
importlists FilePath
fp = StateT
  [(FilePath, [ModuleTree])]
  (StateT IState (ExceptT Err IO))
  [ModuleTree]
-> [(FilePath, [ModuleTree])] -> Idris [ModuleTree]
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ([FilePath]
-> FilePath
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
btree [] FilePath
fp) []
 where
  addFile :: FilePath -> [ModuleTree] ->
             StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]
  addFile :: FilePath
-> [ModuleTree]
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
addFile FilePath
f [ModuleTree]
m = do fs <- StateT
  [(FilePath, [ModuleTree])]
  (StateT IState (ExceptT Err IO))
  [(FilePath, [ModuleTree])]
forall s (m :: * -> *). MonadState s m => m s
get
                   put ((f, m) : fs)
                   return m

  btree :: [FilePath] -> FilePath ->
           StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]
  btree :: [FilePath]
-> FilePath
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
btree [FilePath]
stk FilePath
f =
    do i <- Idris IState
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) IState
forall (m :: * -> *) a.
Monad m =>
m a -> StateT [(FilePath, [ModuleTree])] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Idris IState
getIState
       let file = ShowS
extractFileName FilePath
f
       lift $ logLvl 1 $ "CHASING " ++ show file ++ " (" ++ show fp ++ ")"
       ibcsd <- lift $ valIBCSubDir i
       ids   <- lift allImportDirs
       fp   <- lift $ findImport ids ibcsd file
       lift $ logLvl 1 $ "Found " ++ show fp
       mt <- lift $ runIO $ getIModTime fp
       if (file `elem` built)
          then return [MTree fp False mt []]
               else if file `elem` stk then
                       do lift $ tclift $ tfail
                            (Msg $ "Cycle detected in imports: "
                                     ++ showSep " -> " (reverse (file : stk)))
                 else do donetree <- get
                         case lookup file donetree of
                            Just [ModuleTree]
t -> [ModuleTree]
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
forall a.
a
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return [ModuleTree]
t
                            Maybe [ModuleTree]
_ -> do ms <- FilePath
-> IFileType
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
mkChildren FilePath
file IFileType
fp
                                    addFile file ms

    where mkChildren :: FilePath
-> IFileType
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
mkChildren FilePath
file (LIDR FilePath
fn) = do ms <- Bool
-> FilePath
-> [FilePath]
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
children Bool
True FilePath
fn (FilePath
file FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath]
stk)
                                         mt <- lift $ runIO $ getModificationTime fn
                                         return [MTree (LIDR fn) True mt ms]
          mkChildren FilePath
file (IDR FilePath
fn) = do ms <- Bool
-> FilePath
-> [FilePath]
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
children Bool
False FilePath
fn (FilePath
file FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath]
stk)
                                        mt <- lift $ runIO $ getModificationTime fn
                                        return [MTree (IDR fn) True mt ms]
          mkChildren FilePath
file (IBC FilePath
fn IFileType
src)
              = do srcexist <- Idris Bool
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) Bool
forall (m :: * -> *) a.
Monad m =>
m a -> StateT [(FilePath, [ModuleTree])] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris Bool
 -> StateT
      [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) Bool)
-> Idris Bool
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) 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
$ FilePath -> IO Bool
doesFileExist (IFileType -> FilePath
getSrcFile IFileType
src)
                   ms <- if srcexist then
                               do [MTree _ _ _ ms'] <- mkChildren file src
                                  return ms'
                             else return []
                   -- Modification time is the later of the source/ibc modification time
                   smt <- lift $ idrisCatch (runIO $ getIModTime src)
                                    (\Err
c -> IO UTCTime -> Idris UTCTime
forall a. IO a -> Idris a
runIO (IO UTCTime -> Idris UTCTime) -> IO UTCTime -> Idris UTCTime
forall a b. (a -> b) -> a -> b
$ FilePath -> IO UTCTime
getModificationTime FilePath
fn)
                   mt <- lift $ idrisCatch (do t <- runIO $ getModificationTime fn
                                               return (max smt t))
                                    (\Err
c -> UTCTime -> Idris UTCTime
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return UTCTime
smt)
                   -- FIXME: It's also not up to date if anything it imports has
                   -- been modified since its own ibc has.
                   --
                   -- Issue #1592 on the issue tracker.
                   --
                   -- https://github.com/idris-lang/Idris-dev/issues/1592
                   ibcOutdated <- lift $ fn `younger` (getSrcFile src)
                   -- FIXME (EB): The below 'hasValidIBCVersion' that's
                   -- commented out appears to be breaking reloading in vim
                   -- mode. Until we know why, I've commented it out.
                   ibcValid <- return True -- hasValidIBCVersion fn
                   return [MTree (IBC fn src) (ibcOutdated || not ibcValid) mt ms]

          getSrcFile :: IFileType -> FilePath
getSrcFile (IBC FilePath
_ IFileType
src) = IFileType -> FilePath
getSrcFile IFileType
src
          getSrcFile (LIDR FilePath
src) = FilePath
src
          getSrcFile (IDR FilePath
src) = FilePath
src

          younger :: FilePath -> FilePath -> Idris Bool
younger FilePath
ibc FilePath
src = do 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
$ FilePath -> IO Bool
doesFileExist FilePath
src
                               if exist then do
                                   ibct <- runIO $ getModificationTime ibc
                                   srct <- runIO $ getModificationTime src
                                   return (srct > ibct)
                                 else return False

  children :: Bool -> FilePath -> [FilePath] ->
              StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]
  children :: Bool
-> FilePath
-> [FilePath]
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
children Bool
lit FilePath
f [FilePath]
stk = -- idrisCatch
     do exist <- Idris Bool
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) Bool
forall (m :: * -> *) a.
Monad m =>
m a -> StateT [(FilePath, [ModuleTree])] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris Bool
 -> StateT
      [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) Bool)
-> Idris Bool
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) 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
$ FilePath -> IO Bool
doesFileExist FilePath
f
        if exist then do
            lift $ logLvl 1 $ "Reading source " ++ show f
            let modules = [ImportInfo]
-> ([ImportInfo] -> [ImportInfo])
-> Maybe [ImportInfo]
-> [ImportInfo]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] [ImportInfo] -> [ImportInfo]
forall a. a -> a
id (FilePath -> [(FilePath, [ImportInfo])] -> Maybe [ImportInfo]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup FilePath
f [(FilePath, [ImportInfo])]
importlists)
            ms <- mapM (btree stk . import_path) modules
            return (concat ms)
           else return [] -- IBC with no source available
--     (\c -> return []) -- error, can't chase modules here