Grisette.TH

Convenient derivation of all instances relating to Grisette

data EvalModeConfig

Configuration for constraints for evaluation modes tag.

• EvalModeConstraints specifies a list of constraints for the tag, for example, we may use EvalModeBase and EvalModeBV to specify that the evaluation mode must support both base (boolean and data types) and bit vectors. This should be used when the data type uses bit vectors.
• EvalModeSpecified specifies a that an evaluation mode tag should be specialized to a specific tag for all the instances.

Constructors

EvalModeConstraints [Name]

EvalModeSpecified EvalModeTag

data DeriveConfig

Configuration for deriving instances for a GADT.

Constructors

DeriveConfig

Fields

• evalModeConfig :: [(Int, EvalModeConfig)]
• bitSizePositions :: [Int]
• fpBitSizePositions :: [(Int, Int)]
• needExtraMergeableUnderEvalMode :: Bool
• needExtraMergeableWithConcretizedEvalMode :: Bool

Instances

Monoid DeriveConfig

Defined in Grisette.Internal.TH.GADT.Common

Methods

mempty :: DeriveConfig

mappend :: DeriveConfig -> DeriveConfig -> DeriveConfig

mconcat :: [DeriveConfig] -> DeriveConfig

Semigroup DeriveConfig

Defined in Grisette.Internal.TH.GADT.Common

Methods

(<>) :: DeriveConfig -> DeriveConfig -> DeriveConfig

sconcat :: NonEmpty DeriveConfig -> DeriveConfig

stimes :: Integral b => b -> DeriveConfig -> DeriveConfig

deriveGADT :: [Name] -> [Name] -> Q [Dec]

Derive the specified classes for a GADT with the given name.

See deriveGADTWith for more details.

deriveGADTWith :: DeriveConfig -> [Name] -> [Name] -> Q [Dec]

Derive the specified classes for a GADT with the given name.

Support the following classes.

• Mergeable
• Mergeable1
• Mergeable2
• Mergeable3
• EvalSym
• EvalSym1
• EvalSym2
• ExtractSym
• ExtractSym1
• ExtractSym2
• SubstSym
• SubstSym1
• SubstSym2
• NFData
• NFData1
• NFData2
• Hashable
• Hashable1
• Hashable2
• Show
• Show1
• Show2
• PPrint
• PPrint1
• PPrint2
• AllSyms
• AllSyms1
• AllSyms2
• Eq
• Eq1
• Eq2
• Ord
• Ord1
• Ord2
• SymOrd
• SymOrd1
• SymOrd2
• SymEq
• SymEq1
• SymEq2
• UnifiedSymEq
• UnifiedSymEq1
• UnifiedSymEq2
• UnifiedSymOrd
• UnifiedSymOrd1
• UnifiedSymOrd2
• ToSym
• ToSym1
• ToSym2
• ToCon
• ToCon1
• ToCon2
• Serial
• Serial1
• Serial2
• SimpleMergeable
• SimpleMergeable1
• SimpleMergeable2

Note that the following type classes cannot be derived for GADTs with existential type variables.

• Eq1
• Eq2
• SymEq1
• SymEq2
• Ord1
• Ord2
• SymOrd1
• SymOrd2

allClasses0 :: [Name]

All the classes that can be derived for GADTs.

This includes:

• Mergeable
• EvalSym
• ExtractSym
• SubstSym
• NFData
• Hashable
• Show
• PPrint
• AllSyms
• Eq
• SymEq
• SymOrd
• UnifiedSymEq
• Ord
• UnifiedSymOrd
• Serial
• ToCon
• ToSym

allClasses01 :: [Name]

All the classes that can be derived for GADT functors.

This includes all the classes in allClasses0 and allClasses1.

allClasses012 :: [Name]

All the classes that can be derived for GADTfunctors.

This includes all the classes in allClasses0, allClasses1, and allClasses2.

basicClasses0 :: [Name]

Basic classes for GADTs.

This includes:

• Mergeable
• EvalSym
• ExtractSym
• SubstSym
• NFData
• Hashable
• Show
• PPrint
• AllSyms
• Eq
• SymEq
• SymOrd
• UnifiedSymEq

These classes can be derived for most GADTs.

noExistentialClasses0 :: [Name]

Classes that can only be derived for GADTs without existential type variables.

This includes:

• Serial
• ToCon
• ToSym

ordClasses0 :: [Name]

Concrete ordered classes that can be derived for GADTs that

• uses unified evaluation mode, or
• does not contain any symbolic variables.

This includes:

• Ord
• UnifiedSymOrd

basicClasses1 :: [Name]

Basic classes for GADT functors.

This includes:

• Mergeable1
• EvalSym1
• ExtractSym1
• SubstSym1
• NFData1
• Hashable1
• Show1
• PPrint1
• AllSyms1
• Eq1
• SymEq1
• SymOrd1
• UnifiedSymEq1

