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

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
  ( SupportedPrim (..),
    UnaryOp (..),
    BinaryOp (..),
    TernaryOp (..),
    TypedSymbol (..),
    SomeTypedSymbol (..),
    showUntyped,
    withSymbolSupported,
    someTypedSymbol,
    Term (..),
    UTerm (..),
    FunArg (..),
    type (-->) (..),
  )
where

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

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

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

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

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

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

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

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

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

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

instance Lift (TypedSymbol t) where
  liftTyped :: forall (m :: * -> *).
Quote m =>
TypedSymbol t -> Code m (TypedSymbol t)
liftTyped (SimpleSymbol 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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep t -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t)
  show (IndexedSymbol String
str Int
i) = String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep t -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t)
  show (WithInfo TypedSymbol t
s a
info) = TypedSymbol t -> String
forall t. TypedSymbol t -> String
showUntyped TypedSymbol t
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
info String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep t -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t)

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

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

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

instance SupportedPrim t => IsString (TypedSymbol t) where
  fromString :: String -> TypedSymbol t
fromString = String -> TypedSymbol t
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 = a
SupportedPrim t => a
a
withSymbolSupported (IndexedSymbol String
_ Int
_) SupportedPrim t => a
a = a
SupportedPrim t => a
a
withSymbolSupported (WithInfo TypedSymbol t
_ a
_) SupportedPrim t => a
a = a
SupportedPrim t => a
a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

