{-# LANGUAGE ScopedTypeVariables #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
  ( pevalDivIntegralTerm,
    pevalModIntegralTerm,
    pevalQuotIntegralTerm,
    pevalRemIntegralTerm,
    pevalDivBoundedIntegralTerm,
    pevalModBoundedIntegralTerm,
    pevalQuotBoundedIntegralTerm,
    pevalRemBoundedIntegralTerm,
  )
where

import Grisette.Core.Data.BV
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold
import Grisette.IR.SymPrim.Data.Prim.Utils

-- div
pevalDivIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
pevalDivIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalDivIntegralTerm = forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDivIntegralTerm forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
divIntegralTerm

doPevalDivIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Maybe (Term a)
doPevalDivIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDivIntegralTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) | a
b forall a. Eq a => a -> a -> Bool
/= a
0 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
a forall a. Integral a => a -> a -> a
`div` a
b
doPevalDivIntegralTerm Term a
a (ConTerm Id
_ a
1) = forall a. a -> Maybe a
Just Term a
a
doPevalDivIntegralTerm Term a
_ Term a
_ = forall a. Maybe a
Nothing

pevalDivBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Term a
pevalDivBoundedIntegralTerm :: forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalDivBoundedIntegralTerm = forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDivBoundedIntegralTerm forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
divBoundedIntegralTerm

doPevalDivBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Maybe (Term a)
doPevalDivBoundedIntegralTerm :: forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDivBoundedIntegralTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) | a
b forall a. Eq a => a -> a -> Bool
/= a
0 Bool -> Bool -> Bool
&& (a
b forall a. Eq a => a -> a -> Bool
/= -a
1 Bool -> Bool -> Bool
|| a
a forall a. Eq a => a -> a -> Bool
/= forall a. Bounded a => a
minBound) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
a forall a. Integral a => a -> a -> a
`div` a
b
doPevalDivBoundedIntegralTerm Term a
a (ConTerm Id
_ a
1) = forall a. a -> Maybe a
Just Term a
a
doPevalDivBoundedIntegralTerm Term a
_ Term a
_ = forall a. Maybe a
Nothing

-- mod
pevalModIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
pevalModIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalModIntegralTerm = forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalModIntegralTerm forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
modIntegralTerm

doPevalModIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Maybe (Term a)
doPevalModIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalModIntegralTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) | a
b forall a. Eq a => a -> a -> Bool
/= a
0 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
a forall a. Integral a => a -> a -> a
`mod` a
b
doPevalModIntegralTerm Term a
_ (ConTerm Id
_ a
1) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
0
doPevalModIntegralTerm Term a
_ (ConTerm Id
_ (-1)) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
0
doPevalModIntegralTerm Term a
_ Term a
_ = forall a. Maybe a
Nothing

pevalModBoundedIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
pevalModBoundedIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalModBoundedIntegralTerm = forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalModIntegralTerm

-- quot
pevalQuotIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
pevalQuotIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalQuotIntegralTerm = forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalQuotIntegralTerm forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
quotIntegralTerm

doPevalQuotIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Maybe (Term a)
doPevalQuotIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalQuotIntegralTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) | a
b forall a. Eq a => a -> a -> Bool
/= a
0 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
a forall a. Integral a => a -> a -> a
`quot` a
b
doPevalQuotIntegralTerm Term a
a (ConTerm Id
_ a
1) = forall a. a -> Maybe a
Just Term a
a
doPevalQuotIntegralTerm Term a
_ Term a
_ = forall a. Maybe a
Nothing

pevalQuotBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Term a
pevalQuotBoundedIntegralTerm :: forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalQuotBoundedIntegralTerm = forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalQuotBoundedIntegralTerm forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
quotBoundedIntegralTerm

doPevalQuotBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Maybe (Term a)
doPevalQuotBoundedIntegralTerm :: forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalQuotBoundedIntegralTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) | a
b forall a. Eq a => a -> a -> Bool
/= a
0 Bool -> Bool -> Bool
&& (a
b forall a. Eq a => a -> a -> Bool
/= -a
1 Bool -> Bool -> Bool
|| a
a forall a. Eq a => a -> a -> Bool
/= forall a. Bounded a => a
minBound) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
a forall a. Integral a => a -> a -> a
`quot` a
b
doPevalQuotBoundedIntegralTerm Term a
a (ConTerm Id
_ a
1) = forall a. a -> Maybe a
Just Term a
a
doPevalQuotBoundedIntegralTerm Term a
_ Term a
_ = forall a. Maybe a
Nothing

-- rem
pevalRemIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
pevalRemIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalRemIntegralTerm = forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalRemIntegralTerm forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
remIntegralTerm

doPevalRemIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Maybe (Term a)
doPevalRemIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalRemIntegralTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) | a
b forall a. Eq a => a -> a -> Bool
/= a
0 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
a forall a. Integral a => a -> a -> a
`rem` a
b
doPevalRemIntegralTerm Term a
_ (ConTerm Id
_ a
1) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
0
doPevalRemIntegralTerm Term a
_ (ConTerm Id
_ (-1)) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
0
doPevalRemIntegralTerm Term a
_ Term a
_ = forall a. Maybe a
Nothing

pevalRemBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Term a
pevalRemBoundedIntegralTerm :: forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalRemBoundedIntegralTerm = forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalRemIntegralTerm