{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm
-- 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.PEvalFromIntegralTerm () where

import Data.Proxy (Proxy (Proxy))
import qualified Data.SBV as SBV
import qualified Data.SBV.Internals as SBVI
import GHC.TypeLits (KnownNat, type (<=))
import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP (FP, ValidFP)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim
  ( bvIsNonZeroFromGEq1,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalFromIntegralTerm (pevalFromIntegralTerm, sbvFromIntegralTerm),
    SupportedNonFuncPrim (withNonFuncPrim),
    SupportedPrim,
    Term,
    conTerm,
    fromIntegralTerm,
    pattern ConTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold (unaryUnfoldOnce)

pevalFromIntegralTermGeneric ::
  (PEvalFromIntegralTerm a b, SupportedPrim b) => Term a -> Term b
pevalFromIntegralTermGeneric :: forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
pevalFromIntegralTermGeneric =
  PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary a b
forall {t} {t}.
(SupportedPrim t, Integral t, Num t) =>
Term t -> Maybe (Term t)
doPEvalFromIntegralTerm TotalRuleUnary a b
forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
fromIntegralTerm
  where
    doPEvalFromIntegralTerm :: Term t -> Maybe (Term t)
doPEvalFromIntegralTerm (ConTerm t
a) = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just (Term t -> Maybe (Term t)) -> Term t -> Maybe (Term t)
forall a b. (a -> b) -> a -> b
$ t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm (t -> Term t) -> t -> Term t
forall a b. (a -> b) -> a -> b
$ t -> t
forall a b. (Integral a, Num b) => a -> b
fromIntegral t
a
    doPEvalFromIntegralTerm Term t
_ = Maybe (Term t)
forall a. Maybe a
Nothing

instance PEvalFromIntegralTerm Integer Integer where
  pevalFromIntegralTerm :: Term Integer -> Term Integer
pevalFromIntegralTerm = Term Integer -> Term Integer
forall a. a -> a
id
  sbvFromIntegralTerm :: SBVType Integer -> SBVType Integer
sbvFromIntegralTerm = SBV Integer -> SBV Integer
SBVType Integer -> SBVType Integer
forall a. a -> a
id

instance PEvalFromIntegralTerm Integer AlgReal where
  pevalFromIntegralTerm :: Term Integer -> Term AlgReal
pevalFromIntegralTerm = Term Integer -> Term AlgReal
forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
pevalFromIntegralTermGeneric
  sbvFromIntegralTerm :: SBVType Integer -> SBVType AlgReal
sbvFromIntegralTerm SBVType Integer
l = forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @Integer ((NonFuncPrimConstraint Integer => SBVType AlgReal)
 -> SBVType AlgReal)
-> (NonFuncPrimConstraint Integer => SBVType AlgReal)
-> SBVType AlgReal
forall a b. (a -> b) -> a -> b
$ SBV Integer -> SBV AlgReal
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV Integer
SBVType Integer
l

instance (KnownNat n, 1 <= n) => PEvalFromIntegralTerm Integer (WordN n) where
  pevalFromIntegralTerm :: Term Integer -> Term (WordN n)
pevalFromIntegralTerm = Term Integer -> Term (WordN n)
forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
pevalFromIntegralTermGeneric
  sbvFromIntegralTerm :: SBVType Integer -> SBVType (WordN n)
sbvFromIntegralTerm SBVType Integer
l =
    Proxy n
-> (BVIsNonZero n => SBVType (WordN n)) -> SBVType (WordN n)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => SBVType (WordN n)) -> SBVType (WordN n))
-> (BVIsNonZero n => SBVType (WordN n)) -> SBVType (WordN n)
forall a b. (a -> b) -> a -> b
$
      forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @Integer ((NonFuncPrimConstraint Integer => SBVType (WordN n))
 -> SBVType (WordN n))
-> (NonFuncPrimConstraint Integer => SBVType (WordN n))
-> SBVType (WordN n)
forall a b. (a -> b) -> a -> b
$
        SBV Integer -> SBV (WordN n)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV Integer
