{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Eta reduce" #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.TabularFun
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.TabularFun
  ( type (=->) (..),
  )
where

import Control.DeepSeq (NFData, NFData1)
import Data.Bifunctor (Bifunctor (second))
import Data.Hashable (Hashable)
import qualified Data.SBV as SBV
import qualified Data.SBV.Dynamic as SBVD
import GHC.Generics (Generic, Generic1)
import Grisette.Internal.Core.Data.Class.Function (Function ((#)))
import Grisette.Internal.SymPrim.Prim.Internal.IsZero (KnownIsZero)
import Grisette.Internal.SymPrim.Prim.Internal.PartialEval (totalize2)
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( NonFuncSBVRep (NonFuncSBVBaseType),
    PEvalApplyTerm (pevalApplyTerm, sbvApplyTerm),
    SBVRep (SBVType),
    SupportedNonFuncPrim (conNonFuncSBVTerm, withNonFuncPrim),
    SupportedPrim
      ( conSBVTerm,
        defaultValue,
        parseSMTModelResult,
        pevalITETerm,
        sbvEq,
        sbvIte,
        symSBVName,
        symSBVTerm,
        withPrim
      ),
    SupportedPrimConstraint (PrimConstraint),
    Term (ConTerm),
    applyTerm,
    conTerm,
    partitionCVArg,
    pevalDefaultEqTerm,
    pevalEqTerm,
    pevalITEBasicTerm,
    translateTypeError,
  )
import Language.Haskell.TH.Syntax (Lift)
import Type.Reflection (typeRep)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim

-- |
-- Functions as a table. Use the `#` operator to apply the function.
--
-- >>> :set -XTypeOperators
-- >>> let f = TabularFun [(1, 2), (3, 4)] 0 :: Int =-> Int
-- >>> f # 1
-- 2
-- >>> f # 2
-- 0
-- >>> f # 3
-- 4
data (=->) a b = TabularFun {forall a b. (a =-> b) -> [(a, b)]
funcTable :: [(a, b)], forall a b. (a =-> b) -> b
defaultFuncValue :: b}
  deriving (Int -> (a =-> b) -> ShowS
[a =-> b] -> ShowS
(a =-> b) -> String
(Int -> (a =-> b) -> ShowS)
-> ((a =-> b) -> String) -> ([a =-> b] -> ShowS) -> Show (a =-> b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> (a =-> b) -> ShowS
forall a b. (Show a, Show b) => [a =-> b] -> ShowS
forall a b. (Show a, Show b) => (a =-> b) -> String
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> (a =-> b) -> ShowS
showsPrec :: Int -> (a =-> b) -> ShowS
$cshow :: forall a b. (Show a, Show b) => (a =-> b) -> String
show :: (a =-> b) -> String
$cshowList :: forall a b. (Show a, Show b) => [a =-> b] -> ShowS
showList :: [a =-> b] -> ShowS
Show, (a =-> b) -> (a =-> b) -> Bool
((a =-> b) -> (a =-> b) -> Bool)
-> ((a =-> b) -> (a =-> b) -> Bool) -> Eq (a =-> b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. (Eq a, Eq b) => (a =-> b) -> (a =-> b) -> Bool
$c== :: forall a b. (Eq a, Eq b) => (a =-> b) -> (a =-> b) -> Bool
== :: (a =-> b) -> (a =-> b) -> Bool
$c/= :: forall a b. (Eq a, Eq b) => (a =-> b) -> (a =-> b) -> Bool
/= :: (a =-> b) -> (a =-> b) -> Bool
Eq, (forall x. (a =-> b) -> Rep (a =-> b) x)
-> (forall x. Rep (a =-> b) x -> a =-> b) -> Generic (a =-> b)
forall x. Rep (a =-> b) x -> a =-> b
forall x. (a =-> b) -> Rep (a =-> b) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a b x. Rep (a =-> b) x -> a =-> b
forall a b x. (a =-> b) -> Rep (a =-> b) x
$cfrom :: forall a b x. (a =-> b) -> Rep (a =-> b) x
from :: forall x. (a =-> b) -> Rep (a =-> b) x
$cto :: forall a b x. Rep (a =-> b) x -> a =-> b
to :: forall x. Rep (a =-> b) x -> a =-> b
Generic, (forall a. (a =-> a) -> Rep1 ((=->) a) a)
-> (forall a. Rep1 ((=->) a) a -> a =-> a) -> Generic1 ((=->) a)
forall a. Rep1 ((=->) a) a -> a =-> a
forall a. (a =-> a) -> Rep1 ((=->) a) a
forall a a. Rep1 ((=->) a) a -> a =-> a
forall a a. (a =-> a) -> Rep1 ((=->) a) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cfrom1 :: forall a a. (a =-> a) -> Rep1 ((=->) a) a
from1 :: forall a. (a =-> a) -> Rep1 ((=->) a) a
$cto1 :: forall a a. Rep1 ((=->) a) a -> a =-> a
to1 :: forall a. Rep1 ((=->) a) a -> a =-> a
Generic1, (forall (m :: * -> *). Quote m => (a =-> b) -> m Exp)
-> (forall (m :: * -> *). Quote m => (a =-> b) -> Code m (a =-> b))
-> Lift (a =-> b)
forall a b (m :: * -> *).
(Lift a, Lift b, Quote m) =>
(a =-> b) -> m Exp
forall a b (m :: * -> *).
(Lift a, Lift b, Quote m) =>
(a =-> b) -> Code m (a =-> b)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => (a =-> b) -> m Exp
forall (m :: * -> *). Quote m => (a =-> b) -> Code m (a =-> b)
$clift :: forall a b (m :: * -> *).
(Lift a, Lift b, Quote m) =>
(a =-> b) -> m Exp
lift :: forall (m :: * -> *). Quote m => (a =-> b) -> m Exp
$cliftTyped :: forall a b (m :: * -> *).
(Lift a, Lift b, Quote m) =>
(a =-> b) -> Code m (a =-> b)
liftTyped :: forall (m :: * -> *). Quote m => (a =-> b) -> Code m (a =-> b)
Lift, (a =-> b) -> ()
((a =-> b) -> ()) -> NFData (a =-> b)
forall a. (a -> ()) -> NFData a
forall a b. (NFData a, NFData b) => (a =-> b) -> ()
$crnf :: forall a b. (NFData a, NFData b) => (a =-> b) -> ()
rnf :: (a =-> b) -> ()
NFData, (forall a. (a -> ()) -> (a =-> a) -> ()) -> NFData1 ((=->) a)
forall a a. NFData a => (a -> ()) -> (a =-> a) -> ()
forall a. (a -> ()) -> (a =-> a) -> ()
forall (f :: * -> *).
(forall a. (a -> ()) -> f a -> ()) -> NFData1 f
$cliftRnf :: forall a a. NFData a => (a -> ()) -> (a =-> a) -> ()
liftRnf :: forall a. (a -> ()) -> (a =-> a) -> ()
NFData1)

infixr 0 =->

instance (Eq a) => Function (a =-> b) a b where
  (TabularFun [(a, b)]
table b
d) # :: (a =-> b) -> a -> b
# a
a = [(a, b)] -> b
go [(a, b)]
table
    where
      go :: [(a, b)] -> b
go [] = b
d
      go ((a
av, b
bv) : [(a, b)]
s)
        | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
av = b
bv
        | Bool
otherwise = [(a, b)] -> b
go [(a, b)]
s

instance (Hashable a, Hashable b) => Hashable (a =-> b)

instance
  (SupportedNonFuncPrim a, SupportedPrim b) =>
  SupportedPrimConstraint (a =-> b)
  where
  type
    PrimConstraint n (a =-> b) =
      ( SupportedNonFuncPrim a,
        SupportedPrim b,
        PrimConstraint n b
      )

instance (SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a =-> b) where
  type SBVType n (a =-> b) = SBV.SBV (NonFuncSBVBaseType n a) -> SBVType n b

parseTabularFunSMTModelResult ::
  forall a b.
  (SupportedNonFuncPrim a, SupportedPrim b) =>
  Int ->
  ([([SBVD.CV], SBVD.CV)], SBVD.CV) ->
  a =-> b
parseTabularFunSMTModelResult :: forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult Int
level ([([CV], CV)]
l, CV
s) =
  [(a, b)] -> b -> a =-> b
forall a b. [(a, b)] -> b -> a =-> b
TabularFun
    ( ([([CV], CV)] -> b) -> (a, [([CV], CV)]) -> (a, b)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second
        (\[([CV], CV)]
r -> Int -> ([([CV], CV)], CV) -> b
forall t. SupportedPrim t => Int -> ([([CV], CV)], CV) -> t
parseSMTModelResult (Int
level Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ([([CV], CV)]
r, CV
s))
        ((a, [([CV], CV)]) -> (a, b)) -> [(a, [([CV], CV)])] -> [(a, b)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
SupportedNonFuncPrim a =>
[([CV], CV)] -> [(a, [([CV], CV)])]
partitionCVArg @a [([CV], CV)]
l
    )
    (Int -> ([([CV], CV)], CV) -> b
forall t. SupportedPrim t => Int -> ([([CV], CV)], CV) -> t
parseSMTModelResult (Int
level Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ([], CV
s))

instance
  (SupportedNonFuncPrim a, SupportedNonFuncPrim b) =>
  SupportedPrim (a =-> b)
  where
  defaultValue :: a =-> b
defaultValue = [(a, b)] -> b -> a =-> b
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] b
forall t. SupportedPrim t => t
defaultValue
  pevalITETerm :: Term Bool -> Term (a =-> b) -> Term (a =-> b) -> Term (a =-> b)
pevalITETerm = Term Bool -> Term (a =-> b) -> Term (a =-> b) -> Term (a =-> b)
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term (a =-> b) -> Term (a =-> b) -> Term Bool
pevalEqTerm = Term (a =-> b) -> Term (a =-> b) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> (a =-> b) -> SBVType n (a =-> b)
conSBVTerm proxy n
p a =-> b
f =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
   Mergeable (SBVType n b), SMTDefinable (SBVType n b),
   Mergeable (SBVType n b),
   SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
  SBVType n (a =-> b))
 -> SBVType n (a =-> b))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
     Mergeable (SBVType n b), SMTDefinable (SBVType n b),
     Mergeable (SBVType n b),
     SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
    SBVType n (a =-> b))
-> SBVType n (a =-> b)
forall a b. (a -> b) -> a -> b
$
      proxy n -> (a =-> b) -> SBV (NonFuncSBVBaseType n a) -> SBVType n b
forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
 Mergeable (SBVType integerBitWidth b),
 KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy n
p a =-> b
f
  symSBVName :: TypedSymbol (a =-> b) -> Int -> String
symSBVName TypedSymbol (a =-> b)
_ Int
num = String
"tfunc2" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
num
  symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n (a =-> b))
symSBVTerm (proxy n
p :: proxy n) String
name =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
   Mergeable (SBVType n a), SMTDefinable (SBVType n a),
   Mergeable (SBVType n a),
   SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
  m (SBVType n (a =-> b)))
 -> m (SBVType n (a =-> b)))
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    m (SBVType n (a =-> b)))
-> m (SBVType n (a =-> b))
forall a b. (a -> b) -> a -> b
$
      forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
   Mergeable (SBVType n b), SMTDefinable (SBVType n b),
   Mergeable (SBVType n b),
   SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
  m (SBVType n (a =-> b)))
 -> m (SBVType n (a =-> b)))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
     Mergeable (SBVType n b), SMTDefinable (SBVType n b),
     Mergeable (SBVType n b),
     SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
    m (SBVType n (a =-> b)))
