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