SBVType Integer
l

instance (KnownNat n, 1 <= n) => PEvalFromIntegralTerm Integer (IntN n) where
  pevalFromIntegralTerm :: Term Integer -> Term (IntN n)
pevalFromIntegralTerm = Term Integer -> Term (IntN n)
forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
pevalFromIntegralTermGeneric
  sbvFromIntegralTerm :: SBVType Integer -> SBVType (IntN n)
sbvFromIntegralTerm SBVType Integer
l =
    Proxy n -> (BVIsNonZero n => SBVType (IntN n)) -> SBVType (IntN n)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => SBVType (IntN n)) -> SBVType (IntN n))
-> (BVIsNonZero n => SBVType (IntN n)) -> SBVType (IntN n)
forall a b. (a -> b) -> a -> b
$
      forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @Integer ((NonFuncPrimConstraint Integer => SBVType (IntN n))
 -> SBVType (IntN n))
-> (NonFuncPrimConstraint Integer => SBVType (IntN n))
-> SBVType (IntN n)
forall a b. (a -> b) -> a -> b
$
        SBV Integer -> SBV (IntN n)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV Integer
SBVType Integer
l

genericFPCast ::
  forall a r.
  (SBV.HasKind a, SBV.HasKind r) =>
  SBV.SRoundingMode ->
  SBV.SBV a ->
  SBV.SBV r
genericFPCast :: forall a r.
(HasKind a, HasKind r) =>
SRoundingMode -> SBV a -> SBV r
genericFPCast SRoundingMode
rm SBV a
f = SVal -> SBV r
forall a. SVal -> SBV a
SBVI.SBV (Kind -> Either CV (Cached SV) -> SVal
SBVI.SVal Kind
kTo (Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right ((State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
SBVI.cache State -> IO SV
r)))
  where
    kFrom :: Kind
kFrom = SBV a -> Kind
forall a. HasKind a => a -> Kind
SBVI.kindOf SBV a
f
    kTo :: Kind
kTo = Proxy r -> Kind
forall a. HasKind a => a -> Kind
SBVI.kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @r)
    r :: State -> IO SV
r State
st = do
      msv <- State -> SRoundingMode -> IO SV
forall a. State -> SBV a -> IO SV
SBVI.sbvToSV State
st SRoundingMode
rm
      xsv <- SBVI.sbvToSV st f
      SBVI.newExpr st kTo $
        SBVI.SBVApp
          (SBVI.IEEEFP (SBVI.FP_Cast kFrom kTo msv))
          [xsv]

instance (ValidFP eb sb) => PEvalFromIntegralTerm Integer (FP eb sb) where
  pevalFromIntegralTerm :: Term Integer -> Term (FP eb sb)
pevalFromIntegralTerm = Term Integer -> Term (FP eb sb)
forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
pevalFromIntegralTermGeneric
  sbvFromIntegralTerm :: SBVType Integer -> SBVType (FP eb sb)
sbvFromIntegralTerm SBVType Integer
l =
    forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @Integer ((NonFuncPrimConstraint Integer => SBVType (FP eb sb))
 -> SBVType (FP eb sb))
-> (NonFuncPrimConstraint Integer => SBVType (FP eb sb))
-> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$
      SRoundingMode -> SBV Integer -> SFloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
SRoundingMode -> SBV Integer -> SFloatingPoint eb sb
forall a (eb :: Nat) (sb :: Nat).
(IEEEFloatConvertible a, ValidFloat eb sb) =>
SRoundingMode -> SBV a -> SFloatingPoint eb sb
SBV.toSFloatingPoint SRoundingMode
SBV.sRoundNearestTiesToEven SBV Integer
SBVType Integer
l

instance (KnownNat n, 1 <= n) => PEvalFromIntegralTerm (WordN n) Integer where
  pevalFromIntegralTerm :: Term (WordN n) -> Term Integer
