3820110 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Ensure modules are loaded independently

Fixes #1021 This also exposed a couple of bugs in the library, in which things were being used but not imported, but we were getting away with it because of the previous problem. This relies on a bit of a hack to preserve missing cases, type inference information and interactive editing data, which is not saved in ibcs, but should be.

commit3820110510ad3968996a3a39ac52706ffb95aa45 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 3 Apr 2014, 01:29 (13 years ago) parent53a5014

11 files changed+88−34

compare with master

unifiedsplit

libs/prelude/Prelude/Applicative.idr+2 libs/prelude/Prelude/Chars.idr+3 libs/prelude/Prelude/Fin.idr+5 libs/prelude/Prelude/Nat.idr+4 libs/prelude/Prelude/Uninhabited.idr+2−7 src/Idris/AbsSyntax.hs+7 src/Idris/AbsSyntaxTree.hs+2−6 src/Idris/ElabDecls.hs+2−1 src/Idris/IBC.hs+6−3 src/Idris/Parser.hs+8 src/Idris/REPL.hs+47−17

libs/prelude/Prelude/Applicative.idr+2

@@ -1,6 +1,8 @@

11module Prelude.Applicative

33import Builtins

4+import Prelude.Basics

5+import Prelude.Classes

46import Prelude.Functor

68---- Applicative functors/Idioms

libs/prelude/Prelude/Chars.idr+3

@@ -1,6 +1,9 @@

11module Prelude.Char

22-- Functions operating over Chars

4+import Prelude.Bool

5+import Prelude.Classes

6+import Prelude.List

47import Builtins

69||| Return the ASCII representation of the character.

libs/prelude/Prelude/Fin.idr+5

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

33import Prelude.Nat

44import Prelude.Either

5+import Prelude.Uninhabited

67%default total

@@ -11,6 +12,10 @@ data Fin : (n : Nat) -> Type where

1112 fZ : Fin (S k)

1213 fS : Fin k -> Fin (S k)

1314

15+instance Uninhabited (Fin Z) where

16+ uninhabited fZ impossible

17+ uninhabited (fS f) impossible

18+

1419fSInjective : (m : Fin k) -> (n : Fin k) -> fS m = fS n -> m = n

1520fSInjective left _ refl = refl

1621

libs/prelude/Prelude/Nat.idr+4

@@ -6,6 +6,7 @@ import Prelude.Algebra

66import Prelude.Bool

77import Prelude.Cast

88import Prelude.Classes

9+import Prelude.Uninhabited

910

1011%access public

1112%default total

@@ -20,6 +21,9 @@ import Prelude.Classes

2021-- name hints for interactive editing

2122%name Nat k,j,i,n,m

2223

24+instance Uninhabited (Z = S n) where

25+ uninhabited refl impossible

26+

2327--------------------------------------------------------------------------------

2428-- Syntactic tests

2529--------------------------------------------------------------------------------

libs/prelude/Prelude/Uninhabited.idr+2−7

@@ -1,18 +1,13 @@

11module Prelude.Uninhabited

3+import Builtins

35||| A canonical proof that some type is empty

46class Uninhabited t where

57 ||| If I have a t, I've had a contradiction

68 ||| @ t the uninhabited type

79 total uninhabited : t -> _|_

810

9−instance Uninhabited (Fin Z) where

10− uninhabited fZ impossible

11− uninhabited (fS f) impossible

12−

13−instance Uninhabited (Z = S n) where

14− uninhabited refl impossible

15−

1611||| Use an absurd assumption to discharge a proof obligation

1712||| @ t some empty type

1813||| @ a the goal type

src/Idris/AbsSyntax.hs+7

@@ -88,6 +88,10 @@ addDyLib libs = do i <- getIState

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

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

9090

91+addImported :: FilePath -> Idris ()

92+addImported f = do i <- getIState

93+ putIState $ i { idris_imported = nub $ f : idris_imported i }

94+

9195addLangExt :: LanguageExt -> Idris ()

9296addLangExt TypeProviders = do i <- getIState

9397 putIState $ i {

@@ -357,6 +361,9 @@ addNameIdx' i n

357361getHdrs :: Codegen -> Idris [String]

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

359363

364+getImported :: Idris [FilePath]

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

366+

360367setErrSpan :: FC -> Idris ()

361368setErrSpan x = do i <- getIState;

362369 case (errSpan i) of

src/Idris/AbsSyntaxTree.hs+2−6

@@ -91,11 +91,6 @@ data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines sh

9191 | ColsWide Int -- ^ Manually specified - must be positive

9292 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise

9393

94−-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

95−-- without typechecking).

96−-- This will include all the functions and data declarations, plus fixity declarations

97−-- and syntax macros.

98−

9994-- | The global state used in the Idris monad

