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

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.

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.

Instances

EmbPrj SerialisedRange

Methods

icode :: SerialisedRange -> S Int32

icod_ :: SerialisedRange -> S Int32

value :: Int32 -> R SerialisedRange

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

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

class ICODE t b where

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

Minimal complete definition

icodeArgs

Methods

icodeArgs :: IsBase t ~ b => All EmbPrj (Domains t) => Proxy t -> Products (Domains t) -> S [Int32]

Instances

(~) Bool (IsBase t) True => ICODE t True

Methods

icodeArgs :: Proxy * t -> Products (Domains t) -> S [Int32]

ICODE t (IsBase t) => ICODE (a -> t) False

Methods

icodeArgs :: Proxy * (a -> t) -> Products (Domains (a -> 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 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]

icodeN' :: forall t. ICODE t (IsBase t) => Currying (Domains t) (S Int32) => All EmbPrj (Domains t) => t -> Arrows (Domains t) (S Int32)

icodeN' is the same as icodeN except that there is no tag

class VALU t b where

Minimal complete definition

valuN', valueArgs

Methods

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)))

Instances

VALU t True

Methods

valuN' :: t -> Products (Constant * * Int32 (Domains t)) -> R (CoDomain t)

valueArgs :: Proxy * t -> Node -> Maybe (Products (Constant * * Int32 (Domains t)))

VALU t (IsBase t) => VALU (a -> t) False

Methods

valuN' :: (a -> t) -> Products (Constant * * Int32 (Domains (a -> t))) -> R (CoDomain (a -> t))

valueArgs :: Proxy * (a -> t) -> Node -> Maybe (Products (Constant * * Int32 (Domains (a -> 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))

valueN :: forall t. VALU t (IsBase t) => All EmbPrj (CoDomain t ': Domains t) => t -> Int32 -> R (CoDomain t)