{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

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

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

import Control.DeepSeq (NFData (rnf))
import Data.Bifunctor (Bifunctor (second))
import Data.Foldable (Foldable (foldl'))
import Data.Hashable (Hashable (hashWithSalt))
import qualified Data.SBV as SBV
import qualified Data.SBV.Dynamic as SBVD
import GHC.Generics (Generic)
import Grisette.Internal.Core.Data.Class.Function (Function ((#)))
import Grisette.Internal.Core.Data.MemoUtils (htmemo)
import Grisette.Internal.Core.Data.Symbol
  ( Symbol (IndexedSymbol, SimpleSymbol),
    withInfo,
  )
import Grisette.Internal.SymPrim.Prim.Internal.PartialEval (totalize2)
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( SBVRep,
    SupportedPrim (parseSMTModelResult, sbvEq),
    partitionCVArg,
  )
import Grisette.Internal.SymPrim.Prim.SomeTerm (SomeTerm (SomeTerm))
import Grisette.Internal.SymPrim.Prim.Term
  ( BinaryOp (pevalBinary),
    LinkedRep (underlyingTerm, wrapTerm),
    NonFuncSBVBaseType,
    PEvalApplyTerm (pevalApplyTerm, sbvApplyTerm),
    PEvalBVSignConversionTerm (pevalBVToSignedTerm, pevalBVToUnsignedTerm),
    PEvalBVTerm (pevalBVConcatTerm, pevalBVExtendTerm, pevalBVSelectTerm),
    PEvalBitwiseTerm
      ( pevalAndBitsTerm,
        pevalComplementBitsTerm,
        pevalOrBitsTerm,
        pevalXorBitsTerm
      ),
    PEvalDivModIntegralTerm
      ( pevalDivIntegralTerm,
        pevalModIntegralTerm
      ),
    PEvalNumTerm
      ( pevalAbsNumTerm,
        pevalAddNumTerm,
        pevalMulNumTerm,
        pevalNegNumTerm,
        pevalSignumNumTerm
      ),
    PEvalOrdTerm (pevalLeOrdTerm, pevalLtOrdTerm),
    PEvalRotateTerm (pevalRotateRightTerm),
    PEvalShiftTerm (pevalShiftLeftTerm, pevalShiftRightTerm),
    SBVType,
    SupportedNonFuncPrim (withNonFuncPrim),
    SupportedPrim
      ( conSBVTerm,
        defaultValue,
        pevalITETerm,
        symSBVName,
        symSBVTerm,
        withPrim
      ),
    SupportedPrimConstraint (PrimConstraint),
    Term
      ( AbsNumTerm,
        AddNumTerm,
        AndBitsTerm,
        AndTerm,
        ApplyTerm,
        BVConcatTerm,
        BVExtendTerm,
        BVSelectTerm,
        BinaryTerm,
        ComplementBitsTerm,
        ConTerm,
        DivIntegralTerm,
        EqTerm,
        ITETerm,
        LeOrdTerm,
        LtOrdTerm,
        ModIntegralTerm,
        MulNumTerm,
        NegNumTerm,
        NotTerm,
        OrBitsTerm,
        OrTerm,
        QuotIntegralTerm,
        RemIntegralTerm,
        RotateLeftTerm,
        RotateRightTerm,
        ShiftLeftTerm,
        ShiftRightTerm,
        SignumNumTerm,
        SymTerm,
        TernaryTerm,
        ToSignedTerm,
        ToUnsignedTerm,
        UnaryTerm,
        XorBitsTerm
      ),
    TernaryOp (pevalTernary),
    TypedSymbol (TypedSymbol, unTypedSymbol),
    UnaryOp (pevalUnary),
    applyTerm,
    conTerm,
    pevalAndTerm,
    pevalDefaultEqTerm,
    pevalEqTerm,
    pevalITEBasicTerm,
    pevalNotTerm,
    pevalOrTerm,
    pevalQuotIntegralTerm,
    pevalRemIntegralTerm,
    pevalRotateLeftTerm,
    pformat,
    someTypedSymbol,
    symTerm,
    translateTypeError,
  )
import Language.Haskell.TH.Syntax (Lift (liftTyped))
import Type.Reflection
  ( TypeRep,
    eqTypeRep,
    typeRep,
    pattern App,
    type (:~~:) (HRefl),
  )
import Unsafe.Coerce (unsafeCoerce)

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

-- | General symbolic function type. Use the '#' operator to apply the function.
-- Note that this function should be applied to symbolic values only. It is by
-- itself already a symbolic value, but can be considered partially concrete
-- as the function body is specified. Use 'Grisette.SymPrim.SymPrim.-~>'
-- for uninterpreted general symbolic functions.
--
-- The result would be partially evaluated.
--
-- >>> :set -XOverloadedStrings
-- >>> :set -XTypeOperators
-- >>> let f = ("x" :: TypedSymbol Integer) --> ("x" + 1 + "y" :: SymInteger) :: Integer --> Integer
-- >>> f # 1    -- 1 has the type SymInteger
-- (+ 2 y)
-- >>> f # "a"  -- "a" has the type SymInteger
-- (+ 1 (+ a y))
data (-->) a b where
  GeneralFun ::
    (SupportedPrim a, SupportedPrim b) =>
    TypedSymbol a ->
    Term b ->
    a --> b

instance (LinkedRep a sa, LinkedRep b sb) => Function (a --> b) sa sb where
  (GeneralFun TypedSymbol a
s Term b
t) # :: (a --> b) -> sa -> sb
# sa
x = Term b -> sb
forall con sym. LinkedRep con sym => Term con -> sym
wrapTerm (Term b -> sb) -> Term b -> sb
forall a b. (a -> b) -> a -> b
$ TypedSymbol a -> Term a -> Term b -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
s (sa -> Term a
forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm sa
x) Term b
t

infixr 0 -->

buildGeneralFun ::
  (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b
buildGeneralFun :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun TypedSymbol a
arg Term b
v =
  TypedSymbol a -> Term b -> a --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun
    (Symbol -> TypedSymbol a
forall t. SupportedPrim t => Symbol -> TypedSymbol t
TypedSymbol Symbol
newarg)
    (TypedSymbol a -> Term a -> Term b -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
arg (Symbol -> Term a
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm Symbol
newarg) Term b
v)
  where
    newarg :: Symbol
newarg = case TypedSymbol a -> Symbol
forall t. TypedSymbol t -> Symbol
unTypedSymbol TypedSymbol a
arg of
      SimpleSymbol Identifier
s -> Identifier -> Symbol
SimpleSymbol (Identifier -> ARG -> Identifier
forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Identifier -> a -> Identifier
withInfo Identifier
s ARG
ARG)
      IndexedSymbol Identifier
s Int
i -> Identifier -> Int -> Symbol
IndexedSymbol (Identifier -> ARG -> Identifier
forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Identifier -> a -> Identifier
withInfo Identifier
s ARG
ARG) Int
i

data ARG = ARG
  deriving (ARG -> ARG -> Bool
(ARG -> ARG -> Bool) -> (ARG -> ARG -> Bool) -> Eq ARG
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ARG -> ARG -> Bool
== :: ARG -> ARG -> Bool
$c/= :: ARG -> ARG -> Bool
/= :: ARG -> ARG -> Bool
Eq, Eq ARG
Eq ARG =>
(ARG -> ARG -> Ordering)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> ARG)
-> (ARG -> ARG -> ARG)
-> Ord ARG
ARG -> ARG -> Bool
ARG -> ARG -> Ordering
ARG -> ARG -> ARG
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ARG -> ARG -> Ordering
compare :: ARG -> ARG -> Ordering
$c< :: ARG -> ARG -> Bool
< :: ARG -> ARG -> Bool
$c<= :: ARG -> ARG -> Bool
<= :: ARG -> ARG -> Bool
$c> :: ARG -> ARG -> Bool
> :: ARG -> ARG -> Bool
$c>= :: ARG -> ARG -> Bool
>= :: ARG -> ARG -> Bool
$cmax :: ARG -> ARG -> ARG
max :: ARG -> ARG -> ARG
$cmin :: ARG -> ARG -> ARG
min :: ARG -> ARG -> ARG
Ord, (forall (m :: * -> *). Quote m => ARG -> m Exp)
-> (forall (m :: * -> *). Quote m => ARG -> Code m ARG) -> Lift ARG
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => ARG -> m Exp
forall (m :: * -> *). Quote m => ARG -> Code m ARG
$clift :: forall (m :: * -> *). Quote m => ARG -> m Exp
lift :: forall (m :: * -> *). Quote m => ARG -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
liftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
Lift, Int -> ARG -> ShowS
[ARG] -> ShowS
ARG -> String
(Int -> ARG -> ShowS)
-> (ARG -> String) -> ([ARG] -> ShowS) -> Show ARG
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ARG -> ShowS
showsPrec :: Int -> ARG -> ShowS
$cshow :: ARG -> String
show :: ARG -> String
$cshowList :: [ARG] -> ShowS
showList :: [ARG] -> ShowS
Show, (forall x. ARG -> Rep ARG x)
-> (forall x. Rep ARG x -> ARG) -> Generic ARG
forall x. Rep ARG x -> ARG
forall x. ARG -> Rep ARG x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ARG -> Rep ARG x
from :: forall x. ARG -> Rep ARG x
$cto :: forall x. Rep ARG x -> ARG
to :: forall x. Rep ARG x -> ARG
Generic)

instance NFData ARG where
  rnf :: ARG -> ()
rnf ARG
ARG = ()

instance Hashable ARG where
  hashWithSalt :: Int -> ARG -> Int
hashWithSalt Int
s ARG
ARG = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int)

instance Eq (a --> b) where
  GeneralFun TypedSymbol a
sym1 Term b
tm1 == :: (a --> b) -> (a --> b) -> Bool
== GeneralFun TypedSymbol a
sym2 Term b
tm2 = TypedSymbol a
sym1 TypedSymbol a -> TypedSymbol a -> Bool
forall a. Eq a => a -> a -> Bool
== TypedSymbol a
sym2 Bool -> Bool -> Bool
&& Term b
tm1 Term b -> Term b -> Bool
forall a. Eq a => a -> a -> Bool
== Term b
tm2

instance Show (a --> b) where
  show :: (a --> b) -> String
show (GeneralFun TypedSymbol a
sym Term b
tm) = String
"\\(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypedSymbol a -> String
forall a. Show a => a -> String
show TypedSymbol a
sym String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term b -> String
forall t. SupportedPrim t => Term t -> String
pformat Term b
tm

instance Lift (a --> b) where
  liftTyped :: forall (m :: * -> *). Quote m => (a --> b) -> Code m (a --> b)
liftTyped (GeneralFun TypedSymbol a
sym Term b
tm) = [||TypedSymbol a -> Term b -> a --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol a
sym Term b
tm||]

instance Hashable (a --> b) where
  Int
s hashWithSalt :: Int -> (a --> b) -> Int
`hashWithSalt` (GeneralFun TypedSymbol a
sym Term b
tm) = Int
s Int -> TypedSymbol a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol a
sym Int -> Term b -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Term b
tm

instance NFData (a --> b) where
  rnf :: (a --> b) -> ()
rnf (GeneralFun TypedSymbol a
sym Term b
tm) = TypedSymbol a -> ()
forall a. NFData a => a -> ()
rnf TypedSymbol a
sym () -> () -> ()
forall a b. a -> b -> b
`seq` Term b -> ()
forall a. NFData a => a -> ()
rnf Term b
tm

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

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

parseGeneralFunSMTModelResult ::
  forall a b.
  (SupportedNonFuncPrim a, SupportedPrim b) =>
  Int ->
  ([([SBVD.CV], SBVD.CV)], SBVD.CV) ->
  a --> b
parseGeneralFunSMTModelResult :: forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a --> b
parseGeneralFunSMTModelResult Int
level ([([CV], CV)]
l, CV
s) =
  let sym :: Symbol
sym = Identifier -> Int -> Symbol
IndexedSymbol Identifier
"arg" Int
level
      funs :: [(a, b)]
funs =
        ([([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
      def :: b
def = 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)
      body :: Term b
body =
        (Term b -> (a, b) -> Term b) -> Term b -> [(a, b)] -> Term b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
          ( \Term b
acc (a
v, b
f) ->
              Term Bool -> Term b -> Term b -> Term b
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm
                (Term a -> Term a -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm (Symbol -> Term a
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm Symbol
sym) (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
v))
                (b -> Term b
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm b
f)
                Term b
acc
          )
          (b -> Term b
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm b
def)
          [(a, b)]
funs
   in TypedSymbol a -> Term b -> a --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun (Symbol -> TypedSymbol a
forall t. SupportedPrim t => Symbol -> TypedSymbol t
TypedSymbol Symbol
sym) Term b
body

instance
  (SupportedNonFuncPrim a, SupportedNonFuncPrim b) =>
  SupportedPrim (a --> b)
  where
  defaultValue :: a --> b
defaultValue = TypedSymbol a -> Term b -> a --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun (Symbol -> TypedSymbol a
forall t. SupportedPrim t => Symbol -> TypedSymbol t
TypedSymbol Symbol
"a") (b -> Term b
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm 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 t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITEBasicTerm
  pevalEqTerm :: Term (a --> b) -> Term (a --> b) -> Term Bool
pevalEqTerm = Term (a --> b) -> Term (a --> b) -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalDefaultEqTerm
  conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> (a --> b) -> SBVType n (a --> b)
conSBVTerm proxy n
_ a --> b
_ =
    Maybe String
-> TypeRep (a --> b) -> SBV (NonFuncSBVBaseType n a) -> SBVType n b
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. GeneralFun must have already been "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"partial evaluated away before reaching this point."
      )
      (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a --> b))
  symSBVName :: TypedSymbol (a --> b) -> Int -> String
symSBVName TypedSymbol (a --> b)
_ Int
num = String
"gfunc2_" 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
  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. GeneralFun 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
parseGeneralFunSMTModelResult

instance
  {-# OVERLAPPING #-}
  ( SupportedNonFuncPrim a,
    SupportedNonFuncPrim b,
    SupportedNonFuncPrim c,
    SupportedPrim a,
    SupportedPrim b,
    SupportedPrim c
  ) =>
  SupportedPrim (a --> b --> c)
  where
  defaultValue :: a --> (b --> c)
defaultValue = TypedSymbol a -> Term (b --> c) -> a --> (b --> c)
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun (Symbol -> TypedSymbol a
forall t. SupportedPrim t => Symbol -> TypedSymbol t
TypedSymbol Symbol
"a") ((b --> c) -> Term (b --> c)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm 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 t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITEBasicTerm
  pevalEqTerm :: Term (a --> (b --> c)) -> Term (a --> (b --> c)) -> Term Bool
pevalEqTerm = Term (a --> (b --> c)) -> Term (a --> (b --> c)) -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalDefaultEqTerm
  conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> (a --> (b --> c)) -> SBVType n (a --> (b --> c))
conSBVTerm proxy n
_ a --> (b --> c)
_ =
    Maybe String
-> TypeRep (a --> (b --> c))
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBVType n c
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. GeneralFun must have already been "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"partial evaluated away before reaching this point."
      )
      (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a --> b --> c))
  symSBVName :: TypedSymbol (a --> (b --> c)) -> Int -> String
symSBVName TypedSymbol (a --> (b --> c))
_ Int
num = String
"gfunc3_" 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
  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. GeneralFun 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
parseGeneralFunSMTModelResult

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 = TypedSymbol a -> Term (b --> (c --> d)) -> a --> (b --> (c --> d))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun (Symbol -> TypedSymbol a
forall t. SupportedPrim t => Symbol -> TypedSymbol t
TypedSymbol Symbol
"a") ((b --> (c --> d)) -> Term (b --> (c --> d))
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm 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 t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
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 t. SupportedPrim t => Term t -> Term t -> 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
_ 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
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. GeneralFun must have already been "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"partial evaluated away before reaching this point."
      )
      (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a --> b --> c --> d))
  symSBVName :: TypedSymbol (a --> (b --> (c --> d))) -> Int -> String
symSBVName TypedSymbol (a --> (b --> (c --> d)))
_ Int
num = String
"gfunc4_" 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
  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. GeneralFun 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
parseGeneralFunSMTModelResult

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 = TypedSymbol a
-> Term (b --> (c --> (d --> e)))
-> a --> (b --> (c --> (d --> e)))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun (Symbol -> TypedSymbol a
forall t. SupportedPrim t => Symbol -> TypedSymbol t
TypedSymbol Symbol
"a") ((b --> (c --> (d --> e))) -> Term (b --> (c --> (d --> e)))
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm 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 t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
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 t. SupportedPrim t => Term t -> Term t -> 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
_ 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
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. GeneralFun must have already been "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"partial evaluated away before reaching this point."
      )
      (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a --> b --> c --> d --> e))
  symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> e)))) -> Int -> String
symSBVName TypedSymbol (a --> (b --> (c --> (d --> e))))
_ Int
num = String
"gfunc5_" 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
  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. GeneralFun 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
parseGeneralFunSMTModelResult

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 = TypedSymbol a
-> Term (b --> (c --> (d --> (e --> f))))
-> a --> (b --> (c --> (d --> (e --> f))))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun (Symbol -> TypedSymbol a
forall t. SupportedPrim t => Symbol -> TypedSymbol t
TypedSymbol Symbol
"a") ((b --> (c --> (d --> (e --> f))))
-> Term (b --> (c --> (d --> (e --> f))))
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm 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 t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
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 t. SupportedPrim t => Term t -> Term t -> 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
_ 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
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. GeneralFun must have already been "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"partial evaluated away before reaching this point."
      )
      (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a --> b --> c --> d --> e --> f))
  symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> (e --> f)))))
