Agda.TypeChecking.Serialise.Base

Documentation

type Node = [Int32]

Constructor tag (maybe omitted) and argument indices.

newtype FreshAndReuse

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

Constructors

FreshAndReuse

Fields

• farFresh :: Int32

  Number of hash map misses.

farEmpty :: FreshAndReuse

lensFresh :: Lens' FreshAndReuse Int32

type QNameId = [NameId]

Two QNames are equal if their QNameId is equal.

qnameId :: QName -> QNameId

Computing a qualified names composed ID.

data Dict

State of the the encoder.

Constructors

Dict

Fields

• nodeD :: !(HashTable Node Int32)

  Written to interface file.

• stringD :: !(HashTable String Int32)

  Written to interface file.

• lTextD :: !(HashTable Text Int32)

  Written to interface file.

• sTextD :: !(HashTable Text Int32)

  Written to interface file.

• integerD :: !(HashTable Integer Int32)

  Written to interface file.

• doubleD :: !(HashTable Double Int32)

  Written to interface file. Dicitionaries which are not serialized, but provide short cuts to speed up serialization:

• termD :: !(HashTable (Ptr Term) Int32)

  Not written to interface file. Andreas, Makoto, AIM XXI Memoizing A.Name does not buy us much if we already memoize A.QName.

• nameD :: !(HashTable NameId Int32)

  Not written to interface file.

• qnameD :: !(HashTable QNameId Int32)

  Not written to interface file. Fresh UIDs and reuse statistics:

• nodeC :: !(IORef FreshAndReuse)
• stringC :: !(IORef FreshAndReuse)
• lTextC :: !(IORef FreshAndReuse)
• sTextC :: !(IORef FreshAndReuse)
• integerC :: !(IORef FreshAndReuse)
• doubleC :: !(IORef FreshAndReuse)
• termC :: !(IORef FreshAndReuse)
• nameC :: !(IORef FreshAndReuse)
• qnameC :: !(IORef FreshAndReuse)
• stats :: !(HashTable String Int)
• collectStats :: Bool

  If True collect in stats the quantities of calls to icode for each Typeable a.

emptyDict

Arguments

:: Bool

Collect statistics for icode calls?

-> IO Dict

Creates an empty dictionary.

data U

Universal type, wraps everything.

Constructors

forall a.Typeable a => U !a

type Memo = IOArray Int32 (HashMap TypeRep U)

Univeral memo structure, to introduce sharing during decoding

data St

State of the decoder.

Constructors

St

Fields

• nodeE :: !(Array Int32 Node)

  Obtained from interface file.

• stringE :: !(Array Int32 String)

  Obtained from interface file.

• lTextE :: !(Array Int32 Text)

  Obtained from interface file.

• sTextE :: !(Array Int32 Text)

  Obtained from interface file.

• integerE :: !(Array Int32 Integer)

  Obtained from interface file.

• doubleE :: !(Array Int32 Double)

  Obtained from interface file.

• nodeMemo :: !Memo

  Created and modified by decoder. Used to introduce sharing while deserializing objects.

• modFile :: !ModuleToSource

  Maps module names to file names. Constructed by the decoder.

• includes :: [AbsolutePath]

  The include directories.

type S a = ReaderT Dict IO a

Monad used by the encoder.

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

Monad used by the decoder.

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

malformed :: R a

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

class Typeable a => EmbPrj a where

Minimal complete definition

Nothing

Methods

icode

Arguments

:: a

-> S Int32

Serialization (wrapper).

icod_

Arguments

:: a

-> S Int32

Serialization (worker).

default icod_ :: (Enum a, Bounded a) => a -> S Int32

value

Arguments

:: Int32

-> R a

Deserialization.

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

Instances

EmbPrj Range

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Range -> S Int32

icod_ :: Range -> S Int32

value :: Int32 -> R Range

EmbPrj ExecutablesFile

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ExecutablesFile -> S Int32

icod_ :: ExecutablesFile -> S Int32

value :: Int32 -> R ExecutablesFile

EmbPrj LibPositionInfo

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibPositionInfo -> S Int32

icod_ :: LibPositionInfo -> S Int32

value :: Int32 -> R LibPositionInfo

EmbPrj LibWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning -> S Int32

icod_ :: LibWarning -> S Int32

value :: Int32 -> R LibWarning

EmbPrj LibWarning'

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning' -> S Int32

icod_ :: LibWarning' -> S Int32

value :: Int32 -> R LibWarning'

EmbPrj OptionsPragma

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: OptionsPragma -> S Int32

icod_ :: OptionsPragma -> S Int32

value :: Int32 -> R OptionsPragma

