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

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

-- $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 = PrimConstraint t => a
i
  termCache :: Cache (Term t)
  termCache = forall a. (Interned a, Typeable a) => Cache a
typeMemoizedCache
  pformatCon :: t -> String
  default pformatCon :: (Show t) => t -> String
  pformatCon = forall a. Show a => a -> String
show
  pformatSym :: TypedSymbol t -> String
  pformatSym = forall t. TypedSymbol t -> String
showUntyped
  defaultValue :: t
  defaultValueDynamic :: proxy t -> ModelValue
  defaultValueDynamic proxy t
_ = forall a. (Show a, Eq a, Hashable a, Typeable a) => a -> ModelValue
toModelValue (forall t. SupportedPrim t => t
defaultValue @t)

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

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

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

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

instance Lift (TypedSymbol t) where
  liftTyped :: forall (m :: * -> *).
Quote m =>
TypedSymbol t -> Code m (TypedSymbol t)
liftTyped (SimpleSymbol String
x) = [||SimpleSymbol x||]
  liftTyped (IndexedSymbol String
x Int
i) = [||IndexedSymbol x i||]
  liftTyped (WithInfo TypedSymbol t
s1 a
i1) = [||WithInfo s1 i1||]

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

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

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

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

instance (SupportedPrim t) => IsString (TypedSymbol t) where
  fromString :: String -> TypedSymbol t
fromString = forall t. SupportedPrim t => String -> TypedSymbol t
SimpleSymbol

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

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

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

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

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

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

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

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

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

instance Lift (Term t) where
  lift :: forall (m :: * -> *). Quote m => Term t -> m Exp
lift = forall a (m :: * -> *). Quote m => Splice m a -> m Exp
unTypeSplice forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (m :: * -> *). (Lift t, Quote m) => t -> Code m t
liftTyped
  liftTyped :: forall (m :: * -> *). Quote m => Term t -> Code m (Term t)
liftTyped (ConTerm Int
_ t
i) = [||conTerm i||]
  liftTyped (SymTerm Int
_ TypedSymbol t
sym) = [||symTerm sym||]
  liftTyped (UnaryTerm Int
_ tag
tag Term arg
arg) = [||constructUnary tag arg||]
  liftTyped (BinaryTerm Int
_ tag
tag Term arg1
arg1 Term arg2
arg2) = [||constructBinary tag arg1 arg2||]
  liftTyped (TernaryTerm Int
_ tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) = [||constructTernary tag arg1 arg2 arg3||]
  liftTyped (NotTerm Int
_ Term Bool
arg) = [||notTerm arg||]
  liftTyped (OrTerm Int
_ Term Bool
arg1 Term Bool
arg2) = [||orTerm arg1 arg2||]
  liftTyped (AndTerm Int
_ Term Bool
arg1 Term Bool
arg2) = [||andTerm arg1 arg2||]
  liftTyped (EqvTerm Int
_ Term t
arg1 Term t
arg2) = [||eqvTerm arg1 arg2||]
  liftTyped (ITETerm Int
_ Term Bool
cond Term t
arg1 Term t
arg2) = [||iteTerm cond arg1 arg2||]
  liftTyped (AddNumTerm Int
_ Term t
arg1 Term t
arg2) = [||addNumTerm arg1 arg2||]
  liftTyped (UMinusNumTerm Int
_ Term t
arg) = [||uminusNumTerm arg||]
  liftTyped (TimesNumTerm Int
_ Term t
arg1 Term t
arg2) = [||timesNumTerm arg1 arg2||]
  liftTyped (AbsNumTerm Int
_ Term t
arg) = [||absNumTerm arg||]
  liftTyped (SignumNumTerm Int
_ Term t
arg) = [||signumNumTerm arg||]
  liftTyped (LTNumTerm Int
_ Term t
arg1 Term t
arg2) = [||ltNumTerm arg1 arg2||]
  liftTyped (LENumTerm Int
_ Term t
arg1 Term t
arg2) = [||leNumTerm arg1 arg2||]
  liftTyped (AndBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||andBitsTerm arg1 arg2||]
  liftTyped (OrBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||orBitsTerm arg1 arg2||]
  liftTyped (XorBitsTerm Int
_ Term t
arg1 Term t
arg2) = [||xorBitsTerm arg1 arg2||]
  liftTyped (ComplementBitsTerm Int
_ Term t
arg) = [||complementBitsTerm arg||]
  liftTyped (ShiftBitsTerm Int
_ Term t
arg Int
n) = [||shiftBitsTerm arg n||]
  liftTyped (RotateBitsTerm Int
_ Term t
arg Int
n) = [||rotateBitsTerm arg n||]
  liftTyped (BVToSignedTerm Int
_ Term (ubv n)
v) = [||bvToSignedTerm v||]
  liftTyped (BVToUnsignedTerm Int
_ Term (sbv n)
v) = [||bvToUnsignedTerm v||]
  liftTyped (BVConcatTerm Int
_ Term (bv a)
arg1 Term (bv b)
arg2) = [||bvconcatTerm arg1 arg2||]
  liftTyped (BVSelectTerm Int
_ (TypeRep ix
_ :: TypeRep ix) (TypeRep w
_ :: TypeRep w) Term (bv n)
arg) = [||bvselectTerm (Proxy @ix) (Proxy @w) arg||]
  liftTyped (BVExtendTerm Int
_ Bool
signed (TypeRep r
_ :: TypeRep n) Term (bv l)
arg) = [||bvextendTerm signed (Proxy @n) arg||]
  liftTyped (TabularFunApplyTerm Int
_ Term (a =-> t)
func Term a
arg) = [||tabularFunApplyTerm func arg||]
  liftTyped (GeneralFunApplyTerm Int
_ Term (a --> t)
func Term a
arg) = [||generalFunApplyTerm func arg||]
  liftTyped (DivIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||divIntegralTerm arg1 arg2||]
  liftTyped (ModIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||modIntegralTerm arg1 arg2||]
  liftTyped (QuotIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||quotIntegralTerm arg1 arg2||]
  liftTyped (RemIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||remIntegralTerm arg1 arg2||]
  liftTyped (DivBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||divBoundedIntegralTerm arg1 arg2||]
  liftTyped (ModBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||modBoundedIntegralTerm arg1 arg2||]
  liftTyped (QuotBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||quotBoundedIntegralTerm arg1 arg2||]
  liftTyped (RemBoundedIntegralTerm Int
_ Term t
arg1 Term t
arg2) = [||remBoundedIntegralTerm arg1 arg2||]

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

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

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

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

