{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
-- 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.InternedTerm.TermSubstitution
  ( substTerm,
  )
where

import Grisette.Core.Data.MemoUtils (htmemo)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
  ( conTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
  ( SomeTerm (SomeTerm),
  )
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
  ( BinaryOp (partialEvalBinary),
    SupportedPrim,
    Term
      ( AbsNumTerm,
        AddNumTerm,
        AndBitsTerm,
        AndTerm,
        BVConcatTerm,
        BVExtendTerm,
        BVSelectTerm,
        BVToSignedTerm,
        BVToUnsignedTerm,
        BinaryTerm,
        ComplementBitsTerm,
        ConTerm,
        DivBoundedIntegralTerm,
        DivIntegralTerm,
        EqvTerm,
        GeneralFunApplyTerm,
        ITETerm,
        LENumTerm,
        LTNumTerm,
        ModBoundedIntegralTerm,
        ModIntegralTerm,
        NotTerm,
        OrBitsTerm,
        OrTerm,
        QuotBoundedIntegralTerm,
        QuotIntegralTerm,
        RemBoundedIntegralTerm,
        RemIntegralTerm,
        RotateBitsTerm,
        ShiftBitsTerm,
        SignumNumTerm,
        SymTerm,
        TabularFunApplyTerm,
        TernaryTerm,
        TimesNumTerm,
        UMinusNumTerm,
        UnaryTerm,
        XorBitsTerm
      ),
    TernaryOp (partialEvalTernary),
    TypedSymbol,
    UnaryOp (partialEvalUnary),
    someTypedSymbol,
    type (-->) (GeneralFun),
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
  ( pevalBVConcatTerm,
    pevalBVExtendTerm,
    pevalBVSelectTerm,
    pevalBVToSignedTerm,
    pevalBVToUnsignedTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
  ( pevalAndBitsTerm,
    pevalComplementBitsTerm,
    pevalOrBitsTerm,
    pevalRotateBitsTerm,
    pevalShiftBitsTerm,
    pevalXorBitsTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
  ( pevalAndTerm,
    pevalEqvTerm,
    pevalITETerm,
    pevalNotTerm,
    pevalOrTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
  ( pevalGeneralFunApplyTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
  ( pevalDivBoundedIntegralTerm,
    pevalDivIntegralTerm,
    pevalModBoundedIntegralTerm,
    pevalModIntegralTerm,
    pevalQuotBoundedIntegralTerm,
    pevalQuotIntegralTerm,
    pevalRemBoundedIntegralTerm,
    pevalRemIntegralTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
  ( pevalAbsNumTerm,
    pevalAddNumTerm,
    pevalLeNumTerm,
    pevalLtNumTerm,
    pevalSignumNumTerm,
    pevalTimesNumTerm,
    pevalUMinusNumTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
  ( pevalTabularFunApplyTerm,
  )
import Type.Reflection
  ( TypeRep,
    eqTypeRep,
    typeRep,
    pattern App,
    type (:~~:) (HRefl),
  )
import Unsafe.Coerce (unsafeCoerce)

substTerm :: forall a b. (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term a -> Term b -> Term b
substTerm :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
sym Term a
term = forall x. SupportedPrim x => Term x -> Term x
gov
  where
    gov :: (SupportedPrim x) => Term x -> Term x
    gov :: forall x. SupportedPrim x => Term x -> Term x
gov Term x
b = case SomeTerm -> SomeTerm
go (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term x
b) of
      SomeTerm Term a
v -> forall a b. a -> b
unsafeCoerce Term a
v
    go :: SomeTerm -> SomeTerm
    go :: SomeTerm -> SomeTerm
go = forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo forall a b. (a -> b) -> a -> b
$ \stm :: SomeTerm
stm@(SomeTerm (Term a
tm :: Term v)) ->
      case Term a
tm of
        ConTerm Id
_ a
cv -> case (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep v) of
          App (App TypeRep a
gf TypeRep b
_) TypeRep b
_ ->
            case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
gf (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(-->)) of
              Just a :~~: (-->)
HRefl -> case a
cv of
                GeneralFun TypedSymbol b
sym1 Term b
tm1 ->
                  if forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol b
sym1 forall a. Eq a => a -> a -> Bool
== forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
sym
                    then SomeTerm
stm
                    else forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm 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
$ forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol b
sym1 (forall x. SupportedPrim x => Term x -> Term x
gov Term b
tm1)
              Maybe (a :~~: (-->))
Nothing -> SomeTerm
stm
          TypeRep a
_ -> SomeTerm
stm
        SymTerm Id
_ TypedSymbol a
ts -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ if forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
ts forall a. Eq a => a -> a -> Bool
== forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
sym then forall a b. a -> b
unsafeCoerce Term a
term else Term a
tm
        UnaryTerm Id
_ tag
tag Term arg
te -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall tag arg t.
(UnaryOp tag arg t, Typeable tag, Typeable t) =>
tag -> Term arg -> Term t
partialEvalUnary tag
tag (forall x. SupportedPrim x => Term x -> Term x
gov Term arg
te)
        BinaryTerm Id
_ tag
tag Term arg1
te Term arg2
te' -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall tag arg1 arg2 t.
(BinaryOp tag arg1 arg2 t, Typeable tag, Typeable t) =>
tag -> Term arg1 -> Term arg2 -> Term t
partialEvalBinary tag
tag (forall x. SupportedPrim x => Term x -> Term x
gov Term arg1
te) (forall x. SupportedPrim x => Term x -> Term x
gov Term arg2
te')
        TernaryTerm Id
_ tag
tag Term arg1
op1 Term arg2
op2 Term arg3
op3 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall tag arg1 arg2 arg3 t.
(TernaryOp tag arg1 arg2 arg3 t, Typeable tag, Typeable t) =>
tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
partialEvalTernary tag
tag (forall x. SupportedPrim x => Term x -> Term x
gov Term arg1
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term arg2
op2) (forall x. SupportedPrim x => Term x -> Term x
gov Term arg3
op3)
        NotTerm Id
_ Term Bool
op -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
pevalNotTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op)
        OrTerm Id
_ Term Bool
op1 Term Bool
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op2)
        AndTerm Id
_ Term Bool
op1 Term Bool
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op2)
        EqvTerm Id
_ Term t1
op1 Term t1
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op2)
        ITETerm Id
_ Term Bool
c Term a
op1 Term a
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm (forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
c) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        AddNumTerm Id
_ Term a
op1 Term a
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        UMinusNumTerm Id
_ Term a
op -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        TimesNumTerm Id
_ Term a
op1 Term a
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        AbsNumTerm Id
_ Term a
op -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        SignumNumTerm Id
_ Term a
op -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        LTNumTerm Id
_ Term t1
op1 Term t1
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op2)
        LENumTerm Id
_ Term t1
op1 Term t1
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op2)
        AndBitsTerm Id
_ Term a
op1 Term a
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAndBitsTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        OrBitsTerm Id
_ Term a
op1 Term a
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalOrBitsTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        XorBitsTerm Id
_ Term a
op1 Term a
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalXorBitsTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        ComplementBitsTerm Id
_ Term a
op -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        ShiftBitsTerm Id
_ Term a
op Id
n -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Id -> Term a
pevalShiftBitsTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op) Id
n
        RotateBitsTerm Id
_ Term a
op Id
n -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Id -> Term a
pevalRotateBitsTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op) Id
n
        BVToSignedTerm Id
_ Term (ubv n)
op -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall (ubv :: Nat -> *) (sbv :: Nat -> *) (n :: Nat).
(forall (n1 :: Nat).
 (KnownNat n1, 1 <= n1) =>
 SupportedPrim (ubv n1),
 forall (n1 :: Nat).
 (KnownNat n1, 1 <= n1) =>
 SupportedPrim (sbv n1),
 Typeable ubv, Typeable sbv, KnownNat n, 1 <= n,
 BVSignConversion (ubv n) (sbv n)) =>
Term (ubv n) -> Term (sbv n)
pevalBVToSignedTerm Term (ubv n)
op
        BVToUnsignedTerm Id
_ Term (sbv n)
op -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall (ubv :: Nat -> *) (sbv :: Nat -> *) (n :: Nat).
(forall (n1 :: Nat).
 (KnownNat n1, 1 <= n1) =>
 SupportedPrim (ubv n1),
 forall (n1 :: Nat).
 (KnownNat n1, 1 <= n1) =>
 SupportedPrim (sbv n1),
 Typeable ubv, Typeable sbv, KnownNat n, 1 <= n,
 BVSignConversion (ubv n) (sbv n)) =>
Term (sbv n) -> Term (ubv n)
pevalBVToUnsignedTerm Term (sbv n)
op
        BVConcatTerm Id
_ Term (bv a)
op1 Term (bv b)
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall (bv :: Nat -> *) (a :: Nat) (b :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat a, KnownNat b, KnownNat (a + b), 1 <= a,
 1 <= b, 1 <= (a + b), SizedBV bv) =>
Term (bv a) -> Term (bv b) -> Term (bv (a + b))
pevalBVConcatTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term (bv a)
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term (bv b)
op2)
        BVSelectTerm Id
_ TypeRep ix
ix TypeRep w
w Term (bv n)
op -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
       (p :: Nat -> *) (q :: Nat -> *).
(forall (n1 :: Nat).
 (KnownNat n1, 1 <= n1) =>
 SupportedPrim (bv n1),
 Typeable bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n, SizedBV bv) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
pevalBVSelectTerm TypeRep ix
ix TypeRep w
w (forall x. SupportedPrim x => Term x -> Term x
gov Term (bv n)
op)
        BVExtendTerm Id
_ Bool
n TypeRep r
signed Term (bv l)
op -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
 SizedBV bv) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalBVExtendTerm Bool
n TypeRep r
signed (forall x. SupportedPrim x => Term x -> Term x
gov Term (bv l)
op)
        TabularFunApplyTerm Id
_ Term (a =-> a)
f Term a
op -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> Term a -> Term b
pevalTabularFunApplyTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term (a =-> a)
f) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        GeneralFunApplyTerm Id
_ Term (a --> a)
f Term a
op -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term (a --> a)
f) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        DivIntegralTerm Id
_ Term a
op1 Term a
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalDivIntegralTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        ModIntegralTerm Id
_ Term a
op1 Term a
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalModIntegralTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        QuotIntegralTerm Id
_ Term a
op1 Term a
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalQuotIntegralTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        RemIntegralTerm Id
_ Term a
op1 Term a
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalRemIntegralTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        DivBoundedIntegralTerm Id
_ Term a
op1 Term a
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalDivBoundedIntegralTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        ModBoundedIntegralTerm Id
_ Term a
op1 Term a
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalModBoundedIntegralTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        QuotBoundedIntegralTerm Id
_ Term a
op1 Term a
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalQuotBoundedIntegralTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        RemBoundedIntegralTerm Id
_ Term a
op1 Term a
op2 -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalRemBoundedIntegralTerm (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)