{-# LANGUAGE TemplateHaskell, StandaloneKindSignatures, UndecidableInstances #-}
{-# LANGUAGE NoStarIsType #-}
module Language.Fortran.Repr.Type.Scalar.Int where
import Language.Fortran.Repr.Type.Scalar.Common
import GHC.Generics ( Generic )
import Data.Data ( Data )
import Data.Singletons.TH
import Prelude.Singletons hiding ( type (-), type (*) )
import Data.Ord.Singletons
import GHC.TypeNats
$(singletons [d|
data FTInt
= FTInt1
| FTInt2
| FTInt4
| FTInt8
| FTInt16
deriving stock (Eq, Ord, Show)
|])
deriving stock instance Generic FTInt
deriving stock instance Data FTInt
deriving stock instance Enum FTInt
type FTIntCombine :: FTInt -> FTInt -> FTInt
type family FTIntCombine k1 k2 where
FTIntCombine k k = k
FTIntCombine 'FTInt16 _ = 'FTInt16
FTIntCombine _ 'FTInt16 = 'FTInt16
FTIntCombine 'FTInt8 _ = 'FTInt8
FTIntCombine _ 'FTInt8 = 'FTInt8
FTIntCombine 'FTInt4 _ = 'FTInt4
FTIntCombine _ 'FTInt4 = 'FTInt4
FTIntCombine 'FTInt2 _ = 'FTInt2
FTIntCombine _ 'FTInt2 = 'FTInt2
FTIntCombine 'FTInt1 'FTInt1 = 'FTInt1
instance FKinded FTInt where
type FKindOf 'FTInt1 = 1
type FKindOf 'FTInt2 = 2
type FKindOf 'FTInt4 = 4
type FKindOf 'FTInt8 = 8
type FKindOf 'FTInt16 = 16
type FKindDefault = 'FTInt4
parseFKind :: Natural -> Maybe FTInt
parseFKind = \case Natural
1 -> forall a. a -> Maybe a
Just FTInt
FTInt1
Natural
2 -> forall a. a -> Maybe a
Just FTInt
FTInt2
Natural
4 -> forall a. a -> Maybe a
Just FTInt
FTInt4
Natural
8 -> forall a. a -> Maybe a
Just FTInt
FTInt8
Natural
16 -> forall a. a -> Maybe a
Just FTInt
FTInt16
Natural
_ -> forall a. Maybe a
Nothing
printFKind :: FTInt -> Natural
printFKind (FromSing Sing a
x) = case Sing a
x of
Sing a
SFTInt a
SFTInt1 -> forall k (a :: k) (n :: Natural).
(n ~ FKindOf a, KnownNat n) =>
Sing a -> Natural
reifyKinded Sing a
x
Sing a
SFTInt a
SFTInt2 -> forall k (a :: k) (n :: Natural).
(n ~ FKindOf a, KnownNat n) =>
Sing a -> Natural
reifyKinded Sing a
x
Sing a
SFTInt a
SFTInt4 -> forall k (a :: k) (n :: Natural).
(n ~ FKindOf a, KnownNat n) =>
Sing a -> Natural
reifyKinded Sing a
x
Sing a
SFTInt a
SFTInt8 -> forall k (a :: k) (n :: Natural).
(n ~ FKindOf a, KnownNat n) =>
Sing a -> Natural
reifyKinded Sing a
x
Sing a
SFTInt a
SFTInt16 -> forall k (a :: k) (n :: Natural).
(n ~ FKindOf a, KnownNat n) =>
Sing a -> Natural
reifyKinded Sing a
x
type FTIntMax :: FTInt -> Nat
type family FTIntMax k where
FTIntMax 'FTInt1 = 2^(8*1 -1) - 1
FTIntMax 'FTInt2 = 2^(8*2 -1) - 1
FTIntMax 'FTInt4 = 2^(8*4 -1) - 1
FTIntMax 'FTInt8 = 2^(8*8 -1) - 1
FTIntMax 'FTInt16 = 2^(8*16-1) - 1
type FTIntMin :: FTInt -> Nat
type family FTIntMin k where
FTIntMin 'FTInt1 = 2^(8*1 -1)
FTIntMin 'FTInt2 = 2^(8*2 -1)
FTIntMin 'FTInt4 = 2^(8*4 -1)
FTIntMin 'FTInt8 = 2^(8*8 -1)
FTIntMin 'FTInt16 = 2^(8*16-1)