{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# 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 (..),
    UnaryOp (..),
    BinaryOp (..),
    TernaryOp (..),
    TypedSymbol (..),
    SomeTypedSymbol (..),
    showUntyped,
    withSymbolSupported,
    someTypedSymbol,
    Term (..),
    UTerm (..),
    FunArg (..),
    type (-->) (..),
  )
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.Class.BitVector
import Grisette.Core.Data.Class.Function
import Grisette.IR.SymPrim.Data.BV
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)

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
  BVConcatTerm ::
    ( SupportedPrim (bv a),
      SupportedPrim (bv b),
      SupportedPrim (bv c),
      KnownNat a,
      KnownNat b,
      KnownNat c,
      BVConcat (bv a) (bv b) (bv c)
    ) =>
    {-# UNPACK #-} !Id ->
    !(Term (bv a)) ->
    !(Term (bv b)) ->
    Term (bv c)
  BVSelectTerm ::
    ( SupportedPrim (bv a),
      SupportedPrim (bv w),
      KnownNat a,
      KnownNat w,
      KnownNat ix,
      BVSelect (bv a) ix w (bv w)
    ) =>
    {-# UNPACK #-} !Id ->
    !(TypeRep ix) ->
    !(TypeRep w) ->
    !(Term (bv a)) ->
    Term (bv w)
  BVExtendTerm ::
    ( SupportedPrim (bv a),
      SupportedPrim (bv b),
      KnownNat a,
      KnownNat b,
      KnownNat n,
      BVExtend (bv a) n (bv b)
    ) =>
    {-# UNPACK #-} !Id ->
    !Bool ->
    !(TypeRep n) ->
    !(Term (bv a)) ->
    Term (bv b)
  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
  DivIntegerTerm :: !Id -> Term Integer -> Term Integer -> Term Integer
  ModIntegerTerm :: !Id -> Term Integer -> Term Integer -> Term Integer

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 (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 a)
arg) = [||bvselectTerm (Proxy @ix) (Proxy @w) arg||]
  liftTyped (BVExtendTerm Int
_ Bool
signed (TypeRep n
_ :: TypeRep n) Term (bv a)
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 (DivIntegerTerm Int
_ Term Integer
arg1 Term Integer
arg2) = [||divIntegerTerm arg1 arg2||]
  liftTyped (ModIntegerTerm Int
_ Term Integer
arg1 Term Integer
arg2) = [||modIntegerTerm 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 (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 a)
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 a)
arg forall a. [a] -> [a] -> [a]
++ String
"}"
  show (BVExtendTerm Int
i Bool
signed TypeRep n
n Term (bv a)
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 n
n forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (bv a)
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 (DivIntegerTerm Int
i Term Integer
arg1 Term Integer
arg2) =
    String
"DivInteger{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 Integer
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Integer
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ModIntegerTerm Int
i Term Integer
arg1 Term Integer
arg2) =
    String
"ModInteger{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 Integer
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Integer
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
  UBVConcatTerm ::
    ( SupportedPrim (bv a),
      SupportedPrim (bv b),
      SupportedPrim (bv c),
      KnownNat a,
      KnownNat b,
      KnownNat c,
      BVConcat (bv a) (bv b) (bv c)
    ) =>
    !(Term (bv a)) ->
    !(Term (bv b)) ->
    UTerm (bv c)
  UBVSelectTerm ::
    ( SupportedPrim (bv a),
      SupportedPrim (bv w),
      KnownNat a,
      KnownNat ix,
      KnownNat w,
      BVSelect (bv a) ix w (bv w)
    ) =>
    !(TypeRep ix) ->
    !(TypeRep w) ->
    !(Term (bv a)) ->
    UTerm (bv w)
  UBVExtendTerm ::
    ( SupportedPrim (bv a),
      SupportedPrim (bv b),
      KnownNat a,
      KnownNat b,
      KnownNat n,
      BVExtend (bv a) n (bv b)
    ) =>
    !Bool ->
    !(TypeRep n) ->
    !(Term (bv a)) ->
    UTerm (bv b)
  UTabularFunApplyTerm ::
    ( SupportedPrim a,
      SupportedPrim b
    ) =>
    Term (a =-> b) ->
    Term a ->
    UTerm b
  UGeneralFunApplyTerm ::
    ( SupportedPrim a,
      SupportedPrim b
    ) =>
    Term (a --> b) ->
    Term a ->
    UTerm b
  UDivIntegerTerm :: Term Integer -> Term Integer -> UTerm Integer
  UModIntegerTerm :: Term Integer -> Term Integer -> UTerm Integer

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)
    DBVSelectTerm ::
      forall bv (a :: Nat) (w :: Nat) (ix :: Nat).
      !(TypeRep ix) ->
      !(TypeRep (bv a), Id) ->
      Description (Term (bv w))
    DBVExtendTerm ::
      forall bv (a :: Nat) (b :: Nat) (n :: Nat).
      !Bool ->
      !(TypeRep n) ->
      {-# UNPACK #-} !(TypeRep (bv a), Id) ->
      Description (Term (bv b))
    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)
    DDivIntegerTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Integer)
    DModIntegerTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Integer)

  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 a t.