-> m (SBVType n (a =-> b))
forall a b. (a -> b) -> a -> b
$
        SBVType n (a =-> b) -> m (SBVType n (a =-> b))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVType n (a =-> b) -> m (SBVType n (a =-> b)))
-> SBVType n (a =-> b) -> m (SBVType n (a =-> b))
forall a b. (a -> b) -> a -> b
$
          String
-> SBV (NonFuncSBVBaseType n a) -> SBV (NonFuncSBVBaseType n b)
forall a. SMTDefinable a => String -> a
SBV.uninterpret String
name
  withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint n (a =-> b),
     SMTDefinable (SBVType n (a =-> b)),
     Mergeable (SBVType n (a =-> b)), Typeable (SBVType n (a =-> b))) =>
    a)
-> a
withPrim p n
p (PrimConstraint n (a =-> b), SMTDefinable (SBVType n (a =-> b)),
 Mergeable (SBVType n (a =-> b)), Typeable (SBVType n (a =-> b))) =>
a
r = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @a p n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
   Mergeable (SBVType n a), SMTDefinable (SBVType n a),
   Mergeable (SBVType n a),
   SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$ forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b p n
p a
(SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
 Mergeable (SBVType n b), SMTDefinable (SBVType n b),
 Mergeable (SBVType n b),
 SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
a
(PrimConstraint n (a =-> b), SMTDefinable (SBVType n (a =-> b)),
 Mergeable (SBVType n (a =-> b)), Typeable (SBVType n (a =-> b))) =>
a
r
  sbvIte :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBV Bool
-> SBVType n (a =-> b)
-> SBVType n (a =-> b)
-> SBVType n (a =-> b)
sbvIte proxy n
p = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b proxy n
p (SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
 Mergeable (SBVType n b), SMTDefinable (SBVType n b),
 Mergeable (SBVType n b),
 SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
SBV Bool
-> (SBV (NonFuncSBVBaseType n a) -> SBVType n b)
-> (SBV (NonFuncSBVBaseType n a) -> SBVType n b)
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n b
SBV Bool
-> (SBV (NonFuncSBVBaseType n a) -> SBV (NonFuncSBVBaseType n b))
-> (SBV (NonFuncSBVBaseType n a) -> SBV (NonFuncSBVBaseType n b))
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
SBV Bool
-> (SBV (NonFuncSBVBaseType n a) -> SBVType n b)
-> (SBV (NonFuncSBVBaseType n a) -> SBVType n b)
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n b
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
  sbvEq :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> SBVType n (a =-> b) -> SBVType n (a =-> b) -> SBV Bool
sbvEq proxy n
_ SBVType n (a =-> b)
_ =
    Maybe String
-> TypeRep (a =-> b)
-> (SBV (NonFuncSBVBaseType n a) -> SBVType n b)
-> SBV Bool
forall a b. HasCallStack => Maybe String -> TypeRep a -> b
translateTypeError
      ( String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
          String
"BUG. Please send a bug report. TabularFun is not supported for "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"equality comparison."
      )
      (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a =-> b))
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> b
parseSMTModelResult = Int -> ([([CV], CV)], CV) -> a =-> b
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult

instance
  {-# OVERLAPPING #-}
  ( SupportedNonFuncPrim a,
    SupportedNonFuncPrim b,
    SupportedNonFuncPrim c,
    SupportedPrim a,
    SupportedPrim b,
    SupportedPrim c
  ) =>
  SupportedPrim (a =-> b =-> c)
  where
  defaultValue :: a =-> (b =-> c)
defaultValue = [(a, b =-> c)] -> (b =-> c) -> a =-> (b =-> c)
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] b =-> c
forall t. SupportedPrim t => t
defaultValue
  pevalITETerm :: Term Bool
-> Term (a =-> (b =-> c))
-> Term (a =-> (b =-> c))
-> Term (a =-> (b =-> c))
pevalITETerm = Term Bool
-> Term (a =-> (b =-> c))
-> Term (a =-> (b =-> c))
-> Term (a =-> (b =-> c))
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term (a =-> (b =-> c)) -> Term (a =-> (b =-> c)) -> Term Bool
pevalEqTerm = Term (a =-> (b =-> c)) -> Term (a =-> (b =-> c)) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> (a =-> (b =-> c)) -> SBVType n (a =-> (b =-> c))
conSBVTerm proxy n
p a =-> (b =-> c)
f =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @c proxy n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
   Mergeable (SBVType n c), SMTDefinable (SBVType n c),
   Mergeable (SBVType n c),
   SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
  SBVType n (a =-> (b =-> c)))
 -> SBVType n (a =-> (b =-> c)))
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
     Mergeable (SBVType n c), SMTDefinable (SBVType n c),
     Mergeable (SBVType n c),
     SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
    SBVType n (a =-> (b =-> c)))
-> SBVType n (a =-> (b =-> c))
forall a b. (a -> b) -> a -> b
$
      proxy n
-> (a =-> (b =-> c))
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n (b =-> c)
forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
 Mergeable (SBVType integerBitWidth b),
 KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy n