-> Int -> String
symSBVName TypedSymbol (a --> (b --> (c --> (d --> (e --> f)))))
_ Int
num = String
"gfunc6_" 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
  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. GeneralFun 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
parseGeneralFunSMTModelResult

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 = TypedSymbol a
-> Term (b --> (c --> (d --> (e --> (f --> g)))))
-> a --> (b --> (c --> (d --> (e --> (f --> g)))))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun (Symbol -> TypedSymbol a
forall t. SupportedPrim t => Symbol -> TypedSymbol t
TypedSymbol Symbol
"a") ((b --> (c --> (d --> (e --> (f --> g)))))
-> Term (b --> (c --> (d --> (e --> (f --> g)))))
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm 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 t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
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 t. SupportedPrim t => Term t -> Term t -> 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
_ 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
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. GeneralFun must have already been "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"partial evaluated away before reaching this point."
      )
      (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a --> b --> c --> d --> e --> f --> g))
  symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> g))))))
-> Int -> String
symSBVName TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> g))))))
_ Int
num = String
"gfunc7_" 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
  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. GeneralFun 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
parseGeneralFunSMTModelResult

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 = TypedSymbol a
-> Term (b --> (c --> (d --> (e --> (f --> (g --> h))))))
-> a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun (Symbol -> TypedSymbol a
forall t. SupportedPrim t => Symbol -> TypedSymbol t
TypedSymbol Symbol
"a") ((b --> (c --> (d --> (e --> (f --> (g --> h))))))
-> Term (b --> (c --> (d --> (e --> (f --> (g --> h))))))
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm 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 t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
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 t. SupportedPrim t => Term t -> Term t -> 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
_ 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
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. GeneralFun must have already been "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"partial evaluated away before reaching this point."
      )
      (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a --> b --> c --> d --> e --> f --> g --> h))
  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
