{-# LANGUAGE ScopedTypeVariables #-}
{-# HLINT ignore "Eta reduce" #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

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

import Grisette.Internal.SymPrim.FP (FP, ValidFP)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim ()
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalFloatingTerm
      ( pevalSqrtTerm,
        withSbvFloatingTermConstraint
      ),
    SupportedPrim (withPrim),
    sqrtTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold
  ( generalUnaryUnfolded,
  )

instance (ValidFP eb sb) => PEvalFloatingTerm (FP eb sb) where
  pevalSqrtTerm :: Term (FP eb sb) -> Term (FP eb sb)
pevalSqrtTerm = (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. Floating a => a -> a
sqrt Term (FP eb sb) -> Term (FP eb sb)
forall a. PEvalFloatingTerm a => Term a -> Term a
sqrtTerm
  withSbvFloatingTermConstraint :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (Floating (SBVType n (FP eb sb)) => r) -> r
withSbvFloatingTermConstraint proxy n
p Floating (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
Floating (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