    {-# 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 :: forall a. EmbPrj a => a -> TCM Encoded
    encode a
    a = do
        Bool
    collectStats <- String -> Int -> TCMT IO Bool
    forall (m :: * -> *). MonadDebug m => String -> Int -> m Bool
    hasVerbosity String
    "profile.serialize" Int
    20
        SourceToModule
    fileMod <- TCM SourceToModule
    sourceToModule
        newD :: Dict
    newD@(Dict HashTable Node Int32
    nD HashTable String 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 String Int
    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
        [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, Eq b) =>
    h RealWorld b b -> IO [b]
    l HashTable RealWorld Text Int32
    HashTable Text Int32
    stD
        [String]
    ltL <- IO [String] -> TCMT IO [String]
    forall {c}. IO c -> TCMT IO c
    benchSort (IO [String] -> TCMT IO [String])
    -> IO [String] -> TCMT IO [String]
    forall a b. (a -> b) -> a -> b
    $ HashTable RealWorld String Int32 -> IO [String]
    forall {b} {h :: * -> * -> * -> *} {b}.
    (Ord b, HashTable h, Hashable b, Eq b) =>
    h RealWorld b b -> IO [b]
    l HashTable RealWorld String Int32
    HashTable String 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, 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.
        String -> Int -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
    verboseS String
    "profile.sharing" Int
    10 (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
          String -> IORef FreshAndReuse -> TCMT IO ()
    statistics String
    "pointers" IORef FreshAndReuse
    tC
        String -> Int -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
    verboseS String
    "profile.serialize" Int
    10 (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
          String -> IORef FreshAndReuse -> TCMT IO ()
    statistics String
    "Integer"     IORef FreshAndReuse
    iC
          String -> IORef FreshAndReuse -> TCMT IO ()
    statistics String
    "Lazy Text"   IORef FreshAndReuse
    ltC
          String -> IORef FreshAndReuse -> TCMT IO ()
    statistics String
    "Strict Text" IORef FreshAndReuse
    stC
          String -> IORef FreshAndReuse -> TCMT IO ()
    statistics String
    "Text"        IORef FreshAndReuse
    bC
          String -> IORef FreshAndReuse -> TCMT IO ()
    statistics String
    "Double"      IORef FreshAndReuse
    dC
          String -> IORef FreshAndReuse -> TCMT IO ()
    statistics String
    "Node"        IORef FreshAndReuse
    nC
          String -> IORef FreshAndReuse -> TCMT IO ()
    statistics String
    "Shared Term" IORef FreshAndReuse
    tC
          String -> IORef FreshAndReuse -> TCMT IO ()
    statistics String
    "A.QName"     IORef FreshAndReuse
    qnameC
          String -> IORef FreshAndReuse -> TCMT IO ()
    statistics String
    "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 String Integer
    stats <- (Integer -> Integer -> Integer)
    -> [(String, Integer)] -> Map String Integer
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith Integer -> Integer -> Integer
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([(String, Integer)] -> Map String Integer)
    -> ([(String, Int)] -> [(String, Integer)])
    -> [(String, Int)]
    -> Map String Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((String, Int) -> (String, Integer))
    -> [(String, Int)] -> [(String, Integer)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Int -> Integer) -> (String, Int) -> (String, Integer)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger) ([(String, Int)] -> Map String Integer)
    -> TCMT IO [(String, Int)] -> TCMT IO (Map String Integer)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
            IO [(String, Int)] -> TCMT IO [(String, Int)]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [(String, Int)] -> TCMT IO [(String, Int)])
    -> IO [(String, Int)] -> TCMT IO [(String, Int)]
    forall a b. (a -> b) -> a -> b
    $ HashTable String Int -> IO [(String, Int)]
    forall (h :: * -> * -> * -> *) k v.
    (HashTable h, Eq k, Hashable k) =>
    IOHashTable h k v -> IO [(k, v)]
    H.toList HashTable String Int
    stats
          (Map String Integer -> Map String Integer) -> TCMT IO ()
    modifyStatistics ((Map String Integer -> Map String Integer) -> TCMT IO ())
    -> (Map String Integer -> Map String Integer) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Integer -> Integer)
    -> Map String Integer -> Map String Integer -> Map String 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 String 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], [String], [Text], [Text], [Integer], [Double])
    -> ByteString
    forall a. Binary a => a -> ByteString
    B.encode (Int32
    root, [Node]
    nL, [String]
    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 :: String -> IORef FreshAndReuse -> TCMT IO ()
    statistics String
    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
          String -> Integer -> TCMT IO ()
    forall (m :: * -> *).
    MonadStatistics m =>
    String -> Integer -> m ()
    tickN (String
    kind String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "  (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 :: forall a. EmbPrj a => 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 String
    s) -> String -> IO (Maybe ModuleToSource, Either TypeError a)
    forall {m :: * -> *} {a} {b}.
    Monad m =>
    String -> m (Maybe a, Either TypeError b)
    noResult String
    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, [String]
    ltL, [Text]
    stL, [Text]
    bL, [Integer]
    iL, [Double]
    dL), ByteString
    s, Int64
    _) <- ((Int32, [Node], [String], [Text], [Text], [Integer], [Double]),
     ByteString, Int64)
    -> IO
         ((Int32, [Node], [String], [Text], [Text], [Integer], [Double]),
          ByteString, Int64)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (((Int32, [Node], [String], [Text], [Text], [Integer], [Double]),
      ByteString, Int64)
     -> IO
          ((Int32, [Node], [String], [Text], [Text], [Integer], [Double]),
           ByteString, Int64))
    -> ((Int32, [Node], [String], [Text], [Text], [Integer], [Double]),
        ByteString, Int64)
    -> IO
         ((Int32, [Node], [String], [Text], [Text], [Integer], [Double]),
          ByteString, Int64)
    forall a b. (a -> b) -> a -> b
    $ Get (Int32, [Node], [String], [Text], [Text], [Integer], [Double])
    -> ByteString
    -> Int64
    -> ((Int32, [Node], [String], [Text], [Text], [Integer], [Double]),
        ByteString, Int64)
    forall a. Get a -> ByteString -> Int64 -> (a, ByteString, Int64)
    runGetState Get (Int32, [Node], [String], [Text], [Text], [Integer], [Double])
    forall t. Binary t => Get t
    B.get ByteString
    s Int64
    0
        if Bool -> Bool
    not (ByteString -> Bool
    forall a. Null a => a -> Bool
    null ByteString
    s)
         then String -> IO (Maybe ModuleToSource, Either TypeError a)
    forall {m :: * -> *} {a} {b}.
    Monad m =>
    String -> m (Maybe a, Either TypeError b)
    noResult String
    "Garbage at end."
         else do

          St
    st <- Array Int32 Node
    -> Array Int32 String
    -> 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) ([String] -> Array Int32 String
    forall {a :: * -> * -> *} {e} {i}.
    (IArray a e, Ix i, Num i) =>
    [e] -> a i e
    ar [String]
    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
          String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "import.iface" Int
    5 (String -> TCMT IO ()) -> String -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "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 :: String -> m (Maybe a, Either TypeError b)
    noResult String
    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
    $ String -> TypeError
    GenericError String
    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 :: String -> Interface -> TCMT IO ByteString
    encodeFile String
    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 -> String -> IO ()
    createDirectoryIfMissing Bool
    True (String -> String
    takeDirectory String
    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
    $ String -> ByteString -> IO ()
    L.writeFile String
    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 String ByteString
    s <- IO (Either String ByteString) -> TCMT IO (Either String ByteString)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Either String ByteString)
     -> TCMT IO (Either String ByteString))
    -> IO (Either String ByteString)
    -> TCMT IO (Either String ByteString)
    forall a b. (a -> b) -> a -> b
    $
           (ErrorCall -> IO (Either String ByteString))
    -> IO (Either String ByteString) -> IO (Either String ByteString)
    forall e a. Exception e => (e -> IO a) -> IO a -> IO a
    E.handle (\(E.ErrorCall String
    s) -> Either String ByteString -> IO (Either String ByteString)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Either String ByteString
    forall a b. a -> Either a b
    Left String
    s)) (IO (Either String ByteString) -> IO (Either String ByteString))
    -> IO (Either String ByteString) -> IO (Either String ByteString)
    forall a b. (a -> b) -> a -> b
    $
           Either String ByteString -> IO (Either String ByteString)
    forall a. a -> IO a
    E.evaluate (Either String ByteString -> IO (Either String ByteString))
    -> Either String ByteString -> IO (Either String ByteString)
    forall a b. (a -> b) -> a -> b
    $
           let (Word64
    ver, ByteString
    s', Int64
    _) = Get Word64 -> ByteString -> Int64 -> (Word64, ByteString, Int64)
    forall a. Get a -> ByteString -> Int64 -> (a, ByteString, Int64)
    runGetState Get Word64
    forall t. Binary t => Get t
    B.get (Int64 -> ByteString -> ByteString
    L.drop Int64
    16 ByteString
    s) Int64
    0 in
           if Word64
    ver Word64 -> Word64 -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Word64
    currentInterfaceVersion
           then String -> Either String ByteString
    forall a b. a -> Either a b
    Left String
    "Wrong interface version."
           else ByteString -> Either String ByteString
    forall a b. b -> Either a b
    Right (ByteString -> Either String ByteString)
    -> ByteString -> Either String 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 String -> Builder
    forall a. HasCallStack => String -> a
    error String
    "Garbage at end.")
                  (\DecompressError
    err -> String -> Builder
    forall a. HasCallStack => String -> a
    error (DecompressError -> String
    forall a. Show a => a -> String
    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 String ByteString
    s of
        Right ByteString
    s  -> ByteString -> TCM (Maybe Interface)
    forall a. EmbPrj a => ByteString -> TCM (Maybe a)
    decode ByteString
    s
        Left String
    err -> do
          String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "import.iface" Int
    5 (String -> TCMT IO ()) -> String -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
            String
    "Error when decoding interface file: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    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 -> Int64
    L.length ByteString
    s Int64 -> Int64 -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int64
    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
    $ Int64 -> ByteString -> ByteString
    L.take Int64
    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 :: String -> TCM (Maybe Interface)
    decodeFile String
    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 (String -> IO ByteString
    L.readFile String
    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