{-# 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.Foldable (traverse_)
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.Interaction.Options.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
20250801 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 <- liftIO $ emptyDict collectStats
    root     <- liftIO $ (`runReaderT` newD) $ icode a
    nodeL    <- benchSort $ l (nodeD newD)
    stringL  <- benchSort $ l (stringD newD)
    lTextL   <- benchSort $ l (lTextD newD)
    sTextL   <- benchSort $ l (sTextD newD)
    integerL <- benchSort $ l (integerD newD)
    varSetL <- benchSort $ l (varSetD newD)
    doubleL  <- benchSort $ l (doubleD newD)

    -- Record reuse statistics.
    whenProfile Profile.Sharing $ do
      statistics "pointers" (termC newD)
    whenProfile Profile.Serialize $ do
      statistics "Integer"     (integerC newD)
      statistics "VarSet"      (varSetC newD)
      statistics "Lazy Text"   (lTextC newD)
      statistics "Strict Text" (sTextC newD)
      statistics "String"      (stringC newD)
      statistics "Double"      (doubleC newD)
      statistics "Node"        (nodeC newD)
      statistics "Shared Term" (termC newD)
      statistics "A.QName"     (qnameC newD)
      statistics "A.Name"      (nameC newD)
    when collectStats $ do
      stats <- map (second fromIntegral) <$> do
        liftIO $ List.sort <$> H.toList (stats newD)
      traverse_ (uncurry tickN) stats
    -- Encode hashmaps and root, and compress.
    bits1 <- Bench.billTo [ Bench.Serialization, Bench.BinaryEncode ] $
      return $!! B.encode (root, nodeL, stringL, lTextL, sTextL, integerL, varSetL, doubleL)
    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, nodeL, stringL, lTextL, sTextL, integerL, varSetL, doubleL), 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 nodeA = ListLike [Word32] -> Array Word32 [Word32]
forall a. ListLike a -> Array Word32 a
ar ListLike [Word32]
nodeL
    nm <- liftIO (newArray (bounds nodeA) MEEmpty)
    let st = St
          { nodeE :: Array Word32 [Word32]
nodeE = Array Word32 [Word32]
nodeA
          , stringE :: Array Word32 String
stringE = ListLike String -> Array Word32 String
forall a. ListLike a -> Array Word32 a
ar ListLike String
stringL
          , lTextE :: Array Word32 Text
lTextE = ListLike Text -> Array Word32 Text
forall a. ListLike a -> Array Word32 a
ar ListLike Text
lTextL
          , sTextE :: Array Word32 Text
sTextE = ListLike Text -> Array Word32 Text
forall a. ListLike a -> Array Word32 a
ar ListLike Text
sTextL
          , integerE :: Array Word32 Integer
integerE = ListLike Integer -> Array Word32 Integer
forall a. ListLike a -> Array Word32 a
ar ListLike Integer
integerL
          , varSetE :: Array Word32 VarSet
varSetE = ListLike VarSet -> Array Word32 VarSet
forall a. ListLike a -> Array Word32 a
ar ListLike VarSet
varSetL
          , doubleE :: Array Word32 Double
doubleE = ListLike Double -> Array Word32 Double
forall a. ListLike a -> Array Word32 a
ar ListLike Double
doubleL
          , nodeMemo :: IOArray Word32 MemoEntry
nodeMemo = IOArray Word32 MemoEntry
nm
          , modFile :: ModuleToSource
modFile = ModuleToSource
mf
          , includes :: List1 AbsolutePath
includes = List1 AbsolutePath
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)