Agda.TypeChecking.Serialise.Base

Documentation

type Node = [Int32]

Constructor tag (maybe omitted) and argument indices.

type HashTable k v = BasicHashTable k v

The type of hashtables used in this module.

A very limited amount of testing indicates that CuckooHashTable is somewhat slower than BasicHashTable, and that LinearHashTable and the hashtables from Data.Hashtable are much slower.

data FreshAndReuse

Structure providing fresh identifiers for hash map and counting hash map hits (i.e. when no fresh identifier required).

Constructors

FreshAndReuse

Fields

farFresh :: !Int32

Number of hash map misses.

farReuse :: !Int32

Number of hash map hits.

farEmpty :: FreshAndReuse

lensFresh :: Lens' Int32 FreshAndReuse

lensReuse :: Lens' Int32 FreshAndReuse

type QNameId = [NameId]

Two QNames are equal if their QNameId is equal.

qnameId :: QName -> QNameId

Computing a qualified names composed ID.

data Dict

State of the the encoder.

Constructors

Dict

Fields

nodeD :: !(HashTable Node Int32)

Written to interface file.

stringD :: !(HashTable String Int32)

Written to interface file.

bstringD :: !(HashTable ByteString Int32)

Written to interface file.

integerD :: !(HashTable Integer Int32)

Written to interface file.

doubleD :: !(HashTable Double Int32)

Written to interface file. Dicitionaries which are not serialized, but provide short cuts to speed up serialization:

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.

nameD :: !(HashTable NameId Int32)

Not written to interface file.

qnameD :: !(HashTable QNameId Int32)

Not written to interface file. Fresh UIDs and reuse statistics:

nodeC :: !(IORef FreshAndReuse)

stringC :: !(IORef FreshAndReuse)

bstringC :: !(IORef FreshAndReuse)

integerC :: !(IORef FreshAndReuse)

doubleC :: !(IORef FreshAndReuse)

termC :: !(IORef FreshAndReuse)

nameC :: !(IORef FreshAndReuse)

qnameC :: !(IORef FreshAndReuse)

stats :: !(HashTable String Int)

collectStats :: Bool

If True collect in stats the quantities of calls to icode for each Typeable a.

absPathD :: !(HashTable AbsolutePath Int32)

Not written to interface file.

emptyDict

Arguments

:: Bool

Collect statistics for icode calls?

-> IO Dict

Creates an empty dictionary.

data U

Universal type, wraps everything.

Constructors

forall a . Typeable a => U !a

type Memo = HashTable (Int32, TypeRep) U

Univeral memo structure, to introduce sharing during decoding

data St

State of the decoder.

Constructors

St

Fields

nodeE :: !(Array Int32 Node)

Obtained from interface file.

stringE :: !(Array Int32 String)

Obtained from interface file.

bstringE :: !(Array Int32 ByteString)

Obtained from interface file.

integerE :: !(Array Int32 Integer)

Obtained from interface file.

doubleE :: !(Array Int32 Double)

Obtained from interface file.

nodeMemo :: !Memo

Created and modified by decoder. Used to introduce sharing while deserializing objects.

modFile :: !ModuleToSource

Maps module names to file names. Constructed by the decoder.

includes :: [AbsolutePath]

The include directories.

mkShared :: Term -> Term

type S a = ReaderT Dict IO a

Monad used by the encoder.

type R a = ExceptT TypeError (StateT St IO) a

Monad used by the decoder.

TCM is not used because the associated overheads would make decoding slower.

malformed :: R a

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

class Typeable a => EmbPrj a where

Minimal complete definition

icod_, value

Methods

icode

Arguments

:: a

-> S Int32

Serialization (wrapper).

icod_

Arguments

:: a

-> S Int32

Serialization (worker).

value

Arguments

:: Int32

-> R a

Deserialization.

tickICode :: forall a. Typeable a => a -> S ()

Increase entry for a in stats.

runGetState :: Get a -> ByteString -> ByteOffset -> (a, ByteString, ByteOffset)

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.

icodeX :: (Eq k, Hashable k) => (Dict -> HashTable k Int32) -> (Dict -> IORef FreshAndReuse) -> k -> S Int32

icodeInteger :: Integer -> S Int32

icodeDouble :: Double -> S Int32

icodeString :: String -> S Int32

icodeN :: Node -> S Int32

icodeMemo

Arguments

