{-# 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,
    freshArgSymbol,
  )
where

import Control.DeepSeq (NFData (rnf))
import Data.Bifunctor (Bifunctor (second))
import Data.Foldable (Foldable (foldl', toList))
import qualified Data.HashSet as HS
import Data.Hashable (Hashable (hashWithSalt))
import Data.List.NonEmpty (NonEmpty ((:|)))
import Data.Maybe (fromJust)
import qualified Data.SBV as SBV
import qualified Data.SBV.Dynamic as SBVD
import Grisette.Internal.Core.Data.Class.Function
  ( Apply (FunType, apply),
    Function ((#)),
  )
import Grisette.Internal.Core.Data.MemoUtils (htmemo)
import Grisette.Internal.Core.Data.Symbol
  ( Symbol (IndexedSymbol),
  )
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
  ( 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),
    SomeTypedAnySymbol,
    SomeTypedConstantSymbol,
    SupportedNonFuncPrim (withNonFuncPrim),
    SupportedPrim
      ( castTypedSymbol,
        defaultValue,
        parseSMTModelResult,
        pevalDistinctTerm,
        pevalITETerm,
        primTypeRep,
        withPrim
      ),
    SupportedPrimConstraint (PrimConstraint),
    SymRep (SymType),
    SymbolKind (AnyKind),
    Term
      ( AbsNumTerm,
        AddNumTerm,
        AndBitsTerm,
        AndTerm,
        ApplyTerm,
        BVConcatTerm,
        BVExtendTerm,
        BVSelectTerm,
        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,
        ToFPTerm,
        XorBitsTerm
      ),
    TypedAnySymbol,
    TypedConstantSymbol,
    TypedSymbol,
    applyTerm,
    conTerm,
    eqHeteroSymbol,
    existsTerm,
    forallTerm,
    introSupportedPrimConstraint,
    partitionCVArg,
    pevalAndTerm,
    pevalEqTerm,
    pevalITEBasicTerm,
    pevalNotTerm,
    pevalOrTerm,
    pevalQuotIntegralTerm,
    pevalRemIntegralTerm,
    pevalRotateLeftTerm,
    pformatTerm,
    someTypedSymbol,
    symTerm,
    translateTypeError,
    typedAnySymbol,
    typedConstantSymbol,
    withConstantSymbolSupported,
    withSymbolSupported,
  )
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 ::
    (SupportedNonFuncPrim 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 -> HashSet SomeTypedConstantSymbol -> Term b -> Term b
forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a
-> Term a -> HashSet SomeTypedConstantSymbol -> Term b -> Term b
substTerm TypedConstantSymbol a
s (sa -> Term a
forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm sa
x) HashSet SomeTypedConstantSymbol
forall a. HashSet a
HS.empty Term b
t

infixr 0 -->

extractSymSomeTermIncludeBoundedVars ::
  SomeTerm -> HS.HashSet SomeTypedAnySymbol
extractSymSomeTermIncludeBoundedVars :: SomeTerm -> HashSet SomeTypedAnySymbol
extractSymSomeTermIncludeBoundedVars = (SomeTerm -> HashSet SomeTypedAnySymbol)
-> SomeTerm -> HashSet SomeTypedAnySymbol
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo SomeTerm -> HashSet SomeTypedAnySymbol
go
  where
    goTyped :: Term a -> HS.HashSet SomeTypedAnySymbol
    goTyped :: forall a. Term a -> HashSet SomeTypedAnySymbol
goTyped = SomeTerm -> HashSet SomeTypedAnySymbol
go (SomeTerm -> HashSet SomeTypedAnySymbol)
-> (Term a -> SomeTerm) -> Term a -> HashSet SomeTypedAnySymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term a -> SomeTerm
forall a. Term a -> SomeTerm
someTerm

    go :: SomeTerm -> HS.HashSet SomeTypedAnySymbol
    go :: SomeTerm -> HashSet SomeTypedAnySymbol
go (SomeTerm (SymTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ (TypedAnySymbol a
sym :: TypedAnySymbol a))) =
      SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol
forall a. Hashable a => a -> HashSet a
HS.singleton (SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol)
-> SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol
forall a b. (a -> b) -> a -> b
$ TypedAnySymbol a -> SomeTypedAnySymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedAnySymbol a
sym
    go (SomeTerm (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ a
cv :: Term v)) =
      case (TypeRep a
forall t. SupportedPrim t => TypeRep t
primTypeRep :: TypeRep v) of
        App (App TypeRep a
gf TypeRep b
_) TypeRep b
_ ->
          case TypeRep (-->) -> TypeRep a -> Maybe ((-->) :~~: a)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> *). Typeable a => TypeRep a
typeRep @(-->)) TypeRep a
gf of
            Just (-->) :~~: a
HRefl ->
              case a
cv of
                GeneralFun (TypedConstantSymbol b
tsym :: TypedConstantSymbol x) Term b
tm ->
                  HashSet SomeTypedAnySymbol
-> HashSet SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HS.union
                    ( SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol
forall a. Hashable a => a -> HashSet a
HS.singleton
                        (TypedSymbol 'AnyKind b -> SomeTypedAnySymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol (TypedSymbol 'AnyKind b -> SomeTypedAnySymbol)
-> TypedSymbol 'AnyKind b -> SomeTypedAnySymbol
forall a b. (a -> b) -> a -> b
$ Maybe (TypedSymbol 'AnyKind b) -> TypedSymbol 'AnyKind b
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (TypedSymbol 'AnyKind b) -> TypedSymbol 'AnyKind b)
-> Maybe (TypedSymbol 'AnyKind b) -> TypedSymbol 'AnyKind b
forall a b. (a -> b) -> a -> b
$ TypedConstantSymbol b -> Maybe (TypedSymbol 'AnyKind b)
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 b -> Maybe (TypedSymbol knd' b)
castTypedSymbol TypedConstantSymbol b
tsym)
                    )
                    (HashSet SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol)
-> HashSet SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol
forall a b. (a -> b) -> a -> b
$ SomeTerm -> HashSet SomeTypedAnySymbol
go (Term b -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term b
tm)
            Maybe ((-->) :~~: a)
Nothing -> HashSet SomeTypedAnySymbol
forall a. HashSet a
HS.empty
        TypeRep a
_ -> HashSet SomeTypedAnySymbol
forall a. HashSet a
HS.empty
    go (SomeTerm (ForallTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ TypedSymbol 'ConstantKind t1
sym Term Bool
arg)) =
      TypedSymbol 'ConstantKind t1
-> ((SupportedNonFuncPrim t1, Typeable t1) =>
    HashSet SomeTypedAnySymbol)
-> HashSet SomeTypedAnySymbol
forall t a.
TypedSymbol 'ConstantKind t
-> ((SupportedNonFuncPrim t, Typeable t) => a) -> a
withConstantSymbolSupported TypedSymbol 'ConstantKind t1
sym (((SupportedNonFuncPrim t1, Typeable t1) =>
  HashSet SomeTypedAnySymbol)
 -> HashSet SomeTypedAnySymbol)
-> ((SupportedNonFuncPrim t1, Typeable t1) =>
    HashSet SomeTypedAnySymbol)
-> HashSet SomeTypedAnySymbol
forall a b. (a -> b) -> a -> b
$
        SomeTypedAnySymbol
-> HashSet SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HS.insert (TypedSymbol 'AnyKind t1 -> SomeTypedAnySymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol (TypedSymbol 'AnyKind t1 -> SomeTypedAnySymbol)
-> TypedSymbol 'AnyKind t1 -> SomeTypedAnySymbol
forall a b. (a -> b) -> a -> b
$ Maybe (TypedSymbol 'AnyKind t1) -> TypedSymbol 'AnyKind t1
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (TypedSymbol 'AnyKind t1) -> TypedSymbol 'AnyKind t1)
-> Maybe (TypedSymbol 'AnyKind t1) -> TypedSymbol 'AnyKind t1
forall a b. (a -> b) -> a -> b
$ TypedSymbol 'ConstantKind t1 -> Maybe (TypedSymbol 'AnyKind t1)
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 t1 -> Maybe (TypedSymbol knd' t1)
castTypedSymbol TypedSymbol 'ConstantKind t1
sym) (HashSet SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol)
-> HashSet SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol
forall a b. (a -> b) -> a -> b
$
          Term Bool -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term Bool
arg
    go (SomeTerm (ExistsTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ TypedSymbol 'ConstantKind t1
sym Term Bool
arg)) =
      TypedSymbol 'ConstantKind t1
-> ((SupportedNonFuncPrim t1, Typeable t1) =>
    HashSet SomeTypedAnySymbol)
-> HashSet SomeTypedAnySymbol
forall t a.
TypedSymbol 'ConstantKind t
-> ((SupportedNonFuncPrim t, Typeable t) => a) -> a
withConstantSymbolSupported TypedSymbol 'ConstantKind t1
sym (((SupportedNonFuncPrim t1, Typeable t1) =>
  HashSet SomeTypedAnySymbol)
 -> HashSet SomeTypedAnySymbol)
-> ((SupportedNonFuncPrim t1, Typeable t1) =>
    HashSet SomeTypedAnySymbol)
-> HashSet SomeTypedAnySymbol
forall a b. (a -> b) -> a -> b
$
        SomeTypedAnySymbol
-> HashSet SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HS.insert (TypedSymbol 'AnyKind t1 -> SomeTypedAnySymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol (TypedSymbol 'AnyKind t1 -> SomeTypedAnySymbol)
-> TypedSymbol 'AnyKind t1 -> SomeTypedAnySymbol
forall a b. (a -> b) -> a -> b
$ Maybe (TypedSymbol 'AnyKind t1) -> TypedSymbol 'AnyKind t1
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (TypedSymbol 'AnyKind t1) -> TypedSymbol 'AnyKind t1)
-> Maybe (TypedSymbol 'AnyKind t1) -> TypedSymbol 'AnyKind t1
forall a b. (a -> b) -> a -> b
$ TypedSymbol 'ConstantKind t1 -> Maybe (TypedSymbol 'AnyKind t1)
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 t1 -> Maybe (TypedSymbol knd' t1)
castTypedSymbol TypedSymbol 'ConstantKind t1
sym) (HashSet SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol)
-> HashSet SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol
forall a b. (a -> b) -> a -> b
$
          Term Bool -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term Bool
arg
    go (SomeTerm (NotTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term Bool
arg)) = Term Bool -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term Bool
arg
    go (SomeTerm (OrTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term Bool
arg1 Term Bool
arg2)) = Term Bool -> Term Bool -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term Bool
arg1 Term Bool
arg2
    go (SomeTerm (AndTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term Bool
arg1 Term Bool
arg2)) = Term Bool -> Term Bool -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term Bool
arg1 Term Bool
arg2
    go (SomeTerm (EqTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term t1
arg1 Term t1
arg2)) = Term t1 -> Term t1 -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term t1
arg1 Term t1
arg2
    go (SomeTerm (DistinctTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ NonEmpty (Term t1)
args)) =
      [HashSet SomeTypedAnySymbol] -> HashSet SomeTypedAnySymbol
forall a. Monoid a => [a] -> a
mconcat ([HashSet SomeTypedAnySymbol] -> HashSet SomeTypedAnySymbol)
-> ([Term t1] -> [HashSet SomeTypedAnySymbol])
-> [Term t1]
-> HashSet SomeTypedAnySymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term t1 -> HashSet SomeTypedAnySymbol)
-> [Term t1] -> [HashSet SomeTypedAnySymbol]
forall a b. (a -> b) -> [a] -> [b]
map Term t1 -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goTyped ([Term t1] -> HashSet SomeTypedAnySymbol)
-> [Term t1] -> HashSet SomeTypedAnySymbol
forall a b. (a -> b) -> a -> b
$ NonEmpty (Term t1) -> [Term t1]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (Term t1)
args
    go (SomeTerm (ITETerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term Bool
cond Term a
arg1 Term a
arg2)) = Term Bool -> Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b c.
Term a -> Term b -> Term c -> HashSet SomeTypedAnySymbol
goTernary Term Bool
cond Term a
arg1 Term a
arg2
    go (SomeTerm (AddNumTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg1 Term a
arg2)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (NegNumTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg)) = Term a -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term a
arg
    go (SomeTerm (MulNumTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg1 Term a
arg2)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (AbsNumTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg)) = Term a -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term a
arg
    go (SomeTerm (SignumNumTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg)) = Term a -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term a
arg
    go (SomeTerm (LtOrdTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term t1
arg1 Term t1
arg2)) = Term t1 -> Term t1 -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term t1
arg1 Term t1
arg2
    go (SomeTerm (LeOrdTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term t1
arg1 Term t1
arg2)) = Term t1 -> Term t1 -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term t1
arg1 Term t1
arg2
    go (SomeTerm (AndBitsTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg1 Term a
arg2)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (OrBitsTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg1 Term a
arg2)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (XorBitsTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg1 Term a
arg2)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (ComplementBitsTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg)) = Term a -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term a
arg
    go (SomeTerm (ShiftLeftTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg Term a
n)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
arg Term a
n
    go (SomeTerm (ShiftRightTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg Term a
n)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
arg Term a
n
    go (SomeTerm (RotateLeftTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg Term a
n)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
arg Term a
n
    go (SomeTerm (RotateRightTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg Term a
n)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
arg Term a
n
    go (SomeTerm (BitCastTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg)) = Term a -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term a
arg
    go (SomeTerm (BitCastOrTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
d Term a
arg)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
d Term a
arg
    go (SomeTerm (BVConcatTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term (bv l)
arg1 Term (bv r)
arg2)) = Term (bv l) -> Term (bv r) -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term (bv l)
arg1 Term (bv r)
arg2
    go (SomeTerm (BVSelectTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Proxy ix
_ Proxy w
_ Term (bv n)
arg)) = Term (bv n) -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term (bv n)
arg
    go (SomeTerm (BVExtendTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Bool
_ Proxy r
_ Term (bv l)
arg)) = Term (bv l) -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term (bv l)
arg
    go (SomeTerm (ApplyTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term f
func Term a
arg)) = Term f -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term f
func Term a
arg
    go (SomeTerm (DivIntegralTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg1 Term a
arg2)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (ModIntegralTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg1 Term a
arg2)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (QuotIntegralTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg1 Term a
arg2)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (RemIntegralTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg1 Term a
arg2)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (FPTraitTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ FPTrait
_ Term (FP eb sb)
arg)) = Term (FP eb sb) -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term (FP eb sb)
arg
    go (SomeTerm (FdivTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg1 Term a
arg2)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (RecipTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg)) = Term a -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term a
arg
    go (SomeTerm (FloatingUnaryTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ FloatingUnaryOp
_ Term a
arg)) = Term a -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term a
arg
    go (SomeTerm (PowerTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg1 Term a
arg2)) = Term a -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (FPUnaryTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ FPUnaryOp
_ Term (FP eb sb)
arg)) = Term (FP eb sb) -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term (FP eb sb)
arg
    go (SomeTerm (FPBinaryTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ FPBinaryOp
_ Term (FP eb sb)
arg1 Term (FP eb sb)
arg2)) = Term (FP eb sb) -> Term (FP eb sb) -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term (FP eb sb)
arg1 Term (FP eb sb)
arg2
    go (SomeTerm (FPRoundingUnaryTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ FPRoundingUnaryOp
_ Term FPRoundingMode
_ Term (FP eb sb)
arg)) = Term (FP eb sb) -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term (FP eb sb)
arg
    go (SomeTerm (FPRoundingBinaryTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ FPRoundingBinaryOp
_ Term FPRoundingMode
_ Term (FP eb sb)
arg1 Term (FP eb sb)
arg2)) = Term (FP eb sb) -> Term (FP eb sb) -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term (FP eb sb)
arg1 Term (FP eb sb)
arg2
    go (SomeTerm (FPFMATerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term FPRoundingMode
mode Term (FP eb sb)
arg1 Term (FP eb sb)
arg2 Term (FP eb sb)
arg3)) =
      [HashSet SomeTypedAnySymbol] -> HashSet SomeTypedAnySymbol
forall a. Monoid a => [a] -> a
mconcat
        [ Term FPRoundingMode -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goTyped Term FPRoundingMode
mode,
          Term (FP eb sb) -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goTyped Term (FP eb sb)
arg1,
          Term (FP eb sb) -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goTyped Term (FP eb sb)
arg2,
          Term (FP eb sb) -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goTyped Term (FP eb sb)
arg3
        ]
    go (SomeTerm (FromIntegralTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
arg)) = Term a -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary Term a
arg
    go (SomeTerm (FromFPOrTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term a
d Term FPRoundingMode
mode Term (FP eb sb)
arg)) = Term a
-> Term FPRoundingMode
-> Term (FP eb sb)
-> HashSet SomeTypedAnySymbol
forall a b c.
Term a -> Term b -> Term c -> HashSet SomeTypedAnySymbol
goTernary Term a
d Term FPRoundingMode
mode Term (FP eb sb)
arg
    go (SomeTerm (ToFPTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term FPRoundingMode
mode Term a
arg Proxy eb
_ Proxy sb
_)) = Term FPRoundingMode -> Term a -> HashSet SomeTypedAnySymbol
forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term FPRoundingMode
mode Term a
arg
    goUnary :: Term a -> HS.HashSet SomeTypedAnySymbol
    goUnary :: forall a. Term a -> HashSet SomeTypedAnySymbol
goUnary = Term a -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goTyped
    goBinary ::
      Term a ->
      Term b ->
      HS.HashSet SomeTypedAnySymbol
    goBinary :: forall a b. Term a -> Term b -> HashSet SomeTypedAnySymbol
goBinary Term a
a Term b
b = Term a -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goTyped Term a
a HashSet SomeTypedAnySymbol
-> HashSet SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol
forall a. Semigroup a => a -> a -> a
<> Term b -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goTyped Term b
b
    goTernary ::
      Term a ->
      Term b ->
      Term c ->
      HS.HashSet SomeTypedAnySymbol
    goTernary :: forall a b c.
Term a -> Term b -> Term c -> HashSet SomeTypedAnySymbol
goTernary Term a
a Term b
b Term c
c = Term a -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goTyped Term a
a HashSet SomeTypedAnySymbol
-> HashSet SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol
forall a. Semigroup a => a -> a -> a
<> Term b -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goTyped Term b
b HashSet SomeTypedAnySymbol
-> HashSet SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol
forall a. Semigroup a => a -> a -> a
<> Term c -> HashSet SomeTypedAnySymbol
forall a. Term a -> HashSet SomeTypedAnySymbol
goTyped Term c
c

-- | Generate a fresh argument symbol that is not used as bounded or unbounded
-- variables in the function body for a general symbolic function.
freshArgSymbol ::
  forall a. (SupportedNonFuncPrim a) => [SomeTerm] -> TypedConstantSymbol a
freshArgSymbol :: forall a.
SupportedNonFuncPrim a =>
[SomeTerm] -> TypedConstantSymbol a
freshArgSymbol [SomeTerm]
terms = Symbol -> TypedSymbol 'ConstantKind a
forall t.
SupportedNonFuncPrim t =>
Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol (Symbol -> TypedSymbol 'ConstantKind a)
-> Symbol -> TypedSymbol 'ConstantKind a
forall a b. (a -> b) -> a -> b
$ Int -> Symbol
go Int
0
  where
    allSymbols :: HashSet SomeTypedAnySymbol
allSymbols = [HashSet SomeTypedAnySymbol] -> HashSet SomeTypedAnySymbol
forall a. Monoid a => [a] -> a
mconcat ([HashSet SomeTypedAnySymbol] -> HashSet SomeTypedAnySymbol)
-> [HashSet SomeTypedAnySymbol] -> HashSet SomeTypedAnySymbol
forall a b. (a -> b) -> a -> b
$ SomeTerm -> HashSet SomeTypedAnySymbol
extractSymSomeTermIncludeBoundedVars (SomeTerm -> HashSet SomeTypedAnySymbol)
-> [SomeTerm] -> [HashSet SomeTypedAnySymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SomeTerm]
terms
    go :: Int -> Symbol
    go :: Int -> Symbol
go Int
n =
      let currentSymbol :: Symbol
currentSymbol = Identifier -> Int -> Symbol
IndexedSymbol Identifier
"arg" Int
n
          currentTypedSymbol :: SomeTypedAnySymbol
currentTypedSymbol =
            TypedSymbol 'AnyKind a -> SomeTypedAnySymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol (Symbol -> TypedSymbol 'AnyKind a
forall t. SupportedPrim t => Symbol -> TypedSymbol 'AnyKind t
typedAnySymbol Symbol
currentSymbol :: TypedAnySymbol a)
       in if SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HS.member SomeTypedAnySymbol
currentTypedSymbol HashSet SomeTypedAnySymbol
allSymbols
            then Int -> Symbol
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
            else Symbol
currentSymbol

-- | Build a general symbolic function with a bounded symbol and a term.
buildGeneralFun ::
  forall a b.
  (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.
(SupportedNonFuncPrim a, SupportedPrim b) =>
TypedConstantSymbol a -> Term b -> a --> b
GeneralFun
    TypedConstantSymbol a
argSymbol
    (TypedConstantSymbol a
-> Term a -> HashSet SomeTypedConstantSymbol -> Term b -> Term b
forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a
-> Term a -> HashSet SomeTypedConstantSymbol -> Term b -> Term b
substTerm TypedConstantSymbol a
arg (TypedConstantSymbol a -> Term a
forall (knd :: SymbolKind) t. TypedSymbol knd t -> Term t
symTerm TypedConstantSymbol a
argSymbol) HashSet SomeTypedConstantSymbol
forall a. HashSet a
HS.empty Term b
v)
  where
    argSymbol :: TypedConstantSymbol a
argSymbol = [SomeTerm] -> TypedConstantSymbol a
forall a.
SupportedNonFuncPrim a =>
[SomeTerm] -> TypedConstantSymbol a
freshArgSymbol [Term b -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term b
v]

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. 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.
(SupportedNonFuncPrim 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

instance (Apply st, LinkedRep ca sa, LinkedRep ct st) => Apply (ca --> ct) where
  type FunType (ca --> ct) = SymType ca -> FunType (SymType ct)
  apply :: (ca --> ct) -> FunType (ca --> ct)
apply ca --> ct
uf sa
a = st -> FunType st
forall uf. Apply uf => uf -> FunType uf
apply (ca --> ct
uf (ca --> ct) -> sa -> st
forall f arg ret. Function f arg ret => f -> arg -> ret
# sa
a)

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 f a b.
(PEvalApplyTerm f a b, SupportedPrim b) =>
Term f -> Term a -> Term b
applyTerm
  where
    doPevalApplyTerm :: Term (a --> b) -> Term a -> Maybe (Term b)
doPevalApplyTerm (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ (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 -> HashSet SomeTypedConstantSymbol -> Term b -> Term b
forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a
-> Term a -> HashSet SomeTypedConstantSymbol -> Term b -> Term b
substTerm TypedConstantSymbol a
arg Term a
v HashSet SomeTypedConstantSymbol
forall a. HashSet a
HS.empty Term b
tm
    doPevalApplyTerm (ITETerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 :: TypedSymbol 'ConstantKind a
sym = Symbol -> TypedSymbol 'ConstantKind a
forall t.
SupportedNonFuncPrim t =>
Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol (Symbol -> TypedSymbol 'ConstantKind a)
-> Symbol -> TypedSymbol 'ConstantKind a
forall a b. (a -> b) -> a -> b
$ 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 (TypedSymbol 'ConstantKind a -> Term a
forall (knd :: SymbolKind) t. TypedSymbol knd t -> Term t
symTerm TypedSymbol 'ConstantKind a
sym) (a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm a
v))
                (b -> Term b
forall t. SupportedPrim t => t -> Term t
conTerm b
f)
                Term b
acc
          )
          (b -> Term b
forall t. SupportedPrim t => t -> Term t
conTerm b
def)
          [(a, b)]
funs
   in TypedSymbol 'ConstantKind a -> Term b -> a --> b
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
TypedConstantSymbol a -> Term b -> a --> b
buildGeneralFun TypedSymbol 'ConstantKind a
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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ a
cv :: Term x)) =
      case (TypeRep a
forall t. SupportedPrim t => TypeRep t
primTypeRep :: 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 => 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.
(SupportedNonFuncPrim 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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. TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool
forallTerm TypedSymbol 'ConstantKind t1
tsym) Term Bool
b
    goSome SomeTerm -> SomeTerm
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (ExistsTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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. TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool
existsTerm TypedSymbol 'ConstantKind t1
tsym) Term Bool
b
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (NotTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ Term t1
arg1 Term t1
arg2)) =
      Term t1
-> ((SupportedPrim t1, Typeable t1) => SomeTerm) -> SomeTerm
forall t a. Term t -> ((SupportedPrim t, Typeable t) => a) -> a
introSupportedPrimConstraint Term t1
arg1 (((SupportedPrim t1, Typeable t1) => SomeTerm) -> SomeTerm)
-> ((SupportedPrim t1, Typeable t1) => SomeTerm) -> SomeTerm
forall a b. (a -> b) -> a -> b
$
        (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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ args :: NonEmpty (Term t1)
args@(Term t1
arg1 :| [Term t1]
_))) =
      Term t1
-> ((SupportedPrim t1, Typeable t1) => SomeTerm) -> SomeTerm
forall t a. Term t -> ((SupportedPrim t, Typeable t) => a) -> a
introSupportedPrimConstraint Term t1
arg1 (((SupportedPrim t1, Typeable t1) => SomeTerm) -> SomeTerm)
-> ((SupportedPrim t1, Typeable t1) => SomeTerm) -> SomeTerm
forall a b. (a -> b) -> a -> b
$
        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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ (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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ (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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ Proxy ix
ix Proxy 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 (Proxy ix -> Proxy 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 Proxy ix
ix Proxy w
w) Term (bv n)
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (BVExtendTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ Bool
n Proxy 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 -> Proxy 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 Proxy r
signed) Term (bv l)
arg
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (ApplyTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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)) =>
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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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)) =>
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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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)) =>
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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ (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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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 ->
  HS.HashSet SomeTypedConstantSymbol ->
  Term b ->
  Term b
substTerm :: forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a
-> Term a -> HashSet SomeTypedConstantSymbol -> 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
    ( \TypedSymbol 'AnyKind a
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 TypedSymbol 'AnyKind a
-> ((SupportedPrim a, Typeable a) => Term a) -> Term a
forall (knd :: SymbolKind) t a.
TypedSymbol knd t -> ((SupportedPrim t, Typeable t) => a) -> a
withSymbolSupported TypedSymbol 'AnyKind a
t (((SupportedPrim a, Typeable a) => Term a) -> Term a)
-> ((SupportedPrim a, Typeable a) => Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ TypedSymbol 'AnyKind a -> Term a
forall (knd :: SymbolKind) t. TypedSymbol knd t -> Term t
symTerm TypedSymbol 'AnyKind a
t
    )

supportedPrimFunUpTo
  [|buildGeneralFun (typedConstantSymbol "a") (conTerm defaultValue)|]
  [|
    \c t f -> case (t, f) of
      ( ConTerm _ _ _ _ (GeneralFun (ta :: TypedConstantSymbol a) a),
        ConTerm _ _ _ _ (GeneralFun tb b)
        ) ->
          conTerm $
            GeneralFun argSymbol $
              pevalITETerm
                c
                (substTerm ta (symTerm argSymbol) HS.empty a)
                (substTerm tb (symTerm argSymbol) HS.empty b)
          where
            argSymbol :: TypedConstantSymbol a
            argSymbol = freshArgSymbol [SomeTerm a, SomeTerm b]
      _ -> pevalITEBasicTerm c t f
    |]
  [|parseGeneralFunSMTModelResult|]
  ( \tyVars ->
      [|
        translateTypeError
          (Just "x")
          ( typeRep ::
              TypeRep
                $( foldl1 (\fty ty -> [t|$ty --> $fty|])
                     . reverse
                     $ tyVars
                 )
          )
        |]
  )
  "GeneralFun"
  "gfunc"
  ''(-->)
  8