{-# 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,
        BinaryTerm,
        ComplementBitsTerm,
        ConTerm,
        DivBoundedIntegralTerm,
        DivIntegralTerm,
        EqvTerm,
        GeneralFunApplyTerm,
        ITETerm,
        LENumTerm,
        LTNumTerm,
        ModBoundedIntegralTerm,
        ModIntegralTerm,
        NotTerm,
        OrBitsTerm,
        OrTerm,
        QuotBoundedIntegralTerm,
        QuotIntegralTerm,
        RemBoundedIntegralTerm,
        RemIntegralTerm,
        RotateLeftTerm,
        RotateRightTerm,
        ShiftLeftTerm,
        ShiftRightTerm,
        SignumNumTerm,
        SymTerm,
        TabularFunApplyTerm,
        TernaryTerm,
        TimesNumTerm,
        ToSignedTerm,
        ToUnsignedTerm,
        UMinusNumTerm,
        UnaryTerm,
        XorBitsTerm
      ),
    TernaryOp (partialEvalTernary),
    TypedSymbol,
    UnaryOp (partialEvalUnary),
    someTypedSymbol,
    type (-->) (GeneralFun),
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
  ( pevalBVConcatTerm,
    pevalBVExtendTerm,
    pevalBVSelectTerm,
    pevalToSignedTerm,
    pevalToUnsignedTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
  ( pevalAndBitsTerm,
    pevalComplementBitsTerm,
    pevalOrBitsTerm,
    pevalRotateLeftTerm,
    pevalRotateRightTerm,
    pevalShiftLeftTerm,
    pevalShiftRightTerm,
    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 = Term b -> Term b
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 (Term x -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term x
b) of
      SomeTerm Term a
v -> Term a -> Term x
forall a b. a -> b
unsafeCoerce Term a
v
    go :: SomeTerm -> SomeTerm
    go :: SomeTerm -> SomeTerm
go = (SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo ((SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm)
-> (SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
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 (TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep v) of
          App (App TypeRep a
gf TypeRep b
_) TypeRep b
_ ->
            case TypeRep a -> TypeRep (-->) -> Maybe (a :~~: (-->))
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
forall (a :: * -> * -> *). Typeable a => TypeRep a
typeRep @(-->)) of
              Just a :~~: (-->)
HRefl -> case a
cv of
                GeneralFun TypedSymbol b
sym1 Term b
tm1 ->
                  if TypedSymbol b -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol b
sym1 SomeTypedSymbol -> SomeTypedSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
sym
                    then SomeTerm
stm
                    else Term (b --> b) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (b --> b) -> SomeTerm) -> Term (b --> b) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ (b --> b) -> Term (b --> b)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm ((b --> b) -> Term (b --> b)) -> (b --> b) -> Term (b --> b)
forall a b. (a -> b) -> a -> b
$ TypedSymbol b -> Term b -> b --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol b
sym1 (Term b -> Term b
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 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ if TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
ts SomeTypedSymbol -> SomeTypedSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
sym then Term a -> Term a
forall a b. a -> b
unsafeCoerce Term a
term else Term a
tm
        UnaryTerm Id
_ tag
tag Term arg
te -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ tag -> Term arg -> Term a
forall tag arg t.
(UnaryOp tag arg t, Typeable tag, Typeable t) =>
tag -> Term arg -> Term t
partialEvalUnary tag
tag (Term arg -> Term arg
forall x. SupportedPrim x => Term x -> Term x
gov Term arg
te)
        BinaryTerm Id
_ tag
tag Term arg1
te Term arg2
te' -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ tag -> Term arg1 -> Term arg2 -> Term a
forall tag arg1 arg2 t.
(BinaryOp tag arg1 arg2 t, Typeable tag, Typeable t) =>
tag -> Term arg1 -> Term arg2 -> Term t
partialEvalBinary tag
tag (Term arg1 -> Term arg1
forall x. SupportedPrim x => Term x -> Term x
gov Term arg1
te) (Term arg2 -> Term arg2
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 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term a
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 (Term arg1 -> Term arg1
forall x. SupportedPrim x => Term x -> Term x
gov Term arg1
op1) (Term arg2 -> Term arg2
forall x. SupportedPrim x => Term x -> Term x
gov Term arg2
op2) (Term arg3 -> Term arg3
forall x. SupportedPrim x => Term x -> Term x
gov Term arg3
op3)
        NotTerm Id
_ Term Bool
op -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
pevalNotTerm (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op)
        OrTerm Id
_ Term Bool
op1 Term Bool
op2 -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op1) (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op2)
        AndTerm Id
_ Term Bool
op1 Term Bool
op2 -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op1) (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op2)
        EqvTerm Id
_ Term t1
op1 Term t1
op2 -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term t1 -> Term t1 -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op1) (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op2)
        ITETerm Id
_ Term Bool
c Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term a -> Term a -> Term a
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
c) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        AddNumTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        UMinusNumTerm Id
_ Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        TimesNumTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        AbsNumTerm Id
_ Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        SignumNumTerm Id
_ Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        LTNumTerm Id
_ Term t1
op1 Term t1
op2 -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term t1 -> Term t1 -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op1) (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op2)
        LENumTerm Id
