Safe Haskell | None |
---|---|
Language | Haskell98 |
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 Source #
Encodes something. To ensure relocatability file paths in positions are replaced with module names.
encodeFile :: FilePath -> Interface -> TCM () Source #
Encodes something. To ensure relocatability file paths in positions are replaced with module names.
encodeInterface :: Interface -> TCM ByteString Source #
decode :: EmbPrj a => ByteString -> TCM (Maybe a) Source #
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) Source #
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) Source #