{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.SymFP
-- 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.SymFP
  ( SymFP (SymFP),
    SymFP16,
    SymFP32,
    SymFP64,
    SymFPRoundingMode (SymFPRoundingMode),
  )
where

import Control.DeepSeq (NFData)
import Data.Hashable (Hashable (hashWithSalt))
import Data.String (IsString (fromString))
import GHC.Generics (Generic)
import Grisette.Internal.Core.Data.Class.Function (Apply (FunType, apply))
import Grisette.Internal.Core.Data.Class.Solvable
  ( Solvable (con, conView, ssym, sym),
  )
import Grisette.Internal.SymPrim.AllSyms (AllSyms (allSymsS), SomeSym (SomeSym))
import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP)
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( ConRep (ConType),
    LinkedRep (underlyingTerm, wrapTerm),
    PEvalFloatingTerm (pevalSqrtTerm),
    PEvalFractionalTerm (pevalFdivTerm, pevalRecipTerm),
    PEvalNumTerm
      ( pevalAbsNumTerm,
        pevalAddNumTerm,
        pevalMulNumTerm,
        pevalNegNumTerm,
        pevalSignumNumTerm
      ),
    SymRep (SymType),
    Term (ConTerm),
    conTerm,
    pevalSubNumTerm,
    pformat,
    symTerm,
  )
import Language.Haskell.TH.Syntax (Lift)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> import Grisette.Backend
-- >>> import Data.Proxy

-- | Symbolic IEEE 754 floating-point number with @eb@ exponent bits and @sb@
-- significand bits.
--
-- >>> :set -XOverloadedStrings -XDataKinds
-- >>> "a" + 2.0 :: SymFP 11 53
-- (+ a 2.0)
-- >>> symFpAdd rne "a" 2.0 :: SymFP 11 53
-- (fp.add rne a 2.0)
--
-- More operations are available. Please refer to "Grisette.Core#g:symops" for
-- more information.
newtype SymFP eb sb = SymFP {forall (eb :: Nat) (sb :: Nat). SymFP eb sb -> Term (FP eb sb)
underlyingFPTerm :: Term (FP eb sb)}
  deriving ((forall (m :: * -> *). Quote m => SymFP eb sb -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    SymFP eb sb -> Code m (SymFP eb sb))
-> Lift (SymFP eb sb)
forall (eb :: Nat) (sb :: Nat) (m :: * -> *).
Quote m =>
SymFP eb sb -> m Exp
forall (eb :: Nat) (sb :: Nat) (m :: * -> *).
Quote m =>
SymFP eb sb -> Code m (SymFP eb sb)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymFP eb sb -> m Exp
forall (m :: * -> *).
Quote m =>
SymFP eb sb -> Code m (SymFP eb sb)
$clift :: forall (eb :: Nat) (sb :: Nat) (m :: * -> *).
Quote m =>
SymFP eb sb -> m Exp
lift :: forall (m :: * -> *). Quote m => SymFP eb sb -> m Exp
$cliftTyped :: forall (eb :: Nat) (sb :: Nat) (m :: * -> *).
Quote m =>
SymFP eb sb -> Code m (SymFP eb sb)
liftTyped :: forall (m :: * -> *).
Quote m =>
SymFP eb sb -> Code m (SymFP eb sb)
Lift, (forall x. SymFP eb sb -> Rep (SymFP eb sb) x)
-> (forall x. Rep (SymFP eb sb) x -> SymFP eb sb)
-> Generic (SymFP eb sb)
forall (eb :: Nat) (sb :: Nat) x.
Rep (SymFP eb sb) x -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat) x.
SymFP eb sb -> Rep (SymFP eb sb) x
forall x. Rep (SymFP eb sb) x -> SymFP eb sb
forall x. SymFP eb sb -> Rep (SymFP eb sb) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (eb :: Nat) (sb :: Nat) x.
SymFP eb sb -> Rep (SymFP eb sb) x
from :: forall x. SymFP eb sb -> Rep (SymFP eb sb) x
$cto :: forall (eb :: Nat) (sb :: Nat) x.
Rep (SymFP eb sb) x -> SymFP eb sb
to :: forall x. Rep (SymFP eb sb) x -> SymFP eb sb
Generic)
  deriving anyclass (SymFP eb sb -> ()
(SymFP eb sb -> ()) -> NFData (SymFP eb sb)
forall (eb :: Nat) (sb :: Nat). SymFP eb sb -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (eb :: Nat) (sb :: Nat). SymFP eb sb -> ()
rnf :: SymFP eb sb -> ()
NFData)

-- | Symbolic IEEE 754 half-precision floating-point number.
type SymFP16 = SymFP 5 11

