content: {-# LANGUAGE AllowAmbiguousTypes #-}
  {-# LANGUAGE BinaryLiterals #-}
  {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE FunctionalDependencies #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE QuantifiedConstraints #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  module Grisette.Backend.TermRewritingGen
    ( TermRewritingSpec (..),
      GeneralSpec (..),
      DifferentSizeBVSpec (..),
      FixedSizedBVWithBoolSpec (..),
      BoolWithFixedSizedBVSpec (..),
      BoolWithLIASpec (..),
      LIAWithBoolSpec (..),
      BoolWithNRASpec (..),
      NRAWithBoolSpec (..),
      BoolOnlySpec (..),
      constructUnarySpec,
      constructBinarySpec,
      constructTernarySpec,
      divIntegralSpec,
      modIntegralSpec,
      quotIntegralSpec,
      remIntegralSpec,
      negNumSpec,
      mulNumSpec,
      addNumSpec,
      absNumSpec,
      signumNumSpec,
      ltOrdSpec,
      leOrdSpec,
      iteSpec,
      eqvSpec,
      distinctSpec,
      notSpec,
      andSpec,
      orSpec,
      shiftLeftSpec,
      shiftRightSpec,
      rotateLeftSpec,
      rotateRightSpec,
      fpTraitSpec,
      fdivSpec,
      recipSpec,
      floatingUnarySpec,
      powerSpec,
      fpUnaryOpSpec,
      fpBinaryOpSpec,
      fpRoundingUnaryOpSpec,
      fpRoundingBinarySpec,
      fpFMASpec,
      bitCastSpec,
      bitCastOrSpec,
      fromFPOrSpec,
      toFPSpec,
      bvconcatSpec,
      bvselectSpec,
      bvextendSpec,
      andBitsSpec,
      orBitsSpec,
      xorBitsSpec,
      complementBitsSpec,
      IEEEFPSpec (..),
      IEEEFPBoolOpSpec (..),
      FPRoundingModeSpec (..),
      FPRoundingModeBoolOpSpec (..),
    )
  where
  
  import Data.Bits (FiniteBits)
  import Data.Data (Proxy (Proxy), Typeable)
  import Data.Functor ((<&>))
  import Data.Kind (Type)
  import Data.List.NonEmpty (NonEmpty ((:|)))
  import qualified Data.Text as T
  import GHC.TypeLits (KnownNat, Nat, type (+), type (<=))
  import Grisette
    ( Identifier,
      SExpr (Atom),
      SizedBV,
      SymRotate,
      SymShift,
      withMetadata,
    )
  import Grisette.Internal.SymPrim.AlgReal (AlgReal)
  import Grisette.Internal.SymPrim.FP
    ( FP,
      FPRoundingMode (RNA, RNE, RTN, RTP, RTZ),
      ValidFP,
    )
  import Grisette.Internal.SymPrim.Prim.Internal.Term
    ( FPBinaryOp (FPMaximum, FPMaximumNumber, FPMinimum, FPMinimumNumber, FPRem),
      FPRoundingBinaryOp (FPAdd, FPDiv, FPMul, FPSub),
      FPRoundingUnaryOp (FPRoundToIntegral, FPSqrt),
      FPUnaryOp (FPAbs, FPNeg),
      FloatingUnaryOp (FloatingSqrt),
      PEvalBitCastOrTerm (pevalBitCastOrTerm),
      PEvalBitCastTerm (pevalBitCastTerm),
      PEvalFloatingTerm (pevalFloatingUnaryTerm, pevalPowerTerm),
      PEvalFractionalTerm (pevalRecipTerm),
      PEvalIEEEFPConvertibleTerm (pevalFromFPOrTerm, pevalToFPTerm),
      SupportedPrim (pevalDistinctTerm),
      bitCastOrTerm,
      bitCastTerm,
      fdivTerm,
      floatingUnaryTerm,
      fpBinaryTerm,
      fpFMATerm,
      fpRoundingBinaryTerm,
      fpRoundingUnaryTerm,
      fpUnaryTerm,
      fromFPOrTerm,
      powerTerm,
      toFPTerm,
    )
  import Grisette.Internal.SymPrim.Prim.Term
    ( FPTrait
        ( FPIsInfinite,
          FPIsNaN,
          FPIsNegative,
          FPIsNegativeInfinite,
          FPIsNegativeZero,
          FPIsNormal,
          FPIsPoint,
          FPIsPositive,
          FPIsPositiveInfinite,
          FPIsPositiveZero,
          FPIsSubnormal,
          FPIsZero
        ),
      PEvalBVTerm
        ( pevalBVConcatTerm,
          pevalBVExtendTerm,
          pevalBVSelectTerm
        ),
      PEvalBitwiseTerm
        ( pevalAndBitsTerm,
          pevalComplementBitsTerm,
          pevalOrBitsTerm,
          pevalXorBitsTerm
        ),
      PEvalDivModIntegralTerm
        ( pevalDivIntegralTerm,
          pevalModIntegralTerm,
          pevalQuotIntegralTerm,
          pevalRemIntegralTerm
        ),
      PEvalFractionalTerm (pevalFdivTerm),
      PEvalNumTerm
        ( pevalAbsNumTerm,
          pevalAddNumTerm,
          pevalMulNumTerm,
          pevalNegNumTerm,
          pevalSignumNumTerm
        ),
      PEvalOrdTerm (pevalLeOrdTerm, pevalLtOrdTerm),
      PEvalRotateTerm
        ( pevalRotateLeftTerm,
          pevalRotateRightTerm
        ),
      PEvalShiftTerm
        ( pevalShiftLeftTerm,
          pevalShiftRightTerm
        ),
      SupportedNonFuncPrim,
      SupportedPrim (pevalITETerm),
      Term,
      absNumTerm,
      addNumTerm,
      andBitsTerm,
      andTerm,
      bvConcatTerm,
      bvExtendTerm,
      bvSelectTerm,
      complementBitsTerm,
      conTerm,
      distinctTerm,
      divIntegralTerm,
      eqTerm,
      fpTraitTerm,
      iteTerm,
      leOrdTerm,
      ltOrdTerm,
      modIntegralTerm,
      mulNumTerm,
      negNumTerm,
      notTerm,
      orBitsTerm,
      orTerm,
      pevalAndTerm,
      pevalEqTerm,
      pevalFPBinaryTerm,
      pevalFPFMATerm,
      pevalFPRoundingBinaryTerm,
      pevalFPRoundingUnaryTerm,
      pevalFPTraitTerm,
      pevalFPUnaryTerm,
      pevalNotTerm,
      pevalOrTerm,
      pformatTerm,
      quotIntegralTerm,
      recipTerm,
      remIntegralTerm,
      rotateLeftTerm,
      rotateRightTerm,
      shiftLeftTerm,
      shiftRightTerm,
      signumNumTerm,
      ssymTerm,
      xorBitsTerm,
    )
  import Test.QuickCheck (Arbitrary (arbitrary), Gen, elements, frequency, oneof, sized)
  
  -- import Grisette.Internal.SymPrim.FP (FPRoundingMode(RNE))
  
  class (SupportedNonFuncPrim b) => TermRewritingSpec a b | a -> b where
    norewriteVer :: a -> Term b
    rewriteVer :: a -> Term b
    wrap :: Term b -> Term b -> a
    same :: a -> Term Bool
    counterExample :: a -> Term Bool
    counterExample = notTerm . same
    symSpec :: Identifier -> a
    symSpec s = wrap (ssymTerm s) (ssymTerm s)
    conSpec :: b -> a
    conSpec v = wrap (conTerm v) (conTerm v)
  
  constructUnarySpec ::
    forall a av b bv.
    ( TermRewritingSpec a av,
      TermRewritingSpec b bv
    ) =>
    (Term av -> Term bv) ->
    (Term av -> Term bv) ->
    a ->
    b
  constructUnarySpec construct partial a =
    wrap (construct $ norewriteVer a) (partial $ rewriteVer a)
  
  constructBinarySpec ::
    forall a av b bv c cv.
    ( TermRewritingSpec a av,
      TermRewritingSpec b bv,
      TermRewritingSpec c cv
    ) =>
    (Term av -> Term bv -> Term cv) ->
    (Term av -> Term bv -> Term cv) ->
    a ->
    b ->
    c
  constructBinarySpec construct partial a b =
    wrap
      (construct (norewriteVer a) (norewriteVer b))
      (partial (rewriteVer a) (rewriteVer b))
  
  constructTernarySpec ::
    forall a av b bv c cv d dv.
    ( TermRewritingSpec a av,
      TermRewritingSpec b bv,
      TermRewritingSpec c cv,
      TermRewritingSpec d dv
    ) =>
    (Term av -> Term bv -> Term cv -> Term dv) ->
    (Term av -> Term bv -> Term cv -> Term dv) ->
    a ->
    b ->
    c ->
    d
  constructTernarySpec construct partial a b c =
    wrap
      (construct (norewriteVer a) (norewriteVer b) (norewriteVer c))
      (partial (rewriteVer a) (rewriteVer b) (rewriteVer c))
  
  notSpec :: (TermRewritingSpec a Bool) => a -> a
  notSpec = constructUnarySpec notTerm pevalNotTerm
  
  andSpec :: (TermRewritingSpec a Bool) => a -> a -> a
  andSpec = constructBinarySpec andTerm pevalAndTerm
  
  orSpec :: (TermRewritingSpec a Bool) => a -> a -> a
  orSpec = constructBinarySpec orTerm pevalOrTerm
  
  eqvSpec :: (TermRewritingSpec a av, TermRewritingSpec b Bool) => a -> a -> b
  eqvSpec = constructBinarySpec eqTerm pevalEqTerm
  
  distinctSpec ::
    (TermRewritingSpec a av, TermRewritingSpec b Bool) => NonEmpty a -> b
  distinctSpec l =
    wrap
      (distinctTerm (norewriteVer <$> l))
      (pevalDistinctTerm (rewriteVer <$> l))
  
  iteSpec :: (TermRewritingSpec a Bool, TermRewritingSpec b bv) => a -> b -> b -> b
  iteSpec = constructTernarySpec iteTerm pevalITETerm
  
  addNumSpec :: (TermRewritingSpec a av, PEvalNumTerm av) => a -> a -> a
  addNumSpec = constructBinarySpec addNumTerm pevalAddNumTerm
  
  negNumSpec :: (TermRewritingSpec a av, PEvalNumTerm av) => a -> a
  negNumSpec = constructUnarySpec negNumTerm pevalNegNumTerm
  
  mulNumSpec :: (TermRewritingSpec a av, PEvalNumTerm av) => a -> a -> a
  mulNumSpec = constructBinarySpec mulNumTerm pevalMulNumTerm
  
  absNumSpec :: (TermRewritingSpec a av, PEvalNumTerm av) => a -> a
  absNumSpec = constructUnarySpec absNumTerm pevalAbsNumTerm
  
  signumNumSpec :: (TermRewritingSpec a av, PEvalNumTerm av) => a -> a
  signumNumSpec = constructUnarySpec signumNumTerm pevalSignumNumTerm
  
  bitCastSpec ::
    ( TermRewritingSpec a av,
      TermRewritingSpec b bv,
      PEvalBitCastTerm av bv
    ) =>
    a ->
    b
  bitCastSpec = constructUnarySpec bitCastTerm pevalBitCastTerm
  
  bitCastOrSpec ::
    ( TermRewritingSpec a av,
      TermRewritingSpec b bv,
      PEvalBitCastOrTerm av bv
    ) =>
    b ->
    a ->
    b
  bitCastOrSpec = constructBinarySpec bitCastOrTerm pevalBitCastOrTerm
  
  ltOrdSpec ::
    (TermRewritingSpec a av, PEvalOrdTerm av, TermRewritingSpec b Bool) =>
    a ->
    a ->
    b
  ltOrdSpec = constructBinarySpec ltOrdTerm pevalLtOrdTerm
  
  leOrdSpec ::
    (TermRewritingSpec a av, PEvalOrdTerm av, TermRewritingSpec b Bool) =>
    a ->
    a ->
    b
  leOrdSpec = constructBinarySpec leOrdTerm pevalLeOrdTerm
  
  andBitsSpec :: (TermRewritingSpec a av, PEvalBitwiseTerm av) => a -> a -> a
  andBitsSpec = constructBinarySpec andBitsTerm pevalAndBitsTerm
  
  orBitsSpec :: (TermRewritingSpec a av, PEvalBitwiseTerm av) => a -> a -> a
  orBitsSpec = constructBinarySpec orBitsTerm pevalOrBitsTerm
  
  xorBitsSpec :: (TermRewritingSpec a av, PEvalBitwiseTerm av) => a -> a -> a
  xorBitsSpec = constructBinarySpec xorBitsTerm pevalXorBitsTerm
  
  complementBitsSpec :: (TermRewritingSpec a av, PEvalBitwiseTerm av) => a -> a
  complementBitsSpec = constructUnarySpec complementBitsTerm pevalComplementBitsTerm
  
  shiftLeftSpec :: (TermRewritingSpec a av, PEvalShiftTerm av) => a -> a -> a
  shiftLeftSpec = constructBinarySpec shiftLeftTerm pevalShiftLeftTerm
  
  shiftRightSpec :: (TermRewritingSpec a av, PEvalShiftTerm av) => a -> a -> a
  shiftRightSpec = constructBinarySpec shiftRightTerm pevalShiftRightTerm
  
  rotateLeftSpec :: (TermRewritingSpec a av, PEvalRotateTerm av) => a -> a -> a
  rotateLeftSpec = constructBinarySpec rotateLeftTerm pevalRotateLeftTerm
  
  rotateRightSpec :: (TermRewritingSpec a av, PEvalRotateTerm av) => a -> a -> a
  rotateRightSpec = constructBinarySpec rotateRightTerm pevalRotateRightTerm
  
  bvconcatSpec ::
    ( TermRewritingSpec a (bv an),
      TermRewritingSpec b (bv bn),
      TermRewritingSpec c (bv (an + bn)),
      PEvalBVTerm bv,
      KnownNat an,
      KnownNat bn,
      KnownNat (an + bn),
      1 <= an,
      1 <= bn,
      1 <= an + bn
    ) =>
    a ->
    b ->
    c
  bvconcatSpec = constructBinarySpec bvConcatTerm pevalBVConcatTerm
  
  bvselectSpec ::
    ( TermRewritingSpec a (bv an),
      TermRewritingSpec b (bv bn),
      PEvalBVTerm bv,
      KnownNat an,
      KnownNat ix,
      KnownNat bn,
      1 <= an,
      1 <= bn,
      ix + bn <= an
    ) =>
    proxy ix ->
    proxy bn ->
    a ->
    b
  bvselectSpec p1 p2 = constructUnarySpec (bvSelectTerm p1 p2) (pevalBVSelectTerm p1 p2)
  
  bvextendSpec ::
    ( TermRewritingSpec a (bv an),
      TermRewritingSpec b (bv bn),
      PEvalBVTerm bv,
      KnownNat an,
      KnownNat bn,
      1 <= an,
      1 <= bn,
      an <= bn
    ) =>
    Bool ->
    proxy bn ->
    a ->
    b
  bvextendSpec signed p = constructUnarySpec (bvExtendTerm signed p) (pevalBVExtendTerm signed p)
  
  divIntegralSpec :: (TermRewritingSpec a b, PEvalDivModIntegralTerm b) => a -> a -> a
  divIntegralSpec = constructBinarySpec divIntegralTerm pevalDivIntegralTerm
  
  modIntegralSpec :: (TermRewritingSpec a b, PEvalDivModIntegralTerm b) => a -> a -> a
  modIntegralSpec = constructBinarySpec modIntegralTerm pevalModIntegralTerm
  
  quotIntegralSpec :: (TermRewritingSpec a b, PEvalDivModIntegralTerm b) => a -> a -> a
  quotIntegralSpec = constructBinarySpec quotIntegralTerm pevalQuotIntegralTerm
  
  remIntegralSpec :: (TermRewritingSpec a b, PEvalDivModIntegralTerm b) => a -> a -> a
  remIntegralSpec = constructBinarySpec remIntegralTerm pevalRemIntegralTerm
  
  fpTraitSpec ::
    ( ValidFP eb fb,
      TermRewritingSpec a (FP eb fb),
      TermRewritingSpec b Bool
    ) =>
    FPTrait ->
    a ->
    b
  fpTraitSpec trait = constructUnarySpec (fpTraitTerm trait) (pevalFPTraitTerm trait)
  
  fdivSpec :: (TermRewritingSpec a av, PEvalFractionalTerm av) => a -> a -> a
  fdivSpec = constructBinarySpec fdivTerm pevalFdivTerm
  
  recipSpec :: (TermRewritingSpec a av, PEvalFractionalTerm av) => a -> a
  recipSpec = constructUnarySpec recipTerm pevalRecipTerm
  
  floatingUnarySpec ::
    (TermRewritingSpec a av, PEvalFloatingTerm av) => FloatingUnaryOp -> a -> a
  floatingUnarySpec op =
    constructUnarySpec
      (floatingUnaryTerm op)
      (pevalFloatingUnaryTerm op)
  
  powerSpec ::
    (TermRewritingSpec a av, PEvalFloatingTerm av) => a -> a -> a
  powerSpec = constructBinarySpec powerTerm pevalPowerTerm
  
  fpUnaryOpSpec ::
    ( ValidFP eb fb,
      TermRewritingSpec a (FP eb fb)
    ) =>
    FPUnaryOp ->
    a ->
    a
  fpUnaryOpSpec op = constructUnarySpec (fpUnaryTerm op) (pevalFPUnaryTerm op)
  
  fpBinaryOpSpec ::
    ( ValidFP eb fb,
      TermRewritingSpec a (FP eb fb)
    ) =>
    FPBinaryOp ->
    a ->
    a ->
    a
  fpBinaryOpSpec op = constructBinarySpec (fpBinaryTerm op) (pevalFPBinaryTerm op)
  
  fpRoundingUnaryOpSpec ::
    ( ValidFP eb fb,
      TermRewritingSpec a (FP eb fb),
      TermRewritingSpec r FPRoundingMode
    ) =>
    FPRoundingUnaryOp ->
    r ->
    a ->
    a
  fpRoundingUnaryOpSpec op =
    constructBinarySpec (fpRoundingUnaryTerm op) (pevalFPRoundingUnaryTerm op)
  
  fpRoundingBinarySpec ::
    ( ValidFP eb fb,
      TermRewritingSpec a (FP eb fb),
      TermRewritingSpec r FPRoundingMode
    ) =>
    FPRoundingBinaryOp ->
    r ->
    a ->
    a ->
    a
  fpRoundingBinarySpec op =
    constructTernarySpec (fpRoundingBinaryTerm op) (pevalFPRoundingBinaryTerm op)
  
  fpFMASpec ::
    ( ValidFP eb fb,
      TermRewritingSpec a (FP eb fb),
      TermRewritingSpec r FPRoundingMode
    ) =>
    r ->
    a ->
    a ->
    a ->
    a
  fpFMASpec a b c d =
    wrap
      (fpFMATerm (norewriteVer a) (norewriteVer b) (norewriteVer c) (norewriteVer d))
      (pevalFPFMATerm (rewriteVer a) (rewriteVer b) (rewriteVer c) (norewriteVer d))
  
  fromFPOrSpec ::
    ( ValidFP eb fb,
      TermRewritingSpec a (FP eb fb),
      TermRewritingSpec rd FPRoundingMode,
      TermRewritingSpec b i,
      PEvalIEEEFPConvertibleTerm i
    ) =>
    b ->
    rd ->
    a ->
    b
  fromFPOrSpec = constructTernarySpec fromFPOrTerm pevalFromFPOrTerm
  
  toFPSpec ::
    ( ValidFP eb fb,
      TermRewritingSpec a (FP eb fb),
      TermRewritingSpec rd FPRoundingMode,
      TermRewritingSpec b i,
      PEvalIEEEFPConvertibleTerm i
    ) =>
    rd ->
    b ->
    a
  toFPSpec = constructBinarySpec toFPTerm pevalToFPTerm
  
  data BoolOnlySpec = BoolOnlySpec (Term Bool) (Term Bool)
  
  instance Show BoolOnlySpec where
    show (BoolOnlySpec n r) = "BoolOnlySpec { no: " ++ pformatTerm n ++ ", re: " ++ pformatTerm r ++ " }"
  
  instance TermRewritingSpec BoolOnlySpec Bool where
    norewriteVer (BoolOnlySpec n _) = n
    rewriteVer (BoolOnlySpec _ r) = r
    wrap = BoolOnlySpec
    same s = eqTerm (norewriteVer s) (rewriteVer s)
  
  boolonly :: Int -> Gen BoolOnlySpec
  boolonly 0 =
    let s =
          oneof $
            return . symSpec . (`withMetadata` (Atom ("bool" :: T.Text)))
              <$> ["a", "b", "c", "d", "e", "f", "g"]
        r = oneof $ return . conSpec <$> [True, False]
     in oneof [r, s]
  boolonly n | n > 0 = do
    v1 <- boolonly (n - 1)
    v2 <- boolonly (n - 1)
    v3 <- boolonly (n - 1)
    oneof
      [ return $ notSpec v1,
        return $ andSpec v1 v2,
        return $ orSpec v1 v2,
        return $ eqvSpec v1 v2,
        return $ distinctSpec $ v1 :| [],
        return $ distinctSpec $ v1 :| [v2],
        return $ distinctSpec $ v1 :| [v2, v3],
        return $ iteSpec v1 v2 v3
      ]
  boolonly _ = error "Should never be called"
  
  instance Arbitrary BoolOnlySpec where
    arbitrary = sized boolonly
  
  data BoolWithLIASpec = BoolWithLIASpec (Term Bool) (Term Bool)
  
  instance Show BoolWithLIASpec where
    show (BoolWithLIASpec n r) = "BoolWithLIASpec { no: " ++ pformatTerm n ++ ", re: " ++ pformatTerm r ++ " }"
  
  instance TermRewritingSpec BoolWithLIASpec Bool where
    norewriteVer (BoolWithLIASpec n _) = n
    rewriteVer (BoolWithLIASpec _ r) = r
    wrap = BoolWithLIASpec
    same s = eqTerm (norewriteVer s) (rewriteVer s)
  
  data LIAWithBoolSpec = LIAWithBoolSpec (Term Integer) (Term Integer)
  
  instance Show LIAWithBoolSpec where
    show (LIAWithBoolSpec n r) =
      "LIAWithBoolSpec { no: " ++ pformatTerm n ++ ", re: " ++ pformatTerm r ++ " }"
  
  instance TermRewritingSpec LIAWithBoolSpec Integer where
    norewriteVer (LIAWithBoolSpec n _) = n
    rewriteVer (LIAWithBoolSpec _ r) = r
    wrap = LIAWithBoolSpec
    same s = eqTerm (norewriteVer s) (rewriteVer s)
  
  boolWithLIA :: Int -> Gen BoolWithLIASpec
  boolWithLIA 0 =
    let s =
          oneof $
            return . symSpec . (`withMetadata` (Atom ("bool" :: T.Text)))
              <$> ["a", "b", "c", "d", "e", "f", "g"]
        r = oneof $ return . conSpec <$> [True, False]
     in oneof [r, s]
  boolWithLIA n | n > 0 = do
    v1 <- boolWithLIA (n - 1)
    v2 <- boolWithLIA (n - 1)
    v3 <- boolWithLIA (n - 1)
    v1i <- liaWithBool (n - 1)
    v2i <- liaWithBool (n - 1)
    v3i <- liaWithBool (n - 1)
    frequency
      [ (1, return $ notSpec v1),
        (1, return $ andSpec v1 v2),
        (1, return $ orSpec v1 v2),
        (1, return $ eqvSpec v1 v2),
        (4, return $ eqvSpec v1i v2i),
        (1, return $ distinctSpec $ v1 :| []),
        (1, return $ distinctSpec $ v1 :| [v2]),
        (1, return $ distinctSpec $ v1 :| [v2, v3]),
        (2, return $ distinctSpec $ v1i :| []),
        (2, return $ distinctSpec $ v1i :| [v2i]),
        (2, return $ distinctSpec $ v1i :| [v2i, v3i]),
        (5, return $ ltOrdSpec v1i v2i),
        (5, return $ leOrdSpec v1i v2i),
        (1, return $ iteSpec v1 v2 v3)
      ]
  boolWithLIA _ = error "Should never be called"
  
  liaWithBool :: Int -> Gen LIAWithBoolSpec
  liaWithBool 0 =
    let s =
          oneof $
            return . symSpec . (`withMetadata` (Atom ("int" :: T.Text)))
              <$> ["a", "b", "c", "d", "e", "f", "g"]
        r = conSpec <$> arbitrary
     in oneof [r, s]
  liaWithBool n | n > 0 = do
    v1b <- boolWithLIA (n - 1)
    v1i <- liaWithBool (n - 1)
    v2i <- liaWithBool (n - 1)
    oneof
      [ return $ negNumSpec v1i,
        return $ absNumSpec v1i,
        return $ signumNumSpec v1i,
        return $ addNumSpec v1i v2i,
        return $ iteSpec v1b v1i v2i
      ]
  liaWithBool _ = error "Should never be called"
  
  instance Arbitrary BoolWithLIASpec where
    arbitrary = sized boolWithLIA
  
  instance Arbitrary LIAWithBoolSpec where
    arbitrary = sized liaWithBool
  
  data FixedSizedBVWithBoolSpec (bv :: Nat -> Type) (n :: Nat) = FixedSizedBVWithBoolSpec (Term (bv n)) (Term (bv n))
  
  instance (SupportedNonFuncPrim (bv n)) => Show (FixedSizedBVWithBoolSpec bv n) where
    show (FixedSizedBVWithBoolSpec n r) = "FixedSizedBVWithBoolSpec { no: " ++ pformatTerm n ++ ", re: " ++ pformatTerm r ++ " }"
  
  instance (SupportedNonFuncPrim (bv n)) => TermRewritingSpec (FixedSizedBVWithBoolSpec bv n) (bv n) where
    norewriteVer (FixedSizedBVWithBoolSpec n _) = n
    rewriteVer (FixedSizedBVWithBoolSpec _ r) = r
    wrap = FixedSizedBVWithBoolSpec
    same s = eqTerm (norewriteVer s) (rewriteVer s)
  
  data BoolWithFixedSizedBVSpec (bv :: Nat -> Type) (n :: Nat) = BoolWithFixedSizedBVSpec (Term Bool) (Term Bool)
  
  instance Show (BoolWithFixedSizedBVSpec bv n) where
    show (BoolWithFixedSizedBVSpec n r) =
      "BoolWithFixedSizedBVSpec { no: " ++ pformatTerm n ++ ", re: " ++ pformatTerm r ++ " }"
  
  instance TermRewritingSpec (BoolWithFixedSizedBVSpec bv n) Bool where
    norewriteVer (BoolWithFixedSizedBVSpec n _) = n
    rewriteVer (BoolWithFixedSizedBVSpec _ r) = r
    wrap = BoolWithFixedSizedBVSpec
    same s = eqTerm (norewriteVer s) (rewriteVer s)
  
  boolWithFSBV ::
    forall p1 p2 bv n.
    (SupportedBV bv n) =>
    p1 bv ->
    p2 n ->
    Int ->
    Gen (BoolWithFixedSizedBVSpec bv n)
  boolWithFSBV _ _ 0 =
    let s =
          oneof $
            return . symSpec . (`withMetadata` (Atom ("bool" :: T.Text)))
              <$> ["a", "b", "c", "d", "e", "f", "g"]
        r = oneof $ return . conSpec <$> [True, False]
     in oneof [r, s]
  boolWithFSBV pbv pn n | n > 0 = do
    v1 <- boolWithFSBV pbv pn (n - 1)
    v2 <- boolWithFSBV pbv pn (n - 1)
    v3 <- boolWithFSBV pbv pn (n - 1)
    v1i <- fsbvWithBool pbv pn (n - 1)
    v2i <- fsbvWithBool pbv pn (n - 1)
    v3i <- fsbvWithBool pbv pn (n - 1)
    frequency
      [ (1, return $ notSpec v1),
        (1, return $ andSpec v1 v2),
        (1, return $ orSpec v1 v2),
        (1, return $ eqvSpec v1 v2),
        (5, return $ eqvSpec v1i v2i),
        (1, return $ distinctSpec $ v1 :| []),
        (1, return $ distinctSpec $ v1 :| [v2]),
        (1, return $ distinctSpec $ v1 :| [v2, v3]),
        (2, return $ distinctSpec $ v1i :| []),
        (2, return $ distinctSpec $ v1i :| [v2i]),
        (2, return $ distinctSpec $ v1i :| [v2i, v3i]),
        (5, return $ ltOrdSpec v1i v2i),
        (5, return $ leOrdSpec v1i v2i),
        (1, return $ iteSpec v1 v2 v3)
      ]
  boolWithFSBV _ _ _ = error "Should never be called"
  
  fsbvWithBool ::
    forall p1 p2 bv n.
    (SupportedBV bv n) =>
    p1 bv ->
    p2 n ->
    Int ->
    Gen (FixedSizedBVWithBoolSpec bv n)
  fsbvWithBool _ _ 0 =
    let s =
          oneof $
            return . symSpec . (`withMetadata` (Atom ("int" :: T.Text)))
              <$> ["a", "b", "c", "d", "e", "f", "g"]
        r =
          conSpec
            <$> oneof
              [ return minBound,
                return maxBound,
                fromInteger <$> arbitrary
              ]
     in oneof [r, s]
  fsbvWithBool pbv pn n | n > 0 = do
    v1b <- boolWithFSBV pbv pn (n - 1)
    v1i <- fsbvWithBool pbv pn (n - 1)
    v2i <- fsbvWithBool pbv pn (n - 1)
    oneof
      [ return $ negNumSpec v1i,
        return $ absNumSpec v1i,
        return $ signumNumSpec v1i,
        return $ addNumSpec v1i v2i,
        return $ mulNumSpec v1i v2i,
        return $ andBitsSpec v1i v2i,
        return $ orBitsSpec v1i v2i,
        return $ xorBitsSpec v1i v2i,
        return $ complementBitsSpec v1i,
        return $ shiftLeftSpec v1i v2i,
        return $ rotateLeftSpec v1i v2i,
        return $ shiftRightSpec v1i v2i,
        return $ rotateRightSpec v1i v2i,
        return $ iteSpec v1b v1i v2i
      ]
  fsbvWithBool _ _ _ = error "Should never be called"
  
  instance (SupportedBV bv n) => Arbitrary (BoolWithFixedSizedBVSpec bv n) where
    arbitrary = sized (boolWithFSBV (Proxy @bv) (Proxy @n))
  
  instance (SupportedBV bv n) => Arbitrary (FixedSizedBVWithBoolSpec bv n) where
    arbitrary = sized (fsbvWithBool Proxy Proxy)
  
  data DifferentSizeBVSpec bv (n :: Nat) = DifferentSizeBVSpec (Term (bv n)) (Term (bv n))
  
  instance (SupportedNonFuncPrim (bv n)) => Show (DifferentSizeBVSpec bv n) where
    show (DifferentSizeBVSpec n r) = "DSizeBVSpec { no: " ++ pformatTerm n ++ ", re: " ++ pformatTerm r ++ " }"
  
  instance (SupportedNonFuncPrim (bv n)) => TermRewritingSpec (DifferentSizeBVSpec bv n) (bv n) where
    norewriteVer (DifferentSizeBVSpec n _) = n
    rewriteVer (DifferentSizeBVSpec _ r) = r
    wrap = DifferentSizeBVSpec
    same s = eqTerm (norewriteVer s) (rewriteVer s)
  
  type SupportedBV bv (n :: Nat) =
    ( SupportedPrim (bv n),
      SupportedNonFuncPrim (bv n),
      Ord (bv n),
      Num (bv n),
      FiniteBits (bv n),
      Integral (bv n),
      Bounded (bv n),
      SymShift (bv n),
      SymRotate (bv n),
      PEvalShiftTerm (bv n),
      PEvalRotateTerm (bv n),
      PEvalNumTerm (bv n),
      PEvalOrdTerm (bv n),
      PEvalBitwiseTerm (bv n),
      KnownNat n,
      PEvalBVTerm bv,
      1 <= n
    )
  
  dsbv1 ::
    forall proxy bv.
    ( SupportedBV bv 1,
      SupportedBV bv 2,
      SupportedBV bv 3,
      SupportedBV bv 4
    ) =>
    proxy bv ->
    Int ->
    Gen (DifferentSizeBVSpec bv 1)
  dsbv1 _ 0 =
    let s =
          oneof $
            return . symSpec . (`withMetadata` (Atom ("bv1" :: T.Text)))
              <$> ["a", "b", "c", "d", "e", "f", "g"]
        r = conSpec . fromInteger <$> arbitrary
     in oneof [r, s]
  dsbv1 p depth | depth > 0 = do
    v1 <- dsbv1 p (depth - 1)
    v1' <- dsbv1 p (depth - 1)
    v2 <- dsbv2 p (depth - 1)
    v3 <- dsbv3 p (depth - 1)
    v4 <- dsbv4 p (depth - 1)
    oneof
      [ return $ negNumSpec v1,
        return $ absNumSpec v1,
        return $ signumNumSpec v1,
        return $ addNumSpec v1 v1',
        return $ mulNumSpec v1 v1',
        return $ andBitsSpec v1 v1',
        return $ orBitsSpec v1 v1',
        return $ xorBitsSpec v1 v1',
        return $ complementBitsSpec v1,
        return $ shiftLeftSpec v1 v1',
        return $ rotateLeftSpec v1 v1',
        return $ shiftRightSpec v1 v1',
        return $ rotateRightSpec v1 v1',
        return $ bvselectSpec (Proxy @0) (Proxy @1) v4,
        return $ bvselectSpec (Proxy @1) (Proxy @1) v4,
        return $ bvselectSpec (Proxy @2) (Proxy @1) v4,
        return $ bvselectSpec (Proxy @3) (Proxy @1) v4,
        return $ bvselectSpec (Proxy @0) (Proxy @1) v3,
        return $ bvselectSpec (Proxy @1) (Proxy @1) v3,
        return $ bvselectSpec (Proxy @2) (Proxy @1) v3,
        return $ bvselectSpec (Proxy @0) (Proxy @1) v2,
        return $ bvselectSpec (Proxy @1) (Proxy @1) v2,
        return $ bvselectSpec (Proxy @0) (Proxy @1) v1
      ]
  dsbv1 _ _ = error "Should never be called"
  
  dsbv2 ::
    forall proxy bv.
    ( SupportedBV bv 1,
      SupportedBV bv 2,
      SupportedBV bv 3,
      SupportedBV bv 4
    ) =>
    proxy bv ->
    Int ->
    Gen (DifferentSizeBVSpec bv 2)
  dsbv2 _ 0 =
    let s =
          oneof $
            return . symSpec . (`withMetadata` (Atom ("bv2" :: T.Text)))
              <$> ["a", "b", "c", "d", "e", "f", "g"]
        r = conSpec . fromInteger <$> arbitrary
     in oneof [r, s]
  dsbv2 p depth | depth > 0 = do
    v1 <- dsbv1 p (depth - 1)
    v1' <- dsbv1 p (depth - 1)
    v2 <- dsbv2 p (depth - 1)
    v2' <- dsbv2 p (depth - 1)
    v3 <- dsbv3 p (depth - 1)
    v4 <- dsbv4 p (depth - 1)
    oneof
      [ return $ negNumSpec v2,
        return $ absNumSpec v2,
        return $ signumNumSpec v2,
        return $ addNumSpec v2 v2',
        return $ mulNumSpec v2 v2',
        return $ andBitsSpec v2 v2',
        return $ orBitsSpec v2 v2',
        return $ xorBitsSpec v2 v2',
        return $ complementBitsSpec v2,
        return $ shiftLeftSpec v2 v2',
        return $ rotateLeftSpec v2 v2',
        return $ shiftRightSpec v2 v2',
        return $ rotateRightSpec v2 v2',
        return $ bvselectSpec (Proxy @0) (Proxy @2) v4,
        return $ bvselectSpec (Proxy @1) (Proxy @2) v4,
        return $ bvselectSpec (Proxy @2) (Proxy @2) v4,
        return $ bvselectSpec (Proxy @0) (Proxy @2) v3,
        return $ bvselectSpec (Proxy @1) (Proxy @2) v3,
        return $ bvselectSpec (Proxy @0) (Proxy @2) v2,
        return $ bvconcatSpec v1 v1',
        return $ bvextendSpec False (Proxy @2) v1,
        return $ bvextendSpec True (Proxy @2) v1
      ]
  dsbv2 _ _ = error "Should never be called"
  
  dsbv3 ::
    forall proxy bv.
    ( SupportedBV bv 1,
      SupportedBV bv 2,
      SupportedBV bv 3,
      SupportedBV bv 4
    ) =>
    proxy bv ->
    Int ->
    Gen (DifferentSizeBVSpec bv 3)
  dsbv3 _ 0 =
    let s =
          oneof $
            return . symSpec . (`withMetadata` (Atom ("bv3" :: T.Text)))
              <$> ["a", "b", "c", "d", "e", "f", "g"]
        r = conSpec . fromInteger <$> arbitrary
     in oneof [r, s]
  dsbv3 p depth | depth > 0 = do
    v1 <- dsbv1 p (depth - 1)
    v2 <- dsbv2 p (depth - 1)
    v3 <- dsbv3 p (depth - 1)
    v3' <- dsbv3 p (depth - 1)
    v4 <- dsbv4 p (depth - 1)
    oneof
      [ return $ negNumSpec v3,
        return $ absNumSpec v3,
        return $ signumNumSpec v3,
        return $ addNumSpec v3 v3',
        return $ mulNumSpec v3 v3',
        return $ andBitsSpec v3 v3',
        return $ orBitsSpec v3 v3',
        return $ xorBitsSpec v3 v3',
        return $ complementBitsSpec v3,
        return $ shiftLeftSpec v3 v3',
        return $ rotateLeftSpec v3 v3',
        return $ shiftRightSpec v3 v3',
        return $ rotateRightSpec v3 v3',
        return $ bvselectSpec (Proxy @0) (Proxy @3) v4,
        return $ bvselectSpec (Proxy @1) (Proxy @3) v4,
        return $ bvselectSpec (Proxy @0) (Proxy @3) v3,
        return $ bvconcatSpec v1 v2,
        return $ bvconcatSpec v2 v1,
        return $ bvextendSpec False (Proxy @3) v1,
        return $ bvextendSpec True (Proxy @3) v1,
        return $ bvextendSpec False (Proxy @3) v2,
        return $ bvextendSpec True (Proxy @3) v2
      ]
  dsbv3 _ _ = error "Should never be called"
  
  dsbv4 ::
    forall proxy bv.
    ( SupportedBV bv 1,
      SupportedBV bv 2,
      SupportedBV bv 3,
      SupportedBV bv 4
    ) =>
    proxy bv ->
    Int ->
    Gen (DifferentSizeBVSpec bv 4)
  dsbv4 _ 0 =
    let s =
          oneof $
            return . symSpec . (`withMetadata` (Atom ("bv4" :: T.Text)))
              <$> ["a", "b", "c", "d", "e", "f", "g"]
        r = conSpec . fromInteger <$> arbitrary
     in oneof [r, s]
  dsbv4 p depth | depth > 0 = do
    v1 <- dsbv1 p (depth - 1)
    v2 <- dsbv2 p (depth - 1)
    v2' <- dsbv2 p (depth - 1)
    v3 <- dsbv3 p (depth - 1)
    v4 <- dsbv4 p (depth - 1)
    v4' <- dsbv4 p (depth - 1)
    oneof
      [ return $ negNumSpec v4,
        return $ absNumSpec v4,
        return $ signumNumSpec v4,
        return $ addNumSpec v4 v4',
        return $ mulNumSpec v4 v4',
        return $ andBitsSpec v4 v4',
        return $ orBitsSpec v4 v4',
        return $ xorBitsSpec v4 v4',
        return $ complementBitsSpec v4,
        return $ shiftLeftSpec v4 v4',
        return $ rotateLeftSpec v4 v4',
        return $ shiftRightSpec v4 v4',
        return $ rotateRightSpec v4 v4',
        return $ bvselectSpec (Proxy @0) (Proxy @4) v4,
        return $ bvconcatSpec v1 v3,
        return $ bvconcatSpec v2 v2',
        return $ bvconcatSpec v3 v1,
        return $ bvextendSpec False (Proxy @4) v1,
        return $ bvextendSpec True (Proxy @4) v1,
        return $ bvextendSpec False (Proxy @4) v2,
        return $ bvextendSpec True (Proxy @4) v2,
        return $ bvextendSpec False (Proxy @4) v3,
        return $ bvextendSpec True (Proxy @4) v3
      ]
  dsbv4 _ _ = error "Should never be called"
  
  instance
    ( SupportedBV bv 1,
      SupportedBV bv 2,
      SupportedBV bv 3,
      SupportedBV bv 4,
      Typeable bv,
      SizedBV bv
    ) =>
    Arbitrary (DifferentSizeBVSpec bv 4)
    where
    arbitrary = sized (dsbv4 Proxy)
  
  data GeneralSpec s = GeneralSpec (Term s) (Term s)
  
  instance (SupportedPrim s) => Show (GeneralSpec s) where
    show (GeneralSpec n r) = "GeneralSpec { no: " ++ pformatTerm n ++ ", re: " ++ pformatTerm r ++ " }"
  
  instance (SupportedNonFuncPrim s) => TermRewritingSpec (GeneralSpec s) s where
    norewriteVer (GeneralSpec n _) = n
    rewriteVer (GeneralSpec _ r) = r
    wrap = GeneralSpec
    same s = eqTerm (norewriteVer s) (rewriteVer s)
  
  data IEEEFPSpec eb sb = IEEEFPSpec (Term (FP eb sb)) (Term (FP eb sb))
  
  instance (ValidFP eb sb) => Show (IEEEFPSpec eb sb) where
    show (IEEEFPSpec n r) =
      "IEEEFPSpec { no: " ++ pformatTerm n ++ ", re: " ++ pformatTerm r ++ " }"
  
  instance (ValidFP eb sb) => TermRewritingSpec (IEEEFPSpec eb sb) (FP eb sb) where
    norewriteVer (IEEEFPSpec n _) = n
    rewriteVer (IEEEFPSpec _ r) = r
    wrap = IEEEFPSpec
    same s =
      orTerm
        ( andTerm
            (fpTraitTerm FPIsNaN (norewriteVer s))
            (fpTraitTerm FPIsNaN (rewriteVer s))
        )
        (eqTerm (norewriteVer s) (rewriteVer s))
  
  instance (ValidFP eb sb) => Arbitrary (IEEEFPSpec eb sb) where
    arbitrary = do
      bool :: BoolOnlySpec <-
        oneof [conSpec <$> arbitrary, return $ symSpec "bool"]
      rounding :: FPRoundingModeSpec <- arbitrary
      let gen =
            oneof
              [conSpec <$> arbitrary, return $ symSpec "a", return $ symSpec "b"]
      a <- gen
      b <- gen
      c <- gen
      let regular =
            [ a,
              iteSpec bool a b,
              addNumSpec a a,
              negNumSpec a,
              mulNumSpec a b,
              absNumSpec a,
              signumNumSpec a,
              fdivSpec a b,
              recipSpec a,
              floatingUnarySpec FloatingSqrt a
            ]
      let uop = fpUnaryOpSpec <$> [FPAbs, FPNeg] <*> return a
      let bop =
            fpBinaryOpSpec
              <$> [ FPRem,
                    FPMinimum,
                    FPMaximum,
                    FPMaximumNumber,
                    FPMinimumNumber
                  ]
              <*> [a]
              <*> [b]
      let ruop =
            fpRoundingUnaryOpSpec
              <$> [FPSqrt, FPRoundToIntegral]
              <*> [rounding]
              <*> [a]
      let rbop =
            fpRoundingBinarySpec
              <$> [FPAdd, FPSub, FPMul, FPDiv]
              <*> [rounding]
              <*> [a]
              <*> [b]
      oneof $
        return
          <$> regular
            ++ uop
            ++ bop
            ++ ruop
            ++ rbop
            ++ [fpFMASpec rounding a b c]
  
  data IEEEFPBoolOpSpec (eb :: Nat) (sb :: Nat)
    = IEEEFPBoolOpSpec (Term Bool) (Term Bool)
  
  instance Show (IEEEFPBoolOpSpec eb sb) where
    show (IEEEFPBoolOpSpec n r) =
      "IEEEFPBoolOpSpec { no: " ++ pformatTerm n ++ ", re: " ++ pformatTerm r ++ " }"
  
  instance TermRewritingSpec (IEEEFPBoolOpSpec eb sb) Bool where
    norewriteVer (IEEEFPBoolOpSpec n _) = n
    rewriteVer (IEEEFPBoolOpSpec _ r) = r
    wrap = IEEEFPBoolOpSpec
    same s = eqTerm (norewriteVer s) (rewriteVer s)
  
  singleFPBoolOpSpecGen ::
    forall eb sb. (ValidFP eb sb) => Gen (IEEEFPBoolOpSpec eb sb)
  singleFPBoolOpSpecGen = do
    s0 :: IEEEFPSpec eb sb <- arbitrary
    s1 :: IEEEFPSpec eb sb <- arbitrary
    s2 :: IEEEFPSpec eb sb <- arbitrary
    let traitGens =
          [ FPIsNaN,
            FPIsPositive,
            FPIsNegative,
            FPIsPositiveInfinite,
            FPIsNegativeInfinite,
            FPIsInfinite,
            FPIsPositiveZero,
            FPIsNegativeZero,
            FPIsZero,
            FPIsNormal,
            FPIsSubnormal,
            FPIsPoint
          ]
            <&> (\trait -> return $ fpTraitSpec trait s0)
    let cmpGens =
          return
            <$> [ eqvSpec s0 s1,
                  distinctSpec $ s0 :| [],
                  distinctSpec $ s0 :| [s1],
                  distinctSpec $ s0 :| [s1, s2],
                  ltOrdSpec s0 s1,
                  leOrdSpec s0 s1
                ]
    oneof $ traitGens ++ cmpGens
  
  instance (ValidFP eb sb) => Arbitrary (IEEEFPBoolOpSpec eb sb) where
    arbitrary = singleFPBoolOpSpecGen
  
  data FPRoundingModeSpec
    = FPRoundingModeSpec (Term FPRoundingMode) (Term FPRoundingMode)
  
  instance Show FPRoundingModeSpec where
    show (FPRoundingModeSpec n r) =
      "FPRoundingModeSpec { no: " ++ pformatTerm n ++ ", re: " ++ pformatTerm r ++ " }"
  
  instance TermRewritingSpec FPRoundingModeSpec FPRoundingMode where
    norewriteVer (FPRoundingModeSpec n _) = n
    rewriteVer (FPRoundingModeSpec _ r) = r
    wrap = FPRoundingModeSpec
    same s = eqTerm (norewriteVer s) (rewriteVer s)
  
  instance Arbitrary FPRoundingModeSpec where
    arbitrary =
      elements
        [ conSpec RNE,
          conSpec RNA,
          conSpec RTP,
          conSpec RTN,
          conSpec RTZ,
          symSpec "a",
          symSpec "b"
        ]
  
  data FPRoundingModeBoolOpSpec = FPRoundingModeBoolOpSpec (Term Bool) (Term Bool)
  
  instance Show FPRoundingModeBoolOpSpec where
    show (FPRoundingModeBoolOpSpec n r) =
      "FPRoundingModeBoolOpSpec { no: " ++ pformatTerm n ++ ", re: " ++ pformatTerm r ++ " }"
  
  instance TermRewritingSpec FPRoundingModeBoolOpSpec Bool where
    norewriteVer (FPRoundingModeBoolOpSpec n _) = n
    rewriteVer (FPRoundingModeBoolOpSpec _ r) = r
    wrap = FPRoundingModeBoolOpSpec
    same s = eqTerm (norewriteVer s) (rewriteVer s)
  
  instance Arbitrary FPRoundingModeBoolOpSpec where
    arbitrary = do
      l :: FPRoundingModeSpec <- arbitrary
      r <- arbitrary
      x <- arbitrary
      elements
        [ eqvSpec l r,
          distinctSpec $ l :| [],
          distinctSpec $ l :| [r],
          distinctSpec $ l :| [r, x],
          ltOrdSpec l r,
          leOrdSpec l r
        ]
  
  data BoolWithNRASpec = BoolWithNRASpec (Term Bool) (Term Bool)
  
  instance Show BoolWithNRASpec where
    show (BoolWithNRASpec n r) =
      "BoolWithNRASpec { no: " ++ pformatTerm n ++ ", re: " ++ pformatTerm r ++ " }"
  
  instance TermRewritingSpec BoolWithNRASpec Bool where
    norewriteVer (BoolWithNRASpec n _) = n
    rewriteVer (BoolWithNRASpec _ r) = r
    wrap = BoolWithNRASpec
    same s = eqTerm (norewriteVer s) (rewriteVer s)
  
  data NRAWithBoolSpec = NRAWithBoolSpec (Term AlgReal) (Term AlgReal)
  
  instance Show NRAWithBoolSpec where
    show (NRAWithBoolSpec n r) =
      "NRAWithBoolSpec { no: " ++ pformatTerm n ++ ", re: " ++ pformatTerm r ++ " }"
  
  instance TermRewritingSpec NRAWithBoolSpec AlgReal where
    norewriteVer (NRAWithBoolSpec n _) = n
    rewriteVer (NRAWithBoolSpec _ r) = r
    wrap = NRAWithBoolSpec
    same s = eqTerm (norewriteVer s) (rewriteVer s)
  
  boolWithNRA :: Int -> Gen BoolWithNRASpec
  boolWithNRA 0 =
    let s =
          oneof $
            return . symSpec . (`withMetadata` (Atom ("bool" :: T.Text)))
              <$> ["a", "b", "c", "d", "e", "f", "g"]
        r = oneof $ return . conSpec <$> [True, False]
     in oneof [r, s]
  boolWithNRA n | n > 0 = do
    v1 <- boolWithNRA (n - 1)
    v2 <- boolWithNRA (n - 1)
    v3 <- boolWithNRA (n - 1)
    v1i <- nraWithBool (n - 1)
    v2i <- nraWithBool (n - 1)
    v3i <- nraWithBool (n - 1)
    frequency
      [ (1, return $ notSpec v1),
        (1, return $ andSpec v1 v2),
        (1, return $ orSpec v1 v2),
        (1, return $ eqvSpec v1 v2),
        (5, return $ eqvSpec v1i v2i),
        (1, return $ distinctSpec $ v1 :| []),
        (1, return $ distinctSpec $ v1 :| [v2]),
        (1, return $ distinctSpec $ v1 :| [v2, v3]),
        (2, return $ distinctSpec $ v1i :| []),
        (2, return $ distinctSpec $ v1i :| [v2i]),
        (2, return $ distinctSpec $ v1i :| [v2i, v3i]),
        (5, return $ ltOrdSpec v1i v2i),
        (5, return $ leOrdSpec v1i v2i),
        (1, return $ iteSpec v1 v2 v3)
      ]
  boolWithNRA _ = error "Should never be called"
  
  nraWithBool :: Int -> Gen NRAWithBoolSpec
  nraWithBool 0 =
    let s =
          oneof $
            return . symSpec . (`withMetadata` (Atom ("real" :: T.Text)))
              <$> ["a", "b", "c", "d", "e", "f", "g"]
        r = conSpec <$> arbitrary
     in oneof [r, s]
  nraWithBool n | n > 0 = do
    v1b <- boolWithNRA (n - 1)
    v1i <- nraWithBool (n - 1)
    v2i <- nraWithBool (n - 1)
    oneof
      [ return $ negNumSpec v1i,
        return $ absNumSpec v1i,
        return $ signumNumSpec v1i,
        return $ addNumSpec v1i v2i,
        return $ mulNumSpec v1i v2i,
        return $ fdivSpec v1i v2i,
        return $ recipSpec v1i,
        return $ iteSpec v1b v1i v2i
      ]
  nraWithBool _ = error "Should never be called"
  
  instance Arbitrary BoolWithNRASpec where
    arbitrary = sized boolWithNRA
  
  instance Arbitrary NRAWithBoolSpec where
    arbitrary = sized nraWithBool
  