module Morley.Michelson.Typed.Extract
( fromUType
, toUType
, withUType
, pattern AsUType
, pattern AsUTypeExt
) where
import Data.Singletons (Sing, SingI, SomeSing(..), fromSing, withSingI)
import Morley.Michelson.Typed.Annotation (Notes(..), mkUType, notesSing)
import Morley.Michelson.Typed.T (T(..), toUType)
import Morley.Michelson.Untyped qualified as Un
import Morley.Util.Peano qualified as Peano
{-# ANN module ("HLint: ignore Avoid lambda using `infix`" :: Text) #-}
fromUType :: Un.Ty -> T
fromUType :: Ty -> T
fromUType Ty
ut = Ty -> (forall (t :: T). SingI t => Notes t -> T) -> T
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
ut (SingT t -> T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (SingT t -> T) -> (Notes t -> SingT t) -> Notes t -> T
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Notes t -> SingT t
forall (t :: T). Notes t -> Sing t
notesSing)
withUType
:: Un.Ty
-> (forall t. SingI t => Notes t -> r)
-> r
withUType :: forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType (Un.Ty T
ut TypeAnn
tn) forall (t :: T). SingI t => Notes t -> r
cont = case T
ut of
T
Un.TInt ->
Notes 'TInt -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TInt
NTInt TypeAnn
tn)
T
Un.TNat ->
Notes 'TNat -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TNat
NTNat TypeAnn
tn)
T
Un.TString ->
Notes 'TString -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TString
NTString TypeAnn
tn)
T
Un.TBytes ->
Notes 'TBytes -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TBytes
NTBytes TypeAnn
tn)
T
Un.TMutez ->
Notes 'TMutez -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TMutez
NTMutez TypeAnn
tn)
T
Un.TBool ->
Notes 'TBool -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TBool
NTBool TypeAnn
tn)
T
Un.TKeyHash ->
Notes 'TKeyHash -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TKeyHash
NTKeyHash TypeAnn
tn)
T
Un.TBls12381Fr ->
Notes 'TBls12381Fr -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TBls12381Fr
NTBls12381Fr TypeAnn
tn)
T
Un.TBls12381G1 ->
Notes 'TBls12381G1 -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TBls12381G1
NTBls12381G1 TypeAnn
tn)
T
Un.TBls12381G2 ->
Notes 'TBls12381G2 -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TBls12381G2
NTBls12381G2 TypeAnn
tn)
T
Un.TTimestamp ->
Notes 'TTimestamp -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TTimestamp
NTTimestamp TypeAnn
tn)
T
Un.TAddress ->
Notes 'TAddress -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TAddress
NTAddress TypeAnn
tn)
T
Un.TKey ->
Notes 'TKey -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TKey
NTKey TypeAnn
tn)
T
Un.TUnit ->
Notes 'TUnit -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TUnit
NTUnit TypeAnn
tn)
T
Un.TSignature ->
Notes 'TSignature -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TSignature
NTSignature TypeAnn
tn)
T
Un.TChainId ->
Notes 'TChainId -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TChainId
NTChainId TypeAnn
tn)
T
Un.TChest ->
Notes 'TChest -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TChest
NTChest TypeAnn
tn)
T
Un.TChestKey ->
Notes 'TChestKey -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TChestKey
NTChestKey TypeAnn
tn)
T
Un.TNever ->
Notes 'TNever -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TNever
NTNever TypeAnn
tn)
T
Un.TTxRollupL2Address ->
Notes 'TTxRollupL2Address -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TTxRollupL2Address
NTTxRollupL2Address TypeAnn
tn)
Un.TSaplingState Natural
n ->
(\(SomeSing Sing a
s) -> Sing a -> (SingI a => r) -> r
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a
s ((SingI a => r) -> r) -> (SingI a => r) -> r
forall a b. (a -> b) -> a -> b
$
Notes ('TSaplingState a) -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Sing a -> Notes ('TSaplingState a)
forall (n :: Peano). TypeAnn -> Sing n -> Notes ('TSaplingState n)
NTSaplingState TypeAnn
tn Sing a
s)
) (SomeSing Peano -> r) -> SomeSing Peano -> r
forall a b. (a -> b) -> a -> b
$ Natural -> SomeSing Peano
Peano.someSingNat Natural
n
Un.TSaplingTransaction Natural
n ->
(\(SomeSing Sing a
s) -> Sing a -> (SingI a => r) -> r
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a
s ((SingI a => r) -> r) -> (SingI a => r) -> r
forall a b. (a -> b) -> a -> b
$
Notes ('TSaplingTransaction a) -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Sing a -> Notes ('TSaplingTransaction a)
forall (n :: Peano).
TypeAnn -> Sing n -> Notes ('TSaplingTransaction n)
NTSaplingTransaction TypeAnn
tn Sing a
s)
) (SomeSing Peano -> r) -> SomeSing Peano -> r
forall a b. (a -> b) -> a -> b
$ Natural -> SomeSing Peano
Peano.someSingNat Natural
n
Un.TOption Ty
internalT -> Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
internalT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$
\(Notes t
notesInternalT :: Notes internalT) ->
Notes ('TOption t) -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes t -> Notes ('TOption t)
forall (t1 :: T). TypeAnn -> Notes t1 -> Notes ('TOption t1)
NTOption TypeAnn
tn Notes t
notesInternalT)
Un.TList Ty
listT -> Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
listT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$
\(Notes t
notesListT :: Notes listT) ->
Notes ('TList t) -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes t -> Notes ('TList t)
forall (t1 :: T). TypeAnn -> Notes t1 -> Notes ('TList t1)
NTList TypeAnn
tn Notes t
notesListT)
Un.TSet Ty
setT -> Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
setT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$
\(Notes t
notesSetT :: Notes setT) ->
Notes ('TSet t) -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes t -> Notes ('TSet t)
forall (t1 :: T). TypeAnn -> Notes t1 -> Notes ('TSet t1)
NTSet TypeAnn
tn Notes t
notesSetT)
T
Un.TOperation ->
Notes 'TOperation -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TOperation
NTOperation TypeAnn
tn)
Un.TContract Ty
contractT -> Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
contractT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$
\(Notes t
notesContractT :: Notes contractT) ->
Notes ('TContract t) -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes t -> Notes ('TContract t)
forall (t1 :: T). TypeAnn -> Notes t1 -> Notes ('TContract t1)
NTContract TypeAnn
tn Notes t
notesContractT)
Un.TTicket Ty
ticketT -> Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
ticketT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$
\(Notes t
notesTicketT :: Notes ticketT) ->
Notes ('TTicket t) -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes t -> Notes ('TTicket t)
forall (t1 :: T). TypeAnn -> Notes t1 -> Notes ('TTicket t1)
NTTicket TypeAnn
tn Notes t
notesTicketT)
Un.TPair FieldAnn
la FieldAnn
ra VarAnn
lv VarAnn
rv Ty
lt Ty
rt ->
Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
lt ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
ln ->
Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
rt ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
rn ->
Notes ('TPair t t) -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes t
-> Notes t
-> Notes ('TPair t t)
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes p
-> Notes q
-> Notes ('TPair p q)
NTPair TypeAnn
tn FieldAnn
la FieldAnn
ra VarAnn
lv VarAnn
rv Notes t
ln Notes t
rn)
Un.TOr FieldAnn
la FieldAnn
ra Ty
lt Ty
rt ->
Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
lt ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
ln ->
Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
rt ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
rn ->
Notes ('TOr t t) -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn
-> FieldAnn -> FieldAnn -> Notes t -> Notes t -> Notes ('TOr t t)
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q)
NTOr TypeAnn
tn FieldAnn
la FieldAnn
ra Notes t
ln Notes t
rn)
Un.TLambda Ty
lt Ty
rt ->
Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
lt ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
ln ->
Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
rt ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
rn ->
Notes ('TLambda t t) -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes t -> Notes t -> Notes ('TLambda t t)
forall (p :: T) (q :: T).
TypeAnn -> Notes p -> Notes q -> Notes ('TLambda p q)
NTLambda TypeAnn
tn Notes t
ln Notes t
rn)
Un.TMap Ty
keyT Ty
valT ->
Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
keyT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
keyN ->
Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
valT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
valN ->
forall (t :: T). SingI t => Notes t -> r
cont @('TMap _ _) (TypeAnn -> Notes t -> Notes t -> Notes ('TMap t t)
forall (k :: T) (v :: T).
TypeAnn -> Notes k -> Notes v -> Notes ('TMap k v)
NTMap TypeAnn
tn Notes t
keyN Notes t
valN)
Un.TBigMap Ty
keyT Ty
valT ->
Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
keyT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
keyN ->
Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
valT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
valN ->
forall (t :: T). SingI t => Notes t -> r
cont @('TBigMap _ _) (TypeAnn -> Notes t -> Notes t -> Notes ('TBigMap t t)
forall (k :: T) (v :: T).
TypeAnn -> Notes k -> Notes v -> Notes ('TBigMap k v)
NTBigMap TypeAnn
tn Notes t
keyN Notes t
valN)
data SomeTypedInfo = forall t. SingI t => SomeTypedInfo (Notes t)
pattern AsUType :: () => (SingI t) => Notes t -> Un.Ty
pattern $bAsUType :: forall (t :: T). SingI t => Notes t -> Ty
$mAsUType :: forall {r}.
Ty
-> (forall {t :: T}. SingI t => Notes t -> r) -> (Void# -> r) -> r
AsUType notes <- ((\Ty
ut -> Ty
-> (forall (t :: T). SingI t => Notes t -> SomeTypedInfo)
-> SomeTypedInfo
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
ut forall (t :: T). SingI t => Notes t -> SomeTypedInfo
SomeTypedInfo) -> SomeTypedInfo notes)
where AsUType Notes t
notes = Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes t
notes
{-# COMPLETE AsUType #-}
pattern AsUTypeExt :: () => (SingI t) => Sing t -> Notes t -> Un.Ty
pattern $bAsUTypeExt :: forall (t :: T). SingI t => Sing t -> Notes t -> Ty
$mAsUTypeExt :: forall {r}.
Ty
-> (forall {t :: T}. SingI t => Sing t -> Notes t -> r)
-> (Void# -> r)
-> r
AsUTypeExt sng notes <- AsUType notes@(notesSing -> sng)
where AsUTypeExt Sing t
_ Notes t
notes = Notes t -> Ty
forall (t :: T). SingI t => Notes t -> Ty
AsUType Notes t
notes
{-# COMPLETE AsUTypeExt #-}