{-# LANGUAGE CPP #-}

-- Andreas, Makoto, Francesco 2014-10-15 AIM XX:
-- -O2 does not have any noticable effect on runtime
-- but sabotages cabal repl with -Werror
-- (due to a conflict with --interactive warning)
-- {-# OPTIONS_GHC -O2                      #-}

-- | Structure-sharing serialisation of Agda interface files.

-- -!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-
-- NOTE: Every time the interface format is changed the interface
-- version number should be bumped _in the same patch_.
--
-- See 'currentInterfaceVersion' below.
--
-- -!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-

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 () --instance only

import Agda.TypeChecking.Monad

import Agda.Utils.Hash
import Agda.Utils.IORef

import Agda.Utils.Except
import Agda.Utils.Monad

-- Note that the Binary instance for Int writes 64 bits, but throws
-- away the 32 high bits when reading (at the time of writing, on
-- 32-bit machines). Word64 does not have these problems.

currentInterfaceVersion :: Word64
currentInterfaceVersion :: Word64
currentInterfaceVersion = Word64
20200305 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
10 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
0

-- | The result of 'encode' and 'encodeInterface'.

data Encoded = Encoded
  { Encoded -> ByteString
uncompressed :: L.ByteString
    -- ^ The uncompressed bytestring, without hashes and the interface
    -- version.
  , Encoded -> ByteString
compressed :: L.ByteString
    -- ^ The compressed bytestring.
  }

-- | Encodes something. To ensure relocatability file paths in
-- positions are replaced with module names.

encode :: EmbPrj a => a -> TCM Encoded
encode :: a -> TCM Encoded
encode a
a = do
    Bool
collectStats <- VerboseKey -> VerboseLevel -> TCMT IO Bool
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasVerbosity VerboseKey
"profile.serialize" VerboseLevel
20
    SourceToModule
fileMod <- TCM SourceToModule
sourceToModule
    newD :: Dict
newD@(Dict HashTable Node Int32
nD HashTable VerboseKey Int32
sD HashTable Text Int32
bD HashTable Integer Int32
iD HashTable Double Int32
dD HashTable (Ptr Term) Int32
_tD
      HashTable NameId Int32
_nameD
      HashTable QNameId Int32
_qnameD
      IORef FreshAndReuse
nC IORef FreshAndReuse
sC IORef FreshAndReuse
bC IORef FreshAndReuse
iC IORef FreshAndReuse
dC IORef FreshAndReuse
tC
      IORef FreshAndReuse
nameC
      IORef FreshAndReuse
qnameC
      HashTable VerboseKey VerboseLevel
stats Bool
_ HashTable AbsolutePath Int32
_) <- IO Dict -> TCMT IO Dict
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Dict -> TCMT IO Dict) -> IO Dict -> TCMT IO Dict
forall a b. (a -> b) -> a -> b
$ Bool -> IO Dict
emptyDict Bool
collectStats
    Int32
root <- IO Int32 -> TCMT IO Int32
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int32 -> TCMT IO Int32) -> IO Int32 -> TCMT IO Int32
forall a b. (a -> b) -> a -> b
$ (ReaderT Dict IO Int32 -> Dict -> IO Int32
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` Dict
newD) (ReaderT Dict IO Int32 -> IO Int32)
-> ReaderT Dict IO Int32 -> IO Int32
forall a b. (a -> b) -> a -> b
$ do
       SourceToModule -> S ()
icodeFileMod SourceToModule
fileMod  -- Only fills absPathD from fileMod
       a -> ReaderT Dict IO Int32
forall a. EmbPrj a => a -> ReaderT Dict IO Int32
icode a
a
    [Node]
nL <- IO [Node] -> TCMT IO [Node]
forall c. IO c -> TCMT IO c
benchSort (IO [Node] -> TCMT IO [Node]) -> IO [Node] -> TCMT IO [Node]
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld Node Int32 -> IO [Node]
forall b (h :: * -> * -> * -> *) b.
(Ord b, HashTable h, Hashable b, Eq b) =>
h RealWorld b b -> IO [b]
l HashTable RealWorld Node Int32
HashTable Node Int32
nD
    [VerboseKey]
sL <- IO [VerboseKey] -> TCMT IO [VerboseKey]
forall c. IO c -> TCMT IO c
benchSort (IO [VerboseKey] -> TCMT IO [VerboseKey])
-> IO [VerboseKey] -> TCMT IO [VerboseKey]
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld VerboseKey Int32 -> IO [VerboseKey]
forall b (h :: * -> * -> * -> *) b.
(Ord b, HashTable h, Hashable b, Eq b) =>
h RealWorld b b -> IO [b]
l HashTable RealWorld VerboseKey Int32
HashTable VerboseKey Int32
sD
    [Text]
bL <- IO [Text] -> TCMT IO [Text]
forall c. IO c -> TCMT IO c
benchSort (IO [Text] -> TCMT IO [Text]) -> IO [Text] -> TCMT IO [Text]
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld Text Int32 -> IO [Text]
forall b (h :: * -> * -> * -> *) b.
(Ord b, HashTable h, Hashable b, Eq b) =>
h RealWorld b b -> IO [b]
l HashTable RealWorld Text Int32
HashTable Text Int32
bD
    [Integer]
iL <- IO [Integer] -> TCMT IO [Integer]
forall c. IO c -> TCMT IO c
benchSort (IO [Integer] -> TCMT IO [Integer])
-> IO [Integer] -> TCMT IO [Integer]
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld Integer Int32 -> IO [Integer]
forall b (h :: * -> * -> * -> *) b.
(Ord b, HashTable h, Hashable b, Eq b) =>
h RealWorld b b -> IO [b]
l HashTable RealWorld Integer Int32
HashTable Integer Int32
iD
    [Double]
dL <- IO [Double] -> TCMT IO [Double]
forall c. IO c -> TCMT IO c
benchSort (IO [Double] -> TCMT IO [Double])
-> IO [Double] -> TCMT IO [Double]
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld Double Int32 -> IO [Double]
forall b (h :: * -> * -> * -> *) b.
(Ord b, HashTable h, Hashable b, Eq b) =>
h RealWorld b b -> IO [b]
l HashTable RealWorld Double Int32
HashTable Double Int32
dD
    -- Record reuse statistics.
    VerboseKey -> VerboseLevel -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"profile.sharing" VerboseLevel
10 (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
      VerboseKey -> IORef FreshAndReuse -> TCMT IO ()
statistics VerboseKey
"pointers" IORef FreshAndReuse
tC
    VerboseKey -> VerboseLevel -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"profile.serialize" VerboseLevel
10 (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
      VerboseKey -> IORef FreshAndReuse -> TCMT IO ()
statistics VerboseKey
"Integer"  IORef FreshAndReuse
iC
      VerboseKey -> IORef FreshAndReuse -> TCMT IO ()
statistics VerboseKey
"String"   IORef FreshAndReuse
sC
      VerboseKey -> IORef FreshAndReuse -> TCMT IO ()
statistics VerboseKey
"Text"     IORef FreshAndReuse
bC
      VerboseKey -> IORef FreshAndReuse -> TCMT IO ()
statistics VerboseKey
"Double"   IORef FreshAndReuse
dC
      VerboseKey -> IORef FreshAndReuse -> TCMT IO ()
statistics VerboseKey
"Node"     IORef FreshAndReuse
nC
      VerboseKey -> IORef FreshAndReuse -> TCMT IO ()
statistics VerboseKey
"Shared Term" IORef FreshAndReuse
tC
      VerboseKey -> IORef FreshAndReuse -> TCMT IO ()
statistics VerboseKey
"A.QName"  IORef FreshAndReuse
qnameC
      VerboseKey -> IORef FreshAndReuse -> TCMT IO ()
statistics VerboseKey
"A.Name"  IORef FreshAndReuse
nameC
    Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
collectStats (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
      Map VerboseKey Integer
stats <- [(VerboseKey, Integer)] -> Map VerboseKey Integer
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(VerboseKey, Integer)] -> Map VerboseKey Integer)
-> ([(VerboseKey, VerboseLevel)] -> [(VerboseKey, Integer)])
-> [(VerboseKey, VerboseLevel)]
-> Map VerboseKey Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((VerboseKey, VerboseLevel) -> (VerboseKey, Integer))
-> [(VerboseKey, VerboseLevel)] -> [(VerboseKey, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map ((VerboseLevel -> Integer)
-> (VerboseKey, VerboseLevel) -> (VerboseKey, Integer)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second VerboseLevel -> Integer
forall a. Integral a => a -> Integer
toInteger) ([(VerboseKey, VerboseLevel)] -> Map VerboseKey Integer)
-> TCMT IO [(VerboseKey, VerboseLevel)]
-> TCMT IO (Map VerboseKey Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        IO [(VerboseKey, VerboseLevel)]
-> TCMT IO [(VerboseKey, VerboseLevel)]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [(VerboseKey, VerboseLevel)]
 -> TCMT IO [(VerboseKey, VerboseLevel)])
-> IO [(VerboseKey, VerboseLevel)]
-> TCMT IO [(VerboseKey, VerboseLevel)]
forall a b. (a -> b) -> a -> b
$ HashTable VerboseKey VerboseLevel
-> IO [(VerboseKey, VerboseLevel)]
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> IO [(k, v)]
H.toList HashTable VerboseKey VerboseLevel
stats
      (Map VerboseKey Integer -> Map VerboseKey Integer) -> TCMT IO ()
modifyStatistics ((Map VerboseKey Integer -> Map VerboseKey Integer) -> TCMT IO ())
-> (Map VerboseKey Integer -> Map VerboseKey Integer) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Map VerboseKey Integer
-> Map VerboseKey Integer -> Map VerboseKey Integer
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map VerboseKey Integer
stats
    -- Encode hashmaps and root, and compress.
    ByteString
bits1 <- Account Phase -> TCMT IO ByteString -> TCMT IO ByteString
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [ Phase
Bench.Serialization, Phase
Bench.BinaryEncode ] (TCMT IO ByteString -> TCMT IO ByteString)
-> TCMT IO ByteString -> TCMT IO ByteString
forall a b. (a -> b) -> a -> b
$
      ByteString -> TCMT IO ByteString
forall (m :: * -> *) a. Monad m => a -> m a
return (ByteString -> TCMT IO ByteString)
-> ByteString -> TCMT IO ByteString
forall a b. NFData a => (a -> b) -> a -> b
$!! (Int32, [Node], [VerboseKey], [Text], [Integer], [Double])
-> ByteString
forall a. Binary a => a -> ByteString
B.encode (Int32
root, [Node]
nL, [VerboseKey]
sL, [Text]
bL, [Integer]
iL, [Double]
dL)
    let compressParams :: CompressParams
compressParams = CompressParams
G.defaultCompressParams
          { compressLevel :: CompressionLevel
G.compressLevel    = CompressionLevel
G.bestSpeed
          , compressStrategy :: CompressionStrategy
G.compressStrategy = CompressionStrategy
G.huffmanOnlyStrategy
          }
    ByteString
cbits <- Account Phase -> TCMT IO ByteString -> TCMT IO ByteString
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [ Phase
Bench.Serialization, Phase
Bench.Compress ] (TCMT IO ByteString -> TCMT IO ByteString)
-> TCMT IO ByteString -> TCMT IO ByteString
forall a b. (a -> b) -> a -> b
$
      ByteString -> TCMT IO ByteString
forall (m :: * -> *) a. Monad m => a -> m a
return (ByteString -> TCMT IO ByteString)
-> ByteString -> TCMT IO ByteString
forall a b. NFData a => (a -> b) -> a -> b
$!! CompressParams -> ByteString -> ByteString
G.compressWith CompressParams
compressParams ByteString
bits1
    let x :: ByteString
x = Word64 -> ByteString
forall a. Binary a => a -> ByteString
B.encode Word64
currentInterfaceVersion ByteString -> ByteString -> ByteString
`L.append` ByteString
cbits
    Encoded -> TCM Encoded
forall (m :: * -> *) a. Monad m => a -> m a
return (Encoded :: ByteString -> ByteString -> Encoded
Encoded { uncompressed :: ByteString
uncompressed = ByteString
bits1, compressed :: ByteString
compressed = ByteString
x })
  where
    l :: h RealWorld b b -> IO [b]
l h RealWorld b b
h = ((b, b) -> b) -> [(b, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
List.map (b, b) -> b
forall a b. (a, b) -> a
fst ([(b, b)] -> [b]) -> ([(b, b)] -> [(b, b)]) -> [(b, b)] -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b, b) -> (b, b) -> Ordering) -> [(b, b)] -> [(b, b)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (b -> b -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (b -> b -> Ordering)
-> ((b, b) -> b) -> (b, b) -> (b, b) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (b, b) -> b
forall a b. (a, b) -> b
snd) ([(b, b)] -> [b]) -> IO [(b, b)] -> IO [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOHashTable h b b -> IO [(b, b)]
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> IO [(k, v)]
H.toList h RealWorld b b
IOHashTable h b b
h
    benchSort :: IO c -> TCMT IO c
benchSort = Account Phase -> TCMT IO c -> TCMT IO c
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Serialization, Phase
Bench.Sort] (TCMT IO c -> TCMT IO c)
-> (IO c -> TCMT IO c) -> IO c -> TCMT IO c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO c -> TCMT IO c
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
    statistics :: String -> IORef FreshAndReuse -> TCM ()
    statistics :: VerboseKey -> IORef FreshAndReuse -> TCMT IO ()
statistics VerboseKey
kind IORef FreshAndReuse
ioref = do
      FreshAndReuse Int32
fresh
#ifdef DEBUG
                          reused
#endif
                                 <- IO FreshAndReuse -> TCMT IO FreshAndReuse
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO FreshAndReuse -> TCMT IO FreshAndReuse)
-> IO FreshAndReuse -> TCMT IO FreshAndReuse
forall a b. (a -> b) -> a -> b
$ IORef FreshAndReuse -> IO FreshAndReuse
forall a. IORef a -> IO a
readIORef IORef FreshAndReuse
ioref
      VerboseKey -> Integer -> TCMT IO ()
forall (m :: * -> *).
MonadStatistics m =>
VerboseKey -> Integer -> m ()
tickN (VerboseKey
kind VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"  (fresh)") (Integer -> TCMT IO ()) -> Integer -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int32 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
fresh
#ifdef DEBUG
      tickN (kind ++ " (reused)") $ fromIntegral reused
#endif

-- encode :: EmbPrj a => a -> TCM L.ByteString
-- encode a = do
--     fileMod <- sourceToModule
--     (x, shared, total) <- liftIO $ do
--       newD@(Dict nD sD iD dD _ _ _ _ _ stats _) <- emptyDict fileMod
--       root <- runReaderT (icode a) newD
--       nL <- l nD; sL <- l sD; iL <- l iD; dL <- l dD
--       (shared, total) <- readIORef stats
--       return (B.encode currentInterfaceVersion `L.append`
--               G.compress (B.encode (root, nL, sL, iL, dL)), shared, total)
--     verboseS "profile.sharing" 10 $ do
--       tickN "pointers (reused)" $ fromIntegral shared
--       tickN "pointers" $ fromIntegral total
--     return x
--   where
--   l h = List.map fst . List.sortBy (compare `on` snd) <$> H.toList h

-- | Decodes an uncompressed bytestring (without extra hashes or magic
-- numbers). The result depends on the include path.
--
-- Returns 'Nothing' if a decoding error is encountered.

decode :: EmbPrj a => L.ByteString -> TCM (Maybe a)
decode :: ByteString -> TCM (Maybe a)
decode ByteString
s = do
  ModuleToSource
mf   <- Lens' ModuleToSource TCState -> TCMT IO ModuleToSource
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' ModuleToSource TCState
stModuleToSource
  [AbsolutePath]
incs <- TCMT IO [AbsolutePath]
forall (m :: * -> *). HasOptions m => m [AbsolutePath]
getIncludeDirs

  -- Note that runGetState can raise errors if the input is malformed.
  -- The decoder is (intended to be) strict enough to ensure that all
  -- such errors can be caught by the handler here.

  (Maybe ModuleToSource
mf, Either TypeError a
r) <- IO (Maybe ModuleToSource, Either TypeError a)
-> TCMT IO (Maybe ModuleToSource, Either TypeError a)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe ModuleToSource, Either TypeError a)
 -> TCMT IO (Maybe ModuleToSource, Either TypeError a))
-> IO (Maybe ModuleToSource, Either TypeError a)
-> TCMT IO (Maybe ModuleToSource, Either TypeError a)
forall a b. (a -> b) -> a -> b
$ (ErrorCall -> IO (Maybe ModuleToSource, Either TypeError a))
-> IO (Maybe ModuleToSource, Either TypeError a)
-> IO (Maybe ModuleToSource, Either TypeError a)
forall e a. Exception e => (e -> IO a) -> IO a -> IO a
E.handle (\(E.ErrorCall VerboseKey
s) -> VerboseKey -> IO (Maybe ModuleToSource, Either TypeError a)
forall (m :: * -> *) a b.
Monad m =>
VerboseKey -> m (Maybe a, Either TypeError b)
noResult VerboseKey
s) (IO (Maybe ModuleToSource, Either TypeError a)
 -> IO (Maybe ModuleToSource, Either TypeError a))
-> IO (Maybe ModuleToSource, Either TypeError a)
-> IO (Maybe ModuleToSource, Either TypeError a)
forall a b. (a -> b) -> a -> b
$ do

    ((Int32
r, [Node]
nL, [VerboseKey]
sL, [Text]
bL, [Integer]
iL, [Double]
dL), ByteString
s, ByteOffset
_) <- ((Int32, [Node], [VerboseKey], [Text], [Integer], [Double]),
 ByteString, ByteOffset)
-> IO
     ((Int32, [Node], [VerboseKey], [Text], [Integer], [Double]),
      ByteString, ByteOffset)
forall (m :: * -> *) a. Monad m => a -> m a
return (((Int32, [Node], [VerboseKey], [Text], [Integer], [Double]),
  ByteString, ByteOffset)
 -> IO
      ((Int32, [Node], [VerboseKey], [Text], [Integer], [Double]),
       ByteString, ByteOffset))
-> ((Int32, [Node], [VerboseKey], [Text], [Integer], [Double]),
    ByteString, ByteOffset)
-> IO
     ((Int32, [Node], [VerboseKey], [Text], [Integer], [Double]),
      ByteString, ByteOffset)
forall a b. (a -> b) -> a -> b
$ Get (Int32, [Node], [VerboseKey], [Text], [Integer], [Double])
-> ByteString
-> ByteOffset
-> ((Int32, [Node], [VerboseKey], [Text], [Integer], [Double]),
    ByteString, ByteOffset)
forall a.
Get a -> ByteString -> ByteOffset -> (a, ByteString, ByteOffset)
runGetState Get (Int32, [Node], [VerboseKey], [Text], [Integer], [Double])
forall t. Binary t => Get t
B.get ByteString
s ByteOffset
0
    if ByteString
s ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
/= ByteString
L.empty
     then VerboseKey -> IO (Maybe ModuleToSource, Either TypeError a)
forall (m :: * -> *) a b.
Monad m =>
VerboseKey -> m (Maybe a, Either TypeError b)
noResult VerboseKey
"Garbage at end."
     else do

      St
st <- Array Int32 Node
-> Array Int32 VerboseKey
-> Array Int32 Text
-> Array Int32 Integer
-> Array Int32 Double
-> Memo
-> ModuleToSource
-> [AbsolutePath]
-> St
St ([Node] -> Array Int32 Node
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i, Num i) =>
[e] -> a i e
ar [Node]
nL) ([VerboseKey] -> Array Int32 VerboseKey
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i, Num i) =>
[e] -> a i e
ar [VerboseKey]
sL) ([Text] -> Array Int32 Text
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i, Num i) =>
[e] -> a i e
ar [Text]
bL) ([Integer] -> Array Int32 Integer
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i, Num i) =>
[e] -> a i e
ar [Integer]
iL) ([Double] -> Array Int32 Double
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i, Num i) =>
[e] -> a i e
ar [Double]
dL)
              (HashTable RealWorld (Int32, SomeTypeRep) U
 -> ModuleToSource -> [AbsolutePath] -> St)
-> IO (HashTable RealWorld (Int32, SomeTypeRep) U)
-> IO (ModuleToSource -> [AbsolutePath] -> St)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (HashTable RealWorld (Int32, SomeTypeRep) U)
-> IO (HashTable RealWorld (Int32, SomeTypeRep) U)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (HashTable RealWorld (Int32, SomeTypeRep) U)
forall (h :: * -> * -> * -> *) k v.
HashTable h =>
IO (IOHashTable h k v)
H.new
              IO (ModuleToSource -> [AbsolutePath] -> St)
-> IO ModuleToSource -> IO ([AbsolutePath] -> St)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ModuleToSource -> IO ModuleToSource
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleToSource
mf IO ([AbsolutePath] -> St) -> IO [AbsolutePath] -> IO St
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [AbsolutePath] -> IO [AbsolutePath]
forall (m :: * -> *) a. Monad m => a -> m a
return [AbsolutePath]
incs
      (Either TypeError a
r, St
st) <- StateT St IO (Either TypeError a)
-> St -> IO (Either TypeError a, St)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ExceptT TypeError (StateT St IO) a
-> StateT St IO (Either TypeError a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (Int32 -> ExceptT TypeError (StateT St IO) a
forall a. EmbPrj a => Int32 -> R a
value Int32
r)) St
st
      (Maybe ModuleToSource, Either TypeError a)
-> IO (Maybe ModuleToSource, Either TypeError a)
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleToSource -> Maybe ModuleToSource
forall a. a -> Maybe a
Just (ModuleToSource -> Maybe ModuleToSource)
-> ModuleToSource -> Maybe ModuleToSource
forall a b. (a -> b) -> a -> b
$ St -> ModuleToSource
modFile St
st, Either TypeError a
r)

  case Maybe ModuleToSource
mf of
    Maybe ModuleToSource
Nothing -> () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just ModuleToSource
mf -> Lens' ModuleToSource TCState
stModuleToSource Lens' ModuleToSource TCState -> ModuleToSource -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` ModuleToSource
mf

  case Either TypeError a
r of
    Right a
x -> do
#if __GLASGOW_HASKELL__ >= 804
      -- "Compact" the interfaces (without breaking sharing) to
      -- reduce the amount of memory that is traversed by the
      -- garbage collector.
      Account Phase -> TCM (Maybe a) -> TCM (Maybe a)
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Deserialization, Phase
Bench.Compaction] (TCM (Maybe a) -> TCM (Maybe a)) -> TCM (Maybe a) -> TCM (Maybe a)
forall a b. (a -> b) -> a -> b
$
        IO (Maybe a) -> TCM (Maybe a)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> (Compact a -> a) -> Compact a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compact a -> a