-- | Symbolic IEEE 754 single-precision floating-point number.
type SymFP32 = SymFP 8 24

-- | Symbolic IEEE 754 double-precision floating-point number.
type SymFP64 = SymFP 11 53

instance ConRep (SymFP eb sb) where
  type ConType (SymFP eb sb) = FP eb sb

instance (ValidFP eb sb) => SymRep (FP eb sb) where
  type SymType (FP eb sb) = SymFP eb sb

instance (ValidFP eb sb) => LinkedRep (FP eb sb) (SymFP eb sb) where
  underlyingTerm :: SymFP eb sb -> Term (FP eb sb)
underlyingTerm (SymFP Term (FP eb sb)
a) = Term (FP eb sb)
a
  wrapTerm :: Term (FP eb sb) -> SymFP eb sb
wrapTerm = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP

instance (ValidFP eb sb) => Apply (SymFP eb sb) where
  type FunType (SymFP eb sb) = SymFP eb sb
  apply :: SymFP eb sb -> FunType (SymFP eb sb)
apply = SymFP eb sb -> FunType (SymFP eb sb)
SymFP eb sb -> SymFP eb sb
forall a. a -> a
id

instance (ValidFP eb sb) => Eq (SymFP eb sb) where
  SymFP Term (FP eb sb)
a == :: SymFP eb sb -> SymFP eb sb -> Bool
== SymFP Term (FP eb sb)
b = Term (FP eb sb)
a Term (FP eb sb) -> Term (FP eb sb) -> Bool
forall a. Eq a => a -> a -> Bool
== Term (FP eb sb)
b

instance (ValidFP eb sb) => Hashable (SymFP eb sb) where
  hashWithSalt :: Int -> SymFP eb sb -> Int
hashWithSalt Int
s (SymFP Term (FP eb sb)
a) = Int -> Term (FP eb sb) -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s Term (FP eb sb)
a

instance (ValidFP eb sb) => IsString (SymFP eb sb) where
  fromString :: String -> SymFP eb sb
fromString = Identifier -> SymFP eb sb
forall c t. Solvable c t => Identifier -> t
ssym (Identifier -> SymFP eb sb)
-> (String -> Identifier) -> String -> SymFP eb sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Identifier
forall a. IsString a => String -> a
fromString

instance (ValidFP eb sb) => Solvable (FP eb sb) (SymFP eb sb) where
  con :: FP eb sb -> SymFP eb sb
con = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb)
-> (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> SymFP eb sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FP eb sb -> Term (FP eb sb)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm
  sym :: Symbol -> SymFP eb sb
sym = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb)
-> (Symbol -> Term (FP eb sb)) -> Symbol -> SymFP eb sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Term (FP eb sb)
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm
  conView :: SymFP eb sb -> Maybe (FP eb sb)
conView (SymFP (ConTerm Int
_ FP eb sb
t)) = FP eb sb -> Maybe (FP eb sb)
forall a. a -> Maybe a
Just FP eb sb
t
  conView SymFP eb sb
_ = Maybe (FP eb sb)
forall a. Maybe a
Nothing

instance (ValidFP eb sb) => Show (SymFP eb sb) where
  show :: SymFP eb sb -> String
show (SymFP Term (FP eb sb)
a) = Term (FP eb sb) -> String
forall t. SupportedPrim t => Term t -> String
pformat Term (FP eb sb)
a

instance (ValidFP eb sb) => AllSyms (SymFP eb sb) where
  allSymsS :: SymFP eb sb -> [SomeSym] -> [SomeSym]
allSymsS SymFP eb sb
v = (SymFP eb sb -> SomeSym
forall con sym. LinkedRep con sym => sym -> SomeSym
SomeSym SymFP eb sb
v SomeSym -> [SomeSym] -> [SomeSym]
forall a. a -> [a] -> [a]
:)

instance (ValidFP eb sb) => Num (SymFP eb sb) where
  (SymFP Term (FP eb sb)
l) + :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
+ (SymFP Term (FP eb sb)
r) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalAddNumTerm Term (FP eb sb)
l Term (FP eb sb)
r
  (SymFP Term (FP eb sb)
l) - :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
- (SymFP Term (FP eb sb)
r) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalSubNumTerm Term (FP eb sb)
l Term (FP eb sb)
r
  (SymFP Term (FP eb sb)
l) * :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
* (SymFP Term (FP eb sb)
r) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalMulNumTerm Term (FP eb sb)
l Term (FP eb sb)
r
  negate :: SymFP eb sb -> SymFP eb sb
negate (SymFP Term (FP eb sb)
v) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term (FP eb sb)
v
  abs :: SymFP eb sb -> SymFP eb sb
