{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
  ( identity,
    identityWithTypeRep,
    introSupportedPrimConstraint,
    extractSymbolicsTerm,
    castTerm,
    pformat,
    someTermsSize,
    someTermSize,
    termSize,
    termsSize,
  )
where

import Control.Monad.State
  ( MonadState (get, put),
    State,
    evalState,
    execState,
    gets,
    modify',
  )
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import Data.Interned (Id)
import Data.Typeable
  ( Proxy (Proxy),
    TypeRep,
    Typeable,
    cast,
    typeRep,
  )
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
  ( SomeTerm (SomeTerm),
  )
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
  ( BinaryOp (pformatBinary),
    SomeTypedSymbol (SomeTypedSymbol),
    SupportedPrim (pformatCon, pformatSym),
    Term
      ( AbsNumTerm,
        AddNumTerm,
        AndBitsTerm,
        AndTerm,
        BVConcatTerm,
        BVExtendTerm,
        BVSelectTerm,
        BinaryTerm,
        ComplementBitsTerm,
        ConTerm,
        DivBoundedIntegralTerm,
        DivIntegralTerm,
        EqvTerm,
        GeneralFunApplyTerm,
        ITETerm,
        LENumTerm,
        LTNumTerm,
        ModBoundedIntegralTerm,
        ModIntegralTerm,
        NotTerm,
        OrBitsTerm,
        OrTerm,
        QuotBoundedIntegralTerm,
        QuotIntegralTerm,
        RemBoundedIntegralTerm,
        RemIntegralTerm,
        RotateLeftTerm,
        RotateRightTerm,
        ShiftLeftTerm,
        ShiftRightTerm,
        SignumNumTerm,
        SymTerm,
        TabularFunApplyTerm,
        TernaryTerm,
        TimesNumTerm,
        ToSignedTerm,
        ToUnsignedTerm,
        UMinusNumTerm,
        UnaryTerm,
        XorBitsTerm
      ),
    TernaryOp (pformatTernary),
    TypedSymbol,
    UnaryOp (pformatUnary),
  )
import qualified Type.Reflection as R

identity :: Term t -> Id
identity :: forall t. Term t -> Id
identity = (TypeRep, Id) -> Id
forall a b. (a, b) -> b
snd ((TypeRep, Id) -> Id) -> (Term t -> (TypeRep, Id)) -> Term t -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term t -> (TypeRep, Id)
forall t. Term t -> (TypeRep, Id)
identityWithTypeRep
{-# INLINE identity #-}

identityWithTypeRep :: forall t. Term t -> (TypeRep, Id)
identityWithTypeRep :: forall t. Term t -> (TypeRep, Id)
identityWithTypeRep (ConTerm Id
i t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (SymTerm Id
i TypedSymbol t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (UnaryTerm Id
i tag
_ Term arg
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (BinaryTerm Id
i tag
_ Term arg1
_ Term arg2
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (TernaryTerm Id
i tag
_ Term arg1
_ Term arg2
_ Term arg3
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (NotTerm Id
i Term Bool
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (OrTerm Id
i Term Bool
_ Term Bool
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (AndTerm Id
i Term Bool
_ Term Bool
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (EqvTerm Id
i Term t1
_ Term t1
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ITETerm Id
i Term Bool
_ Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (AddNumTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (UMinusNumTerm Id
i Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (TimesNumTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (AbsNumTerm Id
i Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (SignumNumTerm Id
i Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (LTNumTerm Id
i Term t1
_ Term t1
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (LENumTerm Id
i Term t1
_ Term t1
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (AndBitsTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (OrBitsTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (XorBitsTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ComplementBitsTerm Id
i Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ShiftLeftTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ShiftRightTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (RotateLeftTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (RotateRightTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ToSignedTerm Id
i Term u
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ToUnsignedTerm Id
i Term s
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (BVConcatTerm Id
i Term (bv a)
_ Term (bv b)
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (BVSelectTerm Id
i TypeRep ix
_ TypeRep w
_ Term (bv n)
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (BVExtendTerm Id
i Bool
_ TypeRep r
_ Term (bv l)
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (TabularFunApplyTerm Id
i Term (a =-> t)
_ Term a
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (GeneralFunApplyTerm Id
i Term (a --> t)
_ Term a
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (DivIntegralTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ModIntegralTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (QuotIntegralTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (RemIntegralTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (DivBoundedIntegralTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ModBoundedIntegralTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (QuotBoundedIntegralTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (RemBoundedIntegralTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
{-# INLINE identityWithTypeRep #-}

introSupportedPrimConstraint :: forall t a. Term t -> ((SupportedPrim t) => a) -> a
introSupportedPrimConstraint :: forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint ConTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint SymTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint UnaryTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint BinaryTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint TernaryTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint NotTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint OrTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint AndTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint EqvTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint ITETerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint AddNumTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint UMinusNumTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint TimesNumTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint AbsNumTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint SignumNumTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint LTNumTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint LENumTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint AndBitsTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint OrBitsTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint XorBitsTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint ComplementBitsTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint ShiftLeftTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint RotateLeftTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint ShiftRightTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint RotateRightTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint ToSignedTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint ToUnsignedTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint BVConcatTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint BVSelectTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint BVExtendTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint TabularFunApplyTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint GeneralFunApplyTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint DivIntegralTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint ModIntegralTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint QuotIntegralTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint RemIntegralTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint DivBoundedIntegralTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint ModBoundedIntegralTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint QuotBoundedIntegralTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint RemBoundedIntegralTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
{-# INLINE introSupportedPrimConstraint #-}

extractSymbolicsSomeTerm :: SomeTerm -> S.HashSet SomeTypedSymbol
extractSymbolicsSomeTerm :: SomeTerm -> HashSet SomeTypedSymbol
extractSymbolicsSomeTerm SomeTerm
t1 = State
  (HashMap SomeTerm (HashSet SomeTypedSymbol))
  (HashSet SomeTypedSymbol)
-> HashMap SomeTerm (HashSet SomeTypedSymbol)
-> HashSet SomeTypedSymbol
forall s a. State s a -> s -> a
evalState (SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached SomeTerm
t1) HashMap SomeTerm (HashSet SomeTypedSymbol)
forall k v. HashMap k v
M.empty
  where
    gocached :: SomeTerm -> State (M.HashMap SomeTerm (S.HashSet SomeTypedSymbol)) (S.HashSet SomeTypedSymbol)
    gocached :: SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached SomeTerm
t = do
      Maybe (HashSet SomeTypedSymbol)
v <- (HashMap SomeTerm (HashSet SomeTypedSymbol)
 -> Maybe (HashSet SomeTypedSymbol))
-> StateT
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     Identity
     (Maybe (HashSet SomeTypedSymbol))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SomeTerm
-> HashMap SomeTerm (HashSet SomeTypedSymbol)
-> Maybe (HashSet SomeTypedSymbol)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup SomeTerm
t)
      case Maybe (HashSet SomeTypedSymbol)
v of
        Just HashSet SomeTypedSymbol
x -> HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a.
a -> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return HashSet SomeTypedSymbol
x
        Maybe (HashSet SomeTypedSymbol)
Nothing -> do
          HashSet SomeTypedSymbol
res <- SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
go SomeTerm
t
          HashMap SomeTerm (HashSet SomeTypedSymbol)
st <- StateT
  (HashMap SomeTerm (HashSet SomeTypedSymbol))
  Identity
  (HashMap SomeTerm (HashSet SomeTypedSymbol))
forall s (m :: * -> *). MonadState s m => m s
get
          HashMap SomeTerm (HashSet SomeTypedSymbol)
-> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (HashMap SomeTerm (HashSet SomeTypedSymbol)
 -> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity ())
-> HashMap SomeTerm (HashSet SomeTypedSymbol)
-> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity ()
forall a b. (a -> b) -> a -> b
$ SomeTerm
-> HashSet SomeTypedSymbol
-> HashMap SomeTerm (HashSet SomeTypedSymbol)
-> HashMap SomeTerm (HashSet SomeTypedSymbol)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert SomeTerm
t HashSet SomeTypedSymbol
res HashMap SomeTerm (HashSet SomeTypedSymbol)
st
          HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a.
a -> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return HashSet SomeTypedSymbol
res
    go :: SomeTerm -> State (M.HashMap SomeTerm (S.HashSet SomeTypedSymbol)) (S.HashSet SomeTypedSymbol)
    go :: SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
go (SomeTerm ConTerm {}) = HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a.
a -> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return HashSet SomeTypedSymbol
forall a. HashSet a
S.empty
    go (SomeTerm (SymTerm Id
_ (TypedSymbol a
sym :: TypedSymbol a))) = HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a.
a -> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (HashSet SomeTypedSymbol
 -> State
      (HashMap SomeTerm (HashSet SomeTypedSymbol))
      (HashSet SomeTypedSymbol))
-> HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a b. (a -> b) -> a -> b
$ SomeTypedSymbol -> HashSet SomeTypedSymbol
forall a. Hashable a => a -> HashSet a
S.singleton (SomeTypedSymbol -> HashSet SomeTypedSymbol)
-> SomeTypedSymbol -> HashSet SomeTypedSymbol
forall a b. (a -> b) -> a -> b
$ TypeRep a -> TypedSymbol a -> SomeTypedSymbol
forall t. TypeRep t -> TypedSymbol t -> SomeTypedSymbol
SomeTypedSymbol (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) TypedSymbol a
sym
    go (SomeTerm (UnaryTerm Id
_ tag
_ Term arg
arg)) = Term arg
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term arg
arg
    go (SomeTerm (BinaryTerm Id
_ tag
_ Term arg1
arg1 Term arg2
arg2)) = Term arg1
-> Term arg2
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term arg1
arg1 Term arg2
arg2
    go (SomeTerm (TernaryTerm Id
_ tag
_ Term arg1
arg1 Term arg2
arg2 Term arg3
arg3)) = Term arg1
-> Term arg2
-> Term arg3
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a} {a}.
(SupportedPrim a, SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goTernary Term arg1
arg1 Term arg2
arg2 Term arg3
arg3
    go (SomeTerm (NotTerm Id
_ Term Bool
arg)) = Term Bool
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term Bool
arg
    go (SomeTerm (OrTerm Id
_ Term Bool
arg1 Term Bool
arg2)) = Term Bool
-> Term Bool
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term Bool
arg1 Term Bool
arg2
    go (SomeTerm (AndTerm Id
_ Term Bool
arg1 Term Bool
arg2)) = Term Bool
-> Term Bool
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term Bool
arg1 Term Bool
arg2
    go (SomeTerm (EqvTerm Id
_ Term t1
arg1 Term t1
arg2)) = Term t1
-> Term t1
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term t1
arg1 Term t1
arg2
    go (SomeTerm (ITETerm Id
_ Term Bool
cond Term a
arg1 Term a
arg2)) = Term Bool
-> Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a} {a}.
(SupportedPrim a, SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goTernary Term Bool
cond Term a
arg1 Term a
arg2
    go (SomeTerm (AddNumTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (UMinusNumTerm Id
_ Term a
arg)) = Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term a
arg
    go (SomeTerm (TimesNumTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (AbsNumTerm Id
_ Term a
arg)) = Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term a
arg
    go (SomeTerm (SignumNumTerm Id
_ Term a
arg)) = Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term a
arg
    go (SomeTerm (LTNumTerm Id
_ Term t1
arg1 Term t1
arg2)) = Term t1
-> Term t1
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term t1
arg1 Term t1
arg2
    go (SomeTerm (LENumTerm Id
_ Term t1
arg1 Term t1
arg2)) = Term t1
-> Term t1
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term t1
arg1 Term t1
arg2
    go (SomeTerm (AndBitsTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (OrBitsTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (XorBitsTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (ComplementBitsTerm Id
_ Term a
arg)) = Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term a
arg
    go (SomeTerm (ShiftLeftTerm Id
_ Term a
arg Term a
n1)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg Term a
n1
    go (SomeTerm (ShiftRightTerm Id
_ Term a
arg Term a
n1)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg Term a
n1
    go (SomeTerm (RotateLeftTerm Id
_ Term a
arg Term a
n1)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg Term a
n1
    go (SomeTerm (RotateRightTerm Id
_ Term a
arg Term a
n1)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg Term a
n1
    go (SomeTerm (ToSignedTerm Id
_ Term u
arg)) = Term u
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term u
arg
    go (SomeTerm (ToUnsignedTerm Id
_ Term s
arg)) = Term s
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term s
arg
    go (SomeTerm (BVConcatTerm Id
_ Term (bv a)
arg1 Term (bv b)
arg2)) = Term (bv a)
-> Term (bv b)
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term (bv a)
arg1 Term (bv b)
arg2
    go (SomeTerm (BVSelectTerm Id
_ TypeRep ix
_ TypeRep w
_ Term (bv n)
arg)) = Term (bv n)
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term (bv n)
arg
    go (SomeTerm (BVExtendTerm Id
_ Bool
_ TypeRep r
_ Term (bv l)
arg)) = Term (bv l)
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term (bv l)
arg
    go (SomeTerm (TabularFunApplyTerm Id
_ Term (a =-> a)
func Term a
arg)) = Term (a =-> a)
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term (a =-> a)
func Term a
arg
    go (SomeTerm (GeneralFunApplyTerm Id
_ Term (a --> a)
func Term a
arg)) = Term (a --> a)
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term (a --> a)
func Term a
arg
    go (SomeTerm (DivIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (ModIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (QuotIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (RemIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (DivBoundedIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (ModBoundedIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (QuotBoundedIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (RemBoundedIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    goUnary :: Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term a
arg = SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg)
    goBinary :: Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2 = do
      HashSet SomeTypedSymbol
r1 <- SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg1)
      HashSet SomeTypedSymbol
r2 <- SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg2)
      HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a.
a -> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (HashSet SomeTypedSymbol
 -> State
      (HashMap SomeTerm (HashSet SomeTypedSymbol))
      (HashSet SomeTypedSymbol))
-> HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a b. (a -> b) -> a -> b
$ HashSet SomeTypedSymbol
r1 HashSet SomeTypedSymbol
-> HashSet SomeTypedSymbol -> HashSet SomeTypedSymbol
forall a. Semigroup a => a -> a -> a
<> HashSet SomeTypedSymbol
r2
    goTernary :: Term a
-> Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goTernary Term a
arg1 Term a
arg2 Term a
arg3 = do
      HashSet SomeTypedSymbol
r1 <- SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg1)
      HashSet SomeTypedSymbol
r2 <- SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg2)
      HashSet SomeTypedSymbol
r3 <- SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg3)
      HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a.
a -> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (HashSet SomeTypedSymbol
 -> State
      (HashMap SomeTerm (HashSet SomeTypedSymbol))
      (HashSet SomeTypedSymbol))
-> HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a b. (a -> b) -> a -> b
$ HashSet SomeTypedSymbol
r1 HashSet SomeTypedSymbol
-> HashSet SomeTypedSymbol -> HashSet SomeTypedSymbol
forall a. Semigroup a => a -> a -> a
<> HashSet SomeTypedSymbol
r2 HashSet SomeTypedSymbol
-> HashSet SomeTypedSymbol -> HashSet SomeTypedSymbol
forall a. Semigroup a => a -> a -> a
<> HashSet SomeTypedSymbol
r3
{-# INLINEABLE extractSymbolicsSomeTerm #-}

extractSymbolicsTerm :: (SupportedPrim a) => Term a -> S.HashSet SomeTypedSymbol
extractSymbolicsTerm :: forall a. SupportedPrim a => Term a -> HashSet SomeTypedSymbol
extractSymbolicsTerm Term a
t = SomeTerm -> HashSet SomeTypedSymbol
extractSymbolicsSomeTerm (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t)
{-# INLINE extractSymbolicsTerm #-}

castTerm :: forall a b. (Typeable b) => Term a -> Maybe (Term b)
castTerm :: forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm t :: Term a
t@ConTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@SymTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@UnaryTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@BinaryTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@TernaryTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@NotTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@OrTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@AndTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@EqvTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ITETerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@AddNumTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@UMinusNumTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@TimesNumTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@AbsNumTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@SignumNumTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@LTNumTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@LENumTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@AndBitsTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@OrBitsTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@XorBitsTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ComplementBitsTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ShiftLeftTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ShiftRightTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@RotateLeftTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@RotateRightTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ToSignedTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ToUnsignedTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@BVConcatTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@BVSelectTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@BVExtendTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@TabularFunApplyTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@GeneralFunApplyTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@DivIntegralTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ModIntegralTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@QuotIntegralTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@RemIntegralTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@DivBoundedIntegralTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ModBoundedIntegralTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@QuotBoundedIntegralTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@RemBoundedIntegralTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
{-# INLINE castTerm #-}

pformat :: forall t. (SupportedPrim t) => Term t -> String
pformat :: forall t. SupportedPrim t => Term t -> String
pformat (ConTerm Id
_ t
t) = t -> String
forall t. SupportedPrim t => t -> String
pformatCon t
t
pformat (SymTerm Id
_ TypedSymbol t
sym) = TypedSymbol t -> String
forall t. SupportedPrim t => TypedSymbol t -> String
pformatSym TypedSymbol t
sym
pformat (UnaryTerm Id
_ tag
tag Term arg
arg1) = tag -> Term arg -> String
forall tag arg t. UnaryOp tag arg t => tag -> Term arg -> String
pformatUnary tag
tag Term arg
arg1
pformat (BinaryTerm Id
_ tag
tag Term arg1
arg1 Term arg2
arg2) = tag -> Term arg1 -> Term arg2 -> String
forall tag arg1 arg2 t.
BinaryOp tag arg1 arg2 t =>
tag -> Term arg1 -> Term arg2 -> String
pformatBinary tag
tag Term arg1
arg1 Term arg2
arg2
pformat (TernaryTerm Id
_ tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) = tag -> Term arg1 -> Term arg2 -> Term arg3 -> String
forall tag arg1 arg2 arg3 t.
TernaryOp tag arg1 arg2 arg3 t =>
tag -> Term arg1 -> Term arg2 -> Term arg3 -> String
pformatTernary tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3
pformat (NotTerm Id
_ Term Bool
arg) = String
"(! " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Bool
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (OrTerm Id
_ Term Bool
arg1 Term Bool
arg2) = String
"(|| " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Bool
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Bool
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (AndTerm Id
_ Term Bool
arg1 Term Bool
arg2) = String
"(&& " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Bool
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Bool
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (EqvTerm Id
_ Term t1
arg1 Term t1
arg2) = String
"(= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t1 -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t1 -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ITETerm Id
_ Term Bool
cond Term t
arg1 Term t
arg2) = String
"(ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Bool
cond String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (AddNumTerm Id
_ Term t
arg1 Term t
arg2) = String
"(+ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (UMinusNumTerm Id
_ Term t
arg) = String
"(- " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (TimesNumTerm Id
_ Term t
arg1 Term t
arg2) = String
"(* " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (AbsNumTerm Id
_ Term t
arg) = String
"(abs " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (SignumNumTerm Id
_ Term t
arg) = String
"(signum " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (LTNumTerm Id
_ Term t1
arg1 Term t1
arg2) = String
"(< " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t1 -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t1 -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (LENumTerm Id
_ Term t1
arg1 Term t1
arg2) = String
"(<= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t1 -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t1 -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (AndBitsTerm Id
_ Term t
arg1 Term t
arg2) = String
"(& " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (OrBitsTerm Id
_ Term t
arg1 Term t
arg2) = String
"(| " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (XorBitsTerm Id
_ Term t
arg1 Term t
arg2) = String
"(^ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ComplementBitsTerm Id
_ Term t
arg) = String
"(~ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ShiftLeftTerm Id
_ Term t
arg Term t
n) = String
"(shl " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ShiftRightTerm Id
_ Term t
arg Term t
n) = String
"(shr " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (RotateLeftTerm Id
_ Term t
arg Term t
n) = String
"(rotl " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (RotateRightTerm Id
_ Term t
arg Term t
n) = String
"(rotr " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ToSignedTerm Id
_ Term u
arg) = String
"(u2s " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term u -> String
forall t. SupportedPrim t => Term t -> String
pformat Term u
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ToUnsignedTerm Id
_ Term s
arg) = String
"(s2u " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term s -> String
forall t. SupportedPrim t => Term t -> String
pformat Term s
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (BVConcatTerm Id
_ Term (bv a)
arg1 Term (bv b)
arg2) = String
"(bvconcat " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term (bv a) -> String
forall t. SupportedPrim t => Term t -> String
pformat Term (bv a)
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term (bv b) -> String
forall t. SupportedPrim t => Term t -> String
pformat Term (bv b)
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (BVSelectTerm Id
_ TypeRep ix
ix TypeRep w
w Term (bv n)
arg) = String
"(bvselect " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep ix -> String
forall a. Show a => a -> String
show TypeRep ix
ix String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep w -> String
forall a. Show a => a -> String
show TypeRep w
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term (bv n) -> String
forall t. SupportedPrim t => Term t -> String
pformat Term (bv n)
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (BVExtendTerm Id
_ Bool
signed TypeRep r
n Term (bv l)
arg) =
  (if Bool
signed then String
"(bvsext " else String
"(bvzext ") String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep r -> String
forall a. Show a => a -> String
show TypeRep r
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term (bv l) -> String
forall t. SupportedPrim t => Term t -> String
pformat Term (bv l)
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (TabularFunApplyTerm Id
_ Term (a =-> t)
func Term a
arg) = String
"(apply " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term (a =-> t) -> String
forall t. SupportedPrim t => Term t -> String
pformat Term (a =-> t)
func String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term a -> String
forall t. SupportedPrim t => Term t -> String
pformat Term a
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (GeneralFunApplyTerm Id
_ Term (a --> t)
func Term a
arg) = String
"(apply " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term (a --> t) -> String
forall t. SupportedPrim t => Term t -> String
pformat Term (a --> t)
func String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term a -> String
forall t. SupportedPrim t => Term t -> String
pformat Term a
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (DivIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(div " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ModIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(mod " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (QuotIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(quot " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (RemIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(rem " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (DivBoundedIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(div " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ModBoundedIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(mod " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (QuotBoundedIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(quot " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (RemBoundedIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(rem " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
{-# INLINE pformat #-}

someTermsSize :: [SomeTerm] -> Int
someTermsSize :: [SomeTerm] -> Id
someTermsSize [SomeTerm]
terms = HashSet SomeTerm -> Id
forall a. HashSet a -> Id
S.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
S.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
S.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
S.insert (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t))
    goSome :: SomeTerm -> State (S.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 (S.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@(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@(EqvTerm 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@(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@(UMinusNumTerm 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@(TimesNumTerm 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@(LTNumTerm 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@(LENumTerm 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@(ToSignedTerm Id
_ Term u
arg) = Term b -> Term u -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term u
arg
    go t :: Term b
t@(ToUnsignedTerm Id
_ Term s
arg) = Term b -> Term s -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term s
arg
    go t :: Term b
t@(BVConcatTerm Id
_ Term (bv a)
arg1 Term (bv b)
arg2) = Term b
-> Term (bv a)
-> Term (bv 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 (bv a)
arg1 Term (bv b)
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@(TabularFunApplyTerm Id
_ Term (a =-> b)
func Term a
arg) = Term b
-> Term (a =-> 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 (a =-> b)
func Term a
arg
    go t :: Term b
t@(GeneralFunApplyTerm Id
_ Term (a --> b)
func Term a
arg) = Term b
-> Term (a --> 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 (a --> b)
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@(DivBoundedIntegralTerm 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@(ModBoundedIntegralTerm 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@(QuotBoundedIntegralTerm 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@(RemBoundedIntegralTerm 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
    goUnary :: forall a b. (SupportedPrim a) => Term a -> Term b -> State (S.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 (S.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 (S.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 #-}

someTermSize :: SomeTerm -> Int
someTermSize :: SomeTerm -> Id
someTermSize SomeTerm
term = [SomeTerm] -> Id
someTermsSize [SomeTerm
term]
{-# INLINE someTermSize #-}

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 #-}

termSize :: Term a -> Int
termSize :: forall t. Term t -> Id
termSize Term a
term = [Term a] -> Id
forall a. [Term a] -> Id
termsSize [Term a
term]
{-# INLINE termSize #-}