{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# 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
( SupportedPrim (..),
SymRep (..),
ConRep (..),
LinkedRep (..),
UnaryOp (..),
BinaryOp (..),
TernaryOp (..),
TypedSymbol (..),
SomeTypedSymbol (..),
showUntyped,
withSymbolSupported,
someTypedSymbol,
Term (..),
UTerm (..),
type (-->) (..),
buildGeneralFun,
prettyPrintTerm,
)
where
import Control.DeepSeq (NFData (rnf))
import Data.Bits (Bits, FiniteBits)
import Data.Function (on)
import Data.Hashable (Hashable (hashWithSalt))
import Data.Interned
( Cache,
Id,
Interned (Description, Uninterned, cache, describe, identify),
)
import Data.Kind (Constraint)
import Data.String (IsString (fromString))
import qualified Data.Text as T
import Data.Typeable (Proxy (Proxy), cast)
import GHC.Generics (Generic)
import GHC.TypeNats (KnownNat, Nat, type (+), type (<=))
import Grisette.Core.Data.BV (IntN, WordN)
import Grisette.Core.Data.Class.BitVector
( SizedBV,
)
import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#)))
import Grisette.Core.Data.Class.SignConversion (SignConversion)
import Grisette.Core.Data.Class.SymRotate (SymRotate)
import Grisette.Core.Data.Class.SymShift (SymShift)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches
( typeMemoizedCache,
)
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
( absNumTerm,
addNumTerm,
andBitsTerm,
andTerm,
bvconcatTerm,
bvextendTerm,
bvselectTerm,
complementBitsTerm,
conTerm,
constructBinary,
constructTernary,
constructUnary,
divBoundedIntegralTerm,
divIntegralTerm,
eqvTerm,
generalFunApplyTerm,
iteTerm,
leNumTerm,
ltNumTerm,
modBoundedIntegralTerm,
modIntegralTerm,
notTerm,
orBitsTerm,
orTerm,
quotBoundedIntegralTerm,
quotIntegralTerm,
remBoundedIntegralTerm,
remIntegralTerm,
rotateLeftTerm,
rotateRightTerm,
shiftLeftTerm,
shiftRightTerm,
signumNumTerm,
symTerm,
tabularFunApplyTerm,
timesNumTerm,
toSignedTerm,
toUnsignedTerm,
uminusNumTerm,
xorBitsTerm,
)
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
( substTerm,
)
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
( identity,
introSupportedPrimConstraint,
pformat,
)
import Grisette.IR.SymPrim.Data.Prim.ModelValue
( ModelValue,
toModelValue,
)
import Grisette.IR.SymPrim.Data.Prim.Utils
( eqHeteroRep,
eqTypeRepBool,
)
import Grisette.IR.SymPrim.Data.TabularFun
( type (=->) (TabularFun),
)
import Language.Haskell.TH.Syntax (Lift (lift, liftTyped))
import Language.Haskell.TH.Syntax.Compat (unTypeSplice)
import Type.Reflection
( SomeTypeRep (SomeTypeRep),
TypeRep,
Typeable,
eqTypeRep,
typeRep,
type (:~~:) (HRefl),
)
#if MIN_VERSION_prettyprinter(1,7,0)
import Prettyprinter
( column,
pageWidth,
Doc,
PageWidth(Unbounded, AvailablePerLine),
Pretty(pretty),
)
#else
import Data.Text.Prettyprint.Doc
( column,
pageWidth,
Doc,
PageWidth(Unbounded, AvailablePerLine),
Pretty(pretty),
)
#endif
class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where
type PrimConstraint t :: Constraint
type PrimConstraint _ = ()
default withPrim :: (PrimConstraint t) => proxy t -> ((PrimConstraint t) => a) -> a
withPrim :: proxy t -> ((PrimConstraint t) => a) -> a
withPrim proxy t
_ PrimConstraint t => a
i = a
PrimConstraint t => a
i
termCache :: Cache (Term t)
termCache = Cache (Term t)
forall a. (Interned a, Typeable a) => Cache a
typeMemoizedCache
pformatCon :: t -> String
default pformatCon :: (Show t) => t -> String
pformatCon = t -> String
forall a. Show a => a -> String
show
pformatSym :: TypedSymbol t -> String
pformatSym = TypedSymbol t -> String
forall t. TypedSymbol t -> String
showUntyped
defaultValue :: t
defaultValueDynamic :: proxy t -> ModelValue
defaultValueDynamic proxy t
_ = t -> ModelValue
forall a. (Show a, Eq a, Hashable a, Typeable a) => a -> ModelValue
toModelValue (forall t. SupportedPrim t => t
defaultValue @t)
class ConRep sym where
type ConType sym
class (SupportedPrim con) => SymRep con where
type SymType con
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
data TypedSymbol t where
SimpleSymbol :: (SupportedPrim t) => T.Text -> TypedSymbol t
IndexedSymbol :: (SupportedPrim t) => T.Text -> 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
instance Eq (TypedSymbol t) where
SimpleSymbol Text
x == :: TypedSymbol t -> TypedSymbol t -> Bool
== SimpleSymbol Text
y = Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
y
IndexedSymbol Text
x Int
i == IndexedSymbol Text
y Int
j = Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j Bool -> Bool -> Bool
&& Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
y
WithInfo TypedSymbol t
s1 (a
i1 :: a) == WithInfo TypedSymbol t
s2 (a
i2 :: b) = case TypeRep a -> TypeRep a -> Maybe (a :~~: a)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b) of
Just a :~~: a
HRefl -> a
i1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a
i2 Bool -> Bool -> Bool
&& TypedSymbol t
s1 TypedSymbol t -> TypedSymbol t -> Bool
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 Text
x <= :: TypedSymbol t -> TypedSymbol t -> Bool
<= SimpleSymbol Text
y = Text
x Text -> Text -> Bool
forall a. Ord a => a -> a -> Bool
<= Text
y
IndexedSymbol Text
x Int
i <= IndexedSymbol Text
y Int
j = Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
j Bool -> Bool -> Bool
|| (Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j Bool -> Bool -> Bool
&& Text
x Text -> Text -> Bool
forall a. Ord a => a -> a -> Bool
<= Text
y)
WithInfo TypedSymbol t
s1 (a
i1 :: a) <= WithInfo TypedSymbol t
s2 (a
i2 :: b) = case TypeRep a -> TypeRep a -> Maybe (a :~~: a)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b) of
Just a :~~: a
HRefl -> TypedSymbol t
s1 TypedSymbol t -> TypedSymbol t -> Bool
forall a. Ord a => a -> a -> Bool
< TypedSymbol t
s2 Bool -> Bool -> Bool
|| (TypedSymbol t
s1 TypedSymbol t -> TypedSymbol t -> Bool
forall a. Eq a => a -> a -> Bool
== TypedSymbol t
s2 Bool -> Bool -> Bool
&& a
i1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
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 Text
x) = [||Text -> TypedSymbol t
forall t. SupportedPrim t => Text -> TypedSymbol t
SimpleSymbol Text
x||]
liftTyped (IndexedSymbol Text
x Int
i) = [||Text -> Int -> TypedSymbol t
forall t. SupportedPrim t => Text -> Int -> TypedSymbol t
IndexedSymbol Text
x Int
i||]
liftTyped (WithInfo TypedSymbol t
s1 a
i1) = [||TypedSymbol t -> a -> TypedSymbol t
forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo TypedSymbol t
s1 a
i1||]
instance Show (TypedSymbol t) where
show :: TypedSymbol t -> String
show (SimpleSymbol Text
str) = Text -> String
T.unpack Text
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep t -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t)
show (IndexedSymbol Text
str Int
i) = Text -> String
T.unpack Text
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep t -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t)
show (WithInfo TypedSymbol t
s a
info) = TypedSymbol t -> String
forall t. TypedSymbol t -> String
showUntyped TypedSymbol t
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
info String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep t -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t)
showUntyped :: TypedSymbol t -> String
showUntyped :: forall t. TypedSymbol t -> String
showUntyped (SimpleSymbol Text
str) = Text -> String
T.unpack Text
str
showUntyped (IndexedSymbol Text
str Int
i) = Text -> String
T.unpack Text
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
showUntyped (WithInfo TypedSymbol t
s a
info) = TypedSymbol t -> String
forall t. TypedSymbol t -> String
showUntyped TypedSymbol t
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
info
instance Hashable (TypedSymbol t) where
Int
s hashWithSalt :: Int -> TypedSymbol t -> Int
`hashWithSalt` SimpleSymbol Text
x = Int
s Int -> Text -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Text
x
Int
s `hashWithSalt` IndexedSymbol Text
x Int
i = Int
s Int -> Text -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Text
x Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
i
Int
s `hashWithSalt` WithInfo TypedSymbol t
sym a
info = Int
s Int -> TypedSymbol t -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol t
sym Int -> a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` a
info
instance NFData (TypedSymbol t) where
rnf :: TypedSymbol t -> ()
rnf (SimpleSymbol Text
str) = Text -> ()
forall a. NFData a => a -> ()
rnf Text
str
rnf (IndexedSymbol Text
str Int
i) = Text -> ()
forall a. NFData a => a -> ()
rnf Text
str () -> () -> ()
forall a b. a -> b -> b
`seq` Int -> ()
forall a. NFData a => a -> ()
rnf Int
i
rnf (WithInfo TypedSymbol t
s a
info) = TypedSymbol t -> ()
forall a. NFData a => a -> ()
rnf TypedSymbol t
s () -> () -> ()
forall a b. a -> b -> b
`seq` a -> ()
forall a. NFData a => a -> ()
rnf a
info
instance (SupportedPrim t) => IsString (TypedSymbol t) where
fromString :: String -> TypedSymbol t
fromString = Text -> TypedSymbol t
forall t. SupportedPrim t => Text -> TypedSymbol t
SimpleSymbol (Text -> TypedSymbol t)
-> (String -> Text) -> String -> TypedSymbol t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack
withSymbolSupported :: TypedSymbol t -> ((SupportedPrim t) => a) -> a
withSymbolSupported :: forall t a. TypedSymbol t -> (SupportedPrim t => a) -> a
withSymbolSupported (SimpleSymbol Text
_) SupportedPrim t => a
a = a
SupportedPrim t => a
a
withSymbolSupported (IndexedSymbol Text
_ Int
_) SupportedPrim t => a
a = a
SupportedPrim t => a
a
withSymbolSupported (WithInfo TypedSymbol t
_ a
_) SupportedPrim t => a
a = a
SupportedPrim t => a
a
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) = SomeTypeRep -> ()
forall a. NFData a => a -> ()
rnf (TypeRep t -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep t
p) () -> () -> ()
forall a b. a -> b -> b
`seq` TypedSymbol t -> ()
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 TypeRep t -> TypeRep t -> Maybe (t :~~: t)
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 TypedSymbol t -> TypedSymbol t -> Bool
forall a. Eq a => a -> a -> Bool
== TypedSymbol t
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) =
TypeRep t -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep t
t1 SomeTypeRep -> SomeTypeRep -> Bool
forall a. Ord a => a -> a -> Bool
< TypeRep t -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep t
t2
Bool -> Bool -> Bool
|| ( case TypeRep t -> TypeRep t -> Maybe (t :~~: t)
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 TypedSymbol t -> TypedSymbol t -> Bool
forall a. Ord a => a -> a -> Bool
<= TypedSymbol t
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 Int -> TypedSymbol t -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol t
s1 Int -> TypeRep t -> Int
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) = TypedSymbol t -> String
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 Text
_) = TypeRep t -> TypedSymbol t -> SomeTypedSymbol
forall a. TypeRep a -> TypedSymbol a -> SomeTypedSymbol
SomeTypedSymbol (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t) TypedSymbol t
s
someTypedSymbol s :: TypedSymbol t
s@(IndexedSymbol Text
_ Int
_) = TypeRep t -> TypedSymbol t -> SomeTypedSymbol
forall a. TypeRep a -> TypedSymbol a -> SomeTypedSymbol
SomeTypedSymbol (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t) TypedSymbol t
s
someTypedSymbol s :: TypedSymbol t
s@(WithInfo TypedSymbol t
_ a
_) = TypeRep t -> TypedSymbol t -> SomeTypedSymbol
forall a. TypeRep a -> TypedSymbol a -> SomeTypedSymbol
SomeTypedSymbol (forall a. Typeable a => TypeRep a
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
ShiftLeftTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymShift t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
ShiftRightTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymShift t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
RotateLeftTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymRotate t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
RotateRightTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymRotate t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
ToSignedTerm ::
( SupportedPrim u,
SupportedPrim s,
SignConversion u s
) =>
{-# UNPACK #-} !Id ->
!(Term u) ->
Term s
ToUnsignedTerm ::
( SupportedPrim u,
SupportedPrim s,
SignConversion u s
) =>
{-# UNPACK #-} !Id ->
!(Term s) ->
Term u
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 = Term a -> Int
forall t. Term t -> Int
identity Term a
i Int -> () -> ()
forall a b. a -> b -> b
`seq` ()
instance Lift (Term t) where
lift :: forall (m :: * -> *). Quote m => Term t -> m Exp
lift = Splice m (Term t) -> m Exp
forall a (m :: * -> *). Quote m => Splice m a -> m Exp
unTypeSplice (Splice m (Term t) -> m Exp)
-> (Term t -> Splice m (Term t)) -> Term t -> m Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term t -> Splice m (Term t)
forall t (m :: * -> *). (Lift t, Quote m) => t -> Code m t
forall (m :: * -> *). Quote m => Term t -> Code m (Term t)
liftTyped
liftTyped :: forall (m :: * -> *). Quote m => Term t -> Code m (Term t)
liftTyped (ConTerm Int
_ t
i) = [||t -> Term t
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm t
i||]
liftTyped (SymTerm Int
_ TypedSymbol t
sym) = [||TypedSymbol t -> Term t
forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm TypedSymbol t
sym||]
liftTyped (UnaryTerm Int
_ tag
tag Term arg
arg) = [||tag -> Term arg -> Term t
forall tag arg t.
(SupportedPrim t, UnaryOp tag arg t, Typeable tag, Typeable t,
Show tag) =>
tag -> Term arg -> Term t
constructUnary tag
tag Term arg
arg||]
liftTyped (BinaryTerm Int
_ tag
tag Term arg1
arg1 Term arg2
arg2) = [||tag -> Term arg1 -> Term arg2 -> Term t
forall tag arg1 arg2 t.
(SupportedPrim t, BinaryOp tag arg1 arg2 t, Typeable tag,
Typeable t, Show tag) =>
tag -> Term arg1 -> Term arg2 -> Term t
constructBinary tag
tag Term arg1
arg1 Term arg2
arg2||]
liftTyped (TernaryTerm Int
_ tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) = [||tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
forall tag arg1 arg2 arg3 t.
(SupportedPrim t, TernaryOp tag arg1 arg2 arg3 t, Typeable tag,
Typeable t, Show tag) =>
tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
constructTernary tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3||]
liftTyped (NotTerm Int
_ Term Bool
arg) = [||Term Bool -> Term Bool
notTerm Term Bool
arg||]
liftTyped (OrTerm Int
_ Term Bool
arg1 Term Bool
arg2) = [||Term Bool -> Term Bool -> Term Bool
orTerm Term Bool
arg1 Term Bool
arg2||]
liftTyped (AndTerm Int
_ Term Bool
arg1 Term Bool
arg2) = [||Term Bool -> Term Bool -> Term Bool
andTerm Term Bool
arg1 Term Bool
arg2||]
liftTyped (EqvTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
eqvTerm Term t
arg1 Term t
arg2||]
liftTyped (ITETerm Int
_ Term Bool
cond Term t
arg1 Term t
arg2) = [||Term Bool -> Term a -> Term a -> Term a
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
iteTerm Term Bool
cond Term t
arg1 Term t
arg2||]
liftTyped (AddNumTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a. (SupportedPrim a, Num a) => Term a -> Term a -> Term a
addNumTerm Term t
arg1 Term t
arg2||]
liftTyped (UMinusNumTerm Int
_ Term t
arg) = [||Term a -> Term a
forall a. (SupportedPrim a, Num a) => Term a -> Term a
uminusNumTerm Term t
arg||]
liftTyped (TimesNumTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a. (SupportedPrim a, Num a) => Term a -> Term a -> Term a
timesNumTerm Term t
arg1 Term t
arg2||]
liftTyped (AbsNumTerm Int
_ Term t
arg) = [||Term a -> Term a
forall a. (SupportedPrim a, Num a) => Term a -> Term a
absNumTerm Term t
arg||]
liftTyped (SignumNumTerm Int
_ Term t
arg) = [||Term a -> Term a
forall a. (SupportedPrim a, Num a) => Term a -> Term a
signumNumTerm Term t
arg||]
liftTyped (LTNumTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term Bool
forall a.
(SupportedPrim a, Num a, Ord a) =>
Term a -> Term a -> Term Bool
ltNumTerm Term t
arg1 Term t
arg2||]
liftTyped (LENumTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term Bool
forall a.
(SupportedPrim a, Num a, Ord a) =>
Term a -> Term a -> Term Bool
leNumTerm Term t
arg1 Term t
arg2||]
liftTyped (AndBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a. (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
andBitsTerm Term t
arg1 Term t
arg2||]
liftTyped (OrBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a. (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
orBitsTerm Term t
arg1 Term t
arg2||]
liftTyped (XorBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a. (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
xorBitsTerm Term t
arg1 Term t
arg2||]
liftTyped (ComplementBitsTerm Int
_ Term t
arg) = [||Term a -> Term a
forall a. (SupportedPrim a, Bits a) => Term a -> Term a
complementBitsTerm Term t
arg||]
liftTyped (ShiftLeftTerm Int
_ Term t
arg Term t
n) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymShift a) =>
Term a -> Term a -> Term a
shiftLeftTerm Term t
arg Term t
n||]
liftTyped (ShiftRightTerm Int
_ Term t
arg Term t
n) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymShift a) =>
Term a -> Term a -> Term a
shiftRightTerm Term t
arg Term t
n||]
liftTyped (RotateLeftTerm Int
_ Term t
arg Term t
n) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymRotate a) =>
Term a -> Term a -> Term a
rotateLeftTerm Term t
arg Term t
n||]
liftTyped (RotateRightTerm Int
_ Term t
arg Term t
n) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymRotate a) =>
Term a -> Term a -> Term a
rotateRightTerm Term t
arg Term t
n||]
liftTyped (ToSignedTerm Int
_ Term u
v) = [||Term u -> Term s
forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term u -> Term s
toSignedTerm Term u
v||]
liftTyped (ToUnsignedTerm Int
_ Term s
v) = [||Term s -> Term u
forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term s -> Term u
toUnsignedTerm Term s
v||]
liftTyped (BVConcatTerm Int
_ Term (bv a)
arg1 Term (bv b)
arg2) = [||Term (bv a) -> Term (bv b) -> Term (bv (a + b))
forall (bv :: Nat -> *) (a :: Nat) (b :: Nat).
(forall (n :: Nat). (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) -> Term (bv (a + b))
bvconcatTerm Term (bv a)
arg1 Term (bv b)
arg2||]
liftTyped (BVSelectTerm Int
_ (TypeRep ix
_ :: TypeRep ix) (TypeRep w
_ :: TypeRep w) Term (bv n)
arg) = [||p ix -> q w -> Term (bv n) -> Term (bv w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(forall (n1 :: Nat).
(KnownNat n1, 1 <= n1) =>
SupportedPrim (bv n1),
Typeable bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n, SizedBV bv) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
bvselectTerm (forall (t :: k). Proxy t
forall {k} (t :: k). Proxy t
Proxy @ix) (forall (t :: k). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) Term (bv n)
arg||]
liftTyped (BVExtendTerm Int
_ Bool
signed (TypeRep r
_ :: TypeRep n) Term (bv l)
arg) = [||Bool -> proxy r -> Term (bv l) -> Term (bv r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
SizedBV bv) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
bvextendTerm Bool
signed (forall (t :: k). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) Term (bv l)
arg||]
liftTyped (TabularFunApplyTerm Int
_ Term (a =-> t)
func Term a
arg) = [||Term (a =-> b) -> Term a -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> Term a -> Term b
tabularFunApplyTerm Term (a =-> t)
func Term a
arg||]
liftTyped (GeneralFunApplyTerm Int
_ Term (a --> t)
func Term a
arg) = [||Term (a --> b) -> Term a -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
generalFunApplyTerm Term (a --> t)
func Term a
arg||]
liftTyped (DivIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
divIntegralTerm Term t
arg1 Term t
arg2||]
liftTyped (ModIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
modIntegralTerm Term t
arg1 Term t
arg2||]
liftTyped (QuotIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
quotIntegralTerm Term t
arg1 Term t
arg2||]
liftTyped (RemIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
remIntegralTerm Term t
arg1 Term t
arg2||]
liftTyped (DivBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
divBoundedIntegralTerm Term t
arg1 Term t
arg2||]
liftTyped (ModBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
modBoundedIntegralTerm Term t
arg1 Term t
arg2||]
liftTyped (QuotBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
quotBoundedIntegralTerm Term t
arg1 Term t
arg2||]
liftTyped (RemBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
remBoundedIntegralTerm Term t
arg1 Term t
arg2||]
instance Show (Term ty) where
show :: Term ty -> String
show (ConTerm Int
i ty
v) = String
"ConTerm{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", v=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ty -> String
forall a. Show a => a -> String
show ty
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (SymTerm Int
i TypedSymbol ty
name) =
String
"SymTerm{id="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", name="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypedSymbol ty -> String
forall a. Show a => a -> String
show TypedSymbol ty
name
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", type="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep ty -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @ty)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (UnaryTerm Int
i tag
tag Term arg
arg) = String
"Unary{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", tag=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ tag -> String
forall a. Show a => a -> String
show tag
tag String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg -> String
forall a. Show a => a -> String
show Term arg
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (BinaryTerm Int
i tag
tag Term arg1
arg1 Term arg2
arg2) =
String
"Binary{id="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", tag="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ tag -> String
forall a. Show a => a -> String
show tag
tag
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg1 -> String
forall a. Show a => a -> String
show Term arg1
arg1
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg2 -> String
forall a. Show a => a -> String
show Term arg2
arg2
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (TernaryTerm Int
i tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) =
String
"Ternary{id="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", tag="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ tag -> String
forall a. Show a => a -> String
show tag
tag
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg1 -> String
forall a. Show a => a -> String
show Term arg1
arg1
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg2 -> String
forall a. Show a => a -> String
show Term arg2
arg2
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg3="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg3 -> String
forall a. Show a => a -> String
show Term arg3
arg3
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (NotTerm Int
i Term Bool
arg) = String
"Not{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (OrTerm Int
i Term Bool
arg1 Term Bool
arg2) = String
"Or{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (AndTerm Int
i Term Bool
arg1 Term Bool
arg2) = String
"And{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (EqvTerm Int
i Term t
arg1 Term t
arg2) = String
"Eqv{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (ITETerm Int
i Term Bool
cond Term ty
l Term ty
r) =
String
"ITE{id="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", cond="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
cond
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", then="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
l
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", else="
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
r
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (AddNumTerm Int
i Term ty
arg1 Term ty
arg2) = String
"AddNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (UMinusNumTerm Int
i Term ty
arg) = String
"UMinusNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (TimesNumTerm Int
i Term ty
arg1 Term ty
arg2) = String
"TimesNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (AbsNumTerm Int
i Term ty
arg) = String
"AbsNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (SignumNumTerm Int
i Term ty
arg) = String
"SignumNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (LTNumTerm Int
i Term t
arg1 Term t
arg2) = String
"LTNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (LENumTerm Int
i Term t
arg1 Term t
arg2) = String
"LENum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (AndBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"AndBits{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (OrBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"OrBits{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (XorBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"XorBits{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (ComplementBitsTerm Int
i Term ty
arg) = String
"ComplementBits{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (ShiftLeftTerm Int
i Term ty
arg Term ty
n) = String
"ShiftLeft{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", n=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (ShiftRightTerm Int
i Term ty
arg Term ty
n) = String
"ShiftRight{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", n=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (RotateLeftTerm Int
i Term ty
arg Term ty
n) = String
"RotateLeft{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", n=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (RotateRightTerm Int
i Term ty
arg Term ty
n) = String
"RotateRight{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", n=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (ToSignedTerm Int
i Term u
arg) = String
"ToSigned{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term u -> String
forall a. Show a => a -> String
show Term u
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (ToUnsignedTerm Int
i Term s
arg) = String
"ToUnsigned{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term s -> String
forall a. Show a => a -> String
show Term s
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (BVConcatTerm Int
i Term (bv a)
arg1 Term (bv b)
arg2) = String
"BVConcat{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (bv a) -> String
forall a. Show a => a -> String
show Term (bv a)
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (bv b) -> String
forall a. Show a => a -> String
show Term (bv b)
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (BVSelectTerm Int
i TypeRep ix
ix TypeRep w
w Term (bv n)
arg) =
String
"BVSelect{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", ix=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep ix -> String
forall a. Show a => a -> String
show TypeRep ix
ix String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", w=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep w -> String
forall a. Show a => a -> String
show TypeRep w
w String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (bv n) -> String
forall a. Show a => a -> String
show Term (bv n)
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (BVExtendTerm Int
i Bool
signed TypeRep r
n Term (bv l)
arg) =
String
"BVExtend{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", signed=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show Bool
signed String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", n=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep r -> String
forall a. Show a => a -> String
show TypeRep r
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (bv l) -> String
forall a. Show a => a -> String
show Term (bv l)
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (TabularFunApplyTerm Int
i Term (a =-> ty)
func Term a
arg) =
String
"TabularFunApply{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", func=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (a =-> ty) -> String
forall a. Show a => a -> String
show Term (a =-> ty)
func String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term a -> String
forall a. Show a => a -> String
show Term a
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (GeneralFunApplyTerm Int
i Term (a --> ty)
func Term a
arg) =
String
"GeneralFunApply{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", func=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (a --> ty) -> String
forall a. Show a => a -> String
show Term (a --> ty)
func String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term a -> String
forall a. Show a => a -> String
show Term a
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (DivIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"DivIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (ModIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"ModIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (QuotIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"QuotIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (RemIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"RemIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (DivBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"DivBoundedIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (ModBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"ModBoundedIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (QuotBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"QuotBoundedIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
show (RemBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"RemBoundedIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
prettyPrintTerm :: Term t -> Doc ann
prettyPrintTerm :: forall t ann. Term t -> Doc ann
prettyPrintTerm Term t
v =
(Int -> Doc ann) -> Doc ann
forall ann. (Int -> Doc ann) -> Doc ann
column
( \Int
c ->
(PageWidth -> Doc ann) -> Doc ann
forall ann. (PageWidth -> Doc ann) -> Doc ann
pageWidth ((PageWidth -> Doc ann) -> Doc ann)
-> (PageWidth -> Doc ann) -> Doc ann
forall a b. (a -> b) -> a -> b
$ \case
AvailablePerLine Int
i Double
r ->
if Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
len) Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
r
then Doc ann
"..."
else String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
formatted
PageWidth
Unbounded -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
formatted
)
where
formatted :: String
formatted = Term t -> (SupportedPrim t => String) -> String
forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term t
v ((SupportedPrim t => String) -> String)
-> (SupportedPrim t => String) -> String
forall a b. (a -> b) -> a -> b
$ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
v
len :: Int
len = String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
formatted
instance (SupportedPrim t) => Eq (Term t) where
== :: Term t -> Term t -> Bool
(==) = Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Int -> Int -> Bool) -> (Term t -> Int) -> Term t -> Term t -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Term t -> Int
forall t. Term t -> Int
identity
instance (SupportedPrim t) => Hashable (Term t) where
hashWithSalt :: Int -> Term t -> Int
hashWithSalt Int
s Term t
t = Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Term t -> Int
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
UShiftLeftTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymShift t) => !(Term t) -> !(Term t) -> UTerm t
UShiftRightTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymShift t) => !(Term t) -> !(Term t) -> UTerm t
URotateLeftTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymRotate t) => !(Term t) -> !(Term t) -> UTerm t
URotateRightTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymRotate t) => !(Term t) -> !(Term t) -> UTerm t
UToSignedTerm ::
( SupportedPrim u,
SupportedPrim s,
SignConversion u s
) =>
!(Term u) ->
UTerm s
UToUnsignedTerm ::
( SupportedPrim u,
SupportedPrim s,
SignConversion u s
) =>
!(Term s) ->
UTerm u
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i2 Bool -> Bool -> Bool
&& TypeRep a -> TypeRep b -> 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) = TypeRep a -> TypeRep b -> a -> b -> Bool
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)
DShiftLeftTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DShiftRightTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DRotateLeftTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DRotateRightTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DBVConcatTerm :: TypeRep bv1 -> TypeRep bv2 -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DToSignedTerm ::
!(TypeRep u, Id) ->
Description (Term s)
DToUnsignedTerm ::
!(TypeRep s, Id) ->
Description (Term u)
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) = t -> Description (Term t)
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) =
(TypeRep tag, tag) -> (TypeRep arg, Int) -> Description (Term t)
forall a l t.
(Eq a, Hashable a) =>
(TypeRep a, a) -> (TypeRep l, Int) -> Description (Term t)
DUnaryTerm (TypeRep tag
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag) (TypeRep arg
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, Term arg -> Int
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 (TypeRep tag
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag) (TypeRep arg1
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, Term arg1 -> Int
forall t. Term t -> Int
identity Term arg1
tm1) (TypeRep arg2
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, Term arg2 -> Int
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
(TypeRep tag
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag)
(TypeRep arg1
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, Term arg1 -> Int
forall t. Term t -> Int
identity Term arg1
tm1)
(TypeRep arg2
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, Term arg2 -> Int
forall t. Term t -> Int
identity Term arg2
tm2)
(TypeRep arg3
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, Term arg3 -> Int
forall t. Term t -> Int
identity Term arg3
tm3)
describe (UNotTerm Term Bool
arg) = Int -> Description (Term Bool)
DNotTerm (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
arg)
describe (UOrTerm Term Bool
arg1 Term Bool
arg2) = Int -> Int -> Description (Term Bool)
DOrTerm (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
arg1) (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
arg2)
describe (UAndTerm Term Bool
arg1 Term Bool
arg2) = Int -> Int -> Description (Term Bool)
DAndTerm (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
arg1) (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
arg2)
describe (UEqvTerm (Term t
arg1 :: Term arg) Term t
arg2) = TypeRep t -> Int -> Int -> Description (Term Bool)
forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DEqvTerm (TypeRep t
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
describe (UITETerm Term Bool
cond (Term t
l :: Term arg) Term t
r) = Int -> Int -> Int -> Description (Term t)
forall t. Int -> Int -> Int -> Description (Term t)
DITETerm (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
cond) (Term t -> Int
forall t. Term t -> Int
identity Term t
l) (Term t -> Int
forall t. Term t -> Int
identity Term t
r)
describe (UAddNumTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DAddNumTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
describe (UUMinusNumTerm Term t
arg) = Int -> Description (Term t)
forall t. Int -> Description (Term t)
DUMinusNumTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg)
describe (UTimesNumTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DTimesNumTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
describe (UAbsNumTerm Term t
arg) = Int -> Description (Term t)
forall t. Int -> Description (Term t)
DAbsNumTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg)
describe (USignumNumTerm Term t
arg) = Int -> Description (Term t)
forall t. Int -> Description (Term t)
DSignumNumTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg)
describe (ULTNumTerm (Term t
arg1 :: arg) Term t
arg2) = TypeRep (Term t) -> Int -> Int -> Description (Term Bool)
forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DLTNumTerm (TypeRep (Term t)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
describe (ULENumTerm (Term t
arg1 :: arg) Term t
arg2) = TypeRep (Term t) -> Int -> Int -> Description (Term Bool)
forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DLENumTerm (TypeRep (Term t)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
describe (UAndBitsTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DAndBitsTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
describe (UOrBitsTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DOrBitsTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
describe (UXorBitsTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DXorBitsTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
describe (UComplementBitsTerm Term t
arg) = Int -> Description (Term t)
forall t. Int -> Description (Term t)
DComplementBitsTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg)
describe (UShiftLeftTerm Term t
arg Term t
n) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DShiftLeftTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
n)
describe (UShiftRightTerm Term t
arg Term t
n) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DShiftRightTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
n)
describe (URotateLeftTerm Term t
arg Term t
n) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DRotateLeftTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
n)
describe (URotateRightTerm Term t
arg Term t
n) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DRotateRightTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
n)
describe (UToSignedTerm (Term u
arg :: Term bv)) = (TypeRep u, Int) -> Description (Term t)
forall a s. (TypeRep a, Int) -> Description (Term s)
DToSignedTerm (TypeRep u
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv, Term u -> Int
forall t. Term t -> Int
identity Term u
arg)
describe (UToUnsignedTerm (Term s
arg :: Term bv)) = (TypeRep s, Int) -> Description (Term t)
forall a s. (TypeRep a, Int) -> Description (Term s)
DToSignedTerm (TypeRep s
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv, Term s -> Int
forall t. Term t -> Int
identity Term s
arg)
describe (UBVConcatTerm (Term (bv a)
arg1 :: bv1) (Term (bv b)
arg2 :: bv2)) =
TypeRep (Term (bv a))
-> TypeRep (Term (bv b)) -> Int -> Int -> Description (Term t)
forall a l t.
TypeRep a -> TypeRep l -> Int -> Int -> Description (Term t)
DBVConcatTerm (TypeRep (Term (bv a))
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv1) (TypeRep (Term (bv b))
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv2) (Term (bv a) -> Int
forall t. Term t -> Int
identity Term (bv a)
arg1) (Term (bv b) -> Int
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)) =
TypeRep ix -> (TypeRep (bv n), Int) -> Description (Term (bv w))
forall (a :: Nat -> *) (l :: Nat) (r :: Nat) (w :: Nat).
TypeRep w -> (TypeRep (a l), Int) -> Description (Term (a r))
DBVSelectTerm TypeRep ix
ix (TypeRep (bv n)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, Term (bv n) -> Int
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)) =
Bool
-> TypeRep r -> (TypeRep (bv l), Int) -> Description (Term (bv r))
forall (a :: Nat -> *) (l :: Nat) (r :: Nat).
Bool
-> TypeRep r -> (TypeRep (a l), Int) -> Description (Term (a r))
DBVExtendTerm Bool
signed TypeRep r
n (TypeRep (bv l)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, Term (bv l) -> Int
forall t. Term t -> Int
identity Term (bv l)
arg)
describe (UTabularFunApplyTerm (Term (a =-> t)
func :: Term f) (Term a
arg :: Term a)) =
(TypeRep (a =-> t), Int)
-> (TypeRep a, Int) -> Description (Term t)
forall a b.
(TypeRep (a =-> b), Int)
-> (TypeRep a, Int) -> Description (Term b)
DTabularFunApplyTerm (TypeRep (a =-> t)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep f, Term (a =-> t) -> Int
forall t. Term t -> Int
identity Term (a =-> t)
func) (TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep a, Term a -> Int
forall t. Term t -> Int
identity Term a
arg)
describe (UGeneralFunApplyTerm (Term (a --> t)
func :: Term f) (Term a
arg :: Term a)) =
(TypeRep (a --> t), Int)
-> (TypeRep a, Int) -> Description (Term t)
forall a b.
(TypeRep (a --> b), Int)
-> (TypeRep a, Int) -> Description (Term b)
DGeneralFunApplyTerm (TypeRep (a --> t)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep f, Term (a --> t) -> Int
forall t. Term t -> Int
identity Term (a --> t)
func) (TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep a, Term a -> Int
forall t. Term t -> Int
identity Term a
arg)
describe (UDivIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DDivIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
describe (UModIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DModIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
describe (UQuotIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DRemIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
describe (URemIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DQuotIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
describe (UDivBoundedIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DDivBoundedIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
describe (UModBoundedIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DModBoundedIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
describe (UQuotBoundedIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DRemBoundedIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
describe (URemBoundedIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DQuotBoundedIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
identify :: Int -> Uninterned (Term t) -> Term t
identify Int
i = Uninterned (Term t) -> Term t
UTerm t -> Term t
go
where
go :: UTerm t -> Term t
go (UConTerm t
v) = Int -> t -> Term t
forall t. SupportedPrim t => Int -> t -> Term t
ConTerm Int
i t
v
go (USymTerm TypedSymbol t
v) = Int -> TypedSymbol t -> Term t
forall t. SupportedPrim t => Int -> TypedSymbol t -> Term t
SymTerm Int
i TypedSymbol t
v
go (UUnaryTerm tag
tag Term arg
tm) = Int -> tag -> Term arg -> Term t
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) = Int -> tag -> Term arg1 -> Term arg2 -> Term t
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) = Int -> tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
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) = Int -> Term t -> Term t -> Term Bool
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) = Int -> Term Bool -> Term t -> Term t -> Term t
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) = Int -> Term t -> Term t -> Term t
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) = Int -> Term t -> Term t
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) = Int -> Term t -> Term t -> Term t
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) = Int -> Term t -> Term t
forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
AbsNumTerm Int
i Term t
arg
go (USignumNumTerm Term t
arg) = Int -> Term t -> Term t
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) = Int -> Term t -> Term t -> Term Bool
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) = Int -> Term t -> Term t -> Term Bool
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) = Int -> Term t -> Term t -> Term t
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) = Int -> Term t -> Term t -> Term t
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) = Int -> Term t -> Term t -> Term t
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) = Int -> Term t -> Term t
forall t. (SupportedPrim t, Bits t) => Int -> Term t -> Term t
ComplementBitsTerm Int
i Term t
arg
go (UShiftLeftTerm Term t
arg Term t
n) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Integral t, FiniteBits t, SymShift t) =>
Int -> Term t -> Term t -> Term t
ShiftLeftTerm Int
i Term t
arg Term t
n
go (UShiftRightTerm Term t
arg Term t
n) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Integral t, FiniteBits t, SymShift t) =>
Int -> Term t -> Term t -> Term t
ShiftRightTerm Int
i Term t
arg Term t
n
go (URotateLeftTerm Term t
arg Term t
n) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Integral t, FiniteBits t, SymRotate t) =>
Int -> Term t -> Term t -> Term t
RotateLeftTerm Int
i Term t
arg Term t
n
go (URotateRightTerm Term t
arg Term t
n) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Integral t, FiniteBits t, SymRotate t) =>
Int -> Term t -> Term t -> Term t
RotateRightTerm Int
i Term t
arg Term t
n
go (UToSignedTerm Term u
arg) = Int -> Term u -> Term t
forall a s.
(SupportedPrim a, SupportedPrim s, SignConversion a s) =>
Int -> Term a -> Term s
ToSignedTerm Int
i Term u
arg
go (UToUnsignedTerm Term s
arg) = Int -> Term s -> Term t
forall u a.
(SupportedPrim u, SupportedPrim a, SignConversion u a) =>
Int -> Term a -> Term u
ToUnsignedTerm Int
i Term s
arg
go (UBVConcatTerm Term (bv a)
arg1 Term (bv b)
arg2) = Int -> Term (bv a) -> Term (bv b) -> Term (bv (a + b))
forall (a :: Nat -> *) (l :: Nat) (r :: Nat).
(forall (n :: Nat). (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) = Int -> TypeRep ix -> TypeRep w -> Term (bv n) -> Term (bv w)
forall (a :: Nat -> *) (l :: Nat) (r :: Nat) (w :: Nat).
(forall (n :: Nat). (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) = Int -> Bool -> TypeRep r -> Term (bv l) -> Term (bv r)
forall (a :: Nat -> *) (l :: Nat) (r :: Nat).
(forall (n :: Nat). (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) = Int -> Term (a =-> t) -> Term a -> Term t
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) = Int -> Term (a --> t) -> Term a -> Term t
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) = Int -> Term t -> Term t -> Term t
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) = Int -> Term t -> Term t -> Term t
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) = Int -> Term t -> Term t -> Term t
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) = Int -> Term t -> Term t -> Term t
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) = Int -> Term t -> Term t -> Term t
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) = Int -> Term t -> Term t -> Term t
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) = Int -> Term t -> Term t -> Term t
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) = Int -> Term t -> Term t -> Term t
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 = Cache (Term t)
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 Maybe t -> Maybe t -> Bool
forall a. Eq a => a -> a -> Bool
== t -> Maybe t
forall a. a -> Maybe a
Just t
r
DSymTerm TypedSymbol t
ls == DSymTerm TypedSymbol t
rs = TypedSymbol t
ls TypedSymbol t -> TypedSymbol t -> Bool
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 = (TypeRep tag, tag) -> (TypeRep tag, tag) -> Bool
forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep tag, tag)
tagl (TypeRep tag, tag)
tagr Bool -> Bool -> Bool
&& (TypeRep arg, Int) -> (TypeRep arg, Int) -> 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 =
(TypeRep tag, tag) -> (TypeRep tag, tag) -> Bool
forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep tag, tag)
tagl (TypeRep tag, tag)
tagr Bool -> Bool -> Bool
&& (TypeRep arg1, Int) -> (TypeRep arg1, Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg1, Int)
li1 (TypeRep arg1, Int)
ri1 Bool -> Bool -> Bool
&& (TypeRep arg2, Int) -> (TypeRep arg2, Int) -> 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 =
(TypeRep tag, tag) -> (TypeRep tag, tag) -> Bool
forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep tag, tag)
tagl (TypeRep tag, tag)
tagr Bool -> Bool -> Bool
&& (TypeRep arg1, Int) -> (TypeRep arg1, Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg1, Int)
li1 (TypeRep arg1, Int)
ri1 Bool -> Bool -> Bool
&& (TypeRep arg2, Int) -> (TypeRep arg2, Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg2, Int)
li2 (TypeRep arg2, Int)
ri2 Bool -> Bool -> Bool
&& (TypeRep arg3, Int) -> (TypeRep arg3, Int) -> 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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri
DOrTerm Int
li1 Int
li2 == DOrTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
DAndTerm Int
li1 Int
li2 == DAndTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
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 = TypeRep args -> TypeRep args -> Bool
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep args
lrep TypeRep args
rrep Bool -> Bool -> Bool
&& Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
rc Bool -> Bool -> Bool
&& Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
DAddNumTerm Int
li1 Int
li2 == DAddNumTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
DUMinusNumTerm Int
li == DUMinusNumTerm Int
ri = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri
DTimesNumTerm Int
li1 Int
li2 == DTimesNumTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
DAbsNumTerm Int
li == DAbsNumTerm Int
ri = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri
DSignumNumTerm Int
li == DSignumNumTerm Int
ri = Int
li Int -> Int -> Bool
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 = TypeRep args -> TypeRep args -> Bool
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep args
lrep TypeRep args
rrep Bool -> Bool -> Bool
&& Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
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 = TypeRep args -> TypeRep args -> Bool
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep args
lrep TypeRep args
rrep Bool -> Bool -> Bool
&& Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
DAndBitsTerm Int
li1 Int
li2 == DAndBitsTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
DOrBitsTerm Int
li1 Int
li2 == DOrBitsTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
DXorBitsTerm Int
li1 Int
li2 == DXorBitsTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
DComplementBitsTerm Int
li == DComplementBitsTerm Int
ri = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri
DShiftLeftTerm Int
li Int
ln == DShiftLeftTerm Int
ri Int
rn = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri Bool -> Bool -> Bool
&& Int
ln Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
rn
DShiftRightTerm Int
li Int
ln == DShiftRightTerm Int
ri Int
rn = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri Bool -> Bool -> Bool
&& Int
ln Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
rn
DRotateLeftTerm Int
li Int
ln == DRotateLeftTerm Int
ri Int
rn = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri Bool -> Bool -> Bool
&& Int
ln Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
rn
DRotateRightTerm Int
li Int
ln == DRotateRightTerm Int
ri Int
rn = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri Bool -> Bool -> Bool
&& Int
ln Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
rn
DToSignedTerm (TypeRep u, Int)
li == DToSignedTerm (TypeRep u, Int)
ri = (TypeRep u, Int) -> (TypeRep u, Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep u, Int)
li (TypeRep u, Int)
ri
DToUnsignedTerm (TypeRep s, Int)
li == DToUnsignedTerm (TypeRep s, Int)
ri = (TypeRep s, Int) -> (TypeRep s, Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep s, Int)
li (TypeRep s, Int)
ri
DBVConcatTerm TypeRep bv1
lrep1 TypeRep bv2
lrep2 Int
li1 Int
li2 == DBVConcatTerm TypeRep bv1
rrep1 TypeRep bv2
rrep2 Int
ri1 Int
ri2 =
TypeRep bv1 -> TypeRep bv1 -> Bool
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep bv1
lrep1 TypeRep bv1
rrep1 Bool -> Bool -> Bool
&& TypeRep bv2 -> TypeRep bv2 -> 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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
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 =
TypeRep ix -> TypeRep ix -> Bool
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep ix
lix TypeRep ix
rix Bool -> Bool -> Bool
&& (TypeRep (bv n), Int) -> (TypeRep (bv n), Int) -> 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 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
rIsSigned
Bool -> Bool -> Bool
&& TypeRep r -> TypeRep r -> Bool
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep r
ln TypeRep r
rn
Bool -> Bool -> Bool
&& (TypeRep (bv l), Int) -> (TypeRep (bv l), Int) -> 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 = (TypeRep (a =-> t), Int) -> (TypeRep (a =-> t), Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (a =-> t), Int)
lf (TypeRep (a =-> t), Int)
rf Bool -> Bool -> Bool
&& (TypeRep a, Int) -> (TypeRep a, Int) -> 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 = (TypeRep (a --> t), Int) -> (TypeRep (a --> t), Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (a --> t), Int)
lf (TypeRep (a --> t), Int)
rf Bool -> Bool -> Bool
&& (TypeRep a, Int) -> (TypeRep a, Int) -> 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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
DModIntegralTerm Int
li1 Int
li2 == DModIntegralTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
DQuotIntegralTerm Int
li1 Int
li2 == DQuotIntegralTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
DRemIntegralTerm Int
li1 Int
li2 == DRemIntegralTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
DDivBoundedIntegralTerm Int
li1 Int
li2 == DDivBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
DModBoundedIntegralTerm Int
li1 Int
li2 == DModBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
DQuotBoundedIntegralTerm Int
li1 Int
li2 == DQuotBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
DRemBoundedIntegralTerm Int
li1 Int
li2 == DRemBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
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 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int) Int -> t -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` t
c
hashWithSalt Int
s (DSymTerm TypedSymbol t
name) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1 :: Int) Int -> TypedSymbol t -> 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 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
2 :: Int) Int -> (TypeRep tag, tag) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag Int -> (TypeRep arg, Int) -> Int
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 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
3 :: Int) Int -> (TypeRep tag, tag) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag Int -> (TypeRep arg1, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg1, Int)
id1 Int -> (TypeRep arg2, Int) -> Int
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 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
4 :: Int) Int -> (TypeRep tag, tag) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag Int -> (TypeRep arg1, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg1, Int)
id1 Int -> (TypeRep arg2, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg2, Int)
id2 Int -> (TypeRep arg3, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg3, Int)
id3
hashWithSalt Int
s (DNotTerm Int
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
5 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
hashWithSalt Int
s (DOrTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
6 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DAndTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
7 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DEqvTerm TypeRep args
rep Int
id1 Int
id2) =
Int
s
Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
8 :: Int)
Int -> TypeRep args -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep
Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DITETerm Int
idc Int
id1 Int
id2) =
Int
s
Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
9 :: Int)
Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
idc
Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DAddNumTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
10 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DUMinusNumTerm Int
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
11 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
hashWithSalt Int
s (DTimesNumTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
12 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DAbsNumTerm Int
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
13 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
hashWithSalt Int
s (DSignumNumTerm Int
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
14 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
hashWithSalt Int
s (DLTNumTerm TypeRep args
rep Int
id1 Int
id2) =
Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
15 :: Int) Int -> TypeRep args -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DLENumTerm TypeRep args
rep Int
id1 Int
id2) =
Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
16 :: Int) Int -> TypeRep args -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DAndBitsTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
17 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DOrBitsTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
18 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DXorBitsTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
19 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DComplementBitsTerm Int
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
20 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
hashWithSalt Int
s (DShiftLeftTerm Int
id1 Int
idn) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
38 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
idn
hashWithSalt Int
s (DShiftRightTerm Int
id1 Int
idn) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
39 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
idn
hashWithSalt Int
s (DRotateLeftTerm Int
id1 Int
idn) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
40 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
idn
hashWithSalt Int
s (DRotateRightTerm Int
id1 Int
idn) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
41 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
idn
hashWithSalt Int
s (DToSignedTerm (TypeRep u, Int)
id) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
23 :: Int) Int -> (TypeRep u, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep u, Int)
id
hashWithSalt Int
s (DToUnsignedTerm (TypeRep s, Int)
id) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
24 :: Int) Int -> (TypeRep s, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep s, Int)
id
hashWithSalt Int
s (DBVConcatTerm TypeRep bv1
rep1 TypeRep bv2
rep2 Int
id1 Int
id2) =
Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
25 :: Int) Int -> TypeRep bv1 -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep bv1
rep1 Int -> TypeRep bv2 -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep bv2
rep2 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DBVSelectTerm TypeRep ix
ix (TypeRep (bv n), Int)
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
26 :: Int) Int -> TypeRep ix -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep ix
ix Int -> (TypeRep (bv n), Int) -> Int
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
Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
27 :: Int)
Int -> Bool -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Bool
signed
Int -> TypeRep r -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep r
n
Int -> (TypeRep (bv l), Int) -> Int
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 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
28 :: Int) Int -> (TypeRep (a =-> t), Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (a =-> t), Int)
id1 Int -> (TypeRep a, Int) -> Int
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 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
29 :: Int) Int -> (TypeRep (a --> t), Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (a --> t), Int)
id1 Int -> (TypeRep a, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep a, Int)
id2
hashWithSalt Int
s (DDivIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
30 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DModIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
31 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DQuotIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
32 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DRemIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
33 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DDivBoundedIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
34 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DModBoundedIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
35 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DQuotBoundedIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
36 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DRemBoundedIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
37 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
defaultValueForBool :: Bool
defaultValueForBool :: Bool
defaultValueForBool = Bool
False
defaultValueForBoolDyn :: ModelValue
defaultValueForBoolDyn :: ModelValue
defaultValueForBoolDyn = Bool -> ModelValue
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 = Integer -> ModelValue
forall a. (Show a, Eq a, Hashable a, Typeable a) => a -> ModelValue
toModelValue Integer
defaultValueForInteger
instance SupportedPrim Integer where
pformatCon :: Integer -> String
pformatCon = Integer -> String
forall a. Show a => a -> String
show
defaultValue :: Integer
defaultValue = Integer
defaultValueForInteger
defaultValueDynamic :: forall (proxy :: * -> *). proxy Integer -> ModelValue
defaultValueDynamic proxy Integer
_ = ModelValue
defaultValueForIntegerDyn
instance (KnownNat w, 1 <= w) => SupportedPrim (IntN w) where
type PrimConstraint (IntN w) = (KnownNat w, 1 <= w)
pformatCon :: IntN w -> String
pformatCon = IntN w -> String
forall a. Show a => a -> String
show
defaultValue :: IntN w
defaultValue = IntN w
0
instance (KnownNat w, 1 <= w) => SupportedPrim (WordN w) where
type PrimConstraint (WordN w) = (KnownNat w, 1 <= w)
pformatCon :: WordN w -> String
pformatCon = WordN w -> String
forall a. Show a => a -> String
show
defaultValue :: WordN w
defaultValue = WordN w
0
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 = Term b -> Ret (a --> b)
forall con sym. LinkedRep con sym => Term con -> sym
wrapTerm (Term b -> Ret (a --> b)) -> Term b -> Ret (a --> b)
forall a b. (a -> b) -> a -> b
$ TypedSymbol a -> Term a -> Term b -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
s (sa -> Term a
forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm sa
Arg (a --> b)
x) Term b
t
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 = TypedSymbol a -> Term b -> a --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol a
newarg (TypedSymbol a -> Term a -> Term b -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
arg (TypedSymbol a -> Term a
forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm TypedSymbol a
newarg) Term b
v)
where
newarg :: TypedSymbol a
newarg = TypedSymbol a -> ARG -> TypedSymbol a
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
(ARG -> ARG -> Bool) -> (ARG -> ARG -> Bool) -> Eq ARG
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ARG -> ARG -> Bool
== :: ARG -> ARG -> Bool
$c/= :: ARG -> ARG -> Bool
/= :: ARG -> ARG -> Bool
Eq, Eq ARG
Eq ARG =>
(ARG -> ARG -> Ordering)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> ARG)
-> (ARG -> ARG -> ARG)
-> Ord 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
$ccompare :: ARG -> ARG -> Ordering
compare :: ARG -> ARG -> Ordering
$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
>= :: ARG -> ARG -> Bool
$cmax :: ARG -> ARG -> ARG
max :: ARG -> ARG -> ARG
$cmin :: ARG -> ARG -> ARG
min :: ARG -> ARG -> ARG
Ord, (forall (m :: * -> *). Quote m => ARG -> m Exp)
-> (forall (m :: * -> *). Quote m => ARG -> Code m ARG) -> Lift ARG
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
$clift :: forall (m :: * -> *). Quote m => ARG -> m Exp
lift :: forall (m :: * -> *). Quote m => ARG -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
liftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
Lift, Int -> ARG -> ShowS
[ARG] -> ShowS
ARG -> String
(Int -> ARG -> ShowS)
-> (ARG -> String) -> ([ARG] -> ShowS) -> Show ARG
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ARG -> ShowS
showsPrec :: Int -> ARG -> ShowS
$cshow :: ARG -> String
show :: ARG -> String
$cshowList :: [ARG] -> ShowS
showList :: [ARG] -> ShowS
Show, (forall x. ARG -> Rep ARG x)
-> (forall x. Rep ARG x -> ARG) -> Generic ARG
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
$cfrom :: forall x. ARG -> Rep ARG x
from :: forall x. ARG -> Rep ARG x
$cto :: forall x. Rep ARG x -> ARG
to :: forall x. Rep ARG x -> ARG
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 Int -> Int -> Int
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 TypedSymbol a -> TypedSymbol a -> Bool
forall a. Eq a => a -> a -> Bool
== TypedSymbol a
sym2 Bool -> Bool -> Bool
&& Term b
tm1 Term b -> Term b -> Bool
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
"\\(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypedSymbol a -> String
forall a. Show a => a -> String
show TypedSymbol a
sym String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term b -> String
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) = [||TypedSymbol a -> Term b -> a --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol a
sym Term b
tm||]
instance Hashable (a --> b) where
Int
s hashWithSalt :: Int -> (a --> b) -> Int
`hashWithSalt` (GeneralFun TypedSymbol a
sym Term b
tm) = Int
s Int -> TypedSymbol a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol a
sym Int -> Term b -> Int
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) = TypedSymbol a -> ()
forall a. NFData a => a -> ()
rnf TypedSymbol a
sym () -> () -> ()
forall a b. a -> b -> b
`seq` Term b -> ()
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 = TypedSymbol a -> Term b -> a --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun (Text -> TypedSymbol a
forall t. SupportedPrim t => Text -> TypedSymbol t
SimpleSymbol Text
"a") (b -> Term b
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm b
forall t. SupportedPrim t => t
defaultValue)
instance
(SupportedPrim a, SupportedPrim b) =>
SupportedPrim (a =-> b)
where
type PrimConstraint (a =-> b) = (SupportedPrim a, SupportedPrim b)
defaultValue :: a =-> b
defaultValue = [(a, b)] -> b -> a =-> b
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] (forall t. SupportedPrim t => t
defaultValue @b)