p a =-> (b =-> c)
f
  symSBVName :: TypedSymbol (a =-> (b =-> c)) -> Int -> String
symSBVName TypedSymbol (a =-> (b =-> c))
_ Int
num = String
"tfunc3" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
num
  symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n (a =-> (b =-> c)))
symSBVTerm (proxy n
p :: proxy n) String
name =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
   Mergeable (SBVType n a), SMTDefinable (SBVType n a),
   Mergeable (SBVType n a),
   SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
  m (SBVType n (a =-> (b =-> c))))
 -> m (SBVType n (a =-> (b =-> c))))
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    m (SBVType n (a =-> (b =-> c))))
-> m (SBVType n (a =-> (b =-> c)))
forall a b. (a -> b) -> a -> b
$
      forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
   Mergeable (SBVType n b), SMTDefinable (SBVType n b),
   Mergeable (SBVType n b),
   SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
  m (SBVType n (a =-> (b =-> c))))
 -> m (SBVType n (a =-> (b =-> c))))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
     Mergeable (SBVType n b), SMTDefinable (SBVType n b),
     Mergeable (SBVType n b),
     SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
    m (SBVType n (a =-> (b =-> c))))
-> m (SBVType n (a =-> (b =-> c)))
forall a b. (a -> b) -> a -> b
$
        forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @c proxy n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
   Mergeable (SBVType n c), SMTDefinable (SBVType n c),
   Mergeable (SBVType n c),
   SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
  m (SBVType n (a =-> (b =-> c))))
 -> m (SBVType n (a =-> (b =-> c))))
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
     Mergeable (SBVType n c), SMTDefinable (SBVType n c),
     Mergeable (SBVType n c),
     SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
    m (SBVType n (a =-> (b =-> c))))
-> m (SBVType n (a =-> (b =-> c)))
forall a b. (a -> b) -> a -> b
$
          SBVType n (a =-> (b =-> c)) -> m (SBVType n (a =-> (b =-> c)))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVType n (a =-> (b =-> c)) -> m (SBVType n (a =-> (b =-> c))))
-> SBVType n (a =-> (b =-> c)) -> m (SBVType n (a =-> (b =-> c)))
forall a b. (a -> b) -> a -> b
$
            String
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
forall a. SMTDefinable a => String -> a
SBV.uninterpret String
name
  withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint n (a =-> (b =-> c)),
     SMTDefinable (SBVType n (a =-> (b =-> c))),
     Mergeable (SBVType n (a =-> (b =-> c))),
     Typeable (SBVType n (a =-> (b =-> c)))) =>
    a)
-> a
withPrim p n
p (PrimConstraint n (a =-> (b =-> c)),
 SMTDefinable (SBVType n (a =-> (b =-> c))),
 Mergeable (SBVType n (a =-> (b =-> c))),
 Typeable (SBVType n (a =-> (b =-> c)))) =>
a
r =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @a p n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
   Mergeable (SBVType n a), SMTDefinable (SBVType n a),
   Mergeable (SBVType n a),
   SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
      forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b p n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
   Mergeable (SBVType n b), SMTDefinable (SBVType n b),
   Mergeable (SBVType n b),
   SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
     Mergeable (SBVType n b), SMTDefinable (SBVType n b),
     Mergeable (SBVType n b),
     SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
        forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @c p n
p a
(SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
 Mergeable (SBVType n c), SMTDefinable (SBVType n c),
 Mergeable (SBVType n c),
 SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
a
(PrimConstraint n (a =-> (b =-> c)),
 SMTDefinable (SBVType n (a =-> (b =-> c))),
 Mergeable (SBVType n (a =-> (b =-> c))),
 Typeable (SBVType n (a =-> (b =-> c)))) =>
a
r
  sbvIte :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBV Bool
-> SBVType n (a =-> (b =-> c))
-> SBVType n (a =-> (b =-> c))
-> SBVType n (a =-> (b =-> c))
sbvIte proxy n
p = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @c proxy n
p (SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
 Mergeable (SBVType n c), SMTDefinable (SBVType n c),
 Mergeable (SBVType n c),
 SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b) -> SBVType n c)
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b) -> SBVType n c)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBVType n c
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b) -> SBV (NonFuncSBVBaseType n c))
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b) -> SBV (NonFuncSBVBaseType n c))
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b) -> SBVType n c)
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b) -> SBVType n c)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBVType n c
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
  sbvEq :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBVType n (a =-> (b =-> c))
-> SBVType n (a =-> (b =-> c))
-> SBV Bool
sbvEq proxy n
_ SBVType n (a =-> (b =-> c))
_ =
    Maybe String
-> TypeRep (a =-> (b =-> c))
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b) -> SBVType n c)
-> SBV Bool
forall a b. HasCallStack => Maybe String -> TypeRep a -> b
translateTypeError
      ( String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
          String
"BUG. Please send a bug report. TabularFun is not supported for "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"equality comparison."
      )
      (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a =-> b =-> c))
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> c)
parseSMTModelResult = Int -> ([([CV], CV)], CV) -> a =-> (b =-> c)
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult

instance
  {-# OVERLAPPING #-}
  ( SupportedNonFuncPrim a,
    SupportedNonFuncPrim b,
    SupportedNonFuncPrim c,
    SupportedNonFuncPrim d,
    SupportedPrim a,
    SupportedPrim b,
    SupportedPrim c,
    SupportedPrim d
  ) =>
  SupportedPrim (a =-> b =-> c =-> d)
  where
  defaultValue :: a =-> (b =-> (c =-> d))
defaultValue = [(a, b =-> (c =-> d))]
-> (b =-> (c =-> d)) -> a =-> (b =-> (c =-> d))
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] b =-> (c =-> d)
forall t. SupportedPrim t => t
defaultValue
  pevalITETerm :: Term Bool
-> Term (a =-> (b =-> (c =-> d)))
-> Term (a =-> (b =-> (c =-> d)))
-> Term (a =-> (b =-> (c =-> d)))
pevalITETerm = Term Bool
-> Term (a =-> (b =-> (c =-> d)))
-> Term (a =-> (b =-> (c =-> d)))
-> Term (a =-> (b =-> (c =-> d)))
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term (a =-> (b =-> (c =-> d)))
-> Term (a =-> (b =-> (c =-> d))) -> Term Bool
pevalEqTerm = Term (a =-> (b =-> (c =-> d)))
-> Term (a =-> (b =-> (c =-> d))) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> (a =-> (b =-> (c =-> d))) -> SBVType n (a =-> (b =-> (c =-> d)))
conSBVTerm proxy n
p a =-> (b =-> (c =-> d))
f =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @d proxy n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
   Mergeable (SBVType n d), SMTDefinable (SBVType n d),
   Mergeable (SBVType n d),
   SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
  SBVType n (a =-> (b =-> (c =-> d))))
 -> SBVType n (a =-> (b =-> (c =-> d))))
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
     Mergeable (SBVType n d), SMTDefinable (SBVType n d),
     Mergeable (SBVType n d),
     SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
    SBVType n (a =-> (b =-> (c =-> d))))
-> SBVType n (a =-> (b =-> (c =-> d)))
forall a b. (a -> b) -> a -> b
$
      proxy n
-> (a =-> (b =-> (c =-> d)))
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n (b =-> (c =-> d))
forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
 Mergeable (SBVType integerBitWidth b),
 KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy n
p a =-> (b =-> (c =-> d))
f
  symSBVName :: TypedSymbol (a =-> (b =-> (c =-> d))) -> Int -> String
symSBVName TypedSymbol (a =-> (b =-> (c =-> d)))
_ Int
num = String
"tfunc4" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
num
  symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> d))))
symSBVTerm (proxy n
p :: proxy n) String
name =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
   Mergeable (SBVType n a), SMTDefinable (SBVType n a),
   Mergeable (SBVType n a),
   SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
  m (SBVType n (a =-> (b =-> (c =-> d)))))
 -> m (SBVType n (a =-> (b =-> (c =-> d)))))
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    m (SBVType n (a =-> (b =-> (c =-> d)))))
-> m (SBVType n (a =-> (b =-> (c =-> d))))
forall a b. (a -> b) -> a -> b
$
      forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
   Mergeable (SBVType n b), SMTDefinable (SBVType n b),
   Mergeable (SBVType n b),
   SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
  m (SBVType n (a =-> (b =-> (c =-> d)))))
 -> m (SBVType n (a =-> (b =-> (c =-> d)))))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
     Mergeable (SBVType n b), SMTDefinable (SBVType n b),
     Mergeable (SBVType n b),
     SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
    m (SBVType n (a =-> (b =-> (c =-> d)))))
