7b5f4aa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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 :).

commit7b5f4aa392985c6a7d7fdd5268cebe4adee954b8 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 13 Dec 2014, 17:40 (12 years ago) parentb9e5895

29 files changed+162−90

compare with master

unifiedsplit

libs/base/Decidable/Decidable.idr+1

@@ -1,6 +1,7 @@

11module Decidable.Decidable

33import Data.Rel

4+import Data.Fun

56%access public

libs/base/Decidable/Order.idr+2

@@ -2,6 +2,8 @@ module Decidable.Order

33import Decidable.Decidable

44import Decidable.Equality

5+import Data.Fun

6+import Data.Rel

68%access public

libs/base/System.idr−2

@@ -1,7 +1,5 @@

11module System

3−import Prelude

4−

53%include C "unistd.h"

64%default partial

75%access public

libs/effects/Effects.idr+1−2

@@ -1,8 +1,7 @@

11module Effects

33import Language.Reflection

4−import Control.Catchable

5−import Effect.Default

4+import public Effect.Default

76--- Effectful computations are described as algebraic data types that

87--- explain how an effect is interpreted in some underlying context.

libs/prelude/Decidable/Equality.idr+3

@@ -2,9 +2,12 @@ module Decidable.Equality

33import Builtins

44import Prelude.Basics

5+import Prelude.Bool

6+import Prelude.Classes

57import Prelude.Either

68import Prelude.List

79import Prelude.Vect

10+import Prelude.Nat

811import Prelude.Fin

912import Prelude.Maybe

1013

libs/prelude/IO.idr+1

@@ -1,5 +1,6 @@

11%unqualified

3+import Builtins

34import Prelude.List

56%access public

libs/prelude/Prelude.idr+27−24

@@ -1,29 +1,32 @@

11module Prelude

3−import Builtins

4−import IO

5−

6−import Prelude.Bool

7−import Prelude.Classes

8−import Prelude.Cast

9−import Prelude.Nat

10−import Prelude.Fin

11−import Prelude.List

12−import Prelude.Maybe

13−import Prelude.Monad

14−import Prelude.Applicative

15−import Prelude.Functor

16−import Prelude.Either

17−import Prelude.Vect

18−import Prelude.Strings

19−import Prelude.Chars

20−import Prelude.Traversable

21−import Prelude.Bits

22−import Prelude.Stream

23−import Prelude.Uninhabited

24−import Prelude.Pairs

25−

26−import Decidable.Equality

3+import public Builtins

4+import public IO

6+import public Prelude.Algebra

7+import public Prelude.Basics

8+import public Prelude.Bool

9+import public Prelude.Classes

10+import public Prelude.Cast

11+import public Prelude.Nat

12+import public Prelude.Fin

13+import public Prelude.List

14+import public Prelude.Maybe

15+import public Prelude.Monad

16+import public Prelude.Applicative

17+import public Prelude.Foldable

18+import public Prelude.Functor

19+import public Prelude.Either

20+import public Prelude.Vect

21+import public Prelude.Strings

22+import public Prelude.Chars

23+import public Prelude.Traversable

24+import public Prelude.Bits

25+import public Prelude.Stream

26+import public Prelude.Uninhabited

27+import public Prelude.Pairs

28+

29+import public Decidable.Equality

2730

2831%access public

2932%default total

libs/prelude/Prelude/Applicative.idr+2

@@ -1,7 +1,9 @@

11module Prelude.Applicative

33import Builtins

45import Prelude.Basics

6+import Prelude.Bool

57import Prelude.Classes

68import Prelude.Functor

libs/prelude/Prelude/Bits.idr+8−1

@@ -1,8 +1,15 @@

11module Prelude.Bits

3+import Builtins

5+import Prelude.Basics

6+import Prelude.Bool

7+import Prelude.Cast

8+import Prelude.Classes

9+import Prelude.Foldable

10+import Prelude.Nat

311import Prelude.Strings

412import Prelude.Vect

5−import Prelude.Bool

613

714%access public

815%default total

