{-# 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)
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 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
( BVSignConversion,
SizedBV,
)
import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#)))
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches
( typeMemoizedCache,
)
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
( absNumTerm,
addNumTerm,
andBitsTerm,
andTerm,
bvToSignedTerm,
bvToUnsignedTerm,
bvconcatTerm,
bvextendTerm,
bvselectTerm,
complementBitsTerm,
conTerm,
constructBinary,
constructTernary,
constructUnary,
divBoundedIntegralTerm,
divIntegralTerm,
eqvTerm,
generalFunApplyTerm,
iteTerm,
leNumTerm,
ltNumTerm,
modBoundedIntegralTerm,
modIntegralTerm,
notTerm,
orBitsTerm,
orTerm,
quotBoundedIntegralTerm,
quotIntegralTerm,
remBoundedIntegralTerm,
remIntegralTerm,
rotateBitsTerm,
shiftBitsTerm,
signumNumTerm,
symTerm,
tabularFunApplyTerm,
timesNumTerm,
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 = PrimConstraint t => a
i
termCache :: Cache (Term t)
termCache = forall a. (Interned a, Typeable a) => Cache a
typeMemoizedCache
pformatCon :: t -> String
default pformatCon :: (Show t) => t -> String
pformatCon = forall a. Show a => a -> String
show
pformatSym :: TypedSymbol t -> String
pformatSym = forall t. TypedSymbol t -> String
showUntyped
defaultValue :: t
defaultValueDynamic :: proxy t -> ModelValue
defaultValueDynamic proxy t
_ = forall a. (Show a, Eq a, Hashable a, Typeable a) => a -> ModelValue
toModelValue (forall t. SupportedPrim t => t
defaultValue @t)
class 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) => String -> TypedSymbol t
IndexedSymbol :: (SupportedPrim t) => String -> Int -> TypedSymbol t
WithInfo ::
forall t a.
( SupportedPrim t,
Typeable a,
Ord a,
Lift a,
NFData a,
Show a,
Hashable a
) =>
TypedSymbol t ->
a ->
TypedSymbol t
instance Eq (TypedSymbol t) where
SimpleSymbol String
x == :: TypedSymbol t -> TypedSymbol t -> Bool
== SimpleSymbol String
y = String
x forall a. Eq a => a -> a -> Bool
== String
y
IndexedSymbol String
x Int
i == IndexedSymbol String
y Int
j = Int
i forall a. Eq a => a -> a -> Bool
== Int
j Bool -> Bool -> Bool
&& String
x forall a. Eq a => a -> a -> Bool
== String
y
WithInfo TypedSymbol t
s1 (a
i1 :: a) == WithInfo TypedSymbol t
s2 (a
i2 :: b) = case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b) of
Just a :~~: a
HRefl -> a
i1 forall a. Eq a => a -> a -> Bool
== a
i2 Bool -> Bool -> Bool
&& TypedSymbol t
s1 forall a. Eq a => a -> a -> Bool
== TypedSymbol t
s2
Maybe (a :~~: a)
_ -> Bool
False
TypedSymbol t
_ == TypedSymbol t
_ = Bool
False
instance Ord (TypedSymbol t) where
SimpleSymbol String
x <= :: TypedSymbol t -> TypedSymbol t -> Bool
<= SimpleSymbol String
y = String
x forall a. Ord a => a -> a -> Bool
<= String
y
IndexedSymbol String
x Int
i <= IndexedSymbol String
y Int
j = Int
i forall a. Ord a => a -> a -> Bool
< Int
j Bool -> Bool -> Bool
|| (Int
i forall a. Eq a => a -> a -> Bool
== Int
j Bool -> Bool -> Bool
&& String
x forall a. Ord a => a -> a -> Bool
<= String
y)
WithInfo TypedSymbol t
s1 (a
i1 :: a) <= WithInfo TypedSymbol t
s2 (a
i2 :: b) = case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b) of
Just a :~~: a
HRefl -> TypedSymbol t
s1 forall a. Ord a => a -> a -> Bool
< TypedSymbol t
s2 Bool -> Bool -> Bool
|| (TypedSymbol t
s1 forall a. Eq a => a -> a -> Bool
== TypedSymbol t
s2 Bool -> Bool -> Bool
&& a
i1 forall a. Ord a => a -> a -> Bool
<= a
i2)
Maybe (a :~~: a)
_ -> Bool
False
TypedSymbol t
_ <= TypedSymbol t
_ = Bool
False
instance Lift (TypedSymbol t) where
liftTyped :: forall (m :: * -> *).
Quote m =>
TypedSymbol t -> Code m (TypedSymbol t)
liftTyped (SimpleSymbol String
x) = [||SimpleSymbol x||]
liftTyped (IndexedSymbol String
x Int
i) = [||IndexedSymbol x i||]
liftTyped (WithInfo TypedSymbol t
s1 a
i1) = [||WithInfo s1 i1||]
instance Show (TypedSymbol t) where
show :: TypedSymbol t -> String
show (SimpleSymbol String
str) = String
str forall a. [a] -> [a] -> [a]
++ String
" :: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t)
show (IndexedSymbol String
str Int
i) = String
str forall a. [a] -> [a] -> [a]
++ String
"@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" :: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t)
show (WithInfo TypedSymbol t
s a
info) = forall t. TypedSymbol t -> String
showUntyped TypedSymbol t
s forall a. [a] -> [a] -> [a]
++ String
":" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
info forall a. [a] -> [a] -> [a]
++ String
" :: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t)
showUntyped :: TypedSymbol t -> String
showUntyped :: forall t. TypedSymbol t -> String
showUntyped (SimpleSymbol String
str) = String
str
showUntyped (IndexedSymbol String
str Int
i) = String
str forall a. [a] -> [a] -> [a]
++ String
"@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
showUntyped (WithInfo TypedSymbol t
s a
info) = forall t. TypedSymbol t -> String
showUntyped TypedSymbol t
s forall a. [a] -> [a] -> [a]
++ String
":" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
info
instance Hashable (TypedSymbol t) where
Int
s hashWithSalt :: Int -> TypedSymbol t -> Int
`hashWithSalt` SimpleSymbol String
x = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` String
x
Int
s `hashWithSalt` IndexedSymbol String
x Int
i = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` String
x forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
i
Int
s `hashWithSalt` WithInfo TypedSymbol t
sym a
info = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol t
sym forall a. Hashable a => Int -> a -> Int
`hashWithSalt` a
info
instance NFData (TypedSymbol t) where
rnf :: TypedSymbol t -> ()
rnf (SimpleSymbol String
str) = forall a. NFData a => a -> ()
rnf String
str
rnf (IndexedSymbol String
str Int
i) = forall a. NFData a => a -> ()
rnf String
str seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Int
i
rnf (WithInfo TypedSymbol t
s a
info) = forall a. NFData a => a -> ()
rnf TypedSymbol t
s seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf a
info
instance (SupportedPrim t) => IsString (TypedSymbol t) where
fromString :: String -> TypedSymbol t
fromString = forall t. SupportedPrim t => String -> TypedSymbol t
SimpleSymbol
withSymbolSupported :: TypedSymbol t -> ((SupportedPrim t) => a) -> a
withSymbolSupported :: forall t a. TypedSymbol t -> (SupportedPrim t => a) -> a
withSymbolSupported (SimpleSymbol String
_) SupportedPrim t => a
a = SupportedPrim t => a
a
withSymbolSupported (IndexedSymbol String
_ Int
_) SupportedPrim t => a
a = SupportedPrim t => a
a
withSymbolSupported (WithInfo TypedSymbol t
_ a
_) SupportedPrim t => a
a = SupportedPrim t => a
a
data SomeTypedSymbol where
SomeTypedSymbol :: forall t. TypeRep t -> TypedSymbol t -> SomeTypedSymbol
instance NFData SomeTypedSymbol where
rnf :: SomeTypedSymbol -> ()
rnf (SomeTypedSymbol TypeRep t
p TypedSymbol t
s) = forall a. NFData a => a -> ()
rnf (forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep t
p) seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf TypedSymbol t
s
instance Eq SomeTypedSymbol where
(SomeTypedSymbol TypeRep t
t1 TypedSymbol t
s1) == :: SomeTypedSymbol -> SomeTypedSymbol -> Bool
== (SomeTypedSymbol TypeRep t
t2 TypedSymbol t
s2) = case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep t
t1 TypeRep t
t2 of
Just t :~~: t
HRefl -> TypedSymbol t
s1 forall a. Eq a => a -> a -> Bool
== TypedSymbol t
s2
Maybe (t :~~: t)
_ -> Bool
False
instance Ord SomeTypedSymbol where
(SomeTypedSymbol TypeRep t
t1 TypedSymbol t
s1) <= :: SomeTypedSymbol -> SomeTypedSymbol -> Bool
<= (SomeTypedSymbol TypeRep t
t2 TypedSymbol t
s2) =
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep t
t1 forall a. Ord a => a -> a -> Bool
< forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep t
t2
Bool -> Bool -> Bool
|| ( case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep t
t1 TypeRep t
t2 of
Just t :~~: t
HRefl -> TypedSymbol t
s1 forall a. Ord a => a -> a -> Bool
<= TypedSymbol t
s2
Maybe (t :~~: t)
_ -> Bool
False
)
instance Hashable SomeTypedSymbol where
hashWithSalt :: Int -> SomeTypedSymbol -> Int
hashWithSalt Int
s (SomeTypedSymbol TypeRep t
t1 TypedSymbol t
s1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol t
s1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep t
t1
instance Show SomeTypedSymbol where
show :: SomeTypedSymbol -> String
show (SomeTypedSymbol TypeRep t
_ TypedSymbol t
s) = forall a. Show a => a -> String
show TypedSymbol t
s
someTypedSymbol :: forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol :: forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol s :: TypedSymbol t
s@(SimpleSymbol String
_) = forall a. TypeRep a -> TypedSymbol a -> SomeTypedSymbol
SomeTypedSymbol (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t) TypedSymbol t
s
someTypedSymbol s :: TypedSymbol t
s@(IndexedSymbol String
_ Int
_) = forall a. TypeRep a -> TypedSymbol a -> SomeTypedSymbol
SomeTypedSymbol (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t) TypedSymbol t
s
someTypedSymbol s :: TypedSymbol t
s@(WithInfo TypedSymbol t
_ a
_) = forall a. TypeRep a -> TypedSymbol a -> SomeTypedSymbol
SomeTypedSymbol (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t) TypedSymbol t
s
data Term t where
ConTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !t -> Term t
SymTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(TypedSymbol t) -> Term t
UnaryTerm ::
(UnaryOp tag arg t) =>
{-# UNPACK #-} !Id ->
!tag ->
!(Term arg) ->
Term t
BinaryTerm ::
(BinaryOp tag arg1 arg2 t) =>
{-# UNPACK #-} !Id ->
!tag ->
!(Term arg1) ->
!(Term arg2) ->
Term t
TernaryTerm ::
(TernaryOp tag arg1 arg2 arg3 t) =>
{-# UNPACK #-} !Id ->
!tag ->
!(Term arg1) ->
!(Term arg2) ->
!(Term arg3) ->
Term t
NotTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> Term Bool
OrTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
AndTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
EqvTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
ITETerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t
AddNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
UMinusNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
TimesNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
AbsNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
SignumNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
LTNumTerm :: (SupportedPrim t, Num t, Ord t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
LENumTerm :: (SupportedPrim t, Num t, Ord t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
AndBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
OrBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
XorBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
ComplementBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
ShiftBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> {-# UNPACK #-} !Int -> Term t
RotateBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> {-# UNPACK #-} !Int -> Term t
BVToSignedTerm ::
( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
Typeable ubv,
Typeable sbv,
KnownNat n,
1 <= n,
BVSignConversion (ubv n) (sbv n)
) =>
{-# UNPACK #-} !Id ->
!(Term (ubv n)) ->
Term (sbv n)
BVToUnsignedTerm ::
( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
Typeable ubv,
Typeable sbv,
KnownNat n,
1 <= n,
BVSignConversion (ubv n) (sbv n)
) =>
{-# UNPACK #-} !Id ->
!(Term (sbv n)) ->
Term (ubv n)
BVConcatTerm ::
( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
Typeable bv,
KnownNat a,
KnownNat b,
KnownNat (a + b),
1 <= a,
1 <= b,
1 <= a + b,
SizedBV bv
) =>
{-# UNPACK #-} !Id ->
!(Term (bv a)) ->
!(Term (bv b)) ->
Term (bv (a + b))
BVSelectTerm ::
( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
Typeable bv,
KnownNat n,
KnownNat ix,
KnownNat w,
1 <= n,
1 <= w,
ix + w <= n,
SizedBV bv
) =>
{-# UNPACK #-} !Id ->
!(TypeRep ix) ->
!(TypeRep w) ->
!(Term (bv n)) ->
Term (bv w)
BVExtendTerm ::
( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
Typeable bv,
KnownNat l,
KnownNat r,
1 <= l,
1 <= r,
l <= r,
SizedBV bv
) =>
{-# UNPACK #-} !Id ->
!Bool ->
!(TypeRep r) ->
!(Term (bv l)) ->
Term (bv r)
TabularFunApplyTerm ::
( SupportedPrim a,
SupportedPrim b
) =>
{-# UNPACK #-} !Id ->
Term (a =-> b) ->
Term a ->
Term b
GeneralFunApplyTerm ::
( SupportedPrim a,
SupportedPrim b
) =>
{-# UNPACK #-} !Id ->
Term (a --> b) ->
Term a ->
Term b
DivIntegralTerm :: (SupportedPrim t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
ModIntegralTerm :: (SupportedPrim t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
QuotIntegralTerm :: (SupportedPrim t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
RemIntegralTerm :: (SupportedPrim t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
DivBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
ModBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
QuotBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
RemBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
instance NFData (Term a) where
rnf :: Term a -> ()
rnf Term a
i = forall t. Term t -> Int
identity Term a
i seq :: forall a b. a -> b -> b
`seq` ()
instance Lift (Term t) where
lift :: forall (m :: * -> *). Quote m => Term t -> m Exp
lift = forall a (m :: * -> *). Quote m => Splice m a -> m Exp
unTypeSplice forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (m :: * -> *). (Lift t, Quote m) => t -> Code m t
liftTyped
liftTyped :: forall (m :: * -> *). Quote m => Term t -> Code m (Term t)
liftTyped (ConTerm Int
_ t
i) = [||conTerm i||]
liftTyped (SymTerm Int
_ TypedSymbol t
sym) = [||symTerm sym||]
liftTyped (UnaryTerm Int
_ tag
tag Term arg
arg) = [||constructUnary tag arg||]
liftTyped (BinaryTerm Int
_ tag
tag Term arg1
arg1 Term arg2
arg2) = [||constructBinary tag arg1 arg2||]
liftTyped (TernaryTerm Int
_ tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) = [||constructTernary tag arg1 arg2 arg3||]
liftTyped (NotTerm Int
_ Term Bool
arg) = [||notTerm arg||]
liftTyped (OrTerm Int
_ Term Bool
arg1 Term Bool
arg2) = [||orTerm arg1 arg2||]
liftTyped (AndTerm Int
_ Term Bool
arg1 Term Bool
arg2) = [||andTerm arg1 arg2||]
liftTyped (EqvTerm Int
_ Term t
arg1 Term t
arg2) = [||eqvTerm arg1 arg2||]
liftTyped (ITETerm Int
_ Term Bool
cond Term t
arg1 Term t
arg2) = [||iteTerm cond arg1 arg2||]
liftTyped (AddNumTerm Int
_ Term t
arg1 Term t
arg2) = [||addNumTerm arg1 arg2||]
liftTyped (UMinusNumTerm Int
_ Term t
arg) = [||uminusNumTerm arg||]
liftTyped (TimesNumTerm Int
_ Term t
arg1 Term t
arg2) = [||timesNumTerm arg1 arg2||]
liftTyped (AbsNumTerm Int
_ Term t
arg) = [||absNumTerm arg||]
liftTyped (SignumNumTerm Int
_ Term t
arg) = [||signumNumTerm arg||]
liftTyped (LTNumTerm Int
_ Term t
arg1 Term t
arg2) = [||ltNumTerm arg1 arg2||]
liftTyped (LENumTerm Int
_ Term t
arg1 Term t
arg2) = [||leNumTerm arg1 arg2||]
liftTyped (AndBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||andBitsTerm arg1 arg2||]
liftTyped (OrBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||orBitsTerm arg1 arg2||]
liftTyped (XorBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||xorBitsTerm arg1 arg2||]
liftTyped (ComplementBitsTerm Int
_ Term t
arg) = [||complementBitsTerm arg||]
liftTyped (ShiftBitsTerm Int
_ Term t
arg Int
n) = [||shiftBitsTerm arg n||]
liftTyped (RotateBitsTerm Int
_ Term t
arg Int
n) = [||rotateBitsTerm arg n||]
liftTyped (BVToSignedTerm Int
_ Term (ubv n)
v) = [||bvToSignedTerm v||]
liftTyped (BVToUnsignedTerm Int
_ Term (sbv n)
v) = [||bvToUnsignedTerm v||]
liftTyped (BVConcatTerm Int
_ Term (bv a)
arg1 Term (bv b)
arg2) = [||bvconcatTerm arg1 arg2||]
liftTyped (BVSelectTerm Int
_ (TypeRep ix
_ :: TypeRep ix) (TypeRep w
_ :: TypeRep w) Term (bv n)
arg) = [||bvselectTerm (Proxy @ix) (Proxy @w) arg||]
liftTyped (BVExtendTerm Int
_ Bool
signed (TypeRep r
_ :: TypeRep n) Term (bv l)
arg) = [||bvextendTerm signed (Proxy @n) arg||]
liftTyped (TabularFunApplyTerm Int
_ Term (a =-> t)
func Term a
arg) = [||tabularFunApplyTerm func arg||]
liftTyped (GeneralFunApplyTerm Int
_ Term (a --> t)
func Term a
arg) = [||generalFunApplyTerm func arg||]
liftTyped (DivIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||divIntegralTerm arg1 arg2||]
liftTyped (ModIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||modIntegralTerm arg1 arg2||]
liftTyped (QuotIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||quotIntegralTerm arg1 arg2||]
liftTyped (RemIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||remIntegralTerm arg1 arg2||]
liftTyped (DivBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||divBoundedIntegralTerm arg1 arg2||]
liftTyped (ModBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||modBoundedIntegralTerm arg1 arg2||]
liftTyped (QuotBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||quotBoundedIntegralTerm arg1 arg2||]
liftTyped (RemBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||remBoundedIntegralTerm arg1 arg2||]
instance Show (Term ty) where
show :: Term ty -> String
show (ConTerm Int
i ty
v) = String
"ConTerm{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", v=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ty
v forall a. [a] -> [a] -> [a]
++ String
"}"
show (SymTerm Int
i TypedSymbol ty
name) =
String
"SymTerm{id="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
forall a. [a] -> [a] -> [a]
++ String
", name="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypedSymbol ty
name
forall a. [a] -> [a] -> [a]
++ String
", type="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @ty)
forall a. [a] -> [a] -> [a]
++ String
"}"
show (UnaryTerm Int
i tag
tag Term arg
arg) = String
"Unary{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", tag=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show tag
tag forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (BinaryTerm Int
i tag
tag Term arg1
arg1 Term arg2
arg2) =
String
"Binary{id="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
forall a. [a] -> [a] -> [a]
++ String
", tag="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show tag
tag
forall a. [a] -> [a] -> [a]
++ String
", arg1="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg1
arg1
forall a. [a] -> [a] -> [a]
++ String
", arg2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg2
arg2
forall a. [a] -> [a] -> [a]
++ String
"}"
show (TernaryTerm Int
i tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) =
String
"Ternary{id="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
forall a. [a] -> [a] -> [a]
++ String
", tag="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show tag
tag
forall a. [a] -> [a] -> [a]
++ String
", arg1="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg1
arg1
forall a. [a] -> [a] -> [a]
++ String
", arg2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg2
arg2
forall a. [a] -> [a] -> [a]
++ String
", arg3="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg3
arg3
forall a. [a] -> [a] -> [a]
++ String
"}"
show (NotTerm Int
i Term Bool
arg) = String
"Not{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (OrTerm Int
i Term Bool
arg1 Term Bool
arg2) = String
"Or{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (AndTerm Int
i Term Bool
arg1 Term Bool
arg2) = String
"And{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (EqvTerm Int
i Term t
arg1 Term t
arg2) = String
"Eqv{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (ITETerm Int
i Term Bool
cond Term ty
l Term ty
r) =
String
"ITE{id="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
forall a. [a] -> [a] -> [a]
++ String
", cond="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
cond
forall a. [a] -> [a] -> [a]
++ String
", then="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
l
forall a. [a] -> [a] -> [a]
++ String
", else="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
r
forall a. [a] -> [a] -> [a]
++ String
"}"
show (AddNumTerm Int
i Term ty
arg1 Term ty
arg2) = String
"AddNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (UMinusNumTerm Int
i Term ty
arg) = String
"UMinusNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (TimesNumTerm Int
i Term ty
arg1 Term ty
arg2) = String
"TimesNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (AbsNumTerm Int
i Term ty
arg) = String
"AbsNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (SignumNumTerm Int
i Term ty
arg) = String
"SignumNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (LTNumTerm Int
i Term t
arg1 Term t
arg2) = String
"LTNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (LENumTerm Int
i Term t
arg1 Term t
arg2) = String
"LENum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (AndBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"AndBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (OrBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"OrBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (XorBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"XorBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (ComplementBitsTerm Int
i Term ty
arg) = String
"ComplementBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (ShiftBitsTerm Int
i Term ty
arg Int
n) = String
"ShiftBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
", n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
"}"
show (RotateBitsTerm Int
i Term ty
arg Int
n) = String
"RotateBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
", n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
"}"
show (BVToSignedTerm Int
i Term (ubv n)
arg) = String
"BVToSigned{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (ubv n)
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (BVToUnsignedTerm Int
i Term (sbv n)
arg) = String
"BVToUnsigned{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (sbv n)
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (BVConcatTerm Int
i Term (bv a)
arg1 Term (bv b)
arg2) = String
"BVConcat{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (bv a)
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (bv b)
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (BVSelectTerm Int
i TypeRep ix
ix TypeRep w
w Term (bv n)
arg) =
String
"BVSelect{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", ix=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep ix
ix forall a. [a] -> [a] -> [a]
++ String
", w=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep w
w forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (bv n)
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (BVExtendTerm Int
i Bool
signed TypeRep r
n Term (bv l)
arg) =
String
"BVExtend{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", signed=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Bool
signed forall a. [a] -> [a] -> [a]
++ String
", n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep r
n forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (bv l)
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (TabularFunApplyTerm Int
i Term (a =-> ty)
func Term a
arg) =
String
"TabularFunApply{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", func=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (a =-> ty)
func forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term a
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (GeneralFunApplyTerm Int
i Term (a --> ty)
func Term a
arg) =
String
"GeneralFunApply{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", func=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (a --> ty)
func forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term a
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (DivIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"DivIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (ModIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"ModIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (QuotIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"QuotIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (RemIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"RemIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (DivBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"DivBoundedIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (ModBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"ModBoundedIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (QuotBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"QuotBoundedIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (RemBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
String
"RemBoundedIntegral{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
prettyPrintTerm :: Term t -> Doc ann
prettyPrintTerm :: forall t ann. Term t -> Doc ann
prettyPrintTerm Term t
v =
forall ann. (Int -> Doc ann) -> Doc ann
column
( \Int
c ->
forall ann. (PageWidth -> Doc ann) -> Doc ann
pageWidth forall a b. (a -> b) -> a -> b
$ \case
AvailablePerLine Int
i Double
r ->
if forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
c forall a. Num a => a -> a -> a
+ Int
len) forall a. Ord a => a -> a -> Bool
> forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i forall a. Num a => a -> a -> a
* Double
r
then Doc ann
"..."
else forall a ann. Pretty a => a -> Doc ann
pretty String
formatted
PageWidth
Unbounded -> forall a ann. Pretty a => a -> Doc ann
pretty String
formatted
)
where
formatted :: String
formatted = forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term t
v forall a b. (a -> b) -> a -> b
$ forall t. SupportedPrim t => Term t -> String
pformat Term t
v
len :: Int
len = forall (t :: * -> *) a. Foldable t => t a -> Int
length String
formatted
instance (SupportedPrim t) => Eq (Term t) where
== :: Term t -> Term t -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall t. Term t -> Int
identity
instance (SupportedPrim t) => Hashable (Term t) where
hashWithSalt :: Int -> Term t -> Int
hashWithSalt Int
s Term t
t = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s forall a b. (a -> b) -> a -> b
$ forall t. Term t -> Int
identity Term t
t
data UTerm t where
UConTerm :: (SupportedPrim t) => !t -> UTerm t
USymTerm :: (SupportedPrim t) => !(TypedSymbol t) -> UTerm t
UUnaryTerm :: (UnaryOp tag arg t) => !tag -> !(Term arg) -> UTerm t
UBinaryTerm ::
(BinaryOp tag arg1 arg2 t) =>
!tag ->
!(Term arg1) ->
!(Term arg2) ->
UTerm t
UTernaryTerm ::
(TernaryOp tag arg1 arg2 arg3 t) =>
!tag ->
!(Term arg1) ->
!(Term arg2) ->
!(Term arg3) ->
UTerm t
UNotTerm :: !(Term Bool) -> UTerm Bool
UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
UEqvTerm :: (SupportedPrim t) => !(Term t) -> !(Term t) -> UTerm Bool
UITETerm :: (SupportedPrim t) => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t
UAddNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
UUMinusNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
UTimesNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
UAbsNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
USignumNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
ULTNumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool
ULENumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool
UAndBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
UOrBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
UXorBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
UComplementBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> UTerm t
UShiftBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t
URotateBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t
UBVToSignedTerm ::
( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
Typeable ubv,
Typeable sbv,
KnownNat n,
1 <= n,
BVSignConversion (ubv n) (sbv n)
) =>
!(Term (ubv n)) ->
UTerm (sbv n)
UBVToUnsignedTerm ::
( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
Typeable ubv,
Typeable sbv,
KnownNat n,
1 <= n,
BVSignConversion (ubv n) (sbv n)
) =>
!(Term (sbv n)) ->
UTerm (ubv n)
UBVConcatTerm ::
( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
Typeable bv,
KnownNat a,
KnownNat b,
KnownNat (a + b),
1 <= a,
1 <= b,
1 <= a + b,
SizedBV bv
) =>
!(Term (bv a)) ->
!(Term (bv b)) ->
UTerm (bv (a + b))
UBVSelectTerm ::
( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
Typeable bv,
KnownNat n,
KnownNat ix,
KnownNat w,
1 <= n,
1 <= w,
ix + w <= n,
SizedBV bv
) =>
!(TypeRep ix) ->
!(TypeRep w) ->
!(Term (bv n)) ->
UTerm (bv w)
UBVExtendTerm ::
( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
Typeable bv,
KnownNat l,
KnownNat r,
1 <= l,
1 <= r,
l <= r,
SizedBV bv
) =>
!Bool ->
!(TypeRep r) ->
!(Term (bv l)) ->
UTerm (bv r)
UTabularFunApplyTerm ::
( SupportedPrim a,
SupportedPrim b
) =>
Term (a =-> b) ->
Term a ->
UTerm b
UGeneralFunApplyTerm ::
( SupportedPrim a,
SupportedPrim b
) =>
Term (a --> b) ->
Term a ->
UTerm b
UDivIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
UModIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
UQuotIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
URemIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
UDivBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
UModBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
UQuotBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
URemBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
eqTypedId :: (TypeRep a, Id) -> (TypeRep b, Id) -> Bool
eqTypedId :: forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep a
a, Int
i1) (TypeRep b
b, Int
i2) = Int
i1 forall a. Eq a => a -> a -> Bool
== Int
i2 Bool -> Bool -> Bool
&& forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep a
a TypeRep b
b
{-# INLINE eqTypedId #-}
eqHeteroTag :: (Eq a) => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag :: forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep a
tpa, a
taga) (TypeRep b
tpb, b
tagb) = forall a b. Eq a => TypeRep a -> TypeRep b -> a -> b -> Bool
eqHeteroRep TypeRep a
tpa TypeRep b
tpb a
taga b
tagb
{-# INLINE eqHeteroTag #-}
instance (SupportedPrim t) => Interned (Term t) where
type Uninterned (Term t) = UTerm t
data Description (Term t) where
DConTerm :: t -> Description (Term t)
DSymTerm :: TypedSymbol t -> Description (Term t)
DUnaryTerm ::
(Eq tag, Hashable tag) =>
{-# UNPACK #-} !(TypeRep tag, tag) ->
{-# UNPACK #-} !(TypeRep arg, Id) ->
Description (Term t)
DBinaryTerm ::
(Eq tag, Hashable tag) =>
{-# UNPACK #-} !(TypeRep tag, tag) ->
{-# UNPACK #-} !(TypeRep arg1, Id) ->
{-# UNPACK #-} !(TypeRep arg2, Id) ->
Description (Term t)
DTernaryTerm ::
(Eq tag, Hashable tag) =>
{-# UNPACK #-} !(TypeRep tag, tag) ->
{-# UNPACK #-} !(TypeRep arg1, Id) ->
{-# UNPACK #-} !(TypeRep arg2, Id) ->
{-# UNPACK #-} !(TypeRep arg3, Id) ->
Description (Term t)
DNotTerm :: {-# UNPACK #-} !Id -> Description (Term Bool)
DOrTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
DAndTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
DEqvTerm :: TypeRep args -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
DITETerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DAddNumTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DUMinusNumTerm :: {-# UNPACK #-} !Id -> Description (Term t)
DTimesNumTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DAbsNumTerm :: {-# UNPACK #-} !Id -> Description (Term t)
DSignumNumTerm :: {-# UNPACK #-} !Id -> Description (Term t)
DLTNumTerm :: TypeRep args -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
DLENumTerm :: TypeRep args -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
DAndBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DOrBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DXorBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DComplementBitsTerm :: {-# UNPACK #-} !Id -> Description (Term t)
DShiftBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Int -> Description (Term t)
DRotateBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Int -> Description (Term t)
DBVConcatTerm :: TypeRep bv1 -> TypeRep bv2 -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DBVToSignedTerm ::
forall ubv sbv (n :: Nat).
!(TypeRep (ubv n), Id) ->
Description (Term (sbv n))
DBVToUnsignedTerm ::
forall sbv ubv (n :: Nat).
!(TypeRep (sbv n), Id) ->
Description (Term (ubv n))
DBVSelectTerm ::
forall bv (n :: Nat) (w :: Nat) (ix :: Nat).
!(TypeRep ix) ->
!(TypeRep (bv n), Id) ->
Description (Term (bv w))
DBVExtendTerm ::
forall bv (l :: Nat) (r :: Nat).
!Bool ->
!(TypeRep r) ->
{-# UNPACK #-} !(TypeRep (bv l), Id) ->
Description (Term (bv r))
DTabularFunApplyTerm ::
{-# UNPACK #-} !(TypeRep (a =-> b), Id) ->
{-# UNPACK #-} !(TypeRep a, Id) ->
Description (Term b)
DGeneralFunApplyTerm ::
{-# UNPACK #-} !(TypeRep (a --> b), Id) ->
{-# UNPACK #-} !(TypeRep a, Id) ->
Description (Term b)
DDivIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
DModIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
DQuotIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
DRemIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
DDivBoundedIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
DModBoundedIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
DQuotBoundedIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
DRemBoundedIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
describe :: Uninterned (Term t) -> Description (Term t)
describe (UConTerm t
v) = forall t. t -> Description (Term t)
DConTerm t
v
describe ((USymTerm TypedSymbol t
name) :: UTerm t) = forall t. TypedSymbol t -> Description (Term t)
DSymTerm @t TypedSymbol t
name
describe ((UUnaryTerm (tag
tag :: tagt) (Term arg
tm :: Term arg)) :: UTerm t) =
forall a l t.
(Eq a, Hashable a) =>
(TypeRep a, a) -> (TypeRep l, Int) -> Description (Term t)
DUnaryTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, forall t. Term t -> Int
identity Term arg
tm)
describe ((UBinaryTerm (tag
tag :: tagt) (Term arg1
tm1 :: Term arg1) (Term arg2
tm2 :: Term arg2)) :: UTerm t) =
forall a l r t.
(Eq a, Hashable a) =>
(TypeRep a, a)
-> (TypeRep l, Int) -> (TypeRep r, Int) -> Description (Term t)
DBinaryTerm @tagt @arg1 @arg2 @t (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, forall t. Term t -> Int
identity Term arg1
tm1) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, forall t. Term t -> Int
identity Term arg2
tm2)
describe ((UTernaryTerm (tag
tag :: tagt) (Term arg1
tm1 :: Term arg1) (Term arg2
tm2 :: Term arg2) (Term arg3
tm3 :: Term arg3)) :: UTerm t) =
forall a l r w t.
(Eq a, Hashable a) =>
(TypeRep a, a)
-> (TypeRep l, Int)
-> (TypeRep r, Int)
-> (TypeRep w, Int)
-> Description (Term t)
DTernaryTerm @tagt @arg1 @arg2 @arg3 @t
(forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag)
(forall {k} (a :: k). Typeable a => TypeRep a
typeRep, forall t. Term t -> Int
identity Term arg1
tm1)
(forall {k} (a :: k). Typeable a => TypeRep a
typeRep, forall t. Term t -> Int
identity Term arg2
tm2)
(forall {k} (a :: k). Typeable a => TypeRep a
typeRep, forall t. Term t -> Int
identity Term arg3
tm3)
describe (UNotTerm Term Bool
arg) = Int -> Description (Term Bool)
DNotTerm (forall t. Term t -> Int
identity Term Bool
arg)
describe (UOrTerm Term Bool
arg1 Term Bool
arg2) = Int -> Int -> Description (Term Bool)
DOrTerm (forall t. Term t -> Int
identity Term Bool
arg1) (forall t. Term t -> Int
identity Term Bool
arg2)
describe (UAndTerm Term Bool
arg1 Term Bool
arg2) = Int -> Int -> Description (Term Bool)
DAndTerm (forall t. Term t -> Int
identity Term Bool
arg1) (forall t. Term t -> Int
identity Term Bool
arg2)
describe (UEqvTerm (Term t
arg1 :: Term arg) Term t
arg2) = forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DEqvTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UITETerm Term Bool
cond (Term t
l :: Term arg) Term t
r) = forall t. Int -> Int -> Int -> Description (Term t)
DITETerm (forall t. Term t -> Int
identity Term Bool
cond) (forall t. Term t -> Int
identity Term t
l) (forall t. Term t -> Int
identity Term t
r)
describe (UAddNumTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DAddNumTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UUMinusNumTerm Term t
arg) = forall t. Int -> Description (Term t)
DUMinusNumTerm (forall t. Term t -> Int
identity Term t
arg)
describe (UTimesNumTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DTimesNumTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UAbsNumTerm Term t
arg) = forall t. Int -> Description (Term t)
DAbsNumTerm (forall t. Term t -> Int
identity Term t
arg)
describe (USignumNumTerm Term t
arg) = forall t. Int -> Description (Term t)
DSignumNumTerm (forall t. Term t -> Int
identity Term t
arg)
describe (ULTNumTerm (Term t
arg1 :: arg) Term t
arg2) = forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DLTNumTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (ULENumTerm (Term t
arg1 :: arg) Term t
arg2) = forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DLENumTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UAndBitsTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DAndBitsTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UOrBitsTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DOrBitsTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UXorBitsTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DXorBitsTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UComplementBitsTerm Term t
arg) = forall t. Int -> Description (Term t)
DComplementBitsTerm (forall t. Term t -> Int
identity Term t
arg)
describe (UShiftBitsTerm Term t
arg Int
n) = forall t. Int -> Int -> Description (Term t)
DShiftBitsTerm (forall t. Term t -> Int
identity Term t
arg) Int
n
describe (URotateBitsTerm Term t
arg Int
n) = forall t. Int -> Int -> Description (Term t)
DRotateBitsTerm (forall t. Term t -> Int
identity Term t
arg) Int
n
describe (UBVToSignedTerm (Term (ubv n)
arg :: Term bv)) = forall (a :: Natural -> *) (l :: Natural -> *) (r :: Natural).
(TypeRep (a r), Int) -> Description (Term (l r))
DBVToSignedTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv, forall t. Term t -> Int
identity Term (ubv n)
arg)
describe (UBVToUnsignedTerm (Term (sbv n)
arg :: Term bv)) = forall (a :: Natural -> *) (l :: Natural -> *) (r :: Natural).
(TypeRep (a r), Int) -> Description (Term (l r))
DBVToSignedTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv, forall t. Term t -> Int
identity Term (sbv n)
arg)
describe (UBVConcatTerm (Term (bv a)
arg1 :: bv1) (Term (bv b)
arg2 :: bv2)) =
forall a l t.
TypeRep a -> TypeRep l -> Int -> Int -> Description (Term t)
DBVConcatTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv1) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv2) (forall t. Term t -> Int
identity Term (bv a)
arg1) (forall t. Term t -> Int
identity Term (bv b)
arg2)
describe (UBVSelectTerm (TypeRep ix
ix :: TypeRep ix) TypeRep w
_ (Term (bv n)
arg :: Term arg)) =
forall (a :: Natural -> *) (l :: Natural) (r :: Natural)
(w :: Natural).
TypeRep w -> (TypeRep (a l), Int) -> Description (Term (a r))
DBVSelectTerm TypeRep ix
ix (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, forall t. Term t -> Int
identity Term (bv n)
arg)
describe (UBVExtendTerm Bool
signed (TypeRep r
n :: TypeRep n) (Term (bv l)
arg :: Term arg)) =
forall (a :: Natural -> *) (l :: Natural) (r :: Natural).
Bool
-> TypeRep r -> (TypeRep (a l), Int) -> Description (Term (a r))
DBVExtendTerm Bool
signed TypeRep r
n (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, forall t. Term t -> Int
identity Term (bv l)
arg)
describe (UTabularFunApplyTerm (Term (a =-> t)
func :: Term f) (Term a
arg :: Term a)) =
forall a b.
(TypeRep (a =-> b), Int)
-> (TypeRep a, Int) -> Description (Term b)
DTabularFunApplyTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep f, forall t. Term t -> Int
identity Term (a =-> t)
func) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep a, forall t. Term t -> Int
identity Term a
arg)
describe (UGeneralFunApplyTerm (Term (a --> t)
func :: Term f) (Term a
arg :: Term a)) =
forall a b.
(TypeRep (a --> b), Int)
-> (TypeRep a, Int) -> Description (Term b)
DGeneralFunApplyTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep f, forall t. Term t -> Int
identity Term (a --> t)
func) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep a, forall t. Term t -> Int
identity Term a
arg)
describe (UDivIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DDivIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UModIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DModIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UQuotIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DRemIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (URemIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DQuotIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UDivBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DDivBoundedIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UModBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DModBoundedIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UQuotBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DRemBoundedIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (URemBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DQuotBoundedIntegralTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
identify :: Int -> Uninterned (Term t) -> Term t
identify Int
i = UTerm t -> Term t
go
where
go :: UTerm t -> Term t
go (UConTerm t
v) = forall t. SupportedPrim t => Int -> t -> Term t
ConTerm Int
i t
v
go (USymTerm TypedSymbol t
v) = forall t. SupportedPrim t => Int -> TypedSymbol t -> Term t
SymTerm Int
i TypedSymbol t
v
go (UUnaryTerm tag
tag Term arg
tm) = forall a l t. UnaryOp a l t => Int -> a -> Term l -> Term t
UnaryTerm Int
i tag
tag Term arg
tm
go (UBinaryTerm tag
tag Term arg1
tm1 Term arg2
tm2) = forall a l r t.
BinaryOp a l r t =>
Int -> a -> Term l -> Term r -> Term t
BinaryTerm Int
i tag
tag Term arg1
tm1 Term arg2
tm2
go (UTernaryTerm tag
tag Term arg1
tm1 Term arg2
tm2 Term arg3
tm3) = forall a l r w t.
TernaryOp a l r w t =>
Int -> a -> Term l -> Term r -> Term w -> Term t
TernaryTerm Int
i tag
tag Term arg1
tm1 Term arg2
tm2 Term arg3
tm3
go (UNotTerm Term Bool
arg) = Int -> Term Bool -> Term Bool
NotTerm Int
i Term Bool
arg
go (UOrTerm Term Bool
arg1 Term Bool
arg2) = Int -> Term Bool -> Term Bool -> Term Bool
OrTerm Int
i Term Bool
arg1 Term Bool
arg2
go (UAndTerm Term Bool
arg1 Term Bool
arg2) = Int -> Term Bool -> Term Bool -> Term Bool
AndTerm Int
i Term Bool
arg1 Term Bool
arg2
go (UEqvTerm Term t
arg1 Term t
arg2) = forall a. SupportedPrim a => Int -> Term a -> Term a -> Term Bool
EqvTerm Int
i Term t
arg1 Term t
arg2
go (UITETerm Term Bool
cond Term t
l Term t
r) = forall t.
SupportedPrim t =>
Int -> Term Bool -> Term t -> Term t -> Term t
ITETerm Int
i Term Bool
cond Term t
l Term t
r
go (UAddNumTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Num t) =>
Int -> Term t -> Term t -> Term t
AddNumTerm Int
i Term t
arg1 Term t
arg2
go (UUMinusNumTerm Term t
arg) = forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
UMinusNumTerm Int
i Term t
arg
go (UTimesNumTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Num t) =>
Int -> Term t -> Term t -> Term t
TimesNumTerm Int
i Term t
arg1 Term t
arg2
go (UAbsNumTerm Term t
arg) = forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
AbsNumTerm Int
i Term t
arg
go (USignumNumTerm Term t
arg) = forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
SignumNumTerm Int
i Term t
arg
go (ULTNumTerm Term t
arg1 Term t
arg2) = forall a.
(SupportedPrim a, Num a, Ord a) =>
Int -> Term a -> Term a -> Term Bool
LTNumTerm Int
i Term t
arg1 Term t
arg2
go (ULENumTerm Term t
arg1 Term t
arg2) = forall a.
(SupportedPrim a, Num a, Ord a) =>
Int -> Term a -> Term a -> Term Bool
LENumTerm Int
i Term t
arg1 Term t
arg2
go (UAndBitsTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Term t -> Term t
AndBitsTerm Int
i Term t
arg1 Term t
arg2
go (UOrBitsTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Term t -> Term t
OrBitsTerm Int
i Term t
arg1 Term t
arg2
go (UXorBitsTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Term t -> Term t
XorBitsTerm Int
i Term t
arg1 Term t
arg2
go (UComplementBitsTerm Term t
arg) = forall t. (SupportedPrim t, Bits t) => Int -> Term t -> Term t
ComplementBitsTerm Int
i Term t
arg
go (UShiftBitsTerm Term t
arg Int
n) = forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Int -> Term t
ShiftBitsTerm Int
i Term t
arg Int
n
go (URotateBitsTerm Term t
arg Int
n) = forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Int -> Term t
RotateBitsTerm Int
i Term t
arg Int
n
go (UBVToSignedTerm Term (ubv n)
arg) = forall (a :: Natural -> *) (l :: Natural -> *) (r :: Natural).
(forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SupportedPrim (a n),
forall (n :: Natural). (KnownNat n, 1 <= n) => SupportedPrim (l n),
Typeable a, Typeable l, KnownNat r, 1 <= r,
BVSignConversion (a r) (l r)) =>
Int -> Term (a r) -> Term (l r)
BVToSignedTerm Int
i Term (ubv n)
arg
go (UBVToUnsignedTerm Term (sbv n)
arg) = forall (a :: Natural -> *) (l :: Natural -> *) (r :: Natural).
(forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SupportedPrim (a n),
forall (n :: Natural). (KnownNat n, 1 <= n) => SupportedPrim (l n),
Typeable a, Typeable l, KnownNat r, 1 <= r,
BVSignConversion (a r) (l r)) =>
Int -> Term (l r) -> Term (a r)
BVToUnsignedTerm Int
i Term (sbv n)
arg
go (UBVConcatTerm Term (bv a)
arg1 Term (bv b)
arg2) = forall (a :: Natural -> *) (l :: Natural) (r :: Natural).
(forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SupportedPrim (a n),
Typeable a, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l,
1 <= r, 1 <= (l + r), SizedBV a) =>
Int -> Term (a l) -> Term (a r) -> Term (a (l + r))
BVConcatTerm Int
i Term (bv a)
arg1 Term (bv b)
arg2
go (UBVSelectTerm TypeRep ix
ix TypeRep w
w Term (bv n)
arg) = forall (a :: Natural -> *) (l :: Natural) (r :: Natural)
(w :: Natural).
(forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SupportedPrim (a n),
Typeable a, KnownNat l, KnownNat r, KnownNat w, 1 <= l, 1 <= w,
(r + w) <= l, SizedBV a) =>
Int -> TypeRep r -> TypeRep w -> Term (a l) -> Term (a w)
BVSelectTerm Int
i TypeRep ix
ix TypeRep w
w Term (bv n)
arg
go (UBVExtendTerm Bool
signed TypeRep r
n Term (bv l)
arg) = forall (a :: Natural -> *) (l :: Natural) (r :: Natural).
(forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SupportedPrim (a n),
Typeable a, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
SizedBV a) =>
Int -> Bool -> TypeRep r -> Term (a l) -> Term (a r)
BVExtendTerm Int
i Bool
signed TypeRep r
n Term (bv l)
arg
go (UTabularFunApplyTerm Term (a =-> t)
func Term a
arg) = forall a b.
(SupportedPrim a, SupportedPrim b) =>
Int -> Term (a =-> b) -> Term a -> Term b
TabularFunApplyTerm Int
i Term (a =-> t)
func Term a
arg
go (UGeneralFunApplyTerm Term (a --> t)
func Term a
arg) = forall a b.
(SupportedPrim a, SupportedPrim b) =>
Int -> Term (a --> b) -> Term a -> Term b
GeneralFunApplyTerm Int
i Term (a --> t)
func Term a
arg
go (UDivIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Integral t) =>
Int -> Term t -> Term t -> Term t
DivIntegralTerm Int
i Term t
arg1 Term t
arg2
go (UModIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Integral t) =>
Int -> Term t -> Term t -> Term t
ModIntegralTerm Int
i Term t
arg1 Term t
arg2
go (UQuotIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Integral t) =>
Int -> Term t -> Term t -> Term t
QuotIntegralTerm Int
i Term t
arg1 Term t
arg2
go (URemIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Integral t) =>
Int -> Term t -> Term t -> Term t
RemIntegralTerm Int
i Term t
arg1 Term t
arg2
go (UDivBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Int -> Term t -> Term t -> Term t
DivBoundedIntegralTerm Int
i Term t
arg1 Term t
arg2
go (UModBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Int -> Term t -> Term t -> Term t
ModBoundedIntegralTerm Int
i Term t
arg1 Term t
arg2
go (UQuotBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Int -> Term t -> Term t -> Term t
QuotBoundedIntegralTerm Int
i Term t
arg1 Term t
arg2
go (URemBoundedIntegralTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Int -> Term t -> Term t -> Term t
RemBoundedIntegralTerm Int
i Term t
arg1 Term t
arg2
cache :: Cache (Term t)
cache = forall t. SupportedPrim t => Cache (Term t)
termCache
instance (SupportedPrim t) => Eq (Description (Term t)) where
DConTerm (t
l :: tyl) == :: Description (Term t) -> Description (Term t) -> Bool
== DConTerm (t
r :: tyr) = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast @tyl @tyr t
l forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just t
r
DSymTerm TypedSymbol t
ls == DSymTerm TypedSymbol t
rs = TypedSymbol t
ls forall a. Eq a => a -> a -> Bool
== TypedSymbol t
rs
DUnaryTerm ((TypeRep tag, tag)
tagl :: tagl) (TypeRep arg, Int)
li == DUnaryTerm ((TypeRep tag, tag)
tagr :: tagr) (TypeRep arg, Int)
ri = forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep tag, tag)
tagl (TypeRep tag, tag)
tagr Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg, Int)
li (TypeRep arg, Int)
ri
DBinaryTerm ((TypeRep tag, tag)
tagl :: tagl) (TypeRep arg1, Int)
li1 (TypeRep arg2, Int)
li2 == DBinaryTerm ((TypeRep tag, tag)
tagr :: tagr) (TypeRep arg1, Int)
ri1 (TypeRep arg2, Int)
ri2 =
forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep tag, tag)
tagl (TypeRep tag, tag)
tagr Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg1, Int)
li1 (TypeRep arg1, Int)
ri1 Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg2, Int)
li2 (TypeRep arg2, Int)
ri2
DTernaryTerm ((TypeRep tag, tag)
tagl :: tagl) (TypeRep arg1, Int)
li1 (TypeRep arg2, Int)
li2 (TypeRep arg3, Int)
li3 == DTernaryTerm ((TypeRep tag, tag)
tagr :: tagr) (TypeRep arg1, Int)
ri1 (TypeRep arg2, Int)
ri2 (TypeRep arg3, Int)
ri3 =
forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep tag, tag)
tagl (TypeRep tag, tag)
tagr Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg1, Int)
li1 (TypeRep arg1, Int)
ri1 Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg2, Int)
li2 (TypeRep arg2, Int)
ri2 Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg3, Int)
li3 (TypeRep arg3, Int)
ri3
DNotTerm Int
li == DNotTerm Int
ri = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri
DOrTerm Int
li1 Int
li2 == DOrTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DAndTerm Int
li1 Int
li2 == DAndTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DEqvTerm TypeRep args
lrep Int
li1 Int
li2 == DEqvTerm TypeRep args
rrep Int
ri1 Int
ri2 = forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep args
lrep TypeRep args
rrep Bool -> Bool -> Bool
&& Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DITETerm Int
lc Int
li1 Int
li2 == DITETerm Int
rc Int
ri1 Int
ri2 = Int
lc forall a. Eq a => a -> a -> Bool
== Int
rc Bool -> Bool -> Bool
&& Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DAddNumTerm Int
li1 Int
li2 == DAddNumTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DUMinusNumTerm Int
li == DUMinusNumTerm Int
ri = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri
DTimesNumTerm Int
li1 Int
li2 == DTimesNumTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DAbsNumTerm Int
li == DAbsNumTerm Int
ri = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri
DSignumNumTerm Int
li == DSignumNumTerm Int
ri = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri
DLTNumTerm TypeRep args
lrep Int
li1 Int
li2 == DLTNumTerm TypeRep args
rrep Int
ri1 Int
ri2 = forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep args
lrep TypeRep args
rrep Bool -> Bool -> Bool
&& Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DLENumTerm TypeRep args
lrep Int
li1 Int
li2 == DLENumTerm TypeRep args
rrep Int
ri1 Int
ri2 = forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep args
lrep TypeRep args
rrep Bool -> Bool -> Bool
&& Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DAndBitsTerm Int
li1 Int
li2 == DAndBitsTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DOrBitsTerm Int
li1 Int
li2 == DOrBitsTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DXorBitsTerm Int
li1 Int
li2 == DXorBitsTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DComplementBitsTerm Int
li == DComplementBitsTerm Int
ri = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri
DShiftBitsTerm Int
li Int
ln == DShiftBitsTerm Int
ri Int
rn = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri Bool -> Bool -> Bool
&& Int
ln forall a. Eq a => a -> a -> Bool
== Int
rn
DRotateBitsTerm Int
li Int
ln == DRotateBitsTerm Int
ri Int
rn = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri Bool -> Bool -> Bool
&& Int
ln forall a. Eq a => a -> a -> Bool
== Int
rn
DBVToSignedTerm (TypeRep (ubv n), Int)
li == DBVToSignedTerm (TypeRep (ubv n), Int)
ri = forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (ubv n), Int)
li (TypeRep (ubv n), Int)
ri
DBVToUnsignedTerm (TypeRep (sbv n), Int)
li == DBVToUnsignedTerm (TypeRep (sbv n), Int)
ri = forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (sbv n), Int)
li (TypeRep (sbv n), Int)
ri
DBVConcatTerm TypeRep bv1
lrep1 TypeRep bv2
lrep2 Int
li1 Int
li2 == DBVConcatTerm TypeRep bv1
rrep1 TypeRep bv2
rrep2 Int
ri1 Int
ri2 =
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep bv1
lrep1 TypeRep bv1
rrep1 Bool -> Bool -> Bool
&& forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep bv2
lrep2 TypeRep bv2
rrep2 Bool -> Bool -> Bool
&& Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DBVSelectTerm TypeRep ix
lix (TypeRep (bv n), Int)
li == DBVSelectTerm TypeRep ix
rix (TypeRep (bv n), Int)
ri =
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep ix
lix TypeRep ix
rix Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (bv n), Int)
li (TypeRep (bv n), Int)
ri
DBVExtendTerm Bool
lIsSigned TypeRep r
ln (TypeRep (bv l), Int)
li == DBVExtendTerm Bool
rIsSigned TypeRep r
rn (TypeRep (bv l), Int)
ri =
Bool
lIsSigned forall a. Eq a => a -> a -> Bool
== Bool
rIsSigned
Bool -> Bool -> Bool
&& forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep r
ln TypeRep r
rn
Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (bv l), Int)
li (TypeRep (bv l), Int)
ri
DTabularFunApplyTerm (TypeRep (a =-> t), Int)
lf (TypeRep a, Int)
li == DTabularFunApplyTerm (TypeRep (a =-> t), Int)
rf (TypeRep a, Int)
ri = forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (a =-> t), Int)
lf (TypeRep (a =-> t), Int)
rf Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep a, Int)
li (TypeRep a, Int)
ri
DGeneralFunApplyTerm (TypeRep (a --> t), Int)
lf (TypeRep a, Int)
li == DGeneralFunApplyTerm (TypeRep (a --> t), Int)
rf (TypeRep a, Int)
ri = forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (a --> t), Int)
lf (TypeRep (a --> t), Int)
rf Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep a, Int)
li (TypeRep a, Int)
ri
DDivIntegralTerm Int
li1 Int
li2 == DDivIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DModIntegralTerm Int
li1 Int
li2 == DModIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DQuotIntegralTerm Int
li1 Int
li2 == DQuotIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DRemIntegralTerm Int
li1 Int
li2 == DRemIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DDivBoundedIntegralTerm Int
li1 Int
li2 == DDivBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DModBoundedIntegralTerm Int
li1 Int
li2 == DModBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DQuotBoundedIntegralTerm Int
li1 Int
li2 == DQuotBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DRemBoundedIntegralTerm Int
li1 Int
li2 == DRemBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
Description (Term t)
_ == Description (Term t)
_ = Bool
False
instance (SupportedPrim t) => Hashable (Description (Term t)) where
hashWithSalt :: Int -> Description (Term t) -> Int
hashWithSalt Int
s (DConTerm t
c) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` t
c
hashWithSalt Int
s (DSymTerm TypedSymbol t
name) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol t
name
hashWithSalt Int
s (DUnaryTerm (TypeRep tag, tag)
tag (TypeRep arg, Int)
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
2 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg, Int)
id1
hashWithSalt Int
s (DBinaryTerm (TypeRep tag, tag)
tag (TypeRep arg1, Int)
id1 (TypeRep arg2, Int)
id2) =
Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
3 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg1, Int)
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg2, Int)
id2
hashWithSalt Int
s (DTernaryTerm (TypeRep tag, tag)
tag (TypeRep arg1, Int)
id1 (TypeRep arg2, Int)
id2 (TypeRep arg3, Int)
id3) =
Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
4 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg1, Int)
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg2, Int)
id2 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg3, Int)
id3
hashWithSalt Int
s (DNotTerm Int
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
5 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
hashWithSalt Int
s (DOrTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
6 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DAndTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
7 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DEqvTerm TypeRep args
rep Int
id1 Int
id2) =
Int
s
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
8 :: Int)
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DITETerm Int
idc Int
id1 Int
id2) =
Int
s
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
9 :: Int)
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
idc
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DAddNumTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
10 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DUMinusNumTerm Int
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
11 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
hashWithSalt Int
s (DTimesNumTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
12 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DAbsNumTerm Int
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
13 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
hashWithSalt Int
s (DSignumNumTerm Int
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
14 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
hashWithSalt Int
s (DLTNumTerm TypeRep args
rep Int
id1 Int
id2) =
Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
15 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DLENumTerm TypeRep args
rep Int
id1 Int
id2) =
Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
16 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DAndBitsTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
17 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DOrBitsTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
18 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DXorBitsTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
19 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DComplementBitsTerm Int
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
20 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
hashWithSalt Int
s (DShiftBitsTerm Int
id1 Int
n) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
21 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
n
hashWithSalt Int
s (DRotateBitsTerm Int
id1 Int
n) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
22 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
n
hashWithSalt Int
s (DBVToSignedTerm (TypeRep (ubv n), Int)
id) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
23 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (ubv n), Int)
id
hashWithSalt Int
s (DBVToUnsignedTerm (TypeRep (sbv n), Int)
id) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
24 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (sbv n), Int)
id
hashWithSalt Int
s (DBVConcatTerm TypeRep bv1
rep1 TypeRep bv2
rep2 Int
id1 Int
id2) =
Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
25 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep bv1
rep1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep bv2
rep2 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DBVSelectTerm TypeRep ix
ix (TypeRep (bv n), Int)
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
26 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep ix
ix forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (bv n), Int)
id1
hashWithSalt Int
s (DBVExtendTerm Bool
signed TypeRep r
n (TypeRep (bv l), Int)
id1) =
Int
s
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
27 :: Int)
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Bool
signed
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep r
n
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (bv l), Int)
id1
hashWithSalt Int
s (DTabularFunApplyTerm (TypeRep (a =-> t), Int)
id1 (TypeRep a, Int)
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
28 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (a =-> t), Int)
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep a, Int)
id2
hashWithSalt Int
s (DGeneralFunApplyTerm (TypeRep (a --> t), Int)
id1 (TypeRep a, Int)
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
29 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (a --> t), Int)
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep a, Int)
id2
hashWithSalt Int
s (DDivIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
30 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DModIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
31 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DQuotIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
32 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DRemIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
33 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DDivBoundedIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
34 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DModBoundedIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
35 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DQuotBoundedIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
36 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DRemBoundedIntegralTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
37 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
defaultValueForBool :: Bool
defaultValueForBool :: Bool
defaultValueForBool = Bool
False
defaultValueForBoolDyn :: ModelValue
defaultValueForBoolDyn :: ModelValue
defaultValueForBoolDyn = forall a. (Show a, Eq a, Hashable a, Typeable a) => a -> ModelValue
toModelValue Bool
defaultValueForBool
instance SupportedPrim Bool where
pformatCon :: Bool -> String
pformatCon Bool
True = String
"true"
pformatCon Bool
False = String
"false"
defaultValue :: Bool
defaultValue = Bool
defaultValueForBool
defaultValueDynamic :: forall (proxy :: * -> *). proxy Bool -> ModelValue
defaultValueDynamic proxy Bool
_ = ModelValue
defaultValueForBoolDyn
defaultValueForInteger :: Integer
defaultValueForInteger :: Integer
defaultValueForInteger = Integer
0
defaultValueForIntegerDyn :: ModelValue
defaultValueForIntegerDyn :: ModelValue
defaultValueForIntegerDyn = forall a. (Show a, Eq a, Hashable a, Typeable a) => a -> ModelValue
toModelValue Integer
defaultValueForInteger
instance SupportedPrim Integer where
pformatCon :: Integer -> String
pformatCon = forall a. Show a => a -> String
show
defaultValue :: Integer
defaultValue = Integer
defaultValueForInteger
defaultValueDynamic :: forall (proxy :: * -> *). proxy Integer -> ModelValue
defaultValueDynamic proxy Integer
_ = ModelValue
defaultValueForIntegerDyn
instance (KnownNat w, 1 <= w) => SupportedPrim (IntN w) where
type PrimConstraint (IntN w) = (KnownNat w, 1 <= w)
pformatCon :: IntN w -> String
pformatCon = forall a. Show a => a -> String
show
defaultValue :: IntN w
defaultValue = IntN w
0
instance (KnownNat w, 1 <= w) => SupportedPrim (WordN w) where
type PrimConstraint (WordN w) = (KnownNat w, 1 <= w)
pformatCon :: WordN w -> String
pformatCon = forall a. Show a => a -> String
show
defaultValue :: WordN w
defaultValue = WordN w
0
data (-->) a b where
GeneralFun :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b
instance (LinkedRep a sa, LinkedRep b sb) => Function (a --> b) where
type Arg (a --> b) = SymType a
type Ret (a --> b) = SymType b
(GeneralFun TypedSymbol a
s Term b
t) # :: (a --> b) -> Arg (a --> b) -> Ret (a --> b)
# Arg (a --> b)
x = forall con sym. LinkedRep con sym => Term con -> sym
wrapTerm forall a b. (a -> b) -> a -> b
$ forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
s (forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm Arg (a --> b)
x) Term b
t
infixr 0 -->
buildGeneralFun :: () => (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b
buildGeneralFun :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun TypedSymbol a
arg Term b
v = forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol a
newarg (forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
arg (forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm TypedSymbol a
newarg) Term b
v)
where
newarg :: TypedSymbol a
newarg = forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo TypedSymbol a
arg ARG
ARG
data ARG = ARG
deriving (ARG -> ARG -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ARG -> ARG -> Bool
$c/= :: ARG -> ARG -> Bool
== :: ARG -> ARG -> Bool
$c== :: ARG -> ARG -> Bool
Eq, Eq ARG
ARG -> ARG -> Bool
ARG -> ARG -> Ordering
ARG -> ARG -> ARG
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ARG -> ARG -> ARG
$cmin :: ARG -> ARG -> ARG
max :: ARG -> ARG -> ARG
$cmax :: ARG -> ARG -> ARG
>= :: ARG -> ARG -> Bool
$c>= :: ARG -> ARG -> Bool
> :: ARG -> ARG -> Bool
$c> :: ARG -> ARG -> Bool
<= :: ARG -> ARG -> Bool
$c<= :: ARG -> ARG -> Bool
< :: ARG -> ARG -> Bool
$c< :: ARG -> ARG -> Bool
compare :: ARG -> ARG -> Ordering
$ccompare :: ARG -> ARG -> Ordering
Ord, forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => ARG -> m Exp
forall (m :: * -> *). Quote m => ARG -> Code m ARG
liftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
$cliftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
lift :: forall (m :: * -> *). Quote m => ARG -> m Exp
$clift :: forall (m :: * -> *). Quote m => ARG -> m Exp
Lift, Int -> ARG -> ShowS
[ARG] -> ShowS
ARG -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ARG] -> ShowS
$cshowList :: [ARG] -> ShowS
show :: ARG -> String
$cshow :: ARG -> String
showsPrec :: Int -> ARG -> ShowS
$cshowsPrec :: Int -> ARG -> ShowS
Show, forall x. Rep ARG x -> ARG
forall x. ARG -> Rep ARG x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ARG x -> ARG
$cfrom :: forall x. ARG -> Rep ARG x
Generic)
instance NFData ARG where
rnf :: ARG -> ()
rnf ARG
ARG = ()
instance Hashable ARG where
hashWithSalt :: Int -> ARG -> Int
hashWithSalt Int
s ARG
ARG = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int)
instance Eq (a --> b) where
GeneralFun TypedSymbol a
sym1 Term b
tm1 == :: (a --> b) -> (a --> b) -> Bool
== GeneralFun TypedSymbol a
sym2 Term b
tm2 = TypedSymbol a
sym1 forall a. Eq a => a -> a -> Bool
== TypedSymbol a
sym2 Bool -> Bool -> Bool
&& Term b
tm1 forall a. Eq a => a -> a -> Bool
== Term b
tm2
instance Show (a --> b) where
show :: (a --> b) -> String
show (GeneralFun TypedSymbol a
sym Term b
tm) = String
"\\(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypedSymbol a
sym forall a. [a] -> [a] -> [a]
++ String
") -> " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term b
tm
instance Lift (a --> b) where
liftTyped :: forall (m :: * -> *). Quote m => (a --> b) -> Code m (a --> b)
liftTyped (GeneralFun TypedSymbol a
sym Term b
tm) = [||GeneralFun sym tm||]
instance Hashable (a --> b) where
Int
s hashWithSalt :: Int -> (a --> b) -> Int
`hashWithSalt` (GeneralFun TypedSymbol a
sym Term b
tm) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol a
sym forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Term b
tm
instance NFData (a --> b) where
rnf :: (a --> b) -> ()
rnf (GeneralFun TypedSymbol a
sym Term b
tm) = forall a. NFData a => a -> ()
rnf TypedSymbol a
sym seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Term b
tm
instance (SupportedPrim a, SupportedPrim b) => SupportedPrim (a --> b) where
type PrimConstraint (a --> b) = (SupportedPrim a, SupportedPrim b)
defaultValue :: a --> b
defaultValue = forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun (forall t. SupportedPrim t => String -> TypedSymbol t
SimpleSymbol String
"a") (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall t. SupportedPrim t => t
defaultValue)
instance
(SupportedPrim a, SupportedPrim b) =>
SupportedPrim (a =-> b)
where
type PrimConstraint (a =-> b) = (SupportedPrim a, SupportedPrim b)
defaultValue :: a =-> b
defaultValue = forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] (forall t. SupportedPrim t => t
defaultValue @b)