Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- withDict :: HasDict c e => e -> (c => r) -> r
- data Dict a where
- newtype a :- b = Sub (a => Dict b)
- class SingI (a :: k) where
- type Path = [Branch]
- data Branch
- data Constrained c f where
- pattern SomePackedVal :: () => PackedValScope t => Value t -> SomePackedVal
- pattern SomeConstant :: () => ConstantScope t => Value t -> SomeConstant
- pattern SomeConstrainedValue :: forall c. () => forall a. c a => Value a -> SomeConstrainedValue c
- pattern SomeStorage :: () => StorageScope t => Value t -> SomeStorage
- pattern SomeValue :: () => SingI t => Value t -> SomeValue
- ligoLayout :: GenericStrategy
- ligoCombLayout :: GenericStrategy
- data T
- = TKey
- | TUnit
- | TSignature
- | TChainId
- | TOption T
- | TList T
- | TSet T
- | TOperation
- | TContract T
- | TTicket T
- | TPair T T
- | TOr T T
- | TLambda T T
- | TMap T T
- | TBigMap T T
- | TInt
- | TNat
- | TString
- | TBytes
- | TMutez
- | TBool
- | TKeyHash
- | TBls12381Fr
- | TBls12381G1
- | TBls12381G2
- | TTimestamp
- | TAddress
- | TChest
- | TChestKey
- | TSaplingState Peano
- | TSaplingTransaction Peano
- | TNever
- toUType :: T -> Ty
- buildStack :: [T] -> Doc
- data SingT :: T -> Type where
- STKey :: SingT ('TKey :: T)
- STUnit :: SingT ('TUnit :: T)
- STSignature :: SingT ('TSignature :: T)
- STChainId :: SingT ('TChainId :: T)
- STOption :: forall (n :: T). (Sing n) -> SingT ('TOption n :: T)
- STList :: forall (n :: T). (Sing n) -> SingT ('TList n :: T)
- STSet :: forall (n :: T). (Sing n) -> SingT ('TSet n :: T)
- STOperation :: SingT ('TOperation :: T)
- STContract :: forall (n :: T). (Sing n) -> SingT ('TContract n :: T)
- STTicket :: forall (n :: T). (Sing n) -> SingT ('TTicket n :: T)
- STPair :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TPair n n :: T)
- STOr :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TOr n n :: T)
- STLambda :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TLambda n n :: T)
- STMap :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TMap n n :: T)
- STBigMap :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TBigMap n n :: T)
- STInt :: SingT ('TInt :: T)
- STNat :: SingT ('TNat :: T)
- STString :: SingT ('TString :: T)
- STBytes :: SingT ('TBytes :: T)
- STMutez :: SingT ('TMutez :: T)
- STBool :: SingT ('TBool :: T)
- STKeyHash :: SingT ('TKeyHash :: T)
- STBls12381Fr :: SingT ('TBls12381Fr :: T)
- STBls12381G1 :: SingT ('TBls12381G1 :: T)
- STBls12381G2 :: SingT ('TBls12381G2 :: T)
- STTimestamp :: SingT ('TTimestamp :: T)
- STAddress :: SingT ('TAddress :: T)
- STChest :: SingT ('TChest :: T)
- STChestKey :: SingT ('TChestKey :: T)
- STSaplingState :: forall (n :: Nat). (Sing n) -> SingT ('TSaplingState n :: T)
- STSaplingTransaction :: forall (n :: Nat). (Sing n) -> SingT ('TSaplingTransaction n :: T)
- STNever :: SingT ('TNever :: T)
- castSingE :: forall (a :: T) (b :: T) t. (SingI a, SingI b) => t a -> Either Text (t b)
- castM :: forall (a :: T) (b :: T) t m. (SingI a, SingI b, Monad m) => t a -> (forall x. MismatchError T -> m x) -> m (t b)
- requireEq :: forall (a :: T) (b :: T) m. (SingI a, SingI b, Monad m) => (forall x. MismatchError T -> m x) -> m (a :~: b)
- eqP :: forall (a :: T) (b :: T). (SingI a, SingI b) => Proxy a -> Proxy b -> Maybe (a :~: b)
- data TPredicateSym
- type ForbidNonComparable = ForbidT 'PSNonComparable
- type ForbidNestedBigMaps = ForbidT 'PSNestedBigMaps
- type ForbidBigMap = ForbidT 'PSBigMap
- type ForbidTicket = ForbidT 'PSTicket
- type ForbidContract = ForbidT 'PSContract
- type ForbidOp = ForbidT 'PSOp
- class ForbidManyT (ForbidT p t) '[p] t => ForbidT p t
- type family ContainsT p t where ...
- data SingTPredicateSym :: TPredicateSym -> Type where
- SPSOp :: SingTPredicateSym ('PSOp :: TPredicateSym)
- SPSContract :: SingTPredicateSym ('PSContract :: TPredicateSym)
- SPSTicket :: SingTPredicateSym ('PSTicket :: TPredicateSym)
- SPSBigMap :: SingTPredicateSym ('PSBigMap :: TPredicateSym)
- SPSNestedBigMaps :: SingTPredicateSym ('PSNestedBigMaps :: TPredicateSym)
- SPSSaplingState :: SingTPredicateSym ('PSSaplingState :: TPredicateSym)
- SPSNonComparable :: SingTPredicateSym ('PSNonComparable :: TPredicateSym)
- data TPresence p t where
- TPresent :: ContainsT p t ~ 'True => TPresence p t
- TAbsent :: ContainsT p t ~ 'False => TPresence p t
- pattern SaplingStateAbsent :: () => ContainsSaplingState t ~ 'False => SaplingStatePresence t
- pattern SaplingStatePresent :: () => ContainsSaplingState t ~ 'True => SaplingStatePresence t
- pattern NestedBigMapsAbsent :: () => ContainsNestedBigMaps t ~ 'False => NestedBigMapsPresence t
- pattern NestedBigMapsPresent :: () => ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresence t
- pattern BigMapAbsent :: () => ContainsBigMap t ~ 'False => BigMapPresence t
- pattern BigMapPresent :: () => ContainsBigMap t ~ 'True => BigMapPresence t
- pattern TicketAbsent :: () => ContainsTicket t ~ 'False => TicketPresence t
- pattern TicketPresent :: () => ContainsTicket t ~ 'True => TicketPresence t
- pattern ContractAbsent :: () => ContainsContract t ~ 'False => ContractPresence t
- pattern ContractPresent :: () => ContainsContract t ~ 'True => ContractPresence t
- pattern OpPresent :: () => ContainsOp t ~ 'True => OpPresence t
- pattern OpAbsent :: () => ContainsOp t ~ 'False => OpPresence t
- checkTPresence :: forall p ty. Sing p -> Sing ty -> TPresence p ty
- tPresence :: Sing p -> Sing t -> Maybe (ContainsT p t :~: 'True)
- tAbsence :: Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
- class (SingI t, RecSuperC Comparable t, ForbidNonComparable t) => Comparable t
- data Comparability t where
- CanBeCompared :: (Comparable t, ComparabilityImplies t) => Comparability t
- CannotBeCompared :: ContainsT 'PSNonComparable t ~ 'True => Comparability t
- comparableImplies :: forall t proxy. ForbidNonComparable t => proxy t -> Dict (ComparabilityImplies t)
- checkComparability :: Sing t -> Comparability t
- comparabilityPresence :: Sing t -> Maybe (Dict (Comparable t))
- data NotWellTyped = NotWellTyped {}
- class (SingI t, RecSuperC WellTyped t, WellTypedConstraints t) => WellTyped t
- data BadTypeForScope
- getWTP :: forall t. SingI t => Either NotWellTyped (Dict (WellTyped t))
- getWTP' :: Sing t -> Either NotWellTyped (Dict (WellTyped t))
- class ComparabilityScopeC (ComparabilityScope t) t => ComparabilityScope t
- class UntypedValScopeC (UntypedValScope t) t => UntypedValScope t
- class ViewableScopeC (ViewableScope t) t => ViewableScope t
- class UnpackedValScopeC (UnpackedValScope t) t => UnpackedValScope t
- class PackedValScopeC (PackedValScope t) t => PackedValScope t
- type family IsDupableScope (t :: T) :: Bool where ...
- class DupableScopeC (DupableScope t) t => DupableScope t
- class ConstantScopeC (ConstantScope t) t => ConstantScope t
- class StorageScopeC (StorageScope t) t => StorageScope t
- class ParameterScopeC (ParameterScope t) t => ParameterScope t
- class WithDeMorganScope (c :: T -> Constraint) t a b where
- withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret
- deMorganForbidT :: forall a b r p. (ContainsT p a || ContainsT p b) ~ 'False => Sing p -> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
- type IsComparable t = Not (ContainsT 'PSNonComparable t)
- type ProperNonComparableValBetterErrors t = (SingI t, ForbidNonComparable t)
- type ProperUntypedValBetterErrors t = (SingI t, ForbidOp t)
- type ProperViewableBetterErrors t = (SingI t, ForbidOp t, ForbidBigMap t, ForbidTicket t)
- type ProperUnpackedValBetterErrors t = (ProperPackedValBetterErrors t, ProperConstantBetterErrors t)
- type ProperPackedValBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidTicket t, ForbidSaplingState t)
- type ProperDupableBetterErrors t = (SingI t, ForbidTicket t)
- type ProperConstantBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidContract t, ForbidTicket t, ForbidSaplingState t)
- type ProperStorageBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t)
- type ProperParameterBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t)
- type NestedBigMapsPresence (t :: T) = TPresence 'PSNestedBigMaps t
- type BigMapPresence (t :: T) = TPresence 'PSBigMap t
- type TicketPresence (t :: T) = TPresence 'PSTicket t
- type ContractPresence (t :: T) = TPresence 'PSContract t
- type OpPresence (t :: T) = TPresence 'PSOp t
- class ContainsNestedBigMaps t ~ 'False => HasNoNestedBigMaps t
- class ContainsBigMap t ~ 'False => HasNoBigMap t
- class ContainsTicket t ~ 'False => HasNoTicket t
- class ContainsContract t ~ 'False => HasNoContract t
- class ContainsOp t ~ 'False => HasNoOp t
- type ContainsNestedBigMaps t = ContainsT 'PSNestedBigMaps t
- type ContainsBigMap t = ContainsT 'PSBigMap t
- type ContainsTicket t = ContainsT 'PSTicket t
- type ContainsContract t = ContainsT 'PSContract t
- type ContainsOp t = ContainsT 'PSOp t
- checkOpPresence :: Sing (ty :: T) -> TPresence 'PSOp ty
- checkContractTypePresence :: Sing (ty :: T) -> TPresence 'PSContract ty
- checkTicketPresence :: Sing (ty :: T) -> TPresence 'PSTicket ty
- checkBigMapPresence :: Sing (ty :: T) -> TPresence 'PSBigMap ty
- checkNestedBigMapsPresence :: Sing (ty :: T) -> TPresence 'PSNestedBigMaps ty
- opAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidOp t)
- contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidContract t)
- bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidBigMap t)
- nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidNestedBigMaps t)
- comparabilityImpliesNoNestedBigMaps :: forall t. (SingI t, IsComparable t ~ 'True) => ContainsNestedBigMaps t :~: 'False
- comparabilityImpliesNoOp :: forall t. (SingI t, IsComparable t ~ 'True) => ContainsOp t :~: 'False
- getComparableProofS :: Sing (a :: T) -> Maybe (Dict (Comparable a))
- class CheckScope (c :: Constraint) where
- checkScope :: Either BadTypeForScope (Dict c)
- type FieldDescriptions = [(Symbol, (Maybe Symbol, [(Symbol, Symbol)]))]
- newtype EpName = UnsafeEpName {}
- data HandleImplicitDefaultEp
- data EpNameFromRefAnnError = InEpNameBadAnnotation FieldAnn
- pattern DefEpName :: EpName
- epNameFromParamAnn :: FieldAnn -> Maybe EpName
- epNameToParamAnn :: EpName -> FieldAnn
- epNameFromRefAnn :: FieldAnn -> Either EpNameFromRefAnnError EpName
- epNameToRefAnn :: EpName -> FieldAnn
- newtype ViewName where
- UnsafeViewName {
- unViewName :: Text
- pattern ViewName :: Text -> ViewName
- UnsafeViewName {
- data BadViewNameError
- mkViewName :: Text -> Either BadViewNameError ViewName
- viewNameToMText :: ViewName -> MText
- data ViewsSetError = DuplicatedViewName ViewName
- 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
- NTSaplingState :: forall (n :: Peano). TypeAnn -> Sing n -> Notes ('TSaplingState n)
- NTSaplingTransaction :: forall (n :: Peano). TypeAnn -> Sing n -> Notes ('TSaplingTransaction 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 '[]
- 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 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 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 Anns3'' :: (Typeable a, SingI t, SingI u) => Annotation a -> Notes t -> Notes u -> Anns '[Annotation a, Notes t, Notes u]
- pattern Anns3' :: (Each '[Typeable] '[a, b], SingI t) => Annotation a -> Annotation b -> Notes t -> Anns '[Annotation a, Annotation b, Notes t]
- pattern Anns3 :: Each '[Typeable] '[a, b, c] => Annotation a -> Annotation b -> Annotation c -> Anns '[Annotation a, Annotation b, Annotation c]
- pattern Anns2' :: (Typeable a, SingI t) => Annotation a -> Notes t -> Anns '[Annotation a, Notes t]
- pattern Anns1 :: Typeable a => Annotation a -> Anns '[Annotation a]
- pattern Anns2 :: Each '[Typeable] '[a, b] => Annotation a -> Annotation b -> Anns '[Annotation a, Annotation b]
- notesSing :: Notes t -> Sing t
- notesT :: Notes t -> T
- mkUType :: Notes x -> Ty
- starNotes :: forall t. SingI t => Notes t
- isStar :: SingI t => Notes t -> Bool
- insertTypeAnn :: forall (b :: T). TypeAnn -> Notes b -> Notes b
- class AnnotateInstr (xs :: [Type]) r where
- annotateInstr :: Anns xs -> AnnotateInstrArg xs r -> r
- type AnnVar = Anns '[VarAnn]
- pattern AsUTypeExt :: () => SingI t => Sing t -> Notes t -> Ty
- pattern AsUType :: () => SingI t => Notes t -> Ty
- fromUType :: Ty -> T
- withUType :: Ty -> (forall t. SingI t => Notes t -> r) -> r
- data SomeViewsSet' instr where
- SomeViewsSet :: SingI st => ViewsSet' instr st -> SomeViewsSet' instr
- newtype ViewsSet' instr st where
- data SomeView' instr st where
- data View' instr arg st ret = (ViewableScope arg, SingI st, ViewableScope ret) => View {}
- type ViewCode' instr arg st ret = instr '['TPair arg st] '[ret]
- someViewName :: SomeView' instr st -> ViewName
- mkViewsSet :: [SomeView' instr st] -> Either ViewsSetError (ViewsSet' instr st)
- emptyViewsSet :: forall instr st. ViewsSet' instr st
- addViewToSet :: View' instr arg st ret -> ViewsSet' instr st -> Either ViewsSetError (ViewsSet' instr st)
- lookupView :: forall instr st. ViewName -> ViewsSet' instr st -> Maybe (SomeView' instr st)
- viewsSetNames :: forall instr st. ViewsSet' instr st -> Set ViewName
- data EpLiftSequence (arg :: T) (param :: T) where
- EplArgHere :: EpLiftSequence arg arg
- EplWrapLeft :: (SingI subparam, SingI r) => EpLiftSequence arg subparam -> EpLiftSequence arg ('TOr subparam r)
- EplWrapRight :: (SingI l, SingI subparam) => EpLiftSequence arg subparam -> EpLiftSequence arg ('TOr l subparam)
- data ParamEpError
- data ArmCoord
- type ArmCoords = [ArmCoord]
- data ParamNotes (t :: T) = UnsafeParamNotes {}
- data ParseEpAddressError
- data EpAddress where
- EpAddress' { }
- pattern EpAddress :: KindedAddress kind -> EpName -> EpAddress
- pattern ParamNotes :: Notes t -> RootAnn -> ParamNotes t
- formatEpAddress :: EpAddress -> Text
- mformatEpAddress :: EpAddress -> MText
- parseEpAddress :: Text -> Either ParseEpAddressError EpAddress
- parseEpAddressRaw :: ByteString -> Either ParseEpAddressError EpAddress
- starParamNotes :: SingI t => ParamNotes t
- mkParamNotes :: Notes t -> RootAnn -> Either ParamEpError (ParamNotes t)
- data MkEntrypointCallRes param where
- MkEntrypointCallRes :: ParameterScope arg => Notes arg -> EntrypointCallT param arg -> MkEntrypointCallRes param
- data SomeEntrypointCallT (arg :: T) = forall param.ParameterScope param => SomeEpc (EntrypointCallT param arg)
- type family ForbidOr (t :: T) :: Constraint where ...
- data EntrypointCallT (param :: T) (arg :: T) = ParameterScope arg => EntrypointCall {
- epcName :: EpName
- epcParamProxy :: Proxy param
- epcLiftSequence :: EpLiftSequence arg param
- unsafeEpcCallRoot :: ParameterScope param => EntrypointCallT param param
- epcPrimitive :: forall p. (ParameterScope p, ForbidOr p) => EntrypointCallT p p
- unsafeSepcCallRoot :: ParameterScope param => SomeEntrypointCallT param
- sepcPrimitive :: forall t. (ParameterScope t, ForbidOr t) => SomeEntrypointCallT t
- sepcName :: SomeEntrypointCallT arg -> EpName
- mkEntrypointCall :: ParameterScope param => EpName -> ParamNotes param -> Maybe (MkEntrypointCallRes param)
- mkDefEntrypointCall :: ParameterScope param => ParamNotes param -> MkEntrypointCallRes param
- tyImplicitAccountParam :: ParamNotes 'TUnit
- data Contract' instr cp st = (ParameterScope cp, StorageScope st) => Contract {
- cCode :: ContractCode' instr cp st
- cParamNotes :: ParamNotes cp
- cStoreNotes :: Notes st
- cViews :: ViewsSet' instr st
- cEntriesOrder :: EntriesOrder
- class IsNotInView
- newtype ContractCode' instr cp st = ContractCode {
- unContractCode :: instr (ContractInp cp st) (ContractOut st)
- type ContractOut st = '[ContractOut1 st]
- type ContractOut1 st = 'TPair ('TList 'TOperation) st
- type ContractInp param st = '[ContractInp1 param st]
- type ContractInp1 param st = 'TPair param st
- mkContractCode :: (IsNotInView => instr (ContractInp cp st) (ContractOut st)) -> ContractCode' instr cp st
- defaultContract :: (ParameterScope cp, StorageScope st) => (IsNotInView => instr (ContractInp cp st) (ContractOut st)) -> Contract' instr cp st
- mapContractCodeBlock :: (instr (ContractInp cp st) (ContractOut st) -> instr (ContractInp cp st) (ContractOut st)) -> Contract' instr cp st -> Contract' instr cp st
- mapContractCodeBlockM :: Monad m => (instr (ContractInp cp st) (ContractOut st) -> m (instr (ContractInp cp st) (ContractOut st))) -> Contract' instr cp st -> m (Contract' instr cp st)
- mapContractViewBlocks :: (forall arg ret. ViewCode' instr arg st ret -> ViewCode' instr arg st ret) -> Contract' instr cp st -> Contract' instr cp st
- mapContractViewBlocksM :: Monad m => (forall arg ret. ViewCode' instr arg st ret -> m (ViewCode' instr arg st ret)) -> Contract' instr cp st -> m (Contract' instr cp st)
- mapContractCode :: (forall i o. instr i o -> instr i o) -> Contract' instr cp st -> Contract' instr cp st
- mapContractCodeM :: Monad m => (forall i o. instr i o -> m (instr i o)) -> Contract' instr cp st -> m (Contract' instr cp st)
- data LambdaCode' instr inp out where
- LambdaCode :: (forall i o. Show (instr i o), forall i o. Eq (instr i o), forall i o. NFData (instr i o)) => RemFail instr (inp ': '[]) (out ': '[]) -> LambdaCode' instr inp out
- LambdaCodeRec :: (forall i o. Show (instr i o), forall i o. Eq (instr i o), forall i o. NFData (instr i o)) => RemFail instr (inp ': ('TLambda inp out ': '[])) (out ': '[]) -> LambdaCode' instr inp out
- data Value' instr t where
- VKey :: PublicKey -> Value' instr 'TKey
- VUnit :: Value' instr 'TUnit
- VSignature :: Signature -> Value' instr 'TSignature
- VChainId :: ChainId -> Value' instr 'TChainId
- VOption :: forall t instr. SingI t => Maybe (Value' instr t) -> Value' instr ('TOption t)
- VList :: forall t instr. SingI t => [Value' instr t] -> Value' instr ('TList t)
- VSet :: forall t instr. Comparable t => Set (Value' instr t) -> Value' instr ('TSet t)
- VOp :: Operation' instr -> Value' instr 'TOperation
- VContract :: forall arg instr. (SingI arg, ForbidOp arg) => Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
- VTicket :: forall arg instr. Comparable arg => Address -> Value' instr arg -> Natural -> Value' instr ('TTicket arg)
- VPair :: forall l r instr. (Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
- VOr :: forall l r instr. (SingI l, SingI r) => Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
- VLam :: forall inp out instr. (SingI inp, SingI out) => LambdaCode' instr inp out -> Value' instr ('TLambda inp out)
- VMap :: forall k v instr. (SingI v, Comparable k) => Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
- VBigMap :: forall k v instr. (SingI v, Comparable k, ForbidBigMap v) => Maybe Natural -> Map (Value' instr k) (Value' instr v) -> Value' instr ('TBigMap k v)
- VInt :: Integer -> Value' instr 'TInt
- VNat :: Natural -> Value' instr 'TNat
- VString :: MText -> Value' instr 'TString
- VBytes :: ByteString -> Value' instr 'TBytes
- VMutez :: Mutez -> Value' instr 'TMutez
- VBool :: Bool -> Value' instr 'TBool
- VKeyHash :: KeyHash -> Value' instr 'TKeyHash
- VTimestamp :: Timestamp -> Value' instr 'TTimestamp
- VAddress :: EpAddress -> Value' instr 'TAddress
- VBls12381Fr :: Bls12381Fr -> Value' instr 'TBls12381Fr
- VBls12381G1 :: Bls12381G1 -> Value' instr 'TBls12381G1
- VBls12381G2 :: Bls12381G2 -> Value' instr 'TBls12381G2
- VChest :: Chest -> Value' instr 'TChest
- VChestKey :: ChestKey -> Value' instr 'TChestKey
- data RemFail (instr :: k -> k -> Type) (i :: k) (o :: k) where
- RfNormal :: instr i o -> RemFail instr i o
- RfAlwaysFails :: (forall o'. instr i o') -> RemFail instr i o
- data Emit instr t = PackedValScope t => Emit {}
- data CreateContract instr cp st = (forall i o. Show (instr i o), forall i o. Eq (instr i o)) => CreateContract {
- ccOriginator :: L1Address
- ccDelegate :: Maybe KeyHash
- ccBalance :: Mutez
- ccStorageVal :: Value' instr st
- ccContract :: Contract' instr cp st
- ccCounter :: GlobalCounter
- data SetDelegate = SetDelegate {}
- data TransferTokens instr p = TransferTokens {
- ttTransferArgument :: Value' instr p
- ttAmount :: Mutez
- ttContract :: Value' instr ('TContract p)
- ttCounter :: GlobalCounter
- data Operation' instr where
- OpTransferTokens :: ParameterScope p => TransferTokens instr p -> Operation' instr
- OpSetDelegate :: SetDelegate -> Operation' instr
- OpCreateContract :: (forall i o. Show (instr i o), forall i o. NFData (instr i o), Typeable instr, ParameterScope cp, StorageScope st) => CreateContract instr cp st -> Operation' instr
- OpEmit :: PackedValScope t => Emit instr t -> Operation' instr
- rfMerge :: (forall o'. instr i1 o' -> instr i2 o' -> instr i3 o') -> RemFail instr i1 o -> RemFail instr i2 o -> RemFail instr i3 o
- rfAnyInstr :: RemFail instr i o -> instr i o
- rfMapAnyInstr :: (forall o'. instr i1 o' -> instr i2 o') -> RemFail instr i1 o -> RemFail instr i2 o
- addressToVContract :: forall t instr kind. (ParameterScope t, ForbidOr t) => KindedAddress kind -> Value' instr ('TContract t)
- buildVContract :: Value' instr ('TContract arg) -> Doc
- compileEpLiftSequence :: EpLiftSequence arg param -> Value' instr arg -> Value' instr param
- liftCallArg :: EntrypointCallT param arg -> Value' instr arg -> Value' instr param
- valueTypeSanity :: Value' instr t -> Dict (SingI t)
- mkVLam :: (SingI inp, SingI out, forall i o. Show (instr i o), forall i o. Eq (instr i o), forall i o. NFData (instr i o)) => (IsNotInView => RemFail instr '[inp] '[out]) -> Value' instr ('TLambda inp out)
- mkVLamRec :: (SingI inp, SingI out, forall i o. Show (instr i o), forall i o. Eq (instr i o), forall i o. NFData (instr i o)) => (IsNotInView => RemFail instr '[inp, 'TLambda inp out] '[out]) -> Value' instr ('TLambda inp out)
- withValueTypeSanity :: Value' instr t -> (SingI t => a) -> a
- eqValueExt :: Value' instr t1 -> Value' instr t2 -> Bool
- class EDivOp (n :: T) (m :: T) where
- class SliceOp (c :: T) where
- class ConcatOp (c :: T) where
- evalConcat :: Value' instr c -> Value' instr c -> Value' instr c
- evalConcat' :: [Value' instr c] -> Value' instr c
- class GetOp (c :: T) where
- class UpdOp (c :: T) where
- class SizeOp (c :: T) where
- class IterOp (c :: T) where
- class MapOp (c :: T) where
- class MemOp (c :: T) where
- divMich :: Integral a => a -> a -> a
- modMich :: Integral a => a -> a -> a
- type Bls12381MulBadOrder a1 a2 = DelayError (((('Text "Multiplication of " :<>: 'ShowType a2) :<>: 'Text " and ") :<>: 'ShowType a1) :<>: 'Text " works only other way around")
- data Ge
- data Le
- data Gt
- data Lt
- data Neq
- data Eq'
- data Compare
- data Lsr
- data Lsl
- data Not
- data Xor
- data And
- data Or
- data Neg
- data Abs
- data EDiv
- data Mul
- data SubMutez
- data Sub
- data Add
- class ToBytesArithOp (n :: T) where
- evalToBytesOp :: Value' instr n -> Value' instr 'TBytes
- class ToIntArithOp (n :: T) where
- evalToIntOp :: Value' instr n -> Value' instr 'TInt
- class UnaryArithOp aop (n :: T) where
- type UnaryArithRes aop n :: T
- evalUnaryArithOp :: proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
- data ArithError n m
- data MutezArithErrorType
- data ShiftArithErrorType
- class (Typeable n, Typeable m) => ArithOp aop (n :: T) (m :: T) where
- compareOp :: Comparable t => Value' i t -> Value' i t -> Integer
- evalToNatOp :: Value' instr 'TBytes -> Value' instr 'TNat
- data SomeMeta where
- data ExtInstr s
- data CommentType
- newtype PrintComment (st :: [T]) = PrintComment {
- unPrintComment :: [Either Text (StackRef st)]
- data StackRef (st :: [T]) where
- StackRef :: RequireLongerThan st idx => PeanoNatural idx -> StackRef st
- data TestAssert (s :: [T]) where
- TestAssert :: Text -> PrintComment inp -> Instr inp ('TBool ': out) -> TestAssert inp
- data Instr (inp :: [T]) (out :: [T]) where
- WithLoc :: ErrorSrcPos -> Instr a b -> Instr a b
- Meta :: SomeMeta -> Instr a b -> Instr a b
- Seq :: Instr a b -> Instr b c -> Instr a c
- Nop :: Instr s s
- Ext :: ExtInstr s -> Instr s s
- Nested :: Instr inp out -> Instr inp out
- DocGroup :: DocGrouping -> Instr inp out -> Instr inp out
- AnnCAR :: Anns '[VarAnn, FieldAnn] -> Instr ('TPair a b ': s) (a ': s)
- AnnCDR :: Anns '[VarAnn, FieldAnn] -> Instr ('TPair a b ': s) (b ': s)
- DROP :: Instr (a ': s) s
- DROPN :: forall (n :: Peano) s. RequireLongerOrSameLength s n => PeanoNatural n -> Instr s (Drop n s)
- AnnDUP :: DupableScope a => AnnVar -> Instr (a ': s) (a ': (a ': s))
- AnnDUPN :: forall (n :: Peano) inp out a. (ConstraintDUPN n inp out a, DupableScope a) => AnnVar -> PeanoNatural n -> Instr inp out
- SWAP :: Instr (a ': (b ': s)) (b ': (a ': s))
- DIG :: forall (n :: Peano) inp out a. ConstraintDIG n inp out a => PeanoNatural n -> Instr inp out
- DUG :: forall (n :: Peano) inp out a. ConstraintDUG n inp out a => PeanoNatural n -> Instr inp out
- AnnPUSH :: forall t s. ConstantScope t => Anns '[VarAnn, Notes t] -> Value' Instr t -> Instr s (t ': s)
- AnnSOME :: Anns '[TypeAnn, VarAnn] -> Instr (a ': s) ('TOption a ': s)
- AnnNONE :: forall a s. SingI a => Anns '[TypeAnn, VarAnn, Notes a] -> Instr s ('TOption a ': s)
- AnnUNIT :: Anns '[TypeAnn, VarAnn] -> Instr s ('TUnit ': s)
- IF_NONE :: Instr s s' -> Instr (a ': s) s' -> Instr ('TOption a ': s) s'
- AnnPAIR :: Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn] -> Instr (a ': (b ': s)) ('TPair a b ': s)
- AnnUNPAIR :: Anns '[VarAnn, VarAnn, FieldAnn, FieldAnn] -> Instr ('TPair a b ': s) (a ': (b ': s))
- AnnPAIRN :: forall n inp. ConstraintPairN n inp => AnnVar -> PeanoNatural n -> Instr inp (PairN n inp)
- UNPAIRN :: forall (n :: Peano) (pair :: T) (s :: [T]). ConstraintUnpairN n pair => PeanoNatural n -> Instr (pair ': s) (UnpairN n pair ++ s)
- AnnLEFT :: SingI b => Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes b] -> Instr (a ': s) ('TOr a b ': s)
- AnnRIGHT :: SingI a => Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a] -> Instr (b ': s) ('TOr a b ': s)
- IF_LEFT :: Instr (a ': s) s' -> Instr (b ': s) s' -> Instr ('TOr a b ': s) s'
- AnnNIL :: SingI p => Anns '[TypeAnn, VarAnn, Notes p] -> Instr s ('TList p ': s)
- AnnCONS :: AnnVar -> Instr (a ': ('TList a ': s)) ('TList a ': s)
- IF_CONS :: Instr (a ': ('TList a ': s)) s' -> Instr s s' -> Instr ('TList a ': s) s'
- AnnSIZE :: SizeOp c => AnnVar -> Instr (c ': s) ('TNat ': s)
- AnnEMPTY_SET :: Comparable e => Anns '[TypeAnn, VarAnn, Notes e] -> Instr s ('TSet e ': s)
- AnnEMPTY_MAP :: (SingI b, Comparable a) => Anns '[TypeAnn, VarAnn, Notes a, Notes b] -> Instr s ('TMap a b ': s)
- AnnEMPTY_BIG_MAP :: (SingI b, Comparable a, ForbidBigMap b) => Anns '[TypeAnn, VarAnn, Notes a, Notes b] -> Instr s ('TBigMap a b ': s)
- AnnMAP :: (MapOp c, SingI b) => AnnVar -> Instr (MapOpInp c ': s) (b ': s) -> Instr (c ': s) (MapOpRes c b ': s)
- ITER :: IterOp c => Instr (IterOpEl c ': s) s -> Instr (c ': s) s
- AnnMEM :: MemOp c => AnnVar -> Instr (MemOpKey c ': (c ': s)) ('TBool ': s)
- AnnGET :: (GetOp c, SingI (GetOpVal c)) => AnnVar -> Instr (GetOpKey c ': (c ': s)) ('TOption (GetOpVal c) ': s)
- AnnGETN :: forall (ix :: Peano) (pair :: T) (s :: [T]). ConstraintGetN ix pair => AnnVar -> PeanoNatural ix -> Instr (pair ': s) (GetN ix pair ': s)
- AnnUPDATE :: UpdOp c => AnnVar -> Instr (UpdOpKey c ': (UpdOpParams c ': (c ': s))) (c ': s)
- AnnUPDATEN :: forall (ix :: Peano) (val :: T) (pair :: T) (s :: [T]). ConstraintUpdateN ix pair => AnnVar -> PeanoNatural ix -> Instr (val ': (pair ': s)) (UpdateN ix val pair ': s)
- AnnGET_AND_UPDATE :: (GetOp c, UpdOp c, SingI (GetOpVal c), UpdOpKey c ~ GetOpKey c) => AnnVar -> Instr (UpdOpKey c ': (UpdOpParams c ': (c ': s))) ('TOption (GetOpVal c) ': (c ': s))
- IF :: Instr s s' -> Instr s s' -> Instr ('TBool ': s) s'
- LOOP :: Instr s ('TBool ': s) -> Instr ('TBool ': s) s
- LOOP_LEFT :: Instr (a ': s) ('TOr a b ': s) -> Instr ('TOr a b ': s) (b ': s)
- AnnLAMBDA :: forall i o s. (SingI i, SingI o) => Anns '[VarAnn, Notes i, Notes o] -> RemFail Instr '[i] '[o] -> Instr s ('TLambda i o ': s)
- AnnLAMBDA_REC :: forall i o s. (SingI i, SingI o) => Anns '[VarAnn, Notes i, Notes o] -> RemFail Instr '[i, 'TLambda i o] '[o] -> Instr s ('TLambda i o ': s)
- AnnEXEC :: AnnVar -> Instr (t1 ': ('TLambda t1 t2 ': s)) (t2 ': s)
- AnnAPPLY :: forall a b c s. (ConstantScope a, SingI b) => AnnVar -> Instr (a ': ('TLambda ('TPair a b) c ': s)) ('TLambda b c ': s)
- DIP :: Instr a c -> Instr (b ': a) (b ': c)
- DIPN :: forall (n :: Peano) inp out s s'. ConstraintDIPN n inp out s s' => PeanoNatural n -> Instr s s' -> Instr inp out
- FAILWITH :: (SingI a, ConstantScope a) => Instr (a ': s) t
- AnnCAST :: forall a s. SingI a => Anns '[VarAnn, Notes a] -> Instr (a ': s) (a ': s)
- AnnRENAME :: AnnVar -> Instr (a ': s) (a ': s)
- AnnPACK :: PackedValScope a => AnnVar -> Instr (a ': s) ('TBytes ': s)
- AnnUNPACK :: (UnpackedValScope a, SingI a) => Anns '[TypeAnn, VarAnn, Notes a] -> Instr ('TBytes ': s) ('TOption a ': s)
- AnnCONCAT :: ConcatOp c => AnnVar -> Instr (c ': (c ': s)) (c ': s)
- AnnCONCAT' :: ConcatOp c => AnnVar -> Instr ('TList c ': s) (c ': s)
- AnnSLICE :: (SliceOp c, SingI c) => AnnVar -> Instr ('TNat ': ('TNat ': (c ': s))) ('TOption c ': s)
- AnnISNAT :: AnnVar -> Instr ('TInt ': s) ('TOption 'TNat ': s)
- AnnADD :: ArithOp Add n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes Add n m ': s)
- AnnSUB :: ArithOp Sub n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes Sub n m ': s)
- AnnSUB_MUTEZ :: AnnVar -> Instr ('TMutez ': ('TMutez ': s)) ('TOption 'TMutez ': s)
- AnnMUL :: ArithOp Mul n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes Mul n m ': s)
- AnnEDIV :: ArithOp EDiv n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes EDiv n m ': s)
- AnnABS :: UnaryArithOp Abs n => AnnVar -> Instr (n ': s) (UnaryArithRes Abs n ': s)
- AnnNEG :: UnaryArithOp Neg n => AnnVar -> Instr (n ': s) (UnaryArithRes Neg n ': s)
- AnnLSL :: ArithOp Lsl n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes Lsl n m ': s)
- AnnLSR :: ArithOp Lsr n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes Lsr n m ': s)
- AnnOR :: ArithOp Or n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes Or n m ': s)
- AnnAND :: ArithOp And n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes And n m ': s)
- AnnXOR :: ArithOp Xor n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes Xor n m ': s)
- AnnNOT :: (SingI n, UnaryArithOp Not n) => AnnVar -> Instr (n ': s) (UnaryArithRes Not n ': s)
- AnnCOMPARE :: Comparable n => AnnVar -> Instr (n ': (n ': s)) ('TInt ': s)
- AnnEQ :: UnaryArithOp Eq' n => AnnVar -> Instr (n ': s) (UnaryArithRes Eq' n ': s)
- AnnNEQ :: UnaryArithOp Neq n => AnnVar -> Instr (n ': s) (UnaryArithRes Neq n ': s)
- AnnLT :: UnaryArithOp Lt n => AnnVar -> Instr (n ': s) (UnaryArithRes Lt n ': s)
- AnnGT :: UnaryArithOp Gt n => AnnVar -> Instr (n ': s) (UnaryArithRes Gt n ': s)
- AnnLE :: UnaryArithOp Le n => AnnVar -> Instr (n ': s) (UnaryArithRes Le n ': s)
- AnnGE :: UnaryArithOp Ge n => AnnVar -> Instr (n ': s) (UnaryArithRes Ge n ': s)
- AnnINT :: ToIntArithOp n => AnnVar -> Instr (n ': s) ('TInt ': s)
- AnnBYTES :: ToBytesArithOp n => AnnVar -> Instr (n ': s) ('TBytes ': s)
- AnnNAT :: AnnVar -> Instr ('TBytes ': s) ('TNat ': s)
- AnnVIEW :: (SingI arg, ViewableScope ret) => Anns '[VarAnn, Notes ret] -> ViewName -> Instr (arg ': ('TAddress ': s)) ('TOption ret ': s)
- AnnSELF :: forall (arg :: T) s. (ParameterScope arg, IsNotInView) => AnnVar -> SomeEntrypointCallT arg -> Instr s ('TContract arg ': s)
- AnnCONTRACT :: ParameterScope p => Anns '[VarAnn, Notes p] -> EpName -> Instr ('TAddress ': s) ('TOption ('TContract p) ': s)
- AnnTRANSFER_TOKENS :: (ParameterScope p, IsNotInView) => AnnVar -> Instr (p ': ('TMutez ': ('TContract p ': s))) ('TOperation ': s)
- AnnSET_DELEGATE :: IsNotInView => AnnVar -> Instr ('TOption 'TKeyHash ': s) ('TOperation ': s)
- AnnCREATE_CONTRACT :: (ParameterScope p, StorageScope g, IsNotInView) => Anns '[VarAnn, VarAnn] -> Contract' Instr p g -> Instr ('TOption 'TKeyHash ': ('TMutez ': (g ': s))) ('TOperation ': ('TAddress ': s))
- AnnIMPLICIT_ACCOUNT :: AnnVar -> Instr ('TKeyHash ': s) ('TContract 'TUnit ': s)
- AnnNOW :: AnnVar -> Instr s ('TTimestamp ': s)
- AnnAMOUNT :: AnnVar -> Instr s ('TMutez ': s)
- AnnBALANCE :: AnnVar -> Instr s ('TMutez ': s)
- AnnVOTING_POWER :: AnnVar -> Instr ('TKeyHash ': s) ('TNat ': s)
- AnnTOTAL_VOTING_POWER :: AnnVar -> Instr s ('TNat ': s)
- AnnCHECK_SIGNATURE :: AnnVar -> Instr ('TKey ': ('TSignature ': ('TBytes ': s))) ('TBool ': s)
- AnnSHA256 :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s)
- AnnSHA512 :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s)
- AnnBLAKE2B :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s)
- AnnSHA3 :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s)
- AnnKECCAK :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s)
- AnnHASH_KEY :: AnnVar -> Instr ('TKey ': s) ('TKeyHash ': s)
- AnnPAIRING_CHECK :: AnnVar -> Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) ': s) ('TBool ': s)
- AnnSOURCE :: AnnVar -> Instr s ('TAddress ': s)
- AnnSENDER :: AnnVar -> Instr s ('TAddress ': s)
- AnnADDRESS :: AnnVar -> Instr ('TContract a ': s) ('TAddress ': s)
- AnnCHAIN_ID :: AnnVar -> Instr s ('TChainId ': s)
- AnnLEVEL :: AnnVar -> Instr s ('TNat ': s)
- AnnSELF_ADDRESS :: AnnVar -> Instr s ('TAddress ': s)
- NEVER :: Instr ('TNever ': s) t
- AnnTICKET_DEPRECATED :: Comparable a => AnnVar -> Instr (a ': ('TNat ': s)) ('TTicket a ': s)
- AnnTICKET :: Comparable a => AnnVar -> Instr (a ': ('TNat ': s)) ('TOption ('TTicket a) ': s)
- AnnREAD_TICKET :: AnnVar -> Instr ('TTicket a ': s) (RightComb ['TAddress, a, 'TNat] ': ('TTicket a ': s))
- AnnSPLIT_TICKET :: AnnVar -> Instr ('TTicket a ': ('TPair 'TNat 'TNat ': s)) ('TOption ('TPair ('TTicket a) ('TTicket a)) ': s)
- AnnJOIN_TICKETS :: AnnVar -> Instr ('TPair ('TTicket a) ('TTicket a) ': s) ('TOption ('TTicket a) ': s)
- AnnOPEN_CHEST :: AnnVar -> Instr ('TChestKey ': ('TChest ': ('TNat ': s))) ('TOr 'TBytes 'TBool ': s)
- AnnSAPLING_EMPTY_STATE :: AnnVar -> Sing n -> Instr s ('TSaplingState n ': s)
- AnnSAPLING_VERIFY_UPDATE :: AnnVar -> Instr ('TSaplingTransaction n ': ('TSaplingState n ': s)) ('TOption ('TPair 'TBytes ('TPair 'TInt ('TSaplingState n))) ': s)
- AnnMIN_BLOCK_TIME :: [AnyAnn] -> Instr s ('TNat ': s)
- AnnEMIT :: PackedValScope t => AnnVar -> FieldAnn -> Maybe (Notes t) -> Instr (t ': s) ('TOperation ': s)
- pattern NAT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TNat s) => Instr inp out
- pattern BYTES :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) 'TBytes s, ToBytesArithOp n) => Instr inp out
- pattern EMIT :: forall {inp} {out}. () => forall (t :: T) (s :: [T]). (inp ~ '(:) t s, out ~ '(:) 'TOperation s, PackedValScope t) => FieldAnn -> Maybe (Notes t) -> Instr inp out
- pattern MIN_BLOCK_TIME :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TNat s) => Instr inp out
- pattern SAPLING_VERIFY_UPDATE :: forall {inp} {out}. () => forall (n :: Peano) (s :: [T]). (inp ~ '(:) ('TSaplingTransaction n) ('(:) ('TSaplingState n) s), out ~ '(:) ('TOption ('TPair 'TBytes ('TPair 'TInt ('TSaplingState n)))) s) => Instr inp out
- pattern SAPLING_EMPTY_STATE :: forall {inp} {out}. () => forall (n :: Peano) (s :: [T]). (inp ~ s, out ~ '(:) ('TSaplingState n) s) => Sing n -> Instr inp out
- pattern OPEN_CHEST :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TChestKey ('(:) 'TChest ('(:) 'TNat s)), out ~ '(:) ('TOr 'TBytes 'TBool) s) => Instr inp out
- pattern JOIN_TICKETS :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) ('TPair ('TTicket a) ('TTicket a)) s, out ~ '(:) ('TOption ('TTicket a)) s) => Instr inp out
- pattern SPLIT_TICKET :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) ('TTicket a) ('(:) ('TPair 'TNat 'TNat) s), out ~ '(:) ('TOption ('TPair ('TTicket a) ('TTicket a))) s) => Instr inp out
- pattern READ_TICKET :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) ('TTicket a) s, out ~ '(:) (RightComb ('(:) 'TAddress ('(:) a ('(:) 'TNat ('[] :: [T]))))) ('(:) ('TTicket a) s)) => Instr inp out
- pattern TICKET_DEPRECATED :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a ('(:) 'TNat s), out ~ '(:) ('TTicket a) s, Comparable a) => Instr inp out
- pattern TICKET :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a ('(:) 'TNat s), out ~ '(:) ('TOption ('TTicket a)) s, Comparable a) => Instr inp out
- pattern SELF_ADDRESS :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TAddress s) => Instr inp out
- pattern LEVEL :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TNat s) => Instr inp out
- pattern CHAIN_ID :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TChainId s) => Instr inp out
- pattern ADDRESS :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) ('TContract a) s, out ~ '(:) 'TAddress s) => Instr inp out
- pattern SENDER :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TAddress s) => Instr inp out
- pattern SOURCE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TAddress s) => Instr inp out
- pattern PAIRING_CHECK :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) ('TList ('TPair 'TBls12381G1 'TBls12381G2)) s, out ~ '(:) 'TBool s) => Instr inp out
- pattern HASH_KEY :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKey s, out ~ '(:) 'TKeyHash s) => Instr inp out
- pattern KECCAK :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out
- pattern SHA3 :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out
- pattern BLAKE2B :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out
- pattern CHECK_SIGNATURE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKey ('(:) 'TSignature ('(:) 'TBytes s)), out ~ '(:) 'TBool s) => Instr inp out
- pattern TOTAL_VOTING_POWER :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TNat s) => Instr inp out
- pattern VOTING_POWER :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKeyHash s, out ~ '(:) 'TNat s) => Instr inp out
- pattern BALANCE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TMutez s) => Instr inp out
- pattern AMOUNT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TMutez s) => Instr inp out
- pattern NOW :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TTimestamp s) => Instr inp out
- pattern IMPLICIT_ACCOUNT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKeyHash s, out ~ '(:) ('TContract 'TUnit) s) => Instr inp out
- pattern CREATE_CONTRACT :: forall {inp} {out}. () => forall (p :: T) (g :: T) (s :: [T]). (inp ~ '(:) ('TOption 'TKeyHash) ('(:) 'TMutez ('(:) g s)), out ~ '(:) 'TOperation ('(:) 'TAddress s), ParameterScope p, StorageScope g, IsNotInView) => Contract' Instr p g -> Instr inp out
- pattern SET_DELEGATE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) ('TOption 'TKeyHash) s, out ~ '(:) 'TOperation s, IsNotInView) => Instr inp out
- pattern TRANSFER_TOKENS :: forall {inp} {out}. () => forall (p :: T) (s :: [T]). (inp ~ '(:) p ('(:) 'TMutez ('(:) ('TContract p) s)), out ~ '(:) 'TOperation s, ParameterScope p, IsNotInView) => Instr inp out
- pattern CONTRACT :: forall {inp} {out}. () => forall (p :: T) (s :: [T]). (inp ~ '(:) 'TAddress s, out ~ '(:) ('TOption ('TContract p)) s, ParameterScope p) => EpName -> Instr inp out
- pattern SELF :: forall {inp} {out}. () => forall (arg :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TContract arg) s, ParameterScope arg, IsNotInView) => SomeEntrypointCallT arg -> Instr inp out
- pattern VIEW :: forall {inp} {out}. () => forall (arg :: T) (ret :: T) (s :: [T]). (inp ~ '(:) arg ('(:) 'TAddress s), out ~ '(:) ('TOption ret) s, SingI arg, ViewableScope ret) => ViewName -> Instr inp out
- pattern INT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) 'TInt s, ToIntArithOp n) => Instr inp out
- pattern NEQ :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Neq n) s, UnaryArithOp Neq n) => Instr inp out
- pattern COMPARE :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n ('(:) n s), out ~ '(:) 'TInt s, Comparable n) => Instr inp out
- pattern NOT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Not n) s, SingI n, UnaryArithOp Not n) => Instr inp out
- pattern XOR :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Xor n m) s, ArithOp Xor n m) => Instr inp out
- pattern AND :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes And n m) s, ArithOp And n m) => Instr inp out
- pattern OR :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Or n m) s, ArithOp Or n m) => Instr inp out
- pattern LSR :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Lsr n m) s, ArithOp Lsr n m) => Instr inp out
- pattern LSL :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Lsl n m) s, ArithOp Lsl n m) => Instr inp out
- pattern NEG :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Neg n) s, UnaryArithOp Neg n) => Instr inp out
- pattern ABS :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Abs n) s, UnaryArithOp Abs n) => Instr inp out
- pattern EDIV :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes EDiv n m) s, ArithOp EDiv n m) => Instr inp out
- pattern MUL :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Mul n m) s, ArithOp Mul n m) => Instr inp out
- pattern SUB_MUTEZ :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TMutez ('(:) 'TMutez s), out ~ '(:) ('TOption 'TMutez) s) => Instr inp out
- pattern SUB :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Sub n m) s, ArithOp Sub n m) => Instr inp out
- pattern ADD :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Add n m) s, ArithOp Add n m) => Instr inp out
- pattern ISNAT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TInt s, out ~ '(:) ('TOption 'TNat) s) => Instr inp out
- pattern SLICE :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) 'TNat ('(:) 'TNat ('(:) c s)), out ~ '(:) ('TOption c) s, SliceOp c, SingI c) => Instr inp out
- pattern CONCAT' :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) ('TList c) s, out ~ '(:) c s, ConcatOp c) => Instr inp out
- pattern CONCAT :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) c ('(:) c s), out ~ '(:) c s, ConcatOp c) => Instr inp out
- pattern UNPACK :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) ('TOption a) s, UnpackedValScope a, SingI a) => Instr inp out
- pattern PACK :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) 'TBytes s, PackedValScope a) => Instr inp out
- pattern RENAME :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) a s) => Instr inp out
- pattern CAST :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) a s, SingI a) => Instr inp out
- pattern APPLY :: forall {inp} {out}. () => forall (a :: T) (b :: T) (c :: T) (s :: [T]). (inp ~ '(:) a ('(:) ('TLambda ('TPair a b) c) s), out ~ '(:) ('TLambda b c) s, ConstantScope a, SingI b) => Instr inp out
- pattern EXEC :: forall {inp} {out}. () => forall (t1 :: T) (t2 :: T) (s :: [T]). (inp ~ '(:) t1 ('(:) ('TLambda t1 t2) s), out ~ '(:) t2 s) => Instr inp out
- pattern LAMBDA_REC :: forall s r. () => forall i o. (SingI i, SingI o, r ~ ('TLambda i o ': s)) => (IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o]) -> Instr s r
- pattern LAMBDA :: forall s r. () => forall i o. (SingI i, SingI o, r ~ ('TLambda i o ': s)) => (IsNotInView => RemFail Instr '[i] '[o]) -> Instr s r
- pattern GET_AND_UPDATE :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) (UpdOpKey c) ('(:) (UpdOpParams c) ('(:) c s)), out ~ '(:) ('TOption (GetOpVal c)) ('(:) c s), GetOp c, UpdOp c, SingI (GetOpVal c), (~) (UpdOpKey c) (GetOpKey c)) => Instr inp out
- pattern UPDATEN :: forall {inp} {out}. () => forall (ix :: Peano) (val :: T) (pair :: T) (s :: [T]). (inp ~ '(:) val ('(:) pair s), out ~ '(:) (UpdateN ix val pair) s, ConstraintUpdateN ix pair) => PeanoNatural ix -> Instr inp out
- pattern UPDATE :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) (UpdOpKey c) ('(:) (UpdOpParams c) ('(:) c s)), out ~ '(:) c s, UpdOp c) => Instr inp out
- pattern GETN :: forall {inp} {out}. () => forall (ix :: Peano) (pair :: T) (s :: [T]). (inp ~ '(:) pair s, out ~ '(:) (GetN ix pair) s, ConstraintGetN ix pair) => PeanoNatural ix -> Instr inp out
- pattern GET :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) (GetOpKey c) ('(:) c s), out ~ '(:) ('TOption (GetOpVal c)) s, GetOp c, SingI (GetOpVal c)) => Instr inp out
- pattern MEM :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) (MemOpKey c) ('(:) c s), out ~ '(:) 'TBool s, MemOp c) => Instr inp out
- pattern MAP :: forall {inp} {out}. () => forall (c :: T) (b :: T) (s :: [T]). (inp ~ '(:) c s, out ~ '(:) (MapOpRes c b) s, MapOp c, SingI b) => Instr ('(:) (MapOpInp c) s) ('(:) b s) -> Instr inp out
- pattern EMPTY_BIG_MAP :: forall {inp} {out}. () => forall (b :: T) (a :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TBigMap a b) s, SingI b, Comparable a, ForbidBigMap b) => Instr inp out
- pattern EMPTY_MAP :: forall {inp} {out}. () => forall (b :: T) (a :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TMap a b) s, SingI b, Comparable a) => Instr inp out
- pattern EMPTY_SET :: forall {inp} {out}. () => forall (e :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TSet e) s, Comparable e) => Instr inp out
- pattern SIZE :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) c s, out ~ '(:) 'TNat s, SizeOp c) => Instr inp out
- pattern CONS :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a ('(:) ('TList a) s), out ~ '(:) ('TList a) s) => Instr inp out
- pattern NIL :: forall {inp} {out}. () => forall (p :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TList p) s, SingI p) => Instr inp out
- pattern RIGHT :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) b s, out ~ '(:) ('TOr a b) s, SingI a) => Instr inp out
- pattern LEFT :: forall {inp} {out}. () => forall (b :: T) (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) ('TOr a b) s, SingI b) => Instr inp out
- pattern PAIRN :: forall {inp} {out}. () => forall (n :: Peano) (inp :: [T]). (inp ~ inp, out ~ PairN n inp, ConstraintPairN n inp) => PeanoNatural n -> Instr inp out
- pattern UNPAIR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) ('TPair a b) s, out ~ '(:) a ('(:) b s)) => Instr inp out
- pattern PAIR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) a ('(:) b s), out ~ '(:) ('TPair a b) s) => Instr inp out
- pattern UNIT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TUnit s) => Instr inp out
- pattern SOME :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) ('TOption a) s) => Instr inp out
- pattern PUSH :: forall {inp} {out}. () => forall (t :: T) (s :: [T]). (inp ~ s, out ~ '(:) t s, ConstantScope t) => Value' Instr t -> Instr inp out
- pattern DUPN :: forall {inp} {out}. () => forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T). (inp ~ inp, out ~ out, ConstraintDUPN n inp out a, DupableScope a) => PeanoNatural n -> Instr inp out
- pattern DUP :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) a ('(:) a s), DupableScope a) => Instr inp out
- pattern CDR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) ('TPair a b) s, out ~ '(:) b s) => Instr inp out
- pattern CAR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) ('TPair a b) s, out ~ '(:) a s) => Instr inp out
- pattern GE :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Ge n) s, UnaryArithOp Ge n) => Instr inp out
- pattern SHA256 :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out
- pattern SHA512 :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out
- pattern LE :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Le n) s, UnaryArithOp Le n) => Instr inp out
- pattern NONE :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TOption a) s, SingI a) => Instr inp out
- pattern GT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Gt n) s, UnaryArithOp Gt n) => Instr inp out
- pattern LT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Lt n) s, UnaryArithOp Lt n) => Instr inp out
- pattern EQ :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Eq' n) s, UnaryArithOp Eq' n) => Instr inp out
- pattern ConcreteMeta :: Typeable meta => meta -> Instr i o -> Instr i o
- pattern (:#) :: Instr a b -> Instr b c -> Instr a c
- castInstr :: forall inp1 out1 inp2 out2. (SingI inp1, SingI out1, SingI inp2, SingI out2) => Instr inp1 out1 -> Maybe (Instr inp2 out2)
- mkStackRef :: forall (gn :: Nat) st n. (n ~ ToPeano gn, SingIPeano gn, RequireLongerThan st n) => StackRef st
- frameInstr :: forall s a b. Instr a b -> Instr (a ++ s) (b ++ s)
- type SomeViewsSet = SomeViewsSet' Instr
- type ViewsSet = ViewsSet' Instr
- type SomeView = SomeView' Instr
- type View = View' Instr
- type ViewCode arg st ret = ViewCode' Instr arg st ret
- type Contract = Contract' Instr
- type ContractCode cp st = ContractCode' Instr cp st
- type Operation = Operation' Instr
- type Value = Value' Instr
- data SomeAnns where
- data PushableStorageSplit s st where
- ConstantStorage :: ConstantScope st => Value st -> PushableStorageSplit s st
- PushableValueStorage :: StorageScope st => Instr s (st ': s) -> PushableStorageSplit s st
- PartlyPushableStorage :: (StorageScope heavy, StorageScope st) => Value heavy -> Instr (heavy ': s) (st ': s) -> PushableStorageSplit s st
- data CtorEffectsApp m = CtorEffectsApp {}
- data DfsSettings m = DfsSettings {
- dsGoToValues :: Bool
- dsCtorEffectsApp :: CtorEffectsApp m
- dsInstrStep :: forall i o. Instr i o -> m (Instr i o)
- dsValueStep :: forall t'. Value t' -> m (Value t')
- dfsTraverseInstr :: forall m inp out. Monad m => DfsSettings m -> Instr inp out -> m (Instr inp out)
- dfsFoldInstr :: forall x inp out. Monoid x => DfsSettings (Writer x) -> (forall i o. Instr i o -> x) -> Instr inp out -> x
- dfsModifyInstr :: DfsSettings Identity -> (forall i o. Instr i o -> Instr i o) -> Instr inp out -> Instr inp out
- analyzeInstrFailure :: Instr i o -> RemFail Instr i o
- linearizeLeft :: Instr inp out -> Instr inp out
- linearizeLeftDeep :: Instr inp out -> Instr inp out
- dfsMapValue :: forall t. DfsSettings Identity -> Value t -> Value t
- dfsTraverseValue :: forall t m. Monad m => DfsSettings m -> Value t -> m (Value t)
- dfsFoldMapValue :: Monoid x => (forall t'. Value t' -> x) -> Value t -> x
- dfsFoldMapValueM :: (Monoid x, Monad m) => (forall t'. Value t' -> m x) -> Value t -> m x
- isStringValue :: Value t -> Maybe MText
- isBytesValue :: Value t -> Maybe ByteString
- allAtomicValues :: forall t a. (forall t'. Value t' -> Maybe a) -> Value t -> [a]
- splitPushableStorage :: StorageScope t => Value t -> PushableStorageSplit s t
- isMichelsonInstr :: Instr i o -> Bool
- instrAnns :: Instr i o -> Maybe SomeAnns
- class IsoValuesStack (ts :: [Type]) where
- type family ToTs' t where ...
- type family ToTs (ts :: [Type]) :: [T] where ...
- type GenericIsoValue t = (IsoValue t, Generic t, ToT t ~ GValueType (Rep t))
- class ToBigMap m where
- type ToBigMapKey m
- type ToBigMapValue m
- mkBigMap :: m -> BigMap (ToBigMapKey m) (ToBigMapValue m)
- data BigMap k v
- newtype BigMapId k v = BigMapId {}
- data Ticket (arg :: Type) = Ticket {}
- data ContractRef (arg :: Type) = ContractRef {
- crAddress :: Address
- crEntrypoint :: SomeEntrypointCall arg
- type HasNoOpToT a = (IsoValue a, ForbidOp (ToT a))
- type WellTypedToT a = (IsoValue a, WellTyped (ToT a))
- type SomeEntrypointCall arg = SomeEntrypointCallT (ToT arg)
- type EntrypointCall param arg = EntrypointCallT (ToT param) (ToT arg)
- type family ToT' t where ...
- class WellTypedToT a => IsoValue a where
- type KnownIsoT a = (IsoValue a, SingI (ToT a))
- isoValue :: (IsoValue a, IsoValue b) => Iso (Value (ToT a)) (Value (ToT b)) a b
- coerceContractRef :: ToT a ~ ToT b => ContractRef a -> ContractRef b
- contractRefToAddr :: ContractRef cp -> EpAddress
- totsKnownLemma :: forall s. KnownList s :- KnownList (ToTs s)
- totsAppendLemma :: forall a b. KnownList a => Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
- type InstrUnwrapC dt name = (GenericIsoValue dt, GInstrUnwrap (Rep dt) (LnrBranch (GetNamed name dt)) (CtorOnlyField name dt))
- type family GCaseBranchInput ctor x :: CaseClauseParam
- type family GCaseBranchInput ctor x :: CaseClauseParam
- type family GCaseClauses x rest :: [CaseClauseParam]
- type family GCaseClauses x rest :: [CaseClauseParam]
- type CaseClauses a = GCaseClauses (Rep a) '[]
- data CaseClause (inp :: [T]) (out :: [T]) (param :: CaseClauseParam) where
- CaseClause :: RemFail Instr (AppendCtorField x inp) out -> CaseClause inp out ('CaseClauseParam ctor x)
- data CaseClauseParam = CaseClauseParam Symbol CtorField
- type InstrCaseC dt = (GenericIsoValue dt, GInstrCase (Rep dt) '[])
- data MyCompoundType
- type InstrWrapOneC dt name = (InstrWrapC dt name, GetCtorField dt name ~ 'OneField (CtorOnlyField name dt))
- type InstrWrapC dt name = (GenericIsoValue dt, GInstrWrap (Rep dt) (LnrBranch (GetNamed name dt)) (LnrFieldType (GetNamed name dt)))
- type CtorOnlyField name dt = RequireOneField name (GetCtorField dt name)
- type CtorHasOnlyField ctor dt f = GetCtorField dt ctor ~ 'OneField f
- type GetCtorField dt ctor = LnrFieldType (GetNamed ctor dt)
- type family IsPrimitiveValue (x :: Type) :: Bool where ...
- type AppendCtorFieldAxiom (cf :: CtorField) (st :: [Type]) = ToTs (AppendCtorField cf st) ~ AppendCtorField cf (ToTs st)
- type family AppendCtorField cf l where ...
- type family ExtractCtorField (cf :: CtorField) where ...
- data CtorField
- appendCtorFieldAxiom :: (AppendCtorFieldAxiom ('OneField Word) '[Int], AppendCtorFieldAxiom 'NoFields '[Int]) => Dict (AppendCtorFieldAxiom cf st)
- instrWrap :: forall dt name st. InstrWrapC dt name => Label name -> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt ': st)
- instrWrapOne :: forall dt name st. InstrWrapOneC dt name => Label name -> Instr (ToT (CtorOnlyField name dt) ': st) (ToT dt ': st)
- hsWrap :: forall dt name. InstrWrapC dt name => Label name -> ExtractCtorField (GetCtorField dt name) -> dt
- instrCase :: forall dt out inp. InstrCaseC dt => Rec (CaseClause inp out) (CaseClauses dt) -> RemFail Instr (ToT dt ': inp) out
- (//->) :: Label ("c" `AppendSymbol` ctor) -> RemFail Instr (AppendCtorField x inp) out -> CaseClause inp out ('CaseClauseParam ctor x)
- unsafeInstrUnwrap :: forall dt name st. InstrUnwrapC dt name => Label name -> Instr (ToT dt ': st) (ToT (CtorOnlyField name dt) ': st)
- hsUnwrap :: forall dt name. InstrUnwrapC dt name => Label name -> dt -> Maybe (CtorOnlyField name dt)
- type InstrDeconstructC dt st = (GenericIsoValue dt, GInstrDeconstruct (Rep dt) '[] st)
- type family GFieldTypes x rest :: [Type]
- type family GFieldTypes x rest :: [Type]
- type InstrConstructC dt = (GenericIsoValue dt, GInstrConstruct (Rep dt) '[])
- type ConstructorFieldNames dt = GFieldNames (Rep dt)
- type ConstructorFieldTypes dt = GFieldTypes (Rep dt) '[]
- class ToTs xs ~ ToTs ys => CastFieldConstructors xs ys where
- castFieldConstructorsImpl :: Rec (FieldConstructor st) xs -> Rec (FieldConstructor st) ys
- newtype FieldConstructor (st :: [k]) (field :: Type) = FieldConstructor (Instr (ToTs' st) (ToT field ': ToTs' st))
- type InstrSetFieldC dt name = (GenericIsoValue dt, GInstrSetField name (Rep dt) (LnrBranch (GetNamed name dt)) (LnrFieldType (GetNamed name dt)))
- type InstrGetFieldC dt name = (GenericIsoValue dt, GInstrGet name (Rep dt) (LnrBranch (GetNamed name dt)) (LnrFieldType (GetNamed name dt)))
- type GetFieldType dt name = LnrFieldType (GetNamed name dt)
- type family GLookupNamed (name :: Symbol) (x :: Type -> Type) :: Maybe LookupNamedResult where ...
- instrToField :: forall dt name st. InstrGetFieldC dt name => Label name -> Instr (ToT dt ': st) (ToT (GetFieldType dt name) ': st)
- instrGetField :: forall dt name st. (InstrGetFieldC dt name, DupableScope (ToT (GetFieldType dt name))) => Label name -> Instr (ToT dt ': st) (ToT (GetFieldType dt name) ': (ToT dt ': st))
- instrGetFieldOpen :: forall dt name res st. InstrGetFieldC dt name => Instr '[ToT (GetFieldType dt name)] '[res, ToT (GetFieldType dt name)] -> Instr '[ToT (GetFieldType dt name)] '[res] -> Label name -> Instr (ToT dt ': st) (res ': (ToT dt ': st))
- instrSetField :: forall dt name st. InstrSetFieldC dt name => Label name -> Instr (ToT (GetFieldType dt name) ': (ToT dt ': st)) (ToT dt ': st)
- instrSetFieldOpen :: forall dt name new st. InstrSetFieldC dt name => Instr '[new, ToT (GetFieldType dt name)] '[ToT (GetFieldType dt name)] -> Label name -> Instr (new ': (ToT dt ': st)) (ToT dt ': st)
- instrConstruct :: forall dt st. InstrConstructC dt => Rec (FieldConstructor st) (ConstructorFieldTypes dt) -> Instr st (ToT dt ': st)
- instrConstructStack :: forall dt stack st. (InstrConstructC dt, stack ~ ToTs (ConstructorFieldTypes dt)) => Instr (stack ++ st) (ToT dt ': st)
- instrDeconstruct :: forall dt stack (st :: [T]). (InstrDeconstructC dt st, stack ~ ToTs (GFieldTypes (Rep dt) '[])) => Instr (ToT dt ': st) (stack ++ st)
- convertParamNotes :: ParamNotes cp -> ParameterType
- convertContractCode :: forall param store. (SingI param, SingI store) => ContractCode param store -> Contract
- convertContractCodeOptimized :: forall param store. (SingI param, SingI store) => ContractCode param store -> Contract
- convertView :: forall arg store ret. View arg store ret -> View
- convertSomeView :: SomeView st -> View
- convertContract :: Contract param store -> Contract
- convertContractOptimized :: Contract param store -> Contract
- untypeValue :: ForbidOp t => Value' Instr t -> Value
- untypeValueHashable :: ForbidOp t => Value' Instr t -> Value
- untypeValueOptimized :: ForbidOp t => Value' Instr t -> Value
- untypeDemoteT :: forall (t :: T). SingI t => Ty
- instrToOpsOptimized :: HasCallStack => Instr inp out -> [ExpandedOp]
- instrToOps :: HasCallStack => Instr inp out -> [ExpandedOp]
- eqInstrExt :: Instr i1 o1 -> Instr i2 o2 -> Bool
- sampleTypedValue :: forall t. WellTyped t => Sing t -> Maybe (Value t)
- flattenEntrypoints :: HandleImplicitDefaultEp -> ParamNotes t -> Map EpName Ty
- data SomeVBigMap where
- SomeVBigMap :: forall k v. Value ('TBigMap k v) -> SomeVBigMap
- data SomeContractAndStorage where
- SomeContractAndStorage :: forall cp st. (StorageScope st, ParameterScope cp) => Contract cp st -> Value st -> SomeContractAndStorage
- data SomeContract where
- SomeContract :: Contract cp st -> SomeContract
- data SomeIsoValue where
- SomeIsoValue :: KnownIsoT a => a -> SomeIsoValue
- type SomePackedVal = SomeConstrainedValue PackedValScope
- type SomeStorage = SomeConstrainedValue StorageScope
- type SomeConstant = SomeConstrainedValue ConstantScope
- type SomeValue = SomeConstrainedValue SingI
- type SomeConstrainedValue c = Constrained c Value
- type LooseSumC dt = (Generic dt, GLooseSum (Rep dt))
- data ComposeResult a
- toTaggedVal :: LooseSumC dt => dt -> (Text, SomeValue)
- fromTaggedVal :: LooseSumC dt => (Text, SomeValue) -> ComposeResult dt
- data SomeAnnotatedValue where
- SomeAnnotatedValue :: forall t. SingI t => Notes t -> Value t -> SomeAnnotatedValue
- data AnnotatedValue v = AnnotatedValue {}
- data FieldRep a = FieldRep {}
- data ConstructorRep a = ConstructorRep {}
- type ADTRep a = [ConstructorRep a]
- crDescriptionL :: forall a. Lens' (ConstructorRep a) (Maybe Text)
- crFieldsL :: forall a a. Lens (ConstructorRep a) (ConstructorRep a) [FieldRep a] [FieldRep a]
- crNameL :: forall a. Lens' (ConstructorRep a) Text
- type PolyTypeHasDocC ts = Each '[TypeHasDoc] ts
- class GProductHasDoc (x :: Type -> Type)
- class GTypeHasDoc (x :: Type -> Type)
- class IsHomomorphic a
- class HaveCommonTypeCtor a b
- newtype DStorageType = DStorageType DType
- data DType where
- DType :: TypeHasDoc a => Proxy a -> DType
- data SomeTypeWithDoc where
- SomeTypeWithDoc :: TypeHasDoc td => Proxy td -> SomeTypeWithDoc
- type TypeDocMichelsonRep a = Proxy a -> (Maybe DocTypeRepLHS, T)
- type TypeDocHaskellRep a = Proxy a -> FieldDescriptionsV -> Maybe (Maybe DocTypeRepLHS, ADTRep SomeTypeWithDoc)
- class (Typeable a, SingI (TypeDocFieldDescriptions a), FieldDescriptionsValid (TypeDocFieldDescriptions a) a) => TypeHasDoc a where
- type TypeDocFieldDescriptions a :: FieldDescriptions
- typeDocName :: Proxy a -> Text
- typeDocMdDescription :: Markdown
- typeDocMdReference :: Proxy a -> WithinParens -> Markdown
- typeDocDependencies :: Proxy a -> [SomeDocDefinitionItem]
- typeDocHaskellRep :: TypeDocHaskellRep a
- typeDocMichelsonRep :: TypeDocMichelsonRep a
- data FieldSnakeCase
- data FieldCamelCase
- class TypeHasFieldNamingStrategy a where
- typeFieldNamingStrategy :: Text -> Text
- newtype WithinParens = WithinParens Bool
- frDescriptionL :: forall a. Lens' (FieldRep a) (Maybe Text)
- frNameL :: forall a. Lens' (FieldRep a) (Maybe Text)
- frTypeRepL :: forall a a. Lens (FieldRep a) (FieldRep a) a a
- buildADTRep :: forall a. (WithinParens -> a -> Markdown) -> ADTRep a -> Markdown
- applyWithinParens :: WithinParens -> Markdown -> Markdown
- buildTypeWithinParens :: forall a. Typeable a => WithinParens -> Markdown
- typeDocBuiltMichelsonRep :: TypeHasDoc a => Proxy a -> Doc
- dTypeDep :: forall (t :: Type). TypeHasDoc t => SomeDocDefinitionItem
- dTypeDepP :: forall (t :: Type). TypeHasDoc t => Proxy t -> SomeDocDefinitionItem
- dStorage :: forall store. TypeHasDoc store => DStorageType
- customTypeDocMdReference :: (Text, DType) -> [DType] -> WithinParens -> Markdown
- customTypeDocMdReference' :: (Text, DType) -> [WithinParens -> Markdown] -> WithinParens -> Markdown
- homomorphicTypeDocMdReference :: forall (t :: Type). (Typeable t, TypeHasDoc t, IsHomomorphic t) => Proxy t -> WithinParens -> Markdown
- poly1TypeDocMdReference :: forall t (r :: Type) (a :: Type). (r ~ t a, Typeable t, Each '[TypeHasDoc] [r, a], IsHomomorphic t) => Proxy r -> WithinParens -> Markdown
- poly2TypeDocMdReference :: forall t (r :: Type) (a :: Type) (b :: Type). (r ~ t a b, Typeable t, Each '[TypeHasDoc] [r, a, b], IsHomomorphic t) => Proxy r -> WithinParens -> Markdown
- genericTypeDocDependencies :: forall a. (Generic a, GTypeHasDoc (Rep a)) => Proxy a -> [SomeDocDefinitionItem]
- homomorphicTypeDocHaskellRep :: forall a. (Generic a, GTypeHasDoc (Rep a)) => TypeDocHaskellRep a
- concreteTypeDocHaskellRep :: forall a b. (Typeable a, GenericIsoValue a, GTypeHasDoc (Rep a), HaveCommonTypeCtor b a) => TypeDocHaskellRep b
- unsafeConcreteTypeDocHaskellRep :: forall a b. (Typeable a, GenericIsoValue a, GTypeHasDoc (Rep a)) => TypeDocHaskellRep b
- haskellRepNoFields :: TypeDocHaskellRep a -> TypeDocHaskellRep a
- haskellRepMap :: (Text -> Text) -> TypeDocHaskellRep a -> TypeDocHaskellRep a
- haskellAddNewtypeField :: Text -> TypeDocHaskellRep a -> TypeDocHaskellRep a
- haskellRepAdjust :: (Maybe Text -> Maybe Text) -> TypeDocHaskellRep a -> TypeDocHaskellRep a
- homomorphicTypeDocMichelsonRep :: forall a. KnownIsoT a => TypeDocMichelsonRep a
- concreteTypeDocMichelsonRep :: forall a b. (Typeable a, KnownIsoT a, HaveCommonTypeCtor b a) => TypeDocMichelsonRep b
- unsafeConcreteTypeDocMichelsonRep :: forall a b. (Typeable a, KnownIsoT a) => TypeDocMichelsonRep b
- docInstr :: DocItem di => di -> Instr s s
- cutInstrNonDoc :: (forall i o. Instr i o -> Instr i o) -> Instr inp out -> Instr s s
Documentation
withDict :: HasDict c e => e -> (c => r) -> r #
From a Dict
, takes a value in an environment where the instance
witnessed by the Dict
is in scope, and evaluates it.
Essentially a deconstruction of a Dict
into its continuation-style
form.
Can also be used to deconstruct an entailment, a
, using a context :-
ba
.
withDict ::Dict
c -> (c => r) -> r withDict :: a => (a:-
c) -> (c => r) -> r
Values of type
capture a dictionary for a constraint of type Dict
pp
.
e.g.
Dict
::Dict
(Eq
Int
)
captures a dictionary that proves we have an:
instanceEq
Int
Pattern matching on the Dict
constructor will bring this instance into scope.
Instances
() :=> (Semigroup (Dict a)) | |
() :=> (Show (Dict a)) | |
() :=> (Eq (Dict a)) | |
() :=> (Ord (Dict a)) | |
a :=> (Monoid (Dict a)) | |
a :=> (Bounded (Dict a)) | |
a :=> (Enum (Dict a)) | |
a :=> (Read (Dict a)) | |
HasDict a (Dict a) | |
Defined in Data.Constraint | |
(Typeable p, p) => Data (Dict p) | |
Defined in Data.Constraint gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Dict p -> c (Dict p) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Dict p) # toConstr :: Dict p -> Constr # dataTypeOf :: Dict p -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Dict p)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Dict p)) # gmapT :: (forall b. Data b => b -> b) -> Dict p -> Dict p # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Dict p -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Dict p -> r # gmapQ :: (forall d. Data d => d -> u) -> Dict p -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Dict p -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Dict p -> m (Dict p) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Dict p -> m (Dict p) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Dict p -> m (Dict p) # | |
a => Monoid (Dict a) | |
Semigroup (Dict a) | |
a => Bounded (Dict a) | |
a => Enum (Dict a) | |
Defined in Data.Constraint | |
a => Read (Dict a) | |
Show (Dict a) | |
NFData (Dict c) | |
Defined in Data.Constraint | |
Eq (Dict a) | |
Ord (Dict a) | |
This is the type of entailment.
a
is read as :-
ba
"entails" b
.
With this we can actually build a category for Constraint
resolution.
e.g.
Because
is a superclass of Eq
a
, we can show that Ord
a
entails Ord
a
.Eq
a
Because instance
exists, we can show that Ord
a => Ord
[a]
entails Ord
a
as well.Ord
[a]
This relationship is captured in the :-
entailment type here.
Since p
and entailment composes, :-
p:-
forms the arrows of a
Category
of constraints. However, Category
only became sufficiently
general to support this instance in GHC 7.8, so prior to 7.8 this instance
is unavailable.
But due to the coherence of instance resolution in Haskell, this Category
has some very interesting properties. Notably, in the absence of
IncoherentInstances
, this category is "thin", which is to say that
between any two objects (constraints) there is at most one distinguishable
arrow.
This means that for instance, even though there are two ways to derive
, the answers from these two paths _must_ by
construction be equal. This is a property that Haskell offers that is
pretty much unique in the space of languages with things they call "type
classes".Ord
a :-
Eq
[a]
What are the two ways?
Well, we can go from
via the
superclass relationship, and then from Ord
a :-
Eq
a
via the
instance, or we can go from Eq
a :-
Eq
[a]
via the instance
then from Ord
a :-
Ord
[a]
through the superclass relationship
and this diagram by definition must "commute".Ord
[a] :-
Eq
[a]
Diagrammatically,
Ord a ins / \ cls v v Ord [a] Eq a cls \ / ins v v Eq [a]
This safety net ensures that pretty much anything you can write with this library is sensible and can't break any assumptions on the behalf of library authors.
Instances
Category (:-) | Possible since GHC 7.8, when |
() :=> (Show (a :- b)) | |
() :=> (Eq (a :- b)) | |
() :=> (Ord (a :- b)) | |
a => HasDict b (a :- b) | |
Defined in Data.Constraint | |
(Typeable p, Typeable q, p, q) => Data (p :- q) | |
Defined in Data.Constraint gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> (p :- q) -> c (p :- q) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (p :- q) # toConstr :: (p :- q) -> Constr # dataTypeOf :: (p :- q) -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (p :- q)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (p :- q)) # gmapT :: (forall b. Data b => b -> b) -> (p :- q) -> p :- q # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (p :- q) -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (p :- q) -> r # gmapQ :: (forall d. Data d => d -> u) -> (p :- q) -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> (p :- q) -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) # | |
Show (a :- b) | |
a => NFData (a :- b) | |
Defined in Data.Constraint | |
Eq (a :- b) | Assumes |
Ord (a :- b) | Assumes |
Defined in Data.Constraint |
A SingI
constraint is essentially an implicitly-passed singleton.
If you need to satisfy this constraint with an explicit singleton, please
see withSingI
or the Sing
pattern synonym.
Produce the singleton explicitly. You will likely need the ScopedTypeVariables
extension to use this method the way you want.
Instances
Path to a leaf (some field or constructor) in generic tree representation.
Which branch to choose in generic tree representation: left,
straight or right. S
is used when there is one constructor with
one field (something newtype-like).
The reason why we need S
can be explained by this example:
data A = A1 B | A2 Integer
data B = B Bool
Now we may search for A1 constructor or B constructor. Without S
in
both cases path will be the same ([L]).
data Constrained c f where Source #
pattern SomePackedVal :: () => PackedValScope t => Value t -> SomePackedVal | |
pattern SomeConstant :: () => ConstantScope t => Value t -> SomeConstant | |
pattern SomeConstrainedValue :: forall c. () => forall a. c a => Value a -> SomeConstrainedValue c | |
pattern SomeStorage :: () => StorageScope t => Value t -> SomeStorage | |
pattern SomeValue :: () => SingI t => Value t -> SomeValue |
Instances
ligoLayout :: GenericStrategy Source #
Default layout in LIGO.
To be used with customGeneric
, see this method for more info.
This is similar to leftBalanced
, but
- fields are sorted alphabetically;
- always puts as large complete binary subtrees as possible at left.
ligoCombLayout :: GenericStrategy Source #
Comb layout in LIGO ( [@layout:comb]
).
To be used with customGeneric
.
Note: to make comb layout work for sum types, make sure that in LIGO all the constructors are preceded by the bar symbol in your type declaration:
type my_type = [@layout:comb] | Ctor1 of nat ← bar symbol _must_ be here | Ctor2 of int ...
Though the situation may change: https://gitlab.com/ligolang/ligo/-/issues/1104.
Michelson language type with annotations stripped off.
Instances
buildStack :: [T] -> Doc Source #
Format type stack in a pretty way.
data SingT :: T -> Type where Source #
STKey :: SingT ('TKey :: T) | |
STUnit :: SingT ('TUnit :: T) | |
STSignature :: SingT ('TSignature :: T) | |
STChainId :: SingT ('TChainId :: T) | |
STOption :: forall (n :: T). (Sing n) -> SingT ('TOption n :: T) | |
STList :: forall (n :: T). (Sing n) -> SingT ('TList n :: T) | |
STSet :: forall (n :: T). (Sing n) -> SingT ('TSet n :: T) | |
STOperation :: SingT ('TOperation :: T) | |
STContract :: forall (n :: T). (Sing n) -> SingT ('TContract n :: T) | |
STTicket :: forall (n :: T). (Sing n) -> SingT ('TTicket n :: T) | |
STPair :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TPair n n :: T) | |
STOr :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TOr n n :: T) | |
STLambda :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TLambda n n :: T) | |
STMap :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TMap n n :: T) | |
STBigMap :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TBigMap n n :: T) | |
STInt :: SingT ('TInt :: T) | |
STNat :: SingT ('TNat :: T) | |
STString :: SingT ('TString :: T) | |
STBytes :: SingT ('TBytes :: T) | |
STMutez :: SingT ('TMutez :: T) | |
STBool :: SingT ('TBool :: T) | |
STKeyHash :: SingT ('TKeyHash :: T) | |
STBls12381Fr :: SingT ('TBls12381Fr :: T) | |
STBls12381G1 :: SingT ('TBls12381G1 :: T) | |
STBls12381G2 :: SingT ('TBls12381G2 :: T) | |
STTimestamp :: SingT ('TTimestamp :: T) | |
STAddress :: SingT ('TAddress :: T) | |
STChest :: SingT ('TChest :: T) | |
STChestKey :: SingT ('TChestKey :: T) | |
STSaplingState :: forall (n :: Nat). (Sing n) -> SingT ('TSaplingState n :: T) | |
STSaplingTransaction :: forall (n :: Nat). (Sing n) -> SingT ('TSaplingTransaction n :: T) | |
STNever :: SingT ('TNever :: T) |
Instances
(SDecide T, SDecide Peano) => TestCoercion SingT Source # | |
Defined in Morley.Michelson.Typed.Sing | |
(SDecide T, SDecide Peano) => TestEquality SingT Source # | |
Defined in Morley.Michelson.Typed.Sing | |
Show (SingT x) Source # | |
NFData (SingT a) Source # | |
Defined in Morley.Michelson.Typed.Sing | |
Eq (SingT x) Source # | |
Buildable (SingT t) Source # | |
Defined in Morley.Michelson.Typed.Sing |
castSingE :: forall (a :: T) (b :: T) t. (SingI a, SingI b) => t a -> Either Text (t b) Source #
Previously, we were using SingI
constraints in SingT
constructors. That was not so optimal because we have been
spending too much space at runtime. Instead of that, we process
values of SingT
using the function withSingI
in those places
where the SingI
constraint is required. withSingI
allows one
to create the SingI
context for a given Sing
.
castM :: forall (a :: T) (b :: T) t m. (SingI a, SingI b, Monad m) => t a -> (forall x. MismatchError T -> m x) -> m (t b) Source #
Monadic version of castSing
.
Throws an error using the given function if the cast fails.
requireEq :: forall (a :: T) (b :: T) m. (SingI a, SingI b, Monad m) => (forall x. MismatchError T -> m x) -> m (a :~: b) Source #
Monadic version of eqI
.
Throws an error using the given function if the two types are not equal.
eqP :: forall (a :: T) (b :: T). (SingI a, SingI b) => Proxy a -> Proxy b -> Maybe (a :~: b) Source #
data TPredicateSym Source #
Type-level symbol for type predicates used in ContainsT
PSOp | Contains |
PSContract | Contains |
PSTicket | Contains |
PSBigMap | Contains |
PSNestedBigMaps | Contains |
PSSaplingState | Contains |
PSNonComparable | Contains non-comparable types |
Instances
type ForbidNonComparable Source #
= ForbidT 'PSNonComparable | Convenience synonym |
type ForbidNestedBigMaps Source #
= ForbidT 'PSNestedBigMaps | Convenience synonym |
type ForbidBigMap Source #
type ForbidTicket Source #
type ForbidContract Source #
= ForbidT 'PSContract | Convenience synonym |
class ForbidManyT (ForbidT p t) '[p] t => ForbidT p t Source #
Constraint for classes forbidding type presence based on predicate defined
by TPredicateSym
.
Not just a type alias in order to be able to partially apply it (e.g. in
Each
).
Reports errors when a type does not satisfy predicate:
>>>
() :: ForbidT PSOp TOperation => ()
... ... Type `operation` found in ... 'TOperation ... is not allowed in this scope ...>>>
() :: ForbidT PSContract (TContract TUnit) => ()
... ... Type `contract` found in ... 'TContract 'TUnit ... is not allowed in this scope ...>>>
() :: ForbidT PSTicket (TTicket TUnit) => ()
... ... Type `ticket` found in ... 'TTicket 'TUnit ... is not allowed in this scope ...>>>
() :: ForbidT PSBigMap (TBigMap TUnit TUnit) => ()
... ... Type `big_map` found in ... 'TBigMap 'TUnit 'TUnit ... is not allowed in this scope ...>>>
() :: ForbidT PSSaplingState (TSaplingState Z) => ()
... ... Type `sapling_state` found in ... 'TSaplingState 'Z ... is not allowed in this scope ...>>>
() :: ForbidT PSNestedBigMaps (TBigMap TUnit (TBigMap TUnit TUnit)) => ()
... ... Nested `big_map`s found in ... 'TBigMap 'TUnit ('TBigMap 'TUnit 'TUnit) ... are not allowed ...
When the type is ambiguous or polymorphic, suggests adding the corresponding constraint:
>>>
(const () :: ForbidOp t => f t -> ()) undefined
... ... Can't check if type ... t0 ... contains `operation`. Perhaps you need to add ... ForbidT 'PSOp t0 ... constraint? You can also try adding a type annotation. ...
This constraint implies ContainsT ~ False
:
>>>
:{
foo :: ForbidT p t => ContainsT p t :~: False foo = Refl :}
Instances
type family ContainsT p t where ... Source #
data SingTPredicateSym :: TPredicateSym -> Type where Source #
Instances
TestCoercion SingTPredicateSym Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.ForbidT testCoercion :: forall (a :: k) (b :: k). SingTPredicateSym a -> SingTPredicateSym b -> Maybe (Coercion a b) # | |
TestEquality SingTPredicateSym Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.ForbidT testEquality :: forall (a :: k) (b :: k). SingTPredicateSym a -> SingTPredicateSym b -> Maybe (a :~: b) # |
data TPresence p t where Source #
Whether a value of this type _may_ contain a type defined by TPredicateSym
.
TPresent :: ContainsT p t ~ 'True => TPresence p t | |
TAbsent :: ContainsT p t ~ 'False => TPresence p t |
pattern SaplingStateAbsent :: () => ContainsSaplingState t ~ 'False => SaplingStatePresence t | Deprecated: Use TPresence instead |
pattern SaplingStatePresent :: () => ContainsSaplingState t ~ 'True => SaplingStatePresence t | Deprecated: Use TPresence instead |
pattern NestedBigMapsAbsent :: () => ContainsNestedBigMaps t ~ 'False => NestedBigMapsPresence t | Deprecated: Use TPresence instead |
pattern NestedBigMapsPresent :: () => ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresence t | Deprecated: Use TPresence instead |
pattern BigMapAbsent :: () => ContainsBigMap t ~ 'False => BigMapPresence t | Deprecated: Use TPresence instead |
pattern BigMapPresent :: () => ContainsBigMap t ~ 'True => BigMapPresence t | Deprecated: Use TPresence instead |
pattern TicketAbsent :: () => ContainsTicket t ~ 'False => TicketPresence t | Deprecated: Use TPresence instead |
pattern TicketPresent :: () => ContainsTicket t ~ 'True => TicketPresence t | Deprecated: Use TPresence instead |
pattern ContractAbsent :: () => ContainsContract t ~ 'False => ContractPresence t | Deprecated: Use TPresence instead |
pattern ContractPresent :: () => ContainsContract t ~ 'True => ContractPresence t | Deprecated: Use TPresence instead |
pattern OpPresent :: () => ContainsOp t ~ 'True => OpPresence t | Deprecated: Use TPresence instead |
pattern OpAbsent :: () => ContainsOp t ~ 'False => OpPresence t | Deprecated: Use TPresence instead |
checkTPresence :: forall p ty. Sing p -> Sing ty -> TPresence p ty Source #
Check for presence of type defined by TPredicateSym
at runtime. Use
TPredicateSym
singletons (i.e. SingTPredicateSym
) as the first parameter,
e.g.:
>>>
checkTPresence SPSOp STOperation
TPresent>>>
checkTPresence SPSOp STUnit
TAbsent
To only prove absence of some type, it is more efficient to use
deMorganForbidT
or withDeMorganScope
.
class (SingI t, RecSuperC Comparable t, ForbidNonComparable t) => Comparable t Source #
Instances
(SingI t, RecSuperC Comparable t, ForbidNonComparable t) => Comparable t Source # | |
SingI t => CheckScope (Comparable t) Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.CheckScope checkScope :: Either BadTypeForScope (Dict (Comparable t)) Source # |
data Comparability t where Source #
CanBeCompared :: (Comparable t, ComparabilityImplies t) => Comparability t | |
CannotBeCompared :: ContainsT 'PSNonComparable t ~ 'True => Comparability t |
Instances
Show (Comparability t) Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.Comparable showsPrec :: Int -> Comparability t -> ShowS # show :: Comparability t -> String # showList :: [Comparability t] -> ShowS # |
comparableImplies :: forall t proxy. ForbidNonComparable t => proxy t -> Dict (ComparabilityImplies t) Source #
Produce ComparabilityImplies
on demand. Carrying it as Comparable
superclasses turns out to be a little expensive, considering we can produce
evidence on demand in O(1).
checkComparability :: Sing t -> Comparability t Source #
Check if type is comparable or not at runtime. This traverses the
singleton, so it has a considerable runtime cost. If you just need to convince
GHC, you may be looking for comparableImplies
, or perhaps
withDeMorganScope
.
>>>
checkComparability STOperation
CannotBeCompared>>>
checkComparability STAddress
CanBeCompared
comparabilityPresence :: Sing t -> Maybe (Dict (Comparable t)) Source #
Check if type is comparable or not at runtime. This is a Dict
version of
checkComparability
, so the same caveats apply.
>>>
comparabilityPresence STOperation
Nothing>>>
comparabilityPresence STAddress
Just Dict
data NotWellTyped Source #
Error type for when a value is not well-typed.
Instances
Buildable NotWellTyped Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.WellTyped build :: NotWellTyped -> Doc buildList :: [NotWellTyped] -> Doc |
class (SingI t, RecSuperC WellTyped t, WellTypedConstraints t) => WellTyped t Source #
This class encodes Michelson rules w.r.t where it requires comparable
types. Earlier we had a dedicated type for representing comparable types CT
.
But then we integreated those types into T
. This meant that some of the
types that could be formed with various combinations of T
would be
illegal as per Michelson typing rule. Using this class, we inductively
enforce that a type and all types it contains are well typed as per
Michelson's rules.
Instances
(SingI t, RecSuperC WellTyped t, WellTypedConstraints t) => WellTyped t Source # | |
SingI t => CheckScope (WellTyped t) Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.CheckScope checkScope :: Either BadTypeForScope (Dict (WellTyped t)) Source # |
data BadTypeForScope Source #
BtNotComparable | |
BtIsOperation | |
BtHasBigMap | |
BtHasNestedBigMap | |
BtHasContract | |
BtHasTicket | |
BtHasSaplingState |
Instances
getWTP :: forall t. SingI t => Either NotWellTyped (Dict (WellTyped t)) Source #
Given a type, provide evidence that it is well typed w.r.t to the Michelson rules regarding where comparable types are required.
>>>
either pretty print $ getWTP @'TUnit
Dict>>>
either pretty print $ getWTP @('TSet 'TOperation)
Given type is not well typed because 'operation' is not comparable>>>
type Pairs a = 'TPair a a
>>>
type Pairs2 = Pairs (Pairs 'TUnit)
>>>
either pretty print $ getWTP @('TSet ('TPair Pairs2 'TOperation))
Given type is not well typed because pair (pair (pair unit unit) unit unit) operation is not comparable
class ComparabilityScopeC (ComparabilityScope t) t => ComparabilityScope t Source #
Alias for comparable types.
On ambiguous or polymorphic types, suggests adding the constraint:
>>>
(const () :: ComparabilityScope t => f t -> ()) undefined
... ... Can't check if type ... t0 ... contains non-comparable types. Perhaps you need to add ... ComparabilityScope t0 ... constraint? You can also try adding a type annotation. ...
Instances
ComparabilityScopeC (ComparabilityScope t) t => ComparabilityScope t Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.Scopes | |
SingI t => CheckScope (ComparabilityScope t) Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.CheckScope checkScope :: Either BadTypeForScope (Dict (ComparabilityScope t)) Source # |
class UntypedValScopeC (UntypedValScope t) t => UntypedValScope t Source #
Alias for constraints which are required for untyped representation.
On ambiguous or polymorphic types, suggests adding the constraint:
>>>
(const () :: UntypedValScope t => f t -> ()) undefined
... ... Can't check if type ... t0 ... contains `operation`. Perhaps you need to add ... UntypedValScope t0 ... constraint? You can also try adding a type annotation. ...
Instances
UntypedValScopeC (UntypedValScope t) t => UntypedValScope t Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.Scopes |
class ViewableScopeC (ViewableScope t) t => ViewableScope t Source #
Set of constraints that Michelson applies to argument type and return type of views. All info related to views can be found in [TZIP](https:/gitlab.comtezostzip-blobmasterdraftscurrent/draft_views.md).
Not just a type alias in order to be able to partially apply it.
On ambiguous or polymorphic types, suggests adding the constraint:
>>>
(const () :: ViewableScope t => f t -> ()) undefined
... ... Can't check if type ... t0 ... contains `operation`, `big_map` or `ticket`. Perhaps you need to add ... ViewableScope t0 ... constraint? You can also try adding a type annotation. ...
Instances
ViewableScopeC (ViewableScope t) t => ViewableScope t Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.Scopes | |
SingI t => CheckScope (ViewableScope t) Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.CheckScope checkScope :: Either BadTypeForScope (Dict (ViewableScope t)) Source # |
class UnpackedValScopeC (UnpackedValScope t) t => UnpackedValScope t Source #
Set of constraints that Michelson applies to unpacked values.
Same as ConstantScope
.
Not just a type alias in order to show better errors on ambiguity or missing constraint.
On ambiguous or polymorphic types, suggests adding the constraint:
>>>
(const () :: UnpackedValScope t => f t -> ()) undefined
... ... Can't check if type ... t0 ... contains `operation`, `big_map`, `contract`, `ticket` or `sapling_state`. Perhaps you need to add ... UnpackedValScope t0 ... constraint? You can also try adding a type annotation. ...
Instances
UnpackedValScopeC (UnpackedValScope t) t => UnpackedValScope t Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.Scopes | |
SingI t => CheckScope (UnpackedValScope t) Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.CheckScope checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t)) Source # |
class PackedValScopeC (PackedValScope t) t => PackedValScope t Source #
Set of constraints that Michelson applies to packed values.
Not just a type alias in order to be able to partially apply it.
On ambiguous or polymorphic types, suggests adding the constraint:
>>>
(const () :: PackedValScope t => f t -> ()) undefined
... ... Can't check if type ... t0 ... contains `operation`, `big_map`, `ticket` or `sapling_state`. Perhaps you need to add ... PackedValScope t0 ... constraint? You can also try adding a type annotation. ...
Instances
PackedValScopeC (PackedValScope t) t => PackedValScope t Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.Scopes | |
(WithDeMorganScope ForbidOp t a b, WithDeMorganScope ForbidBigMap t a b, WithDeMorganScope ForbidTicket t a b, WithDeMorganScope ForbidSaplingState t a b, WellTyped a, WellTyped b) => WithDeMorganScope PackedValScope t a b Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope withDeMorganScope :: PackedValScope (t a b) => ((PackedValScope a, PackedValScope b) => ret) -> ret Source # | |
SingI t => CheckScope (PackedValScope t) Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.CheckScope checkScope :: Either BadTypeForScope (Dict (PackedValScope t)) Source # |
type family IsDupableScope (t :: T) :: Bool where ... Source #
Returns whether the type is dupable.
IsDupableScope t = Not (ContainsT 'PSTicket t) |
class DupableScopeC (DupableScope t) t => DupableScope t Source #
Alias for constraints which Michelson requires in DUP
instruction.
On ambiguous or polymorphic types, suggests adding the constraint:
>>>
(const () :: DupableScope t => f t -> ()) undefined
... ... Can't check if type ... t0 ... contains `ticket`. Perhaps you need to add ... DupableScope t0 ... constraint? You can also try adding a type annotation. ...
Instances
DupableScopeC (DupableScope t) t => DupableScope t Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.Scopes | |
SingI t => CheckScope (DupableScope t) Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.CheckScope checkScope :: Either BadTypeForScope (Dict (DupableScope t)) Source # |
class ConstantScopeC (ConstantScope t) t => ConstantScope t Source #
Set of constraints that Michelson applies to pushed constants.
Not just a type alias in order to be able to partially apply it
On ambiguous or polymorphic types, suggests adding the constraint:
>>>
(const () :: ConstantScope t => f t -> ()) undefined
... ... Can't check if type ... t0 ... contains `operation`, `big_map`, `contract`, `ticket` or `sapling_state`. Perhaps you need to add ... ConstantScope t0 ... constraint? You can also try adding a type annotation. ...
Instances
ConstantScopeC (ConstantScope t) t => ConstantScope t Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.Scopes | |
(WithDeMorganScope ForbidOp t a b, WithDeMorganScope ForbidBigMap t a b, WithDeMorganScope ForbidContract t a b, WithDeMorganScope ForbidTicket t a b, WithDeMorganScope ForbidSaplingState t a b, WellTyped a, WellTyped b) => WithDeMorganScope ConstantScope t a b Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope withDeMorganScope :: ConstantScope (t a b) => ((ConstantScope a, ConstantScope b) => ret) -> ret Source # | |
SingI t => CheckScope (ConstantScope t) Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.CheckScope checkScope :: Either BadTypeForScope (Dict (ConstantScope t)) Source # |
class StorageScopeC (StorageScope t) t => StorageScope t Source #
Set of constraints that Michelson applies to contract storage.
Not just a type alias in order to be able to partially apply it
Produces human-readable error messages:
>>>
() :: StorageScope (TContract TOperation) => ()
... ... Type `contract` found in ... 'TContract 'TOperation ... is not allowed in this scope ... ... Type `operation` found in ... 'TOperation ... is not allowed in this scope ...>>>
() :: StorageScope TUnit => ()
()
On ambiguous or polymorphic types, suggests adding the constraint:
>>>
(const () :: StorageScope t => f t -> ()) undefined
... ... Can't check if type ... t0 ... contains `operation`, nested `big_map`s or `contract`. Perhaps you need to add ... StorageScope t0 ... constraint? You can also try adding a type annotation. ...
Instances
StorageScopeC (StorageScope t) t => StorageScope t Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.Scopes | |
(WithDeMorganScope ForbidOp t a b, WithDeMorganScope ForbidNestedBigMaps t a b, WithDeMorganScope ForbidContract t a b, WellTyped a, WellTyped b) => WithDeMorganScope StorageScope t a b Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope withDeMorganScope :: StorageScope (t a b) => ((StorageScope a, StorageScope b) => ret) -> ret Source # | |
SingI t => CheckScope (StorageScope t) Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.CheckScope checkScope :: Either BadTypeForScope (Dict (StorageScope t)) Source # |
class ParameterScopeC (ParameterScope t) t => ParameterScope t Source #
Set of constraints that Michelson applies to parameters.
Not just a type alias in order to be able to partially apply it
Produces human-readable error messages:
>>>
() :: ParameterScope (TBigMap TUnit (TBigMap TUnit TOperation)) => ()
... ... Nested `big_map`s found in ... 'TBigMap 'TUnit ('TBigMap 'TUnit 'TOperation) ... are not allowed ... ... Type `operation` found in ... 'TBigMap 'TUnit ('TBigMap 'TUnit 'TOperation) ... is not allowed in this scope ...>>>
() :: ParameterScope (TBigMap TInt TNat) => ()
()
On ambiguous or polymorphic types, suggests adding the constraint:
>>>
(const () :: ParameterScope t => f t -> ()) undefined
... ... Can't check if type ... t0 ... contains `operation` or nested `big_map`s. Perhaps you need to add ... ParameterScope t0 ... constraint? You can also try adding a type annotation. ...
Instances
ParameterScopeC (ParameterScope t) t => ParameterScope t Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.Scopes | |
(WithDeMorganScope ForbidOp t a b, WithDeMorganScope ForbidNestedBigMaps t a b, WellTyped a, WellTyped b) => WithDeMorganScope ParameterScope t a b Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope withDeMorganScope :: ParameterScope (t a b) => ((ParameterScope a, ParameterScope b) => ret) -> ret Source # | |
SingI t => CheckScope (ParameterScope t) Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.CheckScope checkScope :: Either BadTypeForScope (Dict (ParameterScope t)) Source # |
class WithDeMorganScope (c :: T -> Constraint) t a b where Source #
Allows using a scope that can be proven true with a De Morgan law.
Many scopes are defined as not a
(or rather a ~ 'False
) where a
is a
negative property we want to avoid as a Constraint
.
The negative constraints are implemented with a type family that for some
combination types resolves to itself applied to the type arguments in an or
,
e.g. A pair l r
has x
if l
or r
contain x
.
Because of the De Morgan laws not (a or b)
implies (not a) and (not b)
or in our case: pair
does not contain x
-> a
and b
don't contain x
.
withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret Source #
Instances
deMorganForbidT :: forall a b r p. (ContainsT p a || ContainsT p b) ~ 'False => Sing p -> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r Source #
Simpler version of withDeMorganScope
for ForbidT
constraints.
type IsComparable t = Not (ContainsT 'PSNonComparable t) Source #
Deprecated: Use 'Not (ContainsT PSNonComparable t)' instead
type ProperNonComparableValBetterErrors t = (SingI t, ForbidNonComparable t) Source #
Deprecated: Use *Scope instead
type ProperUntypedValBetterErrors t = (SingI t, ForbidOp t) Source #
Deprecated: Use *Scope instead
type ProperViewableBetterErrors t = (SingI t, ForbidOp t, ForbidBigMap t, ForbidTicket t) Source #
Deprecated: Use *Scope instead
type ProperUnpackedValBetterErrors t = (ProperPackedValBetterErrors t, ProperConstantBetterErrors t) Source #
Deprecated: Use *Scope instead
type ProperPackedValBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidTicket t, ForbidSaplingState t) Source #
Deprecated: Use *Scope instead
type ProperDupableBetterErrors t = (SingI t, ForbidTicket t) Source #
Deprecated: Use *Scope instead
type ProperConstantBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidContract t, ForbidTicket t, ForbidSaplingState t) Source #
Deprecated: Use *Scope instead
type ProperStorageBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t) Source #
Deprecated: Use *Scope instead
type ProperParameterBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t) Source #
Deprecated: Use *Scope instead
type NestedBigMapsPresence (t :: T) = TPresence 'PSNestedBigMaps t Source #
Deprecated: Use TPresence instead
Whether a value of this type _may_ contain nested big_map
s.
type BigMapPresence (t :: T) = TPresence 'PSBigMap t Source #
Deprecated: Use TPresence instead
Whether a value of this type _may_ contain a big_map
value.
type TicketPresence (t :: T) = TPresence 'PSTicket t Source #
Deprecated: Use TPresence instead
Whether a value of this type _may_ contain a ticket
value.
type ContractPresence (t :: T) = TPresence 'PSContract t Source #
Deprecated: Use TPresence instead
Whether a value of this type _may_ contain a contract
value.
type OpPresence (t :: T) = TPresence 'PSOp t Source #
Deprecated: Use TPresence instead
Whether a value of this type _may_ contain an operation.
class ContainsNestedBigMaps t ~ 'False => HasNoNestedBigMaps t Source #
Deprecated: Use Forbid* instead
Constraint which ensures that there are no nested bigmaps.
Instances
ContainsNestedBigMaps t ~ 'False => HasNoNestedBigMaps t Source # | |
class ContainsBigMap t ~ 'False => HasNoBigMap t Source #
Deprecated: Use Forbid* instead
Constraint which ensures that a value of type t
does not contain big_map
values.
Instances
ContainsBigMap t ~ 'False => HasNoBigMap t Source # | |
class ContainsTicket t ~ 'False => HasNoTicket t Source #
Deprecated: Use Forbid* instead
Constraint which ensures that a value of type t
does not contain ticket
values.
Instances
ContainsTicket t ~ 'False => HasNoTicket t Source # | |
class ContainsContract t ~ 'False => HasNoContract t Source #
Deprecated: Use Forbid* instead
Constraint which ensures that a value of type t
does not contain contract
values.
Instances
ContainsContract t ~ 'False => HasNoContract t Source # | |
class ContainsOp t ~ 'False => HasNoOp t Source #
Deprecated: Use Forbid* instead
Constraint which ensures that a value of type t
does not contain operations.
Not just a type alias in order to be able to partially apply it
(e.g. in Each
).
Instances
ContainsOp t ~ 'False => HasNoOp t Source # | |
type ContainsNestedBigMaps t = ContainsT 'PSNestedBigMaps t Source #
Deprecated: Use ContainsT
with the corresponding type marker, e.g. 'ContainsT PSOp', 'ContainsT PSTicket', etc
Whether a value of this type _may_ contain nested big_map
s.
Nested big_maps (i.e. big_map which contains another big_map inside of it's value type) are prohibited in all contexts. Some context such as PUSH, APPLY, PACK/UNPACK instructions are more strict because they don't work with big_map at all.
type ContainsBigMap t = ContainsT 'PSBigMap t Source #
Deprecated: Use ContainsT
with the corresponding type marker, e.g. 'ContainsT PSOp', 'ContainsT PSTicket', etc
Whether a value of this type _may_ contain a big_map
value.
type ContainsTicket t = ContainsT 'PSTicket t Source #
Deprecated: Use ContainsT
with the corresponding type marker, e.g. 'ContainsT PSOp', 'ContainsT PSTicket', etc
Whether a value of this type _may_ contain a ticket
value.
type ContainsContract t = ContainsT 'PSContract t Source #
Deprecated: Use ContainsT
with the corresponding type marker, e.g. 'ContainsT PSOp', 'ContainsT PSTicket', etc
Whether a value of this type _may_ contain a contract
value.
In some scopes (constants, storage) appearing for contract type is prohibited. Contracts in input/output of lambdas are allowed without limits though.
type ContainsOp t = ContainsT 'PSOp t Source #
Deprecated: Use ContainsT
with the corresponding type marker, e.g. 'ContainsT PSOp', 'ContainsT PSTicket', etc
Whether a value of this type _may_ contain an operation.
In some scopes (constants, parameters, storage) appearing for operation type is prohibited. Operations in input/output of lambdas are allowed without limits though.
checkOpPresence :: Sing (ty :: T) -> TPresence 'PSOp ty Source #
Deprecated: Use checkTPresence instead
Check at runtime whether a value of the given type _may_ contain an operation.
checkContractTypePresence :: Sing (ty :: T) -> TPresence 'PSContract ty Source #
Deprecated: Use checkTPresence instead
Check at runtime whether a value of the given type _may_ contain a contract
value.
checkTicketPresence :: Sing (ty :: T) -> TPresence 'PSTicket ty Source #
Deprecated: Use checkTPresence instead
Check at runtime whether a value of the given type _may_ contain a ticket
value.
checkBigMapPresence :: Sing (ty :: T) -> TPresence 'PSBigMap ty Source #
Deprecated: Use checkTPresence instead
Check at runtime whether a value of the given type _may_ contain a big_map
value.
checkNestedBigMapsPresence :: Sing (ty :: T) -> TPresence 'PSNestedBigMaps ty Source #
Deprecated: Use checkTPresence instead
Check at runtime whether a value of the given type _may_ contain nested big_map
s.
opAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidOp t) Source #
Deprecated: Use tAbsence instead
Check at runtime that a value of the given type cannot contain operations.
contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidContract t) Source #
Deprecated: Use tAbsence instead
Check at runtime that a value of the given type cannot contain contract
values.
bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidBigMap t) Source #
Deprecated: Use tAbsence instead
Check at runtime that a value of the given type cannot containt big_map
values
nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidNestedBigMaps t) Source #
Deprecated: Use tAbsence instead
Check at runtime that a value of the given type cannot contain nested big_map
s.
comparabilityImpliesNoNestedBigMaps :: forall t. (SingI t, IsComparable t ~ 'True) => ContainsNestedBigMaps t :~: 'False Source #
Deprecated: Already implied by Comparable constraint
Inductive proof that Comparable
implies HasNoNestedBigMaps
. This is
stubbed with an unsafeCoerce Refl
at runtime to avoid runtime traversals.
comparabilityImpliesNoOp :: forall t. (SingI t, IsComparable t ~ 'True) => ContainsOp t :~: 'False Source #
Deprecated: Already implied by Comparable constraint
Inductive proof that Comparable
implies HasNoOp
. This is
stubbed with an unsafeCoerce Refl
at runtime to avoid runtime traversals.
getComparableProofS :: Sing (a :: T) -> Maybe (Dict (Comparable a)) Source #
Deprecated: Use comparabilityPresence
class CheckScope (c :: Constraint) where Source #
Should be present for common scopes.
checkScope :: Either BadTypeForScope (Dict c) Source #
Check that constraint hold for a given type.
Instances
type FieldDescriptions = [(Symbol, (Maybe Symbol, [(Symbol, Symbol)]))] Source #
Description of constructors and fields of some datatype.
This type is just two nested maps represented as associative lists. It is supposed to be interpreted like this:
[(Constructor name, (Maybe constructor description, [(Field name, Field description)]))]
Example with a concrete data type:
data Foo = Foo { fFoo :: Int } | Bar { fBar :: Text } deriving (Generic) type FooDescriptions = '[ '( "Foo", '( 'Just "foo constructor", , '[ '("fFoo", "some number") ]) ) , '( "Bar", '( 'Nothing, , '[ '("fBar", "some string") ]) ) ]
Entrypoint name.
There are two properties we care about:
- Special treatment of the
default
entrypoint name.default
is prohibited in theCONTRACT
instruction and in values ofaddress
andcontract
types. However, it is not prohibited in theSELF
instruction. Hence, the value insideEpName
can be"default"
, so that we can distinguishSELF
andSELF %default
. It is important to distinguish them because their binary representation that is inserted into blockchain is different. For example, typecheckingSELF %default
consumes more gas thanSELF
. In this module, we provide several smart constructors with different handling ofdefault
, please use the appropriate one for your use case. - The set of permitted characters. Intuitively, an entrypoint name should
be valid only if it is a valid annotation (because entrypoints are defined
using field annotations). However, it is not enforced in Tezos.
It is not clear whether this behavior is intended. There is an upstream
issue which received
bug
label, so probably it is considered a bug. Currently we treat it as a bug and deviate from upstream implementation by probiting entrypoint names that are not valid annotations. If Tezos developers fix it soon, we will be happy. If they don't, we should (maybe temporarily) remove this limitation from our code. There is an issue in our repo as well.
Instances
FromJSON EpName Source # | |
ToJSON EpName Source # | |
Defined in Morley.Michelson.Untyped.Entrypoints | |
Generic EpName Source # | |
Show EpName Source # | |
NFData EpName Source # | |
Defined in Morley.Michelson.Untyped.Entrypoints | |
Eq EpName Source # | |
Ord EpName Source # | |
HasCLReader EpName Source # | |
Defined in Morley.Michelson.Untyped.Entrypoints | |
Buildable EpName Source # | |
Defined in Morley.Michelson.Untyped.Entrypoints | |
type Rep EpName Source # | |
Defined in Morley.Michelson.Untyped.Entrypoints |
data HandleImplicitDefaultEp Source #
A simple enum flag to choose how to handle implicit default entrypoint in
mkEntrypointsMap
.
WithoutImplicitDefaultEp | Omit the default entrypoint unless it's specified explicitly. |
WithImplicitDefaultEp | Include the default entrypoint even if it's not specified explicitly. This produces exactly the full set of entrypoints as per Michelson spec. |
Instances
data EpNameFromRefAnnError Source #
Instances
pattern DefEpName :: EpName Source #
This is a bidirectional pattern that can be used for two purposes:
- Construct an
EpName
referring to the default entrypoint. - Use it in pattern-matching or in equality comparison to check whether
EpName
refers to the default entrypoint. This is trickier because there are two possibleEpName
values referring to the default entrypoints.DefEpName
will match only the most common one (no entrypoint). However, there is a special case:SELF
instruction can have explicit%default
reference. For this reason, it is recommended to useisDefEpName
instead. Pattern-matching onDefEpName
is still permitted for backwards compatibility and for the cases when you are sure thatEpName
does not come from theSELF
instruction.
epNameToParamAnn :: EpName -> FieldAnn Source #
Turn entrypoint name into annotation for contract parameter declaration.
epNameFromRefAnn :: FieldAnn -> Either EpNameFromRefAnnError EpName Source #
Make up EpName
from annotation which is reference to an entrypoint.
Note that it's more common for Michelson to prohibit explicit default
entrypoint reference.
Specifically, %default
annotation is probitited in values of address
and contract
types. It's also prohibited in the CONTRACT
instruction.
However, there is an exception: SELF %default
is a perfectly valid
instruction. Hence, when you construct an EpName
from an annotation
that's part of SELF
, you should use epNameFromSelfAnn
instead.
epNameToRefAnn :: EpName -> FieldAnn Source #
Turn entrypoint name into annotation used as reference to entrypoint.
Name of the view.
- It must not exceed 31 chars length;
- Must use [a-zA-Z0-9_.%@] charset.
Instances
data BadViewNameError Source #
Instances
mkViewName :: Text -> Either BadViewNameError ViewName Source #
Construct ViewName
performing all the checks.
viewNameToMText :: ViewName -> MText Source #
Valid view names form a subset of valid Michelson texts.
data ViewsSetError Source #
Errors possible when constructing ViewsSet
.
Instances
Show ViewsSetError Source # | |
Defined in Morley.Michelson.Internal.ViewsSet showsPrec :: Int -> ViewsSetError -> ShowS # show :: ViewsSetError -> String # showList :: [ViewsSetError] -> ShowS # | |
Eq ViewsSetError Source # | |
Defined in Morley.Michelson.Internal.ViewsSet (==) :: ViewsSetError -> ViewsSetError -> Bool # (/=) :: ViewsSetError -> ViewsSetError -> Bool # | |
Buildable ViewsSetError Source # | |
Defined in Morley.Michelson.Internal.ViewsSet build :: ViewsSetError -> Doc buildList :: [ViewsSetError] -> Doc |
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
.
Instances
Lift (Notes t :: Type) Source # | |
Show (Notes t) Source # | |
(SingI t, Default (Anns xs)) => Default (Anns (Notes t ': xs)) Source # | |
Defined in Morley.Michelson.Typed.Annotation | |
NFData (Notes t) Source # | |
Defined in Morley.Michelson.Typed.Annotation | |
Eq (Notes t) Source # | |
ToExpression (Notes t) Source # | |
Defined in Morley.Micheline.Class toExpression :: Notes t -> Expression Source # | |
RenderDoc (Notes t) Source # | |
Defined in Morley.Michelson.Typed.Annotation renderDoc :: RenderContext -> Notes t -> Doc Source # isRenderable :: Notes t -> Bool Source # | |
AnnotateInstr xs r => AnnotateInstr (Notes t ': xs) r Source # | |
Defined in Morley.Michelson.Typed.Annotation |
A typed heterogenous list of annotations. Simplified pattern synonyms for common use cases are provided.
AnnsCons :: Typeable tag => !(Annotation tag) -> Anns xs -> Anns (Annotation tag ': xs) infixr 5 | |
AnnsTyCons :: SingI t => !(Notes t) -> Anns xs -> Anns (Notes t ': xs) infixr 5 | |
AnnsNil :: Anns '[] |
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] | Convenience pattern synonym matching five annotations, first four being
simple, the last one being |
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] | Convenience pattern synonym matching four annotations, first two being
simple, the last two being |
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] | Convenience pattern synonym matching four simple annotations. |
pattern Anns3'' :: (Typeable a, SingI t, SingI u) => Annotation a -> Notes t -> Notes u -> Anns '[Annotation a, Notes t, Notes u] | Convenience pattern synonym matching three annotations, first being
a simple one, the last two being |
pattern Anns3' :: (Each '[Typeable] '[a, b], SingI t) => Annotation a -> Annotation b -> Notes t -> Anns '[Annotation a, Annotation b, Notes t] | Convenience pattern synonym matching three annotations, first two being
simple, the last one being |
pattern Anns3 :: Each '[Typeable] '[a, b, c] => Annotation a -> Annotation b -> Annotation c -> Anns '[Annotation a, Annotation b, Annotation c] | Convenience pattern synonym matching three simple annotations. |
pattern Anns2' :: (Typeable a, SingI t) => Annotation a -> Notes t -> Anns '[Annotation a, Notes t] | Convenience pattern synonym matching two annotations, first being
a simple one, the second being |
pattern Anns1 :: Typeable a => Annotation a -> Anns '[Annotation a] | Convenience pattern synonym matching a single simple annotation. |
pattern Anns2 :: Each '[Typeable] '[a, b] => Annotation a -> Annotation b -> Anns '[Annotation a, Annotation b] | Convenience pattern synonym matching two simple annotations. |
Instances
Each '[Show] rs => Show (Anns rs) Source # | |
(SingI t, Default (Anns xs)) => Default (Anns (Notes t ': xs)) Source # | |
Defined in Morley.Michelson.Typed.Annotation | |
(Typeable tag, Default (Anns xs)) => Default (Anns (Annotation tag ': xs)) Source # | |
Defined in Morley.Michelson.Typed.Annotation def :: Anns (Annotation tag ': xs) # | |
Default (Anns ('[] :: [Type])) Source # | |
Defined in Morley.Michelson.Typed.Annotation | |
NFData (Anns xs) Source # | |
Defined in Morley.Michelson.Typed.Annotation | |
(Eq r, Eq (Anns rs)) => Eq (Anns (r ': rs)) Source # | |
Eq (Anns ('[] :: [Type])) Source # | |
notesSing :: Notes t -> Sing t Source #
Forget information about annotations, pick singleton with the same type.
starNotes :: forall t. SingI t => Notes t Source #
In memory of NStar
constructor.
Generates notes with no annotations.
insertTypeAnn :: forall (b :: T). TypeAnn -> Notes b -> Notes b Source #
Insert the provided type annotation into the provided notes.
class AnnotateInstr (xs :: [Type]) r where Source #
Utility typeclass to simplify extracting annotations from Anns
and
passing those as arguments to an untyped instruction data constructor.
annotateInstr :: Anns xs -> AnnotateInstrArg xs r -> r Source #
Instances
AnnotateInstr ('[] :: [Type]) r Source # | |
Defined in Morley.Michelson.Typed.Annotation annotateInstr :: Anns '[] -> AnnotateInstrArg '[] r -> r Source # | |
AnnotateInstr xs r => AnnotateInstr (Notes t ': xs) r Source # | |
Defined in Morley.Michelson.Typed.Annotation | |
AnnotateInstr xs r => AnnotateInstr (Annotation tag ': xs) r Source # | |
Defined in Morley.Michelson.Typed.Annotation annotateInstr :: Anns (Annotation tag ': xs) -> AnnotateInstrArg (Annotation tag ': xs) r -> r Source # |
pattern AsUType :: () => SingI t => Notes t -> Ty Source #
Transparently represent untyped Ty
as wrapper over Notes t
from typed world with SingI t
constraint.
As expression this carries logic of mkUType
, and as pattern it performs
withUType
but may make code a bit cleaner.
Note about constraints: pattern signatures usually require two constraints -
one they require and another one which they provide. In our case we require
nothing (thus first constraint is ()
) and provide some knowledge about t
.
withUType :: Ty -> (forall t. SingI t => Notes t -> r) -> r Source #
Convert Ty
to the isomorphic set of information from typed world.
data SomeViewsSet' instr where Source #
SomeViewsSet :: SingI st => ViewsSet' instr st -> SomeViewsSet' instr |
Instances
(forall (i :: [T]) (o :: [T]). Show (instr i o)) => Show (SomeViewsSet' instr) Source # | |
Defined in Morley.Michelson.Typed.View showsPrec :: Int -> SomeViewsSet' instr -> ShowS # show :: SomeViewsSet' instr -> String # showList :: [SomeViewsSet' instr] -> ShowS # | |
(forall (i :: [T]) (o :: [T]). NFData (instr i o)) => NFData (SomeViewsSet' instr) Source # | |
Defined in Morley.Michelson.Typed.View rnf :: SomeViewsSet' instr -> () # | |
(forall (i :: [T]) (o :: [T]). Eq (instr i o)) => Eq (SomeViewsSet' instr) Source # | |
Defined in Morley.Michelson.Typed.View (==) :: SomeViewsSet' instr -> SomeViewsSet' instr -> Bool # (/=) :: SomeViewsSet' instr -> SomeViewsSet' instr -> Bool # |
newtype ViewsSet' instr st Source #
Views that belong to one contract.
ViewsSet | |
|
pattern UnsafeViewsSet :: Map ViewName (SomeView' instr st) -> ViewsSet' instr st | Deprecated: Use ViewsSet instead |
pattern ViewsList :: [SomeView' instr st] -> ViewsSet' instr st |
Instances
(forall (i :: [T]) (o :: [T]). Show (instr i o)) => Show (ViewsSet' instr st) Source # | |
Default (ViewsSet' instr st) Source # | |
Defined in Morley.Michelson.Typed.View | |
(forall (i :: [T]) (o :: [T]). NFData (instr i o)) => NFData (ViewsSet' instr st) Source # | |
Defined in Morley.Michelson.Typed.View | |
(forall (i :: [T]) (o :: [T]). Eq (instr i o)) => Eq (ViewsSet' instr st) Source # | |
Container (ViewsSet' instr st) Source # | |
Defined in Morley.Michelson.Typed.View toList :: ViewsSet' instr st -> [Element (ViewsSet' instr st)] # null :: ViewsSet' instr st -> Bool # foldr :: (Element (ViewsSet' instr st) -> b -> b) -> b -> ViewsSet' instr st -> b # foldl :: (b -> Element (ViewsSet' instr st) -> b) -> b -> ViewsSet' instr st -> b # foldl' :: (b -> Element (ViewsSet' instr st) -> b) -> b -> ViewsSet' instr st -> b # length :: ViewsSet' instr st -> Int # elem :: Element (ViewsSet' instr st) -> ViewsSet' instr st -> Bool # foldMap :: Monoid m => (Element (ViewsSet' instr st) -> m) -> ViewsSet' instr st -> m # fold :: ViewsSet' instr st -> Element (ViewsSet' instr st) # foldr' :: (Element (ViewsSet' instr st) -> b -> b) -> b -> ViewsSet' instr st -> b # notElem :: Element (ViewsSet' instr st) -> ViewsSet' instr st -> Bool # all :: (Element (ViewsSet' instr st) -> Bool) -> ViewsSet' instr st -> Bool # any :: (Element (ViewsSet' instr st) -> Bool) -> ViewsSet' instr st -> Bool # and :: ViewsSet' instr st -> Bool # or :: ViewsSet' instr st -> Bool # find :: (Element (ViewsSet' instr st) -> Bool) -> ViewsSet' instr st -> Maybe (Element (ViewsSet' instr st)) # safeHead :: ViewsSet' instr st -> Maybe (Element (ViewsSet' instr st)) # safeMaximum :: ViewsSet' instr st -> Maybe (Element (ViewsSet' instr st)) # safeMinimum :: ViewsSet' instr st -> Maybe (Element (ViewsSet' instr st)) # safeFoldr1 :: (Element (ViewsSet' instr st) -> Element (ViewsSet' instr st) -> Element (ViewsSet' instr st)) -> ViewsSet' instr st -> Maybe (Element (ViewsSet' instr st)) # safeFoldl1 :: (Element (ViewsSet' instr st) -> Element (ViewsSet' instr st) -> Element (ViewsSet' instr st)) -> ViewsSet' instr st -> Maybe (Element (ViewsSet' instr st)) # | |
type Element (ViewsSet' instr st) Source # | |
data SomeView' instr st where Source #
Instances
(forall (arg :: T) (ret :: T). Show (ViewCode' instr arg st ret)) => Show (SomeView' instr st) Source # | |
(forall (arg :: T) (ret :: T). NFData (ViewCode' instr arg st ret)) => NFData (SomeView' instr st) Source # | |
Defined in Morley.Michelson.Typed.View | |
(forall (arg :: T) (ret :: T). Eq (ViewCode' instr arg st ret)) => Eq (SomeView' instr st) Source # | |
data View' instr arg st ret Source #
Contract view.
(ViewableScope arg, SingI st, ViewableScope ret) => View | |
someViewName :: SomeView' instr st -> ViewName Source #
Obtain the name of the view.
mkViewsSet :: [SomeView' instr st] -> Either ViewsSetError (ViewsSet' instr st) Source #
Construct views set.
emptyViewsSet :: forall instr st. ViewsSet' instr st Source #
No views.
addViewToSet :: View' instr arg st ret -> ViewsSet' instr st -> Either ViewsSetError (ViewsSet' instr st) Source #
Add a view to set.
lookupView :: forall instr st. ViewName -> ViewsSet' instr st -> Maybe (SomeView' instr st) Source #
Find a view in the set.
viewsSetNames :: forall instr st. ViewsSet' instr st -> Set ViewName Source #
Get all taken names in views set.
data EpLiftSequence (arg :: T) (param :: T) where Source #
Describes how to construct full contract parameter from given entrypoint argument.
This could be just wrapper over Value arg -> Value param
, but we cannot
use Value
type in this module easily.
EplArgHere :: EpLiftSequence arg arg | |
EplWrapLeft :: (SingI subparam, SingI r) => EpLiftSequence arg subparam -> EpLiftSequence arg ('TOr subparam r) | |
EplWrapRight :: (SingI l, SingI subparam) => EpLiftSequence arg subparam -> EpLiftSequence arg ('TOr l subparam) |
Instances
Show (EpLiftSequence arg param) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints showsPrec :: Int -> EpLiftSequence arg param -> ShowS # show :: EpLiftSequence arg param -> String # showList :: [EpLiftSequence arg param] -> ShowS # | |
NFData (EpLiftSequence arg param) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints rnf :: EpLiftSequence arg param -> () # | |
Eq (EpLiftSequence arg param) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints (==) :: EpLiftSequence arg param -> EpLiftSequence arg param -> Bool # (/=) :: EpLiftSequence arg param -> EpLiftSequence arg param -> Bool # | |
Buildable (EpLiftSequence arg param) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints build :: EpLiftSequence arg param -> Doc buildList :: [EpLiftSequence arg param] -> Doc |
data ParamEpError Source #
Errors specific to parameter type declaration (entrypoints).
Instances
data ParamNotes (t :: T) Source #
Annotations for contract parameter declaration.
Following the Michelson specification, this type has the following invariants:
1. No entrypoint name is duplicated.
2. If default
entrypoint is explicitly assigned, no "arm" remains uncallable.
Instances
data ParseEpAddressError Source #
Instances
Address with optional entrypoint name attached to it.
EpAddress' | |
|
pattern EpAddress :: KindedAddress kind -> EpName -> EpAddress |
Instances
pattern ParamNotes :: Notes t -> RootAnn -> ParamNotes t Source #
formatEpAddress :: EpAddress -> Text Source #
mformatEpAddress :: EpAddress -> MText Source #
parseEpAddress :: Text -> Either ParseEpAddressError EpAddress Source #
Parse an address which can be suffixed with entrypoint name (e.g. "tz1faswCTDciRzE4oJ9jn2Vm2dvjeyA9fUzU%entrypoint").
parseEpAddressRaw :: ByteString -> Either ParseEpAddressError EpAddress Source #
Parses byte representation of entrypoint address.
For every address
KT1QbdJ7M7uAQZwLpvzerUyk7LYkJWDL7eDh%foo%bar
we get the following byte representation
01afab866e7f1e74f9bba388d66b246276ce50bf4700666f6f25626172 ______________________________________//__/____ address % ep1 % ep2
starParamNotes :: SingI t => ParamNotes t Source #
Parameter without annotations.
mkParamNotes :: Notes t -> RootAnn -> Either ParamEpError (ParamNotes t) Source #
Construct ParamNotes
performing all necessary checks.
data MkEntrypointCallRes param where Source #
MkEntrypointCallRes :: ParameterScope arg => Notes arg -> EntrypointCallT param arg -> MkEntrypointCallRes param |
data SomeEntrypointCallT (arg :: T) Source #
EntrypointCallT
with hidden parameter type.
This requires argument to satisfy ParameterScope
constraint.
Strictly speaking, entrypoint argument may one day start having different
set of constraints comparing to ones applied to parameter, but this seems
unlikely.
forall param.ParameterScope param => SomeEpc (EntrypointCallT param arg) |
Instances
Show (SomeEntrypointCallT arg) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints showsPrec :: Int -> SomeEntrypointCallT arg -> ShowS # show :: SomeEntrypointCallT arg -> String # showList :: [SomeEntrypointCallT arg] -> ShowS # | |
NFData (SomeEntrypointCallT arg) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints rnf :: SomeEntrypointCallT arg -> () # | |
Eq (SomeEntrypointCallT arg) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints (==) :: SomeEntrypointCallT arg -> SomeEntrypointCallT arg -> Bool # (/=) :: SomeEntrypointCallT arg -> SomeEntrypointCallT arg -> Bool # | |
Buildable (SomeEntrypointCallT arg) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints build :: SomeEntrypointCallT arg -> Doc buildList :: [SomeEntrypointCallT arg] -> Doc |
type family ForbidOr (t :: T) :: Constraint where ... Source #
data EntrypointCallT (param :: T) (arg :: T) Source #
Reference for calling a specific entrypoint of type arg
.
ParameterScope arg => EntrypointCall | |
|
Instances
Show (EntrypointCallT param arg) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints showsPrec :: Int -> EntrypointCallT param arg -> ShowS # show :: EntrypointCallT param arg -> String # showList :: [EntrypointCallT param arg] -> ShowS # | |
NFData (EntrypointCallT param arg) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints rnf :: EntrypointCallT param arg -> () # | |
Eq (EntrypointCallT param arg) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints (==) :: EntrypointCallT param arg -> EntrypointCallT param arg -> Bool # (/=) :: EntrypointCallT param arg -> EntrypointCallT param arg -> Bool # | |
Buildable (EntrypointCallT param arg) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints build :: EntrypointCallT param arg -> Doc buildList :: [EntrypointCallT param arg] -> Doc |
unsafeEpcCallRoot :: ParameterScope param => EntrypointCallT param param Source #
Construct EntrypointCallT
which calls no entrypoint and assumes that
there is no explicit "default" one.
Validity of such operation is not ensured.
epcPrimitive :: forall p. (ParameterScope p, ForbidOr p) => EntrypointCallT p p Source #
Call parameter which has no entrypoints, always safe.
unsafeSepcCallRoot :: ParameterScope param => SomeEntrypointCallT param Source #
Construct SomeEntrypointCallT
which calls no entrypoint and assumes that
there is no explicit "default" one.
Validity of such operation is not ensured.
sepcPrimitive :: forall t. (ParameterScope t, ForbidOr t) => SomeEntrypointCallT t Source #
Call parameter which has no entrypoints, always safe.
sepcName :: SomeEntrypointCallT arg -> EpName Source #
mkEntrypointCall :: ParameterScope param => EpName -> ParamNotes param -> Maybe (MkEntrypointCallRes param) Source #
Build EntrypointCallT
.
Here we accept entrypoint name and type information for the parameter of target contract.
Returns Nothing
if entrypoint is not found.
Prefer using mkDefEntrypointCall
for the default entrypoint.
mkDefEntrypointCall :: ParameterScope param => ParamNotes param -> MkEntrypointCallRes param Source #
Build EntrypointCallT
calling the default entrypoint. Unlike
mkEntrypointCall
, always succeeds.
tyImplicitAccountParam :: ParamNotes 'TUnit Source #
parameter
type of implicit account.
data Contract' instr cp st Source #
Typed contract and information about annotations which is not present in the contract code.
(ParameterScope cp, StorageScope st) => Contract | |
|
Instances
ToExpression (Contract cp st) Source # | |
Defined in Morley.Micheline.Class toExpression :: Contract cp st -> Expression Source # | |
ContainsDoc (Contract cp st) Source # | |
Defined in Morley.Michelson.Typed.Doc buildDocUnfinalized :: Contract cp st -> ContractDoc Source # | |
ContainsUpdateableDoc (Contract cp st) Source # | |
Defined in Morley.Michelson.Typed.Doc modifyDocEntirely :: (SomeDocItem -> SomeDocItem) -> Contract cp st -> Contract cp st Source # | |
(forall (i :: [T]) (o :: [T]). Show (instr i o)) => Show (Contract' instr cp st) Source # | |
(forall (i :: [T]) (o :: [T]). NFData (instr i o)) => NFData (Contract' instr cp st) Source # | |
Defined in Morley.Michelson.Typed.Contract | |
(forall (i :: [T]) (o :: [T]). Eq (instr i o)) => Eq (Contract' instr cp st) Source # | |
class IsNotInView Source #
Constraint ensuring the given code does not appear on the top level of a
view. Some Michelson instructions are forbidden on the top level of views,
but allowed in main contract code, and also inside lambdas in views. Hence,
this constraint can be provided by mkContractCode
or by mkVLam
.
Instances
(TypeError ('Text "Not allowed on the top level of a view") :: Constraint) => IsNotInView Source # | |
Defined in Morley.Michelson.Typed.Contract |
newtype ContractCode' instr cp st Source #
A wrapper for contract code. The newtype is mostly there to avoid
accidentally passing code from inside ContractCode
into a view for example,
as semantics are slightly different.
ContractCode | |
|
Instances
type ContractOut st = '[ContractOut1 st] Source #
type ContractOut1 st = 'TPair ('TList 'TOperation) st Source #
type ContractInp param st = '[ContractInp1 param st] Source #
type ContractInp1 param st = 'TPair param st Source #
mkContractCode :: (IsNotInView => instr (ContractInp cp st) (ContractOut st)) -> ContractCode' instr cp st Source #
A helper to construct ContractCode'
. This helper provides the constraint
that the contract code is not in a view.
defaultContract :: (ParameterScope cp, StorageScope st) => (IsNotInView => instr (ContractInp cp st) (ContractOut st)) -> Contract' instr cp st Source #
mapContractCodeBlock :: (instr (ContractInp cp st) (ContractOut st) -> instr (ContractInp cp st) (ContractOut st)) -> Contract' instr cp st -> Contract' instr cp st Source #
Transform contract code
block.
To map e.g. views too, see mapContractCode
.
mapContractCodeBlockM :: Monad m => (instr (ContractInp cp st) (ContractOut st) -> m (instr (ContractInp cp st) (ContractOut st))) -> Contract' instr cp st -> m (Contract' instr cp st) Source #
Transform contract code
block, monadic version.
To map e.g. views too, see mapContractCodeM
.
mapContractViewBlocks :: (forall arg ret. ViewCode' instr arg st ret -> ViewCode' instr arg st ret) -> Contract' instr cp st -> Contract' instr cp st Source #
mapContractViewBlocksM :: Monad m => (forall arg ret. ViewCode' instr arg st ret -> m (ViewCode' instr arg st ret)) -> Contract' instr cp st -> m (Contract' instr cp st) Source #
mapContractCode :: (forall i o. instr i o -> instr i o) -> Contract' instr cp st -> Contract' instr cp st Source #
Map all the blocks with some code in the contract.
mapContractCodeM :: Monad m => (forall i o. instr i o -> m (instr i o)) -> Contract' instr cp st -> m (Contract' instr cp st) Source #
Map all the blocks with some code in the contract, monadic version.
data LambdaCode' instr inp out where Source #
Code of a lambda value, either recursive or non-recursive.
Note the quantified constraints on the constructors. We opt to carry those here
and not on the respective instances for the sake of simplifying downstream
instance definitions. Constraining each instance with quantified constraints
gets very long-winded very fast, and it wouldn't work with deriveGADTNFData
.
LambdaCode :: (forall i o. Show (instr i o), forall i o. Eq (instr i o), forall i o. NFData (instr i o)) => RemFail instr (inp ': '[]) (out ': '[]) -> LambdaCode' instr inp out | |
LambdaCodeRec :: (forall i o. Show (instr i o), forall i o. Eq (instr i o), forall i o. NFData (instr i o)) => RemFail instr (inp ': ('TLambda inp out ': '[])) (out ': '[]) -> LambdaCode' instr inp out |
Instances
Show (LambdaCode' instr inp out) Source # | |
Defined in Morley.Michelson.Typed.Value showsPrec :: Int -> LambdaCode' instr inp out -> ShowS # show :: LambdaCode' instr inp out -> String # showList :: [LambdaCode' instr inp out] -> ShowS # | |
NFData (LambdaCode' instr inp out) Source # | |
Defined in Morley.Michelson.Typed.Value rnf :: LambdaCode' instr inp out -> () # | |
Eq (LambdaCode' instr inp out) Source # | |
Defined in Morley.Michelson.Typed.Value (==) :: LambdaCode' instr inp out -> LambdaCode' instr inp out -> Bool # (/=) :: LambdaCode' instr inp out -> LambdaCode' instr inp out -> Bool # |
data Value' instr t where Source #
Representation of a Michelson value.
Since values (i.e. lambdas, operations) can include instructions, this type
depends on the type used to represent instructions, which is the parameter
instr
. It is itself a polymorphic type, parametrized by the Michelson types of
its input and output stacks.
The primary motivator for polymorphism is breaking cyclic dependencies between
this module and Morley.Michelson.Typed.Instr. In principle instr
can also be
used as an extension point, but at the time of writing it isn't used as such, it
is always eventually unified with Instr
.
t
is the value's Michelson type.
VKey :: PublicKey -> Value' instr 'TKey | |
VUnit :: Value' instr 'TUnit | |
VSignature :: Signature -> Value' instr 'TSignature | |
VChainId :: ChainId -> Value' instr 'TChainId | |
VOption :: forall t instr. SingI t => Maybe (Value' instr t) -> Value' instr ('TOption t) | |
VList :: forall t instr. SingI t => [Value' instr t] -> Value' instr ('TList t) | |
VSet :: forall t instr. Comparable t => Set (Value' instr t) -> Value' instr ('TSet t) | |
VOp :: Operation' instr -> Value' instr 'TOperation | |
VContract :: forall arg instr. (SingI arg, ForbidOp arg) => Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg) | |
VTicket :: forall arg instr. Comparable arg => Address -> Value' instr arg -> Natural -> Value' instr ('TTicket arg) | |
VPair :: forall l r instr. (Value' instr l, Value' instr r) -> Value' instr ('TPair l r) | |
VOr :: forall l r instr. (SingI l, SingI r) => Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r) | |
VLam :: forall inp out instr. (SingI inp, SingI out) => LambdaCode' instr inp out -> Value' instr ('TLambda inp out) | |
VMap :: forall k v instr. (SingI v, Comparable k) => Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v) | |
VBigMap | |
| |
VInt :: Integer -> Value' instr 'TInt | |
VNat :: Natural -> Value' instr 'TNat | |
VString :: MText -> Value' instr 'TString | |
VBytes :: ByteString -> Value' instr 'TBytes | |
VMutez :: Mutez -> Value' instr 'TMutez | |
VBool :: Bool -> Value' instr 'TBool | |
VKeyHash :: KeyHash -> Value' instr 'TKeyHash | |
VTimestamp :: Timestamp -> Value' instr 'TTimestamp | |
VAddress :: EpAddress -> Value' instr 'TAddress | |
VBls12381Fr :: Bls12381Fr -> Value' instr 'TBls12381Fr | |
VBls12381G1 :: Bls12381G1 -> Value' instr 'TBls12381G1 | |
VBls12381G2 :: Bls12381G2 -> Value' instr 'TBls12381G2 | |
VChest :: Chest -> Value' instr 'TChest | |
VChestKey :: ChestKey -> Value' instr 'TChestKey |
Instances
data RemFail (instr :: k -> k -> Type) (i :: k) (o :: k) where Source #
Wrapper over instruction which remembers whether this instruction always fails or not.
RfNormal :: instr i o -> RemFail instr i o | |
RfAlwaysFails :: (forall o'. instr i o') -> RemFail instr i o |
Instances
(forall (o' :: k). Show (instr i o')) => Show (RemFail instr i o) Source # | |
(forall (o' :: k). NFData (instr i o')) => NFData (RemFail instr i o) Source # | |
Defined in Morley.Michelson.Typed.Value | |
Eq (instr i o) => Eq (RemFail instr i o) Source # | Ignoring distinction between constructors here, comparing only semantics. |
PackedValScope t => Emit | |
data CreateContract instr cp st Source #
(forall i o. Show (instr i o), forall i o. Eq (instr i o)) => CreateContract | |
|
Instances
Show (CreateContract instr cp st) Source # | |
Defined in Morley.Michelson.Typed.Value showsPrec :: Int -> CreateContract instr cp st -> ShowS # show :: CreateContract instr cp st -> String # showList :: [CreateContract instr cp st] -> ShowS # | |
(forall (i :: [T]) (o :: [T]). NFData (instr i o)) => NFData (CreateContract instr cp st) Source # | |
Defined in Morley.Michelson.Typed.Value rnf :: CreateContract instr cp st -> () # | |
Eq (CreateContract instr cp st) Source # | |
Defined in Morley.Michelson.Typed.Value (==) :: CreateContract instr cp st -> CreateContract instr cp st -> Bool # (/=) :: CreateContract instr cp st -> CreateContract instr cp st -> Bool # | |
Buildable (Value' instr st) => Buildable (CreateContract instr cp st) Source # | |
Defined in Morley.Michelson.Typed.Value build :: CreateContract instr cp st -> Doc buildList :: [CreateContract instr cp st] -> Doc |
data SetDelegate Source #
Instances
data TransferTokens instr p Source #
TransferTokens | |
|
Instances
data Operation' instr where Source #
Data type, representing operation, list of which is returned by Michelson contract (according to calling convention).
These operations are to be further executed against system state after the contract execution.
OpTransferTokens :: ParameterScope p => TransferTokens instr p -> Operation' instr | |
OpSetDelegate :: SetDelegate -> Operation' instr | |
OpCreateContract :: (forall i o. Show (instr i o), forall i o. NFData (instr i o), Typeable instr, ParameterScope cp, StorageScope st) => CreateContract instr cp st -> Operation' instr | |
OpEmit :: PackedValScope t => Emit instr t -> Operation' instr |
Instances
rfMerge :: (forall o'. instr i1 o' -> instr i2 o' -> instr i3 o') -> RemFail instr i1 o -> RemFail instr i2 o -> RemFail instr i3 o Source #
Merge two execution branches.
rfAnyInstr :: RemFail instr i o -> instr i o Source #
Get code disregard whether it always fails or not.
rfMapAnyInstr :: (forall o'. instr i1 o' -> instr i2 o') -> RemFail instr i1 o -> RemFail instr i2 o Source #
Modify inner code.
addressToVContract :: forall t instr kind. (ParameterScope t, ForbidOr t) => KindedAddress kind -> Value' instr ('TContract t) Source #
Make value of contract
type which refers to the given address and
does not call any entrypoint.
buildVContract :: Value' instr ('TContract arg) -> Doc Source #
compileEpLiftSequence :: EpLiftSequence arg param -> Value' instr arg -> Value' instr param Source #
Turn EpLiftSequence
into actual function on Value
s.
liftCallArg :: EntrypointCallT param arg -> Value' instr arg -> Value' instr param Source #
Lift entrypoint argument to full parameter.
mkVLam :: (SingI inp, SingI out, forall i o. Show (instr i o), forall i o. Eq (instr i o), forall i o. NFData (instr i o)) => (IsNotInView => RemFail instr '[inp] '[out]) -> Value' instr ('TLambda inp out) Source #
mkVLamRec :: (SingI inp, SingI out, forall i o. Show (instr i o), forall i o. Eq (instr i o), forall i o. NFData (instr i o)) => (IsNotInView => RemFail instr '[inp, 'TLambda inp out] '[out]) -> Value' instr ('TLambda inp out) Source #
withValueTypeSanity :: Value' instr t -> (SingI t => a) -> a Source #
Provide a witness of that value's type is known.
eqValueExt :: Value' instr t1 -> Value' instr t2 -> Bool Source #
Extended values comparison - it does not require Value
s to be
of the same type, only their content to match.
class EDivOp (n :: T) (m :: T) where Source #
evalEDivOp :: Value' instr n -> Value' instr m -> Value' instr ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m))) Source #
Instances
EDivOp 'TInt 'TInt Source # | |
Defined in Morley.Michelson.Typed.Polymorphic | |
EDivOp 'TInt 'TNat Source # | |
Defined in Morley.Michelson.Typed.Polymorphic | |
EDivOp 'TMutez 'TMutez Source # | |
Defined in Morley.Michelson.Typed.Polymorphic | |
EDivOp 'TMutez 'TNat Source # | |
Defined in Morley.Michelson.Typed.Polymorphic | |
EDivOp 'TNat 'TInt Source # | |
Defined in Morley.Michelson.Typed.Polymorphic | |
EDivOp 'TNat 'TNat Source # | |
Defined in Morley.Michelson.Typed.Polymorphic |
class ConcatOp (c :: T) where Source #
evalConcat :: Value' instr c -> Value' instr c -> Value' instr c Source #
evalConcat' :: [Value' instr c] -> Value' instr c Source #
class GetOp (c :: T) where Source #
evalGet :: Value' instr (GetOpKey c) -> Value' instr c -> Maybe (Value' instr (GetOpVal c)) Source #
class UpdOp (c :: T) where Source #
evalUpd :: Value' instr (UpdOpKey c) -> Value' instr (UpdOpParams c) -> Value' instr c -> Value' instr c Source #
Instances
UpdOp ('TSet a) Source # | |
Defined in Morley.Michelson.Typed.Polymorphic | |
UpdOp ('TBigMap k v) Source # | |
Defined in Morley.Michelson.Typed.Polymorphic | |
UpdOp ('TMap k v) Source # | |
Defined in Morley.Michelson.Typed.Polymorphic |
class IterOp (c :: T) where Source #
Instances
IterOp ('TList e) Source # | |
Defined in Morley.Michelson.Typed.Polymorphic | |
IterOp ('TSet e) Source # | |
Defined in Morley.Michelson.Typed.Polymorphic | |
IterOp ('TMap k v) Source # | |
Defined in Morley.Michelson.Typed.Polymorphic |
class MapOp (c :: T) where Source #
mapOpToList :: Value' instr c -> [Value' instr (MapOpInp c)] Source #
mapOpFromList :: SingI b => Value' instr c -> [Value' instr b] -> Value' instr (MapOpRes c b) Source #
Instances
MapOp ('TList e) Source # | |
Defined in Morley.Michelson.Typed.Polymorphic mapOpToList :: forall (instr :: [T] -> [T] -> Type). Value' instr ('TList e) -> [Value' instr (MapOpInp ('TList e))] Source # mapOpFromList :: forall (b :: T) (instr :: [T] -> [T] -> Type). SingI b => Value' instr ('TList e) -> [Value' instr b] -> Value' instr (MapOpRes ('TList e) b) Source # mapOpNotes :: Notes ('TList e) -> Notes (MapOpInp ('TList e)) Source # | |
MapOp ('TOption e) Source # | |
Defined in Morley.Michelson.Typed.Polymorphic mapOpToList :: forall (instr :: [T] -> [T] -> Type). Value' instr ('TOption e) -> [Value' instr (MapOpInp ('TOption e))] Source # mapOpFromList :: forall (b :: T) (instr :: [T] -> [T] -> Type). SingI b => Value' instr ('TOption e) -> [Value' instr b] -> Value' instr (MapOpRes ('TOption e) b) Source # mapOpNotes :: Notes ('TOption e) -> Notes (MapOpInp ('TOption e)) Source # | |
MapOp ('TMap k v) Source # | |
Defined in Morley.Michelson.Typed.Polymorphic mapOpToList :: forall (instr :: [T] -> [T] -> Type). Value' instr ('TMap k v) -> [Value' instr (MapOpInp ('TMap k v))] Source # mapOpFromList :: forall (b :: T) (instr :: [T] -> [T] -> Type). SingI b => Value' instr ('TMap k v) -> [Value' instr b] -> Value' instr (MapOpRes ('TMap k v) b) Source # mapOpNotes :: Notes ('TMap k v) -> Notes (MapOpInp ('TMap k v)) Source # |
divMich :: Integral a => a -> a -> a Source #
Computing div
function in Michelson style.
When divisor is negative, Haskell gives x as integer part,
while Michelson gives x+1.
modMich :: Integral a => a -> a -> a Source #
Computing mod
function in Michelson style.
When divisor is negative, Haskell gives a negative modulo,
while there is a positive modulo in Michelson.
type Bls12381MulBadOrder a1 a2 = DelayError (((('Text "Multiplication of " :<>: 'ShowType a2) :<>: 'Text " and ") :<>: 'ShowType a1) :<>: 'Text " works only other way around") Source #
Instances
UnaryArithOp Ge 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith | |
type UnaryArithRes Ge 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith |
Instances
UnaryArithOp Le 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith | |
type UnaryArithRes Le 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith |
Instances
UnaryArithOp Gt 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith | |
type UnaryArithRes Gt 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith |
Instances
UnaryArithOp Lt 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith | |
type UnaryArithRes Lt 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith |
Instances
UnaryArithOp Neq 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith | |
type UnaryArithRes Neq 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith |
Instances
UnaryArithOp Eq' 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith | |
type UnaryArithRes Eq' 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith |
Instances
ArithOp Lsr 'TBytes 'TNat Source # | |
Defined in Morley.Michelson.Typed.Arith evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Lsr -> Value' instr 'TBytes -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TBytes) (Value' instr 'TNat)) (Value' instr (ArithRes Lsr 'TBytes 'TNat)) Source # commutativityProof :: Maybe $ Dict (ArithRes Lsr 'TBytes 'TNat ~ ArithRes Lsr 'TNat 'TBytes, ArithOp Lsr 'TNat 'TBytes) Source # | |
ArithOp Lsr 'TNat 'TNat Source # | |
Defined in Morley.Michelson.Typed.Arith evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Lsr -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Lsr 'TNat 'TNat)) Source # commutativityProof :: Maybe $ Dict (ArithRes Lsr 'TNat 'TNat ~ ArithRes Lsr 'TNat 'TNat, ArithOp Lsr 'TNat 'TNat) Source # | |
type ArithRes Lsr 'TBytes 'TNat Source # | |
type ArithRes Lsr 'TNat 'TNat Source # | |
Instances
ArithOp Lsl 'TBytes 'TNat Source # | |
Defined in Morley.Michelson.Typed.Arith evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Lsl -> Value' instr 'TBytes -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TBytes) (Value' instr 'TNat)) (Value' instr (ArithRes Lsl 'TBytes 'TNat)) Source # commutativityProof :: Maybe $ Dict (ArithRes Lsl 'TBytes 'TNat ~ ArithRes Lsl 'TNat 'TBytes, ArithOp Lsl 'TNat 'TBytes) Source # | |
ArithOp Lsl 'TNat 'TNat Source # | |
Defined in Morley.Michelson.Typed.Arith evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Lsl -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Lsl 'TNat 'TNat)) Source # commutativityProof :: Maybe $ Dict (ArithRes Lsl 'TNat 'TNat ~ ArithRes Lsl 'TNat 'TNat, ArithOp Lsl 'TNat 'TNat) Source # | |
type ArithRes Lsl 'TBytes 'TNat Source # | |
type ArithRes Lsl 'TNat 'TNat Source # | |
Instances
UnaryArithOp Not 'TBool Source # | |
Defined in Morley.Michelson.Typed.Arith | |
UnaryArithOp Not 'TBytes Source # | |
Defined in Morley.Michelson.Typed.Arith | |
UnaryArithOp Not 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith | |
UnaryArithOp Not 'TNat Source # | |
Defined in Morley.Michelson.Typed.Arith | |
type UnaryArithRes Not 'TBool Source # | |
Defined in Morley.Michelson.Typed.Arith | |
type UnaryArithRes Not 'TBytes Source # | |
Defined in Morley.Michelson.Typed.Arith | |
type UnaryArithRes Not 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith | |
type UnaryArithRes Not 'TNat Source # | |
Defined in Morley.Michelson.Typed.Arith |
Instances
Instances
Instances
Instances
Instances
UnaryArithOp Abs 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith | |
type UnaryArithRes Abs 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith |
Instances
Instances
Instances
ArithOp SubMutez 'TMutez 'TMutez Source # | |
Defined in Morley.Michelson.Typed.Arith evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy SubMutez -> Value' instr 'TMutez -> Value' instr 'TMutez -> Either (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)) (Value' instr (ArithRes SubMutez 'TMutez 'TMutez)) Source # commutativityProof :: Maybe $ Dict (ArithRes SubMutez 'TMutez 'TMutez ~ ArithRes SubMutez 'TMutez 'TMutez, ArithOp SubMutez 'TMutez 'TMutez) Source # | |
type ArithRes SubMutez 'TMutez 'TMutez Source # | |
Instances
Instances
class ToBytesArithOp (n :: T) where Source #
Class for conversions to bytes.
Instances
class ToIntArithOp (n :: T) where Source #
Class for conversions to an integer value.
Instances
ToIntArithOp 'TBls12381Fr Source # | |
Defined in Morley.Michelson.Typed.Arith evalToIntOp :: forall (instr :: [T] -> [T] -> Type). Value' instr 'TBls12381Fr -> Value' instr 'TInt Source # | |
ToIntArithOp 'TBytes Source # | |
ToIntArithOp 'TNat Source # | |
class UnaryArithOp aop (n :: T) where Source #
Class for unary arithmetic operation.
type UnaryArithRes aop n :: T Source #
evalUnaryArithOp :: proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n) Source #
Instances
data ArithError n m Source #
Represents an arithmetic error of the operation.
Instances
data MutezArithErrorType Source #
Denotes the error type occurred in the arithmetic operation involving mutez.
Instances
data ShiftArithErrorType Source #
Denotes the error type occurred in the arithmetic shift operation.
Instances
class (Typeable n, Typeable m) => ArithOp aop (n :: T) (m :: T) where Source #
Class for binary arithmetic operation.
Takes binary operation marker as op
parameter,
types of left operand n
and right operand m
.
Typeable
constraints in superclass are necessary for error messages.
type ArithRes aop n m :: T Source #
Type family ArithRes
denotes the type resulting from
computing operation op
from operands of types n
and m
.
For instance, adding integer to natural produces integer,
which is reflected in following instance of type family:
ArithRes Add CNat CInt = CInt
.
evalOp :: proxy aop -> Value' instr n -> Value' instr m -> Either (ArithError (Value' instr n) (Value' instr m)) (Value' instr (ArithRes aop n m)) Source #
Evaluate arithmetic operation on given operands.
commutativityProof :: Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n) Source #
An operation can marked as commutative, it does not affect its runtime behavior, but enables certain optimization in the optimizer. We conservatively consider operations non-commutative by default.
Note that there is one unusual case: AND
works with int : nat
but not with nat : int
. That's how it's specified in Michelson.
Instances
compareOp :: Comparable t => Value' i t -> Value' i t -> Integer Source #
Implementation for COMPARE
instruction.
TEST_ASSERT (TestAssert s) | |
PRINT (PrintComment s) | |
DOC_ITEM SomeDocItem | |
COMMENT_ITEM CommentType | |
STACKTYPE StackTypePattern |
Instances
data CommentType Source #
FunctionStarts Text | |
FunctionEnds Text | |
StatementStarts Text | |
StatementEnds Text | |
JustComment Text | |
StackTypeComment (Maybe [T]) |
|
Instances
newtype PrintComment (st :: [T]) Source #
A print format with references into the stack
PrintComment | |
|
Instances
data StackRef (st :: [T]) where Source #
A reference into the stack of a given type.
StackRef :: RequireLongerThan st idx => PeanoNatural idx -> StackRef st | Keeps 0-based index to a stack element counting from the top. |
data TestAssert (s :: [T]) where Source #
TestAssert :: Text -> PrintComment inp -> Instr inp ('TBool ': out) -> TestAssert inp |
Instances
Show (TestAssert s) Source # | |
Defined in Morley.Michelson.Typed.Instr showsPrec :: Int -> TestAssert s -> ShowS # show :: TestAssert s -> String # showList :: [TestAssert s] -> ShowS # | |
NFData (TestAssert s) Source # | |
Defined in Morley.Michelson.Typed.Instr rnf :: TestAssert s -> () # | |
SingI s => Eq (TestAssert s) Source # | |
Defined in Morley.Michelson.Typed.Convert (==) :: TestAssert s -> TestAssert s -> Bool # (/=) :: TestAssert s -> TestAssert s -> Bool # |
data Instr (inp :: [T]) (out :: [T]) where Source #
Representation of Michelson instruction or sequence of instructions.
Each Michelson instruction is represented by exactly one
constructor of this data type. Sequence of instructions
is represented with use of Seq
constructor in following
way: SWAP; DROP ; DUP;
-> SWAP `Seq` DROP `Seq` DUP
.
Special case where there are no instructions is represented
by constructor Nop
, e.g. IF_NONE {} { SWAP; DROP; }
->
IF_NONE Nop (SWAP `Seq` DROP)
.
Type parameter inp
states for input stack type. That is,
type of the stack that is required for operation to execute.
Type parameter out
states for output stack type or type
of stack that will be left after instruction's execution.
Each constructor here corresponding to an instruction that can have
annotations is represented as AnnX
, where X
is the name of
the instruction. These constructors accept a typed heterogenous list of
annotations as the first argument. Pattern synonyms without the Ann
prefix are provided, those ignore annotations entirely.
We need this AnnX
constructors to carry annotations for PACK
.
When typechecking a sequence of instructions, we'll attach annotations from the
"untyped" instruction to the typed one. Note that if an instruction has a type argument,
e.g. `PUSH (int :t) 2` we'll attach typed Notes
for this type instead; other
annotations are used as-is.
The interpreter mostly ignores annotations, with the exception of those used for entrypoint resolution.
The serializer (Morley.Michelson.Interpret.Pack) can restore the original "untyped" instruction from annotations on the "typed" one.
AnnSELF
and AnnCONTRACT
are a special case: field annotations on these
instructions carry semantic meaning (specify the entrypoint), hence those
are stored separately from other annotations, to simplify checking for
invariants in "typed" contracts.
WithLoc :: ErrorSrcPos -> Instr a b -> Instr a b | A wrapper carrying original source location of the instruction. TODO [#283]: replace this wrapper with something more clever and abstract. |
Meta :: SomeMeta -> Instr a b -> Instr a b | A wrapper allowing arbitrary user metadata to be stored by some instruction.
TODO [#689]: Use this instead of |
Seq :: Instr a b -> Instr b c -> Instr a c infixr 8 | |
Nop :: Instr s s | Nop operation. Missing in Michelson spec, added to parse construction like `IF {} { SWAP; DROP; }`. |
Ext :: ExtInstr s -> Instr s s | |
Nested :: Instr inp out -> Instr inp out | Nested wrapper is going to wrap a sequence of instructions with { }. It is crucial because serialisation of a contract depends on precise structure of its code. |
DocGroup :: DocGrouping -> Instr inp out -> Instr inp out | Places documentation generated for given instruction under some group.
This is not part of |
AnnCAR :: Anns '[VarAnn, FieldAnn] -> Instr ('TPair a b ': s) (a ': s) | |
AnnCDR :: Anns '[VarAnn, FieldAnn] -> Instr ('TPair a b ': s) (b ': s) | |
DROP :: Instr (a ': s) s | |
DROPN :: forall (n :: Peano) s. RequireLongerOrSameLength s n => PeanoNatural n -> Instr s (Drop n s) | |
AnnDUP :: DupableScope a => AnnVar -> Instr (a ': s) (a ': (a ': s)) | |
AnnDUPN :: forall (n :: Peano) inp out a. (ConstraintDUPN n inp out a, DupableScope a) => AnnVar -> PeanoNatural n -> Instr inp out | |
SWAP :: Instr (a ': (b ': s)) (b ': (a ': s)) | |
DIG :: forall (n :: Peano) inp out a. ConstraintDIG n inp out a => PeanoNatural n -> Instr inp out | |
DUG :: forall (n :: Peano) inp out a. ConstraintDUG n inp out a => PeanoNatural n -> Instr inp out | |
AnnPUSH :: forall t s. ConstantScope t => Anns '[VarAnn, Notes t] -> Value' Instr t -> Instr s (t ': s) | |
AnnSOME :: Anns '[TypeAnn, VarAnn] -> Instr (a ': s) ('TOption a ': s) | |
AnnNONE :: forall a s. SingI a => Anns '[TypeAnn, VarAnn, Notes a] -> Instr s ('TOption a ': s) | |
AnnUNIT :: Anns '[TypeAnn, VarAnn] -> Instr s ('TUnit ': s) | |
IF_NONE :: Instr s s' -> Instr (a ': s) s' -> Instr ('TOption a ': s) s' | |
AnnPAIR :: Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn] -> Instr (a ': (b ': s)) ('TPair a b ': s) | |
AnnUNPAIR :: Anns '[VarAnn, VarAnn, FieldAnn, FieldAnn] -> Instr ('TPair a b ': s) (a ': (b ': s)) | |
AnnPAIRN :: forall n inp. ConstraintPairN n inp => AnnVar -> PeanoNatural n -> Instr inp (PairN n inp) |
|
UNPAIRN :: forall (n :: Peano) (pair :: T) (s :: [T]). ConstraintUnpairN n pair => PeanoNatural n -> Instr (pair ': s) (UnpairN n pair ++ s) |
|
AnnLEFT :: SingI b => Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes b] -> Instr (a ': s) ('TOr a b ': s) | |
AnnRIGHT :: SingI a => Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a] -> Instr (b ': s) ('TOr a b ': s) | |
IF_LEFT :: Instr (a ': s) s' -> Instr (b ': s) s' -> Instr ('TOr a b ': s) s' | |
AnnNIL :: SingI p => Anns '[TypeAnn, VarAnn, Notes p] -> Instr s ('TList p ': s) | |
AnnCONS :: AnnVar -> Instr (a ': ('TList a ': s)) ('TList a ': s) | |
IF_CONS :: Instr (a ': ('TList a ': s)) s' -> Instr s s' -> Instr ('TList a ': s) s' | |
AnnSIZE :: SizeOp c => AnnVar -> Instr (c ': s) ('TNat ': s) | |
AnnEMPTY_SET :: Comparable e => Anns '[TypeAnn, VarAnn, Notes e] -> Instr s ('TSet e ': s) | |
AnnEMPTY_MAP :: (SingI b, Comparable a) => Anns '[TypeAnn, VarAnn, Notes a, Notes b] -> Instr s ('TMap a b ': s) | |
AnnEMPTY_BIG_MAP :: (SingI b, Comparable a, ForbidBigMap b) => Anns '[TypeAnn, VarAnn, Notes a, Notes b] -> Instr s ('TBigMap a b ': s) | |
AnnMAP :: (MapOp c, SingI b) => AnnVar -> Instr (MapOpInp c ': s) (b ': s) -> Instr (c ': s) (MapOpRes c b ': s) | |
ITER :: IterOp c => Instr (IterOpEl c ': s) s -> Instr (c ': s) s | |
AnnMEM :: MemOp c => AnnVar -> Instr (MemOpKey c ': (c ': s)) ('TBool ': s) | |
AnnGET :: (GetOp c, SingI (GetOpVal c)) => AnnVar -> Instr (GetOpKey c ': (c ': s)) ('TOption (GetOpVal c) ': s) | |
AnnGETN :: forall (ix :: Peano) (pair :: T) (s :: [T]). ConstraintGetN ix pair => AnnVar -> PeanoNatural ix -> Instr (pair ': s) (GetN ix pair ': s) | Get the node at index For example, a pair with 3 elements pair / \ a pair / \ b c Where the nodes are numbered as follows: 0 / \ 1 2 / \ 3 4
Note that
|
AnnUPDATE :: UpdOp c => AnnVar -> Instr (UpdOpKey c ': (UpdOpParams c ': (c ': s))) (c ': s) | |
AnnUPDATEN :: forall (ix :: Peano) (val :: T) (pair :: T) (s :: [T]). ConstraintUpdateN ix pair => AnnVar -> PeanoNatural ix -> Instr (val ': (pair ': s)) (UpdateN ix val pair ': s) | Update the node at index
Note that
|
AnnGET_AND_UPDATE :: (GetOp c, UpdOp c, SingI (GetOpVal c), UpdOpKey c ~ GetOpKey c) => AnnVar -> Instr (UpdOpKey c ': (UpdOpParams c ': (c ': s))) ('TOption (GetOpVal c) ': (c ': s)) | |
IF :: Instr s s' -> Instr s s' -> Instr ('TBool ': s) s' | |
LOOP :: Instr s ('TBool ': s) -> Instr ('TBool ': s) s | |
LOOP_LEFT :: Instr (a ': s) ('TOr a b ': s) -> Instr ('TOr a b ': s) (b ': s) | |
AnnLAMBDA :: forall i o s. (SingI i, SingI o) => Anns '[VarAnn, Notes i, Notes o] -> RemFail Instr '[i] '[o] -> Instr s ('TLambda i o ': s) | |
AnnLAMBDA_REC :: forall i o s. (SingI i, SingI o) => Anns '[VarAnn, Notes i, Notes o] -> RemFail Instr '[i, 'TLambda i o] '[o] -> Instr s ('TLambda i o ': s) | |
AnnEXEC :: AnnVar -> Instr (t1 ': ('TLambda t1 t2 ': s)) (t2 ': s) | |
AnnAPPLY :: forall a b c s. (ConstantScope a, SingI b) => AnnVar -> Instr (a ': ('TLambda ('TPair a b) c ': s)) ('TLambda b c ': s) | |
DIP :: Instr a c -> Instr (b ': a) (b ': c) | |
DIPN :: forall (n :: Peano) inp out s s'. ConstraintDIPN n inp out s s' => PeanoNatural n -> Instr s s' -> Instr inp out | |
FAILWITH :: (SingI a, ConstantScope a) => Instr (a ': s) t | |
AnnCAST :: forall a s. SingI a => Anns '[VarAnn, Notes a] -> Instr (a ': s) (a ': s) | |
AnnRENAME :: AnnVar -> Instr (a ': s) (a ': s) | |
AnnPACK :: PackedValScope a => AnnVar -> Instr (a ': s) ('TBytes ': s) | |
AnnUNPACK :: (UnpackedValScope a, SingI a) => Anns '[TypeAnn, VarAnn, Notes a] -> Instr ('TBytes ': s) ('TOption a ': s) | |
AnnCONCAT :: ConcatOp c => AnnVar -> Instr (c ': (c ': s)) (c ': s) | |
AnnCONCAT' :: ConcatOp c => AnnVar -> Instr ('TList c ': s) (c ': s) | |
AnnSLICE :: (SliceOp c, SingI c) => AnnVar -> Instr ('TNat ': ('TNat ': (c ': s))) ('TOption c ': s) | |
AnnISNAT :: AnnVar -> Instr ('TInt ': s) ('TOption 'TNat ': s) | |
AnnADD :: ArithOp Add n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes Add n m ': s) | |
AnnSUB :: ArithOp Sub n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes Sub n m ': s) | |
AnnSUB_MUTEZ :: AnnVar -> Instr ('TMutez ': ('TMutez ': s)) ('TOption 'TMutez ': s) | |
AnnMUL :: ArithOp Mul n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes Mul n m ': s) | |
AnnEDIV :: ArithOp EDiv n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes EDiv n m ': s) | |
AnnABS :: UnaryArithOp Abs n => AnnVar -> Instr (n ': s) (UnaryArithRes Abs n ': s) | |
AnnNEG :: UnaryArithOp Neg n => AnnVar -> Instr (n ': s) (UnaryArithRes Neg n ': s) | |
AnnLSL :: ArithOp Lsl n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes Lsl n m ': s) | |
AnnLSR :: ArithOp Lsr n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes Lsr n m ': s) | |
AnnOR :: ArithOp Or n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes Or n m ': s) | |
AnnAND :: ArithOp And n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes And n m ': s) | |
AnnXOR :: ArithOp Xor n m => AnnVar -> Instr (n ': (m ': s)) (ArithRes Xor n m ': s) | |
AnnNOT :: (SingI n, UnaryArithOp Not n) => AnnVar -> Instr (n ': s) (UnaryArithRes Not n ': s) | |
AnnCOMPARE :: Comparable n => AnnVar -> Instr (n ': (n ': s)) ('TInt ': s) | |
AnnEQ :: UnaryArithOp Eq' n => AnnVar -> Instr (n ': s) (UnaryArithRes Eq' n ': s) | |
AnnNEQ :: UnaryArithOp Neq n => AnnVar -> Instr (n ': s) (UnaryArithRes Neq n ': s) | |
AnnLT :: UnaryArithOp Lt n => AnnVar -> Instr (n ': s) (UnaryArithRes Lt n ': s) | |
AnnGT :: UnaryArithOp Gt n => AnnVar -> Instr (n ': s) (UnaryArithRes Gt n ': s) | |
AnnLE :: UnaryArithOp Le n => AnnVar -> Instr (n ': s) (UnaryArithRes Le n ': s) | |
AnnGE :: UnaryArithOp Ge n => AnnVar -> Instr (n ': s) (UnaryArithRes Ge n ': s) | |
AnnINT :: ToIntArithOp n => AnnVar -> Instr (n ': s) ('TInt ': s) | |
AnnBYTES :: ToBytesArithOp n => AnnVar -> Instr (n ': s) ('TBytes ': s) | |
AnnNAT :: AnnVar -> Instr ('TBytes ': s) ('TNat ': s) | |
AnnVIEW :: (SingI arg, ViewableScope ret) => Anns '[VarAnn, Notes ret] -> ViewName -> Instr (arg ': ('TAddress ': s)) ('TOption ret ': s) | |
AnnSELF :: forall (arg :: T) s. (ParameterScope arg, IsNotInView) => AnnVar -> SomeEntrypointCallT arg -> Instr s ('TContract arg ': s) | Note that the field annotation on |
AnnCONTRACT :: ParameterScope p => Anns '[VarAnn, Notes p] -> EpName -> Instr ('TAddress ': s) ('TOption ('TContract p) ': s) | Note that the field annotation on |
AnnTRANSFER_TOKENS :: (ParameterScope p, IsNotInView) => AnnVar -> Instr (p ': ('TMutez ': ('TContract p ': s))) ('TOperation ': s) | |
AnnSET_DELEGATE :: IsNotInView => AnnVar -> Instr ('TOption 'TKeyHash ': s) ('TOperation ': s) | |
AnnCREATE_CONTRACT :: (ParameterScope p, StorageScope g, IsNotInView) => Anns '[VarAnn, VarAnn] -> Contract' Instr p g -> Instr ('TOption 'TKeyHash ': ('TMutez ': (g ': s))) ('TOperation ': ('TAddress ': s)) | |
AnnIMPLICIT_ACCOUNT :: AnnVar -> Instr ('TKeyHash ': s) ('TContract 'TUnit ': s) | |
AnnNOW :: AnnVar -> Instr s ('TTimestamp ': s) | |
AnnAMOUNT :: AnnVar -> Instr s ('TMutez ': s) | |
AnnBALANCE :: AnnVar -> Instr s ('TMutez ': s) | |
AnnVOTING_POWER :: AnnVar -> Instr ('TKeyHash ': s) ('TNat ': s) | |
AnnTOTAL_VOTING_POWER :: AnnVar -> Instr s ('TNat ': s) | |
AnnCHECK_SIGNATURE :: AnnVar -> Instr ('TKey ': ('TSignature ': ('TBytes ': s))) ('TBool ': s) | |
AnnSHA256 :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s) | |
AnnSHA512 :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s) | |
AnnBLAKE2B :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s) | |
AnnSHA3 :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s) | |
AnnKECCAK :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s) | |
AnnHASH_KEY :: AnnVar -> Instr ('TKey ': s) ('TKeyHash ': s) | |
AnnPAIRING_CHECK :: AnnVar -> Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) ': s) ('TBool ': s) | |
AnnSOURCE :: AnnVar -> Instr s ('TAddress ': s) | |
AnnSENDER :: AnnVar -> Instr s ('TAddress ': s) | |
AnnADDRESS :: AnnVar -> Instr ('TContract a ': s) ('TAddress ': s) | |
AnnCHAIN_ID :: AnnVar -> Instr s ('TChainId ': s) | |
AnnLEVEL :: AnnVar -> Instr s ('TNat ': s) | |
AnnSELF_ADDRESS :: AnnVar -> Instr s ('TAddress ': s) | |
NEVER :: Instr ('TNever ': s) t | |
AnnTICKET_DEPRECATED :: Comparable a => AnnVar -> Instr (a ': ('TNat ': s)) ('TTicket a ': s) | |
AnnTICKET :: Comparable a => AnnVar -> Instr (a ': ('TNat ': s)) ('TOption ('TTicket a) ': s) | |
AnnREAD_TICKET :: AnnVar -> Instr ('TTicket a ': s) (RightComb ['TAddress, a, 'TNat] ': ('TTicket a ': s)) | |
AnnSPLIT_TICKET :: AnnVar -> Instr ('TTicket a ': ('TPair 'TNat 'TNat ': s)) ('TOption ('TPair ('TTicket a) ('TTicket a)) ': s) | |
AnnJOIN_TICKETS :: AnnVar -> Instr ('TPair ('TTicket a) ('TTicket a) ': s) ('TOption ('TTicket a) ': s) | |
AnnOPEN_CHEST :: AnnVar -> Instr ('TChestKey ': ('TChest ': ('TNat ': s))) ('TOr 'TBytes 'TBool ': s) | |
AnnSAPLING_EMPTY_STATE :: AnnVar -> Sing n -> Instr s ('TSaplingState n ': s) | |
AnnSAPLING_VERIFY_UPDATE :: AnnVar -> Instr ('TSaplingTransaction n ': ('TSaplingState n ': s)) ('TOption ('TPair 'TBytes ('TPair 'TInt ('TSaplingState n))) ': s) | |
AnnMIN_BLOCK_TIME :: [AnyAnn] -> Instr s ('TNat ': s) | |
AnnEMIT :: PackedValScope t => AnnVar -> FieldAnn -> Maybe (Notes t) -> Instr (t ': s) ('TOperation ': s) |
pattern NAT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TNat s) => Instr inp out | |
pattern BYTES :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) 'TBytes s, ToBytesArithOp n) => Instr inp out | |
pattern EMIT :: forall {inp} {out}. () => forall (t :: T) (s :: [T]). (inp ~ '(:) t s, out ~ '(:) 'TOperation s, PackedValScope t) => FieldAnn -> Maybe (Notes t) -> Instr inp out | |
pattern MIN_BLOCK_TIME :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TNat s) => Instr inp out | |
pattern SAPLING_VERIFY_UPDATE :: forall {inp} {out}. () => forall (n :: Peano) (s :: [T]). (inp ~ '(:) ('TSaplingTransaction n) ('(:) ('TSaplingState n) s), out ~ '(:) ('TOption ('TPair 'TBytes ('TPair 'TInt ('TSaplingState n)))) s) => Instr inp out | |
pattern SAPLING_EMPTY_STATE :: forall {inp} {out}. () => forall (n :: Peano) (s :: [T]). (inp ~ s, out ~ '(:) ('TSaplingState n) s) => Sing n -> Instr inp out | |
pattern OPEN_CHEST :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TChestKey ('(:) 'TChest ('(:) 'TNat s)), out ~ '(:) ('TOr 'TBytes 'TBool) s) => Instr inp out | Deprecated: Due to a vulnerability discovered in time-lock protocol, OPEN_CHEST is temporarily deprecated since Lima |
pattern JOIN_TICKETS :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) ('TPair ('TTicket a) ('TTicket a)) s, out ~ '(:) ('TOption ('TTicket a)) s) => Instr inp out | |
pattern SPLIT_TICKET :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) ('TTicket a) ('(:) ('TPair 'TNat 'TNat) s), out ~ '(:) ('TOption ('TPair ('TTicket a) ('TTicket a))) s) => Instr inp out | |
pattern READ_TICKET :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) ('TTicket a) s, out ~ '(:) (RightComb ('(:) 'TAddress ('(:) a ('(:) 'TNat ('[] :: [T]))))) ('(:) ('TTicket a) s)) => Instr inp out | |
pattern TICKET_DEPRECATED :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a ('(:) 'TNat s), out ~ '(:) ('TTicket a) s, Comparable a) => Instr inp out | |
pattern TICKET :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a ('(:) 'TNat s), out ~ '(:) ('TOption ('TTicket a)) s, Comparable a) => Instr inp out | |
pattern SELF_ADDRESS :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TAddress s) => Instr inp out | |
pattern LEVEL :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TNat s) => Instr inp out | |
pattern CHAIN_ID :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TChainId s) => Instr inp out | |
pattern ADDRESS :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) ('TContract a) s, out ~ '(:) 'TAddress s) => Instr inp out | |
pattern SENDER :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TAddress s) => Instr inp out | |
pattern SOURCE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TAddress s) => Instr inp out | |
pattern PAIRING_CHECK :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) ('TList ('TPair 'TBls12381G1 'TBls12381G2)) s, out ~ '(:) 'TBool s) => Instr inp out | |
pattern HASH_KEY :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKey s, out ~ '(:) 'TKeyHash s) => Instr inp out | |
pattern KECCAK :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out | |
pattern SHA3 :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out | |
pattern BLAKE2B :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out | |
pattern CHECK_SIGNATURE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKey ('(:) 'TSignature ('(:) 'TBytes s)), out ~ '(:) 'TBool s) => Instr inp out | |
pattern TOTAL_VOTING_POWER :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TNat s) => Instr inp out | |
pattern VOTING_POWER :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKeyHash s, out ~ '(:) 'TNat s) => Instr inp out | |
pattern BALANCE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TMutez s) => Instr inp out | |
pattern AMOUNT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TMutez s) => Instr inp out | |
pattern NOW :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TTimestamp s) => Instr inp out | |
pattern IMPLICIT_ACCOUNT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKeyHash s, out ~ '(:) ('TContract 'TUnit) s) => Instr inp out | |
pattern CREATE_CONTRACT :: forall {inp} {out}. () => forall (p :: T) (g :: T) (s :: [T]). (inp ~ '(:) ('TOption 'TKeyHash) ('(:) 'TMutez ('(:) g s)), out ~ '(:) 'TOperation ('(:) 'TAddress s), ParameterScope p, StorageScope g, IsNotInView) => Contract' Instr p g -> Instr inp out | |
pattern SET_DELEGATE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) ('TOption 'TKeyHash) s, out ~ '(:) 'TOperation s, IsNotInView) => Instr inp out | |
pattern TRANSFER_TOKENS :: forall {inp} {out}. () => forall (p :: T) (s :: [T]). (inp ~ '(:) p ('(:) 'TMutez ('(:) ('TContract p) s)), out ~ '(:) 'TOperation s, ParameterScope p, IsNotInView) => Instr inp out | |
pattern CONTRACT :: forall {inp} {out}. () => forall (p :: T) (s :: [T]). (inp ~ '(:) 'TAddress s, out ~ '(:) ('TOption ('TContract p)) s, ParameterScope p) => EpName -> Instr inp out | |
pattern SELF :: forall {inp} {out}. () => forall (arg :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TContract arg) s, ParameterScope arg, IsNotInView) => SomeEntrypointCallT arg -> Instr inp out | |
pattern VIEW :: forall {inp} {out}. () => forall (arg :: T) (ret :: T) (s :: [T]). (inp ~ '(:) arg ('(:) 'TAddress s), out ~ '(:) ('TOption ret) s, SingI arg, ViewableScope ret) => ViewName -> Instr inp out | |
pattern INT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) 'TInt s, ToIntArithOp n) => Instr inp out | |
pattern NEQ :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Neq n) s, UnaryArithOp Neq n) => Instr inp out | |
pattern COMPARE :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n ('(:) n s), out ~ '(:) 'TInt s, Comparable n) => Instr inp out | |
pattern NOT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Not n) s, SingI n, UnaryArithOp Not n) => Instr inp out | |
pattern XOR :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Xor n m) s, ArithOp Xor n m) => Instr inp out | |
pattern AND :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes And n m) s, ArithOp And n m) => Instr inp out | |
pattern OR :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Or n m) s, ArithOp Or n m) => Instr inp out | |
pattern LSR :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Lsr n m) s, ArithOp Lsr n m) => Instr inp out | |
pattern LSL :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Lsl n m) s, ArithOp Lsl n m) => Instr inp out | |
pattern NEG :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Neg n) s, UnaryArithOp Neg n) => Instr inp out | |
pattern ABS :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Abs n) s, UnaryArithOp Abs n) => Instr inp out | |
pattern EDIV :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes EDiv n m) s, ArithOp EDiv n m) => Instr inp out | |
pattern MUL :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Mul n m) s, ArithOp Mul n m) => Instr inp out | |
pattern SUB_MUTEZ :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TMutez ('(:) 'TMutez s), out ~ '(:) ('TOption 'TMutez) s) => Instr inp out | |
pattern SUB :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Sub n m) s, ArithOp Sub n m) => Instr inp out | |
pattern ADD :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Add n m) s, ArithOp Add n m) => Instr inp out | |
pattern ISNAT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TInt s, out ~ '(:) ('TOption 'TNat) s) => Instr inp out | |
pattern SLICE :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) 'TNat ('(:) 'TNat ('(:) c s)), out ~ '(:) ('TOption c) s, SliceOp c, SingI c) => Instr inp out | |
pattern CONCAT' :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) ('TList c) s, out ~ '(:) c s, ConcatOp c) => Instr inp out | |
pattern CONCAT :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) c ('(:) c s), out ~ '(:) c s, ConcatOp c) => Instr inp out | |
pattern UNPACK :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) ('TOption a) s, UnpackedValScope a, SingI a) => Instr inp out | |
pattern PACK :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) 'TBytes s, PackedValScope a) => Instr inp out | |
pattern RENAME :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) a s) => Instr inp out | |
pattern CAST :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) a s, SingI a) => Instr inp out | |
pattern APPLY :: forall {inp} {out}. () => forall (a :: T) (b :: T) (c :: T) (s :: [T]). (inp ~ '(:) a ('(:) ('TLambda ('TPair a b) c) s), out ~ '(:) ('TLambda b c) s, ConstantScope a, SingI b) => Instr inp out | |
pattern EXEC :: forall {inp} {out}. () => forall (t1 :: T) (t2 :: T) (s :: [T]). (inp ~ '(:) t1 ('(:) ('TLambda t1 t2) s), out ~ '(:) t2 s) => Instr inp out | |
pattern LAMBDA_REC :: forall s r. () => forall i o. (SingI i, SingI o, r ~ ('TLambda i o ': s)) => (IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o]) -> Instr s r | |
pattern LAMBDA :: forall s r. () => forall i o. (SingI i, SingI o, r ~ ('TLambda i o ': s)) => (IsNotInView => RemFail Instr '[i] '[o]) -> Instr s r | |
pattern GET_AND_UPDATE :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) (UpdOpKey c) ('(:) (UpdOpParams c) ('(:) c s)), out ~ '(:) ('TOption (GetOpVal c)) ('(:) c s), GetOp c, UpdOp c, SingI (GetOpVal c), (~) (UpdOpKey c) (GetOpKey c)) => Instr inp out | |
pattern UPDATEN :: forall {inp} {out}. () => forall (ix :: Peano) (val :: T) (pair :: T) (s :: [T]). (inp ~ '(:) val ('(:) pair s), out ~ '(:) (UpdateN ix val pair) s, ConstraintUpdateN ix pair) => PeanoNatural ix -> Instr inp out | |
pattern UPDATE :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) (UpdOpKey c) ('(:) (UpdOpParams c) ('(:) c s)), out ~ '(:) c s, UpdOp c) => Instr inp out | |
pattern GETN :: forall {inp} {out}. () => forall (ix :: Peano) (pair :: T) (s :: [T]). (inp ~ '(:) pair s, out ~ '(:) (GetN ix pair) s, ConstraintGetN ix pair) => PeanoNatural ix -> Instr inp out | |
pattern GET :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) (GetOpKey c) ('(:) c s), out ~ '(:) ('TOption (GetOpVal c)) s, GetOp c, SingI (GetOpVal c)) => Instr inp out | |
pattern MEM :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) (MemOpKey c) ('(:) c s), out ~ '(:) 'TBool s, MemOp c) => Instr inp out | |
pattern MAP :: forall {inp} {out}. () => forall (c :: T) (b :: T) (s :: [T]). (inp ~ '(:) c s, out ~ '(:) (MapOpRes c b) s, MapOp c, SingI b) => Instr ('(:) (MapOpInp c) s) ('(:) b s) -> Instr inp out | |
pattern EMPTY_BIG_MAP :: forall {inp} {out}. () => forall (b :: T) (a :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TBigMap a b) s, SingI b, Comparable a, ForbidBigMap b) => Instr inp out | |
pattern EMPTY_MAP :: forall {inp} {out}. () => forall (b :: T) (a :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TMap a b) s, SingI b, Comparable a) => Instr inp out | |
pattern EMPTY_SET :: forall {inp} {out}. () => forall (e :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TSet e) s, Comparable e) => Instr inp out | |
pattern SIZE :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) c s, out ~ '(:) 'TNat s, SizeOp c) => Instr inp out | |
pattern CONS :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a ('(:) ('TList a) s), out ~ '(:) ('TList a) s) => Instr inp out | |
pattern NIL :: forall {inp} {out}. () => forall (p :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TList p) s, SingI p) => Instr inp out | |
pattern RIGHT :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) b s, out ~ '(:) ('TOr a b) s, SingI a) => Instr inp out | |
pattern LEFT :: forall {inp} {out}. () => forall (b :: T) (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) ('TOr a b) s, SingI b) => Instr inp out | |
pattern PAIRN :: forall {inp} {out}. () => forall (n :: Peano) (inp :: [T]). (inp ~ inp, out ~ PairN n inp, ConstraintPairN n inp) => PeanoNatural n -> Instr inp out | |
pattern UNPAIR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) ('TPair a b) s, out ~ '(:) a ('(:) b s)) => Instr inp out | |
pattern PAIR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) a ('(:) b s), out ~ '(:) ('TPair a b) s) => Instr inp out | |
pattern UNIT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TUnit s) => Instr inp out | |
pattern SOME :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) ('TOption a) s) => Instr inp out | |
pattern PUSH :: forall {inp} {out}. () => forall (t :: T) (s :: [T]). (inp ~ s, out ~ '(:) t s, ConstantScope t) => Value' Instr t -> Instr inp out | |
pattern DUPN :: forall {inp} {out}. () => forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T). (inp ~ inp, out ~ out, ConstraintDUPN n inp out a, DupableScope a) => PeanoNatural n -> Instr inp out | |
pattern DUP :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) a ('(:) a s), DupableScope a) => Instr inp out | |
pattern CDR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) ('TPair a b) s, out ~ '(:) b s) => Instr inp out | |
pattern CAR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) ('TPair a b) s, out ~ '(:) a s) => Instr inp out | |
pattern GE :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Ge n) s, UnaryArithOp Ge n) => Instr inp out | |
pattern SHA256 :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out | |
pattern SHA512 :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out | |
pattern LE :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Le n) s, UnaryArithOp Le n) => Instr inp out | |
pattern NONE :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TOption a) s, SingI a) => Instr inp out | |
pattern GT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Gt n) s, UnaryArithOp Gt n) => Instr inp out | |
pattern LT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Lt n) s, UnaryArithOp Lt n) => Instr inp out | |
pattern EQ :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Eq' n) s, UnaryArithOp Eq' n) => Instr inp out |
Instances
pattern ConcreteMeta :: Typeable meta => meta -> Instr i o -> Instr i o Source #
A convenience pattern synonym for Meta
,
matching on a concrete given type wrapped by SomeMeta
, e.g.
\case { ContreteMeta (x :: Word) -> ... }
pattern (:#) :: Instr a b -> Instr b c -> Instr a c infixr 8 Source #
Right-associative operator for Seq
.
>>>
Debug.show (DROP :# UNIT :# Nop) == Debug.show (DROP :# (UNIT :# Nop))
True
castInstr :: forall inp1 out1 inp2 out2. (SingI inp1, SingI out1, SingI inp2, SingI out2) => Instr inp1 out1 -> Maybe (Instr inp2 out2) Source #
mkStackRef :: forall (gn :: Nat) st n. (n ~ ToPeano gn, SingIPeano gn, RequireLongerThan st n) => StackRef st Source #
Create a stack reference, performing checks at compile time.
frameInstr :: forall s a b. Instr a b -> Instr (a ++ s) (b ++ s) Source #
Execute given instruction on truncated stack.
This is sound because for all Michelson instructions the following property
holds: if some code accepts stack i
and produces stack o
, when it can
also be run on stack i + s
producing stack o + s
; and also because
Michelson never makes implicit assumptions on types, rather you have to
express all "yet ambiguous" type information in code.
The complexity of this operation is linear in the number of instructions. If possible, avoid nested uses as that would imply multiple traversals. Worst case, complexity can become quadratic.
type SomeViewsSet = SomeViewsSet' Instr Source #
type ContractCode cp st = ContractCode' Instr cp st Source #
type Operation = Operation' Instr Source #
data PushableStorageSplit s st where Source #
Result of splitting a storage Value
of st
on the stack s
.
The idea behind this is to either: prove that the whole Value
can be put on
the stack without containing a single big_map
or to split it into:
a Value
containing its big_map
s and an instruction to reconstruct the
storage.
The main idea behind this is to create a large storage in Michelson code to
then create a contract using CREATE_CONTRACT
.
Note: a simpler solution would have been to replace big_map
Value
s with
an EMPTY_BIG_MAP
followed by many UPDATE
to push its content, but sadly
a bug (tezostezos1154) prevents this from being done.
ConstantStorage :: ConstantScope st => Value st -> PushableStorageSplit s st | The type of the storage is fully constant. |
PushableValueStorage :: StorageScope st => Instr s (st ': s) -> PushableStorageSplit s st | The type of the storage is not a constant, but its value does not contain
|
PartlyPushableStorage :: (StorageScope heavy, StorageScope st) => Value heavy -> Instr (heavy ': s) (st ': s) -> PushableStorageSplit s st | The type of the storage and part of its value (here |
data CtorEffectsApp m Source #
Describes how intermediate nodes in instruction tree are accounted.
CtorEffectsApp | |
|
Instances
Buildable (CtorEffectsApp x) Source # | |
Defined in Morley.Michelson.Typed.Util build :: CtorEffectsApp x -> Doc buildList :: [CtorEffectsApp x] -> Doc |
data DfsSettings m Source #
Options for dfsTraverseInstr
family of functions.
DfsSettings | |
|
Instances
Applicative x => Default (DfsSettings x) Source # | |
Defined in Morley.Michelson.Typed.Util def :: DfsSettings x # |
dfsTraverseInstr :: forall m inp out. Monad m => DfsSettings m -> Instr inp out -> m (Instr inp out) Source #
Traverse a typed instruction in depth-first order.
The dsInstrStep
and dsValueStep
actions will be applied in bottom-to-top order, i.e.
first to the children of a node, then to the node itself.
dfsFoldInstr :: forall x inp out. Monoid x => DfsSettings (Writer x) -> (forall i o. Instr i o -> x) -> Instr inp out -> x Source #
Specialization of dfsTraverseInstr
for case when changing the instruction is
not required.
dfsModifyInstr :: DfsSettings Identity -> (forall i o. Instr i o -> Instr i o) -> Instr inp out -> Instr inp out Source #
Specialization of dfsTraverseInstr
which only modifies given instruction.
analyzeInstrFailure :: Instr i o -> RemFail Instr i o Source #
Check whether instruction fails at each execution path or have at least one non-failing path.
This function assumes that given instruction contains no dead code (contract with dead code cannot be valid Michelson contract) and may behave in unexpected way if such is present. Term "dead code" includes instructions which render into empty Michelson, like Morley extensions. On the other hand, this function does not traverse the whole instruction tree; performs fastest on left-growing combs.
Often we already have information about instruction failure, use this function only in cases when this info is actually unavailable or hard to use.
linearizeLeft :: Instr inp out -> Instr inp out Source #
There are many ways to represent a sequence of more than 2 instructions.
E. g. for i1; i2; i3
it can be Seq i1 $ Seq i2 i3
or Seq (Seq i1 i2) i3
.
This function enforces a particular structure. Specifically, it makes each
Seq
have a single instruction (i. e. not Seq
) in its second argument.
This function also erases redundant Nop
s.
Please note that this function is not recursive, it does not
linearize contents of IF
and similar instructions.
linearizeLeftDeep :: Instr inp out -> Instr inp out Source #
"Deep" version of linearizeLeft
. It recursively linearizes
instructions stored in other instructions.
dfsMapValue :: forall t. DfsSettings Identity -> Value t -> Value t Source #
Traverse a value in depth-first order.
dfsTraverseValue :: forall t m. Monad m => DfsSettings m -> Value t -> m (Value t) Source #
Traverse a value in depth-first order.
dfsFoldMapValue :: Monoid x => (forall t'. Value t' -> x) -> Value t -> x Source #
Specialization of dfsMapValue
for case when changing the value is
not required.
dfsFoldMapValueM :: (Monoid x, Monad m) => (forall t'. Value t' -> m x) -> Value t -> m x Source #
Specialization of dfsMapValue
for case when changing the value is
not required.
isBytesValue :: Value t -> Maybe ByteString Source #
If value is a bytestring, return the stored bytestring.
allAtomicValues :: forall t a. (forall t'. Value t' -> Maybe a) -> Value t -> [a] Source #
Takes a selector which checks whether a value can be converted to something. Recursively applies it to all values. Collects extracted values in a list.
splitPushableStorage :: StorageScope t => Value t -> PushableStorageSplit s t Source #
Splits the given storage Value
into a PushableStorageSplit
.
This is based off the fact that the only storages that cannot be directly
PUSH
ed are the ones that contain BigMap
s and tickets.
See difference between StorageScope
and ConstantScope
.
So what we do here is to create a Value
as small as possible with all the
big_map
s in it (if any) and an Instr
that can use it to rebuild the original
storage Value
.
Note: This is done this way to avoid using EMPTY_BIG_MAP
instructions, see
PushableStorageSplit
for motivation.
isMichelsonInstr :: Instr i o -> Bool Source #
Whether this instruction is a real Michelson instruction.
Only the root is in question, children in the instruction tree are not accounted for.
>>>
isMichelsonInstr (Seq Nop Nop)
True
>>>
isMichelsonInstr (Ext $ COMMENT_ITEM "comment")
False
This function is helpful e.g. in debugger.
instrAnns :: Instr i o -> Maybe SomeAnns Source #
Get annotations from a typed Instr
. This doesn't recurse, use with
dfsFoldInstr
to collect all annotations in a tree/sequence.
class IsoValuesStack (ts :: [Type]) where Source #
Isomorphism between Michelson stack and its Haskell reflection.
toValStack :: Rec Identity ts -> Rec Value (ToTs ts) Source #
fromValStack :: Rec Value (ToTs ts) -> Rec Identity ts Source #
Instances
IsoValuesStack ('[] :: [Type]) Source # | |
(IsoValue t, IsoValuesStack st) => IsoValuesStack (t ': st) Source # | |
type family ToTs (ts :: [Type]) :: [T] where ... Source #
Type function to convert a Haskell stack type to T
-based one.
type GenericIsoValue t = (IsoValue t, Generic t, ToT t ~ GValueType (Rep t)) Source #
Whether Michelson representation of the type is derived via Generics.
class ToBigMap m where Source #
type ToBigMapKey m Source #
type ToBigMapValue m Source #
mkBigMap :: m -> BigMap (ToBigMapKey m) (ToBigMapValue m) Source #
Instances
Instances
Phantom type that represents the ID of a big_map with
keys of type k
and values of type v
.
Instances
(Typeable k2, Typeable v, Typeable k1, Typeable k3) => Data (BigMapId k2 v) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Value gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BigMapId k2 v -> c (BigMapId k2 v) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (BigMapId k2 v) # toConstr :: BigMapId k2 v -> Constr # dataTypeOf :: BigMapId k2 v -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (BigMapId k2 v)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (BigMapId k2 v)) # gmapT :: (forall b. Data b => b -> b) -> BigMapId k2 v -> BigMapId k2 v # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BigMapId k2 v -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BigMapId k2 v -> r # gmapQ :: (forall d. Data d => d -> u) -> BigMapId k2 v -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BigMapId k2 v -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BigMapId k2 v -> m (BigMapId k2 v) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BigMapId k2 v -> m (BigMapId k2 v) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BigMapId k2 v -> m (BigMapId k2 v) # | |
Num (BigMapId k2 v) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Value (+) :: BigMapId k2 v -> BigMapId k2 v -> BigMapId k2 v # (-) :: BigMapId k2 v -> BigMapId k2 v -> BigMapId k2 v # (*) :: BigMapId k2 v -> BigMapId k2 v -> BigMapId k2 v # negate :: BigMapId k2 v -> BigMapId k2 v # abs :: BigMapId k2 v -> BigMapId k2 v # signum :: BigMapId k2 v -> BigMapId k2 v # fromInteger :: Integer -> BigMapId k2 v # | |
Show (BigMapId k2 v) Source # | |
IsoValue (BigMapId k2 v) Source # | |
Buildable (BigMapId k2 v) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Value | |
type ToT (BigMapId k2 v) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Value |
data Ticket (arg :: Type) Source #
Ticket type.
Instances
Show arg => Show (Ticket arg) Source # | |
Eq arg => Eq (Ticket arg) Source # | |
PolyTypeHasDocC '[a] => TypeHasDoc (Ticket a) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc type TypeDocFieldDescriptions (Ticket a) :: FieldDescriptions Source # typeDocName :: Proxy (Ticket a) -> Text Source # typeDocMdDescription :: Markdown Source # typeDocMdReference :: Proxy (Ticket a) -> WithinParens -> Markdown Source # typeDocDependencies :: Proxy (Ticket a) -> [SomeDocDefinitionItem] Source # typeDocHaskellRep :: TypeDocHaskellRep (Ticket a) Source # typeDocMichelsonRep :: TypeDocMichelsonRep (Ticket a) Source # | |
(Comparable (ToT a), IsoValue a) => IsoValue (Ticket a) Source # | |
type TypeDocFieldDescriptions (Ticket a) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc | |
type ToT (Ticket a) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Value |
data ContractRef (arg :: Type) Source #
Since Contract
name is used to designate contract code, lets call
analogy of TContract
type as follows.
Note that type argument always designates an argument of entrypoint.
If a contract has explicit default entrypoint (and no root entrypoint),
ContractRef
referring to it can never have the entire parameter as its
type argument.
Instances
type SomeEntrypointCall arg = SomeEntrypointCallT (ToT arg) Source #
type EntrypointCall param arg = EntrypointCallT (ToT param) (ToT arg) Source #
class WellTypedToT a => IsoValue a where Source #
Isomorphism between Michelson values and plain Haskell types.
Default implementation of this typeclass converts ADTs to Michelson "pair"s and "or"s.
Nothing
Type function that converts a regular Haskell type into a T
type.
type ToT a = GValueType (Rep a)
toVal :: a -> Value (ToT a) Source #
Converts a Haskell structure into Value
representation.
default toVal :: (Generic a, GIsoValue (Rep a), ToT a ~ GValueType (Rep a)) => a -> Value (ToT a) Source #
fromVal :: Value (ToT a) -> a Source #
Converts a Value
into Haskell type.
Instances
isoValue :: (IsoValue a, IsoValue b) => Iso (Value (ToT a)) (Value (ToT b)) a b Source #
An optic witnessing the isomorphism between a michelson type and a haskell type.
coerceContractRef :: ToT a ~ ToT b => ContractRef a -> ContractRef b Source #
Replace type argument of ContractRef
with isomorphic one.
contractRefToAddr :: ContractRef cp -> EpAddress Source #
type InstrUnwrapC dt name = (GenericIsoValue dt, GInstrUnwrap (Rep dt) (LnrBranch (GetNamed name dt)) (CtorOnlyField name dt)) Source #
type family GCaseBranchInput ctor x :: CaseClauseParam Source #
Instances
type GCaseBranchInput ctor (U1 :: Type -> Type) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseBranchInput ctor (Rec0 a) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseBranchInput ctor (x :*: y) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseBranchInput ctor (S1 i x) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum |
type family GCaseBranchInput ctor x :: CaseClauseParam Source #
Instances
type GCaseBranchInput ctor (U1 :: Type -> Type) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseBranchInput ctor (Rec0 a) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseBranchInput ctor (x :*: y) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseBranchInput ctor (S1 i x) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum |
type family GCaseClauses x rest :: [CaseClauseParam] Source #
Instances
type GCaseClauses (V1 :: Type -> Type) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseClauses (x :+: y) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseClauses (C1 ('MetaCons ctor _1 _2) x) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseClauses (D1 i x) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum |
type family GCaseClauses x rest :: [CaseClauseParam] Source #
Instances
type GCaseClauses (V1 :: Type -> Type) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseClauses (x :+: y) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseClauses (C1 ('MetaCons ctor _1 _2) x) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseClauses (D1 i x) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum |
type CaseClauses a = GCaseClauses (Rep a) '[] Source #
List of CaseClauseParam
s required to pattern match on the given type.
data CaseClause (inp :: [T]) (out :: [T]) (param :: CaseClauseParam) where Source #
Type information about single case clause.
CaseClause :: RemFail Instr (AppendCtorField x inp) out -> CaseClause inp out ('CaseClauseParam ctor x) |
data CaseClauseParam Source #
In what different case branches differ - related constructor name and input stack type which the branch starts with.
type InstrCaseC dt = (GenericIsoValue dt, GInstrCase (Rep dt) '[]) Source #
data MyCompoundType Source #
Instances
Generic MyCompoundType Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum type Rep MyCompoundType :: Type -> Type # from :: MyCompoundType -> Rep MyCompoundType x # to :: Rep MyCompoundType x -> MyCompoundType # | |
IsoValue MyCompoundType Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum type ToT MyCompoundType :: T Source # toVal :: MyCompoundType -> Value (ToT MyCompoundType) Source # fromVal :: Value (ToT MyCompoundType) -> MyCompoundType Source # | |
type Rep MyCompoundType Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type ToT MyCompoundType Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum |
type InstrWrapOneC dt name = (InstrWrapC dt name, GetCtorField dt name ~ 'OneField (CtorOnlyField name dt)) Source #
type InstrWrapC dt name = (GenericIsoValue dt, GInstrWrap (Rep dt) (LnrBranch (GetNamed name dt)) (LnrFieldType (GetNamed name dt))) Source #
type CtorOnlyField name dt = RequireOneField name (GetCtorField dt name) Source #
Expect referred constructor to have only one field (otherwise compile error is raised) and extract its type.
type CtorHasOnlyField ctor dt f = GetCtorField dt ctor ~ 'OneField f Source #
Expect referred constructor to have only one field (in form of constraint) and extract its type.
type GetCtorField dt ctor = LnrFieldType (GetNamed ctor dt) Source #
Get type of constructor fields (one or zero) referred by given datatype and name.
type family IsPrimitiveValue (x :: Type) :: Bool where ... Source #
Whether given type represents an atomic Michelson value.
IsPrimitiveValue (Maybe _) = 'True | |
IsPrimitiveValue (NamedF _ _ _) = 'True | |
IsPrimitiveValue Integer = 'True | |
IsPrimitiveValue Natural = 'True | |
IsPrimitiveValue Text = 'True | |
IsPrimitiveValue MText = 'True | |
IsPrimitiveValue Bool = 'True | |
IsPrimitiveValue ByteString = 'True | |
IsPrimitiveValue Mutez = 'True | |
IsPrimitiveValue Address = 'True | |
IsPrimitiveValue EpAddress = 'True | |
IsPrimitiveValue KeyHash = 'True | |
IsPrimitiveValue Timestamp = 'True | |
IsPrimitiveValue PublicKey = 'True | |
IsPrimitiveValue Signature = 'True | |
IsPrimitiveValue (ContractRef _) = 'True | |
IsPrimitiveValue (BigMap _ _) = 'True | |
IsPrimitiveValue (Map _ _) = 'True | |
IsPrimitiveValue (Set _) = 'True | |
IsPrimitiveValue [_] = 'True | |
IsPrimitiveValue (Operation' _) = 'True | |
IsPrimitiveValue ChainId = 'True | |
IsPrimitiveValue _ = 'False |
type AppendCtorFieldAxiom (cf :: CtorField) (st :: [Type]) = ToTs (AppendCtorField cf st) ~ AppendCtorField cf (ToTs st) Source #
To use AppendCtorField
not only here for T
-based stacks, but also
later in Lorentz with Type
-based stacks we need the following property.
type family AppendCtorField cf l where ... Source #
Push field to stack, if any.
AppendCtorField ('OneField t) (l :: [T]) = ToT t ': l | |
AppendCtorField ('OneField t) (l :: [Type]) = t ': l | |
AppendCtorField 'NoFields (l :: [T]) = l | |
AppendCtorField 'NoFields (l :: [Type]) = l |
type family ExtractCtorField (cf :: CtorField) where ... Source #
Get something as field of the given constructor.
ExtractCtorField ('OneField t) = t | |
ExtractCtorField 'NoFields = () |
We support only two scenarious - constructor with one field and without fields. Nonetheless, it's not that sad since for sum types we can't even assign names to fields if there are many (the style guide prohibits partial records).
appendCtorFieldAxiom :: (AppendCtorFieldAxiom ('OneField Word) '[Int], AppendCtorFieldAxiom 'NoFields '[Int]) => Dict (AppendCtorFieldAxiom cf st) Source #
Proof of AppendCtorFieldAxiom
.
instrWrap :: forall dt name st. InstrWrapC dt name => Label name -> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt ': st) Source #
Wrap given element into a constructor with the given name.
Mentioned constructor must have only one field.
Since labels interpretable by OverloadedLabels
extension cannot
start with capital latter, prepend constructor name with letter
"c" (see examples below).
instrWrapOne :: forall dt name st. InstrWrapOneC dt name => Label name -> Instr (ToT (CtorOnlyField name dt) ': st) (ToT dt ': st) Source #
Like instrWrap
but only works for contructors with a single field.
Results in a type error if a constructor with no field is used instead.
hsWrap :: forall dt name. InstrWrapC dt name => Label name -> ExtractCtorField (GetCtorField dt name) -> dt Source #
Wrap a haskell value into a constructor with the given name.
This is symmetric to instrWrap
.
instrCase :: forall dt out inp. InstrCaseC dt => Rec (CaseClause inp out) (CaseClauses dt) -> RemFail Instr (ToT dt ': inp) out Source #
Pattern-match on the given datatype.
(//->) :: Label ("c" `AppendSymbol` ctor) -> RemFail Instr (AppendCtorField x inp) out -> CaseClause inp out ('CaseClauseParam ctor x) infixr 8 Source #
Lift an instruction to case clause.
You should write out constructor name corresponding to the clause explicitly. Prefix constructor name with "c" letter, otherwise your label will not be recognized by Haskell parser. Passing constructor name can be circumvented but doing so is not recomended as mentioning contructor name improves readability and allows avoiding some mistakes.
unsafeInstrUnwrap :: forall dt name st. InstrUnwrapC dt name => Label name -> Instr (ToT dt ': st) (ToT (CtorOnlyField name dt) ': st) Source #
Unwrap a constructor with the given name.
Rules which apply to instrWrap
function work here as well.
Although, unlike instrWrap
, this function does not work for nullary
constructors.
hsUnwrap :: forall dt name. InstrUnwrapC dt name => Label name -> dt -> Maybe (CtorOnlyField name dt) Source #
Try to unwrap a constructor with the given name.
type InstrDeconstructC dt st = (GenericIsoValue dt, GInstrDeconstruct (Rep dt) '[] st) Source #
Constraint for instrConstruct
.
type family GFieldTypes x rest :: [Type] Source #
Instances
type GFieldTypes (U1 :: Type -> Type) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Product | |
type GFieldTypes (V1 :: Type -> Type) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Product | |
type GFieldTypes (Rec0 a) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Product | |
type GFieldTypes (x :*: y) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Product | |
type GFieldTypes (x :+: y) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Product | |
type GFieldTypes (M1 t i x) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Product |
type family GFieldTypes x rest :: [Type] Source #
Instances
type GFieldTypes (U1 :: Type -> Type) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Product | |
type GFieldTypes (V1 :: Type -> Type) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Product | |
type GFieldTypes (Rec0 a) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Product | |
type GFieldTypes (x :*: y) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Product | |
type GFieldTypes (x :+: y) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Product | |
type GFieldTypes (M1 t i x) rest Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Product |
type InstrConstructC dt = (GenericIsoValue dt, GInstrConstruct (Rep dt) '[]) Source #
Constraint for instrConstruct
and gInstrConstructStack
.
type ConstructorFieldNames dt = GFieldNames (Rep dt) Source #
Names of all fields in a datatype.
type ConstructorFieldTypes dt = GFieldTypes (Rep dt) '[] Source #
Types of all fields in a datatype.
class ToTs xs ~ ToTs ys => CastFieldConstructors xs ys where Source #
Ability to pass list of fields with the same ToTs. It may be useful if you don't want to work with NamedF in ConstructorFieldTypes.
castFieldConstructorsImpl :: Rec (FieldConstructor st) xs -> Rec (FieldConstructor st) ys Source #
Instances
CastFieldConstructors ('[] :: [Type]) ('[] :: [Type]) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Product castFieldConstructorsImpl :: forall {k} (st :: [k]). Rec (FieldConstructor st) '[] -> Rec (FieldConstructor st) '[] Source # | |
(CastFieldConstructors xs ys, ToTs xs ~ ToTs ys, ToT x ~ ToT y) => CastFieldConstructors (x ': xs) (y ': ys) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Product castFieldConstructorsImpl :: forall {k} (st :: [k]). Rec (FieldConstructor st) (x ': xs) -> Rec (FieldConstructor st) (y ': ys) Source # |
newtype FieldConstructor (st :: [k]) (field :: Type) Source #
Way to construct one of the fields in a complex datatype.
FieldConstructor (Instr (ToTs' st) (ToT field ': ToTs' st)) |
type InstrSetFieldC dt name = (GenericIsoValue dt, GInstrSetField name (Rep dt) (LnrBranch (GetNamed name dt)) (LnrFieldType (GetNamed name dt))) Source #
Constraint for instrSetField
.
type InstrGetFieldC dt name = (GenericIsoValue dt, GInstrGet name (Rep dt) (LnrBranch (GetNamed name dt)) (LnrFieldType (GetNamed name dt))) Source #
Constraint for instrGetField
.
type GetFieldType dt name = LnrFieldType (GetNamed name dt) Source #
Get type of field by datatype it is contained in and field name.
type family GLookupNamed (name :: Symbol) (x :: Type -> Type) :: Maybe LookupNamedResult where ... Source #
GLookupNamed name (D1 _ x) = GLookupNamed name x | |
GLookupNamed name (C1 _ x) = GLookupNamed name x | |
GLookupNamed name (S1 ('MetaSel ('Just recName) _ _ _) (Rec0 a)) = If (name == recName) ('Just $ 'LNR a '[]) 'Nothing | |
GLookupNamed name (S1 _ (Rec0 (NamedF f a fieldName))) = If (name == fieldName) ('Just $ 'LNR (NamedInner (NamedF f a fieldName)) '[]) 'Nothing | |
GLookupNamed _ (S1 _ _) = 'Nothing | |
GLookupNamed name (x :*: y) = LNMergeFound name (GLookupNamed name x) (GLookupNamed name y) | |
GLookupNamed name (_ :+: _) = TypeError (('Text "Cannot seek for a field " :<>: 'ShowType name) :<>: 'Text " in sum type") | |
GLookupNamed _ U1 = 'Nothing | |
GLookupNamed _ V1 = TypeError ('Text "Cannot access fields of void-like type") |
instrToField :: forall dt name st. InstrGetFieldC dt name => Label name -> Instr (ToT dt ': st) (ToT (GetFieldType dt name) ': st) Source #
Make an instruction which accesses given field of the given datatype.
instrGetField :: forall dt name st. (InstrGetFieldC dt name, DupableScope (ToT (GetFieldType dt name))) => Label name -> Instr (ToT dt ': st) (ToT (GetFieldType dt name) ': (ToT dt ': st)) Source #
Make an instruction which copies given field of the given datatype.
This behaves exactly as Seq DUP (instrToField #name)
, but does not require
the entire datatype to be dupable (the field ofc still must be dupable).
If we follow the path from the root to the copied field in the pairs tree, the more nodes contain non-dupable elements in the subtree, the less efficient this function becomes. Assuming that all fields are accessed equally often, the most optimal representation would be to put all dupable elements to one subtree of the root, and all non-dupable elements in the second subtree of the root.
instrGetFieldOpen :: forall dt name res st. InstrGetFieldC dt name => Instr '[ToT (GetFieldType dt name)] '[res, ToT (GetFieldType dt name)] -> Instr '[ToT (GetFieldType dt name)] '[res] -> Label name -> Instr (ToT dt ': st) (res ': (ToT dt ': st)) Source #
"Open" version of instrGetField
, meaning that it accepts
continuations that accept the copied field. This allows chaining
getters without requiring DupableScope
on the intermediate fields.
Accepted continuations:
- The one that leaves the field on stack (and does a duplication inside). Used when the datatype had an unfortunate placement of non-dupable fields, or the intermediate field contains non-dupable elements, so the duplication cannot occur automatically in between.
- The one that consumes the field, used in case we managed to call
DUP
earlier to make the instruction's implementation smaller, and now we only need to access the field withCAR
andCDR
s.
Note that only one continuation will be chosen eventually, no contract size overhead is expected in this regard.
instrSetField :: forall dt name st. InstrSetFieldC dt name => Label name -> Instr (ToT (GetFieldType dt name) ': (ToT dt ': st)) (ToT dt ': st) Source #
For given complex type dt
and its field fieldTy
update the field value.
instrSetFieldOpen :: forall dt name new st. InstrSetFieldC dt name => Instr '[new, ToT (GetFieldType dt name)] '[ToT (GetFieldType dt name)] -> Label name -> Instr (new ': (ToT dt ': st)) (ToT dt ': st) Source #
"Open" version of instrSetField
, meaning that it accepts a continuation
that describes how to update the field. This allows chaining setters with
zero overhead and without requiring DupableScope
on the intermediate fields
(if we supported only closed setters that work directly with one datatype, we
would need to duplicate intermediate fields to chain setters).
instrConstruct :: forall dt st. InstrConstructC dt => Rec (FieldConstructor st) (ConstructorFieldTypes dt) -> Instr st (ToT dt ': st) Source #
For given complex type dt
and its field fieldTy
update the field value.
instrConstructStack :: forall dt stack st. (InstrConstructC dt, stack ~ ToTs (ConstructorFieldTypes dt)) => Instr (stack ++ st) (ToT dt ': st) Source #
instrDeconstruct :: forall dt stack (st :: [T]). (InstrDeconstructC dt st, stack ~ ToTs (GFieldTypes (Rep dt) '[])) => Instr (ToT dt ': st) (stack ++ st) Source #
For given complex type dt
deconstruct it to its field types.
convertParamNotes :: ParamNotes cp -> ParameterType Source #
Convert typed parameter annotations to an untyped ParameterType
.
convertContractCode :: forall param store. (SingI param, SingI store) => ContractCode param store -> Contract Source #
Convert typed ContractCode
to an untyped Contract
.
convertContractCodeOptimized :: forall param store. (SingI param, SingI store) => ContractCode param store -> Contract Source #
Convert typed ContractCode
to an untyped Contract
using optimized
representation.
convertView :: forall arg store ret. View arg store ret -> View Source #
convertSomeView :: SomeView st -> View Source #
convertContract :: Contract param store -> Contract Source #
convertContractOptimized :: Contract param store -> Contract Source #
untypeValue :: ForbidOp t => Value' Instr t -> Value Source #
Convert a typed value to an untyped human-readable representation
untypeValueHashable :: ForbidOp t => Value' Instr t -> Value Source #
Like untypeValueOptimized
, but without list notation for pairs.
Created to match octez-client hash data
behaviour for typed values.
untypeValueOptimized :: ForbidOp t => Value' Instr t -> Value Source #
Convert a typed value to an untyped optimized representation
untypeDemoteT :: forall (t :: T). SingI t => Ty Source #
Convert a Haskell type-level type tag into an untyped value representation.
This function is intended to be used with TypeApplications
.
instrToOpsOptimized :: HasCallStack => Instr inp out -> [ExpandedOp] Source #
Convert Haskell-typed Instr
to a list of optimized untyped operations
instrToOps :: HasCallStack => Instr inp out -> [ExpandedOp] Source #
Convert Haskell-typed Instr
to a list of human-readable untyped operations
sampleTypedValue :: forall t. WellTyped t => Sing t -> Maybe (Value t) Source #
Generate a value used for generating examples in documentation.
Since not for all types it is possible to produce a sensible example,
the result is optional. E.g. for operations, never
, not proper
types like contract operation
we return Nothing
.
flattenEntrypoints :: HandleImplicitDefaultEp -> ParamNotes t -> Map EpName Ty Source #
Flatten a provided list of notes to a map of its entrypoints and its
corresponding utype. Please refer to mkEntrypointsMap
in regards to how
duplicate entrypoints are handled.
data SomeVBigMap where Source #
SomeVBigMap :: forall k v. Value ('TBigMap k v) -> SomeVBigMap |
data SomeContractAndStorage where Source #
Represents a typed contract & a storage value of the type expected by the contract.
SomeContractAndStorage :: forall cp st. (StorageScope st, ParameterScope cp) => Contract cp st -> Value st -> SomeContractAndStorage |
Instances
Show SomeContractAndStorage Source # | |
Defined in Morley.Michelson.Typed.Existential showsPrec :: Int -> SomeContractAndStorage -> ShowS # show :: SomeContractAndStorage -> String # showList :: [SomeContractAndStorage] -> ShowS # |
data SomeContract where Source #
SomeContract :: Contract cp st -> SomeContract |
Instances
Show SomeContract Source # | |
Defined in Morley.Michelson.Typed.Existential showsPrec :: Int -> SomeContract -> ShowS # show :: SomeContract -> String # showList :: [SomeContract] -> ShowS # | |
NFData SomeContract Source # | |
Defined in Morley.Michelson.Typed.Existential rnf :: SomeContract -> () # |
data SomeIsoValue where Source #
Hides some Haskell value put in line with Michelson Value
.
SomeIsoValue :: KnownIsoT a => a -> SomeIsoValue |
type SomeValue = SomeConstrainedValue SingI Source #
type SomeConstrainedValue c = Constrained c Value Source #
type LooseSumC dt = (Generic dt, GLooseSum (Rep dt)) Source #
Constraint for toTaggedVal
and fromTaggedVal
.
data ComposeResult a Source #
Possible outcomes of an attempt to construct a Haskell ADT value from constructor name and relevant data.
ComposeOk a | Composed fine. |
ComposeCtorNotFound | No constructor with such name. |
ComposeFieldTypeMismatch T T | Found required constructor, but type of data does not correspond to provided one. |
Instances
Functor ComposeResult Source # | |
Defined in Morley.Michelson.Typed.Haskell.LooseSum fmap :: (a -> b) -> ComposeResult a -> ComposeResult b # (<$) :: a -> ComposeResult b -> ComposeResult a # | |
Monoid (ComposeResult a) Source # | |
Defined in Morley.Michelson.Typed.Haskell.LooseSum mempty :: ComposeResult a # mappend :: ComposeResult a -> ComposeResult a -> ComposeResult a # mconcat :: [ComposeResult a] -> ComposeResult a # | |
Semigroup (ComposeResult a) Source # | |
Defined in Morley.Michelson.Typed.Haskell.LooseSum (<>) :: ComposeResult a -> ComposeResult a -> ComposeResult a # sconcat :: NonEmpty (ComposeResult a) -> ComposeResult a # stimes :: Integral b => b -> ComposeResult a -> ComposeResult a # |
toTaggedVal :: LooseSumC dt => dt -> (Text, SomeValue) Source #
Decompose Haskell type into constructor name and
data it carries, converting the latter into Michelson Value
.
fromTaggedVal :: LooseSumC dt => (Text, SomeValue) -> ComposeResult dt Source #
Inverse to toTaggedVal
.
data SomeAnnotatedValue where Source #
SomeAnnotatedValue :: forall t. SingI t => Notes t -> Value t -> SomeAnnotatedValue |
Instances
Show SomeAnnotatedValue Source # | |
Defined in Morley.Michelson.Typed.AnnotatedValue showsPrec :: Int -> SomeAnnotatedValue -> ShowS # show :: SomeAnnotatedValue -> String # showList :: [SomeAnnotatedValue] -> ShowS # | |
Eq SomeAnnotatedValue Source # | |
Defined in Morley.Michelson.Typed.AnnotatedValue (==) :: SomeAnnotatedValue -> SomeAnnotatedValue -> Bool # (/=) :: SomeAnnotatedValue -> SomeAnnotatedValue -> Bool # | |
Buildable SomeAnnotatedValue Source # | |
Defined in Morley.Michelson.Typed.AnnotatedValue build :: SomeAnnotatedValue -> Doc buildList :: [SomeAnnotatedValue] -> Doc |
data AnnotatedValue v Source #
Instances
Show (AnnotatedValue v) Source # | |
Defined in Morley.Michelson.Typed.AnnotatedValue showsPrec :: Int -> AnnotatedValue v -> ShowS # show :: AnnotatedValue v -> String # showList :: [AnnotatedValue v] -> ShowS # | |
Eq (AnnotatedValue v) Source # | |
Defined in Morley.Michelson.Typed.AnnotatedValue (==) :: AnnotatedValue v -> AnnotatedValue v -> Bool # (/=) :: AnnotatedValue v -> AnnotatedValue v -> Bool # | |
Buildable (AnnotatedValue v) Source # | |
Defined in Morley.Michelson.Typed.AnnotatedValue build :: AnnotatedValue v -> Doc buildList :: [AnnotatedValue v] -> Doc |
Representation of a field with an optional description.
data ConstructorRep a Source #
Representation of a constructor with an optional description.
type ADTRep a = [ConstructorRep a] Source #
Stands for representation of some Haskell ADT corresponding to
Michelson value. Type parameter a
is what you put in place of
each field of the datatype, e.g. information about field type.
This representation also includes descriptions of constructors and fields.
crDescriptionL :: forall a. Lens' (ConstructorRep a) (Maybe Text) Source #
crFieldsL :: forall a a. Lens (ConstructorRep a) (ConstructorRep a) [FieldRep a] [FieldRep a] Source #
type PolyTypeHasDocC ts = Each '[TypeHasDoc] ts Source #
Constraint, required when deriving TypeHasDoc
for polymorphic type
with the least possible number of methods defined manually.
class GProductHasDoc (x :: Type -> Type) Source #
Product type traversal for TypeHasDoc
.
gProductDocHaskellRep
Instances
GProductHasDoc (U1 :: Type -> Type) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc gProductDocHaskellRep :: [(Text, Text)] -> [FieldRep SomeTypeWithDoc] | |
(GProductHasDoc x, GProductHasDoc y) => GProductHasDoc (x :*: y) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc gProductDocHaskellRep :: [(Text, Text)] -> [FieldRep SomeTypeWithDoc] | |
(TypeHasDoc a, KnownSymbol field) => GProductHasDoc (S1 ('MetaSel ('Just field) _1 _2 _3) (Rec0 a)) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc gProductDocHaskellRep :: [(Text, Text)] -> [FieldRep SomeTypeWithDoc] | |
TypeHasDoc a => GProductHasDoc (S1 ('MetaSel ('Nothing :: Maybe Symbol) _1 _2 _3) (Rec0 a)) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc gProductDocHaskellRep :: [(Text, Text)] -> [FieldRep SomeTypeWithDoc] |
class GTypeHasDoc (x :: Type -> Type) Source #
Generic traversal for automatic deriving of some methods in TypeHasDoc
.
gTypeDocHaskellRep
Instances
GTypeHasDoc (V1 :: Type -> Type) Source # | |
(GTypeHasDoc x, GTypeHasDoc y) => GTypeHasDoc (x :+: y) Source # | |
(GProductHasDoc x, KnownSymbol ctor) => GTypeHasDoc (C1 ('MetaCons ctor _1 _2) x) Source # | |
GTypeHasDoc x => GTypeHasDoc (D1 ('MetaData _a _b _c 'False) x) Source # | |
GTypeHasDoc x => GTypeHasDoc (D1 ('MetaData _a _b _c 'True) x) Source # | |
class IsHomomorphic a Source #
Require this type to be homomorphic.
Instances
IsHomomorphic (a :: k) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc | |
(TypeError ('Text "Type is not homomorphic: " :<>: 'ShowType (a b)) :: Constraint) => IsHomomorphic (a b :: k2) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc |
class HaveCommonTypeCtor a b Source #
Require two types to be built from the same type constructor.
E.g. HaveCommonTypeCtor (Maybe Integer) (Maybe Natural)
is defined,
while HaveCmmonTypeCtor (Maybe Integer) [Integer]
is not.
Instances
HaveCommonTypeCtor (a :: k) (a :: k) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc | |
HaveCommonTypeCtor ac bc => HaveCommonTypeCtor (ac a :: k2) (bc b :: k4) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc |
newtype DStorageType Source #
Doc element with description of contract storage type.
Instances
Doc element with description of a type.
DType :: TypeHasDoc a => Proxy a -> DType |
Instances
Eq DType Source # | |
Ord DType Source # | |
DocItem DType Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc type DocItemPlacement DType :: DocItemPlacementKind Source # type DocItemReferenced DType :: DocItemReferencedKind Source # docItemPos :: Natural Source # docItemSectionName :: Maybe Text Source # docItemSectionDescription :: Maybe Markdown Source # docItemSectionNameStyle :: DocSectionNameStyle Source # docItemRef :: DType -> DocItemRef (DocItemPlacement DType) (DocItemReferenced DType) Source # docItemToMarkdown :: HeaderLevel -> DType -> Markdown Source # docItemToToc :: HeaderLevel -> DType -> Markdown Source # docItemDependencies :: DType -> [SomeDocDefinitionItem] Source # docItemsOrder :: [DType] -> [DType] Source # | |
Buildable DType Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc | |
type DocItemPlacement DType Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc | |
type DocItemReferenced DType Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc |
data SomeTypeWithDoc where Source #
Data hides some type implementing TypeHasDoc
.
SomeTypeWithDoc :: TypeHasDoc td => Proxy td -> SomeTypeWithDoc |
type TypeDocMichelsonRep a = Proxy a -> (Maybe DocTypeRepLHS, T) Source #
Signature of typeDocMichelsonRep
function.
As in TypeDocHaskellRep
, set the first element of the pair to Nothing
for primitive types, otherwise it stands as some instantiation of a type,
and its Michelson representation is given in the second element of the pair.
Examples of rendered representation:
pair int nat
- for homomorphic type.MyError Integer = pair string int
- concrete sample for polymorphic type.
type TypeDocHaskellRep a = Proxy a -> FieldDescriptionsV -> Maybe (Maybe DocTypeRepLHS, ADTRep SomeTypeWithDoc) Source #
Signature of typeDocHaskellRep
function.
A value of FieldDescriptionsV
is provided by the library to make sure that
instances won't replace it with an unchecked value.
When value is Just
, it contains types which this type is built from.
First element of provided pair may contain name a concrete type which has
the same type constructor as a
(or just a
for homomorphic types), and
the second element of the pair - its unfolding in Haskell.
For example, for some newtype MyNewtype = MyNewtype (Integer, Natural)
we would not specify the first element in the pair because MyNewtype
is
already a concrete type, and second element would contain (Integer, Natural)
.
For polymorphic types like newtype MyPolyNewtype a = MyPolyNewtype (Text, a)
,
we want to describe its representation on some example of a
, because
working with type variables is too non-trivial; so the first element of
the pair may be e.g. "MyPolyNewType Integer"
, and the second one shows
that it unfolds to (Text, Integer)
.
When rendered, values of this type look like:
(Integer, Natural)
- for homomorphic type.MyError Integer = (Text, Integer)
- concrete sample for polymorphic type.
class (Typeable a, SingI (TypeDocFieldDescriptions a), FieldDescriptionsValid (TypeDocFieldDescriptions a) a) => TypeHasDoc a where Source #
Description for a Haskell type appearing in documentation.
type TypeDocFieldDescriptions a :: FieldDescriptions Source #
Description of constructors and fields of a
.
See FieldDescriptions
documentation for an example of usage.
Descriptions will be checked at compile time to make sure that only existing constructors and fields are referenced.
For that check to work instance Generic a
is required whenever TypeDocFieldDescriptions
is not empty.
For implementation of the check see FieldDescriptionsValid
type family.
type TypeDocFieldDescriptions _ = '[]
typeDocName :: Proxy a -> Text Source #
Name of type as it appears in definitions section.
Each type must have its own unique name because it will be used in identifier for references.
Default definition derives name from Generics. If it does not fit, consider defining this function manually. (We tried using Data.Data for this, but it produces names including module names which is not do we want).
default typeDocName :: (Generic a, KnownSymbol (GenericTypeName a)) => Proxy a -> Text Source #
typeDocMdDescription :: Markdown Source #
Explanation of a type. Markdown formatting is allowed.
typeDocMdReference :: Proxy a -> WithinParens -> Markdown Source #
How reference to this type is rendered, in Markdown.
Examples:
[Integer](#type-integer)
,[Maybe](#type-Maybe) [()](#type-unit)
.
Consider using one of the following functions as default implementation; which one to use depends on number of type arguments in your type:
If none of them fits your purposes precisely, consider using
customTypeDocMdReference
.
default typeDocMdReference :: (Typeable a, IsHomomorphic a) => Proxy a -> WithinParens -> Markdown Source #
typeDocDependencies :: Proxy a -> [SomeDocDefinitionItem] Source #
All types which this type directly contains.
Used in automatic types discovery.
default typeDocDependencies :: (Generic a, GTypeHasDoc (Rep a)) => Proxy a -> [SomeDocDefinitionItem] Source #
typeDocHaskellRep :: TypeDocHaskellRep a Source #
For complex types - their immediate Haskell representation.
For primitive types set this to Nothing
.
For homomorphic types use homomorphicTypeDocHaskellRep
implementation.
For polymorphic types consider using concreteTypeDocHaskellRep
as implementation.
Modifier haskellRepNoFields
can be used to hide names of fields,
beneficial for newtypes.
Use haskellRepAdjust
or haskellRepMap
for more involved adjustments.
Also, consider defining an instance of TypeHasFieldNamingStrategy
instead
of defining this method -- the former can be used downstream, e.g. in
lorentz, for better naming consistency.
default typeDocHaskellRep :: (Generic a, GTypeHasDoc (Rep a), IsHomomorphic a, TypeHasFieldNamingStrategy a) => TypeDocHaskellRep a Source #
typeDocMichelsonRep :: TypeDocMichelsonRep a Source #
Final michelson representation of a type.
For homomorphic types use homomorphicTypeDocMichelsonRep
implementation.
For polymorphic types consider using concreteTypeDocMichelsonRep
as implementation.
default typeDocMichelsonRep :: (KnownIsoT a, IsHomomorphic a) => TypeDocMichelsonRep a Source #
Instances
data FieldSnakeCase Source #
Empty datatype used as marker for DerivingVia
with
TypeHasFieldNamingStrategy
.
Uses
strategy.toSnake
. dropPrefix
Instances
data FieldCamelCase Source #
Empty datatype used as marker for DerivingVia
with
TypeHasFieldNamingStrategy
.
Uses stripFieldPrefix
strategy.
Instances
class TypeHasFieldNamingStrategy a where Source #
Field naming strategy used by a type. id
by default.
Some common options include: > typeFieldNamingStrategy = stripFieldPrefix > typeFieldNamingStrategy = toSnake . dropPrefix
This is used by the default implementation of typeDocHaskellRep
and
intended to be reused downstream.
You can also use DerivingVia
together with FieldCamelCase
and
FieldSnakeCase
to easily define instances of this class:
data MyType = ... deriving TypeHasFieldNamingStrategy via FieldCamelCase
Nothing
typeFieldNamingStrategy :: Text -> Text Source #
Instances
TypeHasFieldNamingStrategy (a :: k) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc typeFieldNamingStrategy :: Text -> Text Source # | |
TypeHasFieldNamingStrategy FieldCamelCase Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc typeFieldNamingStrategy :: Text -> Text Source # | |
TypeHasFieldNamingStrategy FieldSnakeCase Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc typeFieldNamingStrategy :: Text -> Text Source # |
newtype WithinParens Source #
Whether given text should be rendered grouped in parentheses (if they make sense).
buildADTRep :: forall a. (WithinParens -> a -> Markdown) -> ADTRep a -> Markdown Source #
Show given ADTRep
in a neat way.
applyWithinParens :: WithinParens -> Markdown -> Markdown Source #
buildTypeWithinParens :: forall a. Typeable a => WithinParens -> Markdown Source #
Show type, wrapping into parentheses if necessary.
typeDocBuiltMichelsonRep :: TypeHasDoc a => Proxy a -> Doc Source #
Fully render Michelson representation of a type.
Since this will be used in markdown, the type is forced to a single line.
>>>
data Foo = Foo () () () () () () () () () () () () deriving (Generic, IsoValue)
>>>
instance TypeHasDoc Foo where typeDocMdDescription = "Foo type"
>>>
typeDocBuiltMichelsonRep $ Proxy @Foo
**Final Michelson representation:** `pair (pair (pair unit unit unit) unit unit unit) (pair unit unit unit) unit unit unit`
dTypeDep :: forall (t :: Type). TypeHasDoc t => SomeDocDefinitionItem Source #
Create a DType
in form suitable for putting to typeDocDependencies
.
dTypeDepP :: forall (t :: Type). TypeHasDoc t => Proxy t -> SomeDocDefinitionItem Source #
Proxy version of dTypeDep
.
dStorage :: forall store. TypeHasDoc store => DStorageType Source #
Shortcut for DStorageType
.
customTypeDocMdReference :: (Text, DType) -> [DType] -> WithinParens -> Markdown Source #
Render a reference to a type which consists of type constructor (you have to provide name of this type constructor and documentation for the whole type) and zero or more type arguments.
customTypeDocMdReference' :: (Text, DType) -> [WithinParens -> Markdown] -> WithinParens -> Markdown Source #
More generic version of customTypeDocMdReference
, it accepts
arguments not as types with doc, but printers for them.
homomorphicTypeDocMdReference :: forall (t :: Type). (Typeable t, TypeHasDoc t, IsHomomorphic t) => Proxy t -> WithinParens -> Markdown Source #
Derive typeDocMdReference
, for homomorphic types only.
poly1TypeDocMdReference :: forall t (r :: Type) (a :: Type). (r ~ t a, Typeable t, Each '[TypeHasDoc] [r, a], IsHomomorphic t) => Proxy r -> WithinParens -> Markdown Source #
Derive typeDocMdReference
, for polymorphic type with one
type argument, like Maybe Integer
.
poly2TypeDocMdReference :: forall t (r :: Type) (a :: Type) (b :: Type). (r ~ t a b, Typeable t, Each '[TypeHasDoc] [r, a, b], IsHomomorphic t) => Proxy r -> WithinParens -> Markdown Source #
Derive typeDocMdReference
, for polymorphic type with two
type arguments, like Lambda Integer Natural
.
genericTypeDocDependencies :: forall a. (Generic a, GTypeHasDoc (Rep a)) => Proxy a -> [SomeDocDefinitionItem] Source #
Implement typeDocDependencies
via getting all immediate fields
of a datatype.
Note: this will not include phantom types, I'm not sure yet how this scenario should be handled (@martoon).
homomorphicTypeDocHaskellRep :: forall a. (Generic a, GTypeHasDoc (Rep a)) => TypeDocHaskellRep a Source #
Implement typeDocHaskellRep
for a homomorphic type.
Note that it does not require your type to be of IsHomomorphic
instance,
which can be useful for some polymorphic types which, for documentation
purposes, we want to consider homomorphic.
Example: Operation
is in fact polymorphic, but we don't want this fact to
be reflected in the documentation.
concreteTypeDocHaskellRep :: forall a b. (Typeable a, GenericIsoValue a, GTypeHasDoc (Rep a), HaveCommonTypeCtor b a) => TypeDocHaskellRep b Source #
Implement typeDocHaskellRep
on example of given concrete type.
This is a best effort attempt to implement typeDocHaskellRep
for polymorphic
types, as soon as there is no simple way to preserve type variables when
automatically deriving Haskell representation of a type.
unsafeConcreteTypeDocHaskellRep :: forall a b. (Typeable a, GenericIsoValue a, GTypeHasDoc (Rep a)) => TypeDocHaskellRep b Source #
Version of concreteTypeDocHaskellRep
which does not ensure
whether the type for which representation is built is any similar to
the original type which you implement a TypeHasDoc
instance for.
haskellRepNoFields :: TypeDocHaskellRep a -> TypeDocHaskellRep a Source #
Erase fields from Haskell datatype representation.
Use this when rendering fields names is undesired.
haskellRepMap :: (Text -> Text) -> TypeDocHaskellRep a -> TypeDocHaskellRep a Source #
Like haskellRepAdjust
, but can't add or remove field names.
haskellAddNewtypeField :: Text -> TypeDocHaskellRep a -> TypeDocHaskellRep a Source #
Add field name for newtype
.
Since newtype
field is automatically erased. Use this function
to add the desired field name.
haskellRepAdjust :: (Maybe Text -> Maybe Text) -> TypeDocHaskellRep a -> TypeDocHaskellRep a Source #
Adjust field names using a function. Can add or remove field names.
homomorphicTypeDocMichelsonRep :: forall a. KnownIsoT a => TypeDocMichelsonRep a Source #
Implement typeDocMichelsonRep
for homomorphic type.
concreteTypeDocMichelsonRep :: forall a b. (Typeable a, KnownIsoT a, HaveCommonTypeCtor b a) => TypeDocMichelsonRep b Source #
Implement typeDocMichelsonRep
on example of given concrete type.
This function exists for the same reason as concreteTypeDocHaskellRep
.
unsafeConcreteTypeDocMichelsonRep :: forall a b. (Typeable a, KnownIsoT a) => TypeDocMichelsonRep b Source #
Version of unsafeConcreteTypeDocHaskellRep
which does not ensure
whether the type for which representation is built is any similar to
the original type which you implement a TypeHasDoc
instance for.
cutInstrNonDoc :: (forall i o. Instr i o -> Instr i o) -> Instr inp out -> Instr s s Source #
Leave only instructions related to documentation.
Generated documentation for resulting instruction remains the same, but semantics of instruction itself gets lost. We have to pass optimizer here as an argument to avoid cyclic dependencies.