10095data IState = IState {

10196 tt_ctxt :: Context, -- ^ All the currently defined names and their terms

@@ -134,6 +129,7 @@ data IState = IState {

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

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

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

132+ idris_imported :: [FilePath], -- ^ Imported ibc file names

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

138134 errSpan :: Maybe FC,

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

@@ -225,7 +221,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

225221 emptyContext emptyContext emptyContext emptyContext

226222 emptyContext emptyContext

227223 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

228− [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

224+ [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

229225 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

230226 AutomaticWidth

231227

src/Idris/ElabDecls.hs+2−1

@@ -59,7 +59,8 @@ checkAddDef add toplvl fc [] = return []

5959checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

6060 = do ctxt <- getContext

6161 (t', _) <- recheckC fc [] t

62− when add $ addDeferred [(n, (i, top, t, toplvl))]

62+ when add $ do addDeferred [(n, (i, top, t, toplvl))]

63+ addIBC (IBCDef n)

6364 ns' <- checkAddDef add toplvl fc ns

6465 return ((n, (i, top, t')) : ns')

6566-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t

src/Idris/IBC.hs+6−3

@@ -76,9 +76,12 @@ initIBC :: IBCFile

7676initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

7777

7878loadIBC :: FilePath -> Idris ()

79−loadIBC fp = do iLOG $ "Loading ibc " ++ fp

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

81− process ibcf fp

79+loadIBC fp = do imps <- getImported

80+ when (not (fp `elem` imps)) $

81+ do iLOG $ "Loading ibc " ++ fp

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

83+ process ibcf fp

84+ addImported fp

8285

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

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

src/Idris/Parser.hs+8

@@ -1213,6 +1213,14 @@ loadSource h lidr f

12131213 file_in <- runIO $ readFile f

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

12151215 (mname, imports, pos) <- parseImports f file

1216+ ids <- allImportDirs

1217+ ibcsd <- valIBCSubDir i

1218+ mapM_ (\f -> do fp <- runIO $ findImport ids ibcsd f

1219+ case fp of

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

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

1222+ IBC fn src -> loadIBC fn)

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

12161224 reportParserWarnings

12171225

12181226 -- process and check module aliases

src/Idris/REPL.hs+47−17

@@ -1147,30 +1147,32 @@ loadInputs h inputs

11471147 let ninputs = zip [1..] inputs

11481148 ifiles <- mapWhileOK (\(num, input) ->

11491149 do putIState ist

1150− v <- verbose

1151− -- when v $ iputStrLn $ "(" ++ show num ++ "/" ++

1152− -- show (length inputs) ++

1153− -- ") " ++ input

11541150 modTree <- buildTree

11551151 (map snd (take (num-1) ninputs))

11561152 input

11571153 let ifiles = getModuleFiles modTree

11581154 iLOG ("MODULE TREE : " ++ show modTree)

11591155 iLOG ("RELOAD: " ++ show ifiles)

1160− when (not (all ibc ifiles) || loadCode) $ tryLoad ifiles

1156+ when (not (all ibc ifiles) || loadCode) $

1157+ tryLoad False (filter (not . ibc) ifiles)

11611158 -- return the files that need rechecking

1162− return (if (all ibc ifiles) then ifiles else []))

1159+ return ifiles)

11631160 ninputs

11641161 inew <- getIState

1165− -- to check everything worked consistently (in particular, will catch

1166− -- if the ibc version is out of date) if we weren't loading per

1167− -- module

1162+ let tidata = idris_tyinfodata inew

1163+ let lineapps = idris_lineapps inew

1164+ let patdefs = idris_patdefs inew

1165+ -- If it worked, load the whole thing from all the ibcs together

11681166 case errSpan inew of

11691167 Nothing ->

1170− do putIState ist

1171− when (not loadCode) $ tryLoad $ nub (concat ifiles)

1168+ do putIState (ist { idris_tyinfodata = tidata })

1169+ ibcfiles <- mapM findNewIBC (nub (concat ifiles))

1170+ tryLoad True (mapMaybe id ibcfiles)

11721171 _ -> return ()

1173− putIState inew)

1172+ ist <- getIState

1173+ putIState (ist { idris_tyinfodata = tidata,

1174+ idris_lineapps = lineapps,

1175+ idris_patdefs = patdefs }))

11741176 (\e -> do i <- getIState

11751177 case e of

11761178 At f _ -> do setErrSpan f

@@ -1179,15 +1181,43 @@ loadInputs h inputs

11791181 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

11801182 iputStrLn (pshow i e))

11811183 where -- load all files, stop if any fail

1182− tryLoad :: [IFileType] -> Idris ()

1183− tryLoad [] = return ()

1184− tryLoad (f : fs) = do loadFromIFile h f

1185− ok <- noErrors

1186− when ok $ tryLoad fs

1184+ tryLoad :: Bool -> [IFileType] -> Idris ()

1185+ tryLoad keepstate [] = return ()

1186+ tryLoad keepstate (f : fs)

1187+ = do ist <- getIState

1188+ loadFromIFile h f

1189+ inew <- getIState

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

1191+ -- preserve it all from source inputs

1192+ let tidata = idris_tyinfodata inew

1193+ let lineapps = idris_lineapps inew

1194+ let patdefs = idris_patdefs inew

1195+ ok <- noErrors

1196+ when ok $ do when (not keepstate) $ putIState ist

1197+ ist <- getIState

1198+ putIState (ist { idris_tyinfodata = tidata,

1199+ idris_lineapps = lineapps,

1200+ idris_patdefs = patdefs })

1201+ tryLoad keepstate fs

11871202

11881203 ibc (IBC _ _) = True

11891204 ibc _ = False

11901205

1206+ findNewIBC :: IFileType -> Idris (Maybe IFileType)

1207+ findNewIBC i@(IBC _ _) = return (Just i)

1208+ findNewIBC s@(IDR f) = do ist <- get

1209+ ibcsd <- valIBCSubDir ist

1210+ let ibc = ibcPathNoFallback ibcsd f

1211+ ok <- runIO $ doesFileExist ibc

1212+ if ok then return (Just (IBC ibc s))

1213+ else return Nothing

1214+ findNewIBC s@(LIDR f) = do ist <- get

1215+ ibcsd <- valIBCSubDir ist

1216+ let ibc = ibcPathNoFallback ibcsd f

1217+ ok <- runIO $ doesFileExist ibc

1218+ if ok then return (Just (IBC ibc s))

1219+ else return Nothing

1220+

11911221 -- Like mapM, but give up when there's an error

11921222 mapWhileOK f [] = return []

11931223 mapWhileOK f (x : xs) = do x' <- f x