| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Serialise
Description
Structure-sharing serialisation of Agda interface files.
Synopsis
- type InterfacePrefix = (Hash, Hash, Word64)
- type Encoded = (Word32, Array Node, Array String, Array Text, Array Text, Array Integer, Array VarSet, Array Double)
- encode :: EmbPrj a => a -> TCM Encoded
- encodeFile :: FilePath -> Interface -> TCM Interface
- decode :: EmbPrj a => Encoded -> MaybeT TCM a
- decodeFile :: FilePath -> TCM (Maybe Interface)
- decodeInterface :: ByteString -> MaybeT TCM Interface
- deserializeInterface :: ByteString -> MaybeT TCM Encoded
- deserializeHashes :: ByteString -> IO (Maybe (Hash, Hash))
Documentation
type Encoded = (Word32, Array Node, Array String, Array Text, Array Text, Array Integer, Array VarSet, Array Double) Source #
Hash-consed encoding of a value.
encode :: EmbPrj a => a -> TCM Encoded Source #
Encodes something as a hash-consed tuple of arrays. To ensure relocatability, file paths in positions are replaced with module names.
encodeFile :: FilePath -> Interface -> TCM Interface Source #
Encodes an interface. To ensure relocatability file paths in positions are replaced with module names. A hash-consed and compacted interface is returned.
decode :: EmbPrj a => Encoded -> MaybeT TCM a Source #
Decode a hash-consed value. The result depends on the include path.
decodeInterface :: ByteString -> MaybeT TCM Interface Source #
Decode an interface from a bytestring. We check the stored interface version against the current interface version, but we don't do anything with the hash prefix.
deserializeHashes :: ByteString -> IO (Maybe (Hash, Hash)) Source #