pevalFromIntegralTerm = Term (WordN n) -> Term Integer
forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
pevalFromIntegralTermGeneric
  sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType Integer
sbvFromIntegralTerm SBVType (WordN n)
l =
    Proxy n -> (BVIsNonZero n => SBVType Integer) -> SBVType Integer
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => SBVType Integer) -> SBVType Integer)
-> (BVIsNonZero n => SBVType Integer) -> SBVType Integer
forall a b. (a -> b) -> a -> b
$
      forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @Integer ((NonFuncPrimConstraint Integer => SBVType Integer)
 -> SBVType Integer)
-> (NonFuncPrimConstraint Integer => SBVType Integer)
-> SBVType Integer
forall a b. (a -> b) -> a -> b
$
        SBV (WordN n) -> SBV Integer
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV (WordN n)
SBVType (WordN n)
l

instance
  (KnownNat n, 1 <= n, KnownNat m, 1 <= m) =>
  PEvalFromIntegralTerm (WordN n) (WordN m)
  where
  pevalFromIntegralTerm :: Term (WordN n) -> Term (WordN m)
pevalFromIntegralTerm = Term (WordN n) -> Term (WordN m)
forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
pevalFromIntegralTermGeneric
  sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType (WordN m)
sbvFromIntegralTerm SBVType (WordN n)
l =
    Proxy n
-> (BVIsNonZero n => SBVType (WordN m)) -> SBVType (WordN m)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => SBVType (WordN m)) -> SBVType (WordN m))
-> (BVIsNonZero n => SBVType (WordN m)) -> SBVType (WordN m)
forall a b. (a -> b) -> a -> b
$
      Proxy m
-> (BVIsNonZero m => SBVType (WordN m)) -> SBVType (WordN m)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m) ((BVIsNonZero m => SBVType (WordN m)) -> SBVType (WordN m))
-> (BVIsNonZero m => SBVType (WordN m)) -> SBVType (WordN m)
forall a b. (a -> b) -> a -> b
$
        forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @Integer ((NonFuncPrimConstraint Integer => SBVType (WordN m))
 -> SBVType (WordN m))
-> (NonFuncPrimConstraint Integer => SBVType (WordN m))
-> SBVType (WordN m)
forall a b. (a -> b) -> a -> b
$
          SBV (WordN n) -> SBV (WordN m)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV (WordN n)
SBVType (WordN n)
l

instance
  (KnownNat n, 1 <= n, KnownNat m, 1 <= m) =>
  PEvalFromIntegralTerm (WordN n) (IntN m)
  where
  pevalFromIntegralTerm :: Term (WordN n) -> Term (IntN m)
pevalFromIntegralTerm = Term (WordN n) -> Term (IntN m)
forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
pevalFromIntegralTermGeneric
  sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType (IntN m)
sbvFromIntegralTerm SBVType (WordN n)
l =
    Proxy n -> (BVIsNonZero n => SBVType (IntN m)) -> SBVType (IntN m)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => SBVType (IntN m)) -> SBVType (IntN m))
-> (BVIsNonZero n => SBVType (IntN m)) -> SBVType (IntN m)
forall a b. (a -> b) -> a -> b
$
      Proxy m -> (BVIsNonZero m => SBVType (IntN m)) -> SBVType (IntN m)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m) ((BVIsNonZero m => SBVType (IntN m)) -> SBVType (IntN m))
-> (BVIsNonZero m => SBVType (IntN m)) -> SBVType (IntN m)
forall a b. (a -> b) -> a -> b
$
        forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @Integer ((NonFuncPrimConstraint Integer => SBVType (IntN m))
 -> SBVType (IntN m))
-> (NonFuncPrimConstraint Integer => SBVType (IntN m))
-> SBVType (IntN m)
forall a b. (a -> b) -> a -> b
$
          SBV (WordN n) -> SBV (IntN m)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV (WordN n)
