{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
-- 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.Term
  ( SupportedPrim (..),
    SymRep (..),
    ConRep (..),
    LinkedRep (..),
    UnaryOp (..),
    BinaryOp (..),
    TernaryOp (..),
    TypedSymbol (..),
    SomeTypedSymbol (..),
    showUntyped,
    withSymbolSupported,
    someTypedSymbol,
    Term (..),
    UTerm (..),
    type (-->) (..),
    buildGeneralFun,
  )
where

import Control.DeepSeq
import Data.Bits
import Data.Function (on)
import Data.Hashable
import Data.Interned
import Data.Kind
import Data.String
import Data.Typeable (Proxy (..), cast)
import GHC.Generics
import GHC.TypeNats
import Grisette.Core.Data.BV
import Grisette.Core.Data.Class.BitVector
import Grisette.Core.Data.Class.Function
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
import Grisette.IR.SymPrim.Data.Prim.ModelValue
import Grisette.IR.SymPrim.Data.Prim.Utils
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.TabularFun
import Language.Haskell.TH.Syntax
import Language.Haskell.TH.Syntax.Compat
import Type.Reflection

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.IR.SymPrim

-- | Indicates that a type is supported and can be represented as a symbolic
-- term.
class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where
  type PrimConstraint t :: Constraint
  type PrimConstraint t = ()
  default withPrim :: (PrimConstraint t) => proxy t -> ((PrimConstraint t) => a) -> a
  withPrim :: proxy t -> ((PrimConstraint t) => a) -> a
  withPrim proxy t
_ PrimConstraint t => a
i = PrimConstraint t => a
i
  termCache :: Cache (Term t)
  termCache = forall a. (Interned a, Typeable a) => Cache a
typeMemoizedCache
  pformatCon :: t -> String
  default pformatCon :: (Show t) => t -> String
  pformatCon = forall a. Show a => a -> String
show
  pformatSym :: TypedSymbol t -> String
  pformatSym = forall t. TypedSymbol t -> String
showUntyped
  defaultValue :: t
  defaultValueDynamic :: proxy t -> ModelValue
  defaultValueDynamic proxy t
_ = forall a. (Show a, Eq a, Hashable a, Typeable a) => a -> ModelValue
toModelValue (forall t. SupportedPrim t => t
defaultValue @t)

-- | Type family to resolve the concrete type associated with a symbolic type.
class ConRep sym where
  type ConType sym

-- | Type family to resolve the symbolic type associated with a concrete type.
class (SupportedPrim con) => SymRep con where
  type SymType con

-- | One-to-one mapping between symbolic types and concrete types.
class
  (ConRep sym, SymRep con, sym ~ SymType con, con ~ ConType sym) =>
  LinkedRep con sym
    | con -> sym,
      sym -> con
  where
  underlyingTerm :: sym -> Term con
  wrapTerm :: Term con -> sym

class
  (SupportedPrim arg, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) =>
  UnaryOp tag arg t
    | tag arg -> t
  where
  partialEvalUnary :: (Typeable tag, Typeable t) => tag -> Term arg -> Term t
  pformatUnary :: tag -> Term arg -> String

class
  ( SupportedPrim arg1,
    SupportedPrim arg2,
    SupportedPrim t,
    Lift tag,
    NFData tag,
    Show tag,
    Typeable tag,
    Eq tag,
    Hashable tag
  ) =>
  BinaryOp tag arg1 arg2 t
    | tag arg1 arg2 -> t
  where
  partialEvalBinary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term t
  pformatBinary :: tag -> Term arg1 -> Term arg2 -> String

class
  ( SupportedPrim arg1,
    SupportedPrim arg2,
    SupportedPrim arg3,
    SupportedPrim t,
    Lift tag,
    NFData tag,
    Show tag,
    Typeable tag,
    Eq tag,
    Hashable tag
  ) =>
  TernaryOp tag arg1 arg2 arg3 t
    | tag arg1 arg2 arg3 -> t
  where
  partialEvalTernary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
  pformatTernary :: tag -> Term arg1 -> Term arg2 -> Term arg3 -> String

-- | A typed symbol is a symbol that is associated with a type. Note that the
-- same symbol bodies with different types are considered different symbols
-- and can coexist in a term.
--
-- Simple symbols can be created with the 'OverloadedStrings' extension:
--
-- >>> :set -XOverloadedStrings
-- >>> "a" :: TypedSymbol Bool
-- a :: Bool
data TypedSymbol t where
  SimpleSymbol :: (SupportedPrim t) => String -> TypedSymbol t
  IndexedSymbol :: (SupportedPrim t) => String -> Int -> TypedSymbol t
  WithInfo ::
    forall t a.
    ( SupportedPrim t,
      Typeable a,
      Ord a,
      Lift a,
      NFData a,
      Show a,
      Hashable a
    ) =>
    TypedSymbol t ->
    a ->
    TypedSymbol t

-- deriving (Eq, Ord, Generic, Lift, NFData)

instance Eq (TypedSymbol t) where
  SimpleSymbol String
x == :: TypedSymbol t -> TypedSymbol t -> Bool
== SimpleSymbol String
y = String
x forall a. Eq a => a -> a -> Bool
== String
y
  IndexedSymbol String
x Int
i == IndexedSymbol String
y Int
j = Int
i forall a. Eq a => a -> a -> Bool
== Int
j Bool -> Bool -> Bool
&& String
x forall a. Eq a => a -> a -> Bool
== String
y
  WithInfo TypedSymbol t
s1 (a
i1 :: a) == WithInfo TypedSymbol t
s2 (a
i2 :: b) = case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b) of
    Just a :~~: a
HRefl -> a
i1 forall a. Eq a => a -> a -> Bool
== a
i2 Bool -> Bool -> Bool
&& TypedSymbol t
s1 forall a. Eq a => a -> a -> Bool
== TypedSymbol t
s2
    Maybe (a :~~: a)
_ -> Bool
False
  TypedSymbol t
_ == TypedSymbol t
_ = Bool
False

instance Ord (TypedSymbol t) where
  SimpleSymbol String
x <= :: TypedSymbol t -> TypedSymbol t -> Bool
<= SimpleSymbol String
y = String
x forall a. Ord a => a -> a -> Bool
<= String
y
  IndexedSymbol String
x Int
i <= IndexedSymbol String
y Int
j = Int
i forall a. Ord a => a -> a -> Bool
< Int
j Bool -> Bool -> Bool
|| (Int
i forall a. Eq a => a -> a -> Bool
== Int
j Bool -> Bool -> Bool
&& String
x forall a. Ord a => a -> a -> Bool
<= String
y)
  WithInfo TypedSymbol t
s1 (a
i1 :: a) <= WithInfo TypedSymbol t
s2 (a
i2 :: b) = case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b) of
    Just a :~~: a
HRefl -> TypedSymbol t
s1 forall a. Ord a => a -> a -> Bool
< TypedSymbol t
s2 Bool -> Bool -> Bool
|| (TypedSymbol t
s1 forall a. Eq a => a -> a -> Bool
== TypedSymbol t
s2 Bool -> Bool -> Bool
&& a
i1 forall a. Ord a => a -> a -> Bool
<= a
i2)
    Maybe (a :~~: a)
_ -> Bool
False
  TypedSymbol t
_ <= TypedSymbol t
_ = Bool
False

instance Lift (TypedSymbol t) where
  liftTyped :: forall (m :: * -> *).
Quote m =>
TypedSymbol t -> Code m (TypedSymbol t)
liftTyped (SimpleSymbol String
x) = [||SimpleSymbol x||]
  liftTyped (IndexedSymbol String
x Int
i) = [||IndexedSymbol x i||]
  liftTyped (WithInfo TypedSymbol t
s1 a
i1) = [||WithInfo s1 i1||]

instance Show (TypedSymbol t) where
  show :: TypedSymbol t -> String
show (SimpleSymbol String
str) = String
str forall a. [a] -> [a] -> [a]
++ String
" :: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t)
  show (IndexedSymbol String
str Int
i) = String
str forall a. [a] -> [a] -> [a]
++ String
"@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" :: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t)
  show (WithInfo TypedSymbol t
s a
info) = forall t. TypedSymbol t -> String
showUntyped TypedSymbol t
s forall a. [a] -> [a] -> [a]
++ String
":" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
info forall a. [a] -> [a] -> [a]
++ String
" :: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t)

showUntyped :: TypedSymbol t -> String
showUntyped :: forall t. TypedSymbol t -> String
showUntyped (SimpleSymbol String
str) = String
str
showUntyped (IndexedSymbol String
str Int
i) = String
str forall a. [a] -> [a] -> [a]
++ String
"@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
showUntyped (WithInfo TypedSymbol t
s a
info) = forall t. TypedSymbol t -> String
showUntyped TypedSymbol t
s forall a. [a] -> [a] -> [a]
++ String
":" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
info

instance Hashable (TypedSymbol t) where
  Int
s hashWithSalt :: Int -> TypedSymbol t -> Int
`hashWithSalt` SimpleSymbol String
x = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` String
x
  Int
s `hashWithSalt` IndexedSymbol String
x Int
i = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` String
x forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
i
  Int
