Safe Haskell | None |
---|---|
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
- type FieldDescriptions = [(Symbol, (Maybe Symbol, [(Symbol, Symbol)]))]
- data T
- toUType :: T -> Ty
- buildStack :: [T] -> Builder
- data SingT z 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)
- 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. Demote (KindOf a) -> Demote (KindOf b) -> m x) -> m (t b)
- requireEq :: forall (a :: T) (b :: T) m. (SingI a, SingI b, Monad m) => (forall x. Demote (KindOf a) -> Demote (KindOf b) -> m x) -> m (a :~: b)
- eqP :: forall (a :: T) (b :: T). (SingI a, SingI b) => Proxy a -> Proxy b -> Maybe (a :~: b)
- 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, ForbidOp t, ForbidBigMap t, ForbidTicket t)
- type ProperDupableBetterErrors t = (SingI t, ForbidTicket t)
- type ProperConstantBetterErrors t = (SingI t, ForbidOp t, ForbidBigMap t, ForbidContract t, ForbidTicket t)
- type ProperStorageBetterErrors t = (SingI t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t)
- type ProperParameterBetterErrors t = (SingI t, ForbidOp t, ForbidNestedBigMaps t)
- class WithDeMorganScope (c :: T -> Constraint) t a b where
- withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret
- class CheckScope (c :: Constraint) where
- checkScope :: Either BadTypeForScope (Dict c)
- type UntypedValScope t = (SingI t, HasNoOp t)
- class (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => ViewableScope t
- class (PackedValScope t, ConstantScope t) => UnpackedValScope t
- class (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => PackedValScope t
- class (SingI t, HasNoTicket t) => DupableScope t
- class (SingI t, HasNoOp t, HasNoBigMap t, HasNoContract t, HasNoTicket t) => ConstantScope t
- class (SingI t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) => StorageScope t
- class (SingI t, HasNoOp t, HasNoNestedBigMaps t) => ParameterScope t
- data BadTypeForScope
- data NestedBigMapsPresence (t :: T)
- = ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresent
- | ContainsNestedBigMaps t ~ 'False => NestedBigMapsAbsent
- data BigMapPresence (t :: T)
- = ContainsBigMap t ~ 'True => BigMapPresent
- | ContainsBigMap t ~ 'False => BigMapAbsent
- data TicketPresence (t :: T)
- = ContainsTicket t ~ 'True => TicketPresent
- | ContainsTicket t ~ 'False => TicketAbsent
- data ContractPresence (t :: T)
- = ContainsContract t ~ 'True => ContractPresent
- | ContainsContract t ~ 'False => ContractAbsent
- data OpPresence (t :: T)
- = ContainsOp t ~ 'True => OpPresent
- | ContainsOp t ~ 'False => OpAbsent
- type ForbidNonComparable t = FailOnNonComparableFound (IsComparable t)
- type ForbidNestedBigMaps t = FailOnNestedBigMapsFound (ContainsNestedBigMaps t)
- type ForbidBigMap t = FailOnBigMapFound (ContainsBigMap t)
- type ForbidTicket t = FailOnTicketFound (ContainsTicket t)
- type ForbidContract t = FailOnContractFound (ContainsContract t)
- type ForbidOp t = FailOnOperationFound (ContainsOp t)
- type family FailOnNonComparableFound (comparable :: Bool) :: Constraint where ...
- type family FailOnNestedBigMapsFound (enabled :: Bool) :: Constraint where ...
- type family FailOnBigMapFound (enabled :: Bool) :: Constraint where ...
- type family FailOnTicketFound (enabled :: Bool) :: Constraint where ...
- type family FailOnContractFound (enabled :: Bool) :: Constraint where ...
- type family FailOnOperationFound (enabled :: Bool) :: Constraint where ...
- 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 family IsComparable (t :: T) :: Bool where ...
- type family ContainsNestedBigMaps (t :: T) :: Bool where ...
- type family ContainsBigMap (t :: T) :: Bool where ...
- type family ContainsTicket (t :: T) :: Bool where ...
- type family ContainsContract (t :: T) :: Bool where ...
- type family ContainsOp (t :: T) :: Bool where ...
- forbiddenOp :: forall t a. (SingI t, ForbidOp t) => (HasNoOp t => a) -> a
- forbiddenBigMap :: forall t a. (SingI t, ForbidBigMap t) => (HasNoBigMap t => a) -> a
- forbiddenNestedBigMaps :: forall t a. (SingI t, ForbidNestedBigMaps t) => (HasNoNestedBigMaps t => a) -> a
- forbiddenContractType :: forall t a. (SingI t, ForbidContract t) => (HasNoContract t => a) -> a
- checkOpPresence :: Sing (ty :: T) -> OpPresence ty
- checkContractTypePresence :: Sing (ty :: T) -> ContractPresence ty
- checkTicketPresence :: Sing (ty :: T) -> TicketPresence ty
- checkBigMapPresence :: Sing (ty :: T) -> BigMapPresence ty
- checkNestedBigMapsPresence :: Sing (ty :: T) -> NestedBigMapsPresence ty
- opAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoOp t)
- contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoContract t)
- bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoBigMap t)
- nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoNestedBigMaps t)
- properParameterEvi :: forall t. ProperParameterBetterErrors t :- ParameterScope t
- properStorageEvi :: forall t. ProperStorageBetterErrors t :- StorageScope t
- properConstantEvi :: forall t. ProperConstantBetterErrors t :- ConstantScope t
- properDupableEvi :: forall t. ProperDupableBetterErrors t :- DupableScope t
- properPackedValEvi :: forall t. ProperPackedValBetterErrors t :- PackedValScope t
- properUnpackedValEvi :: forall t. ProperUnpackedValBetterErrors t :- UnpackedValScope t
- properViewableEvi :: forall t. ProperViewableBetterErrors t :- ViewableScope t
- properUntypedValEvi :: forall t. ProperUntypedValBetterErrors t :- UntypedValScope t
- ligoLayout :: GenericStrategy
- ligoCombLayout :: GenericStrategy
- newtype EpName = UnsafeEpName {}
- 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 {
- mkViewName :: Text -> Either BadViewNameError ViewName
- unsafeMkViewName :: HasCallStack => Text -> ViewName
- viewNameToMText :: ViewName -> MText
- newtype OpSize = OpSize {}
- opSizeHardLimit :: OpSize
- smallTransferOpSize :: OpSize
- 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
- data AnnConvergeError where
- AnnConvergeError :: forall (tag :: Type). (Buildable (Annotation tag), Show (Annotation tag), Typeable tag) => Annotation tag -> Annotation tag -> AnnConvergeError
- notesSing :: SingI t => Notes t -> Sing t
- notesT :: SingI t => Notes t -> T
- starNotes :: forall t. SingI t => Notes t
- isStar :: SingI t => Notes t -> Bool
- converge :: Notes t -> Notes t -> Either AnnConvergeError (Notes t)
- insertTypeAnn :: forall (b :: T). TypeAnn -> Notes b -> Notes b
- convergeAnns :: forall (tag :: Type). (Buildable (Annotation tag), Show (Annotation tag), Typeable tag) => Annotation tag -> Annotation tag -> Either AnnConvergeError (Annotation tag)
- convergeDestrAnns :: FieldAnn -> FieldAnn -> Either AnnConvergeError FieldAnn
- data SomeViewsSet' instr where
- SomeViewsSet :: SingI st => ViewsSet' instr st -> SomeViewsSet' instr
- data ViewsSetError = DuplicatedViewName ViewName
- 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 :: ViewsSet' instr st
- addViewToSet :: View' instr arg st ret -> ViewsSet' instr st -> Either ViewsSetError (ViewsSet' instr st)
- lookupView :: ViewName -> ViewsSet' instr st -> Maybe (SomeView' instr st)
- viewsSetNames :: ViewsSet' instr st -> [ViewName]
- pattern AsUTypeExt :: () => SingI t => Sing t -> Notes t -> Ty
- pattern AsUType :: () => SingI t => Notes t -> Ty
- fromUType :: Ty -> T
- mkUType :: SingI x => Notes x -> Ty
- mkUType' :: (Sing x, Notes x) -> Ty
- withUType :: Ty -> (forall t. SingI t => Notes t -> r) -> r
- 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 = EpAddress {}
- pattern ParamNotes :: Notes t -> RootAnn -> ParamNotes t
- formatEpAddress :: EpAddress -> Text
- mformatEpAddress :: EpAddress -> MText
- parseEpAddress :: Text -> Either ParseEpAddressError EpAddress
- unsafeParseEpAddress :: HasCallStack => Text -> EpAddress
- parseEpAddressRaw :: ByteString -> Either ParseEpAddressError EpAddress
- unsafeParseEpAddressRaw :: ByteString -> 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)
- 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
- type ContractCode' instr cp st = 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
- defaultContract :: (ParameterScope cp, StorageScope st) => ContractCode' instr cp st -> Contract' instr cp st
- mapContractCodeBlock :: (ContractCode' instr cp st -> ContractCode' instr cp st) -> Contract' instr cp st -> 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
- mapContractCode :: (forall i o. instr i o -> instr i o) -> Contract' instr cp st -> Contract' instr cp st
- mapEntriesOrdered :: Contract' instr cp st -> (ParamNotes cp -> a) -> (Notes st -> a) -> (ContractCode' instr cp st -> a) -> [a]
- 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. (SingI t, Comparable t) => Set (Value' instr t) -> Value' instr ('TSet t)
- VOp :: Operation' instr -> Value' instr 'TOperation
- VContract :: forall arg instr. (SingI arg, HasNoOp 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, 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 ': '[]) -> Value' instr ('TLambda inp out)
- VMap :: forall k v instr. (SingI k, SingI v, Comparable k) => Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
- VBigMap :: forall k v instr. (SingI k, SingI v, Comparable k, HasNoBigMap 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 Comparability t where
- CanBeCompared :: Comparable t => Comparability t
- CannotBeCompared :: IsComparable t ~ 'False => Comparability t
- type ComparabilityScope t = (SingI t, Comparable t)
- class IsComparable t ~ 'True => Comparable t
- 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 CreateContract instr cp st = (forall i o. Show (instr i o), forall i o. Eq (instr i o)) => CreateContract {
- ccOriginator :: Address
- 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
- 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
- getComparableProofS :: Sing (a :: T) -> Maybe (Dict (Comparable a))
- checkComparability :: Sing t -> Comparability t
- comparabilityPresence :: Sing t -> Maybe (Dict $ Comparable t)
- addressToVContract :: forall t instr. (ParameterScope t, ForbidOr t) => Address -> Value' instr ('TContract t)
- buildVContract :: Value' instr ('TContract arg) -> Builder
- 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)
- 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 family Bls12381MulBadOrder a1 a2 where ...
- 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 Sub
- data Add
- 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
- type ArithRes aop n m :: T
- convergeArith :: proxy aop -> Notes n -> Notes m -> Either AnnConvergeError (Notes (ArithRes aop n m))
- evalOp :: proxy aop -> Value' instr n -> Value' instr m -> Either (ArithError (Value' instr n) (Value' instr m)) (Value' instr (ArithRes aop n m))
- commutativityProof :: Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
- compareOp :: Comparable t => Value' i t -> Value' i t -> Integer
- 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 :: InstrCallStack -> Instr a b -> Instr a b
- Meta :: SomeMeta -> Instr a b -> Instr a b
- InstrWithNotes :: forall a (topElems :: [T]) (s :: [T]). (RMap topElems, RecordToList topElems, ReifyConstraint Show Notes topElems, ReifyConstraint NFData Notes topElems, Each '[SingI] topElems) => Proxy s -> Rec Notes topElems -> Instr a (topElems ++ s) -> Instr a (topElems ++ s)
- InstrWithVarNotes :: NonEmpty VarAnn -> Instr a b -> Instr a b
- InstrWithVarAnns :: VarAnns -> Instr a b -> Instr a b
- FrameInstr :: forall a b s. (KnownList a, KnownList b) => Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
- 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
- Fn :: Text -> StackFn -> Instr inp out -> Instr inp out
- AnnCAR :: VarAnn -> FieldAnn -> Instr ('TPair a b ': s) (a ': s)
- AnnCDR :: 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)
- DUP :: DupableScope a => Instr (a ': s) (a ': (a ': s))
- DUPN :: forall (n :: Peano) inp out a. (ConstraintDUPN n inp out a, DupableScope a) => 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
- PUSH :: forall t s. ConstantScope t => Value' Instr t -> Instr s (t ': s)
- SOME :: Instr (a ': s) ('TOption a ': s)
- NONE :: forall a s. SingI a => Instr s ('TOption a ': s)
- UNIT :: Instr s ('TUnit ': s)
- IF_NONE :: Instr s s' -> Instr (a ': s) s' -> Instr ('TOption a ': s) s'
- AnnPAIR :: TypeAnn -> FieldAnn -> FieldAnn -> Instr (a ': (b ': s)) ('TPair a b ': s)
- AnnUNPAIR :: VarAnn -> VarAnn -> FieldAnn -> FieldAnn -> Instr ('TPair a b ': s) (a ': (b ': s))
- PAIRN :: forall n inp. ConstraintPairN n inp => 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 => TypeAnn -> FieldAnn -> FieldAnn -> Instr (a ': s) ('TOr a b ': s)
- AnnRIGHT :: SingI a => TypeAnn -> FieldAnn -> FieldAnn -> Instr (b ': s) ('TOr a b ': s)
- IF_LEFT :: Instr (a ': s) s' -> Instr (b ': s) s' -> Instr ('TOr a b ': s) s'
- NIL :: SingI p => Instr s ('TList p ': s)
- CONS :: Instr (a ': ('TList a ': s)) ('TList a ': s)
- IF_CONS :: Instr (a ': ('TList a ': s)) s' -> Instr s s' -> Instr ('TList a ': s) s'
- SIZE :: SizeOp c => Instr (c ': s) ('TNat ': s)
- EMPTY_SET :: (SingI e, Comparable e) => Instr s ('TSet e ': s)
- EMPTY_MAP :: (SingI a, SingI b, Comparable a) => Instr s ('TMap a b ': s)
- EMPTY_BIG_MAP :: (SingI a, SingI b, Comparable a, HasNoBigMap b) => Instr s ('TBigMap a b ': s)
- MAP :: (MapOp c, SingI b) => 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
- MEM :: MemOp c => Instr (MemOpKey c ': (c ': s)) ('TBool ': s)
- GET :: (GetOp c, SingI (GetOpVal c)) => Instr (GetOpKey c ': (c ': s)) ('TOption (GetOpVal c) ': s)
- GETN :: forall (ix :: Peano) (pair :: T) (s :: [T]). ConstraintGetN ix pair => PeanoNatural ix -> Instr (pair ': s) (GetN ix pair ': s)
- UPDATE :: UpdOp c => Instr (UpdOpKey c ': (UpdOpParams c ': (c ': s))) (c ': s)
- UPDATEN :: forall (ix :: Peano) (val :: T) (pair :: T) (s :: [T]). ConstraintUpdateN ix pair => PeanoNatural ix -> Instr (val ': (pair ': s)) (UpdateN ix val pair ': s)
- GET_AND_UPDATE :: (GetOp c, UpdOp c, SingI (GetOpVal c), UpdOpKey c ~ GetOpKey c) => 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)
- LAMBDA :: forall i o s. (SingI i, SingI o) => Value' Instr ('TLambda i o) -> Instr s ('TLambda i o ': s)
- EXEC :: Instr (t1 ': ('TLambda t1 t2 ': s)) (t2 ': s)
- APPLY :: forall a b c s. (ConstantScope a, SingI b) => 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
- CAST :: forall a s. SingI a => Instr (a ': s) (a ': s)
- RENAME :: Instr (a ': s) (a ': s)
- PACK :: PackedValScope a => Instr (a ': s) ('TBytes ': s)
- UNPACK :: (UnpackedValScope a, SingI a) => Instr ('TBytes ': s) ('TOption a ': s)
- CONCAT :: ConcatOp c => Instr (c ': (c ': s)) (c ': s)
- CONCAT' :: ConcatOp c => Instr ('TList c ': s) (c ': s)
- SLICE :: (SliceOp c, SingI c) => Instr ('TNat ': ('TNat ': (c ': s))) ('TOption c ': s)
- ISNAT :: Instr ('TInt ': s) ('TOption 'TNat ': s)
- ADD :: ArithOp Add n m => Instr (n ': (m ': s)) (ArithRes Add n m ': s)
- SUB :: ArithOp Sub n m => Instr (n ': (m ': s)) (ArithRes Sub n m ': s)
- MUL :: ArithOp Mul n m => Instr (n ': (m ': s)) (ArithRes Mul n m ': s)
- EDIV :: ArithOp EDiv n m => Instr (n ': (m ': s)) (ArithRes EDiv n m ': s)
- ABS :: UnaryArithOp Abs n => Instr (n ': s) (UnaryArithRes Abs n ': s)
- NEG :: UnaryArithOp Neg n => Instr (n ': s) (UnaryArithRes Neg n ': s)
- LSL :: ArithOp Lsl n m => Instr (n ': (m ': s)) (ArithRes Lsl n m ': s)
- LSR :: ArithOp Lsr n m => Instr (n ': (m ': s)) (ArithRes Lsr n m ': s)
- OR :: ArithOp Or n m => Instr (n ': (m ': s)) (ArithRes Or n m ': s)
- AND :: ArithOp And n m => Instr (n ': (m ': s)) (ArithRes And n m ': s)
- XOR :: ArithOp Xor n m => Instr (n ': (m ': s)) (ArithRes Xor n m ': s)
- NOT :: UnaryArithOp Not n => Instr (n ': s) (UnaryArithRes Not n ': s)
- COMPARE :: (Comparable n, SingI n) => Instr (n ': (n ': s)) ('TInt ': s)
- EQ :: UnaryArithOp Eq' n => Instr (n ': s) (UnaryArithRes Eq' n ': s)
- NEQ :: UnaryArithOp Neq n => Instr (n ': s) (UnaryArithRes Neq n ': s)
- LT :: UnaryArithOp Lt n => Instr (n ': s) (UnaryArithRes Lt n ': s)
- GT :: UnaryArithOp Gt n => Instr (n ': s) (UnaryArithRes Gt n ': s)
- LE :: UnaryArithOp Le n => Instr (n ': s) (UnaryArithRes Le n ': s)
- GE :: UnaryArithOp Ge n => Instr (n ': s) (UnaryArithRes Ge n ': s)
- INT :: ToIntArithOp n => Instr (n ': s) ('TInt ': s)
- VIEW :: (SingI arg, ViewableScope ret) => ViewName -> Notes ret -> Instr (arg ': ('TAddress ': s)) ('TOption ret ': s)
- SELF :: forall (arg :: T) s. ParameterScope arg => SomeEntrypointCallT arg -> Instr s ('TContract arg ': s)
- CONTRACT :: ParameterScope p => Notes p -> EpName -> Instr ('TAddress ': s) ('TOption ('TContract p) ': s)
- TRANSFER_TOKENS :: ParameterScope p => Instr (p ': ('TMutez ': ('TContract p ': s))) ('TOperation ': s)
- SET_DELEGATE :: Instr ('TOption 'TKeyHash ': s) ('TOperation ': s)
- CREATE_CONTRACT :: (ParameterScope p, StorageScope g) => Contract' Instr p g -> Instr ('TOption 'TKeyHash ': ('TMutez ': (g ': s))) ('TOperation ': ('TAddress ': s))
- IMPLICIT_ACCOUNT :: Instr ('TKeyHash ': s) ('TContract 'TUnit ': s)
- NOW :: Instr s ('TTimestamp ': s)
- AMOUNT :: Instr s ('TMutez ': s)
- BALANCE :: Instr s ('TMutez ': s)
- VOTING_POWER :: Instr ('TKeyHash ': s) ('TNat ': s)
- TOTAL_VOTING_POWER :: Instr s ('TNat ': s)
- CHECK_SIGNATURE :: Instr ('TKey ': ('TSignature ': ('TBytes ': s))) ('TBool ': s)
- SHA256 :: Instr ('TBytes ': s) ('TBytes ': s)
- SHA512 :: Instr ('TBytes ': s) ('TBytes ': s)
- BLAKE2B :: Instr ('TBytes ': s) ('TBytes ': s)
- SHA3 :: Instr ('TBytes ': s) ('TBytes ': s)
- KECCAK :: Instr ('TBytes ': s) ('TBytes ': s)
- HASH_KEY :: Instr ('TKey ': s) ('TKeyHash ': s)
- PAIRING_CHECK :: Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) ': s) ('TBool ': s)
- SOURCE :: Instr s ('TAddress ': s)
- SENDER :: Instr s ('TAddress ': s)
- ADDRESS :: Instr ('TContract a ': s) ('TAddress ': s)
- CHAIN_ID :: Instr s ('TChainId ': s)
- LEVEL :: Instr s ('TNat ': s)
- SELF_ADDRESS :: Instr s ('TAddress ': s)
- NEVER :: Instr ('TNever ': s) t
- TICKET :: Comparable a => Instr (a ': ('TNat ': s)) ('TTicket a ': s)
- READ_TICKET :: Instr ('TTicket a ': s) (RightComb ['TAddress, a, 'TNat] ': ('TTicket a ': s))
- SPLIT_TICKET :: Instr ('TTicket a ': ('TPair 'TNat 'TNat ': s)) ('TOption ('TPair ('TTicket a) ('TTicket a)) ': s)
- JOIN_TICKETS :: Instr ('TPair ('TTicket a) ('TTicket a) ': s) ('TOption ('TTicket a) ': s)
- OPEN_CHEST :: Instr ('TChestKey ': ('TChest ': ('TNat ': s))) ('TOr 'TBytes 'TBool ': s)
- type family UpdateN (ix :: Peano) (val :: T) (pair :: T) :: T where ...
- type ConstraintUpdateN (ix :: Peano) (pair :: T) = TypeErrorUnless (CombedPairNodeIndexIsValid ix pair) (If (IsPair pair) ((((('Text "'UPDATE " :<>: 'ShowType (FromPeano ix)) :<>: 'Text "' expects the 2nd element of the stack to be a right-combed pair with at least ") :<>: 'ShowType (FromPeano ix + 1)) :<>: 'Text " nodes,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairNodeCount pair))) :<>: 'Text " nodes.")) ('Text "Expected the 2nd element of the stack to be a pair, but found: " :<>: 'ShowType pair))
- type family GetN (ix :: Peano) (pair :: T) :: T where ...
- type ConstraintGetN (ix :: Peano) (pair :: T) = TypeErrorUnless (CombedPairNodeIndexIsValid ix pair) (If (IsPair pair) ((((('Text "'GET " :<>: 'ShowType (FromPeano ix)) :<>: 'Text "' expects a right-combed pair with at least ") :<>: 'ShowType (FromPeano ix + 1)) :<>: 'Text " nodes at the top of the stack,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairNodeCount pair))) :<>: 'Text " nodes.")) ('Text "Expected a pair at the top of the stack, but found: " :<>: 'ShowType pair))
- type family UnpairN (n :: Peano) (s :: T) :: [T] where ...
- type ConstraintUnpairN (n :: Peano) (pair :: T) = (TypeErrorUnless (n >= ToPeano 2) ('Text "'UNPAIR n' expects n \8805 2"), TypeErrorUnless (CombedPairLeafCountIsAtLeast n pair) (If (IsPair pair) ((((('Text "'UNPAIR " :<>: 'ShowType (FromPeano n)) :<>: 'Text "' expects a right-combed pair with at least ") :<>: 'ShowType (FromPeano n)) :<>: 'Text " elements at the top of the stack,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairLeafCount pair))) :<>: 'Text " elements.")) ('Text "Expected a pair at the top of the stack, but found: " :<>: 'ShowType pair)))
- type family RightComb (s :: [T]) :: T where ...
- type PairN (n :: Peano) (s :: [T]) = RightComb (Take n s) ': Drop n s
- type ConstraintPairN (n :: Peano) (inp :: [T]) = (RequireLongerOrSameLength inp n, TypeErrorUnless (n >= ToPeano 2) ('Text "'PAIR n' expects n \8805 2"))
- type ConstraintDUG n inp out a = ConstraintDUG' T n inp out a
- type ConstraintDUG' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (RequireLongerThan out n, inp ~ (a ': Drop ('S 'Z) inp), out ~ (Take n (Drop ('S 'Z) inp) ++ (a ': Drop ('S n) inp)))
- type ConstraintDIG n inp out a = ConstraintDIG' T n inp out a
- type ConstraintDIG' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (RequireLongerThan inp n, inp ~ (Take n inp ++ (a ': Drop ('S n) inp)), out ~ (a ': (Take n inp ++ Drop ('S n) inp)))
- type ConstraintDIPN n inp out s s' = ConstraintDIPN' T n inp out s s'
- type ConstraintDIPN' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (s :: [kind]) (s' :: [kind]) = (RequireLongerOrSameLength inp n, (Take n inp ++ s) ~ inp, (Take n inp ++ s') ~ out)
- type ConstraintDUPN n inp out a = ConstraintDUPN' T n inp out a
- type ConstraintDUPN' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (RequireLongerOrSameLength inp n, (n > 'Z) ~ 'True, inp ~ (Take (Decrement n) inp ++ (a ': Drop n inp)), out ~ (a ': inp))
- pattern RIGHT :: () => (SingI a, i ~ (b ': s), o ~ ('TOr a b ': s)) => Instr i o
- pattern LEFT :: () => (SingI b, i ~ (a ': s), o ~ ('TOr a b ': s)) => Instr i o
- pattern PAIR :: () => (i ~ (a ': (b ': s)), o ~ ('TPair a b ': s)) => Instr i o
- pattern UNPAIR :: () => (i ~ ('TPair a b ': s), o ~ (a ': (b ': s))) => Instr i o
- pattern CDR :: () => (i ~ ('TPair a b ': s), o ~ (b ': s)) => Instr i o
- pattern CAR :: () => (i ~ ('TPair a b ': s), o ~ (a ': s)) => 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, SingI (ToPeano gn), RequireLongerThan st n) => StackRef st
- 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 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 x = CtorEffectsApp {}
- data DfsSettings x = DfsSettings {}
- ceaBottomToTop :: CtorEffectsApp x
- dfsInstr :: forall x inp out. Semigroup x => DfsSettings x -> (forall i o. Instr i o -> (Instr i o, x)) -> Instr inp out -> (Instr inp out, x)
- dfsFoldInstr :: forall x inp out. Semigroup x => DfsSettings x -> (forall i o. Instr i o -> x) -> Instr inp out -> x
- dfsModifyInstr :: DfsSettings () -> (forall i o. Instr i o -> Instr i o) -> Instr inp out -> Instr inp out
- linearizeLeft :: Instr inp out -> Instr inp out
- linearizeLeftDeep :: Instr inp out -> Instr inp out
- dfsMapValue :: forall t. (forall t'. Value t' -> Value t') -> Value t -> Value t
- dfsTraverseValue :: forall t m. Monad m => (forall t'. Value t' -> m (Value t')) -> 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
- class (SingI t, WellTypedSuperC t) => WellTyped (t :: T)
- class IsoValuesStack (ts :: [Type]) where
- type family ToTs' (t :: [k]) :: [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 = HasNoOp (ToT a)
- type WellTypedIsoValue a = (WellTyped (ToT a), IsoValue a)
- type WellTypedToT a = WellTyped (ToT a)
- type SomeEntrypointCall arg = SomeEntrypointCallT (ToT arg)
- type EntrypointCall param arg = EntrypointCallT (ToT param) (ToT arg)
- type family ToT' (t :: k) :: T where ...
- class WellTypedToT a => IsoValue a where
- type KnownIsoT 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 :: [CaseClauseParam]
- type family GCaseClauses x :: [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 :: CtorField) (l :: [k]) :: [k] 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 = (GenericIsoValue dt, GInstrDeconstruct (Rep dt))
- 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)
- instrSetField :: forall dt name st. InstrSetFieldC dt name => Label name -> Instr (ToT (GetFieldType dt name) ': (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), KnownList stack) => Instr (stack ++ st) (ToT dt ': st)
- instrDeconstruct :: forall dt stack st. (InstrDeconstructC dt, stack ~ ToTs (ConstructorFieldTypes dt), KnownList stack) => Instr (ToT dt ': st) (stack ++ st)
- convertParamNotes :: SingI cp => ParamNotes cp -> ParameterType
- convertContractCode :: 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
- untypeValue :: HasNoOp t => Value' Instr t -> Value
- untypeValueHashable :: HasNoOp t => Value' Instr t -> Value
- untypeValueOptimized :: HasNoOp t => Value' Instr t -> Value
- untypeDemoteT :: forall (t :: T). SingI t => Ty
- instrToOpsOptimized :: HasCallStack => Instr inp out -> [ExpandedOp]
- instrToOps :: HasCallStack => Instr inp out -> [ExpandedOp]
- sampleTypedValue :: Sing t -> Maybe (Value t)
- flattenEntrypoints :: SingI t => ParamNotes t -> Map EpName Ty
- instrOpSize :: Instr inp out -> OpSize
- contractOpSize :: Contract cp st -> OpSize
- valueOpSize :: UntypedValScope t => Value t -> OpSize
- data SomeStorage where
- SomeStorage :: forall st. StorageScope st => Value st -> SomeStorage
- 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
- data SomeConstant where
- SomeConstant :: (ConstantScope t, SingI t) => Value t -> SomeConstant
- data SomeValue where
- data SomeConstrainedValue (c :: T -> Constraint) where
- SomeConstrainedValue :: forall (t :: T) (c :: T -> Constraint). c t => Value t -> SomeConstrainedValue c
- 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
- 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 -> Builder
- 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
- haskellAddNewtypeField :: Text -> TypeDocHaskellRep a -> TypeDocHaskellRep a
- haskellRepStripFieldPrefix :: HasCallStack => 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
- buildInstrDocWithGitRev :: DGitRevision -> Instr inp out -> ContractDoc
- buildInstrDoc :: Instr inp out -> ContractDoc
- modifyInstrAllDoc :: (SomeDocItem -> SomeDocItem) -> Instr inp out -> Instr inp out
- modifyInstrDoc :: (DocItem i1, DocItem i2) => (i1 -> Maybe i2) -> Instr inp out -> Instr inp out
- 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
HasDict a (Dict a) | |
Defined in Data.Constraint | |
a :=> (Read (Dict a)) | |
a :=> (Monoid (Dict a)) | |
a :=> (Enum (Dict a)) | |
a :=> (Bounded (Dict a)) | |
() :=> (Eq (Dict a)) | |
() :=> (Ord (Dict a)) | |
() :=> (Show (Dict a)) | |
() :=> (Semigroup (Dict a)) | |
a => Bounded (Dict a) | |
a => Enum (Dict a) | |
Defined in Data.Constraint | |
Eq (Dict a) | |
(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) # | |
Ord (Dict a) | |
a => Read (Dict a) | |
Show (Dict a) | |
Semigroup (Dict a) | |
a => Monoid (Dict a) | |
NFData (Dict c) | |
Defined in Data.Constraint |
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 |
() :=> (Eq (a :- b)) | |
() :=> (Ord (a :- b)) | |
() :=> (Show (a :- b)) | |
a => HasDict b (a :- b) | |
Defined in Data.Constraint | |
Eq (a :- b) | Assumes |
(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) # | |
Ord (a :- b) | Assumes |
Defined in Data.Constraint | |
Show (a :- b) | |
a => NFData (a :- b) | |
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]).
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") ]) ) ]
Michelson language type with annotations stripped off.
Instances
buildStack :: [T] -> Builder Source #
Format type stack in a pretty way.
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) | |
STNever :: SingT ('TNever :: T) |
Instances
SDecide T => TestCoercion SingT Source # | |
Defined in Morley.Michelson.Typed.Sing | |
SDecide T => TestEquality SingT Source # | |
Defined in Morley.Michelson.Typed.Sing |
castM :: forall (a :: T) (b :: T) t m. (SingI a, SingI b, Monad m) => t a -> (forall x. Demote (KindOf a) -> Demote (KindOf b) -> 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. Demote (KindOf a) -> Demote (KindOf b) -> 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 #
type ProperNonComparableValBetterErrors t = (SingI t, ForbidNonComparable t) Source #
type ProperUntypedValBetterErrors t = (SingI t, ForbidOp t) Source #
type ProperViewableBetterErrors t = (SingI t, ForbidOp t, ForbidBigMap t, ForbidTicket t) Source #
type ProperUnpackedValBetterErrors t = (ProperPackedValBetterErrors t, ProperConstantBetterErrors t) Source #
type ProperPackedValBetterErrors t = (SingI t, ForbidOp t, ForbidBigMap t, ForbidTicket t) Source #
type ProperDupableBetterErrors t = (SingI t, ForbidTicket t) Source #
type ProperConstantBetterErrors t = (SingI t, ForbidOp t, ForbidBigMap t, ForbidContract t, ForbidTicket t) Source #
type ProperStorageBetterErrors t = (SingI t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t) Source #
type ProperParameterBetterErrors t = (SingI t, ForbidOp t, ForbidNestedBigMaps 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
.
GHC is however not able to prove this, so we need to use another (impossible)
error
to forcefully "prove" one of the two scopes.
Funnily enough however GHC is able to prove that if one holds then the other
does too, so we don't actually have to prove both, see mkWithDeMorgan
.
withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret Source #
Instances
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 UntypedValScope t = (SingI t, HasNoOp t) Source #
Alias for constraints which are required for untyped representation.
class (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket 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.
Not just a type alias in order to be able to partially apply it
Instances
(SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => ViewableScope t Source # | |
Defined in Morley.Michelson.Typed.Scope | |
SingI t => CheckScope (ViewableScope t) Source # | |
Defined in Morley.Michelson.Typed.Scope checkScope :: Either BadTypeForScope (Dict (ViewableScope t)) Source # |
class (PackedValScope t, ConstantScope t) => UnpackedValScope t Source #
Set of constraints that Michelson applies to unpacked values.
It is different from PackedValScope
, e.g. contract
type cannot appear
in a value we unpack to.
Not just a type alias in order to be able to partially apply it
Instances
(PackedValScope t, ConstantScope t) => UnpackedValScope t Source # | |
Defined in Morley.Michelson.Typed.Scope | |
(WithDeMorganScope PackedValScope t a b, WithDeMorganScope ConstantScope t a b, SingI a, SingI b) => WithDeMorganScope UnpackedValScope t a b Source # | |
Defined in Morley.Michelson.Typed.Scope withDeMorganScope :: UnpackedValScope (t a b) => ((UnpackedValScope a, UnpackedValScope b) => ret) -> ret Source # | |
SingI t => CheckScope (UnpackedValScope t) Source # | |
Defined in Morley.Michelson.Typed.Scope checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t)) Source # |
class (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket 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
Instances
(SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => PackedValScope t Source # | |
Defined in Morley.Michelson.Typed.Scope | |
(WithDeMorganScope HasNoOp t a b, WithDeMorganScope HasNoBigMap t a b, WithDeMorganScope HasNoTicket t a b, SingI a, SingI b) => WithDeMorganScope PackedValScope t a b Source # | |
Defined in Morley.Michelson.Typed.Scope withDeMorganScope :: PackedValScope (t a b) => ((PackedValScope a, PackedValScope b) => ret) -> ret Source # | |
SingI t => CheckScope (PackedValScope t) Source # | |
Defined in Morley.Michelson.Typed.Scope checkScope :: Either BadTypeForScope (Dict (PackedValScope t)) Source # |
class (SingI t, HasNoTicket t) => DupableScope t Source #
Alias for constraints which Michelson requires in DUP
instruction.
Instances
(SingI t, HasNoTicket t) => DupableScope t Source # | |
Defined in Morley.Michelson.Typed.Scope | |
SingI t => CheckScope (DupableScope t) Source # | |
Defined in Morley.Michelson.Typed.Scope checkScope :: Either BadTypeForScope (Dict (DupableScope t)) Source # |
class (SingI t, HasNoOp t, HasNoBigMap t, HasNoContract t, HasNoTicket 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
Instances
(SingI t, HasNoOp t, HasNoBigMap t, HasNoContract t, HasNoTicket t) => ConstantScope t Source # | |
Defined in Morley.Michelson.Typed.Scope | |
(WithDeMorganScope HasNoOp t a b, WithDeMorganScope HasNoBigMap t a b, WithDeMorganScope HasNoContract t a b, WithDeMorganScope HasNoTicket t a b, SingI a, SingI b) => WithDeMorganScope ConstantScope t a b Source # | |
Defined in Morley.Michelson.Typed.Scope withDeMorganScope :: ConstantScope (t a b) => ((ConstantScope a, ConstantScope b) => ret) -> ret Source # | |
SingI t => CheckScope (ConstantScope t) Source # | |
Defined in Morley.Michelson.Typed.Scope checkScope :: Either BadTypeForScope (Dict (ConstantScope t)) Source # |
class (SingI t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract 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
Instances
(SingI t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) => StorageScope t Source # | |
Defined in Morley.Michelson.Typed.Scope | |
(WithDeMorganScope HasNoOp t a b, WithDeMorganScope HasNoNestedBigMaps t a b, WithDeMorganScope HasNoContract t a b, SingI a, SingI b) => WithDeMorganScope StorageScope t a b Source # | |
Defined in Morley.Michelson.Typed.Scope withDeMorganScope :: StorageScope (t a b) => ((StorageScope a, StorageScope b) => ret) -> ret Source # | |
SingI t => CheckScope (StorageScope t) Source # | |
Defined in Morley.Michelson.Typed.Scope checkScope :: Either BadTypeForScope (Dict (StorageScope t)) Source # |
class (SingI t, HasNoOp t, HasNoNestedBigMaps 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
Instances
(SingI t, HasNoOp t, HasNoNestedBigMaps t) => ParameterScope t Source # | |
Defined in Morley.Michelson.Typed.Scope | |
(WithDeMorganScope HasNoOp t a b, WithDeMorganScope HasNoNestedBigMaps t a b, SingI a, SingI b) => WithDeMorganScope ParameterScope t a b Source # | |
Defined in Morley.Michelson.Typed.Scope withDeMorganScope :: ParameterScope (t a b) => ((ParameterScope a, ParameterScope b) => ret) -> ret Source # | |
SingI t => CheckScope (ParameterScope t) Source # | |
Defined in Morley.Michelson.Typed.Scope checkScope :: Either BadTypeForScope (Dict (ParameterScope t)) Source # |
data BadTypeForScope Source #
Instances
data NestedBigMapsPresence (t :: T) Source #
Whether a value of this type _may_ contain nested big_map
s.
ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresent | A value of type |
ContainsNestedBigMaps t ~ 'False => NestedBigMapsAbsent | A value of type |
data BigMapPresence (t :: T) Source #
Whether a value of this type _may_ contain a big_map
value.
ContainsBigMap t ~ 'True => BigMapPresent | A value of type |
ContainsBigMap t ~ 'False => BigMapAbsent | A value of type |
data TicketPresence (t :: T) Source #
Whether a value of this type _may_ contain a ticket
value.
ContainsTicket t ~ 'True => TicketPresent | A value of type |
ContainsTicket t ~ 'False => TicketAbsent | A value of type |
data ContractPresence (t :: T) Source #
Whether a value of this type _may_ contain a contract
value.
ContainsContract t ~ 'True => ContractPresent | A value of type |
ContainsContract t ~ 'False => ContractAbsent | A value of type |
data OpPresence (t :: T) Source #
Whether a value of this type _may_ contain an operation.
ContainsOp t ~ 'True => OpPresent | A value of type |
ContainsOp t ~ 'False => OpAbsent | A value of type |
type ForbidNonComparable t = FailOnNonComparableFound (IsComparable t) Source #
Constraint that rises human-readable error message, in case given value can't be compared
type ForbidBigMap t = FailOnBigMapFound (ContainsBigMap t) Source #
type ForbidTicket t = FailOnTicketFound (ContainsTicket t) Source #
type ForbidContract t = FailOnContractFound (ContainsContract t) Source #
type ForbidOp t = FailOnOperationFound (ContainsOp t) Source #
type family FailOnNonComparableFound (comparable :: Bool) :: Constraint where ... Source #
Report a human-readable error that given value is not comparable
FailOnNonComparableFound 'True = () | |
FailOnNonComparableFound 'False = TypeError ('Text "Only comparable types are allowed here") |
type family FailOnNestedBigMapsFound (enabled :: Bool) :: Constraint where ... Source #
FailOnNestedBigMapsFound 'True = TypeError ('Text "Nested BigMaps are not allowed") | |
FailOnNestedBigMapsFound 'False = () |
type family FailOnBigMapFound (enabled :: Bool) :: Constraint where ... Source #
Report a human-readable error about TBigMap
at a wrong place.
FailOnBigMapFound 'True = TypeError ('Text "BigMaps are not allowed in this scope") | |
FailOnBigMapFound 'False = () |
type family FailOnTicketFound (enabled :: Bool) :: Constraint where ... Source #
Report a human-readable error about TTicket
at a wrong place.
FailOnTicketFound 'True = TypeError ('Text "Type `ticket` is not allowed in this scope") | |
FailOnTicketFound 'False = () |
type family FailOnContractFound (enabled :: Bool) :: Constraint where ... Source #
Report a human-readable error about TContract
at a wrong place.
FailOnContractFound 'True = TypeError ('Text "Type `contract` is not allowed in this scope") | |
FailOnContractFound 'False = () |
type family FailOnOperationFound (enabled :: Bool) :: Constraint where ... Source #
Report a human-readable error about TOperation
at a wrong place.
FailOnOperationFound 'True = TypeError ('Text "Operations are not allowed in this scope") | |
FailOnOperationFound 'False = () |
class ContainsNestedBigMaps t ~ 'False => HasNoNestedBigMaps t Source #
Constraint which ensures that there are no nested bigmaps.
Instances
ContainsNestedBigMaps t ~ 'False => HasNoNestedBigMaps t Source # | |
Defined in Morley.Michelson.Typed.Scope | |
SingI a => WithDeMorganScope HasNoNestedBigMaps 'TPair a b Source # | |
Defined in Morley.Michelson.Typed.Scope withDeMorganScope :: HasNoNestedBigMaps ('TPair a b) => ((HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret) -> ret Source # | |
SingI a => WithDeMorganScope HasNoNestedBigMaps 'TOr a b Source # | |
Defined in Morley.Michelson.Typed.Scope withDeMorganScope :: HasNoNestedBigMaps ('TOr a b) => ((HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret) -> ret Source # | |
SingI t => CheckScope (HasNoNestedBigMaps t) Source # | |
Defined in Morley.Michelson.Typed.Scope checkScope :: Either BadTypeForScope (Dict (HasNoNestedBigMaps t)) Source # |
class ContainsBigMap t ~ 'False => HasNoBigMap t Source #
Constraint which ensures that a value of type t
does not contain big_map
values.
Instances
ContainsBigMap t ~ 'False => HasNoBigMap t Source # | |
Defined in Morley.Michelson.Typed.Scope | |
SingI a => WithDeMorganScope HasNoBigMap 'TPair a b Source # | |
Defined in Morley.Michelson.Typed.Scope withDeMorganScope :: HasNoBigMap ('TPair a b) => ((HasNoBigMap a, HasNoBigMap b) => ret) -> ret Source # | |
SingI a => WithDeMorganScope HasNoBigMap 'TOr a b Source # | |
Defined in Morley.Michelson.Typed.Scope withDeMorganScope :: HasNoBigMap ('TOr a b) => ((HasNoBigMap a, HasNoBigMap b) => ret) -> ret Source # | |
SingI t => CheckScope (HasNoBigMap t) Source # | |
Defined in Morley.Michelson.Typed.Scope checkScope :: Either BadTypeForScope (Dict (HasNoBigMap t)) Source # |
class ContainsTicket t ~ 'False => HasNoTicket t Source #
Constraint which ensures that a value of type t
does not contain ticket
values.
Instances
ContainsTicket t ~ 'False => HasNoTicket t Source # | |
Defined in Morley.Michelson.Typed.Scope | |
SingI a => WithDeMorganScope HasNoTicket 'TPair a b Source # | |
Defined in Morley.Michelson.Typed.Scope withDeMorganScope :: HasNoTicket ('TPair a b) => ((HasNoTicket a, HasNoTicket b) => ret) -> ret Source # | |
SingI a => WithDeMorganScope HasNoTicket 'TOr a b Source # | |
Defined in Morley.Michelson.Typed.Scope withDeMorganScope :: HasNoTicket ('TOr a b) => ((HasNoTicket a, HasNoTicket b) => ret) -> ret Source # | |
SingI t => CheckScope (HasNoTicket t) Source # | |
Defined in Morley.Michelson.Typed.Scope checkScope :: Either BadTypeForScope (Dict (HasNoTicket t)) Source # |
class ContainsContract t ~ 'False => HasNoContract t Source #
Constraint which ensures that a value of type t
does not contain contract
values.
Instances
ContainsContract t ~ 'False => HasNoContract t Source # | |
Defined in Morley.Michelson.Typed.Scope | |
SingI a => WithDeMorganScope HasNoContract 'TPair a b Source # | |
Defined in Morley.Michelson.Typed.Scope withDeMorganScope :: HasNoContract ('TPair a b) => ((HasNoContract a, HasNoContract b) => ret) -> ret Source # | |
SingI a => WithDeMorganScope HasNoContract 'TOr a b Source # | |
Defined in Morley.Michelson.Typed.Scope withDeMorganScope :: HasNoContract ('TOr a b) => ((HasNoContract a, HasNoContract b) => ret) -> ret Source # | |
SingI t => CheckScope (HasNoContract t) Source # | |
Defined in Morley.Michelson.Typed.Scope checkScope :: Either BadTypeForScope (Dict (HasNoContract t)) Source # |
class ContainsOp t ~ 'False => HasNoOp t Source #
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 # | |
Defined in Morley.Michelson.Typed.Scope | |
SingI a => WithDeMorganScope HasNoOp 'TPair a b Source # | |
Defined in Morley.Michelson.Typed.Scope | |
SingI a => WithDeMorganScope HasNoOp 'TOr a b Source # | |
Defined in Morley.Michelson.Typed.Scope | |
SingI k => WithDeMorganScope HasNoOp 'TMap k v Source # | |
Defined in Morley.Michelson.Typed.Scope | |
SingI k => WithDeMorganScope HasNoOp 'TBigMap k v Source # | |
Defined in Morley.Michelson.Typed.Scope | |
SingI t => CheckScope (HasNoOp t) Source # | |
Defined in Morley.Michelson.Typed.Scope checkScope :: Either BadTypeForScope (Dict (HasNoOp t)) Source # |
type family IsComparable (t :: T) :: Bool where ... Source #
Constraint which ensures that type is comparable.
IsComparable ('TPair a b) = IsComparable a && IsComparable b | |
IsComparable ('TOption t) = IsComparable t | |
IsComparable 'TBls12381Fr = 'False | |
IsComparable 'TBls12381G1 = 'False | |
IsComparable 'TBls12381G2 = 'False | |
IsComparable ('TList _) = 'False | |
IsComparable ('TSet _) = 'False | |
IsComparable 'TOperation = 'False | |
IsComparable ('TContract _) = 'False | |
IsComparable ('TTicket _) = 'False | |
IsComparable ('TOr a b) = IsComparable a && IsComparable b | |
IsComparable ('TLambda _ _) = 'False | |
IsComparable ('TMap _ _) = 'False | |
IsComparable ('TBigMap _ _) = 'False | |
IsComparable 'TChest = 'False | |
IsComparable 'TChestKey = 'False | |
IsComparable _ = 'True |
type family ContainsNestedBigMaps (t :: T) :: Bool where ... Source #
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.
ContainsNestedBigMaps 'TKey = 'False | |
ContainsNestedBigMaps 'TUnit = 'False | |
ContainsNestedBigMaps 'TSignature = 'False | |
ContainsNestedBigMaps 'TChainId = 'False | |
ContainsNestedBigMaps ('TOption t) = ContainsNestedBigMaps t | |
ContainsNestedBigMaps ('TList t) = ContainsNestedBigMaps t | |
ContainsNestedBigMaps ('TSet _) = 'False | |
ContainsNestedBigMaps 'TOperation = 'False | |
ContainsNestedBigMaps ('TContract _) = 'False | |
ContainsNestedBigMaps ('TPair a b) = ContainsNestedBigMaps a || ContainsNestedBigMaps b | |
ContainsNestedBigMaps ('TOr a b) = ContainsNestedBigMaps a || ContainsNestedBigMaps b | |
ContainsNestedBigMaps ('TLambda _ _) = 'False | |
ContainsNestedBigMaps ('TMap _ v) = ContainsNestedBigMaps v | |
ContainsNestedBigMaps ('TBigMap _ v) = ContainsBigMap v | |
ContainsNestedBigMaps _ = 'False |
type family ContainsBigMap (t :: T) :: Bool where ... Source #
Whether a value of this type _may_ contain a big_map
value.
ContainsBigMap 'TKey = 'False | |
ContainsBigMap 'TUnit = 'False | |
ContainsBigMap 'TSignature = 'False | |
ContainsBigMap 'TChainId = 'False | |
ContainsBigMap ('TOption t) = ContainsBigMap t | |
ContainsBigMap ('TList t) = ContainsBigMap t | |
ContainsBigMap ('TSet _) = 'False | |
ContainsBigMap 'TOperation = 'False | |
ContainsBigMap ('TContract _) = 'False | |
ContainsBigMap ('TPair a b) = ContainsBigMap a || ContainsBigMap b | |
ContainsBigMap ('TOr a b) = ContainsBigMap a || ContainsBigMap b | |
ContainsBigMap ('TLambda _ _) = 'False | |
ContainsBigMap ('TMap _ v) = ContainsBigMap v | |
ContainsBigMap ('TBigMap _ _) = 'True | |
ContainsBigMap _ = 'False |
type family ContainsTicket (t :: T) :: Bool where ... Source #
Whether a value of this type _may_ contain a ticket
value.
ContainsTicket ('TOption t) = ContainsTicket t | |
ContainsTicket ('TList t) = ContainsTicket t | |
ContainsTicket ('TSet _) = 'False | |
ContainsTicket ('TTicket _) = 'True | |
ContainsTicket ('TPair a b) = ContainsTicket a || ContainsTicket b | |
ContainsTicket ('TOr a b) = ContainsTicket a || ContainsTicket b | |
ContainsTicket ('TLambda _ _) = 'False | |
ContainsTicket ('TMap _ v) = ContainsTicket v | |
ContainsTicket ('TBigMap _ v) = ContainsTicket v | |
ContainsTicket _ = 'False |
type family ContainsContract (t :: T) :: Bool where ... Source #
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.
ContainsContract 'TKey = 'False | |
ContainsContract 'TUnit = 'False | |
ContainsContract 'TSignature = 'False | |
ContainsContract 'TChainId = 'False | |
ContainsContract ('TOption t) = ContainsContract t | |
ContainsContract ('TList t) = ContainsContract t | |
ContainsContract ('TSet _) = 'False | |
ContainsContract 'TOperation = 'False | |
ContainsContract ('TContract _) = 'True | |
ContainsContract ('TPair a b) = ContainsContract a || ContainsContract b | |
ContainsContract ('TOr a b) = ContainsContract a || ContainsContract b | |
ContainsContract ('TLambda _ _) = 'False | |
ContainsContract ('TMap _ v) = ContainsContract v | |
ContainsContract ('TBigMap _ v) = ContainsContract v | |
ContainsContract _ = 'False |
type family ContainsOp (t :: T) :: Bool where ... Source #
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.
ContainsOp 'TKey = 'False | |
ContainsOp 'TUnit = 'False | |
ContainsOp 'TSignature = 'False | |
ContainsOp 'TChainId = 'False | |
ContainsOp ('TOption t) = ContainsOp t | |
ContainsOp ('TList t) = ContainsOp t | |
ContainsOp ('TSet t) = ContainsOp t | |
ContainsOp 'TOperation = 'True | |
ContainsOp ('TContract _) = 'False | |
ContainsOp ('TTicket t) = ContainsOp t | |
ContainsOp ('TPair a b) = ContainsOp a || ContainsOp b | |
ContainsOp ('TOr a b) = ContainsOp a || ContainsOp b | |
ContainsOp ('TLambda _ _) = 'False | |
ContainsOp ('TMap k v) = ContainsOp k || ContainsOp v | |
ContainsOp ('TBigMap k v) = ContainsOp k || ContainsOp v | |
ContainsOp _ = 'False |
forbiddenBigMap :: forall t a. (SingI t, ForbidBigMap t) => (HasNoBigMap t => a) -> a Source #
forbiddenNestedBigMaps :: forall t a. (SingI t, ForbidNestedBigMaps t) => (HasNoNestedBigMaps t => a) -> a Source #
forbiddenContractType :: forall t a. (SingI t, ForbidContract t) => (HasNoContract t => a) -> a Source #
Reify HasNoContract
contraint from ForbidContract
.
checkOpPresence :: Sing (ty :: T) -> OpPresence ty Source #
Check at runtime whether a value of the given type _may_ contain an operation.
checkContractTypePresence :: Sing (ty :: T) -> ContractPresence ty Source #
Check at runtime whether a value of the given type _may_ contain a contract
value.
checkTicketPresence :: Sing (ty :: T) -> TicketPresence ty Source #
Check at runtime whether a value of the given type _may_ contain a ticket
value.
checkBigMapPresence :: Sing (ty :: T) -> BigMapPresence ty Source #
Check at runtime whether a value of the given type _may_ contain a big_map
value.
checkNestedBigMapsPresence :: Sing (ty :: T) -> NestedBigMapsPresence ty Source #
Check at runtime whether a value of the given type _may_ contain nested big_map
s.
opAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoOp t) Source #
Check at runtime that a value of the given type cannot contain operations.
contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoContract t) Source #
Check at runtime that a value of the given type cannot contain contract
values.
bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoBigMap t) Source #
Check at runtime that a value of the given type cannot containt big_map
values
nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoNestedBigMaps t) Source #
Check at runtime that a value of the given type cannot contain nested big_map
s.
properParameterEvi :: forall t. ProperParameterBetterErrors t :- ParameterScope t Source #
properStorageEvi :: forall t. ProperStorageBetterErrors t :- StorageScope t Source #
properConstantEvi :: forall t. ProperConstantBetterErrors t :- ConstantScope t Source #
properDupableEvi :: forall t. ProperDupableBetterErrors t :- DupableScope t Source #
properPackedValEvi :: forall t. ProperPackedValBetterErrors t :- PackedValScope t Source #
properUnpackedValEvi :: forall t. ProperUnpackedValBetterErrors t :- UnpackedValScope t Source #
properViewableEvi :: forall t. ProperViewableBetterErrors t :- ViewableScope t Source #
properUntypedValEvi :: forall t. ProperUntypedValBetterErrors t :- UntypedValScope t Source #
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.
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
Eq EpName Source # | |
Ord EpName Source # | |
Show EpName Source # | |
Generic EpName Source # | |
ToJSON EpName Source # | |
Defined in Morley.Michelson.Untyped.Entrypoints | |
FromJSON EpName Source # | |
NFData EpName Source # | |
Defined in Morley.Michelson.Untyped.Entrypoints | |
Buildable EpName Source # | |
Defined in Morley.Michelson.Untyped.Entrypoints | |
HasCLReader EpName Source # | |
Defined in Morley.Michelson.Untyped.Entrypoints | |
type Rep EpName Source # | |
Defined in Morley.Michelson.Untyped.Entrypoints |
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
mkViewName :: Text -> Either BadViewNameError ViewName Source #
Construct ViewName
performing all the checks.
unsafeMkViewName :: HasCallStack => Text -> ViewName Source #
Unsafe constructor for ViewName
.
viewNameToMText :: ViewName -> MText Source #
Valid view names form a subset of valid Michelson texts.
Operation size in bytes.
We use newtype wrapper because there are different units of measure (another one is gas, and we don't want to confuse them).
opSizeHardLimit :: OpSize Source #
Maximal operation size allowed by Tezos production nodes.
smallTransferOpSize :: OpSize Source #
Base cost of any transfer of 0 mutez with no extra parameters.
(Add valueOpSize <param>
to it to get assessment of actual transfer op size)
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
Eq (Notes t) Source # | |
Show (Notes t) Source # | |
NFData (Notes t) Source # | |
Defined in Morley.Michelson.Typed.Annotation | |
Buildable (Notes t) Source # | |
Defined in Morley.Michelson.Typed.Annotation | |
RenderDoc (Notes t) Source # | |
Defined in Morley.Michelson.Typed.Annotation | |
SingI t => ToExpression (Notes t) Source # | |
Defined in Morley.Micheline.Class toExpression :: Notes t -> Expression Source # |
data AnnConvergeError where Source #
AnnConvergeError :: forall (tag :: Type). (Buildable (Annotation tag), Show (Annotation tag), Typeable tag) => Annotation tag -> Annotation tag -> AnnConvergeError |
Instances
Eq AnnConvergeError Source # | |
Defined in Morley.Michelson.Typed.Annotation (==) :: AnnConvergeError -> AnnConvergeError -> Bool # (/=) :: AnnConvergeError -> AnnConvergeError -> Bool # | |
Show AnnConvergeError Source # | |
Defined in Morley.Michelson.Typed.Annotation showsPrec :: Int -> AnnConvergeError -> ShowS # show :: AnnConvergeError -> String # showList :: [AnnConvergeError] -> ShowS # | |
NFData AnnConvergeError Source # | |
Defined in Morley.Michelson.Typed.Annotation rnf :: AnnConvergeError -> () # | |
Buildable AnnConvergeError Source # | |
Defined in Morley.Michelson.Typed.Annotation build :: AnnConvergeError -> Builder # |
starNotes :: forall t. SingI t => Notes t Source #
In memory of NStar
constructor.
Generates notes with no annotations.
converge :: Notes t -> Notes t -> Either AnnConvergeError (Notes t) Source #
Combines two annotations trees a
and b
into a new one c
in such a way that c
can be obtained from both a
and b
by replacing
some empty leaves with type or/and field annotations.
insertTypeAnn :: forall (b :: T). TypeAnn -> Notes b -> Notes b Source #
Insert the provided type annotation into the provided notes.
convergeAnns :: forall (tag :: Type). (Buildable (Annotation tag), Show (Annotation tag), Typeable tag) => Annotation tag -> Annotation tag -> Either AnnConvergeError (Annotation tag) Source #
Converge two type or field notes (which may be wildcards).
convergeDestrAnns :: FieldAnn -> FieldAnn -> Either AnnConvergeError FieldAnn Source #
Converge two field notes in CAR, CDR or UNPAIR, given that one of them may be a special annotation.
data SomeViewsSet' instr where Source #
SomeViewsSet :: SingI st => ViewsSet' instr st -> SomeViewsSet' instr |
Instances
(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 # | |
(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 -> () # |
data ViewsSetError Source #
Errors possible when constructing 'ViewsSet''.
Instances
Eq ViewsSetError Source # | |
Defined in Morley.Michelson.Typed.View (==) :: ViewsSetError -> ViewsSetError -> Bool # (/=) :: ViewsSetError -> ViewsSetError -> Bool # | |
Show ViewsSetError Source # | |
Defined in Morley.Michelson.Typed.View showsPrec :: Int -> ViewsSetError -> ShowS # show :: ViewsSetError -> String # showList :: [ViewsSetError] -> ShowS # | |
Buildable ViewsSetError Source # | |
Defined in Morley.Michelson.Typed.View build :: ViewsSetError -> Builder # |
newtype ViewsSet' instr st Source #
Views that belong to one contract.
Invariant: all view names are unique.
Implementation note: lookups still take linear time.
We use Seq
for simplicity, as in either case we need to preserve the order
of views (so that decoding/encoding roundtrip).
UnsafeViewsSet | |
|
pattern ViewsSet :: Seq (SomeView' instr st) -> ViewsSet' instr st | |
pattern ViewsList :: [SomeView' instr st] -> ViewsSet' instr st |
Instances
(forall (i :: [T]) (o :: [T]). Eq (instr i o)) => Eq (ViewsSet' instr st) Source # | |
(forall (i :: [T]) (o :: [T]). Show (instr i o)) => Show (ViewsSet' instr st) Source # | |
(forall (i :: [T]) (o :: [T]). NFData (instr i o)) => NFData (ViewsSet' instr st) Source # | |
Defined in Morley.Michelson.Typed.View | |
Default (ViewsSet' instr st) Source # | |
Defined in Morley.Michelson.Typed.View | |
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). Eq (ViewCode' instr arg st ret)) => Eq (SomeView' instr st) Source # | |
(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 |
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 :: 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 :: ViewName -> ViewsSet' instr st -> Maybe (SomeView' instr st) Source #
Find a view in the set.
viewsSetNames :: ViewsSet' instr st -> [ViewName] Source #
Get all taken names in views set.
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 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
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 # | |
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 -> () # | |
Buildable (EpLiftSequence arg param) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints build :: EpLiftSequence arg param -> Builder # |
data ParamEpError Source #
Errors specific to parameter type declaration (entrypoints).
Instances
Instances
Eq ArmCoord Source # | |
Show ArmCoord Source # | |
Generic ArmCoord Source # | |
NFData ArmCoord Source # | |
Defined in Morley.Michelson.Typed.Entrypoints | |
Buildable ArmCoord Source # | |
Defined in Morley.Michelson.Typed.Entrypoints | |
RenderDoc ArmCoord Source # | |
Defined in Morley.Michelson.Typed.Entrypoints | |
type Rep ArmCoord Source # | |
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. TODO: come up with better name?
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").
unsafeParseEpAddress :: HasCallStack => Text -> EpAddress Source #
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
Eq (SomeEntrypointCallT arg) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints (==) :: SomeEntrypointCallT arg -> SomeEntrypointCallT arg -> Bool # (/=) :: SomeEntrypointCallT arg -> SomeEntrypointCallT arg -> Bool # | |
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 -> () # | |
Buildable (SomeEntrypointCallT arg) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints build :: SomeEntrypointCallT arg -> Builder # |
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
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 # | |
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 -> () # | |
Buildable (EntrypointCallT param arg) Source # | |
Defined in Morley.Michelson.Typed.Entrypoints build :: EntrypointCallT param arg -> Builder # |
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.
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
ContainsUpdateableDoc (Contract cp st) Source # | |
Defined in Morley.Michelson.Typed.Doc modifyDocEntirely :: (SomeDocItem -> SomeDocItem) -> Contract cp st -> Contract cp st Source # | |
ContainsDoc (Contract cp st) Source # | |
Defined in Morley.Michelson.Typed.Doc buildDocUnfinalized :: Contract cp st -> ContractDoc Source # | |
ToExpression (Contract cp st) Source # | |
Defined in Morley.Micheline.Class toExpression :: Contract cp st -> Expression Source # | |
(forall (i :: [T]) (o :: [T]). Eq (instr i o)) => Eq (Contract' instr 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 |
type ContractCode' instr cp st = instr (ContractInp cp st) (ContractOut st) Source #
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 #
defaultContract :: (ParameterScope cp, StorageScope st) => ContractCode' instr cp st -> Contract' instr cp st Source #
mapContractCodeBlock :: (ContractCode' instr cp st -> ContractCode' instr cp st) -> Contract' instr cp st -> Contract' instr cp st Source #
Transform contract code
block.
To map e.g. views too, see mapContractCode
.
mapContractViewBlocks :: (forall arg ret. ViewCode' instr arg st ret -> ViewCode' instr arg st ret) -> Contract' instr cp st -> 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.
mapEntriesOrdered :: Contract' instr cp st -> (ParamNotes cp -> a) -> (Notes st -> a) -> (ContractCode' instr cp st -> a) -> [a] Source #
Map each typed contract fields by the given function and sort the output
based on the EntriesOrder
.
data Value' instr t where Source #
Representation of Michelson value.
Type parameter instr
stands for Michelson instruction
type, i.e. data type to represent an instruction of language.
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. (SingI t, Comparable t) => Set (Value' instr t) -> Value' instr ('TSet t) | |
VOp :: Operation' instr -> Value' instr 'TOperation | |
VContract :: forall arg instr. (SingI arg, HasNoOp 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, 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 ': '[]) -> Value' instr ('TLambda inp out) | |
VMap :: forall k v instr. (SingI k, 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 Comparability t where Source #
CanBeCompared :: Comparable t => Comparability t | |
CannotBeCompared :: IsComparable t ~ 'False => Comparability t |
type ComparabilityScope t = (SingI t, Comparable t) Source #
Alias for comparable types.
class IsComparable t ~ 'True => Comparable t Source #
tcompare
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
Eq (instr i o) => Eq (RemFail instr i o) Source # | Ignoring distinction between constructors here, comparing only semantics. |
(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 |
data CreateContract instr cp st Source #
(forall i o. Show (instr i o), forall i o. Eq (instr i o)) => CreateContract | |
|
Instances
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 # | |
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 -> () # | |
Buildable (CreateContract instr cp st) Source # | |
Defined in Morley.Michelson.Typed.Value build :: CreateContract instr cp st -> Builder # |
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 |
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.
getComparableProofS :: Sing (a :: T) -> Maybe (Dict (Comparable a)) Source #
checkComparability :: Sing t -> Comparability t Source #
comparabilityPresence :: Sing t -> Maybe (Dict $ Comparable t) Source #
addressToVContract :: forall t instr. (ParameterScope t, ForbidOr t) => Address -> Value' instr ('TContract t) Source #
Make value of contract
type which refers to the given address and
does not call any entrypoint.
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.
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 #
convergeEDiv :: Notes n -> Notes m -> Either AnnConvergeError (Notes ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))) Source #
Converge the notes of given operands.
evalEDivOp :: Value' instr n -> Value' instr m -> Value' instr ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m))) Source #
Instances
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 ('TMap k v) Source # | |
Defined in Morley.Michelson.Typed.Polymorphic | |
UpdOp ('TBigMap 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 ('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 family Bls12381MulBadOrder a1 a2 where ... 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 'TNat 'TNat Source # | |
Defined in Morley.Michelson.Typed.Arith convergeArith :: proxy Lsr -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Lsr 'TNat 'TNat)) Source # 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 'TNat 'TNat Source # | |
Instances
ArithOp Lsl 'TNat 'TNat Source # | |
Defined in Morley.Michelson.Typed.Arith convergeArith :: proxy Lsl -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Lsl 'TNat 'TNat)) Source # 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 'TNat 'TNat Source # | |
Instances
UnaryArithOp Not 'TInt Source # | |
Defined in Morley.Michelson.Typed.Arith | |
UnaryArithOp Not 'TNat Source # | |
Defined in Morley.Michelson.Typed.Arith | |
UnaryArithOp Not 'TBool 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 | |
type UnaryArithRes Not 'TBool 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
Instances
class ToIntArithOp (n :: T) where Source #
Class for conversions to an integer value.
Instances
ToIntArithOp 'TNat Source # | |
ToIntArithOp 'TBls12381Fr Source # | |
Defined in Morley.Michelson.Typed.Arith evalToIntOp :: forall (instr :: [T] -> [T] -> Type). Value' instr 'TBls12381Fr -> Value' instr 'TInt 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
.
convergeArith :: proxy aop -> Notes n -> Notes m -> Either AnnConvergeError (Notes (ArithRes aop n m)) Source #
Converge the notes of given operands.
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
SingI s => Eq (TestAssert s) Source # | |
Defined in Morley.Michelson.Typed.Convert (==) :: TestAssert s -> TestAssert s -> Bool # (/=) :: TestAssert s -> TestAssert s -> Bool # | |
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 -> () # |
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.
WithLoc :: InstrCallStack -> 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 |
InstrWithNotes :: forall a (topElems :: [T]) (s :: [T]). (RMap topElems, RecordToList topElems, ReifyConstraint Show Notes topElems, ReifyConstraint NFData Notes topElems, Each '[SingI] topElems) => Proxy s -> Rec Notes topElems -> Instr a (topElems ++ s) -> Instr a (topElems ++ s) | A wrapper for instructions that, when interpreted, will place field/type annotations on one or more of the elements at the top of the stack. This can wrap only instructions with at least one non-failing execution branch. See: Note [Annotations] |
InstrWithVarNotes :: NonEmpty VarAnn -> Instr a b -> Instr a b | A wrapper for instructions that have var annotations, e.g. `SOME_INSTR @ann1`. This information is necessary for serializing the instruction back to json/binary. See: Note [Annotations] |
InstrWithVarAnns :: VarAnns -> Instr a b -> Instr a b | A wrapper for instructions that, when interpreted, will place var annotations on one or more of the elements at the top of the stack. See: Note [Annotations] |
FrameInstr :: forall a b s. (KnownList a, KnownList b) => Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s) | Execute given instruction on truncated stack. This can wrap only instructions with at least one non-failing execution branch. Morley has no such instruction, it is used solely in eDSLs.
This instruction is sound because for all Michelson instructions
the following property holds: if some code accepts stack |
Seq :: Instr a b -> Instr b c -> Instr a c | |
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 |
Fn :: Text -> StackFn -> Instr inp out -> Instr inp out | Represents a typed stack function.
This is not part of |
AnnCAR :: VarAnn -> FieldAnn -> Instr ('TPair a b ': s) (a ': s) | CAR and CDR's original annotations must be retained inside the instruction's constructor. See: Note [Annotations - Exceptional scenarios]. |
AnnCDR :: 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) | |
DUP :: DupableScope a => Instr (a ': s) (a ': (a ': s)) | |
DUPN :: forall (n :: Peano) inp out a. (ConstraintDUPN n inp out a, DupableScope a) => 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 | |
PUSH :: forall t s. ConstantScope t => Value' Instr t -> Instr s (t ': s) | |
SOME :: Instr (a ': s) ('TOption a ': s) | |
NONE :: forall a s. SingI a => Instr s ('TOption a ': s) | |
UNIT :: Instr s ('TUnit ': s) | |
IF_NONE :: Instr s s' -> Instr (a ': s) s' -> Instr ('TOption a ': s) s' | |
AnnPAIR :: TypeAnn -> FieldAnn -> FieldAnn -> Instr (a ': (b ': s)) ('TPair a b ': s) | PAIR's original annotations must be retained inside the instruction's constructor. See: Note [Annotations - Exceptional scenarios]. |
AnnUNPAIR :: VarAnn -> VarAnn -> FieldAnn -> FieldAnn -> Instr ('TPair a b ': s) (a ': (b ': s)) | UNPAIR's original annotations must be retained inside the instruction's constructor. See: Note [Annotations - Exceptional scenarios]. |
PAIRN :: forall n inp. ConstraintPairN n inp => 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 => TypeAnn -> FieldAnn -> FieldAnn -> Instr (a ': s) ('TOr a b ': s) | LEFT and RIGHT's original annotations must be retained inside the instruction's constructor. See: Note [Annotations - Exceptional scenarios]. |
AnnRIGHT :: SingI a => TypeAnn -> FieldAnn -> FieldAnn -> Instr (b ': s) ('TOr a b ': s) | |
IF_LEFT :: Instr (a ': s) s' -> Instr (b ': s) s' -> Instr ('TOr a b ': s) s' | |
NIL :: SingI p => Instr s ('TList p ': s) | |
CONS :: Instr (a ': ('TList a ': s)) ('TList a ': s) | |
IF_CONS :: Instr (a ': ('TList a ': s)) s' -> Instr s s' -> Instr ('TList a ': s) s' | |
SIZE :: SizeOp c => Instr (c ': s) ('TNat ': s) | |
EMPTY_SET :: (SingI e, Comparable e) => Instr s ('TSet e ': s) | |
EMPTY_MAP :: (SingI a, SingI b, Comparable a) => Instr s ('TMap a b ': s) | |
EMPTY_BIG_MAP :: (SingI a, SingI b, Comparable a, HasNoBigMap b) => Instr s ('TBigMap a b ': s) | |
MAP :: (MapOp c, SingI b) => 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 | |
MEM :: MemOp c => Instr (MemOpKey c ': (c ': s)) ('TBool ': s) | |
GET :: (GetOp c, SingI (GetOpVal c)) => Instr (GetOpKey c ': (c ': s)) ('TOption (GetOpVal c) ': s) | |
GETN :: forall (ix :: Peano) (pair :: T) (s :: [T]). ConstraintGetN ix pair => 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
|
UPDATE :: UpdOp c => Instr (UpdOpKey c ': (UpdOpParams c ': (c ': s))) (c ': s) | |
UPDATEN :: forall (ix :: Peano) (val :: T) (pair :: T) (s :: [T]). ConstraintUpdateN ix pair => PeanoNatural ix -> Instr (val ': (pair ': s)) (UpdateN ix val pair ': s) | Update the node at index
Note that
|
GET_AND_UPDATE :: (GetOp c, UpdOp c, SingI (GetOpVal c), UpdOpKey c ~ GetOpKey c) => 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) | |
LAMBDA :: forall i o s. (SingI i, SingI o) => Value' Instr ('TLambda i o) -> Instr s ('TLambda i o ': s) | |
EXEC :: Instr (t1 ': ('TLambda t1 t2 ': s)) (t2 ': s) | |
APPLY :: forall a b c s. (ConstantScope a, SingI b) => 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 | |
CAST :: forall a s. SingI a => Instr (a ': s) (a ': s) | |
RENAME :: Instr (a ': s) (a ': s) | |
PACK :: PackedValScope a => Instr (a ': s) ('TBytes ': s) | |
UNPACK :: (UnpackedValScope a, SingI a) => Instr ('TBytes ': s) ('TOption a ': s) | |
CONCAT :: ConcatOp c => Instr (c ': (c ': s)) (c ': s) | |
CONCAT' :: ConcatOp c => Instr ('TList c ': s) (c ': s) | |
SLICE :: (SliceOp c, SingI c) => Instr ('TNat ': ('TNat ': (c ': s))) ('TOption c ': s) | |
ISNAT :: Instr ('TInt ': s) ('TOption 'TNat ': s) | |
ADD :: ArithOp Add n m => Instr (n ': (m ': s)) (ArithRes Add n m ': s) | |
SUB :: ArithOp Sub n m => Instr (n ': (m ': s)) (ArithRes Sub n m ': s) | |
MUL :: ArithOp Mul n m => Instr (n ': (m ': s)) (ArithRes Mul n m ': s) | |
EDIV :: ArithOp EDiv n m => Instr (n ': (m ': s)) (ArithRes EDiv n m ': s) | |
ABS :: UnaryArithOp Abs n => Instr (n ': s) (UnaryArithRes Abs n ': s) | |
NEG :: UnaryArithOp Neg n => Instr (n ': s) (UnaryArithRes Neg n ': s) | |
LSL :: ArithOp Lsl n m => Instr (n ': (m ': s)) (ArithRes Lsl n m ': s) | |
LSR :: ArithOp Lsr n m => Instr (n ': (m ': s)) (ArithRes Lsr n m ': s) | |
OR :: ArithOp Or n m => Instr (n ': (m ': s)) (ArithRes Or n m ': s) | |
AND :: ArithOp And n m => Instr (n ': (m ': s)) (ArithRes And n m ': s) | |
XOR :: ArithOp Xor n m => Instr (n ': (m ': s)) (ArithRes Xor n m ': s) | |
NOT :: UnaryArithOp Not n => Instr (n ': s) (UnaryArithRes Not n ': s) | |
COMPARE :: (Comparable n, SingI n) => Instr (n ': (n ': s)) ('TInt ': s) | |
EQ :: UnaryArithOp Eq' n => Instr (n ': s) (UnaryArithRes Eq' n ': s) | |
NEQ :: UnaryArithOp Neq n => Instr (n ': s) (UnaryArithRes Neq n ': s) | |
LT :: UnaryArithOp Lt n => Instr (n ': s) (UnaryArithRes Lt n ': s) | |
GT :: UnaryArithOp Gt n => Instr (n ': s) (UnaryArithRes Gt n ': s) | |
LE :: UnaryArithOp Le n => Instr (n ': s) (UnaryArithRes Le n ': s) | |
GE :: UnaryArithOp Ge n => Instr (n ': s) (UnaryArithRes Ge n ': s) | |
INT :: ToIntArithOp n => Instr (n ': s) ('TInt ': s) | |
VIEW :: (SingI arg, ViewableScope ret) => ViewName -> Notes ret -> Instr (arg ': ('TAddress ': s)) ('TOption ret ': s) | |
SELF :: forall (arg :: T) s. ParameterScope arg => SomeEntrypointCallT arg -> Instr s ('TContract arg ': s) | |
CONTRACT :: ParameterScope p => Notes p -> EpName -> Instr ('TAddress ': s) ('TOption ('TContract p) ': s) | |
TRANSFER_TOKENS :: ParameterScope p => Instr (p ': ('TMutez ': ('TContract p ': s))) ('TOperation ': s) | |
SET_DELEGATE :: Instr ('TOption 'TKeyHash ': s) ('TOperation ': s) | |
CREATE_CONTRACT :: (ParameterScope p, StorageScope g) => Contract' Instr p g -> Instr ('TOption 'TKeyHash ': ('TMutez ': (g ': s))) ('TOperation ': ('TAddress ': s)) | |
IMPLICIT_ACCOUNT :: Instr ('TKeyHash ': s) ('TContract 'TUnit ': s) | |
NOW :: Instr s ('TTimestamp ': s) | |
AMOUNT :: Instr s ('TMutez ': s) | |
BALANCE :: Instr s ('TMutez ': s) | |
VOTING_POWER :: Instr ('TKeyHash ': s) ('TNat ': s) | |
TOTAL_VOTING_POWER :: Instr s ('TNat ': s) | |
CHECK_SIGNATURE :: Instr ('TKey ': ('TSignature ': ('TBytes ': s))) ('TBool ': s) | |
SHA256 :: Instr ('TBytes ': s) ('TBytes ': s) | |
SHA512 :: Instr ('TBytes ': s) ('TBytes ': s) | |
BLAKE2B :: Instr ('TBytes ': s) ('TBytes ': s) | |
SHA3 :: Instr ('TBytes ': s) ('TBytes ': s) | |
KECCAK :: Instr ('TBytes ': s) ('TBytes ': s) | |
HASH_KEY :: Instr ('TKey ': s) ('TKeyHash ': s) | |
PAIRING_CHECK :: Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) ': s) ('TBool ': s) | |
SOURCE :: Instr s ('TAddress ': s) | |
SENDER :: Instr s ('TAddress ': s) | |
ADDRESS :: Instr ('TContract a ': s) ('TAddress ': s) | |
CHAIN_ID :: Instr s ('TChainId ': s) | |
LEVEL :: Instr s ('TNat ': s) | |
SELF_ADDRESS :: Instr s ('TAddress ': s) | |
NEVER :: Instr ('TNever ': s) t | |
TICKET :: Comparable a => Instr (a ': ('TNat ': s)) ('TTicket a ': s) | |
READ_TICKET :: Instr ('TTicket a ': s) (RightComb ['TAddress, a, 'TNat] ': ('TTicket a ': s)) | |
SPLIT_TICKET :: Instr ('TTicket a ': ('TPair 'TNat 'TNat ': s)) ('TOption ('TPair ('TTicket a) ('TTicket a)) ': s) | |
JOIN_TICKETS :: Instr ('TPair ('TTicket a) ('TTicket a) ': s) ('TOption ('TTicket a) ': s) | |
OPEN_CHEST :: Instr ('TChestKey ': ('TChest ': ('TNat ': s))) ('TOr 'TBytes 'TBool ': s) |
Instances
type family UpdateN (ix :: Peano) (val :: T) (pair :: T) :: T where ... Source #
Update the node at index ix
of a right-combed pair.
type ConstraintUpdateN (ix :: Peano) (pair :: T) = TypeErrorUnless (CombedPairNodeIndexIsValid ix pair) (If (IsPair pair) ((((('Text "'UPDATE " :<>: 'ShowType (FromPeano ix)) :<>: 'Text "' expects the 2nd element of the stack to be a right-combed pair with at least ") :<>: 'ShowType (FromPeano ix + 1)) :<>: 'Text " nodes,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairNodeCount pair))) :<>: 'Text " nodes.")) ('Text "Expected the 2nd element of the stack to be a pair, but found: " :<>: 'ShowType pair)) Source #
type family GetN (ix :: Peano) (pair :: T) :: T where ... Source #
Get the node at index ix
of a right-combed pair.
type ConstraintGetN (ix :: Peano) (pair :: T) = TypeErrorUnless (CombedPairNodeIndexIsValid ix pair) (If (IsPair pair) ((((('Text "'GET " :<>: 'ShowType (FromPeano ix)) :<>: 'Text "' expects a right-combed pair with at least ") :<>: 'ShowType (FromPeano ix + 1)) :<>: 'Text " nodes at the top of the stack,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairNodeCount pair))) :<>: 'Text " nodes.")) ('Text "Expected a pair at the top of the stack, but found: " :<>: 'ShowType pair)) Source #
type family UnpairN (n :: Peano) (s :: T) :: [T] where ... Source #
Splits a right-combed pair into n
elements.
UnpairN (ToPeano 3) ('TPair 'TInt ('TPair 'TString 'TUnit)) ~ '[ 'TInt, 'TString, 'TUnit]
UnpairN (ToPeano 3) ('TPair 'TInt ('TPair 'TString ('TPair 'TUnit 'TInt))) ~ '[ 'TInt, 'TString, 'TPair 'TUnit 'TInt]
type ConstraintUnpairN (n :: Peano) (pair :: T) = (TypeErrorUnless (n >= ToPeano 2) ('Text "'UNPAIR n' expects n \8805 2"), TypeErrorUnless (CombedPairLeafCountIsAtLeast n pair) (If (IsPair pair) ((((('Text "'UNPAIR " :<>: 'ShowType (FromPeano n)) :<>: 'Text "' expects a right-combed pair with at least ") :<>: 'ShowType (FromPeano n)) :<>: 'Text " elements at the top of the stack,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairLeafCount pair))) :<>: 'Text " elements.")) ('Text "Expected a pair at the top of the stack, but found: " :<>: 'ShowType pair))) Source #
type family RightComb (s :: [T]) :: T where ... Source #
Folds a stack into a right-combed pair.
RightComb '[ 'TInt, 'TString, 'TUnit ] ~ 'TPair 'TInt ('TPair 'TString 'TUnit)
type ConstraintPairN (n :: Peano) (inp :: [T]) = (RequireLongerOrSameLength inp n, TypeErrorUnless (n >= ToPeano 2) ('Text "'PAIR n' expects n \8805 2")) Source #
type ConstraintDUG n inp out a = ConstraintDUG' T n inp out a Source #
type ConstraintDUG' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (RequireLongerThan out n, inp ~ (a ': Drop ('S 'Z) inp), out ~ (Take n (Drop ('S 'Z) inp) ++ (a ': Drop ('S n) inp))) Source #
Constraint that is used in DUG, we want to share it with typechecking code and eDSL code.
type ConstraintDIG n inp out a = ConstraintDIG' T n inp out a Source #
type ConstraintDIG' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (RequireLongerThan inp n, inp ~ (Take n inp ++ (a ': Drop ('S n) inp)), out ~ (a ': (Take n inp ++ Drop ('S n) inp))) Source #
Constraint that is used in DIG, we want to share it with typechecking code and eDSL code.
type ConstraintDIPN n inp out s s' = ConstraintDIPN' T n inp out s s' Source #
type ConstraintDIPN' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (s :: [kind]) (s' :: [kind]) = (RequireLongerOrSameLength inp n, (Take n inp ++ s) ~ inp, (Take n inp ++ s') ~ out) Source #
Constraint that is used in DIPN, we want to share it with typechecking code and eDSL code.
type ConstraintDUPN n inp out a = ConstraintDUPN' T n inp out a Source #
type ConstraintDUPN' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (RequireLongerOrSameLength inp n, (n > 'Z) ~ 'True, inp ~ (Take (Decrement n) inp ++ (a ': Drop n inp)), out ~ (a ': inp)) Source #
Constraint that is used in DUPN, we want to share it with typechecking code and eDSL code.
pattern (:#) :: Instr a b -> Instr b c -> Instr a c infixr 8 Source #
Right-associative operator for Seq
.
>>>
show (DROP :# UNIT :# Nop) == 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, SingI (ToPeano gn), RequireLongerThan st n) => StackRef st Source #
Create a stack reference, performing checks at compile time.
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 x Source #
Describes how intermediate nodes in instruction tree are accounted.
CtorEffectsApp | |
|
Instances
Show (CtorEffectsApp x) Source # | |
Defined in Morley.Michelson.Typed.Util showsPrec :: Int -> CtorEffectsApp x -> ShowS # show :: CtorEffectsApp x -> String # showList :: [CtorEffectsApp x] -> ShowS # |
data DfsSettings x Source #
Options for dfsInstr
.
DfsSettings | |
|
Instances
Show (DfsSettings x) Source # | |
Defined in Morley.Michelson.Typed.Util showsPrec :: Int -> DfsSettings x -> ShowS # show :: DfsSettings x -> String # showList :: [DfsSettings x] -> ShowS # | |
Default (DfsSettings x) Source # | |
Defined in Morley.Michelson.Typed.Util def :: DfsSettings x # |
ceaBottomToTop :: CtorEffectsApp x Source #
Gather effects first for children nodes, then for their parents.
dfsInstr :: forall x inp out. Semigroup x => DfsSettings x -> (forall i o. Instr i o -> (Instr i o, x)) -> Instr inp out -> (Instr inp out, x) Source #
Traverse a typed instruction in depth-first order.
<>
is used to concatenate intermediate results.
Each instructions can be changed using the supplied step
function.
It does not consider extra instructions (not present in Michelson).
dfsFoldInstr :: forall x inp out. Semigroup x => DfsSettings x -> (forall i o. Instr i o -> x) -> Instr inp out -> x Source #
Specialization of dfsInstr
for case when changing the instruction is
not required.
dfsModifyInstr :: DfsSettings () -> (forall i o. Instr i o -> Instr i o) -> Instr inp out -> Instr inp out Source #
Specialization of dfsInstr
which only modifies given instruction.
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. (forall t'. Value t' -> Value t') -> Value t -> Value t Source #
Traverse a value in depth-first order.
dfsTraverseValue :: forall t m. Monad m => (forall t'. Value t' -> m (Value t')) -> 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.
class (SingI t, WellTypedSuperC t) => WellTyped (t :: 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
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' (t :: [k]) :: [T] where ... Source #
Overloaded version of ToTs
to work on Haskell and T
stacks.
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
Ord k => ToBigMap [(k, v)] Source # | |
Defined in Morley.Michelson.Typed.Haskell.Value type ToBigMapKey [(k, v)] Source # type ToBigMapValue [(k, v)] Source # mkBigMap :: [(k, v)] -> BigMap (ToBigMapKey [(k, v)]) (ToBigMapValue [(k, v)]) Source # | |
Ord k => ToBigMap (NonEmpty (k, v)) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Value type ToBigMapKey (NonEmpty (k, v)) Source # type ToBigMapValue (NonEmpty (k, v)) Source # mkBigMap :: NonEmpty (k, v) -> BigMap (ToBigMapKey (NonEmpty (k, v))) (ToBigMapValue (NonEmpty (k, v))) Source # | |
ToBigMap (Map k v) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Value type ToBigMapKey (Map k v) Source # type ToBigMapValue (Map k v) Source # mkBigMap :: Map k v -> BigMap (ToBigMapKey (Map k v)) (ToBigMapValue (Map k v)) Source # |
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 # | |
Buildable (BigMapId k2 v) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Value | |
IsoValue (BigMapId k2 v) Source # | |
type ToT (BigMapId k2 v) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Value |
data Ticket (arg :: Type) Source #
Ticket type.
Instances
Eq arg => Eq (Ticket arg) Source # | |
Show arg => Show (Ticket arg) Source # | |
(Comparable (ToT a), IsoValue a) => IsoValue (Ticket a) 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 # | |
type ToT (Ticket a) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Value | |
type TypeDocFieldDescriptions (Ticket a) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Doc |
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 HasNoOpToT a = HasNoOp (ToT a) Source #
type WellTypedToT a = WellTyped (ToT a) Source #
type SomeEntrypointCall arg = SomeEntrypointCallT (ToT arg) Source #
type EntrypointCall param arg = EntrypointCallT (ToT param) (ToT arg) Source #
type family ToT' (t :: k) :: T where ... Source #
Overloaded version of ToT
to work on Haskell and T
types.
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 (S1 i x) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseBranchInput ctor (x :*: y) 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 (S1 i x) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseBranchInput ctor (x :*: y) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum |
type family GCaseClauses x :: [CaseClauseParam] Source #
Instances
type GCaseClauses (V1 :: Type -> Type) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseClauses (x :+: y) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseClauses (D1 i x) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseClauses (C1 ('MetaCons ctor _1 _2) x) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum |
type family GCaseClauses x :: [CaseClauseParam] Source #
Instances
type GCaseClauses (V1 :: Type -> Type) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseClauses (x :+: y) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseClauses (D1 i x) Source # | |
Defined in Morley.Michelson.Typed.Haskell.Instr.Sum | |
type GCaseClauses (C1 ('MetaCons ctor _1 _2) x) 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 :: CtorField) (l :: [k]) :: [k] 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 = (GenericIsoValue dt, GInstrDeconstruct (Rep dt)) Source #
Constraint for instrConstruct
.
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 instrToField
.
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.
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.
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), KnownList stack) => Instr (stack ++ st) (ToT dt ': st) Source #
instrDeconstruct :: forall dt stack st. (InstrDeconstructC dt, stack ~ ToTs (ConstructorFieldTypes dt), KnownList stack) => Instr (ToT dt ': st) (stack ++ st) Source #
For given complex type dt
deconstruct it to its field types.
convertParamNotes :: SingI cp => 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
.
convertView :: forall arg store ret. View arg store ret -> View Source #
convertSomeView :: SomeView st -> View Source #
convertContract :: Contract param store -> Contract Source #
untypeValue :: HasNoOp t => Value' Instr t -> Value Source #
Convert a typed value to an untyped human-readable representation
untypeValueHashable :: HasNoOp t => Value' Instr t -> Value Source #
Like untypeValueOptimized
, but without list notation for pairs.
Created to match tezos-client hash data
behaviour for typed values.
untypeValueOptimized :: HasNoOp 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 :: 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 :: SingI t => 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.
instrOpSize :: Instr inp out -> OpSize Source #
Estimate instruction operation size.
contractOpSize :: Contract cp st -> OpSize Source #
Estimate contract code operation size.
valueOpSize :: UntypedValScope t => Value t -> OpSize Source #
Estimate value operation size.
data SomeStorage where Source #
SomeStorage :: forall st. StorageScope st => Value st -> SomeStorage |
Instances
Show SomeStorage Source # | |
Defined in Morley.Michelson.Typed.Existential showsPrec :: Int -> SomeStorage -> ShowS # show :: SomeStorage -> String # showList :: [SomeStorage] -> ShowS # |
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 |
data SomeConstant where Source #
SomeConstant :: (ConstantScope t, SingI t) => Value t -> SomeConstant |
Instances
Buildable SomeConstant Source # | |
Defined in Morley.Michelson.Typed.Existential build :: SomeConstant -> Builder # | |
RenderDoc SomeConstant Source # | |
Defined in Morley.Michelson.Typed.Existential renderDoc :: RenderContext -> SomeConstant -> Doc Source # isRenderable :: SomeConstant -> Bool Source # |
data SomeConstrainedValue (c :: T -> Constraint) where Source #
SomeConstrainedValue :: forall (t :: T) (c :: T -> Constraint). c t => Value t -> SomeConstrainedValue c |
Instances
Show (SomeConstrainedValue c) Source # | |
Defined in Morley.Michelson.Typed.Existential showsPrec :: Int -> SomeConstrainedValue c -> ShowS # show :: SomeConstrainedValue c -> String # showList :: [SomeConstrainedValue c] -> ShowS # |
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 # | |
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 # | |
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 # |
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
Eq SomeAnnotatedValue Source # | |
Defined in Morley.Michelson.Typed.AnnotatedValue (==) :: SomeAnnotatedValue -> SomeAnnotatedValue -> Bool # (/=) :: SomeAnnotatedValue -> SomeAnnotatedValue -> Bool # | |
Show SomeAnnotatedValue Source # | |
Defined in Morley.Michelson.Typed.AnnotatedValue showsPrec :: Int -> SomeAnnotatedValue -> ShowS # show :: SomeAnnotatedValue -> String # showList :: [SomeAnnotatedValue] -> ShowS # | |
Buildable SomeAnnotatedValue Source # | |
Defined in Morley.Michelson.Typed.AnnotatedValue build :: SomeAnnotatedValue -> Builder # |
data AnnotatedValue v Source #
Instances
Eq (AnnotatedValue v) Source # | |
Defined in Morley.Michelson.Typed.AnnotatedValue (==) :: AnnotatedValue v -> AnnotatedValue v -> Bool # (/=) :: AnnotatedValue v -> AnnotatedValue v -> Bool # | |
Show (AnnotatedValue v) Source # | |
Defined in Morley.Michelson.Typed.AnnotatedValue showsPrec :: Int -> AnnotatedValue v -> ShowS # show :: AnnotatedValue v -> String # showList :: [AnnotatedValue v] -> ShowS # | |
SingI (ToT v) => Buildable (AnnotatedValue v) Source # | |
Defined in Morley.Michelson.Typed.AnnotatedValue build :: AnnotatedValue v -> Builder # |
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 => GProductHasDoc (S1 ('MetaSel ('Nothing :: Maybe Symbol) _1 _2 _3) (Rec0 a)) 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] |
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 # | |
GTypeHasDoc x => GTypeHasDoc (D1 ('MetaData _a _b _c 'True) x) Source # | |
GTypeHasDoc x => GTypeHasDoc (D1 ('MetaData _a _b _c 'False) x) Source # | |
(GProductHasDoc x, KnownSymbol ctor) => GTypeHasDoc (C1 ('MetaCons ctor _1 _2) 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 # | |
Show 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 # | |
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 polymorhpic 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 polymorhpic 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 polymorhpic 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 polymorhpic types consider using concreteTypeDocHaskellRep
as implementation.
Modifier haskellRepNoFields
can be used to hide names of fields,
beneficial for newtypes.
Another modifier called haskellRepStripFieldPrefix
can be used for datatypes
to leave only meaningful part of name in every field.
default typeDocHaskellRep :: (Generic a, GTypeHasDoc (Rep a), IsHomomorphic a) => TypeDocHaskellRep a Source #
typeDocMichelsonRep :: TypeDocMichelsonRep a Source #
Final michelson representation of a type.
For homomorphic types use homomorphicTypeDocMichelsonRep
implementation.
For polymorhpic types consider using concreteTypeDocMichelsonRep
as implementation.
default typeDocMichelsonRep :: (KnownIsoT a, IsHomomorphic a) => TypeDocMichelsonRep a Source #
Instances
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 -> Builder Source #
Fully render Michelson representation of a type.
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 polymorhpic types which, for documentation
purposes, we want to consider homomorphic.
Example: Operation
is in fact polymorhpic, 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 polymorhpic
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.
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.
haskellRepStripFieldPrefix :: HasCallStack => TypeDocHaskellRep a -> TypeDocHaskellRep a Source #
Cut fields prefixes which we use according to the style guide.
E.g. cmMyField
field will be transformed to myField
.
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.
buildInstrDocWithGitRev :: DGitRevision -> Instr inp out -> ContractDoc Source #
Deprecated: Use `buildDoc . attachDocCommons gitRev` instead.
Assemble contract documentation with the revision of the contract.
buildInstrDoc :: Instr inp out -> ContractDoc Source #
Deprecated: Use buildDoc
instead.
Assemble contract documentation.
modifyInstrAllDoc :: (SomeDocItem -> SomeDocItem) -> Instr inp out -> Instr inp out Source #
Deprecated: Use modifyDocEntirely
instead.
Modify all documentation items recursively.
modifyInstrDoc :: (DocItem i1, DocItem i2) => (i1 -> Maybe i2) -> Instr inp out -> Instr inp out Source #
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.