{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE QuantifiedConstraints #-}

{- | Fortran CHAR value representation.

Currently only CHARs of known length.
-}

module Language.Fortran.Repr.Value.Scalar.String where

import GHC.TypeNats
import Language.Fortran.Repr.Compat.Natural
import Data.Text ( Text )
import qualified Data.Text as Text
import Language.Fortran.Repr.Util ( natVal'' )
import Data.Proxy
import Unsafe.Coerce

import Text.PrettyPrint.GenericPretty ( Out )
import Text.PrettyPrint.GenericPretty.ViaShow ( OutShowly(..) )
import Data.Binary
import Data.Data

import Data.Singletons
import GHC.TypeLits.Singletons

-- TODO unsafe constructor do not use >:(
-- need context for Reasons(TM)
data FString (l :: NaturalK) = KnownNat l => FString Text
deriving stock instance Show (FString l)
deriving stock instance Eq   (FString l)
deriving stock instance Ord  (FString l) -- TODO
deriving stock instance KnownNat l => Data (FString l)

{-
instance Data (FString l) where
    --gunfold k z c = k (z (\x -> case someFString x of SomeFString y -> y))
    gunfold k z c = k (z (FString @l))
-}

eqFString :: FString l -> FString r -> Bool
eqFString :: forall (l :: Natural) (r :: Natural).
FString l -> FString r -> Bool
eqFString (FString Text
l) (FString Text
r) = Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
r

-- | This is a painful instance to define. We cheat by leveraging the instance
--   of the length-hiding type 'SomeFString', then asserting length. It's CPU
--   and memory inefficient and has backwards dependencies, but is comfortably
--   safe.
instance KnownNat l => Binary (FString l) where
    put :: FString l -> Put
put FString l
t = SomeFString -> Put
forall t. Binary t => t -> Put
put (FString l -> SomeFString
forall (l :: Natural). KnownNat l => FString l -> SomeFString
SomeFString FString l
t)
    get :: Get (FString l)
get =
        forall t. Binary t => Get t
get @SomeFString Get SomeFString
-> (SomeFString -> Get (FString l)) -> Get (FString l)
forall a b. Get a -> (a -> Get b) -> Get b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          SomeFString (FString Text
t) ->
            case forall (l :: Natural). KnownNat l => Text -> Maybe (FString l)
fString @l Text
t of
              Just FString l
t' -> FString l -> Get (FString l)
forall a. a -> Get a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FString l
t'
              Maybe (FString l)
Nothing -> String -> Get (FString l)
forall a. String -> Get a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"FString had incorrect length"

-- | Attempt to a 'Text' into an 'FString' of the given length.
fString :: forall l. KnownNat l => Text -> Maybe (FString l)
fString :: forall (l :: Natural). KnownNat l => Text -> Maybe (FString l)
fString Text
s =
    if   Text -> Int
Text.length Text
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (a :: Natural). KnownNat a => Natural
natVal'' @l)
    then FString l -> Maybe (FString l)
forall a. a -> Maybe a
Just (FString l -> Maybe (FString l)) -> FString l -> Maybe (FString l)
forall a b. (a -> b) -> a -> b
$ Text -> FString l
forall (l :: Natural). KnownNat l => Text -> FString l
FString Text
s
    else Maybe (FString l)
forall a. Maybe a
Nothing

fStringLen :: forall l. KnownNat l => FString l -> Natural
fStringLen :: forall (l :: Natural). KnownNat l => FString l -> Natural
fStringLen FString l
_ = forall (a :: Natural). KnownNat a => Natural
natVal'' @l

data SomeFString = forall (l :: NaturalK). KnownNat l => SomeFString (FString l)
deriving stock instance Show SomeFString
deriving via (OutShowly SomeFString) instance Out SomeFString

instance Eq SomeFString where
    (SomeFString FString l
l) == :: SomeFString -> SomeFString -> Bool
== (SomeFString FString l
r) = FString l
l FString l -> FString l -> Bool
forall (l :: Natural) (r :: Natural).
FString l -> FString r -> Bool
`eqFString` FString l
r

-- TODO impossible??
instance Data SomeFString where

{-
dataSomeFStringT = mkDataType "TODO" [dataSomeFStringC1]
dataSomeFStringC1 = mkConstr dataSomeFStringT "SomeFString" [] Prefix
instance Data SomeFString where
    dataTypeOf _ = dataSomeFStringT
    toConstr = \case
      SomeFString{} -> dataSomeFStringC1
    --gunfold k z c = k (z SomeFString)
    gunfold k z c = k (z (\(FString fstr :: FString l) -> SomeFString @l (FString fstr)))
-}

instance Binary SomeFString where
    put :: SomeFString -> Put
put (SomeFString (FString Text
t)) = Text -> Put
forall t. Binary t => t -> Put
put Text
t
    get :: Get SomeFString
get = Text -> SomeFString
someFString (Text -> SomeFString) -> Get Text -> Get SomeFString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Binary t => Get t
get @Text

-- | Lift a 'Text' into 'SomeFString'.
someFString :: Text -> SomeFString
someFString :: Text -> SomeFString
someFString Text
t =
    case Natural -> SomeNat
someNatVal (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Text -> Int
Text.length Text
t)) of
      SomeNat (Proxy n
_ :: Proxy l) -> FString n -> SomeFString
forall (l :: Natural). KnownNat l => FString l -> SomeFString
SomeFString (FString n -> SomeFString) -> FString n -> SomeFString
forall a b. (a -> b) -> a -> b
$ forall (l :: Natural). KnownNat l => Text -> FString l
FString @l Text
t

