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

module Agda.TypeChecking.Serialise.Base where

import Control.Exception (evaluate)

import Control.Monad.Catch (catchAll)
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 )

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.

type Node = [Int32]

-- | Structure providing fresh identifiers for hash map
--   and counting hash map hits (i.e. when no fresh identifier required).
#ifdef DEBUG
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
                           0
#endif

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

#ifdef DEBUG
lensReuse :: Lens' Int32 FreshAndReuse
lensReuse f r = f (farReuse r) <&> \ i -> r { farReuse = i }
#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) = forall a b. (a -> b) -> [a] -> [b]
map Name -> NameId
nameId forall a b. (a -> b) -> a -> b
$ Name
nforall 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
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. IO (HashTable k v)
H.empty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k v. IO (HashTable k v)
H.empty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k v. IO (HashTable k v)
H.empty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k v. IO (HashTable k v)
H.empty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k v. IO (HashTable k v)
H.empty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k v. IO (HashTable k v)
H.empty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k v. IO (HashTable k v)
H.empty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k v. IO (HashTable k v)
H.empty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k v. IO (HashTable k v)
H.empty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. a -> IO (IORef a)
newIORef FreshAndReuse
farEmpty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k v. IO (HashTable k v)
H.empty
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
collectStats

-- | Universal type, wraps everything.
data U = forall a . Typeable a => U !a

-- | Univeral memo structure, to introduce sharing during decoding
type Memo = IOArray Int32 (Hm.HashMap TypeRep U) -- node index -> (type rep -> value)

-- | State of the decoder.
data St = St
  { St -> Array Int32 Node
nodeE     :: !(Array Int32 Node)     -- ^ 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 a = ExceptT TypeError (StateT St IO) a

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

malformed :: R a
malformed :: forall a. R a
malformed = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError String
"Malformed input."

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
    forall a. Typeable a => a -> S ()
tickICode a
a
    forall a. EmbPrj a => a -> S Int32
icod_ a
a

  -- Simple enumeration types can be (de)serialized using (from/to)Enum.

  default value :: (Enum a) => Int32 -> R a
  value Int32
i = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. a -> IO a
evaluate (forall a. Enum a => Int -> a
toEnum (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
i))) forall (m :: * -> *) a.
MonadCatch m =>
m a -> (SomeException -> m a) -> m a
`catchAll` forall a b. a -> b -> a
const forall a. R a
malformed

  default icod_ :: (Enum a) => a -> S Int32
  icod_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => a -> Int
fromEnum

-- | Increase entry for @a@ in 'stats'.
tickICode :: forall a. Typeable a => a -> S ()
tickICode :: forall a. Typeable a => a -> S ()
tickICode a
_ = forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> Bool
collectStats) forall a b. (a -> b) -> a -> b
$ do
    let key :: String
key = String
"icode " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy a))
    HashTable String Int
hmap <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable String Int
stats
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do
      Int
n <- forall a. a -> Maybe a -> a
fromMaybe Int
0 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v.
(Eq k, Hashable k) =>
HashTable k v -> k -> IO (Maybe v)
H.lookup HashTable String Int
hmap String
key
      forall k v. (Eq k, Hashable k) => HashTable k v -> k -> v -> IO ()
H.insert HashTable String Int
hmap String
key forall a b. (a -> b) -> a -> b
$! Int
n forall a. Num a => a -> a -> a
+ Int
1

-- | 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 -> [ByteString] -> (a, ByteString, ByteOffset)
feed (forall a. Get a -> Decoder a
B.runGetIncremental Get a
g) (ByteString -> [ByteString]
L.toChunks ByteString
s)
  where
    feed :: Decoder a -> [ByteString] -> (a, ByteString, ByteOffset)
