Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Serialise

Description

Structure-sharing serialisation of Agda interface files.

Synopsis

Documentation

encode :: EmbPrj a => a -> TCM ByteString Source

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

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

Minimal complete definition

icod_, value

Instances

EmbPrj Bool Source
EmbPrj Char Source
EmbPrj Double Source
EmbPrj Int Source
EmbPrj Int32 Source
EmbPrj Integer Source
EmbPrj Word64 Source
EmbPrj String Source
EmbPrj () Source
EmbPrj Fixity' Source
EmbPrj AbsolutePath Source
EmbPrj Name Source
EmbPrj Range Source
EmbPrj Interval Source
EmbPrj Position Source
EmbPrj NameId Source
EmbPrj IsAbstract Source
EmbPrj Access Source
EmbPrj Relevance Source
EmbPrj Hiding Source
EmbPrj Induction Source
EmbPrj Delayed Source
EmbPrj MemberId Source
EmbPrj GlobalId Source
EmbPrj LocalId Source
EmbPrj Exp Source
EmbPrj TopLevelModuleName Source
EmbPrj QName Source
EmbPrj NamePart Source
EmbPrj Name Source
EmbPrj Range Source
EmbPrj GenPart Source
EmbPrj Precedence Source
EmbPrj Fixity Source
EmbPrj Associativity Source
EmbPrj AmbiguousQName Source
EmbPrj ModuleName Source
EmbPrj QName Source
EmbPrj Literal Source
EmbPrj AbstractModule Source
EmbPrj AbstractName Source
EmbPrj WhyInScope Source
EmbPrj KindOfName Source
EmbPrj NameSpace Source
EmbPrj LocalVar Source
EmbPrj ScopeInfo Source
EmbPrj NameSpaceId Source
EmbPrj Scope Source
EmbPrj CompressedFile Source
EmbPrj Aspects Source
EmbPrj OtherAspect Source
EmbPrj NameKind Source
EmbPrj Aspect Source
EmbPrj Pattern Source
EmbPrj TypedBinding Source
EmbPrj TypedBindings Source
EmbPrj LamBinding Source
EmbPrj LetBinding Source
EmbPrj Expr Source
EmbPrj Permutation Source
EmbPrj ConPatternInfo Source
EmbPrj Pattern Source
EmbPrj ClauseBody Source
EmbPrj Clause Source
EmbPrj LevelAtom Source
EmbPrj PlusLevel Source
EmbPrj Level Source
EmbPrj Sort Source
EmbPrj Telescope Source
EmbPrj Type Source
EmbPrj Term Source
EmbPrj ConHead Source
EmbPrj EInterface Source
EmbPrj InjectiveFun Source
EmbPrj Relevance Source
EmbPrj Forced Source
EmbPrj Tag Source
EmbPrj CompiledClauses Source
EmbPrj CtxId Source
EmbPrj MutualId Source
EmbPrj TermHead Source
EmbPrj FunctionInverse Source
EmbPrj Defn Source
EmbPrj Projection Source
EmbPrj Occurrence Source
EmbPrj CompiledRepresentation Source
EmbPrj Polarity Source
EmbPrj HaskellExport Source
EmbPrj HaskellRepresentation Source
EmbPrj Definition Source
EmbPrj RewriteRule Source
EmbPrj NLPat Source
EmbPrj DisplayTerm Source
EmbPrj DisplayForm Source
EmbPrj Section Source
EmbPrj Signature Source
EmbPrj Interface Source
EmbPrj a => EmbPrj [a] Source
EmbPrj a => EmbPrj (Maybe a) Source
(Ord a, EmbPrj a) => EmbPrj (Set a) Source
EmbPrj a => EmbPrj (Ranged a) Source
EmbPrj c => EmbPrj (ArgInfo c) Source
EmbPrj a => EmbPrj (WithHiding a) Source
EmbPrj a => EmbPrj (Drop a) Source
EmbPrj a => EmbPrj (Abs a) Source
EmbPrj a => EmbPrj (Elim' a) Source
EmbPrj a => EmbPrj (Case a) Source
EmbPrj a => EmbPrj (WithArity a) Source
EmbPrj a => EmbPrj (Builtin a) Source
EmbPrj a => EmbPrj (Open a) Source
(EmbPrj a, EmbPrj b) => EmbPrj (a, b) Source
(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b) Source
(Ord a, Ord b, EmbPrj a, EmbPrj b) => EmbPrj (BiMap a b) Source
(Eq k, Hashable k, EmbPrj k, EmbPrj v) => EmbPrj (HashMap k v) Source
(EmbPrj s, EmbPrj t) => EmbPrj (Named s t) Source
(EmbPrj a, EmbPrj c) => EmbPrj (Dom c a) Source
(EmbPrj a, EmbPrj c) => EmbPrj (Arg c a) Source
(EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj (a, b, c) Source