{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}

{- HLINT ignore "Unused LANGUAGE pragma" -}

module Grisette.Internal.SymPrim.FP
  ( ValidFP,
    FP (..),
    FP16,
    FP32,
    FP64,
    withValidFPProofs,
    FPRoundingMode (..),
    allFPRoundingMode,
  )
where

import Control.DeepSeq (NFData (rnf))
import Data.Bits (Bits (complement, shiftL, shiftR, xor, (.&.)))
import Data.Hashable (Hashable (hashWithSalt))
import Data.Int (Int16, Int32, Int64)
import Data.Maybe (fromJust)
import Data.Proxy (Proxy (Proxy))
import Data.SBV
  ( BVIsNonZero,
    FloatingPoint,
    SWord,
    SymVal (literal, unliteral),
    ValidFloat,
    Word16,
    Word32,
    Word64,
    infinity,
    nan,
    sFloatingPointAsSWord,
    sWordAsSFloatingPoint,
  )
import Data.Type.Equality (type (:~:) (Refl))
import GHC.Generics (Generic)
import GHC.TypeLits (KnownNat, Nat, natVal, type (+), type (<=))
import Grisette.Internal.Core.Data.Class.BitCast (BitCast (bitCast))
import Grisette.Internal.Core.Data.Class.BitVector (SizedBV (sizedBVConcat))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.Utils.Parameterized
  ( KnownProof (KnownProof),
    knownAdd,
    unsafeAxiom,
    unsafeLeqProof,
    withKnownProof,
    withLeqProof,
  )
import Language.Haskell.TH.Syntax (Lift (liftTyped))
import Test.QuickCheck (frequency, oneof)
import qualified Test.QuickCheck as QC

bvIsNonZeroFromGEq1 ::
  forall w r proxy.
  (1 <= w) =>
  proxy w ->
  ((BVIsNonZero w) => r) ->
  r
bvIsNonZeroFromGEq1 :: forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 proxy w
_ BVIsNonZero w => r
r1 = case w :~: 1
forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: w :~: 1 of
  w :~: 1
Refl -> r
BVIsNonZero w => r
r1

-- | A type-level proof that the given bit-widths are valid for a floating-point
-- number.
type ValidFP (eb :: Nat) (sb :: Nat) = ValidFloat eb sb

-- | IEEE 754 floating-point number with @eb@ exponent bits and @sb@ significand
-- bits.
newtype FP (eb :: Nat) (sb :: Nat) = FP {forall (eb :: Natural) (sb :: Natural).
FP eb sb -> FloatingPoint eb sb
unFP :: FloatingPoint eb sb}
  deriving newtype (FP eb sb -> FP eb sb -> Bool
(FP eb sb -> FP eb sb -> Bool)
-> (FP eb sb -> FP eb sb -> Bool) -> Eq (FP eb sb)
forall (eb :: Natural) (sb :: Natural).
FP eb sb -> FP eb sb -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (eb :: Natural) (sb :: Natural).
FP eb sb -> FP eb sb -> Bool
== :: FP eb sb -> FP eb sb -> Bool
$c/= :: forall (eb :: Natural) (sb :: Natural).
FP eb sb -> FP eb sb -> Bool
/= :: FP eb sb -> FP eb sb -> Bool
Eq, Int -> FP eb sb -> ShowS
[FP eb sb] -> ShowS
FP eb sb -> String
(Int -> FP eb sb -> ShowS)
-> (FP eb sb -> String) -> ([FP eb sb] -> ShowS) -> Show (FP eb sb)
forall (eb :: Natural) (sb :: Natural). Int -> FP eb sb -> ShowS
forall (eb :: Natural) (sb :: Natural). [FP eb sb] -> ShowS
forall (eb :: Natural) (sb :: Natural). FP eb sb -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (eb :: Natural) (sb :: Natural). Int -> FP eb sb -> ShowS
showsPrec :: Int -> FP eb sb -> ShowS
$cshow :: forall (eb :: Natural) (sb :: Natural). FP eb sb -> String
show :: FP eb sb -> String
$cshowList :: forall (eb :: Natural) (sb :: Natural). [FP eb sb] -> ShowS
showList :: [FP eb sb] -> ShowS
Show)

