Copyright	(c) Sirui Lu 2021-2024
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	None
Language	Haskell2010

Grisette.Internal.SymPrim.Prim.Internal.Caches

Description

Synopsis

data SomeStableName where
- SomeStableName :: forall a. StableName a -> SomeStableName
type Id = Word32
type StableIdent = StableName (Any :: Type)
type Digest = Word32
data CachedInfo = CachedInfo {
- cachedThreadId :: !WeakThreadId
- cachedDigest :: !Digest
- cachedId :: !Id
- cachedStableIdent :: !StableIdent
}
class Interned t where
- data Description t
- type Uninterned t
- describe :: Uninterned t -> Description t
- identify :: CachedInfo -> Uninterned t -> t
- threadId :: t -> WeakThreadId
- descriptionDigest :: Description t -> Digest
intern :: (Interned t, Typeable t, Hashable (Description t), Eq (Description t)) => Uninterned t -> IO t
haveCache :: IO Bool
threadCacheSize :: WeakThreadId -> IO Int
threadCacheLiveSize :: WeakThreadId -> IO Int

Documentation

data SomeStableName where Source #

A type-erased stable name.

Constructors

SomeStableName :: forall a. StableName a -> SomeStableName

Instances

Instances details

Eq SomeStableName Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Utils Methods (==) :: SomeStableName -> SomeStableName -> Bool # (/=) :: SomeStableName -> SomeStableName -> Bool #

type Id = Word32 Source #

A unique identifier for a term.

type StableIdent = StableName (Any :: Type) Source #

The identity of a term.

type Digest = Word32 Source #

A digest of a term.

data CachedInfo Source #

Information about a cached term.

Constructors

CachedInfo
Fields cachedThreadId :: !WeakThreadId cachedDigest :: !Digest cachedId :: !Id cachedStableIdent :: !StableIdent

Instances

Instances details

NFData CachedInfo Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods rnf :: CachedInfo -> () #

class Interned t where Source #

A class for interning terms.

Associated Types

data Description t Source #

type Uninterned t Source #

Methods

describe :: Uninterned t -> Description t Source #

identify :: CachedInfo -> Uninterned t -> t Source #

threadId :: t -> WeakThreadId Source #

descriptionDigest :: Description t -> Digest Source #

Instances

Instances details

Interned (Term t) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Associated Types

