Copyright	(c) Sirui Lu 2024
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	None
Language	Haskell2010

Grisette.Internal.Unified.Class.UnifiedFromIntegral

Description

Synopsis

class UnifiedFromIntegral (mode :: EvalModeTag) a b where
- withBaseFromIntegral :: (If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) => r) -> r
symFromIntegral :: forall (mode :: EvalModeTag) a b. (DecideEvalMode mode, UnifiedFromIntegral mode a b) => a -> b

Documentation

class UnifiedFromIntegral (mode :: EvalModeTag) a b where Source #

A class that provides unified conversion from integral types.

We use this type class to help resolve the constraints for SymFromIntegral.

Methods

withBaseFromIntegral :: (If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) => r) -> r Source #

Instances

Instances details

UnifiedFromIntegral 'C Integer AlgReal Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral Integer, Num AlgReal) (SymFromIntegral Integer AlgReal) => r) -> r Source #
UnifiedFromIntegral 'C Integer Integer Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral Integer, Num Integer) (SymFromIntegral Integer Integer) => r) -> r Source #
UnifiedFromIntegral 'S SymInteger SymAlgReal Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral SymInteger, Num SymAlgReal) (SymFromIntegral SymInteger SymAlgReal) => r) -> r Source #
UnifiedFromIntegral 'S SymInteger SymInteger Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral SymInteger, Num SymInteger) (SymFromIntegral SymInteger SymInteger) => r) -> r Source #
(DecideEvalMode mode, If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b)) => UnifiedFromIntegral mode a b Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedFromIntegral 'C Integer (IntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral Integer, Num (IntN n)) (SymFromIntegral Integer (IntN n)) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedFromIntegral 'C Integer (WordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral Integer, Num (WordN n)) (SymFromIntegral Integer (WordN n)) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedFromIntegral 'S SymInteger (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral SymInteger, Num (SymIntN n)) (SymFromIntegral SymInteger (SymIntN n)) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedFromIntegral 'S SymInteger (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral SymInteger, Num (SymWordN n)) (SymFromIntegral SymInteger (SymWordN n)) => r) -> r Source #
ValidFP eb sb => UnifiedFromIntegral 'C Integer (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral Integer, Num (FP eb sb)) (SymFromIntegral Integer (FP eb sb)) => r) -> r Source #
ValidFP eb sb => UnifiedFromIntegral 'S SymInteger (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral SymInteger, Num (SymFP eb sb)) (SymFromIntegral SymInteger (SymFP eb sb)) => r) -> r Source #
(KnownNat n', 1 <= n') => UnifiedFromIntegral 'C (IntN n') AlgReal Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral (IntN n'), Num AlgReal) (SymFromIntegral (IntN n') AlgReal) => r) -> r Source #
(KnownNat n', 1 <= n') => UnifiedFromIntegral 'C (IntN n') Integer Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral (IntN n'), Num Integer) (SymFromIntegral (IntN n') Integer) => r) -> r Source #
(KnownNat n', 1 <= n') => UnifiedFromIntegral 'C (WordN n') AlgReal Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral (WordN n'), Num AlgReal) (SymFromIntegral (WordN n') AlgReal) => r) -> r Source #
(KnownNat n', 1 <= n') => UnifiedFromIntegral 'C (WordN n') Integer Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral (WordN n'), Num Integer) (SymFromIntegral (WordN n') Integer) => r) -> r Source #
(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymIntN n') SymAlgReal Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num SymAlgReal) (SymFromIntegral (SymIntN n') SymAlgReal) => r) -> r Source #
(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymIntN n') SymInteger Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num SymInteger) (SymFromIntegral (SymIntN n') SymInteger) => r) -> r Source #
(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymWordN n') SymAlgReal Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num SymAlgReal) (SymFromIntegral (SymWordN n') SymAlgReal) => r) -> r Source #
(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymWordN n') SymInteger Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num SymInteger) (SymFromIntegral (SymWordN n') SymInteger) => r) -> r Source #
(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'C (IntN n') (IntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral (IntN n'), Num (IntN n)) (SymFromIntegral (IntN n') (IntN n)) => r) -> r Source #
(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'C (IntN n') (WordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral (IntN n'), Num (WordN n)) (SymFromIntegral (IntN n') (WordN n)) => r) -> r Source #
(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'C (WordN n') (IntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral (WordN n'), Num (IntN n)) (SymFromIntegral (WordN n') (IntN n)) => r) -> r Source #
(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'C (WordN n') (WordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral (WordN n'), Num (WordN n)) (SymFromIntegral (WordN n') (WordN n)) => r) -> r Source #
(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymIntN n') (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num (SymIntN n)) (SymFromIntegral (SymIntN n') (SymIntN n)) => r) -> r Source #
(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymIntN n') (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num (SymWordN n)) (SymFromIntegral (SymIntN n') (SymWordN n)) => r) -> r Source #
(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymWordN n') (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num (SymIntN n)) (SymFromIntegral (SymWordN n') (SymIntN n)) => r) -> r Source #
(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymWordN n') (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num (SymWordN n)) (SymFromIntegral (SymWordN n') (SymWordN n)) => r) -> r Source #
(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'C (IntN n') (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral (IntN n'), Num (FP eb sb)) (SymFromIntegral (IntN n') (FP eb sb)) => r) -> r Source #
(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'C (WordN n') (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral (WordN n'), Num (FP eb sb)) (SymFromIntegral (WordN n') (FP eb sb)) => r) -> r Source #
(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'S (SymIntN n') (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num (SymFP eb sb)) (SymFromIntegral (SymIntN n') (SymFP eb sb)) => r) -> r Source #
(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'S (SymWordN n') (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num (SymFP eb sb)) (SymFromIntegral (SymWordN n') (SymFP eb sb)) => r) -> r Source #

symFromIntegral :: forall (mode :: EvalModeTag) a b. (DecideEvalMode mode, UnifiedFromIntegral mode a b) => a -> b Source #

Unified symFromIntegral operation.

This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:

symFromIntegral @mode a