{- | 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
[FIntI k] -> ShowS
FIntI k -> String
(Int -> FIntI k -> ShowS)
-> (FIntI k -> String) -> ([FIntI k] -> ShowS) -> Show (FIntI k)
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
$cshowsPrec :: forall (k :: FTInt). Int -> FIntI k -> ShowS
showsPrec :: Int -> FIntI k -> ShowS
$cshow :: forall (k :: FTInt). FIntI k -> String
show :: FIntI k -> String
$cshowList :: forall (k :: FTInt). [FIntI k] -> ShowS
showList :: [FIntI k] -> ShowS
Show, (forall x. FIntI k -> Rep (FIntI k) x)
-> (forall x. Rep (FIntI k) x -> FIntI k) -> Generic (FIntI k)
forall x. Rep (FIntI k) x -> FIntI k
forall x. FIntI k -> Rep (FIntI k) x
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
$cfrom :: forall (k :: FTInt) x. FIntI k -> Rep (FIntI k) x
from :: forall x. FIntI k -> Rep (FIntI k) x
$cto :: forall (k :: FTInt) x. Rep (FIntI k) x -> FIntI k
to :: forall x. Rep (FIntI k) x -> FIntI k
Generic, Typeable (FIntI k)
Typeable (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))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (FIntI k))
-> (FIntI k -> Constr)
-> (FIntI k -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (FIntI k)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (FIntI k)))
-> ((forall b. Data b => b -> b) -> FIntI k -> FIntI k)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> FIntI k -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> FIntI k -> r)
-> (forall u. (forall d. Data d => d -> u) -> FIntI k -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> FIntI k -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> FIntI k -> m (FIntI k))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FIntI k -> m (FIntI k))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FIntI k -> m (FIntI k))
-> Data (FIntI k)
FIntI k -> Constr
FIntI k -> DataType
(forall b. Data b => b -> b) -> FIntI k -> FIntI k
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 u. Int -> (forall d. Data d => d -> u) -> FIntI k -> u
forall u. (forall d. Data d => d -> u) -> FIntI k -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FIntI k -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FIntI k -> r
forall (k :: FTInt). Typeable k => Typeable (FIntI k)
forall (k :: FTInt). Typeable k => FIntI k -> Constr
forall (k :: FTInt). Typeable k => FIntI k -> DataType
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 (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FIntI k -> m (FIntI k)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FIntI k -> m (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)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (FIntI k))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FIntI k -> 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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (FIntI k)
$ctoConstr :: forall (k :: FTInt). Typeable k => FIntI k -> Constr
toConstr :: FIntI k -> Constr
$cdataTypeOf :: forall (k :: FTInt). Typeable k => FIntI k -> DataType
dataTypeOf :: FIntI k -> DataType
$cdataCast1 :: forall (k :: FTInt) (t :: * -> *) (c :: * -> *).
(Typeable k, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (FIntI k))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (FIntI k))
$cgmapT :: forall (k :: FTInt).
Typeable k =>
(forall b. Data b => b -> b) -> FIntI k -> FIntI k
gmapT :: (forall b. Data b => b -> b) -> FIntI k -> FIntI k
$cgmapQl :: 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
$cgmapQr :: forall (k :: FTInt) r r'.
Typeable k =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FIntI k -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FIntI k -> r
$cgmapQ :: forall (k :: FTInt) u.
Typeable k =>
(forall d. Data d => d -> u) -> FIntI k -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FIntI k -> u
$cgmapM :: forall (k :: FTInt) (m :: * -> *).
(Typeable k, Monad 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)
$cgmapMp :: 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)
$cgmapMo :: forall (k :: FTInt) (m :: * -> *).
(Typeable k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> FIntI k -> m (FIntI k)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FIntI k -> m (FIntI k)
Data)
    deriving (FIntI k -> FIntI k -> Bool
(FIntI k -> FIntI k -> Bool)
-> (FIntI k -> FIntI k -> Bool) -> Eq (FIntI k)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (k :: FTInt). 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
Eq, Eq (FIntI k)
Eq (FIntI k) =>
(FIntI k -> FIntI k -> Ordering)
-> (FIntI k -> FIntI k -> Bool)
-> (FIntI k -> FIntI k -> Bool)
-> (FIntI k -> FIntI k -> Bool)
-> (FIntI k -> FIntI k -> Bool)
-> (FIntI k -> FIntI k -> FIntI k)
-> (FIntI k -> FIntI k -> FIntI k)
-> Ord (FIntI k)
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
$ccompare :: forall (k :: FTInt). FIntI k -> FIntI k -> Ordering
compare :: FIntI k -> FIntI k -> Ordering
$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
>= :: FIntI k -> FIntI k -> Bool
$cmax :: forall (k :: FTInt). FIntI k -> FIntI k -> FIntI k
max :: FIntI k -> FIntI k -> FIntI k
$cmin :: forall (k :: FTInt). FIntI k -> FIntI k -> FIntI k
min :: FIntI k -> FIntI k -> FIntI k
Ord) via Integer
    deriving anyclass (Get (FIntI k)
[FIntI k] -> Put
FIntI k -> Put
(FIntI k -> Put)
-> Get (FIntI k) -> ([FIntI k] -> Put) -> Binary (FIntI k)
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
$cput :: forall (k :: FTInt). FIntI k -> Put
put :: FIntI k -> Put
$cget :: forall (k :: FTInt). Get (FIntI k)
get :: Get (FIntI k)
$cputList :: forall (k :: FTInt). [FIntI k] -> Put
putList :: [FIntI k] -> Put
Binary, Int -> FIntI k -> Doc
[FIntI k] -> Doc
FIntI k -> Doc
(Int -> FIntI k -> Doc)
-> (FIntI k -> Doc) -> ([FIntI k] -> Doc) -> Out (FIntI k)
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
$cdocPrec :: forall (k :: FTInt). Int -> FIntI k -> Doc
docPrec :: Int -> FIntI k -> Doc
$cdoc :: forall (k :: FTInt). FIntI k -> Doc
doc :: FIntI k -> Doc
$cdocList :: forall (k :: FTInt). [FIntI k] -> Doc
docList :: [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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> rep -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound @rep)
    then String -> Maybe String
forall a. a -> Maybe a
Just String
"TODO too large"
    else if 　Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< rep -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
minBound @rep)
         then String -> Maybe String
forall a. a -> Maybe a
Just String
"TODO too small"
         else Maybe String
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 Integer -> Integer -> Bool
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)) =
    FIntI (FTIntCombine fk fk) -> SomeFIntI
forall (fk :: FTInt). FIntI fk -> SomeFIntI
SomeFIntI (FIntI (FTIntCombine fk fk) -> SomeFIntI)
-> FIntI (FTIntCombine fk fk) -> SomeFIntI
forall a b. (a -> b) -> a -> b
$ forall (k :: FTInt). Integer -> FIntI k
FIntI @(FTIntCombine lfk rfk) (Integer -> FIntI (FTIntCombine fk fk))
-> Integer -> FIntI (FTIntCombine fk fk)
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
      -}
-}