EmbPrj ConfluenceCheck

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ConfluenceCheck -> S Int32

icod_ :: ConfluenceCheck -> S Int32

value :: Int32 -> R ConfluenceCheck

EmbPrj InfectiveCoinfective

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: InfectiveCoinfective -> S Int32

icod_ :: InfectiveCoinfective -> S Int32

value :: Int32 -> R InfectiveCoinfective

EmbPrj OptionWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: OptionWarning -> S Int32

icod_ :: OptionWarning -> S Int32

value :: Int32 -> R OptionWarning

EmbPrj PragmaOptions

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: PragmaOptions -> S Int32

icod_ :: PragmaOptions -> S Int32

value :: Int32 -> R PragmaOptions

EmbPrj WarningMode

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningMode -> S Int32

icod_ :: WarningMode -> S Int32

value :: Int32 -> R WarningMode

EmbPrj WarningName

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningName -> S Int32

icod_ :: WarningName -> S Int32

value :: Int32 -> R WarningName

EmbPrj BindName

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindName -> S Int32

icod_ :: BindName -> S Int32

value :: Int32 -> R BindName

EmbPrj AmbiguousQName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: AmbiguousQName -> S Int32

icod_ :: AmbiguousQName -> S Int32

value :: Int32 -> R AmbiguousQName

EmbPrj ModuleName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ModuleName -> S Int32

icod_ :: ModuleName -> S Int32

value :: Int32 -> R ModuleName

EmbPrj Name

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32

icod_ :: Name -> S Int32

value :: Int32 -> R Name

EmbPrj QName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QName -> S Int32

icod_ :: QName -> S Int32

value :: Int32 -> R QName

EmbPrj Suffix

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Suffix -> S Int32

icod_ :: Suffix -> S Int32

value :: Int32 -> R Suffix

EmbPrj BuiltinId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: BuiltinId -> S Int32

icod_ :: BuiltinId -> S Int32

value :: Int32 -> R BuiltinId

EmbPrj PrimitiveId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: PrimitiveId -> S Int32

icod_ :: PrimitiveId -> S Int32

value :: Int32 -> R PrimitiveId

EmbPrj SomeBuiltin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: SomeBuiltin -> S Int32

icod_ :: SomeBuiltin -> S Int32

value :: Int32 -> R SomeBuiltin

EmbPrj Access

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Access -> S Int32

icod_ :: Access -> S Int32

value :: Int32 -> R Access

EmbPrj Annotation

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Annotation -> S Int32

icod_ :: Annotation -> S Int32

value :: Int32 -> R Annotation

EmbPrj ArgInfo

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ArgInfo -> S Int32

icod_ :: ArgInfo -> S Int32

value :: Int32 -> R ArgInfo

EmbPrj Associativity

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Associativity -> S Int32

icod_ :: Associativity -> S Int32

value :: Int32 -> R Associativity

EmbPrj BoundVariablePosition

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: BoundVariablePosition -> S Int32

icod_ :: BoundVariablePosition -> S Int32

value :: Int32 -> R BoundVariablePosition

EmbPrj Cohesion

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Cohesion -> S Int32

icod_ :: Cohesion -> S Int32

value :: Int32 -> R Cohesion

EmbPrj ConOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ConOrigin -> S Int32

icod_ :: ConOrigin -> S Int32

value :: Int32 -> R ConOrigin

EmbPrj Cubical

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Cubical -> S Int32

icod_ :: Cubical -> S Int32

value :: Int32 -> R Cubical

EmbPrj ExpandedEllipsis

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ExpandedEllipsis -> S Int32

icod_ :: ExpandedEllipsis -> S Int32

value :: Int32 -> R ExpandedEllipsis

EmbPrj FileType

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FileType -> S Int32

icod_ :: FileType -> S Int32

value :: Int32 -> R FileType

EmbPrj Fixity

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Fixity -> S Int32

icod_ :: Fixity -> S Int32

value :: Int32 -> R Fixity

EmbPrj Fixity'

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Fixity' -> S Int32

icod_ :: Fixity' -> S Int32

value :: Int32 -> R Fixity'

EmbPrj FixityLevel

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FixityLevel -> S Int32

icod_ :: FixityLevel -> S Int32

value :: Int32 -> R FixityLevel

EmbPrj FreeVariables

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FreeVariables -> S Int32

icod_ :: FreeVariables -> S Int32

value :: Int32 -> R FreeVariables

EmbPrj Hiding

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Hiding -> S Int32

icod_ :: Hiding -> S Int32

value :: Int32 -> R Hiding

EmbPrj IsAbstract

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: IsAbstract -> S Int32

