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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Serialise.Base

Synopsis

- type Node = [Int32]
- type HashTable k v = BasicHashTable k v
- data FreshAndReuse = FreshAndReuse {
  - farFresh :: !Int32
  - farReuse :: !Int32
  }
- farEmpty :: FreshAndReuse
- lensFresh :: Lens' Int32 FreshAndReuse
- lensReuse :: Lens' Int32 FreshAndReuse
- type QNameId = [NameId]
- qnameId :: QName -> QNameId
- data Dict = Dict {
  - nodeD :: !(HashTable Node Int32)
  - stringD :: !(HashTable String Int32)
  - textD :: !(HashTable Text Int32)
  - integerD :: !(HashTable Integer Int32)
  - doubleD :: !(HashTable Double Int32)
  - termD :: !(HashTable (Ptr Term) Int32)
  - nameD :: !(HashTable NameId Int32)
  - qnameD :: !(HashTable QNameId Int32)
  - 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
  - absPathD :: !(HashTable AbsolutePath Int32)
  }
- emptyDict :: Bool -> IO Dict
- data U = Typeable a => U !a
- type Memo = HashTable (Int32, TypeRep) U
- data St = St {
  - nodeE :: !(Array Int32 Node)
  - stringE :: !(Array Int32 String)
  - textE :: !(Array Int32 Text)
  - integerE :: !(Array Int32 Integer)
  - doubleE :: !(Array Int32 Double)
  - nodeMemo :: !Memo
  - modFile :: !ModuleToSource
  - includes :: [AbsolutePath]
  }
- type S a = ReaderT Dict IO a
- type R a = ExceptT TypeError (StateT St IO) a
- malformed :: R a
- class Typeable a => EmbPrj a where
  - icode :: a -> S Int32
  - icod_ :: a -> S Int32
  - value :: Int32 -> R a
- tickICode :: forall a. Typeable a => a -> S ()
- runGetState :: Get a -> ByteString -> ByteOffset -> (a, ByteString, ByteOffset)
- 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 :: (Ord a, Hashable a) => (Dict -> HashTable a Int32) -> (Dict -> IORef FreshAndReuse) -> a -> S Int32 -> S Int32
- vcase :: forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
- class ICODE t b where
  - icodeArgs :: IsBase t ~ b => All EmbPrj (Domains t) => Proxy t -> Products (Domains 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' :: forall t. ICODE t (IsBase t) => Currying (Domains t) (S Int32) => All EmbPrj (Domains t) => t -> Arrows (Domains t) (S Int32)
- class VALU t b where
  - 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)))
- 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)

# Documentation

type Node = [Int32] Source #

Constructor tag (maybe omitted) and argument indices.

type HashTable k v = BasicHashTable k v Source #

The type of hashtables used in this module.

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

data 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 :: !Int32

  Number of hash map misses.

- farReuse :: !Int32

  Number of hash map hits.

farEmpty :: FreshAndReuse Source #

lensFresh :: Lens' Int32 FreshAndReuse Source #

lensReuse :: Lens' Int32 FreshAndReuse 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 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 Source #

Arguments

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

Creates an empty dictionary.

data U Source #

Universal type, wraps everything.

Constructors

Typeable a => U !a |

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

Univeral memo structure, to introduce sharing during decoding

data St Source #

State of the decoder.

Constructors

St |

Fields

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

Monad used by the encoder.

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

Monad used by the decoder.

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

malformed :: R a Source #

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

class Typeable a => EmbPrj a where Source #

Minimal complete definition

Nothing

Methods

icode Source #

Arguments

:: a |
-> S Int32 | Serialization (wrapper).

icod_ Source #

Arguments

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

value Source #

Arguments

:: Int32 |
-> R a | Deserialization.

value Source #

Arguments

:: Enum a |
=> Int32 |
-> R a | Deserialization.

icod_ Source #

Arguments

:: Enum a |
=> a |
-> S Int32 | Serialization (worker).

Instances

