{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
( SupportedPrim (..),
UnaryOp (..),
BinaryOp (..),
TernaryOp (..),
TypedSymbol (..),
SomeTypedSymbol (..),
showUntyped,
withSymbolSupported,
someTypedSymbol,
Term (..),
UTerm (..),
FunArg (..),
type (-->) (..),
)
where
import Control.DeepSeq
import Data.Bits
import Data.Function (on)
import Data.Hashable
import Data.Interned
import Data.Kind
import Data.String
import Data.Typeable (Proxy (..), cast)
import GHC.Generics
import GHC.TypeNats
import Grisette.Core.Data.Class.BitVector
import Grisette.Core.Data.Class.Function
import Grisette.IR.SymPrim.Data.BV
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
import Grisette.IR.SymPrim.Data.Prim.ModelValue
import Grisette.IR.SymPrim.Data.Prim.Utils
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.TabularFun
import Language.Haskell.TH.Syntax
import Language.Haskell.TH.Syntax.Compat
import Type.Reflection
class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where
type PrimConstraint t :: Constraint
type PrimConstraint t = ()
default withPrim :: PrimConstraint t => proxy t -> (PrimConstraint t => a) -> a
withPrim :: proxy t -> (PrimConstraint t => a) -> a
withPrim proxy t
_ PrimConstraint t => a
i = PrimConstraint t => a
i
termCache :: Cache (Term t)
termCache = forall a. (Interned a, Typeable a) => Cache a
typeMemoizedCache
pformatCon :: t -> String
default pformatCon :: (Show t) => t -> String
pformatCon = forall a. Show a => a -> String
show
pformatSym :: TypedSymbol t -> String
pformatSym = forall t. TypedSymbol t -> String
showUntyped
defaultValue :: t
defaultValueDynamic :: proxy t -> ModelValue
defaultValueDynamic proxy t
_ = forall a. (Show a, Eq a, Hashable a, Typeable a) => a -> ModelValue
toModelValue (forall t. SupportedPrim t => t
defaultValue @t)
class
(SupportedPrim arg, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) =>
UnaryOp tag arg t
| tag arg -> t
where
partialEvalUnary :: (Typeable tag, Typeable t) => tag -> Term arg -> Term t
pformatUnary :: tag -> Term arg -> String
class
( SupportedPrim arg1,
SupportedPrim arg2,
SupportedPrim t,
Lift tag,
NFData tag,
Show tag,
Typeable tag,
Eq tag,
Hashable tag
) =>
BinaryOp tag arg1 arg2 t
| tag arg1 arg2 -> t
where
partialEvalBinary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term t
pformatBinary :: tag -> Term arg1 -> Term arg2 -> String
class
( SupportedPrim arg1,
SupportedPrim arg2,
SupportedPrim arg3,
SupportedPrim t,
Lift tag,
NFData tag,
Show tag,
Typeable tag,
Eq tag,
Hashable tag
) =>
TernaryOp tag arg1 arg2 arg3 t
| tag arg1 arg2 arg3 -> t
where
partialEvalTernary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
pformatTernary :: tag -> Term arg1 -> Term arg2 -> Term arg3 -> String
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
BVConcatTerm ::
( SupportedPrim (bv a),
SupportedPrim (bv b),
SupportedPrim (bv c),
KnownNat a,
KnownNat b,
KnownNat c,
BVConcat (bv a) (bv b) (bv c)
) =>
{-# UNPACK #-} !Id ->
!(Term (bv a)) ->
!(Term (bv b)) ->
Term (bv c)
BVSelectTerm ::
( SupportedPrim (bv a),
SupportedPrim (bv w),
KnownNat a,
KnownNat w,
KnownNat ix,
BVSelect (bv a) ix w (bv w)
) =>
{-# UNPACK #-} !Id ->
!(TypeRep ix) ->
!(TypeRep w) ->
!(Term (bv a)) ->
Term (bv w)
BVExtendTerm ::
( SupportedPrim (bv a),
SupportedPrim (bv b),
KnownNat a,
KnownNat b,
KnownNat n,
BVExtend (bv a) n (bv b)
) =>
{-# UNPACK #-} !Id ->
!Bool ->
!(TypeRep n) ->
!(Term (bv a)) ->
Term (bv b)
TabularFunApplyTerm ::
( SupportedPrim a,
SupportedPrim b
) =>
{-# UNPACK #-} !Id ->
Term (a =-> b) ->
Term a ->
Term b
GeneralFunApplyTerm ::
( SupportedPrim a,
SupportedPrim b
) =>
{-# UNPACK #-} !Id ->
Term (a --> b) ->
Term a ->
Term b
DivIntegerTerm :: !Id -> Term Integer -> Term Integer -> Term Integer
ModIntegerTerm :: !Id -> Term Integer -> Term Integer -> Term Integer
instance NFData (Term a) where
rnf :: Term a -> ()
rnf Term a
i = forall t. Term t -> Int
identity Term a
i seq :: forall a b. a -> b -> b
`seq` ()
instance Lift (Term t) where
lift :: forall (m :: * -> *). Quote m => Term t -> m Exp
lift = forall a (m :: * -> *). Quote m => Splice m a -> m Exp
unTypeSplice forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (m :: * -> *). (Lift t, Quote m) => t -> Code m t
liftTyped
liftTyped :: forall (m :: * -> *). Quote m => Term t -> Code m (Term t)
liftTyped (ConTerm Int
_ t
i) = [||conTerm i||]
liftTyped (SymTerm Int
_ TypedSymbol t
sym) = [||symTerm sym||]
liftTyped (UnaryTerm Int
_ tag
tag Term arg
arg) = [||constructUnary tag arg||]
liftTyped (BinaryTerm Int
_ tag
tag Term arg1
arg1 Term arg2
arg2) = [||constructBinary tag arg1 arg2||]
liftTyped (TernaryTerm Int
_ tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) = [||constructTernary tag arg1 arg2 arg3||]
liftTyped (NotTerm Int
_ Term Bool
arg) = [||notTerm arg||]
liftTyped (OrTerm Int
_ Term Bool
arg1 Term Bool
arg2) = [||orTerm arg1 arg2||]
liftTyped (AndTerm Int
_ Term Bool
arg1 Term Bool
arg2) = [||andTerm arg1 arg2||]
liftTyped (EqvTerm Int
_ Term t
arg1 Term t
arg2) = [||eqvTerm arg1 arg2||]
liftTyped (ITETerm Int
_ Term Bool
cond Term t
arg1 Term t
arg2) = [||iteTerm cond arg1 arg2||]
liftTyped (AddNumTerm Int
_ Term t
arg1 Term t
arg2) = [||addNumTerm arg1 arg2||]
liftTyped (UMinusNumTerm Int
_ Term t
arg) = [||uminusNumTerm arg||]
liftTyped (TimesNumTerm Int
_ Term t
arg1 Term t
arg2) = [||timesNumTerm arg1 arg2||]
liftTyped (AbsNumTerm Int
_ Term t
arg) = [||absNumTerm arg||]
liftTyped (SignumNumTerm Int
_ Term t
arg) = [||signumNumTerm arg||]
liftTyped (LTNumTerm Int
_ Term t
arg1 Term t
arg2) = [||ltNumTerm arg1 arg2||]
liftTyped (LENumTerm Int
_ Term t
arg1 Term t
arg2) = [||leNumTerm arg1 arg2||]
liftTyped (AndBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||andBitsTerm arg1 arg2||]
liftTyped (OrBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||orBitsTerm arg1 arg2||]
liftTyped (XorBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||xorBitsTerm arg1 arg2||]
liftTyped (ComplementBitsTerm Int
_ Term t
arg) = [||complementBitsTerm arg||]
liftTyped (ShiftBitsTerm Int
_ Term t
arg Int
n) = [||shiftBitsTerm arg n||]
liftTyped (RotateBitsTerm Int
_ Term t
arg Int
n) = [||rotateBitsTerm arg n||]
liftTyped (BVConcatTerm Int
_ Term (bv a)
arg1 Term (bv b)
arg2) = [||bvconcatTerm arg1 arg2||]
liftTyped (BVSelectTerm Int
_ (TypeRep ix
_ :: TypeRep ix) (TypeRep w
_ :: TypeRep w) Term (bv a)
arg) = [||bvselectTerm (Proxy @ix) (Proxy @w) arg||]
liftTyped (BVExtendTerm Int
_ Bool
signed (TypeRep n
_ :: TypeRep n) Term (bv a)
arg) = [||bvextendTerm signed (Proxy @n) arg||]
liftTyped (TabularFunApplyTerm Int
_ Term (a =-> t)
func Term a
arg) = [||tabularFunApplyTerm func arg||]
liftTyped (GeneralFunApplyTerm Int
_ Term (a --> t)
func Term a
arg) = [||generalFunApplyTerm func arg||]
liftTyped (DivIntegerTerm Int
_ Term Integer
arg1 Term Integer
arg2) = [||divIntegerTerm arg1 arg2||]
liftTyped (ModIntegerTerm Int
_ Term Integer
arg1 Term Integer
arg2) = [||modIntegerTerm arg1 arg2||]
instance Show (Term ty) where
show :: Term ty -> String
show (ConTerm Int
i ty
v) = String
"ConTerm{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", v=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ty
v forall a. [a] -> [a] -> [a]
++ String
"}"
show (SymTerm Int
i TypedSymbol ty
name) =
String
"SymTerm{id="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
forall a. [a] -> [a] -> [a]
++ String
", name="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypedSymbol ty
name
forall a. [a] -> [a] -> [a]
++ String
", type="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @ty)
forall a. [a] -> [a] -> [a]
++ String
"}"
show (UnaryTerm Int
i tag
tag Term arg
arg) = String
"Unary{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", tag=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show tag
tag forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (BinaryTerm Int
i tag
tag Term arg1
arg1 Term arg2
arg2) =
String
"Binary{id="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
forall a. [a] -> [a] -> [a]
++ String
", tag="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show tag
tag
forall a. [a] -> [a] -> [a]
++ String
", arg1="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg1
arg1
forall a. [a] -> [a] -> [a]
++ String
", arg2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg2
arg2
forall a. [a] -> [a] -> [a]
++ String
"}"
show (TernaryTerm Int
i tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) =
String
"Ternary{id="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
forall a. [a] -> [a] -> [a]
++ String
", tag="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show tag
tag
forall a. [a] -> [a] -> [a]
++ String
", arg1="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg1
arg1
forall a. [a] -> [a] -> [a]
++ String
", arg2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg2
arg2
forall a. [a] -> [a] -> [a]
++ String
", arg3="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term arg3
arg3
forall a. [a] -> [a] -> [a]
++ String
"}"
show (NotTerm Int
i Term Bool
arg) = String
"Not{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (OrTerm Int
i Term Bool
arg1 Term Bool
arg2) = String
"Or{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (AndTerm Int
i Term Bool
arg1 Term Bool
arg2) = String
"And{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (EqvTerm Int
i Term t
arg1 Term t
arg2) = String
"Eqv{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (ITETerm Int
i Term Bool
cond Term ty
l Term ty
r) =
String
"ITE{id="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
forall a. [a] -> [a] -> [a]
++ String
", cond="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
cond
forall a. [a] -> [a] -> [a]
++ String
", then="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
l
forall a. [a] -> [a] -> [a]
++ String
", else="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
r
forall a. [a] -> [a] -> [a]
++ String
"}"
show (AddNumTerm Int
i Term ty
arg1 Term ty
arg2) = String
"AddNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (UMinusNumTerm Int
i Term ty
arg) = String
"UMinusNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (TimesNumTerm Int
i Term ty
arg1 Term ty
arg2) = String
"TimesNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (AbsNumTerm Int
i Term ty
arg) = String
"AbsNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (SignumNumTerm Int
i Term ty
arg) = String
"SignumNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (LTNumTerm Int
i Term t
arg1 Term t
arg2) = String
"LTNum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (LENumTerm Int
i Term t
arg1 Term t
arg2) = String
"LENum{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (AndBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"AndBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (OrBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"OrBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (XorBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"XorBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (ComplementBitsTerm Int
i Term ty
arg) = String
"ComplementBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (ShiftBitsTerm Int
i Term ty
arg Int
n) = String
"ShiftBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
", n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
"}"
show (RotateBitsTerm Int
i Term ty
arg Int
n) = String
"RotateBits{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term ty
arg forall a. [a] -> [a] -> [a]
++ String
", n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
"}"
show (BVConcatTerm Int
i Term (bv a)
arg1 Term (bv b)
arg2) = String
"BVConcat{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (bv a)
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (bv b)
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (BVSelectTerm Int
i TypeRep ix
ix TypeRep w
w Term (bv a)
arg) =
String
"BVSelect{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", ix=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep ix
ix forall a. [a] -> [a] -> [a]
++ String
", w=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep w
w forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (bv a)
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (BVExtendTerm Int
i Bool
signed TypeRep n
n Term (bv a)
arg) =
String
"BVExtend{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", signed=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Bool
signed forall a. [a] -> [a] -> [a]
++ String
", n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep n
n forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (bv a)
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (TabularFunApplyTerm Int
i Term (a =-> ty)
func Term a
arg) =
String
"TabularFunApply{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", func=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (a =-> ty)
func forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term a
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (GeneralFunApplyTerm Int
i Term (a --> ty)
func Term a
arg) =
String
"GeneralFunApply{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", func=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (a --> ty)
func forall a. [a] -> [a] -> [a]
++ String
", arg=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term a
arg forall a. [a] -> [a] -> [a]
++ String
"}"
show (DivIntegerTerm Int
i Term Integer
arg1 Term Integer
arg2) =
String
"DivInteger{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Integer
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Integer
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
show (ModIntegerTerm Int
i Term Integer
arg1 Term Integer
arg2) =
String
"ModInteger{id=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
", arg1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Integer
arg1 forall a. [a] -> [a] -> [a]
++ String
", arg2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Integer
arg2 forall a. [a] -> [a] -> [a]
++ String
"}"
instance (SupportedPrim t) => Eq (Term t) where
== :: Term t -> Term t -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall t. Term t -> Int
identity
instance (SupportedPrim t) => Hashable (Term t) where
hashWithSalt :: Int -> Term t -> Int
hashWithSalt Int
s Term t
t = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s forall a b. (a -> b) -> a -> b
$ forall t. Term t -> Int
identity Term t
t
data UTerm t where
UConTerm :: (SupportedPrim t) => !t -> UTerm t
USymTerm :: (SupportedPrim t) => !(TypedSymbol t) -> UTerm t
UUnaryTerm :: (UnaryOp tag arg t) => !tag -> !(Term arg) -> UTerm t
UBinaryTerm ::
(BinaryOp tag arg1 arg2 t) =>
!tag ->
!(Term arg1) ->
!(Term arg2) ->
UTerm t
UTernaryTerm ::
(TernaryOp tag arg1 arg2 arg3 t) =>
!tag ->
!(Term arg1) ->
!(Term arg2) ->
!(Term arg3) ->
UTerm t
UNotTerm :: !(Term Bool) -> UTerm Bool
UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
UEqvTerm :: SupportedPrim t => !(Term t) -> !(Term t) -> UTerm Bool
UITETerm :: SupportedPrim t => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t
UAddNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
UUMinusNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
UTimesNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
UAbsNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
USignumNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
ULTNumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool
ULENumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool
UAndBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
UOrBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
UXorBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
UComplementBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> UTerm t
UShiftBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t
URotateBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t
UBVConcatTerm ::
( SupportedPrim (bv a),
SupportedPrim (bv b),
SupportedPrim (bv c),
KnownNat a,
KnownNat b,
KnownNat c,
BVConcat (bv a) (bv b) (bv c)
) =>
!(Term (bv a)) ->
!(Term (bv b)) ->
UTerm (bv c)
UBVSelectTerm ::
( SupportedPrim (bv a),
SupportedPrim (bv w),
KnownNat a,
KnownNat ix,
KnownNat w,
BVSelect (bv a) ix w (bv w)
) =>
!(TypeRep ix) ->
!(TypeRep w) ->
!(Term (bv a)) ->
UTerm (bv w)
UBVExtendTerm ::
( SupportedPrim (bv a),
SupportedPrim (bv b),
KnownNat a,
KnownNat b,
KnownNat n,
BVExtend (bv a) n (bv b)
) =>
!Bool ->
!(TypeRep n) ->
!(Term (bv a)) ->
UTerm (bv b)
UTabularFunApplyTerm ::
( SupportedPrim a,
SupportedPrim b
) =>
Term (a =-> b) ->
Term a ->
UTerm b
UGeneralFunApplyTerm ::
( SupportedPrim a,
SupportedPrim b
) =>
Term (a --> b) ->
Term a ->
UTerm b
UDivIntegerTerm :: Term Integer -> Term Integer -> UTerm Integer
UModIntegerTerm :: Term Integer -> Term Integer -> UTerm Integer
eqTypedId :: (TypeRep a, Id) -> (TypeRep b, Id) -> Bool
eqTypedId :: forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep a
a, Int
i1) (TypeRep b
b, Int
i2) = Int
i1 forall a. Eq a => a -> a -> Bool
== Int
i2 Bool -> Bool -> Bool
&& forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep a
a TypeRep b
b
{-# INLINE eqTypedId #-}
eqHeteroTag :: Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag :: forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep a
tpa, a
taga) (TypeRep b
tpb, b
tagb) = forall a b. Eq a => TypeRep a -> TypeRep b -> a -> b -> Bool
eqHeteroRep TypeRep a
tpa TypeRep b
tpb a
taga b
tagb
{-# INLINE eqHeteroTag #-}
instance (SupportedPrim t) => Interned (Term t) where
type Uninterned (Term t) = UTerm t
data Description (Term t) where
DConTerm :: t -> Description (Term t)
DSymTerm :: TypedSymbol t -> Description (Term t)
DUnaryTerm ::
(Eq tag, Hashable tag) =>
{-# UNPACK #-} !(TypeRep tag, tag) ->
{-# UNPACK #-} !(TypeRep arg, Id) ->
Description (Term t)
DBinaryTerm ::
(Eq tag, Hashable tag) =>
{-# UNPACK #-} !(TypeRep tag, tag) ->
{-# UNPACK #-} !(TypeRep arg1, Id) ->
{-# UNPACK #-} !(TypeRep arg2, Id) ->
Description (Term t)
DTernaryTerm ::
(Eq tag, Hashable tag) =>
{-# UNPACK #-} !(TypeRep tag, tag) ->
{-# UNPACK #-} !(TypeRep arg1, Id) ->
{-# UNPACK #-} !(TypeRep arg2, Id) ->
{-# UNPACK #-} !(TypeRep arg3, Id) ->
Description (Term t)
DNotTerm :: {-# UNPACK #-} !Id -> Description (Term Bool)
DOrTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
DAndTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
DEqvTerm :: TypeRep args -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
DITETerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DAddNumTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DUMinusNumTerm :: {-# UNPACK #-} !Id -> Description (Term t)
DTimesNumTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DAbsNumTerm :: {-# UNPACK #-} !Id -> Description (Term t)
DSignumNumTerm :: {-# UNPACK #-} !Id -> Description (Term t)
DLTNumTerm :: TypeRep args -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
DLENumTerm :: TypeRep args -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
DAndBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DOrBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DXorBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DComplementBitsTerm :: {-# UNPACK #-} !Id -> Description (Term t)
DShiftBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Int -> Description (Term t)
DRotateBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Int -> Description (Term t)
DBVConcatTerm :: TypeRep bv1 -> TypeRep bv2 -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
DBVSelectTerm ::
forall bv (a :: Nat) (w :: Nat) (ix :: Nat).
!(TypeRep ix) ->
!(TypeRep (bv a), Id) ->
Description (Term (bv w))
DBVExtendTerm ::
forall bv (a :: Nat) (b :: Nat) (n :: Nat).
!Bool ->
!(TypeRep n) ->
{-# UNPACK #-} !(TypeRep (bv a), Id) ->
Description (Term (bv b))
DTabularFunApplyTerm ::
{-# UNPACK #-} !(TypeRep (a =-> b), Id) ->
{-# UNPACK #-} !(TypeRep a, Id) ->
Description (Term b)
DGeneralFunApplyTerm ::
{-# UNPACK #-} !(TypeRep (a --> b), Id) ->
{-# UNPACK #-} !(TypeRep a, Id) ->
Description (Term b)
DDivIntegerTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Integer)
DModIntegerTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Integer)
describe :: Uninterned (Term t) -> Description (Term t)
describe (UConTerm t
v) = forall t. t -> Description (Term t)
DConTerm t
v
describe ((USymTerm TypedSymbol t
name) :: UTerm t) = forall t. TypedSymbol t -> Description (Term t)
DSymTerm @t TypedSymbol t
name
describe ((UUnaryTerm (tag
tag :: tagt) (Term arg
tm :: Term arg)) :: UTerm t) =
forall a a t.
(Eq a, Hashable a) =>
(TypeRep a, a) -> (TypeRep a, Int) -> Description (Term t)
DUnaryTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, forall t. Term t -> Int
identity Term arg
tm)
describe ((UBinaryTerm (tag
tag :: tagt) (Term arg1
tm1 :: Term arg1) (Term arg2
tm2 :: Term arg2)) :: UTerm t) =
forall a a b t.
(Eq a, Hashable a) =>
(TypeRep a, a)
-> (TypeRep a, Int) -> (TypeRep b, Int) -> Description (Term t)
DBinaryTerm @tagt @arg1 @arg2 @t (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, forall t. Term t -> Int
identity Term arg1
tm1) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep, forall t. Term t -> Int
identity Term arg2
tm2)
describe ((UTernaryTerm (tag
tag :: tagt) (Term arg1
tm1 :: Term arg1) (Term arg2
tm2 :: Term arg2) (Term arg3
tm3 :: Term arg3)) :: UTerm t) =
forall a a b n t.
(Eq a, Hashable a) =>
(TypeRep a, a)
-> (TypeRep a, Int)
-> (TypeRep b, Int)
-> (TypeRep n, Int)
-> Description (Term t)
DTernaryTerm @tagt @arg1 @arg2 @arg3 @t
(forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag)
(forall {k} (a :: k). Typeable a => TypeRep a
typeRep, forall t. Term t -> Int
identity Term arg1
tm1)
(forall {k} (a :: k). Typeable a => TypeRep a
typeRep, forall t. Term t -> Int
identity Term arg2
tm2)
(forall {k} (a :: k). Typeable a => TypeRep a
typeRep, forall t. Term t -> Int
identity Term arg3
tm3)
describe (UNotTerm Term Bool
arg) = Int -> Description (Term Bool)
DNotTerm (forall t. Term t -> Int
identity Term Bool
arg)
describe (UOrTerm Term Bool
arg1 Term Bool
arg2) = Int -> Int -> Description (Term Bool)
DOrTerm (forall t. Term t -> Int
identity Term Bool
arg1) (forall t. Term t -> Int
identity Term Bool
arg2)
describe (UAndTerm Term Bool
arg1 Term Bool
arg2) = Int -> Int -> Description (Term Bool)
DAndTerm (forall t. Term t -> Int
identity Term Bool
arg1) (forall t. Term t -> Int
identity Term Bool
arg2)
describe (UEqvTerm (Term t
arg1 :: Term arg) Term t
arg2) = forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DEqvTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UITETerm Term Bool
cond (Term t
l :: Term arg) Term t
r) = forall t. Int -> Int -> Int -> Description (Term t)
DITETerm (forall t. Term t -> Int
identity Term Bool
cond) (forall t. Term t -> Int
identity Term t
l) (forall t. Term t -> Int
identity Term t
r)
describe (UAddNumTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DAddNumTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UUMinusNumTerm Term t
arg) = forall t. Int -> Description (Term t)
DUMinusNumTerm (forall t. Term t -> Int
identity Term t
arg)
describe (UTimesNumTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DTimesNumTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UAbsNumTerm Term t
arg) = forall t. Int -> Description (Term t)
DAbsNumTerm (forall t. Term t -> Int
identity Term t
arg)
describe (USignumNumTerm Term t
arg) = forall t. Int -> Description (Term t)
DSignumNumTerm (forall t. Term t -> Int
identity Term t
arg)
describe (ULTNumTerm (Term t
arg1 :: arg) Term t
arg2) = forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DLTNumTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (ULENumTerm (Term t
arg1 :: arg) Term t
arg2) = forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DLENumTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UAndBitsTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DAndBitsTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UOrBitsTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DOrBitsTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UXorBitsTerm Term t
arg1 Term t
arg2) = forall t. Int -> Int -> Description (Term t)
DXorBitsTerm (forall t. Term t -> Int
identity Term t
arg1) (forall t. Term t -> Int
identity Term t
arg2)
describe (UComplementBitsTerm Term t
arg) = forall t. Int -> Description (Term t)
DComplementBitsTerm (forall t. Term t -> Int
identity Term t
arg)
describe (UShiftBitsTerm Term t
arg Int
n) = forall t. Int -> Int -> Description (Term t)
DShiftBitsTerm (forall t. Term t -> Int
identity Term t
arg) Int
n
describe (URotateBitsTerm Term t
arg Int
n) = forall t. Int -> Int -> Description (Term t)
DRotateBitsTerm (forall t. Term t -> Int
identity Term t
arg) Int
n
describe (UBVConcatTerm (Term (bv a)
arg1 :: bv1) (Term (bv b)
arg2 :: bv2)) =
forall a a t.
TypeRep a -> TypeRep a -> Int -> Int -> Description (Term t)
DBVConcatTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv1) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv2) (forall t. Term t -> Int
identity Term (bv a)
arg1) (forall t. Term t -> Int
identity Term (bv b)
arg2)
describe (UBVSelectTerm (TypeRep ix
ix :: TypeRep ix) TypeRep w
_ (Term (bv a)
arg :: Term arg)) =
forall (a :: Natural -> *) (a :: Natural) (b :: Natural)
(n :: Natural).
TypeRep n -> (TypeRep (a a), Int) -> Description (Term (a b))
DBVSelectTerm TypeRep ix
ix (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, forall t. Term t -> Int
identity Term (bv a)
arg)
describe (UBVExtendTerm Bool
signed (TypeRep n
n :: TypeRep n) (Term (bv a)
arg :: Term arg)) =
forall (a :: Natural -> *) (a :: Natural) (b :: Natural)
(n :: Natural).
Bool
-> TypeRep n -> (TypeRep (a a), Int) -> Description (Term (a b))
DBVExtendTerm Bool
signed TypeRep n
n (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, forall t. Term t -> Int
identity Term (bv a)
arg)
describe (UTabularFunApplyTerm (Term (a =-> t)
func :: Term f) (Term a
arg :: Term a)) =
forall a b.
(TypeRep (a =-> b), Int)
-> (TypeRep a, Int) -> Description (Term b)
DTabularFunApplyTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep f, forall t. Term t -> Int
identity Term (a =-> t)
func) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep a, forall t. Term t -> Int
identity Term a
arg)
describe (UGeneralFunApplyTerm (Term (a --> t)
func :: Term f) (Term a
arg :: Term a)) =
forall a b.
(TypeRep (a --> b), Int)
-> (TypeRep a, Int) -> Description (Term b)
DGeneralFunApplyTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep f, forall t. Term t -> Int
identity Term (a --> t)
func) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep a, forall t. Term t -> Int
identity Term a
arg)
describe (UDivIntegerTerm Term Integer
arg1 Term Integer
arg2) = Int -> Int -> Description (Term Integer)
DDivIntegerTerm (forall t. Term t -> Int
identity Term Integer
arg1) (forall t. Term t -> Int
identity Term Integer
arg2)
describe (UModIntegerTerm Term Integer
arg1 Term Integer
arg2) = Int -> Int -> Description (Term Integer)
DModIntegerTerm (forall t. Term t -> Int
identity Term Integer
arg1) (forall t. Term t -> Int
identity Term Integer
arg2)
identify :: Int -> Uninterned (Term t) -> Term t
identify Int
i = UTerm t -> Term t
go
where
go :: UTerm t -> Term t
go (UConTerm t
v) = forall t. SupportedPrim t => Int -> t -> Term t
ConTerm Int
i t
v
go (USymTerm TypedSymbol t
v) = forall t. SupportedPrim t => Int -> TypedSymbol t -> Term t
SymTerm Int
i TypedSymbol t
v
go (UUnaryTerm tag
tag Term arg
tm) = forall a a t. UnaryOp a a t => Int -> a -> Term a -> Term t
UnaryTerm Int
i tag
tag Term arg
tm
go (UBinaryTerm tag
tag Term arg1
tm1 Term arg2
tm2) = forall a a b t.
BinaryOp a a b t =>
Int -> a -> Term a -> Term b -> Term t
BinaryTerm Int
i tag
tag Term arg1
tm1 Term arg2
tm2
go (UTernaryTerm tag
tag Term arg1
tm1 Term arg2
tm2 Term arg3
tm3) = forall a a b n t.
TernaryOp a a b n t =>
Int -> a -> Term a -> Term b -> Term n -> Term t
TernaryTerm Int
i tag
tag Term arg1
tm1 Term arg2
tm2 Term arg3
tm3
go (UNotTerm Term Bool
arg) = Int -> Term Bool -> Term Bool
NotTerm Int
i Term Bool
arg
go (UOrTerm Term Bool
arg1 Term Bool
arg2) = Int -> Term Bool -> Term Bool -> Term Bool
OrTerm Int
i Term Bool
arg1 Term Bool
arg2
go (UAndTerm Term Bool
arg1 Term Bool
arg2) = Int -> Term Bool -> Term Bool -> Term Bool
AndTerm Int
i Term Bool
arg1 Term Bool
arg2
go (UEqvTerm Term t
arg1 Term t
arg2) = forall a. SupportedPrim a => Int -> Term a -> Term a -> Term Bool
EqvTerm Int
i Term t
arg1 Term t
arg2
go (UITETerm Term Bool
cond Term t
l Term t
r) = forall t.
SupportedPrim t =>
Int -> Term Bool -> Term t -> Term t -> Term t
ITETerm Int
i Term Bool
cond Term t
l Term t
r
go (UAddNumTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Num t) =>
Int -> Term t -> Term t -> Term t
AddNumTerm Int
i Term t
arg1 Term t
arg2
go (UUMinusNumTerm Term t
arg) = forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
UMinusNumTerm Int
i Term t
arg
go (UTimesNumTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Num t) =>
Int -> Term t -> Term t -> Term t
TimesNumTerm Int
i Term t
arg1 Term t
arg2
go (UAbsNumTerm Term t
arg) = forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
AbsNumTerm Int
i Term t
arg
go (USignumNumTerm Term t
arg) = forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
SignumNumTerm Int
i Term t
arg
go (ULTNumTerm Term t
arg1 Term t
arg2) = forall a.
(SupportedPrim a, Num a, Ord a) =>
Int -> Term a -> Term a -> Term Bool
LTNumTerm Int
i Term t
arg1 Term t
arg2
go (ULENumTerm Term t
arg1 Term t
arg2) = forall a.
(SupportedPrim a, Num a, Ord a) =>
Int -> Term a -> Term a -> Term Bool
LENumTerm Int
i Term t
arg1 Term t
arg2
go (UAndBitsTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Term t -> Term t
AndBitsTerm Int
i Term t
arg1 Term t
arg2
go (UOrBitsTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Term t -> Term t
OrBitsTerm Int
i Term t
arg1 Term t
arg2
go (UXorBitsTerm Term t
arg1 Term t
arg2) = forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Term t -> Term t
XorBitsTerm Int
i Term t
arg1 Term t
arg2
go (UComplementBitsTerm Term t
arg) = forall t. (SupportedPrim t, Bits t) => Int -> Term t -> Term t
ComplementBitsTerm Int
i Term t
arg
go (UShiftBitsTerm Term t
arg Int
n) = forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Int -> Term t
ShiftBitsTerm Int
i Term t
arg Int
n
go (URotateBitsTerm Term t
arg Int
n) = forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Int -> Term t
RotateBitsTerm Int
i Term t
arg Int
n
go (UBVConcatTerm Term (bv a)
arg1 Term (bv b)
arg2) = forall (a :: Natural -> *) (a :: Natural) (b :: Natural)
(n :: Natural).
(SupportedPrim (a a), SupportedPrim (a b), SupportedPrim (a n),
KnownNat a, KnownNat b, KnownNat n, BVConcat (a a) (a b) (a n)) =>
Int -> Term (a a) -> Term (a b) -> Term (a n)
BVConcatTerm Int
i Term (bv a)
arg1 Term (bv b)
arg2
go (UBVSelectTerm TypeRep ix
ix TypeRep w
w Term (bv a)
arg) = forall (a :: Natural -> *) (a :: Natural) (b :: Natural)
(n :: Natural).
(SupportedPrim (a a), SupportedPrim (a b), KnownNat a, KnownNat b,
KnownNat n, BVSelect (a a) n b (a b)) =>
Int -> TypeRep n -> TypeRep b -> Term (a a) -> Term (a b)
BVSelectTerm Int
i TypeRep ix
ix TypeRep w
w Term (bv a)
arg
go (UBVExtendTerm Bool
signed TypeRep n
n Term (bv a)
arg) = forall (a :: Natural -> *) (a :: Natural) (b :: Natural)
(n :: Natural).
(SupportedPrim (a a), SupportedPrim (a b), KnownNat a, KnownNat b,
KnownNat n, BVExtend (a a) n (a b)) =>
Int -> Bool -> TypeRep n -> Term (a a) -> Term (a b)
BVExtendTerm Int
i Bool
signed TypeRep n
n Term (bv a)
arg
go (UTabularFunApplyTerm Term (a =-> t)
func Term a
arg) = forall a b.
(SupportedPrim a, SupportedPrim b) =>
Int -> Term (a =-> b) -> Term a -> Term b
TabularFunApplyTerm Int
i Term (a =-> t)
func Term a
arg
go (UGeneralFunApplyTerm Term (a --> t)
func Term a
arg) = forall a b.
(SupportedPrim a, SupportedPrim b) =>
Int -> Term (a --> b) -> Term a -> Term b
GeneralFunApplyTerm Int
i Term (a --> t)
func Term a
arg
go (UDivIntegerTerm Term Integer
arg1 Term Integer
arg2) = Int -> Term Integer -> Term Integer -> Term Integer
DivIntegerTerm Int
i Term Integer
arg1 Term Integer
arg2
go (UModIntegerTerm Term Integer
arg1 Term Integer
arg2) = Int -> Term Integer -> Term Integer -> Term Integer
ModIntegerTerm Int
i Term Integer
arg1 Term Integer
arg2
cache :: Cache (Term t)
cache = forall t. SupportedPrim t => Cache (Term t)
termCache
instance (SupportedPrim t) => Eq (Description (Term t)) where
DConTerm (t
l :: tyl) == :: Description (Term t) -> Description (Term t) -> Bool
== DConTerm (t
r :: tyr) = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast @tyl @tyr t
l forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just t
r
DSymTerm TypedSymbol t
ls == DSymTerm TypedSymbol t
rs = TypedSymbol t
ls forall a. Eq a => a -> a -> Bool
== TypedSymbol t
rs
DUnaryTerm ((TypeRep tag, tag)
tagl :: tagl) (TypeRep arg, Int)
li == DUnaryTerm ((TypeRep tag, tag)
tagr :: tagr) (TypeRep arg, Int)
ri = forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep tag, tag)
tagl (TypeRep tag, tag)
tagr Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg, Int)
li (TypeRep arg, Int)
ri
DBinaryTerm ((TypeRep tag, tag)
tagl :: tagl) (TypeRep arg1, Int)
li1 (TypeRep arg2, Int)
li2 == DBinaryTerm ((TypeRep tag, tag)
tagr :: tagr) (TypeRep arg1, Int)
ri1 (TypeRep arg2, Int)
ri2 =
forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep tag, tag)
tagl (TypeRep tag, tag)
tagr Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg1, Int)
li1 (TypeRep arg1, Int)
ri1 Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg2, Int)
li2 (TypeRep arg2, Int)
ri2
DTernaryTerm ((TypeRep tag, tag)
tagl :: tagl) (TypeRep arg1, Int)
li1 (TypeRep arg2, Int)
li2 (TypeRep arg3, Int)
li3 == DTernaryTerm ((TypeRep tag, tag)
tagr :: tagr) (TypeRep arg1, Int)
ri1 (TypeRep arg2, Int)
ri2 (TypeRep arg3, Int)
ri3 =
forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep tag, tag)
tagl (TypeRep tag, tag)
tagr Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg1, Int)
li1 (TypeRep arg1, Int)
ri1 Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg2, Int)
li2 (TypeRep arg2, Int)
ri2 Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg3, Int)
li3 (TypeRep arg3, Int)
ri3
DNotTerm Int
li == DNotTerm Int
ri = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri
DOrTerm Int
li1 Int
li2 == DOrTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DAndTerm Int
li1 Int
li2 == DAndTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DEqvTerm TypeRep args
lrep Int
li1 Int
li2 == DEqvTerm TypeRep args
rrep Int
ri1 Int
ri2 = forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep args
lrep TypeRep args
rrep Bool -> Bool -> Bool
&& Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DITETerm Int
lc Int
li1 Int
li2 == DITETerm Int
rc Int
ri1 Int
ri2 = Int
lc forall a. Eq a => a -> a -> Bool
== Int
rc Bool -> Bool -> Bool
&& Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DAddNumTerm Int
li1 Int
li2 == DAddNumTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DUMinusNumTerm Int
li == DUMinusNumTerm Int
ri = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri
DTimesNumTerm Int
li1 Int
li2 == DTimesNumTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DAbsNumTerm Int
li == DAbsNumTerm Int
ri = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri
DSignumNumTerm Int
li == DSignumNumTerm Int
ri = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri
DLTNumTerm TypeRep args
lrep Int
li1 Int
li2 == DLTNumTerm TypeRep args
rrep Int
ri1 Int
ri2 = forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep args
lrep TypeRep args
rrep Bool -> Bool -> Bool
&& Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DLENumTerm TypeRep args
lrep Int
li1 Int
li2 == DLENumTerm TypeRep args
rrep Int
ri1 Int
ri2 = forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep args
lrep TypeRep args
rrep Bool -> Bool -> Bool
&& Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DAndBitsTerm Int
li1 Int
li2 == DAndBitsTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DOrBitsTerm Int
li1 Int
li2 == DOrBitsTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DXorBitsTerm Int
li1 Int
li2 == DXorBitsTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DComplementBitsTerm Int
li == DComplementBitsTerm Int
ri = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri
DShiftBitsTerm Int
li Int
ln == DShiftBitsTerm Int
ri Int
rn = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri Bool -> Bool -> Bool
&& Int
ln forall a. Eq a => a -> a -> Bool
== Int
rn
DRotateBitsTerm Int
li Int
ln == DRotateBitsTerm Int
ri Int
rn = Int
li forall a. Eq a => a -> a -> Bool
== Int
ri Bool -> Bool -> Bool
&& Int
ln forall a. Eq a => a -> a -> Bool
== Int
rn
DBVConcatTerm TypeRep bv1
lrep1 TypeRep bv2
lrep2 Int
li1 Int
li2 == DBVConcatTerm TypeRep bv1
rrep1 TypeRep bv2
rrep2 Int
ri1 Int
ri2 =
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep bv1
lrep1 TypeRep bv1
rrep1 Bool -> Bool -> Bool
&& forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep bv2
lrep2 TypeRep bv2
rrep2 Bool -> Bool -> Bool
&& Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DBVSelectTerm TypeRep ix
lix (TypeRep (bv a), Int)
li == DBVSelectTerm TypeRep ix
rix (TypeRep (bv a), Int)
ri =
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep ix
lix TypeRep ix
rix Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (bv a), Int)
li (TypeRep (bv a), Int)
ri
DBVExtendTerm Bool
lIsSigned TypeRep n
ln (TypeRep (bv a), Int)
li == DBVExtendTerm Bool
rIsSigned TypeRep n
rn (TypeRep (bv a), Int)
ri =
Bool
lIsSigned forall a. Eq a => a -> a -> Bool
== Bool
rIsSigned
Bool -> Bool -> Bool
&& forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep n
ln TypeRep n
rn
Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (bv a), Int)
li (TypeRep (bv a), Int)
ri
DTabularFunApplyTerm (TypeRep (a =-> t), Int)
lf (TypeRep a, Int)
li == DTabularFunApplyTerm (TypeRep (a =-> t), Int)
rf (TypeRep a, Int)
ri = forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (a =-> t), Int)
lf (TypeRep (a =-> t), Int)
rf Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep a, Int)
li (TypeRep a, Int)
ri
DGeneralFunApplyTerm (TypeRep (a --> t), Int)
lf (TypeRep a, Int)
li == DGeneralFunApplyTerm (TypeRep (a --> t), Int)
rf (TypeRep a, Int)
ri = forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (a --> t), Int)
lf (TypeRep (a --> t), Int)
rf Bool -> Bool -> Bool
&& forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep a, Int)
li (TypeRep a, Int)
ri
DDivIntegerTerm Int
li1 Int
li2 == DDivIntegerTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
DModIntegerTerm Int
li1 Int
li2 == DModIntegerTerm Int
ri1 Int
ri2 = Int
li1 forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 forall a. Eq a => a -> a -> Bool
== Int
ri2
Description (Term t)
_ == Description (Term t)
_ = Bool
False
instance (SupportedPrim t) => Hashable (Description (Term t)) where
hashWithSalt :: Int -> Description (Term t) -> Int
hashWithSalt Int
s (DConTerm t
c) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` t
c
hashWithSalt Int
s (DSymTerm TypedSymbol t
name) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol t
name
hashWithSalt Int
s (DUnaryTerm (TypeRep tag, tag)
tag (TypeRep arg, Int)
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
2 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg, Int)
id1
hashWithSalt Int
s (DBinaryTerm (TypeRep tag, tag)
tag (TypeRep arg1, Int)
id1 (TypeRep arg2, Int)
id2) =
Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
3 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg1, Int)
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg2, Int)
id2
hashWithSalt Int
s (DTernaryTerm (TypeRep tag, tag)
tag (TypeRep arg1, Int)
id1 (TypeRep arg2, Int)
id2 (TypeRep arg3, Int)
id3) =
Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
4 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg1, Int)
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg2, Int)
id2 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg3, Int)
id3
hashWithSalt Int
s (DNotTerm Int
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
5 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
hashWithSalt Int
s (DOrTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
6 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DAndTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
7 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DEqvTerm TypeRep args
rep Int
id1 Int
id2) =
Int
s
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
8 :: Int)
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DITETerm Int
idc Int
id1 Int
id2) =
Int
s
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
9 :: Int)
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
idc
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DAddNumTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
10 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DUMinusNumTerm Int
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
11 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
hashWithSalt Int
s (DTimesNumTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
12 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DAbsNumTerm Int
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
13 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
hashWithSalt Int
s (DSignumNumTerm Int
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
14 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
hashWithSalt Int
s (DLTNumTerm TypeRep args
rep Int
id1 Int
id2) =
Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
15 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DLENumTerm TypeRep args
rep Int
id1 Int
id2) =
Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
16 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DAndBitsTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
17 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DOrBitsTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
18 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DXorBitsTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
19 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DComplementBitsTerm Int
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
20 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
hashWithSalt Int
s (DShiftBitsTerm Int
id1 Int
n) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
21 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
n
hashWithSalt Int
s (DRotateBitsTerm Int
id1 Int
n) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
22 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
n
hashWithSalt Int
s (DBVConcatTerm TypeRep bv1
rep1 TypeRep bv2
rep2 Int
id1 Int
id2) =
Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
23 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep bv1
rep1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep bv2
rep2 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DBVSelectTerm TypeRep ix
ix (TypeRep (bv a), Int)
id1) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
24 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep ix
ix forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (bv a), Int)
id1
hashWithSalt Int
s (DBVExtendTerm Bool
signed TypeRep n
n (TypeRep (bv a), Int)
id1) =
Int
s
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
25 :: Int)
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Bool
signed
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep n
n
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (bv a), Int)
id1
hashWithSalt Int
s (DTabularFunApplyTerm (TypeRep (a =-> t), Int)
id1 (TypeRep a, Int)
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
26 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (a =-> t), Int)
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep a, Int)
id2
hashWithSalt Int
s (DGeneralFunApplyTerm (TypeRep (a --> t), Int)
id1 (TypeRep a, Int)
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
27 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (a --> t), Int)
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep a, Int)
id2
hashWithSalt Int
s (DDivIntegerTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
28 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
hashWithSalt Int
s (DModIntegerTerm Int
id1 Int
id2) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
29 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
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 FunArg = FunArg deriving (Int -> FunArg -> ShowS
[FunArg] -> ShowS
FunArg -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FunArg] -> ShowS
$cshowList :: [FunArg] -> ShowS
show :: FunArg -> String
$cshow :: FunArg -> String
showsPrec :: Int -> FunArg -> ShowS
$cshowsPrec :: Int -> FunArg -> ShowS
Show, FunArg -> FunArg -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FunArg -> FunArg -> Bool
$c/= :: FunArg -> FunArg -> Bool
== :: FunArg -> FunArg -> Bool
$c== :: FunArg -> FunArg -> Bool
Eq, forall x. Rep FunArg x -> FunArg
forall x. FunArg -> Rep FunArg x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep FunArg x -> FunArg
$cfrom :: forall x. FunArg -> Rep FunArg x
Generic, Eq FunArg
FunArg -> FunArg -> Bool
FunArg -> FunArg -> Ordering
FunArg -> FunArg -> FunArg
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: FunArg -> FunArg -> FunArg
$cmin :: FunArg -> FunArg -> FunArg
max :: FunArg -> FunArg -> FunArg
$cmax :: FunArg -> FunArg -> FunArg
>= :: FunArg -> FunArg -> Bool
$c>= :: FunArg -> FunArg -> Bool
> :: FunArg -> FunArg -> Bool
$c> :: FunArg -> FunArg -> Bool
<= :: FunArg -> FunArg -> Bool
$c<= :: FunArg -> FunArg -> Bool
< :: FunArg -> FunArg -> Bool
$c< :: FunArg -> FunArg -> Bool
compare :: FunArg -> FunArg -> Ordering
$ccompare :: FunArg -> FunArg -> Ordering
Ord, forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => FunArg -> m Exp
forall (m :: * -> *). Quote m => FunArg -> Code m FunArg
liftTyped :: forall (m :: * -> *). Quote m => FunArg -> Code m FunArg
$cliftTyped :: forall (m :: * -> *). Quote m => FunArg -> Code m FunArg
lift :: forall (m :: * -> *). Quote m => FunArg -> m Exp
$clift :: forall (m :: * -> *). Quote m => FunArg -> m Exp
Lift, Eq FunArg
Int -> FunArg -> Int
FunArg -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: FunArg -> Int
$chash :: FunArg -> Int
hashWithSalt :: Int -> FunArg -> Int
$chashWithSalt :: Int -> FunArg -> Int
Hashable, FunArg -> ()
forall a. (a -> ()) -> NFData a
rnf :: FunArg -> ()
$crnf :: FunArg -> ()
NFData)
data (-->) a b where
GeneralFun :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b
infixr 0 -->
instance Eq (a --> b) where
GeneralFun TypedSymbol a
sym1 Term b
tm1 == :: (a --> b) -> (a --> b) -> Bool
== GeneralFun TypedSymbol a
sym2 Term b
tm2 = TypedSymbol a
sym1 forall a. Eq a => a -> a -> Bool
== TypedSymbol a
sym2 Bool -> Bool -> Bool
&& Term b
tm1 forall a. Eq a => a -> a -> Bool
== Term b
tm2
instance Show (a --> b) where
show :: (a --> b) -> String
show (GeneralFun TypedSymbol a
sym Term b
tm) = String
"\\(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypedSymbol a
sym forall a. [a] -> [a] -> [a]
++ String
") -> " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term b
tm
instance Lift (a --> b) where
liftTyped :: forall (m :: * -> *). Quote m => (a --> b) -> Code m (a --> b)
liftTyped (GeneralFun TypedSymbol a
sym Term b
tm) = [||GeneralFun sym tm||]
instance Hashable (a --> b) where
Int
s hashWithSalt :: Int -> (a --> b) -> Int
`hashWithSalt` (GeneralFun TypedSymbol a
sym Term b
tm) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol a
sym forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Term b
tm
instance NFData (a --> b) where
rnf :: (a --> b) -> ()
rnf (GeneralFun TypedSymbol a
sym Term b
tm) = forall a. NFData a => a -> ()
rnf TypedSymbol a
sym seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Term b
tm
instance (SupportedPrim a, SupportedPrim b) => SupportedPrim (a --> b) where
type PrimConstraint (a --> b) = (SupportedPrim a, SupportedPrim b)
defaultValue :: a --> b
defaultValue = forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun (forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo (forall t. SupportedPrim t => String -> TypedSymbol t
SimpleSymbol String
"a") FunArg
FunArg) (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall t. SupportedPrim t => t
defaultValue)