libs/prelude/Prelude/Either.idr+3

@@ -2,6 +2,9 @@

33import Builtins

5+import Prelude.Basics

6+import Prelude.Bool

7+import Prelude.Classes

58import Prelude.Maybe

69import Prelude.List

710

libs/prelude/Prelude/Fin.idr+7

@@ -1,5 +1,12 @@

11module Prelude.Fin

3+import Builtins

5+import Prelude.Basics

6+import Prelude.Bool

7+import Prelude.Cast

8+import Prelude.Classes

9+import Prelude.Maybe

310import Prelude.Nat

411import Prelude.Either

512import Prelude.Uninhabited

libs/prelude/Prelude/Foldable.idr+1

@@ -2,6 +2,7 @@ module Prelude.Foldable

33import Builtins

44import Prelude.Bool

5+import Prelude.Basics

56import Prelude.Classes

67import Prelude.Algebra

libs/prelude/Prelude/List.idr+2

@@ -4,6 +4,8 @@ import Builtins

55import Prelude.Algebra

66import Prelude.Basics

7+import Prelude.Bool

8+import Prelude.Classes

79import Prelude.Foldable

810import Prelude.Functor

911import Prelude.Maybe

libs/prelude/Prelude/Maybe.idr+3

@@ -2,7 +2,10 @@ module Prelude.Maybe

33import Builtins

44import Prelude.Algebra

5+import Prelude.Basics

6+import Prelude.Bool

57import Prelude.Cast

8+import Prelude.Classes

69import Prelude.Foldable

710

811%access public

libs/prelude/Prelude/Nat.idr+1

@@ -3,6 +3,7 @@ module Prelude.Nat

33import Builtins

55import Prelude.Algebra

6+import Prelude.Basics

67import Prelude.Bool

78import Prelude.Cast

89import Prelude.Classes

libs/prelude/Prelude/Stream.idr+4

@@ -1,6 +1,10 @@

11module Prelude.Stream

3+import Builtins

5+import Prelude.Basics

36import Prelude.Functor

7+import Prelude.Nat

48import Prelude.Vect

610%access public

libs/prelude/Prelude/Strings.idr+8−1

@@ -1,11 +1,18 @@

11module Prelude.Strings

33import Builtins

4−import Prelude.List

5+import Prelude.Algebra

6+import Prelude.Basics

7+import Prelude.Bool

58import Prelude.Chars

69import Prelude.Cast

10+import Prelude.Classes

711import Prelude.Either

812import Prelude.Foldable

13+import Prelude.Functor

14+import Prelude.List

15+import Prelude.Nat

916

1017||| Appends two strings together.

1118|||

libs/prelude/Prelude/Traversable.idr+4

@@ -1,7 +1,11 @@

11module Prelude.Traversable

3+import Builtins

5+import Prelude.Basics

36import Prelude.Applicative

47import Prelude.Foldable

8+import Prelude.Functor

610traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()

711traverse_ f = foldr (($>) . f) (pure ())

libs/prelude/Prelude/Vect.idr+5−1

@@ -1,12 +1,16 @@

11module Prelude.Vect

3+import Builtins

5+import Prelude.Basics

6+import Prelude.Bool

37import Prelude.Fin

48import Prelude.Foldable

59import Prelude.Functor

10+import Prelude.Maybe

611import Prelude.List

712import Prelude.Classes

813import Prelude.Nat

9−import Prelude.Bool

1014import Prelude.Uninhabited

1115

1216%access public

src/Idris/AbsSyntax.hs+7−6

@@ -97,9 +97,10 @@ addAutoImport fp = do i <- getIState

9797addHdr :: Codegen -> String -> Idris ()

9898addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }

9999

100−addImported :: FilePath -> Idris ()

101−addImported f = do i <- getIState

102− putIState $ i { idris_imported = nub $ f : idris_imported i }

100+addImported :: Bool -> FilePath -> Idris ()

101+addImported pub f

102+ = do i <- getIState

103+ putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }

103104

104105addLangExt :: LanguageExt -> Idris ()