abs (SymFP Term (FP eb sb)
v) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalNumTerm t => Term t -> Term t
pevalAbsNumTerm Term (FP eb sb)
v
  signum :: SymFP eb sb -> SymFP eb sb
signum (SymFP Term (FP eb sb)
v) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalNumTerm t => Term t -> Term t
pevalSignumNumTerm Term (FP eb sb)
v
  fromInteger :: Integer -> SymFP eb sb
fromInteger = FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con (FP eb sb -> SymFP eb sb)
-> (Integer -> FP eb sb) -> Integer -> SymFP eb sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> FP eb sb
forall a. Num a => Integer -> a
fromInteger

instance (ValidFP eb sb) => Fractional (SymFP eb sb) where
  (SymFP Term (FP eb sb)
l) / :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
/ (SymFP Term (FP eb sb)
r) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalFractionalTerm t => Term t -> Term t -> Term t
pevalFdivTerm Term (FP eb sb)
l Term (FP eb sb)
r
  recip :: SymFP eb sb -> SymFP eb sb
recip (SymFP Term (FP eb sb)
v) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalFractionalTerm t => Term t -> Term t
pevalRecipTerm Term (FP eb sb)
v
  fromRational :: Rational -> SymFP eb sb
fromRational = FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con (FP eb sb -> SymFP eb sb)
-> (Rational -> FP eb sb) -> Rational -> SymFP eb sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> FP eb sb
forall a. Fractional a => Rational -> a
fromRational

instance (ValidFP eb sb) => Floating (SymFP eb sb) where
  pi :: SymFP eb sb
pi = String -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"pi isn't supported by the underlying sbv library"
  exp :: SymFP eb sb -> SymFP eb sb
exp = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"exp isn't supported by the underlying sbv library"
  log :: SymFP eb sb -> SymFP eb sb
log = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"log isn't supported by the underlying sbv library"
  sqrt :: SymFP eb sb -> SymFP eb sb
sqrt (SymFP Term (FP eb sb)
v) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalFloatingTerm t => Term t -> Term t
pevalSqrtTerm Term (FP eb sb)
v
  ** :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
(**) = String -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"(**) isn't supported by the underlying sbv library"
  logBase :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
logBase = String -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"logBase isn't supported by the underlying sbv library"
  sin :: SymFP eb sb -> SymFP eb sb
sin = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"sin isn't supported by the underlying sbv library"
  cos :: SymFP eb sb -> SymFP eb sb
cos = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"cos isn't supported by the underlying sbv library"
  asin :: SymFP eb sb -> SymFP eb sb
asin = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"asin isn't supported by the underlying sbv library"
  acos :: SymFP eb sb -> SymFP eb sb
acos = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"acos isn't supported by the underlying sbv library"
  atan :: SymFP eb sb -> SymFP eb sb
atan = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"atan isn't supported by the underlying sbv library"
  sinh :: SymFP eb sb -> SymFP eb sb
sinh = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"sinh isn't supported by the underlying sbv library"
  cosh :: SymFP eb sb -> SymFP eb sb
cosh = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"cosh isn't supported by the underlying sbv library"
  asinh :: SymFP eb sb -> SymFP eb sb
asinh = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"asinh isn't supported by the underlying sbv library"
  acosh :: SymFP eb sb -> SymFP eb sb
acosh = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"acosh isn't supported by the underlying sbv library"
  atanh :: SymFP eb sb -> SymFP eb sb
atanh = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"atanh isn't supported by the underlying sbv library"

-- | Symbolic floating-point rounding mode.
newtype SymFPRoundingMode = SymFPRoundingMode (Term FPRoundingMode)
  deriving ((forall (m :: * -> *). Quote m => SymFPRoundingMode -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    SymFPRoundingMode -> Code m SymFPRoundingMode)
-> Lift SymFPRoundingMode
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymFPRoundingMode -> m Exp
forall (m :: * -> *).
Quote m =>
SymFPRoundingMode -> Code m SymFPRoundingMode
$clift :: forall (m :: * -> *). Quote m => SymFPRoundingMode -> m Exp
lift :: forall (m :: * -> *). Quote m => SymFPRoundingMode -> m Exp
$cliftTyped :: forall (m :: * -> *).
Quote m =>
SymFPRoundingMode -> Code m SymFPRoundingMode
liftTyped :: forall (m :: * -> *).
Quote m =>
SymFPRoundingMode -> Code m SymFPRoundingMode
Lift, (forall x. SymFPRoundingMode -> Rep SymFPRoundingMode x)
-> (forall x. Rep SymFPRoundingMode x -> SymFPRoundingMode)
-> Generic SymFPRoundingMode
forall x. Rep SymFPRoundingMode x -> SymFPRoundingMode
forall x. SymFPRoundingMode -> Rep SymFPRoundingMode x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SymFPRoundingMode -> Rep SymFPRoundingMode x
from :: forall x. SymFPRoundingMode -> Rep SymFPRoundingMode x
$cto :: forall x. Rep SymFPRoundingMode x -> SymFPRoundingMode
to :: forall x. Rep SymFPRoundingMode x -> SymFPRoundingMode
Generic)
  deriving anyclass (SymFPRoundingMode -> ()
(SymFPRoundingMode -> ()) -> NFData SymFPRoundingMode
forall a. (a -> ()) -> NFData a
$crnf :: SymFPRoundingMode -> ()
rnf :: SymFPRoundingMode -> ()
NFData)

