{-# OPTIONS_GHC -fno-warn-orphans #-}
module Michelson.Typed.Sing
( SingT (..)
, KnownT
, withSomeSingT
, fromSingT
) where
import Data.Kind (Type)
import Data.Singletons (Sing, SingI(..), SingKind(..), SomeSing(..))
import Michelson.Typed.T (T(..))
data SingT :: T -> Type where
STKey :: SingT 'TKey
STUnit :: SingT 'TUnit
STSignature :: SingT 'TSignature
STChainId :: SingT 'TChainId
STOption :: KnownT a => Sing a -> SingT ( 'TOption a)
STList :: KnownT a => Sing a -> SingT ( 'TList a )
STSet :: KnownT a => Sing a -> SingT ( 'TSet a )
STOperation :: SingT 'TOperation
STContract :: (KnownT a)
=> Sing a -> SingT ( 'TContract a )
STPair :: (KnownT a, KnownT b)
=> Sing a -> Sing b -> SingT ('TPair a b)
STOr :: (KnownT a, KnownT b)
=> Sing a -> Sing b -> SingT ('TOr a b)
STLambda :: (KnownT a, KnownT b)
=> Sing a -> Sing b -> SingT ('TLambda a b)
STMap :: (KnownT a, KnownT b)
=> Sing a -> Sing b -> SingT ('TMap a b)
STBigMap :: (KnownT a, KnownT b)
=> Sing a -> Sing b -> SingT ('TBigMap a b)
STInt :: SingT 'TInt
STNat :: SingT 'TNat
STString :: SingT 'TString
STBytes :: SingT 'TBytes
STMutez :: SingT 'TMutez
STBool :: SingT 'TBool
STKeyHash :: SingT 'TKeyHash
STTimestamp :: SingT 'TTimestamp
STAddress :: SingT 'TAddress
type instance Sing = SingT
class (Typeable t, SingI t) => KnownT (t :: T)
instance (Typeable t, SingI t) => KnownT t
data SomeSingT where
SomeSingT :: forall (a :: T). (KnownT a)
=> Sing a -> SomeSingT
withSomeSingT
:: T
-> (forall (a :: T). (KnownT a) => Sing a -> r)
-> r
withSomeSingT :: T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT t :: T
t f :: forall (a :: T). KnownT a => Sing a -> r
f = (\(SomeSingT s :: Sing a
s) -> Sing a -> r
forall (a :: T). KnownT a => Sing a -> r
f Sing a
s) (T -> SomeSingT
toSingT T
t)
fromSingT :: Sing (a :: T) -> T
fromSingT :: Sing a -> T
fromSingT = \case
STKey -> T
TKey
STUnit -> T
TUnit
STSignature -> T
TSignature
STChainId -> T
TChainId
STOption t -> T -> T
TOption (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
t)
STList t -> T -> T
TList (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
t)
STSet t -> T -> T
TSet (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
t)
STOperation -> T
TOperation
STContract t -> T -> T
TContract (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
t)
STPair a b -> T -> T -> T
TPair (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
a) (Sing b -> T
forall (a :: T). Sing a -> T
fromSingT Sing b
b)
STOr a b -> T -> T -> T
TOr (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
a) (Sing b -> T
forall (a :: T). Sing a -> T
fromSingT Sing b
b)
STLambda a b -> T -> T -> T
TLambda (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
a) (Sing b -> T
forall (a :: T). Sing a -> T
fromSingT Sing b
b)
STMap a b -> T -> T -> T
TMap (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
a) (Sing b -> T
forall (a :: T). Sing a -> T
fromSingT Sing b
b)
STBigMap a b -> T -> T -> T
TBigMap (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
a) (Sing b -> T
forall (a :: T). Sing a -> T
fromSingT Sing b
b)
STInt -> T
TInt
STNat -> T
TNat
STString -> T
TString
STBytes -> T
TBytes
STMutez -> T
TMutez
STBool -> T
TBool
STKeyHash -> T
TKeyHash
STTimestamp -> T
TTimestamp
STAddress -> T
TAddress
toSingT :: T -> SomeSingT
toSingT :: T -> SomeSingT
toSingT = \case
TKey -> Sing 'TKey -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TKey
SingT 'TKey
STKey
TUnit -> Sing 'TUnit -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TUnit
SingT 'TUnit
STUnit
TSignature -> Sing 'TSignature -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TSignature
SingT 'TSignature
STSignature
TChainId -> Sing 'TChainId -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TChainId
SingT 'TChainId
STChainId
TOption t :: T
t -> T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
t ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \tSing :: Sing a
tSing -> Sing ('TOption a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TOption a) -> SomeSingT) -> Sing ('TOption a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> SingT ('TOption a)
forall (a :: T). KnownT a => Sing a -> SingT ('TOption a)
STOption Sing a
tSing
TList t :: T
t -> T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
t ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \tSing :: Sing a
tSing -> Sing ('TList a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TList a) -> SomeSingT) -> Sing ('TList a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> SingT ('TList a)
forall (a :: T). KnownT a => Sing a -> SingT ('TList a)
STList Sing a
tSing
TSet ct :: T
ct -> T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
ct ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \ctSing :: Sing a
ctSing -> Sing ('TSet a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TSet a) -> SomeSingT) -> Sing ('TSet a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> SingT ('TSet a)
forall (a :: T). KnownT a => Sing a -> SingT ('TSet a)
STSet Sing a
ctSing
TOperation -> Sing 'TOperation -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TOperation
SingT 'TOperation
STOperation
TContract t :: T
t -> T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
t ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \tSing :: Sing a
tSing -> Sing ('TContract a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TContract a) -> SomeSingT)
-> Sing ('TContract a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> SingT ('TContract a)
forall (a :: T). KnownT a => Sing a -> SingT ('TContract a)
STContract Sing a
tSing
TPair l :: T
l r :: T
r ->
T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
l ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \lSing :: Sing a
lSing ->
T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
r ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \rSing :: Sing a
rSing ->
Sing ('TPair a a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TPair a a) -> SomeSingT) -> Sing ('TPair a a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> SingT ('TPair a a)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TPair a a)
STPair Sing a
lSing Sing a
rSing
TOr l :: T
l r :: T
r ->
T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
l ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \lSing :: Sing a
lSing ->
T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
r ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \rSing :: Sing a
rSing ->
Sing ('TOr a a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TOr a a) -> SomeSingT) -> Sing ('TOr a a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> SingT ('TOr a a)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TOr a a)
STOr Sing a
lSing Sing a
rSing
TLambda l :: T
l r :: T
r ->
T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
l ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \lSing :: Sing a
lSing ->
T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
r ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \rSing :: Sing a
rSing ->
Sing ('TLambda a a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TLambda a a) -> SomeSingT)
-> Sing ('TLambda a a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> SingT ('TLambda a a)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TLambda a a)
STLambda Sing a
lSing Sing a
rSing
TMap l :: T
l r :: T
r ->
T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
l ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \lSing :: Sing a
lSing ->
T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
r ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \rSing :: Sing a
rSing ->
Sing ('TMap a a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TMap a a) -> SomeSingT) -> Sing ('TMap a a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> SingT ('TMap a a)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TMap a a)
STMap Sing a
lSing Sing a
rSing
TBigMap l :: T
l r :: T
r ->
T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
l ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \lSing :: Sing a
lSing ->
T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
r ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \rSing :: Sing a
rSing ->
Sing ('TBigMap a a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TBigMap a a) -> SomeSingT)
-> Sing ('TBigMap a a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> SingT ('TBigMap a a)
forall (a :: T) (b :: T).
(KnownT a, KnownT b) =>
Sing a -> Sing b -> SingT ('TBigMap a b)
STBigMap Sing a
lSing Sing a
rSing
TInt -> Sing 'TInt -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TInt
SingT 'TInt
STInt
TNat -> Sing 'TNat -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TNat
SingT 'TNat
STNat
TString -> Sing 'TString -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TString
SingT 'TString
STString
TBytes -> Sing 'TBytes -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TBytes
SingT 'TBytes
STBytes
TMutez -> Sing 'TMutez -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TMutez
SingT 'TMutez
STMutez
TBool -> Sing 'TBool -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TBool
SingT 'TBool
STBool
TKeyHash -> Sing 'TKeyHash -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TKeyHash
SingT 'TKeyHash
STKeyHash
TTimestamp -> Sing 'TTimestamp -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TTimestamp
SingT 'TTimestamp
STTimestamp
TAddress -> Sing 'TAddress -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TAddress
SingT 'TAddress
STAddress
instance SingKind T where
type Demote T = T
fromSing :: Sing a -> Demote T
fromSing = Sing a -> Demote T
forall (a :: T). Sing a -> T
fromSingT
toSing :: Demote T -> SomeSing T
toSing t :: Demote T
t = case T -> SomeSingT
toSingT Demote T
T
t of SomeSingT s :: Sing a
s -> Sing a -> SomeSing T
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing a
s
instance SingI 'TKey where
sing :: Sing 'TKey
sing = Sing 'TKey
SingT 'TKey
STKey
instance SingI 'TUnit where
sing :: Sing 'TUnit
sing = Sing 'TUnit
SingT 'TUnit
STUnit
instance SingI 'TSignature where
sing :: Sing 'TSignature
sing = Sing 'TSignature
SingT 'TSignature
STSignature
instance SingI 'TChainId where
sing :: Sing 'TChainId
sing = Sing 'TChainId
SingT 'TChainId
STChainId
instance (KnownT a) => SingI ( 'TOption (a :: T)) where
sing :: Sing ('TOption a)
sing = Sing a -> SingT ('TOption a)
forall (a :: T). KnownT a => Sing a -> SingT ('TOption a)
STOption Sing a
forall k (a :: k). SingI a => Sing a
sing
instance (KnownT a) => SingI ( 'TList (a :: T)) where
sing :: Sing ('TList a)
sing = Sing a -> SingT ('TList a)
forall (a :: T). KnownT a => Sing a -> SingT ('TList a)
STList Sing a
forall k (a :: k). SingI a => Sing a
sing
instance (KnownT a) => SingI ( 'TSet (a :: T)) where
sing :: Sing ('TSet a)
sing = Sing a -> SingT ('TSet a)
forall (a :: T). KnownT a => Sing a -> SingT ('TSet a)
STSet Sing a
forall k (a :: k). SingI a => Sing a
sing
instance SingI 'TOperation where
sing :: Sing 'TOperation
sing = Sing 'TOperation
SingT 'TOperation
STOperation
instance (KnownT a) =>
SingI ( 'TContract (a :: T)) where
sing :: Sing ('TContract a)
sing = Sing a -> SingT ('TContract a)
forall (a :: T). KnownT a => Sing a -> SingT ('TContract a)
STContract Sing a
forall k (a :: k). SingI a => Sing a
sing
instance (KnownT a, KnownT b) =>
SingI ( 'TPair a b) where
sing :: Sing ('TPair a b)
sing = Sing a -> Sing b -> SingT ('TPair a b)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TPair a a)
STPair Sing a
forall k (a :: k). SingI a => Sing a
sing Sing b
forall k (a :: k). SingI a => Sing a
sing
instance (KnownT a, KnownT b) =>
SingI ( 'TOr a b) where
sing :: Sing ('TOr a b)
sing = Sing a -> Sing b -> SingT ('TOr a b)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TOr a a)
STOr Sing a
forall k (a :: k). SingI a => Sing a
sing Sing b
forall k (a :: k). SingI a => Sing a
sing
instance (KnownT a, KnownT b) =>
SingI ( 'TLambda a b) where
sing :: Sing ('TLambda a b)
sing = Sing a -> Sing b -> SingT ('TLambda a b)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TLambda a a)
STLambda Sing a
forall k (a :: k). SingI a => Sing a
sing Sing b
forall k (a :: k). SingI a => Sing a
sing
instance (KnownT a, KnownT b) =>
SingI ( 'TMap a b) where
sing :: Sing ('TMap a b)
sing = Sing a -> Sing b -> SingT ('TMap a b)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TMap a a)
STMap Sing a
forall k (a :: k). SingI a => Sing a
sing Sing b
forall k (a :: k). SingI a => Sing a
sing
instance (KnownT a, KnownT b) =>
SingI ( 'TBigMap a b) where
sing :: Sing ('TBigMap a b)
sing = Sing a -> Sing b -> SingT ('TBigMap a b)
forall (a :: T) (b :: T).
(KnownT a, KnownT b) =>
Sing a -> Sing b -> SingT ('TBigMap a b)
STBigMap Sing a
forall k (a :: k). SingI a => Sing a
sing Sing b
forall k (a :: k). SingI a => Sing a
sing
instance SingI 'TInt where
sing :: Sing 'TInt
sing = Sing 'TInt
SingT 'TInt
STInt
instance SingI 'TNat where
sing :: Sing 'TNat
sing = Sing 'TNat
SingT 'TNat
STNat
instance SingI 'TString where
sing :: Sing 'TString
sing = Sing 'TString
SingT 'TString
STString
instance SingI 'TBytes where
sing :: Sing 'TBytes
sing = Sing 'TBytes
SingT 'TBytes
STBytes
instance SingI 'TMutez where
sing :: Sing 'TMutez
sing = Sing 'TMutez
SingT 'TMutez
STMutez
instance SingI 'TBool where
sing :: Sing 'TBool
sing = Sing 'TBool
SingT 'TBool
STBool
instance SingI 'TKeyHash where
sing :: Sing 'TKeyHash
sing = Sing 'TKeyHash
SingT 'TKeyHash
STKeyHash
instance SingI 'TTimestamp where
sing :: Sing 'TTimestamp
sing = Sing 'TTimestamp
SingT 'TTimestamp
STTimestamp
instance SingI 'TAddress where
sing :: Sing 'TAddress
sing = Sing 'TAddress
SingT 'TAddress
STAddress