{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Eta reduce" #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm
-- Copyright   :   (c) Sirui Lu 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.Instances.PEvalOrdTerm
  ( pevalGeneralLtOrdTerm,
    pevalGeneralLeOrdTerm,
  )
where

import Control.Monad (msum)
import Data.Foldable (Foldable (foldl'))
import qualified Data.SBV as SBV
import GHC.TypeNats (KnownNat, type (<=))
import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP
  ( FP,
    FPRoundingMode,
    ValidFP,
    allFPRoundingMode,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm ()
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalNumTerm (pevalNegNumTerm),
    PEvalOrdTerm
      ( pevalLeOrdTerm,
        pevalLtOrdTerm,
        sbvLeOrdTerm,
        sbvLtOrdTerm,
        withSbvOrdTermConstraint
      ),
    SupportedPrim (conSBVTerm, withPrim),
    Term (AddNumTerm, ConTerm),
    conTerm,
    leOrdTerm,
    ltOrdTerm,
    pevalSubNumTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold (binaryUnfoldOnce)

-- | General partially evaluation of less than operation.
pevalGeneralLtOrdTerm :: (PEvalOrdTerm a) => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm :: forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm = PartialRuleBinary a a Bool
-> TotalRuleBinary a a Bool -> TotalRuleBinary a a Bool
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLtOrdTerm TotalRuleBinary a a Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
ltOrdTerm

doPevalGeneralLtOrdTerm ::
  (PEvalOrdTerm a) => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLtOrdTerm :: forall a. PEvalOrdTerm a => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLtOrdTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) = Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
b
doPevalGeneralLtOrdTerm Term a
_ Term a
_ = Maybe (Term Bool)
forall a. Maybe a
Nothing

-- | General partially evaluation of less than or equal to operation.
pevalGeneralLeOrdTerm :: (PEvalOrdTerm a) => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm :: forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm = PartialRuleBinary a a Bool
-> TotalRuleBinary a a Bool -> TotalRuleBinary a a Bool
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLeOrdTerm TotalRuleBinary a a Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
leOrdTerm

doPevalGeneralLeOrdTerm ::
  (PEvalOrdTerm a) => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLeOrdTerm :: forall a. PEvalOrdTerm a => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLeOrdTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) = Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b
doPevalGeneralLeOrdTerm Term a
_ Term a
_ = Maybe (Term Bool)
forall a. Maybe a
Nothing

instance PEvalOrdTerm Integer where
  pevalLtOrdTerm :: Term Integer -> Term Integer -> Term Bool
pevalLtOrdTerm = PartialRuleBinary Integer Integer Bool
-> (Term Integer -> Term Integer -> Term Bool)
-> Term Integer
-> Term Integer
-> Term Bool
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary Integer Integer Bool
forall {a}.
(PEvalOrdTerm a, PEvalNumTerm a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalLtOrdTerm Term Integer -> Term Integer -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
ltOrdTerm
    where
      doPevalLtOrdTerm :: Term a -> Term a -> Maybe (Term Bool)
doPevalLtOrdTerm Term a
l Term a
r =
        [Maybe (Term Bool)] -> Maybe (Term Bool)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
          [ Term a -> Term a -> Maybe (Term Bool)
forall a. PEvalOrdTerm a => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLtOrdTerm Term a
l Term a
r,
            case (Term a
l, Term a
r) of
              (ConTerm Id
_ a
l, AddNumTerm Id
_ (ConTerm Id
_ a
j) Term a
k) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
l a -> a -> a
forall a. Num a => a -> a -> a
- a
j) Term a
k
              (AddNumTerm Id
_ (ConTerm Id
_ a
i) Term a
j, ConTerm Id
_ a
k) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm Term a
j (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
i)
              ((AddNumTerm Id
_ (ConTerm Id
_ a
j) Term a
k), Term a
l) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$
                  Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm
                    (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
j)
                    (Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalSubNumTerm Term a
l Term a
k)
              (Term a
j, (AddNumTerm Id
_ (ConTerm Id
_ a
k) Term a
l)) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ -a
k) (Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalSubNumTerm Term a
l Term a
j)
              (Term a
l, ConTerm Id
_ a
r) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ -a
r) (Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term a
l)
              (Term a, Term a)
_ -> Maybe (Term Bool)
forall a. Maybe a
Nothing
          ]
  pevalLeOrdTerm :: Term Integer -> Term Integer -> Term Bool
