Morley.Michelson.Typed.Annotation

Module, providing Notes t data type, which holds annotations for a given type t.

Annotation type Notes t is a tree, each leaf is either a star (*) or a constructor holding some annotation data for a given type t. Star corresponds to the case when given Michelson type contains no annotations.

This module also provides some utility functions which are used to combine two annotations trees a and b into a new one c in such a way that c can be obtained from both a and b by replacing some * leaves with type or/and field annotations.

Documentation

data Notes t where

Data type, holding annotation data for a given Michelson type t.

Each constructor corresponds to exactly one constructor of T and holds all type and field annotations that can be attributed to a Michelson type corresponding to t.

Constructors

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

NTSaplingState :: forall (n :: Peano). TypeAnn -> Sing n -> Notes ('TSaplingState n)

NTSaplingTransaction :: forall (n :: Peano). TypeAnn -> Sing n -> Notes ('TSaplingTransaction n)

Instances

Lift (Notes t :: Type)

Defined in Morley.Michelson.Typed.Annotation

Methods

lift :: Notes t -> Q Exp

liftTyped :: Notes t -> Q (TExp (Notes t))

Eq (Notes t)

Defined in Morley.Michelson.Typed.Annotation

Methods

(==) :: Notes t -> Notes t -> Bool

(/=) :: Notes t -> Notes t -> Bool

Show (Notes t)

Defined in Morley.Michelson.Typed.Annotation

Methods

showsPrec :: Int -> Notes t -> ShowS

show :: Notes t -> String

showList :: [Notes t] -> ShowS

NFData (Notes t)

Defined in Morley.Michelson.Typed.Annotation

Methods

rnf :: Notes t -> ()

Buildable (Notes t)

Defined in Morley.Michelson.Typed.Annotation

Methods

build :: Notes t -> Builder

RenderDoc (Notes t)

Defined in Morley.Michelson.Typed.Annotation

Methods

renderDoc :: RenderContext -> Notes t -> Doc

isRenderable :: Notes t -> Bool

ToExpression (Notes t)

Defined in Morley.Micheline.Class

Methods

toExpression :: Notes t -> Expression

data AnnConvergeError where

Constructors

AnnConvergeError :: forall (tag :: Type). (Buildable (Annotation tag), Show (Annotation tag), Typeable tag) => Annotation tag -> Annotation tag -> AnnConvergeError

Instances

Eq AnnConvergeError

Defined in Morley.Michelson.Typed.Annotation

Methods

(==) :: AnnConvergeError -> AnnConvergeError -> Bool

(/=) :: AnnConvergeError -> AnnConvergeError -> Bool

Show AnnConvergeError

Defined in Morley.Michelson.Typed.Annotation

Methods

showsPrec :: Int -> AnnConvergeError -> ShowS

show :: AnnConvergeError -> String

showList :: [AnnConvergeError] -> ShowS

NFData AnnConvergeError

Defined in Morley.Michelson.Typed.Annotation

Methods

rnf :: AnnConvergeError -> ()

Buildable AnnConvergeError

Defined in Morley.Michelson.Typed.Annotation

Methods

build :: AnnConvergeError -> Builder

converge :: Notes t -> Notes t -> Either AnnConvergeError (Notes t)

Combines two annotations trees a and b into a new one c in such a way that c can be obtained from both a and b by replacing some empty leaves with type or/and field annotations.

convergeAnns :: forall (tag :: Type). (Buildable (Annotation tag), Show (Annotation tag), Typeable tag) => Annotation tag -> Annotation tag -> Either AnnConvergeError (Annotation tag)

Converge two type or field notes (which may be wildcards).

convergeDestrAnns :: FieldAnn -> FieldAnn -> Either AnnConvergeError FieldAnn

Converge two field notes in CAR, CDR or UNPAIR, given that one of them may be a special annotation.

insertTypeAnn :: forall (b :: T). TypeAnn -> Notes b -> Notes b

Insert the provided type annotation into the provided notes.

isStar :: SingI t => Notes t -> Bool

Checks if no annotations are present.

starNotes :: forall t. SingI t => Notes t

In memory of NStar constructor. Generates notes with no annotations.

mkUType :: Notes x -> Ty

Get the term-level type of notes, preserving annotations.

notesSing :: Notes t -> Sing t

Forget information about annotations, pick singleton with the same type.

notesT :: Notes t -> T

Get term-level type of notes.