Agda.TypeChecking.Serialise

Structure-sharing serialisation of Agda interface files.

Documentation

encode :: EmbPrj a => a -> TCM ByteString

Encodes something. To ensure relocatability file paths in positions are replaced with module names.

encodeFile :: FilePath -> Interface -> TCM ()

Encodes something. To ensure relocatability file paths in positions are replaced with module names.

encodeInterface :: Interface -> TCM ByteString

decode :: EmbPrj a => ByteString -> TCM (Maybe a)

Decodes something. The result depends on the include path.

Returns Nothing if the input does not start with the right magic number or some other decoding error is encountered.

decodeFile :: FilePath -> TCM (Maybe Interface)

decodeInterface :: ByteString -> TCM (Maybe Interface)

Decodes something. The result depends on the include path.

Returns Nothing if the file does not start with the right magic number or some other decoding error is encountered.

decodeHashes :: ByteString -> Maybe (Hash, Hash)

class Typeable a => EmbPrj a

Minimal complete definition

icod_, value

Instances

EmbPrj SerialisedRange

Methods

icode :: SerialisedRange -> S Int32

icod_ :: SerialisedRange -> S Int32

value :: Int32 -> R SerialisedRange