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

Safe HaskellNone

Agda.TypeChecking.Serialise

Description

Structure-sharing serialisation of Agda interface files.

Synopsis

Documentation

encode :: EmbPrj a => a -> TCM ByteStringSource

Encodes something. To ensure relocatability file paths in positions are replaced with module names.

encodeFileSource

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)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 Typeable a => EmbPrj a Source

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)