{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# HLINT ignore "Eta reduce" #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Strict #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# OPTIONS_GHC -funbox-strict-fields #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Term
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.Prim.Internal.Term
  ( -- * Supported primitive types
    SupportedPrimConstraint (..),
    SupportedPrim (..),
    withSupportedPrimTypeable,
    SymRep (..),
    ConRep (..),
    LinkedRep (..),

    -- * Partial evaluation for the terms
    PEvalApplyTerm (..),
    PEvalBitwiseTerm (..),
    PEvalShiftTerm (..),
    PEvalRotateTerm (..),
    PEvalNumTerm (..),
    pevalSubNumTerm,
    PEvalOrdTerm (..),
    pevalGtOrdTerm,
    pevalGeOrdTerm,
    pevalNEqTerm,
    PEvalDivModIntegralTerm (..),
    PEvalBitCastTerm (..),
    PEvalBitCastOrTerm (..),
    PEvalBVTerm (..),
    PEvalFractionalTerm (..),
    PEvalFloatingTerm (..),
    PEvalFromIntegralTerm (..),
    PEvalIEEEFPConvertibleTerm (..),

    -- * Typed symbols
    SymbolKind (..),
    TypedSymbol (TypedSymbol, unTypedSymbol),
    typedConstantSymbol,
    typedAnySymbol,
    TypedConstantSymbol,
    TypedAnySymbol,
    SomeTypedSymbol (..),
    SomeTypedConstantSymbol,
    SomeTypedAnySymbol,
    IsSymbolKind (..),
    showUntyped,
    withSymbolSupported,
    withConstantSymbolSupported,
    someTypedSymbol,
    eqHeteroSymbol,
    castSomeTypedSymbol,
    withSymbolKind,

    -- * Terms
    FPTrait (..),
    FPUnaryOp (..),
    FPBinaryOp (..),
    FPRoundingUnaryOp (..),
    FPRoundingBinaryOp (..),
    FloatingUnaryOp (..),
    Term (..),
    defaultValueDynamic,
    pattern DynTerm,
    toCurThread,
    termId,
    termIdent,
    typeHashId,
    introSupportedPrimConstraint,
    pformatTerm,
    ModelValue (..),
    toModelValue,
    unsafeFromModelValue,

    -- * Interning
    UTerm (..),
    prettyPrintTerm,
    forallTerm,
    existsTerm,
    conTerm,
    symTerm,
    ssymTerm,
    isymTerm,
    notTerm,
    orTerm,
    andTerm,
    eqTerm,
    distinctTerm,
    iteTerm,
    addNumTerm,
    negNumTerm,
    mulNumTerm,
    absNumTerm,
    signumNumTerm,
    ltOrdTerm,
    leOrdTerm,
    andBitsTerm,
    orBitsTerm,
    xorBitsTerm,
    complementBitsTerm,
    shiftLeftTerm,
    shiftRightTerm,
    rotateLeftTerm,
    rotateRightTerm,
    bitCastTerm,
    bitCastOrTerm,
    bvConcatTerm,
    bvSelectTerm,
    bvExtendTerm,
    bvsignExtendTerm,
    bvzeroExtendTerm,
    applyTerm,
    divIntegralTerm,
    modIntegralTerm,
    quotIntegralTerm,
    remIntegralTerm,
    fpTraitTerm,
    fdivTerm,
    recipTerm,
    floatingUnaryTerm,
    powerTerm,
    fpUnaryTerm,
    fpBinaryTerm,
    fpRoundingUnaryTerm,
    fpRoundingBinaryTerm,
    fpFMATerm,
    fromIntegralTerm,
    fromFPOrTerm,
    toFPTerm,

    -- * Support for boolean type
    trueTerm,
    falseTerm,
    pattern BoolConTerm,
    pattern TrueTerm,
    pattern FalseTerm,
    pattern BoolTerm,
    pevalNotTerm,
    pevalOrTerm,
    pevalAndTerm,
    pevalImplyTerm,
    pevalXorTerm,
    pevalITEBasic,
    pevalITEBasicTerm,
    pevalDefaultEqTerm,
    NonFuncPrimConstraint,
    NonFuncSBVRep (..),
    SupportedNonFuncPrim (..),
    SBVRep (..),
    SBVFreshMonad (..),
    translateTypeError,
    parseSMTModelResultError,
    partitionCVArg,
    parseScalarSMTModelResult,
  )
where

#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

#if !MIN_VERSION_sbv(10, 0, 0)
#define SMTDefinable Uninterpreted
#endif

#if MIN_VERSION_sbv(11,0,0)
import qualified Data.SBV as SBVTC
#endif

import Control.DeepSeq (NFData (rnf))
import Control.Monad (msum)
import Control.Monad.IO.Class (MonadIO)
import qualified Control.Monad.RWS.Lazy as Lazy
import qualified Control.Monad.RWS.Strict as Strict
import Control.Monad.Reader (MonadTrans (lift), ReaderT)
import qualified Control.Monad.State.Lazy as Lazy
import qualified Control.Monad.State.Strict as Strict
import qualified Control.Monad.Writer.Lazy as Lazy
import qualified Control.Monad.Writer.Strict as Strict
import Data.Atomics (atomicModifyIORefCAS_)
import qualified Data.Binary as Binary
import Data.Bits (Bits)
import Data.Bytes.Serial (Serial (deserialize, serialize))
import qualified Data.HashMap.Strict as HM
import Data.Hashable (Hashable (hashWithSalt))
import Data.IORef (IORef, newIORef, readIORef)
import Data.Kind (Constraint, Type)
import Data.List.NonEmpty (NonEmpty ((:|)), toList)
import Data.Maybe (fromMaybe)
import qualified Data.SBV as SBV
import qualified Data.SBV.Dynamic as SBVD
import qualified Data.SBV.Trans as SBVT
import qualified Data.SBV.Trans.Control as SBVTC
import qualified Data.Serialize as Cereal
import Data.String (IsString (fromString))
import Data.Typeable (Proxy (Proxy), cast, typeRepFingerprint)
import GHC.Exts (Any, sortWith)
import GHC.Fingerprint (Fingerprint)
import GHC.Generics (Generic)
import GHC.IO (unsafePerformIO)
import GHC.Stack (HasCallStack)
import GHC.TypeNats (KnownNat, Nat, type (+), type (<=))
import Grisette.Internal.Core.Data.Class.BitCast (BitCast, BitCastOr)
import Grisette.Internal.Core.Data.Class.BitVector
  ( SizedBV,
  )
import Grisette.Internal.Core.Data.Symbol
  ( Identifier,
    Symbol (IndexedSymbol, SimpleSymbol),
  )
import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP)
import Grisette.Internal.SymPrim.Prim.Internal.Caches
  ( Digest,
    Id,
    Ident,
    Interned
      ( Description,
        Uninterned,
        describe,
        descriptionDigest,
        identify,
        threadId
      ),
    intern,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Utils
  ( WeakThreadId,
    myWeakThreadId,
  )
import Language.Haskell.TH.Syntax (Lift (liftTyped))
import Type.Reflection
  ( SomeTypeRep (SomeTypeRep),
    TypeRep,
    Typeable,
    eqTypeRep,
    someTypeRep,
    typeRep,
    withTypeable,
    type (:~~:) (HRefl),
  )
import Unsafe.Coerce (unsafeCoerce)

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

-- | Monads that supports generating sbv fresh variables.
class (MonadIO m) => SBVFreshMonad m where
  sbvFresh :: (SBV.SymVal a) => String -> m (SBV.SBV a)

instance (MonadIO m) => SBVFreshMonad (SBVT.SymbolicT m) where
  sbvFresh :: forall a. SymVal a => String -> SymbolicT m (SBV a)
sbvFresh = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall (m :: * -> *). MonadSymbolic m => String -> m (SBV a)
SBVT.free
  {-# INLINE sbvFresh #-}

instance (MonadIO m) => SBVFreshMonad (SBVTC.QueryT m) where
  sbvFresh :: forall a. SymVal a => String -> QueryT m (SBV a)
sbvFresh = String -> QueryT m (SBV a)
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
String -> m (SBV a)
SBVTC.freshVar
  {-# INLINE sbvFresh #-}

instance (SBVFreshMonad m) => SBVFreshMonad (ReaderT r m) where
  sbvFresh :: forall a. SymVal a => String -> ReaderT r m (SBV a)
sbvFresh = m (SBV a) -> ReaderT r m (SBV a)
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (SBV a) -> ReaderT r m (SBV a))
-> (String -> m (SBV a)) -> String -> ReaderT r m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m (SBV a)
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh
  {-# INLINE sbvFresh #-}

instance (SBVFreshMonad m, Monoid w) => SBVFreshMonad (Lazy.WriterT w m) where
  sbvFresh :: forall a. SymVal a => String -> WriterT w m (SBV a)
sbvFresh = m (SBV a) -> WriterT w m (SBV a)
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (SBV a) -> WriterT w m (SBV a))
-> (String -> m (SBV a)) -> String -> WriterT w m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m (SBV a)
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh
  {-# INLINE sbvFresh #-}

instance (SBVFreshMonad m, Monoid w) => SBVFreshMonad (Lazy.RWST r w s m) where
  sbvFresh :: forall a. SymVal a => String -> RWST r w s m (SBV a)
sbvFresh = m (SBV a) -> RWST r w s m (SBV a)
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (SBV a) -> RWST r w s m (SBV a))
-> (String -> m (SBV a)) -> String -> RWST r w s m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m (SBV a)
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh
  {-# INLINE sbvFresh #-}

instance (SBVFreshMonad m) => SBVFreshMonad (Lazy.StateT s m) where
  sbvFresh :: forall a. SymVal a => String -> StateT s m (SBV a)
sbvFresh = m (SBV a) -> StateT s m (SBV a)
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (SBV a) -> StateT s m (SBV a))
-> (String -> m (SBV a)) -> String -> StateT s m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m (SBV a)
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh
  {-# INLINE sbvFresh #-}

instance (SBVFreshMonad m, Monoid w) => SBVFreshMonad (Strict.WriterT w m) where
  sbvFresh :: forall a. SymVal a => String -> WriterT w m (SBV a)
sbvFresh = m (SBV a) -> WriterT w m (SBV a)
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (SBV a) -> WriterT w m (SBV a))
-> (String -> m (SBV a)) -> String -> WriterT w m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m (SBV a)
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh
  {-# INLINE sbvFresh #-}

instance (SBVFreshMonad m, Monoid w) => SBVFreshMonad (Strict.RWST r w s m) where
  sbvFresh :: forall a. SymVal a => String -> RWST r w s m (SBV a)
sbvFresh = m (SBV a) -> RWST r w s m (SBV a)
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (SBV a) -> RWST r w s m (SBV a))
-> (String -> m (SBV a)) -> String -> RWST r w s m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m (SBV a)
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh
  {-# INLINE sbvFresh #-}

instance (SBVFreshMonad m) => SBVFreshMonad (Strict.StateT s m) where
  sbvFresh :: forall a. SymVal a => String -> StateT s m (SBV a)
sbvFresh = m (SBV a) -> StateT s m (SBV a)
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (SBV a) -> StateT s m (SBV a))
-> (String -> m (SBV a)) -> String -> StateT s m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m (SBV a)
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh
  {-# INLINE sbvFresh #-}

-- | Error message for unsupported types.
translateTypeError :: (HasCallStack) => Maybe String -> TypeRep a -> b
translateTypeError :: forall a b. HasCallStack => Maybe String -> TypeRep a -> b
translateTypeError Maybe String
Nothing TypeRep a
ta =
  String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$
    String
"Don't know how to translate the type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep a -> String
forall a. Show a => a -> String
show TypeRep a
ta String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to SMT"
translateTypeError (Just String
reason) TypeRep a
ta =
  String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$
    String
"Don't know how to translate the type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep a -> String
forall a. Show a => a -> String
show TypeRep a
ta String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to SMT: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
reason

-- | Type class for resolving the base type for the SBV type for the primitive
-- type.
class (SupportedPrim a, Ord a) => NonFuncSBVRep a where
  type NonFuncSBVBaseType a

-- | Type class for resolving the constraint for a supported non-function
-- primitive type.
type NonFuncPrimConstraint a =
  ( SBV.SymVal (NonFuncSBVBaseType a),
    SBV.EqSymbolic (SBVType a),
    SBV.Mergeable (SBVType a),
    SBV.SMTDefinable (SBVType a),
    SBV.Mergeable (SBVType a),
    SBVType a ~ SBV.SBV (NonFuncSBVBaseType a),
    PrimConstraint a
  )

-- | Indicates that a type is supported, can be represented as a symbolic term,
-- is not a function type, and can be lowered to an SBV term.
class (NonFuncSBVRep a) => SupportedNonFuncPrim a where
  conNonFuncSBVTerm :: a -> SBV.SBV (NonFuncSBVBaseType a)
  symNonFuncSBVTerm ::
    (SBVFreshMonad m) => String -> m (SBV.SBV (NonFuncSBVBaseType a))
  withNonFuncPrim :: ((NonFuncPrimConstraint a) => r) -> r

-- | Partition the list of CVs for models for functions.
partitionCVArg ::
  forall a.
  (SupportedNonFuncPrim a) =>
  [([SBVD.CV], SBVD.CV)] ->
  [(a, [([SBVD.CV], SBVD.CV)])]
partitionCVArg :: forall a.
SupportedNonFuncPrim a =>
[([CV], CV)] -> [(a, [([CV], CV)])]
partitionCVArg [([CV], CV)]
cv =
  [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
forall a.
SupportedNonFuncPrim a =>
[(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
partitionOrdCVArg ([(a, [([CV], CV)])] -> [(a, [([CV], CV)])])
-> [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
forall a b. (a -> b) -> a -> b
$
    [([CV], CV)] -> [(a, [([CV], CV)])]
forall a.
SupportedNonFuncPrim a =>
[([CV], CV)] -> [(a, [([CV], CV)])]
parseFirstCVArg [([CV], CV)]
cv
  where
    parseFirstCVArg ::
      forall a.
      (SupportedNonFuncPrim a) =>
      [([SBVD.CV], SBVD.CV)] ->
      [(a, [([SBVD.CV], SBVD.CV)])]
    parseFirstCVArg :: forall a.
SupportedNonFuncPrim a =>
[([CV], CV)] -> [(a, [([CV], CV)])]
parseFirstCVArg =
      (([CV], CV) -> (a, [([CV], CV)]))
-> [([CV], CV)] -> [(a, [([CV], CV)])]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
        ( \case
            (CV
x : [CV]
xs, CV
v) ->
              (Int -> ([([CV], CV)], CV) -> a
forall t. SupportedPrim t => Int -> ([([CV], CV)], CV) -> t
parseSMTModelResult Int
0 ([], CV
x), [([CV]
xs, CV
v)])
            ([CV], CV)
_ -> String -> (a, [([CV], CV)])
forall a. HasCallStack => String -> a
error String
"impossible"
        )
    partitionOrdCVArg ::
      forall a.
      (SupportedNonFuncPrim a) =>
      [(a, [([SBVD.CV], SBVD.CV)])] ->
      [(a, [([SBVD.CV], SBVD.CV)])]
    partitionOrdCVArg :: forall a.
SupportedNonFuncPrim a =>
[(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
partitionOrdCVArg [(a, [([CV], CV)])]
v = [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
forall {a} {a}. Eq a => [(a, [a])] -> [(a, [a])]
go [(a, [([CV], CV)])]
sorted
      where
        sorted :: [(a, [([CV], CV)])]
sorted = ((a, [([CV], CV)]) -> a)
-> [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortWith (a, [([CV], CV)]) -> a
forall a b. (a, b) -> a
fst [(a, [([CV], CV)])]
v :: [(a, [([SBVD.CV], SBVD.CV)])]
        go :: [(a, [a])] -> [(a, [a])]
go ((a, [a])
x : (a, [a])
x1 : [(a, [a])]
xs) =
          if (a, [a]) -> a
forall a b. (a, b) -> a
fst (a, [a])
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a, [a]) -> a
forall a b. (a, b) -> a
fst (a, [a])
x1
            then [(a, [a])] -> [(a, [a])]
go ([(a, [a])] -> [(a, [a])]) -> [(a, [a])] -> [(a, [a])]
forall a b. (a -> b) -> a -> b
$ ((a, [a]) -> a
forall a b. (a, b) -> a
fst (a, [a])
x, (a, [a]) -> [a]
forall a b. (a, b) -> b
snd (a, [a])
x [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ (a, [a]) -> [a]
forall a b. (a, b) -> b
snd (a, [a])
x1) (a, [a]) -> [(a, [a])] -> [(a, [a])]
forall a. a -> [a] -> [a]
: [(a, [a])]
xs
            else (a, [a])
x (a, [a]) -> [(a, [a])] -> [(a, [a])]
forall a. a -> [a] -> [a]
: [(a, [a])] -> [(a, [a])]
go ((a, [a])
x1 (a, [a]) -> [(a, [a])] -> [(a, [a])]
forall a. a -> [a] -> [a]
: [(a, [a])]
xs)
        go [(a, [a])]
x = [(a, [a])]
x

-- | Parse the scalar model result.
parseScalarSMTModelResult ::
  forall v r.
  (SBV.SatModel r, Typeable v) =>
  (r -> v) ->
  ([([SBVD.CV], SBVD.CV)], SBVD.CV) ->
  v
parseScalarSMTModelResult :: forall v r.
(SatModel r, Typeable v) =>
(r -> v) -> ([([CV], CV)], CV) -> v
parseScalarSMTModelResult r -> v
convert cvs :: ([([CV], CV)], CV)
cvs@([], CV
v) = case [CV] -> Maybe (r, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
SBV.parseCVs [CV
v] of
  Just (r
x, [CV]
_) -> r -> v
convert r
x
  Maybe (r, [CV])
Nothing -> TypeRep v -> ([([CV], CV)], CV) -> v
forall a. HasCallStack => TypeRep a -> ([([CV], CV)], CV) -> a
parseSMTModelResultError (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @v) ([([CV], CV)], CV)
cvs
parseScalarSMTModelResult r -> v
_ ([([CV], CV)], CV)
cv = TypeRep v -> ([([CV], CV)], CV) -> v
forall a. HasCallStack => TypeRep a -> ([([CV], CV)], CV) -> a
parseSMTModelResultError (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @v) ([([CV], CV)], CV)
cv

-- | Type class for resolving the SBV type for the primitive type.
class SBVRep t where
  type SBVType t

-- | Type class for resolving the constraint for a supported primitive type.
class SupportedPrimConstraint t where
  type PrimConstraint t :: Constraint
  type PrimConstraint _ = ()

-- | Indicates that a type is supported, can be represented as a symbolic term,
-- and can be lowered to an SBV term.
class
  ( Lift t,
    NFData t,
    SupportedPrimConstraint t,
    SBVRep t
  ) =>
  SupportedPrim t
  where
  primTypeRep :: TypeRep t
  default primTypeRep :: (Typeable t) => TypeRep t
  primTypeRep = TypeRep t
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
  sameCon :: t -> t -> Bool
  default sameCon :: (Eq t) => t -> t -> Bool
  sameCon = t -> t -> Bool
forall a. Eq a => a -> a -> Bool
(==)
  hashConWithSalt :: Int -> t -> Int
  default hashConWithSalt :: (Hashable t) => Int -> t -> Int
  hashConWithSalt = Int -> t -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt
  pformatCon :: t -> String
  default pformatCon :: (Show t) => t -> String
  pformatCon = t -> String
forall a. Show a => a -> String
show
  defaultValue :: t
  pevalITETerm :: Term Bool -> Term t -> Term t -> Term t
  pevalEqTerm :: Term t -> Term t -> Term Bool
  pevalDistinctTerm :: NonEmpty (Term t) -> Term Bool
  conSBVTerm :: t -> SBVType t
  symSBVName :: TypedSymbol 'AnyKind t -> Int -> String
  symSBVTerm :: (SBVFreshMonad m) => String -> m (SBVType t)
  default withPrim ::
    ( PrimConstraint t,
      SBV.SMTDefinable (SBVType t),
      SBV.Mergeable (SBVType t),
      Typeable (SBVType t)
    ) =>
    ( ( PrimConstraint t,
        SBV.SMTDefinable (SBVType t),
        SBV.Mergeable (SBVType t),
        Typeable (SBVType t)
      ) =>
      a
    ) ->
    a
  withPrim ::
    ( ( PrimConstraint t,
        SBV.SMTDefinable (SBVType t),
        SBV.Mergeable (SBVType t),
        Typeable (SBVType t)
      ) =>
      a
    ) ->
    a
  withPrim (PrimConstraint t, SMTDefinable (SBVType t), Mergeable (SBVType t),
 Typeable (SBVType t)) =>
a
i = a
(PrimConstraint t, SMTDefinable (SBVType t), Mergeable (SBVType t),
 Typeable (SBVType t)) =>
a
i
  {-# INLINE withPrim #-}
  sbvIte :: SBV.SBV Bool -> SBVType t -> SBVType t -> SBVType t
  sbvIte = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @t SBV Bool -> SBVType t -> SBVType t -> SBVType t
(PrimConstraint t, SMTDefinable (SBVType t), Mergeable (SBVType t),
 Typeable (SBVType t)) =>
SBV Bool -> SBVType t -> SBVType t -> SBVType t
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
  sbvEq :: SBVType t -> SBVType t -> SBV.SBV Bool
  default sbvEq ::
    (SBVT.EqSymbolic (SBVType t)) => SBVType t -> SBVType t -> SBV.SBV Bool
  sbvEq = SBVType t -> SBVType t -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
(SBV..==)
  sbvDistinct :: NonEmpty (SBVType t) -> SBV.SBV Bool
  default sbvDistinct ::
    (SBVT.EqSymbolic (SBVType t)) => NonEmpty (SBVType t) -> SBV.SBV Bool
  sbvDistinct = [SBVType t] -> SBV Bool
forall a. EqSymbolic a => [a] -> SBV Bool
SBV.distinct ([SBVType t] -> SBV Bool)
-> (NonEmpty (SBVType t) -> [SBVType t])
-> NonEmpty (SBVType t)
-> SBV Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (SBVType t) -> [SBVType t]
forall a. NonEmpty a -> [a]
toList
  parseSMTModelResult :: Int -> ([([SBVD.CV], SBVD.CV)], SBVD.CV) -> t
  castTypedSymbol ::
    (IsSymbolKind knd') => TypedSymbol knd t -> Maybe (TypedSymbol knd' t)
  funcDummyConstraint :: SBVType t -> SBV.SBV Bool

-- | The default value in a dynamic t'ModelValue'.
defaultValueDynamic ::
  forall t proxy. (SupportedPrim t) => proxy t -> ModelValue
defaultValueDynamic :: forall t (proxy :: * -> *).
SupportedPrim t =>
proxy t -> ModelValue
defaultValueDynamic proxy t
_ = t -> ModelValue
forall a. SupportedPrim a => a -> ModelValue
toModelValue (forall t. SupportedPrim t => t
defaultValue @t)

-- | A value with its type information.
data ModelValue where
  ModelValue :: forall v. (SupportedPrim v) => v -> ModelValue

instance NFData ModelValue where
  rnf :: ModelValue -> ()
rnf (ModelValue v
v) = v -> ()
forall a. NFData a => a -> ()
rnf v
v

instance Lift ModelValue where
  liftTyped :: forall (m :: * -> *). Quote m => ModelValue -> Code m ModelValue
liftTyped (ModelValue v
v) = [||v -> ModelValue
forall a. SupportedPrim a => a -> ModelValue
ModelValue v
v||]

instance Show ModelValue where
  show :: ModelValue -> String
show (ModelValue (v
v :: v)) = v -> String
forall t. SupportedPrim t => t -> String
pformatCon v
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep v -> String
forall a. Show a => a -> String
show (forall t. SupportedPrim t => TypeRep t
primTypeRep @v)

instance Eq ModelValue where
  (ModelValue (v
v1 :: v1)) == :: ModelValue -> ModelValue -> Bool
== (ModelValue (v
v2 :: v2)) =
    case TypeRep v -> TypeRep v -> Maybe (v :~~: v)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall t. SupportedPrim t => TypeRep t
primTypeRep @v1) (forall t. SupportedPrim t => TypeRep t
primTypeRep @v2) of
      Just v :~~: v
HRefl -> v -> v -> Bool
forall t. SupportedPrim t => t -> t -> Bool
sameCon v
v1 v
v
v2
      Maybe (v :~~: v)
_ -> Bool
False

instance Hashable ModelValue where
  Int
s hashWithSalt :: Int -> ModelValue -> Int
`hashWithSalt` (ModelValue (v
v :: v)) =
    (Int
s Int -> TypeRep v -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (forall t. SupportedPrim t => TypeRep t
primTypeRep @v)) Int -> v -> Int
forall t. SupportedPrim t => Int -> t -> Int
`hashConWithSalt` v
v

-- | Convert from a model value. Crashes if the types does not match.
unsafeFromModelValue :: forall a. (Typeable a) => ModelValue -> a
unsafeFromModelValue :: forall a. Typeable a => ModelValue -> a
unsafeFromModelValue (ModelValue (v
v :: v)) =
  case TypeRep v -> TypeRep a -> Maybe (v :~~: a)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall t. SupportedPrim t => TypeRep t
primTypeRep @v) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) of
    Just v :~~: a
HRefl -> a
v
v
    Maybe (v :~~: a)
_ ->
      String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$
        String
"Bad model value type, expected type: "
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep a -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a)
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", but got: "
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep v -> String
forall a. Show a => a -> String
show (forall t. SupportedPrim t => TypeRep t
primTypeRep @v)

-- | Convert to a model value.
toModelValue :: forall a. (SupportedPrim a) => a -> ModelValue
toModelValue :: forall a. SupportedPrim a => a -> ModelValue
toModelValue = a -> ModelValue
forall a. SupportedPrim a => a -> ModelValue
ModelValue

-- | Cast a typed symbol to a different kind. Check if the kind is compatible.
castSomeTypedSymbol ::
  (IsSymbolKind knd') => SomeTypedSymbol knd -> Maybe (SomeTypedSymbol knd')
castSomeTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind).
IsSymbolKind knd' =>
SomeTypedSymbol knd -> Maybe (SomeTypedSymbol knd')
castSomeTypedSymbol (SomeTypedSymbol s :: TypedSymbol knd t
s@TypedSymbol {}) =
  TypedSymbol knd' t -> SomeTypedSymbol knd'
forall (knd :: SymbolKind) a.
TypedSymbol knd a -> SomeTypedSymbol knd
SomeTypedSymbol (TypedSymbol knd' t -> SomeTypedSymbol knd')
-> Maybe (TypedSymbol knd' t) -> Maybe (SomeTypedSymbol knd')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypedSymbol knd t -> Maybe (TypedSymbol knd' t)
forall t (knd' :: SymbolKind) (knd :: SymbolKind).
(SupportedPrim t, IsSymbolKind knd') =>
TypedSymbol knd t -> Maybe (TypedSymbol knd' t)
forall (knd' :: SymbolKind) (knd :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd t -> Maybe (TypedSymbol knd' t)
castTypedSymbol TypedSymbol knd t
s
{-# INLINE castSomeTypedSymbol #-}

-- | Error message for failure to parse the SBV model result.
parseSMTModelResultError ::
  (HasCallStack) => TypeRep a -> ([([SBVD.CV], SBVD.CV)], SBVD.CV) -> a
parseSMTModelResultError :: forall a. HasCallStack => TypeRep a -> ([([CV], CV)], CV) -> a
parseSMTModelResultError TypeRep a
ty ([([CV], CV)], CV)
cv =
  String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$
    String
"BUG: cannot parse SBV model value \""
      String -> String -> String
forall a. Semigroup a => a -> a -> a
<> ([([CV], CV)], CV) -> String
forall a. Show a => a -> String
show ([([CV], CV)], CV)
cv
      String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\" to Grisette model value with the type "
      String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TypeRep a -> String
forall a. Show a => a -> String
show TypeRep a
ty

-- | Partial evaluation for inequality terms.
pevalNEqTerm :: (SupportedPrim a) => Term a -> Term a -> Term Bool
pevalNEqTerm :: forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalNEqTerm Term a
l Term a
r = Term Bool -> Term Bool
pevalNotTerm (Term Bool -> Term Bool) -> Term Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqTerm Term a
l Term a
r
{-# INLINE pevalNEqTerm #-}

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

-- | Partial evaluation and lowering for function application terms.
class PEvalApplyTerm f a b | f -> a b where
  pevalApplyTerm :: Term f -> Term a -> Term b
  sbvApplyTerm :: SBVType f -> SBVType a -> SBVType b

-- | Partial evaluation and lowering for bitwise operation terms.
class PEvalBitwiseTerm t where
  pevalAndBitsTerm :: Term t -> Term t -> Term t
  pevalOrBitsTerm :: Term t -> Term t -> Term t
  pevalXorBitsTerm :: Term t -> Term t -> Term t
  pevalComplementBitsTerm :: Term t -> Term t
  withSbvBitwiseTermConstraint :: (((Bits (SBVType t)) => r)) -> r
  sbvAndBitsTerm :: SBVType t -> SBVType t -> SBVType t
  sbvAndBitsTerm = forall t r. PEvalBitwiseTerm t => (Bits (SBVType t) => r) -> r
withSbvBitwiseTermConstraint @t Bits (SBVType t) => SBVType t -> SBVType t -> SBVType t
SBVType t -> SBVType t -> SBVType t
forall a. Bits a => a -> a -> a
(SBV..&.)
  sbvOrBitsTerm :: SBVType t -> SBVType t -> SBVType t
  sbvOrBitsTerm = forall t r. PEvalBitwiseTerm t => (Bits (SBVType t) => r) -> r
withSbvBitwiseTermConstraint @t Bits (SBVType t) => SBVType t -> SBVType t -> SBVType t
SBVType t -> SBVType t -> SBVType t
forall a. Bits a => a -> a -> a
(SBV..|.)
  sbvXorBitsTerm :: SBVType t -> SBVType t -> SBVType t
  sbvXorBitsTerm = forall t r. PEvalBitwiseTerm t => (Bits (SBVType t) => r) -> r
withSbvBitwiseTermConstraint @t Bits (SBVType t) => SBVType t -> SBVType t -> SBVType t
SBVType t -> SBVType t -> SBVType t
forall a. Bits a => a -> a -> a
SBV.xor
  sbvComplementBitsTerm :: SBVType t -> SBVType t
  sbvComplementBitsTerm = forall t r. PEvalBitwiseTerm t => (Bits (SBVType t) => r) -> r
withSbvBitwiseTermConstraint @t Bits (SBVType t) => SBVType t -> SBVType t
SBVType t -> SBVType t
forall a. Bits a => a -> a
SBV.complement

-- | Partial evaluation and lowering for symbolic shifting terms.
class PEvalShiftTerm t where
  pevalShiftLeftTerm :: Term t -> Term t -> Term t
  pevalShiftRightTerm :: Term t -> Term t -> Term t
  withSbvShiftTermConstraint ::
    (((SBV.SIntegral (NonFuncSBVBaseType t)) => r)) -> r
  sbvShiftLeftTerm :: SBVType t -> SBVType t -> SBVType t
  default sbvShiftLeftTerm ::
    (SupportedNonFuncPrim t) => SBVType t -> SBVType t -> SBVType t
  sbvShiftLeftTerm SBVType t
l SBVType t
r =
    forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @t ((NonFuncPrimConstraint t => SBVType t) -> SBVType t)
-> (NonFuncPrimConstraint t => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ forall t r.
PEvalShiftTerm t =>
(SIntegral (NonFuncSBVBaseType t) => r) -> r
withSbvShiftTermConstraint @t ((SIntegral (NonFuncSBVBaseType t) => SBVType t) -> SBVType t)
-> (SIntegral (NonFuncSBVBaseType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ SBV (NonFuncSBVBaseType t)
-> SBV (NonFuncSBVBaseType t) -> SBV (NonFuncSBVBaseType t)
forall a b. (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
SBV.sShiftLeft SBV (NonFuncSBVBaseType t)
SBVType t
l SBV (NonFuncSBVBaseType t)
SBVType t
r
  default sbvShiftRightTerm ::
    (SupportedNonFuncPrim t) => SBVType t -> SBVType t -> SBVType t
  sbvShiftRightTerm :: SBVType t -> SBVType t -> SBVType t
  sbvShiftRightTerm SBVType t
l SBVType t
r =
    forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @t ((NonFuncPrimConstraint t => SBVType t) -> SBVType t)
-> (NonFuncPrimConstraint t => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ forall t r.
PEvalShiftTerm t =>
(SIntegral (NonFuncSBVBaseType t) => r) -> r
withSbvShiftTermConstraint @t ((SIntegral (NonFuncSBVBaseType t) => SBVType t) -> SBVType t)
-> (SIntegral (NonFuncSBVBaseType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ SBV (NonFuncSBVBaseType t)
-> SBV (NonFuncSBVBaseType t) -> SBV (NonFuncSBVBaseType t)
forall a b. (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
SBV.sShiftRight SBV (NonFuncSBVBaseType t)
SBVType t
l SBV (NonFuncSBVBaseType t)
SBVType t
r

-- | Partial evaluation and lowering for symbolic rotate terms.
class PEvalRotateTerm t where
  pevalRotateLeftTerm :: Term t -> Term t -> Term t
  pevalRotateRightTerm :: Term t -> Term t -> Term t
  withSbvRotateTermConstraint ::
    (((SBV.SIntegral (NonFuncSBVBaseType t)) => r)) -> r
  sbvRotateLeftTerm :: SBVType t -> SBVType t -> SBVType t
  default sbvRotateLeftTerm ::
    (SupportedNonFuncPrim t) => SBVType t -> SBVType t -> SBVType t
  sbvRotateLeftTerm SBVType t
l SBVType t
r =
    forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @t ((NonFuncPrimConstraint t => SBVType t) -> SBVType t)
-> (NonFuncPrimConstraint t => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ forall t r.
PEvalRotateTerm t =>
(SIntegral (NonFuncSBVBaseType t) => r) -> r
withSbvRotateTermConstraint @t ((SIntegral (NonFuncSBVBaseType t) => SBVType t) -> SBVType t)
-> (SIntegral (NonFuncSBVBaseType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ SBV (NonFuncSBVBaseType t)
-> SBV (NonFuncSBVBaseType t) -> SBV (NonFuncSBVBaseType t)
forall a b. (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
SBV.sRotateLeft SBV (NonFuncSBVBaseType t)
SBVType t
l SBV (NonFuncSBVBaseType t)
SBVType t
r
  sbvRotateRightTerm :: SBVType t -> SBVType t -> SBVType t
  default sbvRotateRightTerm ::
    (SupportedNonFuncPrim t) => SBVType t -> SBVType t -> SBVType t
  sbvRotateRightTerm SBVType t
l SBVType t
r =
    forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @t ((NonFuncPrimConstraint t => SBVType t) -> SBVType t)
-> (NonFuncPrimConstraint t => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ forall t r.
PEvalRotateTerm t =>
(SIntegral (NonFuncSBVBaseType t) => r) -> r
withSbvRotateTermConstraint @t ((SIntegral (NonFuncSBVBaseType t) => SBVType t) -> SBVType t)
-> (SIntegral (NonFuncSBVBaseType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ SBV (NonFuncSBVBaseType t)
-> SBV (NonFuncSBVBaseType t) -> SBV (NonFuncSBVBaseType t)
forall a b. (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
SBV.sRotateRight SBV (NonFuncSBVBaseType t)
SBVType t
l SBV (NonFuncSBVBaseType t)
SBVType t
r

-- | Partial evaluation and lowering for number terms.
class (Num t) => PEvalNumTerm t where
  pevalAddNumTerm :: Term t -> Term t -> Term t
  pevalNegNumTerm :: Term t -> Term t
  pevalMulNumTerm :: Term t -> Term t -> Term t
  pevalAbsNumTerm :: Term t -> Term t
  pevalSignumNumTerm :: Term t -> Term t
  withSbvNumTermConstraint :: (((Num (SBVType t)) => r)) -> r
  sbvAddNumTerm ::
    SBVType t ->
    SBVType t ->
    SBVType t
  sbvAddNumTerm SBVType t
l SBVType t
r = forall t r. PEvalNumTerm t => (Num (SBVType t) => r) -> r
withSbvNumTermConstraint @t ((Num (SBVType t) => SBVType t) -> SBVType t)
-> (Num (SBVType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ SBVType t
l SBVType t -> SBVType t -> SBVType t
forall a. Num a => a -> a -> a
+ SBVType t
r
  sbvNegNumTerm ::
    SBVType t ->
    SBVType t
  sbvNegNumTerm SBVType t
l = forall t r. PEvalNumTerm t => (Num (SBVType t) => r) -> r
withSbvNumTermConstraint @t ((Num (SBVType t) => SBVType t) -> SBVType t)
-> (Num (SBVType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ -SBVType t
l
  sbvMulNumTerm ::
    SBVType t ->
    SBVType t ->
    SBVType t
  sbvMulNumTerm SBVType t
l SBVType t
r = forall t r. PEvalNumTerm t => (Num (SBVType t) => r) -> r
withSbvNumTermConstraint @t ((Num (SBVType t) => SBVType t) -> SBVType t)
-> (Num (SBVType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ SBVType t
l SBVType t -> SBVType t -> SBVType t
forall a. Num a => a -> a -> a
* SBVType t
r
  sbvAbsNumTerm ::
    SBVType t ->
    SBVType t
  sbvAbsNumTerm SBVType t
l = forall t r. PEvalNumTerm t => (Num (SBVType t) => r) -> r
withSbvNumTermConstraint @t ((Num (SBVType t) => SBVType t) -> SBVType t)
-> (Num (SBVType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ SBVType t -> SBVType t
forall a. Num a => a -> a
abs SBVType t
l
  sbvSignumNumTerm ::
    SBVType t ->
    SBVType t
  sbvSignumNumTerm SBVType t
l = forall t r. PEvalNumTerm t => (Num (SBVType t) => r) -> r
withSbvNumTermConstraint @t ((Num (SBVType t) => SBVType t) -> SBVType t)
-> (Num (SBVType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ SBVType t -> SBVType t
forall a. Num a => a -> a
signum SBVType t
l

-- | Partial evaluation for subtraction terms.
pevalSubNumTerm :: (PEvalNumTerm a) => Term a -> Term a -> Term a
pevalSubNumTerm :: forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalSubNumTerm Term a
l Term a
r = Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalAddNumTerm Term a
l (Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term a
r)

-- | Partial evaluation and lowering for comparison terms.
class PEvalOrdTerm t where
  pevalLtOrdTerm :: Term t -> Term t -> Term Bool
  pevalLeOrdTerm :: Term t -> Term t -> Term Bool
  withSbvOrdTermConstraint :: (((SBV.OrdSymbolic (SBVType t)) => r)) -> r
  sbvLtOrdTerm ::
    SBVType t ->
    SBVType t ->
    SBV.SBV Bool
  sbvLtOrdTerm SBVType t
l SBVType t
r = forall t r. PEvalOrdTerm t => (OrdSymbolic (SBVType t) => r) -> r
withSbvOrdTermConstraint @t ((OrdSymbolic (SBVType t) => SBV Bool) -> SBV Bool)
-> (OrdSymbolic (SBVType t) => SBV Bool) -> SBV Bool
forall a b. (a -> b) -> a -> b
$ SBVType t
l SBVType t -> SBVType t -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
SBV..< SBVType t
r
  sbvLeOrdTerm :: SBVType t -> SBVType t -> SBV.SBV Bool
  sbvLeOrdTerm SBVType t
l SBVType t
r = forall t r. PEvalOrdTerm t => (OrdSymbolic (SBVType t) => r) -> r
withSbvOrdTermConstraint @t ((OrdSymbolic (SBVType t) => SBV Bool) -> SBV Bool)
-> (OrdSymbolic (SBVType t) => SBV Bool) -> SBV Bool
forall a b. (a -> b) -> a -> b
$ SBVType t
l SBVType t -> SBVType t -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
SBV..<= SBVType t
r

-- | Partial evaluation for greater than terms.
pevalGtOrdTerm :: (PEvalOrdTerm a) => Term a -> Term a -> Term Bool
pevalGtOrdTerm :: forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGtOrdTerm = (Term a -> Term a -> Term Bool) -> Term a -> Term a -> Term Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm
{-# INLINE pevalGtOrdTerm #-}

-- | Partial evaluation for greater than or equal to terms.
pevalGeOrdTerm :: (PEvalOrdTerm a) => Term a -> Term a -> Term Bool
pevalGeOrdTerm :: forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeOrdTerm = (Term a -> Term a -> Term Bool) -> Term a -> Term a -> Term Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm
{-# INLINE pevalGeOrdTerm #-}

-- | Partial evaluation and lowering for integer division and modulo terms.
class PEvalDivModIntegralTerm t where
  pevalDivIntegralTerm :: Term t -> Term t -> Term t
  pevalModIntegralTerm :: Term t -> Term t -> Term t
  pevalQuotIntegralTerm :: Term t -> Term t -> Term t
  pevalRemIntegralTerm :: Term t -> Term t -> Term t
  withSbvDivModIntegralTermConstraint ::
    (((SBV.SDivisible (SBVType t)) => r)) -> r
  sbvDivIntegralTerm :: SBVType t -> SBVType t -> SBVType t
  sbvDivIntegralTerm SBVType t
l SBVType t
r =
    forall t r.
PEvalDivModIntegralTerm t =>
(SDivisible (SBVType t) => r) -> r
withSbvDivModIntegralTermConstraint @t ((SDivisible (SBVType t) => SBVType t) -> SBVType t)
-> (SDivisible (SBVType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ SBVType t
l SBVType t -> SBVType t -> SBVType t
forall a. SDivisible a => a -> a -> a
`SBV.sDiv` SBVType t
r
  sbvModIntegralTerm :: SBVType t -> SBVType t -> SBVType t
  sbvModIntegralTerm SBVType t
l SBVType t
r =
    forall t r.
PEvalDivModIntegralTerm t =>
(SDivisible (SBVType t) => r) -> r
withSbvDivModIntegralTermConstraint @t ((SDivisible (SBVType t) => SBVType t) -> SBVType t)
-> (SDivisible (SBVType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ SBVType t
l SBVType t -> SBVType t -> SBVType t
forall a. SDivisible a => a -> a -> a
`SBV.sMod` SBVType t
r
  sbvQuotIntegralTerm :: SBVType t -> SBVType t -> SBVType t
  sbvQuotIntegralTerm SBVType t
l SBVType t
r =
    forall t r.
PEvalDivModIntegralTerm t =>
(SDivisible (SBVType t) => r) -> r
withSbvDivModIntegralTermConstraint @t ((SDivisible (SBVType t) => SBVType t) -> SBVType t)
-> (SDivisible (SBVType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ SBVType t
l SBVType t -> SBVType t -> SBVType t
forall a. SDivisible a => a -> a -> a
`SBV.sQuot` SBVType t
r
  sbvRemIntegralTerm :: SBVType t -> SBVType t -> SBVType t
  sbvRemIntegralTerm SBVType t
l SBVType t
r =
    forall t r.
PEvalDivModIntegralTerm t =>
(SDivisible (SBVType t) => r) -> r
withSbvDivModIntegralTermConstraint @t ((SDivisible (SBVType t) => SBVType t) -> SBVType t)
-> (SDivisible (SBVType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ SBVType t
l SBVType t -> SBVType t -> SBVType t
forall a. SDivisible a => a -> a -> a
`SBV.sRem` SBVType t
r

-- | Partial evaluation and lowering for bitcast terms.
class (BitCast a b) => PEvalBitCastTerm a b where
  pevalBitCastTerm :: Term a -> Term b
  sbvBitCast :: SBVType a -> SBVType b

-- | Partial evaluation and lowering for bitcast or default value terms.
class
  (BitCastOr a b) =>
  PEvalBitCastOrTerm a b
  where
  pevalBitCastOrTerm :: Term b -> Term a -> Term b
  sbvBitCastOr :: SBVType b -> SBVType a -> SBVType b

-- | Partial evaluation and lowering for bit-vector terms.
class (SizedBV bv) => PEvalBVTerm bv where
  pevalBVConcatTerm ::
    (KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
    Term (bv l) ->
    Term (bv r) ->
    Term (bv (l + r))
  pevalBVExtendTerm ::
    (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
    Bool ->
    proxy r ->
    Term (bv l) ->
    Term (bv r)
  pevalBVSelectTerm ::
    (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>
    p ix ->
    q w ->
    Term (bv n) ->
    Term (bv w)
  sbvBVConcatTerm ::
    (KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
    p1 l ->
    p2 r ->
    SBVType (bv l) ->
    SBVType (bv r) ->
    SBVType (bv (l + r))
  sbvBVExtendTerm ::
    (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
    p1 l ->
    p2 r ->
    Bool ->
    SBVType (bv l) ->
    SBVType (bv r)
  sbvBVSelectTerm ::
    ( KnownNat ix,
      KnownNat w,
      KnownNat n,
      1 <= n,
      1 <= w,
      ix + w <= n
    ) =>
    p1 ix ->
    p2 w ->
    p3 n ->
    SBVType (bv n) ->
    SBVType (bv w)

-- | Partial evaluation and lowering for fractional terms.
class (Fractional t) => PEvalFractionalTerm t where
  pevalFdivTerm :: Term t -> Term t -> Term t
  pevalRecipTerm :: Term t -> Term t
  withSbvFractionalTermConstraint ::
    (((Fractional (SBVType t)) => r)) ->
    r
  sbvFdivTerm ::
    SBVType t ->
    SBVType t ->
    SBVType t
  sbvFdivTerm SBVType t
l SBVType t
r = forall t r.
PEvalFractionalTerm t =>
(Fractional (SBVType t) => r) -> r
withSbvFractionalTermConstraint @t ((Fractional (SBVType t) => SBVType t) -> SBVType t)
-> (Fractional (SBVType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ SBVType t
l SBVType t -> SBVType t -> SBVType t
forall a. Fractional a => a -> a -> a
/ SBVType t
r
  sbvRecipTerm ::
    SBVType t ->
    SBVType t
  sbvRecipTerm SBVType t
l = forall t r.
PEvalFractionalTerm t =>
(Fractional (SBVType t) => r) -> r
withSbvFractionalTermConstraint @t ((Fractional (SBVType t) => SBVType t) -> SBVType t)
-> (Fractional (SBVType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$ SBVType t -> SBVType t
forall a. Fractional a => a -> a
recip SBVType t
l

-- | Unary floating point operations.
data FloatingUnaryOp
  = FloatingExp
  | FloatingLog
  | FloatingSqrt
  | FloatingSin
  | FloatingCos
  | FloatingTan
  | FloatingAsin
  | FloatingAcos
  | FloatingAtan
  | FloatingSinh
  | FloatingCosh
  | FloatingTanh
  | FloatingAsinh
  | FloatingAcosh
  | FloatingAtanh
  deriving (FloatingUnaryOp -> FloatingUnaryOp -> Bool
(FloatingUnaryOp -> FloatingUnaryOp -> Bool)
-> (FloatingUnaryOp -> FloatingUnaryOp -> Bool)
-> Eq FloatingUnaryOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FloatingUnaryOp -> FloatingUnaryOp -> Bool
== :: FloatingUnaryOp -> FloatingUnaryOp -> Bool
$c/= :: FloatingUnaryOp -> FloatingUnaryOp -> Bool
/= :: FloatingUnaryOp -> FloatingUnaryOp -> Bool
Eq, Eq FloatingUnaryOp
Eq FloatingUnaryOp =>
(FloatingUnaryOp -> FloatingUnaryOp -> Ordering)
-> (FloatingUnaryOp -> FloatingUnaryOp -> Bool)
-> (FloatingUnaryOp -> FloatingUnaryOp -> Bool)
-> (FloatingUnaryOp -> FloatingUnaryOp -> Bool)
-> (FloatingUnaryOp -> FloatingUnaryOp -> Bool)
-> (FloatingUnaryOp -> FloatingUnaryOp -> FloatingUnaryOp)
-> (FloatingUnaryOp -> FloatingUnaryOp -> FloatingUnaryOp)
-> Ord FloatingUnaryOp
FloatingUnaryOp -> FloatingUnaryOp -> Bool
FloatingUnaryOp -> FloatingUnaryOp -> Ordering
FloatingUnaryOp -> FloatingUnaryOp -> FloatingUnaryOp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FloatingUnaryOp -> FloatingUnaryOp -> Ordering
compare :: FloatingUnaryOp -> FloatingUnaryOp -> Ordering
$c< :: FloatingUnaryOp -> FloatingUnaryOp -> Bool
< :: FloatingUnaryOp -> FloatingUnaryOp -> Bool
$c<= :: FloatingUnaryOp -> FloatingUnaryOp -> Bool
<= :: FloatingUnaryOp -> FloatingUnaryOp -> Bool
$c> :: FloatingUnaryOp -> FloatingUnaryOp -> Bool
> :: FloatingUnaryOp -> FloatingUnaryOp -> Bool
$c>= :: FloatingUnaryOp -> FloatingUnaryOp -> Bool
>= :: FloatingUnaryOp -> FloatingUnaryOp -> Bool
$cmax :: FloatingUnaryOp -> FloatingUnaryOp -> FloatingUnaryOp
max :: FloatingUnaryOp -> FloatingUnaryOp -> FloatingUnaryOp
$cmin :: FloatingUnaryOp -> FloatingUnaryOp -> FloatingUnaryOp
min :: FloatingUnaryOp -> FloatingUnaryOp -> FloatingUnaryOp
Ord, (forall x. FloatingUnaryOp -> Rep FloatingUnaryOp x)
-> (forall x. Rep FloatingUnaryOp x -> FloatingUnaryOp)
-> Generic FloatingUnaryOp
forall x. Rep FloatingUnaryOp x -> FloatingUnaryOp
forall x. FloatingUnaryOp -> Rep FloatingUnaryOp x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FloatingUnaryOp -> Rep FloatingUnaryOp x
from :: forall x. FloatingUnaryOp -> Rep FloatingUnaryOp x
$cto :: forall x. Rep FloatingUnaryOp x -> FloatingUnaryOp
to :: forall x. Rep FloatingUnaryOp x -> FloatingUnaryOp
Generic, Eq FloatingUnaryOp
Eq FloatingUnaryOp =>
(Int -> FloatingUnaryOp -> Int)
-> (FloatingUnaryOp -> Int) -> Hashable FloatingUnaryOp
Int -> FloatingUnaryOp -> Int
FloatingUnaryOp -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> FloatingUnaryOp -> Int
hashWithSalt :: Int -> FloatingUnaryOp -> Int
$chash :: FloatingUnaryOp -> Int
hash :: FloatingUnaryOp -> Int
Hashable, (forall (m :: * -> *). Quote m => FloatingUnaryOp -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    FloatingUnaryOp -> Code m FloatingUnaryOp)
-> Lift FloatingUnaryOp
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => FloatingUnaryOp -> m Exp
forall (m :: * -> *).
Quote m =>
FloatingUnaryOp -> Code m FloatingUnaryOp
$clift :: forall (m :: * -> *). Quote m => FloatingUnaryOp -> m Exp
lift :: forall (m :: * -> *). Quote m => FloatingUnaryOp -> m Exp
$cliftTyped :: forall (m :: * -> *).
Quote m =>
FloatingUnaryOp -> Code m FloatingUnaryOp
liftTyped :: forall (m :: * -> *).
Quote m =>
FloatingUnaryOp -> Code m FloatingUnaryOp
Lift, FloatingUnaryOp -> ()
(FloatingUnaryOp -> ()) -> NFData FloatingUnaryOp
forall a. (a -> ()) -> NFData a
$crnf :: FloatingUnaryOp -> ()
rnf :: FloatingUnaryOp -> ()
NFData, (forall (m :: * -> *). MonadPut m => FloatingUnaryOp -> m ())
-> (forall (m :: * -> *). MonadGet m => m FloatingUnaryOp)
-> Serial FloatingUnaryOp
forall a.
(forall (m :: * -> *). MonadPut m => a -> m ())
-> (forall (m :: * -> *). MonadGet m => m a) -> Serial a
forall (m :: * -> *). MonadGet m => m FloatingUnaryOp
forall (m :: * -> *). MonadPut m => FloatingUnaryOp -> m ()
$cserialize :: forall (m :: * -> *). MonadPut m => FloatingUnaryOp -> m ()
serialize :: forall (m :: * -> *). MonadPut m => FloatingUnaryOp -> m ()
$cdeserialize :: forall (m :: * -> *). MonadGet m => m FloatingUnaryOp
deserialize :: forall (m :: * -> *). MonadGet m => m FloatingUnaryOp
Serial)

instance Cereal.Serialize FloatingUnaryOp where
  put :: Putter FloatingUnaryOp
put = Putter FloatingUnaryOp
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => FloatingUnaryOp -> m ()
serialize
  get :: Get FloatingUnaryOp
get = Get FloatingUnaryOp
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m FloatingUnaryOp
deserialize

instance Binary.Binary FloatingUnaryOp where
  put :: FloatingUnaryOp -> Put
put = FloatingUnaryOp -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => FloatingUnaryOp -> m ()
serialize
  get :: Get FloatingUnaryOp
get = Get FloatingUnaryOp
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m FloatingUnaryOp
deserialize

instance Show FloatingUnaryOp where
  show :: FloatingUnaryOp -> String
show FloatingUnaryOp
FloatingExp = String
"exp"
  show FloatingUnaryOp
FloatingLog = String
"log"
  show FloatingUnaryOp
FloatingSqrt = String
"sqrt"
  show FloatingUnaryOp
FloatingSin = String
"sin"
  show FloatingUnaryOp
FloatingCos = String
"cos"
  show FloatingUnaryOp
FloatingTan = String
"tan"
  show FloatingUnaryOp
FloatingAsin = String
"asin"
  show FloatingUnaryOp
FloatingAcos = String
"acos"
  show FloatingUnaryOp
FloatingAtan = String
"atan"
  show FloatingUnaryOp
FloatingSinh = String
"sinh"
  show FloatingUnaryOp
FloatingCosh = String
"cosh"
  show FloatingUnaryOp
FloatingTanh = String
"tanh"
  show FloatingUnaryOp
FloatingAsinh = String
"asinh"
  show FloatingUnaryOp
FloatingAcosh = String
"acosh"
  show FloatingUnaryOp
FloatingAtanh = String
"atanh"

-- | Partial evaluation and lowering for floating point terms.
class PEvalFloatingTerm t where
  pevalFloatingUnaryTerm :: FloatingUnaryOp -> Term t -> Term t
  pevalPowerTerm :: Term t -> Term t -> Term t
  withSbvFloatingTermConstraint ::
    (((Floating (SBVType t)) => r)) ->
    r
  sbvPowerTerm ::
    SBVType t ->
    SBVType t ->
    SBVType t
  sbvPowerTerm = forall t r. PEvalFloatingTerm t => (Floating (SBVType t) => r) -> r
withSbvFloatingTermConstraint @t Floating (SBVType t) => SBVType t -> SBVType t -> SBVType t
SBVType t -> SBVType t -> SBVType t
forall a. Floating a => a -> a -> a
(**)
  sbvFloatingUnaryTerm ::
    FloatingUnaryOp ->
    SBVType t ->
    SBVType t
  sbvFloatingUnaryTerm FloatingUnaryOp
op SBVType t
l =
    forall t r. PEvalFloatingTerm t => (Floating (SBVType t) => r) -> r
withSbvFloatingTermConstraint @t ((Floating (SBVType t) => SBVType t) -> SBVType t)
-> (Floating (SBVType t) => SBVType t) -> SBVType t
forall a b. (a -> b) -> a -> b
$
      case FloatingUnaryOp
op of
        FloatingUnaryOp
FloatingExp -> SBVType t -> SBVType t
forall a. Floating a => a -> a
exp SBVType t
l
        FloatingUnaryOp
FloatingLog -> SBVType t -> SBVType t
forall a. Floating a => a -> a
log SBVType t
l
        FloatingUnaryOp
FloatingSqrt -> SBVType t -> SBVType t
forall a. Floating a => a -> a
sqrt SBVType t
l
        FloatingUnaryOp
FloatingSin -> SBVType t -> SBVType t
forall a. Floating a => a -> a
sin SBVType t
l
        FloatingUnaryOp
FloatingCos -> SBVType t -> SBVType t
forall a. Floating a => a -> a
cos SBVType t
l
        FloatingUnaryOp
FloatingTan -> SBVType t -> SBVType t
forall a. Floating a => a -> a
tan SBVType t
l
        FloatingUnaryOp
FloatingAsin -> SBVType t -> SBVType t
forall a. Floating a => a -> a
asin SBVType t
l
        FloatingUnaryOp
FloatingAcos -> SBVType t -> SBVType t
forall a. Floating a => a -> a
acos SBVType t
l
        FloatingUnaryOp
FloatingAtan -> SBVType t -> SBVType t
forall a. Floating a => a -> a
atan SBVType t
l
        FloatingUnaryOp
FloatingSinh -> SBVType t -> SBVType t
forall a. Floating a => a -> a
sinh SBVType t
l
        FloatingUnaryOp
FloatingCosh -> SBVType t -> SBVType t
forall a. Floating a => a -> a
cosh SBVType t
l
        FloatingUnaryOp
FloatingTanh -> SBVType t -> SBVType t
forall a. Floating a => a -> a
tanh SBVType t
l
        FloatingUnaryOp
FloatingAsinh -> SBVType t -> SBVType t
forall a. Floating a => a -> a
asinh SBVType t
l
        FloatingUnaryOp
FloatingAcosh -> SBVType t -> SBVType t
forall a. Floating a => a -> a
acosh SBVType t
l
        FloatingUnaryOp
FloatingAtanh -> SBVType t -> SBVType t
forall a. Floating a => a -> a
atanh SBVType t
l

-- | Partial evaluation and lowering for integral terms.
class (Integral a, Num b) => PEvalFromIntegralTerm a b where
  pevalFromIntegralTerm :: Term a -> Term b
  sbvFromIntegralTerm :: SBVType a -> SBVType b

-- | Partial evaluation and lowering for converting from and to IEEE floating
-- point terms.
class PEvalIEEEFPConvertibleTerm a where
  pevalFromFPOrTerm ::
    (ValidFP eb sb) =>
    Term a ->
    Term FPRoundingMode ->
    Term (FP eb sb) ->
    Term a
  pevalToFPTerm ::
    (ValidFP eb sb) => Term FPRoundingMode -> Term a -> Term (FP eb sb)
  sbvFromFPOrTerm ::
    (ValidFP eb sb) =>
    SBVType a ->
    SBVType FPRoundingMode ->
    SBVType (FP eb sb) ->
    SBVType a
  sbvToFPTerm ::
    (ValidFP eb sb) =>
    SBVType FPRoundingMode ->
    SBVType a ->
    SBVType (FP eb sb)

-- Typed Symbols

-- | The kind of a symbol.
--
-- All symbols are 'AnyKind', and all symbols other than general/tabular
-- functions are 'ConstantKind'.
data SymbolKind = ConstantKind | AnyKind

-- | Decision procedure for symbol kinds.
class IsSymbolKind (ty :: SymbolKind) where
  type SymbolKindConstraint ty :: Type -> Constraint
  decideSymbolKind :: Either (ty :~~: 'ConstantKind) (ty :~~: 'AnyKind)

instance IsSymbolKind 'ConstantKind where
  type SymbolKindConstraint 'ConstantKind = SupportedNonFuncPrim
  decideSymbolKind :: Either
  ('ConstantKind :~~: 'ConstantKind) ('ConstantKind :~~: 'AnyKind)
decideSymbolKind = ('ConstantKind :~~: 'ConstantKind)
-> Either
     ('ConstantKind :~~: 'ConstantKind) ('ConstantKind :~~: 'AnyKind)
forall a b. a -> Either a b
Left 'ConstantKind :~~: 'ConstantKind
forall {k1} (a :: k1). a :~~: a
HRefl

instance IsSymbolKind 'AnyKind where
  type SymbolKindConstraint 'AnyKind = SupportedPrim
  decideSymbolKind :: Either ('AnyKind :~~: 'ConstantKind) ('AnyKind :~~: 'AnyKind)
decideSymbolKind = ('AnyKind :~~: 'AnyKind)
-> Either ('AnyKind :~~: 'ConstantKind) ('AnyKind :~~: 'AnyKind)
forall a b. b -> Either a b
Right 'AnyKind :~~: 'AnyKind
forall {k1} (a :: k1). a :~~: a
HRefl

-- | 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:
--
-- >>> "a" :: TypedSymbol 'AnyKind Bool
-- a :: Bool
data TypedSymbol (knd :: SymbolKind) t where
  TypedSymbol ::
    ( SupportedPrim t,
      SymbolKindConstraint knd t,
      IsSymbolKind knd
    ) =>
    {forall t (knd :: SymbolKind). TypedSymbol knd t -> Symbol
unTypedSymbol :: Symbol} ->
    TypedSymbol knd t

-- | Create a typed symbol with constant kinds.
typedConstantSymbol ::
  forall t. (SupportedNonFuncPrim t) => Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol :: forall t.
SupportedNonFuncPrim t =>
Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol = PhantomNonFuncDict t -> Symbol -> TypedSymbol 'ConstantKind t
forall t.
PhantomNonFuncDict t -> Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol' PhantomNonFuncDict t
forall a. SupportedNonFuncPrim a => PhantomNonFuncDict a
getPhantomNonFuncDict
{-# INLINE typedConstantSymbol #-}

{-# NOINLINE typedConstantSymbol' #-}
typedConstantSymbol' ::
  forall t. PhantomNonFuncDict t -> Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol' :: forall t.
PhantomNonFuncDict t -> Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol' PhantomNonFuncDict t
PhantomNonFuncDict Symbol
symbol = Symbol -> TypedSymbol 'ConstantKind t
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
symbol

-- | Create a typed symbol with any kinds.
typedAnySymbol ::
  forall t. (SupportedPrim t) => Symbol -> TypedSymbol 'AnyKind t
typedAnySymbol :: forall t. SupportedPrim t => Symbol -> TypedSymbol 'AnyKind t
typedAnySymbol = PhantomDict t -> Symbol -> TypedSymbol 'AnyKind t
forall t. PhantomDict t -> Symbol -> TypedSymbol 'AnyKind t
typedAnySymbol' PhantomDict t
forall a. SupportedPrim a => PhantomDict a
getPhantomDict
{-# INLINE typedAnySymbol #-}

{-# NOINLINE typedAnySymbol' #-}
typedAnySymbol' ::
  forall t. PhantomDict t -> Symbol -> TypedSymbol 'AnyKind t
typedAnySymbol' :: forall t. PhantomDict t -> Symbol -> TypedSymbol 'AnyKind t
typedAnySymbol' PhantomDict t
PhantomDict Symbol
symbol = Symbol -> TypedSymbol 'AnyKind t
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
symbol

-- | Constant symbol
type TypedConstantSymbol = TypedSymbol 'ConstantKind

-- | Any symbol
type TypedAnySymbol = TypedSymbol 'AnyKind

instance Eq (TypedSymbol knd t) where
  TypedSymbol Symbol
x == :: TypedSymbol knd t -> TypedSymbol knd t -> Bool
== TypedSymbol Symbol
y = Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
y

instance Ord (TypedSymbol knd t) where
  TypedSymbol Symbol
x <= :: TypedSymbol knd t -> TypedSymbol knd t -> Bool
<= TypedSymbol Symbol
y = Symbol
x Symbol -> Symbol -> Bool
forall a. Ord a => a -> a -> Bool
<= Symbol
y

instance Lift (TypedSymbol knd t) where
  liftTyped :: forall (m :: * -> *).
Quote m =>
TypedSymbol knd t -> Code m (TypedSymbol knd t)
liftTyped (TypedSymbol Symbol
x) = [||Symbol -> TypedSymbol knd t
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
x||]

instance Show (TypedSymbol knd t) where
  show :: TypedSymbol knd t -> String
show (TypedSymbol Symbol
symbol) = Symbol -> String
forall a. Show a => a -> String
show Symbol
symbol String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep t -> String
forall a. Show a => a -> String
show (forall t. SupportedPrim t => TypeRep t
primTypeRep @t)

-- | Show a typed symbol without the type information.
showUntyped :: TypedSymbol knd t -> String
showUntyped :: forall (knd :: SymbolKind) t. TypedSymbol knd t -> String
showUntyped (TypedSymbol Symbol
symbol) = Symbol -> String
forall a. Show a => a -> String
show Symbol
symbol

instance Hashable (TypedSymbol knd t) where
  Int
s hashWithSalt :: Int -> TypedSymbol knd t -> Int
`hashWithSalt` TypedSymbol Symbol
x = Int
s Int -> Symbol -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Symbol
x

instance NFData (TypedSymbol knd t) where
  rnf :: TypedSymbol knd t -> ()
rnf (TypedSymbol Symbol
str) = Symbol -> ()
forall a. NFData a => a -> ()
rnf Symbol
str

instance
  ( SupportedPrim t,
    SymbolKindConstraint knd t,
    IsSymbolKind knd
  ) =>
  IsString (TypedSymbol knd t)
  where
  fromString :: String -> TypedSymbol knd t
fromString = Symbol -> TypedSymbol knd t
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol (Symbol -> TypedSymbol knd t)
-> (String -> Symbol) -> String -> TypedSymbol knd t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Symbol
forall a. IsString a => String -> a
fromString

-- | Introduce the 'SupportedPrim' constraint from the t'TypedSymbol'.
withSymbolSupported ::
  forall knd t a.
  TypedSymbol knd t ->
  ((SupportedPrim t, Typeable t) => a) ->
  a
withSymbolSupported :: forall (knd :: SymbolKind) t a.
TypedSymbol knd t -> ((SupportedPrim t, Typeable t) => a) -> a
withSymbolSupported (TypedSymbol Symbol
_) (SupportedPrim t, Typeable t) => a
a =
  forall a b. SupportedPrim a => (Typeable a => b) -> b
withSupportedPrimTypeable @t ((Typeable t => a) -> a) -> (Typeable t => a) -> a
forall a b. (a -> b) -> a -> b
$ a
Typeable t => a
(SupportedPrim t, Typeable t) => a
a
{-# INLINE withSymbolSupported #-}

-- | Introduce the 'SupportedPrim' constraint from the t'TypedSymbol'.
withConstantSymbolSupported ::
  forall t a.
  TypedSymbol 'ConstantKind t ->
  ((SupportedNonFuncPrim t, Typeable t) => a) ->
  a
withConstantSymbolSupported :: forall t a.
TypedSymbol 'ConstantKind t
-> ((SupportedNonFuncPrim t, Typeable t) => a) -> a
withConstantSymbolSupported (TypedSymbol Symbol
_) (SupportedNonFuncPrim t, Typeable t) => a
a =
  forall a b. SupportedPrim a => (Typeable a => b) -> b
withSupportedPrimTypeable @t ((Typeable t => a) -> a) -> (Typeable t => a) -> a
forall a b. (a -> b) -> a -> b
$ a
Typeable t => a
(SupportedNonFuncPrim t, Typeable t) => a
a
{-# INLINE withConstantSymbolSupported #-}

-- | Introduce the 'IsSymbolKind' constraint from the t'TypedSymbol'.
withSymbolKind :: TypedSymbol knd t -> ((IsSymbolKind knd) => a) -> a
withSymbolKind :: forall (knd :: SymbolKind) t a.
TypedSymbol knd t -> (IsSymbolKind knd => a) -> a
withSymbolKind (TypedSymbol Symbol
_) IsSymbolKind knd => a
a = a
IsSymbolKind knd => a
a
{-# INLINE withSymbolKind #-}

-- | A non-indexed symbol. Type information are checked at runtime.
data SomeTypedSymbol knd where
  SomeTypedSymbol ::
    forall knd t.
    TypedSymbol knd t ->
    SomeTypedSymbol knd

-- | Non-indexed constant symbol
type SomeTypedConstantSymbol = SomeTypedSymbol 'ConstantKind

-- | Non-indexed any symbol
type SomeTypedAnySymbol = SomeTypedSymbol 'AnyKind

instance NFData (SomeTypedSymbol knd) where
  rnf :: SomeTypedSymbol knd -> ()
rnf (SomeTypedSymbol TypedSymbol knd t
s) = TypedSymbol knd t -> ()
forall a. NFData a => a -> ()
rnf TypedSymbol knd t
s
  {-# INLINE rnf #-}

instance Lift (SomeTypedSymbol knd) where
  liftTyped :: forall (m :: * -> *).
Quote m =>
SomeTypedSymbol knd -> Code m (SomeTypedSymbol knd)
liftTyped (SomeTypedSymbol TypedSymbol knd t
s) = [||TypedSymbol knd t -> SomeTypedSymbol knd
forall (knd :: SymbolKind) a.
TypedSymbol knd a -> SomeTypedSymbol knd
SomeTypedSymbol TypedSymbol knd t
s||]

instance Eq (SomeTypedSymbol knd) where
  (SomeTypedSymbol (TypedSymbol knd t
s1 :: TypedSymbol knd a))
    == :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Bool
== (SomeTypedSymbol (TypedSymbol knd t
s2 :: TypedSymbol knd b)) =
      TypedSymbol knd t
-> ((SupportedPrim t, Typeable t) => Bool) -> Bool
forall (knd :: SymbolKind) t a.
TypedSymbol knd t -> ((SupportedPrim t, Typeable t) => a) -> a
withSymbolSupported TypedSymbol knd t
s1 (((SupportedPrim t, Typeable t) => Bool) -> Bool)
-> ((SupportedPrim t, Typeable t) => Bool) -> Bool
forall a b. (a -> b) -> a -> b
$
        TypedSymbol knd t
-> ((SupportedPrim t, Typeable t) => Bool) -> Bool
forall (knd :: SymbolKind) t a.
TypedSymbol knd t -> ((SupportedPrim t, Typeable t) => a) -> a
withSymbolSupported TypedSymbol knd t
s2 (((SupportedPrim t, Typeable t) => Bool) -> Bool)
-> ((SupportedPrim t, Typeable t) => Bool) -> Bool
forall a b. (a -> b) -> a -> b
$
          case TypeRep t -> TypeRep t -> Maybe (t :~~: t)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall t. SupportedPrim t => TypeRep t
primTypeRep @a) (forall t. SupportedPrim t => TypeRep t
primTypeRep @b) of
            Just t :~~: t
HRefl -> TypedSymbol knd t
s1 TypedSymbol knd t -> TypedSymbol knd t -> Bool
forall a. Eq a => a -> a -> Bool
== TypedSymbol knd t
TypedSymbol knd t
s2
            Maybe (t :~~: t)
_ -> Bool
False
  {-# INLINE (==) #-}

instance Ord (SomeTypedSymbol knd) where
  (SomeTypedSymbol (TypedSymbol knd t
s1 :: TypedSymbol knd a))
    <= :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Bool
<= (SomeTypedSymbol (TypedSymbol knd t
s2 :: TypedSymbol knd b)) =
      TypedSymbol knd t
-> ((SupportedPrim t, Typeable t) => Bool) -> Bool
forall (knd :: SymbolKind) t a.
TypedSymbol knd t -> ((SupportedPrim t, Typeable t) => a) -> a
withSymbolSupported TypedSymbol knd t
s1 (((SupportedPrim t, Typeable t) => Bool) -> Bool)
-> ((SupportedPrim t, Typeable t) => Bool) -> Bool
forall a b. (a -> b) -> a -> b
$
        TypedSymbol knd t
-> ((SupportedPrim t, Typeable t) => Bool) -> Bool
forall (knd :: SymbolKind) t a.
TypedSymbol knd t -> ((SupportedPrim t, Typeable t) => a) -> a
withSymbolSupported TypedSymbol knd t
s2 (((SupportedPrim t, Typeable t) => Bool) -> Bool)
-> ((SupportedPrim t, Typeable t) => Bool) -> Bool
forall a b. (a -> b) -> a -> b
$
          let t1 :: TypeRep t
t1 = forall t. SupportedPrim t => TypeRep t
primTypeRep @a
              t2 :: TypeRep t
t2 = forall t. SupportedPrim t => TypeRep t
primTypeRep @b
           in TypeRep t -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep t
t1 SomeTypeRep -> SomeTypeRep -> Bool
forall a. Ord a => a -> a -> Bool
< TypeRep t -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep t
t2
                Bool -> Bool -> Bool
|| ( case TypeRep t -> TypeRep t -> Maybe (t :~~: t)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep t
t1 TypeRep t
t2 of
                       Just t :~~: t
HRefl -> TypedSymbol knd t
s1 TypedSymbol knd t -> TypedSymbol knd t -> Bool
forall a. Ord a => a -> a -> Bool
<= TypedSymbol knd t
TypedSymbol knd t
s2
                       Maybe (t :~~: t)
_ -> Bool
False
                   )

instance Hashable (SomeTypedSymbol knd) where
  hashWithSalt :: Int -> SomeTypedSymbol knd -> Int
hashWithSalt Int
s (SomeTypedSymbol TypedSymbol knd t
s1) = Int
s Int -> TypedSymbol knd t -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedSymbol knd t
s1
  {-# INLINE hashWithSalt #-}

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

-- | Construct a t'SomeTypedSymbol' from a t'TypedSymbol'.
someTypedSymbol :: forall knd t. TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol :: forall (knd :: SymbolKind) a.
TypedSymbol knd a -> SomeTypedSymbol knd
someTypedSymbol s :: TypedSymbol knd t
s@(TypedSymbol Symbol
_) = TypedSymbol knd t -> SomeTypedSymbol knd
forall (knd :: SymbolKind) a.
TypedSymbol knd a -> SomeTypedSymbol knd
SomeTypedSymbol TypedSymbol knd t
s
{-# INLINE someTypedSymbol #-}

-- Terms

-- | Traits for IEEE floating point numbers.
data FPTrait
  = FPIsNaN
  | FPIsPositive
  | FPIsNegative
  | FPIsPositiveInfinite
  | FPIsNegativeInfinite
  | FPIsInfinite
  | FPIsPositiveZero
  | FPIsNegativeZero
  | FPIsZero
  | FPIsNormal
  | FPIsSubnormal
  | FPIsPoint
  deriving (FPTrait -> FPTrait -> Bool
(FPTrait -> FPTrait -> Bool)
-> (FPTrait -> FPTrait -> Bool) -> Eq FPTrait
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FPTrait -> FPTrait -> Bool
== :: FPTrait -> FPTrait -> Bool
$c/= :: FPTrait -> FPTrait -> Bool
/= :: FPTrait -> FPTrait -> Bool
Eq, Eq FPTrait
Eq FPTrait =>
(FPTrait -> FPTrait -> Ordering)
-> (FPTrait -> FPTrait -> Bool)
-> (FPTrait -> FPTrait -> Bool)
-> (FPTrait -> FPTrait -> Bool)
-> (FPTrait -> FPTrait -> Bool)
-> (FPTrait -> FPTrait -> FPTrait)
-> (FPTrait -> FPTrait -> FPTrait)
-> Ord FPTrait
FPTrait -> FPTrait -> Bool
FPTrait -> FPTrait -> Ordering
FPTrait -> FPTrait -> FPTrait
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FPTrait -> FPTrait -> Ordering
compare :: FPTrait -> FPTrait -> Ordering
$c< :: FPTrait -> FPTrait -> Bool
< :: FPTrait -> FPTrait -> Bool
$c<= :: FPTrait -> FPTrait -> Bool
<= :: FPTrait -> FPTrait -> Bool
$c> :: FPTrait -> FPTrait -> Bool
> :: FPTrait -> FPTrait -> Bool
$c>= :: FPTrait -> FPTrait -> Bool
>= :: FPTrait -> FPTrait -> Bool
$cmax :: FPTrait -> FPTrait -> FPTrait
max :: FPTrait -> FPTrait -> FPTrait
$cmin :: FPTrait -> FPTrait -> FPTrait
min :: FPTrait -> FPTrait -> FPTrait
Ord, (forall x. FPTrait -> Rep FPTrait x)
-> (forall x. Rep FPTrait x -> FPTrait) -> Generic FPTrait
forall x. Rep FPTrait x -> FPTrait
forall x. FPTrait -> Rep FPTrait x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FPTrait -> Rep FPTrait x
from :: forall x. FPTrait -> Rep FPTrait x
$cto :: forall x. Rep FPTrait x -> FPTrait
to :: forall x. Rep FPTrait x -> FPTrait
Generic, Eq FPTrait
Eq FPTrait =>
(Int -> FPTrait -> Int) -> (FPTrait -> Int) -> Hashable FPTrait
Int -> FPTrait -> Int
FPTrait -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> FPTrait -> Int
hashWithSalt :: Int -> FPTrait -> Int
$chash :: FPTrait -> Int
hash :: FPTrait -> Int
Hashable, (forall (m :: * -> *). Quote m => FPTrait -> m Exp)
-> (forall (m :: * -> *). Quote m => FPTrait -> Code m FPTrait)
-> Lift FPTrait
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => FPTrait -> m Exp
forall (m :: * -> *). Quote m => FPTrait -> Code m FPTrait
$clift :: forall (m :: * -> *). Quote m => FPTrait -> m Exp
lift :: forall (m :: * -> *). Quote m => FPTrait -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => FPTrait -> Code m FPTrait
liftTyped :: forall (m :: * -> *). Quote m => FPTrait -> Code m FPTrait
Lift, FPTrait -> ()
(FPTrait -> ()) -> NFData FPTrait
forall a. (a -> ()) -> NFData a
$crnf :: FPTrait -> ()
rnf :: FPTrait -> ()
NFData, (forall (m :: * -> *). MonadPut m => FPTrait -> m ())
-> (forall (m :: * -> *). MonadGet m => m FPTrait)
-> Serial FPTrait
forall a.
(forall (m :: * -> *). MonadPut m => a -> m ())
-> (forall (m :: * -> *). MonadGet m => m a) -> Serial a
forall (m :: * -> *). MonadGet m => m FPTrait
forall (m :: * -> *). MonadPut m => FPTrait -> m ()
$cserialize :: forall (m :: * -> *). MonadPut m => FPTrait -> m ()
serialize :: forall (m :: * -> *). MonadPut m => FPTrait -> m ()
$cdeserialize :: forall (m :: * -> *). MonadGet m => m FPTrait
deserialize :: forall (m :: * -> *). MonadGet m => m FPTrait
Serial)

instance Cereal.Serialize FPTrait where
  put :: Putter FPTrait
put = Putter FPTrait
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => FPTrait -> m ()
serialize
  get :: Get FPTrait
get = Get FPTrait
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m FPTrait
deserialize

instance Binary.Binary FPTrait where
  put :: FPTrait -> Put
put = FPTrait -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => FPTrait -> m ()
serialize
  get :: Get FPTrait
get = Get FPTrait
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m FPTrait
deserialize

instance Show FPTrait where
  show :: FPTrait -> String
show FPTrait
FPIsNaN = String
"is_nan"
  show FPTrait
FPIsPositive = String
"is_pos"
  show FPTrait
FPIsNegative = String
"is_neg"
  show FPTrait
FPIsPositiveInfinite = String
"is_pos_inf"
  show FPTrait
FPIsNegativeInfinite = String
"is_neg_inf"
  show FPTrait
FPIsInfinite = String
"is_inf"
  show FPTrait
FPIsPositiveZero = String
"is_pos_zero"
  show FPTrait
FPIsNegativeZero = String
"is_neg_zero"
  show FPTrait
FPIsZero = String
"is_zero"
  show FPTrait
FPIsNormal = String
"is_normal"
  show FPTrait
FPIsSubnormal = String
"is_subnormal"
  show FPTrait
FPIsPoint = String
"is_point"

-- | Unary floating point operations.
data FPUnaryOp = FPAbs | FPNeg
  deriving (FPUnaryOp -> FPUnaryOp -> Bool
(FPUnaryOp -> FPUnaryOp -> Bool)
-> (FPUnaryOp -> FPUnaryOp -> Bool) -> Eq FPUnaryOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FPUnaryOp -> FPUnaryOp -> Bool
== :: FPUnaryOp -> FPUnaryOp -> Bool
$c/= :: FPUnaryOp -> FPUnaryOp -> Bool
/= :: FPUnaryOp -> FPUnaryOp -> Bool
Eq, Eq FPUnaryOp
Eq FPUnaryOp =>
(FPUnaryOp -> FPUnaryOp -> Ordering)
-> (FPUnaryOp -> FPUnaryOp -> Bool)
-> (FPUnaryOp -> FPUnaryOp -> Bool)
-> (FPUnaryOp -> FPUnaryOp -> Bool)
-> (FPUnaryOp -> FPUnaryOp -> Bool)
-> (FPUnaryOp -> FPUnaryOp -> FPUnaryOp)
-> (FPUnaryOp -> FPUnaryOp -> FPUnaryOp)
-> Ord FPUnaryOp
FPUnaryOp -> FPUnaryOp -> Bool
FPUnaryOp -> FPUnaryOp -> Ordering
FPUnaryOp -> FPUnaryOp -> FPUnaryOp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FPUnaryOp -> FPUnaryOp -> Ordering
compare :: FPUnaryOp -> FPUnaryOp -> Ordering
$c< :: FPUnaryOp -> FPUnaryOp -> Bool
< :: FPUnaryOp -> FPUnaryOp -> Bool
$c<= :: FPUnaryOp -> FPUnaryOp -> Bool
<= :: FPUnaryOp -> FPUnaryOp -> Bool
$c> :: FPUnaryOp -> FPUnaryOp -> Bool
> :: FPUnaryOp -> FPUnaryOp -> Bool
$c>= :: FPUnaryOp -> FPUnaryOp -> Bool
>= :: FPUnaryOp -> FPUnaryOp -> Bool
$cmax :: FPUnaryOp -> FPUnaryOp -> FPUnaryOp
max :: FPUnaryOp -> FPUnaryOp -> FPUnaryOp
$cmin :: FPUnaryOp -> FPUnaryOp -> FPUnaryOp
min :: FPUnaryOp -> FPUnaryOp -> FPUnaryOp
Ord, (forall x. FPUnaryOp -> Rep FPUnaryOp x)
-> (forall x. Rep FPUnaryOp x -> FPUnaryOp) -> Generic FPUnaryOp
forall x. Rep FPUnaryOp x -> FPUnaryOp
forall x. FPUnaryOp -> Rep FPUnaryOp x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FPUnaryOp -> Rep FPUnaryOp x
from :: forall x. FPUnaryOp -> Rep FPUnaryOp x
$cto :: forall x. Rep FPUnaryOp x -> FPUnaryOp
to :: forall x. Rep FPUnaryOp x -> FPUnaryOp
Generic, Eq FPUnaryOp
Eq FPUnaryOp =>
(Int -> FPUnaryOp -> Int)
-> (FPUnaryOp -> Int) -> Hashable FPUnaryOp
Int -> FPUnaryOp -> Int
FPUnaryOp -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> FPUnaryOp -> Int
hashWithSalt :: Int -> FPUnaryOp -> Int
$chash :: FPUnaryOp -> Int
hash :: FPUnaryOp -> Int
Hashable, (forall (m :: * -> *). Quote m => FPUnaryOp -> m Exp)
-> (forall (m :: * -> *). Quote m => FPUnaryOp -> Code m FPUnaryOp)
-> Lift FPUnaryOp
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => FPUnaryOp -> m Exp
forall (m :: * -> *). Quote m => FPUnaryOp -> Code m FPUnaryOp
$clift :: forall (m :: * -> *). Quote m => FPUnaryOp -> m Exp
lift :: forall (m :: * -> *). Quote m => FPUnaryOp -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => FPUnaryOp -> Code m FPUnaryOp
liftTyped :: forall (m :: * -> *). Quote m => FPUnaryOp -> Code m FPUnaryOp
Lift, FPUnaryOp -> ()
(FPUnaryOp -> ()) -> NFData FPUnaryOp
forall a. (a -> ()) -> NFData a
$crnf :: FPUnaryOp -> ()
rnf :: FPUnaryOp -> ()
NFData, (forall (m :: * -> *). MonadPut m => FPUnaryOp -> m ())
-> (forall (m :: * -> *). MonadGet m => m FPUnaryOp)
-> Serial FPUnaryOp
forall a.
(forall (m :: * -> *). MonadPut m => a -> m ())
-> (forall (m :: * -> *). MonadGet m => m a) -> Serial a
forall (m :: * -> *). MonadGet m => m FPUnaryOp
forall (m :: * -> *). MonadPut m => FPUnaryOp -> m ()
$cserialize :: forall (m :: * -> *). MonadPut m => FPUnaryOp -> m ()
serialize :: forall (m :: * -> *). MonadPut m => FPUnaryOp -> m ()
$cdeserialize :: forall (m :: * -> *). MonadGet m => m FPUnaryOp
deserialize :: forall (m :: * -> *). MonadGet m => m FPUnaryOp
Serial)

instance Cereal.Serialize FPUnaryOp where
  put :: Putter FPUnaryOp
put = Putter FPUnaryOp
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => FPUnaryOp -> m ()
serialize
  get :: Get FPUnaryOp
get = Get FPUnaryOp
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m FPUnaryOp
deserialize

instance Binary.Binary FPUnaryOp where
  put :: FPUnaryOp -> Put
put = FPUnaryOp -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => FPUnaryOp -> m ()
serialize
  get :: Get FPUnaryOp
get = Get FPUnaryOp
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m FPUnaryOp
deserialize

instance Show FPUnaryOp where
  show :: FPUnaryOp -> String
show FPUnaryOp
FPAbs = String
"fp.abs"
  show FPUnaryOp
FPNeg = String
"fp.neg"

-- | Binary floating point operations.
data FPBinaryOp
  = FPRem
  | FPMinimum
  | FPMinimumNumber
  | FPMaximum
  | FPMaximumNumber
  deriving (FPBinaryOp -> FPBinaryOp -> Bool
(FPBinaryOp -> FPBinaryOp -> Bool)
-> (FPBinaryOp -> FPBinaryOp -> Bool) -> Eq FPBinaryOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FPBinaryOp -> FPBinaryOp -> Bool
== :: FPBinaryOp -> FPBinaryOp -> Bool
$c/= :: FPBinaryOp -> FPBinaryOp -> Bool
/= :: FPBinaryOp -> FPBinaryOp -> Bool
Eq, Eq FPBinaryOp
Eq FPBinaryOp =>
(FPBinaryOp -> FPBinaryOp -> Ordering)
-> (FPBinaryOp -> FPBinaryOp -> Bool)
-> (FPBinaryOp -> FPBinaryOp -> Bool)
-> (FPBinaryOp -> FPBinaryOp -> Bool)
-> (FPBinaryOp -> FPBinaryOp -> Bool)
-> (FPBinaryOp -> FPBinaryOp -> FPBinaryOp)
-> (FPBinaryOp -> FPBinaryOp -> FPBinaryOp)
-> Ord FPBinaryOp
FPBinaryOp -> FPBinaryOp -> Bool
FPBinaryOp -> FPBinaryOp -> Ordering
FPBinaryOp -> FPBinaryOp -> FPBinaryOp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FPBinaryOp -> FPBinaryOp -> Ordering
compare :: FPBinaryOp -> FPBinaryOp -> Ordering
$c< :: FPBinaryOp -> FPBinaryOp -> Bool
< :: FPBinaryOp -> FPBinaryOp -> Bool
$c<= :: FPBinaryOp -> FPBinaryOp -> Bool
<= :: FPBinaryOp -> FPBinaryOp -> Bool
$c> :: FPBinaryOp -> FPBinaryOp -> Bool
> :: FPBinaryOp -> FPBinaryOp -> Bool
$c>= :: FPBinaryOp -> FPBinaryOp -> Bool
>= :: FPBinaryOp -> FPBinaryOp -> Bool
$cmax :: FPBinaryOp -> FPBinaryOp -> FPBinaryOp
max :: FPBinaryOp -> FPBinaryOp -> FPBinaryOp
$cmin :: FPBinaryOp -> FPBinaryOp -> FPBinaryOp
min :: FPBinaryOp -> FPBinaryOp -> FPBinaryOp
Ord, (forall x. FPBinaryOp -> Rep FPBinaryOp x)
-> (forall x. Rep FPBinaryOp x -> FPBinaryOp) -> Generic FPBinaryOp
forall x. Rep FPBinaryOp x -> FPBinaryOp
forall x. FPBinaryOp -> Rep FPBinaryOp x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FPBinaryOp -> Rep FPBinaryOp x
from :: forall x. FPBinaryOp -> Rep FPBinaryOp x
$cto :: forall x. Rep FPBinaryOp x -> FPBinaryOp
to :: forall x. Rep FPBinaryOp x -> FPBinaryOp
Generic, Eq FPBinaryOp
Eq FPBinaryOp =>
(Int -> FPBinaryOp -> Int)
-> (FPBinaryOp -> Int) -> Hashable FPBinaryOp
Int -> FPBinaryOp -> Int
FPBinaryOp -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> FPBinaryOp -> Int
hashWithSalt :: Int -> FPBinaryOp -> Int
$chash :: FPBinaryOp -> Int
hash :: FPBinaryOp -> Int
Hashable, (forall (m :: * -> *). Quote m => FPBinaryOp -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    FPBinaryOp -> Code m FPBinaryOp)
-> Lift FPBinaryOp
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => FPBinaryOp -> m Exp
forall (m :: * -> *). Quote m => FPBinaryOp -> Code m FPBinaryOp
$clift :: forall (m :: * -> *). Quote m => FPBinaryOp -> m Exp
lift :: forall (m :: * -> *). Quote m => FPBinaryOp -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => FPBinaryOp -> Code m FPBinaryOp
liftTyped :: forall (m :: * -> *). Quote m => FPBinaryOp -> Code m FPBinaryOp
Lift, FPBinaryOp -> ()
(FPBinaryOp -> ()) -> NFData FPBinaryOp
forall a. (a -> ()) -> NFData a
$crnf :: FPBinaryOp -> ()
rnf :: FPBinaryOp -> ()
NFData, (forall (m :: * -> *). MonadPut m => FPBinaryOp -> m ())
-> (forall (m :: * -> *). MonadGet m => m FPBinaryOp)
-> Serial FPBinaryOp
forall a.
(forall (m :: * -> *). MonadPut m => a -> m ())
-> (forall (m :: * -> *). MonadGet m => m a) -> Serial a
forall (m :: * -> *). MonadGet m => m FPBinaryOp
forall (m :: * -> *). MonadPut m => FPBinaryOp -> m ()
$cserialize :: forall (m :: * -> *). MonadPut m => FPBinaryOp -> m ()
serialize :: forall (m :: * -> *). MonadPut m => FPBinaryOp -> m ()
$cdeserialize :: forall (m :: * -> *). MonadGet m => m FPBinaryOp
deserialize :: forall (m :: * -> *). MonadGet m => m FPBinaryOp
Serial)

instance Cereal.Serialize FPBinaryOp where
  put :: Putter FPBinaryOp
put = Putter FPBinaryOp
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => FPBinaryOp -> m ()
serialize
  get :: Get FPBinaryOp
get = Get FPBinaryOp
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m FPBinaryOp
deserialize

instance Binary.Binary FPBinaryOp where
  put :: FPBinaryOp -> Put
put = FPBinaryOp -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => FPBinaryOp -> m ()
serialize
  get :: Get FPBinaryOp
get = Get FPBinaryOp
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m FPBinaryOp
deserialize

instance Show FPBinaryOp where
  show :: FPBinaryOp -> String
show FPBinaryOp
FPRem = String
"fp.rem"
  show FPBinaryOp
FPMinimum = String
"fp.minimum"
  show FPBinaryOp
FPMinimumNumber = String
"fp.minimumNumber"
  show FPBinaryOp
FPMaximum = String
"fp.maximum"
  show FPBinaryOp
FPMaximumNumber = String
"fp.maximumNumber"

-- | Unary floating point operations with rounding modes.
data FPRoundingUnaryOp = FPSqrt | FPRoundToIntegral
  deriving (FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool
(FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool)
-> (FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool)
-> Eq FPRoundingUnaryOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool
== :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool
$c/= :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool
/= :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool
Eq, Eq FPRoundingUnaryOp
Eq FPRoundingUnaryOp =>
(FPRoundingUnaryOp -> FPRoundingUnaryOp -> Ordering)
-> (FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool)
-> (FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool)
-> (FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool)
-> (FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool)
-> (FPRoundingUnaryOp -> FPRoundingUnaryOp -> FPRoundingUnaryOp)
-> (FPRoundingUnaryOp -> FPRoundingUnaryOp -> FPRoundingUnaryOp)
-> Ord FPRoundingUnaryOp
FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool
FPRoundingUnaryOp -> FPRoundingUnaryOp -> Ordering
FPRoundingUnaryOp -> FPRoundingUnaryOp -> FPRoundingUnaryOp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Ordering
compare :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Ordering
$c< :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool
< :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool
$c<= :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool
<= :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool
$c> :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool
> :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool
$c>= :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool
>= :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool
$cmax :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> FPRoundingUnaryOp
max :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> FPRoundingUnaryOp
$cmin :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> FPRoundingUnaryOp
min :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> FPRoundingUnaryOp
Ord, (forall x. FPRoundingUnaryOp -> Rep FPRoundingUnaryOp x)
-> (forall x. Rep FPRoundingUnaryOp x -> FPRoundingUnaryOp)
-> Generic FPRoundingUnaryOp
forall x. Rep FPRoundingUnaryOp x -> FPRoundingUnaryOp
forall x. FPRoundingUnaryOp -> Rep FPRoundingUnaryOp x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FPRoundingUnaryOp -> Rep FPRoundingUnaryOp x
from :: forall x. FPRoundingUnaryOp -> Rep FPRoundingUnaryOp x
$cto :: forall x. Rep FPRoundingUnaryOp x -> FPRoundingUnaryOp
to :: forall x. Rep FPRoundingUnaryOp x -> FPRoundingUnaryOp
Generic, Eq FPRoundingUnaryOp
Eq FPRoundingUnaryOp =>
(Int -> FPRoundingUnaryOp -> Int)
-> (FPRoundingUnaryOp -> Int) -> Hashable FPRoundingUnaryOp
Int -> FPRoundingUnaryOp -> Int
FPRoundingUnaryOp -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> FPRoundingUnaryOp -> Int
hashWithSalt :: Int -> FPRoundingUnaryOp -> Int
$chash :: FPRoundingUnaryOp -> Int
hash :: FPRoundingUnaryOp -> Int
Hashable, (forall (m :: * -> *). Quote m => FPRoundingUnaryOp -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    FPRoundingUnaryOp -> Code m FPRoundingUnaryOp)
-> Lift FPRoundingUnaryOp
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => FPRoundingUnaryOp -> m Exp
forall (m :: * -> *).
Quote m =>
FPRoundingUnaryOp -> Code m FPRoundingUnaryOp
$clift :: forall (m :: * -> *). Quote m => FPRoundingUnaryOp -> m Exp
lift :: forall (m :: * -> *). Quote m => FPRoundingUnaryOp -> m Exp
$cliftTyped :: forall (m :: * -> *).
Quote m =>
FPRoundingUnaryOp -> Code m FPRoundingUnaryOp
liftTyped :: forall (m :: * -> *).
Quote m =>
FPRoundingUnaryOp -> Code m FPRoundingUnaryOp
Lift, FPRoundingUnaryOp -> ()
(FPRoundingUnaryOp -> ()) -> NFData FPRoundingUnaryOp
forall a. (a -> ()) -> NFData a
$crnf :: FPRoundingUnaryOp -> ()
rnf :: FPRoundingUnaryOp -> ()
NFData, (forall (m :: * -> *). MonadPut m => FPRoundingUnaryOp -> m ())
-> (forall (m :: * -> *). MonadGet m => m FPRoundingUnaryOp)
-> Serial FPRoundingUnaryOp
forall a.
(forall (m :: * -> *). MonadPut m => a -> m ())
-> (forall (m :: * -> *). MonadGet m => m a) -> Serial a
forall (m :: * -> *). MonadGet m => m FPRoundingUnaryOp
forall (m :: * -> *). MonadPut m => FPRoundingUnaryOp -> m ()
$cserialize :: forall (m :: * -> *). MonadPut m => FPRoundingUnaryOp -> m ()
serialize :: forall (m :: * -> *). MonadPut m => FPRoundingUnaryOp -> m ()
$cdeserialize :: forall (m :: * -> *). MonadGet m => m FPRoundingUnaryOp
deserialize :: forall (m :: * -> *). MonadGet m => m FPRoundingUnaryOp
Serial)

instance Cereal.Serialize FPRoundingUnaryOp where
  put :: Putter FPRoundingUnaryOp
put = Putter FPRoundingUnaryOp
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => FPRoundingUnaryOp -> m ()
serialize
  get :: Get FPRoundingUnaryOp
get = Get FPRoundingUnaryOp
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m FPRoundingUnaryOp
deserialize

instance Binary.Binary FPRoundingUnaryOp where
  put :: FPRoundingUnaryOp -> Put
put = FPRoundingUnaryOp -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => FPRoundingUnaryOp -> m ()
serialize
  get :: Get FPRoundingUnaryOp
get = Get FPRoundingUnaryOp
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m FPRoundingUnaryOp
deserialize

instance Show FPRoundingUnaryOp where
  show :: FPRoundingUnaryOp -> String
show FPRoundingUnaryOp
FPSqrt = String
"fp.sqrt"
  show FPRoundingUnaryOp
FPRoundToIntegral = String
"fp.roundToIntegral"

-- | Binary floating point operations with rounding modes.
data FPRoundingBinaryOp = FPAdd | FPSub | FPMul | FPDiv
  deriving (FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool
(FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool)
-> (FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool)
-> Eq FPRoundingBinaryOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool
== :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool
$c/= :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool
/= :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool
Eq, Eq FPRoundingBinaryOp
Eq FPRoundingBinaryOp =>
(FPRoundingBinaryOp -> FPRoundingBinaryOp -> Ordering)
-> (FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool)
-> (FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool)
-> (FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool)
-> (FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool)
-> (FPRoundingBinaryOp -> FPRoundingBinaryOp -> FPRoundingBinaryOp)
-> (FPRoundingBinaryOp -> FPRoundingBinaryOp -> FPRoundingBinaryOp)
-> Ord FPRoundingBinaryOp
FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool
FPRoundingBinaryOp -> FPRoundingBinaryOp -> Ordering
FPRoundingBinaryOp -> FPRoundingBinaryOp -> FPRoundingBinaryOp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Ordering
compare :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Ordering
$c< :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool
< :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool
$c<= :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool
<= :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool
$c> :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool
> :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool
$c>= :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool
>= :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool
$cmax :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> FPRoundingBinaryOp
max :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> FPRoundingBinaryOp
$cmin :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> FPRoundingBinaryOp
min :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> FPRoundingBinaryOp
Ord, (forall x. FPRoundingBinaryOp -> Rep FPRoundingBinaryOp x)
-> (forall x. Rep FPRoundingBinaryOp x -> FPRoundingBinaryOp)
-> Generic FPRoundingBinaryOp
forall x. Rep FPRoundingBinaryOp x -> FPRoundingBinaryOp
forall x. FPRoundingBinaryOp -> Rep FPRoundingBinaryOp x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FPRoundingBinaryOp -> Rep FPRoundingBinaryOp x
from :: forall x. FPRoundingBinaryOp -> Rep FPRoundingBinaryOp x
$cto :: forall x. Rep FPRoundingBinaryOp x -> FPRoundingBinaryOp
to :: forall x. Rep FPRoundingBinaryOp x -> FPRoundingBinaryOp
Generic, Eq FPRoundingBinaryOp
Eq FPRoundingBinaryOp =>
(Int -> FPRoundingBinaryOp -> Int)
-> (FPRoundingBinaryOp -> Int) -> Hashable FPRoundingBinaryOp
Int -> FPRoundingBinaryOp -> Int
FPRoundingBinaryOp -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> FPRoundingBinaryOp -> Int
hashWithSalt :: Int -> FPRoundingBinaryOp -> Int
$chash :: FPRoundingBinaryOp -> Int
hash :: FPRoundingBinaryOp -> Int
Hashable, (forall (m :: * -> *). Quote m => FPRoundingBinaryOp -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    FPRoundingBinaryOp -> Code m FPRoundingBinaryOp)
-> Lift FPRoundingBinaryOp
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => FPRoundingBinaryOp -> m Exp
forall (m :: * -> *).
Quote m =>
FPRoundingBinaryOp -> Code m FPRoundingBinaryOp
$clift :: forall (m :: * -> *). Quote m => FPRoundingBinaryOp -> m Exp
lift :: forall (m :: * -> *). Quote m => FPRoundingBinaryOp -> m Exp
$cliftTyped :: forall (m :: * -> *).
Quote m =>
FPRoundingBinaryOp -> Code m FPRoundingBinaryOp
liftTyped :: forall (m :: * -> *).
Quote m =>
FPRoundingBinaryOp -> Code m FPRoundingBinaryOp
Lift, FPRoundingBinaryOp -> ()
(FPRoundingBinaryOp -> ()) -> NFData FPRoundingBinaryOp
forall a. (a -> ()) -> NFData a
$crnf :: FPRoundingBinaryOp -> ()
rnf :: FPRoundingBinaryOp -> ()
NFData, (forall (m :: * -> *). MonadPut m => FPRoundingBinaryOp -> m ())
-> (forall (m :: * -> *). MonadGet m => m FPRoundingBinaryOp)
-> Serial FPRoundingBinaryOp
forall a.
(forall (m :: * -> *). MonadPut m => a -> m ())
-> (forall (m :: * -> *). MonadGet m => m a) -> Serial a
forall (m :: * -> *). MonadGet m => m FPRoundingBinaryOp
forall (m :: * -> *). MonadPut m => FPRoundingBinaryOp -> m ()
$cserialize :: forall (m :: * -> *). MonadPut m => FPRoundingBinaryOp -> m ()
serialize :: forall (m :: * -> *). MonadPut m => FPRoundingBinaryOp -> m ()
$cdeserialize :: forall (m :: * -> *). MonadGet m => m FPRoundingBinaryOp
deserialize :: forall (m :: * -> *). MonadGet m => m FPRoundingBinaryOp
Serial)

instance Cereal.Serialize FPRoundingBinaryOp where
  put :: Putter FPRoundingBinaryOp
put = Putter FPRoundingBinaryOp
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => FPRoundingBinaryOp -> m ()
serialize
  get :: Get FPRoundingBinaryOp
get = Get FPRoundingBinaryOp
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m FPRoundingBinaryOp
deserialize

instance Binary.Binary FPRoundingBinaryOp where
  put :: FPRoundingBinaryOp -> Put
put = FPRoundingBinaryOp -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => FPRoundingBinaryOp -> m ()
serialize
  get :: Get FPRoundingBinaryOp
get = Get FPRoundingBinaryOp
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m FPRoundingBinaryOp
deserialize

instance Show FPRoundingBinaryOp where
  show :: FPRoundingBinaryOp -> String
show FPRoundingBinaryOp
FPAdd = String
"fp.add"
  show FPRoundingBinaryOp
FPSub = String
"fp.sub"
  show FPRoundingBinaryOp
FPMul = String
"fp.mul"
  show FPRoundingBinaryOp
FPDiv = String
"fp.div"

-- | Internal representation for Grisette symbolic terms.
data Term t where
  ConTerm ::
    (SupportedPrim t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !t ->
    Term t
  SymTerm ::
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(TypedSymbol 'AnyKind t) ->
    Term t
  ForallTerm ::
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(TypedSymbol 'ConstantKind t) ->
    !(Term Bool) ->
    Term Bool
  ExistsTerm ::
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(TypedSymbol 'ConstantKind t) ->
    !(Term Bool) ->
    Term Bool
  NotTerm ::
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term Bool) ->
    Term Bool
  OrTerm ::
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term Bool) ->
    !(Term Bool) ->
    Term Bool
  AndTerm ::
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term Bool) ->
    !(Term Bool) ->
    Term Bool
  EqTerm ::
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term Bool
  DistinctTerm ::
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(NonEmpty (Term t)) ->
    Term Bool
  ITETerm ::
    (SupportedPrim t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term Bool) ->
    !(Term t) ->
    !(Term t) ->
    Term t
  AddNumTerm ::
    (SupportedPrim t, PEvalNumTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term t
  NegNumTerm ::
    (SupportedPrim t, PEvalNumTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    Term t
  MulNumTerm ::
    (SupportedPrim t, PEvalNumTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term t
  AbsNumTerm ::
    (SupportedPrim t, PEvalNumTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    Term t
  SignumNumTerm ::
    (SupportedPrim t, PEvalNumTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    Term t
  LtOrdTerm ::
    (SupportedPrim t, PEvalOrdTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term Bool
  LeOrdTerm ::
    (SupportedPrim t, PEvalOrdTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term Bool
  AndBitsTerm ::
    (SupportedPrim t, PEvalBitwiseTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term t
  OrBitsTerm ::
    (SupportedPrim t, PEvalBitwiseTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term t
  XorBitsTerm ::
    (SupportedPrim t, PEvalBitwiseTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term t
  ComplementBitsTerm ::
    (SupportedPrim t, PEvalBitwiseTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    Term t
  ShiftLeftTerm ::
    (SupportedPrim t, PEvalShiftTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term t
  ShiftRightTerm ::
    (SupportedPrim t, PEvalShiftTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term t
  RotateLeftTerm ::
    (SupportedPrim t, PEvalRotateTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term t
  RotateRightTerm ::
    (SupportedPrim t, PEvalRotateTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term t
  BitCastTerm ::
    (SupportedPrim b, PEvalBitCastTerm a b) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term a) ->
    Term b
  BitCastOrTerm ::
    (SupportedPrim b, PEvalBitCastOrTerm a b) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term b) ->
    !(Term a) ->
    Term b
  BVConcatTerm ::
    ( PEvalBVTerm bv,
      KnownNat l,
      KnownNat r,
      KnownNat (l + r),
      1 <= l,
      1 <= r,
      1 <= l + r,
      SupportedPrim (bv (l + r))
    ) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term (bv l)) ->
    !(Term (bv r)) ->
    Term (bv (l + r))
  BVSelectTerm ::
    ( PEvalBVTerm bv,
      KnownNat n,
      KnownNat ix,
      KnownNat w,
      1 <= n,
      1 <= w,
      ix + w <= n,
      SupportedPrim (bv w)
    ) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Proxy ix) ->
    !(Proxy w) ->
    !(Term (bv n)) ->
    Term (bv w)
  BVExtendTerm ::
    ( PEvalBVTerm bv,
      KnownNat l,
      KnownNat r,
      1 <= l,
      1 <= r,
      l <= r,
      SupportedPrim (bv r)
    ) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !Bool ->
    !(Proxy r) ->
    !(Term (bv l)) ->
    Term (bv r)
  ApplyTerm ::
    (PEvalApplyTerm f a b, SupportedPrim b) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term f) ->
    !(Term a) ->
    Term b
  DivIntegralTerm ::
    (SupportedPrim t, PEvalDivModIntegralTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term t
  ModIntegralTerm ::
    (SupportedPrim t, PEvalDivModIntegralTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term t
  QuotIntegralTerm ::
    (SupportedPrim t, PEvalDivModIntegralTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term t
  RemIntegralTerm ::
    (SupportedPrim t, PEvalDivModIntegralTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term t
  FPTraitTerm ::
    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !FPTrait ->
    !(Term (FP eb sb)) ->
    Term Bool
  FdivTerm ::
    (SupportedPrim t, PEvalFractionalTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term t
  RecipTerm ::
    (SupportedPrim t, PEvalFractionalTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    Term t
  FloatingUnaryTerm ::
    (SupportedPrim t, PEvalFloatingTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !FloatingUnaryOp ->
    !(Term t) ->
    Term t
  PowerTerm ::
    (SupportedPrim t, PEvalFloatingTerm t) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term t) ->
    !(Term t) ->
    Term t
  FPUnaryTerm ::
    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !FPUnaryOp ->
    !(Term (FP eb sb)) ->
    Term (FP eb sb)
  FPBinaryTerm ::
    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !FPBinaryOp ->
    !(Term (FP eb sb)) ->
    !(Term (FP eb sb)) ->
    Term (FP eb sb)
  FPRoundingUnaryTerm ::
    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !FPRoundingUnaryOp ->
    !(Term FPRoundingMode) ->
    !(Term (FP eb sb)) ->
    Term (FP eb sb)
  FPRoundingBinaryTerm ::
    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !FPRoundingBinaryOp ->
    !(Term FPRoundingMode) ->
    !(Term (FP eb sb)) ->
    !(Term (FP eb sb)) ->
    Term (FP eb sb)
  FPFMATerm ::
    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term FPRoundingMode) ->
    !(Term (FP eb sb)) ->
    !(Term (FP eb sb)) ->
    !(Term (FP eb sb)) ->
    Term (FP eb sb)
  FromIntegralTerm ::
    (PEvalFromIntegralTerm a b, SupportedPrim b) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term a) ->
    Term b
  FromFPOrTerm ::
    ( PEvalIEEEFPConvertibleTerm a,
      ValidFP eb sb,
      SupportedPrim a
    ) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term a) ->
    !(Term FPRoundingMode) ->
    !(Term (FP eb sb)) ->
    Term a
  ToFPTerm ::
    ( PEvalIEEEFPConvertibleTerm a,
      ValidFP eb sb,
      SupportedPrim (FP eb sb)
    ) =>
    WeakThreadId ->
    {-# UNPACK #-} !Digest ->
    Id ->
    Ident ->
    !(Term FPRoundingMode) ->
    !(Term a) ->
    Proxy eb ->
    Proxy sb ->
    Term (FP eb sb)

-- | Pattern for term with dynamic typing.
pattern DynTerm :: forall a b. (SupportedPrim a) => Term a -> Term b
pattern $mDynTerm :: forall {r} {a} {b}.
SupportedPrim a =>
Term b -> (Term a -> r) -> ((# #) -> r) -> r
DynTerm x <-
  ( ( \Term b
v ->
        Term b
-> ((SupportedPrim b, Typeable b) => Maybe (Term a))
-> Maybe (Term a)
forall t a. Term t -> ((SupportedPrim t, Typeable t) => a) -> a
introSupportedPrimConstraint Term b
v (((SupportedPrim b, Typeable b) => Maybe (Term a))
 -> Maybe (Term a))
-> ((SupportedPrim b, Typeable b) => Maybe (Term a))
-> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$
          forall a b. SupportedPrim a => (Typeable a => b) -> b
withSupportedPrimTypeable @a ((Typeable a => Maybe (Term a)) -> Maybe (Term a))
-> (Typeable a => Maybe (Term a)) -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$
            Term b -> Maybe (Term a)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term b
v
    ) ->
      Just x
    )

-- | The identity of the term.
termIdent :: Term t -> Ident
termIdent :: forall t. Term t -> Ident
termIdent (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i t
_) = Ident
i
termIdent (SymTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i TypedSymbol 'AnyKind t
_) = Ident
i
termIdent (ForallTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i TypedSymbol 'ConstantKind t
_ Term Bool
_) = Ident
i
termIdent (ExistsTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i TypedSymbol 'ConstantKind t
_ Term Bool
_) = Ident
i
termIdent (NotTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term Bool
_) = Ident
i
termIdent (OrTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term Bool
_ Term Bool
_) = Ident
i
termIdent (AndTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term Bool
_ Term Bool
_) = Ident
i
termIdent (EqTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (DistinctTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i NonEmpty (Term t)
_) = Ident
i
termIdent (ITETerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term Bool
_ Term t
_ Term t
_) = Ident
i
termIdent (AddNumTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (NegNumTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_) = Ident
i
termIdent (MulNumTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (AbsNumTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_) = Ident
i
termIdent (SignumNumTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_) = Ident
i
termIdent (LtOrdTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (LeOrdTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (AndBitsTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (OrBitsTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (XorBitsTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (ComplementBitsTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_) = Ident
i
termIdent (ShiftLeftTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (ShiftRightTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (RotateLeftTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (RotateRightTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (BitCastTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term a
_) = Ident
i
termIdent (BitCastOrTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term a
_) = Ident
i
termIdent (BVConcatTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term (bv l)
_ Term (bv r)
_) = Ident
i
termIdent (BVSelectTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Proxy ix
_ Proxy w
_ Term (bv n)
_) = Ident
i
termIdent (BVExtendTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Bool
_ Proxy r
_ Term (bv l)
_) = Ident
i
termIdent (ApplyTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term f
_ Term a
_) = Ident
i
termIdent (DivIntegralTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (ModIntegralTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (QuotIntegralTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (RemIntegralTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (FPTraitTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i FPTrait
_ Term (FP eb sb)
_) = Ident
i
termIdent (FdivTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (RecipTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_) = Ident
i
termIdent (FloatingUnaryTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i FloatingUnaryOp
_ Term t
_) = Ident
i
termIdent (PowerTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term t
_) = Ident
i
termIdent (FPUnaryTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i FPUnaryOp
_ Term (FP eb sb)
_) = Ident
i
termIdent (FPBinaryTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i FPBinaryOp
_ Term (FP eb sb)
_ Term (FP eb sb)
_) = Ident
i
termIdent (FPRoundingUnaryTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i FPRoundingUnaryOp
_ Term FPRoundingMode
_ Term (FP eb sb)
_) = Ident
i
termIdent (FPRoundingBinaryTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i FPRoundingBinaryOp
_ Term FPRoundingMode
_ Term (FP eb sb)
_ Term (FP eb sb)
_) = Ident
i
termIdent (FPFMATerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term FPRoundingMode
_ Term (FP eb sb)
_ Term (FP eb sb)
_ Term (FP eb sb)
_) = Ident
i
termIdent (FromIntegralTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term a
_) = Ident
i
termIdent (FromFPOrTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term t
_ Term FPRoundingMode
_ Term (FP eb sb)
_) = Ident
i
termIdent (ToFPTerm WeakThreadId
_ Digest
_ Digest
_ Ident
i Term FPRoundingMode
_ Term a
_ Proxy eb
_ Proxy sb
_) = Ident
i
{-# INLINE termIdent #-}

-- | Return the ID of a term.
termId :: Term t -> Id
termId :: forall t. Term t -> Digest
termId Term t
t = case Term t -> HashId
forall t. Term t -> HashId
hashId Term t
t of
  HashId Digest
_ Digest
i -> Digest
i
{-# INLINE termId #-}

baseHash :: Term t -> Digest
baseHash :: forall t. Term t -> Digest
baseHash Term t
t = case Term t -> HashId
forall t. Term t -> HashId
hashId Term t
t of
  HashId Digest
h Digest
_ -> Digest
h
{-# INLINE baseHash #-}

data HashId = HashId {-# UNPACK #-} !Digest Id deriving (Int -> HashId -> String -> String
[HashId] -> String -> String
HashId -> String
(Int -> HashId -> String -> String)
-> (HashId -> String)
-> ([HashId] -> String -> String)
-> Show HashId
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> HashId -> String -> String
showsPrec :: Int -> HashId -> String -> String
$cshow :: HashId -> String
show :: HashId -> String
$cshowList :: [HashId] -> String -> String
showList :: [HashId] -> String -> String
Show)

instance Eq HashId where
  HashId Digest
_ Digest
l == :: HashId -> HashId -> Bool
== HashId Digest
_ Digest
r = Digest
l Digest -> Digest -> Bool
forall a. Eq a => a -> a -> Bool
== Digest
r
  {-# INLINE (==) #-}

instance Hashable HashId where
  hashWithSalt :: Int -> HashId -> Int
hashWithSalt Int
s (HashId Digest
i Digest
_) = Int -> Digest -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s Digest
i
  {-# INLINE hashWithSalt #-}

eqHashId :: HashId -> HashId -> Bool
eqHashId :: HashId -> HashId -> Bool
eqHashId = HashId -> HashId -> Bool
forall a. Eq a => a -> a -> Bool
(==)
{-# INLINE eqHashId #-}

data TypeHashId = TypeHashId {-# UNPACK #-} !Fingerprint {-# UNPACK #-} !HashId
  deriving (Int -> TypeHashId -> String -> String
[TypeHashId] -> String -> String
TypeHashId -> String
(Int -> TypeHashId -> String -> String)
-> (TypeHashId -> String)
-> ([TypeHashId] -> String -> String)
-> Show TypeHashId
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> TypeHashId -> String -> String
showsPrec :: Int -> TypeHashId -> String -> String
$cshow :: TypeHashId -> String
show :: TypeHashId -> String
$cshowList :: [TypeHashId] -> String -> String
showList :: [TypeHashId] -> String -> String
Show)

instance Eq TypeHashId where
  TypeHashId Fingerprint
l HashId
li == :: TypeHashId -> TypeHashId -> Bool
== TypeHashId Fingerprint
r HashId
ri = Fingerprint
l Fingerprint -> Fingerprint -> Bool
forall a. Eq a => a -> a -> Bool
== Fingerprint
r Bool -> Bool -> Bool
&& HashId
li HashId -> HashId -> Bool
forall a. Eq a => a -> a -> Bool
== HashId
ri
  {-# INLINE (==) #-}

instance Hashable TypeHashId where
  hashWithSalt :: Int -> TypeHashId -> Int
hashWithSalt Int
s (TypeHashId Fingerprint
tp HashId
i) = Int
s Int -> Fingerprint -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Fingerprint
tp Int -> HashId -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` HashId
i
  {-# INLINE hashWithSalt #-}

hashId :: Term t -> HashId
hashId :: forall t. Term t -> HashId
hashId Term t
t = case Term t -> TypeHashId
forall t. Term t -> TypeHashId
typeHashId Term t
t of
  TypeHashId Fingerprint
_ HashId
hi -> HashId
hi
{-# INLINE hashId #-}

typeFingerprint :: forall t. (SupportedPrim t) => Fingerprint
typeFingerprint :: forall t. SupportedPrim t => Fingerprint
typeFingerprint = SomeTypeRep -> Fingerprint
typeRepFingerprint (SomeTypeRep -> Fingerprint) -> SomeTypeRep -> Fingerprint
forall a b. (a -> b) -> a -> b
$ TypeRep t -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep (TypeRep t -> SomeTypeRep) -> TypeRep t -> SomeTypeRep
forall a b. (a -> b) -> a -> b
$ forall t. SupportedPrim t => TypeRep t
primTypeRep @t
{-# INLINE typeFingerprint #-}

-- | Return the ID and the type representation of a term.
typeHashId :: forall t. Term t -> TypeHashId
typeHashId :: forall t. Term t -> TypeHashId
typeHashId (ConTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (SymTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ TypedSymbol {}) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (ForallTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ TypedSymbol 'ConstantKind t
_ Term Bool
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (ExistsTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ TypedSymbol 'ConstantKind t
_ Term Bool
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (NotTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term Bool
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (OrTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term Bool
_ Term Bool
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (AndTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term Bool
_ Term Bool
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (EqTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (DistinctTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ NonEmpty (Term t)
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (ITETerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term Bool
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (AddNumTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (NegNumTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (MulNumTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (AbsNumTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (SignumNumTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (LtOrdTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (LeOrdTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (AndBitsTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (OrBitsTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (XorBitsTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (ComplementBitsTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (ShiftLeftTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (ShiftRightTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (RotateLeftTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (RotateRightTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (BitCastTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term a
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (BitCastOrTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term a
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (BVConcatTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term (bv l)
_ Term (bv r)
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (BVSelectTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Proxy ix
_ Proxy w
_ Term (bv n)
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (BVExtendTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Bool
_ Proxy r
_ Term (bv l)
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (ApplyTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term f
_ Term a
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (DivIntegralTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (ModIntegralTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (QuotIntegralTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (RemIntegralTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (FPTraitTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ FPTrait
_ Term (FP eb sb)
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (FdivTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (RecipTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (FloatingUnaryTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ FloatingUnaryOp
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (PowerTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ Term t
_ Term t
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (FPUnaryTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ FPUnaryOp
_ Term (FP eb sb)
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (FPBinaryTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ FPBinaryOp
_ Term (FP eb sb)
_ Term (FP eb sb)
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (FPRoundingUnaryTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ FPRoundingUnaryOp
_ Term FPRoundingMode
_ Term (FP eb sb)
_) = Fingerprint -> HashId -> TypeHashId
TypeHashId (forall t. SupportedPrim t => Fingerprint
typeFingerprint @t) (HashId -> TypeHashId) -> HashId -> TypeHashId
forall a b. (a -> b) -> a -> b
$ Digest -> Digest -> HashId
HashId Digest
ha Digest
i
typeHashId (FPRoundingBinaryTerm WeakThreadId
_ Digest
ha Digest
i Ident
_ FPRoundingBinaryOp
_ Term FPRoundingMode
_ Term (FP eb sb)
_ Term (FP eb sb)
_) =