{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Language.Fortran.Repr.Value.Scalar.Common where
import Language.Fortran.Repr.Type.Scalar.Common
import Data.Singletons
import Text.PrettyPrint.GenericPretty ( Out )
import Text.PrettyPrint.GenericPretty.ViaShow ( OutShowly(..) )
import Data.Binary
import Data.Data ( Data, Typeable )
import Data.Kind
data SomeFKinded k ft where
SomeFKinded
:: forall {k} ft (fk :: k)
. (SingKind k, SingI fk, Data (ft fk))
=> ft fk
-> SomeFKinded k ft
deriving stock instance
( SingKind k
, forall (fk :: k). SingI fk
, forall (fk :: k). Data (ft fk)
, Typeable ft
, Typeable k
) => Data (SomeFKinded k ft)
deriving stock instance (forall fk. Show (ft fk)) => Show (SomeFKinded k ft)
deriving via OutShowly (SomeFKinded k ft) instance (forall fk. Show (ft fk)) => Out (SomeFKinded k ft)
instance
( Binary (Demote k)
, SingKind k
, forall (fk :: k). SingI fk => Binary (ft fk)
, forall (fk :: k). Data (ft fk)
) => Binary (SomeFKinded k ft) where
put :: SomeFKinded k ft -> Put
put someV :: SomeFKinded k ft
someV@(SomeFKinded ft fk
v) = do
forall t. Binary t => t -> Put
put forall a b. (a -> b) -> a -> b
$ forall {k} k (ft :: k -> *). SomeFKinded k ft -> Demote k
someFKindedKind SomeFKinded k ft
someV
forall t. Binary t => t -> Put
put ft fk
v
get :: Get (SomeFKinded k ft)
get = forall t. Binary t => Get t
get @(Demote k) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Demote k
kindTag ->
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k
kindTag forall (fk :: k). Sing fk -> Get (SomeFKinded k ft)
f
where
f :: forall (fk :: k). Sing fk -> Get (SomeFKinded k ft)
f :: forall (fk :: k). Sing fk -> Get (SomeFKinded k ft)
f Sing fk
kind = do
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI @fk Sing fk
kind forall a b. (a -> b) -> a -> b
$ do
ft fk
v <- forall t. Binary t => Get t
get @(ft fk)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => a
undefined
someFKindedKind :: SomeFKinded k ft -> Demote k
someFKindedKind :: forall {k} k (ft :: k -> *). SomeFKinded k ft -> Demote k
someFKindedKind (SomeFKinded (ft fk
_ :: ft fk)) = forall {k} (a :: k). (SingKind k, SingI a) => Demote k
demote @fk
class FKinded a where
type FKindedT a
type FKindedC a b :: Constraint
fKind :: a -> FKindedT a