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.TH

Contents

Convenient derivation of all instances relating to Grisette
Smart constructors that merges in a monad
Smart constructors that are polymorphic in evaluation modes

Description

Synopsis

data EvalModeConfig
- = EvalModeConstraints [Name]
- | EvalModeSpecified EvalModeTag
data DeriveConfig = DeriveConfig {
- evalModeConfig :: [(Int, EvalModeConfig)]
- bitSizePositions :: [Int]
- fpBitSizePositions :: [(Int, Int)]
- unconstrainedPositions :: [Int]
- needExtraMergeableUnderEvalMode :: Bool
- needExtraMergeableWithConcretizedEvalMode :: Bool
- useNoStrategy :: Bool
- useSerialForCerealAndBinary :: Bool
}
derive :: [Name] -> [Name] -> Q [Dec]
deriveWith :: DeriveConfig -> [Name] -> [Name] -> Q [Dec]
allClasses0 :: [Name]
allClasses01 :: [Name]
allClasses012 :: [Name]
basicClasses0 :: [Name]
noExistentialClasses0 :: [Name]
concreteOrdClasses0 :: [Name]
basicClasses1 :: [Name]
noExistentialClasses1 :: [Name]
concreteOrdClasses1 :: [Name]
basicClasses2 :: [Name]
noExistentialClasses2 :: [Name]
concreteOrdClasses2 :: [Name]
showClasses :: [Name]
pprintClasses :: [Name]
evalSymClasses :: [Name]
extractSymClasses :: [Name]
substSymClasses :: [Name]
allSymsClasses :: [Name]
eqClasses :: [Name]
ordClasses :: [Name]
symOrdClasses :: [Name]
symEqClasses :: [Name]
unifiedSymOrdClasses :: [Name]
unifiedSymEqClasses :: [Name]
mergeableClasses :: [Name]
nfDataClasses :: [Name]
hashableClasses :: [Name]
toSymClasses :: [Name]
toConClasses :: [Name]
serialClasses :: [Name]
simpleMergeableClasses :: [Name]
unifiedSimpleMergeableClasses :: [Name]
filterExactNumArgs :: Int -> [Name] -> [Name]
filterLeqNumArgs :: Int -> [Name] -> [Name]
makePrefixedSmartCtor :: String -> Name -> Q [Dec]
makeNamedSmartCtor :: [String] -> Name -> Q [Dec]
makeSmartCtor :: Name -> Q [Dec]
makeSmartCtorWith :: (String -> String) -> Name -> Q [Dec]
makePrefixedUnifiedCtor :: [Name] -> String -> Name -> Q [Dec]
makeNamedUnifiedCtor :: [Name] -> [String] -> Name -> Q [Dec]
makeUnifiedCtor :: [Name] -> Name -> Q [Dec]
makeUnifiedCtorWith :: [Name] -> (String -> String) -> Name -> Q [Dec]

Convenient derivation of all instances relating to Grisette

data EvalModeConfig Source #

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 Source #

Configuration for deriving instances for a data type.

Constructors

DeriveConfig
Fields evalModeConfig :: [(Int, EvalModeConfig)] bitSizePositions :: [Int] fpBitSizePositions :: [(Int, Int)] unconstrainedPositions :: [Int] needExtraMergeableUnderEvalMode :: Bool needExtraMergeableWithConcretizedEvalMode :: Bool useNoStrategy :: Bool useSerialForCerealAndBinary :: Bool

Instances

Instances details

Monoid DeriveConfig Source #
Instance details Defined in Grisette.Internal.TH.Derivation.Common Methods mempty :: DeriveConfig # mappend :: DeriveConfig -> DeriveConfig -> DeriveConfig # mconcat :: [DeriveConfig] -> DeriveConfig #
Semigroup DeriveConfig Source #
Instance details Defined in Grisette.Internal.TH.Derivation.Common Methods (<>) :: DeriveConfig -> DeriveConfig -> DeriveConfig # sconcat :: NonEmpty DeriveConfig -> DeriveConfig # stimes :: Integral b => b -> DeriveConfig -> DeriveConfig #

