{-# LANGUAGE CPP                  #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE UndecidableInstances #-} -- Due to ICODE vararg typeclass
{-# LANGUAGE MagicHash            #-}
{-# LANGUAGE UnboxedTuples        #-}

{-
András, 2023-10-2:

All code in Agda/TypeChecking/Serialise should be strict, since serialization necessarily
forces all data, eventually.
  - (<$!>) should be used instead of lazy fmap.
  - Any redex that's passed to `return`, a lazy constructor, or a function, should
    be forced beforehand with strict `let`, strict binding or ($!).
-}

module Agda.TypeChecking.Serialise.Base where

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 (StateT, gets)

import Data.Proxy

import Data.Array.IArray
import Data.Array.IO
import qualified Data.HashMap.Strict as Hm
import qualified Data.ByteString.Lazy as L
import Data.Hashable
import Data.Int (Int32)
import Data.Maybe
import qualified Data.Binary as B
import qualified Data.Binary.Get as B
import qualified Data.Text      as T
import qualified Data.Text.Lazy as TL
import Data.Typeable ( cast, Typeable, TypeRep, typeRep, typeRepFingerprint )
import GHC.Exts (Word(..), timesWord2#, xor#, Any)
import GHC.Fingerprint.Type
import Unsafe.Coerce

import Agda.Syntax.Common (NameId)
import Agda.Syntax.Internal (Term, QName(..), ModuleName(..), nameId)
import Agda.TypeChecking.Monad.Base (TypeError(GenericError), ModuleToSource)

import Agda.Utils.FileName
import Agda.Utils.HashTable (HashTable)
import qualified Agda.Utils.HashTable as H
import Agda.Utils.IORef
import Agda.Utils.Lens
import Agda.Utils.Monad
import Agda.Utils.Pointer
import Agda.Utils.TypeLevel

-- | Constructor tag (maybe omitted) and argument indices.
data Node = Empty | Cons !Int32 !Node deriving Node -> Node -> Bool
(Node -> Node -> Bool) -> (Node -> Node -> Bool) -> Eq Node
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Node -> Node -> Bool
== :: Node -> Node -> Bool
$c/= :: Node -> Node -> Bool
/= :: Node -> Node -> Bool
Eq

instance Hashable Node where
  -- Adapted from https://github.com/tkaitchuck/aHash/wiki/AHash-fallback-algorithm
  hashWithSalt :: Int -> Node -> Int
hashWithSalt Int
h Node
n = Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word -> Node -> Word
go (Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
h) Node
n) where
    xor :: Word -> Word -> Word
xor (W# Word#
x) (W# Word#
y) = Word# -> Word
W# (Word# -> Word# -> Word#
xor# Word#
x Word#
y)

    foldedMul :: Word -> Word -> Word
    foldedMul :: Word -> Word -> Word
foldedMul (W# Word#
x) (W# Word#
y) = case Word# -> Word# -> (# Word#, Word# #)
timesWord2# Word#
x Word#
y of (# Word#
hi, Word#
lo #) -> Word# -> Word
W# (Word# -> Word# -> Word#
xor# Word#
hi Word#
lo)

    combine :: Word -> Word -> Word
    combine :: Word -> Word -> Word
combine Word
x Word
y = Word -> Word -> Word
foldedMul (Word -> Word -> Word
xor Word
x Word
y) Word
11400714819323198549

    go :: Word -> Node -> Word
    go :: Word -> Node -> Word
go !Word
h Node
Empty       = Word
h
    go  Word
h (Cons Int32
n Node
ns) = Word -> Node -> Word
go (Word -> Word -> Word
combine Word
h (Int32 -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
n)) Node
ns

  hash :: Node -> Int
hash = Int -> Node -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
3032525626373534813

instance B.Binary Node where

  get :: Get Node
get = Int -> Get Node
go (Int -> Get Node) -> Get Int -> Get Node
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Get Int
forall t. Binary t => Get t
B.get where

    go :: Int -> B.Get Node
    go :: Int -> Get Node
go Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 =
      Node -> Get Node
forall a. a -> Get a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Node
Empty
    go Int
n = do
      !x    <- Get Int32
forall t. Binary t => Get t
B.get
      !node <- go (n - 1)
      pure $ Cons x node

  put :: Node -> Put
put Node
n = Int -> Put
forall t. Binary t => t -> Put
B.put (Node -> Int
len Node
n) Put -> Put -> Put
forall a. Semigroup a => a -> a -> a
<> Node -> Put
go Node
n where

    len :: Node -> Int
    len :: Node -> Int
len = Int -> Node -> Int
forall {t}. Num t => t -> Node -> t
go Int
0 where
      go :: t -> Node -> t
go !t
acc Node
Empty     = t
acc
      go t
acc (Cons Int32
_ Node
n) = t -> Node -> t
go (t
acc t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) Node
n

    go :: Node -> B.Put
    go :: Node -> Put
go Node
Empty       = Put
forall a. Monoid a => a
mempty
    go (Cons Int32
n Node
ns) = Int32 -> Put
forall t. Binary t => t -> Put
B.put Int32
n Put -> Put -> Put
forall a. Semigroup a => a -> a -> a
<> Node -> Put
go Node
ns

-- | Association lists mapping TypeRep fingerprints to values. In some cases
--   values with different types have the same serialized representation. This
--   structure disambiguates them.
data MemoEntry = MEEmpty | MECons {-# unpack #-} !Fingerprint !Any !MemoEntry

-- 2023-10-2 András: `typeRepFingerprint` usually inlines a 4-way case, which
-- yields significant code size increase as GHC often inlines the same code into
-- the branches. This wouldn't matter in "normal" code but the serialization
-- instances use very heavy inlining. The NOINLINE cuts down on the code size.
fingerprintNoinline :: TypeRep -> Fingerprint
fingerprintNoinline :: TypeRep -> Fingerprint
fingerprintNoinline TypeRep
rep = TypeRep -> Fingerprint
typeRepFingerprint TypeRep
rep
{-# NOINLINE fingerprintNoinline #-}

lookupME :: forall a b. Proxy a -> Fingerprint -> MemoEntry -> (a -> b) -> b -> b
lookupME :: forall a b.
Proxy a -> Fingerprint -> MemoEntry -> (a -> b) -> b -> b
lookupME Proxy a
proxy Fingerprint
fprint MemoEntry
me a -> b
found b
notfound = Fingerprint -> MemoEntry -> b
go Fingerprint
fprint MemoEntry
me where
  go :: Fingerprint -> MemoEntry -> b
  go :: Fingerprint -> MemoEntry -> b
go Fingerprint
fp MemoEntry
MEEmpty =
    b
notfound
  go Fingerprint
fp (MECons Fingerprint
fp' Any
x MemoEntry
me)
    | Fingerprint
fp Fingerprint -> Fingerprint -> Bool
forall a. Eq a => a -> a -> Bool
== Fingerprint
fp' = a -> b
found (Any -> a
forall a b. a -> b
unsafeCoerce Any
x)
    | Bool
True      = Fingerprint -> MemoEntry -> b
go Fingerprint
fp MemoEntry
me
{-# NOINLINE lookupME #-}

-- | Structure providing fresh identifiers for hash map
--   and counting hash map hits (i.e. when no fresh identifier required).
#ifdef DEBUG_SERIALISATION
data FreshAndReuse = FreshAndReuse
  { farFresh :: !Int32 -- ^ Number of hash map misses.
  , farReuse :: !Int32 -- ^ Number of hash map hits.
  }
#else
newtype FreshAndReuse = FreshAndReuse
  { FreshAndReuse -> Int32
farFresh :: Int32 -- ^ Number of hash map misses.
  }
#endif

farEmpty :: FreshAndReuse
farEmpty :: FreshAndReuse
farEmpty = Int32 -> FreshAndReuse
FreshAndReuse Int32
0
#ifdef DEBUG_SERIALISATION
                           0
#endif

lensFresh :: Lens' FreshAndReuse Int32
lensFresh :: Lens' FreshAndReuse Int32
lensFresh Int32 -> f Int32
f FreshAndReuse
r = Int32 -> f Int32
f (FreshAndReuse -> Int32
farFresh FreshAndReuse
r) f Int32 -> (Int32 -> FreshAndReuse) -> f FreshAndReuse
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Int32
i -> FreshAndReuse
r { farFresh = i }
{-# INLINE lensFresh #-}

#ifdef DEBUG_SERIALISATION
lensReuse :: Lens' FreshAndReuse Int32
lensReuse f r = f (farReuse r) <&> \ i -> r { farReuse = i }
{-# INLINE lensReuse #-}
#endif

-- | Two 'QName's are equal if their @QNameId@ is equal.
type QNameId = [NameId]

-- | Computing a qualified names composed ID.
qnameId :: QName -> QNameId
qnameId :: QName -> QNameId
qnameId (QName (MName [Name]
ns) Name
n) = (Name -> NameId) -> [Name] -> QNameId
forall a b. (a -> b) -> [a] -> [b]
map Name -> NameId
nameId ([Name] -> QNameId) -> [Name] -> QNameId
forall a b. (a -> b) -> a -> b
$ Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
ns

-- | State of the the encoder.
data Dict = Dict
  -- Dictionaries which are serialized:
  { Dict -> HashTable Node Int32
nodeD        :: !(HashTable Node    Int32)    -- ^ Written to interface file.
  , Dict -> HashTable String Int32
stringD      :: !(HashTable String  Int32)    -- ^ Written to interface file.
  , Dict -> HashTable Text Int32
lTextD       :: !(HashTable TL.Text Int32)    -- ^ Written to interface file.
  , Dict -> HashTable Text Int32
sTextD       :: !(HashTable T.Text  Int32)    -- ^ Written to interface file.
  , Dict -> HashTable Integer Int32
integerD     :: !(HashTable Integer Int32)    -- ^ Written to interface file.
  , Dict -> HashTable Double Int32
doubleD      :: !(HashTable Double  Int32)    -- ^ Written to interface file.
  -- Dicitionaries which are not serialized, but provide
  -- short cuts to speed up serialization:
  , Dict -> HashTable (Ptr Term) Int32
termD        :: !(HashTable (Ptr Term) Int32) -- ^ Not written to interface file.
  -- Andreas, Makoto, AIM XXI
  -- Memoizing A.Name does not buy us much if we already memoize A.QName.
  , Dict -> HashTable NameId Int32
nameD        :: !(HashTable NameId  Int32)    -- ^ Not written to interface file.
  , Dict -> HashTable QNameId Int32
qnameD       :: !(HashTable QNameId Int32)    -- ^ Not written to interface file.
  -- Fresh UIDs and reuse statistics:
  , Dict -> IORef FreshAndReuse
nodeC        :: !(IORef FreshAndReuse)  -- counters for fresh indexes
  , Dict -> IORef FreshAndReuse
stringC      :: !(IORef FreshAndReuse)
  , Dict -> IORef FreshAndReuse
lTextC       :: !(IORef FreshAndReuse)
  , Dict -> IORef FreshAndReuse
sTextC       :: !(IORef FreshAndReuse)
  , Dict -> IORef FreshAndReuse
integerC     :: !(IORef FreshAndReuse)
  , Dict -> IORef FreshAndReuse
doubleC      :: !(IORef FreshAndReuse)
  , Dict -> IORef FreshAndReuse
termC        :: !(IORef FreshAndReuse)
  , Dict -> IORef FreshAndReuse
nameC        :: !(IORef FreshAndReuse)
  , Dict -> IORef FreshAndReuse
qnameC       :: !(IORef FreshAndReuse)
  , Dict -> HashTable String Int
stats        :: !(HashTable String Int)
  , Dict -> Bool
collectStats :: !Bool
    -- ^ If @True@ collect in @stats@ the quantities of
    --   calls to @icode@ for each @Typeable a@.
  }

-- | Creates an empty dictionary.
emptyDict
  :: Bool
     -- ^ Collect statistics for @icode@ calls?
  -> IO Dict
emptyDict :: Bool -> IO Dict
emptyDict Bool
collectStats = HashTable Node Int32
-> HashTable String Int32
-> HashTable Text Int32
-> HashTable Text Int32
-> HashTable Integer Int32
-> HashTable Double Int32
-> HashTable (Ptr Term) Int32
-> HashTable NameId Int32
-> HashTable QNameId Int32
-> IORef FreshAndReuse
-> IORef FreshAndReuse
-> IORef FreshAndReuse
-> IORef FreshAndReuse
-> IORef FreshAndReuse
-> IORef FreshAndReuse
-> IORef FreshAndReuse
-> IORef FreshAndReuse
-> IORef FreshAndReuse
-> HashTable String Int
-> Bool
-> Dict
Dict
  (HashTable Node Int32
 -> HashTable String Int32
 -> HashTable Text Int32
 -> HashTable Text Int32
 -> HashTable Integer Int32
 -> HashTable Double Int32
 -> HashTable (Ptr Term) Int32
 -> HashTable NameId Int32
 -> HashTable QNameId Int32
 -> IORef FreshAndReuse
 -> IORef FreshAndReuse
 -> IORef FreshAndReuse
 -> IORef FreshAndReuse
 -> IORef FreshAndReuse
 -> IORef FreshAndReuse
 -> IORef FreshAndReuse
 -> IORef FreshAndReuse
 -> IORef FreshAndReuse
 -> HashTable String Int
 -> Bool
 -> Dict)
-> IO (HashTable Node Int32)
-> IO
     (HashTable String Int32
      -> HashTable Text Int32
      -> HashTable Text Int32
      -> HashTable Integer Int32
      -> HashTable Double Int32
      -> HashTable (Ptr Term) Int32
      -> HashTable NameId Int32
      -> HashTable QNameId Int32
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> HashTable String Int
      -> Bool
      -> Dict)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (HashTable Node Int32)
forall k v. IO (HashTable k v)
H.empty
  IO
  (HashTable String Int32
   -> HashTable Text Int32
   -> HashTable Text Int32
   -> HashTable Integer Int32
   -> HashTable Double Int32
   -> HashTable (Ptr Term) Int32
   -> HashTable NameId Int32
   -> HashTable QNameId Int32
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> HashTable String Int
   -> Bool
   -> Dict)
-> IO (HashTable String Int32)
-> IO
     (HashTable Text Int32
      -> HashTable Text Int32
      -> HashTable Integer Int32
      -> HashTable Double Int32
      -> HashTable (Ptr Term) Int32
      -> HashTable NameId Int32
      -> HashTable QNameId Int32
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> HashTable String Int
      -> Bool
      -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO (HashTable String Int32)
forall k v. IO (HashTable k v)
H.empty
  IO
  (HashTable Text Int32
   -> HashTable Text Int32
   -> HashTable Integer Int32
   -> HashTable Double Int32
   -> HashTable (Ptr Term) Int32
   -> HashTable NameId Int32
   -> HashTable QNameId Int32
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> HashTable String Int
   -> Bool
   -> Dict)
-> IO (HashTable Text Int32)
-> IO
     (HashTable Text Int32
      -> HashTable Integer Int32
      -> HashTable Double Int32
      -> HashTable (Ptr Term) Int32
      -> HashTable NameId Int32
      -> HashTable QNameId Int32
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> HashTable String Int
      -> Bool
      -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO (HashTable Text Int32)
forall k v. IO (HashTable k v)
H.empty
  IO
  (HashTable Text Int32
   -> HashTable Integer Int32
   -> HashTable Double Int32
   -> HashTable (Ptr Term) Int32
   -> HashTable NameId Int32
   -> HashTable QNameId Int32
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> HashTable String Int
   -> Bool
   -> Dict)
-> IO (HashTable Text Int32)
-> IO
     (HashTable Integer Int32
      -> HashTable Double Int32
      -> HashTable (Ptr Term) Int32
      -> HashTable NameId Int32
      -> HashTable QNameId Int32
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> HashTable String Int
      -> Bool
      -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO (HashTable Text Int32)
forall k v. IO (HashTable k v)
H.empty
  IO
  (HashTable Integer Int32
   -> HashTable Double Int32
   -> HashTable (Ptr Term) Int32
   -> HashTable NameId Int32
   -> HashTable QNameId Int32
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> HashTable String Int
   -> Bool
   -> Dict)
-> IO (HashTable Integer Int32)
-> IO
     (HashTable Double Int32
      -> HashTable (Ptr Term) Int32
      -> HashTable NameId Int32
      -> HashTable QNameId Int32
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> HashTable String Int
      -> Bool
      -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO (HashTable Integer Int32)
forall k v. IO (HashTable k v)
H.empty
  IO
  (HashTable Double Int32
   -> HashTable (Ptr Term) Int32
   -> HashTable NameId Int32
   -> HashTable QNameId Int32
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> HashTable String Int
   -> Bool
   -> Dict)
-> IO (HashTable Double Int32)
-> IO
     (HashTable (Ptr Term) Int32
      -> HashTable NameId Int32
      -> HashTable QNameId Int32
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> HashTable String Int
      -> Bool
      -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO (HashTable Double Int32)
forall k v. IO (HashTable k v)
H.empty
  IO
  (HashTable (Ptr Term) Int32
   -> HashTable NameId Int32
   -> HashTable QNameId Int32
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> HashTable String Int
   -> Bool
   -> Dict)
-> IO (HashTable (Ptr Term) Int32)
-> IO
     (HashTable NameId Int32
      -> HashTable QNameId Int32
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> HashTable String Int
      -> Bool
      -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO (HashTable (Ptr Term) Int32)
forall k v. IO (HashTable k v)
H.empty
  IO
  (HashTable NameId Int32
   -> HashTable QNameId Int32
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> HashTable String Int
   -> Bool
   -> Dict)
-> IO (HashTable NameId Int32)
-> IO
     (HashTable QNameId Int32
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> HashTable String Int
      -> Bool
      -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO (HashTable NameId Int32)
forall k v. IO (HashTable k v)
H.empty
  IO
  (HashTable QNameId Int32
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> HashTable String Int
   -> Bool
   -> Dict)
-> IO (HashTable QNameId Int32)
-> IO
     (IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> HashTable String Int
      -> Bool
      -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO (HashTable QNameId Int32)
forall k v. IO (HashTable k v)
H.empty
  IO
  (IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> HashTable String Int
   -> Bool
   -> Dict)
-> IO (IORef FreshAndReuse)
-> IO
     (IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> HashTable String Int
      -> Bool
      -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FreshAndReuse -> IO (IORef FreshAndReuse)
forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  IO
  (IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> HashTable String Int
   -> Bool
   -> Dict)
-> IO (IORef FreshAndReuse)
-> IO
     (IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> HashTable String Int
      -> Bool
      -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FreshAndReuse -> IO (IORef FreshAndReuse)
forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  IO
  (IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> HashTable String Int
   -> Bool
   -> Dict)
-> IO (IORef FreshAndReuse)
-> IO
     (IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> HashTable String Int
      -> Bool
      -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FreshAndReuse -> IO (IORef FreshAndReuse)
forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  IO
  (IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> HashTable String Int
   -> Bool
   -> Dict)
-> IO (IORef FreshAndReuse)
-> IO
     (IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> HashTable String Int
      -> Bool
      -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FreshAndReuse -> IO (IORef FreshAndReuse)
forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  IO
  (IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> HashTable String Int
   -> Bool
   -> Dict)
-> IO (IORef FreshAndReuse)
-> IO
     (IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> HashTable String Int
      -> Bool
      -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FreshAndReuse -> IO (IORef FreshAndReuse)
forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  IO
  (IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> HashTable String Int
   -> Bool
   -> Dict)
-> IO (IORef FreshAndReuse)
-> IO
     (IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> IORef FreshAndReuse
      -> HashTable String Int
      -> Bool
      -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FreshAndReuse -> IO (IORef FreshAndReuse)
forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  IO
  (IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> IORef FreshAndReuse
   -> HashTable String Int
   -> Bool
   -> Dict)
-> IO (IORef FreshAndReuse)
-> IO
     (IORef FreshAndReuse
      -> IORef FreshAndReuse -> HashTable String Int -> Bool -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FreshAndReuse -> IO (IORef FreshAndReuse)
forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  IO
  (IORef FreshAndReuse
   -> IORef FreshAndReuse -> HashTable String Int -> Bool -> Dict)
-> IO (IORef FreshAndReuse)
-> IO (IORef FreshAndReuse -> HashTable String Int -> Bool -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FreshAndReuse -> IO (IORef FreshAndReuse)
forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  IO (IORef FreshAndReuse -> HashTable String Int -> Bool -> Dict)
-> IO (IORef FreshAndReuse)
-> IO (HashTable String Int -> Bool -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FreshAndReuse -> IO (IORef FreshAndReuse)
forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  IO (HashTable String Int -> Bool -> Dict)
-> IO (HashTable String Int) -> IO (Bool -> Dict)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO (HashTable String Int)
forall k v. IO (HashTable k v)
H.empty
  IO (Bool -> Dict) -> IO Bool -> IO Dict
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> IO Bool
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
collectStats

-- | Univeral memo structure, to introduce sharing during decoding
type Memo = IOArray Int32 MemoEntry

-- | State of the decoder.
data St = St
  { St -> Array Int32 [Int32]
nodeE     :: !(Array Int32 [Int32])  -- ^ Obtained from interface file.
  , St -> Array Int32 String
stringE   :: !(Array Int32 String)   -- ^ Obtained from interface file.
  , St -> Array Int32 Text
lTextE    :: !(Array Int32 TL.Text)  -- ^ Obtained from interface file.
  , St -> Array Int32 Text
sTextE    :: !(Array Int32 T.Text)   -- ^ Obtained from interface file.
  , St -> Array Int32 Integer
integerE  :: !(Array Int32 Integer)  -- ^ Obtained from interface file.
  , St -> Array Int32 Double
doubleE   :: !(Array Int32 Double)   -- ^ Obtained from interface file.
  , St -> Memo
nodeMemo  :: !Memo
    -- ^ Created and modified by decoder.
    --   Used to introduce sharing while deserializing objects.
  , St -> ModuleToSource
modFile   :: !ModuleToSource
    -- ^ Maps module names to file names. Constructed by the decoder.
  , St -> [AbsolutePath]
includes  :: ![AbsolutePath]
    -- ^ The include directories.
  }

-- | Monad used by the encoder.

type S a = ReaderT Dict IO a

-- | Monad used by the decoder.
--
-- 'TCM' is not used because the associated overheads would make
-- decoding slower.

type R = StateT St IO

-- | Throws an error which is suitable when the data stream is
-- malformed.

malformed :: R a
malformed :: forall a. R a
malformed = IO a -> StateT St IO a
forall a. IO a -> StateT St IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> StateT St IO a) -> IO a -> StateT St IO a
forall a b. (a -> b) -> a -> b
$ ErrorCall -> IO a
forall e a. (HasCallStack, Exception e) => e -> IO a
E.throwIO (ErrorCall -> IO a) -> ErrorCall -> IO a
forall a b. (a -> b) -> a -> b
$ String -> ErrorCall
E.ErrorCall String
"Malformed input."
{-# NOINLINE malformed #-} -- 2023-10-2 András: cold code, so should be out-of-line.

class Typeable a => EmbPrj a where
  icode :: a -> S Int32  -- ^ Serialization (wrapper).
  icod_ :: a -> S Int32  -- ^ Serialization (worker).
  value :: Int32 -> R a  -- ^ Deserialization.

  icode a
a = do
    !r <- a -> S Int32
forall a. EmbPrj a => a -> S Int32
icod_ a
a
    tickICode a
    pure r
  {-# INLINE icode #-}

  -- Simple enumeration types can be (de)serialized using (from/to)Enum.
  default value :: (Enum a, Bounded a) => Int32 -> R a
  value Int32
i =
    let i' :: Int
i' = Int32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
i in
    if Int
i' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= a -> Int
forall a. Enum a => a -> Int
fromEnum (a
forall a. Bounded a => a
minBound :: a) Bool -> Bool -> Bool
&& Int
i' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= a -> Int
forall a. Enum a => a -> Int
fromEnum (a
forall a. Bounded a => a
maxBound :: a)
    then a -> R a
forall a. a -> StateT St IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> R a) -> a -> R a
forall a b. (a -> b) -> a -> b
$! Int -> a
forall a. Enum a => Int -> a
toEnum Int
i'
    else R a
forall a. R a
malformed

  default icod_ :: (Enum a, Bounded a) => a -> S Int32
  icod_ a
x = Int32 -> S Int32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int32 -> S Int32) -> Int32 -> S Int32
forall a b. (a -> b) -> a -> b
$! Int -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int32) -> Int -> Int32
forall a b. (a -> b) -> a -> b
$! a -> Int
forall a. Enum a => a -> Int
fromEnum a
x

-- | The actual logic of `tickICode` is cold code, so it's out-of-line,
--   to decrease code size and avoid cache pollution.
goTickIcode :: forall a. Typeable a => Proxy a -> S ()
goTickIcode :: forall a. Typeable a => Proxy a -> S ()
goTickIcode Proxy a
p = do
  let key :: String
key = String
"icode " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (Proxy a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy a
p)
  hmap <- (Dict -> HashTable String Int)
-> ReaderT Dict IO (HashTable String Int)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable String Int
stats
  liftIO $ do
    n <- fromMaybe 0 <$> H.lookup hmap key
    H.insert hmap key $! n + 1
{-# NOINLINE goTickIcode #-}

-- | Increase entry for @a@ in 'stats'.
tickICode :: forall a. Typeable a => a -> S ()
tickICode :: forall a. Typeable a => a -> S ()
tickICode a
_ = ReaderT Dict IO Bool -> S () -> S ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((Dict -> Bool) -> ReaderT Dict IO Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> Bool
collectStats) (S () -> S ()) -> S () -> S ()
forall a b. (a -> b) -> a -> b
$ Proxy a -> S ()
forall a. Typeable a => Proxy a -> S ()
goTickIcode (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy a)
{-# INLINE tickICode #-}

-- | Data.Binary.runGetState is deprecated in favour of runGetIncremental.
--   Reimplementing it in terms of the new function. The new Decoder type contains
--   strict byte strings so we need to be careful not to feed the entire lazy byte
--   string to the decoder at once.
runGetState :: B.Get a -> L.ByteString -> B.ByteOffset -> (a, L.ByteString, B.ByteOffset)
runGetState :: forall a.
Get a -> ByteString -> ByteOffset -> (a, ByteString, ByteOffset)
runGetState Get a
g ByteString
s ByteOffset
n = Decoder a -> [StrictByteString] -> (a, ByteString, ByteOffset)
feed (Get a -> Decoder a
forall a. Get a -> Decoder a
B.runGetIncremental Get a
g) (ByteString -> [StrictByteString]
L.toChunks ByteString
s)
  where
    feed :: Decoder a -> [StrictByteString] -> (a, ByteString, ByteOffset)
feed (B.Done StrictByteString
s ByteOffset
n' a
x) [StrictByteString]
ss     = (a
x, [StrictByteString] -> ByteString
L.fromChunks (StrictByteString
s StrictByteString -> [StrictByteString] -> [StrictByteString]
forall a. a -> [a] -> [a]
: [StrictByteString]
ss), ByteOffset
n ByteOffset -> ByteOffset -> ByteOffset
forall a. Num a => a -> a -> a
+ ByteOffset
n')
    feed (B.Fail StrictByteString
_ ByteOffset
_ String
err) [StrictByteString]
_     = String -> (a, ByteString, ByteOffset)
forall a. HasCallStack => String -> a
error String
err
    feed (B.Partial Maybe StrictByteString -> Decoder a
f) (StrictByteString
s : [StrictByteString]
ss) = Decoder a -> [StrictByteString] -> (a, ByteString, ByteOffset)
feed (Maybe StrictByteString -> Decoder a
f (Maybe StrictByteString -> Decoder a)
-> Maybe StrictByteString -> Decoder a
forall a b. (a -> b) -> a -> b
$ StrictByteString -> Maybe StrictByteString
forall a. a -> Maybe a
Just StrictByteString
s) [StrictByteString]
ss
    feed (B.Partial Maybe StrictByteString -> Decoder a
f) []       = Decoder a -> [StrictByteString] -> (a, ByteString, ByteOffset)
feed (Maybe StrictByteString -> Decoder a
f Maybe StrictByteString
forall a. Maybe a
Nothing) []

-- Specializing icodeX leads to Warning like
-- src/full/Agda/TypeChecking/Serialise.hs:1297:1: Warning:
--     RULE left-hand side too complicated to desugar
--       case cobox_aQY5 of _ [Occ=Dead] { ghc-prim:GHC.Types.Eq# cobox ->
--       icodeX @ String $dEq_aQY3 $dHashable_aQY4
--       }
--
-- type ICodeX k
--   =  (Dict -> HashTable k Int32)
--   -> (Dict -> IORef Int32)
--   -> k -> S Int32
-- {-# SPECIALIZE icodeX :: ICodeX String  #-}
-- {-# SPECIALIZE icodeX :: ICodeX Integer #-}
-- {-# SPECIALIZE icodeX :: ICodeX Double  #-}
-- {-# SPECIALIZE icodeX :: ICodeX Node    #-}

-- Andreas, 2014-10-16 AIM XX:
-- Inlining this increases Serialization time by 10%
-- Makoto's theory: code size increase might lead to
-- instruction cache misses.
-- {-# INLINE icodeX #-}
icodeX :: (Eq k, Hashable k)
  =>  (Dict -> HashTable k Int32)
  -> (Dict -> IORef FreshAndReuse)
  -> k -> S Int32
icodeX :: forall k.
(Eq k, Hashable k) =>
(Dict -> HashTable k Int32)
-> (Dict -> IORef FreshAndReuse) -> k -> S Int32
icodeX Dict -> HashTable k Int32
dict Dict -> IORef FreshAndReuse
counter k
key = do
  d <- (Dict -> HashTable k Int32) -> ReaderT Dict IO (HashTable k Int32)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable k Int32
dict
  c <- asks counter
  liftIO $ do
    mi <- H.lookup d key
    case mi of
      Just Int32
i  -> do
#ifdef DEBUG_SERIALISATION
        modifyIORef' c $ over lensReuse (+ 1)
#endif
        Int32 -> IO Int32
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int32 -> IO Int32) -> Int32 -> IO Int32
forall a b. (a -> b) -> a -> b
$! Int32
i
      Maybe Int32
Nothing -> do
        !fresh <- (FreshAndReuse -> Lens' FreshAndReuse Int32 -> Int32
forall o i. o -> Lens' o i -> i
^. (Int32 -> f Int32) -> FreshAndReuse -> f FreshAndReuse
Lens' FreshAndReuse Int32
lensFresh) (FreshAndReuse -> Int32) -> IO FreshAndReuse -> IO Int32
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do IORef FreshAndReuse
-> (FreshAndReuse -> FreshAndReuse) -> IO FreshAndReuse
forall a. IORef a -> (a -> a) -> IO a
readModifyIORef' IORef FreshAndReuse
c ((FreshAndReuse -> FreshAndReuse) -> IO FreshAndReuse)
-> (FreshAndReuse -> FreshAndReuse) -> IO FreshAndReuse
forall a b. (a -> b) -> a -> b
$ Lens' FreshAndReuse Int32 -> LensMap FreshAndReuse Int32
forall o i. Lens' o i -> LensMap o i
over (Int32 -> f Int32) -> FreshAndReuse -> f FreshAndReuse
Lens' FreshAndReuse Int32
lensFresh (Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+ Int32
1)
        H.insert d key fresh
        return fresh

-- Instead of inlining icodeX, we manually specialize it to
-- its four uses: Integer, String, Double, Node.
-- Not a great gain (hardly noticeable), but not harmful.

icodeInteger :: Integer -> S Int32
icodeInteger :: Integer -> S Int32
icodeInteger Integer
key = do
  d <- (Dict -> HashTable Integer Int32)
-> ReaderT Dict IO (HashTable Integer Int32)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable Integer Int32
integerD
  c <- asks integerC
  liftIO $ do
    mi <- H.lookup d key
    case mi of
      Just Int32
i  -> do
#ifdef DEBUG_SERIALISATION
        modifyIORef' c $ over lensReuse (+ 1)
#endif
        Int32 -> IO Int32
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int32 -> IO Int32) -> Int32 -> IO Int32
forall a b. (a -> b) -> a -> b
$! Int32
i
      Maybe Int32
Nothing -> do
        !fresh <- (FreshAndReuse -> Lens' FreshAndReuse Int32 -> Int32
forall o i. o -> Lens' o i -> i
^. (Int32 -> f Int32) -> FreshAndReuse -> f FreshAndReuse
Lens' FreshAndReuse Int32
lensFresh) (FreshAndReuse -> Int32) -> IO FreshAndReuse -> IO Int32
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do IORef FreshAndReuse
-> (FreshAndReuse -> FreshAndReuse) -> IO FreshAndReuse
forall a. IORef a -> (a -> a) -> IO a
readModifyIORef' IORef FreshAndReuse
c ((FreshAndReuse -> FreshAndReuse) -> IO FreshAndReuse)
-> (FreshAndReuse -> FreshAndReuse) -> IO FreshAndReuse
forall a b. (a -> b) -> a -> b
$ Lens' FreshAndReuse Int32 -> LensMap FreshAndReuse Int32
forall o i. Lens' o i -> LensMap o i
over (Int32 -> f Int32) -> FreshAndReuse -> f FreshAndReuse
Lens' FreshAndReuse Int32
lensFresh (Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+ Int32
1)
        H.insert d key fresh
        return fresh

icodeDouble :: Double -> S Int32
icodeDouble :: Double -> S Int32
icodeDouble Double
key = do
  d <- (Dict -> HashTable Double Int32)
-> ReaderT Dict IO (HashTable Double Int32)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable Double Int32
doubleD
  c <- asks doubleC
  liftIO $ do
    mi <- H.lookup d key
    case mi of
      Just Int32
i  -> do
#ifdef DEBUG_SERIALISATION
        modifyIORef' c $ over lensReuse (+ 1)
#endif
        Int32 -> IO Int32
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int32 -> IO Int32) -> Int32 -> IO Int32
forall a b. (a -> b) -> a -> b
$! Int32
i
      Maybe Int32
Nothing -> do
        !fresh <- (FreshAndReuse -> Lens' FreshAndReuse Int32 -> Int32
forall o i. o -> Lens' o i -> i
^. (Int32 -> f Int32) -> FreshAndReuse -> f FreshAndReuse
Lens' FreshAndReuse Int32
lensFresh) (FreshAndReuse -> Int32) -> IO FreshAndReuse -> IO Int32
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do IORef FreshAndReuse
-> (FreshAndReuse -> FreshAndReuse) -> IO FreshAndReuse
forall a. IORef a -> (a -> a) -> IO a
readModifyIORef' IORef FreshAndReuse
c ((FreshAndReuse -> FreshAndReuse) -> IO FreshAndReuse)
-> (FreshAndReuse -> FreshAndReuse) -> IO FreshAndReuse
forall a b. (a -> b) -> a -> b
$ Lens' FreshAndReuse Int32 -> LensMap FreshAndReuse Int32
forall o i. Lens' o i -> LensMap o i
over (Int32 -> f Int32) -> FreshAndReuse -> f FreshAndReuse
Lens' FreshAndReuse Int32
lensFresh (Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+ Int32
1)
        H.insert d key fresh
        return fresh

icodeString :: String -> S Int32
icodeString :: String -> S Int32
icodeString String
key = do
  d <- (Dict -> HashTable String Int32)
-> ReaderT Dict IO (HashTable String Int32)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable String Int32
stringD
  c <- asks stringC
  liftIO $ do
    mi <- H.lookup d key
    case mi of
      Just Int32
i  -> do
#ifdef DEBUG_SERIALISATION
        modifyIORef' c $ over lensReuse (+ 1)
#endif
        Int32 -> IO Int32
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
i
      Maybe Int32
Nothing -> do
        !fresh <- (FreshAndReuse -> Lens' FreshAndReuse Int32 -> Int32
forall o i. o -> Lens' o i -> i
^. (Int32 -> f Int32) -> FreshAndReuse -> f FreshAndReuse
Lens' FreshAndReuse Int32
lensFresh) (FreshAndReuse -> Int32) -> IO FreshAndReuse -> IO Int32
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do IORef FreshAndReuse
-> (FreshAndReuse -> FreshAndReuse) -> IO FreshAndReuse
forall a. IORef a -> (a -> a) -> IO a
readModifyIORef' IORef FreshAndReuse
c ((FreshAndReuse -> FreshAndReuse) -> IO FreshAndReuse)
-> (FreshAndReuse -> FreshAndReuse) -> IO FreshAndReuse
forall a b. (a -> b) -> a -> b
$ Lens' FreshAndReuse Int32 -> LensMap FreshAndReuse Int32
forall o i. Lens' o i -> LensMap o i
over (Int32 -> f Int32) -> FreshAndReuse -> f FreshAndReuse
Lens' FreshAndReuse Int32
lensFresh (Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+ Int32
1)
        H.insert d key fresh
        return fresh

icodeNode :: Node -> S Int32
icodeNode :: Node -> S Int32
icodeNode Node
key = do
  d <- (Dict -> HashTable Node Int32)
-> ReaderT Dict IO (HashTable Node Int32)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable Node Int32
nodeD
  c <- asks nodeC
  liftIO $ do
    mi <- H.lookup d key
    case mi of
      Just Int32
i  -> do
#ifdef DEBUG_SERIALISATION
        modifyIORef' c $ over lensReuse (+ 1)
#endif
        Int32 -> IO Int32
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int32 -> IO Int32) -> Int32 -> IO Int32
forall a b. (a -> b) -> a -> b
$! Int32
i
      Maybe Int32
Nothing -> do
        !fresh <- (FreshAndReuse -> Lens' FreshAndReuse Int32 -> Int32
forall o i. o -> Lens' o i -> i
^. (Int32 -> f Int32) -> FreshAndReuse -> f FreshAndReuse
Lens' FreshAndReuse Int32
lensFresh) (FreshAndReuse -> Int32) -> IO FreshAndReuse -> IO Int32
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do IORef FreshAndReuse
-> (FreshAndReuse -> FreshAndReuse) -> IO FreshAndReuse
forall a. IORef a -> (a -> a) -> IO a
readModifyIORef' IORef FreshAndReuse
c ((FreshAndReuse -> FreshAndReuse) -> IO FreshAndReuse)
-> (FreshAndReuse -> FreshAndReuse) -> IO FreshAndReuse
forall a b. (a -> b) -> a -> b
$ Lens' FreshAndReuse Int32 -> LensMap FreshAndReuse Int32
forall o i. Lens' o i -> LensMap o i
over (Int32 -> f Int32) -> FreshAndReuse -> f FreshAndReuse
Lens' FreshAndReuse Int32
lensFresh (Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+ Int32
1)
        H.insert d key fresh
        return fresh

-- icodeN :: [Int32] -> S Int32
-- icodeN = icodeX nodeD nodeC

-- | @icode@ only if thing has not seen before.
icodeMemo
  :: (Ord a, Hashable a)
  => (Dict -> HashTable a Int32)    -- ^ Memo structure for thing of key @a@.
  -> (Dict -> IORef FreshAndReuse)  -- ^ Statistics.
  -> a        -- ^ Key to the thing.
  -> S Int32  -- ^ Fallback computation to encode the thing.
  -> S Int32  -- ^ Encoded thing.
icodeMemo :: forall a.
(Ord a, Hashable a) =>
(Dict -> HashTable a Int32)
-> (Dict -> IORef FreshAndReuse) -> a -> S Int32 -> S Int32
icodeMemo Dict -> HashTable a Int32
getDict Dict -> IORef FreshAndReuse
getCounter a
a S Int32
icodeP = do
    h  <- (Dict -> HashTable a Int32) -> ReaderT Dict IO (HashTable a Int32)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable a Int32
getDict
    mi <- liftIO $ H.lookup h a
    st <- asks getCounter
    case mi of
      Just Int32
i  -> IO Int32 -> S Int32
forall a. IO a -> ReaderT Dict IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int32 -> S Int32) -> IO Int32 -> S Int32
forall a b. (a -> b) -> a -> b
$ do
#ifdef DEBUG_SERIALISATION
        modifyIORef' st $ over lensReuse (+ 1)
#endif
        Int32 -> IO Int32
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int32 -> IO Int32) -> Int32 -> IO Int32
forall a b. (a -> b) -> a -> b
$! Int32
i
      Maybe Int32
Nothing -> do
        IO () -> S ()
forall a. IO a -> ReaderT Dict IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> S ()) -> IO () -> S ()
forall a b. (a -> b) -> a -> b
$ IORef FreshAndReuse -> (FreshAndReuse -> FreshAndReuse) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef FreshAndReuse
st ((FreshAndReuse -> FreshAndReuse) -> IO ())
-> (FreshAndReuse -> FreshAndReuse) -> IO ()
forall a b. (a -> b) -> a -> b
$ Lens' FreshAndReuse Int32 -> LensMap FreshAndReuse Int32
forall o i. Lens' o i -> LensMap o i
over (Int32 -> f Int32) -> FreshAndReuse -> f FreshAndReuse
Lens' FreshAndReuse Int32
lensFresh (Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+ Int32
1)
        !i <- S Int32
icodeP
        liftIO $ H.insert h a i
        return i

{-# INLINE vcase #-}
-- | @vcase value ix@ decodes thing represented by @ix :: Int32@
--   via the @valu@ function and stores it in 'nodeMemo'.
--   If @ix@ is present in 'nodeMemo', @valu@ is not used, but
--   the thing is read from 'nodeMemo' instead.
vcase :: forall a . EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase :: forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R a
valu = \Int32
ix -> do
    memo <- (St -> Memo) -> StateT St IO Memo
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Memo
nodeMemo
    let fp = TypeRep -> Fingerprint
fingerprintNoinline (Proxy a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy a))
    -- to introduce sharing, see if we have seen a thing
    -- represented by ix before
    slot <- liftIO $ readArray memo ix
    lookupME (Proxy :: Proxy a) fp slot
      -- use the stored value
      pure
      -- read new value and save it
      do !v <- valu . (! ix) =<< gets nodeE
         liftIO $ writeArray memo ix $! MECons fp (unsafeCoerce v) slot
         return v

-- | @icodeArgs proxy (a1, ..., an)@ maps @icode@ over @a1@, ..., @an@
--   and returns the corresponding list of @Int32@.

class ICODE t b where
  icodeArgs :: IsBase t ~ b => All EmbPrj (Domains t) =>
               Proxy t -> StrictProducts (Domains t) -> S Node

instance IsBase t ~ 'True => ICODE t 'True where
  icodeArgs :: (IsBase t ~ 'True, All EmbPrj (Domains t)) =>
Proxy t -> StrictProducts (Domains t) -> S Node
icodeArgs Proxy t
_ StrictProducts (Domains t)
_  = Node -> S Node
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Node
Empty
  {-# INLINE icodeArgs #-}

instance ICODE t (IsBase t) => ICODE (a -> t) 'False where
  icodeArgs :: (IsBase (a -> t) ~ 'False, All EmbPrj (Domains (a -> t))) =>
Proxy (a -> t) -> StrictProducts (Domains (a -> t)) -> S Node
icodeArgs Proxy (a -> t)
_ (Pair a
a Foldr StrictPair () (If (IsBase t) '[] (Domains' t))
as) = do
    !hd   <- a -> S Int32
forall a. EmbPrj a => a -> S Int32
icode a
a
    !node <- icodeArgs (Proxy :: Proxy t) as
    pure $ Cons hd node
  {-# INLINE icodeArgs #-}

-- | @icodeN tag t a1 ... an@ serialises the arguments @a1@, ..., @an@ of the
--   constructor @t@ together with a tag @tag@ picked to disambiguate between
--   different constructors.
--   It corresponds to @icodeNode . (tag :) =<< mapM icode [a1, ..., an]@

{-# INLINE icodeN #-}
icodeN :: forall t. ICODE t (IsBase t) => StrictCurrying (Domains t) (S Int32) =>
          All EmbPrj (Domains t) =>
          Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN :: forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
tag t
_ =
  Proxy (If (IsBase t) '[] (Domains' t))
-> Proxy (S Int32)
-> (StrictProducts (If (IsBase t) '[] (Domains' t)) -> S Int32)
-> Arrows (If (IsBase t) '[] (Domains' t)) (S Int32)
forall (as :: [*]) b.
StrictCurrying as b =>
Proxy as -> Proxy b -> (StrictProducts as -> b) -> Arrows as b
strictCurrys (Proxy (Domains t)
Proxy (If (IsBase t) '[] (Domains' t))
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Domains t)) (Proxy (S Int32)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (S Int32)) ((StrictProducts (If (IsBase t) '[] (Domains' t)) -> S Int32)
 -> Arrows (If (IsBase t) '[] (Domains' t)) (S Int32))
-> (StrictProducts (If (IsBase t) '[] (Domains' t)) -> S Int32)
-> Arrows (If (IsBase t) '[] (Domains' t)) (S Int32)
forall a b. (a -> b) -> a -> b
$ \ !StrictProducts (If (IsBase t) '[] (Domains' t))
args -> do
    !node <- Proxy t -> StrictProducts (Domains t) -> S Node
forall t (b :: Bool).
(ICODE t b, IsBase t ~ b, All EmbPrj (Domains t)) =>
Proxy t -> StrictProducts (Domains t) -> S Node
icodeArgs (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t) StrictProducts (Domains t)
StrictProducts (If (IsBase t) '[] (Domains' t))
args
    icodeNode $ Cons tag node

-- | @icodeN'@ is the same as @icodeN@ except that there is no tag
{-# INLINE icodeN' #-}
icodeN' :: forall t. ICODE t (IsBase t) => StrictCurrying (Domains t) (S Int32) =>
           All EmbPrj (Domains t) =>
           t -> Arrows (Domains t) (S Int32)
icodeN' :: forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' t
_ =
  Proxy (If (IsBase t) '[] (Domains' t))
-> Proxy (S Int32)
-> (StrictProducts (If (IsBase t) '[] (Domains' t)) -> S Int32)
-> Arrows (If (IsBase t) '[] (Domains' t)) (S Int32)
forall (as :: [*]) b.
StrictCurrying as b =>
Proxy as -> Proxy b -> (StrictProducts as -> b) -> Arrows as b
strictCurrys (Proxy (Domains t)
Proxy (If (IsBase t) '[] (Domains' t))
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Domains t)) (Proxy (S Int32)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (S Int32)) ((StrictProducts (If (IsBase t) '[] (Domains' t)) -> S Int32)
 -> Arrows (If (IsBase t) '[] (Domains' t)) (S Int32))
-> (StrictProducts (If (IsBase t) '[] (Domains' t)) -> S Int32)
-> Arrows (If (IsBase t) '[] (Domains' t)) (S Int32)
forall a b. (a -> b) -> a -> b
$ \ !StrictProducts (If (IsBase t) '[] (Domains' t))
args -> do
    !node <- Proxy t -> StrictProducts (Domains t) -> S Node
forall t (b :: Bool).
(ICODE t b, IsBase t ~ b, All EmbPrj (Domains t)) =>
Proxy t -> StrictProducts (Domains t) -> S Node
icodeArgs (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t) StrictProducts (Domains t)
StrictProducts (If (IsBase t) '[] (Domains' t))
args
    icodeNode node

-- Instead of having up to 25 versions of @valu N@, we define
-- the class VALU which generates them by typeclass resolution.
-- All of these should get inlined at compile time.

class VALU t b where

  valuN' :: b ~ IsBase t =>
            All EmbPrj (Domains t) =>
            t -> StrictProducts (Constant Int32 (Domains t)) -> R (CoDomain t)

  valueArgs :: b ~ IsBase t =>
               All EmbPrj (CoDomain t ': Domains t) =>
               Proxy t -> [Int32] -> Maybe (StrictProducts (Constant Int32 (Domains t)))

instance VALU t 'True where
  {-# INLINE valuN' #-}
  valuN' :: ('True ~ IsBase t, All EmbPrj (Domains t)) =>
t -> StrictProducts (Constant Int32 (Domains t)) -> R (CoDomain t)
valuN' t
c () = t -> StateT St IO t
forall a. a -> StateT St IO a
forall (m :: * -> *) a. Monad m => a -> m a
return t
c

  {-# INLINE valueArgs #-}
  valueArgs :: ('True ~ IsBase t, All EmbPrj (CoDomain t : Domains t)) =>
Proxy t
-> [Int32] -> Maybe (StrictProducts (Constant Int32 (Domains t)))
valueArgs Proxy t
_ [Int32]
xs = case [Int32]
xs of
    [] -> () -> Maybe ()
forall a. a -> Maybe a
Just ()
    [Int32]
_  -> Maybe ()
Maybe (StrictProducts (Constant Int32 (Domains t)))
forall a. Maybe a
Nothing


instance VALU t (IsBase t) => VALU (a -> t) 'False where
  {-# INLINE valuN' #-}
  valuN' :: ('False ~ IsBase (a -> t), All EmbPrj (Domains (a -> t))) =>
(a -> t)
-> StrictProducts (Constant Int32 (Domains (a -> t)))
-> R (CoDomain (a -> t))
valuN' a -> t
c (Pair Int32
a Foldr
  StrictPair
  ()
  (Foldr'
     (ConsMap0 (Constant1 Int32)) '[] (If (IsBase t) '[] (Domains' t)))
as) = do
    !v <- Int32 -> R a
forall a. EmbPrj a => Int32 -> R a
value Int32
a
    let !cv = a -> t
c a
v
    valuN' cv as

  {-# INLINE valueArgs #-}
  valueArgs :: ('False ~ IsBase (a -> t),
 All EmbPrj (CoDomain (a -> t) : Domains (a -> t))) =>
Proxy (a -> t)
-> [Int32]
-> Maybe (StrictProducts (Constant Int32 (Domains (a -> t))))
valueArgs Proxy (a -> t)
_ [Int32]
xs = case [Int32]
xs of
    Int32
x : [Int32]
xs' -> Int32
-> Foldr
     StrictPair
     ()
     (Foldr'
        (ConsMap0 (Constant1 Int32)) '[] (If (IsBase t) '[] (Domains' t)))
-> StrictPair
     Int32
     (Foldr
        StrictPair
        ()
        (Foldr'
           (ConsMap0 (Constant1 Int32)) '[] (If (IsBase t) '[] (Domains' t))))
forall a b. a -> b -> StrictPair a b
Pair Int32
x (Foldr
   StrictPair
   ()
   (Foldr'
      (ConsMap0 (Constant1 Int32)) '[] (If (IsBase t) '[] (Domains' t)))
 -> StrictPair
      Int32
      (Foldr
         StrictPair
         ()
         (Foldr'
            (ConsMap0 (Constant1 Int32))
            '[]
            (If (IsBase t) '[] (Domains' t)))))
-> Maybe
     (Foldr
        StrictPair
        ()
        (Foldr'
           (ConsMap0 (Constant1 Int32)) '[] (If (IsBase t) '[] (Domains' t))))
-> Maybe
     (StrictPair
        Int32
        (Foldr
           StrictPair
           ()
           (Foldr'
              (ConsMap0 (Constant1 Int32))
              '[]
              (If (IsBase t) '[] (Domains' t)))))
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Proxy t
-> [Int32] -> Maybe (StrictProducts (Constant Int32 (Domains t)))
forall t (b :: Bool).
(VALU t b, b ~ IsBase t, All EmbPrj (CoDomain t : Domains t)) =>
Proxy t
-> [Int32] -> Maybe (StrictProducts (Constant Int32 (Domains t)))
valueArgs (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t) [Int32]
xs'
    [Int32]
_       -> Maybe
  (StrictPair
     Int32
     (Foldr
        StrictPair
        ()
        (Foldr'
           (ConsMap0 (Constant1 Int32))
           '[]
           (If (IsBase t) '[] (Domains' t)))))
Maybe (StrictProducts (Constant Int32 (Domains (a -> t))))
forall a. Maybe a
Nothing

{-# INLINE valuN #-}
valuN :: forall t. VALU t (IsBase t) =>
         StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)) =>
         All EmbPrj (Domains t) =>
         t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN :: forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN t
f = Proxy
  (Foldr'
     (ConsMap0 (Constant1 Int32)) '[] (If (IsBase t) '[] (Domains' t)))
-> Proxy (R (If (IsBase t) t (CoDomain' t)))
-> (StrictProducts
      (Foldr'
         (ConsMap0 (Constant1 Int32)) '[] (If (IsBase t) '[] (Domains' t)))
    -> R (If (IsBase t) t (CoDomain' t)))
-> Arrows
     (Foldr'
        (ConsMap0 (Constant1 Int32)) '[] (If (IsBase t) '[] (Domains' t)))
     (R (If (IsBase t) t (CoDomain' t)))
forall (as :: [*]) b.
StrictCurrying as b =>
Proxy as -> Proxy b -> (StrictProducts as -> b) -> Arrows as b
strictCurrys (Proxy (Constant Int32 (Domains t))
Proxy
  (Foldr'
     (ConsMap0 (Constant1 Int32)) '[] (If (IsBase t) '[] (Domains' t)))
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Constant Int32 (Domains t)))
                 (Proxy (R (CoDomain t))
Proxy (R (If (IsBase t) t (CoDomain' t)))
forall {k} (t :: k). Proxy t
Proxy :: Proxy (R (CoDomain t)))
                 (t -> StrictProducts (Constant Int32 (Domains t)) -> R (CoDomain t)
forall t (b :: Bool).
(VALU t b, b ~ IsBase t, All EmbPrj (Domains t)) =>
t -> StrictProducts (Constant Int32 (Domains t)) -> R (CoDomain t)
valuN' t
f)

{-# INLINE valueN #-}
valueN :: forall t. VALU t (IsBase t) =>
          All EmbPrj (CoDomain t ': Domains t) =>
          t -> Int32 -> R (CoDomain t)
valueN :: forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN t
t = ([Int32] -> R (If (IsBase t) t (CoDomain' t)))
-> Int32 -> R (If (IsBase t) t (CoDomain' t))
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R (If (IsBase t) t (CoDomain' t))
valu where
  valu :: [Int32] -> R (If (IsBase t) t (CoDomain' t))
valu [Int32]
int32s = case Proxy t
-> [Int32] -> Maybe (StrictProducts (Constant Int32 (Domains t)))
forall t (b :: Bool).
(VALU t b, b ~ IsBase t, All EmbPrj (CoDomain t : Domains t)) =>
Proxy t
-> [Int32] -> Maybe (StrictProducts (Constant Int32 (Domains t)))
valueArgs (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t) [Int32]
int32s of
                  Maybe (StrictProducts (Constant Int32 (Domains t)))
Nothing -> R (If (IsBase t) t (CoDomain' t))
forall a. R a
malformed
                  Just StrictProducts (Constant Int32 (Domains t))
vs -> t
-> StrictProducts (Constant Int32 (Domains t))
-> StateT St IO (CoDomain t)
forall t (b :: Bool).
(VALU t b, b ~ IsBase t, All EmbPrj (Domains t)) =>
t -> StrictProducts (Constant Int32 (Domains t)) -> R (CoDomain t)
valuN' t
t StrictProducts (Constant Int32 (Domains t))
vs