"gfunc8_" 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
  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. GeneralFun 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
parseGeneralFunSMTModelResult

pevalGeneralFunApplyTerm ::
  ( SupportedNonFuncPrim a,
    SupportedPrim b,
    SupportedPrim (a --> b)
  ) =>
  Term (a --> b) ->
  Term a ->
  Term b
pevalGeneralFunApplyTerm :: forall a b.
(SupportedNonFuncPrim a, SupportedPrim b,
 SupportedPrim (a --> b)) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm = (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)
forall {a} {b}.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Maybe (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 :: Term (a --> b) -> Term a -> Maybe (Term b)
doPevalApplyTerm (ConTerm Int
_ (GeneralFun TypedSymbol a
arg Term b
tm)) Term a
v =
      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
$ TypedSymbol a -> Term a -> Term b -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
arg Term a
v Term b
tm
    doPevalApplyTerm (ITETerm Int
_ Term Bool
c Term (a --> b)
l Term (a --> b)
r) Term a
v =
      Term b -> Maybe (Term b)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term b -> Maybe (Term b)) -> Term b -> Maybe (Term b)
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term b -> Term b -> Term b
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm Term Bool
c (Term (a --> b) -> Term a -> Term b
forall f a b. PEvalApplyTerm f a b => Term f -> Term a -> Term b
pevalApplyTerm Term (a --> b)
l Term a
v) (Term (a --> b) -> Term a -> Term b
forall f a b. PEvalApplyTerm f a b => Term f -> Term a -> Term b
pevalApplyTerm Term (a --> b)
r Term a
v)
    doPevalApplyTerm Term (a --> b)
