Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Serialise
Description
Structure-sharing serialisation of Agda interface files.
- encode :: EmbPrj a => a -> TCM ByteString
- encodeFile :: FilePath -> Interface -> TCM ()
- encodeInterface :: Interface -> TCM ByteString
- decode :: EmbPrj a => ByteString -> TCM (Maybe a)
- decodeFile :: FilePath -> TCM (Maybe Interface)
- decodeInterface :: ByteString -> TCM (Maybe Interface)
- decodeHashes :: ByteString -> Maybe (Hash, Hash)
- class Typeable a => EmbPrj a
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.
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) #