Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Module, containing data types for Michelson value.
Synopsis
- data Instr (inp :: [T]) (out :: [T]) where
- WithLoc :: ErrorSrcPos -> Instr a b -> Instr a b
- Meta :: SomeMeta -> Instr a b -> Instr a b
- FrameInstr :: forall a b s. (KnownList a, KnownList b) => Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
- Seq :: Instr a b -> Instr b c -> Instr a c
- Nop :: Instr s s
- Ext :: ExtInstr s -> Instr s s
- Nested :: Instr inp out -> Instr inp out
- DocGroup :: DocGrouping -> Instr inp out -> Instr inp out
- 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 :: (SingI e, Comparable e) => Anns '[TypeAnn, VarAnn, Notes e] -> Instr s ('TSet e ': s)
- AnnEMPTY_MAP :: (SingI a, SingI b, Comparable a) => Anns '[TypeAnn, VarAnn, Notes a, Notes b] -> Instr s ('TMap a b ': s)
- AnnEMPTY_BIG_MAP :: (SingI a, SingI b, Comparable a, HasNoBigMap 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] -> Value' Instr ('TLambda i 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 :: UnaryArithOp Not n => AnnVar -> Instr (n ': s) (UnaryArithRes Not n ': s)
- AnnCOMPARE :: (Comparable n, SingI 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)
- 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 :: Comparable a => AnnVar -> Instr (a ': ('TNat ': s)) ('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)
- pattern CAR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) ('TPair a b) s, out ~ '(:) a s) => 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 DUP :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) a ('(:) a s), DupableScope a) => 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 PUSH :: forall {inp} {out}. () => forall (t :: T) (s :: [T]). (inp ~ s, out ~ '(:) t s, ConstantScope t) => Value' Instr t -> Instr inp out
- pattern SOME :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) ('TOption a) s) => 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 UNIT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TUnit 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 UNPAIR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) ('TPair a b) s, out ~ '(:) a ('(:) b s)) => 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 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 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 NIL :: forall {inp} {out}. () => forall (p :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TList p) s, SingI p) => 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 SIZE :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) c s, out ~ '(:) 'TNat s, SizeOp c) => Instr inp out
- pattern EMPTY_SET :: forall {inp} {out}. () => forall (e :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TSet e) s, SingI e, Comparable e) => Instr inp out
- pattern EMPTY_MAP :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TMap a b) s, SingI a, SingI b, Comparable a) => Instr inp out
- pattern EMPTY_BIG_MAP :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TBigMap a b) s, SingI a, SingI b, Comparable a, HasNoBigMap b) => 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 MEM :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) (MemOpKey c) ('(:) c s), out ~ '(:) 'TBool s, MemOp c) => 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 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 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 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 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 LAMBDA :: forall {inp} {out}. () => forall (i :: T) (o :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TLambda i o) s, SingI i, SingI o) => Value' Instr ('TLambda i o) -> 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 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 CAST :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) a s, SingI a) => Instr inp out
- pattern RENAME :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) a s) => 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 UNPACK :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) ('TOption a) s, UnpackedValScope a, SingI a) => 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 CONCAT' :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) ('TList c) s, out ~ '(:) c s, ConcatOp c) => 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 ISNAT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TInt s, out ~ '(:) ('TOption 'TNat) s) => 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 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 SUB_MUTEZ :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TMutez ('(:) 'TMutez s), out ~ '(:) ('TOption 'TMutez) s) => 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 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 ABS :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Abs n) s, UnaryArithOp Abs n) => 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 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 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 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 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 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 NOT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Not n) s, UnaryArithOp Not n) => Instr inp out
- pattern COMPARE :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n ('(:) n s), out ~ '(:) 'TInt s, Comparable n, SingI n) => Instr inp out
- pattern EQ :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Eq' n) s, UnaryArithOp Eq' n) => Instr inp out
- pattern NEQ :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Neq n) s, UnaryArithOp Neq n) => Instr inp out
- pattern LT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Lt n) s, UnaryArithOp Lt n) => Instr inp out
- pattern GT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Gt n) s, UnaryArithOp Gt n) => 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 GE :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Ge n) s, UnaryArithOp Ge n) => 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 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 SELF :: forall {inp} {out}. () => forall (arg :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TContract arg) s, ParameterScope arg, IsNotInView) => SomeEntrypointCallT arg -> 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 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 SET_DELEGATE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) ('TOption 'TKeyHash) s, out ~ '(:) 'TOperation s, IsNotInView) => 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 IMPLICIT_ACCOUNT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKeyHash s, out ~ '(:) ('TContract 'TUnit) s) => Instr inp out
- pattern NOW :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TTimestamp s) => Instr inp out
- pattern AMOUNT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TMutez s) => Instr inp out
- pattern BALANCE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TMutez s) => Instr inp out
- pattern VOTING_POWER :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKeyHash s, out ~ '(:) 'TNat s) => Instr inp out
- pattern TOTAL_VOTING_POWER :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TNat 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 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 BLAKE2B :: 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 KECCAK :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out
- pattern HASH_KEY :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKey s, out ~ '(:) 'TKeyHash 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 SOURCE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TAddress s) => Instr inp out
- pattern SENDER :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TAddress 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 CHAIN_ID :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TChainId s) => Instr inp out
- pattern LEVEL :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TNat s) => Instr inp out
- pattern SELF_ADDRESS :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TAddress s) => Instr inp out
- pattern TICKET :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a ('(:) 'TNat s), out ~ '(:) ('TTicket a) s, Comparable a) => 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 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 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 OPEN_CHEST :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TChestKey ('(:) 'TChest ('(:) 'TNat s)), out ~ '(:) ('TOr 'TBytes 'TBool) 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 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 MIN_BLOCK_TIME :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TNat s) => Instr inp out
- castInstr :: forall inp1 out1 inp2 out2. (SingI inp1, SingI out1, SingI inp2, SingI out2) => Instr inp1 out1 -> Maybe (Instr inp2 out2)
- pattern (:#) :: Instr a b -> Instr b c -> Instr a c
- data ExtInstr s
- data CommentType
- data StackRef (st :: [T]) where
- StackRef :: RequireLongerThan st idx => PeanoNatural idx -> StackRef st
- mkStackRef :: forall (gn :: Nat) st n. (n ~ ToPeano gn, SingIPeano gn, RequireLongerThan st n) => 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
- pattern ConcreteMeta :: Typeable meta => meta -> Instr i o -> Instr i o
- type ConstraintDUPN n inp out a = ConstraintDUPN' T n inp out a
- type ConstraintDUPN' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (RequireLongerOrSameLength inp n, (n > 'Z) ~ 'True, inp ~ (Take (Decrement n) inp ++ (a ': Drop n inp)), out ~ (a ': inp))
- type ConstraintDIPN n inp out s s' = ConstraintDIPN' T n inp out s s'
- type ConstraintDIPN' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (s :: [kind]) (s' :: [kind]) = (RequireLongerOrSameLength inp n, (Take n inp ++ s) ~ inp, (Take n inp ++ s') ~ out)
- type ConstraintDIG n inp out a = ConstraintDIG' T n inp out a
- type ConstraintDIG' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (KnownList inp, RequireLongerThan inp n, inp ~ (Take n inp ++ (a ': Drop ('S n) inp)), out ~ (a ': (Take n inp ++ Drop ('S n) inp)))
- type ConstraintDUG n inp out a = ConstraintDUG' T n inp out a
- type ConstraintDUG' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (RequireLongerThan out n, inp ~ (a ': Drop ('S 'Z) inp), out ~ (Take n (Drop ('S 'Z) inp) ++ (a ': Drop ('S n) inp)))
- type ConstraintPairN (n :: Peano) (inp :: [T]) = (RequireLongerOrSameLength inp n, TypeErrorUnless (n >= ToPeano 2) ('Text "'PAIR n' expects n \8805 2"))
- type PairN (n :: Peano) (s :: [T]) = RightComb (Take n s) ': Drop n s
- type family RightComb (s :: [T]) :: T where ...
- type ConstraintUnpairN (n :: Peano) (pair :: T) = (TypeErrorUnless (n >= ToPeano 2) ('Text "'UNPAIR n' expects n \8805 2"), TypeErrorUnless (CombedPairLeafCountIsAtLeast n pair) (If (IsPair pair) ((((('Text "'UNPAIR " :<>: 'ShowType (FromPeano n)) :<>: 'Text "' expects a right-combed pair with at least ") :<>: 'ShowType (FromPeano n)) :<>: 'Text " elements at the top of the stack,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairLeafCount pair))) :<>: 'Text " elements.")) ('Text "Expected a pair at the top of the stack, but found: " :<>: 'ShowType pair)))
- type family UnpairN (n :: Peano) (s :: T) :: [T] where ...
- type ConstraintGetN (ix :: Peano) (pair :: T) = TypeErrorUnless (CombedPairNodeIndexIsValid ix pair) (If (IsPair pair) ((((('Text "'GET " :<>: 'ShowType (FromPeano ix)) :<>: 'Text "' expects a right-combed pair with at least ") :<>: 'ShowType (FromPeano ix + 1)) :<>: 'Text " nodes at the top of the stack,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairNodeCount pair))) :<>: 'Text " nodes.")) ('Text "Expected a pair at the top of the stack, but found: " :<>: 'ShowType pair))
- type family GetN (ix :: Peano) (pair :: T) :: T where ...
- type ConstraintUpdateN (ix :: Peano) (pair :: T) = TypeErrorUnless (CombedPairNodeIndexIsValid ix pair) (If (IsPair pair) ((((('Text "'UPDATE " :<>: 'ShowType (FromPeano ix)) :<>: 'Text "' expects the 2nd element of the stack to be a right-combed pair with at least ") :<>: 'ShowType (FromPeano ix + 1)) :<>: 'Text " nodes,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairNodeCount pair))) :<>: 'Text " nodes.")) ('Text "Expected the 2nd element of the stack to be a pair, but found: " :<>: 'ShowType pair))
- type family UpdateN (ix :: Peano) (val :: T) (pair :: T) :: T where ...
Documentation
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 |
FrameInstr :: forall a b s. (KnownList a, KnownList b) => Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s) | Execute given instruction on truncated stack. This can wrap only instructions with at least one non-failing execution branch. Morley has no such instruction, it is used solely in eDSLs.
This instruction is sound because for all Michelson instructions
the following property holds: if some code accepts stack |
Seq :: Instr a b -> Instr b c -> Instr a c | |
Nop :: Instr s s | Nop operation. Missing in Michelson spec, added to parse construction like `IF {} { SWAP; DROP; }`. |
Ext :: ExtInstr s -> Instr s s | |
Nested :: Instr inp out -> Instr inp out | Nested wrapper is going to wrap a sequence of instructions with { }. It is crucial because serialisation of a contract depends on precise structure of its code. |
DocGroup :: DocGrouping -> Instr inp out -> Instr inp out | Places documentation generated for given instruction under some group.
This is not part of |
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 :: (SingI e, Comparable e) => Anns '[TypeAnn, VarAnn, Notes e] -> Instr s ('TSet e ': s) | |
AnnEMPTY_MAP :: (SingI a, SingI b, Comparable a) => Anns '[TypeAnn, VarAnn, Notes a, Notes b] -> Instr s ('TMap a b ': s) | |
AnnEMPTY_BIG_MAP :: (SingI a, SingI b, Comparable a, HasNoBigMap 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] -> Value' Instr ('TLambda i 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 :: UnaryArithOp Not n => AnnVar -> Instr (n ': s) (UnaryArithRes Not n ': s) | |
AnnCOMPARE :: (Comparable n, SingI 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) | |
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 :: Comparable a => AnnVar -> Instr (a ': ('TNat ': s)) ('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) |
pattern CAR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) ('TPair a b) s, out ~ '(:) a s) => 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 DUP :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) a ('(:) a s), DupableScope a) => 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 PUSH :: forall {inp} {out}. () => forall (t :: T) (s :: [T]). (inp ~ s, out ~ '(:) t s, ConstantScope t) => Value' Instr t -> Instr inp out | |
pattern SOME :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) ('TOption a) s) => 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 UNIT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TUnit 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 UNPAIR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) ('TPair a b) s, out ~ '(:) a ('(:) b s)) => 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 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 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 NIL :: forall {inp} {out}. () => forall (p :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TList p) s, SingI p) => 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 SIZE :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) c s, out ~ '(:) 'TNat s, SizeOp c) => Instr inp out | |
pattern EMPTY_SET :: forall {inp} {out}. () => forall (e :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TSet e) s, SingI e, Comparable e) => Instr inp out | |
pattern EMPTY_MAP :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TMap a b) s, SingI a, SingI b, Comparable a) => Instr inp out | |
pattern EMPTY_BIG_MAP :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TBigMap a b) s, SingI a, SingI b, Comparable a, HasNoBigMap b) => 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 MEM :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) (MemOpKey c) ('(:) c s), out ~ '(:) 'TBool s, MemOp c) => 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 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 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 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 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 LAMBDA :: forall {inp} {out}. () => forall (i :: T) (o :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TLambda i o) s, SingI i, SingI o) => Value' Instr ('TLambda i o) -> 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 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 CAST :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) a s, SingI a) => Instr inp out | |
pattern RENAME :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) a s) => 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 UNPACK :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) ('TOption a) s, UnpackedValScope a, SingI a) => 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 CONCAT' :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) ('TList c) s, out ~ '(:) c s, ConcatOp c) => 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 ISNAT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TInt s, out ~ '(:) ('TOption 'TNat) s) => 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 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 SUB_MUTEZ :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TMutez ('(:) 'TMutez s), out ~ '(:) ('TOption 'TMutez) s) => 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 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 ABS :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Abs n) s, UnaryArithOp Abs n) => 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 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 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 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 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 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 NOT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Not n) s, UnaryArithOp Not n) => Instr inp out | |
pattern COMPARE :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n ('(:) n s), out ~ '(:) 'TInt s, Comparable n, SingI n) => Instr inp out | |
pattern EQ :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Eq' n) s, UnaryArithOp Eq' n) => Instr inp out | |
pattern NEQ :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Neq n) s, UnaryArithOp Neq n) => Instr inp out | |
pattern LT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Lt n) s, UnaryArithOp Lt n) => Instr inp out | |
pattern GT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Gt n) s, UnaryArithOp Gt n) => 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 GE :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Ge n) s, UnaryArithOp Ge n) => 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 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 SELF :: forall {inp} {out}. () => forall (arg :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TContract arg) s, ParameterScope arg, IsNotInView) => SomeEntrypointCallT arg -> 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 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 SET_DELEGATE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) ('TOption 'TKeyHash) s, out ~ '(:) 'TOperation s, IsNotInView) => 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 IMPLICIT_ACCOUNT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKeyHash s, out ~ '(:) ('TContract 'TUnit) s) => Instr inp out | |
pattern NOW :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TTimestamp s) => Instr inp out | |
pattern AMOUNT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TMutez s) => Instr inp out | |
pattern BALANCE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TMutez s) => Instr inp out | |
pattern VOTING_POWER :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKeyHash s, out ~ '(:) 'TNat s) => Instr inp out | |
pattern TOTAL_VOTING_POWER :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TNat 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 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 BLAKE2B :: 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 KECCAK :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out | |
pattern HASH_KEY :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKey s, out ~ '(:) 'TKeyHash 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 SOURCE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TAddress s) => Instr inp out | |
pattern SENDER :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TAddress 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 CHAIN_ID :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TChainId s) => Instr inp out | |
pattern LEVEL :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TNat s) => Instr inp out | |
pattern SELF_ADDRESS :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TAddress s) => Instr inp out | |
pattern TICKET :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a ('(:) 'TNat s), out ~ '(:) ('TTicket a) s, Comparable a) => 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 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 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 OPEN_CHEST :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TChestKey ('(:) 'TChest ('(:) 'TNat s)), out ~ '(:) ('TOr 'TBytes 'TBool) 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 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 MIN_BLOCK_TIME :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TNat s) => Instr inp out |
Instances
castInstr :: forall inp1 out1 inp2 out2. (SingI inp1, SingI out1, SingI inp2, SingI out2) => Instr inp1 out1 -> Maybe (Instr inp2 out2) Source #
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
TEST_ASSERT (TestAssert s) | |
PRINT (PrintComment s) | |
DOC_ITEM SomeDocItem | |
COMMENT_ITEM CommentType | |
STACKTYPE StackTypePattern |
Instances
data CommentType Source #
FunctionStarts Text | |
FunctionEnds Text | |
StatementStarts Text | |
StatementEnds Text | |
JustComment Text | |
StackTypeComment (Maybe [T]) |
|
Instances
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. |
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.
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 # |
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) -> ... }
type ConstraintDUPN n inp out a = ConstraintDUPN' T n inp out a Source #
type ConstraintDUPN' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (RequireLongerOrSameLength inp n, (n > 'Z) ~ 'True, inp ~ (Take (Decrement n) inp ++ (a ': Drop n inp)), out ~ (a ': inp)) Source #
Constraint that is used in DUPN, we want to share it with typechecking code and eDSL code.
type ConstraintDIPN n inp out s s' = ConstraintDIPN' T n inp out s s' Source #
type ConstraintDIPN' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (s :: [kind]) (s' :: [kind]) = (RequireLongerOrSameLength inp n, (Take n inp ++ s) ~ inp, (Take n inp ++ s') ~ out) Source #
Constraint that is used in DIPN, we want to share it with typechecking code and eDSL code.
type ConstraintDIG n inp out a = ConstraintDIG' T n inp out a Source #
type ConstraintDIG' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (KnownList inp, RequireLongerThan inp n, inp ~ (Take n inp ++ (a ': Drop ('S n) inp)), out ~ (a ': (Take n inp ++ Drop ('S n) inp))) Source #
Constraint that is used in DIG, we want to share it with typechecking code and eDSL code.
type ConstraintDUG n inp out a = ConstraintDUG' T n inp out a Source #
type ConstraintDUG' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (RequireLongerThan out n, inp ~ (a ': Drop ('S 'Z) inp), out ~ (Take n (Drop ('S 'Z) inp) ++ (a ': Drop ('S n) inp))) Source #
Constraint that is used in DUG, we want to share it with typechecking code and eDSL code.
type ConstraintPairN (n :: Peano) (inp :: [T]) = (RequireLongerOrSameLength inp n, TypeErrorUnless (n >= ToPeano 2) ('Text "'PAIR n' expects n \8805 2")) Source #
type family RightComb (s :: [T]) :: T where ... Source #
Folds a stack into a right-combed pair.
RightComb '[ 'TInt, 'TString, 'TUnit ] ~ 'TPair 'TInt ('TPair 'TString 'TUnit)
type ConstraintUnpairN (n :: Peano) (pair :: T) = (TypeErrorUnless (n >= ToPeano 2) ('Text "'UNPAIR n' expects n \8805 2"), TypeErrorUnless (CombedPairLeafCountIsAtLeast n pair) (If (IsPair pair) ((((('Text "'UNPAIR " :<>: 'ShowType (FromPeano n)) :<>: 'Text "' expects a right-combed pair with at least ") :<>: 'ShowType (FromPeano n)) :<>: 'Text " elements at the top of the stack,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairLeafCount pair))) :<>: 'Text " elements.")) ('Text "Expected a pair at the top of the stack, but found: " :<>: 'ShowType pair))) Source #
type family UnpairN (n :: Peano) (s :: T) :: [T] where ... Source #
Splits a right-combed pair into n
elements.
UnpairN (ToPeano 3) ('TPair 'TInt ('TPair 'TString 'TUnit)) ~ '[ 'TInt, 'TString, 'TUnit]
UnpairN (ToPeano 3) ('TPair 'TInt ('TPair 'TString ('TPair 'TUnit 'TInt))) ~ '[ 'TInt, 'TString, 'TPair 'TUnit 'TInt]
type ConstraintGetN (ix :: Peano) (pair :: T) = TypeErrorUnless (CombedPairNodeIndexIsValid ix pair) (If (IsPair pair) ((((('Text "'GET " :<>: 'ShowType (FromPeano ix)) :<>: 'Text "' expects a right-combed pair with at least ") :<>: 'ShowType (FromPeano ix + 1)) :<>: 'Text " nodes at the top of the stack,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairNodeCount pair))) :<>: 'Text " nodes.")) ('Text "Expected a pair at the top of the stack, but found: " :<>: 'ShowType pair)) Source #
type family GetN (ix :: Peano) (pair :: T) :: T where ... Source #
Get the node at index ix
of a right-combed pair.
type ConstraintUpdateN (ix :: Peano) (pair :: T) = TypeErrorUnless (CombedPairNodeIndexIsValid ix pair) (If (IsPair pair) ((((('Text "'UPDATE " :<>: 'ShowType (FromPeano ix)) :<>: 'Text "' expects the 2nd element of the stack to be a right-combed pair with at least ") :<>: 'ShowType (FromPeano ix + 1)) :<>: 'Text " nodes,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairNodeCount pair))) :<>: 'Text " nodes.")) ('Text "Expected the 2nd element of the stack to be a pair, but found: " :<>: 'ShowType pair)) Source #