105106addLangExt TypeProviders = do i <- getIState

@@ -382,7 +383,7 @@ addNameIdx' i n

382383getHdrs :: Codegen -> Idris [String]

383384getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)

384385

385−getImported :: Idris [FilePath]

386+getImported :: Idris [(FilePath, Bool)]

386387getImported = do i <- getIState; return (idris_imported i)

387388

388389setErrSpan :: FC -> Idris ()

@@ -1576,8 +1577,8 @@ aiFn inpat expat qq ist fc f ds as

15761577 _ -> True

15771578

15781579 getAccessibility n

1579− = case lookupDefAcc n False (tt_ctxt ist) of

1580− [(n,t)] -> t

1580+ = case lookupDefAccExact n False (tt_ctxt ist) of

1581+ Just (n,t) -> t

15811582 _ -> Public

15821583

15831584 insertImpl :: [PArg] -> [PArg] -> [PArg]

src/Idris/AbsSyntaxTree.hs+2−2

@@ -187,7 +187,7 @@ data IState = IState {

187187 idris_libs :: [(Codegen, String)],

188188 idris_cgflags :: [(Codegen, String)],

189189 idris_hdrs :: [(Codegen, String)],

190− idris_imported :: [FilePath], -- ^ Imported ibc file names

190+ idris_imported :: [(FilePath, Bool)], -- ^ Imported ibc file names, whether public

191191 proof_list :: [(Name, [String])],

192192 errSpan :: Maybe FC,

193193 parserWarnings :: [(FC, Err)],

@@ -259,7 +259,7 @@ data IBCWrite = IBCFix FixDecl

259259 | IBCMetavar Name

260260 | IBCSyntax Syntax

261261 | IBCKeyword String

262− | IBCImport FilePath

262+ | IBCImport (Bool, FilePath) -- True = import public

263263 | IBCImportDir FilePath

264264 | IBCObj Codegen FilePath

265265 | IBCLib Codegen String

src/Idris/Chaser.hs+1−1

@@ -138,7 +138,7 @@ buildTree built fp = btree [] fp

138138 (_, modules, _) <- parseImports f file

139139 -- The chaser should never report warnings from sub-modules

140140 clearParserWarnings

141− ms <- mapM (btree done) [realName | (realName, alias, fc) <- modules]

141+ ms <- mapM (btree done) [realName | (_, realName, alias, fc) <- modules]

142142 return (concat ms)

143143 else return [] -- IBC with no source available

144144-- (\c -> return []) -- error, can't chase modules here

src/Idris/Core/Evaluate.hs+1−1

@@ -981,7 +981,7 @@ isTCDict n ctxt

981981

982982lookupP :: Name -> Context -> [Term]

983983lookupP n ctxt

984− = do def <- lookupCtxt n (definitions ctxt)

984+ = do def <- lookupCtxt n (definitions ctxt)

985985 p <- case def of

986986 (Function ty tm, a, _, _) -> return (P Ref n ty, a)

987987 (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)

src/Idris/IBC.hs+43−29

@@ -32,12 +32,12 @@ import Codec.Compression.Zlib (compress)

3232import Util.Zlib (decompressEither)

3333

3434ibcVersion :: Word8

35−ibcVersion = 87

35+ibcVersion = 88

3636

3737data IBCFile = IBCFile { ver :: Word8,

3838 sourcefile :: FilePath,

3939 symbols :: [Name],

40− ibc_imports :: [FilePath],

40+ ibc_imports :: [(Bool, FilePath)],

4141 ibc_importdirs :: [FilePath],

4242 ibc_implicits :: [(Name, [PArg])],

4343 ibc_fixes :: [FixDecl],

@@ -83,13 +83,18 @@ deriving instance Binary IBCFile

8383initIBC :: IBCFile

8484initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing

8585

86−loadIBC :: FilePath -> Idris ()

87−loadIBC fp = do imps <- getImported

88− when (not (fp `elem` imps)) $

89− do iLOG $ "Loading ibc " ++ fp

86+loadIBC :: Bool -- ^ True = reexport, False = make everything private

87+ -> FilePath -> Idris ()

88+loadIBC reexport fp

89+ = do imps <- getImported

90+ let redo = case lookup fp imps of

91+ Nothing -> True

92+ Just p -> not p && reexport

93+ when redo $

94+ do iLOG $ "Loading ibc " ++ fp ++ " " ++ show reexport

9095 ibcf <- runIO $ (bdecode fp :: IO IBCFile)

91− process ibcf fp

92− addImported fp

96+ process reexport ibcf fp

97+ addImported reexport fp

9398

9499bencode :: Binary a => FilePath -> a -> IO ()

95100bencode 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 }

250255ibc i (IBCTotCheckErr fc err) f = return f { ibc_totcheckfail = (fc, err) : ibc_totcheckfail f }

251256ibc i (IBCParsedRegion fc) f = return f { ibc_parsedSpan = Just fc }

252257

253−process :: IBCFile -> FilePath -> Idris ()

254−process i fn

258+process :: Bool -> -- ^ Reexporting

259+ IBCFile -> FilePath -> Idris ()

260+process reexp i fn

255261 | ver i /= ibcVersion = do iLOG "ibc out of date"

256262 ifail "Incorrect ibc version --- please rebuild"

257263 | otherwise =

@@ -277,9 +283,9 @@ process i fn

277283 pCGFlags (ibc_cgflags i)

278284 pDyLibs (ibc_dynamic_libs i)

279285 pHdrs (ibc_hdrs i)

280− pDefs (symbols i) (ibc_defs i)

286+ pDefs reexp (symbols i) (ibc_defs i)

281287 pPatdefs (ibc_patdefs i)

282− pAccess (ibc_access i)

288+ pAccess reexp (ibc_access i)

283289 pFlags (ibc_flags i)

284290 pFnInfo (ibc_fninfo i)

285291 pTotal (ibc_total i)

@@ -317,21 +323,22 @@ pParsedSpan fc = do ist <- getIState

317323pImportDirs :: [FilePath] -> Idris ()

318324pImportDirs fs = mapM_ addImportDir fs

319325

320−pImports :: [FilePath] -> Idris ()

326+pImports :: [(Bool, FilePath)] -> Idris ()

321327pImports fs

322− = do mapM_ (\f -> do i <- getIState

328+ = do mapM_ (\(re, f) ->

329+ do i <- getIState

323330 ibcsd <- valIBCSubDir i

324331 ids <- allImportDirs

325332 fp <- findImport ids ibcsd f

326− if (f `elem` imported i)

327− then iLOG $ "Already read " ++ f

328− else do putIState (i { imported = f : imported i })

329− case fp of

330− LIDR fn -> do iLOG $ "Failed at " ++ fn

331− ifail "Must be an ibc"

332− IDR fn -> do iLOG $ "Failed at " ++ fn

333− ifail "Must be an ibc"

334− IBC fn src -> loadIBC fn)

333+-- if (f `elem` imported i)

334+-- then iLOG $ "Already read " ++ f

335+ putIState (i { imported = f : imported i })

336+ case fp of

337+ LIDR fn -> do iLOG $ "Failed at " ++ fn

338+ ifail "Must be an ibc"

339+ IDR fn -> do iLOG $ "Failed at " ++ fn

340+ ifail "Must be an ibc"

341+ IBC fn src -> loadIBC re fn)

335342 fs

336343

337344pImps :: [(Name, [PArg])] -> Idris ()

@@ -428,8 +435,8 @@ pPatdefs ds

428435 putIState (i { idris_patdefs = addDef n d (idris_patdefs i) }))

