{-|
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 (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 a.
a
-> StateT
     (Set IFileType, Map IFileType (Bool, [IFileType])) Identity a
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 a. a -> m a
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)
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 ([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

                    -- 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
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

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

                    -- Cache the result
                    (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 a. a -> m a
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 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
   IState
i <- Idris IState
getIState
   let file :: FilePath
file = ShowS
extractFileName FilePath
f
   FilePath
ibcsd <- IState -> Idris FilePath
valIBCSubDir IState
i
   Idris [(FilePath, [ImportInfo])]
-> (Err -> Idris [(FilePath, [ImportInfo])])
-> Idris [(FilePath, [ImportInfo])]
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do
       [FilePath]
srcds <- Idris [FilePath]
allSourceDirs
       IFileType
fp <- [FilePath] -> FilePath -> FilePath -> Idris IFileType
findImport [FilePath]
srcds FilePath
ibcsd FilePath
file
       let parsef :: FilePath
parsef = IFileType -> FilePath
fname IFileType
fp
       case FilePath -> [(FilePath, [ImportInfo])] -> Maybe [ImportInfo]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup FilePath
parsef [(FilePath, [ImportInfo])]
acc of
            Just [ImportInfo]
_ -> [(FilePath, [ImportInfo])]
-> [FilePath] -> Idris [(FilePath, [ImportInfo])]
getImports [(FilePath, [ImportInfo])]
acc [FilePath]
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
$ FilePath -> IO Bool
doesFileExist FilePath
parsef
               if Bool
exist then do
                   FilePath
src_in <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO (IO FilePath -> Idris FilePath) -> IO FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSource FilePath
parsef
                   FilePath
src <- if IFileType -> Bool
lit IFileType
fp then TC FilePath -> Idris FilePath
forall a. TC a -> Idris a
tclift (TC FilePath -> Idris FilePath) -> TC FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> TC FilePath
unlit FilePath
parsef FilePath
src_in
                                    else FilePath -> Idris FilePath
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
src_in
                   (Maybe (Docstring ())
_, [FilePath]
_, [ImportInfo]
modules, Maybe Mark
_) <- FilePath
-> FilePath
-> Idris
     (Maybe (Docstring ()), [FilePath], [ImportInfo], Maybe Mark)
parseImports FilePath
parsef FilePath
src
                   Idris ()
clearParserWarnings
                   [(FilePath, [ImportInfo])]
-> [FilePath] -> Idris [(FilePath, [ImportInfo])]
getImports ((FilePath
parsef, [ImportInfo]
modules) (FilePath, [ImportInfo])
-> [(FilePath, [ImportInfo])] -> [(FilePath, [ImportInfo])]
forall a. a -> [a] -> [a]
: [(FilePath, [ImportInfo])]
acc)
                              ([FilePath]
fs [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ (ImportInfo -> FilePath) -> [ImportInfo] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map ImportInfo -> FilePath
import_path [ImportInfo]
modules)
                     else [(FilePath, [ImportInfo])]
-> [FilePath] -> Idris [(FilePath, [ImportInfo])]
getImports ((FilePath
parsef, []) (FilePath, [ImportInfo])
-> [(FilePath, [ImportInfo])] -> [(FilePath, [ImportInfo])]
forall a. a -> [a] -> [a]
: [(FilePath, [ImportInfo])]
acc) [FilePath]
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 [(FilePath, [ModuleTree])]
fs <- StateT
  [(FilePath, [ModuleTree])]
  (StateT IState (ExceptT Err IO))
  [(FilePath, [ModuleTree])]
forall s (m :: * -> *). MonadState s m => m s
get
                   [(FilePath, [ModuleTree])]
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((FilePath
f, [ModuleTree]
m) (FilePath, [ModuleTree])
-> [(FilePath, [ModuleTree])] -> [(FilePath, [ModuleTree])]
forall a. a -> [a] -> [a]
: [(FilePath, [ModuleTree])]
fs)
                   [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]
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 IState
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 :: FilePath
file = ShowS
extractFileName FilePath
f
       Idris ()
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) ()
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 ()
 -> StateT
      [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) ())
-> Idris ()
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) ()
forall a b. (a -> b) -> a -> b
$ Int -> FilePath -> Idris ()
logLvl Int
1 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"CHASING " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> FilePath
show FilePath
file FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
" (" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> FilePath
show FilePath
fp FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
")"
       FilePath
ibcsd <- Idris FilePath
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     FilePath
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 FilePath
 -> StateT
      [(FilePath, [ModuleTree])]
      (StateT IState (ExceptT Err IO))
      FilePath)
-> Idris FilePath
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     FilePath
forall a b. (a -> b) -> a -> b
$ IState -> Idris FilePath
valIBCSubDir IState
i
       [FilePath]
ids   <- Idris [FilePath]
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [FilePath]
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 [FilePath]
allImportDirs
       IFileType
fp   <- Idris IFileType
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     IFileType
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 IFileType
 -> StateT
      [(FilePath, [ModuleTree])]
      (StateT IState (ExceptT Err IO))
      IFileType)
