{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.TermUtils
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.Prim.TermUtils
  ( extractTerm,
    castTerm,
    someTermsSize,
    someTermSize,
    termSize,
    termsSize,
  )
where

import Control.Monad.State
  ( State,
    execState,
    gets,
    modify',
  )
import Data.Data (cast)
import Data.Foldable (Foldable (toList), traverse_)
import qualified Data.HashSet as HS
import Grisette.Internal.Core.Data.MemoUtils (htmemo2)
import Grisette.Internal.SymPrim.GeneralFun (type (-->) (GeneralFun))
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( IsSymbolKind (SymbolKindConstraint),
    SomeTypedConstantSymbol,
    SomeTypedSymbol (SomeTypedSymbol),
    SupportedPrim (castTypedSymbol),
    Term
      ( AbsNumTerm,
        AddNumTerm,
        AndBitsTerm,
        AndTerm,
        ApplyTerm,
        BVConcatTerm,
        BVExtendTerm,
        BVSelectTerm,
        BinaryTerm,
        BitCastOrTerm,
        BitCastTerm,
        ComplementBitsTerm,
        ConTerm,
        DistinctTerm,
        DivIntegralTerm,
        EqTerm,
        ExistsTerm,
        FPBinaryTerm,
        FPFMATerm,
        FPRoundingBinaryTerm,
        FPRoundingUnaryTerm,
        FPTraitTerm,
        FPUnaryTerm,
        FdivTerm,
        FloatingUnaryTerm,
        ForallTerm,
        FromFPOrTerm,
        FromIntegralTerm,
        ITETerm,
        LeOrdTerm,
        LtOrdTerm,
        ModIntegralTerm,
        MulNumTerm,
        NegNumTerm,
        NotTerm,
        OrBitsTerm,
        OrTerm,
        PowerTerm,
        QuotIntegralTerm,
        RecipTerm,
        RemIntegralTerm,
        RotateLeftTerm,
        RotateRightTerm,
        ShiftLeftTerm,
        ShiftRightTerm,
        SignumNumTerm,
        SymTerm,
        TernaryTerm,
        ToFPTerm,
        UnaryTerm,
        XorBitsTerm
      ),
    TypedAnySymbol,
    introSupportedPrimConstraint,
    someTypedSymbol,
  )
import Grisette.Internal.SymPrim.Prim.SomeTerm
  ( SomeTerm (SomeTerm),
  )
import Type.Reflection
  ( TypeRep,
    Typeable,
    eqTypeRep,
    typeRep,
    pattern App,
    type (:~~:) (HRefl),
  )
import qualified Type.Reflection as R

extractSymSomeTerm ::
  forall knd.
  (IsSymbolKind knd) =>
  HS.HashSet (SomeTypedConstantSymbol) ->
  SomeTerm ->
  Maybe (HS.HashSet (SomeTypedSymbol knd))
extractSymSomeTerm :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
extractSymSomeTerm = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
initialMemo
  where
    gotyped ::
      (SupportedPrim a) =>
      ( HS.HashSet (SomeTypedConstantSymbol) ->
        SomeTerm ->
        Maybe (HS.HashSet (SomeTypedSymbol knd))
      ) ->
      HS.HashSet (SomeTypedConstantSymbol) ->
      Term a ->
      Maybe (HS.HashSet (SomeTypedSymbol knd))
    gotyped :: forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
boundedSymbols Term a
a = HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
boundedSymbols (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
a)
    initialMemo ::
      HS.HashSet (SomeTypedConstantSymbol) ->
      SomeTerm ->
      Maybe (HS.HashSet (SomeTypedSymbol knd))
    initialMemo :: HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
initialMemo = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
forall k1 k2 a.
(Eq k1, Hashable k1, Eq k2, Hashable k2) =>
(k1 -> k2 -> a) -> k1 -> k2 -> a
htmemo2 ((HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
initialMemo)
    {-# NOINLINE initialMemo #-}

    go ::
      ( HS.HashSet (SomeTypedConstantSymbol) ->
        SomeTerm ->
        Maybe (HS.HashSet (SomeTypedSymbol knd))
      ) ->
      HS.HashSet (SomeTypedConstantSymbol) ->
      SomeTerm ->
      Maybe (HS.HashSet (SomeTypedSymbol knd))
    go :: (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (SymTerm Id
_ (TypedAnySymbol a
sym :: TypedAnySymbol a))) =
      case (TypedAnySymbol 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 TypedAnySymbol a
sym, TypedAnySymbol a -> Maybe (TypedSymbol knd 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 TypedAnySymbol a
sym) of
        (Just TypedSymbol 'ConstantKind a
sym', Maybe (TypedSymbol knd a)
_) | 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 -> HashSet (SomeTypedSymbol knd)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return HashSet (SomeTypedSymbol knd)
forall a. HashSet a
HS.empty
        (Maybe (TypedSymbol 'ConstantKind a)
_, Just TypedSymbol knd a
sym') ->
          HashSet (SomeTypedSymbol knd)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (HashSet (SomeTypedSymbol knd)
 -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet (SomeTypedSymbol knd)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b. (a -> b) -> a -> b
$ SomeTypedSymbol knd -> HashSet (SomeTypedSymbol knd)
forall a. Hashable a => a -> HashSet a
HS.singleton (SomeTypedSymbol knd -> HashSet (SomeTypedSymbol knd))
-> SomeTypedSymbol knd -> HashSet (SomeTypedSymbol knd)
forall a b. (a -> b) -> a -> b
$ TypeRep a -> TypedSymbol knd a -> SomeTypedSymbol knd
forall (knd :: SymbolKind) t.
TypeRep t -> TypedSymbol knd t -> SomeTypedSymbol knd
SomeTypedSymbol (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) TypedSymbol knd a
sym'
        (Maybe (TypedSymbol 'ConstantKind a), Maybe (TypedSymbol knd a))
_ -> Maybe (HashSet (SomeTypedSymbol knd))
forall a. Maybe a
Nothing
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (ConTerm Id
_ a
cv :: Term v)) =
      case (TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep v) of
        App (App TypeRep a
gf TypeRep b
_) TypeRep b
_ ->
          case TypeRep (-->) -> 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
sym (Term b
tm :: Term r) ->
                let newmemo :: HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
forall k1 k2 a.
(Eq k1, Hashable k1, Eq k2, Hashable k2) =>
(k1 -> k2 -> a) -> k1 -> k2 -> a
htmemo2 ((HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo)
                    {-# NOINLINE newmemo #-}
                 in (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped
                      HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
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)
                      Term b
tm
            Maybe ((-->) :~~: a)
Nothing -> HashSet (SomeTypedSymbol knd)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return HashSet (SomeTypedSymbol knd)
forall a. HashSet a
HS.empty
        TypeRep a
_ -> HashSet (SomeTypedSymbol knd)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return HashSet (SomeTypedSymbol knd)
forall a. HashSet a
HS.empty
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (ForallTerm Id
_ TypedSymbol 'ConstantKind t1
sym Term Bool
arg)) =
      let newmemo :: HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
forall k1 k2 a.
(Eq k1, Hashable k1, Eq k2, Hashable k2) =>
(k1 -> k2 -> a) -> k1 -> k2 -> a
htmemo2 ((HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo)
          {-# NOINLINE newmemo #-}
       in (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term Bool
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
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
sym) HashSet SomeTypedConstantSymbol
bs) Term Bool
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (ExistsTerm Id
_ TypedSymbol 'ConstantKind t1
sym Term Bool
arg)) =
      let newmemo :: HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
forall k1 k2 a.
(Eq k1, Hashable k1, Eq k2, Hashable k2) =>
(k1 -> k2 -> a) -> k1 -> k2 -> a
htmemo2 ((HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo)
          {-# NOINLINE newmemo #-}
       in (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term Bool
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
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
sym) HashSet SomeTypedConstantSymbol
bs) Term Bool
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (UnaryTerm Id
_ tag
_ Term arg
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term arg
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term arg
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (BinaryTerm Id
_ tag
_ Term arg1
arg1 Term arg2
arg2)) =
      (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term arg1
-> Term arg2
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term arg1
arg1 Term arg2
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (TernaryTerm Id
_ tag
_ Term arg1
arg1 Term arg2
arg2 Term arg3
arg3)) =
      (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term arg1
-> Term arg2
-> Term arg3
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Term c
-> Maybe (HashSet (SomeTypedSymbol knd))
goTernary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term arg1
arg1 Term arg2
arg2 Term arg3
arg3
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (NotTerm Id
_ Term Bool
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term Bool
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term Bool
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (OrTerm Id
_ Term Bool
arg1 Term Bool
arg2)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term Bool
-> Term Bool
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term Bool
arg1 Term Bool
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (AndTerm Id
_ Term Bool
arg1 Term Bool
arg2)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term Bool
-> Term Bool
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term Bool
arg1 Term Bool
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (EqTerm Id
_ Term t1
arg1 Term t1
arg2)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term t1
-> Term t1
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term t1
arg1 Term t1
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (DistinctTerm Id
_ NonEmpty (Term t1)
args)) =
      [Maybe (HashSet (SomeTypedSymbol knd))]
-> Maybe (HashSet (SomeTypedSymbol knd))
combineAllSets ([Maybe (HashSet (SomeTypedSymbol knd))]
 -> Maybe (HashSet (SomeTypedSymbol knd)))
-> [Maybe (HashSet (SomeTypedSymbol knd))]
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b. (a -> b) -> a -> b
$ (Term t1 -> Maybe (HashSet (SomeTypedSymbol knd)))
-> [Term t1] -> [Maybe (HashSet (SomeTypedSymbol knd))]
forall a b. (a -> b) -> [a] -> [b]
map ((HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term t1
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs) ([Term t1] -> [Maybe (HashSet (SomeTypedSymbol knd))])
-> [Term t1] -> [Maybe (HashSet (SomeTypedSymbol knd))]
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 HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (ITETerm Id
_ Term Bool
cond Term a
arg1 Term a
arg2)) =
      (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term Bool
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Term c
-> Maybe (HashSet (SomeTypedSymbol knd))
goTernary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term Bool
cond Term a
arg1 Term a
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (AddNumTerm Id
_ Term a
arg1 Term a
arg2)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (NegNumTerm Id
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (MulNumTerm Id
_ Term a
arg1 Term a
arg2)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (AbsNumTerm Id
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (SignumNumTerm Id
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (LtOrdTerm Id
_ Term t1
arg1 Term t1
arg2)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term t1
-> Term t1
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term t1
arg1 Term t1
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (LeOrdTerm Id
_ Term t1
arg1 Term t1
arg2)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term t1
-> Term t1
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term t1
arg1 Term t1
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (AndBitsTerm Id
_ Term a
arg1 Term a
arg2)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (OrBitsTerm Id
_ Term a
arg1 Term a
arg2)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (XorBitsTerm Id
_ Term a
arg1 Term a
arg2)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (ComplementBitsTerm Id
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (ShiftLeftTerm Id
_ Term a
arg Term a
n1)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg Term a
n1
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (ShiftRightTerm Id
_ Term a
arg Term a
n1)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg Term a
n1
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (RotateLeftTerm Id
_ Term a
arg Term a
n1)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg Term a
n1
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (RotateRightTerm Id
_ Term a
arg Term a
n1)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg Term a
n1
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (BitCastTerm Id
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (BitCastOrTerm Id
_ Term a
d Term a
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
d Term a
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (BVConcatTerm Id
_ Term (bv l)
arg1 Term (bv r)
arg2)) =
      (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (bv l)
-> Term (bv r)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (bv l)
arg1 Term (bv r)
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (BVSelectTerm Id
_ TypeRep ix
_ TypeRep w
_ Term (bv n)
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (bv n)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (bv n)
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (BVExtendTerm Id
_ Bool
_ TypeRep r
_ Term (bv l)
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (bv l)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (bv l)
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (ApplyTerm Id
_ Term f
func Term a
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term f
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term f
func Term a
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (DivIntegralTerm Id
_ Term a
arg1 Term a
arg2)) =
      (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (ModIntegralTerm Id
_ Term a
arg1 Term a
arg2)) =
      (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (QuotIntegralTerm Id
_ Term a
arg1 Term a
arg2)) =
      (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (RemIntegralTerm Id
_ Term a
arg1 Term a
arg2)) =
      (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FPTraitTerm Id
_ FPTrait
_ Term (FP eb sb)
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FdivTerm Id
_ Term a
arg1 Term a
arg2)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (RecipTerm Id
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FloatingUnaryTerm Id
_ FloatingUnaryOp
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (PowerTerm Id
_ Term a
arg1 Term a
arg2)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FPUnaryTerm Id
_ FPUnaryOp
_ Term (FP eb sb)
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FPBinaryTerm Id
_ FPBinaryOp
_ Term (FP eb sb)
arg1 Term (FP eb sb)
arg2)) =
      (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg1 Term (FP eb sb)
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FPRoundingUnaryTerm Id
_ FPRoundingUnaryOp
_ Term FPRoundingMode
_ Term (FP eb sb)
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FPRoundingBinaryTerm Id
_ FPRoundingBinaryOp
_ Term FPRoundingMode
_ Term (FP eb sb)
arg1 Term (FP eb sb)
arg2)) =
      (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg1 Term (FP eb sb)
arg2
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FPFMATerm Id
_ Term FPRoundingMode
mode Term (FP eb sb)
arg1 Term (FP eb sb)
arg2 Term (FP eb sb)
arg3)) =
      [Maybe (HashSet (SomeTypedSymbol knd))]
-> Maybe (HashSet (SomeTypedSymbol knd))
combineAllSets
        [ (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term FPRoundingMode
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term FPRoundingMode
mode,
          (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg1,
          (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg2,
          (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg3
        ]
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FromIntegralTerm Id
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FromFPOrTerm Id
_ Term a
d Term FPRoundingMode
mode Term (FP eb sb)
arg)) =
      (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Term c
-> Maybe (HashSet (SomeTypedSymbol knd))
goTernary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
d Term FPRoundingMode
mode Term (FP eb sb)
arg
    go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (ToFPTerm Id
_ Term FPRoundingMode
mode Term a
arg Proxy eb
_ Proxy sb
_)) = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term FPRoundingMode
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term FPRoundingMode
mode Term a
arg
    goUnary ::
      (SupportedPrim a) =>
      (HS.HashSet (SomeTypedConstantSymbol) -> SomeTerm -> Maybe (HS.HashSet (SomeTypedSymbol knd))) ->
      HS.HashSet (SomeTypedConstantSymbol) ->
      Term a ->
      Maybe (HS.HashSet (SomeTypedSymbol knd))
    goUnary :: forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary = (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped
    goBinary ::
      (SupportedPrim a, SupportedPrim b) =>
      (HS.HashSet (SomeTypedConstantSymbol) -> SomeTerm -> Maybe (HS.HashSet (SomeTypedSymbol knd))) ->
      HS.HashSet (SomeTypedConstantSymbol) ->
      Term a ->
      Term b ->
      Maybe (HS.HashSet (SomeTypedSymbol knd))
    goBinary :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term b
arg2 =
      Maybe (HashSet (SomeTypedSymbol knd))
-> Maybe (HashSet (SomeTypedSymbol knd))
-> Maybe (HashSet (SomeTypedSymbol knd))
forall {a}.
Eq a =>
Maybe (HashSet a) -> Maybe (HashSet a) -> Maybe (HashSet a)
combineSet ((HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1) ((HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term b
arg2)
    goTernary ::
      (SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
      (HS.HashSet (SomeTypedConstantSymbol) -> SomeTerm -> Maybe (HS.HashSet (SomeTypedSymbol knd))) ->
      HS.HashSet (SomeTypedConstantSymbol) ->
      Term a ->
      Term b ->
      Term c ->
      Maybe (HS.HashSet (SomeTypedSymbol knd))
    goTernary :: forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Term c
-> Maybe (HashSet (SomeTypedSymbol knd))
goTernary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term b
arg2 Term c
arg3 =
      [Maybe (HashSet (SomeTypedSymbol knd))]
-> Maybe (HashSet (SomeTypedSymbol knd))
combineAllSets
        [ (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1,
          (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term b
arg2,
          (HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term c
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
 -> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term c
arg3
        ]
    combineSet :: Maybe (HashSet a) -> Maybe (HashSet a) -> Maybe (HashSet a)
combineSet (Just HashSet a
a) (Just HashSet a
b) = HashSet a -> Maybe (HashSet a)
forall a. a -> Maybe a
Just (HashSet a -> Maybe (HashSet a)) -> HashSet a -> Maybe (HashSet a)
forall a b. (a -> b) -> a -> b
$ HashSet a -> HashSet a -> HashSet a
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HS.union HashSet a
a HashSet a
b
    combineSet Maybe (HashSet a)
_ Maybe (HashSet a)
_ = Maybe (HashSet a)
forall a. Maybe a
Nothing
    combineAllSets :: [Maybe (HashSet (SomeTypedSymbol knd))]
-> Maybe (HashSet (SomeTypedSymbol knd))
combineAllSets = (Maybe (HashSet (SomeTypedSymbol knd))
 -> Maybe (HashSet (SomeTypedSymbol knd))
 -> Maybe (HashSet (SomeTypedSymbol knd)))
-> [Maybe (HashSet (SomeTypedSymbol knd))]
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Maybe (HashSet (SomeTypedSymbol knd))
-> Maybe (HashSet (SomeTypedSymbol knd))
-> Maybe (HashSet (SomeTypedSymbol knd))
forall {a}.
Eq a =>
Maybe (HashSet a) -> Maybe (HashSet a) -> Maybe (HashSet a)
combineSet
{-# INLINEABLE extractSymSomeTerm #-}

-- | Extract all the symbols in a term.
extractTerm ::
  (IsSymbolKind knd, SymbolKindConstraint knd a, SupportedPrim a) =>
  HS.HashSet (SomeTypedConstantSymbol) ->
  Term a ->
  Maybe (HS.HashSet (SomeTypedSymbol knd))
extractTerm :: forall (knd :: SymbolKind) a.
(IsSymbolKind knd, SymbolKindConstraint knd a, SupportedPrim a) =>
HashSet SomeTypedConstantSymbol
-> Term a -> Maybe (HashSet (SomeTypedSymbol knd))
extractTerm HashSet SomeTypedConstantSymbol
initialBoundedSymbols Term a
t =
  HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
forall (knd :: SymbolKind).
IsSymbolKind knd =>
HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
extractSymSomeTerm HashSet SomeTypedConstantSymbol
initialBoundedSymbols (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t)
{-# INLINE extractTerm #-}

-- | Cast a term to another type.
castTerm :: forall a b. (Typeable b) => Term a -> Maybe (Term b)
castTerm :: forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm Term a
t = Term a -> (SupportedPrim a => Maybe (Term b)) -> Maybe (Term b)
forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term a
t ((SupportedPrim a => Maybe (Term b)) -> Maybe (Term b))
-> (SupportedPrim a => Maybe (Term b)) -> Maybe (Term b)
forall a b. (a -> b) -> a -> b
$ Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
{-# INLINE castTerm #-}

-- | Compute the size of a list of terms. Do not count the same term twice.
someTermsSize :: [SomeTerm] -> Int
someTermsSize :: [SomeTerm] -> Id
someTermsSize [SomeTerm]
terms = HashSet SomeTerm -> Id
forall a. HashSet a -> Id
HS.size (HashSet SomeTerm -> Id) -> HashSet SomeTerm -> Id
forall a b. (a -> b) -> a -> b
$ State (HashSet SomeTerm) [()]
-> HashSet SomeTerm -> HashSet SomeTerm
forall s a. State s a -> s -> s
execState ((SomeTerm -> StateT (HashSet SomeTerm) Identity ())
-> [SomeTerm] -> State (HashSet SomeTerm) [()]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse SomeTerm -> StateT (HashSet SomeTerm) Identity ()
goSome [SomeTerm]
terms) HashSet SomeTerm
forall a. HashSet a
HS.empty
  where
    exists :: Term a -> m Bool
exists Term a
t = (HashSet SomeTerm -> Bool) -> m Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SomeTerm -> HashSet SomeTerm -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HS.member (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t))
    add :: Term a -> m ()
add Term a
t = (HashSet SomeTerm -> HashSet SomeTerm) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (SomeTerm -> HashSet SomeTerm -> HashSet SomeTerm
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HS.insert (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t))
    goSome :: SomeTerm -> State (HS.HashSet SomeTerm) ()
    goSome :: SomeTerm -> StateT (HashSet SomeTerm) Identity ()
goSome (SomeTerm Term a
b) = Term a -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term a
b
    go :: forall b. Term b -> State (HS.HashSet SomeTerm) ()
    go :: forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go t :: Term b
t@ConTerm {} = Term b -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term b
t
    go t :: Term b
t@SymTerm {} = Term b -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term b
t
    go t :: Term b
t@(ForallTerm Id
_ TypedSymbol 'ConstantKind t1
_ Term Bool
arg) = Term b -> Term Bool -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term Bool
arg
    go t :: Term b
t@(ExistsTerm Id
_ TypedSymbol 'ConstantKind t1
_ Term Bool
arg) = Term b -> Term Bool -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term Bool
arg
    go t :: Term b
t@(UnaryTerm Id
_ tag
_ Term arg
arg) = Term b -> Term arg -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term arg
arg
    go t :: Term b
t@(BinaryTerm Id
_ tag
_ Term arg1
arg1 Term arg2
arg2) = Term b
-> Term arg1 -> Term arg2 -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term arg1
arg1 Term arg2
arg2
    go t :: Term b
t@(TernaryTerm Id
_ tag
_ Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) = Term b
-> Term arg1
-> Term arg2
-> Term arg3
-> StateT (HashSet SomeTerm) Identity ()
forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a
-> Term b
-> Term c
-> Term d
-> StateT (HashSet SomeTerm) Identity ()
goTernary Term b
t Term arg1
arg1 Term arg2
arg2 Term arg3
arg3
    go t :: Term b
t@(NotTerm Id
_ Term Bool
arg) = Term b -> Term Bool -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term Bool
arg
    go t :: Term b
t@(OrTerm Id
_ Term Bool
arg1 Term Bool
arg2) = Term b
-> Term Bool -> Term Bool -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term Bool
arg1 Term Bool
arg2
    go t :: Term b
t@(AndTerm Id
_ Term Bool
arg1 Term Bool
arg2) = Term b
-> Term Bool -> Term Bool -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term Bool
arg1 Term Bool
arg2
    go t :: Term b
t@(EqTerm Id
_ Term t1
arg1 Term t1
arg2) = Term b
-> Term t1 -> Term t1 -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term t1
arg1 Term t1
arg2
    go t :: Term b
t@(DistinctTerm Id
_ NonEmpty (Term t1)
args) = do
      Bool
b <- Term b -> StateT (HashSet SomeTerm) Identity Bool
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m Bool
exists Term b
t
      if Bool
b
        then () -> StateT (HashSet SomeTerm) Identity ()
forall a. a -> StateT (HashSet SomeTerm) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else do
          Term b -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term b
t
          (Term t1 -> StateT (HashSet SomeTerm) Identity ())
-> NonEmpty (Term t1) -> StateT (HashSet SomeTerm) Identity ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Term t1 -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go NonEmpty (Term t1)
args
    go t :: Term b
t@(ITETerm Id
_ Term Bool
cond Term b
arg1 Term b
arg2) = Term b
-> Term Bool
-> Term b
-> Term b
-> StateT (HashSet SomeTerm) Identity ()
forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a
-> Term b
-> Term c
-> Term d
-> StateT (HashSet SomeTerm) Identity ()
goTernary Term b
t Term Bool
cond Term b
arg1 Term b
arg2
    go t :: Term b
t@(AddNumTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(NegNumTerm Id
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(MulNumTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(AbsNumTerm Id
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(SignumNumTerm Id
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(LtOrdTerm Id
_ Term t1
arg1 Term t1
arg2) = Term b
-> Term t1 -> Term t1 -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term t1
arg1 Term t1
arg2
    go t :: Term b
t@(LeOrdTerm Id
_ Term t1
arg1 Term t1
arg2) = Term b
-> Term t1 -> Term t1 -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term t1
arg1 Term t1
arg2
    go t :: Term b
t@(AndBitsTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(OrBitsTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(XorBitsTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(ComplementBitsTerm Id
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(ShiftLeftTerm Id
_ Term b
arg Term b
n) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg Term b
n
    go t :: Term b
t@(ShiftRightTerm Id
_ Term b
arg Term b
n) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg Term b
n
    go t :: Term b
t@(RotateLeftTerm Id
_ Term b
arg Term b
n) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg Term b
n
    go t :: Term b
t@(RotateRightTerm Id
_ Term b
arg Term b
n) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg Term b
n
    go t :: Term b
t@(BitCastTerm Id
_ Term a
arg) = Term b -> Term a -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term a
arg
    go t :: Term b
t@(BitCastOrTerm Id
_ Term b
d Term a
arg) = Term b -> Term b -> Term a -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
d Term a
arg
    go t :: Term b
t@(BVConcatTerm Id
_ Term (bv l)
arg1 Term (bv r)
arg2) = Term b
-> Term (bv l)
-> Term (bv r)
-> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term (bv l)
arg1 Term (bv r)
arg2
    go t :: Term b
t@(BVSelectTerm Id
_ TypeRep ix
_ TypeRep w
_ Term (bv n)
arg) = Term b -> Term (bv n) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (bv n)
arg
    go t :: Term b
t@(BVExtendTerm Id
_ Bool
_ TypeRep r
_ Term (bv l)
arg) = Term b -> Term (bv l) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (bv l)
arg
    go t :: Term b
t@(ApplyTerm Id
_ Term f
func Term a
arg) = Term b -> Term f -> Term a -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term f
func Term a
arg
    go t :: Term b
t@(DivIntegralTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(ModIntegralTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(QuotIntegralTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(RemIntegralTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(FPTraitTerm Id
_ FPTrait
_ Term (FP eb sb)
arg) = Term b -> Term (FP eb sb) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (FP eb sb)
arg
    go t :: Term b
t@(FdivTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(RecipTerm Id
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(FloatingUnaryTerm Id
_ FloatingUnaryOp
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(PowerTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(FPUnaryTerm Id
_ FPUnaryOp
_ Term (FP eb sb)
arg) = Term b -> Term (FP eb sb) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (FP eb sb)
arg
    go t :: Term b
t@(FPBinaryTerm Id
_ FPBinaryOp
_ Term (FP eb sb)
arg1 Term (FP eb sb)
arg2) = Term b
-> Term (FP eb sb)
-> Term (FP eb sb)
-> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term (FP eb sb)
arg1 Term (FP eb sb)
arg2
    go t :: Term b
t@(FPRoundingUnaryTerm Id
_ FPRoundingUnaryOp
_ Term FPRoundingMode
_ Term (FP eb sb)
arg) = Term b -> Term (FP eb sb) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (FP eb sb)
arg
    go t :: Term b
t@(FPRoundingBinaryTerm Id
_ FPRoundingBinaryOp
_ Term FPRoundingMode
_ Term (FP eb sb)
arg1 Term (FP eb sb)
arg2) = Term b
-> Term (FP eb sb)
-> Term (FP eb sb)
-> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term (FP eb sb)
arg1 Term (FP eb sb)
arg2
    go t :: Term b
t@(FPFMATerm Id
_ Term FPRoundingMode
_ Term (FP eb sb)
arg1 Term (FP eb sb)
arg2 Term (FP eb sb)
arg3) = Term b
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
-> StateT (HashSet SomeTerm) Identity ()
forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a
-> Term b
-> Term c
-> Term d
-> StateT (HashSet SomeTerm) Identity ()
goTernary Term b
t Term (FP eb sb)
arg1 Term (FP eb sb)
arg2 Term (FP eb sb)
arg3
    go t :: Term b
t@(FromIntegralTerm Id
_ Term a
arg) = Term b -> Term a -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term a
arg
    go t :: Term b
t@(FromFPOrTerm Id
_ Term b
d Term FPRoundingMode
mode Term (FP eb sb)
arg) =
      Term b
-> Term b
-> Term FPRoundingMode
-> Term (FP eb sb)
-> StateT (HashSet SomeTerm) Identity ()
forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a
-> Term b
-> Term c
-> Term d
-> StateT (HashSet SomeTerm) Identity ()
goTernary Term b
t Term b
d Term FPRoundingMode
mode Term (FP eb sb)
arg
    go t :: Term b
t@(ToFPTerm Id
_ Term FPRoundingMode
mode Term a
arg Proxy eb
_ Proxy sb
_) = Term b
-> Term FPRoundingMode
-> Term a
-> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term FPRoundingMode
mode Term a
arg
    goUnary :: forall a b. (SupportedPrim a) => Term a -> Term b -> State (HS.HashSet SomeTerm) ()
    goUnary :: forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term a
t Term b
arg = do
      Bool
b <- Term a -> StateT (HashSet SomeTerm) Identity Bool
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m Bool
exists Term a
t
      if Bool
b
        then () -> StateT (HashSet SomeTerm) Identity ()
forall a. a -> StateT (HashSet SomeTerm) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else do
          Term a -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term a
t
          Term b -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term b
arg
    goBinary ::
      forall a b c.
      (SupportedPrim a, SupportedPrim b) =>
      Term a ->
      Term b ->
      Term c ->
      State (HS.HashSet SomeTerm) ()
    goBinary :: forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term a
t Term b
arg1 Term c
arg2 = do
      Bool
b <- Term a -> StateT (HashSet SomeTerm) Identity Bool
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m Bool
exists Term a
t
      if Bool
b
        then () -> StateT (HashSet SomeTerm) Identity ()
forall a. a -> StateT (HashSet SomeTerm) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else do
          Term a -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term a
t
          Term b -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term b
arg1
          Term c -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term c
arg2
    goTernary ::
      forall a b c d.
      (SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
      Term a ->
      Term b ->
      Term c ->
      Term d ->
      State (HS.HashSet SomeTerm) ()
    goTernary :: forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a
-> Term b
-> Term c
-> Term d
-> StateT (HashSet SomeTerm) Identity ()
goTernary Term a
t Term b
arg1 Term c
arg2 Term d
arg3 = do
      Bool
b <- Term a -> StateT (HashSet SomeTerm) Identity Bool
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m Bool
exists Term a
t
      if Bool
b
        then () -> StateT (HashSet SomeTerm) Identity ()
forall a. a -> StateT (HashSet SomeTerm) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else do
          Term a -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term a
t
          Term b -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term b
arg1
          Term c -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term c
arg2
          Term d -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term d
arg3
{-# INLINEABLE someTermsSize #-}

-- | Compute the size of a list of terms. Do not count the same term twice.
someTermSize :: SomeTerm -> Int
someTermSize :: SomeTerm -> Id
someTermSize SomeTerm
term = [SomeTerm] -> Id
someTermsSize [SomeTerm
term]
{-# INLINE someTermSize #-}

-- | Compute the size of a list of terms. Do not count the same term twice.
termsSize :: [Term a] -> Int
termsSize :: forall a. [Term a] -> Id
termsSize [Term a]
terms =
  [SomeTerm] -> Id
someTermsSize ([SomeTerm] -> Id) -> [SomeTerm] -> Id
forall a b. (a -> b) -> a -> b
$
    (\Term a
x -> Term a -> (SupportedPrim a => SomeTerm) -> SomeTerm
forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term a
x ((SupportedPrim a => SomeTerm) -> SomeTerm)
-> (SupportedPrim a => SomeTerm) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
x) (Term a -> SomeTerm) -> [Term a] -> [SomeTerm]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term a]
terms
{-# INLINEABLE termsSize #-}

-- | Compute the size of a term.
termSize :: Term a -> Int
termSize :: forall a. Term a -> Id
termSize Term a
term = [Term a] -> Id
forall a. [Term a] -> Id
termsSize [Term a
term]
{-# INLINE termSize #-}