Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

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 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.

encodeFile

Arguments

:: 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)

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.

class Typeable a => EmbPrj a

Instances

EmbPrj Bool |
EmbPrj Char |
EmbPrj Double |
EmbPrj Int |
EmbPrj Int32 |
EmbPrj Integer |
EmbPrj String |
EmbPrj () |
EmbPrj Permutation |
EmbPrj AbsolutePath |
EmbPrj Range |
EmbPrj Interval |
EmbPrj Position |
EmbPrj NameId |
EmbPrj IsAbstract |
EmbPrj Access |
EmbPrj Relevance |
EmbPrj Hiding |
EmbPrj Induction |
EmbPrj Delayed |
EmbPrj MemberId |
EmbPrj GlobalId |
EmbPrj LocalId |
EmbPrj Exp |
EmbPrj TopLevelModuleName |
EmbPrj QName |
EmbPrj NamePart |
EmbPrj Name |
EmbPrj Range |
EmbPrj GenPart |
EmbPrj Precedence |
EmbPrj Fixity |
EmbPrj Fixity' |
EmbPrj AmbiguousQName |
EmbPrj ModuleName |
EmbPrj QName |
EmbPrj Name |
EmbPrj Literal |
EmbPrj CompressedFile |
EmbPrj MetaInfo |
EmbPrj OtherAspect |
EmbPrj NameKind |
EmbPrj Aspect |
EmbPrj AbstractModule |
EmbPrj AbstractName |
EmbPrj KindOfName |
EmbPrj NameSpace |
EmbPrj ScopeInfo |
EmbPrj NameSpaceId |
EmbPrj Scope |
EmbPrj Pattern |
EmbPrj ClauseBody |
EmbPrj Clause |
EmbPrj LevelAtom |
EmbPrj PlusLevel |
EmbPrj Level |
EmbPrj Sort |
EmbPrj Telescope |
EmbPrj Type |
EmbPrj Term |
EmbPrj EInterface |
EmbPrj InjectiveFun |
EmbPrj Relevance |
EmbPrj Forced |
EmbPrj Tag |
EmbPrj CompiledClauses |
EmbPrj Pattern |
EmbPrj TypedBinding |
EmbPrj TypedBindings |
EmbPrj LamBinding |
EmbPrj LetBinding |
EmbPrj Expr |
EmbPrj CtxId |
EmbPrj MutualId |
EmbPrj TermHead |
EmbPrj FunctionInverse |
EmbPrj Defn |
EmbPrj Occurrence |
EmbPrj CompiledRepresentation |
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 (Dom a) |
EmbPrj a => EmbPrj (Abs a) |
EmbPrj a => EmbPrj (Case a) |
EmbPrj a => EmbPrj (WithArity 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) |
(Eq k, Hashable k, EmbPrj k, EmbPrj v) => EmbPrj (HashMap k v) |
(EmbPrj s, EmbPrj t) => EmbPrj (Named s t) |
(EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj (a, b, c) |