{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# 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.BV (IntN, WordN)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim ()
import Grisette.Internal.SymPrim.Prim.Internal.IsZero
  ( IsZeroCases (IsZeroEvidence, NonZeroEvidence),
    KnownIsZero (isZero),
  )
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalNumTerm
      ( pevalAbsNumTerm,
        pevalAddNumTerm,
        pevalMulNumTerm,
        pevalNegNumTerm,
        pevalSignumNumTerm,
        withSbvNumTermConstraint
      ),
    SupportedPrim (withPrim),
    Term (AbsNumTerm, AddNumTerm, ConTerm, MulNumTerm, NegNumTerm),
    absNumTerm,
    addNumTerm,
    conTerm,
    mulNumTerm,
    negNumTerm,
    pevalSubNumTerm,
    signumNumTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold
  ( binaryUnfoldOnce,
    unaryUnfoldOnce,
  )

-- Add
pevalDefaultAddNumTerm :: (PEvalNumTerm a) => Term a -> Term a -> Term a
pevalDefaultAddNumTerm :: forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalDefaultAddNumTerm =
  PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce
    PartialRuleBinary a a a
forall a. PEvalNumTerm 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)

doPevalDefaultAddNumTerm ::
  (PEvalNumTerm a) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultAddNumTerm :: forall a. PEvalNumTerm a => Term a -> Term a -> Maybe (Term a)