-> Idris IFileType
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     IFileType
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath -> FilePath -> Idris IFileType
findImport [FilePath]
ids FilePath
ibcsd FilePath
file
       Idris ()
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) ()
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 ()
 -> StateT
      [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) ())
-> Idris ()
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) ()
forall a b. (a -> b) -> a -> b
$ Int -> FilePath -> Idris ()
logLvl Int
1 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Found " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ IFileType -> FilePath
forall a. Show a => a -> FilePath
show IFileType
fp
       UTCTime
mt <- Idris UTCTime
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) UTCTime
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 UTCTime
 -> StateT
      [(FilePath, [ModuleTree])]
      (StateT IState (ExceptT Err IO))
      UTCTime)
-> Idris UTCTime
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) UTCTime
forall a b. (a -> b) -> a -> b
$ 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
$ IFileType -> IO UTCTime
getIModTime IFileType
fp
       if (FilePath
file FilePath -> [FilePath] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath]
built)
          then [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 [IFileType -> Bool -> UTCTime -> [ModuleTree] -> ModuleTree
MTree IFileType
fp Bool
False UTCTime
mt []]
               else if FilePath
file FilePath -> [FilePath] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath]
stk then
                       do Idris [ModuleTree]
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
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 [ModuleTree]
 -> StateT
      [(FilePath, [ModuleTree])]
      (StateT IState (ExceptT Err IO))
      [ModuleTree])
-> Idris [ModuleTree]
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [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
                            (FilePath -> Err
forall t. FilePath -> Err' t
Msg (FilePath -> Err) -> FilePath -> Err
forall a b. (a -> b) -> a -> b
$ FilePath
"Cycle detected in imports: "
                                     FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath -> [FilePath] -> FilePath
showSep FilePath
" -> " ([FilePath] -> [FilePath]
forall a. [a] -> [a]
reverse (FilePath
file FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath]
stk)))
                 else do [(FilePath, [ModuleTree])]
donetree <- StateT
  [(FilePath, [ModuleTree])]
  (StateT IState (ExceptT Err IO))
  [(FilePath, [ModuleTree])]
forall s (m :: * -> *). MonadState s m => m s
get
                         case FilePath -> [(FilePath, [ModuleTree])] -> Maybe [ModuleTree]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup FilePath
file [(FilePath, [ModuleTree])]
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 [ModuleTree]
ms <- FilePath
-> IFileType
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
mkChildren FilePath
file IFileType
fp
                                    FilePath
-> [ModuleTree]
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
addFile FilePath
file [ModuleTree]
ms

    where mkChildren :: FilePath
-> IFileType
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
mkChildren FilePath
file (LIDR FilePath
fn) = do [ModuleTree]
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)
                                         UTCTime
mt <- Idris UTCTime
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) UTCTime
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 UTCTime
 -> StateT
      [(FilePath, [ModuleTree])]
      (StateT IState (ExceptT Err IO))
      UTCTime)
-> Idris UTCTime
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) UTCTime
forall a b. (a -> b) -> a -> b
$ 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
                                         [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 [IFileType -> Bool -> UTCTime -> [ModuleTree] -> ModuleTree
MTree (FilePath -> IFileType
LIDR FilePath
fn) Bool
True UTCTime
mt [ModuleTree]
ms]
          mkChildren FilePath
file (IDR FilePath
fn) = do [ModuleTree]
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)
                                        UTCTime
mt <- Idris UTCTime
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) UTCTime
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 UTCTime
 -> StateT
      [(FilePath, [ModuleTree])]
      (StateT IState (ExceptT Err IO))
      UTCTime)