_ Term a
_ = Maybe (Term b)
forall a. Maybe a
Nothing

instance
  ( SupportedPrim (a --> b),
    SupportedNonFuncPrim a,
    SupportedPrim b
  ) =>
  PEvalApplyTerm (a --> b) a b
  where
  pevalApplyTerm :: Term (a --> b) -> Term a -> Term b
pevalApplyTerm = Term (a --> b) -> Term a -> Term b
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b,
 SupportedPrim (a --> b)) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm
  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

substTerm :: forall a b. (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term a -> Term b -> Term b
substTerm :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
sym Term a
term = Term b -> Term b
forall x. SupportedPrim x => Term x -> Term x
gov
  where
    gov :: (SupportedPrim x) => Term x -> Term x
    gov :: forall x. SupportedPrim x => Term x -> Term x
gov Term x
b = case SomeTerm -> SomeTerm
go (Term x -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term x
b) of
      SomeTerm Term a
v -> Term a -> Term x
forall a b. a -> b
unsafeCoerce Term a
v
    go :: SomeTerm -> SomeTerm
    go :: SomeTerm -> SomeTerm
go = (SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo ((SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm)
-> (SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall a b. (a -> b) -> a -> b
$ \stm :: SomeTerm
stm@(SomeTerm (Term a
tm :: Term v)) ->
      case Term a
tm of
        ConTerm Int
_ a
cv -> case (TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep v) of
          App (App TypeRep a
gf TypeRep b
_) TypeRep b
_ ->
            case TypeRep a -> TypeRep (-->) -> Maybe (a :~~: (-->))
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
gf (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> *). Typeable a => TypeRep a
typeRep @(-->)) of
              Just a :~~: (-->)
HRefl -> case a
cv of
                GeneralFun TypedSymbol b
sym1 Term b
tm1 ->
                  if TypedSymbol b -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol b
sym1 SomeTypedSymbol -> SomeTypedSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
sym
                    then SomeTerm
stm
                    else Term (b --> b) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (b --> b) -> SomeTerm) -> Term (b --> b) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ (b --> b) -> Term (b --> b)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm ((b --> b) -> Term (b --> b)) -> (b --> b) -> Term (b --> b)
forall a b. (a -> b) -> a -> b
$ TypedSymbol b -> Term b -> b --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol b
sym1 (Term b -> Term b
forall x. SupportedPrim x => Term x -> Term x
gov Term b
tm1)
              Maybe (a :~~: (-->))
Nothing -> SomeTerm
stm
          TypeRep a
_ -> SomeTerm
stm
        SymTerm Int
_ TypedSymbol a
ts -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ if TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
ts SomeTypedSymbol -> SomeTypedSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
sym then Term a -> Term a
forall a b. a -> b
unsafeCoerce Term a
term else Term a
tm
        UnaryTerm Int
_ tag
tag Term arg
te -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ tag -> Term arg -> Term a
forall tag arg t.
(UnaryOp tag arg t, Typeable tag, Typeable t) =>
tag -> Term arg -> Term t
pevalUnary tag
tag (Term arg -> Term arg
forall x. SupportedPrim x => Term x -> Term x
gov Term arg
te)
        BinaryTerm Int
_ tag
tag Term arg1
te Term arg2
te' -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ tag -> Term arg1 -> Term arg2 -> Term a
forall tag arg1 arg2 t.
(BinaryOp tag arg1 arg2 t, Typeable tag, Typeable t) =>
tag -> Term arg1 -> Term arg2 -> Term t
pevalBinary tag
tag (Term arg1 -> Term arg1
forall x. SupportedPrim x => Term x -> Term x
gov Term arg1
te) (Term arg2 -> Term arg2
forall x. SupportedPrim x => Term x -> Term x
gov Term arg2
te')
        TernaryTerm Int
_ tag
tag Term arg1
op1 Term arg2
op2 Term arg3
op3 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term a
forall tag arg1 arg2 arg3 t.
(TernaryOp tag arg1 arg2 arg3 t, Typeable tag, Typeable t) =>
tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
pevalTernary tag
tag (Term arg1 -> Term arg1
forall x. SupportedPrim x => Term x -> Term x
gov Term arg1
op1) (Term arg2 -> Term arg2
forall x. SupportedPrim x => Term x -> Term x
gov Term arg2
op2) (Term arg3 -> Term arg3
forall x. SupportedPrim x => Term x -> Term x
gov Term arg3
op3)
        NotTerm Int
_ Term Bool
op -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
pevalNotTerm (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op)
        OrTerm Int
_ Term Bool
op1 Term Bool
op2 -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op1) (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op2)
        AndTerm Int
_ Term Bool
op1 Term Bool
op2 -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op1) (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op2)
        EqTerm Int
_ Term t1
op1 Term t1
op2 -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term t1 -> Term t1 -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op1) (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op2)
        ITETerm Int
