String.hs

{-# 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 (FString l) (FString r) = l == 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 t = put (SomeFString t)
    get =
        get @SomeFString >>= \case
          SomeFString (FString t) ->
            case fString @l t of
              Just t' -> pure t'
              Nothing -> fail "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 s =
    if   Text.length s == fromIntegral (natVal'' @l)
    then Just $ FString s
    else Nothing

fStringLen :: forall l. KnownNat l => FString l -> Natural
fStringLen _ = 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 l) == (SomeFString r) = l `eqFString` 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 (FString t)) = put t
    get = someFString <$> get @Text

-- | Lift a 'Text' into 'SomeFString'.
someFString :: Text -> SomeFString
someFString t =
    case someNatVal (fromIntegral (Text.length t)) of
      SomeNat (_ :: Proxy l) -> SomeFString $ FString @l t

someFStringLen :: SomeFString -> Natural
someFStringLen (SomeFString s) = fStringLen 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 (FString sl) (FString sr) =
    unsafeCoerce $ FString @ll $ sl <> sr

concatSomeFString :: SomeFString -> SomeFString -> SomeFString
concatSomeFString (SomeFString l) (SomeFString r) =
    case concatFString l r of s@FString{} -> SomeFString s

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

someFStringBOp :: (Text -> Text -> r) -> SomeFString -> SomeFString -> r
someFStringBOp f (SomeFString l) (SomeFString r) = fStringBOp f l r