morley-1.20.0: Developer tools for the Michelson Language
Safe HaskellSafe-Inferred
LanguageHaskell2010

Morley.Michelson.Typed.ClassifiedInstr.Internal.MainImpl

Description

Main implementation of the classifier machinery.

Synopsis

Documentation

data ClassifiedInstr :: InstrClass -> [T] -> [T] -> Type where Source #

Classified instruction. Has the same shape as typed Instr, but its type also carries information about the classes of the constructor.

Constructors

C_WithLoc :: forall (inp :: [T]) (out :: [T]). ErrorSrcPos -> (Instr inp out) -> ClassifiedInstr ('InstrClass 'OneChild 'FailingNormal 'Phantom 'DoesNotHaveAnns) inp out 
C_Meta :: forall (inp :: [T]) (out :: [T]). SomeMeta -> (Instr inp out) -> ClassifiedInstr ('InstrClass 'OneChild 'FailingNormal 'Phantom 'DoesNotHaveAnns) inp out 
C_Seq :: forall (inp :: [T]) (b :: [T]) (out :: [T]). (Instr inp b) -> (Instr b out) -> ClassifiedInstr ('InstrClass 'TwoChildren 'FailingNormal 'Structural 'DoesNotHaveAnns) inp out 
C_Nop :: forall (inp :: [T]). ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'Additional 'DoesNotHaveAnns) inp inp 
C_Ext :: forall (inp :: [T]). (ExtInstr inp) -> ClassifiedInstr ('InstrClass 'MayHaveChildren 'FailingNormal 'Additional 'DoesNotHaveAnns) inp inp 
C_Nested :: forall (inp :: [T]) (out :: [T]). (Instr inp out) -> ClassifiedInstr ('InstrClass 'OneChild 'FailingNormal 'Structural 'DoesNotHaveAnns) inp out 
C_DocGroup :: forall (inp :: [T]) (out :: [T]). DocGrouping -> (Instr inp out) -> ClassifiedInstr ('InstrClass 'OneChild 'FailingNormal 'Phantom 'DoesNotHaveAnns) inp out 
C_AnnCAR :: forall (a :: T) (b :: T) (s :: [T]). (Anns ('(:) VarAnn ('(:) FieldAnn ('[] :: [Type])))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) ('TPair a b) s) ('(:) a s) 
C_AnnCDR :: forall (a :: T) (b :: T) (s :: [T]). (Anns ('(:) VarAnn ('(:) FieldAnn ('[] :: [Type])))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) ('TPair a b) s) ('(:) b s) 
C_DROP :: forall (a :: T) (out :: [T]). ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesNotHaveAnns) ('(:) a out) out 
C_DROPN :: forall (n :: Peano) (inp :: [T]). RequireLongerOrSameLength inp n => (PeanoNatural n) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesNotHaveAnns) inp (Drop n inp) 
C_AnnDUP :: forall (a :: T) (s :: [T]). DupableScope a => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) a s) ('(:) a ('(:) a s)) 
C_AnnDUPN :: forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T). (ConstraintDUPN n inp out a, DupableScope a) => AnnVar -> (PeanoNatural n) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp out 
C_SWAP :: forall (a :: T) (b :: T) (s :: [T]). ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesNotHaveAnns) ('(:) a ('(:) b s)) ('(:) b ('(:) a s)) 
C_DIG :: forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T). ConstraintDIG n inp out a => (PeanoNatural n) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesNotHaveAnns) inp out 
C_DUG :: forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T). ConstraintDUG n inp out a => (PeanoNatural n) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesNotHaveAnns) inp out 
C_AnnPUSH :: forall (t :: T) (inp :: [T]). ConstantScope t => (Anns ('(:) VarAnn ('(:) (Notes t) ('[] :: [Type])))) -> (Value' Instr t) -> ClassifiedInstr ('InstrClass 'HasIndirectChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) t inp) 
C_AnnSOME :: forall (a :: T) (s :: [T]). (Anns ('(:) TypeAnn ('(:) VarAnn ('[] :: [Type])))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) a s) ('(:) ('TOption a) s) 
C_AnnNONE :: forall (a :: T) (inp :: [T]). SingI a => (Anns ('(:) TypeAnn ('(:) VarAnn ('(:) (Notes a) ('[] :: [Type]))))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) ('TOption a) inp) 
C_AnnUNIT :: forall (inp :: [T]). (Anns ('(:) TypeAnn ('(:) VarAnn ('[] :: [Type])))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) 'TUnit inp) 
C_IF_NONE :: forall (s :: [T]) (out :: [T]) (a :: T). (Instr s out) -> (Instr ('(:) a s) out) -> ClassifiedInstr ('InstrClass 'TwoChildren 'FailingNormal 'FromMichelson 'DoesNotHaveAnns) ('(:) ('TOption a) s) out 
C_AnnPAIR :: forall (a :: T) (b :: T) (s :: [T]). (Anns ('(:) TypeAnn ('(:) VarAnn ('(:) FieldAnn ('(:) FieldAnn ('[] :: [Type])))))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) a ('(:) b s)) ('(:) ('TPair a b) s) 
C_AnnUNPAIR :: forall (a :: T) (b :: T) (s :: [T]). (Anns ('(:) VarAnn ('(:) VarAnn ('(:) FieldAnn ('(:) FieldAnn ('[] :: [Type])))))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) ('TPair a b) s) ('(:) a ('(:) b s)) 
C_AnnPAIRN :: forall (n :: Peano) (inp :: [T]). ConstraintPairN n inp => AnnVar -> (PeanoNatural n) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) (RightComb (LazyTake n inp)) (Drop n inp)) 
C_UNPAIRN :: forall (n :: Peano) (pair :: T) (s :: [T]). ConstraintUnpairN n pair => (PeanoNatural n) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesNotHaveAnns) ('(:) pair s) ((++) (UnpairN n pair) s) 
C_AnnLEFT :: forall (b :: T) (a :: T) (s :: [T]). SingI b => (Anns ('(:) TypeAnn ('(:) VarAnn ('(:) FieldAnn ('(:) FieldAnn ('(:) (Notes b) ('[] :: [Type]))))))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) a s) ('(:) ('TOr a b) s) 
C_AnnRIGHT :: forall (a :: T) (b :: T) (s :: [T]). SingI a => (Anns ('(:) TypeAnn ('(:) VarAnn ('(:) FieldAnn ('(:) FieldAnn ('(:) (Notes a) ('[] :: [Type]))))))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) b s) ('(:) ('TOr a b) s) 
C_IF_LEFT :: forall (a :: T) (s :: [T]) (out :: [T]) (b :: T). (Instr ('(:) a s) out) -> (Instr ('(:) b s) out) -> ClassifiedInstr ('InstrClass 'TwoChildren 'FailingNormal 'FromMichelson 'DoesNotHaveAnns) ('(:) ('TOr a b) s) out 
C_AnnNIL :: forall (p :: T) (inp :: [T]). SingI p => (Anns ('(:) TypeAnn ('(:) VarAnn ('(:) (Notes p) ('[] :: [Type]))))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) ('TList p) inp) 
C_AnnCONS :: forall (a :: T) (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) a ('(:) ('TList a) s)) ('(:) ('TList a) s) 
C_IF_CONS :: forall (a :: T) (s :: [T]) (out :: [T]). (Instr ('(:) a ('(:) ('TList a) s)) out) -> (Instr s out) -> ClassifiedInstr ('InstrClass 'TwoChildren 'FailingNormal 'FromMichelson 'DoesNotHaveAnns) ('(:) ('TList a) s) out 
C_AnnSIZE :: forall (c :: T) (s :: [T]). SizeOp c => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) c s) ('(:) 'TNat s) 
C_AnnEMPTY_SET :: forall (e :: T) (inp :: [T]). Comparable e => (Anns ('(:) TypeAnn ('(:) VarAnn ('(:) (Notes e) ('[] :: [Type]))))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) ('TSet e) inp) 
C_AnnEMPTY_MAP :: forall (b :: T) (a :: T) (inp :: [T]). (SingI b, Comparable a) => (Anns ('(:) TypeAnn ('(:) VarAnn ('(:) (Notes a) ('(:) (Notes b) ('[] :: [Type])))))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) ('TMap a b) inp) 
C_AnnEMPTY_BIG_MAP :: forall (b :: T) (a :: T) (inp :: [T]). (SingI b, Comparable a, ForbidBigMap b) => (Anns ('(:) TypeAnn ('(:) VarAnn ('(:) (Notes a) ('(:) (Notes b) ('[] :: [Type])))))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) ('TBigMap a b) inp) 
C_AnnMAP :: forall (c :: T) (b :: T) (s :: [T]). (MapOp c, SingI b) => AnnVar -> (Instr ('(:) (MapOpInp c) s) ('(:) b s)) -> ClassifiedInstr ('InstrClass 'OneChild 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) c s) ('(:) (MapOpRes c b) s) 
C_ITER :: forall (c :: T) (out :: [T]). IterOp c => (Instr ('(:) (IterOpEl c) out) out) -> ClassifiedInstr ('InstrClass 'OneChild 'FailingNormal 'FromMichelson 'DoesNotHaveAnns) ('(:) c out) out 
C_AnnMEM :: forall (c :: T) (s :: [T]). MemOp c => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) (MemOpKey c) ('(:) c s)) ('(:) 'TBool s) 
C_AnnGET :: forall (c :: T) (s :: [T]). (GetOp c, SingI (GetOpVal c)) => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) (GetOpKey c) ('(:) c s)) ('(:) ('TOption (GetOpVal c)) s) 
C_AnnGETN :: forall (ix :: Peano) (pair :: T) (s :: [T]). ConstraintGetN ix pair => AnnVar -> (PeanoNatural ix) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) pair s) ('(:) (GetN ix pair) s) 
C_AnnUPDATE :: forall (c :: T) (s :: [T]). UpdOp c => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) (UpdOpKey c) ('(:) (UpdOpParams c) ('(:) c s))) ('(:) c s) 
C_AnnUPDATEN :: forall (ix :: Peano) (val :: T) (pair :: T) (s :: [T]). ConstraintUpdateN ix pair => AnnVar -> (PeanoNatural ix) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) val ('(:) pair s)) ('(:) (UpdateN ix val pair) s) 
C_AnnGET_AND_UPDATE :: forall (c :: T) (s :: [T]). (GetOp c, UpdOp c, SingI (GetOpVal c), (~) (UpdOpKey c) (GetOpKey c)) => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) (UpdOpKey c) ('(:) (UpdOpParams c) ('(:) c s))) ('(:) ('TOption (GetOpVal c)) ('(:) c s)) 
C_IF :: forall (s :: [T]) (out :: [T]). (Instr s out) -> (Instr s out) -> ClassifiedInstr ('InstrClass 'TwoChildren 'FailingNormal 'FromMichelson 'DoesNotHaveAnns) ('(:) 'TBool s) out 
C_LOOP :: forall (out :: [T]). (Instr out ('(:) 'TBool out)) -> ClassifiedInstr ('InstrClass 'OneChild 'FailingNormal 'FromMichelson 'DoesNotHaveAnns) ('(:) 'TBool out) out 
C_LOOP_LEFT :: forall (a :: T) (s :: [T]) (b :: T). (Instr ('(:) a s) ('(:) ('TOr a b) s)) -> ClassifiedInstr ('InstrClass 'OneChild 'FailingNormal 'FromMichelson 'DoesNotHaveAnns) ('(:) ('TOr a b) s) ('(:) b s) 
C_AnnLAMBDA :: forall (i :: T) (o :: T) (inp :: [T]). (SingI i, SingI o) => (Anns ('(:) VarAnn ('(:) (Notes i) ('(:) (Notes o) ('[] :: [Type]))))) -> (RemFail Instr ('(:) i ('[] :: [T])) ('(:) o ('[] :: [T]))) -> ClassifiedInstr ('InstrClass 'HasIndirectChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) ('TLambda i o) inp) 
C_AnnLAMBDA_REC :: forall (i :: T) (o :: T) (inp :: [T]). (SingI i, SingI o) => (Anns ('(:) VarAnn ('(:) (Notes i) ('(:) (Notes o) ('[] :: [Type]))))) -> (RemFail Instr ('(:) i ('(:) ('TLambda i o) ('[] :: [T]))) ('(:) o ('[] :: [T]))) -> ClassifiedInstr ('InstrClass 'HasIndirectChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) ('TLambda i o) inp) 
C_AnnEXEC :: forall (t1 :: T) (t2 :: T) (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) t1 ('(:) ('TLambda t1 t2) s)) ('(:) t2 s) 
C_AnnAPPLY :: forall (a :: T) (b :: T) (c :: T) (s :: [T]). (ConstantScope a, SingI b) => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) a ('(:) ('TLambda ('TPair a b) c) s)) ('(:) ('TLambda b c) s) 
C_DIP :: forall (a :: [T]) (c :: [T]) (b :: T). (Instr a c) -> ClassifiedInstr ('InstrClass 'OneChild 'FailingNormal 'FromMichelson 'DoesNotHaveAnns) ('(:) b a) ('(:) b c) 
C_DIPN :: forall (n :: Peano) (inp :: [T]) (out :: [T]) (s :: [T]) (s' :: [T]). ConstraintDIPN n inp out s s' => (PeanoNatural n) -> (Instr s s') -> ClassifiedInstr ('InstrClass 'OneChild 'FailingNormal 'FromMichelson 'DoesNotHaveAnns) inp out 
C_FAILWITH :: forall (a :: T) (s :: [T]) (out :: [T]). (SingI a, ConstantScope a) => ClassifiedInstr ('InstrClass 'NoChildren 'AlwaysFailing 'FromMichelson 'DoesNotHaveAnns) ('(:) a s) out 
C_AnnCAST :: forall (a :: T) (s :: [T]). SingI a => (Anns ('(:) VarAnn ('(:) (Notes a) ('[] :: [Type])))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) a s) ('(:) a s) 
C_AnnRENAME :: forall (a :: T) (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) a s) ('(:) a s) 
C_AnnPACK :: forall (a :: T) (s :: [T]). PackedValScope a => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) a s) ('(:) 'TBytes s) 
C_AnnUNPACK :: forall (a :: T) (s :: [T]). (UnpackedValScope a, SingI a) => (Anns ('(:) TypeAnn ('(:) VarAnn ('(:) (Notes a) ('[] :: [Type]))))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TBytes s) ('(:) ('TOption a) s) 
C_AnnCONCAT :: forall (c :: T) (s :: [T]). ConcatOp c => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) c ('(:) c s)) ('(:) c s) 
C_AnnCONCAT' :: forall (c :: T) (s :: [T]). ConcatOp c => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) ('TList c) s) ('(:) c s) 
C_AnnSLICE :: forall (c :: T) (s :: [T]). (SliceOp c, SingI c) => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TNat ('(:) 'TNat ('(:) c s))) ('(:) ('TOption c) s) 
C_AnnISNAT :: forall (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TInt s) ('(:) ('TOption 'TNat) s) 
C_AnnADD :: forall (n :: T) (m :: T) (s :: [T]). ArithOp Add n m => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n ('(:) m s)) ('(:) (ArithRes Add n m) s) 
C_AnnSUB :: forall (n :: T) (m :: T) (s :: [T]). ArithOp Sub n m => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n ('(:) m s)) ('(:) (ArithRes Sub n m) s) 
C_AnnSUB_MUTEZ :: forall (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TMutez ('(:) 'TMutez s)) ('(:) ('TOption 'TMutez) s) 
C_AnnMUL :: forall (n :: T) (m :: T) (s :: [T]). ArithOp Mul n m => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n ('(:) m s)) ('(:) (ArithRes Mul n m) s) 
C_AnnEDIV :: forall (n :: T) (m :: T) (s :: [T]). ArithOp EDiv n m => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n ('(:) m s)) ('(:) (ArithRes EDiv n m) s) 
C_AnnABS :: forall (n :: T) (s :: [T]). UnaryArithOp Abs n => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n s) ('(:) (UnaryArithRes Abs n) s) 
C_AnnNEG :: forall (n :: T) (s :: [T]). UnaryArithOp Neg n => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n s) ('(:) (UnaryArithRes Neg n) s) 
C_AnnLSL :: forall (n :: T) (m :: T) (s :: [T]). ArithOp Lsl n m => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n ('(:) m s)) ('(:) (ArithRes Lsl n m) s) 
C_AnnLSR :: forall (n :: T) (m :: T) (s :: [T]). ArithOp Lsr n m => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n ('(:) m s)) ('(:) (ArithRes Lsr n m) s) 
C_AnnOR :: forall (n :: T) (m :: T) (s :: [T]). ArithOp Or n m => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n ('(:) m s)) ('(:) (ArithRes Or n m) s) 
C_AnnAND :: forall (n :: T) (m :: T) (s :: [T]). ArithOp And n m => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n ('(:) m s)) ('(:) (ArithRes And n m) s) 
C_AnnXOR :: forall (n :: T) (m :: T) (s :: [T]). ArithOp Xor n m => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n ('(:) m s)) ('(:) (ArithRes Xor n m) s) 
C_AnnNOT :: forall (n :: T) (s :: [T]). (SingI n, UnaryArithOp Not n) => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n s) ('(:) (UnaryArithRes Not n) s) 
C_AnnCOMPARE :: forall (n :: T) (s :: [T]). Comparable n => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n ('(:) n s)) ('(:) 'TInt s) 
C_AnnEQ :: forall (n :: T) (s :: [T]). UnaryArithOp Eq' n => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n s) ('(:) (UnaryArithRes Eq' n) s) 
C_AnnNEQ :: forall (n :: T) (s :: [T]). UnaryArithOp Neq n => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n s) ('(:) (UnaryArithRes Neq n) s) 
C_AnnLT :: forall (n :: T) (s :: [T]). UnaryArithOp Lt n => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n s) ('(:) (UnaryArithRes Lt n) s) 
C_AnnGT :: forall (n :: T) (s :: [T]). UnaryArithOp Gt n => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n s) ('(:) (UnaryArithRes Gt n) s) 
C_AnnLE :: forall (n :: T) (s :: [T]). UnaryArithOp Le n => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n s) ('(:) (UnaryArithRes Le n) s) 
C_AnnGE :: forall (n :: T) (s :: [T]). UnaryArithOp Ge n => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n s) ('(:) (UnaryArithRes Ge n) s) 
C_AnnINT :: forall (n :: T) (s :: [T]). ToIntArithOp n => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n s) ('(:) 'TInt s) 
C_AnnBYTES :: forall (n :: T) (s :: [T]). ToBytesArithOp n => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) n s) ('(:) 'TBytes s) 
C_AnnNAT :: forall (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TBytes s) ('(:) 'TNat s) 
C_AnnVIEW :: forall (arg :: T) (ret :: T) (s :: [T]). (SingI arg, ViewableScope ret) => (Anns ('(:) VarAnn ('(:) (Notes ret) ('[] :: [Type])))) -> ViewName -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) arg ('(:) 'TAddress s)) ('(:) ('TOption ret) s) 
C_AnnSELF :: forall (arg :: T) (inp :: [T]). (ParameterScope arg, IsNotInView) => AnnVar -> (SomeEntrypointCallT arg) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) ('TContract arg) inp) 
C_AnnCONTRACT :: forall (p :: T) (s :: [T]). ParameterScope p => (Anns ('(:) VarAnn ('(:) (Notes p) ('[] :: [Type])))) -> EpName -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TAddress s) ('(:) ('TOption ('TContract p)) s) 
C_AnnTRANSFER_TOKENS :: forall (p :: T) (s :: [T]). (ParameterScope p, IsNotInView) => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) p ('(:) 'TMutez ('(:) ('TContract p) s))) ('(:) 'TOperation s) 
C_AnnSET_DELEGATE :: forall (s :: [T]). IsNotInView => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) ('TOption 'TKeyHash) s) ('(:) 'TOperation s) 
C_AnnCREATE_CONTRACT :: forall (p :: T) (g :: T) (s :: [T]). (ParameterScope p, StorageScope g, IsNotInView) => (Anns ('(:) VarAnn ('(:) VarAnn ('[] :: [Type])))) -> (Contract' Instr p g) -> ClassifiedInstr ('InstrClass 'HasIndirectChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) ('TOption 'TKeyHash) ('(:) 'TMutez ('(:) g s))) ('(:) 'TOperation ('(:) 'TAddress s)) 
C_AnnIMPLICIT_ACCOUNT :: forall (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TKeyHash s) ('(:) ('TContract 'TUnit) s) 
C_AnnNOW :: forall (inp :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) 'TTimestamp inp) 
C_AnnAMOUNT :: forall (inp :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) 'TMutez inp) 
C_AnnBALANCE :: forall (inp :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) 'TMutez inp) 
C_AnnVOTING_POWER :: forall (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TKeyHash s) ('(:) 'TNat s) 
C_AnnTOTAL_VOTING_POWER :: forall (inp :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) 'TNat inp) 
C_AnnCHECK_SIGNATURE :: forall (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TKey ('(:) 'TSignature ('(:) 'TBytes s))) ('(:) 'TBool s) 
C_AnnSHA256 :: forall (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TBytes s) ('(:) 'TBytes s) 
C_AnnSHA512 :: forall (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TBytes s) ('(:) 'TBytes s) 
C_AnnBLAKE2B :: forall (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TBytes s) ('(:) 'TBytes s) 
C_AnnSHA3 :: forall (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TBytes s) ('(:) 'TBytes s) 
C_AnnKECCAK :: forall (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TBytes s) ('(:) 'TBytes s) 
C_AnnHASH_KEY :: forall (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TKey s) ('(:) 'TKeyHash s) 
C_AnnPAIRING_CHECK :: forall (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) ('TList ('TPair 'TBls12381G1 'TBls12381G2)) s) ('(:) 'TBool s) 
C_AnnSOURCE :: forall (inp :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) 'TAddress inp) 
C_AnnSENDER :: forall (inp :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) 'TAddress inp) 
C_AnnADDRESS :: forall (a :: T) (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) ('TContract a) s) ('(:) 'TAddress s) 
C_AnnCHAIN_ID :: forall (inp :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) 'TChainId inp) 
C_AnnLEVEL :: forall (inp :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) 'TNat inp) 
C_AnnSELF_ADDRESS :: forall (inp :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) 'TAddress inp) 
C_NEVER :: forall (s :: [T]) (out :: [T]). ClassifiedInstr ('InstrClass 'NoChildren 'AlwaysFailing 'FromMichelson 'DoesNotHaveAnns) ('(:) 'TNever s) out 
C_AnnTICKET_DEPRECATED :: forall (a :: T) (s :: [T]). Comparable a => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) a ('(:) 'TNat s)) ('(:) ('TTicket a) s) 
C_AnnTICKET :: forall (a :: T) (s :: [T]). Comparable a => AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) a ('(:) 'TNat s)) ('(:) ('TOption ('TTicket a)) s) 
C_AnnREAD_TICKET :: forall (a :: T) (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) ('TTicket a) s) ('(:) (RightComb ('(:) 'TAddress ('(:) a ('(:) 'TNat ('[] :: [T]))))) ('(:) ('TTicket a) s)) 
C_AnnSPLIT_TICKET :: forall (a :: T) (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) ('TTicket a) ('(:) ('TPair 'TNat 'TNat) s)) ('(:) ('TOption ('TPair ('TTicket a) ('TTicket a))) s) 
C_AnnJOIN_TICKETS :: forall (a :: T) (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) ('TPair ('TTicket a) ('TTicket a)) s) ('(:) ('TOption ('TTicket a)) s) 
C_AnnOPEN_CHEST :: forall (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) 'TChestKey ('(:) 'TChest ('(:) 'TNat s))) ('(:) ('TOr 'TBytes 'TBool) s) 
C_AnnSAPLING_EMPTY_STATE :: forall (n :: Peano) (inp :: [T]). AnnVar -> (Sing n) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) ('TSaplingState n) inp) 
C_AnnSAPLING_VERIFY_UPDATE :: forall (n :: Peano) (s :: [T]). AnnVar -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) ('(:) ('TSaplingTransaction n) ('(:) ('TSaplingState n) s)) ('(:) ('TOption ('TPair 'TBytes ('TPair 'TInt ('TSaplingState n)))) s) 
C_AnnMIN_BLOCK_TIME :: forall (inp :: [T]). [AnyAnn] -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveNonStandardAnns) inp ('(:) 'TNat inp) 
C_AnnEMIT :: forall (t :: T) (s :: [T]). PackedValScope t => AnnVar -> FieldAnn -> (Maybe (Notes t)) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveNonStandardAnns) ('(:) t s) ('(:) 'TOperation s) 

Instances

Instances details
SingI cls => WithClassifiedInstr (ClassifiedInstr cls) Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.WithClassifiedInstr

Associated Types

type WCIConstraint (ClassifiedInstr cls) cls' Source #

Methods

withClassifiedInstr :: forall t (inp :: [T]) (out :: [T]) r. ClassifyInstr t => (forall (cls0 :: InstrClass). (SingI cls0, WCIConstraint (ClassifiedInstr cls) cls0) => Sing (GetClassified cls0) -> ClassifiedInstr cls0 inp out -> r) -> ClassifiedInstr cls inp out -> r Source #

type WCIConstraint (ClassifiedInstr cls) cls' Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.WithClassifiedInstr

type WCIConstraint (ClassifiedInstr cls) cls' = cls ~ cls'

data WellClassifiedInstr inp out Source #

Existential for ClassifiedInstr hiding the class. Use classifyInstr to get it.

Constructors

forall cls.SingI cls => WCI 

Fields

classifyInstr :: Instr inp out -> WellClassifiedInstr inp out Source #

Convert typed Instr to WellClassifiedInstr.

getInstrClass :: forall t c inp out. (SingI c, ClassifyInstr t) => ClassifiedInstr c inp out -> Sing (GetClassified c :: t) Source #

Given a well-classified instruction, get a particular classification for it. The general use pattern is:

case classifyInstr i of
  WCI instr -> case getInstrClass instr of
    SMayHaveChildren -> case instr of
      C_Ext _ -> _
      -- ...
    -- ...

You should use withClassifiedInstr, as it provides a less verbose interface.