-----------------------------------------------------------------------
-- |
-- Module           : What4.FloatMode
-- Description      : Mode values for controlling the "interpreted" floating point mode.
-- Copyright        : (c) Galois, Inc 2014-2022
-- License          : BSD3
-- Maintainer       : rdockins@galois.com
-- Stability        : provisional
--
-- Desired instances for the @IsInterpretedFloatExprBuilder@ class are selected
-- via the different mode values from this module.
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module What4.FloatMode
  ( type FloatMode
  , FloatModeRepr(..)
  , FloatIEEE
  , FloatUninterpreted
  , FloatReal
  ) where

import           Data.Kind (Type)
import           Data.Parameterized.Classes


-- | Mode flag for how floating-point values should be interpreted.
data FloatMode where
  FloatIEEE :: FloatMode
  FloatUninterpreted :: FloatMode
  FloatReal :: FloatMode

-- | In this mode "interpreted" floating-point values are treated
--   as bit-precise IEEE-754 floats.
type FloatIEEE = 'FloatIEEE

-- | In this mode "interpreted" floating-point values are treated
--   as bitvectors of the appropriate width, and all operations on
--   them are translated as uninterpreted functions.
type FloatUninterpreted = 'FloatUninterpreted

-- | In this mode "interpreted" floating-point values are treated
--   as real-number values, to the extent possible. Expressions that
--   would result in infinities or NaN will yield unspecified values in
--   this mode, or directly produce runtime errors.
type FloatReal = 'FloatReal

data FloatModeRepr :: FloatMode -> Type where
  FloatIEEERepr          :: FloatModeRepr FloatIEEE
  FloatUninterpretedRepr :: FloatModeRepr FloatUninterpreted
  FloatRealRepr          :: FloatModeRepr FloatReal

instance Show (FloatModeRepr fm) where
  showsPrec :: Int -> FloatModeRepr fm -> ShowS
showsPrec Int
_ FloatModeRepr fm
FloatIEEERepr          = String -> ShowS
showString String
"FloatIEEE"
  showsPrec Int
_ FloatModeRepr fm
FloatUninterpretedRepr = String -> ShowS
showString String
"FloatUninterpreted"
  showsPrec Int
_ FloatModeRepr fm
FloatRealRepr          = String -> ShowS
showString String
"FloatReal"

instance ShowF FloatModeRepr

instance KnownRepr FloatModeRepr FloatIEEE          where knownRepr :: FloatModeRepr 'FloatIEEE
knownRepr = FloatModeRepr 'FloatIEEE
FloatIEEERepr
instance KnownRepr FloatModeRepr FloatUninterpreted where knownRepr :: FloatModeRepr 'FloatUninterpreted
knownRepr = FloatModeRepr 'FloatUninterpreted
FloatUninterpretedRepr
instance KnownRepr FloatModeRepr FloatReal          where knownRepr :: FloatModeRepr 'FloatReal
knownRepr = FloatModeRepr 'FloatReal
FloatRealRepr

instance TestEquality FloatModeRepr where
  testEquality :: forall (a :: FloatMode) (b :: FloatMode).
FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b)
testEquality FloatModeRepr a
FloatIEEERepr           FloatModeRepr b
FloatIEEERepr           = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality FloatModeRepr a
FloatUninterpretedRepr  FloatModeRepr b
FloatUninterpretedRepr  = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality FloatModeRepr a
FloatRealRepr           FloatModeRepr b
FloatRealRepr           = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality FloatModeRepr a
_ FloatModeRepr b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing