Safe Haskell | None |
---|
Agda.TypeChecking.Serialise
Description
Structure-sharing serialisation of Agda interface files.
- encode :: EmbPrj a => a -> TCM ByteString
- encodeFile :: EmbPrj a => FilePath -> a -> TCM ()
- decode :: EmbPrj a => ByteString -> TCM (Maybe a)
- decodeFile :: EmbPrj a => FilePath -> TCM (Maybe a)
- 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.
Encodes something. To ensure relocatability file paths in positions are replaced with module names.
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 :: EmbPrj a => FilePath -> TCM (Maybe a)
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.
Instances