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

Description

 
Synopsis

Convenient TH procedures for ADTs

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

Make an ADT compatible with Grisette.

This will generate instances for the ADT with the given classes, and smart constructors for each constructor.

The derivation is done with the given configuration.

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

Make an ADT compatible with Grisette.

This will generate most useful instances for the ADT, and smart constructors for each constructor.

This does not include Ord instances.

See derive, basicClasses0, and makeSmartCtor for more details.

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

Make an ADT compatible with Grisette.

This will generate most useful instances for the ADT, and smart constructors for each constructor.

This does not include Ord instances.

See derive, basicClasses01, and makeSmartCtor for more details.

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

Make an ADT compatible with Grisette.

This will generate most useful instances for the ADT, and smart constructors for each constructor.

This does not include Ord instances.

See derive, basicClasses012, and makeSmartCtor for more details.

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

Make an ADT compatible with Grisette.

This will generate most useful instances for the ADT, and smart constructors for each constructor.

This does not include Ord instances.

The derivation is done with the given configuration.

See deriveWith, basicClasses0, and makeSmartCtor for more details.

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

Make an ADT compatible with Grisette.

This will generate most useful instances for the ADT, and smart constructors for each constructor.

This does not include Ord instances.

The derivation is done with the given configuration.

See deriveWith, basicClasses01, and makeSmartCtor for more details.

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

Make an ADT compatible with Grisette.

This will generate most useful instances for the ADT, and smart constructors for each constructor.

This does not include Ord instances.

The derivation is done with the given configuration.

See deriveWith, basicClasses012, and makeSmartCtor for more details.

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

Make an ADT compatible with Grisette.

This will generate almost all useful instances for the ADT, and smart constructors for each constructor.

This cannot be used for ADTs with existential type variables.

See derive, allClasses0, and makeSmartCtor for more details.

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

Make an ADT compatible with Grisette.

This will generate almost all useful instances for the ADT, and smart constructors for each constructor.

This cannot be used for ADTs with existential type variables.

See derive, allClasses01, and makeSmartCtor for more details.

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

Make an ADT compatible with Grisette.

This will generate almost all useful instances for the ADT, and smart constructors for each constructor.

This cannot be used for ADTs with existential type variables.

See derive, allClasses012, and makeSmartCtor for more details.

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

Make an ADT compatible with Grisette.

This will generate almost all useful instances for the ADT, and smart constructors for each constructor.

This cannot be used for ADTs with existential type variables.

The derivation is done with the given configuration.

See deriveWith, allClasses0, and makeSmartCtor for more details.

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

Make an ADT compatible with Grisette.

This will generate almost all useful instances for the ADT, and smart constructors for each constructor.

This cannot be used for ADTs with existential type variables.

The derivation is done with the given configuration.

See deriveWith, allClasses01, and makeSmartCtor for more details.

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

Make an ADT compatible with Grisette.

This will generate almost all useful instances for the ADT, and smart constructors for each constructor.

This cannot be used for ADTs with existential type variables.

The derivation is done with the given configuration.

See deriveWith, allClasses012, and makeSmartCtor for more details.

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

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.

basicClasses1 :: [Name] Source #

Basic classes for GADT functors.

This includes:

basicClasses2 :: [Name] Source #

Basic classes for GADT functors.

This includes:

basicClasses01 :: [Name] Source #

Basic classes for GADT functors.

This includes all the classes in basicClasses0 and basicClasses1.

basicClasses012 :: [Name] Source #

Basic classes for GADT functors.

This includes all the classes in basicClasses0 and basicClasses1 and basicClasses2.

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 (will fail to derive if the type contains any symbolic variables)
  • UnifiedSymOrd

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:

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:

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:

ordClasses :: [Name] Source #

Ord classes that can be derived for GADTs.

This includes:

  • Ord (will fail to derive if the type contains any symbolic variables)
  • Ord1 (will fail to derive if the type contains any symbolic variables)
  • Ord2 (will fail to derive if the type contains any symbolic variables)

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:

  • Hashable (will fail to derive if the type contains any symbolic variables)
  • Hashable1 (will fail to derive if the type contains any symbolic variables)
  • Hashable2 (will fail to derive if the type contains any symbolic variables)

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