429436 ds

430437

431−pDefs :: [Name] -> [(Name, Def)] -> Idris ()

432−pDefs syms ds

438+pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()

439+pDefs reexp syms ds

433440 = mapM_ (\ (n, d) ->

434441 do let d' = updateDef d

435442 case d' of

@@ -438,7 +445,10 @@ pDefs syms ds

438445 solveDeferred n

439446 i <- getIState

440447-- logLvl 1 $ "Added " ++ show (n, d')

441− putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds

448+ putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

449+ if (not reexp) then do iLOG $ "Not exporting " ++ show n

450+ setAccessibility n Hidden

451+ else iLOG $ "Exporting " ++ show n) ds

442452 where

443453 updateDef (CaseOp c t args o s cd)

444454 = CaseOp c t args (map updateOrig o) s (updateCD cd)

@@ -462,9 +472,13 @@ pDefs syms ds

462472pDocs :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))] -> Idris ()

463473pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds

464474

465−pAccess :: [(Name, Accessibility)] -> Idris ()

466−pAccess ds = mapM_ (\ (n, a) ->

467− do i <- getIState

475+pAccess :: Bool -> -- ^ Reexporting?

476+ [(Name, Accessibility)] -> Idris ()

477+pAccess reexp ds

478+ = mapM_ (\ (n, a_in) ->

479+ do let a = if reexp then a_in else Hidden

480+ logLvl 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

481+ i <- getIState

468482 putIState (i { tt_ctxt = setAccess n a (tt_ctxt i) }))

469483 ds

470484

src/Idris/Parser.hs+19−17

@@ -109,13 +109,14 @@ moduleHeader = try (do noDocCommentHere "Modules cannot have documentation c

109109 Import ::= 'import' Identifier_t ';'?;

110110@

111111 -}

112−import_ :: IdrisParser (String, Maybe String, FC)

112+import_ :: IdrisParser (Bool, String, Maybe String, FC)

113113import_ = do fc <- getFC

114114 reserved "import"

115+ reexport <- option False (do reserved "public"; return True)

115116 id <- identifier

116117 newName <- optional (reserved "as" *> identifier)

117118 option ';' (lchar ';')

118− return (toPath id, toPath <$> newName, fc)

119+ return (reexport, toPath id, toPath <$> newName, fc)

119120 <?> "import statement"

120121 where toPath = foldl1' (</>) . Spl.splitOn "."

121122

@@ -1132,14 +1133,14 @@ parseTactic :: IState -> String -> Result PTactic

11321133parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

11331134

11341135-- | Parse module header and imports

1135−parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)

