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

libs/base/Decidable/Decidable.idr+1

compare with master

unifiedsplit

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

1module Decidable.Decidable

2

3import Data.Rel

4+import Data.Fun

4

5

5%access public

6%access public

6

7

libs/base/Decidable/Order.idr+2

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

2

3import Decidable.Decidable

4import Decidable.Equality

5+import Data.Fun

6+import Data.Rel

5

7

6%access public

8%access public

7

9

libs/base/System.idr−2

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

1module System

2

3−import Prelude

4−

5%include C "unistd.h"

3%include C "unistd.h"

6%default partial

4%default partial

7%access public

5%access public

libs/effects/Effects.idr+1−2

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

1module Effects

2

3import Language.Reflection

4−import Control.Catchable

5−import Effect.Default

4+import public Effect.Default

6

5

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

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

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

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

libs/prelude/Decidable/Equality.idr+3

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

2

3import Builtins

4import Prelude.Basics

5+import Prelude.Bool

6+import Prelude.Classes

5import Prelude.Either

7import Prelude.Either

6import Prelude.List

8import Prelude.List

7import Prelude.Vect

9import Prelude.Vect

10+import Prelude.Nat

8import Prelude.Fin

11import Prelude.Fin

9import Prelude.Maybe

12import Prelude.Maybe

10

13

libs/prelude/IO.idr+1

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

1%unqualified

2

3+import Builtins

3import Prelude.List

4import Prelude.List

4

5

5%access public

6%access public

libs/prelude/Prelude.idr+27−24

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

1module Prelude

2

3−import Builtins

3+import public Builtins

4−import IO

4+import public IO

5−

5+

6+import public Prelude.Algebra

7+import public Prelude.Basics

6−import Prelude.Bool

8+import public Prelude.Bool

7−import Prelude.Classes

9+import public Prelude.Classes

8−import Prelude.Cast

10+import public Prelude.Cast

9−import Prelude.Nat

11+import public Prelude.Nat

10−import Prelude.Fin

12+import public Prelude.Fin

11−import Prelude.List

13+import public Prelude.List

12−import Prelude.Maybe

14+import public Prelude.Maybe

13−import Prelude.Monad

15+import public Prelude.Monad

14−import Prelude.Applicative

16+import public Prelude.Applicative

17+import public Prelude.Foldable

15−import Prelude.Functor

18+import public Prelude.Functor

16−import Prelude.Either

19+import public Prelude.Either

17−import Prelude.Vect

20+import public Prelude.Vect

18−import Prelude.Strings

21+import public Prelude.Strings

19−import Prelude.Chars

22+import public Prelude.Chars

20−import Prelude.Traversable

23+import public Prelude.Traversable

21−import Prelude.Bits

24+import public Prelude.Bits

22−import Prelude.Stream

25+import public Prelude.Stream

23−import Prelude.Uninhabited

26+import public Prelude.Uninhabited

24−import Prelude.Pairs

27+import public Prelude.Pairs

25−

28+

26−import Decidable.Equality

29+import public Decidable.Equality

27

30

28%access public

31%access public

29%default total

32%default total

libs/prelude/Prelude/Applicative.idr+2

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

1module Prelude.Applicative

2

3import Builtins

4+

4import Prelude.Basics

5import Prelude.Basics

6+import Prelude.Bool

5import Prelude.Classes

7import Prelude.Classes

6import Prelude.Functor

8import Prelude.Functor

7

9

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

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

1module Prelude.Bits

2

3+import Builtins

4+

5+import Prelude.Basics

6+import Prelude.Bool

7+import Prelude.Cast

8+import Prelude.Classes

9+import Prelude.Foldable

10+import Prelude.Nat

3import Prelude.Strings

11import Prelude.Strings

4import Prelude.Vect

12import Prelude.Vect

5−import Prelude.Bool

6

13

7%access public

14%access public

8%default total

15%default total

libs/prelude/Prelude/Either.idr+3

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

2

3import Builtins

4

5+import Prelude.Basics

6+import Prelude.Bool

7+import Prelude.Classes

5import Prelude.Maybe

8import Prelude.Maybe

6import Prelude.List

9import Prelude.List

7

10

libs/prelude/Prelude/Fin.idr+7

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

1module Prelude.Fin

2

3+import Builtins

4+

5+import Prelude.Basics

6+import Prelude.Bool

7+import Prelude.Cast

8+import Prelude.Classes

9+import Prelude.Maybe

3import Prelude.Nat