-- Workaround for https://github.com/GaloisInc/libBF-hs/pull/32, which affects
-- the correctness of the Ord instance for 'Data.SBV.FloatingPoint'.
instance (ValidFP eb sb) => Ord (FP eb sb) where
  FP FloatingPoint eb sb
x < :: FP eb sb -> FP eb sb -> Bool
< FP FloatingPoint eb sb
y | FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
x Bool -> Bool -> Bool
|| FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
y = Bool
False
  FP FloatingPoint eb sb
x < FP FloatingPoint eb sb
y = FloatingPoint eb sb
x FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
forall a. Ord a => a -> a -> Bool
< FloatingPoint eb sb
y
  FP FloatingPoint eb sb
x <= :: FP eb sb -> FP eb sb -> Bool
<= FP FloatingPoint eb sb
y | FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
x Bool -> Bool -> Bool
|| FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
y = Bool
False
  FP FloatingPoint eb sb
x <= FP FloatingPoint eb sb
y = FloatingPoint eb sb
x FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
forall a. Ord a => a -> a -> Bool
<= FloatingPoint eb sb
y
  FP FloatingPoint eb sb
x > :: FP eb sb -> FP eb sb -> Bool
> FP FloatingPoint eb sb
y | FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
x Bool -> Bool -> Bool
|| FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
y = Bool
False
  FP FloatingPoint eb sb
x > FP FloatingPoint eb sb
y = FloatingPoint eb sb
x FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
forall a. Ord a => a -> a -> Bool
> FloatingPoint eb sb
y
  FP FloatingPoint eb sb
x >= :: FP eb sb -> FP eb sb -> Bool
>= FP FloatingPoint eb sb
y | FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
x Bool -> Bool -> Bool
|| FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
y = Bool
False
  FP FloatingPoint eb sb
x >= FP FloatingPoint eb sb
y = FloatingPoint eb sb
x FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
forall a. Ord a => a -> a -> Bool
>= FloatingPoint eb sb
y

-- | IEEE 754 half-precision floating-point number.
type FP16 = FP 5 11

-- | IEEE 754 single-precision floating-point number.
type FP32 = FP 8 24

-- | IEEE 754 double-precision floating-point number.
type FP64 = FP 11 53

-- | Some type-level witnesses that could be derived from 'ValidFP'.
withValidFPProofs ::
  forall eb sb r.
  (ValidFP eb sb) =>
  ( ( KnownNat (eb + sb),
      BVIsNonZero (eb + sb),
      1 <= eb + sb,
      1 <= eb,
      1 <= sb
    ) =>
    r
  ) ->
  r
withValidFPProofs :: forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs (KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
 1 <= eb, 1 <= sb) =>
r
r =
  KnownProof (eb + sb) -> (KnownNat (eb + sb) => r) -> r
forall (n :: Natural) r. KnownProof n -> (KnownNat n => r) -> r
withKnownProof (KnownProof eb -> KnownProof sb -> KnownProof (eb + sb)
forall (m :: Natural) (n :: Natural).
KnownProof m -> KnownProof n -> KnownProof (m + n)
knownAdd (forall (n :: Natural). KnownNat n => KnownProof n
KnownProof @eb) (forall (n :: Natural). KnownNat n => KnownProof n
KnownProof @sb)) ((KnownNat (eb + sb) => r) -> r) -> (KnownNat (eb + sb) => r) -> r
forall a b. (a -> b) -> a -> b
$
    LeqProof 1 (eb + sb) -> ((1 <= (eb + sb)) => r) -> r
