{-# HLINT ignore "Eta reduce" #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

-- |
-- 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,
    generalSubstSomeTerm,
    substTerm,
  )
where

import Control.DeepSeq (NFData (rnf))
import Data.Bifunctor (Bifunctor (second))
import Data.Foldable (Foldable (foldl'))
import qualified Data.HashSet as HS
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.FunInstanceGen (supportedPrimFunUpTo)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP
  ( pevalFPBinaryTerm,
    pevalFPFMATerm,
    pevalFPRoundingBinaryTerm,
    pevalFPRoundingUnaryTerm,
    pevalFPTraitTerm,
    pevalFPUnaryTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.PartialEval (totalize2)
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( BinaryOp (pevalBinary),
    IsSymbolKind,
    LinkedRep (underlyingTerm, wrapTerm),
    NonFuncPrimConstraint,
    NonFuncSBVBaseType,
    PEvalApplyTerm (pevalApplyTerm, sbvApplyTerm),
    PEvalBVTerm (pevalBVConcatTerm, pevalBVExtendTerm, pevalBVSelectTerm),
    PEvalBitCastOrTerm (pevalBitCastOrTerm),
    PEvalBitCastTerm (pevalBitCastTerm),
    PEvalBitwiseTerm
      ( pevalAndBitsTerm,
        pevalComplementBitsTerm,
        pevalOrBitsTerm,
        pevalXorBitsTerm
      ),
    PEvalDivModIntegralTerm
      ( pevalDivIntegralTerm,
        pevalModIntegralTerm
      ),
    PEvalFloatingTerm (pevalFloatingUnaryTerm, pevalPowerTerm),
    PEvalFractionalTerm (pevalFdivTerm, pevalRecipTerm),
    PEvalFromIntegralTerm (pevalFromIntegralTerm),
    PEvalIEEEFPConvertibleTerm (pevalFromFPOrTerm, pevalToFPTerm),
    PEvalNumTerm
      ( pevalAbsNumTerm,
        pevalAddNumTerm,
        pevalMulNumTerm,
        pevalNegNumTerm,
        pevalSignumNumTerm
      ),
    PEvalOrdTerm (pevalLeOrdTerm, pevalLtOrdTerm),
    PEvalRotateTerm (pevalRotateRightTerm),
    PEvalShiftTerm (pevalShiftLeftTerm, pevalShiftRightTerm),
    SBVRep (SBVType),
    SomeTypedConstantSymbol,
    SupportedNonFuncPrim (withNonFuncPrim),
    SupportedPrim
      ( castTypedSymbol,
        defaultValue,
        parseSMTModelResult,
        pevalDistinctTerm,
        pevalITETerm,
        withPrim
      ),
    SupportedPrimConstraint (PrimConstraint),
    SymbolKind (AnyKind),
    Term
      ( AbsNumTerm,
        AddNumTerm,
        AndBitsTerm,
        AndTerm,
        ApplyTerm,
        BVConcatTerm,
        BVExtendTerm,
        BVSelectTerm,
        BinaryTerm,
        BitCastOrTerm,
        BitCastTerm,
        ComplementBitsTerm,
        ConTerm,
        DistinctTerm,
        DivIntegralTerm,
        EqTerm,
        ExistsTerm,
        FPBinaryTerm,
        FPFMATerm,
        FPRoundingBinaryTerm,
        FPRoundingUnaryTerm,
        FPTraitTerm,
        FPUnaryTerm,
        FdivTerm,
        FloatingUnaryTerm,
        ForallTerm,
        FromFPOrTerm,
        FromIntegralTerm,
        ITETerm,
        LeOrdTerm,
        LtOrdTerm,
        ModIntegralTerm,
        MulNumTerm,
        NegNumTerm,
        NotTerm,
        OrBitsTerm,
        OrTerm,
        PowerTerm,
        QuotIntegralTerm,
        RecipTerm,
        RemIntegralTerm,
        RotateLeftTerm,
        RotateRightTerm,
        ShiftLeftTerm,
        ShiftRightTerm,
        SignumNumTerm,
        SymTerm,
        TernaryTerm,
        ToFPTerm,
        UnaryTerm,
        XorBitsTerm
      ),
    TernaryOp (pevalTernary),
    TypedConstantSymbol,
    TypedSymbol (TypedSymbol, unTypedSymbol),
    UnaryOp (pevalUnary),
    applyTerm,
    conTerm,
    eqHeteroSymbol,
    existsTerm,
    forallTerm,
    partitionCVArg,
    pevalAndTerm,
    pevalEqTerm,
    pevalNotTerm,
    pevalOrTerm,
    pevalQuotIntegralTerm,
    pevalRemIntegralTerm,
    pevalRotateLeftTerm,
    pformatTerm,
    someTypedSymbol,
    symTerm,
    translateTypeError,
  )
import Grisette.Internal.SymPrim.Prim.SomeTerm (SomeTerm (SomeTerm), someTerm)
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.
--
-- >>> let f = ("x" :: TypedConstantSymbol 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) =>
    TypedConstantSymbol a ->
    Term b ->
    a --> b

instance (LinkedRep a sa, LinkedRep b sb) => Function (a --> b) sa sb where
  (GeneralFun TypedConstantSymbol 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
$ TypedConstantSymbol a -> Term a -> Term b -> Term b
forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a -> Term a -> Term b -> Term b
substTerm TypedConstantSymbol a
s (sa -> Term a
forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm sa
x) Term b
t

infixr 0 -->

-- | Build a general symbolic function with a bounded symbol and a term.
buildGeneralFun ::
  (SupportedNonFuncPrim a, SupportedPrim b) =>
  TypedConstantSymbol a ->
  Term b ->
  a --> b
buildGeneralFun :: forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
TypedConstantSymbol a -> Term b -> a --> b
buildGeneralFun TypedConstantSymbol a
arg Term b
v =
  TypedConstantSymbol a -> Term b -> a --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedConstantSymbol a -> Term b -> a --> b
GeneralFun
    (Symbol -> TypedConstantSymbol a
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
newarg)
    (TypedConstantSymbol a -> Term a -> Term b -> Term b
forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a -> Term a -> Term b -> Term b
substTerm TypedConstantSymbol 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 TypedConstantSymbol a -> Symbol
forall t (knd :: SymbolKind). TypedSymbol knd t -> Symbol
unTypedSymbol TypedConstantSymbol 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 TypedConstantSymbol a
sym1 Term b
tm1 == :: (a --> b) -> (a --> b) -> Bool
== GeneralFun TypedConstantSymbol a
sym2 Term b
tm2 = TypedConstantSymbol a
sym1 TypedConstantSymbol a -> TypedConstantSymbol a -> Bool
forall a. Eq a => a -> a -> Bool
== TypedConstantSymbol 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 TypedConstantSymbol a
sym Term b
tm) = String
"\\(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypedConstantSymbol a -> String
forall a. Show a => a -> String
show TypedConstantSymbol 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
pformatTerm Term b
tm

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

instance Hashable (a --> b) where
  Int
s hashWithSalt :: Int -> (a --> b) -> Int
`hashWithSalt` (GeneralFun TypedConstantSymbol a
sym Term b
tm) = Int
s Int -> TypedConstantSymbol a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedConstantSymbol 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 TypedConstantSymbol a
sym Term b
tm) = TypedConstantSymbol a -> ()
forall a. NFData a => a -> ()
rnf TypedConstantSymbol 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 (a --> b) =
      ( SupportedNonFuncPrim a,
        SupportedPrim b,
        NonFuncPrimConstraint a,
        PrimConstraint b,
        SBVType (a --> b) ~ (SBV.SBV (NonFuncSBVBaseType a) -> SBVType b)
      )

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

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 TypedConstantSymbol 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
$ TypedConstantSymbol a -> Term a -> Term b -> Term b
forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a -> Term a -> Term b -> Term b
substTerm TypedConstantSymbol 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 :: SBVType (a --> b) -> SBVType a -> SBVType b
sbvApplyTerm SBVType (a --> b)
f SBVType a
a =
    forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(a --> b) (((PrimConstraint (a --> b), SMTDefinable (SBVType (a --> b)),
   Mergeable (SBVType (a --> b)), Typeable (SBVType (a --> b))) =>
  SBVType b)
 -> SBVType b)
-> ((PrimConstraint (a --> b), SMTDefinable (SBVType (a --> b)),
     Mergeable (SBVType (a --> b)), Typeable (SBVType (a --> b))) =>
    SBVType b)
-> SBVType b
forall a b. (a -> b) -> a -> b
$ forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @a (((SymVal (NonFuncSBVBaseType a), EqSymbolic (SBVType a),
   Mergeable (SBVType a), SMTDefinable (SBVType a),
   Mergeable (SBVType a), SBVType a ~ SBV (NonFuncSBVBaseType a),
   PrimConstraint a) =>
  SBVType b)
 -> SBVType b)
-> ((SymVal (NonFuncSBVBaseType a), EqSymbolic (SBVType a),
     Mergeable (SBVType a), SMTDefinable (SBVType a),
     Mergeable (SBVType a), SBVType a ~ SBV (NonFuncSBVBaseType a),
     PrimConstraint a) =>
    SBVType b)
-> SBVType b
forall a b. (a -> b) -> a -> b
$ SBVType (a --> b)
SBV (NonFuncSBVBaseType a) -> SBVType b
f SBV (NonFuncSBVBaseType a)
SBVType a
a

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 ->
              case [([CV], CV)]
r of
                [([], CV
v)] -> 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
v)
                [([CV], CV)]
_ -> 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 TypedConstantSymbol a -> Term b -> a --> b
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
TypedConstantSymbol a -> Term b -> a --> b
buildGeneralFun (Symbol -> TypedConstantSymbol a
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
sym) Term b
body

-- | General procedure for substituting symbols in a term.
{-# NOINLINE generalSubstSomeTerm #-}
generalSubstSomeTerm ::
  forall v.
  (forall a. TypedSymbol 'AnyKind a -> Term a) ->
  HS.HashSet SomeTypedConstantSymbol ->
  Term v ->
  Term v
generalSubstSomeTerm :: forall v.
(forall a. TypedSymbol 'AnyKind a -> Term a)
-> HashSet SomeTypedConstantSymbol -> Term v -> Term v
generalSubstSomeTerm forall a. TypedSymbol 'AnyKind a -> Term a
subst HashSet SomeTypedConstantSymbol
initialBoundedSymbols = (SomeTerm -> SomeTerm) -> Term v -> Term v
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
initialMemo
  where
    go :: forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
    go :: forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term a
a = case SomeTerm -> SomeTerm
memo (SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> SomeTerm
forall a. Term a -> SomeTerm
someTerm Term a
a of
      SomeTerm Term a
v -> Term a -> Term a
forall a b. a -> b
unsafeCoerce Term a
v
    initialMemo :: SomeTerm -> SomeTerm
    initialMemo :: SomeTerm -> SomeTerm
initialMemo = (SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo ((SomeTerm -> SomeTerm)
-> HashSet SomeTypedConstantSymbol -> SomeTerm -> SomeTerm
goSome SomeTerm -> SomeTerm
initialMemo HashSet SomeTypedConstantSymbol
initialBoundedSymbols)
    {-# NOINLINE initialMemo #-}
    goSome ::
      (SomeTerm -> SomeTerm) ->
      HS.HashSet SomeTypedConstantSymbol ->
      SomeTerm ->
      SomeTerm
    goSome :: (SomeTerm -> SomeTerm)
-> HashSet SomeTypedConstantSymbol -> SomeTerm -> SomeTerm
goSome SomeTerm -> SomeTerm
_ HashSet SomeTypedConstantSymbol
bs c :: SomeTerm
c@(SomeTerm (ConTerm Int
_ a
cv :: Term x)) =
      case (TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep x) 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 TypedConstantSymbol b
sym (Term b
tm :: Term r) ->
                let newmemo :: SomeTerm -> SomeTerm
newmemo =
                      (SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo
                        ( (SomeTerm -> SomeTerm)
-> HashSet SomeTypedConstantSymbol -> SomeTerm -> SomeTerm
goSome
                            SomeTerm -> SomeTerm
newmemo
                            (HashSet SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HS.union (SomeTypedConstantSymbol -> HashSet SomeTypedConstantSymbol
forall a. Hashable a => a -> HashSet a
HS.singleton (TypedConstantSymbol b -> SomeTypedConstantSymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedConstantSymbol b
sym)) HashSet SomeTypedConstantSymbol
bs)
                        )
                    {-# NOINLINE newmemo #-}
                 in 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
$ TypedConstantSymbol b -> Term b -> b --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedConstantSymbol a -> Term b -> a --> b
GeneralFun TypedConstantSymbol b
sym ((SomeTerm -> SomeTerm) -> Term b -> Term b
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
newmemo Term b
tm)
            Maybe (a :~~: (-->))
Nothing -> SomeTerm
c
        TypeRep a
_ -> SomeTerm
c
    goSome SomeTerm -> SomeTerm
_ HashSet SomeTypedConstantSymbol
bs c :: SomeTerm
c@(SomeTerm ((SymTerm Int
_ TypedSymbol 'AnyKind a
sym) :: Term a)) =
      case TypedSymbol 'AnyKind a -> Maybe (TypedSymbol 'ConstantKind a)
forall t (knd' :: SymbolKind) (knd :: SymbolKind).
(SupportedPrim t, IsSymbolKind knd') =>
TypedSymbol knd t -> Maybe (TypedSymbol knd' t)
forall (knd' :: SymbolKind) (knd :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd a -> Maybe (TypedSymbol knd' a)
castTypedSymbol TypedSymbol 'AnyKind a
sym of
        Just TypedSymbol 'ConstantKind a
sym' | SomeTypedConstantSymbol -> HashSet SomeTypedConstantSymbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HS.member (TypedSymbol 'ConstantKind a -> SomeTypedConstantSymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedSymbol 'ConstantKind a
sym') HashSet SomeTypedConstantSymbol
bs -> SomeTerm
c
        Maybe (TypedSymbol 'ConstantKind a)
_ -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ TypedSymbol 'AnyKind a -> Term a
forall a. TypedSymbol 'AnyKind a -> Term a
subst TypedSymbol 'AnyKind a
sym
    goSome SomeTerm -> SomeTerm
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (ForallTerm Int
_ TypedSymbol 'ConstantKind t1
tsym Term Bool
b)) =
      let newmemo :: SomeTerm -> SomeTerm
newmemo =
            (SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo ((SomeTerm -> SomeTerm)
-> HashSet SomeTypedConstantSymbol -> SomeTerm -> SomeTerm
goSome SomeTerm -> SomeTerm
newmemo (SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HS.insert (TypedSymbol 'ConstantKind t1 -> SomeTypedConstantSymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedSymbol 'ConstantKind t1
tsym) HashSet SomeTypedConstantSymbol
bs))
          {-# NOINLINE newmemo #-}
       in (SomeTerm -> SomeTerm)
-> (Term Bool -> Term Bool) -> Term Bool -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
newmemo (TypedSymbol 'ConstantKind t1 -> Term Bool -> Term Bool
forall t.
(SupportedNonFuncPrim t, Typeable t) =>
TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool
forallTerm TypedSymbol 'ConstantKind t1
tsym) Term Bool
b
    goSome SomeTerm -> SomeTerm
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (ExistsTerm Int
_ TypedSymbol 'ConstantKind t1
tsym Term Bool
b)) =
      let newmemo :: SomeTerm -> SomeTerm
newmemo =
            (SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo ((SomeTerm -> SomeTerm)
-> HashSet SomeTypedConstantSymbol -> SomeTerm -> SomeTerm
goSome SomeTerm -> SomeTerm
newmemo (SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HS.insert (TypedSymbol 'ConstantKind t1 -> SomeTypedConstantSymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedSymbol 'ConstantKind t1
tsym) HashSet SomeTypedConstantSymbol
bs))
          {-# NOINLINE newmemo #-}
       in (SomeTerm -> SomeTerm)
-> (Term Bool -> Term Bool) -> Term Bool -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
newmemo (TypedSymbol 'ConstantKind t1 -> Term Bool -> Term Bool
forall t.
(SupportedNonFuncPrim t, Typeable t) =>
TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool
existsTerm TypedSymbol 'ConstantKind t1
tsym) Term Bool
b
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (UnaryTerm Int
_ tag
tag (Term arg
arg :: Term a))) =
      (SomeTerm -> SomeTerm)
-> (Term arg -> Term a) -> Term arg -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (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
arg
    goSome
      SomeTerm -> SomeTerm
memo
      HashSet SomeTypedConstantSymbol
_
      (SomeTerm (BinaryTerm Int
_ tag
tag (Term arg1
arg1 :: Term a1) (Term arg2
arg2 :: Term a2))) =
        (SomeTerm -> SomeTerm)
-> (Term arg1 -> Term arg2 -> Term a)
-> Term arg1
-> Term arg2
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo (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
arg1 Term arg2
arg2
    goSome
      SomeTerm -> SomeTerm
memo
      HashSet SomeTypedConstantSymbol
_
      ( SomeTerm
          ( TernaryTerm
              Int
_
              tag
tag
              (Term arg1
arg1 :: Term a1)
              (Term arg2
arg2 :: Term a2)
              (Term arg3
arg3 :: Term a3)
            )
        ) = do
        (SomeTerm -> SomeTerm)
-> (Term arg1 -> Term arg2 -> Term arg3 -> Term a)
-> Term arg1
-> Term arg2
-> Term arg3
-> SomeTerm
forall {a} {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a -> Term a)
-> Term a
-> Term a
-> Term a
-> SomeTerm
goTernary SomeTerm -> SomeTerm
memo (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
arg1 Term arg2
arg2 Term arg3
arg3
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (NotTerm Int
_ Term Bool
arg)) =
      (SomeTerm -> SomeTerm)
-> (Term Bool -> Term Bool) -> Term Bool -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo Term Bool -> Term Bool
pevalNotTerm Term Bool
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (OrTerm Int
_ Term Bool
arg1 Term Bool
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term Bool -> Term Bool -> Term Bool)
-> Term Bool
-> Term Bool
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
arg1 Term Bool
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (AndTerm Int
_ Term Bool
arg1 Term Bool
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term Bool -> Term Bool -> Term Bool)
-> Term Bool
-> Term Bool
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
arg1 Term Bool
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (EqTerm Int
_ Term t1
arg1 Term t1
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term t1 -> Term t1 -> Term Bool)
-> Term t1
-> Term t1
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term t1 -> Term t1 -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term t1
arg1 Term t1
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (DistinctTerm Int
_ NonEmpty (Term t1)
args)) =
      Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ NonEmpty (Term t1) -> Term Bool
forall t. SupportedPrim t => NonEmpty (Term t) -> Term Bool
pevalDistinctTerm ((Term t1 -> Term t1) -> NonEmpty (Term t1) -> NonEmpty (Term t1)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SomeTerm -> SomeTerm) -> Term t1 -> Term t1
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo) NonEmpty (Term t1)
args)
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (ITETerm Int
_ Term Bool
cond Term a
arg1 Term a
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term Bool -> Term a -> Term a -> Term a)
-> Term Bool
-> Term a
-> Term a
-> SomeTerm
forall {a} {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a -> Term a)
-> Term a
-> Term a
-> Term a
-> SomeTerm
goTernary SomeTerm -> SomeTerm
memo Term Bool -> Term a -> Term a -> Term a
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm Term Bool
cond Term a
arg1 Term a
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (AddNumTerm Int
_ Term a
arg1 Term a
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalAddNumTerm Term a
arg1 Term a
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (NegNumTerm Int
_ Term a
arg)) =
      (SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term a
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (MulNumTerm Int
_ Term a
arg1 Term a
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalMulNumTerm Term a
arg1 Term a
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (AbsNumTerm Int
_ Term a
arg)) =
      (SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalAbsNumTerm Term a
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (SignumNumTerm Int
_ Term a
arg)) =
      (SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalSignumNumTerm Term a
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (LtOrdTerm Int
_ Term t1
arg1 Term t1
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term t1 -> Term t1 -> Term Bool)
-> Term t1
-> Term t1
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term t1 -> Term t1 -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalLtOrdTerm Term t1
arg1 Term t1
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (LeOrdTerm Int
_ Term t1
arg1 Term t1
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term t1 -> Term t1 -> Term Bool)
-> Term t1
-> Term t1
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term t1 -> Term t1 -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalLeOrdTerm Term t1
arg1 Term t1
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (AndBitsTerm Int
_ Term a
arg1 Term a
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t -> Term t
pevalAndBitsTerm Term a
arg1 Term a
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (OrBitsTerm Int
_ Term a
arg1 Term a
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t -> Term t
pevalOrBitsTerm Term a
arg1 Term a
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (XorBitsTerm Int
_ Term a
arg1 Term a
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t -> Term t
pevalXorBitsTerm Term a
arg1 Term a
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (ComplementBitsTerm Int
_ Term a
arg)) =
      (SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo Term a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t
pevalComplementBitsTerm Term a
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (ShiftLeftTerm Int
_ Term a
arg Term a
n)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftLeftTerm Term a
arg Term a
n
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (RotateLeftTerm Int
_ Term a
arg Term a
n)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalRotateTerm t => Term t -> Term t -> Term t
pevalRotateLeftTerm Term a
arg Term a
n
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (ShiftRightTerm Int
_ Term a
arg Term a
n)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftRightTerm Term a
arg Term a
n
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (RotateRightTerm Int
_ Term a
arg Term a
n)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalRotateTerm t => Term t -> Term t -> Term t
pevalRotateRightTerm Term a
arg Term a
n
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (BitCastTerm Int
_ (Term a
arg :: Term a) :: Term r)) =
      (SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (forall a b. PEvalBitCastTerm a b => Term a -> Term b
pevalBitCastTerm @a @r) Term a
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (BitCastOrTerm Int
_ (Term a
d :: term r) (Term a
arg :: Term a) :: Term r)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo (forall a b. PEvalBitCastOrTerm a b => Term b -> Term a -> Term b
pevalBitCastOrTerm @a @r) Term a
d Term a
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (BVConcatTerm Int
_ Term (bv l)
arg1 Term (bv r)
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term (bv l) -> Term (bv r) -> Term (bv (l + r)))
-> Term (bv l)
-> Term (bv r)
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term (bv l) -> Term (bv r) -> Term (bv (l + r))
forall (l :: Natural) (r :: Natural).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
pevalBVConcatTerm Term (bv l)
arg1 Term (bv r)
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (BVSelectTerm Int
_ TypeRep ix
ix TypeRep w
w Term (bv n)
arg)) =
      (SomeTerm -> SomeTerm)
-> (Term (bv n) -> Term (bv w)) -> Term (bv n) -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (TypeRep ix -> TypeRep w -> Term (bv n) -> Term (bv w)
forall (n :: Natural) (ix :: Natural) (w :: Natural)
       (p :: Natural -> *) (q :: Natural -> *).
(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 :: Natural -> *) (n :: Natural) (ix :: Natural)
       (w :: Natural) (p :: Natural -> *) (q :: Natural -> *).
(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)
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (BVExtendTerm Int
_ Bool
n TypeRep r
signed Term (bv l)
arg)) =
      (SomeTerm -> SomeTerm)
-> (Term (bv l) -> Term (bv r)) -> Term (bv l) -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (Bool -> TypeRep r -> Term (bv l) -> Term (bv r)
forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(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)
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (ApplyTerm Int
_ Term f
f Term a
arg)) =
      (SomeTerm -> SomeTerm)
-> (Term f -> Term a -> Term a) -> Term f -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term f -> Term a -> Term a
forall f a b. PEvalApplyTerm f a b => Term f -> Term a -> Term b
pevalApplyTerm Term f
f Term a
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (DivIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalDivIntegralTerm Term a
arg1 Term a
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (ModIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalModIntegralTerm Term a
arg1 Term a
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (QuotIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalQuotIntegralTerm Term a
arg1 Term a
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (RemIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalRemIntegralTerm Term a
arg1 Term a
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FPTraitTerm Int
_ FPTrait
trait Term (FP eb sb)
arg)) =
      (SomeTerm -> SomeTerm)
-> (Term (FP eb sb) -> Term Bool) -> Term (FP eb sb) -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (FPTrait -> Term (FP eb sb) -> Term Bool
forall (eb :: Natural) (sb :: Natural).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
trait) Term (FP eb sb)
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FdivTerm Int
_ Term a
arg1 Term a
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalFractionalTerm t => Term t -> Term t -> Term t
pevalFdivTerm Term a
arg1 Term a
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (RecipTerm Int
_ Term a
arg)) =
      (SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo Term a -> Term a
forall t. PEvalFractionalTerm t => Term t -> Term t
pevalRecipTerm Term a
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FloatingUnaryTerm Int
_ FloatingUnaryOp
op Term a
arg)) =
      (SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (FloatingUnaryOp -> Term a -> Term a
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
op) Term a
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (PowerTerm Int
_ Term a
arg1 Term a
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalFloatingTerm t => Term t -> Term t -> Term t
pevalPowerTerm Term a
arg1 Term a
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FPUnaryTerm Int
_ FPUnaryOp
op Term (FP eb sb)
arg)) =
      (SomeTerm -> SomeTerm)
-> (Term (FP eb sb) -> Term (FP eb sb))
-> Term (FP eb sb)
-> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Natural) (sb :: Natural).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPUnaryTerm FPUnaryOp
op) Term (FP eb sb)
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FPBinaryTerm Int
_ FPBinaryOp
op Term (FP eb sb)
arg1 Term (FP eb sb)
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb))
-> Term (FP eb sb)
-> Term (FP eb sb)
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo (FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Natural) (sb :: Natural).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPBinaryTerm FPBinaryOp
op) Term (FP eb sb)
arg1 Term (FP eb sb)
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FPRoundingUnaryTerm Int
_ FPRoundingUnaryOp
op Term FPRoundingMode
mode Term (FP eb sb)
arg)) =
      (SomeTerm -> SomeTerm)
-> (Term (FP eb sb) -> Term (FP eb sb))
-> Term (FP eb sb)
-> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Natural) (sb :: Natural).
(ValidFP eb sb, SupportedPrim (FP eb sb),
 SupportedPrim FPRoundingMode) =>
FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPRoundingUnaryTerm FPRoundingUnaryOp
op Term FPRoundingMode
mode) Term (FP eb sb)
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FPRoundingBinaryTerm Int
_ FPRoundingBinaryOp
op Term FPRoundingMode
mode Term (FP eb sb)
arg1 Term (FP eb sb)
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb))
-> Term (FP eb sb)
-> Term (FP eb sb)
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo (FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
forall (eb :: Natural) (sb :: Natural).
(ValidFP eb sb, SupportedPrim (FP eb sb),
 SupportedPrim FPRoundingMode) =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPRoundingBinaryTerm FPRoundingBinaryOp
op Term FPRoundingMode
mode) Term (FP eb sb)
arg1 Term (FP eb sb)
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FPFMATerm Int
_ Term FPRoundingMode
mode Term (FP eb sb)
arg1 Term (FP eb sb)
arg2 Term (FP eb sb)
arg3)) =
      Term (FP eb sb) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (FP eb sb) -> SomeTerm) -> Term (FP eb sb) -> SomeTerm
forall a b. (a -> b) -> a -> b
$
        Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
forall (eb :: Natural) (sb :: Natural).
(ValidFP eb sb, SupportedPrim (FP eb sb),
 SupportedPrim FPRoundingMode) =>
Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPFMATerm
          ((SomeTerm -> SomeTerm)
-> Term FPRoundingMode -> Term FPRoundingMode
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term FPRoundingMode
mode)
          ((SomeTerm -> SomeTerm) -> Term (FP eb sb) -> Term (FP eb sb)
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term (FP eb sb)
arg1)
          ((SomeTerm -> SomeTerm) -> Term (FP eb sb) -> Term (FP eb sb)
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term (FP eb sb)
arg2)
          ((SomeTerm -> SomeTerm) -> Term (FP eb sb) -> Term (FP eb sb)
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term (FP eb sb)
arg3)
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FromIntegralTerm Int
_ (Term a
arg :: Term a) :: Term b)) =
      (SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm @a @b) Term a
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FromFPOrTerm Int
_ Term a
d Term FPRoundingMode
mode Term (FP eb sb)
arg)) =
      (SomeTerm -> SomeTerm)
