{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
-- 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.InternedCtors
  ( constructUnary,
    constructBinary,
    constructTernary,
    conTerm,
    symTerm,
    ssymTerm,
    isymTerm,
    sinfosymTerm,
    iinfosymTerm,
    notTerm,
    orTerm,
    andTerm,
    eqvTerm,
    iteTerm,
    addNumTerm,
    uminusNumTerm,
    timesNumTerm,
    absNumTerm,
    signumNumTerm,
    ltNumTerm,
    leNumTerm,
    andBitsTerm,
    orBitsTerm,
    xorBitsTerm,
    complementBitsTerm,
    shiftBitsTerm,
    rotateBitsTerm,
    bvconcatTerm,
    bvselectTerm,
    bvextendTerm,
    bvsignExtendTerm,
    bvzeroExtendTerm,
    tabularFunApplyTerm,
    generalFunApplyTerm,
    divIntegralTerm,
    modIntegralTerm,
    quotIntegralTerm,
    remIntegralTerm,
    divBoundedIntegralTerm,
    modBoundedIntegralTerm,
    quotBoundedIntegralTerm,
    remBoundedIntegralTerm,
  )
where

import Control.DeepSeq
import Data.Array
import Data.Bits
import qualified Data.HashMap.Strict as M
import Data.Hashable
import Data.IORef (atomicModifyIORef')
import Data.Interned
import Data.Interned.Internal
import GHC.IO (unsafeDupablePerformIO)
import GHC.TypeNats
import Grisette.Core.Data.Class.BitVector
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.TabularFun
import Language.Haskell.TH.Syntax
import Type.Reflection

internTerm :: forall t. (SupportedPrim t) => Uninterned (Term t) -> Term t
internTerm :: forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm !Uninterned (Term t)
bt = forall a. IO a -> a
unsafeDupablePerformIO forall a b. (a -> b) -> a -> b
$ forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef (CacheState (Term t))
slot CacheState (Term t) -> (CacheState (Term t), Term t)
go
  where
    slot :: IORef (CacheState (Term t))
slot = forall t. Cache t -> Array Int (IORef (CacheState t))
getCache forall t. Interned t => Cache t
cache forall i e. Ix i => Array i e -> i -> e
! Int
r
    !dt :: Description (Term t)
dt = forall t. Interned t => Uninterned t -> Description t
describe Uninterned (Term t)
bt
    !hdt :: Int
hdt = forall a. Hashable a => a -> Int
hash Description (Term t)
dt
    !wid :: Int
wid = forall t (p :: * -> *). Interned t => p t -> Int
cacheWidth Description (Term t)
dt
    r :: Int
r = Int
hdt forall a. Integral a => a -> a -> a
`mod` Int
wid
    go :: CacheState (Term t) -> (CacheState (Term t), Term t)
go (CacheState Int
i HashMap (Description (Term t)) (Term t)
m) = case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Description (Term t)
dt HashMap (Description (Term t)) (Term t)
m of
      Maybe (Term t)
Nothing -> let t :: Term t
t = forall t. Interned t => Int -> Uninterned t -> t
identify (Int
wid forall a. Num a => a -> a -> a
* Int
i forall a. Num a => a -> a -> a
+ Int
r) Uninterned (Term t)
bt in (forall t. Int -> HashMap (Description t) t -> CacheState t
CacheState (Int
i forall a. Num a => a -> a -> a
+ Int
1) (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Description (Term t)
dt Term t
t HashMap (Description (Term t)) (Term t)
m), Term t
t)
      Just Term t
t -> (forall t. Int -> HashMap (Description t) t -> CacheState t
CacheState Int
i HashMap (Description (Term t)) (Term t)
m, Term t
t)

constructUnary ::
  forall tag arg t.
  (SupportedPrim t, UnaryOp tag arg t, Typeable tag, Typeable t, Show tag) =>
  tag ->
  Term arg ->
  Term t
constructUnary :: forall tag arg t.
(SupportedPrim t, UnaryOp tag arg t, Typeable tag, Typeable t,
 Show tag) =>
tag -> Term arg -> Term t
constructUnary tag
tag Term arg
tm = let x :: Term t
x = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall tag arg t. UnaryOp tag arg t => tag -> Term arg -> UTerm t
UUnaryTerm tag
tag Term arg
tm in Term t
x
{-# INLINE constructUnary #-}

constructBinary ::
  forall tag arg1 arg2 t.
  (SupportedPrim t, BinaryOp tag arg1 arg2 t, Typeable tag, Typeable t, Show tag) =>
  tag ->
  Term arg1 ->
  Term arg2 ->
  Term t
constructBinary :: forall tag arg1 arg2 t.
(SupportedPrim t, BinaryOp tag arg1 arg2 t, Typeable tag,
 Typeable t, Show tag) =>
tag -> Term arg1 -> Term arg2 -> Term t
constructBinary tag
tag Term arg1
tm1 Term arg2
tm2 = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall tag arg1 arg2 t.
BinaryOp tag arg1 arg2 t =>
tag -> Term arg1 -> Term arg2 -> UTerm t
UBinaryTerm tag
tag Term arg1
tm1 Term arg2
tm2
{-# INLINE constructBinary #-}

constructTernary ::
  forall tag arg1 arg2 arg3 t.
  (SupportedPrim t, TernaryOp tag arg1 arg2 arg3 t, Typeable tag, Typeable t, Show tag) =>
  tag ->
  Term arg1 ->
  Term arg2 ->
  Term arg3 ->
  Term t
constructTernary :: forall tag arg1 arg2 arg3 t.
(SupportedPrim t, TernaryOp tag arg1 arg2 arg3 t, Typeable tag,
 Typeable t, Show tag) =>
tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
constructTernary tag
tag Term arg1
tm1 Term arg2
tm2 Term arg3
tm3 = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall tag arg1 arg2 arg3 t.
TernaryOp tag arg1 arg2 arg3 t =>
tag -> Term arg1 -> Term arg2 -> Term arg3 -> UTerm t
UTernaryTerm tag
tag Term arg1
tm1 Term arg2
tm2 Term arg3
tm3
{-# INLINE constructTernary #-}

conTerm :: (SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) => t -> Term t
conTerm :: forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm t
t = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t. SupportedPrim t => t -> UTerm t
UConTerm t
t
{-# INLINE conTerm #-}

symTerm :: forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm :: forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm TypedSymbol t
t = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t. SupportedPrim t => TypedSymbol t -> UTerm t
USymTerm TypedSymbol t
t
{-# INLINE symTerm #-}

ssymTerm :: (SupportedPrim t, Typeable t) => String -> Term t
ssymTerm :: forall t. (SupportedPrim t, Typeable t) => String -> Term t
ssymTerm = forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. SupportedPrim t => String -> TypedSymbol t
SimpleSymbol
{-# INLINE ssymTerm #-}

isymTerm :: (SupportedPrim t, Typeable t) => String -> Int -> Term t
isymTerm :: forall t. (SupportedPrim t, Typeable t) => String -> Int -> Term t
isymTerm String
str Int
idx = forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm forall a b. (a -> b) -> a -> b
$ forall t. SupportedPrim t => String -> Int -> TypedSymbol t
IndexedSymbol String
str Int
idx
{-# INLINE isymTerm #-}

sinfosymTerm ::
  (SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
  String ->
  a ->
  Term t
sinfosymTerm :: forall t a.
(SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a,
 Show a, Hashable a) =>
String -> a -> Term t
sinfosymTerm String
s a
info = forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm forall a b. (a -> b) -> a -> b
$ forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
 Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo (forall t. SupportedPrim t => String -> TypedSymbol t
SimpleSymbol String
s) a
info
{-# INLINE sinfosymTerm #-}

iinfosymTerm ::
  (SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
  String ->
  Int ->
  a ->
  Term t
iinfosymTerm :: forall t a.
(SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a,
 Show a, Hashable a) =>
String -> Int -> a -> Term t
iinfosymTerm String
str Int
idx a
info = forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm forall a b. (a -> b) -> a -> b
$ forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
 Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo (forall t. SupportedPrim t => String -> Int -> TypedSymbol t
IndexedSymbol String
str Int
idx) a
info
{-# INLINE iinfosymTerm #-}

notTerm :: Term Bool -> Term Bool
notTerm :: Term Bool -> Term Bool
notTerm = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term Bool -> UTerm Bool
UNotTerm
{-# INLINE notTerm #-}

orTerm :: Term Bool -> Term Bool -> Term Bool
orTerm :: Term Bool -> Term Bool -> Term Bool
orTerm Term Bool
l Term Bool
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> UTerm Bool
UOrTerm Term Bool
l Term Bool
r
{-# INLINE orTerm #-}

andTerm :: Term Bool -> Term Bool -> Term Bool
andTerm :: Term Bool -> Term Bool -> Term Bool
andTerm Term Bool
l Term Bool
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> UTerm Bool
UAndTerm Term Bool
l Term Bool
r
{-# INLINE andTerm #-}

eqvTerm :: SupportedPrim a => Term a -> Term a -> Term Bool
eqvTerm :: forall a. SupportedPrim a => Term a -> Term a -> Term Bool
eqvTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t1. SupportedPrim t1 => Term t1 -> Term t1 -> UTerm Bool
UEqvTerm Term a
l Term a
r
{-# INLINE eqvTerm #-}

iteTerm :: SupportedPrim a => Term Bool -> Term a -> Term a -> Term a
iteTerm :: forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
iteTerm Term Bool
c Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> UTerm t
UITETerm Term Bool
c Term a
l Term a
r
{-# INLINE iteTerm #-}

addNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a -> Term a
addNumTerm :: forall a. (SupportedPrim a, Num a) => Term a -> Term a -> Term a
addNumTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t. (SupportedPrim t, Num t) => Term t -> Term t -> UTerm t
UAddNumTerm Term a
l Term a
r
{-# INLINE addNumTerm #-}

uminusNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a
uminusNumTerm :: forall a. (SupportedPrim a, Num a) => Term a -> Term a
uminusNumTerm = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. (SupportedPrim t, Num t) => Term t -> UTerm t
UUMinusNumTerm
{-# INLINE uminusNumTerm #-}

timesNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a -> Term a
timesNumTerm :: forall a. (SupportedPrim a, Num a) => Term a -> Term a -> Term a
timesNumTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t. (SupportedPrim t, Num t) => Term t -> Term t -> UTerm t
UTimesNumTerm Term a
l Term a
r
{-# INLINE timesNumTerm #-}

absNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a
absNumTerm :: forall a. (SupportedPrim a, Num a) => Term a -> Term a
absNumTerm = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. (SupportedPrim t, Num t) => Term t -> UTerm t
UAbsNumTerm
{-# INLINE absNumTerm #-}

signumNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a
signumNumTerm :: forall a. (SupportedPrim a, Num a) => Term a -> Term a
signumNumTerm = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. (SupportedPrim t, Num t) => Term t -> UTerm t
USignumNumTerm
{-# INLINE signumNumTerm #-}

ltNumTerm :: (SupportedPrim a, Num a, Ord a) => Term a -> Term a -> Term Bool
ltNumTerm :: forall a.
(SupportedPrim a, Num a, Ord a) =>
Term a -> Term a -> Term Bool
ltNumTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t1.
(SupportedPrim t1, Num t1, Ord t1) =>
Term t1 -> Term t1 -> UTerm Bool
ULTNumTerm Term a
l Term a
r
{-# INLINE ltNumTerm #-}

leNumTerm :: (SupportedPrim a, Num a, Ord a) => Term a -> Term a -> Term Bool
leNumTerm :: forall a.
(SupportedPrim a, Num a, Ord a) =>
Term a -> Term a -> Term Bool
leNumTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t1.
(SupportedPrim t1, Num t1, Ord t1) =>
Term t1 -> Term t1 -> UTerm Bool
ULENumTerm Term a
l Term a
r
{-# INLINE leNumTerm #-}

andBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
andBitsTerm :: forall a. (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
andBitsTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t. (SupportedPrim t, Bits t) => Term t -> Term t -> UTerm t
UAndBitsTerm Term a
l Term a
r
{-# INLINE andBitsTerm #-}

orBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
orBitsTerm :: forall a. (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
orBitsTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t. (SupportedPrim t, Bits t) => Term t -> Term t -> UTerm t
UOrBitsTerm Term a
l Term a
r
{-# INLINE orBitsTerm #-}

xorBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
xorBitsTerm :: forall a. (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
xorBitsTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t. (SupportedPrim t, Bits t) => Term t -> Term t -> UTerm t
UXorBitsTerm Term a
l Term a
r
{-# INLINE xorBitsTerm #-}

complementBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a
complementBitsTerm :: forall a. (SupportedPrim a, Bits a) => Term a -> Term a
complementBitsTerm = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. (SupportedPrim t, Bits t) => Term t -> UTerm t
UComplementBitsTerm
{-# INLINE complementBitsTerm #-}

shiftBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Int -> Term a
shiftBitsTerm :: forall a. (SupportedPrim a, Bits a) => Term a -> Int -> Term a
shiftBitsTerm Term a
t Int
n = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t. (SupportedPrim t, Bits t) => Term t -> Int -> UTerm t
UShiftBitsTerm Term a
t Int
n
{-# INLINE shiftBitsTerm #-}

rotateBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Int -> Term a
rotateBitsTerm :: forall a. (SupportedPrim a, Bits a) => Term a -> Int -> Term a
rotateBitsTerm Term a
t Int
n = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t. (SupportedPrim t, Bits t) => Term t -> Int -> UTerm t
URotateBitsTerm Term a
t Int
n
{-# INLINE rotateBitsTerm #-}

bvconcatTerm ::
  ( SupportedPrim (bv a),
    SupportedPrim (bv b),
    SupportedPrim (bv (a + b)),
    KnownNat a,
    KnownNat b,
    1 <= a,
    1 <= b,
    SizedBV bv
  ) =>
  Term (bv a) ->
  Term (bv b) ->
  Term (bv (a + b))
bvconcatTerm :: forall (bv :: Natural -> *) (a :: Natural) (b :: Natural).
(SupportedPrim (bv a), SupportedPrim (bv b),
 SupportedPrim (bv (a + b)), KnownNat a, KnownNat b, 1 <= a, 1 <= b,
 SizedBV bv) =>
Term (bv a) -> Term (bv b) -> Term (bv (a + b))
bvconcatTerm Term (bv a)
l Term (bv b)
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (a :: Natural) (b :: Natural).
(SupportedPrim (bv a), SupportedPrim (bv b),
 SupportedPrim (bv (a + b)), KnownNat a, KnownNat b, 1 <= a, 1 <= b,
 SizedBV bv) =>
Term (bv a) -> Term (bv b) -> UTerm (bv (a + b))
UBVConcatTerm Term (bv a)
l Term (bv b)
r
{-# INLINE bvconcatTerm #-}

bvselectTerm ::
  forall bv n ix w proxy.
  ( SupportedPrim (bv n),
    SupportedPrim (bv w),
    KnownNat n,
    KnownNat ix,
    KnownNat w,
    1 <= n,
    1 <= w,
    ix + w <= n,
    SizedBV bv
  ) =>
  proxy ix ->
  proxy w ->
  Term (bv n) ->
  Term (bv w)
bvselectTerm :: forall (bv :: Natural -> *) (n :: Natural) (ix :: Natural)
       (w :: Natural) (proxy :: Natural -> *).
(SupportedPrim (bv n), SupportedPrim (bv w), KnownNat n,
 KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n,
 SizedBV bv) =>
proxy ix -> proxy w -> Term (bv n) -> Term (bv w)
bvselectTerm proxy ix
_ proxy w
_ Term (bv n)
v = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (n :: Natural) (w :: Natural)
       (ix :: Natural).
(SupportedPrim (bv n), SupportedPrim (bv w), KnownNat n,
 KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n,
 SizedBV bv) =>
TypeRep ix -> TypeRep w -> Term (bv n) -> UTerm (bv w)
UBVSelectTerm (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @ix) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @w) Term (bv n)
v
{-# INLINE bvselectTerm #-}

bvextendTerm ::
  forall bv l r proxy.
  ( SupportedPrim (bv l),
    SupportedPrim (bv r),
    KnownNat l,
    KnownNat r,
    1 <= l,
    l <= r,
    SizedBV bv
  ) =>
  Bool ->
  proxy r ->
  Term (bv l) ->
  Term (bv r)
bvextendTerm :: forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(SupportedPrim (bv l), SupportedPrim (bv r), KnownNat l,
 KnownNat r, 1 <= l, l <= r, SizedBV bv) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
bvextendTerm Bool
signed proxy r
_ Term (bv l)
v = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(SupportedPrim (bv l), SupportedPrim (bv r), KnownNat l,
 KnownNat r, 1 <= l, l <= r, SizedBV bv) =>
Bool -> TypeRep r -> Term (bv l) -> UTerm (bv r)
UBVExtendTerm Bool
signed (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @r) Term (bv l)
v
{-# INLINE bvextendTerm #-}

bvsignExtendTerm ::
  forall bv l r proxy.
  ( SupportedPrim (bv l),
    SupportedPrim (bv r),
    KnownNat l,
    KnownNat r,
    1 <= l,
    l <= r,
    SizedBV bv
  ) =>
  proxy r ->
  Term (bv l) ->
  Term (bv r)
bvsignExtendTerm :: forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(SupportedPrim (bv l), SupportedPrim (bv r), KnownNat l,
 KnownNat r, 1 <= l, l <= r, SizedBV bv) =>
proxy r -> Term (bv l) -> Term (bv r)
bvsignExtendTerm proxy r
_ Term (bv l)
v = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(SupportedPrim (bv l), SupportedPrim (bv r), KnownNat l,
 KnownNat r, 1 <= l, l <= r, SizedBV bv) =>
Bool -> TypeRep r -> Term (bv l) -> UTerm (bv r)
UBVExtendTerm Bool
True (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @r) Term (bv l)
v
{-# INLINE bvsignExtendTerm #-}

bvzeroExtendTerm ::
  forall bv l r proxy.
  ( SupportedPrim (bv l),
    SupportedPrim (bv r),
    KnownNat l,
    KnownNat r,
    1 <= l,
    l <= r,
    SizedBV bv
  ) =>
  proxy r ->
  Term (bv l) ->
  Term (bv r)
bvzeroExtendTerm :: forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(SupportedPrim (bv l), SupportedPrim (bv r), KnownNat l,
 KnownNat r, 1 <= l, l <= r, SizedBV bv) =>
proxy r -> Term (bv l) -> Term (bv r)
bvzeroExtendTerm proxy r
_ Term (bv l)
v = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(SupportedPrim (bv l), SupportedPrim (bv r), KnownNat l,
 KnownNat r, 1 <= l, l <= r, SizedBV bv) =>
Bool -> TypeRep r -> Term (bv l) -> UTerm (bv r)
UBVExtendTerm Bool
False (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @r) Term (bv l)
v
{-# INLINE bvzeroExtendTerm #-}

tabularFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a =-> b) -> Term a -> Term b
tabularFunApplyTerm :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> Term a -> Term b
tabularFunApplyTerm Term (a =-> b)
f Term a
a = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall a t.
(SupportedPrim a, SupportedPrim t) =>
Term (a =-> t) -> Term a -> UTerm t
UTabularFunApplyTerm Term (a =-> b)
f Term a
a
{-# INLINE tabularFunApplyTerm #-}

generalFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a --> b) -> Term a -> Term b
generalFunApplyTerm :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
generalFunApplyTerm Term (a --> b)
f Term a
a = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall a t.
(SupportedPrim a, SupportedPrim t) =>
Term (a --> t) -> Term a -> UTerm t
UGeneralFunApplyTerm Term (a --> b)
f Term a
a
{-# INLINE generalFunApplyTerm #-}

divIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
divIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
divIntegralTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Integral t) =>
Term t -> Term t -> UTerm t
UDivIntegralTerm Term a
l Term a
r
{-# INLINE divIntegralTerm #-}

modIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
modIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
modIntegralTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Integral t) =>
Term t -> Term t -> UTerm t
UModIntegralTerm Term a
l Term a
r
{-# INLINE modIntegralTerm #-}

quotIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
quotIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
quotIntegralTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Integral t) =>
Term t -> Term t -> UTerm t
UQuotIntegralTerm Term a
l Term a
r
{-# INLINE quotIntegralTerm #-}

remIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
remIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
remIntegralTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Integral t) =>
Term t -> Term t -> UTerm t
URemIntegralTerm Term a
l Term a
r
{-# INLINE remIntegralTerm #-}

divBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Term a
divBoundedIntegralTerm :: forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
divBoundedIntegralTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Term t -> Term t -> UTerm t
UDivBoundedIntegralTerm Term a
l Term a
r
{-# INLINE divBoundedIntegralTerm #-}

modBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Term a
modBoundedIntegralTerm :: forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
modBoundedIntegralTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Term t -> Term t -> UTerm t
UModBoundedIntegralTerm Term a
l Term a
r
{-# INLINE modBoundedIntegralTerm #-}

quotBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Term a
quotBoundedIntegralTerm :: forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
quotBoundedIntegralTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Term t -> Term t -> UTerm t
UQuotBoundedIntegralTerm Term a
l Term a
r
{-# INLINE quotBoundedIntegralTerm #-}

remBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Term a
remBoundedIntegralTerm :: forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
remBoundedIntegralTerm Term a
l Term a
r = forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Term t -> Term t -> UTerm t
URemBoundedIntegralTerm Term a
l Term a
r
{-# INLINE remBoundedIntegralTerm #-}