feed (B.Done ByteString
s ByteOffset
n' a
x) [ByteString]
ss     = (a
x, [ByteString] -> ByteString
L.fromChunks (ByteString
s forall a. a -> [a] -> [a]
: [ByteString]
ss), ByteOffset
n forall a. Num a => a -> a -> a
+ ByteOffset
n')
    feed (B.Fail ByteString
_ ByteOffset
_ String
err) [ByteString]
_     = forall a. HasCallStack => String -> a
error String
err
    feed (B.Partial Maybe ByteString -> Decoder a
f) (ByteString
s : [ByteString]
ss) = Decoder a -> [ByteString] -> (a, ByteString, ByteOffset)
feed (Maybe ByteString -> Decoder a
f forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ByteString
s) [ByteString]
ss
    feed (B.Partial Maybe ByteString -> Decoder a
f) []       = Decoder a -> [ByteString] -> (a, ByteString, ByteOffset)
feed (Maybe ByteString -> Decoder a
f 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
  HashTable k Int32
d <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable k Int32
dict
  IORef FreshAndReuse
c <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> IORef FreshAndReuse
counter
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do
    Maybe Int32
mi <- forall k v.
(Eq k, Hashable k) =>
HashTable k v -> k -> IO (Maybe v)
H.lookup HashTable k Int32
d k
key
    case Maybe Int32
mi of
      Just Int32
i  -> do
#ifdef DEBUG
        modifyIORef' c $ over lensReuse (+1)
#endif
        forall (m :: * -> *) a. Monad m => a -> m a
return Int32
i
      Maybe Int32
Nothing -> do
        Int32
fresh <- (forall o i. o -> Lens' i o -> i
^.Lens' Int32 FreshAndReuse
lensFresh) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do forall a. IORef a -> (a -> a) -> IO a
readModifyIORef' IORef FreshAndReuse
c forall a b. (a -> b) -> a -> b
$ forall i o. Lens' i o -> LensMap i o
over Lens' Int32 FreshAndReuse
lensFresh (forall a. Num a => a -> a -> a
+Int32
1)
        forall k v. (Eq k, Hashable k) => HashTable k v -> k -> v -> IO ()
H.insert HashTable k Int32
d k
key Int32
fresh
        forall (m :: * -> *) a. Monad m => a -> m a
return Int32
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
  HashTable Integer Int32
d <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable Integer Int32
integerD
  IORef FreshAndReuse
c <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> IORef FreshAndReuse
integerC
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do
    Maybe Int32
mi <- forall k v.
(Eq k, Hashable k) =>
HashTable k v -> k -> IO (Maybe v)
H.lookup HashTable Integer Int32
d Integer
key
    case Maybe Int32
mi of
      Just Int32
i  -> do
#ifdef DEBUG
        modifyIORef' c $ over lensReuse (+1)
#endif
        forall (m :: * -> *) a. Monad m => a -> m a
return Int32
i
      Maybe Int32
Nothing -> do
        Int32
fresh <- (forall o i. o -> Lens' i o -> i
^.Lens' Int32 FreshAndReuse
lensFresh) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do forall a. IORef a -> (a -> a) -> IO a
readModifyIORef' IORef FreshAndReuse
c forall a b. (a -> b) -> a -> b
$ forall i o. Lens' i o -> LensMap i o
over Lens' Int32 FreshAndReuse
lensFresh (forall a. Num a => a -> a -> a
+Int32
1)
        forall k v. (Eq k, Hashable k) => HashTable k v -> k -> v -> IO ()
H.insert HashTable Integer Int32
d Integer
key Int32
fresh
        forall (m :: * -> *) a. Monad m => a -> m a
return Int32
fresh

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

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

icodeNode :: Node -> S Int32
icodeNode :: Node -> S Int32
icodeNode Node
key = do
  HashTable Node Int32
d <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable Node Int32
nodeD
  IORef FreshAndReuse
c <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> IORef FreshAndReuse
nodeC
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do
    Maybe Int32
mi <- forall k v.
(Eq k, Hashable k) =>
HashTable k v -> k -> IO (Maybe v)
H.lookup HashTable Node Int32
d Node
key
    case Maybe Int32
mi of
      Just Int32
i  -> do
#ifdef DEBUG
        modifyIORef' c $ over lensReuse (+1)
#endif
        forall (m :: * -> *) a. Monad m => a -> m a
return Int32
i
      Maybe Int32
Nothing -> do
        Int32
fresh <- (forall o i. o -> Lens' i o -> i
^.Lens' Int32 FreshAndReuse
lensFresh) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do forall a. IORef a -> (a -> a) -> IO a
readModifyIORef' IORef FreshAndReuse
c forall a b. (a -> b) -> a -> b
$ forall i o. Lens' i o -> LensMap i o
over Lens' Int32 FreshAndReuse
lensFresh (forall a. Num a => a -> a -> a
+Int32
1)
        forall k v. (Eq k, Hashable k) => HashTable k v -> k -> v -> IO ()
H.insert HashTable Node Int32
d Node
key Int32
fresh
        forall (m :: * -> *) a. Monad m => a -> m a
return Int32
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
    HashTable a Int32
h  <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable a Int32
getDict
    Maybe Int32
mi <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall k v.
(Eq k, Hashable k) =>
HashTable k v -> k -> IO (Maybe v)
H.lookup HashTable a Int32
h a
a
    IORef FreshAndReuse
st <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> IORef FreshAndReuse
getCounter
    case Maybe Int32
mi of
      Just Int32
i  -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do
#ifdef DEBUG
        modifyIORef' st $ over lensReuse (+ 1)
#endif
        forall (m :: * -> *) a. Monad m => a -> m a
return Int32
i
      Maybe Int32
Nothing -> do
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef FreshAndReuse
st forall a b. (a -> b) -> a -> b
$ forall i o. Lens' i o -> LensMap i o
over Lens' Int32 FreshAndReuse
lensFresh (forall a. Num a => a -> a -> a
+Int32
1)
        Int32
i <- S Int32
icodeP
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => HashTable k v -> k -> v -> IO ()
H.insert HashTable a Int32
h a
a Int32
i
        forall (m :: * -> *) a. Monad m => a -> m a
return Int32
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 => (Node -> R a) -> Int32 -> R a
vcase :: forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R a
valu = \Int32
ix -> do
    Memo
memo <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Memo
nodeMemo
    -- compute run-time representation of type a
    let aTyp :: TypeRep
aTyp = forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy a)
    -- to introduce sharing, see if we have seen a thing
    -- represented by ix before
    HashMap TypeRep U
slot <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray Memo
memo Int32
ix
    case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Hm.lookup TypeRep
aTyp HashMap TypeRep U
slot of
      -- yes, we have seen it before, use the version from memo
      Just (U a
u) -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. R a
malformed forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
u)
      -- no, it's new, so generate it via valu and insert it into memo
      Maybe U