-> m (SBVType n (a =-> (b =-> (c =-> d))))
forall a b. (a -> b) -> a -> b
$
        forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @c proxy n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
   Mergeable (SBVType n c), SMTDefinable (SBVType n c),
   Mergeable (SBVType n c),
   SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
  m (SBVType n (a =-> (b =-> (c =-> d)))))
 -> m (SBVType n (a =-> (b =-> (c =-> d)))))
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
     Mergeable (SBVType n c), SMTDefinable (SBVType n c),
     Mergeable (SBVType n c),
     SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
    m (SBVType n (a =-> (b =-> (c =-> d)))))
-> m (SBVType n (a =-> (b =-> (c =-> d))))
forall a b. (a -> b) -> a -> b
$
          forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @d proxy n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
   Mergeable (SBVType n d), SMTDefinable (SBVType n d),
   Mergeable (SBVType n d),
   SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
  m (SBVType n (a =-> (b =-> (c =-> d)))))
 -> m (SBVType n (a =-> (b =-> (c =-> d)))))
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
     Mergeable (SBVType n d), SMTDefinable (SBVType n d),
     Mergeable (SBVType n d),
     SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
    m (SBVType n (a =-> (b =-> (c =-> d)))))
-> m (SBVType n (a =-> (b =-> (c =-> d))))
forall a b. (a -> b) -> a -> b
$
            SBVType n (a =-> (b =-> (c =-> d)))
-> m (SBVType n (a =-> (b =-> (c =-> d))))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVType n (a =-> (b =-> (c =-> d)))
 -> m (SBVType n (a =-> (b =-> (c =-> d)))))
-> SBVType n (a =-> (b =-> (c =-> d)))
-> m (SBVType n (a =-> (b =-> (c =-> d))))
forall a b. (a -> b) -> a -> b
$
              String
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
forall a. SMTDefinable a => String -> a
SBV.uninterpret String
name
  withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint n (a =-> (b =-> (c =-> d))),
     SMTDefinable (SBVType n (a =-> (b =-> (c =-> d)))),
     Mergeable (SBVType n (a =-> (b =-> (c =-> d)))),
     Typeable (SBVType n (a =-> (b =-> (c =-> d))))) =>
    a)
-> a
withPrim p n
p (PrimConstraint n (a =-> (b =-> (c =-> d))),
 SMTDefinable (SBVType n (a =-> (b =-> (c =-> d)))),
 Mergeable (SBVType n (a =-> (b =-> (c =-> d)))),
 Typeable (SBVType n (a =-> (b =-> (c =-> d))))) =>
a
r =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @a p n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
   Mergeable (SBVType n a), SMTDefinable (SBVType n a),
   Mergeable (SBVType n a),
   SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
      forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b p n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
   Mergeable (SBVType n b), SMTDefinable (SBVType n b),
   Mergeable (SBVType n b),
   SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
     Mergeable (SBVType n b), SMTDefinable (SBVType n b),
     Mergeable (SBVType n b),
     SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
        forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @c p n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
   Mergeable (SBVType n c), SMTDefinable (SBVType n c),
   Mergeable (SBVType n c),
   SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
     Mergeable (SBVType n c), SMTDefinable (SBVType n c),
     Mergeable (SBVType n c),
     SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
          forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @d p n
p a
(SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
 Mergeable (SBVType n d), SMTDefinable (SBVType n d),
 Mergeable (SBVType n d),
 SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
a
(PrimConstraint n (a =-> (b =-> (c =-> d))),
 SMTDefinable (SBVType n (a =-> (b =-> (c =-> d)))),
 Mergeable (SBVType n (a =-> (b =-> (c =-> d)))),
 Typeable (SBVType n (a =-> (b =-> (c =-> d))))) =>
a
r
  sbvIte :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBV Bool
-> SBVType n (a =-> (b =-> (c =-> d)))
-> SBVType n (a =-> (b =-> (c =-> d)))
-> SBVType n (a =-> (b =-> (c =-> d)))
sbvIte proxy n
p = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @d proxy n
p (SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
 Mergeable (SBVType n d), SMTDefinable (SBVType n d),
 Mergeable (SBVType n d),
 SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBVType n d)
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBVType n d)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBVType n d
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d))
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d))
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBVType n d)
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBVType n d)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBVType n d
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
  sbvEq :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBVType n (a =-> (b =-> (c =-> d)))
-> SBVType n (a =-> (b =-> (c =-> d)))
-> SBV Bool
sbvEq proxy n
_ SBVType n (a =-> (b =-> (c =-> d)))
_ =
    Maybe String
-> TypeRep (a =-> (b =-> (c =-> d)))
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBVType n d)
-> SBV Bool
forall a b. HasCallStack => Maybe String -> TypeRep a -> b
translateTypeError
      ( String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
          String
"BUG. Please send a bug report. TabularFun is not supported for "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"equality comparison."
      )
      (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a =-> b =-> c =-> d))
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> d))
parseSMTModelResult = Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> d))
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult

instance
  {-# OVERLAPPING #-}
  ( SupportedNonFuncPrim a,
    SupportedNonFuncPrim b,
    SupportedNonFuncPrim c,
    SupportedNonFuncPrim d,
    SupportedNonFuncPrim e,
    SupportedPrim a,
    SupportedPrim b,
    SupportedPrim c,
    SupportedPrim d,
    SupportedPrim e
  ) =>
  SupportedPrim (a =-> b =-> c =-> d =-> e)
  where
  defaultValue :: a =-> (b =-> (c =-> (d =-> e)))
defaultValue = [(a, b =-> (c =-> (d =-> e)))]
-> (b =-> (c =-> (d =-> e))) -> a =-> (b =-> (c =-> (d =-> e)))
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] b =-> (c =-> (d =-> e))
forall t. SupportedPrim t => t
defaultValue
  pevalITETerm :: Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> e))))
-> Term (a =-> (b =-> (c =-> (d =-> e))))
-> Term (a =-> (b =-> (c =-> (d =-> e))))
pevalITETerm = Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> e))))
-> Term (a =-> (b =-> (c =-> (d =-> e))))
-> Term (a =-> (b =-> (c =-> (d =-> e))))
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> e))))
-> Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term Bool
pevalEqTerm = Term (a =-> (b =-> (c =-> (d =-> e))))
-> Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> (a =-> (b =-> (c =-> (d =-> e))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
conSBVTerm proxy n
p a =-> (b =-> (c =-> (d =-> e)))
f =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @e proxy n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
   Mergeable (SBVType n e), SMTDefinable (SBVType n e),
   Mergeable (SBVType n e),
   SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
  SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
 -> SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
     Mergeable (SBVType n e), SMTDefinable (SBVType n e),
     Mergeable (SBVType n e),
     SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
    SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
forall a b. (a -> b) -> a -> b
$
      proxy n
-> (a =-> (b =-> (c =-> (d =-> e))))
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n (b =-> (c =-> (d =-> e)))
forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
 Mergeable (SBVType integerBitWidth b),
 KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy n
p a =-> (b =-> (c =-> (d =-> e)))
f
  symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> e)))) -> Int -> String
symSBVName TypedSymbol (a =-> (b =-> (c =-> (d =-> e))))
_ Int
num = String
"tfunc5" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
num
  symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n
-> String -> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
symSBVTerm (proxy n
p :: proxy n) String
name =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
   Mergeable (SBVType n a), SMTDefinable (SBVType n a),
   Mergeable (SBVType n a),
   SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
forall a b. (a -> b) -> a -> b
$
      forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
   Mergeable (SBVType n b), SMTDefinable (SBVType n b),
   Mergeable (SBVType n b),
   SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
     Mergeable (SBVType n b), SMTDefinable (SBVType n b),
     Mergeable (SBVType n b),
     SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
forall a b. (a -> b) -> a -> b
$
        forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @c proxy n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
   Mergeable (SBVType n c), SMTDefinable (SBVType n c),
   Mergeable (SBVType n c),
   SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
     Mergeable (SBVType n c), SMTDefinable (SBVType n c),
     Mergeable (SBVType n c),
     SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