data Term t where
  ConTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !t -> Term t
  SymTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(TypedSymbol t) -> Term t
  UnaryTerm ::
    (UnaryOp tag arg t) =>
    {-# UNPACK #-} !Id ->
    !tag ->
    !(Term arg) ->
    Term t
  BinaryTerm ::
    (BinaryOp tag arg1 arg2 t) =>
    {-# UNPACK #-} !Id ->
    !tag ->
    !(Term arg1) ->
    !(Term arg2) ->
    Term t
  TernaryTerm ::
    (TernaryOp tag arg1 arg2 arg3 t) =>
    {-# UNPACK #-} !Id ->
    !tag ->
    !(Term arg1) ->
    !(Term arg2) ->
    !(Term arg3) ->
    Term t
  NotTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> Term Bool
  OrTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
  AndTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
  EqvTerm :: SupportedPrim t => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
  ITETerm :: SupportedPrim t => {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t
  AddNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  UMinusNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
  TimesNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  AbsNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
  SignumNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
  LTNumTerm :: (SupportedPrim t, Num t, Ord t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
  LENumTerm :: (SupportedPrim t, Num t, Ord t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
  AndBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  OrBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  XorBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  ComplementBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
  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 = Term a -> Int
forall t. Term t -> Int
identity Term a
i Int -> () -> ()
`seq` ()

instance Lift (Term t) where
  lift :: forall (m :: * -> *). Quote m => Term t -> m Exp
lift = Splice m (Term t) -> m Exp
forall a (m :: * -> *). Quote m => Splice m a -> m Exp
unTypeSplice (Splice m (Term t) -> m Exp)
-> (Term t -> Splice m (Term t)) -> Term t -> m Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term t -> Splice m (Term t)
forall t (m :: * -> *). (Lift t, Quote m) => t -> Code m t
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=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", v=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ty -> String
forall a. Show a => a -> String
show ty
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (SymTerm Int
i TypedSymbol ty
name) =
    String
"SymTerm{id="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", name="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypedSymbol ty -> String
forall a. Show a => a -> String
show TypedSymbol ty
name
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", type="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep ty -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @ty)
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (UnaryTerm Int
i tag
tag Term arg
arg) = String
"Unary{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", tag=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ tag -> String
forall a. Show a => a -> String
show tag
tag String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg -> String
forall a. Show a => a -> String
show Term arg
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (BinaryTerm Int
i tag
tag Term arg1
arg1 Term arg2
arg2) =
    String
"Binary{id="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", tag="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ tag -> String
forall a. Show a => a -> String
show tag
tag
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg1 -> String
forall a. Show a => a -> String
show Term arg1
arg1
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg2 -> String
forall a. Show a => a -> String
show Term arg2
arg2
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (TernaryTerm Int
i tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) =
    String
"Ternary{id="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", tag="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ tag -> String
forall a. Show a => a -> String
show tag
tag
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg1 -> String
forall a. Show a => a -> String
show Term arg1
arg1
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg2 -> String
forall a. Show a => a -> String
show Term arg2
arg2
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg3="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg3 -> String
forall a. Show a => a -> String
show Term arg3
arg3
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (NotTerm Int
i Term Bool
arg) = String
"Not{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (OrTerm Int
i Term Bool
arg1 Term Bool
arg2) = String
"Or{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (AndTerm Int
i Term Bool
arg1 Term Bool
arg2) = String
"And{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (EqvTerm Int
i Term t
arg1 Term t
arg2) = String
"Eqv{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ITETerm Int
i Term Bool
cond Term ty
l Term ty
r) =
    String
"ITE{id="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", cond="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
cond
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", then="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
l
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", else="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
r
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (AddNumTerm Int
i Term ty
arg1 Term ty
arg2) = String
"AddNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (UMinusNumTerm Int
i Term ty
arg) = String
"UMinusNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (TimesNumTerm Int
i Term ty
arg1 Term ty
arg2) = String
"TimesNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (AbsNumTerm Int
i Term ty
arg) = String
"AbsNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (SignumNumTerm Int
i Term ty
arg) = String
"SignumNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (LTNumTerm Int
i Term t
arg1 Term t
arg2) = String
"LTNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (LENumTerm Int
i Term t
arg1 Term t
arg2) = String
"LENum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (AndBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"AndBits{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (OrBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"OrBits{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (XorBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"XorBits{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ComplementBitsTerm Int
i Term ty
arg) = String
"ComplementBits{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ShiftBitsTerm Int
i Term ty
arg Int
n) = String
"ShiftBits{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", n=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (RotateBitsTerm Int
i Term ty
arg Int
n) = String
"RotateBits{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", n=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (BVConcatTerm Int
i Term (bv a)
arg1 Term (bv b)
arg2) = String
"BVConcat{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (bv a) -> String
forall a. Show a => a -> String
show Term (bv a)
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (bv b) -> String
forall a. Show a => a -> String
show Term (bv b)
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (BVSelectTerm Int
i TypeRep ix
ix TypeRep w
w Term (bv a)
arg) =
    String
"BVSelect{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", ix=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep ix -> String
forall a. Show a => a -> String
show TypeRep ix
ix String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", w=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep w -> String
forall a. Show a => a -> String
show TypeRep w
w String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (bv a) -> String
forall a. Show a => a -> String
show Term (bv a)
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (BVExtendTerm Int
i Bool
signed TypeRep n
n Term (bv a)
arg) =
    String
"BVExtend{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", signed=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show Bool
signed String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", n=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep n -> String
forall a. Show a => a -> String
show TypeRep n
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (bv a) -> String
forall a. Show a => a -> String
show Term (bv a)
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (TabularFunApplyTerm Int
i Term (a =-> ty)
func Term a
arg) =
    String
"TabularFunApply{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", func=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (a =-> ty) -> String
forall a. Show a => a -> String
show Term (a =-> ty)
func String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term a -> String
forall a. Show a => a -> String
show Term a
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (GeneralFunApplyTerm Int
i Term (a --> ty)
func Term a
arg) =
    String
"GeneralFunApply{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", func=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (a --> ty) -> String
forall a. Show a => a -> String
show Term (a --> ty)
func String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term a -> String
forall a. Show a => a -> String
show Term a
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (DivIntegerTerm Int
i Term Integer
arg1 Term Integer
arg2) =
    String
"DivInteger{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Integer -> String
forall a. Show a => a -> String
show Term Integer
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Integer -> String
forall a. Show a => a -> String
show Term Integer
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ModIntegerTerm Int
i Term Integer
arg1 Term Integer
arg2) =
    String
"ModInteger{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Integer -> String
forall a. Show a => a -> String
show Term Integer
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Integer -> String
forall a. Show a => a -> String
show Term Integer
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"

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

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

