Agda.TypeChecking.Serialise.Base

Documentation

type Node = [Int32]

Constructor tag (maybe omitted) and argument indices.

type HashTable k v = BasicHashTable k v

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

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' Int32 FreshAndReuse

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.

• textD :: !(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)
• textC :: !(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.

• absPathD :: !(HashTable AbsolutePath Int32)

  Not written to interface file.

emptyDict

Arguments

:: Bool

Collect statistics for icode calls?

-> IO Dict

Creates an empty dictionary.

data U

Universal type, wraps everything.

Constructors

Typeable a => U !a

type Memo = HashTable (Int32, 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.

• textE :: !(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).

value

Arguments

:: Int32

-> R a

Deserialization.

value

Arguments

:: Enum a

=> Int32

-> R a

Deserialization.

icod_

Arguments

:: Enum a

=> a

-> S Int32

Serialization (worker).

Instances

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 Int32

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Int32 -> S Int32

icod_ :: Int32 -> S Int32

value :: Int32 -> R Int32

EmbPrj Integer

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Integer -> S Int32

icod_ :: Integer -> S Int32

value :: Int32 -> R Integer

EmbPrj Word64

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Word64 -> S Int32

icod_ :: Word64 -> S Int32

value :: Int32 -> R Word64

EmbPrj ()

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: () -> S Int32

icod_ :: () -> S Int32

value :: Int32 -> R ()

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 Void

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Void -> S Int32

icod_ :: Void -> S Int32

value :: Int32 -> R Void

EmbPrj IntSet

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: IntSet -> S Int32

icod_ :: IntSet -> S Int32

value :: Int32 -> R IntSet

EmbPrj Doc

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Doc -> S Int32

icod_ :: Doc -> S Int32

value :: Int32 -> R Doc

EmbPrj CutOff

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: CutOff -> S Int32

icod_ :: CutOff -> S Int32

value :: Int32 -> R CutOff

EmbPrj Impossible

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Impossible -> S Int32

icod_ :: Impossible -> S Int32

value :: Int32 -> R Impossible

EmbPrj Empty

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Empty -> S Int32

icod_ :: Empty -> S Int32

value :: Int32 -> R Empty

EmbPrj WarningName

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningName -> S Int32

icod_ :: WarningName -> S Int32

value :: Int32 -> R WarningName

EmbPrj WarningMode

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningMode -> S Int32

icod_ :: WarningMode -> S Int32

value :: Int32 -> R WarningMode

EmbPrj AbsolutePath

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: AbsolutePath -> S Int32

icod_ :: AbsolutePath -> S Int32

value :: Int32 -> R AbsolutePath

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 Permutation

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Permutation -> S Int32

icod_ :: Permutation -> S Int32

value :: Int32 -> R Permutation

EmbPrj GenPart

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: GenPart -> S Int32

icod_ :: GenPart -> S Int32

value :: Int32 -> R GenPart

EmbPrj ExpandedEllipsis

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ExpandedEllipsis -> S Int32

icod_ :: ExpandedEllipsis -> S Int32

value :: Int32 -> R ExpandedEllipsis

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 Associativity

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Associativity -> S Int32

icod_ :: Associativity -> S Int32

value :: Int32 -> R Associativity

EmbPrj FixityLevel

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FixityLevel -> S Int32

icod_ :: FixityLevel -> S Int32

value :: Int32 -> R FixityLevel

EmbPrj MetaId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: MetaId -> S Int32

icod_ :: MetaId -> S Int32

value :: Int32 -> R MetaId

EmbPrj NameId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NameId -> S Int32

icod_ :: NameId -> S Int32

value :: Int32 -> R NameId

EmbPrj IsAbstract

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: IsAbstract -> S Int32

icod_ :: IsAbstract -> S Int32

value :: Int32 -> R IsAbstract

EmbPrj Access

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Access -> S Int32

icod_ :: Access -> S Int32

value :: Int32 -> R Access

EmbPrj DataOrRecord

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: DataOrRecord -> S Int32

icod_ :: DataOrRecord -> S Int32

value :: Int32 -> R DataOrRecord

EmbPrj ProjOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ProjOrigin -> S Int32

icod_ :: ProjOrigin -> S Int32

value :: Int32 -> R ProjOrigin

EmbPrj ConOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ConOrigin -> S Int32

icod_ :: ConOrigin -> S Int32

value :: Int32 -> R ConOrigin

EmbPrj ArgInfo

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ArgInfo -> S Int32

icod_ :: ArgInfo -> S Int32

value :: Int32 -> R ArgInfo

EmbPrj FreeVariables

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FreeVariables -> S Int32

icod_ :: FreeVariables -> S Int32

value :: Int32 -> R FreeVariables

EmbPrj Origin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Origin -> S Int32

icod_ :: Origin -> S Int32

value :: Int32 -> R Origin

EmbPrj Cohesion

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Cohesion -> S Int32

icod_ :: Cohesion -> S Int32

value :: Int32 -> R Cohesion

EmbPrj Relevance

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Relevance -> S Int32

icod_ :: Relevance -> S Int32

value :: Int32 -> R Relevance

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 Q1Origin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Q1Origin -> S Int32

icod_ :: Q1Origin -> S Int32

value :: Int32 -> R Q1Origin

EmbPrj Q0Origin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Q0Origin -> S Int32

icod_ :: Q0Origin -> S Int32

value :: Int32 -> R Q0Origin

EmbPrj Modality

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Modality -> S Int32

icod_ :: Modality -> S Int32

value :: Int32 -> R Modality

EmbPrj Hiding

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Hiding -> S Int32

icod_ :: Hiding -> S Int32

value :: Int32 -> R Hiding

EmbPrj Induction

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Induction -> S Int32

icod_ :: Induction -> S Int32

value :: Int32 -> R Induction

EmbPrj HasEta

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: HasEta -> S Int32

icod_ :: HasEta -> S Int32

value :: Int32 -> R HasEta

EmbPrj FileType

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FileType -> S Int32

icod_ :: FileType -> S Int32

value :: Int32 -> R FileType

EmbPrj Delayed

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Delayed -> S Int32

icod_ :: Delayed -> S Int32

value :: Int32 -> R Delayed

EmbPrj NameInScope

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NameInScope -> S Int32

icod_ :: NameInScope -> S Int32

value :: Int32 -> R NameInScope

EmbPrj TopLevelModuleName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: TopLevelModuleName -> S Int32

icod_ :: TopLevelModuleName -> S Int32

value :: Int32 -> R TopLevelModuleName

EmbPrj QName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QName -> S Int32

icod_ :: QName -> S Int32

value :: Int32 -> R QName

EmbPrj NamePart

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NamePart -> S Int32

icod_ :: NamePart -> S Int32

value :: Int32 -> R NamePart

EmbPrj Name

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32

icod_ :: Name -> S Int32

value :: Int32 -> R Name

EmbPrj Polarity

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Polarity -> S Int32

icod_ :: Polarity -> S Int32

value :: Int32 -> R Polarity

EmbPrj TCWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: TCWarning -> S Int32

icod_ :: TCWarning -> S Int32

value :: Int32 -> R TCWarning

EmbPrj Warning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Warning -> S Int32

icod_ :: Warning -> S Int32

value :: Int32 -> R Warning

EmbPrj Range

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Range -> S Int32

icod_ :: Range -> S Int32

value :: Int32 -> R Range

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 QName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QName -> S Int32

icod_ :: QName -> S Int32

value :: Int32 -> R QName

EmbPrj Name

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32

icod_ :: Name -> S Int32

value :: Int32 -> R Name

EmbPrj Precedence

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Precedence -> S Int32

icod_ :: Precedence -> S Int32

value :: Int32 -> R Precedence

EmbPrj ParenPreference

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ParenPreference -> S Int32

icod_ :: ParenPreference -> S Int32

value :: Int32 -> R ParenPreference

EmbPrj Literal

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Literal -> S Int32

icod_ :: Literal -> S Int32

value :: Int32 -> R Literal

EmbPrj LibWarning'

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning' -> S Int32

icod_ :: LibWarning' -> S Int32

value :: Int32 -> R LibWarning'

EmbPrj Occurrence

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Occurrence -> S Int32

icod_ :: Occurrence -> S Int32

value :: Int32 -> R Occurrence

EmbPrj SplitTag

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: SplitTag -> S Int32

icod_ :: SplitTag -> S Int32

value :: Int32 -> R SplitTag

EmbPrj LazySplit

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: LazySplit -> S Int32

icod_ :: LazySplit -> S Int32

value :: Int32 -> R LazySplit

EmbPrj CompressedFile

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: CompressedFile -> S Int32

icod_ :: CompressedFile -> S Int32

value :: Int32 -> R CompressedFile

EmbPrj TokenBased

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: TokenBased -> S Int32

icod_ :: TokenBased -> S Int32

value :: Int32 -> R TokenBased

EmbPrj DefinitionSite

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: DefinitionSite -> S Int32

icod_ :: DefinitionSite -> S Int32

value :: Int32 -> R DefinitionSite

EmbPrj Aspects

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspects -> S Int32

icod_ :: Aspects -> S Int32

value :: Int32 -> R Aspects

EmbPrj OtherAspect

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: OtherAspect -> S Int32

icod_ :: OtherAspect -> S Int32

value :: Int32 -> R OtherAspect

EmbPrj NameKind

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: NameKind -> S Int32

icod_ :: NameKind -> S Int32

value :: Int32 -> R NameKind

EmbPrj Aspect

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspect -> S Int32

icod_ :: Aspect -> S Int32

value :: Int32 -> R Aspect

EmbPrj AbstractModule

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractModule -> S Int32

icod_ :: AbstractModule -> S Int32

value :: Int32 -> R AbstractModule

EmbPrj NameMetadata

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameMetadata -> S Int32

icod_ :: NameMetadata -> S Int32

value :: Int32 -> R NameMetadata

EmbPrj AbstractName

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractName -> S Int32

icod_ :: AbstractName -> S Int32

value :: Int32 -> R AbstractName

EmbPrj WhyInScope

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: WhyInScope -> S Int32

icod_ :: WhyInScope -> S Int32

value :: Int32 -> R WhyInScope

EmbPrj KindOfName

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: KindOfName -> S Int32

icod_ :: KindOfName -> S Int32

value :: Int32 -> R KindOfName

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 LocalVar

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: LocalVar -> S Int32

icod_ :: LocalVar -> S Int32

value :: Int32 -> R LocalVar

EmbPrj BindingSource

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindingSource -> S Int32

icod_ :: BindingSource -> S Int32

value :: Int32 -> R BindingSource

EmbPrj ScopeInfo

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ScopeInfo -> S Int32

icod_ :: ScopeInfo -> S Int32

value :: Int32 -> R ScopeInfo

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 ConPatLazy

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ConPatLazy -> S Int32

icod_ :: ConPatLazy -> S Int32

value :: Int32 -> R ConPatLazy

EmbPrj ConPatInfo

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ConPatInfo -> S Int32

icod_ :: ConPatInfo -> S Int32

value :: Int32 -> R ConPatInfo

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Clause -> S Int32

icod_ :: Clause -> S Int32

value :: Int32 -> R Clause

EmbPrj Blocked_

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Blocked_ -> S Int32

icod_ :: Blocked_ -> S Int32

value :: Int32 -> R Blocked_

EmbPrj NotBlocked

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NotBlocked -> S Int32

icod_ :: NotBlocked -> S Int32

value :: Int32 -> R NotBlocked

EmbPrj LevelAtom

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: LevelAtom -> S Int32

icod_ :: LevelAtom -> S Int32

value :: Int32 -> R LevelAtom

EmbPrj PlusLevel

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PlusLevel -> S Int32

icod_ :: PlusLevel -> S Int32

value :: Int32 -> R PlusLevel

EmbPrj Level

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Level -> S Int32

icod_ :: Level -> S Int32

value :: Int32 -> R Level

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 ConHead

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ConHead -> S Int32

icod_ :: ConHead -> S Int32

value :: Int32 -> R ConHead

EmbPrj CompiledClauses

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompiledClauses -> S Int32

icod_ :: CompiledClauses -> S Int32

value :: Int32 -> R CompiledClauses

EmbPrj BindName

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindName -> S Int32

icod_ :: BindName -> S Int32

value :: Int32 -> R BindName

EmbPrj DeclarationWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: DeclarationWarning -> S Int32

icod_ :: DeclarationWarning -> S Int32

value :: Int32 -> R DeclarationWarning

EmbPrj LibWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning -> S Int32

icod_ :: LibWarning -> S Int32

value :: Int32 -> R LibWarning

EmbPrj LibPositionInfo

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibPositionInfo -> S Int32

icod_ :: LibPositionInfo -> S Int32

value :: Int32 -> R LibPositionInfo

EmbPrj PragmaOptions

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: PragmaOptions -> S Int32

icod_ :: PragmaOptions -> S Int32

value :: Int32 -> R PragmaOptions

EmbPrj MutualId

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: MutualId -> S Int32

icod_ :: MutualId -> S Int32

value :: Int32 -> R MutualId

EmbPrj TermHead

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: TermHead -> S Int32

icod_ :: TermHead -> S Int32

value :: Int32 -> R TermHead

EmbPrj Defn

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Defn -> S Int32

icod_ :: Defn -> S Int32

value :: Int32 -> R Defn

EmbPrj CompKit

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompKit -> S Int32

icod_ :: CompKit -> S Int32

value :: Int32 -> R CompKit

EmbPrj FunctionFlag

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: FunctionFlag -> S Int32

icod_ :: FunctionFlag -> S Int32

value :: Int32 -> R FunctionFlag

EmbPrj EtaEquality

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: EtaEquality -> S Int32

icod_ :: EtaEquality -> S Int32

value :: Int32 -> R EtaEquality

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 ExtLamInfo

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ExtLamInfo -> S Int32

icod_ :: ExtLamInfo -> S Int32

value :: Int32 -> R ExtLamInfo

EmbPrj System

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: System -> S Int32

icod_ :: System -> S Int32

value :: Int32 -> R System

EmbPrj CompilerPragma

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

Methods

icode :: CompilerPragma -> S Int32

icod_ :: CompilerPragma -> S Int32

value :: Int32 -> R CompilerPragma

EmbPrj IsForced

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: IsForced -> S Int32

icod_ :: IsForced -> S Int32

value :: Int32 -> R IsForced

EmbPrj NumGeneralizableArgs

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NumGeneralizableArgs -> S Int32

icod_ :: NumGeneralizableArgs -> S Int32

value :: Int32 -> R NumGeneralizableArgs

EmbPrj Definition

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Definition -> S Int32

icod_ :: Definition -> S Int32

value :: Int32 -> R Definition

EmbPrj RewriteRule

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: RewriteRule -> S Int32

icod_ :: RewriteRule -> S Int32

value :: Int32 -> R RewriteRule

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 DisplayTerm

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DisplayTerm -> S Int32

icod_ :: DisplayTerm -> S Int32

value :: Int32 -> R DisplayTerm

EmbPrj DisplayForm

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DisplayForm -> S Int32

icod_ :: DisplayForm -> S Int32

value :: Int32 -> R DisplayForm

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 DoGeneralize

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DoGeneralize -> S Int32

icod_ :: DoGeneralize -> S Int32

value :: Int32 -> R DoGeneralize

EmbPrj Interface

Defined in Agda.TypeChecking.Serialise.Instances

Methods

icode :: Interface -> S Int32

icod_ :: Interface -> S Int32

value :: Int32 -> R Interface

EmbPrj ForeignCode

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

Methods

icode :: ForeignCode -> S Int32

icod_ :: ForeignCode -> S Int32

value :: Int32 -> R ForeignCode

EmbPrj CheckpointId

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CheckpointId -> S Int32

icod_ :: CheckpointId -> S Int32

value :: Int32 -> R CheckpointId

EmbPrj SerialisedRange

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: SerialisedRange -> S Int32

icod_ :: SerialisedRange -> S Int32

value :: Int32 -> R SerialisedRange

EmbPrj AbsNameWithFixity

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbsNameWithFixity -> S Int32

icod_ :: AbsNameWithFixity -> S Int32

value :: Int32 -> R AbsNameWithFixity

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 (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 (NonEmpty a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NonEmpty a -> S Int32

icod_ :: NonEmpty a -> S Int32

value :: Int32 -> R (NonEmpty 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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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)

Typeable b => EmbPrj (WithDefault b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: WithDefault b -> S Int32

icod_ :: WithDefault b -> S Int32

value :: Int32 -> R (WithDefault b)

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

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

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

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: BiMap a b -> S Int32

icod_ :: BiMap a b -> S Int32

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

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