a3fa5a4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Bring module loading into Idris monad

This allows proper error signaling, compared to IO, which is important for IDESlave

commita3fa5a487ea0de7f1810934a76b2422520c279e9 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 2 May 2014, 20:24 (12 years ago) parent89c3853

4 files changed+11−10

compare with master

unifiedsplit

src/Idris/Chaser.hs+1−1 src/Idris/IBC.hs+1−1 src/Idris/Imports.hs+7−6 src/Idris/Parser.hs+2−2

src/Idris/Chaser.hs+1−1

@@ -82,7 +82,7 @@ buildTree built fp = btree [] fp

8282 iLOG $ "CHASING " ++ show file

8383 ibcsd <- valIBCSubDir i

8484 ids <- allImportDirs

85− fp <- runIO $ findImport ids ibcsd file

85+ fp <- findImport ids ibcsd file

8686 iLOG $ "Found " ++ show fp

8787 mt <- runIO $ getIModTime fp

8888 if (file `elem` built)

src/Idris/IBC.hs+1−1

@@ -300,7 +300,7 @@ pImports fs

300300 = do mapM_ (\f -> do i <- getIState

301301 ibcsd <- valIBCSubDir i

302302 ids <- allImportDirs

303− fp <- runIO $ findImport ids ibcsd f

303+ fp <- findImport ids ibcsd f

304304 if (f `elem` imported i)

305305 then iLOG $ "Already read " ++ f

306306 else do putIState (i { imported = f : imported i })

src/Idris/Imports.hs+7−6

@@ -1,6 +1,7 @@

11module Idris.Imports where

33import Idris.AbsSyntax

4+import Idris.Error

56import Idris.Core.TT

67import Paths_idris

@@ -43,15 +44,15 @@ ibcPathWithFallback ibcsd fp = do let ibcp = ibcPath ibcsd True fp

4344ibcPathNoFallback :: FilePath -> FilePath -> FilePath

4445ibcPathNoFallback ibcsd fp = ibcPath ibcsd True fp

4546

46−findImport :: [FilePath] -> FilePath -> FilePath -> IO IFileType

47−findImport [] ibcsd fp = fail $ "Can't find import " ++ fp

47+findImport :: [FilePath] -> FilePath -> FilePath -> Idris IFileType

48+findImport [] ibcsd fp = ierror . Msg $ "Can't find import " ++ fp

4849findImport (d:ds) ibcsd fp = do let fp_full = d </> fp

49− ibcp <- ibcPathWithFallback ibcsd fp_full

50+ ibcp <- runIO $ ibcPathWithFallback ibcsd fp_full

5051 let idrp = srcPath fp_full

5152 let lidrp = lsrcPath fp_full

52− ibc <- doesFileExist ibcp

53− idr <- doesFileExist idrp

54− lidr <- doesFileExist lidrp

53+ ibc <- runIO $ doesFileExist ibcp

54+ idr <- runIO $ doesFileExist idrp

55+ lidr <- runIO $ doesFileExist lidrp

5556-- when idr $ putStrLn $ idrp ++ " ok"

5657-- when lidr $ putStrLn $ lidrp ++ " ok"

5758-- when ibc $ putStrLn $ ibcp ++ " ok"

src/Idris/Parser.hs+2−2

@@ -1169,7 +1169,7 @@ loadModule' outh f

11691169 let file = takeWhile (/= ' ') f

11701170 ibcsd <- valIBCSubDir i

11711171 ids <- allImportDirs

1172− fp <- liftIO $ findImport ids ibcsd file

1172+ fp <- findImport ids ibcsd file

11731173 if file `elem` imported i

11741174 then iLOG $ "Already read " ++ file

11751175 else do putIState (i { imported = file : imported i })

@@ -1219,7 +1219,7 @@ loadSource h lidr f

12191219 (mname, imports, pos) <- parseImports f file

12201220 ids <- allImportDirs

12211221 ibcsd <- valIBCSubDir i

1222− mapM_ (\f -> do fp <- runIO $ findImport ids ibcsd f

1222+ mapM_ (\f -> do fp <- findImport ids ibcsd f

12231223 case fp of

12241224 LIDR fn -> ifail $ "No ibc for " ++ f

12251225 IDR fn -> ifail $ "No ibc for " ++ f