    {-# LANGUAGE CPP #-}
    {-# LANGUAGE NondecreasingIndentation #-}

    -- 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 Control.Monad.ST.Trans

    import Data.Array.IArray
    import Data.Array.IO
    import Data.Word
    import Data.Word (Word32)
    import Data.ByteString.Lazy    ( ByteString )
    import Data.ByteString.Builder ( byteString, toLazyByteString )
    import qualified Data.ByteString.Lazy as L
    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 (on)

    import qualified Codec.Compression.GZip as G
    import qualified Codec.Compression.Zlib.Internal as Z

    import GHC.Compact as C

    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 qualified Agda.Utils.HashTable as H
    import Agda.Utils.IORef
    import Agda.Utils.Null
    import qualified Agda.Utils.ProfileOptions as Profile

    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
    20250703 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
        collectStats <- ProfileOption -> TCMT IO Bool
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
    hasProfileOption ProfileOption
    Profile.Serialize
        newD@(Dict nD ltD stD bD iD dD
          _nameD
          _qnameD
          nC ltC stC bC iC dC tC
          nameC
          qnameC
          stats _) <- liftIO $ emptyDict collectStats
        root <- liftIO $ (`runReaderT` newD) $ icode a
        nL  <- benchSort $ l nD
        stL <- benchSort $ l stD
        ltL <- benchSort $ l ltD
        bL  <- benchSort $ l bD
        iL  <- benchSort $ l iD
        dL  <- benchSort $ l dD
        -- Record reuse statistics.
        whenProfile Profile.Sharing $ do
          statistics "pointers" tC
        whenProfile Profile.Serialize $ do
          statistics "Integer"     iC
          statistics "Lazy Text"   ltC
          statistics "Strict Text" stC
          statistics "Text"        bC
          statistics "Double"      dC
          statistics "Node"        nC
          statistics "Shared Term" tC
          statistics "A.QName"     qnameC
          statistics "A.Name"      nameC
        when collectStats $ do
          stats <- Map.fromListWith __IMPOSSIBLE__ . map (second toInteger) <$> do
            liftIO $ List.sort <$> H.toList stats
          modifyStatistics $ Map.unionWith (+) stats
        -- Encode hashmaps and root, and compress.
        bits1 <- Bench.billTo [ Bench.Serialization, Bench.BinaryEncode ] $
          return $!! B.encode (root, nL, ltL, stL, bL, iL, dL)
        let compressParams = CompressParams
    G.defaultCompressParams
              { G.compressLevel    = G.bestSpeed
              , G.compressStrategy = G.huffmanOnlyStrategy
              }
        cbits <- Bench.billTo [ Bench.Serialization, Bench.Compress ] $
          return $!! G.compressWith compressParams bits1
        let x = Word64 -> ByteString
    forall a. Binary a => a -> ByteString
    B.encode Word64
    currentInterfaceVersion ByteString -> ByteString -> ByteString
    forall a. Semigroup a => a -> a -> a
    <> ByteString
    cbits
        return (Encoded { uncompressed = bits1, compressed = x })
      where
        l :: HashTable b b -> IO [b]
    l HashTable 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
    <$> HashTable b b -> IO [(b, b)]
    forall k v. (Eq k, Hashable k) => HashTable k v -> IO [(k, v)]
    H.toList HashTable 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 a. IO a -> TCMT IO a
    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 fresh
    #ifdef DEBUG_SERIALISATION
                              reused
    #endif
                                     <- IO FreshAndReuse -> TCMT IO FreshAndReuse
    forall a. IO a -> TCMT IO a
    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
          tickN (kind ++ "  (fresh)") $ fromIntegral fresh
    #ifdef DEBUG_SERIALISATION
          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)
    --     whenProfile Profile.Sharing $ 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

    newtype ListLike a = ListLike { forall a. ListLike a -> Array Word32 a
    unListLike :: Array Word32 a }

    instance B.Binary a => B.Binary (ListLike a) where
      put :: ListLike a -> Put
    put = ListLike a -> Put
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- Will never serialise this
      get :: Get (ListLike a)
    get = (Array Word32 a -> ListLike a)
    -> Get (Array Word32 a) -> Get (ListLike a)
    forall a b. (a -> b) -> Get a -> Get b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Array Word32 a -> ListLike a
    forall a. Array Word32 a -> ListLike a
    ListLike (Get (Array Word32 a) -> Get (ListLike a))
    -> Get (Array Word32 a) -> Get (ListLike a)
    forall a b. (a -> b) -> a -> b
    $ (forall s. STT s Get (STArray s Word32 a)) -> Get (Array Word32 a)
    forall (m :: * -> *) i e.
    Monad m =>
    (forall s. STT s m (STArray s i e)) -> m (Array i e)
    runSTArray ((forall s. STT s Get (STArray s Word32 a))
     -> Get (Array Word32 a))
    -> (forall s. STT s Get (STArray s Word32 a))
    -> Get (Array Word32 a)
    forall a b. (a -> b) -> a -> b
    $ do
        n <- Get Int -> STT s Get Int
    forall (m :: * -> *) a. Monad m => m a -> STT s m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Get Int
    forall t. Binary t => Get t
    B.get :: B.Get Int)
        -- Andreas, 2024-10-15: If n is zero, create an empty array.
        -- Since our indices are Word32, we need to represent it as [1..0] instead of the usual [0..-1].
        if n <= 0 then (newArray_ (1,0) :: STT s B.Get (STArray s Word32 a)) else do

        arr <- newArray_ (0, fromIntegral n - 1) :: STT s B.Get (STArray s Word32 a)

        -- We'd like to use 'for_ [0..n-1]' here, but unfortunately GHC doesn't unfold
        -- the list construction and so performs worse than the hand-written version.
        let
          getMany Int
    i = if Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    n then () -> STT s Get ()
    forall a. a -> STT s Get a
    forall (m :: * -> *) a. Monad m => a -> m a
    return () else do
            x <- Get a -> STT s Get a
    forall (m :: * -> *) a. Monad m => m a -> STT s m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift Get a
    forall t. Binary t => Get t
    B.get
            unsafeWriteSTArray arr i x
            getMany (i + 1)
        () <- getMany 0

        return arr

    -- | 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
      mf   <- Lens' TCState ModuleToSource -> TCMT IO ModuleToSource
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (ModuleToSource -> f ModuleToSource) -> TCState -> f TCState
    Lens' TCState ModuleToSource
    stModuleToSource
      incs <- 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.

      res <- liftIO $ E.handle (\(E.ErrorCall String
    s) -> Either String (ModuleToSource, a)
    -> IO (Either String (ModuleToSource, a))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Either String (ModuleToSource, a)
     -> IO (Either String (ModuleToSource, a)))
    -> Either String (ModuleToSource, a)
    -> IO (Either String (ModuleToSource, a))
    forall a b. (a -> b) -> a -> b
    $ String -> Either String (ModuleToSource, a)
    forall a b. a -> Either a b
    Left String
    s) $ do
        ((r, nL, ltL, stL, bL, iL, dL), s, _) <- return $ runGetState B.get s 0
        let ar = ListLike a -> Array Word32 a
    forall a. ListLike a -> Array Word32 a
    unListLike
        when (not (null s)) $ E.throwIO $ E.ErrorCall "Garbage at end."
        let nL' = ListLike [Word32] -> Array Word32 [Word32]
    forall a. ListLike a -> Array Word32 a
    ar ListLike [Word32]
    nL
        st <- St nL' (ar ltL) (ar stL) (ar bL) (ar iL) (ar dL)
                <$> liftIO (newArray (bounds nL') MEEmpty)
                <*> return mf <*> return incs
        (r, st) <- runStateT (value r) st
        let !mf = St -> ModuleToSource
    modFile St
    st
        return $ Right (mf, r)

      case res of
        Left String
    s -> 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
    s
          Maybe a -> TCMT IO (Maybe a)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe a
    forall a. Maybe a
    Nothing

        Right (ModuleToSource
    mf, a
    x) -> do
          Lens' TCState ModuleToSource -> ModuleToSource -> TCMT IO ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> a -> m ()
    setTCLens (ModuleToSource -> f ModuleToSource) -> TCState -> f TCState
    Lens' TCState ModuleToSource
    stModuleToSource ModuleToSource
    mf
          -- "Compact" the interfaces (without breaking sharing) to
          -- reduce the amount of memory that is traversed by the
          -- garbage collector.
          Account (BenchPhase (TCMT IO))
    -> TCMT IO (Maybe a) -> TCMT IO (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] (TCMT IO (Maybe a) -> TCMT IO (Maybe a))
    -> TCMT IO (Maybe a) -> TCMT IO (Maybe a)
    forall a b. (a -> b) -> a -> b
    $
            IO (Maybe a) -> TCMT IO (Maybe a)
    forall a. IO a -> TCMT IO 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)

    encodeInterface :: Interface -> TCM Encoded
    encodeInterface :: Interface -> TCM Encoded
    encodeInterface Interface
    i = do
      r <- Interface -> TCM Encoded
    forall a. EmbPrj a => a -> TCM Encoded
    encode Interface
    i
      return r{ compressed = hashes <> compressed 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 a b. PutM a -> PutM b -> PutM b
    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
      r <- Interface -> TCM Encoded
    encodeInterface Interface
    i
      liftIO $ createDirectoryIfMissing True (takeDirectory f)
      liftIO $ L.writeFile f (compressed r)
      return (uncompressed 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.

      s <- IO (Either String ByteString) -> TCMT IO (Either String ByteString)
    forall a. IO a -> TCMT IO a
    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 a. a -> IO a
    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 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 a. a -> TCMT IO a
    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 a b. Get (a -> b) -> Get a -> Get b
    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 a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IO ByteString
    L.readFile String
    f)