Fix visibility of imported things

Fixes #111
Previously, if a module B imports a module A, then a module C imports B,
the public names in A would also be visible to C (i.e. B would
automatically reexport everything from A). This seems to be a bad
default.

This patch changes the default behaviour so that the only names exported
from a module are those defined in that module. If B imports A and wants
to reexport everything in A, then A should be imported with the "public"
modifier (i.e. "import public A").

Several changes have been made to the prelude, since several prelude
modules were taking advantage of the old broken behaviour.

This may cause lots of things to break. Sorry. The fix is typically just
to import the module you should have imported anyway :).

libs/base/Decidable/Decidable.idr

@@ -1,6 +1,7 @@
 module Decidable.Decidable
 
 import Data.Rel
+import Data.Fun
 
 %access public
 

libs/base/Decidable/Order.idr

@@ -2,6 +2,8 @@ module Decidable.Order
 
 import Decidable.Decidable
 import Decidable.Equality
+import Data.Fun
+import Data.Rel
 
 %access public
 

libs/base/System.idr

@@ -1,7 +1,5 @@
 module System
 
-import Prelude
-
 %include C "unistd.h"
 %default partial
 %access public

libs/effects/Effects.idr

@@ -1,8 +1,7 @@
 module Effects
 
 import Language.Reflection
-import Control.Catchable
-import Effect.Default
+import public Effect.Default
 
 --- Effectful computations are described as algebraic data types that
 --- explain how an effect is interpreted in some underlying context.

libs/prelude/Decidable/Equality.idr

@@ -2,9 +2,12 @@ module Decidable.Equality
 
 import Builtins
 import Prelude.Basics
+import Prelude.Bool
+import Prelude.Classes
 import Prelude.Either
 import Prelude.List
 import Prelude.Vect
+import Prelude.Nat
 import Prelude.Fin
 import Prelude.Maybe
 

libs/prelude/IO.idr

@@ -1,5 +1,6 @@
 %unqualified
 
+import Builtins
 import Prelude.List
 
 %access public

libs/prelude/Prelude.idr

@@ -1,29 +1,32 @@
 module Prelude
 
-import Builtins
-import IO
+import public Builtins
+import public IO
 
-import Prelude.Bool
-import Prelude.Classes
-import Prelude.Cast
-import Prelude.Nat
-import Prelude.Fin
-import Prelude.List
-import Prelude.Maybe
-import Prelude.Monad
-import Prelude.Applicative
-import Prelude.Functor
-import Prelude.Either
-import Prelude.Vect
-import Prelude.Strings
-import Prelude.Chars
-import Prelude.Traversable
-import Prelude.Bits
-import Prelude.Stream
-import Prelude.Uninhabited
-import Prelude.Pairs
+import public Prelude.Algebra
+import public Prelude.Basics
+import public Prelude.Bool
+import public Prelude.Classes
+import public Prelude.Cast
+import public Prelude.Nat
+import public Prelude.Fin
+import public Prelude.List
+import public Prelude.Maybe
+import public Prelude.Monad
+import public Prelude.Applicative
+import public Prelude.Foldable
+import public Prelude.Functor
+import public Prelude.Either
+import public Prelude.Vect
+import public Prelude.Strings
+import public Prelude.Chars
+import public Prelude.Traversable
+import public Prelude.Bits
+import public Prelude.Stream
+import public Prelude.Uninhabited
+import public Prelude.Pairs
 
-import Decidable.Equality
+import public Decidable.Equality
 
 %access public
 %default total

libs/prelude/Prelude/Applicative.idr

@@ -1,7 +1,9 @@
 module Prelude.Applicative
 
 import Builtins
+
 import Prelude.Basics
+import Prelude.Bool
 import Prelude.Classes
 import Prelude.Functor
 

libs/prelude/Prelude/Bits.idr

@@ -1,8 +1,15 @@
 module Prelude.Bits
 
+import Builtins
+
+import Prelude.Basics
+import Prelude.Bool
+import Prelude.Cast
+import Prelude.Classes
+import Prelude.Foldable
+import Prelude.Nat
 import Prelude.Strings
 import Prelude.Vect
-import Prelude.Bool
 
 %access public
 %default total

libs/prelude/Prelude/Either.idr

@@ -2,6 +2,9 @@
 
 import Builtins
 
+import Prelude.Basics
+import Prelude.Bool
+import Prelude.Classes
 import Prelude.Maybe
 import Prelude.List
 

libs/prelude/Prelude/Fin.idr

@@ -1,5 +1,12 @@
 module Prelude.Fin
 
