{-# 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 qualified Data.ByteString.Lazy as L
import Data.Hashable
import qualified Data.HashTable.IO as H
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.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]

-- | The type of hashtables used in this module.
--
-- A very limited amount of testing indicates that 'H.CuckooHashTable'
-- is somewhat slower than 'H.BasicHashTable', and that
-- 'H.LinearHashTable' and the hashtables from "Data.Hashtable" are
-- much slower.

#if defined(mingw32_HOST_OS) && defined(x86_64_HOST_ARCH)
type HashTable k v = H.CuckooHashTable k v
#else
type HashTable k v = H.BasicHashTable k v
#endif

-- | 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) f Int32 -> (Int32 -> FreshAndReuse) -> f FreshAndReuse
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) = (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@.
  , Dict -> HashTable AbsolutePath Int32
absPathD     :: !(HashTable AbsolutePath Int32) -- ^ Not written to interface file.
  }

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

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

-- | Univeral memo structure, to introduce sharing during decoding
type Memo = HashTable (Int32, TypeRep) U    -- (node index, type rep)

-- | 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 = TypeError -> ExceptT TypeError (StateT St IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> ExceptT TypeError (StateT St IO) a)
-> TypeError -> ExceptT TypeError (StateT St IO) a
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
    a -> S ()
forall a. Typeable a => a -> S ()
tickICode a
a
    a -> S Int32
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 = IO a -> R a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (a -> IO a
forall a. a -> IO a
evaluate (Int -> a
forall a. Enum a => Int -> a
toEnum (Int32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
i))) R a -> (SomeException -> R a) -> R a
forall (m :: * -> *) a.
MonadCatch m =>
m a -> (SomeException -> m a) -> m a
`catchAll` R a -> SomeException -> R a
forall a b. a -> b -> a
const R a
forall a. R a
malformed

  default icod_ :: (Enum a) => a -> S Int32
  icod_ = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return (Int32 -> S Int32) -> (a -> Int32) -> a -> S Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int32) -> (a -> Int) -> a -> Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Int
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
_ = 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
$ 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
forall {k} (t :: k). Proxy t
Proxy :: Proxy a))
    HashTable RealWorld String Int
hmap <- (Dict -> HashTable RealWorld String Int)
-> ReaderT Dict IO (HashTable RealWorld String Int)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable RealWorld String Int
Dict -> HashTable String Int
stats
    IO () -> S ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> S ()) -> IO () -> S ()
forall a b. (a -> b) -> a -> b
$ do
      Int
n <- Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (Maybe Int -> Int) -> IO (Maybe Int) -> IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashTable String Int -> String -> IO (Maybe Int)
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> k -> IO (Maybe v)
H.lookup HashTable RealWorld String Int
HashTable String Int
hmap String
key
      HashTable String Int -> String -> Int -> IO ()
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> k -> v -> IO ()
H.insert HashTable RealWorld String Int
HashTable String Int
hmap String
key (Int -> IO ()) -> Int -> IO ()
forall a b. (a -> b) -> a -> b
$! Int
n Int -> Int -> Int
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 (Get a -> Decoder a
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 ByteString -> [ByteString] -> [ByteString]
forall a. a -> [a] -> [a]
: [ByteString]
ss), ByteOffset
n ByteOffset -> ByteOffset -> ByteOffset
forall a. Num a => a -> a -> a
+ ByteOffset
n')
    feed (B.Fail ByteString
_ ByteOffset
_ String
err) [ByteString]
_     = String -> (a, ByteString, ByteOffset)
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 (Maybe ByteString -> Decoder a) -> Maybe ByteString -> Decoder a
forall a b. (a -> b) -> a -> b
$ ByteString -> Maybe ByteString
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 Maybe ByteString
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 RealWorld k Int32
d <- (Dict -> HashTable RealWorld k Int32)
-> ReaderT Dict IO (HashTable RealWorld k Int32)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable RealWorld k Int32
Dict -> HashTable k Int32
dict
  IORef FreshAndReuse
c <- (Dict -> IORef FreshAndReuse)
-> ReaderT Dict IO (IORef FreshAndReuse)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> IORef FreshAndReuse
counter
  IO Int32 -> S Int32
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
    Maybe Int32
mi <- HashTable k Int32 -> k -> IO (Maybe Int32)
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> k -> IO (Maybe v)
H.lookup HashTable RealWorld k Int32
HashTable k Int32
d k
key
    case Maybe Int32
mi of
      Just Int32
i  -> do
#ifdef DEBUG
        modifyIORef' c $ over lensReuse (+1)
#endif
        Int32 -> IO Int32
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
i
      Maybe Int32
Nothing -> do
        Int32