forall a. Compact a -> a
C.getCompact (Compact a -> Maybe a) -> IO (Compact a) -> IO (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> IO (Compact a)
forall a. a -> IO (Compact a)
C.compactWithSharing a
x)
#else
      return (Just x)
#endif
    Left TypeError
err -> do
      VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"import.iface" VerboseLevel
5 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Error when decoding interface file"
      -- Andreas, 2014-06-11 deactivated debug printing
      -- in order to get rid of dependency of Serialize on TCM.Pretty
      -- reportSDoc "import.iface" 5 $
      --   "Error when decoding interface file:"
      --   $+$ nest 2 (prettyTCM err)
      Maybe a -> TCM (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing

  where
  ar :: [e] -> a i e
ar [e]
l = (i, i) -> [e] -> a i e
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (i
0, [e] -> i
forall i a. Num i => [a] -> i
List.genericLength [e]
l i -> i -> i
forall a. Num a => a -> a -> a
- i
1) [e]
l

  noResult :: VerboseKey -> m (Maybe a, Either TypeError b)
noResult VerboseKey
s = (Maybe a, Either TypeError b) -> m (Maybe a, Either TypeError b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a
forall a. Maybe a
Nothing, TypeError -> Either TypeError b
forall a b. a -> Either a b
Left (TypeError -> Either TypeError b)
-> TypeError -> Either TypeError b
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError VerboseKey
s)

encodeInterface :: Interface -> TCM Encoded
encodeInterface :: Interface -> TCM Encoded
encodeInterface Interface
i = do
  Encoded
r <- Interface -> TCM Encoded
forall a. EmbPrj a => a -> TCM Encoded
encode Interface
i
  Encoded -> TCM Encoded
forall (m :: * -> *) a. Monad m => a -> m a
return (Encoded
r { compressed :: ByteString
compressed = ByteString -> ByteString -> ByteString
L.append ByteString
hashes (Encoded -> ByteString
compressed Encoded
r) })
  where
    hashes :: L.ByteString
    hashes :: ByteString
hashes = Put -> ByteString
B.runPut (Put -> ByteString) -> Put -> ByteString
forall a b. (a -> b) -> a -> b
$ Word64 -> Put
forall t. Binary t => t -> Put
B.put (Interface -> Word64
iSourceHash Interface
i) Put -> Put -> Put
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Word64 -> Put
forall t. Binary t => t -> Put
B.put (Interface -> Word64
iFullHash Interface
i)

-- | Encodes an interface. To ensure relocatability file paths in
-- positions are replaced with module names.
--
-- An uncompressed bytestring corresponding to the encoded interface
-- is returned.

encodeFile :: FilePath -> Interface -> TCM L.ByteString
encodeFile :: VerboseKey -> Interface -> TCMT IO ByteString
encodeFile VerboseKey
f Interface
i = do
  Encoded
r <- Interface -> TCM Encoded
encodeInterface Interface
i
  IO () -> TCMT IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCMT IO ()) -> IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Bool -> VerboseKey -> IO ()