+import Builtins
+
+import Prelude.Basics
+import Prelude.Bool
+import Prelude.Cast
+import Prelude.Classes
+import Prelude.Maybe
 import Prelude.Nat
 import Prelude.Either
 import Prelude.Uninhabited

libs/prelude/Prelude/Foldable.idr

@@ -2,6 +2,7 @@ module Prelude.Foldable
 
 import Builtins
 import Prelude.Bool
+import Prelude.Basics
 import Prelude.Classes
 import Prelude.Algebra
 

libs/prelude/Prelude/List.idr

@@ -4,6 +4,8 @@ import Builtins
 
 import Prelude.Algebra
 import Prelude.Basics
+import Prelude.Bool
+import Prelude.Classes
 import Prelude.Foldable
 import Prelude.Functor
 import Prelude.Maybe

libs/prelude/Prelude/Maybe.idr

@@ -2,7 +2,10 @@ module Prelude.Maybe
 
 import Builtins
 import Prelude.Algebra
+import Prelude.Basics
+import Prelude.Bool
 import Prelude.Cast
+import Prelude.Classes
 import Prelude.Foldable
 
 %access public

libs/prelude/Prelude/Nat.idr

@@ -3,6 +3,7 @@ module Prelude.Nat
 import Builtins
 
 import Prelude.Algebra
+import Prelude.Basics
 import Prelude.Bool
 import Prelude.Cast
 import Prelude.Classes

libs/prelude/Prelude/Stream.idr

@@ -1,6 +1,10 @@
 module Prelude.Stream
 
+import Builtins
+
+import Prelude.Basics
 import Prelude.Functor
+import Prelude.Nat
 import Prelude.Vect
 
 %access public

libs/prelude/Prelude/Strings.idr

@@ -1,11 +1,18 @@
 module Prelude.Strings
 
 import Builtins
-import Prelude.List
+
+import Prelude.Algebra
+import Prelude.Basics
+import Prelude.Bool
 import Prelude.Chars
 import Prelude.Cast
+import Prelude.Classes
 import Prelude.Either
 import Prelude.Foldable
+import Prelude.Functor
+import Prelude.List
+import Prelude.Nat
 
 ||| Appends two strings together.
 |||

libs/prelude/Prelude/Traversable.idr

@@ -1,7 +1,11 @@
 module Prelude.Traversable
 
+import Builtins
+
+import Prelude.Basics
 import Prelude.Applicative
 import Prelude.Foldable
+import Prelude.Functor
 
 traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
 traverse_ f = foldr (($>) . f) (pure ())

libs/prelude/Prelude/Vect.idr

@@ -1,12 +1,16 @@
 module Prelude.Vect
 
+import Builtins
+
+import Prelude.Basics
+import Prelude.Bool
 import Prelude.Fin
 import Prelude.Foldable
 import Prelude.Functor
+import Prelude.Maybe
 import Prelude.List
 import Prelude.Classes
 import Prelude.Nat
-import Prelude.Bool
 import Prelude.Uninhabited
 
 %access public

src/Idris/AbsSyntax.hs

@@ -97,9 +97,10 @@ addAutoImport fp = do i <- getIState
 addHdr :: Codegen -> String -> Idris ()
 addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
 
-addImported :: FilePath -> Idris ()
-addImported f = do i <- getIState
-                   putIState $ i { idris_imported = nub $ f : idris_imported i }
+addImported :: Bool -> FilePath -> Idris ()
+addImported pub f 
+     = do i <- getIState
+          putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }
 
 addLangExt :: LanguageExt -> Idris ()
 addLangExt TypeProviders = do i <- getIState
@@ -382,7 +383,7 @@ addNameIdx' i n
 getHdrs :: Codegen -> Idris [String]
 getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
 
-getImported ::  Idris [FilePath]
+getImported ::  Idris [(FilePath, Bool)]
 getImported = do i <- getIState; return (idris_imported i)
 
 setErrSpan :: FC -> Idris ()
@@ -1576,8 +1577,8 @@ aiFn inpat expat qq ist fc f ds as
                         _ -> True
 
     getAccessibility n
-             = case lookupDefAcc n False (tt_ctxt ist) of
-                    [(n,t)] -> t
+             = case lookupDefAccExact n False (tt_ctxt ist) of
+                    Just (n,t) -> t
                     _ -> Public
 
     insertImpl :: [PArg] -> [PArg] -> [PArg]

src/Idris/AbsSyntaxTree.hs