SBVType (WordN n)
l

instance (KnownNat n, 1 <= n) => PEvalFromIntegralTerm (WordN n) AlgReal where
  pevalFromIntegralTerm :: Term (WordN n) -> Term AlgReal
pevalFromIntegralTerm = Term (WordN n) -> Term AlgReal
forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
pevalFromIntegralTermGeneric
  sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType AlgReal
sbvFromIntegralTerm SBVType (WordN n)
l =
    Proxy n -> (BVIsNonZero n => SBV AlgReal) -> SBV AlgReal
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1
      (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
      (SBV Integer -> SBV AlgReal
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral (SBV (WordN n) -> SBV Integer
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV (WordN n)
SBVType (WordN n)
l :: SBV.SInteger))

instance
  (KnownNat n, 1 <= n, ValidFP eb sb) =>
  PEvalFromIntegralTerm (WordN n) (FP eb sb)
  where
  pevalFromIntegralTerm :: Term (WordN n) -> Term (FP eb sb)
pevalFromIntegralTerm = Term (WordN n) -> Term (FP eb sb)
forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
pevalFromIntegralTermGeneric
  sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType (FP eb sb)
sbvFromIntegralTerm SBVType (WordN n)
l =
    Proxy n
-> (BVIsNonZero n => SBVType (FP eb sb)) -> SBVType (FP eb sb)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => SBVType (FP eb sb)) -> SBVType (FP eb sb))
-> (BVIsNonZero n => SBVType (FP eb sb)) -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$
      SRoundingMode -> SBV (WordN n) -> SBV (FloatingPoint eb sb)
forall a r.
(HasKind a, HasKind r) =>
SRoundingMode -> SBV a -> SBV r
genericFPCast SRoundingMode
SBV.sRoundNearestTiesToEven SBV (WordN n)
SBVType (WordN n)
l

instance (KnownNat n, 1 <= n) => PEvalFromIntegralTerm (IntN n) Integer where
  pevalFromIntegralTerm :: Term (IntN n) -> Term Integer
pevalFromIntegralTerm = Term (IntN n) -> Term Integer
forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
pevalFromIntegralTermGeneric
  sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType Integer
sbvFromIntegralTerm SBVType (IntN n)
l =
    Proxy n -> (BVIsNonZero n => SBVType Integer) -> SBVType Integer
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => SBVType Integer) -> SBVType Integer)
-> (BVIsNonZero n => SBVType Integer) -> SBVType Integer
forall a b. (a -> b) -> a -> b
$
      forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @Integer ((NonFuncPrimConstraint Integer => SBVType Integer)
 -> SBVType Integer)
-> (NonFuncPrimConstraint Integer => SBVType Integer)
-> SBVType Integer
forall a b. (a -> b) -> a -> b
$
        SBV (IntN n) -> SBV Integer
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV (IntN n)
SBVType (IntN n)
l

instance
  (KnownNat n, 1 <= n, KnownNat m, 1 <= m) =>
  PEvalFromIntegralTerm (IntN n) (WordN m)
  where
  pevalFromIntegralTerm :: Term (IntN n) -> Term (WordN m)
pevalFromIntegralTerm = Term (IntN n) -> Term (WordN m)
forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
pevalFromIntegralTermGeneric
  sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType (WordN m)
sbvFromIntegralTerm SBVType (IntN n)
l =
    Proxy n
-> (BVIsNonZero n => SBVType (WordN m)) -> SBVType (WordN m)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => SBVType (WordN m)) -> SBVType (WordN m))
-> (BVIsNonZero n => SBVType (WordN m)) -> SBVType (WordN m)
forall a b. (a -> b) -> a -> b
$
      Proxy m
-> (BVIsNonZero m => SBVType (WordN m)) -> SBVType (WordN m)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m) ((BVIsNonZero m => SBVType (WordN m)) -> SBVType (WordN m))
-> (BVIsNonZero m => SBVType (WordN m)) -> SBVType (WordN m)
forall a b. (a -> b) -> a -> b
$
        forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @Integer ((NonFuncPrimConstraint Integer => SBVType (WordN m))
 -> SBVType (WordN m))