icod_ :: IsAbstract -> S Int32

value :: Int32 -> R IsAbstract

EmbPrj IsOpaque

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: IsOpaque -> S Int32

icod_ :: IsOpaque -> S Int32

value :: Int32 -> R IsOpaque

EmbPrj Language

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Language -> S Int32

icod_ :: Language -> S Int32

value :: Int32 -> R Language

EmbPrj Lock

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Lock -> S Int32

icod_ :: Lock -> S Int32

value :: Int32 -> R Lock

EmbPrj MetaId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: MetaId -> S Int32

icod_ :: MetaId -> S Int32

value :: Int32 -> R MetaId

EmbPrj Modality

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Modality -> S Int32

icod_ :: Modality -> S Int32

value :: Int32 -> R Modality

EmbPrj NameId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NameId -> S Int32

icod_ :: NameId -> S Int32

value :: Int32 -> R NameId

EmbPrj NotationPart

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NotationPart -> S Int32

icod_ :: NotationPart -> S Int32

value :: Int32 -> R NotationPart

EmbPrj OpaqueId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: OpaqueId -> S Int32

icod_ :: OpaqueId -> S Int32

value :: Int32 -> R OpaqueId

EmbPrj Origin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Origin -> S Int32

icod_ :: Origin -> S Int32

value :: Int32 -> R Origin

EmbPrj PatternOrCopattern

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: PatternOrCopattern -> S Int32

icod_ :: PatternOrCopattern -> S Int32

value :: Int32 -> R PatternOrCopattern

EmbPrj ProjOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ProjOrigin -> S Int32

icod_ :: ProjOrigin -> S Int32

value :: Int32 -> R ProjOrigin

EmbPrj Q0Origin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Q0Origin -> S Int32

icod_ :: Q0Origin -> S Int32

value :: Int32 -> R Q0Origin

EmbPrj Q1Origin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Q1Origin -> S Int32

icod_ :: Q1Origin -> S Int32

value :: Int32 -> R Q1Origin

EmbPrj Quantity

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Quantity -> S Int32

icod_ :: Quantity -> S Int32

value :: Int32 -> R Quantity

EmbPrj QωOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QωOrigin -> S Int32

icod_ :: QωOrigin -> S Int32

value :: Int32 -> R QωOrigin

EmbPrj Relevance

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Relevance -> S Int32

icod_ :: Relevance -> S Int32

value :: Int32 -> R Relevance

EmbPrj Aspect

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspect -> S Int32

icod_ :: Aspect -> S Int32

value :: Int32 -> R Aspect

EmbPrj Aspects

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspects -> S Int32

icod_ :: Aspects -> S Int32

value :: Int32 -> R Aspects

EmbPrj DefinitionSite

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: DefinitionSite -> S Int32

icod_ :: DefinitionSite -> S Int32

value :: Int32 -> R DefinitionSite

EmbPrj Induction

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Induction -> S Int32

icod_ :: Induction -> S Int32

value :: Int32 -> R Induction

EmbPrj NameKind

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: NameKind -> S Int32

icod_ :: NameKind -> S Int32

value :: Int32 -> R NameKind

EmbPrj OtherAspect

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: OtherAspect -> S Int32

icod_ :: OtherAspect -> S Int32

value :: Int32 -> R OtherAspect

EmbPrj TokenBased

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: TokenBased -> S Int32

icod_ :: TokenBased -> S Int32

value :: Int32 -> R TokenBased

EmbPrj Doc

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Doc -> S Int32

icod_ :: Doc -> S Int32

value :: Int32 -> R Doc

EmbPrj DeclarationWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: DeclarationWarning -> S Int32

icod_ :: DeclarationWarning -> S Int32

value :: Int32 -> R DeclarationWarning

EmbPrj DeclarationWarning'

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: DeclarationWarning' -> S Int32

icod_ :: DeclarationWarning' -> S Int32

value :: Int32 -> R DeclarationWarning'

EmbPrj UnicodeOrAscii

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: UnicodeOrAscii -> S Int32

icod_ :: UnicodeOrAscii -> S Int32

value :: Int32 -> R UnicodeOrAscii

EmbPrj Name

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32

icod_ :: Name -> S Int32

value :: Int32 -> R Name

EmbPrj NameInScope

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NameInScope -> S Int32

icod_ :: NameInScope -> S Int32

value :: Int32 -> R NameInScope

EmbPrj NamePart

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NamePart -> S Int32

icod_ :: NamePart -> S Int32

value :: Int32 -> R NamePart

EmbPrj QName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QName -> S Int32

icod_ :: QName -> S Int32

value :: Int32 -> R QName