forall (m :: Natural) (n :: Natural) r.
LeqProof m n -> ((m <= n) => r) -> r
withLeqProof (forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @1 @(eb + sb)) (((1 <= (eb + sb)) => r) -> r) -> ((1 <= (eb + sb)) => r) -> r
forall a b. (a -> b) -> a -> b
$
      LeqProof 1 eb -> ((1 <= eb) => r) -> r
forall (m :: Natural) (n :: Natural) r.
LeqProof m n -> ((m <= n) => r) -> r
withLeqProof (forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @1 @eb) (((1 <= eb) => r) -> r) -> ((1 <= eb) => r) -> r
forall a b. (a -> b) -> a -> b
$
        LeqProof 1 sb -> ((1 <= sb) => r) -> r
forall (m :: Natural) (n :: Natural) r.
LeqProof m n -> ((m <= n) => r) -> r
withLeqProof (forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @1 @sb) (((1 <= sb) => r) -> r) -> ((1 <= sb) => r) -> r
forall a b. (a -> b) -> a -> b
$
          Proxy (eb + sb) -> (BVIsNonZero (eb + sb) => r) -> r
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(eb + sb)) r
(KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
 1 <= eb, 1 <= sb) =>
r
BVIsNonZero (eb + sb) => r
r

instance (ValidFP eb sb, r ~ (eb + sb)) => BitCast (FP eb sb) (WordN r) where
  bitCast :: FP eb sb -> WordN r
bitCast (FP FloatingPoint eb sb
f)
    | FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
f =
        forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  WordN r)
 -> WordN r)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    WordN r)
-> WordN r
forall a b. (a -> b) -> a -> b
$
          WordN eb -> WordN sb -> WordN (eb + sb)
forall (l :: Natural) (r :: Natural).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
WordN l -> WordN r -> WordN (l + r)
forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat (WordN eb -> Int -> WordN eb
forall a. Bits a => a -> Int -> a
shiftR (-WordN eb
1) Int
1 :: WordN eb) WordN sb
highsb
    | Bool
otherwise = WordN r
WordN (eb + sb)
wordn
    where
      sb :: Int
sb = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy sb -> Integer
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb) :: Int
      highsb :: WordN sb
highsb = forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  WordN sb)
 -> WordN sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    WordN sb)
-> WordN sb
forall a b. (a -> b) -> a -> b
$ WordN sb -> Int -> WordN sb
forall a. Bits a => a -> Int -> a
shiftL WordN sb
3 (Int
sb Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2) :: WordN sb
      wordn :: WordN (eb + sb)
      wordn :: WordN (eb + sb)
wordn =
        forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  WordN (eb + sb))
 -> WordN (eb + sb))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    WordN (eb + sb))
-> WordN (eb + sb)
forall a b. (a -> b) -> a -> b
$
          WordN r -> WordN (eb + sb)
forall a b. (Integral a, Num b) => a -> b
fromIntegral (WordN r -> WordN (eb + sb)) -> WordN r -> WordN (eb + sb)
forall a b. (a -> b) -> a -> b
$
            Maybe (WordN r) -> WordN r
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (WordN r) -> WordN r) -> Maybe (WordN r) -> WordN r
forall a b. (a -> b) -> a -> b
$
              SBV (WordN r) -> Maybe (WordN r)
forall a. SymVal a => SBV a -> Maybe a
unliteral (SBV (WordN r) -> Maybe (WordN r))
-> SBV (WordN r) -> Maybe (WordN r)
forall a b. (a -> b) -> a -> b
$
                SFloatingPoint eb sb -> SWord (eb + sb)