-> Idris UTCTime
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) UTCTime
forall a b. (a -> b) -> a -> b
$ 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
                                        [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 [IFileType -> Bool -> UTCTime -> [ModuleTree] -> ModuleTree
MTree (FilePath -> IFileType
IDR FilePath
fn) Bool
True UTCTime
mt [ModuleTree]
ms]
          mkChildren FilePath
file (IBC FilePath
fn IFileType
src)
              = do Bool
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)
                   [ModuleTree]
ms <- if Bool
srcexist then
                               do [MTree IFileType
_ Bool
_ UTCTime
_ [ModuleTree]
ms'] <- FilePath
-> IFileType
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
mkChildren FilePath
file IFileType
src
                                  [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]
ms'
                             else [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 []
                   -- Modification time is the later of the source/ibc modification time
                   UTCTime
smt <- Idris UTCTime
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) UTCTime
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 UTCTime
 -> StateT
      [(FilePath, [ModuleTree])]
      (StateT IState (ExceptT Err IO))
      UTCTime)
-> Idris UTCTime
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) UTCTime
forall a b. (a -> b) -> a -> b
$ Idris UTCTime -> (Err -> Idris UTCTime) -> Idris UTCTime
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (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
$ IFileType -> IO UTCTime
getIModTime IFileType
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)
                   UTCTime
mt <- Idris UTCTime
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) UTCTime
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 UTCTime
 -> StateT
      [(FilePath, [ModuleTree])]
      (StateT IState (ExceptT Err IO))
      UTCTime)
-> Idris UTCTime
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) UTCTime
forall a b. (a -> b) -> a -> b
$ Idris UTCTime -> (Err -> Idris UTCTime) -> Idris UTCTime
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do UTCTime
t <- 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
                                               UTCTime -> Idris UTCTime
forall a. a -> StateT IState (ExceptT Err IO) a
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 -> 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
                   Bool
ibcOutdated <- 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
$ FilePath
fn FilePath -> FilePath -> Idris Bool
`younger` (IFileType -> FilePath
getSrcFile IFileType
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.
                   Bool
ibcValid <- Bool
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) Bool
forall a.
a
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True -- hasValidIBCVersion fn
                   [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 [IFileType -> Bool -> UTCTime -> [ModuleTree] -> ModuleTree
MTree (FilePath -> IFileType -> IFileType
IBC FilePath
fn IFileType
src) (Bool
ibcOutdated Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
ibcValid) UTCTime
mt [ModuleTree]
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 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
$ FilePath -> IO Bool
doesFileExist FilePath
src
                               if Bool
exist then do
                                   UTCTime
ibct <- 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
ibc
                                   UTCTime
srct <- 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
src
                                   Bool -> Idris Bool
forall a. a -> StateT IState (ExceptT Err IO) a
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 a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
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 Bool
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 Bool
exist then do
            Idris ()
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) ()
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 ()
 -> StateT
      [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) ())
-> Idris ()
-> StateT
     [(FilePath, [ModuleTree])] (StateT IState (ExceptT Err IO)) ()
forall a b. (a -> b) -> a -> b
$ Int -> FilePath -> Idris ()
logLvl Int
1 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Reading source " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> FilePath
show FilePath
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 (FilePath -> [(FilePath, [ImportInfo])] -> Maybe [ImportInfo]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup FilePath
f [(FilePath, [ImportInfo])]
importlists)
            [[ModuleTree]]
ms <- (ImportInfo
 -> StateT
      [(FilePath, [ModuleTree])]
      (StateT IState (ExceptT Err IO))
      [ModuleTree])
-> [ImportInfo]
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [[ModuleTree]]
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 ([FilePath]
-> FilePath
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
btree [FilePath]
stk (FilePath
 -> StateT
      [(FilePath, [ModuleTree])]
      (StateT IState (ExceptT Err IO))
      [ModuleTree])
-> (ImportInfo -> FilePath)
-> ImportInfo
-> StateT
     [(FilePath, [ModuleTree])]
     (StateT IState (ExceptT Err IO))
     [ModuleTree]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ImportInfo -> FilePath
import_path) [ImportInfo]
modules
            [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]] -> [ModuleTree]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[ModuleTree]]
ms)
           else [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 [] -- IBC with no source available
--     (\c -> return []) -- error, can't chase modules here