@@ -3,7 +3,7 @@
33
44module Idris.IBC (loadIBC, loadPkgIndex,
55 writeIBC, writePkgIndex,
6− hasValidIBCVersion) where
6+ hasValidIBCVersion, IBCPhase(..)) where
77
88import Idris.Core.Evaluate
99import Idris.Core.TT
@@ -40,13 +40,14 @@ import System.Directory
4040import Codec.Archive.Zip
4141
4242ibcVersion :: Word16
43−ibcVersion = 130
43+ibcVersion = 131
4444
4545-- When IBC is being loaded - we'll load different things (and omit different
4646-- structures/definitions) depending on which phase we're in
4747data IBCPhase = IBC_Building -- ^ when building the module tree
48− | IBC_REPL -- ^ when loading modules for the REPL
49− | IBC_IDE -- ^ when running in IDE mode
48+ | IBC_REPL Bool -- ^ when loading modules for the REPL
49+ -- Bool = True for top level module
50+ deriving (Show, Eq)
5051
5152data IBCFile = IBCFile { ver :: Word16,
5253 sourcefile :: FilePath,
@@ -69,13 +70,10 @@ data IBCFile = IBCFile { ver :: Word16,
6970 ibc_cgflags :: ![(Codegen, String)],
7071 ibc_dynamic_libs :: ![String],
7172 ibc_hdrs :: ![(Codegen, String)],
72− ibc_access :: ![(Name, Accessibility)],
73− ibc_total :: ![(Name, Totality)],
7473 ibc_totcheckfail :: ![(FC, String)],
7574 ibc_flags :: ![(Name, [FnOpt])],
7675 ibc_fninfo :: ![(Name, FnInfo)],
7776 ibc_cg :: ![(Name, CGInfo)],
78− ibc_defs :: ![(Name, Def)],
7977 ibc_docstrings :: ![(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))],
8078 ibc_moduledocs :: ![(Name, Docstring D.DocTerm)],
8179 ibc_transforms :: ![(Name, (Term, Term))],
@@ -94,7 +92,10 @@ data IBCFile = IBCFile { ver :: Word16,
9492 ibc_usage :: ![(Name, Int)],
9593 ibc_exports :: ![Name],
9694 ibc_autohints :: ![(Name, Name)],
97− ibc_deprecated :: ![(Name, String)]
95+ ibc_deprecated :: ![(Name, String)],
96+ ibc_defs :: ![(Name, Def)],
97+ ibc_total :: ![(Name, Totality)],
98+ ibc_access :: ![(Name, Accessibility)]
9899 }
99100 deriving Show
100101{-!
@@ -102,7 +103,7 @@ deriving instance Binary IBCFile
102103!-}
103104
104105initIBC :: IBCFile
105−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] []
106+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] []
106107
107108hasValidIBCVersion :: FilePath -> Idris Bool
108109hasValidIBCVersion fp = do
@@ -113,8 +114,9 @@ hasValidIBCVersion fp = do
113114 return (ver == ibcVersion)
114115
115116loadIBC :: Bool -- ^ True = reexport, False = make everything private
117+ -> IBCPhase
116118 -> FilePath -> Idris ()
117−loadIBC reexport fp
119+loadIBC reexport phase fp
118120 = do imps <- getImported
119121 let redo = case lookup fp imps of
120122 Nothing -> True
@@ -125,7 +127,7 @@ loadIBC reexport fp
125127 case toArchiveOrFail archiveFile of
126128 Left _ -> ifail $ fp ++ " isn't loadable, it may have an old ibc format.\n"
127129 ++ "Please clean and rebuild it."
128− Right archive -> do process reexport archive fp
130+ Right archive -> do process reexport phase archive fp
129131 addImported reexport fp
130132-- dumpTT
131133
@@ -134,7 +136,7 @@ loadPkgIndex :: String -> Idris ()
134136loadPkgIndex pkg = do ddir <- runIO $ getIdrisLibDir
135137 addImportDir (ddir </> pkg)
136138 fp <- findPkgIndex pkg
137− loadIBC True fp
139+ loadIBC True IBC_Building fp
138140
139141
140142makeEntry :: (Binary b) => String -> [b] -> Maybe Entry
@@ -164,13 +166,10 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),
164166 makeEntry "ibc_cgflags" (ibc_cgflags i),
165167 makeEntry "ibc_dynamic_libs" (ibc_dynamic_libs i),
166168 makeEntry "ibc_hdrs" (ibc_hdrs i),
167− makeEntry "ibc_access" (ibc_access i),
168− makeEntry "ibc_total" (ibc_total i),
169169 makeEntry "ibc_totcheckfail" (ibc_totcheckfail i),
170170 makeEntry "ibc_flags" (ibc_flags i),
171171 makeEntry "ibc_fninfo" (ibc_fninfo i),
172172 makeEntry "ibc_cg" (ibc_cg i),
173− makeEntry "ibc_defs" (ibc_defs i),
174173 makeEntry "ibc_docstrings" (ibc_docstrings i),
175174 makeEntry "ibc_moduledocs" (ibc_moduledocs i),
176175 makeEntry "ibc_transforms" (ibc_transforms i),
@@ -189,7 +188,10 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),
189188 makeEntry "ibc_usage" (ibc_usage i),
190189 makeEntry "ibc_exports" (ibc_exports i),
191190 makeEntry "ibc_autohints" (ibc_autohints i),
192− makeEntry "ibc_deprecated" (ibc_deprecated i)]
191+ makeEntry "ibc_deprecated" (ibc_deprecated i),
192+ makeEntry "ibc_defs" (ibc_defs i),
193+ makeEntry "ibc_total" (ibc_total i),
194+ makeEntry "ibc_access" (ibc_access i)]
193195
194196writeArchive :: FilePath -> IBCFile -> Idris ()
195197writeArchive fp i = do let a = L.foldl (\x y -> addEntryToArchive y x) emptyArchive (entries i)
@@ -323,8 +325,9 @@ getEntry alt f a = case findEntryByPath f a of
323325 Just e -> return $! (force . decode . fromEntry) e
324326
325327process :: Bool -- ^ Reexporting
328+ -> IBCPhase
326329 -> Archive -> FilePath -> Idris ()
327−process reexp i fn = do
330+process reexp phase i fn = do
328331 ver <- getEntry 0 "ver" i
329332 when (ver /= ibcVersion) $ do
330333 logIBC 1 "ibc out of date"
@@ -336,7 +339,7 @@ process reexp i fn = do
336339 srcok <- runIO $ doesFileExist source
337340 when srcok $ timestampOlder source fn
338341 pImportDirs =<< getEntry [] "ibc_importdirs" i
339− pImports reexp =<< getEntry [] "ibc_imports" i
342+ pImports reexp phase =<< getEntry [] "ibc_imports" i
340343 pImps =<< getEntry [] "ibc_implicits" i
341344 pFixes =<< getEntry [] "ibc_fixes" i
342345 pStatics =<< getEntry [] "ibc_statics" i
@@ -353,12 +356,9 @@ process reexp i fn = do
353356 pCGFlags =<< getEntry [] "ibc_cgflags" i
354357 pDyLibs =<< getEntry [] "ibc_dynamic_libs" i
355358 pHdrs =<< getEntry [] "ibc_hdrs" i
356− pDefs reexp =<< getEntry [] "ibc_defs" i
357359 pPatdefs =<< getEntry [] "ibc_patdefs" i
358− pAccess reexp =<< getEntry [] "ibc_access" i
359360 pFlags =<< getEntry [] "ibc_flags" i
360361 pFnInfo =<< getEntry [] "ibc_fninfo" i
361− pTotal =<< getEntry [] "ibc_total" i
362362 pTotCheckErr =<< getEntry [] "ibc_totcheckfail" i
363363 pCG =<< getEntry [] "ibc_cg" i
364364 pDocs =<< getEntry [] "ibc_docstrings" i
@@ -379,6 +379,9 @@ process reexp i fn = do
379379 pExports =<< getEntry [] "ibc_exports" i
380380 pAutoHints =<< getEntry [] "ibc_autohints" i
381381 pDeprecate =<< getEntry [] "ibc_deprecated" i
382+ pDefs reexp =<< getEntry [] "ibc_defs" i
383+ pTotal =<< getEntry [] "ibc_total" i
384+ pAccess reexp phase =<< getEntry [] "ibc_access" i
382385
383386timestampOlder :: FilePath -> FilePath -> Idris ()
384387timestampOlder src ibc = do srct <- runIO $ getModificationTime src
@@ -412,8 +415,8 @@ pDeprecate ns = mapM_ (\(n,reason) -> addDeprecated n reason) ns
412415pImportDirs :: [FilePath] -> Idris ()
413416pImportDirs fs = mapM_ addImportDir fs
414417
415−pImports :: Bool -> [(Bool, FilePath)] -> Idris ()
416−pImports reexp fs
418+pImports :: Bool -> IBCPhase -> [(Bool, FilePath)] -> Idris ()
419+pImports reexp phase fs
417420 = do mapM_ (\(re, f) ->
418421 do i <- getIState
419422 ibcsd <- valIBCSubDir i
@@ -422,6 +425,9 @@ pImports reexp fs
422425-- if (f `elem` imported i)
423426-- then logLvl 1 $ "Already read " ++ f
424427 putIState (i { imported = f : imported i })
428+ let phase' = case phase of
429+ IBC_REPL _ -> IBC_REPL False
430+ p -> p
425431 case fp of
426432 LIDR fn -> do
427433 logIBC 1 $ "Failed at " ++ fn
@@ -429,7 +435,7 @@ pImports reexp fs
429435 IDR fn -> do
430436 logIBC 1 $ "Failed at " ++ fn
431437 ifail "Must be an ibc"
432− IBC fn src -> loadIBC (reexp && re) fn)
438+ IBC fn src -> loadIBC (reexp && re) phase' fn)
433439 fs
434440
435441pImps :: [(Name, [PArg])] -> Idris ()
@@ -528,10 +534,7 @@ pDefs reexp ds
528534 _ -> do logIBC 1 $ "SOLVING " ++ show n
529535 solveDeferred n
530536 updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })
531−-- logLvl 1 $ "Added " ++ show (n, d')
532− if (not reexp) then do logIBC 1 $ "Not exporting " ++ show n
533− setAccessibility n Hidden
534− else logIBC 1 $ "Exporting " ++ show n) ds
537+ ) ds
535538 where
536539 updateDef (CaseOp c t args o s cd)
537540 = do o' <- mapM updateOrig o
@@ -599,12 +602,22 @@ pMDocs ds = mapM_ (\ (n, d) -> updateIState (\i ->
599602 i { idris_moduledocs = addDef n d (idris_moduledocs i) })) ds
600603
601604pAccess :: Bool -- ^ Reexporting?
605+ -> IBCPhase
602606 -> [(Name, Accessibility)] -> Idris ()
603−pAccess reexp ds
607+pAccess reexp phase ds
604608 = mapM_ (\ (n, a_in) ->
605609 do let a = if reexp then a_in else Hidden
606610 logIBC 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a
607− updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })) ds
611+ updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })
612+
613+ if (not reexp) then do logIBC 1 $ "Not exporting " ++ show n
614+ setAccessibility n Hidden
615+ else logIBC 1 $ "Exporting " ++ show n
616+ -- Everything should be available at the REPL from
617+ -- things imported publicly
618+ when (phase == IBC_REPL True) $
619+ setAccessibility n Public
620+ ) ds
608621
609622pFlags :: [(Name, [FnOpt])] -> Idris ()
610623pFlags ds = mapM_ (\ (n, a) -> setFlags n a) ds