pevalLeOrdTerm = PartialRuleBinary Integer Integer Bool
-> (Term Integer -> Term Integer -> Term Bool)
-> Term Integer
-> Term Integer
-> Term Bool
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary Integer Integer Bool
forall {a}.
(PEvalOrdTerm a, PEvalNumTerm a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalLeOrdTerm Term Integer -> Term Integer -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
leOrdTerm
    where
      doPevalLeOrdTerm :: Term a -> Term a -> Maybe (Term Bool)
doPevalLeOrdTerm Term a
l Term a
r =
        [Maybe (Term Bool)] -> Maybe (Term Bool)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
          [ Term a -> Term a -> Maybe (Term Bool)
forall a. PEvalOrdTerm a => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLeOrdTerm Term a
l Term a
r,
            case (Term a
l, Term a
r) of
              (ConTerm Id
_ a
l, AddNumTerm Id
_ (ConTerm Id
_ a
j) Term a
k) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
l a -> a -> a
forall a. Num a => a -> a -> a
- a
j) Term a
k
              (AddNumTerm Id
_ (ConTerm Id
_ a
i) Term a
j, ConTerm Id
_ a
k) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm Term a
j (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
i)
              (AddNumTerm Id
_ (ConTerm Id
_ a
j) Term a
k, Term a
l) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
j) (Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalSubNumTerm Term a
l Term a
k)
              (Term a
j, AddNumTerm Id
_ (ConTerm Id
_ a
k) Term a
l) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ -a
k) (Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalSubNumTerm Term a
l Term a
j)
              (Term a
l, ConTerm Id
_ a
r) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ -a
r) (Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term a
l)
              (Term a, Term a)
_ -> Maybe (Term Bool)
forall a. Maybe a
Nothing
          ]
  withSbvOrdTermConstraint :: forall r. (OrdSymbolic (SBVType Integer) => r) -> r
withSbvOrdTermConstraint OrdSymbolic (SBVType Integer) => r
r = r
OrdSymbolic (SBVType Integer) => r
r

instance (KnownNat n, 1 <= n) => PEvalOrdTerm (WordN n) where
  pevalLtOrdTerm :: Term (WordN n) -> Term (WordN n) -> Term Bool
pevalLtOrdTerm = Term (WordN n) -> Term (WordN n) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm
  pevalLeOrdTerm :: Term (WordN n) -> Term (WordN n) -> Term Bool
pevalLeOrdTerm = Term (WordN n) -> Term (WordN n) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm
  withSbvOrdTermConstraint :: forall r. (OrdSymbolic (SBVType (WordN n)) => r) -> r
withSbvOrdTermConstraint OrdSymbolic (SBVType (WordN n)) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(WordN n) r
OrdSymbolic (SBVType (WordN n)) => r
(PrimConstraint (WordN n), SMTDefinable (SBVType (WordN n)),
 Mergeable (SBVType (WordN n)), Typeable (SBVType (WordN n))) =>
r
r

instance (KnownNat n, 1 <= n) => PEvalOrdTerm (IntN n) where
  pevalLtOrdTerm :: Term (IntN n) -> Term (IntN n) -> Term Bool
pevalLtOrdTerm = Term (IntN n) -> Term (IntN n) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm
  pevalLeOrdTerm :: Term (IntN n) -> Term (IntN n) -> Term Bool
pevalLeOrdTerm = Term (IntN n) -> Term (IntN n) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm
  withSbvOrdTermConstraint :: forall r. (OrdSymbolic (SBVType (IntN n)) => r) -> r
withSbvOrdTermConstraint OrdSymbolic (SBVType (IntN n)) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(IntN n) r
OrdSymbolic (SBVType (IntN n)) => r
(PrimConstraint (IntN n), SMTDefinable (SBVType (IntN n)),
 Mergeable (SBVType (IntN n)), Typeable (SBVType (IntN n))) =>
r
r

instance (ValidFP eb sb) => PEvalOrdTerm (FP eb sb) where
  pevalLtOrdTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
pevalLtOrdTerm = Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm
  pevalLeOrdTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
pevalLeOrdTerm = Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm
  withSbvOrdTermConstraint :: forall r. (OrdSymbolic (SBVType (FP eb sb)) => r) -> r
withSbvOrdTermConstraint OrdSymbolic (SBVType (FP eb sb)) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(FP eb sb) r
OrdSymbolic (SBVType (FP eb sb)) => r
(PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)),
 Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) =>
r
r
  sbvLeOrdTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBV Bool
sbvLeOrdTerm SBVType (FP eb sb)
x SBVType (FP eb sb)
y =
    (SBV Bool -> SBV Bool
SBV.sNot (SBV (FloatingPoint eb sb) -> SBV Bool
forall a. IEEEFloating a => SBV a -> SBV Bool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x) SBV Bool -> SBV Bool -> SBV Bool
SBV..&& SBV Bool -> SBV Bool
SBV.sNot (SBV (FloatingPoint eb sb) -> SBV Bool
forall a. IEEEFloating a => SBV a -> SBV Bool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y))
      SBV Bool -> SBV Bool -> SBV Bool
SBV..&& (SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
SBV..<= SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y)

