{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# HLINT ignore "Eta reduce" #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm
-- 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.PEvalDivModIntegralTerm
  ( pevalDefaultDivIntegralTerm,
    pevalDefaultDivBoundedIntegralTerm,
    pevalDefaultModIntegralTerm,
    pevalDefaultQuotIntegralTerm,
    pevalDefaultQuotBoundedIntegralTerm,
    pevalDefaultRemIntegralTerm,
  )
where

import GHC.TypeNats (KnownNat, type (<=))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim ()
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalDivModIntegralTerm
      ( pevalDivIntegralTerm,
        pevalModIntegralTerm,
        pevalQuotIntegralTerm,
        pevalRemIntegralTerm,
        withSbvDivModIntegralTermConstraint
      ),
    SupportedPrim (withPrim),
    Term,
    conTerm,
    divIntegralTerm,
    modIntegralTerm,
    quotIntegralTerm,
    remIntegralTerm,
    pattern ConTerm,
    pattern SupportedTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold (binaryUnfoldOnce)

-- | Default partial evaluation of division operation for integral types.
pevalDefaultDivIntegralTerm ::
  (PEvalDivModIntegralTerm a, Integral a) => Term a -> Term a -> Term a
pevalDefaultDivIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultDivIntegralTerm 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.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultDivIntegralTerm TotalRuleBinary a a a
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
divIntegralTerm Term a
l Term a
r

doPevalDefaultDivIntegralTerm ::
  (PEvalDivModIntegralTerm a, Integral a) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultDivIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultDivIntegralTerm (ConTerm a
a) (ConTerm a
b)
  | a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0 = 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. Integral a => a -> a -> a
`div` a
b
doPevalDefaultDivIntegralTerm Term a
a (ConTerm a
1) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
a
doPevalDefaultDivIntegralTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

-- | Default partial evaluation of division operation for bounded integral
-- types.
pevalDefaultDivBoundedIntegralTerm ::
  (PEvalDivModIntegralTerm a, Bounded a, Integral a) =>
  Term a ->
  Term a ->
  Term a
pevalDefaultDivBoundedIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultDivBoundedIntegralTerm 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.
(PEvalDivModIntegralTerm a, Bounded a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultDivBoundedIntegralTerm TotalRuleBinary a a a
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
divIntegralTerm Term a
l Term a
r

doPevalDefaultDivBoundedIntegralTerm ::
  (PEvalDivModIntegralTerm a, Bounded a, Integral a) =>
  Term a ->
  Term a ->
  Maybe (Term a)
doPevalDefaultDivBoundedIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Bounded a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultDivBoundedIntegralTerm (ConTerm a
a) (ConTerm a
b)
  | a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0 Bool -> Bool -> Bool
&& (a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= -a
1 Bool -> Bool -> Bool
|| a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
forall a. Bounded a => a
minBound) = 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. Integral a => a -> a -> a
`div` a
b
doPevalDefaultDivBoundedIntegralTerm Term a
a (ConTerm a
1) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
a
doPevalDefaultDivBoundedIntegralTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

-- | Default partial evaluation of modulo operation for integral types.
pevalDefaultModIntegralTerm ::
  (PEvalDivModIntegralTerm a, Integral a) => Term a -> Term a -> Term a
pevalDefaultModIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultModIntegralTerm 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.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultModIntegralTerm TotalRuleBinary a a a
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
modIntegralTerm Term a
l Term a
r

doPevalDefaultModIntegralTerm ::
  (PEvalDivModIntegralTerm a, Integral a) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultModIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultModIntegralTerm (ConTerm a
a) (ConTerm a
b)
  | a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0 = 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. Integral a => a -> a -> a
`mod` a
b
doPevalDefaultModIntegralTerm Term a
_ (ConTerm a
1) = 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
doPevalDefaultModIntegralTerm Term a
_ (ConTerm (-1)) = 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
doPevalDefaultModIntegralTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

-- | Default partial evaluation of quotient operation for integral types.
pevalDefaultQuotIntegralTerm ::
  (PEvalDivModIntegralTerm a, Integral a) => Term a -> Term a -> Term a
pevalDefaultQuotIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultQuotIntegralTerm 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.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultQuotIntegralTerm TotalRuleBinary a a a
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
quotIntegralTerm Term a
l Term a
r

doPevalDefaultQuotIntegralTerm ::
  (PEvalDivModIntegralTerm a, Integral a) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultQuotIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultQuotIntegralTerm (ConTerm a
a) (ConTerm a
b)
  | a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0 = 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. Integral a => a -> a -> a
`quot` a
b
doPevalDefaultQuotIntegralTerm Term a
a (ConTerm a
1) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
a
doPevalDefaultQuotIntegralTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

-- | Default partial evaluation of quotient operation for bounded integral
-- types.
pevalDefaultQuotBoundedIntegralTerm ::
  (PEvalDivModIntegralTerm a, Bounded a, Integral a) =>
  Term a ->
  Term a ->
  Term a
pevalDefaultQuotBoundedIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultQuotBoundedIntegralTerm 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.
(PEvalDivModIntegralTerm a, Bounded a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultQuotBoundedIntegralTerm TotalRuleBinary a a a
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
quotIntegralTerm Term a
l Term a
r

doPevalDefaultQuotBoundedIntegralTerm ::
  (PEvalDivModIntegralTerm a, Bounded a, Integral a) =>
  Term a ->
  Term a ->
  Maybe (Term a)
doPevalDefaultQuotBoundedIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Bounded a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultQuotBoundedIntegralTerm (ConTerm a
a) (ConTerm a
b)
  | a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0 Bool -> Bool -> Bool
&& (a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= -a
1 Bool -> Bool -> Bool
|| a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
forall a. Bounded a => a
minBound) = 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. Integral a => a -> a -> a
`quot` a
b
doPevalDefaultQuotBoundedIntegralTerm Term a
a (ConTerm a
1) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
a
doPevalDefaultQuotBoundedIntegralTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

-- | Default partial evaluation of remainder operation for integral types.
pevalDefaultRemIntegralTerm ::
  (PEvalDivModIntegralTerm a, Integral a) => Term a -> Term a -> Term a
pevalDefaultRemIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultRemIntegralTerm 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.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultRemIntegralTerm TotalRuleBinary a a a
forall a. PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
remIntegralTerm Term a
l Term a
r

doPevalDefaultRemIntegralTerm ::
  (PEvalDivModIntegralTerm a, Integral a) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultRemIntegralTerm :: forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultRemIntegralTerm (ConTerm a
a) (ConTerm a
b)
  | a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0 = 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. Integral a => a -> a -> a
`rem` a
b
doPevalDefaultRemIntegralTerm Term a
_ (ConTerm a
1) = 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
doPevalDefaultRemIntegralTerm Term a
_ (ConTerm (-1)) = 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
doPevalDefaultRemIntegralTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

instance PEvalDivModIntegralTerm Integer where
  pevalDivIntegralTerm :: Term Integer -> Term Integer -> Term Integer
pevalDivIntegralTerm = Term Integer -> Term Integer -> Term Integer
forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultDivIntegralTerm
  pevalModIntegralTerm :: Term Integer -> Term Integer -> Term Integer
pevalModIntegralTerm = Term Integer -> Term Integer -> Term Integer
forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultModIntegralTerm
  pevalQuotIntegralTerm :: Term Integer -> Term Integer -> Term Integer
pevalQuotIntegralTerm = Term Integer -> Term Integer -> Term Integer
forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultQuotIntegralTerm
  pevalRemIntegralTerm :: Term Integer -> Term Integer -> Term Integer
pevalRemIntegralTerm = Term Integer -> Term Integer -> Term Integer
forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultRemIntegralTerm
  withSbvDivModIntegralTermConstraint :: forall r. (SDivisible (SBVType Integer) => r) -> r
withSbvDivModIntegralTermConstraint SDivisible (SBVType Integer) => r
r = r
SDivisible (SBVType Integer) => r
r

instance (KnownNat n, 1 <= n) => PEvalDivModIntegralTerm (IntN n) where
  pevalDivIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalDivIntegralTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(PEvalDivModIntegralTerm a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultDivBoundedIntegralTerm
  pevalModIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalModIntegralTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultModIntegralTerm
  pevalQuotIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalQuotIntegralTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(PEvalDivModIntegralTerm a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultQuotBoundedIntegralTerm
  pevalRemIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalRemIntegralTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultRemIntegralTerm
  withSbvDivModIntegralTermConstraint :: forall r. (SDivisible (SBVType (IntN n)) => r) -> r
withSbvDivModIntegralTermConstraint SDivisible (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
SDivisible (SBVType (IntN n)) => r
(PrimConstraint (IntN n), SMTDefinable (SBVType (IntN n)),
 Mergeable (SBVType (IntN n)), Typeable (SBVType (IntN n))) =>
r
r

instance (KnownNat n, 1 <= n) => PEvalDivModIntegralTerm (WordN n) where
  pevalDivIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalDivIntegralTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultDivIntegralTerm
  pevalModIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalModIntegralTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultModIntegralTerm
  pevalQuotIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalQuotIntegralTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultQuotIntegralTerm
  pevalRemIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalRemIntegralTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a.
(PEvalDivModIntegralTerm a, Integral a) =>
Term a -> Term a -> Term a
pevalDefaultRemIntegralTerm
  withSbvDivModIntegralTermConstraint :: forall r. (SDivisible (SBVType (WordN n)) => r) -> r
withSbvDivModIntegralTermConstraint SDivisible (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
SDivisible (SBVType (WordN n)) => r
(PrimConstraint (WordN n), SMTDefinable (SBVType (WordN n)),
 Mergeable (SBVType (WordN n)), Typeable (SBVType (WordN n))) =>
r
r