-- |
-- 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 = forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce Term Integer -> Term Integer -> Maybe (Term Integer)
doPevalDivIntegerTerm Term Integer -> Term Integer -> Term Integer
divIntegerTerm

doPevalDivIntegerTerm :: Term Integer -> Term Integer -> Maybe (Term Integer)
doPevalDivIntegerTerm :: Term Integer -> Term Integer -> Maybe (Term Integer)
doPevalDivIntegerTerm (ConTerm Id
_ Integer
a) (ConTerm Id
_ Integer
b) | Integer
b forall a. Eq a => a -> a -> Bool
/= Integer
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
$ Integer
a forall a. Integral a => a -> a -> a
`div` Integer
b
doPevalDivIntegerTerm Term Integer
a (ConTerm Id
_ Integer
1) = forall a. a -> Maybe a
Just Term Integer
a
doPevalDivIntegerTerm Term Integer
_ Term Integer
_ = forall a. Maybe a
Nothing

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

doPevalModIntegerTerm :: Term Integer -> Term Integer -> Maybe (Term Integer)
doPevalModIntegerTerm :: Term Integer -> Term Integer -> Maybe (Term Integer)
doPevalModIntegerTerm (ConTerm Id
_ Integer
a) (ConTerm Id
_ Integer
b) | Integer
b forall a. Eq a => a -> a -> Bool
/= Integer
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
$ Integer
a forall a. Integral a => a -> a -> a
`mod` Integer
b
doPevalModIntegerTerm Term Integer
_ (ConTerm Id
_ Integer
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 Integer
0
doPevalModIntegerTerm Term Integer
_ (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 Integer
0
doPevalModIntegerTerm Term Integer
_ Term Integer
_ = forall a. Maybe a
Nothing