EmbPrj ParenPreference

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ParenPreference -> S Int32

icod_ :: ParenPreference -> S Int32

value :: Int32 -> R ParenPreference

EmbPrj Precedence

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Precedence -> S Int32

icod_ :: Precedence -> S Int32

value :: Int32 -> R Precedence

EmbPrj ConPatInfo

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ConPatInfo -> S Int32

icod_ :: ConPatInfo -> S Int32

value :: Int32 -> R ConPatInfo

EmbPrj ConPatLazy

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ConPatLazy -> S Int32

icod_ :: ConPatLazy -> S Int32

value :: Int32 -> R ConPatLazy

EmbPrj Blocked_

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Blocked_ -> S Int32

icod_ :: Blocked_ -> S Int32

value :: Int32 -> R Blocked_

EmbPrj Clause

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Clause -> S Int32

icod_ :: Clause -> S Int32

value :: Int32 -> R Clause

EmbPrj ConHead

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ConHead -> S Int32

icod_ :: ConHead -> S Int32

value :: Int32 -> R ConHead

EmbPrj ConPatternInfo

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ConPatternInfo -> S Int32

icod_ :: ConPatternInfo -> S Int32

value :: Int32 -> R ConPatternInfo

EmbPrj DBPatVar

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DBPatVar -> S Int32

icod_ :: DBPatVar -> S Int32

value :: Int32 -> R DBPatVar

EmbPrj DataOrRecord

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DataOrRecord -> S Int32

icod_ :: DataOrRecord -> S Int32

value :: Int32 -> R DataOrRecord

EmbPrj Level

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Level -> S Int32

icod_ :: Level -> S Int32

value :: Int32 -> R Level

EmbPrj NotBlocked

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NotBlocked -> S Int32

icod_ :: NotBlocked -> S Int32

value :: Int32 -> R NotBlocked

EmbPrj PatOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PatOrigin -> S Int32

icod_ :: PatOrigin -> S Int32

value :: Int32 -> R PatOrigin

EmbPrj PatternInfo

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PatternInfo -> S Int32

icod_ :: PatternInfo -> S Int32

value :: Int32 -> R PatternInfo

EmbPrj PlusLevel

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PlusLevel -> S Int32

icod_ :: PlusLevel -> S Int32

value :: Int32 -> R PlusLevel

EmbPrj Sort

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Sort -> S Int32

icod_ :: Sort -> S Int32

value :: Int32 -> R Sort

EmbPrj Term

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Term -> S Int32

icod_ :: Term -> S Int32

value :: Int32 -> R Term

EmbPrj IsFibrant

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: IsFibrant -> S Int32

icod_ :: IsFibrant -> S Int32

value :: Int32 -> R IsFibrant

EmbPrj Univ

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Univ -> S Int32

icod_ :: Univ -> S Int32

value :: Int32 -> R Univ

EmbPrj Literal

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Literal -> S Int32

icod_ :: Literal -> S Int32

value :: Int32 -> R Literal

EmbPrj ParseWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ParseWarning -> S Int32

icod_ :: ParseWarning -> S Int32

value :: Int32 -> R ParseWarning

EmbPrj Range

Ranges are always deserialised as noRange.

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Range -> S Int32

icod_ :: Range -> S Int32

value :: Int32 -> R Range

EmbPrj RangeFile

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: RangeFile -> S Int32

icod_ :: RangeFile -> S Int32

value :: Int32 -> R RangeFile

EmbPrj AbstractModule

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractModule -> S Int32

icod_ :: AbstractModule -> S Int32

value :: Int32 -> R AbstractModule

EmbPrj AbstractName

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractName -> S Int32

icod_ :: AbstractName -> S Int32

value :: Int32 -> R AbstractName

EmbPrj BindingSource

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindingSource -> S Int32

icod_ :: BindingSource -> S Int32

value :: Int32 -> R BindingSource

EmbPrj DataOrRecordModule

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: DataOrRecordModule -> S Int32

icod_ :: DataOrRecordModule -> S Int32

value :: Int32 -> R DataOrRecordModule

EmbPrj KindOfName

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: KindOfName -> S Int32

icod_ :: KindOfName -> S Int32

value :: Int32 -> R KindOfName

EmbPrj LocalVar

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: LocalVar -> S Int32

icod_ :: LocalVar -> S Int32

value :: Int32 -> R LocalVar

EmbPrj NameMetadata

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameMetadata -> S Int32

icod_ :: NameMetadata -> S Int32

value :: Int32 -> R NameMetadata

EmbPrj NameOrModule

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameOrModule -> S Int32

icod_ :: NameOrModule -> S Int32

