{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# HLINT ignore "Eta reduce" #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# 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
  ( pevalDefaultAddNumTerm,
    pevalDefaultNegNumTerm,
  )
where

import Control.Monad (msum)
import Data.Bits (Bits)
import Data.SBV (Bits (isSigned))
import GHC.TypeLits (KnownNat, type (<=))
import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP (FP, ValidFP)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim ()
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalNumTerm
      ( pevalAbsNumTerm,
        pevalAddNumTerm,
        pevalMulNumTerm,
        pevalNegNumTerm,
        pevalSignumNumTerm,
        withSbvNumTermConstraint
      ),
    SupportedPrim (withPrim),
    Term,
    absNumTerm,
    addNumTerm,
    conTerm,
    mulNumTerm,
    negNumTerm,
    pevalSubNumTerm,
    signumNumTerm,
    pattern AbsNumTerm,
    pattern AddNumTerm,
    pattern ConTerm,
    pattern MulNumTerm,
    pattern NegNumTerm,
    pattern SupportedTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold
  ( binaryUnfoldOnce,
    generalBinaryUnfolded,
    generalUnaryUnfolded,
    unaryUnfoldOnce,
  )

-- | Default partial evaluation of addition of numerical terms.
pevalDefaultAddNumTerm :: (PEvalNumTerm a, Eq a) => Term a -> Term a -> Term a
pevalDefaultAddNumTerm :: forall a. (PEvalNumTerm a, Eq a) => Term a -> Term a -> Term a
pevalDefaultAddNumTerm l :: Term a
l@Term a
SupportedTerm Term a
r =
  PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
SupportedPrim c =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce
    PartialRuleBinary a a a
forall a.
(PEvalNumTerm a, Eq a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultAddNumTerm
    (\Term a
a Term a
b -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a
normalizeAddNum (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ TotalRuleBinary a a a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
addNumTerm Term a
a Term a
b)
    Term a
l
    Term a
r

doPevalDefaultAddNumTerm ::
  (PEvalNumTerm a, Eq a) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultAddNumTerm :: forall a.
(PEvalNumTerm a, Eq a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultAddNumTerm (ConTerm a
a) (ConTerm a
b) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> a
forall a. Num a => a -> a -> a
+ a
b
doPevalDefaultAddNumTerm l :: Term a
l@(ConTerm a
a) Term a
b = case (a
a, Term a
b) of
  (a
0, Term a
k) -> Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
k
  (a
l1, AddNumTerm (ConTerm a
j) Term a
k) ->
    Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalAddNumTerm (a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
l1 a -> a -> a
forall a. Num a => a -> a -> a
+ a
j) Term a
k
  (a, Term a)
_ -> Term a -> Term a -> Maybe (Term a)
forall a. PEvalNumTerm a => Term a -> Term a -> Maybe (Term a)
doPevalDefaultAddNumTermNoCon Term a
l Term a
b
doPevalDefaultAddNumTerm Term a
a r :: Term a
r@(ConTerm {}) = Term a -> Term a -> Maybe (Term a)
forall a.
(PEvalNumTerm a, Eq a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultAddNumTerm Term a
r Term a
a
doPevalDefaultAddNumTerm Term a
l Term a
r = Term a -> Term a -> Maybe (Term a)
forall a. PEvalNumTerm a => Term a -> Term a -> Maybe (Term a)
doPevalDefaultAddNumTermNoCon Term a
l Term a
r

doPevalDefaultAddNumTermNoCon ::
  (PEvalNumTerm a) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultAddNumTermNoCon :: forall a. PEvalNumTerm a => Term a -> Term a -> Maybe (Term a)
doPevalDefaultAddNumTermNoCon (AddNumTerm i :: Term a
i@ConTerm {} Term a
j) Term a
k =
  Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalAddNumTerm Term a
i (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalAddNumTerm Term a
j Term a
k
doPevalDefaultAddNumTermNoCon Term a
i (AddNumTerm j :: Term a
j@ConTerm {} Term a
k) =
  Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalAddNumTerm Term a
j (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalAddNumTerm Term a
i Term a
k
doPevalDefaultAddNumTermNoCon (NegNumTerm Term a
i) (NegNumTerm Term a
j) =
  Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a
pevalNegNumTerm (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalAddNumTerm Term a
i Term a
j
doPevalDefaultAddNumTermNoCon
  (MulNumTerm (ConTerm a
i) Term a
j)
  (MulNumTerm (ConTerm a
k) Term a
l)
    | Term a
j Term a -> Term a -> Bool
forall a. Eq a => a -> a -> Bool
== Term a
l = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalMulNumTerm (a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
i a -> a -> a
forall a. Num a => a -> a -> a
+ a
k) Term a
j
doPevalDefaultAddNumTermNoCon
  (MulNumTerm i :: Term a
i@ConTerm {} Term a
j)
  (MulNumTerm k :: Term a
k@(ConTerm {}) Term a
l)
    | Term a
i Term a -> Term a -> Bool
forall a. Eq a => a -> a -> Bool
== Term a
k = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalMulNumTerm Term a
i (Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalAddNumTerm Term a
j Term a
l)
doPevalDefaultAddNumTermNoCon Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

normalizeAddNum :: (PEvalNumTerm a) => Term a -> Term a
normalizeAddNum :: forall a. PEvalNumTerm a => Term a -> Term a
normalizeAddNum (AddNumTerm Term a
l r :: Term a
r@(ConTerm {})) = Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
addNumTerm Term a
r Term a
l
normalizeAddNum Term a
v = Term a
v

-- | Default partial evaluation of negation of numerical terms.
pevalDefaultNegNumTerm :: (PEvalNumTerm a, Eq a) => Term a -> Term a
pevalDefaultNegNumTerm :: forall a. (PEvalNumTerm a, Eq a) => Term a -> Term a
pevalDefaultNegNumTerm l :: Term a
l@Term a
SupportedTerm =
  PartialRuleUnary a a -> TotalRuleUnary a a -> TotalRuleUnary a a
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary a a
forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalDefaultNegNumTerm TotalRuleUnary a a
forall a. PEvalNumTerm a => Term a -> Term a
negNumTerm Term a
l

doPevalDefaultNegNumTerm :: (PEvalNumTerm a) => Term a -> Maybe (Term a)
doPevalDefaultNegNumTerm :: forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalDefaultNegNumTerm (ConTerm a
a) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ -a
a
doPevalDefaultNegNumTerm (NegNumTerm Term a
v) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
v
doPevalDefaultNegNumTerm (AddNumTerm (ConTerm a
l) Term a
r) =
  Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalSubNumTerm (a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ -a
l) Term a
r
doPevalDefaultNegNumTerm (AddNumTerm (NegNumTerm Term a
l) Term a
r) =
  Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalAddNumTerm Term a
l (Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a
pevalNegNumTerm Term a
r)
doPevalDefaultNegNumTerm (AddNumTerm Term a
l (NegNumTerm Term a
r)) =
  Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalAddNumTerm (Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a
pevalNegNumTerm Term a
l) Term a
r
doPevalDefaultNegNumTerm (MulNumTerm (ConTerm a
l) Term a
r) =
  Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalMulNumTerm (a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ -a
l) Term a
r
doPevalDefaultNegNumTerm (MulNumTerm (NegNumTerm {}) Term a
_) =
  [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalDefaultNegNumTerm (MulNumTerm Term a
_ (NegNumTerm {})) =
  [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalDefaultNegNumTerm (AddNumTerm Term a
_ ConTerm {}) = [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalDefaultNegNumTerm Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

-- Mul
pevalDefaultMulNumTerm :: (PEvalNumTerm a, Eq a) => Term a -> Term a -> Term a
pevalDefaultMulNumTerm :: forall a. (PEvalNumTerm a, Eq a) => Term a -> Term a -> Term a
pevalDefaultMulNumTerm l :: Term a
l@Term a
SupportedTerm Term a
r =
  PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
SupportedPrim c =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce
    PartialRuleBinary a a a
forall a.
(PEvalNumTerm a, Eq a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultMulNumTerm
    (\Term a
a Term a
b -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a
normalizeMulNum (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ TotalRuleBinary a a a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
mulNumTerm Term a
a Term a
b)
    Term a
l
    Term a
r

normalizeMulNum :: (PEvalNumTerm a) => Term a -> Term a
normalizeMulNum :: forall a. PEvalNumTerm a => Term a -> Term a
normalizeMulNum (MulNumTerm Term a
l r :: Term a
r@(ConTerm {})) = Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
mulNumTerm Term a
r Term a
l
normalizeMulNum Term a
v = Term a
v

doPevalDefaultMulNumTerm ::
  (PEvalNumTerm a, Eq a) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultMulNumTerm :: forall a.
(PEvalNumTerm a, Eq a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultMulNumTerm (ConTerm a
a) (ConTerm a
b) =
  Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> a
forall a. Num a => a -> a -> a
* a
b
doPevalDefaultMulNumTerm l :: Term a
l@(ConTerm a
a) Term a
b = case (a
a, Term a
b) of
  (a
0, Term a
_) -> Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm a
0
  (a
1, Term a
k) -> Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
k
  (-1, Term a
k) -> Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a
pevalNegNumTerm Term a
k
  (a
l1, MulNumTerm (ConTerm a
j) Term a
k) ->
    Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalMulNumTerm (a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
l1 a -> a -> a
forall a. Num a => a -> a -> a
* a
j) Term a
k
  (a
l1, AddNumTerm (ConTerm a
j) Term a
k) ->
    Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalAddNumTerm (a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
l1 a -> a -> a
forall a. Num a => a -> a -> a
* a
j) (Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalMulNumTerm (a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm a
l1) Term a
k)
  (a
l1, NegNumTerm Term a
j) -> Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalMulNumTerm (a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ -a
l1) Term a
j)
  (a
_, MulNumTerm Term a
_ ConTerm {}) -> [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
  (a
_, AddNumTerm Term a
_ ConTerm {}) -> [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
  (a, Term a)
_ -> Term a -> Term a -> Maybe (Term a)
forall a. PEvalNumTerm a => Term a -> Term a -> Maybe (Term a)
doPevalDefaultMulNumTermNoCon Term a
l Term a
b
doPevalDefaultMulNumTerm Term a
a r :: Term a
r@(ConTerm {}) = Term a -> Term a -> Maybe (Term a)
forall a.
(PEvalNumTerm a, Eq a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultMulNumTerm Term a
r Term a
a
doPevalDefaultMulNumTerm Term a
l Term a
r = Term a -> Term a -> Maybe (Term a)
forall a. PEvalNumTerm a => Term a -> Term a -> Maybe (Term a)
doPevalDefaultMulNumTermNoCon Term a
l Term a
r

doPevalDefaultMulNumTermNoCon ::
  (PEvalNumTerm a) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultMulNumTermNoCon :: forall a. PEvalNumTerm a => Term a -> Term a -> Maybe (Term a)
doPevalDefaultMulNumTermNoCon (MulNumTerm i :: Term a
i@ConTerm {} Term a
j) Term a
k =
  Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalMulNumTerm Term a
i (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalMulNumTerm Term a
j Term a
k
doPevalDefaultMulNumTermNoCon Term a
i (MulNumTerm j :: Term a
j@ConTerm {} Term a
k) =
  Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalMulNumTerm Term a
j (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalMulNumTerm Term a
i Term a
k
doPevalDefaultMulNumTermNoCon (NegNumTerm Term a
i) Term a
j =
  Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a
pevalNegNumTerm (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalMulNumTerm Term a
i Term a
j
doPevalDefaultMulNumTermNoCon Term a
i (NegNumTerm Term a
j) =
  Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a
pevalNegNumTerm (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalMulNumTerm Term a
i Term a
j
doPevalDefaultMulNumTermNoCon Term a
i j :: Term a
j@ConTerm {} = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalMulNumTerm Term a
j Term a
i
doPevalDefaultMulNumTermNoCon (MulNumTerm Term a
_ ConTerm {}) Term a
_ =
  [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalDefaultMulNumTermNoCon Term a
_ (MulNumTerm Term a
_ ConTerm {}) =
  [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalDefaultMulNumTermNoCon Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

-- Abs
pevalBitsAbsNumTerm :: (PEvalNumTerm a, Bits a) => Term a -> Term a
pevalBitsAbsNumTerm :: forall a. (PEvalNumTerm a, Bits a) => Term a -> Term a
pevalBitsAbsNumTerm l :: Term a
l@Term a
SupportedTerm =
  PartialRuleUnary a a -> TotalRuleUnary a a -> TotalRuleUnary a a
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary a a
forall a. (PEvalNumTerm a, Bits a) => Term a -> Maybe (Term a)
doPevalBitsAbsNumTerm TotalRuleUnary a a
forall a. PEvalNumTerm a => Term a -> Term a
absNumTerm Term a
l

doPevalGeneralAbsNumTerm :: (PEvalNumTerm a) => Term a -> Maybe (Term a)
doPevalGeneralAbsNumTerm :: forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalGeneralAbsNumTerm (ConTerm a
a) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Num a => a -> a
abs a
a
doPevalGeneralAbsNumTerm (NegNumTerm Term a
v) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a
pevalAbsNumTerm Term a
v
doPevalGeneralAbsNumTerm t :: Term a
t@(AbsNumTerm {}) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
t
doPevalGeneralAbsNumTerm Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

doPevalBitsAbsNumTerm ::
  forall a. (PEvalNumTerm a, Bits a) => Term a -> Maybe (Term a)
doPevalBitsAbsNumTerm :: forall a. (PEvalNumTerm a, Bits a) => Term a -> Maybe (Term a)
doPevalBitsAbsNumTerm Term a
t =
  [Maybe (Term a)] -> Maybe (Term a)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
    [ if a -> Bool
forall a. Bits a => a -> Bool
isSigned (a
forall a. HasCallStack => a
undefined :: a) then Maybe (Term a)
forall a. Maybe a
Nothing else Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
t,
      Term a -> Maybe (Term a)
forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalGeneralAbsNumTerm Term a
t
    ]

doPevalNoOverflowAbsNumTerm :: (PEvalNumTerm a) => Term a -> Maybe (Term a)
doPevalNoOverflowAbsNumTerm :: forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalNoOverflowAbsNumTerm Term a
t =
  [Maybe (Term a)] -> Maybe (Term a)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
    [ Term a -> Maybe (Term a)
forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalGeneralAbsNumTerm Term a
t,
      case Term a
t of
        MulNumTerm Term a
l Term a
r ->
          Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalMulNumTerm (Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a
pevalAbsNumTerm Term a
l) (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a
pevalAbsNumTerm Term a
r
        Term a
_ -> Maybe (Term a)
forall a. Maybe a
Nothing
    ]

-- Signum

pevalGeneralSignumNumTerm :: (PEvalNumTerm a) => Term a -> Term a
pevalGeneralSignumNumTerm :: forall a. PEvalNumTerm a => Term a -> Term a
pevalGeneralSignumNumTerm l :: Term a
l@Term a
SupportedTerm =
  PartialRuleUnary a a -> TotalRuleUnary a a -> TotalRuleUnary a a
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary a a
forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalGeneralSignumNumTerm TotalRuleUnary a a
forall a. PEvalNumTerm a => Term a -> Term a
signumNumTerm Term a
l

doPevalGeneralSignumNumTerm :: (PEvalNumTerm a) => Term a -> Maybe (Term a)
doPevalGeneralSignumNumTerm :: forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalGeneralSignumNumTerm (ConTerm a
a) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Num a => a -> a
signum a
a
doPevalGeneralSignumNumTerm Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

doPevalNoOverflowSignumNumTerm :: (PEvalNumTerm a) => Term a -> Maybe (Term a)
doPevalNoOverflowSignumNumTerm :: forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalNoOverflowSignumNumTerm Term a
t =
  [Maybe (Term a)] -> Maybe (Term a)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
    [ Term a -> Maybe (Term a)
forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalGeneralSignumNumTerm Term a
t,
      case Term a
t of
        NegNumTerm Term a
v -> Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a
pevalNegNumTerm (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a
pevalSignumNumTerm Term a
v
        MulNumTerm Term a
l Term a
r ->
          Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$
            Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalMulNumTerm (Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a
pevalSignumNumTerm Term a
l) (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$
              Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a
pevalSignumNumTerm Term a
r
        Term a
_ -> Maybe (Term a)
forall a. Maybe a
Nothing
    ]

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 (KnownNat n, 1 <= n) => PEvalNumTerm (WordN n) where
  pevalAddNumTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalAddNumTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a. (PEvalNumTerm a, Eq a) => Term a -> Term a -> Term a
pevalDefaultAddNumTerm
  pevalNegNumTerm :: Term (WordN n) -> Term (WordN n)
pevalNegNumTerm = Term (WordN n) -> Term (WordN n)
forall a. (PEvalNumTerm a, Eq a) => Term a -> Term a
pevalDefaultNegNumTerm
  pevalMulNumTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalMulNumTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a. (PEvalNumTerm a, Eq a) => Term a -> Term a -> Term a
pevalDefaultMulNumTerm
  pevalAbsNumTerm :: Term (WordN n) -> Term (WordN n)
pevalAbsNumTerm = Term (WordN n) -> Term (WordN n)
forall a. (PEvalNumTerm a, Bits a) => Term a -> Term a
pevalBitsAbsNumTerm
  pevalSignumNumTerm :: Term (WordN n) -> Term (WordN n)
pevalSignumNumTerm = Term (WordN n) -> Term (WordN n)
forall a. PEvalNumTerm a => Term a -> Term a
pevalGeneralSignumNumTerm
  withSbvNumTermConstraint :: forall r. (Num (SBVType (WordN n)) => r) -> r
withSbvNumTermConstraint Num (SBVType (WordN n)) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(WordN n) r
Num (SBVType (WordN n)) => r
(PrimConstraint (WordN n), SMTDefinable (SBVType (WordN n)),
 Mergeable (SBVType (WordN n)), Typeable (SBVType (WordN n))) =>
r
r

instance (KnownNat n, 1 <= n) => PEvalNumTerm (IntN n) where
  pevalAddNumTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalAddNumTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a. (PEvalNumTerm a, Eq a) => Term a -> Term a -> Term a
pevalDefaultAddNumTerm
  pevalNegNumTerm :: Term (IntN n) -> Term (IntN n)
pevalNegNumTerm = Term (IntN n) -> Term (IntN n)
forall a. (PEvalNumTerm a, Eq a) => Term a -> Term a
pevalDefaultNegNumTerm
  pevalMulNumTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalMulNumTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a. (PEvalNumTerm a, Eq a) => Term a -> Term a -> Term a
pevalDefaultMulNumTerm
  pevalAbsNumTerm :: Term (IntN n) -> Term (IntN n)
pevalAbsNumTerm = Term (IntN n) -> Term (IntN n)
forall a. (PEvalNumTerm a, Bits a) => Term a -> Term a
pevalBitsAbsNumTerm
  pevalSignumNumTerm :: Term (IntN n) -> Term (IntN n)
pevalSignumNumTerm = Term (IntN n) -> Term (IntN n)
forall a. PEvalNumTerm a => Term a -> Term a
pevalGeneralSignumNumTerm
  withSbvNumTermConstraint :: forall r. (Num (SBVType (IntN n)) => r) -> r
withSbvNumTermConstraint Num (SBVType (IntN n)) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(IntN n) r
Num (SBVType (IntN n)) => r
(PrimConstraint (IntN n), SMTDefinable (SBVType (IntN n)),
 Mergeable (SBVType (IntN n)), Typeable (SBVType (IntN n))) =>
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