Agda-2.6.3.20230805: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Serialise.Base

Synopsis

Documentation

type Node = [Int32] Source #

Constructor tag (maybe omitted) and argument indices.

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 = IOArray Int32 (HashMap 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, Bounded a) => a -> S Int32 Source #

value Source #

Arguments

:: Int32 
-> R a

Deserialization.

default value :: (Enum a, Bounded a) => Int32 -> R a Source #

Instances

Instances details
EmbPrj Range Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj ExecutablesFile Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj LibPositionInfo 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 OptionsPragma Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ConfluenceCheck Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj InfectiveCoinfective Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj OptionWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj PragmaOptions Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj WarningMode Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj WarningName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj BindName 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 Name Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj QName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Suffix Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj BuiltinId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj PrimitiveId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj SomeBuiltin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Access Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj Annotation Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Associativity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj BoundVariablePosition Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Cohesion Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ConOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Cubical Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ExpandedEllipsis Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj FileType 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 FixityLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj FreeVariables Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj IsAbstract Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj IsOpaque Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Language Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Lock Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Modality Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ModuleNameHash Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj NameId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj NotationPart Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj OpaqueId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj PatternOrCopattern Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ProjOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Q0Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Q1Origin 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 Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Aspect Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj Aspects Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj DefinitionSite Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj Induction Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj NameKind Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj OtherAspect Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj TokenBased Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj Doc Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

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 UnicodeOrAscii Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj Name Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj NameInScope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj NamePart Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj QName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ParenPreference Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj Precedence Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj ConPatInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj ConPatLazy Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj Blocked_ Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Clause Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj ConHead Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

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 DataOrRecord Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Level Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj NotBlocked 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 PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Sort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Term Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj IsFibrant Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Univ Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Literal Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ParseWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj Range Source #

Ranges are always deserialised as noRange.

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj RangeFile Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj AbstractModule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj AbstractName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj BindingSource Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj DataOrRecordModule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj KindOfName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj LocalVar Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj NameMetadata 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 NameSpaceId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj Scope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj ScopeInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj WhyInScope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj CutOff Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj LazySplit Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj BuiltinSort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

EmbPrj Definition Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Defn Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj ForeignCode Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

EmbPrj ForeignCodeStack Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

EmbPrj FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Instantiation Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Interface Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances

EmbPrj IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj MutualId 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 NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj OpaqueBlock Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Polarity 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 ProjectionLikenessMissing Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj RecordFieldWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj RemoteMetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj RewriteRule 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 System Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Warning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj AbsNameWithFixity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj SerialisedRange Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

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 ProfileOption Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj ProfileOptions Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj Void Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Int32 Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj CallStack Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj SrcLoc Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Word64 Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj IntSet 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 String Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Integer 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 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 a => EmbPrj (Pattern' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

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 (HasEta' 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 (WithHiding a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

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 (Pattern' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj a => EmbPrj (Substitution' 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 (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 (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 (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 (SplitTree' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

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 (Judgement 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 (List1 a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: List1 a -> S Int32 Source #

icod_ :: List1 a -> S Int32 Source #

value :: Int32 -> R (List1 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 (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 (RangeMap a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

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 (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 [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 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 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 #

(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 a, Typeable b) => EmbPrj (WithDefault' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

(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 #

(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 #

(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 #

(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 #