10import Prelude.Nat

4import Prelude.Either

11import Prelude.Either

5import Prelude.Uninhabited

12import Prelude.Uninhabited

libs/prelude/Prelude/Foldable.idr+1

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

2

3import Builtins

4import Prelude.Bool

5+import Prelude.Basics

5import Prelude.Classes

6import Prelude.Classes

6import Prelude.Algebra

7import Prelude.Algebra

7

8

libs/prelude/Prelude/List.idr+2

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

4

5import Prelude.Algebra

6import Prelude.Basics

7+import Prelude.Bool

8+import Prelude.Classes

7import Prelude.Foldable

9import Prelude.Foldable

8import Prelude.Functor

10import Prelude.Functor

9import Prelude.Maybe

11import Prelude.Maybe

libs/prelude/Prelude/Maybe.idr+3

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

2

3import Builtins

4import Prelude.Algebra

5+import Prelude.Basics

6+import Prelude.Bool

5import Prelude.Cast

7import Prelude.Cast

8+import Prelude.Classes

6import Prelude.Foldable

9import Prelude.Foldable

7

10

8%access public

11%access public

libs/prelude/Prelude/Nat.idr+1

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

3import Builtins

4

5import Prelude.Algebra

6+import Prelude.Basics

6import Prelude.Bool

7import Prelude.Bool

7import Prelude.Cast

8import Prelude.Cast

8import Prelude.Classes

9import Prelude.Classes

libs/prelude/Prelude/Stream.idr+4

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

1module Prelude.Stream

2

3+import Builtins

4+

5+import Prelude.Basics

3import Prelude.Functor

6import Prelude.Functor

7+import Prelude.Nat

4import Prelude.Vect

8import Prelude.Vect

5

9

6%access public

10%access public

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

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

1module Prelude.Strings

2

3import Builtins

4+

5+import Prelude.Algebra

4−import Prelude.List

6+import Prelude.Basics

7+import Prelude.Bool

5import Prelude.Chars

8import Prelude.Chars

6import Prelude.Cast

9import Prelude.Cast

10+import Prelude.Classes

7import Prelude.Either

11import Prelude.Either

8import Prelude.Foldable

12import Prelude.Foldable

13+import Prelude.Functor

14+import Prelude.List

15+import Prelude.Nat

9

16

10||| Appends two strings together.

17||| Appends two strings together.

11|||

18|||

libs/prelude/Prelude/Traversable.idr+4

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

1module Prelude.Traversable

2

3+import Builtins

4+

5+import Prelude.Basics

3import Prelude.Applicative

6import Prelude.Applicative

4import Prelude.Foldable

7import Prelude.Foldable

8+import Prelude.Functor

5

9

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

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

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

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

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

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

1module Prelude.Vect

2

3+import Builtins

4+

5+import Prelude.Basics

6+import Prelude.Bool

3import Prelude.Fin

7import Prelude.Fin

4import Prelude.Foldable

8import Prelude.Foldable

5import Prelude.Functor

9import Prelude.Functor

10+import Prelude.Maybe

6import Prelude.List

11import Prelude.List

7import Prelude.Classes

12import Prelude.Classes

8import Prelude.Nat

13import Prelude.Nat

9−import Prelude.Bool

10import Prelude.Uninhabited

14import Prelude.Uninhabited

11

15

12%access public

16%access public

src/Idris/AbsSyntax.hs+7−6

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

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

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

99

100−addImported :: FilePath -> Idris ()

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

101+addImported pub f

101−addImported f = do i <- getIState

102+ = do i <- getIState

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

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

103

104

104addLangExt :: LanguageExt -> Idris ()

105addLangExt :: LanguageExt -> Idris ()

105addLangExt TypeProviders = do i <- getIState

106addLangExt TypeProviders = do i <- getIState

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

382getHdrs :: Codegen -> Idris [String]

383getHdrs :: Codegen -> Idris [String]

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

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

384

385

385−getImported :: Idris [FilePath]

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

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

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

387

388

388setErrSpan :: FC -> Idris ()

389setErrSpan :: FC -> Idris ()

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

1576 _ -> True

1577 _ -> True

1577

1578

1578 getAccessibility n

1579 getAccessibility n

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

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

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

1581+ Just (n,t) -> t

1581 _ -> Public

1582 _ -> Public

1582

1583

1583 insertImpl :: [PArg] -> [PArg] -> [PArg]

1584 insertImpl :: [PArg] -> [PArg] -> [PArg]

