Agda.TypeChecking.Serialise.Base

Constructor tag (maybe omitted) and argument indices.

Association lists mapping TypeRep fingerprints to values. In some cases values with different types have the same serialized representation. This structure disambiguates them.

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

Two QNames are equal if their QNameId is equal.

Computing a qualified names composed ID.

State of the the encoder.

Creates an empty dictionary.

Univeral memo structure, to introduce sharing during decoding

State of the decoder.

Monad used by the encoder.

Monad used by the decoder.

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

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

The actual logic of tickICode is cold code, so it's out-of-line, to decrease code size and avoid cache pollution.

Increase entry for a in stats.

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.

icode only if thing has not seen before.

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.

icodeArgs proxy (a1, ..., an) maps icode over a1, ..., an and returns the corresponding list of 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' is the same as icodeN except that there is no tag