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
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)
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
instance Eq SomeFString where
(SomeFString (FString Text
sl)) == :: SomeFString -> SomeFString -> Bool
== (SomeFString (FString Text
sr)) = Text
sl forall a. Eq a => a -> a -> Bool
== Text
sr
someFString :: Text -> SomeFString
someFString :: Text -> SomeFString
someFString Text
s =
case Natural -> SomeNat
someNatVal (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Text -> Int
Text.length Text
s)) of
SomeNat (Proxy n
_ :: Proxy n) -> 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 @n Text
s
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