@@ -187,7 +187,7 @@ data IState = IState {
     idris_libs :: [(Codegen, String)],
     idris_cgflags :: [(Codegen, String)],
     idris_hdrs :: [(Codegen, String)],
-    idris_imported :: [FilePath], -- ^ Imported ibc file names
+    idris_imported :: [(FilePath, Bool)], -- ^ Imported ibc file names, whether public
     proof_list :: [(Name, [String])],
     errSpan :: Maybe FC,
     parserWarnings :: [(FC, Err)],
@@ -259,7 +259,7 @@ data IBCWrite = IBCFix FixDecl
               | IBCMetavar Name
               | IBCSyntax Syntax
               | IBCKeyword String
-              | IBCImport FilePath
+              | IBCImport (Bool, FilePath) -- True = import public
               | IBCImportDir FilePath
               | IBCObj Codegen FilePath
               | IBCLib Codegen String

src/Idris/Chaser.hs

@@ -138,7 +138,7 @@ buildTree built fp = btree [] fp
             (_, modules, _) <- parseImports f file
             -- The chaser should never report warnings from sub-modules
             clearParserWarnings
-            ms <- mapM (btree done) [realName | (realName, alias, fc) <- modules]
+            ms <- mapM (btree done) [realName | (_, realName, alias, fc) <- modules]
             return (concat ms)
            else return [] -- IBC with no source available
 --     (\c -> return []) -- error, can't chase modules here

src/Idris/IBC.hs

@@ -32,12 +32,12 @@ import Codec.Compression.Zlib (compress)
 import Util.Zlib (decompressEither)
 
 ibcVersion :: Word8
-ibcVersion = 87
+ibcVersion = 88
 
 data IBCFile = IBCFile { ver :: Word8,
                          sourcefile :: FilePath,
                          symbols :: [Name],
-                         ibc_imports :: [FilePath],
+                         ibc_imports :: [(Bool, FilePath)],
                          ibc_importdirs :: [FilePath],
                          ibc_implicits :: [(Name, [PArg])],
                          ibc_fixes :: [FixDecl],
@@ -83,13 +83,18 @@ deriving instance Binary IBCFile
 initIBC :: IBCFile
 initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing
 
-loadIBC :: FilePath -> Idris ()
-loadIBC fp = do imps <- getImported
-                when (not (fp `elem` imps)) $
-                  do iLOG $ "Loading ibc " ++ fp
+loadIBC :: Bool -- ^ True = reexport, False = make everything private 
+        -> FilePath -> Idris ()
+loadIBC reexport fp 
+           = do imps <- getImported
+                let redo = case lookup fp imps of
+                                Nothing -> True
+                                Just p -> not p && reexport
+                when redo $
+                  do iLOG $ "Loading ibc " ++ fp ++ " " ++ show reexport
                      ibcf <- runIO $ (bdecode fp :: IO IBCFile)
-                     process ibcf fp
-                     addImported fp
+                     process reexport ibcf fp
+                     addImported reexport fp
 
 bencode :: Binary a => FilePath -> a -> IO ()
 bencode f d = B.writeFile f (compress (encode d))
@@ -250,8 +255,9 @@ ibc i (IBCPostulate n) f = return f { ibc_postulates = n : ibc_postulates f }
 ibc i (IBCTotCheckErr fc err) f = return f { ibc_totcheckfail = (fc, err) : ibc_totcheckfail f }
 ibc i (IBCParsedRegion fc) f = return f { ibc_parsedSpan = Just fc }
 
-process :: IBCFile -> FilePath -> Idris ()
-process i fn
+process :: Bool -> -- ^ Reexporting
+           IBCFile -> FilePath -> Idris ()
+process reexp i fn
    | ver i /= ibcVersion = do iLOG "ibc out of date"
                               ifail "Incorrect ibc version --- please rebuild"
    | otherwise =
@@ -277,9 +283,9 @@ process i fn
                pCGFlags (ibc_cgflags i)
                pDyLibs (ibc_dynamic_libs i)
                pHdrs (ibc_hdrs i)
-               pDefs (symbols i) (ibc_defs i)
+               pDefs reexp (symbols i) (ibc_defs i)
                pPatdefs (ibc_patdefs i)
-               pAccess (ibc_access i)
+               pAccess reexp (ibc_access i)
                pFlags (ibc_flags i)
                pFnInfo (ibc_fninfo i)
                pTotal (ibc_total i)
@@ -317,21 +323,22 @@ pParsedSpan fc = do ist <- getIState
 pImportDirs :: [FilePath] -> Idris ()
 pImportDirs fs = mapM_ addImportDir fs
 
-pImports :: [FilePath] -> Idris ()
+pImports :: [(Bool, FilePath)] -> Idris ()
 pImports fs
-  = do mapM_ (\f -> do i <- getIState
+  = do mapM_ (\(re, f) -> 
+                    do i <- getIState
                        ibcsd <- valIBCSubDir i
                        ids <- allImportDirs
                        fp <- findImport ids ibcsd f
-                       if (f `elem` imported i)
-                        then iLOG $ "Already read " ++ f
-                        else do putIState (i { imported = f : imported i })
+--                        if (f `elem` imported i)
+--                         then iLOG $ "Already read " ++ f
+                       putIState (i { imported = f : imported i })
                        case fp of
                             LIDR fn -> do iLOG $ "Failed at " ++ fn
                                           ifail "Must be an ibc"
                             IDR fn -> do iLOG $ "Failed at " ++ fn
                                          ifail "Must be an ibc"
-                                    IBC fn src -> loadIBC fn)
+                            IBC fn src -> loadIBC re fn)
              fs
 
 pImps :: [(Name, [PArg])] -> Idris ()
@@ -428,8 +435,8 @@ pPatdefs ds
                    putIState (i { idris_patdefs = addDef n d (idris_patdefs i) }))
            ds
 
-pDefs :: [Name] -> [(Name, Def)] -> Idris ()
-pDefs syms ds 
+pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()
+pDefs reexp syms ds 
    = mapM_ (\ (n, d) ->
                do let d' = updateDef d
                   case d' of
@@ -438,7 +445,10 @@ pDefs syms ds
                                solveDeferred n 
                   i <- getIState
 --                   logLvl 1 $ "Added " ++ show (n, d')
-                  putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds
+                  putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })
+                  if (not reexp) then do iLOG $ "Not exporting " ++ show n
+                                         setAccessibility n Hidden
+                                 else iLOG $ "Exporting " ++ show n) ds
   where
     updateDef (CaseOp c t args o s cd)
       = CaseOp c t args (map updateOrig o) s (updateCD cd)