value :: Int32 -> R NameOrModule

EmbPrj NameSpace

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameSpace -> S Int32

icod_ :: NameSpace -> S Int32

value :: Int32 -> R NameSpace

EmbPrj NameSpaceId

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameSpaceId -> S Int32

icod_ :: NameSpaceId -> S Int32

value :: Int32 -> R NameSpaceId

EmbPrj Scope

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Scope -> S Int32

icod_ :: Scope -> S Int32

value :: Int32 -> R Scope

EmbPrj ScopeInfo

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ScopeInfo -> S Int32

icod_ :: ScopeInfo -> S Int32

value :: Int32 -> R ScopeInfo

EmbPrj WhyInScope

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: WhyInScope -> S Int32

icod_ :: WhyInScope -> S Int32

value :: Int32 -> R WhyInScope

EmbPrj TopLevelModuleName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: TopLevelModuleName -> S Int32

icod_ :: TopLevelModuleName -> S Int32

value :: Int32 -> R TopLevelModuleName

EmbPrj ModuleNameHash

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ModuleNameHash -> S Int32

icod_ :: ModuleNameHash -> S Int32

value :: Int32 -> R ModuleNameHash

EmbPrj CutOff

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: CutOff -> S Int32

icod_ :: CutOff -> S Int32

value :: Int32 -> R CutOff

EmbPrj CompiledClauses

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompiledClauses -> S Int32

icod_ :: CompiledClauses -> S Int32

value :: Int32 -> R CompiledClauses

EmbPrj LazySplit

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: LazySplit -> S Int32

icod_ :: LazySplit -> S Int32

value :: Int32 -> R LazySplit

EmbPrj SplitTag

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: SplitTag -> S Int32

icod_ :: SplitTag -> S Int32

value :: Int32 -> R SplitTag

EmbPrj BuiltinSort

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: BuiltinSort -> S Int32

icod_ :: BuiltinSort -> S Int32

value :: Int32 -> R BuiltinSort

EmbPrj CheckpointId

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CheckpointId -> S Int32

icod_ :: CheckpointId -> S Int32

value :: Int32 -> R CheckpointId

EmbPrj CompKit

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompKit -> S Int32

icod_ :: CompKit -> S Int32

value :: Int32 -> R CompKit

EmbPrj Comparison

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Comparison -> S Int32

icod_ :: Comparison -> S Int32

value :: Int32 -> R Comparison

EmbPrj CompilerPragma

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

Methods

icode :: CompilerPragma -> S Int32

icod_ :: CompilerPragma -> S Int32

value :: Int32 -> R CompilerPragma

EmbPrj Definition

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Definition -> S Int32

icod_ :: Definition -> S Int32

value :: Int32 -> R Definition

EmbPrj Defn

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Defn -> S Int32

icod_ :: Defn -> S Int32

value :: Int32 -> R Defn

EmbPrj DisplayForm

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DisplayForm -> S Int32

icod_ :: DisplayForm -> S Int32

value :: Int32 -> R DisplayForm

EmbPrj DisplayTerm

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DisplayTerm -> S Int32

icod_ :: DisplayTerm -> S Int32

value :: Int32 -> R DisplayTerm

EmbPrj DoGeneralize

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DoGeneralize -> S Int32

icod_ :: DoGeneralize -> S Int32

value :: Int32 -> R DoGeneralize

EmbPrj EtaEquality

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: EtaEquality -> S Int32

icod_ :: EtaEquality -> S Int32

value :: Int32 -> R EtaEquality

EmbPrj ExtLamInfo

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ExtLamInfo -> S Int32

icod_ :: ExtLamInfo -> S Int32

value :: Int32 -> R ExtLamInfo

EmbPrj ForeignCode

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

Methods

icode :: ForeignCode -> S Int32

icod_ :: ForeignCode -> S Int32

value :: Int32 -> R ForeignCode

EmbPrj ForeignCodeStack

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

Methods

icode :: ForeignCodeStack -> S Int32

icod_ :: ForeignCodeStack -> S Int32

value :: Int32 -> R ForeignCodeStack

EmbPrj FunctionFlag

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: FunctionFlag -> S Int32

icod_ :: FunctionFlag -> S Int32

value :: Int32 -> R FunctionFlag

EmbPrj Instantiation

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Instantiation -> S Int32

icod_ :: Instantiation -> S Int32

value :: Int32 -> R Instantiation

EmbPrj Interface

Defined in Agda.TypeChecking.Serialise.Instances

Methods

icode :: Interface -> S Int32

icod_ :: Interface -> S Int32

value :: Int32 -> R Interface

EmbPrj IsForced

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: IsForced -> S Int32

