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)
- bstringD :: !(HashTable ByteString 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)
- bstringC :: !(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)
- bstringE :: !(Array Int32 ByteString)
- 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
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
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 :: 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] #

Constructor tag (maybe omitted) and argument indices.

type HashTable k v = BasicHashTable k v #

The type of hashtables used in this module.

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

data FreshAndReuse #

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

Constructors

FreshAndReuse
Fields farFresh :: !Int32 Number of hash map misses. farReuse :: !Int32 Number of hash map hits.

farEmpty :: FreshAndReuse #

lensFresh :: Lens' Int32 FreshAndReuse #

lensReuse :: Lens' Int32 FreshAndReuse #

type QNameId = [NameId] #

Two QNames are equal if their QNameId is equal.

qnameId :: QName -> QNameId #

Computing a qualified names composed ID.

data Dict #

State of the the encoder.

Constructors

Dict

Fields

nodeD :: !(HashTable Node Int32)
Written to interface file.
stringD :: !(HashTable String Int32)
Written to interface file.
bstringD :: !(HashTable ByteString 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)
bstringC :: !(IORef FreshAndReuse)
integerC :: !(IORef FreshAndReuse)
doubleC :: !(IORef FreshAndReuse)
termC :: !(IORef FreshAndReuse)
nameC :: !(IORef FreshAndReuse)
qnameC :: !(IORef FreshAndReuse)
stats :: !(HashTable String Int)
collectStats :: Bool
If True collect in stats the quantities of calls to icode for each Typeable a.
absPathD :: !(HashTable AbsolutePath Int32)
Not written to interface file.

emptyDict #

Arguments

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

Creates an empty dictionary.

data U #

Universal type, wraps everything.

Constructors

Typeable a => U !a

type Memo = HashTable (Int32, TypeRep) U #

Univeral memo structure, to introduce sharing during decoding

data St #

State of the decoder.

Constructors

St

Fields

nodeE :: !(Array Int32 Node)
Obtained from interface file.
stringE :: !(Array Int32 String)
Obtained from interface file.
bstringE :: !(Array Int32 ByteString)
Obtained from interface file.
integerE :: !(Array Int32 Integer)
Obtained from interface file.
doubleE :: !(Array Int32 Double)
Obtained from interface file.
nodeMemo :: !Memo
Created and modified by decoder. Used to introduce sharing while deserializing objects.
modFile :: !ModuleToSource
Maps module names to file names. Constructed by the decoder.
includes :: [AbsolutePath]
The include directories.

type S a = ReaderT Dict IO a #

Monad used by the encoder.

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

Monad used by the decoder.

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

malformed :: R a #

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

class Typeable a => EmbPrj a where #

Minimal complete definition

icod_, value

Methods

icode #

Arguments

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

icod_ #

Arguments

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

value #

Arguments

:: Int32
-> R a	Deserialization.

Instances

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

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

Increase entry for a in stats.

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

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

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

icodeInteger :: Integer -> S Int32 #

icodeDouble :: Double -> S Int32 #

icodeString :: String -> S Int32 #

icodeNode :: Node -> S Int32 #

icodeMemo #

Arguments

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

icode only if thing has not seen before.

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

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

class ICODE t b where #

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

Minimal complete definition

icodeArgs

Methods

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

Instances

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

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

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

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

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

class VALU t b where #

Minimal complete definition

valuN', valueArgs

Methods

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

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

Instances

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

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

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