{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Internal.Impl.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.Impl.Unified.BVFPConversion
  ( UnifiedBVFPConversion,
    SafeUnifiedBVFPConversion,
    AllUnifiedBVFPConversion,
  )
where

import Control.Monad.Error.Class (MonadError)
import GHC.TypeLits (KnownNat, type (+), type (<=))
import Grisette.Internal.Internal.Decl.Unified.BVFPConversion
  ( AllUnifiedBVFPConversion,
    SafeUnifiedBVFPConversion,
    SafeUnifiedBVFPConversionImpl,
    UnifiedBVFPConversion,
    UnifiedBVFPConversionImpl,
  )
import Grisette.Internal.Internal.Decl.Unified.UnifiedBV
  ( UnifiedBVImpl (GetIntN, GetWordN),
  )
import Grisette.Internal.Internal.Decl.Unified.UnifiedFP
  ( UnifiedFPImpl (GetFP, GetFPRoundingMode),
  )
import Grisette.Internal.Internal.Impl.Unified.UnifiedBV ()
import Grisette.Internal.Internal.Impl.Unified.UnifiedFP ()
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP
  ( FP,
    FPRoundingMode,
    NotRepresentableFPError,
    ValidFP,
  )
import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)
import Grisette.Internal.SymPrim.SymFP (SymFP, SymFPRoundingMode)
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 (C, S))

instance
  (ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) =>
  UnifiedBVFPConversionImpl
    'C
    WordN
    IntN
    FP
    n
    eb
    sb
    (WordN n)
    (IntN n)
    (FP eb sb)
    FPRoundingMode

instance
  (ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) =>
  UnifiedBVFPConversionImpl
    'S
    SymWordN
    SymIntN
    SymFP
    n
    eb
    sb
    (SymWordN n)
    (SymIntN n)
    (SymFP eb sb)
    SymFPRoundingMode

instance
  ( 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

instance
  ( 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

instance
  ( 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

instance
  ( 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