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

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

module Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFractionalTerm () where

import Grisette.Internal.SymPrim.FP (FP, ValidFP)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim ()
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalFractionalTerm (pevalFdivTerm, pevalRecipTerm, withSbvFractionalTermConstraint),
    SupportedPrim (withPrim),
    fdivTerm,
    recipTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold
  ( generalBinaryUnfolded,
    generalUnaryUnfolded,
  )

instance (ValidFP eb sb) => PEvalFractionalTerm (FP eb sb) where
  pevalFdivTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
pevalFdivTerm = (FP eb sb -> FP eb sb -> FP eb sb)
-> (Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb))
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
(a -> b -> c)
-> (Term a -> Term b -> Term c) -> Term a -> Term b -> Term c
generalBinaryUnfolded FP eb sb -> FP eb sb -> FP eb sb
forall a. Fractional a => a -> a -> a
(/) Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall a. PEvalFractionalTerm a => Term a -> Term a -> Term a
fdivTerm
  pevalRecipTerm :: Term (FP eb sb) -> Term (FP eb sb)
pevalRecipTerm = (FP eb sb -> FP eb sb)
-> (Term (FP eb sb) -> Term (FP eb sb))
-> Term (FP eb sb)
-> Term (FP eb sb)
forall a b.
(Typeable a, SupportedPrim b) =>
(a -> b) -> (Term a -> Term b) -> Term a -> Term b
generalUnaryUnfolded FP eb sb -> FP eb sb
forall a. Fractional a => a -> a
recip Term (FP eb sb) -> Term (FP eb sb)
forall a. PEvalFractionalTerm a => Term a -> Term a
recipTerm
  withSbvFractionalTermConstraint :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (Fractional (SBVType n (FP eb sb)) => r) -> r
withSbvFractionalTermConstraint proxy n
p Fractional (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
Fractional (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