1136+parseImports :: FilePath -> String -> Idris ([String], [(Bool, String, Maybe String, FC)], Maybe Delta)

11361137parseImports fname input

11371138 = do i <- getIState

11381139 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of

11391140 Failure err -> fail (show err)

11401141 Success (x, i) -> do putIState i

11411142 return x

1142− where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)

1143+ where imports :: IdrisParser (([String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState)

11431144 imports = do whiteSpace

11441145 mname <- moduleHeader

11451146 ps <- many import_

@@ -1219,7 +1220,7 @@ loadModule' f

12191220 IDR fn -> loadSource False fn Nothing

12201221 LIDR fn -> loadSource True fn Nothing

12211222 IBC fn src ->

1222− idrisCatch (loadIBC fn)

1223+ idrisCatch (loadIBC True fn)

12231224 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c

12241225 case src of

12251226 IDR sfn -> loadSource False sfn Nothing

@@ -1229,18 +1230,18 @@ loadModule' f

12291230

12301231

12311232{- | Load idris code from file -}

1232−loadFromIFile :: IFileType -> Maybe Int -> Idris ()

1233−loadFromIFile i@(IBC fn src) maxline

1233+loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()

1234+loadFromIFile reexp i@(IBC fn src) maxline

12341235 = do iLOG $ "Skipping " ++ getSrcFile i

1235− idrisCatch (loadIBC fn)

1236+ idrisCatch (loadIBC reexp fn)

12361237 (\err -> ierror $ LoadingFailed fn err)

12371238 where

12381239 getSrcFile (IDR fn) = fn

12391240 getSrcFile (LIDR fn) = fn

12401241 getSrcFile (IBC f src) = getSrcFile src

12411242

1242−loadFromIFile (IDR fn) maxline = loadSource' False fn maxline

1243−loadFromIFile (LIDR fn) maxline = loadSource' True fn maxline

1243+loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline

1244+loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline

12441245

12451246{-| Load idris source code and show error if something wrong happens -}

12461247loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()

@@ -1262,22 +1263,23 @@ loadSource lidr f toline

12621263 file <- if lidr then tclift $ unlit f file_in else return file_in

12631264 (mname, imports_in, pos) <- parseImports f file

12641265 ai <- getAutoImports

1265− let imports = map (\n -> (n, Just n, emptyFC)) ai ++ imports_in

1266+ let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in

12661267 ids <- allImportDirs

12671268 ibcsd <- valIBCSubDir i

1268− mapM_ (\f -> do fp <- findImport ids ibcsd f

1269+ mapM_ (\(re, f) ->

1270+ do fp <- findImport ids ibcsd f

12691271 case fp of

12701272 LIDR fn -> ifail $ "No ibc for " ++ f

12711273 IDR fn -> ifail $ "No ibc for " ++ f

1272− IBC fn src -> loadIBC fn)

1273− [fn | (fn, _, _) <- imports]

1274+ IBC fn src -> loadIBC True fn)

1275+ [(re, fn) | (re, fn, _, _) <- imports]

12741276 reportParserWarnings

12751277

12761278 -- process and check module aliases

12771279 let modAliases = M.fromList

1278− [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]

1280+ [(prep alias, prep realName) | (reexport, realName, Just alias, fc) <- imports]

12791281 prep = map T.pack . reverse . Spl.splitOn "/"

1280− aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]

1282+ aliasNames = [(alias, fc) | (_, _, Just alias, fc) <- imports]

12811283 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames

12821284 case map head . filter ((/= 1) . length) $ histogram of

12831285 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)