_ Term Bool
c Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term a -> Term a -> Term a
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
c) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        AddNumTerm Int
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalAddNumTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        NegNumTerm Int
_ Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        MulNumTerm Int
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalMulNumTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        AbsNumTerm Int
_ Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalAbsNumTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        SignumNumTerm Int
_ Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalSignumNumTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        LtOrdTerm Int
_ Term t1
op1 Term t1
op2 -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term t1 -> Term t1 -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalLtOrdTerm (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op1) (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op2)
        LeOrdTerm Int
_ Term t1
op1 Term t1
op2 -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term t1 -> Term t1 -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalLeOrdTerm (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op1) (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op2)
        AndBitsTerm Int
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t -> Term t
pevalAndBitsTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        OrBitsTerm Int
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t -> Term t
pevalOrBitsTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        XorBitsTerm Int
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t -> Term t
pevalXorBitsTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        ComplementBitsTerm Int
_ Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t
pevalComplementBitsTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        ShiftLeftTerm Int
_ Term a
op Term a
n -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftLeftTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
n)
        RotateLeftTerm Int
_ Term a
op Term a
n -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall t. PEvalRotateTerm t => Term t -> Term t -> Term t
pevalRotateLeftTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
n)
        ShiftRightTerm Int
_ Term a
op Term a
n -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftRightTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
n)
        RotateRightTerm Int
_ Term a
op Term a
n -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall t. PEvalRotateTerm t => Term t -> Term t -> Term t
pevalRotateRightTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
n)
        ToSignedTerm Int
_ Term (u n)
op -> Term (s n) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (s n) -> SomeTerm) -> Term (s n) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term (u n) -> Term (s n)
forall (n :: Nat). (KnownNat n, 1 <= n) => Term (u n) -> Term (s n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (u n) -> Term (s n)
pevalBVToSignedTerm Term (u n)
op
        ToUnsignedTerm Int
_ Term (s n)
op -> Term (u n) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (u n) -> SomeTerm) -> Term (u n) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term (s n) -> Term (u n)
forall (n :: Nat). (KnownNat n, 1 <= n) => Term (s n) -> Term (u n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (s n) -> Term (u n)
pevalBVToUnsignedTerm Term (s n)
op
        BVConcatTerm Int
_ Term (bv l)
op1 Term (bv r)
op2 -> Term (bv (l + r)) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (bv (l + r)) -> SomeTerm) -> Term (bv (l + r)) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term (bv l) -> Term (bv r) -> Term (bv (l + r))
forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
pevalBVConcatTerm (Term (bv l) -> Term (bv l)
forall x. SupportedPrim x => Term x -> Term x
gov Term (bv l)
op1) (Term (bv r) -> Term (bv r)
forall x. SupportedPrim x => Term x -> Term x
gov Term (bv r)
op2)
        BVSelectTerm Int