derive :: [Name] -> [Name] -> Q [Dec] Source #

Derive the specified classes for a data type with the given name.

See deriveWith for more details.

deriveWith :: DeriveConfig -> [Name] -> [Name] -> Q [Dec] Source #

Derive the specified classes for a data type with the given name.

Support the following classes for both vanilla data types and GADTs.

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

allClasses0 :: [Name] Source #

All the classes that can be derived for GADTs.

This includes:

allClasses01 :: [Name] Source #

All the classes that can be derived for GADT functors.

This includes all the classes in allClasses0 and allClasses1.

allClasses012 :: [Name] Source #

All the classes that can be derived for GADT functors.

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

basicClasses0 :: [Name] Source #

Basic classes for GADTs.

This includes:

These classes can be derived for most GADTs.

noExistentialClasses0 :: [Name] Source #

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

This includes:

concreteOrdClasses0 :: [Name] Source #

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] Source #

Basic classes for GADT functors.

This includes:

noExistentialClasses1 :: [Name] Source #

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

This includes:

concreteOrdClasses1 :: [Name] Source #

*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] Source #

Basic classes for GADT functors.

This includes:

noExistentialClasses2 :: [Name] Source #

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

This includes:

concreteOrdClasses2 :: [Name] Source #

*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

showClasses :: [Name] Source #

Show classes that can be derived for GADTs.

This includes:

pprintClasses :: [Name] Source #

PPrint classes that can be derived for GADTs.

This includes:

evalSymClasses :: [Name] Source #

EvalSym classes that can be derived for GADTs.

This includes:

extractSymClasses :: [Name] Source #

ExtractSym classes that can be derived for GADTs.

This includes:

substSymClasses :: [Name] Source #

SubstSym classes that can be derived for GADTs.

This includes:

allSymsClasses :: [Name] Source #

AllSyms classes that can be derived for GADTs.

This includes:

eqClasses :: [Name] Source #

Eq classes that can be derived for GADTs.

This includes:

Eq
Eq1
Eq2

ordClasses :: [Name] Source #

Ord classes that can be derived for GADTs.

This includes:

Ord
Ord1
Ord2

symOrdClasses :: [Name] Source #

SymOrd classes that can be derived for GADTs.

This includes:

symEqClasses :: [Name] Source #

SymEq classes that can be derived for GADTs.

This includes:

unifiedSymOrdClasses :: [Name] Source #

UnifiedSymOrd classes that can be derived for GADTs.

This includes:

unifiedSymEqClasses :: [Name] Source #

UnifiedSymEq classes that can be derived for GADTs.

This includes:

mergeableClasses :: [Name] Source #

Mergeable classes that can be derived for GADTs.

This includes:

nfDataClasses :: [Name] Source #

NFData classes that can be derived for GADTs.

This includes:

hashableClasses :: [Name] Source #

Hashable classes that can be derived for GADTs.

This includes:

toSymClasses :: [Name] Source #

ToSym classes that can be derived for GADTs.

This includes:

toConClasses :: [Name] Source #

ToCon classes that can be derived for GADTs.

This includes:

serialClasses :: [Name] Source #

Serial classes that can be derived for GADTs.

This includes:

simpleMergeableClasses :: [Name] Source #

SimpleMergeable classes that can be derived for GADTs.

This includes:

unifiedSimpleMergeableClasses :: [Name] Source #

UnifiedSimpleMergeable classes that can be derived for GADTs.

This includes:

filterExactNumArgs :: Int -> [Name] -> [Name] Source #

Filter classes that accepts type constructors with exactly n arguments.

filterLeqNumArgs :: Int -> [Name] -> [Name] Source #

Filter classes that accepts type constructors with at most n arguments.

Smart constructors that merges in a monad

makePrefixedSmartCtor Source #

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 Source #

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 Source #

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] Source #

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 Source #

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 Source #

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 Source #

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] Source #

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).