diff --git a/src/Idris/ModTree.idr b/src/Idris/ModTree.idr index 1c9f89184..a9f2d2b94 100644 --- a/src/Idris/ModTree.idr +++ b/src/Idris/ModTree.idr @@ -63,9 +63,10 @@ mkModTree : {auto c : Ref Ctxt Defs} -> {auto a : Ref AllMods (List (ModuleIdent, ModTree))} -> FC -> (done : List ModuleIdent) -> -- if 'mod' is here we have a cycle - (mod : ModuleIdent) -> + (modFP : Maybe FileName) -> -- Sometimes we know already know what the file name is + (mod : ModuleIdent) -> -- Otherwise we'll compute it from the module name Core ModTree -mkModTree loc done mod +mkModTree loc done modFP mod = if mod `elem` done then throw (CyclicImports (done ++ [mod])) else @@ -75,10 +76,10 @@ mkModTree loc done mod -- If we've seen it before, reuse what we found case lookup mod all of Nothing => - do file <- nsToSource loc mod + do file <- maybe (nsToSource loc mod) pure modFP modInfo <- readHeader file let imps = map path (imports modInfo) - ms <- traverse (mkModTree loc (mod :: done)) imps + ms <- traverse (mkModTree loc (mod :: done) Nothing) imps let mt = MkModTree mod (Just file) ms all <- get AllMods put AllMods ((mod, mt) :: all) @@ -131,7 +132,7 @@ getBuildMods loc done fname if fname_ns `elem` map buildNS done then pure [] else - do t <- mkModTree {a} loc [] fname_ns + do t <- mkModTree {a} loc [] (Just fname) fname_ns dm <- newRef DoneMod empty o <- newRef BuildOrder [] mkBuildMods {d=dm} {o} t diff --git a/tests/Main.idr b/tests/Main.idr index 45bfcbf49..92c8a4e7a 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -32,7 +32,7 @@ ttimpTests idrisTests : List String idrisTests - = -- Fundamental language feturea + = -- Fundamental language features ["basic001", "basic002", "basic003", "basic004", "basic005", "basic006", "basic007", "basic008", "basic009", "basic010", "basic011", "basic012", "basic013", "basic014", "basic015", @@ -71,6 +71,7 @@ idrisTests "interface017", -- Miscellaneous REPL "interpreter001", "interpreter002", "interpreter003", "interpreter004", + "interpreter005", -- Implicit laziness, lazy evaluation "lazy001", -- QTT and linearity related diff --git a/tests/idris2/interpreter005/Issue37.idr b/tests/idris2/interpreter005/Issue37.idr new file mode 100644 index 000000000..30e9189ec --- /dev/null +++ b/tests/idris2/interpreter005/Issue37.idr @@ -0,0 +1,2 @@ +test : String +test = "IDR" diff --git a/tests/idris2/interpreter005/Issue37.lidr b/tests/idris2/interpreter005/Issue37.lidr new file mode 100644 index 000000000..a3526a9ce --- /dev/null +++ b/tests/idris2/interpreter005/Issue37.lidr @@ -0,0 +1,2 @@ +> test : String +> test = "LIDR" diff --git a/tests/idris2/interpreter005/expected b/tests/idris2/interpreter005/expected new file mode 100644 index 000000000..df04f6a71 --- /dev/null +++ b/tests/idris2/interpreter005/expected @@ -0,0 +1,3 @@ +1/1: Building Issue37 (Issue37.lidr) +Main> "LIDR" +Main> Bye for now! diff --git a/tests/idris2/interpreter005/input b/tests/idris2/interpreter005/input new file mode 100644 index 000000000..131b8c414 --- /dev/null +++ b/tests/idris2/interpreter005/input @@ -0,0 +1,2 @@ +test +:q diff --git a/tests/idris2/interpreter005/run b/tests/idris2/interpreter005/run new file mode 100755 index 000000000..c8ffb8d83 --- /dev/null +++ b/tests/idris2/interpreter005/run @@ -0,0 +1,3 @@ +$1 --no-banner --no-color --console-width 0 Issue37.lidr < input + +rm -rf build