s `hashWithSalt` WithInfo TypedSymbol t
sym a
info = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol t
sym forall a. Hashable a => Int -> a -> Int
`hashWithSalt` a
info

instance NFData (TypedSymbol t) where
  rnf :: TypedSymbol t -> ()
rnf (SimpleSymbol String
str) = forall a. NFData a => a -> ()
rnf String
str
  rnf (IndexedSymbol String
str Int
i) = forall a. NFData a => a -> ()
rnf String
str seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Int
i
  rnf (WithInfo TypedSymbol t
s a
info) = forall a. NFData a => a -> ()
rnf TypedSymbol t
s seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf a
info

instance (SupportedPrim t) => IsString (TypedSymbol t) where
  fromString :: String -> TypedSymbol t
fromString = forall t. SupportedPrim t => String -> TypedSymbol t
SimpleSymbol

withSymbolSupported :: TypedSymbol t -> ((SupportedPrim t) => a) -> a
withSymbolSupported :: forall t a. TypedSymbol t -> (SupportedPrim t => a) -> a
withSymbolSupported (SimpleSymbol String
_) SupportedPrim t => a
a = SupportedPrim t => a
a
withSymbolSupported (IndexedSymbol String
_ Int
_) SupportedPrim t => a
a = SupportedPrim t => a
a
withSymbolSupported (WithInfo TypedSymbol t
_ a
_) SupportedPrim t => a
a = SupportedPrim t => a
a

{-
data TypedSymbol t where
  TypedSymbol :: (SupportedPrim t) => Symbol -> TypedSymbol t

typedSymbol :: forall proxy t. (SupportedPrim t) => proxy t -> Symbol -> TypedSymbol t
typedSymbol _ = TypedSymbol

instance NFData (TypedSymbol t) where
  rnf (TypedSymbol s) = rnf s

instance Eq (TypedSymbol t) where
  (TypedSymbol s1) == (TypedSymbol s2) = s1 == s2

instance Ord (TypedSymbol t) where
  (TypedSymbol s1) <= (TypedSymbol s2) = s1 <= s2

instance Hashable (TypedSymbol t) where
  hashWithSalt s (TypedSymbol s1) = s `hashWithSalt` s1

instance Show (TypedSymbol t) where
  show (TypedSymbol s) = show s ++ " :: " ++ show (typeRep @t)

instance Lift (TypedSymbol t) where
  liftTyped (TypedSymbol s) = [||TypedSymbol s||]
  -}

data SomeTypedSymbol where
  SomeTypedSymbol :: forall t. TypeRep t -> TypedSymbol t -> SomeTypedSymbol

instance NFData SomeTypedSymbol where
  rnf :: SomeTypedSymbol -> ()
rnf (SomeTypedSymbol TypeRep t
p TypedSymbol t
s) = forall a. NFData a => a -> ()
rnf (forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep t
p) seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf TypedSymbol t
s

instance Eq SomeTypedSymbol where
  (SomeTypedSymbol TypeRep t
t1 TypedSymbol t
s1) == :: SomeTypedSymbol -> SomeTypedSymbol -> Bool
== (SomeTypedSymbol TypeRep t
t2 TypedSymbol t
s2) = case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep t
t1 TypeRep t
t2 of
    Just t :~~: t
HRefl -> TypedSymbol t
s1 forall a. Eq a => a -> a -> Bool
== TypedSymbol t
s2
    Maybe (t :~~: t)
_ -> Bool
False

instance Ord SomeTypedSymbol where
  (SomeTypedSymbol TypeRep t
t1 TypedSymbol t
s1) <= :: SomeTypedSymbol -> SomeTypedSymbol -> Bool
<= (SomeTypedSymbol TypeRep t
t2 TypedSymbol t
s2) =
    forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep t
t1 forall a. Ord a => a -> a -> Bool
< forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep t
t2
      Bool -> Bool -> Bool
|| ( case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep t
t1 TypeRep t
t2 of
             Just t :~~: t
HRefl -> TypedSymbol t
s1 forall a. Ord a => a -> a -> Bool
<= TypedSymbol t
s2
             Maybe (t :~~: t)
_ -> Bool
False
         )

instance Hashable SomeTypedSymbol where
  hashWithSalt :: Int -> SomeTypedSymbol -> Int
