{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
-- 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 (..),
    SymRep (..),
    ConRep (..),
    LinkedRep (..),
    UnaryOp (..),
    BinaryOp (..),
    TernaryOp (..),
    TypedSymbol (..),
    SomeTypedSymbol (..),
    showUntyped,
    withSymbolSupported,
    someTypedSymbol,
    Term (..),
    UTerm (..),
    type (-->) (..),
    buildGeneralFun,
    prettyPrintTerm,
  )
where

import Control.DeepSeq (NFData (rnf))
import Data.Bits (Bits, FiniteBits)
import Data.Function (on)
import Data.Hashable (Hashable (hashWithSalt))
import Data.Interned
  ( Cache,
    Id,
    Interned (Description, Uninterned, cache, describe, identify),
  )
import Data.Kind (Constraint)
import Data.String (IsString (fromString))
import qualified Data.Text as T
import Data.Typeable (Proxy (Proxy), cast)
import GHC.Generics (Generic)
import GHC.TypeNats (KnownNat, Nat, type (+), type (<=))
import Grisette.Core.Data.BV (IntN, WordN)
import Grisette.Core.Data.Class.BitVector
  ( SizedBV,
  )
import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#)))
import Grisette.Core.Data.Class.SignConversion (SignConversion)
import Grisette.Core.Data.Class.SymRotate (SymRotate)
import Grisette.Core.Data.Class.SymShift (SymShift)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches
  ( typeMemoizedCache,
  )
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
  ( absNumTerm,
    addNumTerm,
    andBitsTerm,
    andTerm,
    bvconcatTerm,
    bvextendTerm,
    bvselectTerm,
    complementBitsTerm,
    conTerm,
    constructBinary,
    constructTernary,
    constructUnary,
    divBoundedIntegralTerm,
    divIntegralTerm,
    eqvTerm,
    generalFunApplyTerm,
    iteTerm,
    leNumTerm,
    ltNumTerm,
    modBoundedIntegralTerm,
    modIntegralTerm,
    notTerm,
    orBitsTerm,
    orTerm,
    quotBoundedIntegralTerm,
    quotIntegralTerm,
    remBoundedIntegralTerm,
    remIntegralTerm,
    rotateLeftTerm,
    rotateRightTerm,
    shiftLeftTerm,
    shiftRightTerm,
    signumNumTerm,
    symTerm,
    tabularFunApplyTerm,
    timesNumTerm,
    toSignedTerm,
    toUnsignedTerm,
    uminusNumTerm,
    xorBitsTerm,
  )
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
  ( substTerm,
  )
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
  ( identity,
    introSupportedPrimConstraint,
    pformat,
  )
import Grisette.IR.SymPrim.Data.Prim.ModelValue
  ( ModelValue,
    toModelValue,
  )
import Grisette.IR.SymPrim.Data.Prim.Utils
  ( eqHeteroRep,
    eqTypeRepBool,
  )
import Grisette.IR.SymPrim.Data.TabularFun
  ( type (=->) (TabularFun),
  )
import Language.Haskell.TH.Syntax (Lift (lift, liftTyped))
import Language.Haskell.TH.Syntax.Compat (unTypeSplice)
import Type.Reflection
  ( SomeTypeRep (SomeTypeRep),
    TypeRep,
    Typeable,
    eqTypeRep,
    typeRep,
    type (:~~:) (HRefl),
  )

#if MIN_VERSION_prettyprinter(1,7,0)
import Prettyprinter
  ( column,
    pageWidth,
    Doc,
    PageWidth(Unbounded, AvailablePerLine),
    Pretty(pretty),
  )
#else
import Data.Text.Prettyprint.Doc
  ( column,
    pageWidth,
    Doc,
    PageWidth(Unbounded, AvailablePerLine),
    Pretty(pretty),
  )
#endif

-- $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 _ = ()
  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)

-- | Type family to resolve the concrete type associated with a symbolic type.
class ConRep sym where
  type ConType sym

-- | Type family to resolve the symbolic type associated with a concrete type.
class (SupportedPrim con) => SymRep con where
  type SymType con

-- | One-to-one mapping between symbolic types and concrete types.
class
  (ConRep sym, SymRep con, sym ~ SymType con, con ~ ConType sym) =>
  LinkedRep con sym
    | con -> sym,
      sym -> con
  where
  underlyingTerm :: sym -> Term con
  wrapTerm :: Term con -> sym

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

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

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

-- | 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) => T.Text -> TypedSymbol t
  IndexedSymbol :: (SupportedPrim t) => T.Text -> Int -> TypedSymbol t
  WithInfo ::
    forall t a.
    ( SupportedPrim t,
      Typeable a,
      Ord a,
      Lift a,
      NFData a,
      Show a,
      Hashable a
    ) =>
    TypedSymbol t ->
    a ->
    TypedSymbol t

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

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

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

instance Lift (TypedSymbol t) where
  liftTyped :: forall (m :: * -> *).
Quote m =>
TypedSymbol t -> Code m (TypedSymbol t)
liftTyped (SimpleSymbol Text
x) = [||Text -> TypedSymbol t
forall t. SupportedPrim t => Text -> TypedSymbol t
SimpleSymbol Text
x||]
  liftTyped (IndexedSymbol Text
x Int
i) = [||Text -> Int -> TypedSymbol t
forall t. SupportedPrim t => Text -> Int -> TypedSymbol t
IndexedSymbol Text
x Int
i||]
  liftTyped (WithInfo TypedSymbol t
s1 a
i1) = [||TypedSymbol t -> a -> TypedSymbol t
forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
 Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo TypedSymbol t
s1 a
i1||]

instance Show (TypedSymbol t) where
  show :: TypedSymbol t -> String
show (SimpleSymbol Text
str) = Text -> String
T.unpack Text
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep t -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t)
  show (IndexedSymbol Text
str Int
i) = Text -> String
T.unpack Text
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep t -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t)
  show (WithInfo TypedSymbol t
s a
info) = TypedSymbol t -> String
forall t. TypedSymbol t -> String
showUntyped TypedSymbol t
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
info String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep t -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t)

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

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

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

instance (SupportedPrim t) => IsString (TypedSymbol t) where
  fromString :: String -> TypedSymbol t
fromString = Text -> TypedSymbol t
forall t. SupportedPrim t => Text -> TypedSymbol t
SimpleSymbol (Text -> TypedSymbol t)
-> (String -> Text) -> String -> TypedSymbol t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack

withSymbolSupported :: TypedSymbol t -> ((SupportedPrim t) => a) -> a
withSymbolSupported :: forall t a. TypedSymbol t -> (SupportedPrim t => a) -> a
withSymbolSupported (SimpleSymbol Text
_) SupportedPrim t => a
a = a
SupportedPrim t => a
a
withSymbolSupported (IndexedSymbol Text
_ Int
_) SupportedPrim t => a
a = a
SupportedPrim t => a
a
withSymbolSupported (WithInfo TypedSymbol t
_ a
_) SupportedPrim t => a
a = a
SupportedPrim t => a
a

{-
data 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) () -> () -> ()
forall a b. a -> b -> b
`seq` TypedSymbol t -> ()
forall a. NFData a => a -> ()
rnf TypedSymbol t
s

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

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

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

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

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

