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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Serialise.Base

Synopsis

- data Node
  - = Empty
  - | Cons !Word32 !Node
- data MemoEntry
  - = MEEmpty
  - | MECons !Fingerprint !(Any :: Type) !MemoEntry
- fingerprintNoinline :: TypeRep -> Fingerprint
- lookupME :: Proxy a -> Fingerprint -> MemoEntry -> (a -> b) -> b -> b
- newtype FreshAndReuse = FreshAndReuse {
  - farFresh :: Word32
  }
- farEmpty :: FreshAndReuse
- lensFresh :: Lens' FreshAndReuse Word32
- type QNameId = [NameId]
- qnameId :: QName -> QNameId
- data Dict = Dict {
  - nodeD :: !(HashTable Node Word32)
  - stringD :: !(HashTable String Word32)
  - lTextD :: !(HashTable Text Word32)
  - sTextD :: !(HashTable Text Word32)
  - integerD :: !(HashTable Integer Word32)
  - doubleD :: !(HashTable Double Word32)
  - nameD :: !(HashTable NameId Word32)
  - qnameD :: !(HashTable QNameId Word32)
  - 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
  }
- emptyDict :: Bool -> IO Dict
- type Memo = IOArray Word32 MemoEntry
- data St = St {
  - nodeE :: !(Array Word32 [Word32])
  - stringE :: !(Array Word32 String)
  - lTextE :: !(Array Word32 Text)
  - sTextE :: !(Array Word32 Text)
  - integerE :: !(Array Word32 Integer)
  - doubleE :: !(Array Word32 Double)
  - nodeMemo :: !Memo
  - modFile :: !ModuleToSource
  - includes :: !(List1 AbsolutePath)
  }
- type S a = ReaderT Dict IO a
- type R = StateT St IO
- malformed :: R a
- class Typeable a => EmbPrj a where
  - icode :: a -> S Word32
  - icod_ :: a -> S Word32
  - value :: Word32 -> R a
- goTickIcode :: Typeable a => Proxy a -> S ()
- tickICode :: Typeable a => a -> S ()
- runGetState :: Get a -> ByteString -> ByteOffset -> (a, ByteString, ByteOffset)
- icodeX :: (Eq k, Hashable k) => (Dict -> HashTable k Word32) -> (Dict -> IORef FreshAndReuse) -> k -> S Word32
- icodeInteger :: Integer -> S Word32
- icodeDouble :: Double -> S Word32
- icodeString :: String -> S Word32
- icodeNode :: Node -> S Word32
- icodeMemo :: (Ord a, Hashable a) => (Dict -> HashTable a Word32) -> (Dict -> IORef FreshAndReuse) -> a -> S Word32 -> S Word32
- vcase :: EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
- class ICODE t (b :: Bool) where
  - icodeArgs :: Proxy t -> StrictProducts (Domains t) -> S Node
- icodeN :: (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32), All EmbPrj (Domains t)) => Word32 -> t -> Arrows (Domains t) (S Word32)
- icodeN' :: (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32), All EmbPrj (Domains t)) => t -> Arrows (Domains t) (S Word32)
- class VALU t (b :: Bool) where
  - valuN' :: t -> StrictProducts (Constant Word32 (Domains t)) -> R (CoDomain t)
  - valueArgs :: Proxy t -> [Word32] -> Maybe (StrictProducts (Constant Word32 (Domains t)))