createDirectoryIfMissing Bool
True (VerboseKey -> VerboseKey
takeDirectory VerboseKey
f)
  IO () -> TCMT IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCMT IO ()) -> IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> ByteString -> IO ()
L.writeFile VerboseKey
f (Encoded -> ByteString
compressed Encoded
r)
  ByteString -> TCMT IO ByteString
forall (m :: * -> *) a. Monad m => a -> m a
return (Encoded -> ByteString
uncompressed Encoded
r)

-- | Decodes an interface. The result depends on the include path.
--
-- Returns 'Nothing' if the file does not start with the right magic
-- number or some other decoding error is encountered.

decodeInterface :: L.ByteString -> TCM (Maybe Interface)
decodeInterface :: ByteString -> TCM (Maybe Interface)
decodeInterface ByteString
s = do

  -- Note that runGetState and the decompression code below can raise
  -- errors if the input is malformed. The decoder is (intended to be)
  -- strict enough to ensure that all such errors can be caught by the
  -- handler here or the one in decode.

  Either VerboseKey ByteString
s <- IO (Either VerboseKey ByteString)
-> TCMT IO (Either VerboseKey ByteString)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either VerboseKey ByteString)
 -> TCMT IO (Either VerboseKey ByteString))
-> IO (Either VerboseKey ByteString)
-> TCMT IO (Either VerboseKey ByteString)
forall a b. (a -> b) -> a -> b
$
       (ErrorCall -> IO (Either VerboseKey ByteString))