data UTerm t where
  UConTerm :: (SupportedPrim t) => !t -> UTerm t
  USymTerm :: (SupportedPrim t) => !(TypedSymbol t) -> UTerm t
  UUnaryTerm :: (UnaryOp tag arg t) => !tag -> !(Term arg) -> UTerm t
  UBinaryTerm ::
    (BinaryOp tag arg1 arg2 t) =>
    !tag ->
    !(Term arg1) ->
    !(Term arg2) ->
    UTerm t
  UTernaryTerm ::
    (TernaryOp tag arg1 arg2 arg3 t) =>
    !tag ->
    !(Term arg1) ->
    !(Term arg2) ->
    !(Term arg3) ->
    UTerm t
  UNotTerm :: !(Term Bool) -> UTerm Bool
  UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
  UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
  UEqvTerm :: SupportedPrim t => !(Term t) -> !(Term t) -> UTerm Bool
  UITETerm :: SupportedPrim t => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t
  UAddNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
  UUMinusNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
  UTimesNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
  UAbsNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
  USignumNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
  ULTNumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool
  ULENumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool
  UAndBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
  UOrBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
  UXorBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
  UComplementBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> UTerm t
  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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i2 Bool -> Bool -> Bool
&& TypeRep a -> TypeRep b -> Bool
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep a
a TypeRep b
b
{-# INLINE eqTypedId #-}

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

instance (SupportedPrim t) => Interned (Term t) where
  type Uninterned (Term t) = UTerm t
  data Description (Term t) where
    DConTerm :: t -> Description (Term t)
    DSymTerm :: TypedSymbol t -> Description (Term t)
    DUnaryTerm ::
      (Eq tag, Hashable tag) =>
      {-# UNPACK #-} !(TypeRep tag, tag) ->
      {-# UNPACK #-} !(TypeRep arg, Id) ->
      Description (Term t)
    DBinaryTerm ::
      (Eq tag, Hashable tag) =>
      {-# UNPACK #-} !(TypeRep tag, tag) ->
      {-# UNPACK #-} !(TypeRep arg1, Id) ->
      {-# UNPACK #-} !(TypeRep arg2, Id) ->
      Description (Term t)
    DTernaryTerm ::
      (Eq tag, Hashable tag) =>
      {-# UNPACK #-} !(TypeRep tag, tag) ->
      {-# UNPACK #-} !(TypeRep arg1, Id) ->
      {-# UNPACK #-} !(TypeRep arg2, Id) ->
      {-# UNPACK #-} !(TypeRep arg3, Id) ->
      Description (Term t)
    DNotTerm :: {-# UNPACK #-} !Id -> Description (Term Bool)
    DOrTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
    DAndTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
    DEqvTerm :: TypeRep args -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
    DITETerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DAddNumTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DUMinusNumTerm :: {-# UNPACK #-} !Id -> Description (Term t)
    DTimesNumTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DAbsNumTerm :: {-# UNPACK #-} !Id -> Description (Term t)
    DSignumNumTerm :: {-# UNPACK #-} !Id -> Description (Term t)
    DLTNumTerm :: TypeRep args -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
    DLENumTerm :: TypeRep args -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
    DAndBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DOrBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DXorBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DComplementBitsTerm :: {-# UNPACK #-} !Id -> Description (Term t)
    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) = t -> Description (Term t)
forall t. t -> Description (Term t)
DConTerm t
v
  describe ((USymTerm TypedSymbol t
name) :: UTerm t) = forall t. TypedSymbol t -> Description (Term t)
DSymTerm @t TypedSymbol t
name
  describe ((UUnaryTerm (tag
tag :: tagt) (Term arg
tm :: Term arg)) :: UTerm t) =
    (TypeRep tag, tag) -> (TypeRep arg, Int) -> Description (Term t)
forall a a t.
(Eq a, Hashable a) =>
(TypeRep a, a) -> (TypeRep a, Int) -> Description (Term t)
DUnaryTerm (TypeRep tag
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag) (TypeRep arg
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, Term arg -> Int
forall t. Term t -> Int
identity Term arg
tm)
  describe ((UBinaryTerm (tag
tag :: tagt) (Term arg1
tm1 :: Term arg1) (Term arg2
tm2 :: Term arg2)) :: UTerm t) =
    forall a a b t.
(Eq a, Hashable a) =>
(TypeRep a, a)
-> (TypeRep a, Int) -> (TypeRep b, Int) -> Description (Term t)
DBinaryTerm @tagt @arg1 @arg2 @t (TypeRep tag
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag) (TypeRep arg1
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, Term arg1 -> Int
forall t. Term t -> Int
identity Term arg1
tm1) (TypeRep arg2
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, Term arg2 -> Int
forall t. Term t -> Int
identity Term arg2
tm2)
  describe ((UTernaryTerm (tag
tag :: tagt) (Term arg1
tm1 :: Term arg1) (Term arg2
tm2 :: Term arg2) (Term arg3
tm3 :: Term arg3)) :: UTerm t) =
    forall a 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
      (TypeRep tag
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag)
      (TypeRep arg1
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, Term arg1 -> Int
forall t. Term t -> Int
identity Term arg1
tm1)
      (TypeRep arg2
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, Term arg2 -> Int
forall t. Term t -> Int
identity Term arg2
tm2)
      (TypeRep arg3
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, Term arg3 -> Int
forall t. Term t -> Int
identity Term arg3
tm3)
  describe (UNotTerm Term Bool
arg) = Int -> Description (Term Bool)
DNotTerm (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
arg)
  describe (UOrTerm Term Bool
arg1 Term Bool
arg2) = Int -> Int -> Description (Term Bool)
DOrTerm (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
arg1) (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
arg2)
  describe (UAndTerm Term Bool
arg1 Term Bool
arg2) = Int -> Int -> Description (Term Bool)
DAndTerm (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
arg1) (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
arg2)
  describe (UEqvTerm (Term t
arg1 :: Term arg) Term t
arg2) = TypeRep t -> Int -> Int -> Description (Term Bool)
forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DEqvTerm (TypeRep t
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UITETerm Term Bool
cond (Term t
l :: Term arg) Term t
r) = Int -> Int -> Int -> Description (Term t)
forall t. Int -> Int -> Int -> Description (Term t)
DITETerm (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
cond) (Term t -> Int
forall t. Term t -> Int
identity Term t
l) (Term t -> Int
forall t. Term t -> Int
identity Term t
r)
  describe (UAddNumTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DAddNumTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UUMinusNumTerm Term t
arg) = Int -> Description (Term t)
forall t. Int -> Description (Term t)
DUMinusNumTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg)
  describe (UTimesNumTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DTimesNumTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UAbsNumTerm Term t
arg) = Int -> Description (Term t)
forall t. Int -> Description (Term t)
DAbsNumTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg)
  describe (USignumNumTerm Term t
arg) = Int -> Description (Term t)
forall t. Int -> Description (Term t)
DSignumNumTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg)
  describe (ULTNumTerm (Term t
arg1 :: arg) Term t
arg2) = TypeRep (Term t) -> Int -> Int -> Description (Term Bool)
forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DLTNumTerm (TypeRep (Term t)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (ULENumTerm (Term t
arg1 :: arg) Term t
arg2) = TypeRep (Term t) -> Int -> Int -> Description (Term Bool)
forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DLENumTerm (TypeRep (Term t)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UAndBitsTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DAndBitsTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UOrBitsTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DOrBitsTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UXorBitsTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DXorBitsTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UComplementBitsTerm Term t
arg) = Int -> Description (Term t)
forall t. Int -> Description (Term t)
DComplementBitsTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg)
  describe (UShiftBitsTerm Term t
arg Int
n) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DShiftBitsTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg) Int
n
  describe (URotateBitsTerm Term t
arg Int
n) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DRotateBitsTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg) Int
n
  describe (UBVConcatTerm (Term (bv a)
arg1 :: bv1) (Term (bv b)
arg2 :: bv2)) =
    TypeRep (Term (bv a))
-> TypeRep (Term (bv b)) -> Int -> Int -> Description (Term t)
forall a a t.
TypeRep a -> TypeRep a -> Int -> Int -> Description (Term t)
DBVConcatTerm (TypeRep (Term (bv a))
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv1) (TypeRep (Term (bv b))
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv2) (Term (bv a) -> Int
forall t. Term t -> Int
identity Term (bv a)
arg1) (Term (bv b) -> Int
forall t. Term t -> Int
identity Term (bv b)
arg2)
  describe (UBVSelectTerm (TypeRep ix
ix :: TypeRep ix) TypeRep w
_ (Term (bv a)
arg :: Term arg)) =
    TypeRep ix -> (TypeRep (bv a), Int) -> Description (Term (bv w))
forall (a :: Nat -> *) (a :: Nat) (b :: Nat) (n :: Nat).
TypeRep n -> (TypeRep (a a), Int) -> Description (Term (a b))
DBVSelectTerm TypeRep ix
ix (TypeRep (bv a)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, Term (bv a) -> Int
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)) =
    Bool
-> TypeRep n -> (TypeRep (bv a), Int) -> Description (Term (bv b))
forall (a :: Nat -> *) (a :: Nat) (b :: Nat) (n :: Nat).
Bool
-> TypeRep n -> (TypeRep (a a), Int) -> Description (Term (a b))
DBVExtendTerm Bool
signed TypeRep n
n (TypeRep (bv a)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, Term (bv a) -> Int
forall t. Term t -> Int
identity Term (bv a)
arg)
  describe (UTabularFunApplyTerm (Term (a =-> t)
func :: Term f) (Term a
arg :: Term a)) =
    (TypeRep (a =-> t), Int)
-> (TypeRep a, Int) -> Description (Term t)
forall a b.
(TypeRep (a =-> b), Int)
-> (TypeRep a, Int) -> Description (Term b)
DTabularFunApplyTerm (TypeRep (a =-> t)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep f, Term (a =-> t) -> Int
forall t. Term t -> Int
identity Term (a =-> t)
func) (TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep a, Term a -> Int
forall t. Term t -> Int
identity Term a
arg)
  describe (UGeneralFunApplyTerm (Term (a --> t)
func :: Term f) (Term a
arg :: Term a)) =
    (TypeRep (a --> t), Int)
-> (TypeRep a, Int) -> Description (Term t)
forall a b.
(TypeRep (a --> b), Int)
-> (TypeRep a, Int) -> Description (Term b)
DGeneralFunApplyTerm (TypeRep (a --> t)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep f, Term (a --> t) -> Int
forall t. Term t -> Int
identity Term (a --> t)
func) (TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep a, Term a -> Int
forall t. Term t -> Int
identity Term a
arg)
  describe (UDivIntegerTerm Term Integer
arg1 Term Integer
arg2) = Int -> Int -> Description (Term Integer)
DDivIntegerTerm (Term Integer -> Int
forall t. Term t -> Int
identity Term Integer
arg1) (Term Integer -> Int
forall t. Term t -> Int
identity Term Integer
arg2)
  describe (UModIntegerTerm Term Integer
arg1 Term Integer
arg2) = Int -> Int -> Description (Term Integer)
DModIntegerTerm (Term Integer -> Int
forall t. Term t -> Int
identity Term Integer
arg1) (Term Integer -> Int
forall t. Term t -> Int
identity Term Integer
arg2)
  identify :: Int -> Uninterned (Term t) -> Term t
identify Int
i = Uninterned (Term t) -> Term t
UTerm t -> Term t
go
    where
      go :: UTerm t -> Term t
go (UConTerm t
v) = Int -> t -> Term t
forall t. SupportedPrim t => Int -> t -> Term t
ConTerm Int
i t
v
      go (USymTerm TypedSymbol t
v) = Int -> TypedSymbol t -> Term t
forall t. SupportedPrim t => Int -> TypedSymbol t -> Term t
SymTerm Int
i TypedSymbol t
v
      go (UUnaryTerm tag
tag Term arg
tm) = Int -> tag -> Term arg -> Term t
forall a 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) = Int -> tag -> Term arg1 -> Term arg2 -> Term t
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) = Int -> tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
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) = Int -> Term t -> Term t -> Term Bool
forall a. SupportedPrim a => Int -> Term a -> Term a -> Term Bool
EqvTerm Int
i Term t
arg1 Term t
arg2
      go (UITETerm Term Bool
cond Term t
l Term t
r) = Int -> Term Bool -> Term t -> Term t -> Term t
forall t.
SupportedPrim t =>
Int -> Term Bool -> Term t -> Term t -> Term t
ITETerm Int
i Term Bool
cond Term t
l Term t
r
      go (UAddNumTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Num t) =>
Int -> Term t -> Term t -> Term t
AddNumTerm Int
i Term t
arg1 Term t
arg2
      go (UUMinusNumTerm Term t
arg) = Int -> Term t -> Term t
forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
UMinusNumTerm Int
i Term t
arg
      go (UTimesNumTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Num t) =>
Int -> Term t -> Term t -> Term t
TimesNumTerm Int
i Term t
arg1 Term t
arg2
      go (UAbsNumTerm Term t
arg) = Int -> Term t -> Term t
forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
AbsNumTerm Int
i Term t
arg
      go (USignumNumTerm Term t
arg) = Int -> Term t -> Term t
forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
SignumNumTerm Int
i Term t
arg
      go (ULTNumTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term Bool
forall a.
(SupportedPrim a, Num a, Ord a) =>
Int -> Term a -> Term a -> Term Bool
LTNumTerm Int
i Term t
arg1 Term t
arg2
      go (ULENumTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term Bool
forall a.
(SupportedPrim a, Num a, Ord a) =>
Int -> Term a -> Term a -> Term Bool
LENumTerm Int
i Term t
arg1 Term t
arg2
      go (UAndBitsTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Term t -> Term t
AndBitsTerm Int
i Term t
arg1 Term t
arg2
      go (UOrBitsTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Term t -> Term t
OrBitsTerm Int
i Term t
arg1 Term t
arg2
      go (UXorBitsTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Term t -> Term t
XorBitsTerm Int
i Term t
arg1 Term t
arg2
      go (UComplementBitsTerm Term t
arg) = Int -> Term t -> Term t
forall t. (SupportedPrim t, Bits t) => Int -> Term t -> Term t
ComplementBitsTerm Int
i Term t
arg
      go (UShiftBitsTerm Term t
arg Int
n) = Int -> Term t -> Int -> Term t
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) = Int -> Term t -> Int -> Term t
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) = Int -> Term (bv a) -> Term (bv b) -> Term (bv c)
forall (a :: Nat -> *) (a :: Nat) (b :: Nat) (n :: Nat).
(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) = Int -> TypeRep ix -> TypeRep w -> Term (bv a) -> Term (bv w)
forall (a :: Nat -> *) (a :: Nat) (b :: Nat) (n :: Nat).
(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) = Int -> Bool -> TypeRep n -> Term (bv a) -> Term (bv b)
forall (a :: Nat -> *) (a :: Nat) (b :: Nat) (n :: Nat).
(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) = Int -> Term (a =-> t) -> Term a -> Term t
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Int -> Term (a =-> b) -> Term a -> Term b
TabularFunApplyTerm Int
i Term (a =-> t)
func Term a
arg
      go (UGeneralFunApplyTerm Term (a --> t)
func Term a
arg) = Int -> Term (a --> t) -> Term a -> Term t
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Int -> Term (a --> b) -> Term a -> Term b
GeneralFunApplyTerm Int
i Term (a --> t)
func Term a
arg
      go (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 = Cache (Term t)
forall t. SupportedPrim t => Cache (Term t)
termCache

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

instance (SupportedPrim t) => Hashable (Description (Term t)) where
  hashWithSalt :: Int -> Description (Term t) -> Int
hashWithSalt Int
s (DConTerm t
c) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int) Int -> t -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` t
c
  hashWithSalt Int
s (DSymTerm TypedSymbol t
name) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1 :: Int) Int -> TypedSymbol t -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol t
name
  hashWithSalt Int
s (DUnaryTerm (TypeRep tag, tag)
tag (TypeRep arg, Int)
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
2 :: Int) Int -> (TypeRep tag, tag) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag Int -> (TypeRep arg, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg, Int)
id1
  hashWithSalt Int
s (DBinaryTerm (TypeRep tag, tag)
tag (TypeRep arg1, Int)
id1 (TypeRep arg2, Int)
id2) =
    Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
3 :: Int) Int -> (TypeRep tag, tag) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag Int -> (TypeRep arg1, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg1, Int)
id1 Int -> (TypeRep arg2, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg2, Int)
id2
  hashWithSalt Int
s (DTernaryTerm (TypeRep tag, tag)
tag (TypeRep arg1, Int)
id1 (TypeRep arg2, Int)
id2 (TypeRep arg3, Int)
id3) =
    Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
4 :: Int) Int -> (TypeRep tag, tag) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag Int -> (TypeRep arg1, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg1, Int)
id1 Int -> (TypeRep arg2, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg2, Int)
id2 Int -> (TypeRep arg3, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg3, Int)
id3
  hashWithSalt Int
s (DNotTerm Int
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
5 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
  hashWithSalt Int
s (DOrTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
6 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DAndTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
7 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DEqvTerm TypeRep args
rep Int
id1 Int
id2) =
    Int
s
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
8 :: Int)
      Int -> TypeRep args -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DITETerm Int
idc Int
id1 Int
id2) =
    Int
s
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
9 :: Int)
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
idc
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DAddNumTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
10 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DUMinusNumTerm Int
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
11 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
  hashWithSalt Int
s (DTimesNumTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
12 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DAbsNumTerm Int
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
13 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
  hashWithSalt Int
s (DSignumNumTerm Int
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
14 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
  hashWithSalt Int
s (DLTNumTerm TypeRep args
rep Int
id1 Int
id2) =
    Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
15 :: Int) Int -> TypeRep args -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DLENumTerm TypeRep args
rep Int
id1 Int
id2) =
    Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
16 :: Int) Int -> TypeRep args -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DAndBitsTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
17 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DOrBitsTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
18 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DXorBitsTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
19 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DComplementBitsTerm Int
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
20 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
  hashWithSalt Int
s (DShiftBitsTerm Int
id1 Int
n) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
21 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
n
  hashWithSalt Int
s (DRotateBitsTerm Int
id1 Int
n) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
22 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
n
  hashWithSalt Int
s (DBVConcatTerm TypeRep bv1
rep1 TypeRep bv2
rep2 Int
id1 Int
id2) =
    Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
23 :: Int) Int -> TypeRep bv1 -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep bv1
rep1 Int -> TypeRep bv2 -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep bv2
rep2 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DBVSelectTerm TypeRep ix
ix (TypeRep (bv a), Int)
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
24 :: Int) Int -> TypeRep ix -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep ix
ix Int -> (TypeRep (bv a), Int) -> Int
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
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
25 :: Int)
      Int -> Bool -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Bool
signed
      Int -> TypeRep n -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep n
n
      Int -> (TypeRep (bv a), Int) -> Int
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 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
26 :: Int) Int -> (TypeRep (a =-> t), Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (a =-> t), Int)
id1 Int -> (TypeRep a, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep a, Int)
id2
  hashWithSalt Int
s (DGeneralFunApplyTerm (TypeRep (a --> t), Int)
id1 (TypeRep a, Int)
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
27 :: Int) Int -> (TypeRep (a --> t), Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (a --> t), Int)
id1 Int -> (TypeRep a, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep a, Int)
id2
  hashWithSalt Int
s (DDivIntegerTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
28 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DModIntegerTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
29 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2

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

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

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

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

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

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

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

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

data FunArg = FunArg deriving (Int -> FunArg -> ShowS
[FunArg] -> ShowS
FunArg -> String
(Int -> FunArg -> ShowS)
-> (FunArg -> String) -> ([FunArg] -> ShowS) -> Show FunArg
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
(FunArg -> FunArg -> Bool)
-> (FunArg -> FunArg -> Bool) -> Eq FunArg
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. FunArg -> Rep FunArg x)
-> (forall x. Rep FunArg x -> FunArg) -> Generic FunArg
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
Eq FunArg
-> (FunArg -> FunArg -> Ordering)
-> (FunArg -> FunArg -> Bool)
-> (FunArg -> FunArg -> Bool)
-> (FunArg -> FunArg -> Bool)
-> (FunArg -> FunArg -> Bool)
-> (FunArg -> FunArg -> FunArg)
-> (FunArg -> FunArg -> FunArg)
-> Ord 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 (m :: * -> *). Quote m => FunArg -> m Exp)
-> (forall (m :: * -> *). Quote m => FunArg -> Code m FunArg)
-> Lift FunArg
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, Int -> FunArg -> Int
FunArg -> Int
(Int -> FunArg -> Int) -> (FunArg -> Int) -> Hashable FunArg
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: FunArg -> Int
$chash :: FunArg -> Int
hashWithSalt :: Int -> FunArg -> Int
$chashWithSalt :: Int -> FunArg -> Int
Hashable, FunArg -> ()
(FunArg -> ()) -> NFData FunArg
forall a. (a -> ()) -> NFData a
rnf :: FunArg -> ()
$crnf :: FunArg -> ()
NFData)

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

infixr 0 -->

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

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

instance Lift (a --> b) where
  liftTyped :: forall (m :: * -> *). Quote m => (a --> b) -> Code m (a --> b)
liftTyped (GeneralFun TypedSymbol a
sym Term b
tm) = [||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 Int -> TypedSymbol a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol a
sym Int -> Term b -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Term b
tm

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

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