data Description (Term t)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term data Description (Term t) where DConTerm :: forall t. (t -> t -> Bool) -> !Digest -> t -> Description (Term t) DSymTerm :: forall t. !Digest -> TypedSymbol 'AnyKind t -> Description (Term t) DForallTerm :: forall t1. !Digest -> !(TypedSymbol 'ConstantKind t1) -> !HashId -> Description (Term Bool) DExistsTerm :: forall t1. !Digest -> !(TypedSymbol 'ConstantKind t1) -> !HashId -> Description (Term Bool) DNotTerm :: !Digest -> !HashId -> Description (Term Bool) DOrTerm :: !Digest -> !HashId -> !HashId -> Description (Term Bool) DAndTerm :: !Digest -> !HashId -> !HashId -> Description (Term Bool) DEqTerm :: !Digest -> Fingerprint -> !HashId -> !HashId -> Description (Term Bool) DDistinctTerm :: !Digest -> Fingerprint -> !(NonEmpty HashId) -> Description (Term Bool) DITETerm :: forall t. !Digest -> !HashId -> !HashId -> !HashId -> Description (Term t) DAddNumTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DNegNumTerm :: forall t. !Digest -> !HashId -> Description (Term t) DMulNumTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DAbsNumTerm :: forall t. !Digest -> !HashId -> Description (Term t) DSignumNumTerm :: forall t. !Digest -> !HashId -> Description (Term t) DLtOrdTerm :: !Digest -> !Fingerprint -> !HashId -> !HashId -> Description (Term Bool) DLeOrdTerm :: !Digest -> !Fingerprint -> !HashId -> !HashId -> Description (Term Bool) DAndBitsTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DOrBitsTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DXorBitsTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DComplementBitsTerm :: forall t. !Digest -> !HashId -> Description (Term t) DShiftLeftTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DShiftRightTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DRotateLeftTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DRotateRightTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DBVConcatTerm :: forall t. !Digest -> !TypeHashId -> !TypeHashId -> Description (Term t) DBitCastTerm :: forall t. !Digest -> !TypeHashId -> Description (Term t) DBitCastOrTerm :: forall t. !Digest -> !HashId -> !TypeHashId -> Description (Term t) DBVSelectTerm :: forall (bv :: Nat -> Type) (w :: Nat). !Digest -> !Fingerprint -> !TypeHashId -> Description (Term (bv w)) DBVExtendTerm :: forall (bv :: Nat -> Type) (r :: Nat). !Digest -> !Bool -> !(Proxy r) -> !TypeHashId -> Description (Term (bv r)) DApplyTerm :: forall t. !Digest -> !TypeHashId -> !TypeHashId -> Description (Term t) DDivIntegralTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DModIntegralTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DQuotIntegralTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DRemIntegralTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DFPTraitTerm :: !Digest -> FPTrait -> !TypeHashId -> Description (Term Bool) DFdivTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DRecipTerm :: forall t. !Digest -> !HashId -> Description (Term t) DFloatingUnaryTerm :: forall t. !Digest -> FloatingUnaryOp -> !HashId -> Description (Term t) DPowerTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DFPUnaryTerm :: forall (fp :: Nat -> Nat -> Type) (eb :: Nat) (sb :: Nat). !Digest -> FPUnaryOp -> !HashId -> Description (Term (fp eb sb)) DFPBinaryTerm :: forall (fp :: Nat -> Nat -> Type) (eb :: Nat) (sb :: Nat). !Digest -> FPBinaryOp -> !HashId -> !HashId -> Description (Term (fp eb sb)) DFPRoundingUnaryTerm :: forall (fp :: Nat -> Nat -> Type) (eb :: Nat) (sb :: Nat). !Digest -> FPRoundingUnaryOp -> !HashId -> !HashId -> Description (Term (fp eb sb)) DFPRoundingBinaryTerm :: forall (fp :: Nat -> Nat -> Type) (eb :: Nat) (sb :: Nat). !Digest -> FPRoundingBinaryOp -> !HashId -> !HashId -> !HashId -> Description (Term (fp eb sb)) DFPFMATerm :: forall (fp :: Nat -> Nat -> Type) (eb :: Nat) (sb :: Nat). !Digest -> !HashId -> !HashId -> !HashId -> !HashId -> Description (Term (fp eb sb)) DFromIntegralTerm :: forall t. !Digest -> !TypeHashId -> Description (Term t) DFromFPOrTerm :: forall t. !Digest -> !HashId -> !HashId -> !TypeHashId -> Description (Term t) DToFPTerm :: forall (eb :: Nat) (sb :: Nat). !Digest -> !HashId -> !TypeHashId -> Description (Term (FP eb sb))
type Uninterned (Term t)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type Uninterned (Term t) = UTerm t

Methods

describe :: Uninterned (Term t) -> Description (Term t) Source #

identify :: CachedInfo -> Uninterned (Term t) -> Term t Source #

threadId :: Term t -> WeakThreadId Source #

descriptionDigest :: Description (Term t) -> Digest Source #

intern :: (Interned t, Typeable t, Hashable (Description t), Eq (Description t)) => Uninterned t -> IO t Source #

Internalize a term.

haveCache :: IO Bool Source #

Check if the current thread has a cache.

threadCacheSize :: WeakThreadId -> IO Int Source #

Get the size of the current thread's cache.

threadCacheLiveSize :: WeakThreadId -> IO Int Source #

Get the live size of the current thread's cache.