grisette-0.11.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2024
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellNone
LanguageHaskell2010

Grisette.Internal.Unified.UnifiedData

Description

 
Synopsis

Documentation

type family GetData (mode :: EvalModeTag) v = (r :: Type) | r -> mode v Source #

Get a unified data type. Resolves to v in C mode, and Union v in S mode.

Instances

Instances details
type GetData 'C v Source # 
Instance details

Defined in Grisette.Internal.Unified.UnifiedData

type GetData 'C v = Identity v
type GetData 'S v Source # 
Instance details

Defined in Grisette.Internal.Unified.UnifiedData

type GetData 'S v = Union v

wrapData :: UnifiedDataImpl mode v u => v -> u Source #

Wraps a value into the unified data type.

extractData :: (UnifiedDataImpl mode v u, Mergeable v, Monad m, UnifiedBranching mode m) => u -> m v Source #

Extracts a value from the unified data type.

class UnifiedDataImpl mode v (GetData mode v) => UnifiedData (mode :: EvalModeTag) v Source #

This class is needed as constraint in user code prior to GHC 9.2.1. See the notes in IsMode.

Instances

Instances details
UnifiedDataImpl bool v (GetData bool v) => UnifiedData bool v Source # 
Instance details

Defined in Grisette.Internal.Unified.UnifiedData

class (forall v. UnifiedData bool v, forall v. Mergeable v => UnifiedDataSimpleMergeable v) => AllUnifiedData (bool :: EvalModeTag) Source #

Evaluation mode with unified data types.

Instances

Instances details
(forall v. UnifiedData bool v, forall v. Mergeable v => UnifiedDataSimpleMergeable v) => AllUnifiedData bool Source # 
Instance details

Defined in Grisette.Internal.Unified.UnifiedData