(Eq a, Hashable a) =>
(TypeRep a, a) -> (TypeRep a, 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 a b t.
(Eq a, Hashable a) =>
(TypeRep a, a)
-> (TypeRep a, Int) -> (TypeRep b, 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 a b n t.
(Eq a, Hashable a) =>
(TypeRep a, a)
-> (TypeRep a, Int)
-> (TypeRep b, Int)
-> (TypeRep n, 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 (UBVConcatTerm (Term (bv a)
arg1 :: bv1) (Term (bv b)
arg2 :: bv2)) =
    forall a a t.
TypeRep a -> TypeRep a -> 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 a)
arg :: Term arg)) =
    forall (a :: Natural -> *) (a :: Natural) (b :: Natural)
       (n :: Natural).
TypeRep n -> (TypeRep (a a), Int) -> Description (Term (a b))
DBVSelectTerm TypeRep ix
ix (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, forall t. Term t -> Int
identity Term (bv a)
arg)
  describe (UBVExtendTerm Bool
signed (TypeRep n
n :: TypeRep n) (Term (bv a)
arg :: Term arg)) =
    forall (a :: Natural -> *) (a :: Natural) (b :: Natural)
       (n :: Natural).
Bool
-> TypeRep n -> (TypeRep (a a), Int) -> Description (Term (a b))
DBVExtendTerm Bool
signed TypeRep n
n (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, forall t. Term t -> Int
identity Term (bv a)
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 (UDivIntegerTerm Term Integer
arg1 Term Integer
arg2) = Int -> Int -> Description (Term Integer)
DDivIntegerTerm (forall t. Term t -> Int
identity Term Integer
arg1) (forall t. Term t -> Int
identity Term Integer
arg2)
  describe (UModIntegerTerm Term Integer
arg1 Term Integer
arg2) = Int -> Int -> Description (Term Integer)
DModIntegerTerm (forall t. Term t -> Int
identity Term Integer
arg1) (forall t. Term t -> Int
identity Term Integer
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 a t. UnaryOp a a t => Int -> a -> Term a -> Term t
UnaryTerm Int
i tag
tag Term arg
tm
      go (UBinaryTerm tag
tag Term arg1
tm1 Term arg2
tm2) = forall a a b t.
BinaryOp a a b t =>
Int -> a -> Term a -> Term b -> 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 a b n t.
TernaryOp a a b n t =>
Int -> a -> Term a -> Term b -> Term n -> 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 (UBVConcatTerm Term (bv a)
arg1 Term (bv b)
arg2) = forall (a :: Natural -> *) (a :: Natural) (b :: Natural)
       (n :: Natural).
(SupportedPrim (a a), SupportedPrim (a b), SupportedPrim (a n),
 KnownNat a, KnownNat b, KnownNat n, BVConcat (a a) (a b) (a n)) =>
Int -> Term (a a) -> Term (a b) -> Term (a n)
BVConcatTerm Int
i Term (bv a)
arg1 Term (bv b)
arg2
      go (UBVSelectTerm TypeRep ix
ix TypeRep w
w Term (bv a)
arg) = forall (a :: Natural -> *) (a :: Natural) (b :: Natural)
       (n :: Natural).
(SupportedPrim (a a), SupportedPrim (a b), KnownNat a, KnownNat b,
 KnownNat n, BVSelect (a a) n b (a b)) =>
Int -> TypeRep n -> TypeRep b -> Term (a a) -> Term (a b)
BVSelectTerm Int
i TypeRep ix
ix TypeRep w
w Term (bv a)
arg
      go (UBVExtendTerm Bool
signed TypeRep n
n Term (bv a)
arg) = forall (a :: Natural -> *) (a :: Natural) (b :: Natural)
       (n :: Natural).
(SupportedPrim (a a), SupportedPrim (a b), KnownNat a, KnownNat b,
 KnownNat n, BVExtend (a a) n (a b)) =>
Int -> Bool -> TypeRep n -> Term (a a) -> Term (a b)
BVExtendTerm Int
i Bool
signed TypeRep n
n Term (bv a)
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 (UDivIntegerTerm Term Integer
arg1 Term Integer
arg2) = Int -> Term Integer -> Term Integer -> Term Integer
DivIntegerTerm Int
i Term Integer
arg1 Term Integer
arg2
      go (UModIntegerTerm Term Integer
arg1 Term Integer
arg2) = Int -> Term Integer -> Term Integer -> Term Integer
ModIntegerTerm Int
i Term Integer
arg1 Term Integer
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
  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 a), Int)