forall (eb :: Natural) (sb :: Natural).
(ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
SFloatingPoint eb sb -> SWord (eb + sb)
sFloatingPointAsSWord (SFloatingPoint eb sb -> SWord (eb + sb))
-> SFloatingPoint eb sb -> SWord (eb + sb)
forall a b. (a -> b) -> a -> b
$
                  FloatingPoint eb sb -> SFloatingPoint eb sb
forall a. SymVal a => a -> SBV a
literal FloatingPoint eb sb
f

instance (ValidFP eb sb, r ~ (eb + sb)) => BitCast (FP eb sb) (IntN r) where
  bitCast :: FP eb sb -> IntN r
bitCast FP eb sb
x = forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
 1 <= eb, 1 <= sb) =>
WordN r -> IntN r
WordN r -> IntN r
forall from to. BitCast from to => from -> to
bitCast (FP eb sb -> WordN r
forall from to. BitCast from to => from -> to
bitCast FP eb sb
x :: WordN r)

instance (ValidFP eb sb, r ~ (eb + sb)) => BitCast (WordN r) (FP eb sb) where
  bitCast :: WordN r -> FP eb sb
bitCast WordN r
v = FloatingPoint eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
FloatingPoint eb sb -> FP eb sb
FP FloatingPoint eb sb
fp
    where
      sword :: SWord r
      sword :: SWord r
sword = forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
 1 <= eb, 1 <= sb) =>
WordN r -> SWord r
WordN r -> SWord r
forall a b. (Integral a, Num b) => a -> b
fromIntegral WordN r
v
      fp :: FloatingPoint eb sb
      fp :: FloatingPoint eb sb
fp =
        forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  FloatingPoint eb sb)
 -> FloatingPoint eb sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    FloatingPoint eb sb)
-> FloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$
          Maybe (FloatingPoint eb sb) -> FloatingPoint eb sb
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (FloatingPoint eb sb) -> FloatingPoint eb sb)
-> Maybe (FloatingPoint eb sb) -> FloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$
            SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb)
forall a. SymVal a => SBV a -> Maybe a
unliteral (SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb))
-> SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb)
forall a b. (a -> b) -> a -> b
$
              SWord (eb + sb) -> SBV (FloatingPoint eb sb)
forall (eb :: Natural) (sb :: Natural).
(KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) =>
SWord (eb + sb) -> SFloatingPoint eb sb
sWordAsSFloatingPoint SWord r
SWord (eb + sb)
sword

instance (ValidFP eb sb, r ~ (eb + sb)) => BitCast (IntN r) (FP eb sb) where
  bitCast :: IntN r -> FP eb sb
bitCast IntN r
x = forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  FP eb sb)
 -> FP eb sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    FP eb sb)
-> FP eb sb
forall a b. (a -> b) -> a -> b
$ WordN r -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast (IntN r -> WordN r
forall from to. BitCast from to => from -> to
bitCast IntN r
x :: WordN (eb + sb))

#define BITCAST_VIA_INTERMEDIATE(from, to, intermediate) \
  instance BitCast (from) (to) where \
    bitCast x = bitCast (bitCast x :: intermediate)

#if 1
BITCAST_VIA_INTERMEDIATE(FP64, Double, WordN 64)
BITCAST_VIA_INTERMEDIATE(FP64, Int64, WordN 64)
BITCAST_VIA_INTERMEDIATE(FP64, Word64, WordN 64)
BITCAST_VIA_INTERMEDIATE(Double, FP64, WordN 64)
BITCAST_VIA_INTERMEDIATE(Int64, FP64, WordN 64)
BITCAST_VIA_INTERMEDIATE(Word64, FP64, WordN 64)

BITCAST_VIA_INTERMEDIATE(FP32, Float, WordN 32)
BITCAST_VIA_INTERMEDIATE(FP32, Int32, WordN 32)
BITCAST_VIA_INTERMEDIATE(FP32, Word32, WordN 32)
BITCAST_VIA_INTERMEDIATE(Float, FP32, WordN 32)
BITCAST_VIA_INTERMEDIATE(Int32, FP32, WordN 32)
BITCAST_VIA_INTERMEDIATE(Word32, FP32, WordN 32)