forall a b. (a -> b) -> a -> b
$
          forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @d proxy n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
   Mergeable (SBVType n d), SMTDefinable (SBVType n d),
   Mergeable (SBVType n d),
   SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
     Mergeable (SBVType n d), SMTDefinable (SBVType n d),
     Mergeable (SBVType n d),
     SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
forall a b. (a -> b) -> a -> b
$
            forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @e proxy n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
   Mergeable (SBVType n e), SMTDefinable (SBVType n e),
   Mergeable (SBVType n e),
   SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
     Mergeable (SBVType n e), SMTDefinable (SBVType n e),
     Mergeable (SBVType n e),
     SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
forall a b. (a -> b) -> a -> b
$
              SBVType n (a =-> (b =-> (c =-> (d =-> e))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVType n (a =-> (b =-> (c =-> (d =-> e))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
forall a b. (a -> b) -> a -> b
$
                String
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
forall a. SMTDefinable a => String -> a
SBV.uninterpret String
name
  withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> e)))),
     SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))),
     Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))),
     Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))) =>
    a)
-> a
withPrim p n
p (PrimConstraint n (a =-> (b =-> (c =-> (d =-> e)))),
 SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))),
 Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))),
 Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))) =>
a
r =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @a p n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
   Mergeable (SBVType n a), SMTDefinable (SBVType n a),
   Mergeable (SBVType n a),
   SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
      forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b p n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
   Mergeable (SBVType n b), SMTDefinable (SBVType n b),
   Mergeable (SBVType n b),
   SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
     Mergeable (SBVType n b), SMTDefinable (SBVType n b),
     Mergeable (SBVType n b),
     SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
        forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @c p n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
   Mergeable (SBVType n c), SMTDefinable (SBVType n c),
   Mergeable (SBVType n c),
   SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
     Mergeable (SBVType n c), SMTDefinable (SBVType n c),
     Mergeable (SBVType n c),
     SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
          forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @d p n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
   Mergeable (SBVType n d), SMTDefinable (SBVType n d),
   Mergeable (SBVType n d),
   SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
     Mergeable (SBVType n d), SMTDefinable (SBVType n d),
     Mergeable (SBVType n d),
     SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
            forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @e p n
p a
(SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
 Mergeable (SBVType n e), SMTDefinable (SBVType n e),
 Mergeable (SBVType n e),
 SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
a
(PrimConstraint n (a =-> (b =-> (c =-> (d =-> e)))),
 SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))),
 Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))),
 Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))) =>
a
r
  sbvIte :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBV Bool
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
sbvIte proxy n
p = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @e proxy n
p (SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
 Mergeable (SBVType n e), SMTDefinable (SBVType n e),
 Mergeable (SBVType n e),
 SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBVType n e)
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBVType n e)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBVType n e
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e))
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e))
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBVType n e)
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBVType n e)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBVType n e
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
  sbvEq :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
-> SBV Bool
sbvEq proxy n
_ SBVType n (a =-> (b =-> (c =-> (d =-> e))))
_ =
    Maybe String
-> TypeRep (a =-> (b =-> (c =-> (d =-> e))))
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBVType n e)
-> SBV Bool
forall a b. HasCallStack => Maybe String -> TypeRep a -> b
translateTypeError
      ( String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
          String
"BUG. Please send a bug report. TabularFun is not supported for "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"equality comparison."
      )
      (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a =-> b =-> c =-> d =-> e))
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> e)))
parseSMTModelResult = Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> e)))
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult

instance
  {-# OVERLAPPING #-}
  ( SupportedNonFuncPrim a,
    SupportedNonFuncPrim b,
    SupportedNonFuncPrim c,
    SupportedNonFuncPrim d,
    SupportedNonFuncPrim e,
    SupportedNonFuncPrim f,
    SupportedPrim a,
    SupportedPrim b,
    SupportedPrim c,
    SupportedPrim d,
    SupportedPrim e,
    SupportedPrim f
  ) =>
  SupportedPrim (a =-> b =-> c =-> d =-> e =-> f)
  where
  defaultValue :: a =-> (b =-> (c =-> (d =-> (e =-> f))))
defaultValue = [(a, b =-> (c =-> (d =-> (e =-> f))))]
-> (b =-> (c =-> (d =-> (e =-> f))))
-> a =-> (b =-> (c =-> (d =-> (e =-> f))))
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] b =-> (c =-> (d =-> (e =-> f)))
forall t. SupportedPrim t => t
defaultValue
  pevalITETerm :: Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
pevalITETerm = Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term Bool
pevalEqTerm = Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
conSBVTerm proxy n
p a =-> (b =-> (c =-> (d =-> (e =-> f))))
f =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @f proxy n
p (((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
   Mergeable (SBVType n f), SMTDefinable (SBVType n f),
   Mergeable (SBVType n f),
   SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
  SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
 -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
-> ((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
     Mergeable (SBVType n f), SMTDefinable (SBVType n f),
     Mergeable (SBVType n f),
     SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
    SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
forall a b. (a -> b) -> a -> b
$
      proxy n
-> (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n (b =-> (c =-> (d =-> (e =-> f))))
forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
 Mergeable (SBVType integerBitWidth b),
 KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy n
p a =-> (b =-> (c =-> (d =-> (e =-> f))))
f
  symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> Int -> String
symSBVName TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
_ Int
num = String
"tfunc6" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
num
  symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n
-> String
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
symSBVTerm (proxy n
p :: proxy n) String
name =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
   Mergeable (SBVType n a), SMTDefinable (SBVType n a),
   Mergeable (SBVType n a),
   SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a b. (a -> b) -> a -> b
$
      forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
   Mergeable (SBVType n b), SMTDefinable (SBVType n b),
   Mergeable (SBVType n b),
   SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
     Mergeable (SBVType n b), SMTDefinable (SBVType n b),
     Mergeable (SBVType n b),
     SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a b. (a -> b) -> a -> b
$
        forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @c proxy n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
   Mergeable (SBVType n c), SMTDefinable (SBVType n c),
   Mergeable (SBVType n c),
   SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
     Mergeable (SBVType n c), SMTDefinable (SBVType n c),
     Mergeable (SBVType n c),
     SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a b. (a -> b) -> a -> b
$
          forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @d proxy n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
   Mergeable (SBVType n d), SMTDefinable (SBVType n d),
   Mergeable (SBVType n d),
   SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
     Mergeable (SBVType n d), SMTDefinable (SBVType n d),
     Mergeable (SBVType n d),
     SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a b. (a -> b) -> a -> b
$
            forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @e proxy n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
   Mergeable (SBVType n e), SMTDefinable (SBVType n e),
   Mergeable (SBVType n e),
   SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
     Mergeable (SBVType n e), SMTDefinable (SBVType n e),
     Mergeable (SBVType n e),
     SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a b. (a -> b) -> a -> b
$
              forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @f proxy n
p (((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
   Mergeable (SBVType n f), SMTDefinable (SBVType n f),
   Mergeable (SBVType n f),
   SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> ((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
     Mergeable (SBVType n f), SMTDefinable (SBVType n f),
     Mergeable (SBVType n f),
     SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a b. (a -> b) -> a -> b
$
                SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a b. (a -> b) -> a -> b
$
                  String
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
forall a. SMTDefinable a => String -> a
SBV.uninterpret String
name
  withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> (e =-> f))))),
     SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))),
     Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))),
     Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))) =>
    a)
-> a
withPrim p n
p (PrimConstraint n (a =-> (b =-> (c =-> (d =-> (e =-> f))))),
 SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))),
 Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))),
 Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))) =>
a
r =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @a p n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
   Mergeable (SBVType n a), SMTDefinable (SBVType n a),
   Mergeable (SBVType n a),
   SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
      forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b p n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
   Mergeable (SBVType n b), SMTDefinable (SBVType n b),
   Mergeable (SBVType n b),
   SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
     Mergeable (SBVType n b), SMTDefinable (SBVType n b),
     Mergeable (SBVType n b),
     SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
        forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @c p n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
   Mergeable (SBVType n c), SMTDefinable (SBVType n c),
   Mergeable (SBVType n c),
   SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
     Mergeable (SBVType n c), SMTDefinable (SBVType n c),
     Mergeable (SBVType n c),
     SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
          forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @d p n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
   Mergeable (SBVType n d), SMTDefinable (SBVType n d),
   Mergeable (SBVType n d),
   SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
     Mergeable (SBVType n d), SMTDefinable (SBVType n d),
     Mergeable (SBVType n d),
     SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
            forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @e p n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
   Mergeable (SBVType n e), SMTDefinable (SBVType n e),
   Mergeable (SBVType n e),
   SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
     Mergeable (SBVType n e), SMTDefinable (SBVType n e),
     Mergeable (SBVType n e),
     SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
              forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @f p n