Nothing    -> do
          a
v <- Node -> R a
valu forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int32
ix) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Array Int32 Node
nodeE
          forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray Memo
memo Int32
ix (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Hm.insert TypeRep
aTyp (forall a. Typeable a => a -> U
U a
v) HashMap TypeRep U
slot)
          forall (m :: * -> *) a. Monad m => a -> m a
return a
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 -> Products (Domains t) -> S [Int32]

instance IsBase t ~ 'True => ICODE t 'True where
  icodeArgs :: (IsBase t ~ 'True, All EmbPrj (Domains t)) =>
Proxy t -> Products (Domains t) -> S Node
icodeArgs Proxy t
_ Products (Domains t)
_  = forall (m :: * -> *) a. Monad m => a -> m a
return []

instance ICODE t (IsBase t) => ICODE (a -> t) 'False where
  icodeArgs :: (IsBase (a -> t) ~ 'False, All EmbPrj (Domains (a -> t))) =>
Proxy (a -> t) -> Products (Domains (a -> t)) -> S Node
icodeArgs Proxy (a -> t)
_ (a
a , Foldr (,) () (If (IsBase t) '[] (Domains' t))
as) = forall a. EmbPrj a => a -> S Int32
icode a
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ Int32
hd -> (Int32
hd forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t (b :: Bool).
(ICODE t b, IsBase t ~ b, All EmbPrj (Domains t)) =>
Proxy t -> Products (Domains t) -> S Node
icodeArgs (forall {k} (t :: k). Proxy t
Proxy :: Proxy t) Foldr (,) () (If (IsBase t) '[] (Domains' t))
as

-- | @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) => Currying (Domains t) (S Int32) =>
          All EmbPrj (Domains t) =>
          Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN :: forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
tag t
_ =
  forall (as :: [*]) b.
Currying as b =>
Proxy as -> Proxy b -> (Products as -> b) -> Arrows as b
currys (forall {k} (t :: k). Proxy t
Proxy :: Proxy (Domains t)) (forall {k} (t :: k). Proxy t
Proxy :: Proxy (S Int32)) forall a b. (a -> b) -> a -> b
$ \ Products (If (IsBase t) '[] (Domains' t))
args ->
  Node -> S Int32