BITCAST_VIA_INTERMEDIATE(FP16, Word16, WordN 16)
BITCAST_VIA_INTERMEDIATE(FP16, Int16, WordN 16)
BITCAST_VIA_INTERMEDIATE(Word16, FP16, WordN 16)
BITCAST_VIA_INTERMEDIATE(Int16, FP16, WordN 16)
#endif
instance NFData (FP eb sb) where
  rnf :: FP eb sb -> ()
rnf (FP FloatingPoint eb sb
x) = FloatingPoint eb sb
x FloatingPoint eb sb -> () -> ()
forall a b. a -> b -> b
`seq` ()

instance (ValidFP eb sb) => Lift (FP eb sb) where
  liftTyped :: forall (m :: * -> *). Quote m => FP eb sb -> Code m (FP eb sb)
liftTyped FP eb sb
fp = [||from -> to
forall from to. BitCast from to => from -> to
bitCast from
WordN (eb + sb)
wordnValue||]
    where
      wordnValue :: WordN (eb + sb)
wordnValue = FP eb sb -> WordN (eb + sb)
forall from to. BitCast from to => from -> to
bitCast FP eb sb
fp :: WordN (eb + sb)

instance (ValidFP eb sb) => Hashable (FP eb sb) where
  hashWithSalt :: Int -> FP eb sb -> Int
hashWithSalt Int
salt FP eb sb
x = Int -> WordN (eb + sb) -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt (FP eb sb -> WordN (eb + sb)
forall from to. BitCast from to => from -> to
bitCast FP eb sb
x :: WordN (eb + sb))

deriving newtype instance (ValidFloat eb sb) => Num (FP eb sb)

deriving newtype instance (ValidFloat eb sb) => Fractional (FP eb sb)

deriving newtype instance (ValidFloat eb sb) => Floating (FP eb sb)

deriving newtype instance (ValidFloat eb sb) => Real (FP eb sb)

deriving newtype instance (ValidFloat eb sb) => RealFrac (FP eb sb)

deriving newtype instance (ValidFloat eb sb) => RealFloat (FP eb sb)

instance (ValidFloat eb sb) => QC.Arbitrary (FP eb sb) where
  arbitrary :: Gen (FP eb sb)
arbitrary = do
    [(Int, Gen (FP eb sb))] -> Gen (FP eb sb)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
      [ ( Int
3,
          forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  Gen (FP eb sb))
 -> Gen (FP eb sb))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    Gen (FP eb sb))
-> Gen (FP eb sb)
forall a b. (a -> b) -> a -> b
$
            WordN (eb + sb) -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast
              (WordN (eb + sb) -> FP eb sb)
-> Gen (WordN (eb + sb)) -> Gen (FP eb sb)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Gen (WordN (eb + sb))
forall a. Arbitrary a => Gen a
QC.arbitrary :: QC.Gen (WordN (eb + sb)))
        ),
        ( Int
5,
          -- mostly normalized numbers
          forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  Gen (FP eb sb))
 -> Gen (FP eb sb))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    Gen (FP eb sb))
-> Gen (FP eb sb)
forall a b. (a -> b) -> a -> b
$ do
            WordN eb
e <- Gen (WordN eb)
egen
            WordN sb
s <- Gen (WordN sb)
sgen
            WordN (eb + sb)
msb <- Gen (WordN (eb + sb))
msbGen
            WordN (eb + sb)
smsb <- Gen (WordN (eb + sb))
smsbGen
            FP eb sb -> Gen (FP eb sb)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (FP eb sb -> Gen (FP eb sb)) -> FP eb sb -> Gen (FP eb sb)
