    {-|
    Module           : What4.Utils.OnlyIntRepr
    Copyright        : (c) Galois, Inc. 2020
    License          : BSD3
    Maintainer       : Joe Hendrix <jhendrix@galois.com>

    Defines a GADT for indicating a base type must be an integer.  Used for
    restricting index types in MATLAB arrays.
    -}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE TypeOperators #-}
    module What4.Utils.OnlyIntRepr
      ( OnlyIntRepr(..)
      , toBaseTypeRepr
      ) where

    import Data.Hashable (Hashable(..))
    import Data.Parameterized.Classes (HashableF(..))
    import What4.BaseTypes

    -- | This provides a GADT instance used to indicate a 'BaseType' must have
    -- value 'BaseIntegerType'.
    data OnlyIntRepr tp
       = (tp ~ BaseIntegerType) => OnlyIntRepr

    instance TestEquality OnlyIntRepr where
      testEquality :: forall (a :: BaseType) (b :: BaseType).
    OnlyIntRepr a -> OnlyIntRepr b -> Maybe (a :~: b)
    testEquality OnlyIntRepr a
    OnlyIntRepr OnlyIntRepr b
    OnlyIntRepr = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl

    instance Eq (OnlyIntRepr tp) where
      OnlyIntRepr tp
    OnlyIntRepr == :: OnlyIntRepr tp -> OnlyIntRepr tp -> Bool
    == OnlyIntRepr tp
    OnlyIntRepr = Bool
    True

    instance Hashable (OnlyIntRepr tp) where
      hashWithSalt :: Int -> OnlyIntRepr tp -> Int
    hashWithSalt Int
    s OnlyIntRepr tp
    OnlyIntRepr = Int
    s

    instance HashableF OnlyIntRepr where
      hashWithSaltF :: forall (tp :: BaseType). Int -> OnlyIntRepr tp -> Int
    hashWithSaltF = Int -> OnlyIntRepr tp -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt

    toBaseTypeRepr :: OnlyIntRepr tp -> BaseTypeRepr tp
    toBaseTypeRepr :: forall (tp :: BaseType). OnlyIntRepr tp -> BaseTypeRepr tp
    toBaseTypeRepr OnlyIntRepr tp
    OnlyIntRepr = BaseTypeRepr tp
    BaseTypeRepr BaseIntegerType
    BaseIntegerRepr