git.iko.soy/Idris-dev
on master help sign in
Fix import public error

IBCs should not import as public if the parent is not itself imported as public.

commitf56f05e4d5c49a94a8d2a34cbf20742b108225cf authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 11 Jul 2015, 17:51 (11 years ago) parent268459c
3 files changed+6−6
compare with master
unifiedsplit
libs/contrib/Data/Fun.idr+1−1 src/Idris/IBC.hs+4−4 test/dsl002/Resimp.idr+1−1
libs/contrib/Data/Fun.idr+1−1
@@ -1,6 +1,6 @@
11module Data.Fun
22
3−import Data.Vect
3+import public Data.Vect
44
55%default total
66
src/Idris/IBC.hs+4−4
@@ -312,7 +312,7 @@ process reexp i fn = do
312312 srcok <- runIO $ doesFileExist source
313313 when srcok $ timestampOlder source fn
314314 pImportDirs =<< getEntry [] "ibc_importdirs" i
315− pImports =<< getEntry [] "ibc_imports" i
315+ pImports reexp =<< getEntry [] "ibc_imports" i
316316 pImps =<< getEntry [] "ibc_implicits" i
317317 pFixes =<< getEntry [] "ibc_fixes" i
318318 pStatics =<< getEntry [] "ibc_statics" i
@@ -383,8 +383,8 @@ pAutoHints ns = mapM_ (\(n,h) -> addAutoHint n h) ns
383383pImportDirs :: [FilePath] -> Idris ()
384384pImportDirs fs = mapM_ addImportDir fs
385385
386−pImports :: [(Bool, FilePath)] -> Idris ()
387−pImports fs
386+pImports :: Bool -> [(Bool, FilePath)] -> Idris ()
387+pImports reexp fs
388388 = do mapM_ (\(re, f) ->
389389 do i <- getIState
390390 ibcsd <- valIBCSubDir i
@@ -398,7 +398,7 @@ pImports fs
398398 ifail "Must be an ibc"
399399 IDR fn -> do logLvl 1 $ "Failed at " ++ fn
400400 ifail "Must be an ibc"
401− IBC fn src -> loadIBC re fn)
401+ IBC fn src -> loadIBC (reexp && re) fn)
402402 fs
403403
404404pImps :: [(Name, [PArg])] -> Idris ()
test/dsl002/Resimp.idr+1−1
@@ -1,6 +1,6 @@
11module Resimp
22
3−import Data.Vect
3+import public Data.Vect
44import public Data.Fin
55
66-- IO operations which read a resource