@@ -462,9 +472,13 @@ pDefs syms ds
 pDocs :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))] -> Idris ()
 pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds
 
-pAccess :: [(Name, Accessibility)] -> Idris ()
-pAccess ds = mapM_ (\ (n, a) ->
-                      do i <- getIState
+pAccess :: Bool -> -- ^ Reexporting?
+           [(Name, Accessibility)] -> Idris ()
+pAccess reexp ds 
+        = mapM_ (\ (n, a_in) -> 
+                      do let a = if reexp then a_in else Hidden
+                         logLvl 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a
+                         i <- getIState
                          putIState (i { tt_ctxt = setAccess n a (tt_ctxt i) }))
                    ds
 

src/Idris/Parser.hs

@@ -109,13 +109,14 @@ moduleHeader =     try (do noDocCommentHere "Modules cannot have documentation c
   Import ::= 'import' Identifier_t ';'?;
 @
  -}
-import_ :: IdrisParser (String, Maybe String, FC)
+import_ :: IdrisParser (Bool, String, Maybe String, FC)
 import_ = do fc <- getFC
              reserved "import"
+             reexport <- option False (do reserved "public"; return True)
              id <- identifier
              newName <- optional (reserved "as" *> identifier)
              option ';' (lchar ';')
-             return (toPath id, toPath <$> newName, fc)
+             return (reexport, toPath id, toPath <$> newName, fc)
           <?> "import statement"
   where toPath = foldl1' (</>) . Spl.splitOn "."
 
@@ -1132,14 +1133,14 @@ parseTactic :: IState -> String -> Result PTactic
 parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
 
 -- | Parse module header and imports
-parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)
+parseImports :: FilePath -> String -> Idris ([String], [(Bool, String, Maybe String, FC)], Maybe Delta)
 parseImports fname input
     = do i <- getIState
          case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
               Failure err    -> fail (show err)
               Success (x, i) -> do putIState i
                                    return x
