Safe Haskell | None |
---|
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 ByteStringSource
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 ByteStringSource
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.
decodeFile :: FilePath -> TCM (Maybe Interface)Source
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
class Typeable a => EmbPrj a Source