SafeFromFP.hs

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

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.SafeFromFP
-- 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.Core.Data.Class.SafeFromFP (SafeFromFP (..)) where

import Control.Monad.Error.Class (MonadError (throwError))
import GHC.TypeLits (KnownNat, type (<=))
import Grisette.Internal.Core.Control.Monad.Class.Union (MonadUnion)
import Grisette.Internal.Core.Data.Class.IEEEFP
  ( IEEEFPConvertible (fromFPOr),
    IEEEFPRoundingMode (rna, rne, rtn, rtp, rtz),
    fpIsNaN,
    fpIsNegativeInfinite,
    fpIsPositiveInfinite,
  )
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))
import Grisette.Internal.Core.Data.Class.SimpleMergeable (mrgIf)
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.Core.Data.Class.SymEq (SymEq ((.==)))
import Grisette.Internal.Core.Data.Class.SymIEEEFP
  ( SymIEEEFPTraits
      ( symFpIsNaN,
        symFpIsNegativeInfinite,
        symFpIsPositiveInfinite
      ),
  )
import Grisette.Internal.Core.Data.Class.SymOrd (SymOrd ((.<), (.>)))
import Grisette.Internal.Core.Data.Class.TryMerge
  ( TryMerge,
    mrgSingle,
    tryMerge,
  )
import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP
  ( ConvertibleBound (convertibleLowerBound, convertibleUpperBound),
    FP,
    FPRoundingMode,
    NotRepresentableFPError
      ( FPOverflowError,
        FPUnderflowError,
        NaNError
      ),
    ValidFP,
  )
import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal)
import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)
import Grisette.Internal.SymPrim.SymFP (SymFP, SymFPRoundingMode)
import Grisette.Internal.SymPrim.SymInteger (SymInteger)

-- | Safe conversion from floating point numbers that throws exceptions when
-- the result isn't representable by the type.
class
  (MonadError e m, TryMerge m, IEEEFPConvertible a fp fprd) =>
  SafeFromFP e a fp fprd m
  where
  safeFromFP :: fprd -> fp -> m a

instance
  (MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) =>
  SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m
  where
  safeFromFP mode a
    | fpIsPositiveInfinite a = tryMerge $ throwError FPOverflowError
    | fpIsNegativeInfinite a = tryMerge $ throwError FPUnderflowError
    | fpIsNaN a = tryMerge $ throwError NaNError
    | otherwise = mrgSingle $ fromFPOr undefined mode a

instance
  (MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb) =>
  SafeFromFP
    NotRepresentableFPError
    SymAlgReal
    (SymFP eb sb)
    SymFPRoundingMode
    m
  where
  safeFromFP mode a =
    mrgIf (symFpIsPositiveInfinite a) (tryMerge $ throwError FPOverflowError)
      $ mrgIf
        (symFpIsNegativeInfinite a)
        (tryMerge $ throwError FPUnderflowError)
      $ mrgIf (symFpIsNaN a) (tryMerge $ throwError NaNError)
      $ mrgSingle
      $ fromFPOr 0 mode a

instance
  (MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) =>
  SafeFromFP NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m
  where
  safeFromFP mode a
    | fpIsPositiveInfinite a = tryMerge $ throwError FPOverflowError
    | fpIsNegativeInfinite a = tryMerge $ throwError FPUnderflowError
    | fpIsNaN a = tryMerge $ throwError NaNError
    | otherwise = mrgSingle $ fromFPOr 0 mode a

instance
  (MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb) =>
  SafeFromFP
    NotRepresentableFPError
    SymInteger
    (SymFP eb sb)
    SymFPRoundingMode
    m
  where
  safeFromFP mode a =
    mrgIf (symFpIsPositiveInfinite a) (tryMerge $ throwError FPOverflowError)
      $ mrgIf
        (symFpIsNegativeInfinite a)
        (tryMerge $ throwError FPUnderflowError)
      $ mrgIf
        (symFpIsNaN a)
        (tryMerge $ throwError NaNError)
      $ mrgSingle
      $ fromFPOr 0 mode a

instance
  ( MonadError NotRepresentableFPError m,
    TryMerge m,
    ValidFP eb sb,
    KnownNat n,
    1 <= n
  ) =>
  SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m
  where
  safeFromFP mode a = do
    p :: Integer <- safeFromFP mode a
    if p < (fromIntegral (minBound :: WordN n))
      then tryMerge $ throwError FPUnderflowError
      else
        if p > (fromIntegral (maxBound :: WordN n))
          then tryMerge $ throwError FPOverflowError
          else mrgSingle $ fromIntegral p