EmbPrj Bool Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Bool -> S Int32 Source # icod_ :: Bool -> S Int32 Source # value :: Int32 -> R Bool Source #
EmbPrj Char Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Char -> S Int32 Source # icod_ :: Char -> S Int32 Source # value :: Int32 -> R Char Source #
EmbPrj Double Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Double -> S Int32 Source # icod_ :: Double -> S Int32 Source # value :: Int32 -> R Double Source #
EmbPrj Int Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Int -> S Int32 Source # icod_ :: Int -> S Int32 Source # value :: Int32 -> R Int Source #
EmbPrj Int32 Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Int32 -> S Int32 Source # icod_ :: Int32 -> S Int32 Source # value :: Int32 -> R Int32 Source #
EmbPrj Integer Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Integer -> S Int32 Source # icod_ :: Integer -> S Int32 Source # value :: Int32 -> R Integer Source #
EmbPrj Word64 Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Word64 -> S Int32 Source # icod_ :: Word64 -> S Int32 Source # value :: Int32 -> R Word64 Source #
EmbPrj () Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: () -> S Int32 Source # icod_ :: () -> S Int32 Source # value :: Int32 -> R () Source #
EmbPrj Void Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Void -> S Int32 Source # icod_ :: Void -> S Int32 Source # value :: Int32 -> R Void Source #
EmbPrj String Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: String -> S Int32 Source # icod_ :: String -> S Int32 Source # value :: Int32 -> R String Source #
EmbPrj IntSet Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IntSet -> S Int32 Source # icod_ :: IntSet -> S Int32 Source # value :: Int32 -> R IntSet Source #
EmbPrj Doc Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: Doc -> S Int32 Source # icod_ :: Doc -> S Int32 Source # value :: Int32 -> R Doc Source #
EmbPrj Text Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Text -> S Int32 Source # icod_ :: Text -> S Int32 Source # value :: Int32 -> R Text Source #
EmbPrj CutOff Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: CutOff -> S Int32 Source # icod_ :: CutOff -> S Int32 Source # value :: Int32 -> R CutOff Source #
EmbPrj Impossible Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Impossible -> S Int32 Source # icod_ :: Impossible -> S Int32 Source # value :: Int32 -> R Impossible Source #
EmbPrj Empty Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Empty -> S Int32 Source # icod_ :: Empty -> S Int32 Source # value :: Int32 -> R Empty Source #
EmbPrj WarningName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningName -> S Int32 Source # icod_ :: WarningName -> S Int32 Source # value :: Int32 -> R WarningName Source #
EmbPrj WarningMode Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningMode -> S Int32 Source # icod_ :: WarningMode -> S Int32 Source # value :: Int32 -> R WarningMode Source #
EmbPrj LibWarning' Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: LibWarning' -> S Int32 Source # icod_ :: LibWarning' -> S Int32 Source # value :: Int32 -> R LibWarning' Source #
EmbPrj AbsolutePath Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: AbsolutePath -> S Int32 Source # icod_ :: AbsolutePath -> S Int32 Source # value :: Int32 -> R AbsolutePath Source #
EmbPrj Range Source # | Ranges are always deserialised as `noRange`.
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Range -> S Int32 Source # icod_ :: Range -> S Int32 Source # value :: Int32 -> R Range Source #
EmbPrj Permutation Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Permutation -> S Int32 Source # icod_ :: Permutation -> S Int32 Source # value :: Int32 -> R Permutation Source #
EmbPrj Fixity' Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Fixity' -> S Int32 Source # icod_ :: Fixity' -> S Int32 Source # value :: Int32 -> R Fixity' Source #
EmbPrj MetaId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: MetaId -> S Int32 Source # icod_ :: MetaId -> S Int32 Source # value :: Int32 -> R MetaId Source #
EmbPrj NameId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NameId -> S Int32 Source # icod_ :: NameId -> S Int32 Source # value :: Int32 -> R NameId Source #
EmbPrj IsAbstract Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IsAbstract -> S Int32 Source # icod_ :: IsAbstract -> S Int32 Source # value :: Int32 -> R IsAbstract Source #
EmbPrj Access Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Access -> S Int32 Source # icod_ :: Access -> S Int32 Source # value :: Int32 -> R Access Source #
EmbPrj DataOrRecord Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: DataOrRecord -> S Int32 Source # icod_ :: DataOrRecord -> S Int32 Source # value :: Int32 -> R DataOrRecord Source #
EmbPrj ProjOrigin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ProjOrigin -> S Int32 Source # icod_ :: ProjOrigin -> S Int32 Source # value :: Int32 -> R ProjOrigin Source #
EmbPrj ConOrigin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ConOrigin -> S Int32 Source # icod_ :: ConOrigin -> S Int32 Source # value :: Int32 -> R ConOrigin Source #
EmbPrj ArgInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ArgInfo -> S Int32 Source # icod_ :: ArgInfo -> S Int32 Source # value :: Int32 -> R ArgInfo Source #
EmbPrj FreeVariables Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FreeVariables -> S Int32 Source # icod_ :: FreeVariables -> S Int32 Source # value :: Int32 -> R FreeVariables Source #
EmbPrj Origin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Origin -> S Int32 Source # icod_ :: Origin -> S Int32 Source # value :: Int32 -> R Origin Source #
EmbPrj Relevance Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Relevance -> S Int32 Source # icod_ :: Relevance -> S Int32 Source # value :: Int32 -> R Relevance Source #
EmbPrj Quantity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Quantity -> S Int32 Source # icod_ :: Quantity -> S Int32 Source # value :: Int32 -> R Quantity Source #
EmbPrj Modality Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Modality -> S Int32 Source # icod_ :: Modality -> S Int32 Source # value :: Int32 -> R Modality Source #
EmbPrj Hiding Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Hiding -> S Int32 Source # icod_ :: Hiding -> S Int32 Source # value :: Int32 -> R Hiding Source #
EmbPrj Induction Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Induction -> S Int32 Source # icod_ :: Induction -> S Int32 Source # value :: Int32 -> R Induction Source #
EmbPrj HasEta Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: HasEta -> S Int32 Source # icod_ :: HasEta -> S Int32 Source # value :: Int32 -> R HasEta Source #
EmbPrj FileType Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FileType -> S Int32 Source # icod_ :: FileType -> S Int32 Source # value :: Int32 -> R FileType Source #
EmbPrj Delayed Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Delayed -> S Int32 Source # icod_ :: Delayed -> S Int32 Source # value :: Int32 -> R Delayed Source #
EmbPrj GenPart Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: GenPart -> S Int32 Source # icod_ :: GenPart -> S Int32 Source # value :: Int32 -> R GenPart Source #
EmbPrj NameInScope Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NameInScope -> S Int32 Source # icod_ :: NameInScope -> S Int32 Source # value :: Int32 -> R NameInScope Source #
EmbPrj TopLevelModuleName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: TopLevelModuleName -> S Int32 Source # icod_ :: TopLevelModuleName -> S Int32 Source # value :: Int32 -> R TopLevelModuleName Source #
EmbPrj QName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QName -> S Int32 Source # icod_ :: QName -> S Int32 Source # value :: Int32 -> R QName Source #
EmbPrj NamePart Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NamePart -> S Int32 Source # icod_ :: NamePart -> S Int32 Source # value :: Int32 -> R NamePart Source #
EmbPrj Name Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Name -> S Int32 Source # icod_ :: Name -> S Int32 Source # value :: Int32 -> R Name Source #
EmbPrj AmbiguousQName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: AmbiguousQName -> S Int32 Source # icod_ :: AmbiguousQName -> S Int32 Source # value :: Int32 -> R AmbiguousQName Source #
EmbPrj ModuleName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ModuleName -> S Int32 Source # icod_ :: ModuleName -> S Int32 Source # value :: Int32 -> R ModuleName Source #
EmbPrj QName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QName -> S Int32 Source # icod_ :: QName -> S Int32 Source # value :: Int32 -> R QName Source #
EmbPrj Name Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Name -> S Int32 Source # icod_ :: Name -> S Int32 Source # value :: Int32 -> R Name Source #
EmbPrj Literal Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Literal -> S Int32 Source # icod_ :: Literal -> S Int32 Source # value :: Int32 -> R Literal Source #
EmbPrj Precedence Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Precedence -> S Int32 Source # icod_ :: Precedence -> S Int32 Source # value :: Int32 -> R Precedence Source #
EmbPrj ParenPreference Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ParenPreference -> S Int32 Source # icod_ :: ParenPreference -> S Int32 Source # value :: Int32 -> R ParenPreference Source #
EmbPrj Fixity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Fixity -> S Int32 Source # icod_ :: Fixity -> S Int32 Source # value :: Int32 -> R Fixity Source #
EmbPrj Associativity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Associativity -> S Int32 Source # icod_ :: Associativity -> S Int32 Source # value :: Int32 -> R Associativity Source #
EmbPrj PrecedenceLevel Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: PrecedenceLevel -> S Int32 Source # icod_ :: PrecedenceLevel -> S Int32 Source # value :: Int32 -> R PrecedenceLevel Source #
EmbPrj Range Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Range -> S Int32 Source # icod_ :: Range -> S Int32 Source # value :: Int32 -> R Range Source #
EmbPrj Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Occurrence -> S Int32 Source # icod_ :: Occurrence -> S Int32 Source # value :: Int32 -> R Occurrence Source #
EmbPrj CompressedFile Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: CompressedFile -> S Int32 Source # icod_ :: CompressedFile -> S Int32 Source # value :: Int32 -> R CompressedFile Source #
EmbPrj TokenBased Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: TokenBased -> S Int32 Source # icod_ :: TokenBased -> S Int32 Source # value :: Int32 -> R TokenBased Source #
EmbPrj DefinitionSite Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: DefinitionSite -> S Int32 Source # icod_ :: DefinitionSite -> S Int32 Source # value :: Int32 -> R DefinitionSite Source #
EmbPrj Aspects Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Aspects -> S Int32 Source # icod_ :: Aspects -> S Int32 Source # value :: Int32 -> R Aspects Source #
EmbPrj OtherAspect Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: OtherAspect -> S Int32 Source # icod_ :: OtherAspect -> S Int32 Source # value :: Int32 -> R OtherAspect Source #
EmbPrj NameKind Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: NameKind -> S Int32 Source # icod_ :: NameKind -> S Int32 Source # value :: Int32 -> R NameKind Source #
EmbPrj Aspect Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Aspect -> S Int32 Source # icod_ :: Aspect -> S Int32 Source # value :: Int32 -> R Aspect Source #
EmbPrj AbstractModule Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbstractModule -> S Int32 Source # icod_ :: AbstractModule -> S Int32 Source # value :: Int32 -> R AbstractModule Source #
EmbPrj NameMetadata Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameMetadata -> S Int32 Source # icod_ :: NameMetadata -> S Int32 Source # value :: Int32 -> R NameMetadata Source #
EmbPrj AbstractName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbstractName -> S Int32 Source # icod_ :: AbstractName -> S Int32 Source # value :: Int32 -> R AbstractName Source #
EmbPrj WhyInScope Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: WhyInScope -> S Int32 Source # icod_ :: WhyInScope -> S Int32 Source # value :: Int32 -> R WhyInScope Source #
EmbPrj KindOfName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: KindOfName -> S Int32 Source # icod_ :: KindOfName -> S Int32 Source # value :: Int32 -> R KindOfName Source #
EmbPrj NameSpace Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameSpace -> S Int32 Source # icod_ :: NameSpace -> S Int32 Source # value :: Int32 -> R NameSpace Source #
EmbPrj LocalVar Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: LocalVar -> S Int32 Source # icod_ :: LocalVar -> S Int32 Source # value :: Int32 -> R LocalVar Source #
EmbPrj Binder Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Binder -> S Int32 Source # icod_ :: Binder -> S Int32 Source # value :: Int32 -> R Binder Source #
EmbPrj ScopeInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ScopeInfo -> S Int32 Source # icod_ :: ScopeInfo -> S Int32 Source # value :: Int32 -> R ScopeInfo Source #
EmbPrj NameSpaceId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameSpaceId -> S Int32 Source # icod_ :: NameSpaceId -> S Int32 Source # value :: Int32 -> R NameSpaceId Source #
EmbPrj Scope Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Scope -> S Int32 Source # icod_ :: Scope -> S Int32 Source # value :: Int32 -> R Scope Source #
EmbPrj ConPatLazy Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ConPatLazy -> S Int32 Source # icod_ :: ConPatLazy -> S Int32 Source # value :: Int32 -> R ConPatLazy Source #
EmbPrj ConPatInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ConPatInfo -> S Int32 Source # icod_ :: ConPatInfo -> S Int32 Source # value :: Int32 -> R ConPatInfo Source #
EmbPrj ConPatternInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConPatternInfo -> S Int32 Source # icod_ :: ConPatternInfo -> S Int32 Source # value :: Int32 -> R ConPatternInfo Source #
EmbPrj DBPatVar Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DBPatVar -> S Int32 Source # icod_ :: DBPatVar -> S Int32 Source # value :: Int32 -> R DBPatVar Source #
EmbPrj PatOrigin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PatOrigin -> S Int32 Source # icod_ :: PatOrigin -> S Int32 Source # value :: Int32 -> R PatOrigin Source #
EmbPrj Clause Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Clause -> S Int32 Source # icod_ :: Clause -> S Int32 Source # value :: Int32 -> R Clause Source #
EmbPrj LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: LevelAtom -> S Int32 Source # icod_ :: LevelAtom -> S Int32 Source # value :: Int32 -> R LevelAtom Source #
EmbPrj PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PlusLevel -> S Int32 Source # icod_ :: PlusLevel -> S Int32 Source # value :: Int32 -> R PlusLevel Source #
EmbPrj Level Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Level -> S Int32 Source # icod_ :: Level -> S Int32 Source # value :: Int32 -> R Level Source #
EmbPrj Sort Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Sort -> S Int32 Source # icod_ :: Sort -> S Int32 Source # value :: Int32 -> R Sort Source #
EmbPrj Term Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Term -> S Int32 Source # icod_ :: Term -> S Int32 Source # value :: Int32 -> R Term Source #
EmbPrj ConHead Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConHead -> S Int32 Source # icod_ :: ConHead -> S Int32 Source # value :: Int32 -> R ConHead Source #
EmbPrj SplitTag Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: SplitTag -> S Int32 Source # icod_ :: SplitTag -> S Int32 Source # value :: Int32 -> R SplitTag Source #
EmbPrj CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CompiledClauses -> S Int32 Source # icod_ :: CompiledClauses -> S Int32 Source # value :: Int32 -> R CompiledClauses Source #
EmbPrj BindName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: BindName -> S Int32 Source # icod_ :: BindName -> S Int32 Source # value :: Int32 -> R BindName Source #
EmbPrj DeclarationWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: DeclarationWarning -> S Int32 Source # icod_ :: DeclarationWarning -> S Int32 Source # value :: Int32 -> R DeclarationWarning Source #
EmbPrj LibWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: LibWarning -> S Int32 Source # icod_ :: LibWarning -> S Int32 Source # value :: Int32 -> R LibWarning Source #
EmbPrj LibPositionInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: LibPositionInfo -> S Int32 Source # icod_ :: LibPositionInfo -> S Int32 Source # value :: Int32 -> R LibPositionInfo Source #
EmbPrj PragmaOptions Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: PragmaOptions -> S Int32 Source # icod_ :: PragmaOptions -> S Int32 Source # value :: Int32 -> R PragmaOptions Source #
EmbPrj TCWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: TCWarning -> S Int32 Source # icod_ :: TCWarning -> S Int32 Source # value :: Int32 -> R TCWarning Source #
EmbPrj Warning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: Warning -> S Int32 Source # icod_ :: Warning -> S Int32 Source # value :: Int32 -> R Warning Source #
EmbPrj MutualId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: MutualId -> S Int32 Source # icod_ :: MutualId -> S Int32 Source # value :: Int32 -> R MutualId Source #
EmbPrj TermHead Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: TermHead -> S Int32 Source # icod_ :: TermHead -> S Int32 Source # value :: Int32 -> R TermHead Source #
EmbPrj Defn Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Defn -> S Int32 Source # icod_ :: Defn -> S Int32 Source # value :: Int32 -> R Defn Source #
EmbPrj CompKit Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CompKit -> S Int32 Source # icod_ :: CompKit -> S Int32 Source # value :: Int32 -> R CompKit Source #
EmbPrj FunctionFlag Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: FunctionFlag -> S Int32 Source # icod_ :: FunctionFlag -> S Int32 Source # value :: Int32 -> R FunctionFlag Source #
EmbPrj EtaEquality Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: EtaEquality -> S Int32 Source # icod_ :: EtaEquality -> S Int32 Source # value :: Int32 -> R EtaEquality Source #
EmbPrj ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ProjLams -> S Int32 Source # icod_ :: ProjLams -> S Int32 Source # value :: Int32 -> R ProjLams Source #
EmbPrj Projection Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Projection -> S Int32 Source # icod_ :: Projection -> S Int32 Source # value :: Int32 -> R Projection Source #
EmbPrj ExtLamInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ExtLamInfo -> S Int32 Source # icod_ :: ExtLamInfo -> S Int32 Source # value :: Int32 -> R ExtLamInfo Source #
EmbPrj System Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: System -> S Int32 Source # icod_ :: System -> S Int32 Source # value :: Int32 -> R System Source #
EmbPrj CompilerPragma Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: CompilerPragma -> S Int32 Source # icod_ :: CompilerPragma -> S Int32 Source # value :: Int32 -> R CompilerPragma Source #
EmbPrj IsForced Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: IsForced -> S Int32 Source # icod_ :: IsForced -> S Int32 Source # value :: Int32 -> R IsForced Source #
EmbPrj Polarity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Polarity -> S Int32 Source # icod_ :: Polarity -> S Int32 Source # value :: Int32 -> R Polarity Source #
EmbPrj NumGeneralizableArgs Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NumGeneralizableArgs -> S Int32 Source # icod_ :: NumGeneralizableArgs -> S Int32 Source # value :: Int32 -> R NumGeneralizableArgs Source #
EmbPrj Definition Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Definition -> S Int32 Source # icod_ :: Definition -> S Int32 Source # value :: Int32 -> R Definition Source #
EmbPrj RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: RewriteRule -> S Int32 Source # icod_ :: RewriteRule -> S Int32 Source # value :: Int32 -> R RewriteRule Source #
EmbPrj NLPType Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NLPType -> S Int32 Source # icod_ :: NLPType -> S Int32 Source # value :: Int32 -> R NLPType Source #
EmbPrj NLPat Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NLPat -> S Int32 Source # icod_ :: NLPat -> S Int32 Source # value :: Int32 -> R NLPat Source #
EmbPrj DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DisplayTerm -> S Int32 Source # icod_ :: DisplayTerm -> S Int32 Source # value :: Int32 -> R DisplayTerm Source #
EmbPrj DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DisplayForm -> S Int32 Source # icod_ :: DisplayForm -> S Int32 Source # value :: Int32 -> R DisplayForm Source #
EmbPrj Section Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Section -> S Int32 Source # icod_ :: Section -> S Int32 Source # value :: Int32 -> R Section Source #
EmbPrj Signature Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Signature -> S Int32 Source # icod_ :: Signature -> S Int32 Source # value :: Int32 -> R Signature Source #
EmbPrj DoGeneralize Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DoGeneralize -> S Int32 Source # icod_ :: DoGeneralize -> S Int32 Source # value :: Int32 -> R DoGeneralize Source #
EmbPrj Interface Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances Methods icode :: Interface -> S Int32 Source # icod_ :: Interface -> S Int32 Source # value :: Int32 -> R Interface Source #
EmbPrj ForeignCode Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: ForeignCode -> S Int32 Source # icod_ :: ForeignCode -> S Int32 Source # value :: Int32 -> R ForeignCode Source #
EmbPrj CheckpointId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CheckpointId -> S Int32 Source # icod_ :: CheckpointId -> S Int32 Source # value :: Int32 -> R CheckpointId Source #
EmbPrj SerialisedRange Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: SerialisedRange -> S Int32 Source # icod_ :: SerialisedRange -> S Int32 Source # value :: Int32 -> R SerialisedRange Source #
EmbPrj a => EmbPrj [a] Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: [a] -> S Int32 Source # icod_ :: [a] -> S Int32 Source # value :: Int32 -> R [a] Source #
EmbPrj a => EmbPrj (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Maybe a -> S Int32 Source # icod_ :: Maybe a -> S Int32 Source # value :: Int32 -> R (Maybe a) Source #
EmbPrj a => EmbPrj (Seq a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Seq a -> S Int32 Source # icod_ :: Seq a -> S Int32 Source # value :: Int32 -> R (Seq a) Source #
(Ord a, EmbPrj a) => EmbPrj (Set a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Set a -> S Int32 Source # icod_ :: Set a -> S Int32 Source # value :: Int32 -> R (Set a) Source #
EmbPrj a => EmbPrj (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Maybe a -> S Int32 Source # icod_ :: Maybe a -> S Int32 Source # value :: Int32 -> R (Maybe a) Source #
EmbPrj a => EmbPrj (NonemptyList a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NonemptyList a -> S Int32 Source # icod_ :: NonemptyList a -> S Int32 Source # value :: Int32 -> R (NonemptyList a) Source #
EmbPrj a => EmbPrj (Interval' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Interval' a -> S Int32 Source # icod_ :: Interval' a -> S Int32 Source # value :: Int32 -> R (Interval' a) Source #
EmbPrj a => EmbPrj (Position' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Position' a -> S Int32 Source # icod_ :: Position' a -> S Int32 Source # value :: Int32 -> R (Position' a) Source #
EmbPrj a => EmbPrj (Drop a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Drop a -> S Int32 Source # icod_ :: Drop a -> S Int32 Source # value :: Int32 -> R (Drop a) Source #
EmbPrj a => EmbPrj (Ranged a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Ranged a -> S Int32 Source # icod_ :: Ranged a -> S Int32 Source # value :: Int32 -> R (Ranged a) Source #
EmbPrj a => EmbPrj (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Dom a -> S Int32 Source # icod_ :: Dom a -> S Int32 Source # value :: Int32 -> R (Dom a) Source #
EmbPrj a => EmbPrj (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Arg a -> S Int32 Source # icod_ :: Arg a -> S Int32 Source # value :: Int32 -> R (Arg a) Source #
EmbPrj a => EmbPrj (WithHiding a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: WithHiding a -> S Int32 Source # icod_ :: WithHiding a -> S Int32 Source # value :: Int32 -> R (WithHiding a) Source #
EmbPrj a => EmbPrj (FieldAssignment' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FieldAssignment' a -> S Int32 Source # icod_ :: FieldAssignment' a -> S Int32 Source # value :: Int32 -> R (FieldAssignment' a) Source #
EmbPrj a => EmbPrj (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Substitution' a -> S Int32 Source # icod_ :: Substitution' a -> S Int32 Source # value :: Int32 -> R (Substitution' a) Source #
EmbPrj a => EmbPrj (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Pattern' a -> S Int32 Source # icod_ :: Pattern' a -> S Int32 Source # value :: Int32 -> R (Pattern' a) Source #
EmbPrj a => EmbPrj (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Tele a -> S Int32 Source # icod_ :: Tele a -> S Int32 Source # value :: Int32 -> R (Tele a) Source #
EmbPrj a => EmbPrj (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Type' a -> S Int32 Source # icod_ :: Type' a -> S Int32 Source # value :: Int32 -> R (Type' a) Source #
EmbPrj a => EmbPrj (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Abs a -> S Int32 Source # icod_ :: Abs a -> S Int32 Source # value :: Int32 -> R (Abs a) Source #
EmbPrj a => EmbPrj (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Elim' a -> S Int32 Source # icod_ :: Elim' a -> S Int32 Source # value :: Int32 -> R (Elim' a) Source #
EmbPrj a => EmbPrj (SplitTree' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: SplitTree' a -> S Int32 Source # icod_ :: SplitTree' a -> S Int32 Source # value :: Int32 -> R (SplitTree' a) Source #
EmbPrj a => EmbPrj (Case a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Case a -> S Int32 Source # icod_ :: Case a -> S Int32 Source # value :: Int32 -> R (Case a) Source #
EmbPrj a => EmbPrj (WithArity a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: WithArity a -> S Int32 Source # icod_ :: WithArity a -> S Int32 Source # value :: Int32 -> R (WithArity a) Source #
EmbPrj a => EmbPrj (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Pattern' a -> S Int32 Source # icod_ :: Pattern' a -> S Int32 Source # value :: Int32 -> R (Pattern' a) Source #
Typeable b => EmbPrj (WithDefault b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: WithDefault b -> S Int32 Source # icod_ :: WithDefault b -> S Int32 Source # value :: Int32 -> R (WithDefault b) Source #
EmbPrj a => EmbPrj (Builtin a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Builtin a -> S Int32 Source # icod_ :: Builtin a -> S Int32 Source # value :: Int32 -> R (Builtin a) Source #
EmbPrj a => EmbPrj (FunctionInverse' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: FunctionInverse' a -> S Int32 Source # icod_ :: FunctionInverse' a -> S Int32 Source # value :: Int32 -> R (FunctionInverse' a) Source #
EmbPrj a => EmbPrj (Open a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Open a -> S Int32 Source # icod_ :: Open a -> S Int32 Source # value :: Int32 -> R (Open a) Source #
(EmbPrj a, EmbPrj b) => EmbPrj (Either a b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Either a b -> S Int32 Source # icod_ :: Either a b -> S Int32 Source # value :: Int32 -> R (Either a b) Source #
(EmbPrj a, EmbPrj b) => EmbPrj (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: (a, b) -> S Int32 Source # icod_ :: (a, b) -> S Int32 Source # value :: Int32 -> R (a, b) Source #
(Eq k, Hashable k, EmbPrj k, EmbPrj v) => EmbPrj (HashMap k v) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: HashMap k v -> S Int32 Source # icod_ :: HashMap k v -> S Int32 Source # value :: Int32 -> R (HashMap k v) Source #
(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Map a b -> S Int32 Source # icod_ :: Map a b -> S Int32 Source # value :: Int32 -> R (Map a b) Source #
(Ord a, Ord b, EmbPrj a, EmbPrj b) => EmbPrj (BiMap a b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: BiMap a b -> S Int32 Source # icod_ :: BiMap a b -> S Int32 Source # value :: Int32 -> R (BiMap a b) Source #
(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Trie a b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Trie a b -> S Int32 Source # icod_ :: Trie a b -> S Int32 Source # value :: Int32 -> R (Trie a b) Source #
(EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ImportedName' a b -> S Int32 Source # icod_ :: ImportedName' a b -> S Int32 Source # value :: Int32 -> 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 Int32 Source # icod_ :: Named s t -> S Int32 Source # value :: Int32 -> R (Named s t) Source #
(EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj (a, b, c) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: (a, b, c) -> S Int32 Source # icod_ :: (a, b, c) -> S Int32 Source # value :: Int32 -> R (a, b, c) Source #

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

Increase entry for `a` in `stats`.

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

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

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

icodeInteger :: Integer -> S Int32 Source #

icodeDouble :: Double -> S Int32 Source #

icodeString :: String -> S Int32 Source #

icodeNode :: Node -> S Int32 Source #

icodeMemo Source #

Arguments

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

`icode` only if thing has not seen before.

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

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

class ICODE t b where Source #

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

Methods

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

Instances

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

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

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

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

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

class VALU t b where Source #

Methods

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

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

Instances

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

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

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