forall a b. (a -> b) -> a -> b
$ WordN (eb + sb) -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast (WordN eb -> WordN sb -> WordN (eb + sb)
forall (l :: Natural) (r :: Natural).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
WordN l -> WordN r -> WordN (l + r)
forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat WordN eb
e WordN sb
s WordN (eb + sb) -> WordN (eb + sb) -> WordN (eb + sb)
forall a. Bits a => a -> a -> a
`xor` WordN (eb + sb)
msb WordN (eb + sb) -> WordN (eb + sb) -> WordN (eb + sb)
forall a. Bits a => a -> a -> a
`xor` WordN (eb + sb)
smsb)
        ),
        ( Int
4,
          -- mostly denormalized numbers
          forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  Gen (FP eb sb))
 -> Gen (FP eb sb))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    Gen (FP eb sb))
-> Gen (FP eb sb)
forall a b. (a -> b) -> a -> b
$ do
            WordN sb
s <- Gen (WordN sb)
sgen
            WordN (eb + sb)
msb <- Gen (WordN (eb + sb))
msbGen
            WordN (eb + sb)
smsb <- Gen (WordN (eb + sb))
smsbGen
            FP eb sb -> Gen (FP eb sb)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (FP eb sb -> Gen (FP eb sb)) -> FP eb sb -> Gen (FP eb sb)
forall a b. (a -> b) -> a -> b
$
              WordN (eb + sb) -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast (WordN eb -> WordN sb -> WordN (eb + sb)
forall (l :: Natural) (r :: Natural).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
WordN l -> WordN r -> WordN (l + r)
forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat WordN eb
0 WordN sb
s WordN (eb + sb) -> WordN (eb + sb) -> WordN (eb + sb)
forall a. Bits a => a -> a -> a
`xor` WordN (eb + sb)
msb WordN (eb + sb) -> WordN (eb + sb) -> WordN (eb + sb)
forall a. Bits a => a -> a -> a
.&. WordN (eb + sb) -> WordN (eb + sb)
forall a. Bits a => a -> a
complement WordN (eb + sb)
smsb)
        ),
        (Int
1, [Gen (FP eb sb)] -> Gen (FP eb sb)
forall a. HasCallStack => [Gen a] -> Gen a
oneof ([Gen (FP eb sb)] -> Gen (FP eb sb))
-> [Gen (FP eb sb)] -> Gen (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FP eb sb -> Gen (FP eb sb)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (FP eb sb -> Gen (FP eb sb)) -> [FP eb sb] -> [Gen (FP eb sb)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FP eb sb
forall a. Floating a => a
nan, FP eb sb
0, -FP eb sb
0, FP eb sb
forall a. Floating a => a
infinity, -FP eb sb
forall a. Floating a => a
infinity])
      ]
    where
      eb :: Int
eb = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy eb -> Integer
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @eb) :: Int
      sb :: Int
sb = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy sb -> Integer
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb) :: Int
      egen :: Gen (WordN eb)
egen = forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  Gen (WordN eb))
 -> Gen (WordN eb))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    Gen (WordN eb))
-> Gen (WordN eb)
forall a b. (a -> b) -> a -> b
$ Gen (WordN eb)
(KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
 1 <= eb, 1 <= sb) =>
Gen (WordN eb)
forall a. Arbitrary a => Gen a
QC.arbitrary :: QC.Gen (WordN eb)
      sgen :: Gen (WordN sb)
sgen = forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  Gen (WordN sb))
 -> Gen (WordN sb))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    Gen (WordN sb))
-> Gen (WordN sb)
forall a b. (a -> b) -> a -> b
$ Gen (WordN sb)
(KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
 1 <= eb, 1 <= sb) =>
Gen (WordN sb)
forall a. Arbitrary a => Gen a
QC.arbitrary :: QC.Gen (WordN sb)
      msbGen :: Gen (WordN (eb + sb))
msbGen =
        forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  Gen (WordN (eb + sb)))
 -> Gen (WordN (eb + sb)))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    Gen (WordN (eb + sb)))
-> Gen (WordN (eb + sb))
forall a b. (a -> b) -> a -> b
$
          [Gen (WordN (eb + sb))] -> Gen (WordN (eb + sb))