instance ConRep SymFPRoundingMode where
  type ConType SymFPRoundingMode = FPRoundingMode

instance SymRep FPRoundingMode where
  type SymType FPRoundingMode = SymFPRoundingMode

instance LinkedRep FPRoundingMode SymFPRoundingMode where
  underlyingTerm :: SymFPRoundingMode -> Term FPRoundingMode
underlyingTerm (SymFPRoundingMode Term FPRoundingMode
a) = Term FPRoundingMode
a
  wrapTerm :: Term FPRoundingMode -> SymFPRoundingMode
wrapTerm = Term FPRoundingMode -> SymFPRoundingMode
SymFPRoundingMode

instance Apply SymFPRoundingMode where
  type FunType SymFPRoundingMode = SymFPRoundingMode
  apply :: SymFPRoundingMode -> FunType SymFPRoundingMode
apply = SymFPRoundingMode -> FunType SymFPRoundingMode
SymFPRoundingMode -> SymFPRoundingMode
forall a. a -> a
id

instance Eq SymFPRoundingMode where
  SymFPRoundingMode Term FPRoundingMode
a == :: SymFPRoundingMode -> SymFPRoundingMode -> Bool
== SymFPRoundingMode Term FPRoundingMode
b = Term FPRoundingMode
a Term FPRoundingMode -> Term FPRoundingMode -> Bool
forall a. Eq a => a -> a -> Bool
== Term FPRoundingMode
b

instance Hashable SymFPRoundingMode where
  hashWithSalt :: Int -> SymFPRoundingMode -> Int
hashWithSalt Int
s (SymFPRoundingMode Term FPRoundingMode
a) = Int -> Term FPRoundingMode -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s Term FPRoundingMode
a

instance IsString SymFPRoundingMode where
  fromString :: String -> SymFPRoundingMode
fromString = Identifier -> SymFPRoundingMode
forall c t. Solvable c t => Identifier -> t
ssym (Identifier -> SymFPRoundingMode)
-> (String -> Identifier) -> String -> SymFPRoundingMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Identifier
forall a. IsString a => String -> a
fromString

instance Solvable FPRoundingMode SymFPRoundingMode where
  con :: FPRoundingMode -> SymFPRoundingMode
con = Term FPRoundingMode -> SymFPRoundingMode
SymFPRoundingMode (Term FPRoundingMode -> SymFPRoundingMode)
-> (FPRoundingMode -> Term FPRoundingMode)
-> FPRoundingMode
-> SymFPRoundingMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FPRoundingMode -> Term FPRoundingMode
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm
  sym :: Symbol -> SymFPRoundingMode
sym = Term FPRoundingMode -> SymFPRoundingMode
SymFPRoundingMode (Term FPRoundingMode -> SymFPRoundingMode)
-> (Symbol -> Term FPRoundingMode) -> Symbol -> SymFPRoundingMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Term FPRoundingMode
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm
  conView :: SymFPRoundingMode -> Maybe FPRoundingMode
conView (SymFPRoundingMode (ConTerm Int
_ FPRoundingMode
t)) = FPRoundingMode -> Maybe FPRoundingMode
forall a. a -> Maybe a
Just FPRoundingMode
t
  conView SymFPRoundingMode
_ = Maybe FPRoundingMode
forall a. Maybe a
Nothing

instance Show SymFPRoundingMode where
  show :: SymFPRoundingMode -> String
show (SymFPRoundingMode Term FPRoundingMode
a) = Term FPRoundingMode -> String
forall t. SupportedPrim t => Term t -> String
pformat Term FPRoundingMode
a

instance AllSyms SymFPRoundingMode where
  allSymsS :: SymFPRoundingMode -> [SomeSym] -> [SomeSym]
allSymsS SymFPRoundingMode
v = (SymFPRoundingMode -> SomeSym
forall con sym. LinkedRep con sym => sym -> SomeSym
SomeSym SymFPRoundingMode
v SomeSym -> [SomeSym] -> [SomeSym]
forall a. a -> [a] -> [a]
:)