-  where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)
+  where imports :: IdrisParser (([String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState)
         imports = do whiteSpace
                      mname <- moduleHeader
                      ps    <- many import_
@@ -1219,7 +1220,7 @@ loadModule' f
                     IDR fn  -> loadSource False fn Nothing
                     LIDR fn -> loadSource True  fn Nothing
                     IBC fn src ->
-                      idrisCatch (loadIBC fn)
+                      idrisCatch (loadIBC True fn)
                                  (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
                                            case src of
                                              IDR sfn -> loadSource False sfn Nothing
@@ -1229,18 +1230,18 @@ loadModule' f
 
 
 {- | Load idris code from file -}
-loadFromIFile :: IFileType -> Maybe Int -> Idris ()
-loadFromIFile i@(IBC fn src) maxline
+loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()
+loadFromIFile reexp i@(IBC fn src) maxline
    = do iLOG $ "Skipping " ++ getSrcFile i
-        idrisCatch (loadIBC fn)
+        idrisCatch (loadIBC reexp fn)
                 (\err -> ierror $ LoadingFailed fn err)
   where
     getSrcFile (IDR fn) = fn
     getSrcFile (LIDR fn) = fn
     getSrcFile (IBC f src) = getSrcFile src
 
-loadFromIFile (IDR fn) maxline = loadSource' False fn maxline
-loadFromIFile (LIDR fn) maxline = loadSource' True fn maxline
+loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline
+loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline
 
 {-| Load idris source code and show error if something wrong happens -}
 loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
@@ -1262,22 +1263,23 @@ loadSource lidr f toline
                   file <- if lidr then tclift $ unlit f file_in else return file_in
                   (mname, imports_in, pos) <- parseImports f file
                   ai <- getAutoImports
-                  let imports = map (\n -> (n, Just n, emptyFC)) ai ++ imports_in
+                  let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in
                   ids <- allImportDirs
                   ibcsd <- valIBCSubDir i
-                  mapM_ (\f -> do fp <- findImport ids ibcsd f
+                  mapM_ (\(re, f) -> 
+                               do fp <- findImport ids ibcsd f
                                   case fp of
                                       LIDR fn -> ifail $ "No ibc for " ++ f
                                       IDR fn -> ifail $ "No ibc for " ++ f
-                                      IBC fn src -> loadIBC fn)
-                        [fn | (fn, _, _) <- imports]
+                                      IBC fn src -> loadIBC True fn)
+                        [(re, fn) | (re, fn, _, _) <- imports]
                   reportParserWarnings
 
                   -- process and check module aliases
                   let modAliases = M.fromList
-                        [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]
+                        [(prep alias, prep realName) | (reexport, realName, Just alias, fc) <- imports]
                       prep = map T.pack . reverse . Spl.splitOn "/"
-                      aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]
+                      aliasNames = [(alias, fc) | (_, _, Just alias, fc) <- imports]
                       histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
                   case map head . filter ((/= 1) . length) $ histogram of
                     []       -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
@@ -1289,7 +1291,7 @@ loadSource lidr f toline
                   -- record package info in .ibc
                   imps <- allImportDirs
                   mapM_ addIBC (map IBCImportDir imps)
-                  mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
+                  mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
                   let syntax = defaultSyntax{ syn_namespace = reverse mname,
                                               maxline = toline }
                   ds' <- parseProg syntax f file pos

src/Idris/REPL.hs

@@ -1075,7 +1075,7 @@ process fn Execute
                            runIO $ hClose tmph
                            t <- codegen
                            ir <- compile t tmpn m
-                           runIO $ generate t (head (idris_imported ist)) ir
+                           runIO $ generate t (fst (head (idris_imported ist))) ir
                            case idris_outputmode ist of
                              RawOutput h -> do runIO $ rawSystem tmpn []
                                                return ()
@@ -1091,7 +1091,7 @@ process fn (Compile codegen f)
                                    [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
                        ir <- compile codegen f m
                        i <- getIState
-                       runIO $ generate codegen (head (idris_imported i)) ir
+                       runIO $ generate codegen (fst (head (idris_imported i))) ir
   where fc = fileFC "main"
 process fn (LogLvl i) = setLogLevel i
 -- Elaborate as if LHS of a pattern (debug command)
@@ -1403,7 +1403,7 @@ loadInputs inputs toline -- furthest line to read in input source files
                                                           then Just l
                                                           else Nothing
                                             _ -> Nothing
-                      loadFromIFile f maxline
+                      loadFromIFile True f maxline
                       inew <- getIState
                       -- FIXME: Save these in IBC to avoid this hack! Need to
                       -- preserve it all from source inputs

test/effects001/test021.idr

@@ -1,5 +1,6 @@
 module Main
 
+import Effects
 import Effect.File
 import Effect.State
 import Effect.StdIO

test/effects001/test021a.idr

@@ -1,5 +1,6 @@
 module Main
 
+import Effects
 import Effect.State
 import Effect.Exception
 import Effect.Random

test/io003/test018a.idr

@@ -1,5 +1,6 @@
 module Main
 
+import System
 import System.Concurrency.Process
 
 ping : ProcID String -> ProcID String -> Process String ()