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	Safe-Inferred
Language	Haskell2010

Grisette.Unified.Internal.UnifiedFP

Description

Synopsis

type family GetFP mode = (f :: Nat -> Nat -> Type) | f -> mode
type family GetFPRoundingMode mode = r | r -> mode
class UnifiedFPImpl mode (GetFP mode) eb sb (GetFP mode eb sb) (GetFPRoundingMode mode) => UnifiedFP mode eb sb
class (SafeUnifiedFPImpl mode (GetFP mode) eb sb (GetFP mode eb sb) (GetFPRoundingMode mode) m, UnifiedSafeFromFP mode NotRepresentableFPError (GetInteger mode) (GetFP mode eb sb) (GetFPRoundingMode mode) m) => SafeUnifiedFP mode eb sb m
class (forall eb sb. ValidFP eb sb => UnifiedFP mode eb sb, forall eb sb m. (ValidFP eb sb, UnifiedBranching mode m, MonadError NotRepresentableFPError m) => SafeUnifiedFP mode eb sb m) => AllUnifiedFP mode
class (BasicGrisetteType fp, ConSymConversion (FP eb sb) (SymFP eb sb) fp, UnifiedPrimitive mode fp, Floating fp, SymIEEEFPTraits fp, IEEEFPConstants fp, IEEEFPOp fp, IEEEFPRoundingOp fp rd, UnifiedFromIntegral mode (GetInteger mode) fp, IEEEFPToAlgReal (GetAlgReal mode) fp rd, IEEEFPConvertible (GetInteger mode) fp rd, fpn ~ GetFP mode, fp ~ fpn eb sb, rd ~ GetFPRoundingMode mode) => UnifiedFPImpl (mode :: EvalModeTag) fpn eb sb fp rd | fpn eb sb -> fp rd, fp -> fpn eb sb rd, rd -> fpn, rd eb sb -> fp

Documentation

type family GetFP mode = (f :: Nat -> Nat -> Type) | f -> mode Source #

Get a unified floating point type. Resolves to FP in Con mode, and SymFP in Sym mode.

Instances details

type GetFP 'Con Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedFP type GetFP 'Con = FP
type GetFP 'Sym Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedFP type GetFP 'Sym = SymFP

type family GetFPRoundingMode mode = r | r -> mode Source #

Get a unified floating point rounding mode type. Resolves to FPRoundingMode in Con mode, and SymFPRoundingMode in Sym mode.

Instances details

type GetFPRoundingMode 'Con Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedFP type GetFPRoundingMode 'Con = FPRoundingMode
type GetFPRoundingMode 'Sym Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedFP type GetFPRoundingMode 'Sym = SymFPRoundingMode

class UnifiedFPImpl mode (GetFP mode) eb sb (GetFP mode eb sb) (GetFPRoundingMode mode) => UnifiedFP mode eb sb Source #

Evaluation mode with unified FP type.

Instances details

UnifiedFPImpl mode (GetFP mode) eb sb (GetFP mode eb sb) (GetFPRoundingMode mode) => UnifiedFP mode eb sb Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedFP

class (SafeUnifiedFPImpl mode (GetFP mode) eb sb (GetFP mode eb sb) (GetFPRoundingMode mode) m, UnifiedSafeFromFP mode NotRepresentableFPError (GetInteger mode) (GetFP mode eb sb) (GetFPRoundingMode mode) m) => SafeUnifiedFP mode eb sb m Source #

This class is needed as constraint in user code prior to GHC 9.2.1. See the notes in EvalMode.

Instances details

(SafeUnifiedFPImpl mode (GetFP mode) eb sb (GetFP mode eb sb) (GetFPRoundingMode mode) m, UnifiedSafeFromFP mode NotRepresentableFPError (GetInteger mode) (GetFP mode eb sb) (GetFPRoundingMode mode) m) => SafeUnifiedFP mode eb sb m Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedFP

class (forall eb sb. ValidFP eb sb => UnifiedFP mode eb sb, forall eb sb m. (ValidFP eb sb, UnifiedBranching mode m, MonadError NotRepresentableFPError m) => SafeUnifiedFP mode eb sb m) => AllUnifiedFP mode Source #

Evaluation mode with unified floating point type.

Instances details

(forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => UnifiedFP mode eb sb, forall (eb :: Nat) (sb :: Nat) (m :: Type -> Type). (ValidFP eb sb, UnifiedBranching mode m, MonadError NotRepresentableFPError m) => SafeUnifiedFP mode eb sb m) => AllUnifiedFP mode Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedFP

class (BasicGrisetteType fp, ConSymConversion (FP eb sb) (SymFP eb sb) fp, UnifiedPrimitive mode fp, Floating fp, SymIEEEFPTraits fp, IEEEFPConstants fp, IEEEFPOp fp, IEEEFPRoundingOp fp rd, UnifiedFromIntegral mode (GetInteger mode) fp, IEEEFPToAlgReal (GetAlgReal mode) fp rd, IEEEFPConvertible (GetInteger mode) fp rd, fpn ~ GetFP mode, fp ~ fpn eb sb, rd ~ GetFPRoundingMode mode) => UnifiedFPImpl (mode :: EvalModeTag) fpn eb sb fp rd | fpn eb sb -> fp rd, fp -> fpn eb sb rd, rd -> fpn, rd eb sb -> fp Source #

Implementation for UnifiedFP.

Instances details

ValidFP eb sb => UnifiedFPImpl 'Con FP eb sb (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedFP Associated Types type GetFP 'Con = (f :: Nat -> Nat -> Type) Source # type GetFPRoundingMode 'Con = (r :: Type) Source #
ValidFP eb sb => UnifiedFPImpl 'Sym SymFP eb sb (SymFP eb sb) SymFPRoundingMode Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedFP Associated Types type GetFP 'Sym = (f :: Nat -> Nat -> Type) Source # type GetFPRoundingMode 'Sym = (r :: Type) Source #