Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Main implementation of the classifier machinery.
Synopsis
- data ClassifiedInstr :: InstrClass -> [T] -> [T] -> Type where
- 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_FrameInstr :: forall (a :: [T]) (b :: [T]) (s :: [T]). KnownList a => (Proxy s) -> (Instr a b) -> ClassifiedInstr ('InstrClass 'OneChild 'FailingNormal 'Phantom 'DoesNotHaveAnns) ((++) a s) ((++) b s)
- 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]). (SingI e, Comparable e) => (Anns ('(:) TypeAnn ('(:) VarAnn ('(:) (Notes e) ('[] :: [Type]))))) -> ClassifiedInstr ('InstrClass 'NoChildren 'FailingNormal 'FromMichelson 'DoesHaveStandardAnns) inp ('(:) ('TSet e) inp)
- C_AnnEMPTY_MAP :: forall (a :: T) (b :: T) (inp :: [T]). (SingI a, 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 (a :: T) (b :: T) (inp :: [T]). (SingI a, SingI b, Comparable a, HasNoBigMap 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]). 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, SingI 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_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)
- classifyInstr :: Instr inp out -> WellClassifiedInstr inp out
- data WellClassifiedInstr inp out = forall cls.SingI cls => WCI {
- pickClassifiedInstr :: ClassifiedInstr cls inp out
- getInstrClass :: forall t c inp out. (SingI c, ClassifyInstr t) => ClassifiedInstr c inp out -> Sing (GetClassified c :: t)
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.
Instances
SingI cls => WithClassifiedInstr (ClassifiedInstr cls) Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.WithClassifiedInstr type WCIConstraint (ClassifiedInstr cls) cls' Source # 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 # | |
classifyInstr :: Instr inp out -> WellClassifiedInstr inp out Source #
Convert typed Instr
to WellClassifiedInstr
.
data WellClassifiedInstr inp out Source #
Existential for ClassifiedInstr
hiding the class. Use classifyInstr
to
get it.
forall cls.SingI cls => WCI | |
|
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:
caseclassifyInstr
i ofWCI
instr -> casegetInstrClass
instr ofSMayHaveChildren
-> case instr ofC_Ext
_ -> _ -- ... -- ...
You should use withClassifiedInstr
, as it provides a less verbose interface.