-> IO (Either VerboseKey ByteString)
-> IO (Either VerboseKey ByteString)
forall e a. Exception e => (e -> IO a) -> IO a -> IO a
E.handle (\(E.ErrorCall VerboseKey
s) -> Either VerboseKey ByteString -> IO (Either VerboseKey ByteString)
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseKey -> Either VerboseKey ByteString
forall a b. a -> Either a b
Left VerboseKey
s)) (IO (Either VerboseKey ByteString)
 -> IO (Either VerboseKey ByteString))
-> IO (Either VerboseKey ByteString)
-> IO (Either VerboseKey ByteString)
forall a b. (a -> b) -> a -> b
$
       Either VerboseKey ByteString -> IO (Either VerboseKey ByteString)
forall a. a -> IO a
E.evaluate (Either VerboseKey ByteString -> IO (Either VerboseKey ByteString))
-> Either VerboseKey ByteString
-> IO (Either VerboseKey ByteString)
forall a b. (a -> b) -> a -> b
$
       let (Word64
ver, ByteString
s', ByteOffset
_) = Get Word64
-> ByteString -> ByteOffset -> (Word64, ByteString, ByteOffset)
forall a.
Get a -> ByteString -> ByteOffset -> (a, ByteString, ByteOffset)
runGetState Get Word64
forall t. Binary t => Get t
B.get (ByteOffset -> ByteString -> ByteString
L.drop ByteOffset
16 ByteString
s) ByteOffset
0 in
       if Word64
