| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Serialise

Description
Structure-sharing serialisation of Agda interface files.
Synopsis

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 Data 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 | Source

:: EmbPrj a |
=> FilePath | The encoded data is written to this file.
-> a | Something.
-> TCM () |
Encodes something. To ensure relocatability file paths in positions are replaced with module names.

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 :: EmbPrj a => FilePath -> TCM (Maybe a) | 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.

class Data a => EmbPrj a | Source

Instances

EmbPrj Bool
EmbPrj Char
EmbPrj Double
EmbPrj Int
EmbPrj Integer
EmbPrj String
EmbPrj Permutation
EmbPrj AbsolutePath
EmbPrj Range
EmbPrj Interval
EmbPrj Position
EmbPrj Literal
EmbPrj NameId
EmbPrj IsAbstract
EmbPrj Access
EmbPrj Hiding
EmbPrj Induction
EmbPrj TopLevelModuleName
EmbPrj QName
EmbPrj NamePart
EmbPrj Name
EmbPrj Precedence
EmbPrj Fixity
EmbPrj ModuleName
EmbPrj QName
EmbPrj Name
EmbPrj MetaId
EmbPrj Pattern
EmbPrj ClauseBody
EmbPrj Clause
EmbPrj Telescope
EmbPrj Sort
EmbPrj Type
EmbPrj Term
EmbPrj AbstractModule
EmbPrj AbstractName
EmbPrj KindOfName
EmbPrj NameSpace
EmbPrj ScopeInfo
EmbPrj Scope
EmbPrj Range
EmbPrj MetaInfo
EmbPrj OtherAspect
EmbPrj NameKind
EmbPrj Aspect
EmbPrj CtxId
EmbPrj MutualId
EmbPrj TermHead
EmbPrj FunctionInverse
EmbPrj Delayed
EmbPrj Defn
EmbPrj Occurrence
EmbPrj Polarity
EmbPrj HaskellRepresentation
EmbPrj Definition
EmbPrj DisplayTerm
EmbPrj DisplayForm
EmbPrj Section
EmbPrj Signature
EmbPrj Interface
EmbPrj a => EmbPrj ([] a)
EmbPrj a => EmbPrj (Maybe a)
(Ord a, EmbPrj a) => EmbPrj (Set a)
EmbPrj a => EmbPrj (Arg a)
EmbPrj a => EmbPrj (Abs a)
EmbPrj a => EmbPrj (Builtin a)
EmbPrj a => EmbPrj (Open a)
(EmbPrj a, EmbPrj b) => EmbPrj ((,) a b)
(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b)
(EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj ((,,) a b c)

Produced by Haddock version 2.4.2