doPevalDefaultAddNumTerm (ConTerm Id
_ a
a) (ConTerm Id
_ 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, Typeable t, Hashable t, Eq t, Show 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 Id
_ 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 Id
_ (ConTerm Id
_ 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, Typeable t, Hashable t, Eq t, Show 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 Id
_ a
_) = Term a -> Term a -> Maybe (Term a)
forall a. PEvalNumTerm 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 Id
_ 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 Id
_ 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 Id
_ Term a
i) (NegNumTerm Id
_ 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 Id
_ (ConTerm Id
_ a
i) Term a
j)
  (MulNumTerm Id
_ (ConTerm Id
_ 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, Typeable t, Hashable t, Eq t, Show 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 Id
_ i :: Term a
i@ConTerm {} Term a
j)
  (MulNumTerm Id
_ k :: Term a
k@(ConTerm Id
_ a
_) 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 Id
_ Term a
l r :: Term a
r@(ConTerm Id
_ a
_)) = 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

-- Neg
pevalDefaultNegNumTerm :: (PEvalNumTerm a) => Term a -> Term a
pevalDefaultNegNumTerm :: forall a. PEvalNumTerm a => Term a -> Term a
pevalDefaultNegNumTerm = 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

doPevalDefaultNegNumTerm :: (PEvalNumTerm a) => Term a -> Maybe (Term a)
doPevalDefaultNegNumTerm :: forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalDefaultNegNumTerm (ConTerm Id
_ 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, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ -a
a
doPevalDefaultNegNumTerm (NegNumTerm Id
_ Term a
v) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
v
doPevalDefaultNegNumTerm (AddNumTerm Id
_ (ConTerm Id
_ 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, Typeable t, Hashable t, Eq t, Show 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 Id
_ (NegNumTerm Id
_ 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 Id
_ Term a
l (NegNumTerm Id
_ 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 Id
_ (ConTerm Id
_ 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, Typeable t, Hashable t, Eq t, Show 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 Id
_ (NegNumTerm Id
_ Term a
_) Term a
_) =
  [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalDefaultNegNumTerm (MulNumTerm Id
_ Term a
_ (NegNumTerm Id
_ Term a
_)) =
  [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalDefaultNegNumTerm (AddNumTerm Id
_ 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) => Term a -> Term a -> Term a
pevalDefaultMulNumTerm :: forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalDefaultMulNumTerm =
  PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce
    PartialRuleBinary a a a
forall a. PEvalNumTerm 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)

normalizeMulNum :: (PEvalNumTerm a) => Term a -> Term a
normalizeMulNum :: forall a. PEvalNumTerm a => Term a -> Term a
normalizeMulNum (MulNumTerm Id
_ Term a
l r :: Term a
r@(ConTerm Id
_ a
_)) = 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) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultMulNumTerm :: forall a. PEvalNumTerm a => Term a -> Term a -> Maybe (Term a)
doPevalDefaultMulNumTerm (ConTerm Id
_ a
a) (ConTerm Id
_ 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, Typeable t, Hashable t, Eq t, Show 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 Id
_ 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, Typeable t, Hashable t, Eq t, Show 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 Id
_ (ConTerm Id
_ 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, Typeable t, Hashable t, Eq t, Show 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 Id
_ (ConTerm Id
_ 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, Typeable t, Hashable t, Eq t, Show 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, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
l1) Term a
k)
  (a
l1, NegNumTerm Id
_ 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, Typeable t, Hashable t, Eq t, Show 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 Id
_ Term a
_ ConTerm {}) -> [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
  (a
_, AddNumTerm Id
_ 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 Id
_ a
_) = Term a -> Term a -> Maybe (Term a)
forall a. PEvalNumTerm 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 Id
_ 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 Id
_ 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 Id
_ 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 Id
_ 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 Id
_ Term a
_ ConTerm {}) Term a
_ =
  [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalDefaultMulNumTermNoCon Term a
_ (MulNumTerm Id
_ 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 =
  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

doPevalGeneralAbsNumTerm :: (PEvalNumTerm a) => Term a -> Maybe (Term a)
doPevalGeneralAbsNumTerm :: forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalGeneralAbsNumTerm (ConTerm Id
_ 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, Typeable t, Hashable t, Eq t, Show 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 Id
_ 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 Id
_ Term a
_) = 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
    ]

-- Signum

pevalGeneralSignumNumTerm :: (PEvalNumTerm a) => Term a -> Term a
pevalGeneralSignumNumTerm :: forall a. PEvalNumTerm a => Term a -> Term a
pevalGeneralSignumNumTerm =
  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

doPevalGeneralSignumNumTerm :: (PEvalNumTerm a) => Term a -> Maybe (Term a)
doPevalGeneralSignumNumTerm :: forall a. PEvalNumTerm a => Term a -> Maybe (Term a)
doPevalGeneralSignumNumTerm (ConTerm Id
_ 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, Typeable t, Hashable t, Eq t, Show 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

instance PEvalNumTerm Integer where
  pevalAddNumTerm :: Term Integer -> Term Integer -> Term Integer
pevalAddNumTerm = Term Integer -> Term Integer -> Term Integer
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalDefaultAddNumTerm
  pevalNegNumTerm :: Term Integer -> Term Integer
pevalNegNumTerm = Term Integer -> Term Integer
forall a. PEvalNumTerm a => Term a -> Term a
pevalDefaultNegNumTerm
  pevalMulNumTerm :: Term Integer -> Term Integer -> Term Integer
pevalMulNumTerm = Term Integer -> Term Integer -> Term Integer
forall a. PEvalNumTerm 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)
doPevalIntegerAbsNumTerm Term Integer -> Term Integer
forall a. PEvalNumTerm a => Term a -> Term a
absNumTerm
    where
      doPevalIntegerAbsNumTerm :: Term a -> Maybe (Term a)
doPevalIntegerAbsNumTerm 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 Id
_ 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
          ]
  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)
doPevalIntegerSignumNumTerm Term Integer -> Term Integer
forall a. PEvalNumTerm a => Term a -> Term a
signumNumTerm
    where
      doPevalIntegerSignumNumTerm :: Term a -> Maybe (Term a)
doPevalIntegerSignumNumTerm 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 Id
_ 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 Id
_ 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
          ]
  withSbvNumTermConstraint :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (Num (SBVType n Integer) => r) -> r
withSbvNumTermConstraint proxy n
p Num (SBVType n Integer) => r
r = case proxy n -> IsZeroCases n
forall (a :: Nat) (proxy :: Nat -> *).
KnownIsZero a =>
proxy a -> IsZeroCases a
forall (proxy :: Nat -> *). proxy n -> IsZeroCases n
isZero proxy n
p of
    IsZeroCases n
IsZeroEvidence -> r
Num (SBVType n Integer) => r
r
    IsZeroCases n
NonZeroEvidence -> r
Num (SBVType n 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 => 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 => 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 => 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 (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (Num (SBVType n (WordN n)) => r) -> r
withSbvNumTermConstraint proxy n
p Num (SBVType n (WordN n)) => 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 @(WordN n) proxy n
p r
Num (SBVType n (WordN n)) => r
(PrimConstraint n (WordN n), SMTDefinable (SBVType n (WordN n)),
 Mergeable (SBVType n (WordN n)), Typeable (SBVType n (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 => 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 => 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 => 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 (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (Num (SBVType n (IntN n)) => r) -> r
withSbvNumTermConstraint proxy n
p Num (SBVType n (IntN n)) => 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 @(IntN n) proxy n
p r
Num (SBVType n (IntN n)) => r
(PrimConstraint n (IntN n), SMTDefinable (SBVType n (IntN n)),
 Mergeable (SBVType n (IntN n)), Typeable (SBVType n (IntN n))) =>
r
r