@@ -1289,7 +1291,7 @@ loadSource lidr f toline

12891291 -- record package info in .ibc

12901292 imps <- allImportDirs

12911293 mapM_ addIBC (map IBCImportDir imps)

1292− mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]

1294+ mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]

12931295 let syntax = defaultSyntax{ syn_namespace = reverse mname,

12941296 maxline = toline }

12951297 ds' <- parseProg syntax f file pos

src/Idris/REPL.hs+3−3

@@ -1075,7 +1075,7 @@ process fn Execute

10751075 runIO $ hClose tmph

10761076 t <- codegen

10771077 ir <- compile t tmpn m

1078− runIO $ generate t (head (idris_imported ist)) ir

1078+ runIO $ generate t (fst (head (idris_imported ist))) ir

10791079 case idris_outputmode ist of

10801080 RawOutput h -> do runIO $ rawSystem tmpn []

10811081 return ()

@@ -1091,7 +1091,7 @@ process fn (Compile codegen f)

10911091 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

10921092 ir <- compile codegen f m

10931093 i <- getIState

1094− runIO $ generate codegen (head (idris_imported i)) ir

1094+ runIO $ generate codegen (fst (head (idris_imported i))) ir

10951095 where fc = fileFC "main"

10961096process fn (LogLvl i) = setLogLevel i

10971097-- Elaborate as if LHS of a pattern (debug command)

@@ -1403,7 +1403,7 @@ loadInputs inputs toline -- furthest line to read in input source files

14031403 then Just l

14041404 else Nothing

14051405 _ -> Nothing

1406− loadFromIFile f maxline

1406+ loadFromIFile True f maxline

14071407 inew <- getIState

14081408 -- FIXME: Save these in IBC to avoid this hack! Need to

14091409 -- preserve it all from source inputs

test/effects001/test021.idr+1

@@ -1,5 +1,6 @@

11module Main

3+import Effects

34import Effect.File

45import Effect.State

56import Effect.StdIO

test/effects001/test021a.idr+1

@@ -1,5 +1,6 @@

11module Main

3+import Effects

34import Effect.State

45import Effect.Exception

56import Effect.Random

test/io003/test018a.idr+1

@@ -1,5 +1,6 @@

11module Main

3+import System

34import System.Concurrency.Process

56ping : ProcID String -> ProcID String -> Process String ()