noExistentialClasses1 :: [Name]

*1 classes that can only be derived for GADT functors without existential type variables.

This includes:

• Serial1
• ToCon1
• ToSym1

ordClasses1 :: [Name]

*1 concrete ordered classes that can be derived for GADT functors that

• uses unified evaluation mode, or
• does not contain any symbolic variables.

This includes:

• Ord1
• UnifiedSymOrd1

basicClasses2 :: [Name]

Basic classes for GADT functors.

This includes:

• Mergeable2
• EvalSym2
• ExtractSym2
• SubstSym2
• NFData2
• Hashable2
• Show2
• PPrint2
• AllSyms2
• Eq2
• SymEq2
• SymOrd2
• UnifiedSymEq2

noExistentialClasses2 :: [Name]

*2 classes that can only be derived for GADT functors without existential type variables.

This includes:

• Serial2
• ToCon2
• ToSym2

ordClasses2 :: [Name]

*2 concrete ordered classes that can be derived for GADT functors that

• uses unified evaluation mode, or
• does not contain any symbolic variables.

This includes:

• Ord2
• UnifiedSymOrd2

Smart constructors that merges in a monad

makePrefixedSmartCtor

Arguments

:: String

Prefix for generated wrappers

-> Name

The type to generate the wrappers for

-> Q [Dec]

Generate constructor wrappers that wraps the result in a container with TryMerge.

makePrefixedSmartCtor "mrg" ''Maybe

generates

mrgNothing :: (Mergeable (Maybe a), Applicative m, TryMerge m) => m (Maybe a)
mrgNothing = mrgSingle Nothing
mrgJust :: (Mergeable (Maybe a), Applicative m, TryMerge m) => a -> m (Maybe a)
mrgJust = \x -> mrgSingle (Just x)

makeNamedSmartCtor

Arguments

:: [String]

Names for generated wrappers

-> Name

The type to generate the wrappers for

-> Q [Dec]

Generate constructor wrappers that wraps the result in a container with TryMerge with provided names.

makeNamedSmartCtor ["mrgTuple2"] ''(,)

generates

mrgTuple2 :: (Mergeable (a, b), Applicative m, TryMerge m) => a -> b -> u (a, b)
mrgTuple2 = \v1 v2 -> mrgSingle (v1, v2)

makeSmartCtor

Arguments

:: Name

The type to generate the wrappers for

-> Q [Dec]

Generate constructor wrappers that wraps the result in a container with TryMerge.

makeSmartCtor ''Maybe

generates

nothing :: (Mergeable (Maybe a), Applicative m, TryMerge m) => m (Maybe a)
nothing = mrgSingle Nothing
just :: (Mergeable (Maybe a), Applicative m, TryMerge m) => a -> m (Maybe a)
just = \x -> mrgSingle (Just x)

makeSmartCtorWith :: (String -> String) -> Name -> Q [Dec]

Generate constructor wrappers that wraps the result in a container with TryMerge with provided name transformer.

makeSmartCtorWith (\name -> "mrg" ++ name) ''Maybe

generates

mrgNothing :: (Mergeable (Maybe a), Applicative m, TryMerge m) => m (Maybe a)
mrgNothing = mrgSingle Nothing

Smart constructors that are polymorphic in evaluation modes

makePrefixedUnifiedCtor

Arguments

:: [Name]

-> String

Prefix for generated wrappers

-> Name

The type to generate the wrappers for

-> Q [Dec]

Generate smart constructors to create unified values.

For a type T mode a b c with constructors T1, T2, etc., this function will generate smart constructors with the given prefix, e.g., mkT1, mkT2, etc.

The generated smart constructors will contruct values of type GetData mode (T mode a b c).

makeNamedUnifiedCtor

Arguments

:: [Name]

-> [String]

Names for generated wrappers

-> Name

The type to generate the wrappers for

-> Q [Dec]

Generate smart constructors to create unified values.

For a type T mode a b c with constructors T1, T2, etc., this function will generate smart constructors with the given names.

The generated smart constructors will contruct values of type GetData mode (T mode a b c).

makeUnifiedCtor

Arguments

:: [Name]

-> Name

The type to generate the wrappers for

-> Q [Dec]

Generate smart constructors to create unified values.

For a type T mode a b c with constructors T1, T2, etc., this function will generate smart constructors with the names decapitalized, e.g., t1, t2, etc.

The generated smart constructors will contruct values of type GetData mode (T mode a b c).

makeUnifiedCtorWith :: [Name] -> (String -> String) -> Name -> Q [Dec]

Generate smart constructors to create unified values with provided name transformer.

For a type T mode a b c with constructors T1, T2, etc., this function will generate smart constructors with the name transformed, e.g., given the name transformer (name -> "mk" ++ name), it will generate mkT1, mkT2, mkT2, etc.

The generated smart constructors will contruct values of type GetData mode (T mode a b c).