icod_ :: IsForced -> S Int32

value :: Int32 -> R IsForced

EmbPrj MutualId

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: MutualId -> S Int32

icod_ :: MutualId -> S Int32

value :: Int32 -> R MutualId

EmbPrj NLPSort

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NLPSort -> S Int32

icod_ :: NLPSort -> S Int32

value :: Int32 -> R NLPSort

EmbPrj NLPType

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NLPType -> S Int32

icod_ :: NLPType -> S Int32

value :: Int32 -> R NLPType

EmbPrj NLPat

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NLPat -> S Int32

icod_ :: NLPat -> S Int32

value :: Int32 -> R NLPat

EmbPrj NumGeneralizableArgs

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NumGeneralizableArgs -> S Int32

icod_ :: NumGeneralizableArgs -> S Int32

value :: Int32 -> R NumGeneralizableArgs

EmbPrj OpaqueBlock

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: OpaqueBlock -> S Int32

icod_ :: OpaqueBlock -> S Int32

value :: Int32 -> R OpaqueBlock

EmbPrj Polarity

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Polarity -> S Int32

icod_ :: Polarity -> S Int32

value :: Int32 -> R Polarity

EmbPrj ProjLams

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ProjLams -> S Int32

icod_ :: ProjLams -> S Int32

value :: Int32 -> R ProjLams

EmbPrj Projection

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Projection -> S Int32

icod_ :: Projection -> S Int32

value :: Int32 -> R Projection

EmbPrj ProjectionLikenessMissing

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ProjectionLikenessMissing -> S Int32

icod_ :: ProjectionLikenessMissing -> S Int32

value :: Int32 -> R ProjectionLikenessMissing

EmbPrj RemoteMetaVariable

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: RemoteMetaVariable -> S Int32

icod_ :: RemoteMetaVariable -> S Int32

value :: Int32 -> R RemoteMetaVariable

EmbPrj RewriteRule

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: RewriteRule -> S Int32

icod_ :: RewriteRule -> S Int32

value :: Int32 -> R RewriteRule

EmbPrj Section

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Section -> S Int32

icod_ :: Section -> S Int32

value :: Int32 -> R Section

EmbPrj Signature

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Signature -> S Int32

icod_ :: Signature -> S Int32

value :: Int32 -> R Signature

EmbPrj System

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: System -> S Int32

icod_ :: System -> S Int32

value :: Int32 -> R System

EmbPrj TCWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: TCWarning -> S Int32

icod_ :: TCWarning -> S Int32

value :: Int32 -> R TCWarning

EmbPrj TermHead

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: TermHead -> S Int32

icod_ :: TermHead -> S Int32

value :: Int32 -> R TermHead

EmbPrj Warning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Warning -> S Int32

icod_ :: Warning -> S Int32

value :: Int32 -> R Warning

EmbPrj RecordFieldWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: RecordFieldWarning -> S Int32

icod_ :: RecordFieldWarning -> S Int32

value :: Int32 -> R RecordFieldWarning

EmbPrj Occurrence

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Occurrence -> S Int32

icod_ :: Occurrence -> S Int32

value :: Int32 -> R Occurrence

EmbPrj AbsNameWithFixity

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbsNameWithFixity -> S Int32

icod_ :: AbsNameWithFixity -> S Int32

value :: Int32 -> R AbsNameWithFixity

EmbPrj SerialisedRange

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: SerialisedRange -> S Int32

icod_ :: SerialisedRange -> S Int32

value :: Int32 -> R SerialisedRange

EmbPrj Impossible

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Impossible -> S Int32

icod_ :: Impossible -> S Int32

value :: Int32 -> R Impossible

EmbPrj Permutation

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Permutation -> S Int32

icod_ :: Permutation -> S Int32

value :: Int32 -> R Permutation

EmbPrj ProfileOption

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ProfileOption -> S Int32

icod_ :: ProfileOption -> S Int32

value :: Int32 -> R ProfileOption

EmbPrj ProfileOptions

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ProfileOptions -> S Int32

icod_ :: ProfileOptions -> S Int32

value :: Int32 -> R ProfileOptions

EmbPrj Void

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Void -> S Int32

icod_ :: Void -> S Int32

value :: Int32 -> R Void

EmbPrj Int32

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Int32 -> S Int32

icod_ :: Int32 -> S Int32

value :: Int32 -> R Int32

EmbPrj CallStack

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: CallStack -> S Int32

icod_ :: CallStack -> S Int32

value :: Int32 -> R CallStack

EmbPrj SrcLoc

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: SrcLoc -> S Int32

icod_ :: SrcLoc -> S Int32