ver Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word64
currentInterfaceVersion
       then VerboseKey -> Either VerboseKey ByteString
forall a b. a -> Either a b
Left VerboseKey
"Wrong interface version."
       else ByteString -> Either VerboseKey ByteString
forall a b. b -> Either a b
Right (ByteString -> Either VerboseKey ByteString)
-> ByteString -> Either VerboseKey ByteString
forall a b. (a -> b) -> a -> b
$
            Builder -> ByteString
L.toLazyByteString (Builder -> ByteString) -> Builder -> ByteString
forall a b. (a -> b) -> a -> b
$
            (ByteString -> Builder -> Builder)
-> (ByteString -> Builder)
-> (DecompressError -> Builder)
-> (forall s. DecompressStream (ST s))
-> ByteString
-> Builder
forall a.
(ByteString -> a -> a)
-> (ByteString -> a)
-> (DecompressError -> a)
-> (forall s. DecompressStream (ST s))
-> ByteString
-> a
Z.foldDecompressStreamWithInput
              (\ByteString
s -> (ByteString -> Builder
L.byteString ByteString
s Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>))
              (\ByteString
s -> if ByteString -> Bool
L.null ByteString
s
                     then Builder
forall a. Monoid a => a
mempty
                     else VerboseKey -> Builder
forall a. HasCallStack => VerboseKey -> a
error VerboseKey
"Garbage at end.")
              (\DecompressError
err -> VerboseKey -> Builder
forall a. HasCallStack => VerboseKey -> a
error (DecompressError -> VerboseKey
forall a. Show a => a -> VerboseKey
show DecompressError
err))
              (Format -> DecompressParams -> DecompressStream (ST s)
forall s. Format -> DecompressParams -> DecompressStream (ST s)
Z.decompressST Format
Z.gzipFormat DecompressParams
Z.defaultDecompressParams)
              ByteString