-> (NonFuncPrimConstraint Integer => SBVType (WordN m))
-> SBVType (WordN m)
forall a b. (a -> b) -> a -> b
$
          SBV (IntN n) -> SBV (WordN m)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV (IntN n)
SBVType (IntN n)
l

instance
  (KnownNat n, 1 <= n, KnownNat m, 1 <= m) =>
  PEvalFromIntegralTerm (IntN n) (IntN m)
  where
  pevalFromIntegralTerm :: Term (IntN n) -> Term (IntN m)
pevalFromIntegralTerm = Term (IntN n) -> Term (IntN m)
forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
pevalFromIntegralTermGeneric
  sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType (IntN m)
sbvFromIntegralTerm SBVType (IntN n)
l =
    Proxy n -> (BVIsNonZero n => SBVType (IntN m)) -> SBVType (IntN m)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => SBVType (IntN m)) -> SBVType (IntN m))
-> (BVIsNonZero n => SBVType (IntN m)) -> SBVType (IntN m)
forall a b. (a -> b) -> a -> b
$
      Proxy m -> (BVIsNonZero m => SBVType (IntN m)) -> SBVType (IntN m)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m) ((BVIsNonZero m => SBVType (IntN m)) -> SBVType (IntN m))
-> (BVIsNonZero m => SBVType (IntN m)) -> SBVType (IntN m)
forall a b. (a -> b) -> a -> b
$
        forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @Integer ((NonFuncPrimConstraint Integer => SBVType (IntN m))
 -> SBVType (IntN m))
-> (NonFuncPrimConstraint Integer => SBVType (IntN m))
-> SBVType (IntN m)
forall a b. (a -> b) -> a -> b
$
          SBV (IntN n) -> SBV (IntN m)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV (IntN n)
SBVType (IntN n)
l

instance (KnownNat n, 1 <= n) => PEvalFromIntegralTerm (IntN n) AlgReal where
  pevalFromIntegralTerm :: Term (IntN n) -> Term AlgReal
pevalFromIntegralTerm = Term (IntN n) -> Term AlgReal
forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
pevalFromIntegralTermGeneric
  sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType AlgReal
sbvFromIntegralTerm SBVType (IntN n)
l =
    Proxy n -> (BVIsNonZero n => SBV AlgReal) -> SBV AlgReal
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1
      (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
      (SBV Integer -> SBV AlgReal
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral (SBV (IntN n) -> SBV Integer
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV (IntN n)
SBVType (IntN n)
l :: SBV.SInteger))

instance
  (KnownNat n, 1 <= n, ValidFP eb sb) =>
  PEvalFromIntegralTerm (IntN n) (FP eb sb)
  where
  pevalFromIntegralTerm :: Term (IntN n) -> Term (FP eb sb)
pevalFromIntegralTerm = Term (IntN n) -> Term (FP eb sb)
forall a b.
(PEvalFromIntegralTerm a b, SupportedPrim b) =>
Term a -> Term b
pevalFromIntegralTermGeneric
  sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType (FP eb sb)
sbvFromIntegralTerm SBVType (IntN n)
l =
    Proxy n
-> (BVIsNonZero n => SBVType (FP eb sb)) -> SBVType (FP eb sb)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => SBVType (FP eb sb)) -> SBVType (FP eb sb))
-> (BVIsNonZero n => SBVType (FP eb sb)) -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$
      SRoundingMode -> SBV (IntN n) -> SBV (FloatingPoint eb sb)
forall a r.
(HasKind a, HasKind r) =>
SRoundingMode -> SBV a -> SBV r
genericFPCast SRoundingMode
SBV.sRoundNearestTiesToEven SBV (IntN n)
SBVType (IntN n)
l