fresh <- (FreshAndReuse -> Lens' Int32 FreshAndReuse -> Int32
forall o i. o -> Lens' i o -> i
^.Lens' Int32 FreshAndReuse
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' Int32 FreshAndReuse -> LensMap Int32 FreshAndReuse
forall i o. Lens' i o -> LensMap i o
over Lens' Int32 FreshAndReuse
lensFresh (Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+Int32
1)
        HashTable k Int32 -> k -> Int32 -> IO ()
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> k -> v -> IO ()
H.insert HashTable RealWorld k Int32
HashTable k Int32
d k
key Int32
fresh
        Int32 -> IO Int32
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 RealWorld Integer Int32
d <- (Dict -> HashTable RealWorld Integer Int32)
-> ReaderT Dict IO (HashTable RealWorld Integer Int32)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable RealWorld Integer Int32
Dict -> HashTable Integer Int32
integerD
  IORef FreshAndReuse
c <- (Dict -> IORef FreshAndReuse)
-> ReaderT Dict IO (IORef FreshAndReuse)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> IORef FreshAndReuse
integerC
  IO Int32 -> S Int32
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
    Maybe Int32
mi <- HashTable Integer Int32 -> Integer -> IO (Maybe Int32)
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> k -> IO (Maybe v)
H.lookup HashTable RealWorld Integer Int32
HashTable Integer Int32
d Integer
key
    case Maybe Int32
mi of
      Just Int32
i  -> do
#ifdef DEBUG
        modifyIORef' c $ over lensReuse (+1)
#endif
        Int32 -> IO Int32
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
i
      Maybe Int32
Nothing -> do
        Int32
fresh <- (FreshAndReuse -> Lens' Int32 FreshAndReuse -> Int32
forall o i. o -> Lens' i o -> i
^.Lens' Int32 FreshAndReuse
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' Int32 FreshAndReuse -> LensMap Int32 FreshAndReuse
forall i o. Lens' i o -> LensMap i o
over Lens' Int32 FreshAndReuse
lensFresh (Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+Int32
1)
        HashTable Integer Int32 -> Integer -> Int32 -> IO ()
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> k -> v -> IO ()
H.insert HashTable RealWorld Integer Int32
HashTable Integer Int32
d Integer
key Int32
fresh
        Int32 -> IO Int32
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
fresh

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

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

icodeNode :: Node -> S Int32
icodeNode :: Node -> S Int32
icodeNode Node
key = do
  HashTable RealWorld Node Int32
d <- (Dict -> HashTable RealWorld Node Int32)
-> ReaderT Dict IO (HashTable RealWorld Node Int32)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable RealWorld Node Int32
Dict -> HashTable Node Int32
nodeD
  IORef FreshAndReuse
c <- (Dict -> IORef FreshAndReuse)
-> ReaderT Dict IO (IORef FreshAndReuse)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> IORef FreshAndReuse
nodeC
  IO Int32 -> S Int32
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
    Maybe Int32
mi <- HashTable Node Int32 -> Node -> IO (Maybe Int32)
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> k -> IO (Maybe v)
H.lookup HashTable RealWorld Node Int32
HashTable Node Int32
d Node
key
    case Maybe Int32
mi of
      Just Int32
i  -> do
#ifdef DEBUG
        modifyIORef' c $ over lensReuse (+1)
#endif
        Int32 -> IO Int32
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
i
      Maybe Int32
Nothing -> do
        Int32
fresh <- (FreshAndReuse -> Lens' Int32 FreshAndReuse -> Int32
forall o i. o -> Lens' i o -> i
^.Lens' Int32 FreshAndReuse
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' Int32 FreshAndReuse -> LensMap Int32 FreshAndReuse
forall i o. Lens' i o -> LensMap i o
over Lens' Int32 FreshAndReuse
lensFresh (Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+Int32
1)
        HashTable Node Int32 -> Node -> Int32 -> IO ()
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> k -> v -> IO ()
H.insert HashTable RealWorld Node Int32
HashTable Node Int32
d Node
key Int32
fresh
        Int32 -> IO Int32
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 RealWorld a Int32
h  <- (Dict -> HashTable RealWorld a Int32)
-> ReaderT Dict IO (HashTable RealWorld a Int32)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable RealWorld a Int32
Dict -> HashTable a Int32
getDict
    Maybe Int32
mi <- IO (Maybe Int32) -> ReaderT Dict IO (Maybe Int32)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe Int32) -> ReaderT Dict IO (Maybe Int32))
-> IO (Maybe Int32) -> ReaderT Dict IO (Maybe Int32)
forall a b. (a -> b) -> a -> b
$ HashTable a Int32 -> a -> IO (Maybe Int32)
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> k -> IO (Maybe v)
H.lookup HashTable RealWorld a Int32
HashTable a Int32
h a
a
    IORef FreshAndReuse
st <- (Dict -> IORef FreshAndReuse)
-> ReaderT Dict IO (IORef FreshAndReuse)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> IORef FreshAndReuse
getCounter
    case Maybe Int32
mi of
      Just Int32
i  -> IO Int32 -> S Int32
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
        modifyIORef' st $ over lensReuse (+ 1)
#endif
        Int32 -> IO Int32
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
i
      Maybe Int32
Nothing -> do
        IO () -> S ()
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' Int32 FreshAndReuse -> LensMap Int32 FreshAndReuse
forall i o. Lens' i o -> LensMap i o
over Lens' Int32 FreshAndReuse
lensFresh (Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+Int32
1)
        Int32
i <- S Int32
icodeP
        IO () -> S ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> S ()) -> IO () -> S ()
