Copyright	(c) Sirui Lu 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.Unified.UnifiedData

Description

Synopsis

class (UnifiedSimpleMergeable1 mode (GetData mode), UnifiedBranching mode (GetData mode), UnionView (GetData mode), UnionViewMode mode (GetData mode), Monad (GetData mode), TryMerge (GetData mode)) => UnifiedDataBase (mode :: EvalModeTag)
type family GetData (mode :: EvalModeTag) = (r :: Type -> Type) | r -> mode
type BaseMonad (mode :: EvalModeTag) = GetData mode
wrapData :: UnifiedDataImpl mode v u => v -> u
extractData :: (UnifiedDataImpl mode v u, Mergeable v, Monad m, UnifiedBranching mode m) => u -> m v
class UnifiedDataImpl mode v (GetData mode v) => UnifiedData (mode :: EvalModeTag) v
class (forall v. UnifiedData bool v, forall v. Mergeable v => UnifiedDataSimpleMergeable v) => AllUnifiedData (bool :: EvalModeTag)
symCompare :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymOrd mode a) => a -> a -> GetData mode Ordering
liftSymCompare :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSymOrd1 mode f) => (a -> b -> GetData mode Ordering) -> f a -> f b -> GetData mode Ordering
symCompare1 :: forall (mode :: EvalModeTag) f a. (DecideEvalMode mode, UnifiedSymOrd mode a, UnifiedSymOrd1 mode f) => f a -> f a -> GetData mode Ordering
liftSymCompare2 :: forall (mode :: EvalModeTag) f a b c d. (DecideEvalMode mode, UnifiedSymOrd2 mode f) => (a -> b -> GetData mode Ordering) -> (c -> d -> GetData mode Ordering) -> f a c -> f b d -> GetData mode Ordering
symCompare2 :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSymOrd mode a, UnifiedSymOrd mode b, UnifiedSymOrd2 mode f) => f a b -> f a b -> GetData mode Ordering

Documentation

class (UnifiedSimpleMergeable1 mode (GetData mode), UnifiedBranching mode (GetData mode), UnionView (GetData mode), UnionViewMode mode (GetData mode), Monad (GetData mode), TryMerge (GetData mode)) => UnifiedDataBase (mode :: EvalModeTag) Source #

Instances

Instances details

UnifiedDataBase 'C Source #

Instance details

Defined in Grisette.Internal.Unified.UnifiedData

Associated Types

type GetData 'C
Instance details Defined in Grisette.Internal.Unified.UnifiedData type GetData 'C = Identity

UnifiedDataBase 'S Source #

Instance details

Defined in Grisette.Internal.Unified.UnifiedData

Associated Types

type GetData 'S
Instance details Defined in Grisette.Internal.Unified.UnifiedData type GetData 'S = Union

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

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

Instances

Instances details

type GetData 'C Source #
Instance details Defined in Grisette.Internal.Unified.UnifiedData type GetData 'C = Identity
type GetData 'S Source #
Instance details Defined in Grisette.Internal.Unified.UnifiedData type GetData 'S = Union

type BaseMonad (mode :: EvalModeTag) = GetData mode Source #

A type family that specifies the base monad for the evaluation mode.

Resolves to Identity for C mode, and Union for S mode.

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

symCompare :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymOrd mode a) => a -> a -> GetData mode Ordering Source #

Unified symCompare.

liftSymCompare :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSymOrd1 mode f) => (a -> b -> GetData mode Ordering) -> f a -> f b -> GetData mode Ordering Source #

Unified liftSymCompare.

symCompare1 :: forall (mode :: EvalModeTag) f a. (DecideEvalMode mode, UnifiedSymOrd mode a, UnifiedSymOrd1 mode f) => f a -> f a -> GetData mode Ordering Source #

Unified symCompare1.

liftSymCompare2 :: forall (mode :: EvalModeTag) f a b c d. (DecideEvalMode mode, UnifiedSymOrd2 mode f) => (a -> b -> GetData mode Ordering) -> (c -> d -> GetData mode Ordering) -> f a c -> f b d -> GetData mode Ordering Source #

Unified liftSymCompare2.

symCompare2 :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSymOrd mode a, UnifiedSymOrd mode b, UnifiedSymOrd2 mode f) => f a b -> f a b -> GetData mode Ordering Source #

Unified symCompare2.