8bd99ed · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -356,6 +356,9 @@ Extra-source-files:

356 test/basic015/run

357 test/basic015/*.idr

358 test/basic015/expected

359+ test/basic016/run

360+ test/basic016/*.idr

361+ test/basic016/expected

359

362

360 test/bignum001/run

363 test/bignum001/run

361 test/bignum001/*.idr

364 test/bignum001/*.idr

src/Idris/Chaser.hs+29−16

@@ -1,5 +1,6 @@

1module Idris.Chaser(buildTree, getImports, getModuleFiles, ModuleTree(..)) where

2

3+import Idris.Core.TT

3import Idris.Parser

4import Idris.Parser

4import Idris.AbsSyntax

5import Idris.AbsSyntax

5import Idris.Imports

6import Idris.Imports

@@ -79,22 +80,31 @@ getIModTime (IBC i _) = getModificationTime i

79getIModTime (IDR i) = getModificationTime i

80getIModTime (IDR i) = getModificationTime i

80getIModTime (LIDR i) = getModificationTime i

81getIModTime (LIDR i) = getModificationTime i

81

82

83+getImports :: [(FilePath, [ImportInfo])] -> [FilePath] ->

82−getImports :: FilePath -> Idris (FilePath, [ImportInfo])

84+ Idris [(FilePath, [ImportInfo])]

83−getImports f = do

85+getImports acc [] = return acc

86+getImports acc (f : fs) = do

84− i <- getIState

87+ i <- getIState

85− let file = extractFileName f

88+ let file = extractFileName f

86− ibcsd <- valIBCSubDir i

89+ ibcsd <- valIBCSubDir i

87− ids <- allImportDirs

90+ ids <- allImportDirs

91+ idrisCatch (do

88− fp <- findImport ids ibcsd file

92+ fp <- findImport ["."] ibcsd file

89 let parsef = fname fp

93 let parsef = fname fp

94+ case lookup parsef acc of

95+ Just _ -> getImports acc fs

96+ _ -> do

90− exist <- runIO $ doesFileExist parsef

97+ exist <- runIO $ doesFileExist parsef

91− if exist then do

98+ if exist then do

92− src_in <- runIO $ readSource parsef

99+ src_in <- runIO $ readSource parsef

93− src <- if lit fp then tclift $ unlit parsef src_in else return src_in

100+ src <- if lit fp then tclift $ unlit parsef src_in

101+ else return src_in

94− (_, _, modules, _) <- parseImports parsef src

102+ (_, _, modules, _) <- parseImports parsef src

95− clearParserWarnings

103+ clearParserWarnings

96− return (parsef, modules)

104+ getImports ((parsef, modules) : acc)

105+ (fs ++ map import_path modules)

97− else return (parsef, [])

106+ else getImports ((parsef, []) : acc) fs)

107+ (\_ -> getImports acc fs) -- not in current soure tree, ignore

98 where

108 where

99 lit (LIDR _) = True

109 lit (LIDR _) = True

100 lit _ = False

110 lit _ = False

@@ -127,7 +137,10 @@ buildTree built importlists fp = evalStateT (btree [] fp) []

127 mt <- lift $ runIO $ getIModTime fp

137 mt <- lift $ runIO $ getIModTime fp

128 if (file `elem` built)

138 if (file `elem` built)

129 then return [MTree fp False mt []]

139 then return [MTree fp False mt []]

130− else if file `elem` stk then return []

140+ else if file `elem` stk then

141+ do lift $ tclift $ tfail

142+ (Msg $ "Cycle detected in imports: "

143+ ++ showSep " -> " (reverse (file : stk)))

131 else do donetree <- get

144 else do donetree <- get

132 case lookup file donetree of

145 case lookup file donetree of

133 Just t -> return t

146 Just t -> return t

src/Idris/REPL.hs+3−2

@@ -1513,8 +1513,9 @@ loadInputs inputs toline -- furthest line to read in input source files

1513 -- For each ifile list, check it and build ibcs in the same clean IState

1514 -- so that they don't interfere with each other when checking

1515

1516− importlists <- mapM getImports inputs

1516+ importlists <- getImports [] inputs

1517+

1517− logLvl 5 (show (map (\(i,m) -> (i, map import_path m)) importlists))

1518+ logLvl 1 (show (map (\(i,m) -> (i, map import_path m)) importlists))

1518

1519

1519 let ninputs = zip [1..] inputs

1520 let ninputs = zip [1..] inputs

1520 ifiles <- mapWhileOK (\(num, input) ->

1521 ifiles <- mapWhileOK (\(num, input) ->

test/basic016/CycleA.idrnew file+4

@@ -0,0 +1,4 @@

1+module CycleA

2+

3+import CycleB

4+

test/basic016/CycleB.idrnew file+5

@@ -0,0 +1,5 @@

1+module CycleB

2+

3+import CycleC

4+

5+

test/basic016/CycleC.idrnew file+4

@@ -0,0 +1,4 @@

1+module CycleC

2+

3+import CycleA

4+

test/basic016/expectednew file+1

@@ -0,0 +1 @@

1+Cycle detected in imports: CycleA.idr -> CycleB -> CycleC -> CycleA -> CycleB

test/basic016/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ CycleA.idr --check

3+rm -f *.ibc