s'

  case Either VerboseKey ByteString
s of
    Right ByteString
s  -> ByteString -> TCM (Maybe Interface)
forall a. EmbPrj a => ByteString -> TCM (Maybe a)
decode ByteString
s
    Left VerboseKey
err -> do
      VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"import.iface" VerboseLevel
5 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        VerboseKey
"Error when decoding interface file: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
err
      Maybe Interface -> TCM (Maybe Interface)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Interface
forall a. Maybe a
Nothing

decodeHashes :: L.ByteString -> Maybe (Hash, Hash)
decodeHashes :: ByteString -> Maybe (Word64, Word64)
decodeHashes ByteString
s
  | ByteString -> ByteOffset
L.length ByteString
s ByteOffset -> ByteOffset -> Bool
forall a. Ord a => a -> a -> Bool
< ByteOffset
16 = Maybe (Word64, Word64)
forall a. Maybe a
Nothing
  | Bool
otherwise       = (Word64, Word64) -> Maybe (Word64, Word64)
forall a. a -> Maybe a
Just ((Word64, Word64) -> Maybe (Word64, Word64))
-> (Word64, Word64) -> Maybe (Word64, Word64)
forall a b. (a -> b) -> a -> b
$ Get (Word64, Word64) -> ByteString -> (Word64, Word64)
forall a. Get a -> ByteString -> a
B.runGet Get (Word64, Word64)
getH (ByteString -> (Word64, Word64)) -> ByteString -> (Word64, Word64)
forall a b. (a -> b) -> a -> b
$ ByteOffset -> ByteString -> ByteString
L.take ByteOffset
16 ByteString
s
  where getH :: Get (Word64, Word64)