src/Idris/AbsSyntaxTree.hs+2−2

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

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

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

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

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

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

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

192 errSpan :: Maybe FC,

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

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

259 | IBCMetavar Name

260 | IBCSyntax Syntax

261 | IBCKeyword String

262− | IBCImport FilePath

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

263 | IBCImportDir FilePath

264 | IBCObj Codegen FilePath

265 | IBCLib Codegen String

src/Idris/Chaser.hs+1−1

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

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

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

140 clearParserWarnings

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

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

142 return (concat ms)

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

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

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

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

981

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

983lookupP n ctxt

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

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

985 p <- case def of

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

987 (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)

32import Util.Zlib (decompressEither)

33

34ibcVersion :: Word8

35−ibcVersion = 87

35+ibcVersion = 88

36

37data IBCFile = IBCFile { ver :: Word8,

38 sourcefile :: FilePath,

39 symbols :: [Name],

40− ibc_imports :: [FilePath],

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

41 ibc_importdirs :: [FilePath],

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

43 ibc_fixes :: [FixDecl],

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

83initIBC :: IBCFile

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

85

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

86−loadIBC :: FilePath -> Idris ()

87+ -> FilePath -> Idris ()

88+loadIBC reexport fp

87−loadIBC fp = do imps <- getImported

89+ = do imps <- getImported

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

90+ let redo = case lookup fp imps of

91+ Nothing -> True

92+ Just p -> not p && reexport

93+ when redo $

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

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

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

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

91− process ibcf fp

96+ process reexport ibcf fp

92− addImported fp

97+ addImported reexport fp

93

98

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

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

95bencode f d = B.writeFile f (compress (encode d))

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

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

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

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

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

252

257

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

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

259+ IBCFile -> FilePath -> Idris ()

254−process i fn

260+process reexp i fn

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

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

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

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

257 | otherwise =

263 | otherwise =

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

277 pCGFlags (ibc_cgflags i)

283 pCGFlags (ibc_cgflags i)

278 pDyLibs (ibc_dynamic_libs i)

284 pDyLibs (ibc_dynamic_libs i)

279 pHdrs (ibc_hdrs i)

285 pHdrs (ibc_hdrs i)

280− pDefs (symbols i) (ibc_defs i)

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

281 pPatdefs (ibc_patdefs i)

287 pPatdefs (ibc_patdefs i)

282− pAccess (ibc_access i)

288+ pAccess reexp (ibc_access i)

283 pFlags (ibc_flags i)

289 pFlags (ibc_flags i)

284 pFnInfo (ibc_fninfo i)

290 pFnInfo (ibc_fninfo i)

285 pTotal (ibc_total i)

291 pTotal (ibc_total i)

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

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

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

318pImportDirs fs = mapM_ addImportDir fs

324pImportDirs fs = mapM_ addImportDir fs

319

325

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

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

321pImports fs

327pImports fs

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

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

329+ do i <- getIState

323 ibcsd <- valIBCSubDir i

330 ibcsd <- valIBCSubDir i

324 ids <- allImportDirs

331 ids <- allImportDirs

325 fp <- findImport ids ibcsd f

332 fp <- findImport ids ibcsd f

326− if (f `elem` imported i)

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

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

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

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

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

329− case fp of

336+ case fp of

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

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

331− ifail "Must be an ibc"

338+ ifail "Must be an ibc"

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

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

333− ifail "Must be an ibc"

340+ ifail "Must be an ibc"

334− IBC fn src -> loadIBC fn)

341+ IBC fn src -> loadIBC re fn)

335 fs

342 fs

336

343

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

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

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

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

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

429 ds

436 ds

430

437

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

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

432−pDefs syms ds

439+pDefs reexp syms ds

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

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

434 do let d' = updateDef d

441 do let d' = updateDef d

435 case d' of

442 case d' of

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

438 solveDeferred n

445 solveDeferred n

439 i <- getIState

446 i <- getIState

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

447-- 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

442 where

452 where

443 updateDef (CaseOp c t args o s cd)

453 updateDef (CaseOp c t args o s cd)

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

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

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

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

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

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

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

464

474

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

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

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

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

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

467− do i <- getIState

481+ i <- getIState

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

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

469 ds

483 ds

470

484

src/Idris/Parser.hs+19−17

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

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

110@

111 -}

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

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

113import_ = do fc <- getFC

114 reserved "import"

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

115 id <- identifier

116 id <- identifier

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

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

