Grisette.Unified.Internal.EvalMode

Documentation

class (Typeable mode, UnifiedBool mode, UnifiedPrimitive mode (GetBool mode), Monad (BaseMonad mode), TryMerge (BaseMonad mode), UnifiedBranching mode (BaseMonad mode), AllUnifiedData mode) => EvalModeBase mode

Provide the constraint that the mode is a valid evaluation mode, and provides the support for GetBool and GetData.

For compilers prior to GHC 9.2.1, see the notes for EvalModeAll.

Instances

EvalModeBase 'Con

Defined in Grisette.Unified.Internal.EvalMode

EvalModeBase 'Sym

Defined in Grisette.Unified.Internal.EvalMode

type EvalModeInteger = UnifiedInteger

Provide the support for GetInteger.

For compilers prior to GHC 9.2.1, see the notes for EvalModeAll.

class (AllUnifiedBV mode, AllUnifiedBVBVConversion mode) => EvalModeBV mode

Provide the support for GetIntN, GetWordN, GetSomeIntN, and GetSomeWordN.

For compilers prior to GHC 9.2.1, see the notes for EvalModeAll.

Instances

EvalModeBV 'Con

Defined in Grisette.Unified.Internal.EvalMode

EvalModeBV 'Sym

Defined in Grisette.Unified.Internal.EvalMode

class (AllUnifiedFP mode, AllUnifiedFPFPConversion mode, AllUnifiedBVFPConversion mode) => EvalModeFP mode

Provide the support for GetFP and GetFPRoundingMode.

For compilers prior to GHC 9.2.1, see the notes for EvalModeAll.

Instances

EvalModeFP 'Con

Defined in Grisette.Unified.Internal.EvalMode

EvalModeFP 'Sym

Defined in Grisette.Unified.Internal.EvalMode

type EvalModeAlgReal = UnifiedAlgReal

Provide the support for GetAlgReal.

For compilers prior to GHC 9.2.1, see the notes for EvalModeAll.

class (EvalModeBase mode, EvalModeInteger mode, EvalModeAlgReal mode, EvalModeBV mode, EvalModeFP mode) => EvalModeAll mode

A constraint that specifies that the mode is valid, and provide all the corresponding constraints for the operaions for the types.

Note for users with GHC prior to 9.2.1: the GHC compiler isn't able to resolve the operations for sized bitvectors and data types. In this case, you may need to provide UnifiedBV, SafeUnifiedBV, SafeUnifiedSomeBV, and UnifiedData constraints manually.

For example, the following code is valid for GHC 9.2.1 and later:

fbv ::
  forall mode n.
  (EvalMode mode, KnownNat n, 1 <= n) =>
  GetIntN mode n ->
  GetIntN mode n ->
  GetIntN mode n
fbv l r =
  mrgIte @mode
    (l .== r)
    (l + r)
    (symIte @mode (l .< r) l r)

But with older GHCs, you need to write:

fbv ::
  forall mode n.
  (EvalMode mode, KnownNat n, 1 <= n, UnifiedBV mode n) =>
  GetIntN mode n ->
  GetIntN mode n ->
  GetIntN mode n
fbv l r =
  mrgIte @mode
    (l .== r)
    (l + r)
    (symIte @mode (l .< r) l r)

Instances

EvalModeAll 'Con

Defined in Grisette.Unified.Internal.EvalMode

EvalModeAll 'Sym

Defined in Grisette.Unified.Internal.EvalMode

type MonadEvalModeAll mode m = (EvalModeAll mode, Monad m, TryMerge m, UnifiedBranching mode m)

A constraint that specifies that the mode is valid, and provide all the corresponding constraints for the operations for the types.

This also provide the branching constraints for the monad, and the safe operations: for example, SafeUnifiedInteger provides safeDiv for the integer type with in ExceptT ArithException m.

For users with GHC prior to 9.2.1, see notes in EvalModeAll.

genEvalMode :: String -> [TheoryToUnify] -> DecsQ

This template haskell function generates an EvalMode constraint on demand.

For example, if in your system, you are only working on bit-vectors and booleans, but not floating points, integers, or real numbers, you can use this function to generate a constraint that only includes the necessary constraints:

genEvalMode "MyEvalMode" [UWordN, UIntN, UBool]
f :: MyEvalMode mode => GetBool mode -> GetWordN mode 8 -> GetWordN mode 8
f = ...

This may help with faster compilation times.

Another usage of this custom constraint is to working with uninterpreted functions. The uninterpreted functions aren't available even with EvalModeAll, and is only available with the constraint generated by this function. Note that you need to explicitly list all the uninterpreted function types you need in your system.

genEvalMode "MyEvalModeUF" [UFun [UWordN, UIntN], UFun [UBool, UBool, UWordN]]

This will give us a constraint that allows us to work with booleans and bit-vectors, and also the uninterpreted functions that

• maps an unsigned bit-vector (any bitwidth) to an unsigned integer (any bitwidth), and
• maps two booleans to an unsigned bit-vector (any bitwidth).

You can then use them in your code like this:

f :: MyEvalModeUF mode => GetFun mode (GetWordN mode 8) (GetIntN mode 8) -> GetIntN mode 8
f fun = f # 1

The function will also provide the constraint MonadMyEvalModeUF, which includes the constraints for the monad and the unified branching, similar to MonadEvalModeAll.

For compilers older than GHC 9.2.1, see the notes for EvalModeAll. This function will also generate constraints like MyEvalModeUFFunUWordNUIntN, which can be used to resolve the constraints for older compilers.

The naming conversion is the concatenation of the three parts:

• The base name provided by the user (i.e., MyEvalModeUF),
• Fun,
• The concatenation of all the types in the uninterpreted function (i.e., UWordNUIntN).

The arguments to the type class is as follows:

• The first argument is the mode,
• The second to the end arguments are the natural number arguments for all the types. Here the second argument is the bitwidth of the unsigned bit-vector argument, and the third argument is the bitwidth of the signed bit-vector result.