data UTerm t where
  UConTerm :: (SupportedPrim t) => !t -> UTerm t
  USymTerm :: (SupportedPrim t) => !(TypedSymbol t) -> UTerm t
  UUnaryTerm :: (UnaryOp tag arg t) => !tag -> !(Term arg) -> UTerm t
  UBinaryTerm ::
    (BinaryOp tag arg1 arg2 t) =>
    !tag ->
    !(Term arg1) ->
    !(Term arg2) ->
    UTerm t
  UTernaryTerm ::
    (TernaryOp tag arg1 arg2 arg3 t) =>
    !tag ->
    !(Term arg1) ->
    !(Term arg2) ->
    !(Term arg3) ->
    UTerm t
  UNotTerm :: !(Term Bool) -> UTerm Bool
  UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
  UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
  UEqvTerm :: (SupportedPrim t) => !(Term t) -> !(Term t) -> UTerm Bool
  UITETerm :: (SupportedPrim t) => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t
  UAddNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
  UUMinusNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
  UTimesNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
  UAbsNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
  USignumNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
  ULTNumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool
  ULENumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool
  UAndBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
  UOrBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
  UXorBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t
  UComplementBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> UTerm t
  UShiftBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t
  URotateBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t
  UBVToSignedTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
      Typeable ubv,
      Typeable sbv,
      KnownNat n,
      1 <= n,
      BVSignConversion (ubv n) (sbv n)
    ) =>
    !(Term (ubv n)) ->
    UTerm (sbv n)
  UBVToUnsignedTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
      Typeable ubv,
      Typeable sbv,
      KnownNat n,
      1 <= n,
      BVSignConversion (ubv n) (sbv n)
    ) =>
    !(Term (sbv n)) ->
    UTerm (ubv n)
  UBVConcatTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
      Typeable bv,
      KnownNat a,
      KnownNat b,
      KnownNat (a + b),
      1 <= a,
      1 <= b,
      1 <= a + b,
      SizedBV bv
    ) =>
    !(Term (bv a)) ->
    !(Term (bv b)) ->
    UTerm (bv (a + b))
  UBVSelectTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
      Typeable bv,
      KnownNat n,
      KnownNat ix,
      KnownNat w,
      1 <= n,
      1 <= w,
      ix + w <= n,
      SizedBV bv
    ) =>
    !(TypeRep ix) ->
    !(TypeRep w) ->
    !(Term (bv n)) ->
    UTerm (bv w)
  UBVExtendTerm ::
    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
      Typeable bv,
      KnownNat l,
      KnownNat r,
      1 <= l,
      1 <= r,
      l <= r,
      SizedBV bv
    ) =>
    !Bool ->
    !(TypeRep r) ->
    !(Term (bv l)) ->
    UTerm (bv r)
  UTabularFunApplyTerm ::
    ( SupportedPrim a,
      SupportedPrim b
    ) =>
    Term (a =-> b) ->
    Term a ->
    UTerm b
  UGeneralFunApplyTerm ::
    ( SupportedPrim a,
      SupportedPrim b
    ) =>
    Term (a --> b) ->
    Term a ->
    UTerm b
  UDivIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  UModIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  UQuotIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  URemIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  UDivBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  UModBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  UQuotBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t
  URemBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | 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 = forall con sym. LinkedRep con sym => Term con -> sym
wrapTerm forall a b. (a -> b) -> a -> b
$ forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
s (forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm Arg (a --> b)
x) Term b
t

{-
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 = forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol a
newarg (forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
arg (forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm TypedSymbol a
newarg) Term b
v)
  where
    newarg :: TypedSymbol a
newarg = forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
 Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo TypedSymbol a
arg ARG
ARG

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

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

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

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

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

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

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

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

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

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