| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Morley.Michelson.Typed
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.
Constructors
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.
Methods
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 Methods 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(EqInt)
captures a dictionary that proves we have an:
instanceEqInt
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 Methods 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) | |