forall a b. (a -> b) -> a -> b
$ HashTable a Int32 -> a -> Int32 -> IO ()
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> k -> v -> IO ()
H.insert HashTable RealWorld a Int32
HashTable a Int32
h a
a Int32
i
        Int32 -> S Int32
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
    HashTable RealWorld (Int32, TypeRep) U
memo <- (St -> HashTable RealWorld (Int32, TypeRep) U)
-> ExceptT
     TypeError (StateT St IO) (HashTable RealWorld (Int32, TypeRep) U)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> HashTable RealWorld (Int32, TypeRep) U
St -> Memo
nodeMemo
    -- compute run-time representation of type a
    let aTyp :: TypeRep
aTyp = 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
    Maybe U
maybeU <- IO (Maybe U) -> ExceptT TypeError (StateT St IO) (Maybe U)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe U) -> ExceptT TypeError (StateT St IO) (Maybe U))
-> IO (Maybe U) -> ExceptT TypeError (StateT St IO) (Maybe U)
forall a b. (a -> b) -> a -> b
$ Memo -> (Int32, TypeRep) -> IO (Maybe U)
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> k -> IO (Maybe v)
H.lookup HashTable RealWorld (Int32, TypeRep) U
Memo
memo (Int32
ix, TypeRep
aTyp)
    case Maybe U
maybeU of
      -- yes, we have seen it before, use the version from memo
      Just (U a
u) -> R a -> (a -> R a) -> Maybe a -> R a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe R a
forall a. R a
malformed a -> R a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Maybe a
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 (Node -> R a)
-> (Array Int32 Node -> Node) -> Array Int32 Node -> R a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Array Int32 Node -> Int32 -> Node
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int32
ix) (Array Int32 Node -> R a)
-> ExceptT TypeError (StateT St IO) (Array Int32 Node) -> R a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (St -> Array Int32 Node)
-> ExceptT TypeError (StateT St IO) (Array Int32 Node)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Array Int32 Node
nodeE
          IO () -> ExceptT TypeError (StateT St IO) ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ExceptT TypeError (StateT St IO) ())
-> IO () -> ExceptT TypeError (StateT St IO) ()
forall a b. (a -> b) -> a -> b
$ Memo -> (Int32, TypeRep) -> U -> IO ()
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> k -> v -> IO ()
H.insert HashTable RealWorld (Int32, TypeRep) U
Memo
memo (Int32
ix, TypeRep
aTyp) (a -> U
forall a. Typeable a => a -> U
U a
v)
          a -> R a
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)
_  = Node -> S Node
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) = a -> S Int32
forall a. EmbPrj a => a -> S Int32
icode a
a S Int32 -> (Int32 -> S Node) -> S Node
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ Int32
hd -> (Int32
hd Int32 -> Node -> Node
forall a. a -> [a] -> [a]
:) (Node -> Node) -> S Node -> S Node
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy t -> Products (Domains t) -> S Node
forall t (b :: Bool).
(ICODE t b, IsBase t ~ b, All EmbPrj (Domains t)) =>
Proxy t -> Products (Domains t) -> S Node
icodeArgs (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t) Products (Domains 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
_ =
  Proxy (If (IsBase t) '[] (Domains' t))
-> Proxy (S Int32)
-> (Products (If (IsBase t) '[] (Domains' t)) -> S Int32)
-> Arrows (If (IsBase t) '[] (Domains' t)) (S Int32)
forall (as :: [*]) b.
Currying as b =>
Proxy as -> Proxy b -> (Products as -> b) -> Arrows as b
currys (Proxy (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)) ((Products (If (IsBase t) '[] (Domains' t)) -> S Int32)
 -> Arrows (If (IsBase t) '[] (Domains' t)) (S Int32))
-> (Products (If (IsBase t) '[] (Domains' t)) -> S Int32)
-> Arrows (If (IsBase t) '[] (Domains' t)) (S Int32)
forall a b. (a -> b) -> a -> b
$ \ Products (If (IsBase t) '[] (Domains' t))
args ->
  Node -> S Int32
