{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE QuantifiedConstraints #-}
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
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)
deriving stock instance KnownNat l => Data (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 forall a. Eq a => a -> a -> Bool
== Text
r
instance KnownNat l => Binary (FString l) where
put :: FString l -> Put
put FString l
t = forall t. Binary t => t -> Put
put (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 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' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure FString l
t'
Maybe (FString l)
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"FString had incorrect 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 forall a. Eq a => a -> a -> Bool
== forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (a :: Natural). KnownNat a => Natural
natVal'' @l)
then forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (l :: Natural). KnownNat l => Text -> FString l
FString Text
s
else 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 forall (l :: Natural) (r :: Natural).
FString l -> FString r -> Bool
`eqFString` FString l
r
instance Data SomeFString where
instance Binary SomeFString where
put :: SomeFString -> Put
put (SomeFString (FString Text
t)) = forall t. Binary t => t -> Put
put Text
t
get :: Get SomeFString
get = Text -> SomeFString
someFString forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Binary t => Get t
get @Text
someFString :: Text -> SomeFString
someFString :: Text -> SomeFString
someFString Text
t =
case Natural -> SomeNat
someNatVal (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Text -> Int
Text.length Text
t)) of
SomeNat (Proxy n
_ :: Proxy l) -> forall (l :: Natural). KnownNat l => FString l -> SomeFString
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) = forall (l :: Natural). KnownNat l => FString l -> Natural
fStringLen FString l
s
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) =
forall a b. a -> b
unsafeCoerce forall a b. (a -> b) -> a -> b
$ forall (l :: Natural). KnownNat l => Text -> FString l
FString @ll forall a b. (a -> b) -> a -> b
$ Text
sl 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 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{} -> 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) = 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