Grisette.Unified.Internal.EvalMode

Documentation

class (Typeable mode, UnifiedBool mode, UnifiedPrimitive mode (GetBool mode), UnifiedInteger mode, AllUnifiedBV mode, AllUnifiedData mode, Monad (BaseMonad mode), TryMerge (BaseMonad mode), UnifiedBranching mode (BaseMonad mode)) => EvalMode 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

EvalMode 'Con

Defined in Grisette.Unified.Internal.EvalMode

EvalMode 'Sym

Defined in Grisette.Unified.Internal.EvalMode