module Morley.Michelson.Typed.Extract
( fromUType
, mkUType
, mkUType'
, toUType
, withUType
, pattern AsUType
, pattern AsUTypeExt
) where
import Data.Singletons (Sing, SingI, fromSing)
import Morley.Michelson.Typed.Annotation (Notes(..), notesSing)
import Morley.Michelson.Typed.Sing (SingT(..))
import Morley.Michelson.Typed.T (T(..), toUType)
import qualified Morley.Michelson.Untyped as Un
{-# 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). SingI t => Notes t -> Sing t
notesSing)
mkUType :: SingI x => Notes x -> Un.Ty
mkUType :: Notes x -> Ty
mkUType Notes x
notes = (Sing x, Notes x) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Notes x -> Sing x
forall (t :: T). SingI t => Notes t -> Sing t
notesSing Notes x
notes, Notes x
notes)
mkUType' :: (Sing x, Notes x) -> Un.Ty
mkUType' :: (Sing x, Notes x) -> Ty
mkUType' = \case
(Sing x
STInt, NTInt TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TInt TypeAnn
tn
(Sing x
STNat, NTNat TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TNat TypeAnn
tn
(Sing x
STString, NTString TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TString TypeAnn
tn
(Sing x
STBytes, NTBytes TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBytes TypeAnn
tn
(Sing x
STMutez, NTMutez TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TMutez TypeAnn
tn
(Sing x
STBool, NTBool TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBool TypeAnn
tn
(Sing x
STKeyHash, NTKeyHash TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TKeyHash TypeAnn
tn
(Sing x
STBls12381Fr, NTBls12381Fr TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBls12381Fr TypeAnn
tn
(Sing x
STBls12381G1, NTBls12381G1 TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBls12381G1 TypeAnn
tn
(Sing x
STBls12381G2, NTBls12381G2 TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBls12381G2 TypeAnn
tn
(Sing x
STTimestamp, NTTimestamp TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TTimestamp TypeAnn
tn
(Sing x
STAddress, NTAddress TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TAddress TypeAnn
tn
(Sing x
STKey, NTKey TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TKey TypeAnn
tn
(Sing x
STUnit, NTUnit TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TUnit TypeAnn
tn
(Sing x
STSignature, NTSignature TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TSignature TypeAnn
tn
(Sing x
STChainId, NTChainId TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TChainId TypeAnn
tn
(STOption t, NTOption TypeAnn
tn Notes t
n) -> T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.TOption (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ (Sing t, Notes t) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing t
t, Notes t
n)) TypeAnn
tn
(STList t, NTList TypeAnn
tn Notes t
n) -> T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.TList (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ (Sing t, Notes t) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing t
t, Notes t
n)) TypeAnn
tn
(STSet t, NTSet TypeAnn
tn Notes t
n) -> T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.TSet (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ (Sing t, Notes t) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing t
t, Notes t
n)) TypeAnn
tn
(Sing x
STOperation, NTOperation TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TOperation TypeAnn
tn
(Sing x
STChest, NTChest TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TChest TypeAnn
tn
(Sing x
STChestKey, NTChestKey TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TChestKey TypeAnn
tn
(Sing x
STNever, NTNever TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TNever TypeAnn
tn
(STContract t, NTContract TypeAnn
tn Notes t
n) ->
T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.TContract (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ (Sing t, Notes t) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing t
t, Notes t
n)) TypeAnn
tn
(STTicket t, NTTicket TypeAnn
tn Notes t
n) ->
T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.TTicket (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ (Sing t, Notes t) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing t
t, Notes t
n)) TypeAnn
tn
(STPair t t', NTPair TypeAnn
tn FieldAnn
fl FieldAnn
fr VarAnn
vl VarAnn
vr Notes p
nl Notes q
nr) ->
T -> TypeAnn -> Ty
Un.Ty
(FieldAnn -> FieldAnn -> VarAnn -> VarAnn -> Ty -> Ty -> T
Un.TPair FieldAnn
fl FieldAnn
fr VarAnn
vl VarAnn
vr
((Sing p, Notes p) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing p
t, Notes p
nl))
((Sing q, Notes q) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing q
t', Notes q
nr)))
TypeAnn
tn
(STOr t t', NTOr TypeAnn
tn FieldAnn
fl FieldAnn
fr Notes p
nl Notes q
nr) ->
T -> TypeAnn -> Ty
Un.Ty
(FieldAnn -> FieldAnn -> Ty -> Ty -> T
Un.TOr FieldAnn
fl FieldAnn
fr
((Sing p, Notes p) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing p
t, Notes p
nl))
((Sing q, Notes q) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing q
t', Notes q
nr)))
TypeAnn
tn
(STLambda t t', NTLambda TypeAnn
tn Notes p
np Notes q
nq) ->
T -> TypeAnn -> Ty
Un.Ty
(Ty -> Ty -> T
Un.TLambda
((Sing p, Notes p) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing p
t, Notes p
np))
((Sing q, Notes q) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing q
t', Notes q
nq)))
TypeAnn
tn
(STMap t t', NTMap TypeAnn
tn Notes k
nk Notes v
nv) ->
T -> TypeAnn -> Ty
Un.Ty
(Ty -> Ty -> T
Un.TMap
((Sing k, Notes k) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing k
t, Notes k
nk))
((Sing v, Notes v) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing v
t', Notes v
nv)))
TypeAnn
tn
(STBigMap t t', NTBigMap TypeAnn
tn Notes k
nk Notes v
nv) ->
T -> TypeAnn -> Ty
Un.Ty
(Ty -> Ty -> T
Un.TBigMap
((Sing k, Notes k) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing k
t, Notes k
nk))
((Sing v, Notes v) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing v
t', Notes v
nv)))
TypeAnn
tn
withUType
:: Un.Ty
-> (forall t. SingI t => Notes t -> r)
-> r
withUType :: 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)
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 (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
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 (t :: T). TypeAnn -> Notes t -> Notes ('TList t)
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 (t :: T). TypeAnn -> Notes t -> Notes ('TSet t)
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 (t :: T). TypeAnn -> Notes t -> Notes ('TContract t)
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 (t :: T). TypeAnn -> Notes t -> Notes ('TTicket t)
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) (p :: T).
TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes p
-> Notes p
-> Notes ('TPair p p)
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) (p :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes p -> Notes ('TOr p p)
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) (k :: T).
TypeAnn -> Notes p -> Notes k -> Notes ('TLambda p k)
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 ->
Notes ('TMap t t) -> r
forall (t :: T). SingI t => Notes t -> r
cont @('TMap _ _) (TypeAnn -> Notes t -> Notes t -> Notes ('TMap t t)
forall (k :: T) (k :: T).
TypeAnn -> Notes k -> Notes k -> Notes ('TMap k k)
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 ->
Notes ('TBigMap t t) -> r
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 :: Notes t -> Ty
$mAsUType :: forall r.
Ty
-> (forall (t :: T). SingI t => Notes t -> r) -> (Void# -> r) -> r
AsUType notes <- ((\ut -> withUType ut SomeTypedInfo) -> SomeTypedInfo notes)
where AsUType Notes t
notes = Notes t -> Ty
forall (x :: T). SingI x => Notes x -> Ty
mkUType Notes t
notes
{-# COMPLETE AsUType #-}
pattern AsUTypeExt :: () => (SingI t) => Sing t -> Notes t -> Un.Ty
pattern $bAsUTypeExt :: 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 (x :: T). SingI x => Notes x -> Ty
AsUType Notes t
notes
{-# COMPLETE AsUTypeExt #-}