getH = (,) (Word64 -> Word64 -> (Word64, Word64))
-> Get Word64 -> Get (Word64 -> (Word64, Word64))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get Word64
forall t. Binary t => Get t
B.get Get (Word64 -> (Word64, Word64))
-> Get Word64 -> Get (Word64, Word64)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get Word64
forall t. Binary t => Get t
B.get

decodeFile :: FilePath -> TCM (Maybe Interface)
decodeFile :: VerboseKey -> TCM (Maybe Interface)
decodeFile VerboseKey
f = ByteString -> TCM (Maybe Interface)
decodeInterface (ByteString -> TCM (Maybe Interface))
-> TCMT IO ByteString -> TCM (Maybe Interface)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO ByteString -> TCMT IO ByteString
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (VerboseKey -> IO ByteString
L.readFile VerboseKey
f)

-- | Store a 'SourceToModule' (map from 'AbsolutePath' to 'TopLevelModuleName')
--   as map from 'AbsolutePath' to 'Int32', in order to directly get the identifiers
--   from absolute pathes rather than going through top level module names.
icodeFileMod
  :: SourceToModule
     -- ^ Maps file names to the corresponding module names.
     --   Must contain a mapping for every file name that is later encountered.
  -> S ()
icodeFileMod :: SourceToModule -> S ()
icodeFileMod SourceToModule
fileMod = do
  HashTable RealWorld AbsolutePath Int32
