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