{- | 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 Language.Fortran.Repr.Value.Scalar.Common
import Data.Kind
import Data.Int
import Data.Singletons

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 (Int -> FIntI k -> ShowS
[FIntI k] -> ShowS
FIntI k -> String
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, 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

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

type SomeFIntI = SomeFKinded FTInt FIntI
deriving stock instance Show SomeFIntI
instance Eq SomeFIntI where
    (SomeFKinded (FIntI Integer
l)) == :: SomeFIntI -> SomeFIntI -> Bool
== (SomeFKinded (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 l :: SomeFIntI
l@(SomeFKinded (FIntI Integer
il)) r :: SomeFIntI
r@(SomeFKinded (FIntI Integer
ir)) =
    case (forall k (ft :: k -> *). SomeFKinded k ft -> Demote k
someFKindedKind SomeFIntI
l, forall k (ft :: k -> *). SomeFKinded k ft -> Demote k
someFKindedKind SomeFIntI
r) of
      (FTInt
FTInt16, FTInt
_) -> forall (k :: FTInt). SingI k => SomeFIntI
as @'FTInt16
      (FTInt
_, FTInt
FTInt16) -> forall (k :: FTInt). SingI k => SomeFIntI
as @'FTInt16
      (FTInt
FTInt8, FTInt
_) -> forall (k :: FTInt). SingI k => SomeFIntI
as @'FTInt8
      (FTInt
_, FTInt
FTInt8) -> forall (k :: FTInt). SingI k => SomeFIntI
as @'FTInt8
      (FTInt
FTInt4, FTInt
_) -> forall (k :: FTInt). SingI k => SomeFIntI
as @'FTInt4
      (FTInt
_, FTInt
FTInt4) -> forall (k :: FTInt). SingI k => SomeFIntI
as @'FTInt4
      (FTInt
FTInt2, FTInt
_) -> forall (k :: FTInt). SingI k => SomeFIntI
as @'FTInt2
      (FTInt
_, FTInt
FTInt2) -> forall (k :: FTInt). SingI k => SomeFIntI
as @'FTInt2
      (FTInt
FTInt1, FTInt
FTInt1) -> forall (k :: FTInt). SingI k => SomeFIntI
as @'FTInt1
  where
    x :: Integer
x = Integer -> Integer -> Integer
f Integer
il Integer
ir
    as :: forall (k :: FTInt). SingI k => SomeFIntI
    as :: forall (k :: FTInt). SingI k => SomeFIntI
as = forall k (ft :: k -> *) (fk :: k).
(SingKind k, SingI fk) =>
ft fk -> SomeFKinded k ft
SomeFKinded forall a b. (a -> b) -> a -> b
$ forall (k :: FTInt). Integer -> FIntI k
FIntI @k Integer
x

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