_ Term t1
op1 Term t1
op2 -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term t1 -> Term t1 -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op1) (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op2)
        AndBitsTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAndBitsTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        OrBitsTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalOrBitsTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        XorBitsTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalXorBitsTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        ComplementBitsTerm Id
_ Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        ShiftLeftTerm Id
_ Term a
op Term a
n -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalShiftLeftTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
n)
        RotateLeftTerm Id
_ Term a
op Term a
n -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(Integral a, SymRotate a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalRotateLeftTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
n)
        ShiftRightTerm Id
_ Term a
op Term a
n -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalShiftRightTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
n)
        RotateRightTerm Id
_ Term a
op Term a
n -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(Integral a, SymRotate a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalRotateRightTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
n)
        ToSignedTerm Id
_ Term u
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term u -> Term a
forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term u -> Term s
pevalToSignedTerm Term u
op
        ToUnsignedTerm Id
_ Term s
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term s -> Term a
forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term s -> Term u
pevalToUnsignedTerm Term s
op
        BVConcatTerm Id
_ Term (bv a)
op1 Term (bv b)
op2 -> Term (bv (a + b)) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (bv (a + b)) -> SomeTerm) -> Term (bv (a + b)) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term (bv a) -> Term (bv b) -> Term (bv (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 (Term (bv a) -> Term (bv a)
forall x. SupportedPrim x => Term x -> Term x
gov Term (bv a)
op1) (Term (bv b) -> Term (bv b)
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 -> Term (bv w) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (bv w) -> SomeTerm) -> Term (bv w) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ TypeRep ix -> TypeRep w -> Term (bv n) -> Term (bv w)
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 (Term (bv n) -> Term (bv n)
forall x. SupportedPrim x => Term x -> Term x
gov Term (bv n)
op)
        BVExtendTerm Id
_ Bool
n TypeRep r
signed Term (bv l)
op -> Term (bv r) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (bv r) -> SomeTerm) -> Term (bv r) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Bool -> TypeRep r -> Term (bv l) -> Term (bv r)
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 (Term (bv l) -> Term (bv l)
forall x. SupportedPrim x => Term x -> Term x
gov Term (bv l)
op)
        TabularFunApplyTerm Id
_ Term (a =-> a)
f Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term (a =-> a) -> Term a -> Term a
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> Term a -> Term b
pevalTabularFunApplyTerm (Term (a =-> a) -> Term (a =-> a)
forall x. SupportedPrim x => Term x -> Term x
gov Term (a =-> a)
f) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        GeneralFunApplyTerm Id
_ Term (a --> a)
f Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term (a --> a) -> Term a -> Term a
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm (Term (a --> a) -> Term (a --> a)
forall x. SupportedPrim x => Term x -> Term x
gov Term (a --> a)
f) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
        DivIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalDivIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        ModIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalModIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        QuotIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalQuotIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        RemIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalRemIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        DivBoundedIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalDivBoundedIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        ModBoundedIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalModBoundedIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        QuotBoundedIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalQuotBoundedIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
        RemBoundedIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalRemBoundedIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)