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