value :: Int32 -> R SrcLoc

EmbPrj Word64

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Word64 -> S Int32

icod_ :: Word64 -> S Int32

value :: Int32 -> R Word64

EmbPrj IntSet

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: IntSet -> S Int32

icod_ :: IntSet -> S Int32

value :: Int32 -> R IntSet

EmbPrj Text

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Text -> S Int32

icod_ :: Text -> S Int32

value :: Int32 -> R Text

EmbPrj Text

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Text -> S Int32

icod_ :: Text -> S Int32

value :: Int32 -> R Text

EmbPrj String

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: String -> S Int32

icod_ :: String -> S Int32

value :: Int32 -> R String

EmbPrj Integer

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Integer -> S Int32

icod_ :: Integer -> S Int32

value :: Int32 -> R Integer

EmbPrj ()

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: () -> S Int32

icod_ :: () -> S Int32

value :: Int32 -> R ()

EmbPrj Bool

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Bool -> S Int32

icod_ :: Bool -> S Int32

value :: Int32 -> R Bool

EmbPrj Char

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Char -> S Int32

icod_ :: Char -> S Int32

value :: Int32 -> R Char

EmbPrj Double

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Double -> S Int32

icod_ :: Double -> S Int32

value :: Int32 -> R Double

EmbPrj Int

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Int -> S Int32

icod_ :: Int -> S Int32

value :: Int32 -> R Int

