{-# 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 Data.Proxy (Proxy (Proxy))
import qualified Data.SBV as SBV
import GHC.TypeNats (KnownNat, type (<=))
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.IsZero
  ( IsZeroCases (IsZeroEvidence, NonZeroEvidence),
    KnownIsZero (isZero),
  )
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)

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

-- Le
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 (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (OrdSymbolic (SBVType n Integer) => r) -> r
withSbvOrdTermConstraint proxy n
p OrdSymbolic (SBVType n Integer) => r
r = case proxy n -> IsZeroCases n
forall (a :: Nat) (proxy :: Nat -> *).
KnownIsZero a =>
proxy a -> IsZeroCases a
forall (proxy :: Nat -> *). proxy n -> IsZeroCases n
isZero proxy n
p of
    IsZeroCases n
IsZeroEvidence -> r
OrdSymbolic (SBVType n Integer) => r
r
    IsZeroCases n
NonZeroEvidence -> r
OrdSymbolic (SBVType n 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 (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (OrdSymbolic (SBVType n (WordN n)) => r) -> r
withSbvOrdTermConstraint proxy n
p OrdSymbolic (SBVType n (WordN n)) => r
r = forall t (n :: Nat) (p :: Nat -> *) a.
(SupportedPrim t, KnownIsZero n) =>
p n
-> ((PrimConstraint n t, SMTDefinable (SBVType n t),
     Mergeable (SBVType n t), Typeable (SBVType n t)) =>
    a)
-> a
withPrim @(WordN n) proxy n
p r
OrdSymbolic (SBVType n (WordN n)) => r
(PrimConstraint n (WordN n), SMTDefinable (SBVType n (WordN n)),
 Mergeable (SBVType n (WordN n)), Typeable (SBVType n (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 (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (OrdSymbolic (SBVType n (IntN n)) => r) -> r
withSbvOrdTermConstraint proxy n
p OrdSymbolic (SBVType n (IntN n)) => r
r = forall t (n :: Nat) (p :: Nat -> *) a.
(SupportedPrim t, KnownIsZero n) =>
p n
-> ((PrimConstraint n t, SMTDefinable (SBVType n t),
     Mergeable (SBVType n t), Typeable (SBVType n t)) =>
    a)
-> a
withPrim @(IntN n) proxy n
p r
OrdSymbolic (SBVType n (IntN n)) => r
(PrimConstraint n (IntN n), SMTDefinable (SBVType n (IntN n)),
 Mergeable (SBVType n (IntN n)), Typeable (SBVType n (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 (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (OrdSymbolic (SBVType n (FP eb sb)) => r) -> r
withSbvOrdTermConstraint proxy n
p OrdSymbolic (SBVType n (FP eb sb)) => r
r = forall t (n :: Nat) (p :: Nat -> *) a.
(SupportedPrim t, KnownIsZero n) =>
p n
-> ((PrimConstraint n t, SMTDefinable (SBVType n t),
     Mergeable (SBVType n t), Typeable (SBVType n t)) =>
    a)
-> a
withPrim @(FP eb sb) proxy n
p r
OrdSymbolic (SBVType n (FP eb sb)) => r
(PrimConstraint n (FP eb sb), SMTDefinable (SBVType n (FP eb sb)),
 Mergeable (SBVType n (FP eb sb)),
 Typeable (SBVType n (FP eb sb))) =>
r
r
  sbvLeOrdTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBV Bool
sbvLeOrdTerm proxy n
_ SBVType n (FP eb sb)
x SBVType n (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 n (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 n (FP eb sb)
y))
      SBV Bool -> SBV Bool -> SBV Bool
SBV..&& (SBV (FloatingPoint eb sb)
SBVType n (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 n (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 (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm @FPRoundingMode (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @0) FPRoundingMode
a,
      forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm @FPRoundingMode (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @0) 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 (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm @FPRoundingMode (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @0) FPRoundingMode
a,
      forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm @FPRoundingMode (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @0) 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 (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (OrdSymbolic (SBVType n FPRoundingMode) => r) -> r
withSbvOrdTermConstraint proxy n
p OrdSymbolic (SBVType n FPRoundingMode) => r
r = forall t (n :: Nat) (p :: Nat -> *) a.
(SupportedPrim t, KnownIsZero n) =>
p n
-> ((PrimConstraint n t, SMTDefinable (SBVType n t),
     Mergeable (SBVType n t), Typeable (SBVType n t)) =>
    a)
-> a
withPrim @FPRoundingMode proxy n
p r
OrdSymbolic (SBVType n FPRoundingMode) => r
(PrimConstraint n FPRoundingMode,
 SMTDefinable (SBVType n FPRoundingMode),
 Mergeable (SBVType n FPRoundingMode),
 Typeable (SBVType n FPRoundingMode)) =>
r
r
  sbvLtOrdTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBVType n FPRoundingMode -> SBVType n FPRoundingMode -> SBV Bool
sbvLtOrdTerm proxy n
_ = [(SRoundingMode, SRoundingMode)]
-> SRoundingMode -> SRoundingMode -> SBV Bool
sbvTableLookup [(SRoundingMode, SRoundingMode)]
fpRoundingModeLtTable
  sbvLeOrdTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBVType n FPRoundingMode -> SBVType n FPRoundingMode -> SBV Bool
sbvLeOrdTerm proxy n
_ = [(SRoundingMode, SRoundingMode)]
-> SRoundingMode -> SRoundingMode -> SBV Bool
sbvTableLookup [(SRoundingMode, SRoundingMode)]
fpRoundingModeLeTable