hashWithSalt Int
s (SomeTypedSymbol TypeRep t
t1 TypedSymbol t
s1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol t
s1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep t
t1

instance Show SomeTypedSymbol where
  show :: SomeTypedSymbol -> String
show (SomeTypedSymbol TypeRep t
_ TypedSymbol t
s) = forall a. Show a => a -> String
show TypedSymbol t
s

someTypedSymbol :: forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol :: forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol s :: TypedSymbol t
s@(SimpleSymbol String
_) = forall a. TypeRep a -> TypedSymbol a -> SomeTypedSymbol
SomeTypedSymbol (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t) TypedSymbol t
s
someTypedSymbol s :: TypedSymbol t
s@(IndexedSymbol String
_ Int
_) = forall a. TypeRep a -> TypedSymbol a -> SomeTypedSymbol
SomeTypedSymbol (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t) TypedSymbol t
s
someTypedSymbol s :: TypedSymbol t
s@(WithInfo TypedSymbol t
_ a
_) = forall a. TypeRep a -> TypedSymbol a -> SomeTypedSymbol
SomeTypedSymbol (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t) TypedSymbol t
s

data Term t where
  ConTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !t -> Term t
  SymTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(TypedSymbol t) -> Term t
  UnaryTerm ::
    (UnaryOp tag arg t) =>
    {-# UNPACK #-} !Id ->
    !tag ->
    !(Term arg) ->
    Term t
  BinaryTerm ::
    (BinaryOp tag arg1 arg2 t) =>
    {-# UNPACK #-} !Id ->
    !tag ->
    !(Term arg1) ->
    !(Term arg2) ->
    Term t
  TernaryTerm ::
    (TernaryOp tag arg1 arg2 arg3 t) =>
    {-# UNPACK #-} !Id ->
    !tag ->
    !(Term arg1) ->
    !(Term arg2) ->
    !(Term arg3) ->
    Term t
  NotTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> Term Bool
  OrTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
  AndTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
  EqvTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
  ITETerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t
  AddNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  UMinusNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
  TimesNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  AbsNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
  SignumNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
  LTNumTerm :: (SupportedPrim t, Num t, Ord t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
  LENumTerm :: (SupportedPrim t, Num t, Ord t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
  AndBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  OrBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  XorBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  ComplementBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
  ShiftBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> {-# UNPACK #-} !Int -> Term t
  RotateBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> {-# UNPACK #-} !Int -> Term t
  BVToSignedTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
      Typeable ubv,
      Typeable sbv,
      KnownNat n,
      1 <= n,
      BVSignConversion (ubv n) (sbv n)
    ) =>
    {-# UNPACK #-} !Id ->
    !(Term (ubv n)) ->
    Term (sbv n)
  BVToUnsignedTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
      Typeable ubv,
      Typeable sbv,
      KnownNat n,
      1 <= n,
      BVSignConversion (ubv n) (sbv n)
    ) =>
    {-# UNPACK #-} !Id ->
    !(Term (sbv n)) ->
    Term (ubv n)
  BVConcatTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
      Typeable bv,
      KnownNat a,
      KnownNat b,
      KnownNat (a + b),
      1 <= a,
      1 <= b,
      1 <= a + b,
      SizedBV bv
    ) =>
    {-# UNPACK #-} !Id ->
    !(Term (bv a)) ->
    !(Term (bv b)) ->
    Term (bv (a + b))
  BVSelectTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
      Typeable bv,
      KnownNat n,
      KnownNat ix,
      KnownNat w,
      1 <= n,
      1 <= w,
      ix + w <= n,
      SizedBV bv
    ) =>
    {-# UNPACK #-} !Id ->
    !(TypeRep ix) ->
    !(TypeRep w) ->
    !(Term (bv n)) ->
    Term (bv w)
  BVExtendTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
      Typeable bv,
      KnownNat l,
      KnownNat r,
      1 <= l,
      1 <= r,
      l <= r,
      SizedBV bv
    ) =>
    {-# UNPACK #-} !Id ->
    !Bool ->
    !(TypeRep r) ->
    !(Term (bv l)) ->
    Term (bv r)
  TabularFunApplyTerm ::
    ( SupportedPrim a,
      SupportedPrim b
    ) =>
    {-# UNPACK #-} !Id ->
    Term (a =-> b) ->
    Term a ->
    Term b
  GeneralFunApplyTerm ::
    ( SupportedPrim a,
      SupportedPrim b
    ) =>
    {-# UNPACK #-} !Id ->
    Term (a --> b) ->
    Term a ->
    Term b
  DivIntegralTerm :: (SupportedPrim t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  ModIntegralTerm :: (SupportedPrim t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  QuotIntegralTerm :: (SupportedPrim t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  RemIntegralTerm :: (SupportedPrim t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  DivBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  ModBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  QuotBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  RemBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t

instance NFData (Term a) where
  rnf :: Term a -> ()
rnf Term a
i = forall t. Term t -> Int
identity Term a
i seq :: forall a b. a -> b -> b
`seq` ()

instance Lift (Term t) where
  lift :: forall (m :: * -> *). Quote m => Term t -> m Exp
lift = forall a (m :: * -> *). Quote m => Splice m a -> m Exp
unTypeSplice forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (m :: * -> *). (Lift t, Quote m) => t -> Code m t
liftTyped
  liftTyped :: forall (m :: * -> *). Quote m => Term t -> Code m (Term t)
liftTyped (ConTerm Int
_ t
i) = [||conTerm i||]
  liftTyped (SymTerm Int
_ TypedSymbol t
sym) = [||symTerm sym||]
  liftTyped (UnaryTerm Int
_ tag
tag Term arg
arg) = [||constructUnary tag arg||]
  liftTyped (BinaryTerm Int
_ tag
tag Term arg1
arg1 Term arg2
arg2) = [||constructBinary tag arg1 arg2||]
  liftTyped (TernaryTerm Int
_ tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) = [||constructTernary tag arg1 arg2 arg3||]
  liftTyped (NotTerm Int
_ Term Bool
arg) = [||notTerm arg||]
  liftTyped (OrTerm Int
_ Term Bool
arg1 Term Bool
arg2) = [||orTerm arg1 arg2||]
  liftTyped (AndTerm Int
_ Term Bool
arg1 Term Bool
arg2) = [||andTerm arg1 arg2||]
  liftTyped (EqvTerm Int
_ Term t
arg1 Term t
arg2) = [||eqvTerm arg1 arg2||]
  liftTyped (ITETerm Int
_ Term Bool
cond Term t
arg1 Term t
arg2) = [||iteTerm cond arg1 arg2||]
  liftTyped (AddNumTerm Int
_ Term t
arg1 Term t
arg2) = [||addNumTerm arg1 arg2||]
  liftTyped (UMinusNumTerm Int
_ Term t
arg) = [||uminusNumTerm arg||]
  liftTyped (TimesNumTerm Int
_ Term t
arg1 Term t
arg2) = [||timesNumTerm arg1 arg2||]
  liftTyped (AbsNumTerm Int
_ Term t
arg) = [||absNumTerm arg||]
  liftTyped (SignumNumTerm Int
_ Term t
arg) = [||signumNumTerm arg||]
  liftTyped (LTNumTerm Int
_ Term t
arg1 Term t
arg2) = [||ltNumTerm arg1 arg2||]
  liftTyped (LENumTerm Int
_ Term t
arg1 Term t
arg2) = [||leNumTerm arg1 arg2||]
  liftTyped (AndBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||andBitsTerm arg1 arg2||]
  liftTyped (OrBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||orBitsTerm arg1 arg2||]
  liftTyped (XorBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||xorBitsTerm arg1 arg2||]
  liftTyped (ComplementBitsTerm Int
_ Term t
arg) = [||complementBitsTerm arg||]
  liftTyped (ShiftBitsTerm Int
_ Term t
arg Int
n) = [||shiftBitsTerm arg n||]
  liftTyped (RotateBitsTerm Int
_ Term t
arg Int
n) = [||rotateBitsTerm arg n||]
  liftTyped (BVToSignedTerm Int
_ Term (ubv n)
v) = [||bvToSignedTerm v||]
  liftTyped (BVToUnsignedTerm Int
_ Term (sbv n)
v) = [||bvToUnsignedTerm v||]
  liftTyped (BVConcatTerm Int
_ Term (bv a)
arg1 Term (bv b)
arg2) = [||bvconcatTerm arg1 arg2||]
  liftTyped (BVSelectTerm Int
_ (TypeRep ix
_ :: TypeRep ix) (TypeRep w
_ :: TypeRep w) Term (bv n)
arg) = [||bvselectTerm (Proxy @ix) (Proxy @w) arg||]
  liftTyped (BVExtendTerm Int
_ Bool
signed (TypeRep r
_ :: TypeRep n) Term (bv l)
arg) = [||bvextendTerm signed (Proxy @n) arg||]
  liftTyped (TabularFunApplyTerm Int
_ Term (a =-> t)
func Term a
arg) = [||tabularFunApplyTerm func arg||]
  liftTyped (GeneralFunApplyTerm Int
_ Term (a --> t)
func Term a
arg) = [||generalFunApplyTerm func arg||]
  liftTyped (DivIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||divIntegralTerm arg1 arg2||]
  liftTyped (ModIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||modIntegralTerm arg1 arg2||]
  liftTyped (QuotIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||quotIntegralTerm arg1 arg2||]
  liftTyped (RemIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||remIntegralTerm arg1 arg2||]
  liftTyped (DivBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||divBoundedIntegralTerm arg1 arg2||]
  liftTyped (ModBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||modBoundedIntegralTerm arg1 arg2||]
  liftTyped (QuotBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||quotBoundedIntegralTerm arg1 arg2||]
  liftTyped (RemBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||remBoundedIntegralTerm arg1 arg2||]

instance Show (Term ty) where
  show :: Term ty -> String
show (ConTerm Int
i ty
v) = String
"ConTerm{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", v=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ty
v forall a. [a] -> [a] -> [a]
++ String
"}"
  show (SymTerm Int
i TypedSymbol ty
name) =
    String
"SymTerm{id="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
      forall a. [a] -> [a] -> [a]
++ String
", name="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypedSymbol ty
name
      forall a. [a] -> [a] -> [a]
++ String
", type="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @ty)
      forall a. [a] -> [a] -> [a]
++ String
"}"
  show (UnaryTerm Int
i tag
tag Term arg
arg) = String
"Unary{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", tag=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show tag
tag forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg
arg forall a. [a] -> [a] -> [a]
++ String
"}"
  show (BinaryTerm Int
i tag
tag Term arg1
arg1 Term arg2
arg2) =
    String
"Binary{id="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
      forall a. [a] -> [a] -> [a]
++ String
", tag="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show tag
tag
      forall a. [a] -> [a] -> [a]
++ String
", arg1="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg1
arg1
      forall a. [a] -> [a] -> [a]
++ String
", arg2="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg2
arg2
      forall a. [a] -> [a] -> [a]
++ String
"}"
  show (TernaryTerm Int
i tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) =
    String
"Ternary{id="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
      forall a. [a] -> [a] -> [a]
++ String
", tag="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show tag
tag
      forall a. [a] -> [a] -> [a]
++ String
", arg1="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg1
arg1
      forall a. [a] -> [a] -> [a]
++ String
", arg2="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg2
arg2
      forall a. [a] -> [a] -> [a]
++ String
", arg3="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg3
arg3
      forall a. [a] -> [a] -> [a]
++ String
"}"
  show (NotTerm Int
i Term Bool
arg) = String
"Not{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
arg forall a. [a] -> [a] -> [a]
++ String
"}"
  show (OrTerm Int
i Term Bool
arg1 Term Bool
arg2) = String
"Or{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (AndTerm Int
i Term Bool
arg1 Term Bool
arg2) = String
"And{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (EqvTerm Int
i Term t
arg1 Term t
arg2) = String
"Eqv{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ITETerm Int
i Term Bool
cond Term ty
l Term ty
r) =
    String
"ITE{id="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
      forall a. [a] -> [a] -> [a]
++ String
", cond="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
cond
      forall a. [a] -> [a] -> [a]
++ String
", then="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
l
      forall a. [a] -> [a] -> [a]
++ String
", else="
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
r
      forall a. [a] -> [a] -> [a]
++ String
"}"
  show (AddNumTerm Int
i Term ty
arg1 Term ty
arg2) = String
"AddNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (UMinusNumTerm Int
i Term ty
arg) = String
"UMinusNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
"}"
  show (TimesNumTerm Int
i Term ty
arg1 Term ty
arg2) = String
"TimesNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (AbsNumTerm Int
i Term ty
arg) = String
"AbsNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
"}"
  show (SignumNumTerm Int
i Term ty
arg) = String
"SignumNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
"}"
  show (LTNumTerm Int
i Term t
arg1 Term t
arg2) = String
"LTNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (LENumTerm Int
i Term t
arg1 Term t
arg2) = String
"LENum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (AndBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"AndBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (OrBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"OrBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (XorBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"XorBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ComplementBitsTerm Int
i Term ty
arg) = String
"ComplementBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ShiftBitsTerm Int
i Term ty
arg Int
n) = String
"ShiftBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
", n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
"}"
  show (RotateBitsTerm Int
i Term ty
arg Int
n) = String
"RotateBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
", n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
"}"
  show (BVToSignedTerm Int
i Term (ubv n)
arg) = String
"BVToSigned{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (ubv n)
arg forall a. [a] -> [a] -> [a]
++ String
"}"
  show (BVToUnsignedTerm Int
i Term (sbv n)
arg) = String
"BVToUnsigned{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (sbv n)
arg forall a. [a] -> [a] -> [a]
++ String
"}"
  show (BVConcatTerm Int
i Term (bv a)
arg1 Term (bv b)
arg2) = String
"BVConcat{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (bv a)
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (bv b)
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (BVSelectTerm Int
i TypeRep ix
ix TypeRep w
w Term (bv n)
arg) =
    String
"BVSelect{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", ix=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep ix
ix forall a. [a] -> [a] -> [a]
++ String
", w=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep w
w forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (bv n)
arg forall a. [a] -> [a] -> [a]
++ String
"}"
  show (BVExtendTerm Int
i Bool
signed TypeRep r
n Term (bv l)
arg) =
    String
"BVExtend{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", signed=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Bool
signed forall a. [a] -> [a] -> [a]
++ String
", n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep r
n forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (bv l)
arg forall a. [a] -> [a] -> [a]
++ String
"}"
  show (TabularFunApplyTerm Int
i Term (a =-> ty)
func Term a
arg) =
    String
"TabularFunApply{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", func=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (a =-> ty)
func forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term a
arg forall a. [a] -> [a] -> [a]
++ String
"}"
  show (GeneralFunApplyTerm Int
i Term (a --> ty)
func Term a
arg) =
    String
"GeneralFunApply{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", func=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (a --> ty)
func forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term a
arg forall a. [a] -> [a] -> [a]
++ String
"}"
  show (DivIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"DivIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ModIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"ModIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (QuotIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"QuotIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (RemIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"RemIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (DivBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"DivBoundedIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ModBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"ModBoundedIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (QuotBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"QuotBoundedIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (RemBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"RemBoundedIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"

instance (SupportedPrim t) => Eq (Term t) where
  == :: Term t -> Term t -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall t. Term t -> Int
identity

instance (SupportedPrim t) => Hashable (Term t) where
  hashWithSalt :: Int -> Term t -> Int
hashWithSalt Int
s Term t
t = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s forall a b. (a -> b) -> a -> b
$ forall t. Term t -> Int
identity Term t
t

data UTerm t where
  UConTerm :: (SupportedPrim t) => !t -> UTerm t
  USymTerm :: (SupportedPrim t) => !(TypedSymbol t) -> UTerm t
  UUnaryTerm :: (UnaryOp tag arg t) => !tag -> !(Term arg) -> UTerm t
  UBinaryTerm ::
    (BinaryOp tag arg1 arg2 t) =>
    !tag ->
    !(Term arg1) ->
    !(Term arg2) ->
    UTerm t
  UTernaryTerm ::
    (TernaryOp tag arg1 arg2 arg3 t) =>
    !tag ->
    !(Term arg1) ->
    !(Term arg2) ->
    !(Term arg3) ->
    UTerm t
  UNotTerm :: !(Term Bool) -> UTerm Bool
  UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
  UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
  UEqvTerm :: (SupportedPrim t) => !(Term t) -> !(Term t) -> UTerm Bool
  UITETerm :: (SupportedPrim t) => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t
  UAddNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
  UUMinusNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
  UTimesNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
  UAbsNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
  USignumNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
  ULTNumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool
  ULENumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool
  UAndBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
  UOrBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
  UXorBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
  UComplementBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> UTerm t
  UShiftBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t
  URotateBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t
  UBVToSignedTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
      Typeable ubv,
      Typeable sbv,
      KnownNat n,
      1 <= n,
      BVSignConversion (ubv n) (sbv n)
    ) =>
    !(Term (ubv n)) ->
    UTerm (sbv n)
  UBVToUnsignedTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
      Typeable ubv,
      Typeable sbv,
      KnownNat n,
      1 <= n,
      BVSignConversion (ubv n) (sbv n)
    ) =>
    !(Term (sbv n)) ->
    UTerm (ubv n)
  UBVConcatTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
      Typeable bv,
      KnownNat a,
      KnownNat b,
      KnownNat (a + b),
      1 <= a,
      1 <= b,
      1 <= a + b,
      SizedBV bv
    ) =>
    !(Term (bv a)) ->
    !(Term (bv b)) ->
    UTerm (bv (a + b))
  UBVSelectTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
      Typeable bv,
      KnownNat n,
      KnownNat ix,
      KnownNat w,
      1 <= n,
      1 <= w,
      ix + w <= n,
      SizedBV bv
    ) =>
    !(TypeRep ix) ->
    !(TypeRep w) ->
    !(Term (bv n)) ->
    UTerm (bv w)
  UBVExtendTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
      Typeable bv,
      KnownNat l,
      KnownNat r,
      1 <= l,
      1 <= r,
      l <= r,
      SizedBV bv
    ) =>
    !Bool ->
    !(TypeRep r) ->
    !(Term (bv l)) ->
    UTerm (bv r)
  UTabularFunApplyTerm ::
    ( SupportedPrim a,
      SupportedPrim b
    ) =>
    Term (a =-> b) ->
    Term a ->
    UTerm b
  UGeneralFunApplyTerm ::
    ( SupportedPrim a,
      SupportedPrim b
    ) =>
    Term (a --> b) ->
    Term a ->
    UTerm b
  UDivIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  UModIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  UQuotIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  URemIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  UDivBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  UModBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  UQuotBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  URemBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t

eqTypedId :: (TypeRep a, Id) -> (TypeRep b, Id) -> Bool
eqTypedId :: forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep a
a, Int
i1) (TypeRep b
b, Int
i2) = Int
i1 forall a. Eq a => a -> a -> Bool
== Int
i2 Bool -> Bool -> Bool
&& forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep a
a TypeRep b
b
{-# INLINE eqTypedId #-}

eqHeteroTag :: (Eq a) => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag :: forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep a
tpa, a
taga) (TypeRep b
tpb, b
tagb) = forall a b. Eq a => TypeRep a -> TypeRep b -> a -> b -> Bool
eqHeteroRep TypeRep a
tpa TypeRep b
tpb a
taga b
tagb
{-# INLINE eqHeteroTag #-}

instance (SupportedPrim t) => Interned (Term t) where
  type Uninterned (Term t) = UTerm t
  data Description (Term t) where
    DConTerm :: t -> Description (Term t)
    DSymTerm :: TypedSymbol t -> Description (Term t)
    DUnaryTerm ::
      (Eq tag, Hashable tag) =>
      {-# UNPACK #-} !(TypeRep tag, tag) ->
      {-# UNPACK #-} !(TypeRep arg, Id) ->
      Description (Term t)
    DBinaryTerm ::
      (Eq tag, Hashable tag) =>
      {-# UNPACK #-} !(TypeRep tag, tag) ->
      {-# UNPACK #-} !(TypeRep arg1, Id) ->
      {-# UNPACK #-} !(TypeRep arg2, Id) ->
      Description (Term t)
    DTernaryTerm ::
      (Eq tag, Hashable tag) =>
      {-# UNPACK #-} !(TypeRep tag, tag) ->
      {-# UNPACK #-} !(TypeRep arg1, Id) ->
      {-# UNPACK #-} !(TypeRep arg2, Id) ->
      {-# UNPACK #-} !(TypeRep arg3, Id) ->
      Description (Term t)
    DNotTerm :: {-# UNPACK #-} !Id -> Description (Term Bool)
    DOrTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
    DAndTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
    DEqvTerm :: TypeRep args -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
    DITETerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DAddNumTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DUMinusNumTerm :: {-# UNPACK #-} !Id -> Description (Term t)
    DTimesNumTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DAbsNumTerm :: {-# UNPACK #-} !Id -> Description (Term t)
    DSignumNumTerm :: {-# UNPACK #-} !Id -> Description (Term t)
    DLTNumTerm :: TypeRep args -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
    DLENumTerm :: TypeRep args -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
    DAndBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DOrBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DXorBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DComplementBitsTerm :: {-# UNPACK #-} !Id -> Description (Term t)
    DShiftBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Int -> Description (Term t)
    DRotateBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Int -> Description (Term t)
    DBVConcatTerm :: TypeRep bv1 -> TypeRep bv2 -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DBVToSignedTerm ::
      forall ubv sbv (n :: Nat).
      !(TypeRep (ubv n), Id) ->
      Description (Term (sbv n))
    DBVToUnsignedTerm ::
      forall sbv ubv (n :: Nat).
      !(TypeRep (sbv n), Id) ->
      Description (Term (ubv n))
    DBVSelectTerm ::
      forall bv (n :: Nat) (w :: Nat) (ix :: Nat).
      !(TypeRep ix) ->
      !(TypeRep (bv n), Id) ->
      Description (Term (bv w))
    DBVExtendTerm ::
      forall bv (l :: Nat) (r :: Nat).
      !Bool ->
      !(TypeRep r) ->
      {-# UNPACK #-} !(TypeRep (bv l), Id) ->
      Description (Term (bv r))
    DTabularFunApplyTerm ::
      {-# UNPACK #-} !(TypeRep (a =-> b), Id) ->
      {-# UNPACK #-} !(TypeRep a, Id) ->
      Description (Term b)
    DGeneralFunApplyTerm ::
      {-# UNPACK #-} !(TypeRep (a --> b), Id) ->
      {-# UNPACK #-} !(TypeRep a, Id) ->
      Description (Term b)
    DDivIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
    DModIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
    DQuotIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
    DRemIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
    DDivBoundedIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
    DModBoundedIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
    DQuotBoundedIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
    DRemBoundedIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)

  describe :: Uninterned (Term t) -> Description (Term t)
describe (UConTerm t
v) = forall t. t -> Description (Term t)
DConTerm t
v
  describe ((USymTerm TypedSymbol t
name) :: UTerm t) = forall t. TypedSymbol t -> Description (Term t)
DSymTerm @t TypedSymbol t
name
  describe ((UUnaryTerm (tag
tag :: tagt) (Term arg
tm :: Term arg)) :: UTerm t) =
    forall a l t.
(Eq a, Hashable a) =>
(TypeRep a, a) -> (TypeRep l, Int) -> Description (Term t)
DUnaryTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, forall t. Term t -> Int
identity Term arg
tm)
  describe ((UBinaryTerm (tag
tag :: tagt) (Term arg1
tm1 :: Term arg1) (Term arg2
tm2 :: Term arg2)) :: UTerm t) =
    forall a l r t.
(Eq a, Hashable a) =>
(TypeRep a, a)
-> (TypeRep l, Int) -> (TypeRep r, Int) -> Description (Term t)
DBinaryTerm @tagt @arg1 @arg2 @t (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, forall t. Term t -> Int
identity Term arg1
tm1) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, forall t. Term t -> Int
identity Term arg2
tm2)
  describe ((UTernaryTerm (tag
tag :: tagt) (Term arg1
tm1 :: Term arg1) (Term arg2
tm2 :: Term arg2) (Term arg3
tm3 :: Term arg3)) :: UTerm t) =
    forall a l r w t.
(Eq a, Hashable a) =>
(TypeRep a, a)
-> (TypeRep l, Int)
-> (TypeRep r, Int)
-> (TypeRep w, Int)
-> Description (Term t)
DTernaryTerm @tagt @arg1 @arg2 @arg3 @t
      (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag)
      (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, forall t. Term t -> Int
identity Term arg1
tm1)
      (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, forall t. Term t -> Int
identity Term arg2
tm2)
      (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, forall t. Term t -> Int
identity Term arg3
tm3)
  describe (UNotTerm Term Bool
arg) = Int -> Description (Term Bool)
DNotTerm (forall t. Term t -> Int
identity Term Bool
arg)
  describe (UOrTerm Term Bool
arg1 Term Bool
arg2) = Int -> Int -> Description (Term Bool)
DOrTerm (forall t. Term t -> Int
identity Term Bool
arg1) (forall t. Term t -> Int
identity Term Bool
arg2)
  describe (UAndTerm Term Bool
arg1 Term Bool
arg2) = Int -> Int -> Description (Term Bool)
DAndTerm (forall t. Term t -> Int
identity Term Bool
arg1) (forall t. Term t -> Int
identity Term Bool
arg2)
  describe (UEqvTerm (Term t
arg1 :: Term arg) Term t
arg2) = forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DEqvTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
  describe (UITETerm Term Bool
cond (Term t
l :: Term arg) Term t
r) = forall t. Int -> Int -> Int -> Description (Term t)
DITETerm (forall t. Term t -> Int
identity Term Bool
cond) (forall t. Term t -> Int
identity Term t
l) (forall t. Term t -> Int
identity Term t
r)
  describe (UAddNumTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DAddNumTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
  describe (UUMinusNumTerm Term t
arg) = forall t. Int -> Description (Term t)
DUMinusNumTerm (forall t. Term t -> Int
identity Term t
arg)
  describe (UTimesNumTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DTimesNumTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
  describe (UAbsNumTerm Term t
arg) = forall t. Int -> Description (Term t)
DAbsNumTerm (forall t. Term t -> Int
identity Term t
arg)
  describe (USignumNumTerm Term t
arg) = forall t. Int -> Description (Term t)
DSignumNumTerm (forall t. Term t -> Int
identity Term t
arg)
  describe (ULTNumTerm (Term t
arg1 :: arg) Term t
arg2) = forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DLTNumTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
  describe (ULENumTerm (Term t
arg1 :: arg) Term t
arg2) = forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DLENumTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
  describe (UAndBitsTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DAndBitsTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
  describe (UOrBitsTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DOrBitsTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
  describe (UXorBitsTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DXorBitsTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
  describe (UComplementBitsTerm Term t
arg) = forall t. Int -> Description (Term t)
DComplementBitsTerm (forall t. Term t -> Int
identity Term t
arg)
  describe (UShiftBitsTerm Term t
arg Int
n) = forall t. Int -> Int -> Description (Term t)
DShiftBitsTerm (forall t. Term t -> Int
identity Term t
arg) Int
n
  describe (URotateBitsTerm Term t
arg Int
n) = forall t. Int -> Int -> Description (Term t)
DRotateBitsTerm (forall t. Term t -> Int
identity Term t
arg) Int
n
  describe (UBVToSignedTerm (Term (ubv n)
arg :: Term bv)) = forall (a :: Natural -> *) (l :: Natural -> *) (r :: Natural).
(TypeRep (a r), Int) -> Description (Term (l r))
DBVToSignedTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv, forall t. Term t -> Int
identity Term (ubv n)
arg)
  describe (UBVToUnsignedTerm (Term (sbv n)
arg :: Term bv)) = forall (a :: Natural -> *) (l :: Natural -> *) (r :: Natural).
(TypeRep (a r), Int) -> Description (Term (l r))
DBVToSignedTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv, forall t. Term t -> Int
identity Term (sbv n)
arg)
  describe (UBVConcatTerm (Term (bv a)
arg1 :: bv1) (Term (bv b)
arg2 :: bv2)) =
    forall a l t.
TypeRep a -> TypeRep l -> Int -> Int -> Description (Term t)
DBVConcatTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv1) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv2) (forall t. Term t -> Int
identity Term (bv a)
arg1) (forall t. Term t -> Int
identity Term (bv b)
arg2)
  describe (UBVSelectTerm (TypeRep ix
ix :: TypeRep ix) TypeRep w
_ (Term (bv n)
arg :: Term arg)) =
    forall (a :: Natural -> *) (l :: Natural) (r :: Natural)
       (w :: Natural).
TypeRep w -> (TypeRep (a l), Int) -> Description (Term (a r))
DBVSelectTerm TypeRep ix
ix (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, forall t. Term t -> Int
identity Term (bv n)
arg)
  describe (UBVExtendTerm Bool
signed (TypeRep r
n :: TypeRep n) (Term (bv l)
arg :: Term arg)) =
    forall (a :: Natural -> *) (l :: Natural) (r :: Natural).
Bool
-> TypeRep r -> (TypeRep (a l), Int) -> Description (Term (a r))
DBVExtendTerm Bool
signed TypeRep r
n (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, forall t. Term t -> Int
identity Term (bv l)
arg)
  describe (UTabularFunApplyTerm (Term (a =-> t)
func :: Term f) (Term a
arg :: Term a)) =
    forall a b.
(TypeRep (a =-> b), Int)
-> (TypeRep a, Int) -> Description (Term b)
DTabularFunApplyTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep f, forall t. Term t -> Int
identity Term (a =-> t)
func) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep a, forall t. Term t -> Int
identity Term a
arg)
  describe (UGeneralFunApplyTerm (Term (a --> t)
func :: Term f) (Term a
arg :: Term a)) =
    forall a b.
(TypeRep (a --> b), Int)
-> (TypeRep a, Int) -> Description (Term b)
DGeneralFunApplyTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep f, forall t. Term t -> Int
identity Term (a --> t)
func) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep a, forall t. Term t -> Int
identity Term a
arg)
  describe (UDivIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DDivIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
  describe (UModIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DModIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
  describe (UQuotIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DRemIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
  describe (URemIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DQuotIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
  describe (UDivBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DDivBoundedIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
  describe (UModBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DModBoundedIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
  describe (UQuotBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DRemBoundedIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
  describe (URemBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DQuotBoundedIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)

  identify :: Int -> Uninterned (Term t) -> Term t
identify Int
i = UTerm t -> Term t
go
    where
      go :: UTerm t -> Term t
go (UConTerm t
v) = forall t. SupportedPrim t => Int -> t -> Term t
ConTerm Int
i t
v
      go (USymTerm TypedSymbol t
v) = forall t. SupportedPrim t => Int -> TypedSymbol t -> Term t
SymTerm Int
i TypedSymbol t
v
      go (UUnaryTerm tag
tag Term arg
tm) = forall a l t. UnaryOp a l t => Int -> a -> Term l -> Term t
UnaryTerm Int
i tag
tag Term arg
tm
      go (UBinaryTerm tag
tag Term arg1
tm1 Term arg2
tm2) = forall a l r t.
BinaryOp a l r t =>
Int -> a -> Term l -> Term r -> Term t
BinaryTerm Int
i tag
tag Term arg1
tm1 Term arg2
tm2
      go (UTernaryTerm tag
tag Term arg1
tm1 Term arg2
tm2 Term arg3
tm3) = forall a l r w t.
TernaryOp a l r w t =>
Int -> a -> Term l -> Term r -> Term w -> Term t
TernaryTerm Int
i tag
tag Term arg1
tm1 Term arg2
tm2 Term arg3
tm3
      go (UNotTerm Term Bool
arg) = Int -> Term Bool -> Term Bool
NotTerm Int
i Term Bool
arg
      go (UOrTerm Term Bool
arg1 Term Bool
arg2) = Int -> Term Bool -> Term Bool -> Term Bool
OrTerm Int
i Term Bool
arg1 Term Bool
arg2
      go (UAndTerm Term Bool
arg1 Term Bool
arg2) = Int -> Term Bool -> Term Bool -> Term Bool
AndTerm Int
i Term Bool
arg1 Term Bool
arg2
      go (UEqvTerm Term t
arg1 Term t
arg2) = forall a. SupportedPrim a => Int -> Term a -> Term a -> Term Bool
EqvTerm Int
i Term t
arg1 Term t
arg2
      go (UITETerm Term Bool
cond Term t
l Term t
r) = forall t.
SupportedPrim t =>
Int -> Term Bool -> Term t -> Term t -> Term t
ITETerm Int
i Term Bool
cond Term t
l Term t
r
      go (UAddNumTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Num t) =>
Int -> Term t -> Term t -> Term t
AddNumTerm Int
i Term t
arg1 Term t
arg2
      go (UUMinusNumTerm Term t
arg) = forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
UMinusNumTerm Int
i Term t
arg
      go (UTimesNumTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Num t) =>
Int -> Term t -> Term t -> Term t
TimesNumTerm Int
i Term t
arg1 Term t
arg2
      go (UAbsNumTerm Term t
arg) = forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
AbsNumTerm Int
i Term t
arg
      go (USignumNumTerm Term t
arg) = forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
SignumNumTerm Int
i Term t
arg
      go (ULTNumTerm Term t
arg1 Term t
arg2) = forall a.
(SupportedPrim a, Num a, Ord a) =>
Int -> Term a -> Term a -> Term Bool
LTNumTerm Int
i Term t
arg1 Term t
arg2
      go (ULENumTerm Term t
arg1 Term t
arg2) = forall a.
(SupportedPrim a, Num a, Ord a) =>
Int -> Term a -> Term a -> Term Bool
LENumTerm Int
i Term t
arg1 Term t
arg2
      go (UAndBitsTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Term t -> Term t
AndBitsTerm Int
i Term t
arg1 Term t
arg2
      go (UOrBitsTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Term t -> Term t
OrBitsTerm Int
i Term t
arg1 Term t
arg2
      go (UXorBitsTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Term t -> Term t
XorBitsTerm Int
i Term t
arg1 Term t
arg2
      go (UComplementBitsTerm Term t
arg) = forall t. (SupportedPrim t, Bits t) => Int -> Term t -> Term t
ComplementBitsTerm Int
i Term t
arg
      go (UShiftBitsTerm Term t
arg Int
n) = forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Int -> Term t
ShiftBitsTerm Int
i Term t
arg Int
n
      go (URotateBitsTerm Term t
arg Int
n) = forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Int -> Term t
RotateBitsTerm Int
i Term t
arg Int
n
      go (UBVToSignedTerm Term (ubv n)
arg) = forall (a :: Natural -> *) (l :: Natural -> *) (r :: Natural).
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 SupportedPrim (a n),
 forall (n :: Natural). (KnownNat n, 1 <= n) => SupportedPrim (l n),
 Typeable a, Typeable l, KnownNat r, 1 <= r,
 BVSignConversion (a r) (l r)) =>
Int -> Term (a r) -> Term (l r)
BVToSignedTerm Int
i Term (ubv n)
arg
      go (UBVToUnsignedTerm Term (sbv n)
arg) = forall (a :: Natural -> *) (l :: Natural -> *) (r :: Natural).
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 SupportedPrim (a n),
 forall (n :: Natural). (KnownNat n, 1 <= n) => SupportedPrim (l n),
 Typeable a, Typeable l, KnownNat r, 1 <= r,
 BVSignConversion (a r) (l r)) =>
Int -> Term (l r) -> Term (a r)
BVToUnsignedTerm Int
i Term (sbv n)
arg
      go (UBVConcatTerm Term (bv a)
arg1 Term (bv b)
arg2) = forall (a :: Natural -> *) (l :: Natural) (r :: Natural).
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 SupportedPrim (a n),
 Typeable a, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l,
 1 <= r, 1 <= (l + r), SizedBV a) =>
Int -> Term (a l) -> Term (a r) -> Term (a (l + r))
BVConcatTerm Int
i Term (bv a)
arg1 Term (bv b)
arg2
      go (UBVSelectTerm TypeRep ix
ix TypeRep w
w Term (bv n)
arg) = forall (a :: Natural -> *) (l :: Natural) (r :: Natural)
       (w :: Natural).
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 SupportedPrim (a n),
 Typeable a, KnownNat l, KnownNat r, KnownNat w, 1 <= l, 1 <= w,
 (r + w) <= l, SizedBV a) =>
Int -> TypeRep r -> TypeRep w -> Term (a l) -> Term (a w)
BVSelectTerm Int
i TypeRep ix
ix TypeRep w
w Term (bv n)
arg
      go (UBVExtendTerm Bool
signed TypeRep r
n Term (bv l)
arg) = forall (a :: Natural -> *) (l :: Natural) (r :: Natural).
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 SupportedPrim (a n),
 Typeable a, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
 SizedBV a) =>
Int -> Bool -> TypeRep r -> Term (a l) -> Term (a r)
BVExtendTerm Int
i Bool
signed TypeRep r
n Term (bv l)
arg
      go (UTabularFunApplyTerm Term (a =-> t)
func Term a
arg) = forall a b.
(SupportedPrim a, SupportedPrim b) =>
Int -> Term (a =-> b) -> Term a -> Term b
TabularFunApplyTerm Int
i Term (a =-> t)
func Term a
arg
      go (UGeneralFunApplyTerm Term (a --> t)
func Term a
arg) = forall a b.
(SupportedPrim a, SupportedPrim b) =>
Int -> Term (a --> b) -> Term a -> Term b
GeneralFunApplyTerm Int
i Term (a --> t)
func Term a
arg
      go (UDivIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Integral t) =>
Int -> Term t -> Term t -> Term t
DivIntegralTerm Int
i Term t
arg1 Term t
arg2
      go (UModIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Integral t) =>
Int -> Term t -> Term t -> Term t
ModIntegralTerm Int
i Term t
arg1 Term t
arg2
      go (UQuotIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Integral t) =>
Int -> Term t -> Term t -> Term t
QuotIntegralTerm Int
i Term t
arg1 Term t
arg2
      go (URemIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Integral t) =>
Int -> Term t -> Term t -> Term t
RemIntegralTerm Int
i Term t
arg1 Term t
arg2
      go (UDivBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Int -> Term t -> Term t -> Term t
DivBoundedIntegralTerm Int
i Term t
arg1 Term t
arg2
      go (UModBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Int -> Term t -> Term t -> Term t
ModBoundedIntegralTerm Int
i Term t
arg1 Term t
arg2
      go (UQuotBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Int -> Term t -> Term t -> Term t
QuotBoundedIntegralTerm Int
i Term t
arg1 Term t
arg2
      go (URemBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Int -> Term t -> Term t -> Term t
RemBoundedIntegralTerm Int
i Term t
arg1 Term t
arg2
  cache :: Cache (Term t)
cache = forall t. SupportedPrim t => Cache (Term t)
termCache

instance (SupportedPrim t) => Eq (Description (Term t)) where
  DConTerm (t
l :: tyl) == :: Description (Term t) -> Description (Term t) -> Bool
== DConTerm (t
r :: tyr) = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast @tyl @tyr t
l forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just t
r
  DSymTerm TypedSymbol t
ls == DSymTerm TypedSymbol t
rs = TypedSymbol t
ls forall a. Eq a => a -> a -> Bool
== TypedSymbol t
rs
  DUnaryTerm ((TypeRep tag, tag)
tagl :: tagl) (TypeRep arg, Int)
li == DUnaryTerm ((TypeRep tag, tag)
tagr :: tagr) (TypeRep arg, Int)
ri = forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep tag, tag)
tagl (TypeRep tag, tag)
tagr Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg, Int)
li (TypeRep arg, Int)
ri
  DBinaryTerm ((TypeRep tag, tag)
tagl :: tagl) (TypeRep arg1, Int)
li1 (TypeRep arg2, Int)
li2 == DBinaryTerm ((TypeRep tag, tag)
tagr :: tagr) (TypeRep arg1, Int)
ri1 (TypeRep arg2, Int)
ri2 =
    forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep tag, tag)
tagl (TypeRep tag, tag)
tagr Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg1, Int)
li1 (TypeRep arg1, Int)
ri1 Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg2, Int)
li2 (TypeRep arg2, Int)
ri2
  DTernaryTerm ((TypeRep tag, tag)
tagl :: tagl) (TypeRep arg1, Int)
li1 (TypeRep arg2, Int)
li2 (TypeRep arg3, Int)
li3 == DTernaryTerm ((TypeRep tag, tag)
tagr :: tagr) (TypeRep arg1, Int)
ri1 (TypeRep arg2, Int)
ri2 (TypeRep arg3, Int)
ri3 =
    forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep tag, tag)
tagl (TypeRep tag, tag)
tagr Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg1, Int)
li1 (TypeRep arg1, Int)
ri1 Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg2, Int)
li2 (TypeRep arg2, Int)
ri2 Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg3, Int)
li3 (TypeRep arg3, Int)
ri3
  DNotTerm Int
li == DNotTerm Int
ri = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri
  DOrTerm Int
li1 Int
li2 == DOrTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DAndTerm Int
li1 Int
li2 == DAndTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DEqvTerm TypeRep args
lrep Int
li1 Int
li2 == DEqvTerm TypeRep args
rrep Int
ri1 Int
ri2 = forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep args
lrep TypeRep args
rrep Bool -> Bool -> Bool
&& Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DITETerm Int
lc Int
li1 Int
li2 == DITETerm Int
rc Int
ri1 Int
ri2 = Int
lc forall a. Eq a => a -> a -> Bool
== Int
rc Bool -> Bool -> Bool
&& Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DAddNumTerm Int
li1 Int
li2 == DAddNumTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DUMinusNumTerm Int
li == DUMinusNumTerm Int
ri = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri
  DTimesNumTerm Int
li1 Int
li2 == DTimesNumTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DAbsNumTerm Int
li == DAbsNumTerm Int
ri = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri
  DSignumNumTerm Int
li == DSignumNumTerm Int
ri = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri
  DLTNumTerm TypeRep args
lrep Int
li1 Int
li2 == DLTNumTerm TypeRep args
rrep Int
ri1 Int
ri2 = forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep args
lrep TypeRep args
rrep Bool -> Bool -> Bool
&& Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DLENumTerm TypeRep args
lrep Int
li1 Int
li2 == DLENumTerm TypeRep args
rrep Int
ri1 Int
ri2 = forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep args
lrep TypeRep args
rrep Bool -> Bool -> Bool
&& Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DAndBitsTerm Int
li1 Int
li2 == DAndBitsTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DOrBitsTerm Int
li1 Int
li2 == DOrBitsTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DXorBitsTerm Int
li1 Int
li2 == DXorBitsTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DComplementBitsTerm Int
li == DComplementBitsTerm Int
ri = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri
  DShiftBitsTerm Int
li Int
ln == DShiftBitsTerm Int
ri Int
rn = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri Bool -> Bool -> Bool
&& Int
ln forall a. Eq a => a -> a -> Bool
== Int
rn
  DRotateBitsTerm Int
li Int
ln == DRotateBitsTerm Int
ri Int
rn = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri Bool -> Bool -> Bool
&& Int
ln forall a. Eq a => a -> a -> Bool
== Int
rn
  DBVToSignedTerm (TypeRep (ubv n), Int)
li == DBVToSignedTerm (TypeRep (ubv n), Int)
ri = forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (ubv n), Int)
li (TypeRep (ubv n), Int)
ri
  DBVToUnsignedTerm (TypeRep (sbv n), Int)
li == DBVToUnsignedTerm (TypeRep (sbv n), Int)
ri = forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (sbv n), Int)
li (TypeRep (sbv n), Int)
ri
  DBVConcatTerm TypeRep bv1
lrep1 TypeRep bv2
lrep2 Int
li1 Int
li2 == DBVConcatTerm TypeRep bv1
rrep1 TypeRep bv2
rrep2 Int
ri1 Int
ri2 =
    forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep bv1
lrep1 TypeRep bv1
rrep1 Bool -> Bool -> Bool
&& forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep bv2
lrep2 TypeRep bv2
rrep2 Bool -> Bool -> Bool
&& Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DBVSelectTerm TypeRep ix
lix (TypeRep (bv n), Int)
li == DBVSelectTerm TypeRep ix
rix (TypeRep (bv n), Int)
ri =
    forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep ix
lix TypeRep ix
rix Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (bv n), Int)
li (TypeRep (bv n), Int)
ri
  DBVExtendTerm Bool
lIsSigned TypeRep r
ln (TypeRep (bv l), Int)
li == DBVExtendTerm Bool
rIsSigned TypeRep r
rn (TypeRep (bv l), Int)
ri =
    Bool
lIsSigned forall a. Eq a => a -> a -> Bool
== Bool
rIsSigned
      Bool -> Bool -> Bool
&& forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep r
ln TypeRep r
rn
      Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (bv l), Int)
li (TypeRep (bv l), Int)
ri
  DTabularFunApplyTerm (TypeRep (a =-> t), Int)
lf (TypeRep a, Int)
li == DTabularFunApplyTerm (TypeRep (a =-> t), Int)
rf (TypeRep a, Int)
ri = forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (a =-> t), Int)
lf (TypeRep (a =-> t), Int)
rf Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep a, Int)
li (TypeRep a, Int)
ri
  DGeneralFunApplyTerm (TypeRep (a --> t), Int)
lf (TypeRep a, Int)
li == DGeneralFunApplyTerm (TypeRep (a --> t), Int)
rf (TypeRep a, Int)
ri = forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (a --> t), Int)
lf (TypeRep (a --> t), Int)
rf Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep a, Int)
li (TypeRep a, Int)
ri
  DDivIntegralTerm Int
li1 Int
li2 == DDivIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DModIntegralTerm Int
li1 Int
li2 == DModIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DQuotIntegralTerm Int
li1 Int
li2 == DQuotIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DRemIntegralTerm Int
li1 Int
li2 == DRemIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DDivBoundedIntegralTerm Int
li1 Int
li2 == DDivBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DModBoundedIntegralTerm Int
li1 Int
li2 == DModBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DQuotBoundedIntegralTerm Int
li1 Int
li2 == DQuotBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  DRemBoundedIntegralTerm Int
li1 Int
li2 == DRemBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
  Description (Term t)
_ == Description (Term t)
_ = Bool
False

instance (SupportedPrim t) => Hashable (Description (Term t)) where
  hashWithSalt :: Int -> Description (Term t) -> Int
hashWithSalt Int
s (DConTerm t
c) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` t
c
  hashWithSalt Int
s (DSymTerm TypedSymbol t
name) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol t
name
  hashWithSalt Int
s (DUnaryTerm (TypeRep tag, tag)
tag (TypeRep arg, Int)
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
2 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg, Int)
id1
  hashWithSalt Int
s (DBinaryTerm (TypeRep tag, tag)
tag (TypeRep arg1, Int)
id1 (TypeRep arg2, Int)
id2) =
    Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
3 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg1, Int)
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg2, Int)
id2
  hashWithSalt Int
s (DTernaryTerm (TypeRep tag, tag)
tag (TypeRep arg1, Int)
id1 (TypeRep arg2, Int)
id2 (TypeRep arg3, Int)
id3) =
    Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
4 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg1, Int)
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg2, Int)
id2 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg3, Int)
id3
  hashWithSalt Int
s (DNotTerm Int
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
5 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
  hashWithSalt Int
s (DOrTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
6 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DAndTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
7 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DEqvTerm TypeRep args
rep Int
id1 Int
id2) =
    Int
s
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
8 :: Int)
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DITETerm Int
idc Int
id1 Int
id2) =
    Int
s
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
9 :: Int)
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
idc
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DAddNumTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
10 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DUMinusNumTerm Int
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
11 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
  hashWithSalt Int
s (DTimesNumTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
12 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DAbsNumTerm Int
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
13 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
  hashWithSalt Int
s (DSignumNumTerm Int
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
14 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
  hashWithSalt Int
s (DLTNumTerm TypeRep args
rep Int
id1 Int
id2) =
    Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
15 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DLENumTerm TypeRep args
rep Int
id1 Int
id2) =
    Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
16 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DAndBitsTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
17 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DOrBitsTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
18 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DXorBitsTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
19 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DComplementBitsTerm Int
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
20 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
  hashWithSalt Int
s (DShiftBitsTerm Int
id1 Int
n) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
21 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
n
  hashWithSalt Int
s (DRotateBitsTerm Int
id1 Int
n) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
22 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
n
  hashWithSalt Int
s (DBVToSignedTerm (TypeRep (ubv n), Int)
id) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
23 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (ubv n), Int)
id
  hashWithSalt Int
s (DBVToUnsignedTerm (TypeRep (sbv n), Int)
id) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
24 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (sbv n), Int)
id
  hashWithSalt Int
s (DBVConcatTerm TypeRep bv1
rep1 TypeRep bv2
rep2 Int
id1 Int
id2) =
    Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
25 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep bv1
rep1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep bv2
rep2 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DBVSelectTerm TypeRep ix
ix (TypeRep (bv n), Int)
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
26 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep ix
ix forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (bv n), Int)
id1
  hashWithSalt Int
s (DBVExtendTerm Bool
signed TypeRep r
n (TypeRep (bv l), Int)
id1) =
    Int
s
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
27 :: Int)
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Bool
signed
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep r
n
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (bv l), Int)
id1
  hashWithSalt Int
s (DTabularFunApplyTerm (TypeRep (a =-> t), Int)
id1 (TypeRep a, Int)
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
28 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (a =-> t), Int)
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep a, Int)
id2
  hashWithSalt Int
s (DGeneralFunApplyTerm (TypeRep (a --> t), Int)
id1 (TypeRep a, Int)
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
29 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (a --> t), Int)
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep a, Int)
id2
  hashWithSalt Int
s (DDivIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
30 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DModIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
31 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DQuotIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
32 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DRemIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
33 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DDivBoundedIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
34 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DModBoundedIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
35 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DQuotBoundedIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
36 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DRemBoundedIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
37 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2

-- Basic Bool
defaultValueForBool :: Bool
defaultValueForBool :: Bool
defaultValueForBool = Bool
False

defaultValueForBoolDyn :: ModelValue
defaultValueForBoolDyn :: ModelValue
defaultValueForBoolDyn = forall a. (Show a, Eq a, Hashable a, Typeable a) => a -> ModelValue
toModelValue Bool
defaultValueForBool

instance SupportedPrim Bool where
  pformatCon :: Bool -> String
pformatCon Bool
True = String
"true"
  pformatCon Bool
False = String
"false"
  defaultValue :: Bool
defaultValue = Bool
defaultValueForBool
  defaultValueDynamic :: forall (proxy :: * -> *). proxy Bool -> ModelValue
defaultValueDynamic proxy Bool
_ = ModelValue
defaultValueForBoolDyn

defaultValueForInteger :: Integer
defaultValueForInteger :: Integer
defaultValueForInteger = Integer
0

defaultValueForIntegerDyn :: ModelValue
defaultValueForIntegerDyn :: ModelValue
defaultValueForIntegerDyn = forall a. (Show a, Eq a, Hashable a, Typeable a) => a -> ModelValue
toModelValue Integer
defaultValueForInteger

-- Basic Integer
instance SupportedPrim Integer where
  pformatCon :: Integer -> String
pformatCon = forall a. Show a => a -> String
show
  defaultValue :: Integer
defaultValue = Integer
defaultValueForInteger
  defaultValueDynamic :: forall (proxy :: * -> *). proxy Integer -> ModelValue
defaultValueDynamic proxy Integer
_ = ModelValue
defaultValueForIntegerDyn

-- Signed BV
instance (KnownNat w, 1 <= w) => SupportedPrim (IntN w) where
  type PrimConstraint (IntN w) = (KnownNat w, 1 <= w)
  pformatCon :: IntN w -> String
pformatCon = forall a. Show a => a -> String
show
  defaultValue :: IntN w
defaultValue = IntN w
0

-- Unsigned BV
instance (KnownNat w, 1 <= w) => SupportedPrim (WordN w) where
  type PrimConstraint (WordN w) = (KnownNat w, 1 <= w)
  pformatCon :: WordN w -> String
pformatCon = forall a. Show a => a -> String
show
  defaultValue :: WordN w
defaultValue = WordN w
0

-- | General symbolic function type. Use the '#' operator to apply the function.
-- Note that this function should be applied to symbolic values only. It is by
-- itself already a symbolic value, but can be considered partially concrete
-- as the function body is specified. Use 'Grisette.IR.SymPrim.Data.SymPrim.-~>' for uninterpreted general
-- symbolic functions.
--
-- The result would be partially evaluated.
--
-- >>> :set -XOverloadedStrings
-- >>> :set -XTypeOperators
-- >>> let f = ("x" :: TypedSymbol Integer) --> ("x" + 1 + "y" :: SymInteger) :: Integer --> Integer
-- >>> f # 1    -- 1 has the type SymInteger
-- (+ 2 y)
-- >>> f # "a"  -- "a" has the type SymInteger
-- (+ 1 (+ a y))
data (-->) a b where
  GeneralFun :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b

instance (LinkedRep a sa, LinkedRep b sb) => Function (a --> b) where
  type Arg (a --> b) = SymType a
  type Ret (a --> b) = SymType b
  (GeneralFun TypedSymbol a
s Term b
t) # :: (a --> b) -> Arg (a --> b) -> Ret (a --> b)
# Arg (a --> b)
x = forall con sym. LinkedRep con sym => Term con -> sym
wrapTerm forall a b. (a -> b) -> a -> b
$ forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
s (forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm Arg (a --> b)
x) Term b
t

{-
pattern GeneralFun :: () => (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b
pattern GeneralFun arg v <- GeneralFun arg v

{-# COMPLETE GeneralFun #-}
-}

infixr 0 -->

buildGeneralFun :: () => (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b
buildGeneralFun :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun TypedSymbol a
arg Term b
v = forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol a
newarg (forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
arg (forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm TypedSymbol a
newarg) Term b
v)
  where
    newarg :: TypedSymbol a
newarg = forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
 Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo TypedSymbol a
arg ARG
ARG

data ARG = ARG
  deriving (ARG -> ARG -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ARG -> ARG -> Bool
$c/= :: ARG -> ARG -> Bool
== :: ARG -> ARG -> Bool
$c== :: ARG -> ARG -> Bool
Eq, Eq ARG
ARG -> ARG -> Bool
ARG -> ARG -> Ordering
ARG -> ARG -> ARG
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ARG -> ARG -> ARG
$cmin :: ARG -> ARG -> ARG
max :: ARG -> ARG -> ARG
$cmax :: ARG -> ARG -> ARG
>= :: ARG -> ARG -> Bool
$c>= :: ARG -> ARG -> Bool
> :: ARG -> ARG -> Bool
$c> :: ARG -> ARG -> Bool
<= :: ARG -> ARG -> Bool
$c<= :: ARG -> ARG -> Bool
< :: ARG -> ARG -> Bool
$c< :: ARG -> ARG -> Bool
compare :: ARG -> ARG -> Ordering
$ccompare :: ARG -> ARG -> Ordering
Ord, forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => ARG -> m Exp
forall (m :: * -> *). Quote m => ARG -> Code m ARG
liftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
$cliftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
lift :: forall (m :: * -> *). Quote m => ARG -> m Exp
$clift :: forall (m :: * -> *). Quote m => ARG -> m Exp
Lift, Int -> ARG -> ShowS
[ARG] -> ShowS
ARG -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ARG] -> ShowS
$cshowList :: [ARG] -> ShowS
show :: ARG -> String
$cshow :: ARG -> String
showsPrec :: Int -> ARG -> ShowS
$cshowsPrec :: Int -> ARG -> ShowS
Show, forall x. Rep ARG x -> ARG
forall x. ARG -> Rep ARG x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ARG x -> ARG
$cfrom :: forall x. ARG -> Rep ARG x
Generic)

instance NFData ARG where
  rnf :: ARG -> ()
rnf ARG
ARG = ()

instance Hashable ARG where
  hashWithSalt :: Int -> ARG -> Int
hashWithSalt Int
s ARG
ARG = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int)

instance Eq (a --> b) where
  GeneralFun TypedSymbol a
sym1 Term b
tm1 == :: (a --> b) -> (a --> b) -> Bool
== GeneralFun TypedSymbol a
sym2 Term b
tm2 = TypedSymbol a
sym1 forall a. Eq a => a -> a -> Bool
== TypedSymbol a
sym2 Bool -> Bool -> Bool
&& Term b
tm1 forall a. Eq a => a -> a -> Bool
== Term b
tm2

instance Show (a --> b) where
  show :: (a --> b) -> String
show (GeneralFun TypedSymbol a
sym Term b
tm) = String
"\\(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypedSymbol a
sym forall a. [a] -> [a] -> [a]
++ String
") -> " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term b
tm

instance Lift (a --> b) where
  liftTyped :: forall (m :: * -> *). Quote m => (a --> b) -> Code m (a --> b)
liftTyped (GeneralFun TypedSymbol a
sym Term b
tm) = [||GeneralFun sym tm||]

instance Hashable (a --> b) where
  Int
s hashWithSalt :: Int -> (a --> b) -> Int
`hashWithSalt` (GeneralFun TypedSymbol a
sym Term b
tm) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol a
sym forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Term b
tm

instance NFData (a --> b) where
  rnf :: (a --> b) -> ()
rnf (GeneralFun TypedSymbol a
sym Term b
tm) = forall a. NFData a => a -> ()
rnf TypedSymbol a
sym seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Term b
tm

instance (SupportedPrim a, SupportedPrim b) => SupportedPrim (a --> b) where
  type PrimConstraint (a --> b) = (SupportedPrim a, SupportedPrim b)
  defaultValue :: a --> b
defaultValue = forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun (forall t. SupportedPrim t => String -> TypedSymbol t
SimpleSymbol String
"a") (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall t. SupportedPrim t => t
defaultValue)