someFStringLen :: SomeFString -> Natural
someFStringLen :: SomeFString -> Natural
someFStringLen (SomeFString FString l
s) = FString l -> Natural
forall (l :: Natural). KnownNat l => FString l -> Natural
fStringLen FString l
s

-- TODO dunno how to do this without unsafeCoerce because of the type-level nat
-- addition >:( -- oh actually seems this is an expected usage of it. ok
concatFString
    :: forall ll lr. (KnownNat ll, KnownNat lr)
    => FString ll
    -> FString lr
    -> FString (ll + lr)
concatFString :: forall (ll :: Natural) (lr :: Natural).
(KnownNat ll, KnownNat lr) =>
FString ll -> FString lr -> FString (ll + lr)
concatFString (FString Text
sl) (FString Text
sr) =
    FString ll -> FString (ll + lr)
forall a b. a -> b
unsafeCoerce (FString ll -> FString (ll + lr))
-> FString ll -> FString (ll + lr)
forall a b. (a -> b) -> a -> b
$ forall (l :: Natural). KnownNat l => Text -> FString l
FString @ll (Text -> FString ll) -> Text -> FString ll
forall a b. (a -> b) -> a -> b
$ Text
sl Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
sr

concatSomeFString :: SomeFString -> SomeFString -> SomeFString
concatSomeFString :: SomeFString -> SomeFString -> SomeFString
concatSomeFString (SomeFString FString l
l) (SomeFString FString l
r) =
    case FString l -> FString l -> FString (l + l)
forall (ll :: Natural) (lr :: Natural).
(KnownNat ll, KnownNat lr) =>
FString ll -> FString lr -> FString (ll + lr)
concatFString FString l
l FString l
r of s :: FString (l + l)
s@FString{} -> FString (l + l) -> SomeFString
forall (l :: Natural). KnownNat l => FString l -> SomeFString
SomeFString FString (l + l)
s

fStringBOp :: (Text -> Text -> r) -> FString ll -> FString lr -> r
fStringBOp :: forall r (ll :: Natural) (lr :: Natural).
(Text -> Text -> r) -> FString ll -> FString lr -> r
fStringBOp Text -> Text -> r
f (FString Text
l) (FString Text
r) = Text -> Text -> r
f Text
l Text
r

someFStringBOp :: (Text -> Text -> r) -> SomeFString -> SomeFString -> r
someFStringBOp :: forall r. (Text -> Text -> r) -> SomeFString -> SomeFString -> r
someFStringBOp Text -> Text -> r
f (SomeFString FString l
l) (SomeFString FString l
r) = (Text -> Text -> r) -> FString l -> FString l -> r
forall r (ll :: Natural) (lr :: Natural).
(Text -> Text -> r) -> FString ll -> FString lr -> r
fStringBOp Text -> Text -> r
f FString l
l FString l
r