forall a. HasCallStack => [Gen a] -> Gen a
oneof [WordN (eb + sb) -> Gen (WordN (eb + sb))
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return WordN (eb + sb)
0, WordN (eb + sb) -> Gen (WordN (eb + sb))
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (WordN (eb + sb) -> Gen (WordN (eb + sb)))
-> WordN (eb + sb) -> Gen (WordN (eb + sb))
forall a b. (a -> b) -> a -> b
$ WordN (eb + sb)
1 WordN (eb + sb) -> Int -> WordN (eb + sb)
forall a. Bits a => a -> Int -> a
`shiftL` (Int
eb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
sb Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)] ::
          QC.Gen (WordN (eb + sb))
      smsbGen :: Gen (WordN (eb + sb))
smsbGen =
        forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  Gen (WordN (eb + sb)))
 -> Gen (WordN (eb + sb)))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    Gen (WordN (eb + sb)))
-> Gen (WordN (eb + sb))
forall a b. (a -> b) -> a -> b
$
          [Gen (WordN (eb + sb))] -> Gen (WordN (eb + sb))
forall a. HasCallStack => [Gen a] -> Gen a
oneof [WordN (eb + sb) -> Gen (WordN (eb + sb))
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return WordN (eb + sb)
0, WordN (eb + sb) -> Gen (WordN (eb + sb))
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (WordN (eb + sb) -> Gen (WordN (eb + sb)))
-> WordN (eb + sb) -> Gen (WordN (eb + sb))
forall a b. (a -> b) -> a -> b
$ WordN (eb + sb)
1 WordN (eb + sb) -> Int -> WordN (eb + sb)
forall a. Bits a => a -> Int -> a
`shiftL` (Int
sb Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)] ::
          QC.Gen (WordN (eb + sb))

