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 :).
idris-lang · Dec 13, 2014 · 7b5f4aa · 7b5f4aa
1 parent b9e5895
commit 7b5f4aa
Show file tree

Hide file tree

Showing 29 changed files with 162 additions and 90 deletions.
diff --git a/libs/base/Decidable/Decidable.idr b/libs/base/Decidable/Decidable.idr
@@ -1,6 +1,7 @@
 module Decidable.Decidable
 
 import Data.Rel
+import Data.Fun
 
 %access public
 

diff --git a/libs/base/Decidable/Order.idr b/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
 

diff --git a/libs/base/System.idr b/libs/base/System.idr
@@ -1,7 +1,5 @@
 module System
 
-import Prelude
-
 %include C "unistd.h"
 %default partial
 %access public

diff --git a/libs/effects/Effects.idr b/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.

diff --git a/libs/prelude/Decidable/Equality.idr b/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
 

diff --git a/libs/prelude/IO.idr b/libs/prelude/IO.idr
@@ -1,5 +1,6 @@
 %unqualified
 
+import Builtins
 import Prelude.List
 
 %access public

diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr
@@ -1,29 +1,32 @@
 module Prelude
 
-import Builtins
-import 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 Decidable.Equality
+import public Builtins
+import public IO
+
+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 public Decidable.Equality
 
 %access public
 %default total

diff --git a/libs/prelude/Prelude/Applicative.idr b/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
 

diff --git a/libs/prelude/Prelude/Bits.idr b/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

diff --git a/libs/prelude/Prelude/Either.idr b/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
 

diff --git a/libs/prelude/Prelude/Fin.idr b/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

diff --git a/libs/prelude/Prelude/Foldable.idr b/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
 

diff --git a/libs/prelude/Prelude/List.idr b/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

diff --git a/libs/prelude/Prelude/Maybe.idr b/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

diff --git a/libs/prelude/Prelude/Nat.idr b/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

diff --git a/libs/prelude/Prelude/Stream.idr b/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

diff --git a/libs/prelude/Prelude/Strings.idr b/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.
 |||

diff --git a/libs/prelude/Prelude/Traversable.idr b/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 ())

diff --git a/libs/prelude/Prelude/Vect.idr b/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

diff --git a/src/Idris/AbsSyntax.hs b/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]

diff --git a/src/Idris/AbsSyntaxTree.hs b/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

diff --git a/src/Idris/Chaser.hs b/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
diff --git a/src/Idris/Core/Evaluate.hs b/src/Idris/Core/Evaluate.hs
@@ -981,7 +981,7 @@ isTCDict n ctxt
 
 lookupP :: Name -> Context -> [Term]
 lookupP n ctxt
-   = do def <-  lookupCtxt n (definitions ctxt)
+   = do def <- lookupCtxt n (definitions ctxt)
         p <- case def of
           (Function ty tm, a, _, _) -> return (P Ref n ty, a)
           (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)