{- | Idealized Fortran INTEGER values.

This module stores Fortran INTEGER values in a Haskell 'Integer', together with
a phantom type describing the Fortran kind. This way, we can safely check for
bounds issues, and leave exact behaviour up to the user.
-}

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilyDependencies #-} -- just for better inference (maybe)
{-# LANGUAGE DerivingVia #-}

module Language.Fortran.Repr.Value.Scalar.Int.Idealized where

import Language.Fortran.Repr.Type.Scalar.Int
import Data.Kind
import Data.Int

import GHC.Generics ( Generic )
import Data.Data ( Data )
import Data.Binary ( Binary )
import Text.PrettyPrint.GenericPretty ( Out )

type FIntMRep :: FTInt -> Type
type family FIntMRep k = r | r -> k where
    FIntMRep 'FTInt1 = Int8
    FIntMRep 'FTInt2 = Int16
    FIntMRep 'FTInt4 = Int32
    FIntMRep 'FTInt8 = Int64

newtype FIntI (k :: FTInt) = FIntI Integer
    deriving stock (Int -> FIntI k -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (k :: FTInt). Int -> FIntI k -> ShowS
forall (k :: FTInt). [FIntI k] -> ShowS
forall (k :: FTInt). FIntI k -> String
showList :: [FIntI k] -> ShowS
$cshowList :: forall (k :: FTInt). [FIntI k] -> ShowS
show :: FIntI k -> String
$cshow :: forall (k :: FTInt). FIntI k -> String
showsPrec :: Int -> FIntI k -> ShowS
$cshowsPrec :: forall (k :: FTInt). Int -> FIntI k -> ShowS
Show, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (k :: FTInt) x. Rep (FIntI k) x -> FIntI k
forall (k :: FTInt) x. FIntI k -> Rep (FIntI k) x
$cto :: forall (k :: FTInt) x. Rep (FIntI k) x -> FIntI k
$cfrom :: forall (k :: FTInt) x. FIntI k -> Rep (FIntI k) x
Generic, FIntI k -> DataType
FIntI k -> Constr
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall {k :: FTInt}. Typeable k => Typeable (FIntI k)
forall (k :: FTInt). Typeable k => FIntI k -> DataType
forall (k :: FTInt). Typeable k => FIntI k -> Constr
forall (k :: FTInt).
Typeable k =>
(forall b. Data b => b -> b) -> FIntI k -> FIntI k
forall (k :: FTInt) u.
Typeable k =>
Int -> (forall d. Data d => d -> u) -> FIntI k -> u
forall (k :: FTInt) u.
Typeable k =>
(forall d. Data d => d -> u) -> FIntI k -> [u]
forall (k :: FTInt) r r'.
Typeable k =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FIntI k -> r
forall (k :: FTInt) r r'.
Typeable k =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FIntI k -> r
forall (k :: FTInt) (m :: * -> *).
(Typeable k, Monad m) =>
(forall d. Data d => d -> m d) -> FIntI k -> m (FIntI k)
forall (k :: FTInt) (m :: * -> *).
(Typeable k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> FIntI k -> m (FIntI k)
forall (k :: FTInt) (c :: * -> *).
Typeable k =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (FIntI k)
forall (k :: FTInt) (c :: * -> *).
Typeable k =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FIntI k -> c (FIntI k)
forall (k :: FTInt) (t :: * -> *) (c :: * -> *).
(Typeable k, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (FIntI k))
forall (k :: FTInt) (t :: * -> * -> *) (c :: * -> *).
(Typeable k, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (FIntI k))
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (FIntI k)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FIntI k -> c (FIntI k)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FIntI k -> m (FIntI k)
$cgmapMo :: forall (k :: FTInt) (m :: * -> *).
(Typeable k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> FIntI k -> m (FIntI k)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FIntI k -> m (FIntI k)
$cgmapMp :: forall (k :: FTInt) (m :: * -> *).
(Typeable k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> FIntI k -> m (FIntI k)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FIntI k -> m (FIntI k)
$cgmapM :: forall (k :: FTInt) (m :: * -> *).
(Typeable k, Monad m) =>
(forall d. Data d => d -> m d) -> FIntI k -> m (FIntI k)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FIntI k -> u
$cgmapQi :: forall (k :: FTInt) u.
Typeable k =>
Int -> (forall d. Data d => d -> u) -> FIntI k -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> FIntI k -> [u]
$cgmapQ :: forall (k :: FTInt) u.
Typeable k =>
(forall d. Data d => d -> u) -> FIntI k -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FIntI k -> r
$cgmapQr :: forall (k :: FTInt) r r'.
Typeable k =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FIntI k -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FIntI k -> r
$cgmapQl :: forall (k :: FTInt) r r'.
Typeable k =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FIntI k -> r
gmapT :: (forall b. Data b => b -> b) -> FIntI k -> FIntI k
$cgmapT :: forall (k :: FTInt).
Typeable k =>
(forall b. Data b => b -> b) -> FIntI k -> FIntI k
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (FIntI k))
$cdataCast2 :: forall (k :: FTInt) (t :: * -> * -> *) (c :: * -> *).
(Typeable k, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (FIntI k))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (FIntI k))
$cdataCast1 :: forall (k :: FTInt) (t :: * -> *) (c :: * -> *).
(Typeable k, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (FIntI k))
dataTypeOf :: FIntI k -> DataType
$cdataTypeOf :: forall (k :: FTInt). Typeable k => FIntI k -> DataType
toConstr :: FIntI k -> Constr
$ctoConstr :: forall (k :: FTInt). Typeable k => FIntI k -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (FIntI k)
$cgunfold :: forall (k :: FTInt) (c :: * -> *).
Typeable k =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (FIntI k)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FIntI k -> c (FIntI k)
$cgfoldl :: forall (k :: FTInt) (c :: * -> *).
Typeable k =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FIntI k -> c (FIntI k)
Data)
    deriving (FIntI k -> FIntI k -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (k :: FTInt). FIntI k -> FIntI k -> Bool
/= :: FIntI k -> FIntI k -> Bool
$c/= :: forall (k :: FTInt). FIntI k -> FIntI k -> Bool
== :: FIntI k -> FIntI k -> Bool
$c== :: forall (k :: FTInt). FIntI k -> FIntI k -> Bool
Eq, FIntI k -> FIntI k -> Bool
FIntI k -> FIntI k -> Ordering
FIntI k -> FIntI k -> FIntI k
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (k :: FTInt). Eq (FIntI k)
forall (k :: FTInt). FIntI k -> FIntI k -> Bool
forall (k :: FTInt). FIntI k -> FIntI k -> Ordering
forall (k :: FTInt). FIntI k -> FIntI k -> FIntI k
min :: FIntI k -> FIntI k -> FIntI k
$cmin :: forall (k :: FTInt). FIntI k -> FIntI k -> FIntI k
max :: FIntI k -> FIntI k -> FIntI k
$cmax :: forall (k :: FTInt). FIntI k -> FIntI k -> FIntI k
>= :: FIntI k -> FIntI k -> Bool
$c>= :: forall (k :: FTInt). FIntI k -> FIntI k -> Bool
> :: FIntI k -> FIntI k -> Bool
$c> :: forall (k :: FTInt). FIntI k -> FIntI k -> Bool
<= :: FIntI k -> FIntI k -> Bool
$c<= :: forall (k :: FTInt). FIntI k -> FIntI k -> Bool
< :: FIntI k -> FIntI k -> Bool
$c< :: forall (k :: FTInt). FIntI k -> FIntI k -> Bool
compare :: FIntI k -> FIntI k -> Ordering
$ccompare :: forall (k :: FTInt). FIntI k -> FIntI k -> Ordering
Ord) via Integer
    deriving anyclass (forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
forall (k :: FTInt). Get (FIntI k)
forall (k :: FTInt). [FIntI k] -> Put
forall (k :: FTInt). FIntI k -> Put
putList :: [FIntI k] -> Put
$cputList :: forall (k :: FTInt). [FIntI k] -> Put
get :: Get (FIntI k)
$cget :: forall (k :: FTInt). Get (FIntI k)
put :: FIntI k -> Put
$cput :: forall (k :: FTInt). FIntI k -> Put
Binary, forall a. (Int -> a -> Doc) -> (a -> Doc) -> ([a] -> Doc) -> Out a
forall (k :: FTInt). Int -> FIntI k -> Doc
forall (k :: FTInt). [FIntI k] -> Doc
forall (k :: FTInt). FIntI k -> Doc
docList :: [FIntI k] -> Doc
$cdocList :: forall (k :: FTInt). [FIntI k] -> Doc
doc :: FIntI k -> Doc
$cdoc :: forall (k :: FTInt). FIntI k -> Doc
docPrec :: Int -> FIntI k -> Doc
$cdocPrec :: forall (k :: FTInt). Int -> FIntI k -> Doc
Out)

fIntICheckBounds
    :: forall k rep. (rep ~ FIntMRep k, Bounded rep, Integral rep)
    => FIntI k -> Maybe String
fIntICheckBounds :: forall (k :: FTInt) rep.
(rep ~ FIntMRep k, Bounded rep, Integral rep) =>
FIntI k -> Maybe String
fIntICheckBounds (FIntI Integer
i) =
    if   Integer
i forall a. Ord a => a -> a -> Bool
> forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound @rep)
    then forall a. a -> Maybe a
Just String
"TODO too large"
    else if 　Integer
i forall a. Ord a => a -> a -> Bool
< forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
minBound @rep)
         then forall a. a -> Maybe a
