{-# 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 (traverse_)
import qualified Data.HashSet as HS
import Grisette.Internal.Core.Data.MemoUtils (htmemo)
import Grisette.Internal.SymPrim.GeneralFun (type (-->) (GeneralFun))
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( IsSymbolKind (SymbolKindConstraint),
    SomeTypedConstantSymbol,
    SomeTypedSymbol (SomeTypedSymbol),
    SupportedPrim (castTypedSymbol, primTypeRep),
    Term,
    TypedAnySymbol,
    someTypedSymbol,
    pattern ConTerm,
    pattern ExistsTerm,
    pattern ForallTerm,
    pattern SupportedTerm,
    pattern SymTerm,
  )
import Grisette.Internal.SymPrim.Prim.Pattern (pattern SubTerms)
import Grisette.Internal.SymPrim.Prim.SomeTerm
  ( SomeTerm (SomeTerm),
    someTerm,
  )
import Type.Reflection
  ( TypeRep,
    Typeable,
    eqTypeRep,
    typeRep,
    pattern App,
    type (:~~:) (HRefl),
  )

{-# NOINLINE extractSymSomeTerm #-}
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
initialBounded = (SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
initialMemo HashSet SomeTypedConstantSymbol
initialBounded
  where
    gotyped ::
      ( SomeTerm ->
        Maybe (HS.HashSet (SomeTypedSymbol knd))
      ) ->
      Term a ->
      Maybe (HS.HashSet (SomeTypedSymbol knd))
    gotyped :: forall a.
(SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> Term a -> Maybe (HashSet (SomeTypedSymbol knd))
gotyped SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo Term a
a = SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo (Term a -> SomeTerm
forall a. Term a -> SomeTerm
someTerm Term a
a)
    initialMemo ::
      SomeTerm ->
      Maybe (HS.HashSet (SomeTypedSymbol knd))
    initialMemo :: SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
initialMemo = (SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo ((SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
initialMemo HashSet SomeTypedConstantSymbol
initialBounded)
    {-# NOINLINE initialMemo #-}

    go ::
      ( SomeTerm ->
        Maybe (HS.HashSet (SomeTypedSymbol knd))
      ) ->
      HS.HashSet (SomeTypedConstantSymbol) ->
      SomeTerm ->
      Maybe (HS.HashSet (SomeTypedSymbol knd))
    go :: (SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (SymTerm (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
$ TypedSymbol knd a -> SomeTypedSymbol knd
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
SomeTypedSymbol TypedSymbol knd a
sym'
        (Maybe (TypedSymbol 'ConstantKind a), Maybe (TypedSymbol knd a))
_ -> Maybe (HashSet (SomeTypedSymbol knd))
forall a. Maybe a
Nothing
    go SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (ConTerm a
cv :: Term v)) =
      case (TypeRep a
forall t. SupportedPrim t => TypeRep t
primTypeRep :: TypeRep v) of
        App (App TypeRep a
gf TypeRep b
_) TypeRep b
_ ->
          case TypeRep (-->) -> TypeRep a -> Maybe ((-->) :~~: a)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> *). Typeable a => TypeRep a
typeRep @(-->)) TypeRep a
gf of
            Just (-->) :~~: a
HRefl -> case a
cv of
              GeneralFun TypedConstantSymbol b
sym (Term b
tm :: Term r) ->
                let newBounded :: HashSet SomeTypedConstantSymbol
newBounded = 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
                    newmemo :: SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo = (SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo ((SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo HashSet SomeTypedConstantSymbol
newBounded)
                    {-# NOINLINE newmemo #-}
                 in (SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> Term b -> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
(SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> Term a -> Maybe (HashSet (SomeTypedSymbol knd))
gotyped SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo 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 SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (ForallTerm TypedSymbol 'ConstantKind t
sym Term Bool
arg)) =
      let newBounded :: HashSet SomeTypedConstantSymbol
newBounded = SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HS.insert (TypedSymbol 'ConstantKind t -> SomeTypedConstantSymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedSymbol 'ConstantKind t
sym) HashSet SomeTypedConstantSymbol
bs
          newmemo :: SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo = (SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo ((SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo HashSet SomeTypedConstantSymbol
newBounded)
          {-# NOINLINE newmemo #-}
       in (SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> Term Bool -> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
(SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> Term a -> Maybe (HashSet (SomeTypedSymbol knd))
gotyped SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo Term Bool
arg
    go SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (ExistsTerm TypedSymbol 'ConstantKind t
sym Term Bool
arg)) =
      let newBounded :: HashSet SomeTypedConstantSymbol
newBounded = SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HS.insert (TypedSymbol 'ConstantKind t -> SomeTypedConstantSymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedSymbol 'ConstantKind t
sym) HashSet SomeTypedConstantSymbol
bs
          newmemo :: SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo = (SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo ((SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo HashSet SomeTypedConstantSymbol
newBounded)
          {-# NOINLINE newmemo #-}
       in (SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> Term Bool -> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
(SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> Term a -> Maybe (HashSet (SomeTypedSymbol knd))
gotyped SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo Term Bool
arg
    go SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (SubTerms [SomeTerm]
ts)) = [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
$ (SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> [SomeTerm] -> [Maybe (HashSet (SomeTypedSymbol knd))]
forall a b. (a -> b) -> [a] -> [b]
map SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo [SomeTerm]
ts
    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

-- | 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)
{-# NOINLINE 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 t :: Term a
t@Term a
SupportedTerm = 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] -> Int
someTermsSize [SomeTerm]
terms = HashSet SomeTerm -> Int
forall a. HashSet a -> Int
HS.size (HashSet SomeTerm -> Int) -> HashSet SomeTerm -> Int
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. 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. 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 =>
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 =>
Term a -> m ()
add Term b
t
    go t :: Term b
t@(SubTerms [SomeTerm]
ts) = do
      b <- Term b -> StateT (HashSet SomeTerm) Identity Bool
forall {m :: * -> *} {a}.
MonadState (HashSet SomeTerm) m =>
Term a -> m Bool
exists Term b
t
      if b
        then return ()
        else do
          add t
          traverse_ goSome ts
{-# INLINEABLE someTermsSize #-}

-- | Compute the size of a list of terms. Do not count the same term twice.
someTermSize :: SomeTerm -> Int
someTermSize :: SomeTerm -> Int
someTermSize SomeTerm
term = [SomeTerm] -> Int
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] -> Int
termsSize [Term a]
terms = [SomeTerm] -> Int
someTermsSize ([SomeTerm] -> Int) -> [SomeTerm] -> Int
forall a b. (a -> b) -> a -> b
$ Term a -> SomeTerm
forall a. Term a -> SomeTerm
someTerm (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 -> Int
termSize Term a
term = [Term a] -> Int
forall a. [Term a] -> Int
termsSize [Term a
term]
{-# INLINE termSize #-}