data Term t where
  ConTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !t -> Term t
  SymTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(TypedSymbol t) -> Term t
  UnaryTerm ::
    (UnaryOp tag arg t) =>
    {-# UNPACK #-} !Id ->
    !tag ->
    !(Term arg) ->
    Term t
  BinaryTerm ::
    (BinaryOp tag arg1 arg2 t) =>
    {-# UNPACK #-} !Id ->
    !tag ->
    !(Term arg1) ->
    !(Term arg2) ->
    Term t
  TernaryTerm ::
    (TernaryOp tag arg1 arg2 arg3 t) =>
    {-# UNPACK #-} !Id ->
    !tag ->
    !(Term arg1) ->
    !(Term arg2) ->
    !(Term arg3) ->
    Term t
  NotTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> Term Bool
  OrTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
  AndTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
  EqvTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
  ITETerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t
  AddNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  UMinusNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
  TimesNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  AbsNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
  SignumNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
  LTNumTerm :: (SupportedPrim t, Num t, Ord t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
  LENumTerm :: (SupportedPrim t, Num t, Ord t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
  AndBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  OrBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  XorBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  ComplementBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
  ShiftLeftTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymShift t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  ShiftRightTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymShift t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  RotateLeftTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymRotate t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  RotateRightTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymRotate t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  ToSignedTerm ::
    ( SupportedPrim u,
      SupportedPrim s,
      SignConversion u s
    ) =>
    {-# UNPACK #-} !Id ->
    !(Term u) ->
    Term s
  ToUnsignedTerm ::
    ( SupportedPrim u,
      SupportedPrim s,
      SignConversion u s
    ) =>
    {-# UNPACK #-} !Id ->
    !(Term s) ->
    Term u
  BVConcatTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
      Typeable bv,
      KnownNat a,
      KnownNat b,
      KnownNat (a + b),
      1 <= a,
      1 <= b,
      1 <= a + b,
      SizedBV bv
    ) =>
    {-# UNPACK #-} !Id ->
    !(Term (bv a)) ->
    !(Term (bv b)) ->
    Term (bv (a + b))
  BVSelectTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
      Typeable bv,
      KnownNat n,
      KnownNat ix,
      KnownNat w,
      1 <= n,
      1 <= w,
      ix + w <= n,
      SizedBV bv
    ) =>
    {-# UNPACK #-} !Id ->
    !(TypeRep ix) ->
    !(TypeRep w) ->
    !(Term (bv n)) ->
    Term (bv w)
  BVExtendTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
      Typeable bv,
      KnownNat l,
      KnownNat r,
      1 <= l,
      1 <= r,
      l <= r,
      SizedBV bv
    ) =>
    {-# UNPACK #-} !Id ->
    !Bool ->
    !(TypeRep r) ->
    !(Term (bv l)) ->
    Term (bv r)
  TabularFunApplyTerm ::
    ( SupportedPrim a,
      SupportedPrim b
    ) =>
    {-# UNPACK #-} !Id ->
    Term (a =-> b) ->
    Term a ->
    Term b
  GeneralFunApplyTerm ::
    ( SupportedPrim a,
      SupportedPrim b
    ) =>
    {-# UNPACK #-} !Id ->
    Term (a --> b) ->
    Term a ->
    Term b
  DivIntegralTerm :: (SupportedPrim t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  ModIntegralTerm :: (SupportedPrim t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  QuotIntegralTerm :: (SupportedPrim t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  RemIntegralTerm :: (SupportedPrim t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  DivBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  ModBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  QuotBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
  RemBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t

instance NFData (Term a) where
  rnf :: Term a -> ()
rnf Term a
i = Term a -> Int
forall t. Term t -> Int
identity Term a
i Int -> () -> ()
forall a b. a -> b -> b
`seq` ()

instance Lift (Term t) where
  lift :: forall (m :: * -> *). Quote m => Term t -> m Exp
lift = Splice m (Term t) -> m Exp
forall a (m :: * -> *). Quote m => Splice m a -> m Exp
unTypeSplice (Splice m (Term t) -> m Exp)
-> (Term t -> Splice m (Term t)) -> Term t -> m Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term t -> Splice m (Term t)
forall t (m :: * -> *). (Lift t, Quote m) => t -> Code m t
forall (m :: * -> *). Quote m => Term t -> Code m (Term t)
liftTyped
  liftTyped :: forall (m :: * -> *). Quote m => Term t -> Code m (Term t)
liftTyped (ConTerm Int
_ t
i) = [||t -> Term t
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm t
i||]
  liftTyped (SymTerm Int
_ TypedSymbol t
sym) = [||TypedSymbol t -> Term t
forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm TypedSymbol t
sym||]
  liftTyped (UnaryTerm Int
_ tag
tag Term arg
arg) = [||tag -> Term arg -> Term t
forall tag arg t.
(SupportedPrim t, UnaryOp tag arg t, Typeable tag, Typeable t,
 Show tag) =>
tag -> Term arg -> Term t
constructUnary tag
tag Term arg
arg||]
  liftTyped (BinaryTerm Int
_ tag
tag Term arg1
arg1 Term arg2
arg2) = [||tag -> Term arg1 -> Term arg2 -> Term t
forall tag arg1 arg2 t.
(SupportedPrim t, BinaryOp tag arg1 arg2 t, Typeable tag,
 Typeable t, Show tag) =>
tag -> Term arg1 -> Term arg2 -> Term t
constructBinary tag
tag Term arg1
arg1 Term arg2
arg2||]
  liftTyped (TernaryTerm Int
_ tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) = [||tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
forall tag arg1 arg2 arg3 t.
(SupportedPrim t, TernaryOp tag arg1 arg2 arg3 t, Typeable tag,
 Typeable t, Show tag) =>
tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
constructTernary tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3||]
  liftTyped (NotTerm Int
_ Term Bool
arg) = [||Term Bool -> Term Bool
notTerm Term Bool
arg||]
  liftTyped (OrTerm Int
_ Term Bool
arg1 Term Bool
arg2) = [||Term Bool -> Term Bool -> Term Bool
orTerm Term Bool
arg1 Term Bool
arg2||]
  liftTyped (AndTerm Int
_ Term Bool
arg1 Term Bool
arg2) = [||Term Bool -> Term Bool -> Term Bool
andTerm Term Bool
arg1 Term Bool
arg2||]
  liftTyped (EqvTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
eqvTerm Term t
arg1 Term t
arg2||]
  liftTyped (ITETerm Int
_ Term Bool
cond Term t
arg1 Term t
arg2) = [||Term Bool -> Term a -> Term a -> Term a
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
iteTerm Term Bool
cond Term t
arg1 Term t
arg2||]
  liftTyped (AddNumTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a. (SupportedPrim a, Num a) => Term a -> Term a -> Term a
addNumTerm Term t
arg1 Term t
arg2||]
  liftTyped (UMinusNumTerm Int
_ Term t
arg) = [||Term a -> Term a
forall a. (SupportedPrim a, Num a) => Term a -> Term a
uminusNumTerm Term t
arg||]
  liftTyped (TimesNumTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a. (SupportedPrim a, Num a) => Term a -> Term a -> Term a
timesNumTerm Term t
arg1 Term t
arg2||]
  liftTyped (AbsNumTerm Int
_ Term t
arg) = [||Term a -> Term a
forall a. (SupportedPrim a, Num a) => Term a -> Term a
absNumTerm Term t
arg||]
  liftTyped (SignumNumTerm Int
_ Term t
arg) = [||Term a -> Term a
forall a. (SupportedPrim a, Num a) => Term a -> Term a
signumNumTerm Term t
arg||]
  liftTyped (LTNumTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term Bool
forall a.
(SupportedPrim a, Num a, Ord a) =>
Term a -> Term a -> Term Bool
ltNumTerm Term t
arg1 Term t
arg2||]
  liftTyped (LENumTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term Bool
forall a.
(SupportedPrim a, Num a, Ord a) =>
Term a -> Term a -> Term Bool
leNumTerm Term t
arg1 Term t
arg2||]
  liftTyped (AndBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a. (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
andBitsTerm Term t
arg1 Term t
arg2||]
  liftTyped (OrBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a. (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
orBitsTerm Term t
arg1 Term t
arg2||]
  liftTyped (XorBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a. (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
xorBitsTerm Term t
arg1 Term t
arg2||]
  liftTyped (ComplementBitsTerm Int
_ Term t
arg) = [||Term a -> Term a
forall a. (SupportedPrim a, Bits a) => Term a -> Term a
complementBitsTerm Term t
arg||]
  liftTyped (ShiftLeftTerm Int
_ Term t
arg Term t
n) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymShift a) =>
Term a -> Term a -> Term a
shiftLeftTerm Term t
arg Term t
n||]
  liftTyped (ShiftRightTerm Int
_ Term t
arg Term t
n) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymShift a) =>
Term a -> Term a -> Term a
shiftRightTerm Term t
arg Term t
n||]
  liftTyped (RotateLeftTerm Int
_ Term t
arg Term t
n) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymRotate a) =>
Term a -> Term a -> Term a
rotateLeftTerm Term t
arg Term t
n||]
  liftTyped (RotateRightTerm Int
_ Term t
arg Term t
n) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymRotate a) =>
Term a -> Term a -> Term a
rotateRightTerm Term t
arg Term t
n||]
  liftTyped (ToSignedTerm Int
_ Term u
v) = [||Term u -> Term s
forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term u -> Term s
toSignedTerm Term u
v||]
  liftTyped (ToUnsignedTerm Int
_ Term s
v) = [||Term s -> Term u
forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term s -> Term u
toUnsignedTerm Term s
v||]
  liftTyped (BVConcatTerm Int
_ Term (bv a)
arg1 Term (bv b)
arg2) = [||Term (bv a) -> Term (bv b) -> Term (bv (a + b))
forall (bv :: Nat -> *) (a :: Nat) (b :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat a, KnownNat b, KnownNat (a + b), 1 <= a,
 1 <= b, 1 <= (a + b), SizedBV bv) =>
Term (bv a) -> Term (bv b) -> Term (bv (a + b))
bvconcatTerm Term (bv a)
arg1 Term (bv b)
arg2||]
  liftTyped (BVSelectTerm Int
_ (TypeRep ix
_ :: TypeRep ix) (TypeRep w
_ :: TypeRep w) Term (bv n)
arg) = [||p ix -> q w -> Term (bv n) -> Term (bv w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
       (p :: Nat -> *) (q :: Nat -> *).
(forall (n1 :: Nat).
 (KnownNat n1, 1 <= n1) =>
 SupportedPrim (bv n1),
 Typeable bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n, SizedBV bv) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
bvselectTerm (forall (t :: k). Proxy t
forall {k} (t :: k). Proxy t
Proxy @ix) (forall (t :: k). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) Term (bv n)
arg||]
  liftTyped (BVExtendTerm Int
_ Bool
signed (TypeRep r
_ :: TypeRep n) Term (bv l)
arg) = [||Bool -> proxy r -> Term (bv l) -> Term (bv r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
 SizedBV bv) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
bvextendTerm Bool
signed (forall (t :: k). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) Term (bv l)
arg||]
  liftTyped (TabularFunApplyTerm Int
_ Term (a =-> t)
func Term a
arg) = [||Term (a =-> b) -> Term a -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> Term a -> Term b
tabularFunApplyTerm Term (a =-> t)
func Term a
arg||]
  liftTyped (GeneralFunApplyTerm Int
_ Term (a --> t)
func Term a
arg) = [||Term (a --> b) -> Term a -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
generalFunApplyTerm Term (a --> t)
func Term a
arg||]
  liftTyped (DivIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
divIntegralTerm Term t
arg1 Term t
arg2||]
  liftTyped (ModIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
modIntegralTerm Term t
arg1 Term t
arg2||]
  liftTyped (QuotIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
quotIntegralTerm Term t
arg1 Term t
arg2||]
  liftTyped (RemIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
remIntegralTerm Term t
arg1 Term t
arg2||]
  liftTyped (DivBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
divBoundedIntegralTerm Term t
arg1 Term t
arg2||]
  liftTyped (ModBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
modBoundedIntegralTerm Term t
arg1 Term t
arg2||]
  liftTyped (QuotBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
quotBoundedIntegralTerm Term t
arg1 Term t
arg2||]
  liftTyped (RemBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
remBoundedIntegralTerm Term t
arg1 Term t
arg2||]

instance Show (Term ty) where
  show :: Term ty -> String
show (ConTerm Int
i ty
v) = String
"ConTerm{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", v=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ty -> String
forall a. Show a => a -> String
show ty
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (SymTerm Int
i TypedSymbol ty
name) =
    String
"SymTerm{id="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", name="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypedSymbol ty -> String
forall a. Show a => a -> String
show TypedSymbol ty
name
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", type="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep ty -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @ty)
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (UnaryTerm Int
i tag
tag Term arg
arg) = String
"Unary{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", tag=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ tag -> String
forall a. Show a => a -> String
show tag
tag String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg -> String
forall a. Show a => a -> String
show Term arg
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (BinaryTerm Int
i tag
tag Term arg1
arg1 Term arg2
arg2) =
    String
"Binary{id="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", tag="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ tag -> String
forall a. Show a => a -> String
show tag
tag
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg1 -> String
forall a. Show a => a -> String
show Term arg1
arg1
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg2 -> String
forall a. Show a => a -> String
show Term arg2
arg2
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (TernaryTerm Int
i tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) =
    String
"Ternary{id="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", tag="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ tag -> String
forall a. Show a => a -> String
show tag
tag
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg1 -> String
forall a. Show a => a -> String
show Term arg1
arg1
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg2 -> String
forall a. Show a => a -> String
show Term arg2
arg2
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg3="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term arg3 -> String
forall a. Show a => a -> String
show Term arg3
arg3
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (NotTerm Int
i Term Bool
arg) = String
"Not{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (OrTerm Int
i Term Bool
arg1 Term Bool
arg2) = String
"Or{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (AndTerm Int
i Term Bool
arg1 Term Bool
arg2) = String
"And{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (EqvTerm Int
i Term t
arg1 Term t
arg2) = String
"Eqv{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ITETerm Int
i Term Bool
cond Term ty
l Term ty
r) =
    String
"ITE{id="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", cond="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
cond
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", then="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
l
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", else="
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
r
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (AddNumTerm Int
i Term ty
arg1 Term ty
arg2) = String
"AddNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (UMinusNumTerm Int
i Term ty
arg) = String
"UMinusNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (TimesNumTerm Int
i Term ty
arg1 Term ty
arg2) = String
"TimesNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (AbsNumTerm Int
i Term ty
arg) = String
"AbsNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (SignumNumTerm Int
i Term ty
arg) = String
"SignumNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (LTNumTerm Int
i Term t
arg1 Term t
arg2) = String
"LTNum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (LENumTerm Int
i Term t
arg1 Term t
arg2) = String
"LENum{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall a. Show a => a -> String
show Term t
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (AndBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"AndBits{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (OrBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"OrBits{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (XorBitsTerm Int
i Term ty
arg1 Term ty
arg2) = String
"XorBits{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ComplementBitsTerm Int
i Term ty
arg) = String
"ComplementBits{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ShiftLeftTerm Int
i Term ty
arg Term ty
n) = String
"ShiftLeft{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", n=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ShiftRightTerm Int
i Term ty
arg Term ty
n) = String
"ShiftRight{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", n=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (RotateLeftTerm Int
i Term ty
arg Term ty
n) = String
"RotateLeft{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", n=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (RotateRightTerm Int
i Term ty
arg Term ty
n) = String
"RotateRight{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", n=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ToSignedTerm Int
i Term u
arg) = String
"ToSigned{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term u -> String
forall a. Show a => a -> String
show Term u
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ToUnsignedTerm Int
i Term s
arg) = String
"ToUnsigned{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term s -> String
forall a. Show a => a -> String
show Term s
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (BVConcatTerm Int
i Term (bv a)
arg1 Term (bv b)
arg2) = String
"BVConcat{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (bv a) -> String
forall a. Show a => a -> String
show Term (bv a)
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (bv b) -> String
forall a. Show a => a -> String
show Term (bv b)
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (BVSelectTerm Int
i TypeRep ix
ix TypeRep w
w Term (bv n)
arg) =
    String
