diff --git a/libs/base/Decidable/Decidable.idr b/libs/base/Decidable/Decidable.idr index e820d60e5..4a93c2366 100644 --- 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 index 009bd3d69..bde83d1be 100644 --- 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 index 331d5bc4c..edcacbfad 100644 --- 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 index 03bae7e5b..68b2c5e5f 100644 --- 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 index f1211497f..d549d2a34 100644 --- 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 index ed72b5321..f8aa2429f 100644 --- 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 index a334043af..c8986ee56 100644 --- a/libs/prelude/Prelude.idr +++ b/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 diff --git a/libs/prelude/Prelude/Applicative.idr b/libs/prelude/Prelude/Applicative.idr index 6b713b918..d32327f77 100644 --- 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 index 9d42742ad..22a960d20 100644 --- 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 index 0c9c80d19..6b8e0d8ed 100644 --- 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 index fe96ff22e..96f4fd90d 100644 --- 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 index e33ccb2af..13bb0a3fe 100644 --- 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 index 5f6eda93e..fbedd6c76 100644 --- 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 index e285aeb4f..ae53d22f9 100644 --- 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 index aa53486fc..4682a5cd5 100644 --- 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 index 49c824a00..a97fc7ca4 100644 --- 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 index 380848743..7c241b400 100644 --- 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 index c0cfc6197..5c495c647 100644 --- 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 index 016927934..554050067 100644 --- 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 index 4ef0637d8..498c3b415 100644 --- 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 index f5461bbc3..9f434b1c0 100644 --- 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 index 9158a4832..5b622f3b3 100644 --- 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 index 996efdfc3..80451466b 100644 --- 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) diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs index af390aaf2..ef00dc2e7 100644 --- a/src/Idris/IBC.hs +++ b/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 }) - 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) +-- 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 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 diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs index a575377e1..3507068d3 100644 --- a/src/Idris/Parser.hs +++ b/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 diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs index 7f50a4fa2..6731a2cd4 100644 --- a/src/Idris/REPL.hs +++ b/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 diff --git a/test/effects001/test021.idr b/test/effects001/test021.idr index a5bc4b51e..8fca33cd3 100644 --- a/test/effects001/test021.idr +++ b/test/effects001/test021.idr @@ -1,5 +1,6 @@ module Main +import Effects import Effect.File import Effect.State import Effect.StdIO diff --git a/test/effects001/test021a.idr b/test/effects001/test021a.idr index b623f9431..1a87491af 100644 --- a/test/effects001/test021a.idr +++ b/test/effects001/test021a.idr @@ -1,5 +1,6 @@ module Main +import Effects import Effect.State import Effect.Exception import Effect.Random diff --git a/test/io003/test018a.idr b/test/io003/test018a.idr index 6323ac521..b73c75d27 100644 --- a/test/io003/test018a.idr +++ b/test/io003/test018a.idr @@ -1,5 +1,6 @@ module Main +import System import System.Concurrency.Process ping : ProcID String -> ProcID String -> Process String ()