{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Serialise
( encode, encodeFile, encodeInterface
, decode, decodeFile, decodeInterface, decodeHashes
, EmbPrj
)
where
import System.Directory ( createDirectoryIfMissing )
import System.FilePath ( takeDirectory )
import Control.Arrow (second)
import Control.DeepSeq
import qualified Control.Exception as E
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State.Strict
import Data.Array.IArray
import Data.Word
import qualified Data.ByteString.Builder as L
import qualified Data.ByteString.Lazy as L
import qualified Data.HashTable.IO as H
import qualified Data.Map as Map
import qualified Data.Binary as B
import qualified Data.Binary.Get as B
import qualified Data.Binary.Put as B
import qualified Data.List as List
import Data.Function
import Data.Monoid
import qualified Codec.Compression.GZip as G
import qualified Codec.Compression.Zlib.Internal as Z
#if __GLASGOW_HASKELL__ >= 804
import GHC.Compact as C
#endif
import Agda.Interaction.Options
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Serialise.Base
import Agda.TypeChecking.Serialise.Instances ()
import Agda.TypeChecking.Monad
import Agda.Utils.Hash
import Agda.Utils.IORef
import Agda.Utils.Except
import Agda.Utils.Monad
currentInterfaceVersion :: Word64
currentInterfaceVersion = 20200305 * 10 + 0
data Encoded = Encoded
{ uncompressed :: L.ByteString
, compressed :: L.ByteString
}
encode :: EmbPrj a => a -> TCM Encoded
encode a = do
collectStats <- hasVerbosity "profile.serialize" 20
fileMod <- sourceToModule
newD@(Dict nD sD bD iD dD _tD
_nameD
_qnameD
nC sC bC iC dC tC
nameC
qnameC
stats _ _) <- liftIO $ emptyDict collectStats
root <- liftIO $ (`runReaderT` newD) $ do
icodeFileMod fileMod
icode a
nL <- benchSort $ l nD
sL <- benchSort $ l sD
bL <- benchSort $ l bD
iL <- benchSort $ l iD
dL <- benchSort $ l dD
verboseS "profile.sharing" 10 $ do
statistics "pointers" tC
verboseS "profile.serialize" 10 $ do
statistics "Integer" iC
statistics "String" sC
statistics "Text" bC
statistics "Double" dC
statistics "Node" nC
statistics "Shared Term" tC
statistics "A.QName" qnameC
statistics "A.Name" nameC
when collectStats $ do
stats <- Map.fromList . map (second toInteger) <$> do
liftIO $ H.toList stats
modifyStatistics $ Map.union stats
bits1 <- Bench.billTo [ Bench.Serialization, Bench.BinaryEncode ] $
return $!! B.encode (root, nL, sL, bL, iL, dL)
let compressParams = G.defaultCompressParams
{ G.compressLevel = G.bestSpeed
, G.compressStrategy = G.huffmanOnlyStrategy
}
cbits <- Bench.billTo [ Bench.Serialization, Bench.Compress ] $
return $!! G.compressWith compressParams bits1
let x = B.encode currentInterfaceVersion `L.append` cbits
return (Encoded { uncompressed = bits1, compressed = x })
where
l h = List.map fst . List.sortBy (compare `on` snd) <$> H.toList h
benchSort = Bench.billTo [Bench.Serialization, Bench.Sort] . liftIO
statistics :: String -> IORef FreshAndReuse -> TCM ()
statistics kind ioref = do
FreshAndReuse fresh
#ifdef DEBUG
reused
#endif
<- liftIO $ readIORef ioref
tickN (kind ++ " (fresh)") $ fromIntegral fresh
#ifdef DEBUG
tickN (kind ++ " (reused)") $ fromIntegral reused
#endif
decode :: EmbPrj a => L.ByteString -> TCM (Maybe a)
decode s = do
mf <- useTC stModuleToSource
incs <- getIncludeDirs
(mf, r) <- liftIO $ E.handle (\(E.ErrorCall s) -> noResult s) $ do
((r, nL, sL, bL, iL, dL), s, _) <- return $ runGetState B.get s 0
if s /= L.empty
then noResult "Garbage at end."
else do
st <- St (ar nL) (ar sL) (ar bL) (ar iL) (ar dL)
<$> liftIO H.new
<*> return mf <*> return incs
(r, st) <- runStateT (runExceptT (value r)) st
return (Just $ modFile st, r)
case mf of
Nothing -> return ()
Just mf -> stModuleToSource `setTCLens` mf
case r of
Right x -> do
#if __GLASGOW_HASKELL__ >= 804
Bench.billTo [Bench.Deserialization, Bench.Compaction] $
liftIO (Just . C.getCompact <$> C.compactWithSharing x)
#else
return (Just x)
#endif
Left err -> do
reportSLn "import.iface" 5 $ "Error when decoding interface file"
return Nothing
where
ar l = listArray (0, List.genericLength l - 1) l
noResult s = return (Nothing, Left $ GenericError s)
encodeInterface :: Interface -> TCM Encoded
encodeInterface i = do
r <- encode i
return (r { compressed = L.append hashes (compressed r) })
where
hashes :: L.ByteString
hashes = B.runPut $ B.put (iSourceHash i) >> B.put (iFullHash i)
encodeFile :: FilePath -> Interface -> TCM L.ByteString
encodeFile f i = do
r <- encodeInterface i
liftIO $ createDirectoryIfMissing True (takeDirectory f)
liftIO $ L.writeFile f (compressed r)
return (uncompressed r)
decodeInterface :: L.ByteString -> TCM (Maybe Interface)
decodeInterface s = do
s <- liftIO $
E.handle (\(E.ErrorCall s) -> return (Left s)) $
E.evaluate $
let (ver, s', _) = runGetState B.get (L.drop 16 s) 0 in
if ver /= currentInterfaceVersion
then Left "Wrong interface version."
else Right $
L.toLazyByteString $
Z.foldDecompressStreamWithInput
(\s -> (L.byteString s <>))
(\s -> if L.null s
then mempty
else error "Garbage at end.")
(\err -> error (show err))
(Z.decompressST Z.gzipFormat Z.defaultDecompressParams)
s'
case s of
Right s -> decode s
Left err -> do
reportSLn "import.iface" 5 $
"Error when decoding interface file: " ++ err
return Nothing
decodeHashes :: L.ByteString -> Maybe (Hash, Hash)
decodeHashes s
| L.length s < 16 = Nothing
| otherwise = Just $ B.runGet getH $ L.take 16 s
where getH = (,) <$> B.get <*> B.get
decodeFile :: FilePath -> TCM (Maybe Interface)
decodeFile f = decodeInterface =<< liftIO (L.readFile f)
icodeFileMod
:: SourceToModule
-> S ()
icodeFileMod fileMod = do
hmap <- asks absPathD
forM_ (Map.toList fileMod) $ \ (absolutePath, topLevelModuleName) -> do
i <- icod_ topLevelModuleName
liftIO $ H.insert hmap absolutePath i