"BVSelect{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", ix=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep ix -> String
forall a. Show a => a -> String
show TypeRep ix
ix String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", w=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep w -> String
forall a. Show a => a -> String
show TypeRep w
w String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (bv n) -> String
forall a. Show a => a -> String
show Term (bv n)
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (BVExtendTerm Int
i Bool
signed TypeRep r
n Term (bv l)
arg) =
    String
"BVExtend{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", signed=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show Bool
signed String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", n=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep r -> String
forall a. Show a => a -> String
show TypeRep r
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (bv l) -> String
forall a. Show a => a -> String
show Term (bv l)
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (TabularFunApplyTerm Int
i Term (a =-> ty)
func Term a
arg) =
    String
"TabularFunApply{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", func=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (a =-> ty) -> String
forall a. Show a => a -> String
show Term (a =-> ty)
func String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term a -> String
forall a. Show a => a -> String
show Term a
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (GeneralFunApplyTerm Int
i Term (a --> ty)
func Term a
arg) =
    String
"GeneralFunApply{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", func=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (a --> ty) -> String
forall a. Show a => a -> String
show Term (a --> ty)
func String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term a -> String
forall a. Show a => a -> String
show Term a
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (DivIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"DivIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ModIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"ModIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (QuotIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"QuotIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (RemIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"RemIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (DivBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"DivBoundedIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (ModBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"ModBoundedIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (QuotBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"QuotBoundedIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (RemBoundedIntegralTerm Int
i Term ty
arg1 Term ty
arg2) =
    String
"RemBoundedIntegral{id=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg1=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", arg2=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term ty -> String
forall a. Show a => a -> String
show Term ty
arg2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"

prettyPrintTerm :: Term t -> Doc ann
prettyPrintTerm :: forall t ann. Term t -> Doc ann
prettyPrintTerm Term t
v =
  (Int -> Doc ann) -> Doc ann
forall ann. (Int -> Doc ann) -> Doc ann
column
    ( \Int
c ->
        (PageWidth -> Doc ann) -> Doc ann
forall ann. (PageWidth -> Doc ann) -> Doc ann
pageWidth ((PageWidth -> Doc ann) -> Doc ann)
-> (PageWidth -> Doc ann) -> Doc ann
forall a b. (a -> b) -> a -> b
$ \case
          AvailablePerLine Int
i Double
r ->
            if Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
len) Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
r
              then Doc ann
"..."
              else String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
formatted
          PageWidth
Unbounded -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
formatted
    )
  where
    formatted :: String
formatted = Term t -> (SupportedPrim t => String) -> String
forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term t
v ((SupportedPrim t => String) -> String)
-> (SupportedPrim t => String) -> String
forall a b. (a -> b) -> a -> b
$ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
v
    len :: Int
len = String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
formatted

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

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

data UTerm t where
  UConTerm :: (SupportedPrim t) => !t -> UTerm t
  USymTerm :: (SupportedPrim t) => !(TypedSymbol t) -> UTerm t
  UUnaryTerm :: (UnaryOp tag arg t) => !tag -> !(Term arg) -> UTerm t
  UBinaryTerm ::
    (BinaryOp tag arg1 arg2 t) =>
    !tag ->
    !(Term arg1) ->
    !(Term arg2) ->
    UTerm t
  UTernaryTerm ::
    (TernaryOp tag arg1 arg2 arg3 t) =>
    !tag ->
    !(Term arg1) ->
    !(Term arg2) ->
    !(Term arg3) ->
    UTerm t
  UNotTerm :: !(Term Bool) -> UTerm Bool
  UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
  UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
  UEqvTerm :: (SupportedPrim t) => !(Term t) -> !(Term t) -> UTerm Bool
  UITETerm :: (SupportedPrim t) => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t
  UAddNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
  UUMinusNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
  UTimesNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
  UAbsNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
  USignumNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
  ULTNumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool
  ULENumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool
  UAndBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
  UOrBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
  UXorBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
  UComplementBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> UTerm t
  UShiftLeftTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymShift t) => !(Term t) -> !(Term t) -> UTerm t
  UShiftRightTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymShift t) => !(Term t) -> !(Term t) -> UTerm t
  URotateLeftTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymRotate t) => !(Term t) -> !(Term t) -> UTerm t
  URotateRightTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymRotate t) => !(Term t) -> !(Term t) -> UTerm t
  UToSignedTerm ::
    ( SupportedPrim u,
      SupportedPrim s,
      SignConversion u s
    ) =>
    !(Term u) ->
    UTerm s
  UToUnsignedTerm ::
    ( SupportedPrim u,
      SupportedPrim s,
      SignConversion u s
    ) =>
    !(Term s) ->
    UTerm u
  UBVConcatTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
      Typeable bv,
      KnownNat a,
      KnownNat b,
      KnownNat (a + b),
      1 <= a,
      1 <= b,
      1 <= a + b,
      SizedBV bv
    ) =>
    !(Term (bv a)) ->
    !(Term (bv b)) ->
    UTerm (bv (a + b))
  UBVSelectTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
      Typeable bv,
      KnownNat n,
      KnownNat ix,
      KnownNat w,
      1 <= n,
      1 <= w,
      ix + w <= n,
      SizedBV bv
    ) =>
    !(TypeRep ix) ->
    !(TypeRep w) ->
    !(Term (bv n)) ->
    UTerm (bv w)
  UBVExtendTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
      Typeable bv,
      KnownNat l,
      KnownNat r,
      1 <= l,
      1 <= r,
      l <= r,
      SizedBV bv
    ) =>
    !Bool ->
    !(TypeRep r) ->
    !(Term (bv l)) ->
    UTerm (bv r)
  UTabularFunApplyTerm ::
    ( SupportedPrim a,
      SupportedPrim b
    ) =>
    Term (a =-> b) ->
    Term a ->
    UTerm b
  UGeneralFunApplyTerm ::
    ( SupportedPrim a,
      SupportedPrim b
    ) =>
    Term (a --> b) ->
    Term a ->
    UTerm b
  UDivIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  UModIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  UQuotIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  URemIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  UDivBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  UModBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  UQuotBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  URemBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t