p a
(SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
 Mergeable (SBVType n f), SMTDefinable (SBVType n f),
 Mergeable (SBVType n f),
 SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
a
(PrimConstraint n (a =-> (b =-> (c =-> (d =-> (e =-> f))))),
 SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))),
 Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))),
 Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))) =>
a
r
  sbvIte :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBV Bool
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
sbvIte proxy n
p = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @f proxy n
p (SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
 Mergeable (SBVType n f), SMTDefinable (SBVType n f),
 Mergeable (SBVType n f),
 SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBVType n f)
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBVType n f)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBVType n f
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f))
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f))
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBVType n f)
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBVType n f)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBVType n f
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
  sbvEq :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> SBV Bool
sbvEq proxy n
_ SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
_ =
    Maybe String
-> TypeRep (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBVType n f)
-> SBV Bool
forall a b. HasCallStack => Maybe String -> TypeRep a -> b
translateTypeError
      ( String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
          String
"BUG. Please send a bug report. TabularFun is not supported for "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"equality comparison."
      )
      (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a =-> b =-> c =-> d =-> e =-> f))
  parseSMTModelResult :: Int
-> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> (e =-> f))))
parseSMTModelResult = Int
-> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> (e =-> f))))
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult

-- 7 arguments
instance
  {-# OVERLAPPING #-}
  ( SupportedNonFuncPrim a,
    SupportedNonFuncPrim b,
    SupportedNonFuncPrim c,
    SupportedNonFuncPrim d,
    SupportedNonFuncPrim e,
    SupportedNonFuncPrim f,
    SupportedNonFuncPrim g,
    SupportedPrim a,
    SupportedPrim b,
    SupportedPrim c,
    SupportedPrim d,
    SupportedPrim e,
    SupportedPrim f,
    SupportedPrim g
  ) =>
  SupportedPrim (a =-> b =-> c =-> d =-> e =-> f =-> g)
  where
  defaultValue :: a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
defaultValue = [(a, b =-> (c =-> (d =-> (e =-> (f =-> g)))))]
-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
-> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] b =-> (c =-> (d =-> (e =-> (f =-> g))))
forall t. SupportedPrim t => t
defaultValue
  pevalITETerm :: Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
pevalITETerm = Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term Bool
pevalEqTerm = Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
conSBVTerm proxy n
p a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
f =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @g proxy n
p (((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
   Mergeable (SBVType n g), SMTDefinable (SBVType n g),
   Mergeable (SBVType n g),
   SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
  SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
 -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
-> ((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
     Mergeable (SBVType n g), SMTDefinable (SBVType n g),
     Mergeable (SBVType n g),
     SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
    SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
forall a b. (a -> b) -> a -> b
$
      proxy n
-> (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
 Mergeable (SBVType integerBitWidth b),
 KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy n
p a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
f
  symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Int -> String
symSBVName TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
_ Int
num = String
"tfunc7" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
num
  symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n
-> String
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
symSBVTerm (proxy n
p :: proxy n) String
name =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
   Mergeable (SBVType n a), SMTDefinable (SBVType n a),
   Mergeable (SBVType n a),
   SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
      forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
   Mergeable (SBVType n b), SMTDefinable (SBVType n b),
   Mergeable (SBVType n b),
   SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
     Mergeable (SBVType n b), SMTDefinable (SBVType n b),
     Mergeable (SBVType n b),
     SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
        forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @c proxy n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
   Mergeable (SBVType n c), SMTDefinable (SBVType n c),
   Mergeable (SBVType n c),
   SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
     Mergeable (SBVType n c), SMTDefinable (SBVType n c),
     Mergeable (SBVType n c),
     SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
          forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @d proxy n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
   Mergeable (SBVType n d), SMTDefinable (SBVType n d),
   Mergeable (SBVType n d),
   SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
     Mergeable (SBVType n d), SMTDefinable (SBVType n d),
     Mergeable (SBVType n d),
     SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
            forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @e proxy n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
   Mergeable (SBVType n e), SMTDefinable (SBVType n e),
   Mergeable (SBVType n e),
   SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
     Mergeable (SBVType n e), SMTDefinable (SBVType n e),
     Mergeable (SBVType n e),
     SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
              forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @f proxy n
p (((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
   Mergeable (SBVType n f), SMTDefinable (SBVType n f),
   Mergeable (SBVType n f),
   SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> ((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
     Mergeable (SBVType n f), SMTDefinable (SBVType n f),
     Mergeable (SBVType n f),
     SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
                forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @g proxy n
p (((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
   Mergeable (SBVType n g), SMTDefinable (SBVType n g),
   Mergeable (SBVType n g),
   SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
  m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> ((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
     Mergeable (SBVType n g), SMTDefinable (SBVType n g),
     Mergeable (SBVType n g),
     SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
    m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
                  SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
 -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
                    String
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
forall a. SMTDefinable a => String -> a
SBV.uninterpret String
name
  withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint
       n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))),
     SMTDefinable
       (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))),
     Mergeable
       (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))),
     Typeable
       (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))) =>
    a)
-> a
withPrim p n
p (PrimConstraint
   n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))),
 SMTDefinable
   (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))),
 Mergeable
   (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))),
 Typeable
   (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))) =>
a
r =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @a p n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
   Mergeable (SBVType n a), SMTDefinable (SBVType n a),
   Mergeable (SBVType n a),
   SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
      forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b p n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
   Mergeable (SBVType n b), SMTDefinable (SBVType n b),
   Mergeable (SBVType n b),
   SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
     Mergeable (SBVType n b), SMTDefinable (SBVType n b),
     Mergeable (SBVType n b),
     SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
        forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @c p n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
   Mergeable (SBVType n c), SMTDefinable (SBVType n c),
   Mergeable (SBVType n c),
   SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
     Mergeable (SBVType n c), SMTDefinable (SBVType n c),
     Mergeable (SBVType n c),
     SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
          forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @d p n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
   Mergeable (SBVType n d), SMTDefinable (SBVType n d),
   Mergeable (SBVType n d),
   SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
     Mergeable (SBVType n d), SMTDefinable (SBVType n d),
     Mergeable (SBVType n d),
     SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
            forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @e p n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
   Mergeable (SBVType n e), SMTDefinable (SBVType n e),
   Mergeable (SBVType n e),
   SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
     Mergeable (SBVType n e), SMTDefinable (SBVType n e),
     Mergeable (SBVType n e),
     SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
              forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @f p n
p (((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
   Mergeable (SBVType n f), SMTDefinable (SBVType n f),
   Mergeable (SBVType n f),
   SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
     Mergeable (SBVType n f), SMTDefinable (SBVType n f),
     Mergeable (SBVType n f),
     SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
                forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @g p n
p a
(SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
 Mergeable (SBVType n g), SMTDefinable (SBVType n g),
 Mergeable (SBVType n g),
 SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
a
(PrimConstraint
   n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))),
 SMTDefinable
   (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))),
 Mergeable
   (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))),
 Typeable
   (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))) =>
a
r
  sbvIte :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBV Bool
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
sbvIte proxy n
p = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @g proxy n
p (SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
 Mergeable (SBVType n g), SMTDefinable (SBVType n g),
 Mergeable (SBVType n g),
 SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f)
    -> SBVType n g)
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f)
    -> SBVType n g)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBVType n g
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f)
    -> SBV (NonFuncSBVBaseType n g))
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f)
    -> SBV (NonFuncSBVBaseType n g))
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f)
    -> SBVType n g)
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f)
    -> SBVType n g)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBVType n g
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
  sbvEq :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> SBV Bool
sbvEq proxy n
_ SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
_ =
    Maybe String
-> TypeRep (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f)
    -> SBVType n g)
-> SBV Bool
forall a b. HasCallStack => Maybe String -> TypeRep a -> b
translateTypeError
      ( String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
          String
"BUG. Please send a bug report. TabularFun is not supported for "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"equality comparison."
      )
      (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a =-> b =-> c =-> d =-> e =-> f =-> g))
  parseSMTModelResult :: Int