li == DBVSelectTerm TypeRep ix
rix (TypeRep (bv a), 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 a), Int)
li (TypeRep (bv a), Int)
ri
  DBVExtendTerm Bool
lIsSigned TypeRep n
ln (TypeRep (bv a), Int)
li == DBVExtendTerm Bool
rIsSigned TypeRep n
rn (TypeRep (bv a), 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 n
ln TypeRep n
rn
      Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (bv a), Int)
li (TypeRep (bv a), 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
  DDivIntegerTerm Int
li1 Int
li2 == DDivIntegerTerm 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
  DModIntegerTerm Int
li1 Int
li2 == DModIntegerTerm 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 (DBVConcatTerm TypeRep bv1
rep1 TypeRep bv2
rep2 Int
id1 Int
id2) =
    Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
23 :: 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 a), Int)
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
24 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep ix
ix forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (bv a), Int)
id1
  hashWithSalt Int
s (DBVExtendTerm Bool
signed TypeRep n
n (TypeRep (bv a), Int)
id1) =
    Int
s
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
25 :: Int)
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Bool
signed
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep n
n
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (bv a), 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
26 :: 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
27 :: 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 (DDivIntegerTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
28 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DModIntegerTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
29 :: 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

data FunArg = FunArg deriving (Int -> FunArg -> ShowS
[FunArg] -> ShowS
FunArg -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FunArg] -> ShowS
$cshowList :: [FunArg] -> ShowS
show :: FunArg -> String
$cshow :: FunArg -> String
showsPrec :: Int -> FunArg -> ShowS
$cshowsPrec :: Int -> FunArg -> ShowS
Show, FunArg -> FunArg -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FunArg -> FunArg -> Bool
$c/= :: FunArg -> FunArg -> Bool
== :: FunArg -> FunArg -> Bool
$c== :: FunArg -> FunArg -> Bool
Eq, forall x. Rep FunArg x -> FunArg
forall x. FunArg -> Rep FunArg x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep FunArg x -> FunArg
$cfrom :: forall x. FunArg -> Rep FunArg x
Generic, Eq FunArg
FunArg -> FunArg -> Bool
FunArg -> FunArg -> Ordering
FunArg -> FunArg -> FunArg
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 :: FunArg -> FunArg -> FunArg
$cmin :: FunArg -> FunArg -> FunArg
max :: FunArg -> FunArg -> FunArg
$cmax :: FunArg -> FunArg -> FunArg
>= :: FunArg -> FunArg -> Bool
$c>= :: FunArg -> FunArg -> Bool
> :: FunArg -> FunArg -> Bool
$c> :: FunArg -> FunArg -> Bool
<= :: FunArg -> FunArg -> Bool
$c<= :: FunArg -> FunArg -> Bool
< :: FunArg -> FunArg -> Bool
$c< :: FunArg -> FunArg -> Bool
compare :: FunArg -> FunArg -> Ordering
$ccompare :: FunArg -> FunArg -> 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 => FunArg -> m Exp
forall (m :: * -> *). Quote m => FunArg -> Code m FunArg
liftTyped :: forall (m :: * -> *). Quote m => FunArg -> Code m FunArg
$cliftTyped :: forall (m :: * -> *). Quote m => FunArg -> Code m FunArg
lift :: forall (m :: * -> *). Quote m => FunArg -> m Exp
$clift :: forall (m :: * -> *). Quote m => FunArg -> m Exp
Lift, Eq FunArg
Int -> FunArg -> Int
FunArg -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: FunArg -> Int
$chash :: FunArg -> Int
hashWithSalt :: Int -> FunArg -> Int
$chashWithSalt :: Int -> FunArg -> Int
Hashable, FunArg -> ()
forall a. (a -> ()) -> NFData a
rnf :: FunArg -> ()
$crnf :: FunArg -> ()
NFData)

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

infixr 0 -->

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
GeneralFun (forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
 Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo (forall t. SupportedPrim t => String -> TypedSymbol t
SimpleSymbol String
"a") FunArg
FunArg) (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall t. SupportedPrim t => t
defaultValue)