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

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm
-- 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.PEvalNumTerm () where

import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.FP (FP, ValidFP)
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalNumTerm
      ( pevalAbsNumTerm,
        pevalAddNumTerm,
        pevalMulNumTerm,
        pevalNegNumTerm,
        pevalSignumNumTerm,
        withSbvNumTermConstraint
      ),
    SupportedPrim (withPrim),
    absNumTerm,
    addNumTerm,
    doPevalNoOverflowAbsNumTerm,
    doPevalNoOverflowSignumNumTerm,
    mulNumTerm,
    negNumTerm,
    pevalDefaultAddNumTerm,
    pevalDefaultMulNumTerm,
    pevalDefaultNegNumTerm,
    signumNumTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold
  ( generalBinaryUnfolded,
    generalUnaryUnfolded,
    unaryUnfoldOnce,
  )

instance PEvalNumTerm Integer where
  pevalAddNumTerm :: Term Integer -> Term Integer -> Term Integer
pevalAddNumTerm = Term Integer -> Term Integer -> Term Integer
forall a. (PEvalNumTerm a, Eq a) => Term a -> Term a -> Term a
pevalDefaultAddNumTerm
  pevalNegNumTerm :: Term Integer -> Term Integer
pevalNegNumTerm = Term Integer -> Term Integer
forall a. (PEvalNumTerm a, Eq a) => Term a -> Term a
pevalDefaultNegNumTerm
  pevalMulNumTerm :: Term Integer -> Term Integer -> Term Integer
pevalMulNumTerm = Term Integer -> Term Integer -> Term Integer
forall a. (PEvalNumTerm a, Eq a) => Term a -> Term a -> Term a
pevalDefaultMulNumTerm
  pevalAbsNumTerm :: Term Integer -> Term Integer
pevalAbsNumTerm = PartialRuleUnary Integer Integer
-> (Term Integer -> Term Integer) -> Term Integer -> Term Integer
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary Integer Integer
forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalNoOverflowAbsNumTerm Term Integer -> Term Integer
forall a. PEvalNumTerm a => Term a -> Term a
absNumTerm
  pevalSignumNumTerm :: Term Integer -> Term Integer
pevalSignumNumTerm =
    PartialRuleUnary Integer Integer
-> (Term Integer -> Term Integer) -> Term Integer -> Term Integer
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary Integer Integer
forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalNoOverflowSignumNumTerm Term Integer -> Term Integer
forall a. PEvalNumTerm a => Term a -> Term a
signumNumTerm
  withSbvNumTermConstraint :: forall r. (Num (SBVType Integer) => r) -> r
withSbvNumTermConstraint Num (SBVType Integer) => r
r = r
Num (SBVType Integer) => r
r

instance (ValidFP eb sb) => PEvalNumTerm (FP eb sb) where
  pevalAddNumTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
pevalAddNumTerm = (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. Num a => a -> a -> a
(+) Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
addNumTerm
  pevalNegNumTerm :: Term (FP eb sb) -> Term (FP eb sb)
pevalNegNumTerm = (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. Num a => a -> a
negate Term (FP eb sb) -> Term (FP eb sb)
forall a. PEvalNumTerm a => Term a -> Term a
negNumTerm
  pevalMulNumTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
pevalMulNumTerm = (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. Num a => a -> a -> a
(*) Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
mulNumTerm
  pevalAbsNumTerm :: Term (FP eb sb) -> Term (FP eb sb)
pevalAbsNumTerm = (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. Num a => a -> a
abs Term (FP eb sb) -> Term (FP eb sb)
forall a. PEvalNumTerm a => Term a -> Term a
absNumTerm
  pevalSignumNumTerm :: Term (FP eb sb) -> Term (FP eb sb)
pevalSignumNumTerm = (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. Num a => a -> a
signum Term (FP eb sb) -> Term (FP eb sb)
forall a. PEvalNumTerm a => Term a -> Term a
signumNumTerm
  withSbvNumTermConstraint :: forall r. (Num (SBVType (FP eb sb)) => r) -> r
withSbvNumTermConstraint Num (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
Num (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

instance PEvalNumTerm AlgReal where
  pevalAddNumTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal
pevalAddNumTerm = Term AlgReal -> Term AlgReal -> Term AlgReal
forall a. (PEvalNumTerm a, Eq a) => Term a -> Term a -> Term a
pevalDefaultAddNumTerm
  pevalNegNumTerm :: Term AlgReal -> Term AlgReal
pevalNegNumTerm = Term AlgReal -> Term AlgReal
forall a. (PEvalNumTerm a, Eq a) => Term a -> Term a
pevalDefaultNegNumTerm
  pevalMulNumTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal
pevalMulNumTerm = Term AlgReal -> Term AlgReal -> Term AlgReal
forall a. (PEvalNumTerm a, Eq a) => Term a -> Term a -> Term a
pevalDefaultMulNumTerm
  pevalAbsNumTerm :: Term AlgReal -> Term AlgReal
pevalAbsNumTerm = PartialRuleUnary AlgReal AlgReal
-> (Term AlgReal -> Term AlgReal) -> Term AlgReal -> Term AlgReal
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary AlgReal AlgReal
forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalNoOverflowAbsNumTerm Term AlgReal -> Term AlgReal
forall a. PEvalNumTerm a => Term a -> Term a
absNumTerm
  pevalSignumNumTerm :: Term AlgReal -> Term AlgReal
pevalSignumNumTerm =
    PartialRuleUnary AlgReal AlgReal
-> (Term AlgReal -> Term AlgReal) -> Term AlgReal -> Term AlgReal
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary AlgReal AlgReal
forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalNoOverflowSignumNumTerm Term AlgReal -> Term AlgReal
forall a. PEvalNumTerm a => Term a -> Term a
signumNumTerm
  withSbvNumTermConstraint :: forall r. (Num (SBVType AlgReal) => r) -> r
withSbvNumTermConstraint Num (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
Num (SBVType AlgReal) => r
(PrimConstraint AlgReal, SMTDefinable (SBVType AlgReal),
 Mergeable (SBVType AlgReal), Typeable (SBVType AlgReal)) =>
r
r