Agda-2.6.2.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Serialise.Base

Synopsis

Documentation

type Node = [Int32] Source #

Constructor tag (maybe omitted) and argument indices.

type HashTable k v = BasicHashTable k v Source #

The type of hashtables used in this module.

A very limited amount of testing indicates that CuckooHashTable is somewhat slower than BasicHashTable, and that LinearHashTable and the hashtables from Data.Hashtable are much slower.

newtype FreshAndReuse Source #

Structure providing fresh identifiers for hash map and counting hash map hits (i.e. when no fresh identifier required).

Constructors

FreshAndReuse 

Fields

type QNameId = [NameId] Source #

Two QNames are equal if their QNameId is equal.

qnameId :: QName -> QNameId Source #

Computing a qualified names composed ID.

data Dict Source #

State of the the encoder.

Constructors

Dict 

Fields

emptyDict Source #

Arguments

:: Bool

Collect statistics for icode calls?

-> IO Dict 

Creates an empty dictionary.

data U Source #

Universal type, wraps everything.

Constructors

forall a.Typeable a => U !a 

type Memo = HashTable (Int32, TypeRep) U Source #

Univeral memo structure, to introduce sharing during decoding

data St Source #

State of the decoder.

Constructors

St 

Fields

type S a = ReaderT Dict IO a Source #

Monad used by the encoder.

type R a = ExceptT TypeError (StateT St IO) a Source #

Monad used by the decoder.

TCM is not used because the associated overheads would make decoding slower.

malformed :: R a Source #

Throws an error which is suitable when the data stream is malformed.

class Typeable a => EmbPrj a where Source #

Minimal complete definition

Nothing

Methods

icode Source #

Arguments

:: a 
-> S Int32

Serialization (wrapper).

icod_ Source #

Arguments

:: a 
-> S Int32

Serialization (worker).

default icod_ :: Enum a => a -> S Int32 Source #

value Source #

Arguments

:: Int32 
-> R a

Deserialization.

default value :: Enum a => Int32 -> R a Source #

Instances

Instances details
EmbPrj Bool Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Char Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Double Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Int Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Int32 Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Integer Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Word64 Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj CallStack Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj () Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: () -> S Int32 Source #

icod_ :: () -> S Int32 Source #

value :: Int32 -> R () Source #

EmbPrj String Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Text Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Text Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Void Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj SrcLoc Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj IntSet Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Doc Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj CutOff Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj Impossible Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Permutation Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj AbsolutePath Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Range Source #

Ranges are always deserialised as noRange.

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj GenPart Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ExpandedEllipsis Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Fixity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Associativity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj FixityLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj NameId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ModuleNameHash Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj IsAbstract Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Access Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj ProjOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ConOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj FreeVariables Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Cohesion Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Lock Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Annotation Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj QωOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Q1Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Q0Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Modality Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Induction Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj PatternOrCopattern Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Language Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Cubical Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj FileType Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Delayed Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Precedence Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj ParenPreference Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj UnicodeOrAscii Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj NameInScope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj QName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj NamePart Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Name Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj Warning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj Suffix Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj AmbiguousQName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj QName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Name Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Literal Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj WarningName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj WarningMode Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj ParseWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj LibWarning' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj LibWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj LibPositionInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj ExecutablesFile Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj Range Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj LazySplit Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj DeclarationWarning' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj DeclarationWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj AbstractModule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj NameMetadata Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj AbstractName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj WhyInScope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj KindOfName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj NameOrModule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj NameSpace Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj LocalVar Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj BindingSource Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj ScopeInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj NameSpaceId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj DataOrRecordModule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj Scope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj ConPatLazy Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj ConPatInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj TokenBased Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj DefinitionSite Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj Aspects Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj OtherAspect Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj NameKind Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj Aspect Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj PatOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj PatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Clause Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Blocked_ Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj NotBlocked Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Level Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Sort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj IsFibrant Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Term Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj ConHead Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj DataOrRecord Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj BindName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj ConfluenceCheck Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj PragmaOptions Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj RecordFieldWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Defn Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Projection Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj System Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

EmbPrj IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Definition Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Section Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Signature Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Interface Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances

EmbPrj ForeignCode Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

EmbPrj CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj SerialisedRange Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj AbsNameWithFixity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj a => EmbPrj [a] Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: [a] -> S Int32 Source #

icod_ :: [a] -> S Int32 Source #

value :: Int32 -> R [a] Source #

