-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.PartialEval.Integer
-- 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.Integer
  ( pevalDivIntegerTerm,
    pevalModIntegerTerm,
  )
where

import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold

-- div
pevalDivIntegerTerm :: Term Integer -> Term Integer -> Term Integer
pevalDivIntegerTerm :: Term Integer -> Term Integer -> Term Integer
pevalDivIntegerTerm = PartialRuleBinary Integer Integer Integer
-> (Term Integer -> Term Integer -> Term Integer)
-> Term Integer
-> Term Integer
-> Term Integer
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary Integer Integer Integer
doPevalDivIntegerTerm Term Integer -> Term Integer -> Term Integer
divIntegerTerm

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

-- mod
pevalModIntegerTerm :: Term Integer -> Term Integer -> Term Integer
pevalModIntegerTerm :: Term Integer -> Term Integer -> Term Integer
pevalModIntegerTerm = PartialRuleBinary Integer Integer Integer
-> (Term Integer -> Term Integer -> Term Integer)
-> Term Integer
-> Term Integer
-> Term Integer
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary Integer Integer Integer
doPevalModIntegerTerm Term Integer -> Term Integer -> Term Integer
modIntegerTerm

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