-> (Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a)
-> Term a
-> Term FPRoundingMode
-> Term (FP eb sb)
-> SomeTerm
forall {a} {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a -> Term a)
-> Term a
-> Term a
-> Term a
-> SomeTerm
goTernary SomeTerm -> SomeTerm
memo Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
forall a (eb :: Natural) (sb :: Natural).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
pevalFromFPOrTerm Term a
d Term FPRoundingMode
mode Term (FP eb sb)
arg
    goSome
      SomeTerm -> SomeTerm
memo
      HashSet SomeTypedConstantSymbol
_
      (SomeTerm (ToFPTerm Int
_ Term FPRoundingMode
mode (Term a
arg :: Term a) (Proxy eb
_ :: p eb) (Proxy sb
_ :: q sb))) =
        (SomeTerm -> SomeTerm)
-> (Term FPRoundingMode -> Term a -> Term (FP eb sb))
-> Term FPRoundingMode
-> Term a
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo (forall a (eb :: Natural) (sb :: Natural).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term FPRoundingMode -> Term a -> Term (FP eb sb)
pevalToFPTerm @a @eb @sb) Term FPRoundingMode
mode Term a
arg
    goUnary :: (SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo Term a -> Term a
f Term a
a = 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
f ((SomeTerm -> SomeTerm) -> Term a -> Term a
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term a
a)
    goBinary :: (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
f Term a
a Term a
b = 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
f ((SomeTerm -> SomeTerm) -> Term a -> Term a
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term a
a) ((SomeTerm -> SomeTerm) -> Term a -> Term a
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term a
b)
    goTernary :: (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a -> Term a)
-> Term a
-> Term a
-> Term a
-> SomeTerm
goTernary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a -> Term a
f Term a
a Term a
b Term a
c =
      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 -> Term a
f ((SomeTerm -> SomeTerm) -> Term a -> Term a
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term a
a) ((SomeTerm -> SomeTerm) -> Term a -> Term a
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term a
b) ((SomeTerm -> SomeTerm) -> Term a -> Term a
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term a
c)

-- | Substitute a term for a symbol in a term.
substTerm ::
  forall knd a b.
  (SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
  TypedSymbol knd a ->
  Term a ->
  Term b ->
  Term b
substTerm :: forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a -> Term a -> Term b -> Term b
substTerm TypedSymbol knd a
sym Term a
a =
  (forall a. TypedSymbol 'AnyKind a -> Term a)
-> HashSet SomeTypedConstantSymbol -> Term b -> Term b
forall v.
(forall a. TypedSymbol 'AnyKind a -> Term a)
-> HashSet SomeTypedConstantSymbol -> Term v -> Term v
generalSubstSomeTerm
    ( \t :: TypedSymbol 'AnyKind a
t@(TypedSymbol Symbol
t') ->
        if TypedSymbol knd a -> TypedSymbol 'AnyKind a -> Bool
forall (ta :: SymbolKind) a (tb :: SymbolKind) b.
TypedSymbol ta a -> TypedSymbol tb b -> Bool
eqHeteroSymbol TypedSymbol knd a
sym TypedSymbol 'AnyKind a
t then Term a -> Term a
forall a b. a -> b
unsafeCoerce Term a
a else Symbol -> Term a
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm Symbol
t'
    )
    HashSet SomeTypedConstantSymbol
forall a. HashSet a
HS.empty

supportedPrimFunUpTo
  [|buildGeneralFun (TypedSymbol "a") (conTerm defaultValue)|]
  [|parseGeneralFunSMTModelResult|]
  ( \tyVars ->
      [|
        translateTypeError
          (Just "x")
          ( typeRep ::
              TypeRep
                $( foldl1 (\fty ty -> [t|$ty --> $fty|])
                     . reverse
                     $ tyVars
                 )
          )
        |]
  )
  "GeneralFun"
  "gfunc"
  ''(-->)
  8