module Michelson.Typed.Extract
( fromUType
, mkUType
, toUType
, withUType
, pattern AsUType
) where
import Data.Singletons (SingI, sing)
import Michelson.Typed.Annotation (Notes(..))
import Michelson.Typed.Sing (Sing(..), fromSingCT, fromSingT, withSomeSingCT)
import Michelson.Typed.T (T(..), toUType)
import qualified Michelson.Untyped as Un
{-# ANN module ("HLint: ignore Avoid lambda using `infix`" :: Text) #-}
fromUType :: Un.Type -> T
fromUType ut = withUType ut (fromSingT . fst)
mkUType :: Sing x -> Notes x -> Un.Type
mkUType s notes = case (s, notes) of
(STc ct, NTc tn) -> Un.Type (Un.Tc (fromSingCT ct)) tn
(STKey, NTKey tn) -> Un.Type Un.TKey tn
(STUnit, NTUnit tn) -> Un.Type Un.TUnit tn
(STSignature, NTSignature tn) -> Un.Type Un.TSignature tn
(STChainId, NTChainId tn) -> Un.Type Un.TChainId tn
(STOption t, NTOption tn n) -> Un.Type (Un.TOption (mkUType t n)) tn
(STList t, NTList tn n) -> Un.Type (Un.TList (mkUType t n)) tn
(STSet ct, NTSet tn n) -> Un.Type (Un.TSet $ mkComp ct n) tn
(STOperation, NTOperation tn) -> Un.Type Un.TOperation tn
(STContract t, NTContract tn n) ->
Un.Type (Un.TContract (mkUType t n)) tn
(STPair tl tr, NTPair tn fl fr nl nr) ->
Un.Type (Un.TPair fl fr (mkUType tl nl) (mkUType tr nr)) tn
(STOr tl tr, NTOr tn fl fr nl nr) ->
Un.Type (Un.TOr fl fr (mkUType tl nl) (mkUType tr nr)) tn
(STLambda p q, NTLambda tn np nq) ->
Un.Type (Un.TLambda (mkUType p np) (mkUType q nq)) tn
(STMap k v, NTMap tn nk nv) ->
Un.Type (Un.TMap (mkComp k nk) (mkUType v nv)) tn
(STBigMap k v, NTBigMap tn nk nv) ->
Un.Type (Un.TBigMap (mkComp k nk) (mkUType v nv)) tn
where
mkComp t a = Un.Comparable (fromSingCT t) a
withUType
:: Un.Type
-> (forall t. (Typeable t, SingI t) => (Sing t, Notes t) -> r)
-> r
withUType (Un.Type ut tn) cont = case ut of
Un.Tc tc -> withSomeSingCT tc $
\(_ :: Sing tc) -> cont (sing @('Tc tc), NTc tn)
Un.TKey ->
cont (sing @'TKey, NTKey tn)
Un.TUnit ->
cont (sing @'TUnit, NTUnit tn)
Un.TSignature ->
cont (sing @'TSignature, NTSignature tn)
Un.TChainId ->
cont (sing @'TChainId, NTChainId tn)
Un.TOption internalT -> withUType internalT $
\(_ :: Sing internalT, notesInternalT :: Notes internalT) ->
cont (sing @('TOption internalT), NTOption tn notesInternalT)
Un.TList listT -> withUType listT $
\(_ :: Sing listT, notesListT :: Notes listT) ->
cont (sing @('TList listT), NTList tn notesListT)
Un.TSet (Un.Comparable sCT nsCT) -> withSomeSingCT sCT $
\(_ :: Sing sCT) -> cont (sing @('TSet sCT), NTSet tn nsCT)
Un.TOperation ->
cont (sing @'TOperation, NTOperation tn)
Un.TContract contractT -> withUType contractT $
\(_ :: Sing contractT, notesContractT :: Notes contractT) ->
cont (sing @('TContract contractT), NTContract tn notesContractT)
Un.TPair la ra lt rt ->
withUType lt $ \(_ :: Sing lt, ln :: Notes lt) ->
withUType rt $ \(_ :: Sing rt, rn :: Notes rt) ->
cont (sing @('TPair lt rt), NTPair tn la ra ln rn)
Un.TOr la ra lt rt ->
withUType lt $ \(_ :: Sing lt, ln :: Notes lt) ->
withUType rt $ \(_ :: Sing rt, rn :: Notes rt) ->
cont (sing @('TOr lt rt), NTOr tn la ra ln rn)
Un.TLambda lt rt ->
withUType lt $ \(_ :: Sing lt, ln :: Notes lt) ->
withUType rt $ \(_ :: Sing rt, rn :: Notes rt) ->
cont (sing @('TLambda lt rt), NTLambda tn ln rn)
Un.TMap (Un.Comparable keyT notesT) valT ->
withSomeSingCT keyT $ \(_ :: Sing keyT) ->
withUType valT $ \(_ :: Sing valT, valN :: Notes valt) ->
cont (sing @('TMap keyT valT), NTMap tn notesT valN)
Un.TBigMap (Un.Comparable keyT notesT) valT ->
withSomeSingCT keyT $ \(_ :: Sing keyT) ->
withUType valT $ \(_ :: Sing valT, valN :: Notes valt) ->
cont (sing @('TBigMap keyT valT), NTBigMap tn notesT valN)
data SomeTypedInfo = forall t. (Typeable t, SingI t) => SomeTypedInfo (Sing t, Notes t)
pattern AsUType :: () => (Typeable t, SingI t) => Sing t -> Notes t -> Un.Type
pattern AsUType sng notes <- ((\ut -> withUType ut SomeTypedInfo) -> SomeTypedInfo (sng, notes))
where AsUType sng notes = mkUType sng notes
{-# COMPLETE AsUType #-}