hmap <- (Dict -> HashTable RealWorld AbsolutePath Int32)
-> ReaderT Dict IO (HashTable RealWorld AbsolutePath Int32)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable RealWorld AbsolutePath Int32
Dict -> HashTable AbsolutePath Int32
absPathD
  [(AbsolutePath, TopLevelModuleName)]
-> ((AbsolutePath, TopLevelModuleName) -> S ()) -> S ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (SourceToModule -> [(AbsolutePath, TopLevelModuleName)]
forall k a. Map k a -> [(k, a)]
Map.toList SourceToModule
fileMod) (((AbsolutePath, TopLevelModuleName) -> S ()) -> S ())
-> ((AbsolutePath, TopLevelModuleName) -> S ()) -> S ()
forall a b. (a -> b) -> a -> b
$ \ (AbsolutePath
absolutePath, TopLevelModuleName
topLevelModuleName) -> do
    Int32
i <- TopLevelModuleName -> ReaderT Dict IO Int32
forall a. EmbPrj a => a -> ReaderT Dict IO Int32
icod_ TopLevelModuleName
topLevelModuleName
    IO () -> S ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> S ()) -> IO () -> S ()
forall a b. (a -> b) -> a -> b
$ HashTable AbsolutePath Int32 -> AbsolutePath -> Int32 -> IO ()
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> k -> v -> IO ()
H.insert HashTable RealWorld AbsolutePath Int32
HashTable AbsolutePath Int32
hmap AbsolutePath
absolutePath Int32
i