{-# 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 Prelude hiding ( null )

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.Except
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.Reader
import Control.Monad.State.Strict

import Data.Array.IArray
import Data.Word
import Data.ByteString.Lazy    ( ByteString )
import Data.ByteString.Builder ( byteString, toLazyByteString )
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
#if !(MIN_VERSION_base(4,11,0))
import Data.Semigroup((<>))
#endif

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 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.FileName (canonicalizeAbsolutePath)
import Agda.Utils.Hash
import Agda.Utils.IORef
import Agda.Utils.Null

import Agda.Utils.Impossible

-- 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
20220211 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 :: ByteString
    -- ^ The uncompressed bytestring, without hashes and the interface
    -- version.
  , Encoded -> ByteString
compressed :: 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
ltD HashTable Text Int32
stD 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
ltC IORef FreshAndReuse
stC 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) =>
h RealWorld b b -> IO [b]
l HashTable RealWorld Node Int32
HashTable Node Int32
nD
    [Text]
stL <- 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) =>
h RealWorld b b -> IO [b]
l HashTable RealWorld Text Int32
HashTable Text Int32
stD
    [VerboseKey]
ltL <- 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) =>
h RealWorld b b -> IO [b]
l HashTable RealWorld VerboseKey Int32
HashTable VerboseKey Int32
ltD
    [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) =>
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) =>
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) =>
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
"Lazy Text"   IORef FreshAndReuse
ltC
      VerboseKey -> IORef FreshAndReuse -> TCMT IO ()
statistics VerboseKey
"Strict Text" IORef FreshAndReuse
stC
      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 <- (Integer -> Integer -> Integer)
-> [(VerboseKey, Integer)] -> Map VerboseKey Integer
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Integer -> Integer -> Integer
forall a. HasCallStack => a
__IMPOSSIBLE__ ([(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
$ (Integer -> Integer -> Integer)
-> Map VerboseKey Integer
-> Map VerboseKey Integer
-> Map VerboseKey Integer
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) Map VerboseKey Integer
stats
    -- Encode hashmaps and root, and compress.
    ByteString
bits1 <- Account (BenchPhase (TCMT IO))
-> TCMT IO ByteString -> TCMT IO ByteString
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [ BenchPhase (TCMT IO)
Phase
Bench.Serialization, BenchPhase (TCMT IO)
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], [Text], [Integer], [Double])
-> ByteString
forall a. Binary a => a -> ByteString
B.encode (Int32
root, [Node]
nL, [VerboseKey]
ltL, [Text]
stL, [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 (BenchPhase (TCMT IO))
-> TCMT IO ByteString -> TCMT IO ByteString
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [ BenchPhase (TCMT IO)
Phase
Bench.Serialization, BenchPhase (TCMT IO)
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
forall a. Semigroup a => a -> a -> a
<> 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 (BenchPhase (TCMT IO)) -> TCMT IO c -> TCMT IO c
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Serialization, BenchPhase (TCMT IO)
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 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 <>
--               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 => 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]
ltL, [Text]
stL, [Text]
bL, [Integer]
iL, [Double]
dL), ByteString
s, ByteOffset
_) <- ((Int32, [Node], [VerboseKey], [Text], [Text], [Integer],
  [Double]),
 ByteString, ByteOffset)
-> IO
     ((Int32, [Node], [VerboseKey], [Text], [Text], [Integer],
       [Double]),
      ByteString, ByteOffset)
forall (m :: * -> *) a. Monad m => a -> m a
return (((Int32, [Node], [VerboseKey], [Text], [Text], [Integer],
   [Double]),
  ByteString, ByteOffset)
 -> IO
      ((Int32, [Node], [VerboseKey], [Text], [Text], [Integer],
        [Double]),
       ByteString, ByteOffset))
-> ((Int32, [Node], [VerboseKey], [Text], [Text], [Integer],
     [Double]),
    ByteString, ByteOffset)
-> IO
     ((Int32, [Node], [VerboseKey], [Text], [Text], [Integer],
       [Double]),
      ByteString, ByteOffset)
forall a b. (a -> b) -> a -> b
$ Get
  (Int32, [Node], [VerboseKey], [Text], [Text], [Integer], [Double])
-> ByteString
-> ByteOffset
-> ((Int32, [Node], [VerboseKey], [Text], [Text], [Integer],
     [Double]),
    ByteString, ByteOffset)
forall a.
Get a -> ByteString -> ByteOffset -> (a, ByteString, ByteOffset)
runGetState Get
  (Int32, [Node], [VerboseKey], [Text], [Text], [Integer], [Double])
forall t. Binary t => Get t
B.get ByteString
s ByteOffset
0
    if Bool -> Bool
not (ByteString -> Bool
forall a. Null a => a -> Bool
null ByteString
s)
     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 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]
ltL) ([Text] -> Array Int32 Text
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i, Num i) =>
[e] -> a i e
ar [Text]
stL) ([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)

  Maybe ModuleToSource
-> (ModuleToSource -> TCMT IO ()) -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Maybe ModuleToSource
mf (Lens' ModuleToSource TCState -> ModuleToSource -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens Lens' ModuleToSource TCState
stModuleToSource)

  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 (BenchPhase (TCMT IO)) -> TCM (Maybe a) -> TCM (Maybe a)
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Deserialization, BenchPhase (TCMT IO)
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
hashes ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> Encoded -> ByteString
compressed Encoded
r }
  where
    hashes :: 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 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 :: 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
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
byteString ByteString
s Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>))
              (\ByteString
s -> if ByteString -> Bool
forall a. Null a => a -> Bool
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 :: 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
    -- Andreas, 2020-08-11, issue #4828.
    -- Expand symlinks before storing in the dictonary.
    AbsolutePath
absolutePath <- IO AbsolutePath -> ReaderT Dict IO AbsolutePath
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO AbsolutePath -> ReaderT Dict IO AbsolutePath)
-> IO AbsolutePath -> ReaderT Dict IO AbsolutePath
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> IO AbsolutePath
canonicalizeAbsolutePath AbsolutePath
absolutePath
    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