-> ([([CV], CV)], CV)
-> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
parseSMTModelResult = Int
-> ([([CV], CV)], CV)
-> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult

-- 8 arguments
instance
  {-# OVERLAPPING #-}
  ( SupportedNonFuncPrim a,
    SupportedNonFuncPrim b,
    SupportedNonFuncPrim c,
    SupportedNonFuncPrim d,
    SupportedNonFuncPrim e,
    SupportedNonFuncPrim f,
    SupportedNonFuncPrim g,
    SupportedNonFuncPrim h,
    SupportedPrim a,
    SupportedPrim b,
    SupportedPrim c,
    SupportedPrim d,
    SupportedPrim e,
    SupportedPrim f,
    SupportedPrim g,
    SupportedPrim h
  ) =>
  SupportedPrim (a =-> b =-> c =-> d =-> e =-> f =-> g =-> h)
  where
  defaultValue :: a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
defaultValue = [(a, b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))]
-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
-> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))
forall t. SupportedPrim t => t
defaultValue
  pevalITETerm :: Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
pevalITETerm = Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term Bool
pevalEqTerm = Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> SBVType
     n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
conSBVTerm proxy n
p a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
f =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @h proxy n
p (((SymVal (NonFuncSBVBaseType n h), EqSymbolic (SBVType n h),
   Mergeable (SBVType n h), SMTDefinable (SBVType n h),
   Mergeable (SBVType n h),
   SBVType n h ~ SBV (NonFuncSBVBaseType n h), PrimConstraint n h) =>
  SBVType
    n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
 -> SBVType
      n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
-> ((SymVal (NonFuncSBVBaseType n h), EqSymbolic (SBVType n h),
     Mergeable (SBVType n h), SMTDefinable (SBVType n h),
     Mergeable (SBVType n h),
     SBVType n h ~ SBV (NonFuncSBVBaseType n h), PrimConstraint n h) =>
    SBVType
      n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
-> SBVType
     n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
forall a b. (a -> b) -> a -> b
$
      proxy n
-> (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
 Mergeable (SBVType integerBitWidth b),
 KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy n
p a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
f
  symSBVName :: TypedSymbol
  (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Int -> String
symSBVName TypedSymbol
  (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
_ Int
num = String
"tfunc8" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
num
  symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n
-> String
-> m (SBVType
        n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
symSBVTerm (proxy n
p :: proxy n) String
name =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
   Mergeable (SBVType n a), SMTDefinable (SBVType n a),
   Mergeable (SBVType n a),
   SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
  m (SBVType
       n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
 -> m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
        n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
      forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
   Mergeable (SBVType n b), SMTDefinable (SBVType n b),
   Mergeable (SBVType n b),
   SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
  m (SBVType
       n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
 -> m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
     Mergeable (SBVType n b), SMTDefinable (SBVType n b),
     Mergeable (SBVType n b),
     SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
    m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
        n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
        forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @c proxy n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
   Mergeable (SBVType n c), SMTDefinable (SBVType n c),
   Mergeable (SBVType n c),
   SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
  m (SBVType
       n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
 -> m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
     Mergeable (SBVType n c), SMTDefinable (SBVType n c),
     Mergeable (SBVType n c),
     SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
    m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
        n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
          forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @d proxy n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
   Mergeable (SBVType n d), SMTDefinable (SBVType n d),
   Mergeable (SBVType n d),
   SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
  m (SBVType
       n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
 -> m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
     Mergeable (SBVType n d), SMTDefinable (SBVType n d),
     Mergeable (SBVType n d),
     SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
    m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
        n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
            forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @e proxy n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
   Mergeable (SBVType n e), SMTDefinable (SBVType n e),
   Mergeable (SBVType n e),
   SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
  m (SBVType
       n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
 -> m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
     Mergeable (SBVType n e), SMTDefinable (SBVType n e),
     Mergeable (SBVType n e),
     SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
    m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
        n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
              forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @f proxy n
p (((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
   Mergeable (SBVType n f), SMTDefinable (SBVType n f),
   Mergeable (SBVType n f),
   SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
  m (SBVType
       n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
 -> m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
     Mergeable (SBVType n f), SMTDefinable (SBVType n f),
     Mergeable (SBVType n f),
     SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
    m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
        n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
                forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @g proxy n
p (((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
   Mergeable (SBVType n g), SMTDefinable (SBVType n g),
   Mergeable (SBVType n g),
   SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
  m (SBVType
       n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
 -> m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
     Mergeable (SBVType n g), SMTDefinable (SBVType n g),
     Mergeable (SBVType n g),
     SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
    m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
        n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
                  forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @h proxy n
p (((SymVal (NonFuncSBVBaseType n h), EqSymbolic (SBVType n h),
   Mergeable (SBVType n h), SMTDefinable (SBVType n h),
   Mergeable (SBVType n h),
   SBVType n h ~ SBV (NonFuncSBVBaseType n h), PrimConstraint n h) =>
  m (SBVType
       n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
 -> m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n h), EqSymbolic (SBVType n h),
     Mergeable (SBVType n h), SMTDefinable (SBVType n h),
     Mergeable (SBVType n h),
     SBVType n h ~ SBV (NonFuncSBVBaseType n h), PrimConstraint n h) =>
    m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
        n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
                    SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> m (SBVType
        n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVType
   n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
 -> m (SBVType
         n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> SBVType
     n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> m (SBVType
        n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
                      String
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
-> SBV (NonFuncSBVBaseType n h)
forall a. SMTDefinable a => String -> a
SBV.uninterpret String
name
  withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint
       n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))),
     SMTDefinable
       (SBVType
          n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))),
     Mergeable
       (SBVType
          n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))),
     Typeable
       (SBVType
          n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))) =>
    a)
-> a
withPrim p n
p (PrimConstraint
   n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))),
 SMTDefinable
   (SBVType
      n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))),
 Mergeable
   (SBVType
      n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))),
 Typeable
   (SBVType
      n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))) =>
a
r =
    forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @a p n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
   Mergeable (SBVType n a), SMTDefinable (SBVType n a),
   Mergeable (SBVType n a),
   SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
      forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @b p n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
   Mergeable (SBVType n b), SMTDefinable (SBVType n b),
   Mergeable (SBVType n b),
   SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
     Mergeable (SBVType n b), SMTDefinable (SBVType n b),
     Mergeable (SBVType n b),
     SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
        forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @c p n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
   Mergeable (SBVType n c), SMTDefinable (SBVType n c),
   Mergeable (SBVType n c),
   SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
     Mergeable (SBVType n c), SMTDefinable (SBVType n c),
     Mergeable (SBVType n c),
     SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
          forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @d p n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
   Mergeable (SBVType n d), SMTDefinable (SBVType n d),
   Mergeable (SBVType n d),
   SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
     Mergeable (SBVType n d), SMTDefinable (SBVType n d),
     Mergeable (SBVType n d),
     SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
            forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @e p n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
   Mergeable (SBVType n e), SMTDefinable (SBVType n e),
   Mergeable (SBVType n e),
   SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
     Mergeable (SBVType n e), SMTDefinable (SBVType n e),
     Mergeable (SBVType n e),
     SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
              forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @f p n
p (((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
   Mergeable (SBVType n f), SMTDefinable (SBVType n f),
   Mergeable (SBVType n f),
   SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
     Mergeable (SBVType n f), SMTDefinable (SBVType n f),
     Mergeable (SBVType n f),
     SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
                forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @g p n
p (((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
   Mergeable (SBVType n g), SMTDefinable (SBVType n g),
   Mergeable (SBVType n g),
   SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
  a)
 -> a)
-> ((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
     Mergeable (SBVType n g), SMTDefinable (SBVType n g),
     Mergeable (SBVType n g),
     SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
                  forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @h p n
p a
(SymVal (NonFuncSBVBaseType n h), EqSymbolic (SBVType n h),
 Mergeable (SBVType n h), SMTDefinable (SBVType n h),
 Mergeable (SBVType n h),
 SBVType n h ~ SBV (NonFuncSBVBaseType n h), PrimConstraint n h) =>
a
(PrimConstraint
   n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))),
 SMTDefinable
   (SBVType
      n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))),
 Mergeable
   (SBVType
      n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))),
 Typeable
   (SBVType
      n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))) =>
a
r
  sbvIte :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBV Bool
-> SBVType
     n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> SBVType
     n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> SBVType
     n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
sbvIte proxy n
p = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @h proxy n
p (SymVal (NonFuncSBVBaseType n h), EqSymbolic (SBVType n h),
 Mergeable (SBVType n h), SMTDefinable (SBVType n h),
 Mergeable (SBVType n h),
 SBVType n h ~ SBV (NonFuncSBVBaseType n h), PrimConstraint n h) =>
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f)
    -> SBV (NonFuncSBVBaseType n g)
    -> SBVType n h)
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f)
    -> SBV (NonFuncSBVBaseType n g)
    -> SBVType n h)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
