idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 12:42:02 +03:00
Code Issues Projects Releases Wiki Activity

[ fix #37 ] Use filename if we already know it

Browse Source
This commit is contained in:
Guillaume ALLAIS 2020-09-24 15:24:48 +01:00 committed by G. Allais
parent 0d08c0b81b
commit 416b9578e5
7 changed files with 20 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/Idris/ModTree.idr
View File

@ -63,9 +63,10 @@ mkModTree : {auto c : Ref Ctxt Defs} ->
{auto a : Ref AllMods (List (ModuleIdent, ModTree))} -> {auto a : Ref AllMods (List (ModuleIdent, ModTree))} ->
FC -> FC ->
(done : List ModuleIdent) -> -- if 'mod' is here we have a cycle (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 Core ModTree
mkModTree loc done mod mkModTree loc done modFP mod
= if mod `elem` done = if mod `elem` done
then throw (CyclicImports (done ++ [mod])) then throw (CyclicImports (done ++ [mod]))
else else
@ -75,10 +76,10 @@ mkModTree loc done mod
-- If we've seen it before, reuse what we found -- If we've seen it before, reuse what we found
case lookup mod all of case lookup mod all of
Nothing => Nothing =>
do file <- nsToSource loc mod do file <- maybe (nsToSource loc mod) pure modFP
modInfo <- readHeader file modInfo <- readHeader file
let imps = map path (imports modInfo) 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 let mt = MkModTree mod (Just file) ms
all <- get AllMods all <- get AllMods
put AllMods ((mod, mt) :: all) put AllMods ((mod, mt) :: all)
@ -131,7 +132,7 @@ getBuildMods loc done fname
if fname_ns `elem` map buildNS done if fname_ns `elem` map buildNS done
then pure [] then pure []
else else
do t <- mkModTree {a} loc [] fname_ns do t <- mkModTree {a} loc [] (Just fname) fname_ns
dm <- newRef DoneMod empty dm <- newRef DoneMod empty
o <- newRef BuildOrder [] o <- newRef BuildOrder []
mkBuildMods {d=dm} {o} t mkBuildMods {d=dm} {o} t

3
tests/Main.idr
View File

@ -32,7 +32,7 @@ ttimpTests
idrisTests : List String idrisTests : List String
idrisTests idrisTests
= -- Fundamental language feturea = -- Fundamental language features
["basic001", "basic002", "basic003", "basic004", "basic005", ["basic001", "basic002", "basic003", "basic004", "basic005",
"basic006", "basic007", "basic008", "basic009", "basic010", "basic006", "basic007", "basic008", "basic009", "basic010",
"basic011", "basic012", "basic013", "basic014", "basic015", "basic011", "basic012", "basic013", "basic014", "basic015",
@ -71,6 +71,7 @@ idrisTests
"interface017", "interface017",
-- Miscellaneous REPL -- Miscellaneous REPL
"interpreter001", "interpreter002", "interpreter003", "interpreter004", "interpreter001", "interpreter002", "interpreter003", "interpreter004",
"interpreter005",
-- Implicit laziness, lazy evaluation -- Implicit laziness, lazy evaluation
"lazy001", "lazy001",
-- QTT and linearity related -- QTT and linearity related

2
tests/idris2/interpreter005/Issue37.idr Normal file
View File

@ -0,0 +1,2 @@
test : String
test = "IDR"

2
tests/idris2/interpreter005/Issue37.lidr Normal file
View File

@ -0,0 +1,2 @@
> test : String
> test = "LIDR"

3
tests/idris2/interpreter005/expected Normal file
View File

@ -0,0 +1,3 @@
1/1: Building Issue37 (Issue37.lidr)
Main> "LIDR"
Main> Bye for now!

2
tests/idris2/interpreter005/input Normal file
View File

@ -0,0 +1,2 @@
test
:q

3
tests/idris2/interpreter005/run Executable file
View File

@ -0,0 +1,3 @@
$1 --no-banner --no-color --console-width 0 Issue37.lidr < input
rm -rf build