{-# LANGUAGE DeriveLift #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Morley.Michelson.Typed.Annotation
( Notes (..)
, insertTypeAnn
, isStar
, starNotes
, mkUType
, notesSing
, notesT
, AnnVar
, Anns(.., Anns1, Anns2, Anns2', Anns3, Anns3', Anns3'', Anns4, Anns4'', Anns5')
, AnnotateInstr(..)
) where
import Data.Default (Default(def))
import Data.Singletons (Sing, SingI(..), fromSing)
import Fmt (Buildable(..))
import Language.Haskell.TH.Syntax (Lift)
import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDoc)
import Morley.Michelson.Typed.Sing
import Morley.Michelson.Typed.T (T(..))
import Morley.Michelson.Untyped qualified as Un
import Morley.Michelson.Untyped.Annotation (Annotation, FieldAnn, TypeAnn, VarAnn, noAnn)
import Morley.Util.Peano qualified as Peano
import Morley.Util.PeanoNatural (singPeanoVal)
import Morley.Util.TH
{-# ANN module ("HLint: ignore Avoid lambda using `infix`" :: Text) #-}
data Notes t where
NTKey :: TypeAnn -> Notes 'TKey
NTUnit :: TypeAnn -> Notes 'TUnit
NTSignature :: TypeAnn -> Notes 'TSignature
NTChainId :: TypeAnn -> Notes 'TChainId
NTOption :: TypeAnn -> Notes t -> Notes ('TOption t)
NTList :: TypeAnn -> Notes t -> Notes ('TList t)
NTSet :: TypeAnn -> Notes t -> Notes ('TSet t)
NTOperation :: TypeAnn -> Notes 'TOperation
NTContract :: TypeAnn -> Notes t -> Notes ('TContract t)
NTTicket :: TypeAnn -> Notes t -> Notes ('TTicket t)
NTPair :: TypeAnn -> FieldAnn -> FieldAnn
-> VarAnn -> VarAnn
-> Notes p -> Notes q -> Notes ('TPair p q)
NTOr :: TypeAnn -> FieldAnn -> FieldAnn
-> Notes p -> Notes q -> Notes ('TOr p q)
NTLambda :: TypeAnn -> Notes p -> Notes q -> Notes ('TLambda p q)
NTMap :: TypeAnn -> Notes k -> Notes v -> Notes ('TMap k v)
NTBigMap :: TypeAnn -> Notes k -> Notes v -> Notes ('TBigMap k v)
NTInt :: TypeAnn -> Notes 'TInt
NTNat :: TypeAnn -> Notes 'TNat
NTString :: TypeAnn -> Notes 'TString
NTBytes :: TypeAnn -> Notes 'TBytes
NTMutez :: TypeAnn -> Notes 'TMutez
NTBool :: TypeAnn -> Notes 'TBool
NTKeyHash :: TypeAnn -> Notes 'TKeyHash
NTBls12381Fr :: TypeAnn -> Notes 'TBls12381Fr
NTBls12381G1 :: TypeAnn -> Notes 'TBls12381G1
NTBls12381G2 :: TypeAnn -> Notes 'TBls12381G2
NTTimestamp :: TypeAnn -> Notes 'TTimestamp
NTAddress :: TypeAnn -> Notes 'TAddress
NTChest :: TypeAnn -> Notes 'TChest
NTChestKey :: TypeAnn -> Notes 'TChestKey
NTNever :: TypeAnn -> Notes 'TNever
NTTxRollupL2Address :: TypeAnn -> Notes 'TTxRollupL2Address
NTSaplingState :: forall (n :: Peano.Peano). TypeAnn -> Sing n -> Notes ('TSaplingState n)
NTSaplingTransaction :: forall (n :: Peano.Peano). TypeAnn -> Sing n -> Notes ('TSaplingTransaction n)
deriving stock instance Eq (Notes t)
deriving stock instance Show (Notes t)
deriving stock instance Lift (Notes t)
$(deriveGADTNFData ''Notes)
instance Buildable (Notes t) where
build :: Notes t -> Builder
build = Notes t -> Builder
forall a. RenderDoc a => a -> Builder
buildRenderDoc
instance RenderDoc (Notes t) where
renderDoc :: RenderContext -> Notes t -> Doc
renderDoc RenderContext
pn = RenderContext -> Ty -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
pn (Ty -> Doc) -> (Notes t -> Ty) -> Notes t -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType
notesSing :: Notes t -> Sing t
notesSing :: forall (t :: T). Notes t -> Sing t
notesSing = \case
NTInt TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTNat TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTString TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTBytes TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTMutez TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTBool TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTKeyHash TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTBls12381Fr TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTBls12381G1 TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTBls12381G2 TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTTimestamp TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTAddress TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTKey TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTUnit TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTSignature TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTChainId TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTOption TypeAnn
_ Notes t
n -> Sing t -> SingT ('TOption t)
forall (n :: T). Sing n -> SingT ('TOption n)
STOption (Notes t -> Sing t
forall (t :: T). Notes t -> Sing t
notesSing Notes t
n)
NTList TypeAnn
_ Notes t
n -> Sing t -> SingT ('TList t)
forall (n :: T). Sing n -> SingT ('TList n)
STList (Notes t -> Sing t
forall (t :: T). Notes t -> Sing t
notesSing Notes t
n)
NTSet TypeAnn
_ Notes t
n -> Sing t -> SingT ('TSet t)
forall (n :: T). Sing n -> SingT ('TSet n)
STSet (Notes t -> Sing t
forall (t :: T). Notes t -> Sing t
notesSing Notes t
n)
NTOperation TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTChest TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTChestKey TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTTxRollupL2Address TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTNever TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
NTSaplingState TypeAnn
_ Sing n
s -> Sing n -> SingT ('TSaplingState n)
forall (n :: Peano). Sing n -> SingT ('TSaplingState n)
STSaplingState Sing n
s
NTSaplingTransaction TypeAnn
_ Sing n
s -> Sing n -> SingT ('TSaplingTransaction n)
forall (n :: Peano). Sing n -> SingT ('TSaplingTransaction n)
STSaplingTransaction Sing n
s
NTContract TypeAnn
_ Notes t
n -> Sing t -> SingT ('TContract t)
forall (n :: T). Sing n -> SingT ('TContract n)
STContract (Notes t -> Sing t
forall (t :: T). Notes t -> Sing t
notesSing Notes t
n)
NTTicket TypeAnn
_ Notes t
n -> Sing t -> SingT ('TTicket t)
forall (n :: T). Sing n -> SingT ('TTicket n)
STTicket (Notes t -> Sing t
forall (t :: T). Notes t -> Sing t
notesSing Notes t
n)
NTPair TypeAnn
_ FieldAnn
_ FieldAnn
_ VarAnn
_ VarAnn
_ Notes p
l Notes q
r -> Sing p -> Sing q -> SingT ('TPair p q)
forall (n1 :: T) (n2 :: T).
Sing n1 -> Sing n2 -> SingT ('TPair n1 n2)
STPair (Notes p -> Sing p
forall (t :: T). Notes t -> Sing t
notesSing Notes p
l) (Notes q -> Sing q
forall (t :: T). Notes t -> Sing t
notesSing Notes q
r)
NTOr TypeAnn
_ FieldAnn
_ FieldAnn
_ Notes p
l Notes q
r -> Sing p -> Sing q -> SingT ('TOr p q)
forall (n1 :: T) (n2 :: T).
Sing n1 -> Sing n2 -> SingT ('TOr n1 n2)
STOr (Notes p -> Sing p
forall (t :: T). Notes t -> Sing t
notesSing Notes p
l) (Notes q -> Sing q
forall (t :: T). Notes t -> Sing t
notesSing Notes q
r)
NTLambda TypeAnn
_ Notes p
l Notes q
r -> Sing p -> Sing q -> SingT ('TLambda p q)
forall (n1 :: T) (n2 :: T).
Sing n1 -> Sing n2 -> SingT ('TLambda n1 n2)
STLambda (Notes p -> Sing p
forall (t :: T). Notes t -> Sing t
notesSing Notes p
l) (Notes q -> Sing q
forall (t :: T). Notes t -> Sing t
notesSing Notes q
r)
NTMap TypeAnn
_ Notes k
l Notes v
r -> Sing k -> Sing v -> SingT ('TMap k v)
forall (n1 :: T) (n2 :: T).
Sing n1 -> Sing n2 -> SingT ('TMap n1 n2)
STMap (Notes k -> Sing k
forall (t :: T). Notes t -> Sing t
notesSing Notes k
l) (Notes v -> Sing v
forall (t :: T). Notes t -> Sing t
notesSing Notes v
r)
NTBigMap TypeAnn
_ Notes k
l Notes v
r -> Sing k -> Sing v -> SingT ('TBigMap k v)
forall (n1 :: T) (n2 :: T).
Sing n1 -> Sing n2 -> SingT ('TBigMap n1 n2)
STBigMap (Notes k -> Sing k
forall (t :: T). Notes t -> Sing t
notesSing Notes k
l) (Notes v -> Sing v
forall (t :: T). Notes t -> Sing t
notesSing Notes v
r)
notesT :: Notes t -> T
notesT :: forall (t :: T). Notes t -> T
notesT = 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
mkUType :: Notes x -> Un.Ty
mkUType :: forall (x :: T). Notes x -> Ty
mkUType = \case
NTInt TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TInt TypeAnn
tn
NTNat TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TNat TypeAnn
tn
NTString TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TString TypeAnn
tn
NTBytes TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBytes TypeAnn
tn
NTMutez TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TMutez TypeAnn
tn
NTBool TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBool TypeAnn
tn
NTKeyHash TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TKeyHash TypeAnn
tn
NTBls12381Fr TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBls12381Fr TypeAnn
tn
NTBls12381G1 TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBls12381G1 TypeAnn
tn
NTBls12381G2 TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBls12381G2 TypeAnn
tn
NTTimestamp TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TTimestamp TypeAnn
tn
NTAddress TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TAddress TypeAnn
tn
NTKey TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TKey TypeAnn
tn
NTUnit TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TUnit TypeAnn
tn
NTSignature TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TSignature TypeAnn
tn
NTChainId TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TChainId TypeAnn
tn
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
$ Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes t
n) TypeAnn
tn
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
$ Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes t
n) TypeAnn
tn
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
$ Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes t
n) TypeAnn
tn
NTOperation TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TOperation TypeAnn
tn
NTChest TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TChest TypeAnn
tn
NTChestKey TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TChestKey TypeAnn
tn
NTTxRollupL2Address TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TTxRollupL2Address TypeAnn
tn
NTNever TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TNever TypeAnn
tn
NTSaplingState TypeAnn
tn Sing n
s -> T -> TypeAnn -> Ty
Un.Ty (Natural -> T
Un.TSaplingState (SingNat n -> Natural
forall (n :: Peano). SingNat n -> Natural
singPeanoVal Sing n
SingNat n
s)) TypeAnn
tn
NTSaplingTransaction TypeAnn
tn Sing n
s -> T -> TypeAnn -> Ty
Un.Ty (Natural -> T
Un.TSaplingTransaction (SingNat n -> Natural
forall (n :: Peano). SingNat n -> Natural
singPeanoVal Sing n
SingNat n
s)) TypeAnn
tn
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
$ Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes t
n) TypeAnn
tn
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
$ Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes t
n) TypeAnn
tn
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 (Notes p -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes p
nl) (Notes q -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes q
nr)) TypeAnn
tn
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 (Notes p -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes p
nl) (Notes q -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes q
nr)) TypeAnn
tn
NTLambda TypeAnn
tn Notes p
np Notes q
nq -> T -> TypeAnn -> Ty
Un.Ty (Ty -> Ty -> T
Un.TLambda (Notes p -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes p
np) (Notes q -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes q
nq)) TypeAnn
tn
NTMap TypeAnn
tn Notes k
nk Notes v
nv -> T -> TypeAnn -> Ty
Un.Ty (Ty -> Ty -> T
Un.TMap (Notes k -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes k
nk) (Notes v -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes v
nv)) TypeAnn
tn
NTBigMap TypeAnn
tn Notes k
nk Notes v
nv -> T -> TypeAnn -> Ty
Un.Ty (Ty -> Ty -> T
Un.TBigMap (Notes k -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes k
nk) (Notes v -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes v
nv)) TypeAnn
tn
starNotes :: forall t. SingI t => Notes t
starNotes :: forall (t :: T). SingI t => Notes t
starNotes = Sing t -> Notes t
forall (t :: T). Sing t -> Notes t
starNotes' Sing t
forall {k} (a :: k). SingI a => Sing a
sing
starNotes' :: Sing t -> Notes t
starNotes' :: forall (t :: T). Sing t -> Notes t
starNotes' = \case
Sing t
SingT t
STInt -> TypeAnn -> Notes 'TInt
NTInt TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STNat -> TypeAnn -> Notes 'TNat
NTNat TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STString -> TypeAnn -> Notes 'TString
NTString TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STBytes -> TypeAnn -> Notes 'TBytes
NTBytes TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STMutez -> TypeAnn -> Notes 'TMutez
NTMutez TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STBool -> TypeAnn -> Notes 'TBool
NTBool TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STKeyHash -> TypeAnn -> Notes 'TKeyHash
NTKeyHash TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STBls12381Fr -> TypeAnn -> Notes 'TBls12381Fr
NTBls12381Fr TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STBls12381G1 -> TypeAnn -> Notes 'TBls12381G1
NTBls12381G1 TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STBls12381G2 -> TypeAnn -> Notes 'TBls12381G2
NTBls12381G2 TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STTimestamp -> TypeAnn -> Notes 'TTimestamp
NTTimestamp TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STAddress -> TypeAnn -> Notes 'TAddress
NTAddress TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STKey -> TypeAnn -> Notes 'TKey
NTKey TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STUnit -> TypeAnn -> Notes 'TUnit
NTUnit TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STTxRollupL2Address -> TypeAnn -> Notes 'TTxRollupL2Address
NTTxRollupL2Address TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STNever -> TypeAnn -> Notes 'TNever
NTNever TypeAnn
forall {k} (a :: k). Annotation a
noAnn
STSaplingState Sing n
s -> TypeAnn -> Sing n -> Notes ('TSaplingState n)
forall (t :: Peano). TypeAnn -> Sing t -> Notes ('TSaplingState t)
NTSaplingState TypeAnn
forall {k} (a :: k). Annotation a
noAnn Sing n
s
STSaplingTransaction Sing n
s -> TypeAnn -> Sing n -> Notes ('TSaplingTransaction n)
forall (t :: Peano).
TypeAnn -> Sing t -> Notes ('TSaplingTransaction t)
NTSaplingTransaction TypeAnn
forall {k} (a :: k). Annotation a
noAnn Sing n
s
Sing t
SingT t
STSignature -> TypeAnn -> Notes 'TSignature
NTSignature TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STChainId -> TypeAnn -> Notes 'TChainId
NTChainId TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STOperation -> TypeAnn -> Notes 'TOperation
NTOperation TypeAnn
forall {k} (a :: k). Annotation a
noAnn
STSet Sing n
t -> TypeAnn -> Notes n -> Notes ('TSet n)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TSet t)
NTSet TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Notes n -> Notes ('TSet n)) -> Notes n -> Notes ('TSet n)
forall a b. (a -> b) -> a -> b
$ Sing n -> Notes n
forall (t :: T). Sing t -> Notes t
starNotes' Sing n
t
STList Sing n
t -> TypeAnn -> Notes n -> Notes ('TList n)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TList t)
NTList TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Notes n -> Notes ('TList n)) -> Notes n -> Notes ('TList n)
forall a b. (a -> b) -> a -> b
$ Sing n -> Notes n
forall (t :: T). Sing t -> Notes t
starNotes' Sing n
t
STOption Sing n
t -> TypeAnn -> Notes n -> Notes ('TOption n)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Notes n -> Notes ('TOption n)) -> Notes n -> Notes ('TOption n)
forall a b. (a -> b) -> a -> b
$ Sing n -> Notes n
forall (t :: T). Sing t -> Notes t
starNotes' Sing n
t
STContract Sing n
t -> TypeAnn -> Notes n -> Notes ('TContract n)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TContract t)
NTContract TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Notes n -> Notes ('TContract n))
-> Notes n -> Notes ('TContract n)
forall a b. (a -> b) -> a -> b
$ Sing n -> Notes n
forall (t :: T). Sing t -> Notes t
starNotes' Sing n
t
STTicket Sing n
t -> TypeAnn -> Notes n -> Notes ('TTicket n)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TTicket t)
NTTicket TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Notes n -> Notes ('TTicket n)) -> Notes n -> Notes ('TTicket n)
forall a b. (a -> b) -> a -> b
$ Sing n -> Notes n
forall (t :: T). Sing t -> Notes t
starNotes' Sing n
t
STMap Sing n1
t Sing n2
t' -> TypeAnn -> Notes n1 -> Notes n2 -> Notes ('TMap n1 n2)
forall (t :: T) (xs :: T).
TypeAnn -> Notes t -> Notes xs -> Notes ('TMap t xs)
NTMap TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Sing n1 -> Notes n1
forall (t :: T). Sing t -> Notes t
starNotes' Sing n1
t) (Sing n2 -> Notes n2
forall (t :: T). Sing t -> Notes t
starNotes' Sing n2
t')
STBigMap Sing n1
t Sing n2
t' -> TypeAnn -> Notes n1 -> Notes n2 -> Notes ('TBigMap n1 n2)
forall (t :: T) (xs :: T).
TypeAnn -> Notes t -> Notes xs -> Notes ('TBigMap t xs)
NTBigMap TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Sing n1 -> Notes n1
forall (t :: T). Sing t -> Notes t
starNotes' Sing n1
t) (Sing n2 -> Notes n2
forall (t :: T). Sing t -> Notes t
starNotes' Sing n2
t')
STPair Sing n1
t Sing n2
t' ->
TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes n1
-> Notes n2
-> Notes ('TPair n1 n2)
forall (t :: T) (xs :: T).
TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes t
-> Notes xs
-> Notes ('TPair t xs)
NTPair TypeAnn
forall {k} (a :: k). Annotation a
noAnn FieldAnn
forall {k} (a :: k). Annotation a
noAnn FieldAnn
forall {k} (a :: k). Annotation a
noAnn VarAnn
forall {k} (a :: k). Annotation a
noAnn VarAnn
forall {k} (a :: k). Annotation a
noAnn (Sing n1 -> Notes n1
forall (t :: T). Sing t -> Notes t
starNotes' Sing n1
t) (Sing n2 -> Notes n2
forall (t :: T). Sing t -> Notes t
starNotes' Sing n2
t')
STOr Sing n1
t Sing n2
t' -> TypeAnn
-> FieldAnn
-> FieldAnn
-> Notes n1
-> Notes n2
-> Notes ('TOr n1 n2)
forall (t :: T) (xs :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes t -> Notes xs -> Notes ('TOr t xs)
NTOr TypeAnn
forall {k} (a :: k). Annotation a
noAnn FieldAnn
forall {k} (a :: k). Annotation a
noAnn FieldAnn
forall {k} (a :: k). Annotation a
noAnn (Sing n1 -> Notes n1
forall (t :: T). Sing t -> Notes t
starNotes' Sing n1
t) (Sing n2 -> Notes n2
forall (t :: T). Sing t -> Notes t
starNotes' Sing n2
t')
STLambda Sing n1
t Sing n2
t' -> TypeAnn -> Notes n1 -> Notes n2 -> Notes ('TLambda n1 n2)
forall (t :: T) (xs :: T).
TypeAnn -> Notes t -> Notes xs -> Notes ('TLambda t xs)
NTLambda TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Sing n1 -> Notes n1
forall (t :: T). Sing t -> Notes t
starNotes' Sing n1
t) (Sing n2 -> Notes n2
forall (t :: T). Sing t -> Notes t
starNotes' Sing n2
t')
Sing t
SingT t
STChest -> TypeAnn -> Notes 'TChest
NTChest TypeAnn
forall {k} (a :: k). Annotation a
noAnn
Sing t
SingT t
STChestKey -> TypeAnn -> Notes 'TChestKey
NTChestKey TypeAnn
forall {k} (a :: k). Annotation a
noAnn
isStar :: SingI t => Notes t -> Bool
isStar :: forall (t :: T). SingI t => Notes t -> Bool
isStar = (Notes t -> Notes t -> Bool
forall a. Eq a => a -> a -> Bool
== Notes t
forall (t :: T). SingI t => Notes t
starNotes)
insertTypeAnn :: forall (b :: T). TypeAnn -> Notes b -> Notes b
insertTypeAnn :: forall (b :: T). TypeAnn -> Notes b -> Notes b
insertTypeAnn TypeAnn
nt Notes b
s = case Notes b
s of
NTInt TypeAnn
_ -> TypeAnn -> Notes 'TInt
NTInt TypeAnn
nt
NTNat TypeAnn
_ -> TypeAnn -> Notes 'TNat
NTNat TypeAnn
nt
NTString TypeAnn
_ -> TypeAnn -> Notes 'TString
NTString TypeAnn
nt
NTBytes TypeAnn
_ -> TypeAnn -> Notes 'TBytes
NTBytes TypeAnn
nt
NTMutez TypeAnn
_ -> TypeAnn -> Notes 'TMutez
NTMutez TypeAnn
nt
NTBool TypeAnn
_ -> TypeAnn -> Notes 'TBool
NTBool TypeAnn
nt
NTKeyHash TypeAnn
_ -> TypeAnn -> Notes 'TKeyHash
NTKeyHash TypeAnn
nt
NTBls12381Fr TypeAnn
_ -> TypeAnn -> Notes 'TBls12381Fr
NTBls12381Fr TypeAnn
nt
NTBls12381G1 TypeAnn
_ -> TypeAnn -> Notes 'TBls12381G1
NTBls12381G1 TypeAnn
nt
NTBls12381G2 TypeAnn
_ -> TypeAnn -> Notes 'TBls12381G2
NTBls12381G2 TypeAnn
nt
NTTimestamp TypeAnn
_ -> TypeAnn -> Notes 'TTimestamp
NTTimestamp TypeAnn
nt
NTAddress TypeAnn
_ -> TypeAnn -> Notes 'TAddress
NTAddress TypeAnn
nt
NTKey TypeAnn
_ -> TypeAnn -> Notes 'TKey
NTKey TypeAnn
nt
NTUnit TypeAnn
_ -> TypeAnn -> Notes 'TUnit
NTUnit TypeAnn
nt
NTSignature TypeAnn
_ -> TypeAnn -> Notes 'TSignature
NTSignature TypeAnn
nt
NTOption TypeAnn
_ Notes t
n1 -> TypeAnn -> Notes t -> Notes ('TOption t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
nt Notes t
n1
NTList TypeAnn
_ Notes t
n1 -> TypeAnn -> Notes t -> Notes ('TList t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TList t)
NTList TypeAnn
nt Notes t
n1
NTSet TypeAnn
_ Notes t
n1 -> TypeAnn -> Notes t -> Notes ('TSet t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TSet t)
NTSet TypeAnn
nt Notes t
n1
NTOperation TypeAnn
_ -> TypeAnn -> Notes 'TOperation
NTOperation TypeAnn
nt
NTContract TypeAnn
_ Notes t
n1 -> TypeAnn -> Notes t -> Notes ('TContract t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TContract t)
NTContract TypeAnn
nt Notes t
n1
NTTicket TypeAnn
_ Notes t
n1 -> TypeAnn -> Notes t -> Notes ('TTicket t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TTicket t)
NTTicket TypeAnn
nt Notes t
n1
NTPair TypeAnn
_ FieldAnn
n1 FieldAnn
n2 VarAnn
n3 VarAnn
n4 Notes p
n5 Notes q
n6 -> TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes p
-> Notes q
-> Notes ('TPair p q)
forall (t :: T) (xs :: T).
TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes t
-> Notes xs
-> Notes ('TPair t xs)
NTPair TypeAnn
nt FieldAnn
n1 FieldAnn
n2 VarAnn
n3 VarAnn
n4 Notes p
n5 Notes q
n6
NTOr TypeAnn
_ FieldAnn
n1 FieldAnn
n2 Notes p
n3 Notes q
n4 -> TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q)
forall (t :: T) (xs :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes t -> Notes xs -> Notes ('TOr t xs)
NTOr TypeAnn
nt FieldAnn
n1 FieldAnn
n2 Notes p
n3 Notes q
n4
NTLambda TypeAnn
_ Notes p
n1 Notes q
n2 -> TypeAnn -> Notes p -> Notes q -> Notes ('TLambda p q)
forall (t :: T) (xs :: T).
TypeAnn -> Notes t -> Notes xs -> Notes ('TLambda t xs)
NTLambda TypeAnn
nt Notes p
n1 Notes q
n2
NTMap TypeAnn
_ Notes k
n1 Notes v
n2 -> TypeAnn -> Notes k -> Notes v -> Notes ('TMap k v)
forall (t :: T) (xs :: T).
TypeAnn -> Notes t -> Notes xs -> Notes ('TMap t xs)
NTMap TypeAnn
nt Notes k
n1 Notes v
n2
NTBigMap TypeAnn
_ Notes k
n1 Notes v
n2 -> TypeAnn -> Notes k -> Notes v -> Notes ('TBigMap k v)
forall (t :: T) (xs :: T).
TypeAnn -> Notes t -> Notes xs -> Notes ('TBigMap t xs)
NTBigMap TypeAnn
nt Notes k
n1 Notes v
n2
NTChainId TypeAnn
_ -> TypeAnn -> Notes 'TChainId
NTChainId TypeAnn
nt
NTChest TypeAnn
_ -> TypeAnn -> Notes 'TChest
NTChest TypeAnn
nt
NTChestKey TypeAnn
_ -> TypeAnn -> Notes 'TChestKey
NTChestKey TypeAnn
nt
NTTxRollupL2Address TypeAnn
_ -> TypeAnn -> Notes 'TTxRollupL2Address
NTTxRollupL2Address TypeAnn
nt
NTNever TypeAnn
_ -> TypeAnn -> Notes 'TNever
NTNever TypeAnn
nt
NTSaplingState TypeAnn
_ Sing n
n -> TypeAnn -> Sing n -> Notes ('TSaplingState n)
forall (t :: Peano). TypeAnn -> Sing t -> Notes ('TSaplingState t)
NTSaplingState TypeAnn
nt Sing n
n
NTSaplingTransaction TypeAnn
_ Sing n
n -> TypeAnn -> Sing n -> Notes ('TSaplingTransaction n)
forall (t :: Peano).
TypeAnn -> Sing t -> Notes ('TSaplingTransaction t)
NTSaplingTransaction TypeAnn
nt Sing n
n
data Anns xs where
AnnsCons :: Typeable tag => !(Annotation tag) -> Anns xs -> Anns (Annotation tag ': xs)
AnnsTyCons :: SingI t => !(Notes t) -> Anns xs -> Anns (Notes t ': xs)
AnnsNil :: Anns '[]
infixr 5 `AnnsCons`
infixr 5 `AnnsTyCons`
deriveGADTNFData ''Anns
deriving stock instance (Each '[Show] rs) => Show (Anns rs)
deriving stock instance (Eq r, Eq (Anns rs)) => Eq (Anns (r ': rs))
instance Eq (Anns '[]) where
Anns '[]
AnnsNil == :: Anns '[] -> Anns '[] -> Bool
== Anns '[]
AnnsNil = Bool
True
type AnnVar = Anns '[VarAnn]
instance Default (Anns '[]) where
def :: Anns '[]
def = Anns '[]
AnnsNil
instance (Typeable tag, Default (Anns xs)) => Default (Anns (Annotation tag ': xs)) where
def :: Anns (Annotation tag : xs)
def = Annotation tag
forall {k} (a :: k). Annotation a
noAnn Annotation tag -> Anns xs -> Anns (Annotation tag : xs)
forall {t} (xs :: t) (xs :: [*]).
Typeable xs =>
Annotation xs -> Anns xs -> Anns (Annotation xs : xs)
`AnnsCons` Anns xs
forall a. Default a => a
def
instance (SingI t, Default (Anns xs)) => Default (Anns (Notes t ': xs)) where
def :: Anns (Notes t : xs)
def = Notes t
forall (t :: T). SingI t => Notes t
starNotes Notes t -> Anns xs -> Anns (Notes t : xs)
forall (t :: T) (xs :: [*]).
SingI t =>
Notes t -> Anns xs -> Anns (Notes t : xs)
`AnnsTyCons` Anns xs
forall a. Default a => a
def
type family AnnotateInstrArg (xs :: [Type]) r where
AnnotateInstrArg (Notes _ ': xs) r = Un.Ty -> AnnotateInstrArg xs r
AnnotateInstrArg (x ': xs) r = x -> AnnotateInstrArg xs r
AnnotateInstrArg '[] r = r
class AnnotateInstr (xs :: [Type]) r where
annotateInstr :: Anns xs -> AnnotateInstrArg xs r -> r
instance AnnotateInstr '[] r where
annotateInstr :: Anns '[] -> AnnotateInstrArg '[] r -> r
annotateInstr (Anns '[]
AnnsNil) AnnotateInstrArg '[] r
c = r
AnnotateInstrArg '[] r
c
instance AnnotateInstr xs r => AnnotateInstr (Annotation tag ': xs) r where
annotateInstr :: Anns (Annotation tag : xs)
-> AnnotateInstrArg (Annotation tag : xs) r -> r
annotateInstr (AnnsCons Annotation tag
va Anns xs
xs) AnnotateInstrArg (Annotation tag : xs) r
c = forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr @_ @r Anns xs
xs (AnnotateInstrArg xs r -> r) -> AnnotateInstrArg xs r -> r
forall a b. (a -> b) -> a -> b
$ AnnotateInstrArg (Annotation tag : xs) r
Annotation tag -> AnnotateInstrArg xs r
c Annotation tag
va
instance AnnotateInstr xs r => AnnotateInstr (Notes t ': xs) r where
annotateInstr :: Anns (Notes t : xs) -> AnnotateInstrArg (Notes t : xs) r -> r
annotateInstr (AnnsTyCons Notes t
va Anns xs
xs) AnnotateInstrArg (Notes t : xs) r
c = forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr @_ @r Anns xs
xs (AnnotateInstrArg xs r -> r) -> AnnotateInstrArg xs r -> r
forall a b. (a -> b) -> a -> b
$ AnnotateInstrArg (Notes t : xs) r
Ty -> AnnotateInstrArg xs r
c (Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes t
va)
pattern Anns1 :: Typeable a => Annotation a -> Anns '[Annotation a]
pattern $bAnns1 :: forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
$mAnns1 :: forall {r} {k} {a :: k}.
Typeable a =>
Anns '[Annotation a] -> (Annotation a -> r) -> (Void# -> r) -> r
Anns1 x = x `AnnsCons` AnnsNil
pattern Anns2
:: Each '[Typeable] '[a, b]
=> Annotation a
-> Annotation b
-> Anns '[Annotation a, Annotation b]
pattern $bAnns2 :: forall {k} (a :: k) (b :: k).
Each '[Typeable] '[a, b] =>
Annotation a -> Annotation b -> Anns '[Annotation a, Annotation b]
$mAnns2 :: forall {r} {k} {a :: k} {b :: k}.
Each '[Typeable] '[a, b] =>
Anns '[Annotation a, Annotation b]
-> (Annotation a -> Annotation b -> r) -> (Void# -> r) -> r
Anns2 x y = x `AnnsCons` y `AnnsCons` AnnsNil
pattern Anns2' :: (Typeable a, SingI t) => Annotation a -> Notes t -> Anns '[Annotation a, Notes t]
pattern $bAnns2' :: forall {k} (a :: k) (t :: T).
(Typeable a, SingI t) =>
Annotation a -> Notes t -> Anns '[Annotation a, Notes t]
$mAnns2' :: forall {r} {k} {a :: k} {t :: T}.
(Typeable a, SingI t) =>
Anns '[Annotation a, Notes t]
-> (Annotation a -> Notes t -> r) -> (Void# -> r) -> r
Anns2' x y = x `AnnsCons` y `AnnsTyCons` AnnsNil
pattern Anns3
:: Each '[Typeable] '[a, b, c]
=> Annotation a
-> Annotation b
-> Annotation c
-> Anns '[Annotation a, Annotation b, Annotation c]
pattern $bAnns3 :: forall {k} (a :: k) (b :: k) (c :: k).
Each '[Typeable] '[a, b, c] =>
Annotation a
-> Annotation b
-> Annotation c
-> Anns '[Annotation a, Annotation b, Annotation c]
$mAnns3 :: forall {r} {k} {a :: k} {b :: k} {c :: k}.
Each '[Typeable] '[a, b, c] =>
Anns '[Annotation a, Annotation b, Annotation c]
-> (Annotation a -> Annotation b -> Annotation c -> r)
-> (Void# -> r)
-> r
Anns3 x y z = x `AnnsCons` y `AnnsCons` z `AnnsCons` AnnsNil
pattern Anns3'
:: (Each '[Typeable] '[a, b], SingI t)
=> Annotation a
-> Annotation b
-> Notes t
-> Anns '[Annotation a, Annotation b, Notes t]
pattern $bAnns3' :: forall {k} (a :: k) (b :: k) (t :: T).
(Each '[Typeable] '[a, b], SingI t) =>
Annotation a
-> Annotation b
-> Notes t
-> Anns '[Annotation a, Annotation b, Notes t]
$mAnns3' :: forall {r} {k} {a :: k} {b :: k} {t :: T}.
(Each '[Typeable] '[a, b], SingI t) =>
Anns '[Annotation a, Annotation b, Notes t]
-> (Annotation a -> Annotation b -> Notes t -> r)
-> (Void# -> r)
-> r
Anns3' x y z = x `AnnsCons` y `AnnsCons` z `AnnsTyCons` AnnsNil
pattern Anns3''
:: (Typeable a, SingI t, SingI u)
=> Annotation a
-> Notes t
-> Notes u
-> Anns '[Annotation a, Notes t, Notes u]
pattern $bAnns3'' :: forall {k} (a :: k) (t :: T) (u :: T).
(Typeable a, SingI t, SingI u) =>
Annotation a
-> Notes t -> Notes u -> Anns '[Annotation a, Notes t, Notes u]
$mAnns3'' :: forall {r} {k} {a :: k} {t :: T} {u :: T}.
(Typeable a, SingI t, SingI u) =>
Anns '[Annotation a, Notes t, Notes u]
-> (Annotation a -> Notes t -> Notes u -> r) -> (Void# -> r) -> r
Anns3'' x y z = x `AnnsCons` y `AnnsTyCons` z `AnnsTyCons` AnnsNil
pattern Anns4
:: Each '[Typeable] '[a, b, c, d]
=> Annotation a
-> Annotation b
-> Annotation c
-> Annotation d
-> Anns '[Annotation a, Annotation b, Annotation c, Annotation d]
pattern $bAnns4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
Each '[Typeable] '[a, b, c, d] =>
Annotation a
-> Annotation b
-> Annotation c
-> Annotation d
-> Anns '[Annotation a, Annotation b, Annotation c, Annotation d]
$mAnns4 :: forall {r} {k} {a :: k} {b :: k} {c :: k} {d :: k}.
Each '[Typeable] '[a, b, c, d] =>
Anns '[Annotation a, Annotation b, Annotation c, Annotation d]
-> (Annotation a
-> Annotation b -> Annotation c -> Annotation d -> r)
-> (Void# -> r)
-> r
Anns4 x y z w = x `AnnsCons` y `AnnsCons` z `AnnsCons` w `AnnsCons` AnnsNil
pattern Anns4''
:: (Each '[Typeable] '[a, b], SingI t, SingI u)
=> Annotation a
-> Annotation b
-> Notes t
-> Notes u
-> Anns '[Annotation a, Annotation b, Notes t, Notes u]
pattern $bAnns4'' :: forall {k} (a :: k) (b :: k) (t :: T) (u :: T).
(Each '[Typeable] '[a, b], SingI t, SingI u) =>
Annotation a
-> Annotation b
-> Notes t
-> Notes u
-> Anns '[Annotation a, Annotation b, Notes t, Notes u]
$mAnns4'' :: forall {r} {k} {a :: k} {b :: k} {t :: T} {u :: T}.
(Each '[Typeable] '[a, b], SingI t, SingI u) =>
Anns '[Annotation a, Annotation b, Notes t, Notes u]
-> (Annotation a -> Annotation b -> Notes t -> Notes u -> r)
-> (Void# -> r)
-> r
Anns4'' x y z w
= x `AnnsCons` y `AnnsCons` z `AnnsTyCons` w `AnnsTyCons` AnnsNil
pattern Anns5'
:: (Each '[Typeable] '[a, b, c, d], SingI t)
=> Annotation a
-> Annotation b
-> Annotation c
-> Annotation d
-> Notes t
-> Anns '[Annotation a, Annotation b, Annotation c, Annotation d, Notes t]
pattern $bAnns5' :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (t :: T).
(Each '[Typeable] '[a, b, c, d], SingI t) =>
Annotation a
-> Annotation b
-> Annotation c
-> Annotation d
-> Notes t
-> Anns
'[Annotation a, Annotation b, Annotation c, Annotation d, Notes t]
$mAnns5' :: forall {r} {k} {a :: k} {b :: k} {c :: k} {d :: k} {t :: T}.
(Each '[Typeable] '[a, b, c, d], SingI t) =>
Anns
'[Annotation a, Annotation b, Annotation c, Annotation d, Notes t]
-> (Annotation a
-> Annotation b -> Annotation c -> Annotation d -> Notes t -> r)
-> (Void# -> r)
-> r
Anns5' x y z v w
= x `AnnsCons` y `AnnsCons` z `AnnsCons` v `AnnsCons` w `AnnsTyCons` AnnsNil
{-# COMPLETE Anns1 #-}
{-# COMPLETE Anns2 #-}
{-# COMPLETE Anns2' #-}
{-# COMPLETE Anns3 #-}
{-# COMPLETE Anns3' #-}
{-# COMPLETE Anns3'' #-}
{-# COMPLETE Anns4 #-}
{-# COMPLETE Anns4'' #-}
{-# COMPLETE Anns5' #-}