{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# HLINT ignore "Eta reduce" #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm
  ( pevalDefaultDivIntegralTerm,
    pevalDefaultDivBoundedIntegralTerm,
    pevalDefaultModIntegralTerm,
    pevalDefaultQuotIntegralTerm,
    pevalDefaultQuotBoundedIntegralTerm,
    pevalDefaultRemIntegralTerm,
  )
where

import GHC.TypeNats (KnownNat, type (<=))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim ()
import Grisette.Internal.SymPrim.Prim.Internal.IsZero
  ( IsZeroCases (IsZeroEvidence, NonZeroEvidence),
    KnownIsZero (isZero),
  )
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalDivModIntegralTerm
      ( pevalDivIntegralTerm,
        pevalModIntegralTerm,
        pevalQuotIntegralTerm,
        pevalRemIntegralTerm,
        withSbvDivModIntegralTermConstraint
      ),
    SupportedPrim (withPrim),
    Term (ConTerm),
    conTerm,
    divIntegralTerm,
    modIntegralTerm,
    quotIntegralTerm,
    remIntegralTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold (binaryUnfoldOnce)

-- div
pevalDefaultDivIntegralTerm ::
  (PEvalDivModIntegralTerm a) => Term a -> Term a -> Term a
pevalDefaultDivIntegralTerm :: forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
pevalDefaultDivIntegralTerm =
  PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a a
forall a.
PEvalDivModIntegralTerm a =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultDivIntegralTerm TotalRuleBinary a a a
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
divIntegralTerm

doPevalDefaultDivIntegralTerm ::
  (PEvalDivModIntegralTerm a) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultDivIntegralTerm :: forall a.
PEvalDivModIntegralTerm a =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultDivIntegralTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b)
  | a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0 = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
b
doPevalDefaultDivIntegralTerm Term a
a (ConTerm Id
_ a
1) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
a
doPevalDefaultDivIntegralTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

pevalDefaultDivBoundedIntegralTerm ::
  (PEvalDivModIntegralTerm a, Bounded a) => Term a -> Term a -> Term a
pevalDefaultDivBoundedIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Bounded a) =>
Term a -> Term a -> Term a
pevalDefaultDivBoundedIntegralTerm =
  PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a a
forall a.
(PEvalDivModIntegralTerm a, Bounded a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultDivBoundedIntegralTerm TotalRuleBinary a a a
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
divIntegralTerm

doPevalDefaultDivBoundedIntegralTerm ::
  (PEvalDivModIntegralTerm a, Bounded a) =>
  Term a ->
  Term a ->
  Maybe (Term a)
doPevalDefaultDivBoundedIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Bounded a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultDivBoundedIntegralTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b)
  | a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0 Bool -> Bool -> Bool
&& (a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= -a
1 Bool -> Bool -> Bool
|| a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
forall a. Bounded a => a
minBound) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
b
doPevalDefaultDivBoundedIntegralTerm Term a
a (ConTerm Id
_ a
1) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
a
doPevalDefaultDivBoundedIntegralTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

-- mod
pevalDefaultModIntegralTerm ::
  (PEvalDivModIntegralTerm a) => Term a -> Term a -> Term a
pevalDefaultModIntegralTerm :: forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
pevalDefaultModIntegralTerm =
  PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a a
forall a.
PEvalDivModIntegralTerm a =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultModIntegralTerm TotalRuleBinary a a a
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
modIntegralTerm

doPevalDefaultModIntegralTerm ::
  (PEvalDivModIntegralTerm a) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultModIntegralTerm :: forall a.
PEvalDivModIntegralTerm a =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultModIntegralTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b)
  | a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0 = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> a
forall a. Integral a => a -> a -> a
`mod` a
b
doPevalDefaultModIntegralTerm Term a
_ (ConTerm Id
_ a
1) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
0
doPevalDefaultModIntegralTerm Term a
_ (ConTerm Id
_ (-1)) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
0
doPevalDefaultModIntegralTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

-- quot
pevalDefaultQuotIntegralTerm ::
  (PEvalDivModIntegralTerm a) => Term a -> Term a -> Term a
pevalDefaultQuotIntegralTerm :: forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
pevalDefaultQuotIntegralTerm =
  PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a a
forall a.
PEvalDivModIntegralTerm a =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultQuotIntegralTerm TotalRuleBinary a a a
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
quotIntegralTerm

doPevalDefaultQuotIntegralTerm ::
  (PEvalDivModIntegralTerm a) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultQuotIntegralTerm :: forall a.
PEvalDivModIntegralTerm a =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultQuotIntegralTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b)
  | a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0 = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> a
forall a. Integral a => a -> a -> a
`quot` a
b
doPevalDefaultQuotIntegralTerm Term a
a (ConTerm Id
_ a
1) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
a
doPevalDefaultQuotIntegralTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

pevalDefaultQuotBoundedIntegralTerm ::
  (PEvalDivModIntegralTerm a, Bounded a) => Term a -> Term a -> Term a
pevalDefaultQuotBoundedIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Bounded a) =>
Term a -> Term a -> Term a
pevalDefaultQuotBoundedIntegralTerm =
  PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a a
forall a.
(PEvalDivModIntegralTerm a, Bounded a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultQuotBoundedIntegralTerm TotalRuleBinary a a a
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
quotIntegralTerm

doPevalDefaultQuotBoundedIntegralTerm ::
  (PEvalDivModIntegralTerm a, Bounded a) =>
  Term a ->
  Term a ->
  Maybe (Term a)
doPevalDefaultQuotBoundedIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Bounded a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultQuotBoundedIntegralTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b)
  | a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0 Bool -> Bool -> Bool
