{-# LANGUAGE CPP #-}
{-# 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

#if MIN_VERSION_base(4,20,0)
#else
import Data.Foldable (Foldable (foldl'))
#endif

import Control.DeepSeq (NFData (rnf))
import Data.Bifunctor (Bifunctor (second))
import qualified Data.HashSet as HS
import Data.Hashable (Hashable (hashWithSalt))
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 ()
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
      ),
    PEvalFPTerm
      ( pevalFPBinaryTerm,
        pevalFPFMATerm,
        pevalFPRoundingBinaryTerm,
        pevalFPRoundingUnaryTerm,
        pevalFPTraitTerm,
        pevalFPUnaryTerm
      ),
    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,
    TypedAnySymbol,
    TypedConstantSymbol,
    TypedSymbol,
    applyTerm,
    conTerm,
    eqHeteroSymbol,
    existsTerm,
    forallTerm,
    partitionCVArg,
    pevalAndTerm,
    pevalEqTerm,
    pevalITEBasicTerm,
    pevalNotTerm,
    pevalOrTerm,
    pevalQuotIntegralTerm,
    pevalRemIntegralTerm,
    pevalRotateLeftTerm,
    pformatTerm,
    someTypedSymbol,
    symTerm,
    translateTypeError,
    typedAnySymbol,
    typedConstantSymbol,
    pattern AbsNumTerm,
    pattern AddNumTerm,
    pattern AndBitsTerm,
    pattern AndTerm,
    pattern ApplyTerm,
    pattern BVConcatTerm,
    pattern BVExtendTerm,
    pattern BVSelectTerm,
    pattern BitCastOrTerm,
    pattern BitCastTerm,
    pattern ComplementBitsTerm,
    pattern ConTerm,
    pattern DistinctTerm,
    pattern DivIntegralTerm,
    pattern EqTerm,
    pattern ExistsTerm,
    pattern FPBinaryTerm,
    pattern FPFMATerm,
    pattern FPRoundingBinaryTerm,
    pattern FPRoundingUnaryTerm,
    pattern FPTraitTerm,
    pattern FPUnaryTerm,
    pattern FdivTerm,
    pattern FloatingUnaryTerm,
    pattern ForallTerm,
    pattern FromFPOrTerm,
    pattern FromIntegralTerm,
    pattern ITETerm,
    pattern LeOrdTerm,
    pattern LtOrdTerm,
    pattern ModIntegralTerm,
    pattern MulNumTerm,
    pattern NegNumTerm,
    pattern NotTerm,
    pattern OrBitsTerm,
    pattern OrTerm,
    pattern PowerTerm,
    pattern QuotIntegralTerm,
    pattern RecipTerm,
    pattern RemIntegralTerm,
    pattern RotateLeftTerm,
    pattern RotateRightTerm,
    pattern ShiftLeftTerm,
    pattern ShiftRightTerm,
    pattern SignumNumTerm,
    pattern SupportedTypedSymbol,
    pattern SymTerm,
    pattern ToFPTerm,
    pattern XorBitsTerm,
  )
import Grisette.Internal.SymPrim.Prim.Pattern (pattern SubTerms)
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 (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 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 TypedSymbol 'ConstantKind t
sym Term Bool
arg)) =
      SomeTypedAnySymbol
-> HashSet SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HS.insert (TypedSymbol 'AnyKind t -> SomeTypedAnySymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol (TypedSymbol 'AnyKind t -> SomeTypedAnySymbol)
-> TypedSymbol 'AnyKind t -> SomeTypedAnySymbol
forall a b. (a -> b) -> a -> b
$ Maybe (TypedSymbol 'AnyKind t) -> TypedSymbol 'AnyKind t
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (TypedSymbol 'AnyKind t) -> TypedSymbol 'AnyKind t)
-> Maybe (TypedSymbol 'AnyKind t) -> TypedSymbol 'AnyKind t
forall a b. (a -> b) -> a -> b
$ TypedSymbol 'ConstantKind t -> Maybe (TypedSymbol 'AnyKind t)
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 t -> Maybe (TypedSymbol knd' t)
castTypedSymbol TypedSymbol 'ConstantKind t
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
goTyped Term Bool
arg
    go (SomeTerm (ExistsTerm TypedSymbol 'ConstantKind t
sym Term Bool
arg)) =
      SomeTypedAnySymbol
-> HashSet SomeTypedAnySymbol -> HashSet SomeTypedAnySymbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HS.insert (TypedSymbol 'AnyKind t -> SomeTypedAnySymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol (TypedSymbol 'AnyKind t -> SomeTypedAnySymbol)
-> TypedSymbol 'AnyKind t -> SomeTypedAnySymbol
forall a b. (a -> b) -> a -> b
$ Maybe (TypedSymbol 'AnyKind t) -> TypedSymbol 'AnyKind t
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (TypedSymbol 'AnyKind t) -> TypedSymbol 'AnyKind t)
-> Maybe (TypedSymbol 'AnyKind t) -> TypedSymbol 'AnyKind t
forall a b. (a -> b) -> a -> b
$ TypedSymbol 'ConstantKind t -> Maybe (TypedSymbol 'AnyKind t)
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 t -> Maybe (TypedSymbol knd' t)
castTypedSymbol TypedSymbol 'ConstantKind t
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
goTyped Term Bool
arg
    go (SomeTerm (SubTerms [SomeTerm]
tms)) = [HashSet SomeTypedAnySymbol] -> HashSet SomeTypedAnySymbol
forall a. Monoid a => [a] -> a
mconcat ([HashSet SomeTypedAnySymbol] -> HashSet SomeTypedAnySymbol)
-> ([SomeTerm] -> [HashSet SomeTypedAnySymbol])
-> [SomeTerm]
-> HashSet SomeTypedAnySymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SomeTerm -> HashSet SomeTypedAnySymbol)
-> [SomeTerm] -> [HashSet SomeTypedAnySymbol]
forall a b. (a -> b) -> [a] -> [b]
map SomeTerm -> HashSet SomeTypedAnySymbol
go ([SomeTerm] -> HashSet SomeTypedAnySymbol)
-> [SomeTerm] -> HashSet SomeTypedAnySymbol
forall a b. (a -> b) -> a -> b
$ [SomeTerm]
tms

-- | 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 (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 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 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 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 TypedSymbol 'ConstantKind t
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 t -> SomeTypedConstantSymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedSymbol 'ConstantKind t
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 t -> Term Bool -> Term Bool
forall t. TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool
forallTerm TypedSymbol 'ConstantKind t
tsym) Term Bool
b
    goSome SomeTerm -> SomeTerm
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (ExistsTerm TypedSymbol 'ConstantKind t
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 t -> SomeTypedConstantSymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedSymbol 'ConstantKind t
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 t -> Term Bool -> Term Bool
forall t. TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool
existsTerm TypedSymbol 'ConstantKind t
tsym) Term Bool
b
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (NotTerm 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 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 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 Term t
arg1 Term t
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term t -> Term t -> Term Bool) -> Term t -> Term t -> 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 t -> Term t -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term t
arg1 Term t
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (DistinctTerm NonEmpty (Term t)
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 t) -> Term Bool
forall t. SupportedPrim t => NonEmpty (Term t) -> Term Bool
pevalDistinctTerm ((Term t -> Term t) -> NonEmpty (Term t) -> NonEmpty (Term t)
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 t -> Term t
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo) NonEmpty (Term t)
args)
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (ITETerm 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 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 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 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 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 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 Term t
arg1 Term t
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term t -> Term t -> Term Bool) -> Term t -> Term t -> 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 t -> Term t -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalLtOrdTerm Term t
arg1 Term t
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (LeOrdTerm Term t
arg1 Term t
arg2)) =
      (SomeTerm -> SomeTerm)
-> (Term t -> Term t -> Term Bool) -> Term t -> Term t -> 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 t -> Term t -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalLeOrdTerm Term t
arg1 Term t
arg2
    goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (AndBitsTerm 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 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 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 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 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 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 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 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 (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 (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 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 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 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 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 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 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 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 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 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 =>
FPTrait -> Term (fp eb sb) -> Term Bool
forall (fp :: Natural -> Natural -> *) (eb :: Natural)
       (sb :: Natural).
(PEvalFPTerm fp, ValidFP 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 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 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 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 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 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 =>
FPUnaryOp -> Term (fp eb sb) -> Term (fp eb sb)
forall (fp :: Natural -> Natural -> *) (eb :: Natural)
       (sb :: Natural).
(PEvalFPTerm fp, ValidFP 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 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 =>
FPBinaryOp -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb)
forall (fp :: Natural -> Natural -> *) (eb :: Natural)
       (sb :: Natural).
(PEvalFPTerm fp, ValidFP 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 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 =>
FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb)
forall (fp :: Natural -> Natural -> *) (eb :: Natural)
       (sb :: Natural).
(PEvalFPTerm fp, ValidFP 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 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 =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (fp eb sb)
-> Term (fp eb sb)
-> Term (fp eb sb)
forall (fp :: Natural -> Natural -> *) (eb :: Natural)
       (sb :: Natural).
(PEvalFPTerm fp, ValidFP 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 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 =>
Term FPRoundingMode
-> Term (fp eb sb)
-> Term (fp eb sb)
-> Term (fp eb sb)
-> Term (fp eb sb)
forall (fp :: Natural -> Natural -> *) (eb :: Natural)
       (sb :: Natural).
(PEvalFPTerm fp, ValidFP 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 (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 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 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 sym :: TypedSymbol knd a
sym@TypedSymbol knd a
SupportedTypedSymbol 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 -> 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