Just String
"TODO too small"
         else forall a. Maybe a
Nothing

data SomeFIntI = forall fk. SomeFIntI (FIntI fk)
deriving stock instance Show SomeFIntI
instance Eq SomeFIntI where
    (SomeFIntI (FIntI Integer
l)) == :: SomeFIntI -> SomeFIntI -> Bool
== (SomeFIntI (FIntI Integer
r)) = Integer
l forall a. Eq a => a -> a -> Bool
== Integer
r

-- this might look silly, but it's because even if we don't do kinded
-- calculations, we must still kind the output
someFIntIBOpWrap
    :: (Integer -> Integer -> Integer)
    -> SomeFIntI -> SomeFIntI -> SomeFIntI
someFIntIBOpWrap :: (Integer -> Integer -> Integer)
-> SomeFIntI -> SomeFIntI -> SomeFIntI
someFIntIBOpWrap Integer -> Integer -> Integer
f (SomeFIntI (FIntI Integer
li :: FIntI lfk)) (SomeFIntI (FIntI Integer
ri :: FIntI rfk)) =
    forall (fk :: FTInt). FIntI fk -> SomeFIntI
SomeFIntI forall a b. (a -> b) -> a -> b
$ forall (k :: FTInt). Integer -> FIntI k
FIntI @(FTIntCombine lfk rfk) forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
f Integer
li Integer
ri

{-
fIntIBOpWrap
    :: forall kl kr. (Integer -> Integer -> Integer)
    -> FIntI kl -> FIntI kr -> FIntI (FTIntCombine kl kr)
fIntIBOpWrap f l r =
    case (l, r) of
      (FIntI il :: FIntI 'FTInt16, FIntI ir) -> FIntI @'FTInt16 $ f il ir

    {-
      (FIntI l) (FIntI r) =
    case (demote @kl, demote @kr) of
      (FTInt16, _) -> FIntI @'FTInt16 x
      (_, FTInt16) -> FIntI @'FTInt16 x
      (FTInt8, _)  -> FIntI @'FTInt8 x
      (_, FTInt8)  -> FIntI @'FTInt8 x
      (FTInt4, _)  -> FIntI @'FTInt4 x
      (_, FTInt4)  -> FIntI @'FTInt4 x
      (FTInt2, _)  -> FIntI @'FTInt2 x
      (_, FTInt2)  -> FIntI @'FTInt2 x
      (FTInt1, FTInt1) -> FIntI @'FTInt1 x
      -}
-}