@@ -2,7 +2,8 @@
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
4module Idris.IBC (loadIBC, loadPkgIndex,
4module Idris.IBC (loadIBC, loadPkgIndex,
5− writeIBC, writePkgIndex) where
5+ writeIBC, writePkgIndex,
6+ hasValidIBCVersion) where
7import Idris.Core.Evaluate
8import Idris.Core.Evaluate
8import Idris.Core.TT
9import Idris.Core.TT
@@ -94,6 +95,14 @@ deriving instance Binary IBCFile
94initIBC :: IBCFile
95initIBC :: IBCFile
95initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []
96initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []
98+hasValidIBCVersion :: FilePath -> Idris Bool
99+hasValidIBCVersion fp = do
100+ archiveFile <- runIO $ B.readFile fp
101+ case toArchiveOrFail archiveFile of
102+ Left _ -> return False
103+ Right archive -> do ver <- getEntry 0 "ver" archive
104+ return (ver == ibcVersion)
97loadIBC :: Bool -- ^ True = reexport, False = make everything private
106loadIBC :: Bool -- ^ True = reexport, False = make everything private
98 -> FilePath -> Idris ()
107 -> FilePath -> Idris ()
99loadIBC reexport fp
108loadIBC reexport fp