117 option ';' (lchar ';')

118 option ';' (lchar ';')

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

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

119 <?> "import statement"

120 <?> "import statement"

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

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

121

122

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

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

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

1133

1134

1134-- | Parse module header and imports

1135-- | 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)

1136parseImports fname input

1137parseImports fname input

1137 = do i <- getIState

1138 = do i <- getIState

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

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

1139 Failure err -> fail (show err)

1140 Failure err -> fail (show err)

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

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

1141 return x

1142 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)

1143 imports = do whiteSpace

1144 imports = do whiteSpace

1144 mname <- moduleHeader

1145 mname <- moduleHeader

1145 ps <- many import_

1146 ps <- many import_

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

1219 IDR fn -> loadSource False fn Nothing

1220 IDR fn -> loadSource False fn Nothing

1220 LIDR fn -> loadSource True fn Nothing

1221 LIDR fn -> loadSource True fn Nothing

1221 IBC fn src ->

1222 IBC fn src ->

1222− idrisCatch (loadIBC fn)

1223+ idrisCatch (loadIBC True fn)

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

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

1224 case src of

1225 case src of

1225 IDR sfn -> loadSource False sfn Nothing

1226 IDR sfn -> loadSource False sfn Nothing

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

1229

1230

1231

1231{- | Load idris code from file -}

1232{- | Load idris code from file -}

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

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

1233−loadFromIFile i@(IBC fn src) maxline

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

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

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

1235− idrisCatch (loadIBC fn)

1236+ idrisCatch (loadIBC reexp fn)

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

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

1237 where

1238 where

1238 getSrcFile (IDR fn) = fn

1239 getSrcFile (IDR fn) = fn

1239 getSrcFile (LIDR fn) = fn

1240 getSrcFile (LIDR fn) = fn

1240 getSrcFile (IBC f src) = getSrcFile src

1241 getSrcFile (IBC f src) = getSrcFile src

1241

1242

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

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

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

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

1244

1245

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

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

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

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

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

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

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

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

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

1264 ai <- getAutoImports

1265 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

1266 ids <- allImportDirs

1267 ids <- allImportDirs

1267 ibcsd <- valIBCSubDir i

1268 ibcsd <- valIBCSubDir i

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

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

1270+ do fp <- findImport ids ibcsd f

1269 case fp of

1271 case fp of

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

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

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

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

1272− IBC fn src -> loadIBC fn)

1274+ IBC fn src -> loadIBC True fn)

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

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

1274 reportParserWarnings

1276 reportParserWarnings

1275

1277

1276 -- process and check module aliases

1278 -- process and check module aliases

1277 let modAliases = M.fromList

1279 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]

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

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

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

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

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

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

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

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

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

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

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

1289 -- record package info in .ibc

1291 -- record package info in .ibc

1290 imps <- allImportDirs

1292 imps <- allImportDirs

1291 mapM_ addIBC (map IBCImportDir imps)

1293 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]

1293 let syntax = defaultSyntax{ syn_namespace = reverse mname,

1295 let syntax = defaultSyntax{ syn_namespace = reverse mname,

1294 maxline = toline }

1296 maxline = toline }

1295 ds' <- parseProg syntax f file pos

1297 ds' <- parseProg syntax f file pos

src/Idris/REPL.hs+3−3

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

1075 runIO $ hClose tmph

1076 t <- codegen

1077 ir <- compile t tmpn m

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

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

1079 case idris_outputmode ist of

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

1081 return ()

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

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

1092 ir <- compile codegen f m

1093 i <- getIState

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

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

1095 where fc = fileFC "main"

1096process fn (LogLvl i) = setLogLevel i

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

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

1403 then Just l

1404 else Nothing

1405 _ -> Nothing

1406− loadFromIFile f maxline

1406+ loadFromIFile True f maxline

1407 inew <- getIState

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

1409 -- preserve it all from source inputs

test/effects001/test021.idr+1

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

1module Main

2

3+import Effects

3import Effect.File

4import Effect.File

4import Effect.State

5import Effect.State

5import Effect.StdIO

6import Effect.StdIO

test/effects001/test021a.idr+1

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

1module Main

2

3+import Effects

3import Effect.State

4import Effect.State

4import Effect.Exception

5import Effect.Exception

5import Effect.Random

6import Effect.Random

test/io003/test018a.idr+1

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

1module Main

2

3+import System

3import System.Concurrency.Process

4import System.Concurrency.Process

4

5

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

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