content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE QuantifiedConstraints #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  -- |
  -- Module      :   Grisette.Internal.Internal.Decl.Unified.BVFPConversion
  -- 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.Internal.Decl.Unified.BVFPConversion
    ( UnifiedBVFPConversion,
      UnifiedBVFPConversionImpl,
      SafeUnifiedBVFPConversion,
      SafeUnifiedBVFPConversionImpl,
      AllUnifiedBVFPConversion,
    )
  where
  
  import Control.Monad.Error.Class (MonadError)
  import GHC.TypeLits (KnownNat, type (+), type (<=))
  import Grisette.Internal.Core.Data.Class.BitCast
    ( BitCast,
      BitCastCanonical,
      BitCastOr,
    )
  import Grisette.Internal.Core.Data.Class.IEEEFP
    ( IEEEFPConvertible,
    )
  import Grisette.Internal.Internal.Decl.Unified.UnifiedBV
    ( UnifiedBVImpl (GetIntN, GetWordN),
    )
  import Grisette.Internal.Internal.Decl.Unified.UnifiedFP
    ( UnifiedFPImpl (GetFP, GetFPRoundingMode),
    )
  import Grisette.Internal.SymPrim.FP
    ( NotRepresentableFPError,
      ValidFP,
    )
  import Grisette.Internal.Unified.Class.UnifiedFromIntegral (UnifiedFromIntegral)
  import Grisette.Internal.Unified.Class.UnifiedSafeBitCast (UnifiedSafeBitCast)
  import Grisette.Internal.Unified.Class.UnifiedSafeFromFP (UnifiedSafeFromFP)
  import Grisette.Internal.Unified.Class.UnifiedSimpleMergeable (UnifiedBranching)
  import Grisette.Internal.Unified.EvalModeTag (EvalModeTag)
  
  -- | Implementation for 'UnifiedBVFPConversion'.
  class
    ( UnifiedBVImpl mode wordn intn n word int,
      UnifiedFPImpl mode fpn eb sb fp fprd,
      BitCast word fp,
      BitCast int fp,
      BitCastOr fp word,
      BitCastOr fp int,
      BitCastCanonical fp word,
      BitCastCanonical fp int,
      UnifiedFromIntegral mode word fp,
      UnifiedFromIntegral mode int fp,
      IEEEFPConvertible int fp fprd,
      IEEEFPConvertible word fp fprd
    ) =>
    UnifiedBVFPConversionImpl
      (mode :: EvalModeTag)
      wordn
      intn
      fpn
      n
      eb
      sb
      word
      int
      fp
      fprd
  
  -- | Implementation for 'SafeUnifiedBVFPConversion'.
  class
    ( UnifiedBVFPConversionImpl mode wordn intn fpn n eb sb word int fp fprd,
      UnifiedSafeBitCast mode NotRepresentableFPError fp int m,
      UnifiedSafeBitCast mode NotRepresentableFPError fp word m,
      UnifiedSafeFromFP mode NotRepresentableFPError word fp fprd m
    ) =>
    SafeUnifiedBVFPConversionImpl mode wordn intn fpn n eb sb word int fp fprd m
  
  -- | Unified constraints for safe conversion from bit-vectors to floating point
  -- numbers.
  class
    ( SafeUnifiedBVFPConversionImpl
        mode
        (GetWordN mode)
        (GetIntN mode)
        (GetFP mode)
        n
        eb
        sb
        (GetWordN mode n)
        (GetIntN mode n)
        (GetFP mode eb sb)
        (GetFPRoundingMode mode)
        m
    ) =>
    SafeUnifiedBVFPConversion mode n eb sb m
  
  -- | Unified constraints for conversion from bit-vectors to floating point
  -- numbers.
  class
    ( UnifiedBVFPConversionImpl
        (mode :: EvalModeTag)
        (GetWordN mode)
        (GetIntN mode)
        (GetFP mode)
        n
        eb
        sb
        (GetWordN mode n)
        (GetIntN mode n)
        (GetFP mode eb sb)
        (GetFPRoundingMode mode)
    ) =>
    UnifiedBVFPConversion mode n eb sb
  
  -- | Evaluation mode with unified conversion from bit-vectors to
  -- floating-points.
  class
    ( forall n eb sb.
      (ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) =>
      UnifiedBVFPConversion mode n eb sb,
      forall n eb sb m.
      ( UnifiedBranching mode m,
        ValidFP eb sb,
        KnownNat n,
        1 <= n,
        n ~ (eb + sb),
        MonadError NotRepresentableFPError m
      ) =>
      SafeUnifiedBVFPConversion mode n eb sb m
    ) =>
    AllUnifiedBVFPConversion mode
  