symConvertibleLowerBound ::
  forall conBV symBV n eb sb.
  ( ConvertibleBound conBV,
    ValidFP eb sb,
    KnownNat n,
    1 <= n,
    Solvable (conBV n) (symBV n)
  ) =>
  symBV n ->
  SymFPRoundingMode ->
  SymFP eb sb
symConvertibleLowerBound _ mode =
  symIte
    (mode .== rne)
    (con $ convertibleLowerBound (undefined :: conBV n) rne)
    $ symIte
      (mode .== rna)
      (con $ convertibleLowerBound (undefined :: conBV n) rna)
    $ symIte
      (mode .== rtp)
      (con $ convertibleLowerBound (undefined :: conBV n) rtp)
    $ symIte
      (mode .== rtn)
      (con $ convertibleLowerBound (undefined :: conBV n) rtn)
      (con $ convertibleLowerBound (undefined :: conBV n) rtz)

symConvertibleUpperBound ::
  forall conBV symBV n eb sb.
  ( ConvertibleBound conBV,
    ValidFP eb sb,
    KnownNat n,
    1 <= n,
    Solvable (conBV n) (symBV n)
  ) =>
  symBV n ->
  SymFPRoundingMode ->
  SymFP eb sb
symConvertibleUpperBound _ mode =
  symIte
    (mode .== rne)
    (con $ convertibleUpperBound (undefined :: conBV n) rne)
    $ symIte
      (mode .== rna)
      (con $ convertibleUpperBound (undefined :: conBV n) rna)
    $ symIte
      (mode .== rtp)
      (con $ convertibleUpperBound (undefined :: conBV n) rtp)
    $ symIte
      (mode .== rtn)
      (con $ convertibleUpperBound (undefined :: conBV n) rtn)
      (con $ convertibleUpperBound (undefined :: conBV n) rtz)

instance
  ( MonadError NotRepresentableFPError m,
    MonadUnion m,
    ValidFP eb sb,
    KnownNat n,
    1 <= n
  ) =>
  SafeFromFP NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m
  where
  safeFromFP mode a =
    mrgIf (symFpIsPositiveInfinite a) (tryMerge $ throwError FPOverflowError)
      $ mrgIf
        (symFpIsNegativeInfinite a)
        (tryMerge $ throwError FPUnderflowError)
      $ mrgIf (symFpIsNaN a) (tryMerge $ throwError NaNError)
      $ mrgIf
        (a .< symConvertibleLowerBound (undefined :: SymWordN n) mode)
        (tryMerge $ throwError FPUnderflowError)
      $ mrgIf
        (a .> symConvertibleUpperBound (undefined :: SymWordN n) mode)
        (tryMerge $ throwError FPOverflowError)
      $ mrgSingle
      $ fromFPOr 0 mode a

instance
  ( MonadError NotRepresentableFPError m,
    TryMerge m,
    ValidFP eb sb,
    KnownNat n,
    1 <= n
  ) =>
  SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m
  where
  safeFromFP mode a = do
    p :: Integer <- safeFromFP mode a
    if p < (fromIntegral (minBound :: IntN n))
      then tryMerge $ throwError FPUnderflowError
      else
        if p > (fromIntegral (maxBound :: IntN n))
          then tryMerge $ throwError FPOverflowError
          else mrgSingle $ fromIntegral p

instance
  ( MonadError NotRepresentableFPError m,
    MonadUnion m,
    ValidFP eb sb,
    KnownNat n,
    1 <= n
  ) =>
  SafeFromFP NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m
  where
  safeFromFP mode a =
    mrgIf (symFpIsPositiveInfinite a) (tryMerge $ throwError FPOverflowError)
      $ mrgIf
        (symFpIsNegativeInfinite a)
        (tryMerge $ throwError FPUnderflowError)
      $ mrgIf (symFpIsNaN a) (tryMerge $ throwError NaNError)
      $ mrgIf
        (a .< symConvertibleLowerBound (undefined :: SymIntN n) mode)
        (tryMerge $ throwError FPUnderflowError)
      $ mrgIf
        (a .> symConvertibleUpperBound (undefined :: SymIntN n) mode)
        (tryMerge $ throwError FPOverflowError)
      $ mrgSingle
      $ fromFPOr 0 mode a