- valuN :: (VALU t (IsBase t), StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)), All EmbPrj (Domains t)) => t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
- valueN :: (VALU t (IsBase t), All EmbPrj (CoDomain t ': Domains t)) => t -> Word32 -> R (CoDomain t)

# Documentation

data Node Source #

Constructor tag (maybe omitted) and argument indices.

Constructors

Empty |
Cons !Word32 !Node |

#### Instances

Instances details

Binary Node Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Base Methods put :: Node -> Put Source # get :: Get Node Source # putList :: [Node] -> Put Source #
Eq Node Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Base Methods (==) :: Node -> Node -> Bool Source # (/=) :: Node -> Node -> Bool Source #
Hashable Node Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Base Methods hashWithSalt :: Int -> Node -> Int Source # hash :: Node -> Int Source #

data MemoEntry Source #

Association lists mapping TypeRep fingerprints to values. In some cases values with different types have the same serialized representation. This structure disambiguates them.

Constructors

MEEmpty |
MECons !Fingerprint !(Any :: Type) !MemoEntry |

fingerprintNoinline :: TypeRep -> Fingerprint Source #

lookupME :: Proxy a -> Fingerprint -> MemoEntry -> (a -> b) -> b -> b Source #

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

- farFresh :: Word32

  Number of hash map misses.

farEmpty :: FreshAndReuse Source #

lensFresh :: Lens' FreshAndReuse Word32 Source #

type QNameId = [NameId] Source #

Two `QName`s 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

- nodeD :: !(HashTable Node Word32)

  Written to interface file.

- stringD :: !(HashTable String Word32)

  Written to interface file.

- lTextD :: !(HashTable Text Word32)

  Written to interface file.

- sTextD :: !(HashTable Text Word32)

  Written to interface file.

- integerD :: !(HashTable Integer Word32)

  Written to interface file.

- doubleD :: !(HashTable Double Word32)

  Written to interface file. Dicitionaries which are not serialized, but provide short cuts to speed up serialization: Andreas, Makoto, AIM XXI Memoizing A.Name does not buy us much if we already memoize A.QName.

- nameD :: !(HashTable NameId Word32)

  Not written to interface file.

- qnameD :: !(HashTable QNameId Word32)

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

Arguments

:: Bool | Collect statistics for `icode` calls?
-> IO Dict |

Creates an empty dictionary.

type Memo = IOArray Word32 MemoEntry Source #

Univeral memo structure, to introduce sharing during decoding

data St Source #

State of the decoder.

Constructors

St |

Fields

- nodeE :: !(Array Word32 [Word32])

  Obtained from interface file.

- stringE :: !(Array Word32 String)

  Obtained from interface file.

- lTextE :: !(Array Word32 Text)

  Obtained from interface file.

- sTextE :: !(Array Word32 Text)

  Obtained from interface file.

- integerE :: !(Array Word32 Integer)

  Obtained from interface file.

- doubleE :: !(Array Word32 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 :: !(List1 AbsolutePath)

  The include directories.

type S a = ReaderT Dict IO a Source #

Monad used by the encoder.

type R = StateT St IO 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 Word32 | Serialization (wrapper).

icod_ Source #

Arguments

:: a |
-> S Word32 | Serialization (worker).

default icod_ :: (Enum a, Bounded a) => a -> S Word32 Source #

value Source #

Arguments

:: Word32 |
-> R a | Deserialization.

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

#### Instances

Instances details

EmbPrj Range Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Range -> S Word32 Source # icod_ :: Range -> S Word32 Source # value :: Word32 -> R Range Source #
EmbPrj ExecutablesFile Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ExecutablesFile -> S Word32 Source # icod_ :: ExecutablesFile -> S Word32 Source # value :: Word32 -> R ExecutablesFile Source #
EmbPrj LibPositionInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: LibPositionInfo -> S Word32 Source # icod_ :: LibPositionInfo -> S Word32 Source # value :: Word32 -> R LibPositionInfo Source #
EmbPrj LibWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: LibWarning -> S Word32 Source # icod_ :: LibWarning -> S Word32 Source # value :: Word32 -> R LibWarning Source #
EmbPrj LibWarning' Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: LibWarning' -> S Word32 Source # icod_ :: LibWarning' -> S Word32 Source # value :: Word32 -> R LibWarning' Source #
EmbPrj OptionsPragma Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OptionsPragma -> S Word32 Source # icod_ :: OptionsPragma -> S Word32 Source # value :: Word32 -> R OptionsPragma Source #
EmbPrj OptionWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: OptionWarning -> S Word32 Source # icod_ :: OptionWarning -> S Word32 Source # value :: Word32 -> R OptionWarning Source #
EmbPrj ConfluenceCheck Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ConfluenceCheck -> S Word32 Source # icod_ :: ConfluenceCheck -> S Word32 Source # value :: Word32 -> R ConfluenceCheck Source #
EmbPrj InfectiveCoinfective Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: InfectiveCoinfective -> S Word32 Source # icod_ :: InfectiveCoinfective -> S Word32 Source # value :: Word32 -> R InfectiveCoinfective Source #
EmbPrj PragmaOptions Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: PragmaOptions -> S Word32 Source # icod_ :: PragmaOptions -> S Word32 Source # value :: Word32 -> R PragmaOptions Source #
EmbPrj WarningMode Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningMode -> S Word32 Source # icod_ :: WarningMode -> S Word32 Source # value :: Word32 -> R WarningMode Source #
EmbPrj WarningModeError Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningModeError -> S Word32 Source # icod_ :: WarningModeError -> S Word32 Source # value :: Word32 -> R WarningModeError Source #
EmbPrj WarningName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningName -> S Word32 Source # icod_ :: WarningName -> S Word32 Source # value :: Word32 -> R WarningName Source #
EmbPrj BindName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: BindName -> S Word32 Source # icod_ :: BindName -> S Word32 Source # value :: Word32 -> R BindName Source #
EmbPrj Pattern Source # | Hackish serialization for patterns that deletes dot patterns. So that we can serialize the `WithClauseProjectionFixityMismatch` without having to define serialization of expressions.
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Pattern -> S Word32 Source # icod_ :: Pattern -> S Word32 Source # value :: Word32 -> R Pattern Source #
EmbPrj AmbiguousQName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: AmbiguousQName -> S Word32 Source # icod_ :: AmbiguousQName -> S Word32 Source # value :: Word32 -> R AmbiguousQName Source #
EmbPrj ModuleName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ModuleName -> S Word32 Source # icod_ :: ModuleName -> S Word32 Source # value :: Word32 -> R ModuleName Source #
EmbPrj Name Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Name -> S Word32 Source # icod_ :: Name -> S Word32 Source # value :: Word32 -> R Name Source #
EmbPrj QName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QName -> S Word32 Source # icod_ :: QName -> S Word32 Source # value :: Word32 -> R QName Source #
EmbPrj Suffix Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Suffix -> S Word32 Source # icod_ :: Suffix -> S Word32 Source # value :: Word32 -> R Suffix Source #
EmbPrj BuiltinId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: BuiltinId -> S Word32 Source # icod_ :: BuiltinId -> S Word32 Source # value :: Word32 -> R BuiltinId Source #
EmbPrj PrimitiveId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: PrimitiveId -> S Word32 Source # icod_ :: PrimitiveId -> S Word32 Source # value :: Word32 -> R PrimitiveId Source #
EmbPrj SomeBuiltin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: SomeBuiltin -> S Word32 Source # icod_ :: SomeBuiltin -> S Word32 Source # value :: Word32 -> R SomeBuiltin Source #
EmbPrj Access Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Access -> S Word32 Source # icod_ :: Access -> S Word32 Source # value :: Word32 -> R Access Source #
EmbPrj Annotation Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Annotation -> S Word32 Source # icod_ :: Annotation -> S Word32 Source # value :: Word32 -> R Annotation Source #
EmbPrj ArgInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ArgInfo -> S Word32 Source # icod_ :: ArgInfo -> S Word32 Source # value :: Word32 -> R ArgInfo Source #
EmbPrj Associativity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Associativity -> S Word32 Source # icod_ :: Associativity -> S Word32 Source # value :: Word32 -> R Associativity Source #
EmbPrj BoundVariablePosition Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: BoundVariablePosition -> S Word32 Source # icod_ :: BoundVariablePosition -> S Word32 Source # value :: Word32 -> R BoundVariablePosition Source #
EmbPrj Catchall Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Catchall -> S Word32 Source # icod_ :: Catchall -> S Word32 Source # value :: Word32 -> R Catchall Source #
EmbPrj Cohesion Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Cohesion -> S Word32 Source # icod_ :: Cohesion -> S Word32 Source # value :: Word32 -> R Cohesion Source #
EmbPrj ConOrigin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ConOrigin -> S Word32 Source # icod_ :: ConOrigin -> S Word32 Source # value :: Word32 -> R ConOrigin Source #
EmbPrj ConstructorOrPatternSynonym Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ConstructorOrPatternSynonym -> S Word32 Source # icod_ :: ConstructorOrPatternSynonym -> S Word32 Source # value :: Word32 -> R ConstructorOrPatternSynonym Source #
EmbPrj Cubical Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Cubical -> S Word32 Source # icod_ :: Cubical -> S Word32 Source # value :: Word32 -> R Cubical Source #
EmbPrj ExpandedEllipsis Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ExpandedEllipsis -> S Word32 Source # icod_ :: ExpandedEllipsis -> S Word32 Source # value :: Word32 -> R ExpandedEllipsis Source #
EmbPrj FileType Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FileType -> S Word32 Source # icod_ :: FileType -> S Word32 Source # value :: Word32 -> R FileType Source #
EmbPrj Fixity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Fixity -> S Word32 Source # icod_ :: Fixity -> S Word32 Source # value :: Word32 -> R Fixity Source #
EmbPrj Fixity' Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Fixity' -> S Word32 Source # icod_ :: Fixity' -> S Word32 Source # value :: Word32 -> R Fixity' Source #
EmbPrj FixityLevel Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FixityLevel -> S Word32 Source # icod_ :: FixityLevel -> S Word32 Source # value :: Word32 -> R FixityLevel Source #
EmbPrj FreeVariables Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FreeVariables -> S Word32 Source # icod_ :: FreeVariables -> S Word32 Source # value :: Word32 -> R FreeVariables Source #
EmbPrj Hiding Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Hiding -> S Word32 Source # icod_ :: Hiding -> S Word32 Source # value :: Word32 -> R Hiding Source #
EmbPrj IsAbstract Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IsAbstract -> S Word32 Source # icod_ :: IsAbstract -> S Word32 Source # value :: Word32 -> R IsAbstract Source #
EmbPrj IsInstance Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IsInstance -> S Word32 Source # icod_ :: IsInstance -> S Word32 Source # value :: Word32 -> R IsInstance Source #
EmbPrj IsOpaque Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IsOpaque -> S Word32 Source # icod_ :: IsOpaque -> S Word32 Source # value :: Word32 -> R IsOpaque Source #
EmbPrj Language Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Language -> S Word32 Source # icod_ :: Language -> S Word32 Source # value :: Word32 -> R Language Source #
EmbPrj Lock Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Lock -> S Word32 Source # icod_ :: Lock -> S Word32 Source # value :: Word32 -> R Lock Source #
EmbPrj MetaId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: MetaId -> S Word32 Source # icod_ :: MetaId -> S Word32 Source # value :: Word32 -> R MetaId Source #
EmbPrj ModalPolarity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ModalPolarity -> S Word32 Source # icod_ :: ModalPolarity -> S Word32 Source # value :: Word32 -> R ModalPolarity Source #
EmbPrj Modality Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Modality -> S Word32 Source # icod_ :: Modality -> S Word32 Source # value :: Word32 -> R Modality Source #
EmbPrj NameId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NameId -> S Word32 Source # icod_ :: NameId -> S Word32 Source # value :: Word32 -> R NameId Source #
EmbPrj NotationPart Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NotationPart -> S Word32 Source # icod_ :: NotationPart -> S Word32 Source # value :: Word32 -> R NotationPart Source #
EmbPrj OpaqueId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OpaqueId -> S Word32 Source # icod_ :: OpaqueId -> S Word32 Source # value :: Word32 -> R OpaqueId Source #
EmbPrj Origin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Origin -> S Word32 Source # icod_ :: Origin -> S Word32 Source # value :: Word32 -> R Origin Source #
EmbPrj OriginIrrelevant Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OriginIrrelevant -> S Word32 Source # icod_ :: OriginIrrelevant -> S Word32 Source # value :: Word32 -> R OriginIrrelevant Source #
EmbPrj OriginRelevant Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OriginRelevant -> S Word32 Source # icod_ :: OriginRelevant -> S Word32 Source # value :: Word32 -> R OriginRelevant Source #
EmbPrj OriginShapeIrrelevant Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OriginShapeIrrelevant -> S Word32 Source # icod_ :: OriginShapeIrrelevant -> S Word32 Source # value :: Word32 -> R OriginShapeIrrelevant Source #
EmbPrj OverlapMode Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OverlapMode -> S Word32 Source # icod_ :: OverlapMode -> S Word32 Source # value :: Word32 -> R OverlapMode Source #
EmbPrj PatternOrCopattern Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: PatternOrCopattern -> S Word32 Source # icod_ :: PatternOrCopattern -> S Word32 Source # value :: Word32 -> R PatternOrCopattern Source #
EmbPrj PolarityModality Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: PolarityModality -> S Word32 Source # icod_ :: PolarityModality -> S Word32 Source # value :: Word32 -> R PolarityModality Source #
EmbPrj ProblemId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ProblemId -> S Word32 Source # icod_ :: ProblemId -> S Word32 Source # value :: Word32 -> R ProblemId Source #
EmbPrj ProjOrigin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ProjOrigin -> S Word32 Source # icod_ :: ProjOrigin -> S Word32 Source # value :: Word32 -> R ProjOrigin Source #
EmbPrj Q0Origin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Q0Origin -> S Word32 Source # icod_ :: Q0Origin -> S Word32 Source # value :: Word32 -> R Q0Origin Source #
EmbPrj Q1Origin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Q1Origin -> S Word32 Source # icod_ :: Q1Origin -> S Word32 Source # value :: Word32 -> R Q1Origin Source #
EmbPrj Quantity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Quantity -> S Word32 Source # icod_ :: Quantity -> S Word32 Source # value :: Word32 -> R Quantity Source #
EmbPrj QωOrigin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QωOrigin -> S Word32 Source # icod_ :: QωOrigin -> S Word32 Source # value :: Word32 -> R QωOrigin Source #
EmbPrj Relevance Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Relevance -> S Word32 Source # icod_ :: Relevance -> S Word32 Source # value :: Word32 -> R Relevance Source #
EmbPrj Aspect Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Aspect -> S Word32 Source # icod_ :: Aspect -> S Word32 Source # value :: Word32 -> R Aspect Source #
EmbPrj Aspects Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Aspects -> S Word32 Source # icod_ :: Aspects -> S Word32 Source # value :: Word32 -> R Aspects Source #
EmbPrj DefinitionSite Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: DefinitionSite -> S Word32 Source # icod_ :: DefinitionSite -> S Word32 Source # value :: Word32 -> R DefinitionSite Source #
EmbPrj Induction Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Induction -> S Word32 Source # icod_ :: Induction -> S Word32 Source # value :: Word32 -> R Induction Source #
EmbPrj NameKind Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: NameKind -> S Word32 Source # icod_ :: NameKind -> S Word32 Source # value :: Word32 -> R NameKind Source #
EmbPrj OtherAspect Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: OtherAspect -> S Word32 Source # icod_ :: OtherAspect -> S Word32 Source # value :: Word32 -> R OtherAspect Source #
EmbPrj TokenBased Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: TokenBased -> S Word32 Source # icod_ :: TokenBased -> S Word32 Source # value :: Word32 -> R TokenBased Source #
EmbPrj KwRange Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: KwRange -> S Word32 Source # icod_ :: KwRange -> S Word32 Source # value :: Word32 -> R KwRange Source #
EmbPrj Doc Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: Doc -> S Word32 Source # icod_ :: Doc -> S Word32 Source # value :: Word32 -> R Doc Source #
EmbPrj RecordDirective Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: RecordDirective -> S Word32 Source # icod_ :: RecordDirective -> S Word32 Source # value :: Word32 -> R RecordDirective Source #
EmbPrj DeclarationWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: DeclarationWarning -> S Word32 Source # icod_ :: DeclarationWarning -> S Word32 Source # value :: Word32 -> R DeclarationWarning Source #
EmbPrj DeclarationWarning' Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: DeclarationWarning' -> S Word32 Source # icod_ :: DeclarationWarning' -> S Word32 Source # value :: Word32 -> R DeclarationWarning' Source #
EmbPrj OpenOrImport Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: OpenOrImport -> S Word32 Source # icod_ :: OpenOrImport -> S Word32 Source # value :: Word32 -> R OpenOrImport Source #
EmbPrj UnicodeOrAscii Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: UnicodeOrAscii -> S Word32 Source # icod_ :: UnicodeOrAscii -> S Word32 Source # value :: Word32 -> R UnicodeOrAscii Source #
EmbPrj Name Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Name -> S Word32 Source # icod_ :: Name -> S Word32 Source # value :: Word32 -> R Name Source #
EmbPrj NameInScope Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NameInScope -> S Word32 Source # icod_ :: NameInScope -> S Word32 Source # value :: Word32 -> R NameInScope Source #
EmbPrj NamePart Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NamePart -> S Word32 Source # icod_ :: NamePart -> S Word32 Source # value :: Word32 -> R NamePart Source #
EmbPrj QName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QName -> S Word32 Source # icod_ :: QName -> S Word32 Source # value :: Word32 -> R QName Source #
EmbPrj ParenPreference Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ParenPreference -> S Word32 Source # icod_ :: ParenPreference -> S Word32 Source # value :: Word32 -> R ParenPreference Source #
EmbPrj Precedence Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Precedence -> S Word32 Source # icod_ :: Precedence -> S Word32 Source # value :: Word32 -> R Precedence Source #
EmbPrj ConPatInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ConPatInfo -> S Word32 Source # icod_ :: ConPatInfo -> S Word32 Source # value :: Word32 -> R ConPatInfo Source #
EmbPrj ConPatLazy Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ConPatLazy -> S Word32 Source # icod_ :: ConPatLazy -> S Word32 Source # value :: Word32 -> R ConPatLazy Source #
EmbPrj Blocked_ Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Blocked_ -> S Word32 Source # icod_ :: Blocked_ -> S Word32 Source # value :: Word32 -> R Blocked_ Source #
EmbPrj Clause Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Clause -> S Word32 Source # icod_ :: Clause -> S Word32 Source # value :: Word32 -> R Clause Source #
EmbPrj ConHead Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConHead -> S Word32 Source # icod_ :: ConHead -> S Word32 Source # value :: Word32 -> R ConHead Source #
EmbPrj ConPatternInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConPatternInfo -> S Word32 Source # icod_ :: ConPatternInfo -> S Word32 Source # value :: Word32 -> R ConPatternInfo Source #
EmbPrj DBPatVar Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DBPatVar -> S Word32 Source # icod_ :: DBPatVar -> S Word32 Source # value :: Word32 -> R DBPatVar Source #
EmbPrj DataOrRecord Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DataOrRecord -> S Word32 Source # icod_ :: DataOrRecord -> S Word32 Source # value :: Word32 -> R DataOrRecord Source #
EmbPrj Level Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Level -> S Word32 Source # icod_ :: Level -> S Word32 Source # value :: Word32 -> R Level Source #
EmbPrj NotBlocked Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NotBlocked -> S Word32 Source # icod_ :: NotBlocked -> S Word32 Source # value :: Word32 -> R NotBlocked Source #
EmbPrj PatOrigin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PatOrigin -> S Word32 Source # icod_ :: PatOrigin -> S Word32 Source # value :: Word32 -> R PatOrigin Source #
EmbPrj PatternInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PatternInfo -> S Word32 Source # icod_ :: PatternInfo -> S Word32 Source # value :: Word32 -> R PatternInfo Source #
EmbPrj PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PlusLevel -> S Word32 Source # icod_ :: PlusLevel -> S Word32 Source # value :: Word32 -> R PlusLevel Source #
EmbPrj Sort Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Sort -> S Word32 Source # icod_ :: Sort -> S Word32 Source # value :: Word32 -> R Sort Source #
EmbPrj Term Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Term -> S Word32 Source # icod_ :: Term -> S Word32 Source # value :: Word32 -> R Term Source #
EmbPrj IsFibrant Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: IsFibrant -> S Word32 Source # icod_ :: IsFibrant -> S Word32 Source # value :: Word32 -> R IsFibrant Source #
EmbPrj Univ Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Univ -> S Word32 Source # icod_ :: Univ -> S Word32 Source # value :: Word32 -> R Univ Source #
EmbPrj Literal Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Literal -> S Word32 Source # icod_ :: Literal -> S Word32 Source # value :: Word32 -> R Literal Source #
EmbPrj ParseWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ParseWarning -> S Word32 Source # icod_ :: ParseWarning -> S Word32 Source # value :: Word32 -> R ParseWarning Source #
EmbPrj Range Source # | Ranges are always deserialised as `noRange`.
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Range -> S Word32 Source # icod_ :: Range -> S Word32 Source # value :: Word32 -> R Range Source #
EmbPrj RangeFile Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: RangeFile -> S Word32 Source # icod_ :: RangeFile -> S Word32 Source # value :: Word32 -> R RangeFile Source #
EmbPrj AbstractModule Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbstractModule -> S Word32 Source # icod_ :: AbstractModule -> S Word32 Source # value :: Word32 -> R AbstractModule Source #
EmbPrj AbstractName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbstractName -> S Word32 Source # icod_ :: AbstractName -> S Word32 Source # value :: Word32 -> R AbstractName Source #
EmbPrj BindingSource Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: BindingSource -> S Word32 Source # icod_ :: BindingSource -> S Word32 Source # value :: Word32 -> R BindingSource Source #
EmbPrj DataOrRecordModule Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: DataOrRecordModule -> S Word32 Source # icod_ :: DataOrRecordModule -> S Word32 Source # value :: Word32 -> R DataOrRecordModule Source #
EmbPrj KindOfName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: KindOfName -> S Word32 Source # icod_ :: KindOfName -> S Word32 Source # value :: Word32 -> R KindOfName Source #
EmbPrj LocalVar Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: LocalVar -> S Word32 Source # icod_ :: LocalVar -> S Word32 Source # value :: Word32 -> R LocalVar Source #
EmbPrj NameMetadata Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameMetadata -> S Word32 Source # icod_ :: NameMetadata -> S Word32 Source # value :: Word32 -> R NameMetadata Source #
EmbPrj NameOrModule Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameOrModule -> S Word32 Source # icod_ :: NameOrModule -> S Word32 Source # value :: Word32 -> R NameOrModule Source #
EmbPrj NameSpace Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameSpace -> S Word32 Source # icod_ :: NameSpace -> S Word32 Source # value :: Word32 -> R NameSpace Source #
EmbPrj NameSpaceId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameSpaceId -> S Word32 Source # icod_ :: NameSpaceId -> S Word32 Source # value :: Word32 -> R NameSpaceId Source #
EmbPrj Scope Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Scope -> S Word32 Source # icod_ :: Scope -> S Word32 Source # value :: Word32 -> R Scope Source #
EmbPrj ScopeInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ScopeInfo -> S Word32 Source # icod_ :: ScopeInfo -> S Word32 Source # value :: Word32 -> R ScopeInfo Source #
EmbPrj WhyInScope Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: WhyInScope -> S Word32 Source # icod_ :: WhyInScope -> S Word32 Source # value :: Word32 -> R WhyInScope Source #
EmbPrj TopLevelModuleName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: TopLevelModuleName -> S Word32 Source # icod_ :: TopLevelModuleName -> S Word32 Source # value :: Word32 -> R TopLevelModuleName Source #
EmbPrj ModuleNameHash Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ModuleNameHash -> S Word32 Source # icod_ :: ModuleNameHash -> S Word32 Source # value :: Word32 -> R ModuleNameHash Source #
EmbPrj CutOff Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: CutOff -> S Word32 Source # icod_ :: CutOff -> S Word32 Source # value :: Word32 -> R CutOff Source #
EmbPrj CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CompiledClauses -> S Word32 Source # icod_ :: CompiledClauses -> S Word32 Source # value :: Word32 -> R CompiledClauses Source #
EmbPrj LazySplit Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: LazySplit -> S Word32 Source # icod_ :: LazySplit -> S Word32 Source # value :: Word32 -> R LazySplit Source #
EmbPrj SplitTag Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: SplitTag -> S Word32 Source # icod_ :: SplitTag -> S Word32 Source # value :: Word32 -> R SplitTag Source #
EmbPrj Key Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Key -> S Word32 Source # icod_ :: Key -> S Word32 Source # value :: Word32 -> R Key Source #
EmbPrj BuiltinSort Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: BuiltinSort -> S Word32 Source # icod_ :: BuiltinSort -> S Word32 Source # value :: Word32 -> R BuiltinSort Source #
EmbPrj CheckpointId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CheckpointId -> S Word32 Source # icod_ :: CheckpointId -> S Word32 Source # value :: Word32 -> R CheckpointId Source #
EmbPrj CompKit Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CompKit -> S Word32 Source # icod_ :: CompKit -> S Word32 Source # value :: Word32 -> R CompKit Source #
EmbPrj CompilerPragma Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: CompilerPragma -> S Word32 Source # icod_ :: CompilerPragma -> S Word32 Source # value :: Word32 -> R CompilerPragma Source #
EmbPrj Definition Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Definition -> S Word32 Source # icod_ :: Definition -> S Word32 Source # value :: Word32 -> R Definition Source #
EmbPrj Defn Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Defn -> S Word32 Source # icod_ :: Defn -> S Word32 Source # value :: Word32 -> R Defn Source #
EmbPrj DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DisplayForm -> S Word32 Source # icod_ :: DisplayForm -> S Word32 Source # value :: Word32 -> R DisplayForm Source #
EmbPrj DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DisplayTerm -> S Word32 Source # icod_ :: DisplayTerm -> S Word32 Source # value :: Word32 -> R DisplayTerm Source #
EmbPrj DoGeneralize Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DoGeneralize -> S Word32 Source # icod_ :: DoGeneralize -> S Word32 Source # value :: Word32 -> R DoGeneralize Source #
EmbPrj EtaEquality Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: EtaEquality -> S Word32 Source # icod_ :: EtaEquality -> S Word32 Source # value :: Word32 -> R EtaEquality Source #
EmbPrj ExtLamInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ExtLamInfo -> S Word32 Source # icod_ :: ExtLamInfo -> S Word32 Source # value :: Word32 -> R ExtLamInfo Source #
EmbPrj ForeignCode Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: ForeignCode -> S Word32 Source # icod_ :: ForeignCode -> S Word32 Source # value :: Word32 -> R ForeignCode Source #
EmbPrj ForeignCodeStack Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: ForeignCodeStack -> S Word32 Source # icod_ :: ForeignCodeStack -> S Word32 Source # value :: Word32 -> R ForeignCodeStack Source #
EmbPrj FunctionFlag Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: FunctionFlag -> S Word32 Source # icod_ :: FunctionFlag -> S Word32 Source # value :: Word32 -> R FunctionFlag Source #
EmbPrj IllegalRewriteRuleReason Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: IllegalRewriteRuleReason -> S Word32 Source # icod_ :: IllegalRewriteRuleReason -> S Word32 Source # value :: Word32 -> R IllegalRewriteRuleReason Source #
EmbPrj InstanceInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: InstanceInfo -> S Word32 Source # icod_ :: InstanceInfo -> S Word32 Source # value :: Word32 -> R InstanceInfo Source #
EmbPrj InstanceTable Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: InstanceTable -> S Word32 Source # icod_ :: InstanceTable -> S Word32 Source # value :: Word32 -> R InstanceTable Source #
EmbPrj Instantiation Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Instantiation -> S Word32 Source # icod_ :: Instantiation -> S Word32 Source # value :: Word32 -> R Instantiation Source #
EmbPrj Interface Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances Methods icode :: Interface -> S Word32 Source # icod_ :: Interface -> S Word32 Source # value :: Word32 -> R Interface Source #
EmbPrj IsAmbiguous Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: IsAmbiguous -> S Word32 Source # icod_ :: IsAmbiguous -> S Word32 Source # value :: Word32 -> R IsAmbiguous Source #
EmbPrj IsForced Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: IsForced -> S Word32 Source # icod_ :: IsForced -> S Word32 Source # value :: Word32 -> R IsForced Source #
EmbPrj LHSOrPatSyn Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: LHSOrPatSyn -> S Word32 Source # icod_ :: LHSOrPatSyn -> S Word32 Source # value :: Word32 -> R LHSOrPatSyn Source #
EmbPrj MutualId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: MutualId -> S Word32 Source # icod_ :: MutualId -> S Word32 Source # value :: Word32 -> R MutualId Source #
EmbPrj NLPSort Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NLPSort -> S Word32 Source # icod_ :: NLPSort -> S Word32 Source # value :: Word32 -> R NLPSort Source #
EmbPrj NLPType Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NLPType -> S Word32 Source # icod_ :: NLPType -> S Word32 Source # value :: Word32 -> R NLPType Source #
EmbPrj NLPat Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NLPat -> S Word32 Source # icod_ :: NLPat -> S Word32 Source # value :: Word32 -> R NLPat Source #
EmbPrj NumGeneralizableArgs Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NumGeneralizableArgs -> S Word32 Source # icod_ :: NumGeneralizableArgs -> S Word32 Source # value :: Word32 -> R NumGeneralizableArgs Source #
EmbPrj OpaqueBlock Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: OpaqueBlock -> S Word32 Source # icod_ :: OpaqueBlock -> S Word32 Source # value :: Word32 -> R OpaqueBlock Source #
EmbPrj ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ProjLams -> S Word32 Source # icod_ :: ProjLams -> S Word32 Source # value :: Word32 -> R ProjLams Source #
EmbPrj Projection Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Projection -> S Word32 Source # icod_ :: Projection -> S Word32 Source # value :: Word32 -> R Projection Source #
EmbPrj ProjectionLikenessMissing Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ProjectionLikenessMissing -> S Word32 Source # icod_ :: ProjectionLikenessMissing -> S Word32 Source # value :: Word32 -> R ProjectionLikenessMissing Source #
EmbPrj RemoteMetaVariable Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: RemoteMetaVariable -> S Word32 Source # icod_ :: RemoteMetaVariable -> S Word32 Source # value :: Word32 -> R RemoteMetaVariable Source #
EmbPrj RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: RewriteRule -> S Word32 Source # icod_ :: RewriteRule -> S Word32 Source # value :: Word32 -> R RewriteRule Source #
EmbPrj Section Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Section -> S Word32 Source # icod_ :: Section -> S Word32 Source # value :: Word32 -> R Section Source #
EmbPrj Signature Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Signature -> S Word32 Source # icod_ :: Signature -> S Word32 Source # value :: Word32 -> R Signature Source #
EmbPrj System Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: System -> S Word32 Source # icod_ :: System -> S Word32 Source # value :: Word32 -> R System Source #
EmbPrj TCWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: TCWarning -> S Word32 Source # icod_ :: TCWarning -> S Word32 Source # value :: Word32 -> R TCWarning Source #
EmbPrj TermHead Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: TermHead -> S Word32 Source # icod_ :: TermHead -> S Word32 Source # value :: Word32 -> R TermHead Source #
EmbPrj Warning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: Warning -> S Word32 Source # icod_ :: Warning -> S Word32 Source # value :: Word32 -> R Warning Source #
EmbPrj Comparison Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Comparison -> S Word32 Source # icod_ :: Comparison -> S Word32 Source # value :: Word32 -> R Comparison Source #
EmbPrj Polarity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Polarity -> S Word32 Source # icod_ :: Polarity -> S Word32 Source # value :: Word32 -> R Polarity Source #
EmbPrj RecordFieldWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: RecordFieldWarning -> S Word32 Source # icod_ :: RecordFieldWarning -> S Word32 Source # value :: Word32 -> R RecordFieldWarning Source #
EmbPrj UselessPublicReason Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: UselessPublicReason -> S Word32 Source # icod_ :: UselessPublicReason -> S Word32 Source # value :: Word32 -> R UselessPublicReason Source #
EmbPrj Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Occurrence -> S Word32 Source # icod_ :: Occurrence -> S Word32 Source # value :: Word32 -> R Occurrence Source #
EmbPrj AbsNameWithFixity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbsNameWithFixity -> S Word32 Source # icod_ :: AbsNameWithFixity -> S Word32 Source # value :: Word32 -> R AbsNameWithFixity Source #
EmbPrj SerialisedRange Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: SerialisedRange -> S Word32 Source # icod_ :: SerialisedRange -> S Word32 Source # value :: Word32 -> R SerialisedRange Source #
EmbPrj Impossible Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Impossible -> S Word32 Source # icod_ :: Impossible -> S Word32 Source # value :: Word32 -> R Impossible Source #
EmbPrj Permutation Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Permutation -> S Word32 Source # icod_ :: Permutation -> S Word32 Source # value :: Word32 -> R Permutation Source #
EmbPrj ProfileOption Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ProfileOption -> S Word32 Source # icod_ :: ProfileOption -> S Word32 Source # value :: Word32 -> R ProfileOption Source #
EmbPrj ProfileOptions Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ProfileOptions -> S Word32 Source # icod_ :: ProfileOptions -> S Word32 Source # value :: Word32 -> R ProfileOptions Source #
EmbPrj IntSet Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IntSet -> S Word32 Source # icod_ :: IntSet -> S Word32 Source # value :: Word32 -> R IntSet Source #
EmbPrj Void Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Void -> S Word32 Source # icod_ :: Void -> S Word32 Source # value :: Word32 -> R Void Source #
EmbPrj Int32 Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Int32 -> S Word32 Source # icod_ :: Int32 -> S Word32 Source # value :: Word32 -> R Int32 Source #
EmbPrj CallStack Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: CallStack -> S Word32 Source # icod_ :: CallStack -> S Word32 Source # value :: Word32 -> R CallStack Source #
EmbPrj SrcLoc Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: SrcLoc -> S Word32 Source # icod_ :: SrcLoc -> S Word32 Source # value :: Word32 -> R SrcLoc Source #
EmbPrj Word32 Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Word32 -> S Word32 Source # icod_ :: Word32 -> S Word32 Source # value :: Word32 -> R Word32 Source #
EmbPrj Word64 Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Word64 -> S Word32 Source # icod_ :: Word64 -> S Word32 Source # value :: Word32 -> R Word64 Source #
EmbPrj Text Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Text -> S Word32 Source # icod_ :: Text -> S Word32 Source # value :: Word32 -> R Text Source #
EmbPrj Text Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Text -> S Word32 Source # icod_ :: Text -> S Word32 Source # value :: Word32 -> R Text Source #
EmbPrj Integer Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Integer -> S Word32 Source # icod_ :: Integer -> S Word32 Source # value :: Word32 -> R Integer Source #
EmbPrj String Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: String -> S Word32 Source # icod_ :: String -> S Word32 Source # value :: Word32 -> R String Source #
EmbPrj () Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: () -> S Word32 Source # icod_ :: () -> S Word32 Source # value :: Word32 -> R () Source #
EmbPrj Bool Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Bool -> S Word32 Source # icod_ :: Bool -> S Word32 Source # value :: Word32 -> R Bool Source #
EmbPrj Char Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Char -> S Word32 Source # icod_ :: Char -> S Word32 Source # value :: Word32 -> R Char Source #
EmbPrj Double Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Double -> S Word32 Source # icod_ :: Double -> S Word32 Source # value :: Word32 -> R Double Source #
EmbPrj Int Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Int -> S Word32 Source # icod_ :: Int -> S Word32 Source # value :: Word32 -> R Int Source #
EmbPrj a => EmbPrj (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Pattern' a -> S Word32 Source # icod_ :: Pattern' a -> S Word32 Source # value :: Word32 -> R (Pattern' a) Source #
EmbPrj a => EmbPrj (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Arg a -> S Word32 Source # icod_ :: Arg a -> S Word32 Source # value :: Word32 -> R (Arg a) Source #
EmbPrj a => EmbPrj (HasEta' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: HasEta' a -> S Word32 Source # icod_ :: HasEta' a -> S Word32 Source # value :: Word32 -> R (HasEta' a) Source #
EmbPrj a => EmbPrj (Ranged a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Ranged a -> S Word32 Source # icod_ :: Ranged a -> S Word32 Source # value :: Word32 -> R (Ranged a) Source #
EmbPrj a => EmbPrj (RecordDirectives' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: RecordDirectives' a -> S Word32 Source # icod_ :: RecordDirectives' a -> S Word32 Source # value :: Word32 -> R (RecordDirectives' a) Source #
EmbPrj a => EmbPrj (WithHiding a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: WithHiding a -> S Word32 Source # icod_ :: WithHiding a -> S Word32 Source # value :: Word32 -> R (WithHiding a) Source #
EmbPrj a => EmbPrj (WithOrigin a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: WithOrigin a -> S Word32 Source # icod_ :: WithOrigin a -> S Word32 Source # value :: Word32 -> R (WithOrigin a) Source #
EmbPrj a => EmbPrj (FieldAssignment' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FieldAssignment' a -> S Word32 Source # icod_ :: FieldAssignment' a -> S Word32 Source # value :: Word32 -> R (FieldAssignment' a) Source #
EmbPrj a => EmbPrj (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Abs a -> S Word32 Source # icod_ :: Abs a -> S Word32 Source # value :: Word32 -> R (Abs a) Source #
EmbPrj a => EmbPrj (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Dom a -> S Word32 Source # icod_ :: Dom a -> S Word32 Source # value :: Word32 -> R (Dom a) Source #
EmbPrj a => EmbPrj (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Pattern' a -> S Word32 Source # icod_ :: Pattern' a -> S Word32 Source # value :: Word32 -> R (Pattern' a) Source #
EmbPrj a => EmbPrj (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Substitution' a -> S Word32 Source # icod_ :: Substitution' a -> S Word32 Source # value :: Word32 -> R (Substitution' a) Source #
EmbPrj a => EmbPrj (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Tele a -> S Word32 Source # icod_ :: Tele a -> S Word32 Source # value :: Word32 -> R (Tele a) Source #
EmbPrj a => EmbPrj (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Type' a -> S Word32 Source # icod_ :: Type' a -> S Word32 Source # value :: Word32 -> R (Type' a) Source #
EmbPrj a => EmbPrj (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Elim' a -> S Word32 Source # icod_ :: Elim' a -> S Word32 Source # value :: Word32 -> R (Elim' a) Source #
EmbPrj a => EmbPrj (Interval' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Interval' a -> S Word32 Source # icod_ :: Interval' a -> S Word32 Source # value :: Word32 -> R (Interval' a) Source #
EmbPrj a => EmbPrj (Position' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Position' a -> S Word32 Source # icod_ :: Position' a -> S Word32 Source # value :: Word32 -> R (Position' a) Source #
EmbPrj a => EmbPrj (Case a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Case a -> S Word32 Source # icod_ :: Case a -> S Word32 Source # value :: Word32 -> R (Case a) Source #
EmbPrj a => EmbPrj (WithArity a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: WithArity a -> S Word32 Source # icod_ :: WithArity a -> S Word32 Source # value :: Word32 -> R (WithArity a) Source #
EmbPrj a => EmbPrj (SplitTree' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: SplitTree' a -> S Word32 Source # icod_ :: SplitTree' a -> S Word32 Source # value :: Word32 -> R (SplitTree' a) Source #
(EmbPrj a, Ord a) => EmbPrj (DiscrimTree a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DiscrimTree a -> S Word32 Source # icod_ :: DiscrimTree a -> S Word32 Source # value :: Word32 -> R (DiscrimTree a) Source #
EmbPrj a => EmbPrj (Builtin a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Builtin a -> S Word32 Source # icod_ :: Builtin a -> S Word32 Source # value :: Word32 -> R (Builtin a) Source #
EmbPrj a => EmbPrj (FunctionInverse' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: FunctionInverse' a -> S Word32 Source # icod_ :: FunctionInverse' a -> S Word32 Source # value :: Word32 -> R (FunctionInverse' a) Source #
EmbPrj a => EmbPrj (Judgement a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Judgement a -> S Word32 Source # icod_ :: Judgement a -> S Word32 Source # value :: Word32 -> R (Judgement a) Source #
EmbPrj a => EmbPrj (Open a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Open a -> S Word32 Source # icod_ :: Open a -> S Word32 Source # value :: Word32 -> R (Open a) Source #
EmbPrj a => EmbPrj (List1 a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: List1 a -> S Word32 Source # icod_ :: List1 a -> S Word32 Source # value :: Word32 -> R (List1 a) Source #
EmbPrj a => EmbPrj (List2 a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: List2 a -> S Word32 Source # icod_ :: List2 a -> S Word32 Source # value :: Word32 -> R (List2 a) Source #
EmbPrj a => EmbPrj (Drop a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Drop a -> S Word32 Source # icod_ :: Drop a -> S Word32 Source # value :: Word32 -> R (Drop a) Source #
EmbPrj a => EmbPrj (RangeMap a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: RangeMap a -> S Word32 Source # icod_ :: RangeMap a -> S Word32 Source # value :: Word32 -> R (RangeMap a) Source #
(Ord a, EmbPrj a) => EmbPrj (Set1 a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Set1 a -> S Word32 Source # icod_ :: Set1 a -> S Word32 Source # value :: Word32 -> R (Set1 a) Source #
Typeable a => EmbPrj (SmallSet a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: SmallSet a -> S Word32 Source # icod_ :: SmallSet a -> S Word32 Source # value :: Word32 -> R (SmallSet a) Source #
EmbPrj a => EmbPrj (Seq a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Seq a -> S Word32 Source # icod_ :: Seq a -> S Word32 Source # value :: Word32 -> 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 Word32 Source # icod_ :: Set a -> S Word32 Source # value :: Word32 -> R (Set a) Source #
EmbPrj a => EmbPrj (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Maybe a -> S Word32 Source # icod_ :: Maybe a -> S Word32 Source # value :: Word32 -> R (Maybe a) Source #
EmbPrj a => EmbPrj (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Maybe a -> S Word32 Source # icod_ :: Maybe a -> S Word32 Source # value :: Word32 -> R (Maybe a) Source #
EmbPrj a => EmbPrj [a] Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: [a] -> S Word32 Source # icod_ :: [a] -> S Word32 Source # value :: Word32 -> R [a] Source #
(EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ImportedName' a b -> S Word32 Source # icod_ :: ImportedName' a b -> S Word32 Source # value :: Word32 -> R (ImportedName' a b) Source #
(EmbPrj s, EmbPrj t) => EmbPrj (Named s t) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Named s t -> S Word32 Source # icod_ :: Named s t -> S Word32 Source # value :: Word32 -> 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 Word32 Source # icod_ :: BiMap k v -> S Word32 Source # value :: Word32 -> 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 Word32 Source # icod_ :: Trie a b -> S Word32 Source # value :: Word32 -> R (Trie a b) Source #
(EmbPrj a, Typeable b) => EmbPrj (WithDefault' a b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: WithDefault' a b -> S Word32 Source # icod_ :: WithDefault' a b -> S Word32 Source # value :: Word32 -> R (WithDefault' 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 Word32 Source # icod_ :: Map a b -> S Word32 Source # value :: Word32 -> R (Map a b) Source #
(EmbPrj a, EmbPrj b) => EmbPrj (Either a b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Either a b -> S Word32 Source # icod_ :: Either a b -> S Word32 Source # value :: Word32 -> R (Either a b) 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 Word32 Source # icod_ :: Pair a b -> S Word32 Source # value :: Word32 -> R (Pair 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 Word32 Source # icod_ :: HashMap k v -> S Word32 Source # value :: Word32 -> R (HashMap k v) Source #
(EmbPrj a, EmbPrj b) => EmbPrj (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: (a, b) -> S Word32 Source # icod_ :: (a, b) -> S Word32 Source # value :: Word32 -> 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 Word32 Source # icod_ :: (a, b, c) -> S Word32 Source # value :: Word32 -> R (a, b, c) Source #

goTickIcode :: Typeable a => Proxy a -> S () Source #

The actual logic of `tickICode` is cold code, so it's out-of-line, to decrease code size and avoid cache pollution.

tickICode :: 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 Word32) -> (Dict -> IORef FreshAndReuse) -> k -> S Word32 Source #

icodeInteger :: Integer -> S Word32 Source #

icodeDouble :: Double -> S Word32 Source #

icodeString :: String -> S Word32 Source #

icodeNode :: Node -> S Word32 Source #

icodeMemo Source #

Arguments

:: (Ord a, Hashable a) |
=> (Dict -> HashTable a Word32) | Memo structure for thing of key `a`.
-> (Dict -> IORef FreshAndReuse) | Statistics.
-> a | Key to the thing.
-> S Word32 | Fallback computation to encode the thing.
-> S Word32 | Encoded thing.

`icode` only if thing has not seen before.

vcase :: EmbPrj a => ([Word32] -> R a) -> Word32 -> R a Source #

`vcase value ix` decodes thing represented by `ix :: Word32` 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 :: Bool) where Source #

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

Methods

icodeArgs :: Proxy t -> StrictProducts (Domains t) -> S Node Source #

#### Instances

Instances details

IsBase t ~ 'True => ICODE t 'True Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Base Methods icodeArgs :: Proxy t -> StrictProducts (Domains t) -> S Node Source #
ICODE t (IsBase t) => ICODE (a -> t) 'False Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Base Methods icodeArgs :: Proxy (a -> t) -> StrictProducts (Domains (a -> t)) -> S Node Source #

icodeN :: (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32), All EmbPrj (Domains t)) => Word32 -> t -> Arrows (Domains t) (S Word32) 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' :: (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32), All EmbPrj (Domains t)) => t -> Arrows (Domains t) (S Word32) Source #

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

class VALU t (b :: Bool) where Source #

Methods

valuN' :: t -> StrictProducts (Constant Word32 (Domains t)) -> R (CoDomain t) Source #

valueArgs :: Proxy t -> [Word32] -> Maybe (StrictProducts (Constant Word32 (Domains t))) Source #

#### Instances

Instances details

VALU t 'True Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Base Methods valuN' :: t -> StrictProducts (Constant Word32 (Domains t)) -> R (CoDomain t) Source # valueArgs :: Proxy t -> [Word32] -> Maybe (StrictProducts (Constant Word32 (Domains t))) Source #
VALU t (IsBase t) => VALU (a -> t) 'False Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Base Methods valuN' :: (a -> t) -> StrictProducts (Constant Word32 (Domains (a -> t))) -> R (CoDomain (a -> t)) Source # valueArgs :: Proxy (a -> t) -> [Word32] -> Maybe (StrictProducts (Constant Word32 (Domains (a -> t)))) Source #

valuN :: (VALU t (IsBase t), StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)), All EmbPrj (Domains t)) => t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t)) Source #

valueN :: (VALU t (IsBase t), All EmbPrj (CoDomain t ': Domains t)) => t -> Word32 -> R (CoDomain t) Source #