-> SBVType n h
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f)
    -> SBV (NonFuncSBVBaseType n g)
    -> SBV (NonFuncSBVBaseType n h))
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f)
    -> SBV (NonFuncSBVBaseType n g)
    -> SBV (NonFuncSBVBaseType n h))
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
-> SBV (NonFuncSBVBaseType n h)
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f)
    -> SBV (NonFuncSBVBaseType n g)
    -> SBVType n h)
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f)
    -> SBV (NonFuncSBVBaseType n g)
    -> SBVType n h)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
-> SBVType n h
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
  sbvEq :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBVType
     n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> SBVType
     n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> SBV Bool
sbvEq proxy n
_ SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
_ =
    Maybe String
-> TypeRep
     (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> (SBV (NonFuncSBVBaseType n a)
    -> SBV (NonFuncSBVBaseType n b)
    -> SBV (NonFuncSBVBaseType n c)
    -> SBV (NonFuncSBVBaseType n d)
    -> SBV (NonFuncSBVBaseType n e)
    -> SBV (NonFuncSBVBaseType n f)
    -> SBV (NonFuncSBVBaseType n g)
    -> SBVType n h)
-> SBV Bool
forall a b. HasCallStack => Maybe String -> TypeRep a -> b
translateTypeError
      ( String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
          String
"BUG. Please send a bug report. TabularFun is not supported for "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"equality comparison."
      )
      (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a =-> b =-> c =-> d =-> e =-> f =-> g =-> h))
  parseSMTModelResult :: Int
-> ([([CV], CV)], CV)
-> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
parseSMTModelResult = Int
-> ([([CV], CV)], CV)
-> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult

instance
  (SupportedPrim a, SupportedPrim b, SupportedPrim (a =-> b)) =>
  PEvalApplyTerm (a =-> b) a b
  where
  pevalApplyTerm :: Term (a =-> b) -> Term a -> Term b
pevalApplyTerm = (Term (a =-> b) -> PartialFun (Term a) (Term b))
-> (Term (a =-> b) -> Term a -> Term b)
-> Term (a =-> b)
-> Term a
-> Term b
forall a b c. (a -> PartialFun b c) -> (a -> b -> c) -> a -> b -> c
totalize2 Term (a =-> b) -> PartialFun (Term a) (Term b)
(SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> PartialFun (Term a) (Term b)
doPevalApplyTerm Term (a =-> b) -> Term a -> Term b
forall a b f.
(SupportedPrim a, SupportedPrim b, SupportedPrim f,
 PEvalApplyTerm f a b) =>
Term f -> Term a -> Term b
applyTerm
    where
      doPevalApplyTerm ::
        (SupportedPrim a, SupportedPrim b) =>
        Term (a =-> b) ->
        Term a ->
        Maybe (Term b)
      doPevalApplyTerm :: (SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> PartialFun (Term a) (Term b)
doPevalApplyTerm (ConTerm Int
_ a =-> b
f) (ConTerm Int
_ a
a) = Term b -> Maybe (Term b)
forall a. a -> Maybe a
Just (Term b -> Maybe (Term b)) -> Term b -> Maybe (Term b)
forall a b. (a -> b) -> a -> b
$ b -> Term b
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (b -> Term b) -> b -> Term b
forall a b. (a -> b) -> a -> b
$ a =-> b
f (a =-> b) -> a -> b
forall f arg ret. Function f arg ret => f -> arg -> ret
# a
a
      doPevalApplyTerm (ConTerm Int
_ (TabularFun [(a, b)]
f b
d)) Term a
a = Term b -> Maybe (Term b)
forall a. a -> Maybe a
Just (Term b -> Maybe (Term b)) -> Term b -> Maybe (Term b)
forall a b. (a -> b) -> a -> b
$ [(a, b)] -> Term b
go [(a, b)]
f
        where
          go :: [(a, b)] -> Term b
go [] = b -> Term b
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm b
d
          go ((a
x, b
y) : [(a, b)]
xs) =
            Term Bool -> Term b -> Term b -> Term b
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm (Term a -> Term a -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqTerm Term a
a (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
x)) (b -> Term b
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm b
y) ([(a, b)] -> Term b
go [(a, b)]
xs)
      doPevalApplyTerm Term (a =-> b)
_ Term a
_ = Maybe (Term b)
forall a. Maybe a
Nothing
  sbvApplyTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> SBVType n (a =-> b) -> SBVType n a -> SBVType n b
sbvApplyTerm proxy n
p SBVType n (a =-> b)
f SBVType n a
a =
    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 @(a =-> b) proxy n
p (((PrimConstraint n (a =-> b), SMTDefinable (SBVType n (a =-> b)),
   Mergeable (SBVType n (a =-> b)), Typeable (SBVType n (a =-> b))) =>
  SBVType n b)
 -> SBVType n b)
-> ((PrimConstraint n (a =-> b),
     SMTDefinable (SBVType n (a =-> b)),
     Mergeable (SBVType n (a =-> b)), Typeable (SBVType n (a =-> b))) =>
    SBVType n b)
-> SBVType n b
forall a b. (a -> b) -> a -> b
$ forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
   Mergeable (SBVType n a), SMTDefinable (SBVType n a),
   Mergeable (SBVType n a),
   SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
  SBVType n b)
 -> SBVType n b)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    SBVType n b)
-> SBVType n b
forall a b. (a -> b) -> a -> b
$ SBVType n (a =-> b)
SBV (NonFuncSBVBaseType n a) -> SBVType n b
f SBV (NonFuncSBVBaseType n a)
SBVType n a
a

lowerTFunCon ::
  forall proxy integerBitWidth a b.
  ( SupportedNonFuncPrim a,
    SupportedPrim b,
    SBV.Mergeable (SBVType integerBitWidth b),
    KnownIsZero integerBitWidth
  ) =>
  proxy integerBitWidth ->
  (a =-> b) ->
  ( SBV.SBV (NonFuncSBVBaseType integerBitWidth a) ->
    SBVType integerBitWidth b
  )
lowerTFunCon :: forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
 Mergeable (SBVType integerBitWidth b),
 KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy integerBitWidth
proxy (TabularFun [(a, b)]
l b
d) = [(a, b)]
-> b
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
go [(a, b)]
l b
d
  where
    go :: [(a, b)]
-> b
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
go [] b
d SBV (NonFuncSBVBaseType integerBitWidth a)
_ = proxy integerBitWidth -> b -> SBVType integerBitWidth b
forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> b -> SBVType n b
forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm proxy integerBitWidth
proxy b
d
    go ((a
x, b
r) : [(a, b)]
xs) b
d SBV (NonFuncSBVBaseType integerBitWidth a)
v =
      SBV Bool
-> SBVType integerBitWidth b
-> SBVType integerBitWidth b
-> SBVType integerBitWidth b
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
        (proxy integerBitWidth
-> a -> SBV (NonFuncSBVBaseType integerBitWidth a)
forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> a -> SBV (NonFuncSBVBaseType n a)
forall a (n :: Nat) (proxy :: Nat -> *).
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n -> a -> SBV (NonFuncSBVBaseType n a)
conNonFuncSBVTerm proxy integerBitWidth
proxy a
x SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBV (NonFuncSBVBaseType integerBitWidth a) -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
SBV..== SBV (NonFuncSBVBaseType integerBitWidth a)
v)
        (proxy integerBitWidth -> b -> SBVType integerBitWidth b
forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> b -> SBVType n b
forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm proxy integerBitWidth
proxy b
r)
        ([(a, b)]
-> b
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
go [(a, b)]
xs b
d SBV (NonFuncSBVBaseType integerBitWidth a)
v)