:: (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.

icode only if thing has not seen before.

vcase :: forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a

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.

icode0 :: Int32 -> S Int32

icode1 :: EmbPrj a => Int32 -> a -> S Int32

icode2 :: (EmbPrj a, EmbPrj b) => Int32 -> a -> b -> S Int32

icode3 :: (EmbPrj a, EmbPrj b, EmbPrj c) => Int32 -> a -> b -> c -> S Int32

icode4 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d) => Int32 -> a -> b -> c -> d -> S Int32

icode5 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e) => Int32 -> a -> b -> c -> d -> e -> S Int32

icode6 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f) => Int32 -> a -> b -> c -> d -> e -> f -> S Int32

icode7 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g) => Int32 -> a -> b -> c -> d -> e -> f -> g -> S Int32

icode8 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h) => Int32 -> a -> b -> c -> d -> e -> f -> g -> h -> S Int32

icode9 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i) => Int32 -> a -> b -> c -> d -> e -> f -> g -> h -> i -> S Int32

icode10 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j) => Int32 -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> S Int32

icode11 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j, EmbPrj k) => Int32 -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> S Int32

icode12 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j, EmbPrj k, EmbPrj l) => Int32 -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> S Int32

icode13 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j, EmbPrj k, EmbPrj l, EmbPrj m) => Int32 -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> S Int32

icode14 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j, EmbPrj k, EmbPrj l, EmbPrj m, EmbPrj n) => Int32 -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> S Int32

icode15 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j, EmbPrj k, EmbPrj l, EmbPrj m, EmbPrj n, EmbPrj o) => Int32 -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> S Int32

icode0' :: S Int32

icode1' :: EmbPrj a => a -> S Int32

icode2' :: (EmbPrj a, EmbPrj b) => a -> b -> S Int32

icode3' :: (EmbPrj a, EmbPrj b, EmbPrj c) => a -> b -> c -> S Int32

icode4' :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d) => a -> b -> c -> d -> S Int32

icode5' :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e) => a -> b -> c -> d -> e -> S Int32

icode6' :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f) => a -> b -> c -> d -> e -> f -> S Int32

icode7' :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g) => a -> b -> c -> d -> e -> f -> g -> S Int32

icode8' :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h) => a -> b -> c -> d -> e -> f -> g -> h -> S Int32

icode9' :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i) => a -> b -> c -> d -> e -> f -> g -> h -> i -> S Int32

icode10' :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j) => a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> S Int32

icode11' :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j, EmbPrj k) => a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> S Int32

icode12' :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j, EmbPrj k, EmbPrj l) => a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> S Int32

icode13' :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j, EmbPrj k, EmbPrj l, EmbPrj m) => a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> S Int32

icode14' :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j, EmbPrj k, EmbPrj l, EmbPrj m, EmbPrj n) => a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> S Int32

valu0 :: a -> R a

valu1 :: EmbPrj a => (a -> b) -> Int32 -> R b

valu2 :: (EmbPrj a, EmbPrj b) => (a -> b -> c) -> Int32 -> Int32 -> R c

valu3 :: (EmbPrj a, EmbPrj b, EmbPrj c) => (a -> b -> c -> d) -> Int32 -> Int32 -> Int32 -> R d

valu4 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d) => (a -> b -> c -> d -> e) -> Int32 -> Int32 -> Int32 -> Int32 -> R e

valu5 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e) => (a -> b -> c -> d -> e -> f) -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> R f

valu6 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f) => (a -> b -> c -> d -> e -> f -> g) -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> R g

valu7 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g) => (a -> b -> c -> d -> e -> f -> g -> h) -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> R h

valu8 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h) => (a -> b -> c -> d -> e -> f -> g -> h -> i) -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> R i

valu9 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> R j

valu10 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> R k

valu11 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j, EmbPrj k) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> R l

valu12 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j, EmbPrj k, EmbPrj l) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> R m

valu13 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j, EmbPrj k, EmbPrj l, EmbPrj m) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n) -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> R n

valu14 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j, EmbPrj k, EmbPrj l, EmbPrj m, EmbPrj n) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o) -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> R o

valu15 :: (EmbPrj a, EmbPrj b, EmbPrj c, EmbPrj d, EmbPrj e, EmbPrj f, EmbPrj g, EmbPrj h, EmbPrj i, EmbPrj j, EmbPrj k, EmbPrj l, EmbPrj m, EmbPrj n, EmbPrj o) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p) -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> R p