@@ -41,11 +41,10 @@ import Codec.Archive.Zip
41import Util.Zlib (decompressEither)
41import Util.Zlib (decompressEither)
43ibcVersion :: Word16
43ibcVersion :: Word16
44−ibcVersion = 112
44+ibcVersion = 113
46data IBCFile = IBCFile { ver :: Word16,
46data IBCFile = IBCFile { ver :: Word16,
47 sourcefile :: FilePath,
47 sourcefile :: FilePath,
49 ibc_imports :: ![(Bool, FilePath)],
48 ibc_imports :: ![(Bool, FilePath)],
50 ibc_importdirs :: ![FilePath],
49 ibc_importdirs :: ![FilePath],
51 ibc_implicits :: ![(Name, [PArg])],
50 ibc_implicits :: ![(Name, [PArg])],
@@ -95,7 +94,7 @@ deriving instance Binary IBCFile
97initIBC :: IBCFile
96initIBC :: IBCFile
98−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []
97+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []
100loadIBC :: Bool -- ^ True = reexport, False = make everything private
99loadIBC :: Bool -- ^ True = reexport, False = make everything private
101 -> FilePath -> Idris ()
100 -> FilePath -> Idris ()
@@ -130,7 +129,6 @@ makeEntry name val = if L.null val
130entries :: IBCFile -> [Entry]
129entries :: IBCFile -> [Entry]
131entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),
130entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),
132 makeEntry "sourcefile" (sourcefile i),
131 makeEntry "sourcefile" (sourcefile i),
133− makeEntry "symbols" (symbols i),
134 makeEntry "ibc_imports" (ibc_imports i),
132 makeEntry "ibc_imports" (ibc_imports i),
135 makeEntry "ibc_importdirs" (ibc_importdirs i),
133 makeEntry "ibc_importdirs" (ibc_importdirs i),
136 makeEntry "ibc_implicits" (ibc_implicits i),
134 makeEntry "ibc_implicits" (ibc_implicits i),
@@ -330,9 +328,7 @@ process reexp i fn = do
330 pCGFlags =<< getEntry [] "ibc_cgflags" i
328 pCGFlags =<< getEntry [] "ibc_cgflags" i
331 pDyLibs =<< getEntry [] "ibc_dynamic_libs" i
329 pDyLibs =<< getEntry [] "ibc_dynamic_libs" i
332 pHdrs =<< getEntry [] "ibc_hdrs" i
330 pHdrs =<< getEntry [] "ibc_hdrs" i
333− symbols <- getEntry [] "symbols" i
334− defs <- getEntry [] "ibc_defs" i
335− pDefs reexp symbols defs
331+ pDefs reexp =<< getEntry [] "ibc_defs" i
336 pPatdefs =<< getEntry [] "ibc_patdefs" i
332 pPatdefs =<< getEntry [] "ibc_patdefs" i
337 pAccess reexp =<< getEntry [] "ibc_access" i
333 pAccess reexp =<< getEntry [] "ibc_access" i
338 pFlags =<< getEntry [] "ibc_flags" i
334 pFlags =<< getEntry [] "ibc_flags" i
@@ -485,8 +481,8 @@ pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()
485pPatdefs ds = mapM_ (\ (n, d) -> updateIState (\i ->
481pPatdefs ds = mapM_ (\ (n, d) -> updateIState (\i ->
486 i { idris_patdefs = addDef n (force d) (idris_patdefs i) })) ds
482 i { idris_patdefs = addDef n (force d) (idris_patdefs i) })) ds
488−pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()
484+pDefs :: Bool -> [(Name, Def)] -> Idris ()
489−pDefs reexp syms ds
485+pDefs reexp ds
490 = mapM_ (\ (n, d) ->
486 = mapM_ (\ (n, d) ->
491 do d' <- updateDef d
487 do d' <- updateDef d
492 case d' of
488 case d' of