-- Use this table to avoid accidental breakage introduced by sbv.
fpRoundingModeLtTable :: [(SBV.SRoundingMode, SBV.SRoundingMode)]
fpRoundingModeLtTable :: [(SRoundingMode, SRoundingMode)]
fpRoundingModeLtTable =
  [ ( forall t. SupportedPrim t => t -> SBVType t
conSBVTerm @FPRoundingMode FPRoundingMode
a,
      forall t. SupportedPrim t => t -> SBVType t
conSBVTerm @FPRoundingMode FPRoundingMode
b
    )
    | FPRoundingMode
a <- [FPRoundingMode]
allFPRoundingMode,
      FPRoundingMode
b <- [FPRoundingMode]
allFPRoundingMode,
      FPRoundingMode
a FPRoundingMode -> FPRoundingMode -> Bool
forall a. Ord a => a -> a -> Bool
< FPRoundingMode
b
  ]

fpRoundingModeLeTable :: [(SBV.SRoundingMode, SBV.SRoundingMode)]
fpRoundingModeLeTable :: [(SRoundingMode, SRoundingMode)]
fpRoundingModeLeTable =
  [ ( forall t. SupportedPrim t => t -> SBVType t
conSBVTerm @FPRoundingMode FPRoundingMode
a,
      forall t. SupportedPrim t => t -> SBVType t
conSBVTerm @FPRoundingMode FPRoundingMode
b
    )
    | FPRoundingMode
a <- [FPRoundingMode]
allFPRoundingMode,
      FPRoundingMode
b <- [FPRoundingMode]
allFPRoundingMode,
      FPRoundingMode
a FPRoundingMode -> FPRoundingMode -> Bool
forall a. Ord a => a -> a -> Bool
<= FPRoundingMode
b
  ]

sbvTableLookup ::
  [(SBV.SRoundingMode, SBV.SRoundingMode)] ->
  SBV.SRoundingMode ->
  SBV.SRoundingMode ->
  SBV.SBV Bool
sbvTableLookup :: [(SRoundingMode, SRoundingMode)]
-> SRoundingMode -> SRoundingMode -> SBV Bool
sbvTableLookup [(SRoundingMode, SRoundingMode)]
tbl SRoundingMode
lhs SRoundingMode
rhs =
  (SBV Bool -> (SRoundingMode, SRoundingMode) -> SBV Bool)
-> SBV Bool -> [(SRoundingMode, SRoundingMode)] -> SBV Bool
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
    (\SBV Bool
acc (SRoundingMode
a, SRoundingMode
b) -> SBV Bool
acc SBV Bool -> SBV Bool -> SBV Bool
SBV..|| ((SRoundingMode
lhs SRoundingMode -> SRoundingMode -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
SBV..== SRoundingMode
a) SBV Bool -> SBV Bool -> SBV Bool
SBV..&& (SRoundingMode
rhs SRoundingMode -> SRoundingMode -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
SBV..== SRoundingMode
b)))
    SBV Bool
SBV.sFalse
    [(SRoundingMode, SRoundingMode)]
tbl

instance PEvalOrdTerm FPRoundingMode where
  pevalLtOrdTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool
pevalLtOrdTerm = Term FPRoundingMode -> Term FPRoundingMode -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm
  pevalLeOrdTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool
pevalLeOrdTerm = Term FPRoundingMode -> Term FPRoundingMode -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm
  withSbvOrdTermConstraint :: forall r. (OrdSymbolic (SBVType FPRoundingMode) => r) -> r
withSbvOrdTermConstraint OrdSymbolic (SBVType FPRoundingMode) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @FPRoundingMode r
OrdSymbolic (SBVType FPRoundingMode) => r
(PrimConstraint FPRoundingMode,
 SMTDefinable (SBVType FPRoundingMode),
 Mergeable (SBVType FPRoundingMode),
 Typeable (SBVType FPRoundingMode)) =>
r
r
  sbvLtOrdTerm :: SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBV Bool
sbvLtOrdTerm = [(SRoundingMode, SRoundingMode)]
-> SRoundingMode -> SRoundingMode -> SBV Bool
sbvTableLookup [(SRoundingMode, SRoundingMode)]
fpRoundingModeLtTable
  sbvLeOrdTerm :: SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBV Bool
sbvLeOrdTerm = [(SRoundingMode, SRoundingMode)]
-> SRoundingMode -> SRoundingMode -> SBV Bool
sbvTableLookup [(SRoundingMode, SRoundingMode)]
fpRoundingModeLeTable

instance PEvalOrdTerm AlgReal where
  pevalLtOrdTerm :: Term AlgReal -> Term AlgReal -> Term Bool
pevalLtOrdTerm = Term AlgReal -> Term AlgReal -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm
  pevalLeOrdTerm :: Term AlgReal -> Term AlgReal -> Term Bool
pevalLeOrdTerm = Term AlgReal -> Term AlgReal -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm
  withSbvOrdTermConstraint :: forall r. (OrdSymbolic (SBVType AlgReal) => r) -> r
withSbvOrdTermConstraint OrdSymbolic (SBVType AlgReal) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @AlgReal r
OrdSymbolic (SBVType AlgReal) => r
(PrimConstraint AlgReal, SMTDefinable (SBVType AlgReal),
 Mergeable (SBVType AlgReal), Typeable (SBVType AlgReal)) =>
r
r