_ TypeRep ix
ix TypeRep w
w Term (bv n)
op -> Term (bv w) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (bv w) -> SomeTerm) -> Term (bv w) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ TypeRep ix -> TypeRep w -> Term (bv n) -> Term (bv w)
forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
       (q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
       (p :: Nat -> *) (q :: Nat -> *).
(PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n,
 1 <= w, (ix + w) <= n) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
pevalBVSelectTerm TypeRep ix
ix TypeRep w
w (Term (bv n) -> Term (bv n)
forall x. SupportedPrim x => Term x -> Term x
gov Term (bv n)
op)
        BVExtendTerm Int
_ Bool
n TypeRep r
signed Term (bv l)
op -> Term (bv r) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (bv r) -> SomeTerm) -> Term (bv r) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Bool -> TypeRep r -> Term (bv l) -> Term (bv r)
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalBVExtendTerm Bool
n TypeRep r
signed (Term (bv l) -> Term (bv l)
forall x. SupportedPrim x => Term x -> Term x
gov Term (bv l)
op)
        ApplyTerm Int
_ Term f
f Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term f -> Term a -> Term a
forall f a b. PEvalApplyTerm f a b => Term f -> Term a -> Term b
pevalApplyTerm (Term f -> Term f
forall x. SupportedPrim x => Term x -> Term x
gov Term f
f) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        DivIntegralTerm Int
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalDivIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        ModIntegralTerm Int
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalModIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        QuotIntegralTerm Int
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalQuotIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        RemIntegralTerm Int
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalRemIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)