icodeNode (Node -> S Int32) -> (Node -> Node) -> Node -> S Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int32
tag Int32 -> Node -> Node
forall a. a -> [a] -> [a]
:) (Node -> S Int32) -> S Node -> S Int32
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Proxy t -> Products (Domains t) -> S Node
forall t (b :: Bool).
(ICODE t b, IsBase t ~ b, All EmbPrj (Domains t)) =>
Proxy t -> Products (Domains t) -> S Node
icodeArgs (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t) Products (Domains 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
_ =
  Proxy (If (IsBase t) '[] (Domains' t))
-> Proxy (S Int32)
-> (Products (If (IsBase t) '[] (Domains' t)) -> S Int32)
-> Arrows (If (IsBase t) '[] (Domains' t)) (S Int32)
forall (as :: [*]) b.
Currying as b =>
Proxy as -> Proxy b -> (Products as -> b) -> Arrows as b
currys (Proxy (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)) ((Products (If (IsBase t) '[] (Domains' t)) -> S Int32)
 -> Arrows (If (IsBase t) '[] (Domains' t)) (S Int32))
-> (Products (If (IsBase t) '[] (Domains' t)) -> S Int32)
-> Arrows (If (IsBase t) '[] (Domains' t)) (S Int32)
forall a b. (a -> b) -> a -> b
$ \ Products (If (IsBase t) '[] (Domains' t))
args ->
  Node -> S Int32
icodeNode (Node -> S Int32) -> S Node -> S Int32
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Proxy t -> Products (Domains t) -> S Node
forall t (b :: Bool).
(ICODE t b, IsBase t ~ b, All EmbPrj (Domains t)) =>
Proxy t -> Products (Domains t) -> S Node
icodeArgs (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t) Products (Domains 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 () = t -> ExceptT TypeError (StateT St IO) t
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
    [] -> () -> Maybe ()
forall a. a -> Maybe a
Just ()
    Node
_  -> Maybe (Products (Constant Int32 (Domains t)))
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) = Int32 -> R a
forall a. EmbPrj a => Int32 -> R a
value Int32
a R a
-> (a
    -> ExceptT
         TypeError (StateT St IO) (If (IsBase t) t (CoDomain' t)))
-> ExceptT TypeError (StateT St IO) (If (IsBase t) t (CoDomain' t))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ a
v -> t -> Products (Constant Int32 (Domains t)) -> 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' (a -> t
c a
v) Products (Constant Int32 (Domains t))
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,) (Foldr
   (,)
   ()
   (Foldr'
      (ConsMap0 (Constant1 Int32)) '[] (If (IsBase t) '[] (Domains' t)))
 -> (Int32,
     Foldr
       (,)
       ()
       (Foldr'
          (ConsMap0 (Constant1 Int32))
          '[]
          (If (IsBase t) '[] (Domains' t)))))
-> Maybe
     (Foldr
        (,)
        ()
        (Foldr'
           (ConsMap0 (Constant1 Int32)) '[] (If (IsBase t) '[] (Domains' t))))
-> Maybe
     (Int32,
      Foldr
        (,)
        ()
        (Foldr'
           (ConsMap0 (Constant1 Int32)) '[] (If (IsBase t) '[] (Domains' t))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy t -> Node -> Maybe (Products (Constant Int32 (Domains t)))
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 (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t) Node
xs'
    Node
_         -> Maybe (Products (Constant Int32 (Domains (a -> t))))
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 = Proxy
  (Foldr'
     (ConsMap0 (Constant1 Int32)) '[] (If (IsBase t) '[] (Domains' t)))
-> Proxy (R (If (IsBase t) t (CoDomain' t)))
-> (Products
      (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.
Currying as b =>
Proxy as -> Proxy b -> (Products as -> b) -> Arrows as b
currys (Proxy (Constant Int32 (Domains t))
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Constant Int32 (Domains t)))
                 (Proxy (R (CoDomain t))
forall {k} (t :: k). Proxy t
Proxy :: Proxy (R (CoDomain t)))
                 (t -> Products (Constant Int32 (Domains t)) -> 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 = (Node -> R (If (IsBase t) t (CoDomain' t)))
-> Int32 -> R (If (IsBase t) t (CoDomain' 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 Proxy t -> Node -> Maybe (Products (Constant Int32 (Domains t)))
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 (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t) Node
int32s of
                  Maybe (Products (Constant Int32 (Domains t)))
Nothing -> R (If (IsBase t) t (CoDomain' t))
forall a. R a
malformed
                  Just Products (Constant Int32 (Domains t))
vs -> t
-> Products (Constant Int32 (Domains t))
-> ExceptT TypeError (StateT St IO) (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
t Products (Constant Int32 (Domains t))
vs