icodeNode forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int32
tag forall a. a -> [a] -> [a]
:) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t (b :: Bool).
(ICODE t b, IsBase t ~ b, All EmbPrj (Domains t)) =>
Proxy t -> Products (Domains t) -> S Node
icodeArgs (forall {k} (t :: k). Proxy t
Proxy :: Proxy t) Products (If (IsBase t) '[] (Domains' t))
args

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

-- 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 -> Products (Constant Int32 (Domains t)) -> R (CoDomain t)

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

instance VALU t 'True where

  valuN' :: ('True ~ IsBase t, All EmbPrj (Domains t)) =>
t -> Products (Constant Int32 (Domains t)) -> R (CoDomain t)
valuN' t
c () = forall (m :: * -> *) a. Monad m => a -> m a
return t
c

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


instance VALU t (IsBase t) => VALU (a -> t) 'False where

  valuN' :: ('False ~ IsBase (a -> t), All EmbPrj (Domains (a -> t))) =>
(a -> t)
-> Products (Constant Int32 (Domains (a -> t)))
-> R (CoDomain (a -> t))
valuN' a -> t
c (Int32
a, Foldr
  (,)
  ()
  (Foldr'
     (ConsMap0 (Constant1 Int32)) '[] (If (IsBase t) '[] (Domains' t)))
as) = forall a. EmbPrj a => Int32 -> R a
value Int32
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ a
v -> forall t (b :: Bool).
(VALU t b, b ~ IsBase t, All EmbPrj (Domains t)) =>
t -> Products (Constant Int32 (Domains t)) -> R (CoDomain t)
valuN' (a -> t
c a
v) Foldr
  (,)
  ()
  (Foldr'
     (ConsMap0 (Constant1 Int32)) '[] (If (IsBase t) '[] (Domains' t)))
as

  valueArgs :: ('False ~ IsBase (a -> t),
 All EmbPrj (CoDomain (a -> t) : Domains (a -> t))) =>
Proxy (a -> t)
-> Node -> Maybe (Products (Constant Int32 (Domains (a -> t))))
valueArgs Proxy (a -> t)
_ Node
xs = case Node
xs of
    (Int32
x : Node
xs') -> (Int32
x,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t (b :: Bool).
(VALU t b, b ~ IsBase t, All EmbPrj (CoDomain t : Domains t)) =>
Proxy t -> Node -> Maybe (Products (Constant Int32 (Domains t)))
valueArgs (forall {k} (t :: k). Proxy t
Proxy :: Proxy t) Node
xs'
    Node
_         -> forall a. Maybe a
Nothing

{-# INLINE valuN #-}
valuN :: forall t. VALU t (IsBase t) =>
         Currying (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),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN t
f = forall (as :: [*]) b.
Currying as b =>
Proxy as -> Proxy b -> (Products as -> b) -> Arrows as b
currys (forall {k} (t :: k). Proxy t
Proxy :: Proxy (Constant Int32 (Domains t)))
                 (forall {k} (t :: k). Proxy t
Proxy :: Proxy (R (CoDomain t)))
                 (forall t (b :: Bool).
(VALU t b, b ~ IsBase t, All EmbPrj (Domains t)) =>
t -> Products (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 = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (If (IsBase t) t (CoDomain' t))
valu where
  valu :: Node -> R (If (IsBase t) t (CoDomain' t))
valu Node
int32s = case forall t (b :: Bool).
(VALU t b, b ~ IsBase t, All EmbPrj (CoDomain t : Domains t)) =>
Proxy t -> Node -> Maybe (Products (Constant Int32 (Domains t)))
valueArgs (forall {k} (t :: k). Proxy t
Proxy :: Proxy t) Node
int32s of
                  Maybe (Products (Constant Int32 (Domains t)))
Nothing -> forall a. R a
malformed
                  Just Products (Constant Int32 (Domains t))
vs -> forall t (b :: Bool).
(VALU t b, b ~ IsBase t, All EmbPrj (Domains t)) =>
t -> Products (Constant Int32 (Domains t)) -> R (CoDomain t)
valuN' t
t Products (Constant Int32 (Domains t))
vs