EmbPrj a => EmbPrj (Pattern' a)

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Pattern' a -> S Int32

icod_ :: Pattern' a -> S Int32

value :: Int32 -> R (Pattern' a)

EmbPrj a => EmbPrj (Arg a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Arg a -> S Int32

icod_ :: Arg a -> S Int32

value :: Int32 -> R (Arg a)

EmbPrj a => EmbPrj (HasEta' a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: HasEta' a -> S Int32

icod_ :: HasEta' a -> S Int32

value :: Int32 -> R (HasEta' a)

EmbPrj a => EmbPrj (Ranged a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Ranged a -> S Int32

icod_ :: Ranged a -> S Int32

value :: Int32 -> R (Ranged a)

EmbPrj a => EmbPrj (WithHiding a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: WithHiding a -> S Int32

icod_ :: WithHiding a -> S Int32

value :: Int32 -> R (WithHiding a)

EmbPrj a => EmbPrj (WithOrigin a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: WithOrigin a -> S Int32

icod_ :: WithOrigin a -> S Int32

value :: Int32 -> R (WithOrigin a)

EmbPrj a => EmbPrj (FieldAssignment' a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FieldAssignment' a -> S Int32

icod_ :: FieldAssignment' a -> S Int32

value :: Int32 -> R (FieldAssignment' a)

EmbPrj a => EmbPrj (Abs a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Abs a -> S Int32

icod_ :: Abs a -> S Int32

value :: Int32 -> R (Abs a)

EmbPrj a => EmbPrj (Dom a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Int32

icod_ :: Dom a -> S Int32

value :: Int32 -> R (Dom a)

EmbPrj a => EmbPrj (Pattern' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Pattern' a -> S Int32

icod_ :: Pattern' a -> S Int32

value :: Int32 -> R (Pattern' a)

EmbPrj a => EmbPrj (Substitution' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Substitution' a -> S Int32

icod_ :: Substitution' a -> S Int32

value :: Int32 -> R (Substitution' a)

EmbPrj a => EmbPrj (Tele a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Tele a -> S Int32

icod_ :: Tele a -> S Int32

value :: Int32 -> R (Tele a)

EmbPrj a => EmbPrj (Type' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Type' a -> S Int32

icod_ :: Type' a -> S Int32

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

EmbPrj a => EmbPrj (Elim' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Elim' a -> S Int32

icod_ :: Elim' a -> S Int32

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

EmbPrj a => EmbPrj (Interval' a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Interval' a -> S Int32

icod_ :: Interval' a -> S Int32

value :: Int32 -> R (Interval' a)

EmbPrj a => EmbPrj (Position' a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Position' a -> S Int32

icod_ :: Position' a -> S Int32

value :: Int32 -> R (Position' a)

EmbPrj a => EmbPrj (Case a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Case a -> S Int32

icod_ :: Case a -> S Int32

value :: Int32 -> R (Case a)

EmbPrj a => EmbPrj (WithArity a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: WithArity a -> S Int32

icod_ :: WithArity a -> S Int32

value :: Int32 -> R (WithArity a)

EmbPrj a => EmbPrj (SplitTree' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: SplitTree' a -> S Int32

icod_ :: SplitTree' a -> S Int32

value :: Int32 -> R (SplitTree' a)

EmbPrj a => EmbPrj (Builtin a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Builtin a -> S Int32

icod_ :: Builtin a -> S Int32

value :: Int32 -> R (Builtin a)

EmbPrj a => EmbPrj (FunctionInverse' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: FunctionInverse' a -> S Int32

icod_ :: FunctionInverse' a -> S Int32

value :: Int32 -> R (FunctionInverse' a)

EmbPrj a => EmbPrj (Judgement a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Judgement a -> S Int32

icod_ :: Judgement a -> S Int32

value :: Int32 -> R (Judgement a)

EmbPrj a => EmbPrj (Open a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Open a -> S Int32

icod_ :: Open a -> S Int32

value :: Int32 -> R (Open a)

EmbPrj a => EmbPrj (List1 a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: List1 a -> S Int32

icod_ :: List1 a -> S Int32

value :: Int32 -> R (List1 a)

EmbPrj a => EmbPrj (List2 a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: List2 a -> S Int32

icod_ :: List2 a -> S Int32

value :: Int32 -> R (List2 a)

EmbPrj a => EmbPrj (Drop a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Drop a -> S Int32

icod_ :: Drop a -> S Int32

value :: Int32 -> R (Drop a)

EmbPrj a => EmbPrj (RangeMap a)

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: RangeMap a -> S Int32

icod_ :: RangeMap a -> S Int32

value :: Int32 -> R (RangeMap a)

EmbPrj a => EmbPrj (Seq a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Seq a -> S Int32

icod_ :: Seq a -> S Int32

value :: Int32 -> R (Seq a)

(Ord a, EmbPrj a) => EmbPrj (Set a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Set a -> S Int32

icod_ :: Set a -> S Int32

value :: Int32 -> R (Set a)

EmbPrj a => EmbPrj (Maybe a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Maybe a -> S Int32

icod_ :: Maybe a -> S Int32

value :: Int32 -> R (Maybe a)

EmbPrj a => EmbPrj (Maybe a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Maybe a -> S Int32

icod_ :: Maybe a -> S Int32

value :: Int32 -> R (Maybe a)

EmbPrj a => EmbPrj [a]

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: [a] -> S Int32

icod_ :: [a] -> S Int32

value :: Int32 -> R [a]

(EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ImportedName' a b -> S Int32

icod_ :: ImportedName' a b -> S Int32

value :: Int32 -> R (ImportedName' a b)

(EmbPrj s, EmbPrj t) => EmbPrj (Named s t)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Named s t -> S Int32

icod_ :: Named s t -> S Int32

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

(EmbPrj k, EmbPrj v, EmbPrj (Tag v)) => EmbPrj (BiMap k v)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: BiMap k v -> S Int32

icod_ :: BiMap k v -> S Int32

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

(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Trie a b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Trie a b -> S Int32

icod_ :: Trie a b -> S Int32

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

(EmbPrj a, Typeable b) => EmbPrj (WithDefault' a b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: WithDefault' a b -> S Int32

icod_ :: WithDefault' a b -> S Int32

value :: Int32 -> R (WithDefault' a b)

(EmbPrj a, EmbPrj b) => EmbPrj (Either a b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Either a b -> S Int32

icod_ :: Either a b -> S Int32

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

(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Map a b -> S Int32

icod_ :: Map a b -> S Int32

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

(Eq k, Hashable k, EmbPrj k, EmbPrj v) => EmbPrj (HashMap k v)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: HashMap k v -> S Int32

icod_ :: HashMap k v -> S Int32

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

(EmbPrj a, EmbPrj b) => EmbPrj (Pair a b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Pair a b -> S Int32

icod_ :: Pair a b -> S Int32

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

(EmbPrj a, EmbPrj b) => EmbPrj (a, b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

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

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

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

(EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj (a, b, c)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

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

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

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

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

Increase entry for a in stats.

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

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

icodeInteger :: Integer -> S Int32

icodeDouble :: Double -> S Int32

icodeString :: String -> S Int32

icodeNode :: Node -> S Int32

icodeMemo

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

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

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]

Instances

IsBase t ~ 'True => ICODE t 'True

Defined in Agda.TypeChecking.Serialise.Base

Methods

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

ICODE t (IsBase t) => ICODE (a -> t) 'False

Defined in Agda.TypeChecking.Serialise.Base

Methods

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

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

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)

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

class VALU t b where

Methods

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

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

Instances

VALU t 'True

Defined in Agda.TypeChecking.Serialise.Base

Methods

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

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

VALU t (IsBase t) => VALU (a -> t) 'False

Defined in Agda.TypeChecking.Serialise.Base

Methods

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

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

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

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