data FPRoundingMode = RNE | RNA | RTP | RTN | RTZ
  deriving (FPRoundingMode -> FPRoundingMode -> Bool
(FPRoundingMode -> FPRoundingMode -> Bool)
-> (FPRoundingMode -> FPRoundingMode -> Bool) -> Eq FPRoundingMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FPRoundingMode -> FPRoundingMode -> Bool
== :: FPRoundingMode -> FPRoundingMode -> Bool
$c/= :: FPRoundingMode -> FPRoundingMode -> Bool
/= :: FPRoundingMode -> FPRoundingMode -> Bool
Eq, Eq FPRoundingMode
Eq FPRoundingMode =>
(FPRoundingMode -> FPRoundingMode -> Ordering)
-> (FPRoundingMode -> FPRoundingMode -> Bool)
-> (FPRoundingMode -> FPRoundingMode -> Bool)
-> (FPRoundingMode -> FPRoundingMode -> Bool)
-> (FPRoundingMode -> FPRoundingMode -> Bool)
-> (FPRoundingMode -> FPRoundingMode -> FPRoundingMode)
-> (FPRoundingMode -> FPRoundingMode -> FPRoundingMode)
-> Ord FPRoundingMode
FPRoundingMode -> FPRoundingMode -> Bool
FPRoundingMode -> FPRoundingMode -> Ordering
FPRoundingMode -> FPRoundingMode -> FPRoundingMode
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FPRoundingMode -> FPRoundingMode -> Ordering
compare :: FPRoundingMode -> FPRoundingMode -> Ordering
$c< :: FPRoundingMode -> FPRoundingMode -> Bool
< :: FPRoundingMode -> FPRoundingMode -> Bool
$c<= :: FPRoundingMode -> FPRoundingMode -> Bool
<= :: FPRoundingMode -> FPRoundingMode -> Bool
$c> :: FPRoundingMode -> FPRoundingMode -> Bool
> :: FPRoundingMode -> FPRoundingMode -> Bool
$c>= :: FPRoundingMode -> FPRoundingMode -> Bool
>= :: FPRoundingMode -> FPRoundingMode -> Bool
$cmax :: FPRoundingMode -> FPRoundingMode -> FPRoundingMode
max :: FPRoundingMode -> FPRoundingMode -> FPRoundingMode
$cmin :: FPRoundingMode -> FPRoundingMode -> FPRoundingMode
min :: FPRoundingMode -> FPRoundingMode -> FPRoundingMode
Ord, Int -> FPRoundingMode -> ShowS
[FPRoundingMode] -> ShowS
FPRoundingMode -> String
(Int -> FPRoundingMode -> ShowS)
-> (FPRoundingMode -> String)
-> ([FPRoundingMode] -> ShowS)
-> Show FPRoundingMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FPRoundingMode -> ShowS
showsPrec :: Int -> FPRoundingMode -> ShowS
$cshow :: FPRoundingMode -> String
show :: FPRoundingMode -> String
$cshowList :: [FPRoundingMode] -> ShowS
showList :: [FPRoundingMode] -> ShowS
Show, (forall x. FPRoundingMode -> Rep FPRoundingMode x)
-> (forall x. Rep FPRoundingMode x -> FPRoundingMode)
-> Generic FPRoundingMode
forall x. Rep FPRoundingMode x -> FPRoundingMode
forall x. FPRoundingMode -> Rep FPRoundingMode x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FPRoundingMode -> Rep FPRoundingMode x
from :: forall x. FPRoundingMode -> Rep FPRoundingMode x
$cto :: forall x. Rep FPRoundingMode x -> FPRoundingMode
to :: forall x. Rep FPRoundingMode x -> FPRoundingMode
Generic, (forall (m :: * -> *). Quote m => FPRoundingMode -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    FPRoundingMode -> Code m FPRoundingMode)
-> Lift FPRoundingMode
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => FPRoundingMode -> m Exp
forall (m :: * -> *).
Quote m =>
FPRoundingMode -> Code m FPRoundingMode
$clift :: forall (m :: * -> *). Quote m => FPRoundingMode -> m Exp
lift :: forall (m :: * -> *). Quote m => FPRoundingMode -> m Exp
$cliftTyped :: forall (m :: * -> *).
Quote m =>
FPRoundingMode -> Code m FPRoundingMode
liftTyped :: forall (m :: * -> *).
Quote m =>
FPRoundingMode -> Code m FPRoundingMode
Lift)
  deriving anyclass (Eq FPRoundingMode
Eq FPRoundingMode =>
(Int -> FPRoundingMode -> Int)
-> (FPRoundingMode -> Int) -> Hashable FPRoundingMode
Int -> FPRoundingMode -> Int
FPRoundingMode -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> FPRoundingMode -> Int
hashWithSalt :: Int -> FPRoundingMode -> Int
$chash :: FPRoundingMode -> Int
hash :: FPRoundingMode -> Int
Hashable, FPRoundingMode -> ()
(FPRoundingMode -> ()) -> NFData FPRoundingMode
forall a. (a -> ()) -> NFData a
$crnf :: FPRoundingMode -> ()
rnf :: FPRoundingMode -> ()
NFData)

allFPRoundingMode :: [FPRoundingMode]
allFPRoundingMode :: [FPRoundingMode]
allFPRoundingMode = [FPRoundingMode
RNE, FPRoundingMode
RNA, FPRoundingMode
RTP, FPRoundingMode
RTN, FPRoundingMode
RTZ]

instance QC.Arbitrary FPRoundingMode where
  arbitrary :: Gen FPRoundingMode
arbitrary = [FPRoundingMode] -> Gen FPRoundingMode
forall a. HasCallStack => [a] -> Gen a
QC.elements [FPRoundingMode
RNE, FPRoundingMode
RNA, FPRoundingMode
RTP, FPRoundingMode
RTN, FPRoundingMode
RTZ]