&& (a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= -a
1 Bool -> Bool -> Bool
|| a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
forall a. Bounded a => a
minBound) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> a
forall a. Integral a => a -> a -> a
`quot` a
b
doPevalDefaultQuotBoundedIntegralTerm Term a
a (ConTerm Id
_ a
1) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
a
doPevalDefaultQuotBoundedIntegralTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

-- rem
pevalDefaultRemIntegralTerm ::
  (PEvalDivModIntegralTerm a) => Term a -> Term a -> Term a
pevalDefaultRemIntegralTerm :: forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
pevalDefaultRemIntegralTerm =
  PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a a
forall a.
PEvalDivModIntegralTerm a =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultRemIntegralTerm TotalRuleBinary a a a
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
remIntegralTerm

doPevalDefaultRemIntegralTerm ::
  (PEvalDivModIntegralTerm a) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultRemIntegralTerm :: forall a.
PEvalDivModIntegralTerm a =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultRemIntegralTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b)
  | a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0 = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> a
forall a. Integral a => a -> a -> a
`rem` a
b
doPevalDefaultRemIntegralTerm Term a
_ (ConTerm Id
_ a
1) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
0
doPevalDefaultRemIntegralTerm Term a
_ (ConTerm Id
_ (-1)) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
0
doPevalDefaultRemIntegralTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

instance PEvalDivModIntegralTerm Integer where
  pevalDivIntegralTerm :: Term Integer -> Term Integer -> Term Integer
pevalDivIntegralTerm = Term Integer -> Term Integer -> Term Integer
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
pevalDefaultDivIntegralTerm
  pevalModIntegralTerm :: Term Integer -> Term Integer -> Term Integer
pevalModIntegralTerm = Term Integer -> Term Integer -> Term Integer
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
pevalDefaultModIntegralTerm
  pevalQuotIntegralTerm :: Term Integer -> Term Integer -> Term Integer
pevalQuotIntegralTerm = Term Integer -> Term Integer -> Term Integer
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
pevalDefaultQuotIntegralTerm
  pevalRemIntegralTerm :: Term Integer -> Term Integer -> Term Integer
pevalRemIntegralTerm = Term Integer -> Term Integer -> Term Integer
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
pevalDefaultRemIntegralTerm
  withSbvDivModIntegralTermConstraint :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (SDivisible (SBVType n Integer) => r) -> r
withSbvDivModIntegralTermConstraint proxy n
p SDivisible (SBVType n Integer) => r
r = case proxy n -> IsZeroCases n
forall (a :: Nat) (proxy :: Nat -> *).
KnownIsZero a =>
proxy a -> IsZeroCases a
forall (proxy :: Nat -> *). proxy n -> IsZeroCases n
isZero proxy n
p of
    IsZeroCases n
IsZeroEvidence -> r
SDivisible (SBVType n Integer) => r
r
    IsZeroCases n
NonZeroEvidence -> r
SDivisible (SBVType n Integer) => r
r

instance (KnownNat n, 1 <= n) => PEvalDivModIntegralTerm (IntN n) where
  pevalDivIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalDivIntegralTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(PEvalDivModIntegralTerm a, Bounded a) =>
Term a -> Term a -> Term a
pevalDefaultDivBoundedIntegralTerm
  pevalModIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalModIntegralTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
pevalDefaultModIntegralTerm
  pevalQuotIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalQuotIntegralTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(PEvalDivModIntegralTerm a, Bounded a) =>
Term a -> Term a -> Term a
pevalDefaultQuotBoundedIntegralTerm
  pevalRemIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalRemIntegralTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
pevalDefaultRemIntegralTerm
  withSbvDivModIntegralTermConstraint :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (SDivisible (SBVType n (IntN n)) => r) -> r
withSbvDivModIntegralTermConstraint proxy n
p SDivisible (SBVType n (IntN n)) => r
r = forall t (n :: Nat) (p :: Nat -> *) a.
(SupportedPrim t, KnownIsZero n) =>
p n
-> ((PrimConstraint n t, SMTDefinable (SBVType n t),
     Mergeable (SBVType n t), Typeable (SBVType n t)) =>
    a)
-> a
withPrim @(IntN n) proxy n
p r
SDivisible (SBVType n (IntN n)) => r
(PrimConstraint n (IntN n), SMTDefinable (SBVType n (IntN n)),
 Mergeable (SBVType n (IntN n)), Typeable (SBVType n (IntN n))) =>
r
r

instance (KnownNat n, 1 <= n) => PEvalDivModIntegralTerm (WordN n) where
  pevalDivIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalDivIntegralTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
pevalDefaultDivIntegralTerm
  pevalModIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalModIntegralTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
pevalDefaultModIntegralTerm
  pevalQuotIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalQuotIntegralTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
pevalDefaultQuotIntegralTerm
  pevalRemIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalRemIntegralTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
pevalDefaultRemIntegralTerm
  withSbvDivModIntegralTermConstraint :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (SDivisible (SBVType n (WordN n)) => r) -> r
withSbvDivModIntegralTermConstraint proxy n
p SDivisible (SBVType n (WordN n)) => r
r = forall t (n :: Nat) (p :: Nat -> *) a.
(SupportedPrim t, KnownIsZero n) =>
p n
-> ((PrimConstraint n t, SMTDefinable (SBVType n t),
     Mergeable (SBVType n t), Typeable (SBVType n t)) =>
    a)
-> a
withPrim @(WordN n) proxy n
p r
SDivisible (SBVType n (WordN n)) => r
(PrimConstraint n (WordN n), SMTDefinable (SBVType n (WordN n)),
 Mergeable (SBVType n (WordN n)), Typeable (SBVType n (WordN n))) =>
r
r