eqTypedId :: (TypeRep a, Id) -> (TypeRep b, Id) -> Bool
eqTypedId :: forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep a
a, Int
i1) (TypeRep b
b, Int
i2) = Int
i1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i2 Bool -> Bool -> Bool
&& TypeRep a -> TypeRep b -> Bool
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep a
a TypeRep b
b
{-# INLINE eqTypedId #-}

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

instance (SupportedPrim t) => Interned (Term t) where
  type Uninterned (Term t) = UTerm t
  data Description (Term t) where
    DConTerm :: t -> Description (Term t)
    DSymTerm :: TypedSymbol t -> Description (Term t)
    DUnaryTerm ::
      (Eq tag, Hashable tag) =>
      {-# UNPACK #-} !(TypeRep tag, tag) ->
      {-# UNPACK #-} !(TypeRep arg, Id) ->
      Description (Term t)
    DBinaryTerm ::
      (Eq tag, Hashable tag) =>
      {-# UNPACK #-} !(TypeRep tag, tag) ->
      {-# UNPACK #-} !(TypeRep arg1, Id) ->
      {-# UNPACK #-} !(TypeRep arg2, Id) ->
      Description (Term t)
    DTernaryTerm ::
      (Eq tag, Hashable tag) =>
      {-# UNPACK #-} !(TypeRep tag, tag) ->
      {-# UNPACK #-} !(TypeRep arg1, Id) ->
      {-# UNPACK #-} !(TypeRep arg2, Id) ->
      {-# UNPACK #-} !(TypeRep arg3, Id) ->
      Description (Term t)
    DNotTerm :: {-# UNPACK #-} !Id -> Description (Term Bool)
    DOrTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
    DAndTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
    DEqvTerm :: TypeRep args -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
    DITETerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DAddNumTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DUMinusNumTerm :: {-# UNPACK #-} !Id -> Description (Term t)
    DTimesNumTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DAbsNumTerm :: {-# UNPACK #-} !Id -> Description (Term t)
    DSignumNumTerm :: {-# UNPACK #-} !Id -> Description (Term t)
    DLTNumTerm :: TypeRep args -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
    DLENumTerm :: TypeRep args -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term Bool)
    DAndBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DOrBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DXorBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DComplementBitsTerm :: {-# UNPACK #-} !Id -> Description (Term t)
    DShiftLeftTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DShiftRightTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DRotateLeftTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DRotateRightTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DBVConcatTerm :: TypeRep bv1 -> TypeRep bv2 -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
    DToSignedTerm ::
      !(TypeRep u, Id) ->
      Description (Term s)
    DToUnsignedTerm ::
      !(TypeRep s, Id) ->
      Description (Term u)
    DBVSelectTerm ::
      forall bv (n :: Nat) (w :: Nat) (ix :: Nat).
      !(TypeRep ix) ->
      !(TypeRep (bv n), Id) ->
      Description (Term (bv w))
    DBVExtendTerm ::
      forall bv (l :: Nat) (r :: Nat).
      !Bool ->
      !(TypeRep r) ->
      {-# UNPACK #-} !(TypeRep (bv l), Id) ->
      Description (Term (bv r))
    DTabularFunApplyTerm ::
      {-# UNPACK #-} !(TypeRep (a =-> b), Id) ->
      {-# UNPACK #-} !(TypeRep a, Id) ->
      Description (Term b)
    DGeneralFunApplyTerm ::
      {-# UNPACK #-} !(TypeRep (a --> b), Id) ->
      {-# UNPACK #-} !(TypeRep a, Id) ->
      Description (Term b)
    DDivIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
    DModIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
    DQuotIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
    DRemIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
    DDivBoundedIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
    DModBoundedIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
    DQuotBoundedIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)
    DRemBoundedIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)

  describe :: Uninterned (Term t) -> Description (Term t)
describe (UConTerm t
v) = t -> Description (Term t)
forall t. t -> Description (Term t)
DConTerm t
v
  describe ((USymTerm TypedSymbol t
name) :: UTerm t) = forall t. TypedSymbol t -> Description (Term t)
DSymTerm @t TypedSymbol t
name
  describe ((UUnaryTerm (tag
tag :: tagt) (Term arg
tm :: Term arg)) :: UTerm t) =
    (TypeRep tag, tag) -> (TypeRep arg, Int) -> Description (Term t)
forall a l t.
(Eq a, Hashable a) =>
(TypeRep a, a) -> (TypeRep l, Int) -> Description (Term t)
DUnaryTerm (TypeRep tag
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag) (TypeRep arg
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, Term arg -> Int
forall t. Term t -> Int
identity Term arg
tm)
  describe ((UBinaryTerm (tag
tag :: tagt) (Term arg1
tm1 :: Term arg1) (Term arg2
tm2 :: Term arg2)) :: UTerm t) =
    forall a l r t.
(Eq a, Hashable a) =>
(TypeRep a, a)
-> (TypeRep l, Int) -> (TypeRep r, Int) -> Description (Term t)
DBinaryTerm @tagt @arg1 @arg2 @t (TypeRep tag
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag) (TypeRep arg1
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, Term arg1 -> Int
forall t. Term t -> Int
identity Term arg1
tm1) (TypeRep arg2
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, Term arg2 -> Int
forall t. Term t -> Int
identity Term arg2
tm2)
  describe ((UTernaryTerm (tag
tag :: tagt) (Term arg1
tm1 :: Term arg1) (Term arg2
tm2 :: Term arg2) (Term arg3
tm3 :: Term arg3)) :: UTerm t) =
    forall a l r w t.
(Eq a, Hashable a) =>
(TypeRep a, a)
-> (TypeRep l, Int)
-> (TypeRep r, Int)
-> (TypeRep w, Int)
-> Description (Term t)
DTernaryTerm @tagt @arg1 @arg2 @arg3 @t
      (TypeRep tag
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, tag
tag)
      (TypeRep arg1
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, Term arg1 -> Int
forall t. Term t -> Int
identity Term arg1
tm1)
      (TypeRep arg2
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, Term arg2 -> Int
forall t. Term t -> Int
identity Term arg2
tm2)
      (TypeRep arg3
forall {k} (a :: k). Typeable a => TypeRep a
typeRep, Term arg3 -> Int
forall t. Term t -> Int
identity Term arg3
tm3)
  describe (UNotTerm Term Bool
arg) = Int -> Description (Term Bool)
DNotTerm (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
arg)
  describe (UOrTerm Term Bool
arg1 Term Bool
arg2) = Int -> Int -> Description (Term Bool)
DOrTerm (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
arg1) (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
arg2)
  describe (UAndTerm Term Bool
arg1 Term Bool
arg2) = Int -> Int -> Description (Term Bool)
DAndTerm (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
arg1) (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
arg2)
  describe (UEqvTerm (Term t
arg1 :: Term arg) Term t
arg2) = TypeRep t -> Int -> Int -> Description (Term Bool)
forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DEqvTerm (TypeRep t
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UITETerm Term Bool
cond (Term t
l :: Term arg) Term t
r) = Int -> Int -> Int -> Description (Term t)
forall t. Int -> Int -> Int -> Description (Term t)
DITETerm (Term Bool -> Int
forall t. Term t -> Int
identity Term Bool
cond) (Term t -> Int
forall t. Term t -> Int
identity Term t
l) (Term t -> Int
forall t. Term t -> Int
identity Term t
r)
  describe (UAddNumTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DAddNumTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UUMinusNumTerm Term t
arg) = Int -> Description (Term t)
forall t. Int -> Description (Term t)
DUMinusNumTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg)
  describe (UTimesNumTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DTimesNumTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UAbsNumTerm Term t
arg) = Int -> Description (Term t)
forall t. Int -> Description (Term t)
DAbsNumTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg)
  describe (USignumNumTerm Term t
arg) = Int -> Description (Term t)
forall t. Int -> Description (Term t)
DSignumNumTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg)
  describe (ULTNumTerm (Term t
arg1 :: arg) Term t
arg2) = TypeRep (Term t) -> Int -> Int -> Description (Term Bool)
forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DLTNumTerm (TypeRep (Term t)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (ULENumTerm (Term t
arg1 :: arg) Term t
arg2) = TypeRep (Term t) -> Int -> Int -> Description (Term Bool)
forall a. TypeRep a -> Int -> Int -> Description (Term Bool)
DLENumTerm (TypeRep (Term t)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UAndBitsTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DAndBitsTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UOrBitsTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DOrBitsTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UXorBitsTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DXorBitsTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UComplementBitsTerm Term t
arg) = Int -> Description (Term t)
forall t. Int -> Description (Term t)
DComplementBitsTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg)
  describe (UShiftLeftTerm Term t
arg Term t
n) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DShiftLeftTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
n)
  describe (UShiftRightTerm Term t
arg Term t
n) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DShiftRightTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
n)
  describe (URotateLeftTerm Term t
arg Term t
n) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DRotateLeftTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
n)
  describe (URotateRightTerm Term t
arg Term t
n) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DRotateRightTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg) (Term t -> Int
forall t. Term t -> Int
identity Term t
n)
  describe (UToSignedTerm (Term u
arg :: Term bv)) = (TypeRep u, Int) -> Description (Term t)
forall a s. (TypeRep a, Int) -> Description (Term s)
DToSignedTerm (TypeRep u
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv, Term u -> Int
forall t. Term t -> Int
identity Term u
arg)
  describe (UToUnsignedTerm (Term s
arg :: Term bv)) = (TypeRep s, Int) -> Description (Term t)
forall a s. (TypeRep a, Int) -> Description (Term s)
DToSignedTerm (TypeRep s
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv, Term s -> Int
forall t. Term t -> Int
identity Term s
arg)
  describe (UBVConcatTerm (Term (bv a)
arg1 :: bv1) (Term (bv b)
arg2 :: bv2)) =
    TypeRep (Term (bv a))
-> TypeRep (Term (bv b)) -> Int -> Int -> Description (Term t)
forall a l t.
TypeRep a -> TypeRep l -> Int -> Int -> Description (Term t)
DBVConcatTerm (TypeRep (Term (bv a))
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv1) (TypeRep (Term (bv b))
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep bv2) (Term (bv a) -> Int
forall t. Term t -> Int
identity Term (bv a)
arg1) (Term (bv b) -> Int
forall t. Term t -> Int
identity Term (bv b)
arg2)
  describe (UBVSelectTerm (TypeRep ix
ix :: TypeRep ix) TypeRep w
_ (Term (bv n)
arg :: Term arg)) =
    TypeRep ix -> (TypeRep (bv n), Int) -> Description (Term (bv w))
forall (a :: Nat -> *) (l :: Nat) (r :: Nat) (w :: Nat).
TypeRep w -> (TypeRep (a l), Int) -> Description (Term (a r))
DBVSelectTerm TypeRep ix
ix (TypeRep (bv n)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, Term (bv n) -> Int
forall t. Term t -> Int
identity Term (bv n)
arg)
  describe (UBVExtendTerm Bool
signed (TypeRep r
n :: TypeRep n) (Term (bv l)
arg :: Term arg)) =
    Bool
-> TypeRep r -> (TypeRep (bv l), Int) -> Description (Term (bv r))
forall (a :: Nat -> *) (l :: Nat) (r :: Nat).
Bool
-> TypeRep r -> (TypeRep (a l), Int) -> Description (Term (a r))
DBVExtendTerm Bool
signed TypeRep r
n (TypeRep (bv l)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep arg, Term (bv l) -> Int
forall t. Term t -> Int
identity Term (bv l)
arg)
  describe (UTabularFunApplyTerm (Term (a =-> t)
func :: Term f) (Term a
arg :: Term a)) =
    (TypeRep (a =-> t), Int)
-> (TypeRep a, Int) -> Description (Term t)
forall a b.
(TypeRep (a =-> b), Int)
-> (TypeRep a, Int) -> Description (Term b)
DTabularFunApplyTerm (TypeRep (a =-> t)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep f, Term (a =-> t) -> Int
forall t. Term t -> Int
identity Term (a =-> t)
func) (TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep a, Term a -> Int
forall t. Term t -> Int
identity Term a
arg)
  describe (UGeneralFunApplyTerm (Term (a --> t)
func :: Term f) (Term a
arg :: Term a)) =
    (TypeRep (a --> t), Int)
-> (TypeRep a, Int) -> Description (Term t)
forall a b.
(TypeRep (a --> b), Int)
-> (TypeRep a, Int) -> Description (Term b)
DGeneralFunApplyTerm (TypeRep (a --> t)
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep f, Term (a --> t) -> Int
forall t. Term t -> Int
identity Term (a --> t)
func) (TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep a, Term a -> Int
forall t. Term t -> Int
identity Term a
arg)
  describe (UDivIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DDivIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UModIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DModIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UQuotIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DRemIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (URemIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DQuotIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UDivBoundedIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DDivBoundedIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UModBoundedIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DModBoundedIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (UQuotBoundedIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DRemBoundedIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)
  describe (URemBoundedIntegralTerm Term t
arg1 Term t
arg2) = Int -> Int -> Description (Term t)
forall t. Int -> Int -> Description (Term t)
DQuotBoundedIntegralTerm (Term t -> Int
forall t. Term t -> Int
identity Term t
arg1) (Term t -> Int
forall t. Term t -> Int
identity Term t
arg2)

  identify :: Int -> Uninterned (Term t) -> Term t
identify Int
i = Uninterned (Term t) -> Term t
UTerm t -> Term t
go
    where
      go :: UTerm t -> Term t
go (UConTerm t
v) = Int -> t -> Term t
forall t. SupportedPrim t => Int -> t -> Term t
ConTerm Int
i t
v
      go (USymTerm TypedSymbol t
v) = Int -> TypedSymbol t -> Term t
forall t. SupportedPrim t => Int -> TypedSymbol t -> Term t
SymTerm Int
i TypedSymbol t
v
      go (UUnaryTerm tag
tag Term arg
tm) = Int -> tag -> Term arg -> Term t
forall a l t. UnaryOp a l t => Int -> a -> Term l -> Term t
UnaryTerm Int
i tag
tag Term arg
tm
      go (UBinaryTerm tag
tag Term arg1
tm1 Term arg2
tm2) = Int -> tag -> Term arg1 -> Term arg2 -> Term t
forall a l r t.
BinaryOp a l r t =>
Int -> a -> Term l -> Term r -> Term t
BinaryTerm Int
i tag
tag Term arg1
tm1 Term arg2
tm2
      go (UTernaryTerm tag
tag Term arg1
tm1 Term arg2
tm2 Term arg3
tm3) = Int -> tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
forall a l r w t.
TernaryOp a l r w t =>
Int -> a -> Term l -> Term r -> Term w -> Term t
TernaryTerm Int
i tag
tag Term arg1
tm1 Term arg2
tm2 Term arg3
tm3
      go (UNotTerm Term Bool
arg) = Int -> Term Bool -> Term Bool
NotTerm Int
i Term Bool
arg
      go (UOrTerm Term Bool
arg1 Term Bool
arg2) = Int -> Term Bool -> Term Bool -> Term Bool
OrTerm Int
i Term Bool
arg1 Term Bool
arg2
      go (UAndTerm Term Bool
arg1 Term Bool
arg2) = Int -> Term Bool -> Term Bool -> Term Bool
AndTerm Int
i Term Bool
arg1 Term Bool
arg2
      go (UEqvTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term Bool
forall a. SupportedPrim a => Int -> Term a -> Term a -> Term Bool
EqvTerm Int
i Term t
arg1 Term t
arg2
      go (UITETerm Term Bool
cond Term t
l Term t
r) = Int -> Term Bool -> Term t -> Term t -> Term t
forall t.
SupportedPrim t =>
Int -> Term Bool -> Term t -> Term t -> Term t
ITETerm Int
i Term Bool
cond Term t
l Term t
r
      go (UAddNumTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Num t) =>
Int -> Term t -> Term t -> Term t
AddNumTerm Int
i Term t
arg1 Term t
arg2
      go (UUMinusNumTerm Term t
arg) = Int -> Term t -> Term t
forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
UMinusNumTerm Int
i Term t
arg
      go (UTimesNumTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Num t) =>
Int -> Term t -> Term t -> Term t
TimesNumTerm Int
i Term t
arg1 Term t
arg2
      go (UAbsNumTerm Term t
arg) = Int -> Term t -> Term t
forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
AbsNumTerm Int
i Term t
arg
      go (USignumNumTerm Term t
arg) = Int -> Term t -> Term t
forall t. (SupportedPrim t, Num t) => Int -> Term t -> Term t
SignumNumTerm Int
i Term t
arg
      go (ULTNumTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term Bool
forall a.
(SupportedPrim a, Num a, Ord a) =>
Int -> Term a -> Term a -> Term Bool
LTNumTerm Int
i Term t
arg1 Term t
arg2
      go (ULENumTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term Bool
forall a.
(SupportedPrim a, Num a, Ord a) =>
Int -> Term a -> Term a -> Term Bool
LENumTerm Int
i Term t
arg1 Term t
arg2
      go (UAndBitsTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Term t -> Term t
AndBitsTerm Int
i Term t
arg1 Term t
arg2
      go (UOrBitsTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Term t -> Term t
OrBitsTerm Int
i Term t
arg1 Term t
arg2
      go (UXorBitsTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Bits t) =>
Int -> Term t -> Term t -> Term t
XorBitsTerm Int
i Term t
arg1 Term t
arg2
      go (UComplementBitsTerm Term t
arg) = Int -> Term t -> Term t
forall t. (SupportedPrim t, Bits t) => Int -> Term t -> Term t
ComplementBitsTerm Int
i Term t
arg
      go (UShiftLeftTerm Term t
arg Term t
n) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Integral t, FiniteBits t, SymShift t) =>
Int -> Term t -> Term t -> Term t
ShiftLeftTerm Int
i Term t
arg Term t
n
      go (UShiftRightTerm Term t
arg Term t
n) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Integral t, FiniteBits t, SymShift t) =>
Int -> Term t -> Term t -> Term t
ShiftRightTerm Int
i Term t
arg Term t
n
      go (URotateLeftTerm Term t
arg Term t
n) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Integral t, FiniteBits t, SymRotate t) =>
Int -> Term t -> Term t -> Term t
RotateLeftTerm Int
i Term t
arg Term t
n
      go (URotateRightTerm Term t
arg Term t
n) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Integral t, FiniteBits t, SymRotate t) =>
Int -> Term t -> Term t -> Term t
RotateRightTerm Int
i Term t
arg Term t
n
      go (UToSignedTerm Term u
arg) = Int -> Term u -> Term t
forall a s.
(SupportedPrim a, SupportedPrim s, SignConversion a s) =>
Int -> Term a -> Term s
ToSignedTerm Int
i Term u
arg
      go (UToUnsignedTerm Term s
arg) = Int -> Term s -> Term t
forall u a.
(SupportedPrim u, SupportedPrim a, SignConversion u a) =>
Int -> Term a -> Term u
ToUnsignedTerm Int
i Term s
arg
      go (UBVConcatTerm Term (bv a)
arg1 Term (bv b)
arg2) = Int -> Term (bv a) -> Term (bv b) -> Term (bv (a + b))
forall (a :: Nat -> *) (l :: Nat) (r :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (a n),
 Typeable a, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l,
 1 <= r, 1 <= (l + r), SizedBV a) =>
Int -> Term (a l) -> Term (a r) -> Term (a (l + r))
BVConcatTerm Int
i Term (bv a)
arg1 Term (bv b)
arg2
      go (UBVSelectTerm TypeRep ix
ix TypeRep w
w Term (bv n)
arg) = Int -> TypeRep ix -> TypeRep w -> Term (bv n) -> Term (bv w)
forall (a :: Nat -> *) (l :: Nat) (r :: Nat) (w :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (a n),
 Typeable a, KnownNat l, KnownNat r, KnownNat w, 1 <= l, 1 <= w,
 (r + w) <= l, SizedBV a) =>
Int -> TypeRep r -> TypeRep w -> Term (a l) -> Term (a w)
BVSelectTerm Int
i TypeRep ix
ix TypeRep w
w Term (bv n)
arg
      go (UBVExtendTerm Bool
signed TypeRep r
n Term (bv l)
arg) = Int -> Bool -> TypeRep r -> Term (bv l) -> Term (bv r)
forall (a :: Nat -> *) (l :: Nat) (r :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (a n),
 Typeable a, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
 SizedBV a) =>
Int -> Bool -> TypeRep r -> Term (a l) -> Term (a r)
BVExtendTerm Int
i Bool
signed TypeRep r
n Term (bv l)
arg
      go (UTabularFunApplyTerm Term (a =-> t)
func Term a
arg) = Int -> Term (a =-> t) -> Term a -> Term t
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Int -> Term (a =-> b) -> Term a -> Term b
TabularFunApplyTerm Int
i Term (a =-> t)
func Term a
arg
      go (UGeneralFunApplyTerm Term (a --> t)
func Term a
arg) = Int -> Term (a --> t) -> Term a -> Term t
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Int -> Term (a --> b) -> Term a -> Term b
GeneralFunApplyTerm Int
i Term (a --> t)
func Term a
arg
      go (UDivIntegralTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Integral t) =>
Int -> Term t -> Term t -> Term t
DivIntegralTerm Int
i Term t
arg1 Term t
arg2
      go (UModIntegralTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Integral t) =>
Int -> Term t -> Term t -> Term t
ModIntegralTerm Int
i Term t
arg1 Term t
arg2
      go (UQuotIntegralTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Integral t) =>
Int -> Term t -> Term t -> Term t
QuotIntegralTerm Int
i Term t
arg1 Term t
arg2
      go (URemIntegralTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Integral t) =>
Int -> Term t -> Term t -> Term t
RemIntegralTerm Int
i Term t
arg1 Term t
arg2
      go (UDivBoundedIntegralTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Int -> Term t -> Term t -> Term t
DivBoundedIntegralTerm Int
i Term t
arg1 Term t
arg2
      go (UModBoundedIntegralTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Int -> Term t -> Term t -> Term t
ModBoundedIntegralTerm Int
i Term t
arg1 Term t
arg2
      go (UQuotBoundedIntegralTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Int -> Term t -> Term t -> Term t
QuotBoundedIntegralTerm Int
i Term t
arg1 Term t
arg2
      go (URemBoundedIntegralTerm Term t
arg1 Term t
arg2) = Int -> Term t -> Term t -> Term t
forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Int -> Term t -> Term t -> Term t
RemBoundedIntegralTerm Int
i Term t
arg1 Term t
arg2
  cache :: Cache (Term t)
cache = Cache (Term t)
forall t. SupportedPrim t => Cache (Term t)
termCache

instance (SupportedPrim t) => Eq (Description (Term t)) where
  DConTerm (t
l :: tyl) == :: Description (Term t) -> Description (Term t) -> Bool
== DConTerm (t
r :: tyr) = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast @tyl @tyr t
l Maybe t -> Maybe t -> Bool
forall a. Eq a => a -> a -> Bool
== t -> Maybe t
forall a. a -> Maybe a
Just t
r
  DSymTerm TypedSymbol t
ls == DSymTerm TypedSymbol t
rs = TypedSymbol t
ls TypedSymbol t -> TypedSymbol t -> Bool
forall a. Eq a => a -> a -> Bool
== TypedSymbol t
rs
  DUnaryTerm ((TypeRep tag, tag)
tagl :: tagl) (TypeRep arg, Int)
li == DUnaryTerm ((TypeRep tag, tag)
tagr :: tagr) (TypeRep arg, Int)
ri = (TypeRep tag, tag) -> (TypeRep tag, tag) -> Bool
forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep tag, tag)
tagl (TypeRep tag, tag)
tagr Bool -> Bool -> Bool
&& (TypeRep arg, Int) -> (TypeRep arg, Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg, Int)
li (TypeRep arg, Int)
ri
  DBinaryTerm ((TypeRep tag, tag)
tagl :: tagl) (TypeRep arg1, Int)
li1 (TypeRep arg2, Int)
li2 == DBinaryTerm ((TypeRep tag, tag)
tagr :: tagr) (TypeRep arg1, Int)
ri1 (TypeRep arg2, Int)
ri2 =
    (TypeRep tag, tag) -> (TypeRep tag, tag) -> Bool
forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep tag, tag)
tagl (TypeRep tag, tag)
tagr Bool -> Bool -> Bool
&& (TypeRep arg1, Int) -> (TypeRep arg1, Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg1, Int)
li1 (TypeRep arg1, Int)
ri1 Bool -> Bool -> Bool
&& (TypeRep arg2, Int) -> (TypeRep arg2, Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg2, Int)
li2 (TypeRep arg2, Int)
ri2
  DTernaryTerm ((TypeRep tag, tag)
tagl :: tagl) (TypeRep arg1, Int)
li1 (TypeRep arg2, Int)
li2 (TypeRep arg3, Int)
li3 == DTernaryTerm ((TypeRep tag, tag)
tagr :: tagr) (TypeRep arg1, Int)
ri1 (TypeRep arg2, Int)
ri2 (TypeRep arg3, Int)
ri3 =
    (TypeRep tag, tag) -> (TypeRep tag, tag) -> Bool
forall a b. Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
eqHeteroTag (TypeRep tag, tag)
tagl (TypeRep tag, tag)
tagr Bool -> Bool -> Bool
&& (TypeRep arg1, Int) -> (TypeRep arg1, Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg1, Int)
li1 (TypeRep arg1, Int)
ri1 Bool -> Bool -> Bool
&& (TypeRep arg2, Int) -> (TypeRep arg2, Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg2, Int)
li2 (TypeRep arg2, Int)
ri2 Bool -> Bool -> Bool
&& (TypeRep arg3, Int) -> (TypeRep arg3, Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep arg3, Int)
li3 (TypeRep arg3, Int)
ri3
  DNotTerm Int
li == DNotTerm Int
ri = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri
  DOrTerm Int
li1 Int
li2 == DOrTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DAndTerm Int
li1 Int
li2 == DAndTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DEqvTerm TypeRep args
lrep Int
li1 Int
li2 == DEqvTerm TypeRep args
rrep Int
ri1 Int
ri2 = TypeRep args -> TypeRep args -> Bool
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep args
lrep TypeRep args
rrep Bool -> Bool -> Bool
&& Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DITETerm Int
lc Int
li1 Int
li2 == DITETerm Int
rc Int
ri1 Int
ri2 = Int
lc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
rc Bool -> Bool -> Bool
&& Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DAddNumTerm Int
li1 Int
li2 == DAddNumTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DUMinusNumTerm Int
li == DUMinusNumTerm Int
ri = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri
  DTimesNumTerm Int
li1 Int
li2 == DTimesNumTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DAbsNumTerm Int
li == DAbsNumTerm Int
ri = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri
  DSignumNumTerm Int
li == DSignumNumTerm Int
ri = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri
  DLTNumTerm TypeRep args
lrep Int
li1 Int
li2 == DLTNumTerm TypeRep args
rrep Int
ri1 Int
ri2 = TypeRep args -> TypeRep args -> Bool
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep args
lrep TypeRep args
rrep Bool -> Bool -> Bool
&& Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DLENumTerm TypeRep args
lrep Int
li1 Int
li2 == DLENumTerm TypeRep args
rrep Int
ri1 Int
ri2 = TypeRep args -> TypeRep args -> Bool
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep args
lrep TypeRep args
rrep Bool -> Bool -> Bool
&& Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DAndBitsTerm Int
li1 Int
li2 == DAndBitsTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DOrBitsTerm Int
li1 Int
li2 == DOrBitsTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DXorBitsTerm Int
li1 Int
li2 == DXorBitsTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DComplementBitsTerm Int
li == DComplementBitsTerm Int
ri = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri
  DShiftLeftTerm Int
li Int
ln == DShiftLeftTerm Int
ri Int
rn = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri Bool -> Bool -> Bool
&& Int
ln Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
rn
  DShiftRightTerm Int
li Int
ln == DShiftRightTerm Int
ri Int
rn = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri Bool -> Bool -> Bool
&& Int
ln Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
rn
  DRotateLeftTerm Int
li Int
ln == DRotateLeftTerm Int
ri Int
rn = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri Bool -> Bool -> Bool
&& Int
ln Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
rn
  DRotateRightTerm Int
li Int
ln == DRotateRightTerm Int
ri Int
rn = Int
li Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri Bool -> Bool -> Bool
&& Int
ln Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
rn
  DToSignedTerm (TypeRep u, Int)
li == DToSignedTerm (TypeRep u, Int)
ri = (TypeRep u, Int) -> (TypeRep u, Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep u, Int)
li (TypeRep u, Int)
ri
  DToUnsignedTerm (TypeRep s, Int)
li == DToUnsignedTerm (TypeRep s, Int)
ri = (TypeRep s, Int) -> (TypeRep s, Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep s, Int)
li (TypeRep s, Int)
ri
  DBVConcatTerm TypeRep bv1
lrep1 TypeRep bv2
lrep2 Int
li1 Int
li2 == DBVConcatTerm TypeRep bv1
rrep1 TypeRep bv2
rrep2 Int
ri1 Int
ri2 =
    TypeRep bv1 -> TypeRep bv1 -> Bool
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep bv1
lrep1 TypeRep bv1
rrep1 Bool -> Bool -> Bool
&& TypeRep bv2 -> TypeRep bv2 -> Bool
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep bv2
lrep2 TypeRep bv2
rrep2 Bool -> Bool -> Bool
&& Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DBVSelectTerm TypeRep ix
lix (TypeRep (bv n), Int)
li == DBVSelectTerm TypeRep ix
rix (TypeRep (bv n), Int)
ri =
    TypeRep ix -> TypeRep ix -> Bool
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep ix
lix TypeRep ix
rix Bool -> Bool -> Bool
&& (TypeRep (bv n), Int) -> (TypeRep (bv n), Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (bv n), Int)
li (TypeRep (bv n), Int)
ri
  DBVExtendTerm Bool
lIsSigned TypeRep r
ln (TypeRep (bv l), Int)
li == DBVExtendTerm Bool
rIsSigned TypeRep r
rn (TypeRep (bv l), Int)
ri =
    Bool
lIsSigned Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
rIsSigned
      Bool -> Bool -> Bool
&& TypeRep r -> TypeRep r -> Bool
forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep r
ln TypeRep r
rn
      Bool -> Bool -> Bool
&& (TypeRep (bv l), Int) -> (TypeRep (bv l), Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (bv l), Int)
li (TypeRep (bv l), Int)
ri
  DTabularFunApplyTerm (TypeRep (a =-> t), Int)
lf (TypeRep a, Int)
li == DTabularFunApplyTerm (TypeRep (a =-> t), Int)
rf (TypeRep a, Int)
ri = (TypeRep (a =-> t), Int) -> (TypeRep (a =-> t), Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (a =-> t), Int)
lf (TypeRep (a =-> t), Int)
rf Bool -> Bool -> Bool
&& (TypeRep a, Int) -> (TypeRep a, Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep a, Int)
li (TypeRep a, Int)
ri
  DGeneralFunApplyTerm (TypeRep (a --> t), Int)
lf (TypeRep a, Int)
li == DGeneralFunApplyTerm (TypeRep (a --> t), Int)
rf (TypeRep a, Int)
ri = (TypeRep (a --> t), Int) -> (TypeRep (a --> t), Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep (a --> t), Int)
lf (TypeRep (a --> t), Int)
rf Bool -> Bool -> Bool
&& (TypeRep a, Int) -> (TypeRep a, Int) -> Bool
forall a b. (TypeRep a, Int) -> (TypeRep b, Int) -> Bool
eqTypedId (TypeRep a, Int)
li (TypeRep a, Int)
ri
  DDivIntegralTerm Int
li1 Int
li2 == DDivIntegralTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DModIntegralTerm Int
li1 Int
li2 == DModIntegralTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DQuotIntegralTerm Int
li1 Int
li2 == DQuotIntegralTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DRemIntegralTerm Int
li1 Int
li2 == DRemIntegralTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DDivBoundedIntegralTerm Int
li1 Int
li2 == DDivBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DModBoundedIntegralTerm Int
li1 Int
li2 == DModBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DQuotBoundedIntegralTerm Int
li1 Int
li2 == DQuotBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  DRemBoundedIntegralTerm Int
li1 Int
li2 == DRemBoundedIntegralTerm Int
ri1 Int
ri2 = Int
li1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri1 Bool -> Bool -> Bool
&& Int
li2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ri2
  Description (Term t)
_ == Description (Term t)
_ = Bool
False

instance (SupportedPrim t) => Hashable (Description (Term t)) where
  hashWithSalt :: Int -> Description (Term t) -> Int
hashWithSalt Int
s (DConTerm t
c) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int) Int -> t -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` t
c
  hashWithSalt Int
s (DSymTerm TypedSymbol t
name) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1 :: Int) Int -> TypedSymbol t -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol t
name
  hashWithSalt Int
s (DUnaryTerm (TypeRep tag, tag)
tag (TypeRep arg, Int)
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
2 :: Int) Int -> (TypeRep tag, tag) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag Int -> (TypeRep arg, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg, Int)
id1
  hashWithSalt Int
s (DBinaryTerm (TypeRep tag, tag)
tag (TypeRep arg1, Int)
id1 (TypeRep arg2, Int)
id2) =
    Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
3 :: Int) Int -> (TypeRep tag, tag) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag Int -> (TypeRep arg1, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg1, Int)
id1 Int -> (TypeRep arg2, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg2, Int)
id2
  hashWithSalt Int
s (DTernaryTerm (TypeRep tag, tag)
tag (TypeRep arg1, Int)
id1 (TypeRep arg2, Int)
id2 (TypeRep arg3, Int)
id3) =
    Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
4 :: Int) Int -> (TypeRep tag, tag) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep tag, tag)
tag Int -> (TypeRep arg1, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg1, Int)
id1 Int -> (TypeRep arg2, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg2, Int)
id2 Int -> (TypeRep arg3, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep arg3, Int)
id3
  hashWithSalt Int
s (DNotTerm Int
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
5 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
  hashWithSalt Int
s (DOrTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
6 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DAndTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
7 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DEqvTerm TypeRep args
rep Int
id1 Int
id2) =
    Int
s
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
8 :: Int)
      Int -> TypeRep args -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DITETerm Int
idc Int
id1 Int
id2) =
    Int
s
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
9 :: Int)
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
idc
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DAddNumTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
10 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DUMinusNumTerm Int
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
11 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
  hashWithSalt Int
s (DTimesNumTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
12 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DAbsNumTerm Int
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
13 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
  hashWithSalt Int
s (DSignumNumTerm Int
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
14 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
  hashWithSalt Int
s (DLTNumTerm TypeRep args
rep Int
id1 Int
id2) =
    Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
15 :: Int) Int -> TypeRep args -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DLENumTerm TypeRep args
rep Int
id1 Int
id2) =
    Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
16 :: Int) Int -> TypeRep args -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep args
rep Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DAndBitsTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
17 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DOrBitsTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
18 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DXorBitsTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
19 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DComplementBitsTerm Int
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
20 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1
  hashWithSalt Int
s (DShiftLeftTerm Int
id1 Int
idn) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
38 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
idn
  hashWithSalt Int
s (DShiftRightTerm Int
id1 Int
idn) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
39 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
idn
  hashWithSalt Int
s (DRotateLeftTerm Int
id1 Int
idn) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
40 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
idn
  hashWithSalt Int
s (DRotateRightTerm Int
id1 Int
idn) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
41 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
idn
  hashWithSalt Int
s (DToSignedTerm (TypeRep u, Int)
id) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
23 :: Int) Int -> (TypeRep u, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep u, Int)
id
  hashWithSalt Int
s (DToUnsignedTerm (TypeRep s, Int)
id) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
24 :: Int) Int -> (TypeRep s, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep s, Int)
id
  hashWithSalt Int
s (DBVConcatTerm TypeRep bv1
rep1 TypeRep bv2
rep2 Int
id1 Int
id2) =
    Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
25 :: Int) Int -> TypeRep bv1 -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep bv1
rep1 Int -> TypeRep bv2 -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep bv2
rep2 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DBVSelectTerm TypeRep ix
ix (TypeRep (bv n), Int)
id1) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
26 :: Int) Int -> TypeRep ix -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep ix
ix Int -> (TypeRep (bv n), Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (bv n), Int)
id1
  hashWithSalt Int
s (DBVExtendTerm Bool
signed TypeRep r
n (TypeRep (bv l), Int)
id1) =
    Int
s
      Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
27 :: Int)
      Int -> Bool -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Bool
signed
      Int -> TypeRep r -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep r
n
      Int -> (TypeRep (bv l), Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (bv l), Int)
id1
  hashWithSalt Int
s (DTabularFunApplyTerm (TypeRep (a =-> t), Int)
id1 (TypeRep a, Int)
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
28 :: Int) Int -> (TypeRep (a =-> t), Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (a =-> t), Int)
id1 Int -> (TypeRep a, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep a, Int)
id2
  hashWithSalt Int
s (DGeneralFunApplyTerm (TypeRep (a --> t), Int)
id1 (TypeRep a, Int)
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
29 :: Int) Int -> (TypeRep (a --> t), Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep (a --> t), Int)
id1 Int -> (TypeRep a, Int) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (TypeRep a, Int)
id2
  hashWithSalt Int
s (DDivIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
30 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DModIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
31 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DQuotIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
32 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DRemIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
33 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DDivBoundedIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
34 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DModBoundedIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
35 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DQuotBoundedIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
36 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2
  hashWithSalt Int
s (DRemBoundedIntegralTerm Int
id1 Int
id2) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
37 :: Int) Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id1 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
id2

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

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

instance (LinkedRep a sa, LinkedRep b sb) => Function (a --> b) where
  type Arg (a --> b) = SymType a
  type Ret (a --> b) = SymType b
  (GeneralFun TypedSymbol a
s Term b
t) # :: (a --> b) -> Arg (a --> b) -> Ret (a --> b)
# Arg (a --> b)
x = Term b -> Ret (a --> b)
forall con sym. LinkedRep con sym => Term con -> sym
wrapTerm (Term b -> Ret (a --> b)) -> Term b -> Ret (a --> b)
forall a b. (a -> b) -> a -> b
$ TypedSymbol a -> Term a -> Term b -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
s (sa -> Term a
forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm sa
Arg (a --> b)
x) Term b
t

{-
pattern GeneralFun :: () => (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b
pattern GeneralFun arg v <- GeneralFun arg v

{-# COMPLETE GeneralFun #-}
-}

infixr 0 -->

buildGeneralFun :: () => (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b
buildGeneralFun :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun TypedSymbol a
arg Term b
v = TypedSymbol a -> Term b -> a --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol a
newarg (TypedSymbol a -> Term a -> Term b -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
arg (TypedSymbol a -> Term a
forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm TypedSymbol a
newarg) Term b
v)
  where
    newarg :: TypedSymbol a
newarg = TypedSymbol a -> ARG -> TypedSymbol a
forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
 Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo TypedSymbol a
arg ARG
ARG

data ARG = ARG
  deriving (ARG -> ARG -> Bool
(ARG -> ARG -> Bool) -> (ARG -> ARG -> Bool) -> Eq ARG
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ARG -> ARG -> Bool
== :: ARG -> ARG -> Bool
$c/= :: ARG -> ARG -> Bool
/= :: ARG -> ARG -> Bool
Eq, Eq ARG
Eq ARG =>
(ARG -> ARG -> Ordering)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> ARG)
-> (ARG -> ARG -> ARG)
-> Ord ARG
ARG -> ARG -> Bool
ARG -> ARG -> Ordering
ARG -> ARG -> ARG
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ARG -> ARG -> Ordering
compare :: ARG -> ARG -> Ordering
$c< :: ARG -> ARG -> Bool
< :: ARG -> ARG -> Bool
$c<= :: ARG -> ARG -> Bool
<= :: ARG -> ARG -> Bool
$c> :: ARG -> ARG -> Bool
> :: ARG -> ARG -> Bool
$c>= :: ARG -> ARG -> Bool
>= :: ARG -> ARG -> Bool
$cmax :: ARG -> ARG -> ARG
max :: ARG -> ARG -> ARG
$cmin :: ARG -> ARG -> ARG
min :: ARG -> ARG -> ARG
Ord, (forall (m :: * -> *). Quote m => ARG -> m Exp)
-> (forall (m :: * -> *). Quote m => ARG -> Code m ARG) -> Lift ARG
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => ARG -> m Exp
forall (m :: * -> *). Quote m => ARG -> Code m ARG
$clift :: forall (m :: * -> *). Quote m => ARG -> m Exp
lift :: forall (m :: * -> *). Quote m => ARG -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
liftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
Lift, Int -> ARG -> ShowS
[ARG] -> ShowS
ARG -> String
(Int -> ARG -> ShowS)
-> (ARG -> String) -> ([ARG] -> ShowS) -> Show ARG
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ARG -> ShowS
showsPrec :: Int -> ARG -> ShowS
$cshow :: ARG -> String
show :: ARG -> String
$cshowList :: [ARG] -> ShowS
showList :: [ARG] -> ShowS
Show, (forall x. ARG -> Rep ARG x)
-> (forall x. Rep ARG x -> ARG) -> Generic ARG
forall x. Rep ARG x -> ARG
forall x. ARG -> Rep ARG x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ARG -> Rep ARG x
from :: forall x. ARG -> Rep ARG x
$cto :: forall x. Rep ARG x -> ARG
to :: forall x. Rep ARG x -> ARG
Generic)

instance NFData ARG where
  rnf :: ARG -> ()
rnf ARG
ARG = ()

instance Hashable ARG where
  hashWithSalt :: Int -> ARG -> Int
hashWithSalt Int
s ARG
ARG = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int)

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

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

instance Lift (a --> b) where
  liftTyped :: forall (m :: * -> *). Quote m => (a --> b) -> Code m (a --> b)
liftTyped (GeneralFun TypedSymbol a
sym Term b
tm) = [||TypedSymbol a -> Term b -> a --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol a
sym Term b
tm||]

instance Hashable (a --> b) where
  Int
s hashWithSalt :: Int -> (a --> b) -> Int
`hashWithSalt` (GeneralFun TypedSymbol a
sym Term b
tm) = Int
s Int -> TypedSymbol a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol a
sym Int -> Term b -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Term b
tm

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

instance (SupportedPrim a, SupportedPrim b) => SupportedPrim (a --> b) where
  type PrimConstraint (a --> b) = (SupportedPrim a, SupportedPrim b)
  defaultValue :: a --> b
defaultValue = TypedSymbol a -> Term b -> a --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
buildGeneralFun (Text -> TypedSymbol a
forall t. SupportedPrim t => Text -> TypedSymbol t
SimpleSymbol Text
"a") (b -> Term b
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm b
forall t. SupportedPrim t => t
defaultValue)

instance
  (SupportedPrim a, SupportedPrim b) =>
  SupportedPrim (a =-> b)
  where
  type PrimConstraint (a =-> b) = (SupportedPrim a, SupportedPrim b)
  defaultValue :: a =-> b
defaultValue = [(a, b)] -> b -> a =-> b
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] (forall t. SupportedPrim t => t
defaultValue @b)