EmbPrj a => EmbPrj (Maybe a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Maybe a -> S Int32 Source #

icod_ :: Maybe a -> S Int32 Source #

value :: Int32 -> R (Maybe a) Source #

EmbPrj a => EmbPrj (NonEmpty a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj a => EmbPrj (Seq a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Seq a -> S Int32 Source #

icod_ :: Seq a -> S Int32 Source #

value :: Int32 -> R (Seq a) Source #

(Ord a, EmbPrj a) => EmbPrj (Set a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Set a -> S Int32 Source #

icod_ :: Set a -> S Int32 Source #

value :: Int32 -> R (Set a) Source #

EmbPrj a => EmbPrj (Maybe a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Maybe a -> S Int32 Source #

icod_ :: Maybe a -> S Int32 Source #

value :: Int32 -> R (Maybe a) Source #

EmbPrj a => EmbPrj (Drop a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Drop a -> S Int32 Source #

icod_ :: Drop a -> S Int32 Source #

value :: Int32 -> R (Drop a) Source #

EmbPrj a => EmbPrj (List2 a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: List2 a -> S Int32 Source #

icod_ :: List2 a -> S Int32 Source #

value :: Int32 -> R (List2 a) Source #

EmbPrj a => EmbPrj (Interval' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj a => EmbPrj (Position' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj a => EmbPrj (Ranged a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Ranged a -> S Int32 Source #

icod_ :: Ranged a -> S Int32 Source #

value :: Int32 -> R (Ranged a) Source #

EmbPrj a => EmbPrj (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Arg a -> S Int32 Source #

icod_ :: Arg a -> S Int32 Source #

value :: Int32 -> R (Arg a) Source #

EmbPrj a => EmbPrj (WithOrigin a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj a => EmbPrj (WithHiding a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj a => EmbPrj (HasEta' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj a => EmbPrj (RangeMap a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj a => EmbPrj (PairInt a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj a => EmbPrj (FieldAssignment' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj a => EmbPrj (SplitTree' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj a => EmbPrj (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Elim' a -> S Int32 Source #

icod_ :: Elim' a -> S Int32 Source #

value :: Int32 -> R (Elim' a) Source #

EmbPrj a => EmbPrj (Substitution' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj a => EmbPrj (Pattern' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj a => EmbPrj (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Tele a -> S Int32 Source #

icod_ :: Tele a -> S Int32 Source #

value :: Int32 -> R (Tele a) Source #

EmbPrj a => EmbPrj (Type' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Type' a -> S Int32 Source #

icod_ :: Type' a -> S Int32 Source #

value :: Int32 -> R (Type' a) Source #

EmbPrj a => EmbPrj (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Abs a -> S Int32 Source #

icod_ :: Abs a -> S Int32 Source #

value :: Int32 -> R (Abs a) Source #

EmbPrj a => EmbPrj (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Int32 Source #

icod_ :: Dom a -> S Int32 Source #

value :: Int32 -> R (Dom a) Source #

EmbPrj a => EmbPrj (Case a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Case a -> S Int32 Source #

icod_ :: Case a -> S Int32 Source #

value :: Int32 -> R (Case a) Source #

EmbPrj a => EmbPrj (WithArity a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj a => EmbPrj (Pattern' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Typeable b => EmbPrj (WithDefault b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj a => EmbPrj (Builtin a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj a => EmbPrj (FunctionInverse' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj a => EmbPrj (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Open a -> S Int32 Source #

icod_ :: Open a -> S Int32 Source #

value :: Int32 -> R (Open a) Source #

(EmbPrj a, EmbPrj b) => EmbPrj (Either a b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Either a b -> S Int32 Source #

icod_ :: Either a b -> S Int32 Source #

value :: Int32 -> R (Either a b) Source #

(EmbPrj a, EmbPrj b) => EmbPrj (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: (a, b) -> S Int32 Source #

icod_ :: (a, b) -> S Int32 Source #

value :: Int32 -> R (a, b) Source #

(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Map a b -> S Int32 Source #

icod_ :: Map a b -> S Int32 Source #

value :: Int32 -> R (Map a b) Source #

(Eq k, Hashable k, EmbPrj k, EmbPrj v) => EmbPrj (HashMap k v) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: HashMap k v -> S Int32 Source #

icod_ :: HashMap k v -> S Int32 Source #

value :: Int32 -> R (HashMap k v) Source #

(EmbPrj a, EmbPrj b) => EmbPrj (Pair a b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Pair a b -> S Int32 Source #

icod_ :: Pair a b -> S Int32 Source #

value :: Int32 -> R (Pair a b) Source #

(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Trie a b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Trie a b -> S Int32 Source #

icod_ :: Trie a b -> S Int32 Source #

value :: Int32 -> R (Trie a b) Source #

(EmbPrj k, EmbPrj v, EmbPrj (Tag v)) => EmbPrj (BiMap k v) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: BiMap k v -> S Int32 Source #

icod_ :: BiMap k v -> S Int32 Source #

value :: Int32 -> R (BiMap k v) Source #

(EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

(EmbPrj s, EmbPrj t) => EmbPrj (Named s t) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Named s t -> S Int32 Source #

icod_ :: Named s t -> S Int32 Source #

value :: Int32 -> R (Named s t) Source #

(EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj (a, b, c) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: (a, b, c) -> S Int32 Source #

icod_ :: (a, b, c) -> S Int32 Source #

value :: Int32 -> R (a, b, c) Source #

tickICode :: forall a. Typeable a => a -> S () Source #

Increase entry for a in stats.

runGetState :: Get a -> ByteString -> ByteOffset -> (a, ByteString, ByteOffset) Source #

Data.Binary.runGetState is deprecated in favour of runGetIncremental. Reimplementing it in terms of the new function. The new Decoder type contains strict byte strings so we need to be careful not to feed the entire lazy byte string to the decoder at once.

icodeX :: (Eq k, Hashable k) => (Dict -> HashTable k Int32) -> (Dict -> IORef FreshAndReuse) -> k -> S Int32 Source #

icodeMemo Source #

Arguments

:: (Ord a, Hashable a) 
=> (Dict -> HashTable a Int32)

Memo structure for thing of key a.

-> (Dict -> IORef FreshAndReuse)

Statistics.

-> a

Key to the thing.

-> S Int32

Fallback computation to encode the thing.

-> S Int32

Encoded thing.

icode only if thing has not seen before.

vcase :: forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a Source #

vcase value ix decodes thing represented by ix :: Int32 via the valu function and stores it in nodeMemo. If ix is present in nodeMemo, valu is not used, but the thing is read from nodeMemo instead.

class ICODE t b where Source #

icodeArgs proxy (a1, ..., an) maps icode over a1, ..., an and returns the corresponding list of Int32.

Methods

icodeArgs :: IsBase t ~ b => All EmbPrj (Domains t) => Proxy t -> Products (Domains t) -> S [Int32] Source #

Instances

Instances details
IsBase t ~ 'True => ICODE t 'True Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Base

Methods

icodeArgs :: Proxy t -> Products (Domains t) -> S [Int32] Source #

ICODE t (IsBase t) => ICODE (a -> t) 'False Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Base

Methods

icodeArgs :: Proxy (a -> t) -> Products (Domains (a -> t)) -> S [Int32] Source #

icodeN :: forall t. ICODE t (IsBase t) => Currying (Domains t) (S Int32) => All EmbPrj (Domains t) => Int32 -> t -> Arrows (Domains t) (S Int32) Source #

icodeN tag t a1 ... an serialises the arguments a1, ..., an of the constructor t together with a tag tag picked to disambiguate between different constructors. It corresponds to icodeNode . (tag :) =<< mapM icode [a1, ..., an]

icodeN' :: forall t. ICODE t (IsBase t) => Currying (Domains t) (S Int32) => All EmbPrj (Domains t) => t -> Arrows (Domains t) (S Int32) Source #

icodeN' is the same as icodeN except that there is no tag

class VALU t b where Source #

Methods

valuN' :: b ~ IsBase t => All EmbPrj (Domains t) => t -> Products (Constant Int32 (Domains t)) -> R (CoDomain t) Source #

valueArgs :: b ~ IsBase t => All EmbPrj (CoDomain t ': Domains t) => Proxy t -> Node -> Maybe (Products (Constant Int32 (Domains t))) Source #

Instances

Instances details
VALU t 'True Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Base

VALU t (IsBase t) => VALU (a -> t) 'False Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Base

Methods

valuN' :: (a -> t) -> Products (Constant Int32 (Domains (a -> t))) -> R (CoDomain (a -> t)) Source #

valueArgs :: Proxy (a -> t) -> Node -> Maybe (Products (Constant Int32 (Domains (a -> t)))) Source #

valuN :: forall t. VALU t (IsBase t) => Currying (Constant Int32 (Domains t)) (R (CoDomain t)) => All EmbPrj (Domains t) => t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t)) Source #

valueN :: forall t. VALU t (IsBase t) => All EmbPrj (CoDomain t ': Domains t) => t -> Int32 -> R (CoDomain t) Source #