{-# OPTIONS_GHC -fno-warn-orphans #-}
module Michelson.Typed.Sing
( Sing (..)
, withSomeSingT
, withSomeSingCT
, fromSingT
, fromSingCT
) where
import Data.Kind (Type)
import Data.Singletons (Sing(..), SingI(..), SingKind(..), SomeSing(..))
import Michelson.Typed.T (CT(..), T(..))
data instance Sing :: CT -> Type where
SCInt :: Sing 'CInt
SCNat :: Sing 'CNat
SCString :: Sing 'CString
SCBytes :: Sing 'CBytes
SCMutez :: Sing 'CMutez
SCBool :: Sing 'CBool
SCKeyHash :: Sing 'CKeyHash
SCTimestamp :: Sing 'CTimestamp
SCAddress :: Sing 'CAddress
data instance Sing :: T -> Type where
STc :: (SingI a, Typeable a) => Sing a -> Sing ( 'Tc a)
STKey :: Sing 'TKey
STUnit :: Sing 'TUnit
STSignature :: Sing 'TSignature
STChainId :: Sing 'TChainId
STOption :: (SingI a, Typeable a) => Sing a -> Sing ( 'TOption a)
STList :: (SingI a, Typeable a) => Sing a -> Sing ( 'TList a )
STSet :: (SingI a, Typeable a) => Sing a -> Sing ( 'TSet a )
STOperation :: Sing 'TOperation
STContract :: (SingI a, Typeable a)
=> Sing a -> Sing ( 'TContract a )
STPair :: (SingI a, SingI b, Typeable a, Typeable b)
=> Sing a -> Sing b -> Sing ('TPair a b)
STOr :: (SingI a, SingI b, Typeable a, Typeable b)
=> Sing a -> Sing b -> Sing ('TOr a b)
STLambda :: (SingI a, SingI b, Typeable a, Typeable b)
=> Sing a -> Sing b -> Sing ('TLambda a b)
STMap :: (SingI a, SingI b, Typeable a, Typeable b)
=> Sing a -> Sing b -> Sing ('TMap a b)
STBigMap :: (SingI a, SingI b, Typeable a, Typeable b)
=> Sing a -> Sing b -> Sing ('TBigMap a b)
data SomeSingCT where
SomeSingCT :: forall (a :: CT). (SingI a, Typeable a) => Sing a -> SomeSingCT
withSomeSingCT
:: CT -> (forall (a :: CT). (SingI a, Typeable a) => Sing a -> r) -> r
withSomeSingCT ct f = (\(SomeSingCT s) -> f s) (toSingCT ct)
fromSingCT :: Sing (a :: CT) -> CT
fromSingCT = \case
SCInt -> CInt
SCNat -> CNat
SCString -> CString
SCBytes -> CBytes
SCMutez -> CMutez
SCBool -> CBool
SCKeyHash -> CKeyHash
SCTimestamp -> CTimestamp
SCAddress -> CAddress
toSingCT :: CT -> SomeSingCT
toSingCT = \case
CInt -> SomeSingCT SCInt
CNat -> SomeSingCT SCNat
CString -> SomeSingCT SCString
CBytes -> SomeSingCT SCBytes
CMutez -> SomeSingCT SCMutez
CBool -> SomeSingCT SCBool
CKeyHash -> SomeSingCT SCKeyHash
CTimestamp -> SomeSingCT SCTimestamp
CAddress -> SomeSingCT SCAddress
instance SingKind CT where
type Demote CT = CT
fromSing = fromSingCT
toSing t = case toSingCT t of SomeSingCT s -> SomeSing s
instance SingI 'CInt where
sing = SCInt
instance SingI 'CNat where
sing = SCNat
instance SingI 'CString where
sing = SCString
instance SingI 'CBytes where
sing = SCBytes
instance SingI 'CMutez where
sing = SCMutez
instance SingI 'CBool where
sing = SCBool
instance SingI 'CKeyHash where
sing = SCKeyHash
instance SingI 'CTimestamp where
sing = SCTimestamp
instance SingI 'CAddress where
sing = SCAddress
data SomeSingT where
SomeSingT :: forall (a :: T). (Typeable a, SingI a)
=> Sing a -> SomeSingT
withSomeSingT
:: T
-> (forall (a :: T). (Typeable a, SingI a) => Sing a -> r)
-> r
withSomeSingT t f = (\(SomeSingT s) -> f s) (toSingT t)
fromSingT :: Sing (a :: T) -> T
fromSingT = \case
STc t -> Tc (fromSingCT t)
STKey -> TKey
STUnit -> TUnit
STSignature -> TSignature
STChainId -> TChainId
STOption t -> TOption (fromSingT t)
STList t -> TList (fromSingT t)
STSet t -> TSet (fromSingCT t)
STOperation -> TOperation
STContract t -> TContract (fromSingT t)
STPair a b -> TPair (fromSingT a) (fromSingT b)
STOr a b -> TOr (fromSingT a) (fromSingT b)
STLambda a b -> TLambda (fromSingT a) (fromSingT b)
STMap a b -> TMap (fromSingCT a) (fromSingT b)
STBigMap a b -> TBigMap (fromSingCT a) (fromSingT b)
toSingT :: T -> SomeSingT
toSingT = \case
Tc ct -> withSomeSingCT ct $ \ctSing -> SomeSingT $ STc ctSing
TKey -> SomeSingT STKey
TUnit -> SomeSingT STUnit
TSignature -> SomeSingT STSignature
TChainId -> SomeSingT STChainId
TOption t -> withSomeSingT t $ \tSing -> SomeSingT $ STOption tSing
TList t -> withSomeSingT t $ \tSing -> SomeSingT $ STList tSing
TSet ct -> withSomeSingCT ct $ \ctSing -> SomeSingT $ STSet ctSing
TOperation -> SomeSingT STOperation
TContract t -> withSomeSingT t $ \tSing -> SomeSingT $ STContract tSing
TPair l r ->
withSomeSingT l $ \lSing ->
withSomeSingT r $ \rSing ->
SomeSingT $ STPair lSing rSing
TOr l r ->
withSomeSingT l $ \lSing ->
withSomeSingT r $ \rSing ->
SomeSingT $ STOr lSing rSing
TLambda l r ->
withSomeSingT l $ \lSing ->
withSomeSingT r $ \rSing ->
SomeSingT $ STLambda lSing rSing
TMap l r ->
withSomeSingCT l $ \lSing ->
withSomeSingT r $ \rSing ->
SomeSingT $ STMap lSing rSing
TBigMap l r ->
withSomeSingCT l $ \lSing ->
withSomeSingT r $ \rSing ->
SomeSingT $ STBigMap lSing rSing
instance SingKind T where
type Demote T = T
fromSing = fromSingT
toSing t = case toSingT t of SomeSingT s -> SomeSing s
instance (SingI t, Typeable t) => SingI ( 'Tc (t :: CT)) where
sing = STc sing
instance SingI 'TKey where
sing = STKey
instance SingI 'TUnit where
sing = STUnit
instance SingI 'TSignature where
sing = STSignature
instance SingI 'TChainId where
sing = STChainId
instance (SingI a, Typeable a) => SingI ( 'TOption (a :: T)) where
sing = STOption sing
instance (SingI a, Typeable a) => SingI ( 'TList (a :: T)) where
sing = STList sing
instance (SingI a, Typeable a) => SingI ( 'TSet (a :: CT)) where
sing = STSet sing
instance SingI 'TOperation where
sing = STOperation
instance (SingI a, Typeable a) =>
SingI ( 'TContract (a :: T)) where
sing = STContract sing
instance (SingI a, Typeable a, Typeable b, SingI b) =>
SingI ( 'TPair a b) where
sing = STPair sing sing
instance (SingI a, Typeable a, Typeable b, SingI b) =>
SingI ( 'TOr a b) where
sing = STOr sing sing
instance (SingI a, Typeable a, Typeable b, SingI b) =>
SingI ( 'TLambda a b) where
sing = STLambda sing sing
instance (SingI a, Typeable a, Typeable b, SingI b) =>
SingI ( 'TMap a b) where
sing = STMap sing sing
instance (SingI a, Typeable a, Typeable b, SingI b) =>
SingI ( 'TBigMap a b) where
sing = STBigMap sing sing