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

Morley.Michelson.Typed.ClassifiedInstr

Description

Machinery for typed instruction classification.

Synopsis

Documentation

withClassifiedInstr :: forall t inp out r. (WithClassifiedInstr instr, ClassifyInstr t) => (forall cls. (SingI cls, WCIConstraint instr cls) => Sing (GetClassified cls :: t) -> ClassifiedInstr cls inp out -> r) -> instr inp out -> r Source #

Perform a computation with a classified instruction.

Intended to be used with LambdaCase, e.g.

 isRealInstr :: T.Instr a b -> Bool
 isRealInstr = withClassifiedInstr \case
   SFromMichelson -> True
   SStructural -> False
   SAdditional -> \case
     C_Nop -> False
     C_Ext{} -> True
   SPhantom -> False

You can use withClassifiedInstr again to obtain a different classification:

 go = withClassifiedInstr \case
   SFailingNormal -> withClassifiedInstr \case
     SNoChildren -> _

If you need to reference the original instruction, consider using & for convenient pointful syntax:

 go i = i & withClassifiedInstr \case
   SFailingNormal -> withClassifiedInstr \case
     SNoChildren -> doStuffWith i

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_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) 

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'

Classifications

data NumChildren Source #

Number of children instructions a given instruction constructor has.

Constructors

MayHaveChildren

It is unknown at compile-time whether the instruction has children or not.

HasIndirectChildren

The instruction has children indirectly, as values.

NoChildren

The instruction has no children.

OneChild

The instruction has one child.

TwoChildren

The instruction has two children.

Instances

Instances details
Enum NumChildren Source # 
Instance details

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

Methods

succ :: NumChildren -> NumChildren #

pred :: NumChildren -> NumChildren #

toEnum :: Int -> NumChildren #

fromEnum :: NumChildren -> Int #

enumFrom :: NumChildren -> [NumChildren] #

enumFromThen :: NumChildren -> NumChildren -> [NumChildren] #

enumFromTo :: NumChildren -> NumChildren -> [NumChildren] #

enumFromThenTo :: NumChildren -> NumChildren -> NumChildren -> [NumChildren] #

Show NumChildren Source # 
Instance details

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

Methods

showsPrec :: Int -> NumChildren -> ShowS #

show :: NumChildren -> String #

showList :: [NumChildren] -> ShowS #

ClassifyInstr NumChildren Source # 
Instance details

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

Associated Types

type GetClassified c :: k Source #

Methods

getClassified :: forall (c :: InstrClass). SingInstrClass c -> Sing (GetClassified c) Source #

SingKind NumChildren Source # 
Instance details

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

Associated Types

type Demote NumChildren = (r :: Type) #

Methods

fromSing :: forall (a :: NumChildren). Sing a -> Demote NumChildren #

toSing :: Demote NumChildren -> SomeSing NumChildren #

SDecide NumChildren Source # 
Instance details

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

Methods

(%~) :: forall (a :: NumChildren) (b :: NumChildren). Sing a -> Sing b -> Decision (a :~: b) #

TestCoercion SingNumChildren Source # 
Instance details

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

Methods

testCoercion :: forall (a :: k) (b :: k). SingNumChildren a -> SingNumChildren b -> Maybe (Coercion a b) #

TestEquality SingNumChildren Source # 
Instance details

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

Methods

testEquality :: forall (a :: k) (b :: k). SingNumChildren a -> SingNumChildren b -> Maybe (a :~: b) #

SingI 'HasIndirectChildren Source # 
Instance details

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

Methods

sing :: Sing 'HasIndirectChildren #

SingI 'MayHaveChildren Source # 
Instance details

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

Methods

sing :: Sing 'MayHaveChildren #

SingI 'NoChildren Source # 
Instance details

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

Methods

sing :: Sing 'NoChildren #

SingI 'OneChild Source # 
Instance details

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

Methods

sing :: Sing 'OneChild #

SingI 'TwoChildren Source # 
Instance details

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

Methods

sing :: Sing 'TwoChildren #

SingI InstrClassSym0 Source # 
Instance details

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

Methods

sing :: Sing InstrClassSym0 #

SuppressUnusedWarnings InstrClassSym0 Source # 
Instance details

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

Methods

suppressUnusedWarnings :: () #

type Demote NumChildren Source # 
Instance details

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

type Demote NumChildren = NumChildren
type Sing Source # 
Instance details

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

type Sing = SingNumChildren
type Apply InstrClassSym0 (a6989586621679379732 :: NumChildren) Source # 
Instance details

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

type Apply InstrClassSym0 (a6989586621679379732 :: NumChildren) = InstrClassSym1 a6989586621679379732
type GetClassified ('InstrClass a _1 _2 _3) Source # 
Instance details

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

type GetClassified ('InstrClass a _1 _2 _3) = a

data FailureType Source #

Whether an instruction always fails. An example of always-failing instruction is NEVER.

Constructors

AlwaysFailing

Instruction always fails.

FailingNormal

Instruction might fail if inputs are incorrect, but will generally work.

Instances

Instances details
Enum FailureType Source # 
Instance details

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

Methods

succ :: FailureType -> FailureType #

pred :: FailureType -> FailureType #

toEnum :: Int -> FailureType #

fromEnum :: FailureType -> Int #

enumFrom :: FailureType -> [FailureType] #

enumFromThen :: FailureType -> FailureType -> [FailureType] #

enumFromTo :: FailureType -> FailureType -> [FailureType] #

enumFromThenTo :: FailureType -> FailureType -> FailureType -> [FailureType] #

Show FailureType Source # 
Instance details

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

Methods

showsPrec :: Int -> FailureType -> ShowS #

show :: FailureType -> String #

showList :: [FailureType] -> ShowS #

ClassifyInstr FailureType Source # 
Instance details

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

Associated Types

type GetClassified c :: k Source #

Methods

getClassified :: forall (c :: InstrClass). SingInstrClass c -> Sing (GetClassified c) Source #

SingKind FailureType Source # 
Instance details

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

Associated Types

type Demote FailureType = (r :: Type) #

Methods

fromSing :: forall (a :: FailureType). Sing a -> Demote FailureType #

toSing :: Demote FailureType -> SomeSing FailureType #

SDecide FailureType Source # 
Instance details

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

Methods

(%~) :: forall (a :: FailureType) (b :: FailureType). Sing a -> Sing b -> Decision (a :~: b) #

TestCoercion SingFailureType Source # 
Instance details

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

Methods

testCoercion :: forall (a :: k) (b :: k). SingFailureType a -> SingFailureType b -> Maybe (Coercion a b) #

TestEquality SingFailureType Source # 
Instance details

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

Methods

testEquality :: forall (a :: k) (b :: k). SingFailureType a -> SingFailureType b -> Maybe (a :~: b) #

SingI 'AlwaysFailing Source # 
Instance details

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

Methods

sing :: Sing 'AlwaysFailing #

SingI 'FailingNormal Source # 
Instance details

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

Methods

sing :: Sing 'FailingNormal #

SingI InstrClassSym0 Source # 
Instance details

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

Methods

sing :: Sing InstrClassSym0 #

SuppressUnusedWarnings InstrClassSym0 Source # 
Instance details

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

Methods

suppressUnusedWarnings :: () #

SingI d => SingI (InstrClassSym1 d :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) Source # 
Instance details

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

Methods

sing :: Sing (InstrClassSym1 d) #

SuppressUnusedWarnings (InstrClassSym1 a6989586621679379732 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) Source # 
Instance details

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

Methods

suppressUnusedWarnings :: () #

type Demote FailureType Source # 
Instance details

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

type Demote FailureType = FailureType
type Sing Source # 
Instance details

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

type Sing = SingFailureType
type Apply InstrClassSym0 (a6989586621679379732 :: NumChildren) Source # 
Instance details

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

type Apply InstrClassSym0 (a6989586621679379732 :: NumChildren) = InstrClassSym1 a6989586621679379732
type Apply (InstrClassSym1 a6989586621679379732 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679379733 :: FailureType) Source # 
Instance details

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

type Apply (InstrClassSym1 a6989586621679379732 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679379733 :: FailureType) = InstrClassSym2 a6989586621679379732 a6989586621679379733
type GetClassified ('InstrClass _1 a _2 _3) Source # 
Instance details

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

type GetClassified ('InstrClass _1 a _2 _3) = a

data IsMichelson Source #

Constructors

FromMichelson

There is corresponding instruction in the Michelson spec.

Additional

"Extended instructions". Don't affect execution on chain, but may affect execution on the morley emulator.

Phantom

Wrappers that don't affect execution.

Structural

Michelson structures that are not instructions, e.g. a nested code block.

Instances

Instances details
Enum IsMichelson Source # 
Instance details

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

Methods

succ :: IsMichelson -> IsMichelson #

pred :: IsMichelson -> IsMichelson #

toEnum :: Int -> IsMichelson #

fromEnum :: IsMichelson -> Int #

enumFrom :: IsMichelson -> [IsMichelson] #

enumFromThen :: IsMichelson -> IsMichelson -> [IsMichelson] #

enumFromTo :: IsMichelson -> IsMichelson -> [IsMichelson] #

enumFromThenTo :: IsMichelson -> IsMichelson -> IsMichelson -> [IsMichelson] #

Show IsMichelson Source # 
Instance details

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

Methods

showsPrec :: Int -> IsMichelson -> ShowS #

show :: IsMichelson -> String #

showList :: [IsMichelson] -> ShowS #

ClassifyInstr IsMichelson Source # 
Instance details

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

Associated Types

type GetClassified c :: k Source #

Methods

getClassified :: forall (c :: InstrClass). SingInstrClass c -> Sing (GetClassified c) Source #

SingKind IsMichelson Source # 
Instance details

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

Associated Types

type Demote IsMichelson = (r :: Type) #

Methods

fromSing :: forall (a :: IsMichelson). Sing a -> Demote IsMichelson #

toSing :: Demote IsMichelson -> SomeSing IsMichelson #

SDecide IsMichelson Source # 
Instance details

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

Methods

(%~) :: forall (a :: IsMichelson) (b :: IsMichelson). Sing a -> Sing b -> Decision (a :~: b) #

TestCoercion SingIsMichelson Source # 
Instance details

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

Methods

testCoercion :: forall (a :: k) (b :: k). SingIsMichelson a -> SingIsMichelson b -> Maybe (Coercion a b) #

TestEquality SingIsMichelson Source # 
Instance details

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

Methods

testEquality :: forall (a :: k) (b :: k). SingIsMichelson a -> SingIsMichelson b -> Maybe (a :~: b) #

SingI 'Additional Source # 
Instance details

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

Methods

sing :: Sing 'Additional #

SingI 'FromMichelson Source # 
Instance details

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

Methods

sing :: Sing 'FromMichelson #

SingI 'Phantom Source # 
Instance details

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

Methods

sing :: Sing 'Phantom #

SingI 'Structural Source # 
Instance details

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

Methods

sing :: Sing 'Structural #

SingI InstrClassSym0 Source # 
Instance details

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

Methods

sing :: Sing InstrClassSym0 #

SuppressUnusedWarnings InstrClassSym0 Source # 
Instance details

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

Methods

suppressUnusedWarnings :: () #

SingI d => SingI (InstrClassSym1 d :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) Source # 
Instance details

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

Methods

sing :: Sing (InstrClassSym1 d) #

SuppressUnusedWarnings (InstrClassSym1 a6989586621679379732 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) Source # 
Instance details

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

Methods

suppressUnusedWarnings :: () #

(SingI d1, SingI d2) => SingI (InstrClassSym2 d1 d2 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) Source # 
Instance details

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

Methods

sing :: Sing (InstrClassSym2 d1 d2) #

SuppressUnusedWarnings (InstrClassSym2 a6989586621679379732 a6989586621679379733 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) Source # 
Instance details

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

Methods

suppressUnusedWarnings :: () #

type Demote IsMichelson Source # 
Instance details

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

type Demote IsMichelson = IsMichelson
type Sing Source # 
Instance details

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

type Sing = SingIsMichelson
type Apply InstrClassSym0 (a6989586621679379732 :: NumChildren) Source # 
Instance details

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

type Apply InstrClassSym0 (a6989586621679379732 :: NumChildren) = InstrClassSym1 a6989586621679379732
type Apply (InstrClassSym1 a6989586621679379732 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679379733 :: FailureType) Source # 
Instance details

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

type Apply (InstrClassSym1 a6989586621679379732 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679379733 :: FailureType) = InstrClassSym2 a6989586621679379732 a6989586621679379733
type Apply (InstrClassSym2 a6989586621679379732 a6989586621679379733 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) (a6989586621679379734 :: IsMichelson) Source # 
Instance details

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

type Apply (InstrClassSym2 a6989586621679379732 a6989586621679379733 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) (a6989586621679379734 :: IsMichelson) = InstrClassSym3 a6989586621679379732 a6989586621679379733 a6989586621679379734
type GetClassified ('InstrClass _1 _2 a _3) Source # 
Instance details

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

type GetClassified ('InstrClass _1 _2 a _3) = a

data HasAnns Source #

Whether an instruction carries Michelson annotations.

Constructors

DoesNotHaveAnns 
DoesHaveStandardAnns

Standard means that the first constructor argument contains all annotations as Anns type, which is true for most annotated instructions. There are a couple exceptions, however.

DoesHaveNonStandardAnns 

Instances

Instances details
Enum HasAnns Source # 
Instance details

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

Methods

succ :: HasAnns -> HasAnns #

pred :: HasAnns -> HasAnns #

toEnum :: Int -> HasAnns #

fromEnum :: HasAnns -> Int #

enumFrom :: HasAnns -> [HasAnns] #

enumFromThen :: HasAnns -> HasAnns -> [HasAnns] #

enumFromTo :: HasAnns -> HasAnns -> [HasAnns] #

enumFromThenTo :: HasAnns -> HasAnns -> HasAnns -> [HasAnns] #

Show HasAnns Source # 
Instance details

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

Methods

showsPrec :: Int -> HasAnns -> ShowS #

show :: HasAnns -> String #

showList :: [HasAnns] -> ShowS #

ClassifyInstr HasAnns Source # 
Instance details

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

Associated Types

type GetClassified c :: k Source #

Methods

getClassified :: forall (c :: InstrClass). SingInstrClass c -> Sing (GetClassified c) Source #

SingKind HasAnns Source # 
Instance details

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

Associated Types

type Demote HasAnns = (r :: Type) #

Methods

fromSing :: forall (a :: HasAnns). Sing a -> Demote HasAnns #

toSing :: Demote HasAnns -> SomeSing HasAnns #

SDecide HasAnns Source # 
Instance details

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

Methods

(%~) :: forall (a :: HasAnns) (b :: HasAnns). Sing a -> Sing b -> Decision (a :~: b) #

TestCoercion SingHasAnns Source # 
Instance details

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

Methods

testCoercion :: forall (a :: k) (b :: k). SingHasAnns a -> SingHasAnns b -> Maybe (Coercion a b) #

TestEquality SingHasAnns Source # 
Instance details

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

Methods

testEquality :: forall (a :: k) (b :: k). SingHasAnns a -> SingHasAnns b -> Maybe (a :~: b) #

SingI 'DoesHaveNonStandardAnns Source # 
Instance details

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

Methods

sing :: Sing 'DoesHaveNonStandardAnns #

SingI 'DoesHaveStandardAnns Source # 
Instance details

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

Methods

sing :: Sing 'DoesHaveStandardAnns #

SingI 'DoesNotHaveAnns Source # 
Instance details

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

Methods

sing :: Sing 'DoesNotHaveAnns #

SingI InstrClassSym0 Source # 
Instance details

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

Methods

sing :: Sing InstrClassSym0 #

SuppressUnusedWarnings InstrClassSym0 Source # 
Instance details

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

Methods

suppressUnusedWarnings :: () #

SingI d => SingI (InstrClassSym1 d :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) Source # 
Instance details

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

Methods

sing :: Sing (InstrClassSym1 d) #

SuppressUnusedWarnings (InstrClassSym1 a6989586621679379732 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) Source # 
Instance details

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

Methods

suppressUnusedWarnings :: () #

(SingI d1, SingI d2) => SingI (InstrClassSym2 d1 d2 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) Source # 
Instance details

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

Methods

sing :: Sing (InstrClassSym2 d1 d2) #

SuppressUnusedWarnings (InstrClassSym2 a6989586621679379732 a6989586621679379733 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) Source # 
Instance details

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

Methods

suppressUnusedWarnings :: () #

(SingI d1, SingI d2, SingI d3) => SingI (InstrClassSym3 d1 d2 d3 :: TyFun HasAnns InstrClass -> Type) Source # 
Instance details

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

Methods

sing :: Sing (InstrClassSym3 d1 d2 d3) #

SuppressUnusedWarnings (InstrClassSym3 a6989586621679379732 a6989586621679379733 a6989586621679379734 :: TyFun HasAnns InstrClass -> Type) Source # 
Instance details

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

Methods

suppressUnusedWarnings :: () #

type Demote HasAnns Source # 
Instance details

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

type Demote HasAnns = HasAnns
type Sing Source # 
Instance details

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

type Sing = SingHasAnns
type Apply (InstrClassSym3 a6989586621679379732 a6989586621679379733 a6989586621679379734 :: TyFun HasAnns InstrClass -> Type) (a6989586621679379735 :: HasAnns) Source # 
Instance details

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

type Apply (InstrClassSym3 a6989586621679379732 a6989586621679379733 a6989586621679379734 :: TyFun HasAnns InstrClass -> Type) (a6989586621679379735 :: HasAnns) = 'InstrClass a6989586621679379732 a6989586621679379733 a6989586621679379734 a6989586621679379735
type Apply InstrClassSym0 (a6989586621679379732 :: NumChildren) Source # 
Instance details

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

type Apply InstrClassSym0 (a6989586621679379732 :: NumChildren) = InstrClassSym1 a6989586621679379732
type Apply (InstrClassSym1 a6989586621679379732 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679379733 :: FailureType) Source # 
Instance details

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

type Apply (InstrClassSym1 a6989586621679379732 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679379733 :: FailureType) = InstrClassSym2 a6989586621679379732 a6989586621679379733
type Apply (InstrClassSym2 a6989586621679379732 a6989586621679379733 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) (a6989586621679379734 :: IsMichelson) Source # 
Instance details

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

type Apply (InstrClassSym2 a6989586621679379732 a6989586621679379733 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) (a6989586621679379734 :: IsMichelson) = InstrClassSym3 a6989586621679379732 a6989586621679379733 a6989586621679379734
type GetClassified ('InstrClass _1 _2 _3 a) Source # 
Instance details

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

type GetClassified ('InstrClass _1 _2 _3 a) = a

Singletons

data SingNumChildren :: NumChildren -> Type where Source #

Constructors

SMayHaveChildren :: SingNumChildren ('MayHaveChildren :: NumChildren) 
SHasIndirectChildren :: SingNumChildren ('HasIndirectChildren :: NumChildren) 
SNoChildren :: SingNumChildren ('NoChildren :: NumChildren) 
SOneChild :: SingNumChildren ('OneChild :: NumChildren) 
STwoChildren :: SingNumChildren ('TwoChildren :: NumChildren) 

Instances

Instances details
TestCoercion SingNumChildren Source # 
Instance details

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

Methods

testCoercion :: forall (a :: k) (b :: k). SingNumChildren a -> SingNumChildren b -> Maybe (Coercion a b) #

TestEquality SingNumChildren Source # 
Instance details

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

Methods

testEquality :: forall (a :: k) (b :: k). SingNumChildren a -> SingNumChildren b -> Maybe (a :~: b) #

data SingFailureType :: FailureType -> Type where Source #

Constructors

SAlwaysFailing :: SingFailureType ('AlwaysFailing :: FailureType) 
SFailingNormal :: SingFailureType ('FailingNormal :: FailureType) 

Instances

Instances details
TestCoercion SingFailureType Source # 
Instance details

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

Methods

testCoercion :: forall (a :: k) (b :: k). SingFailureType a -> SingFailureType b -> Maybe (Coercion a b) #

TestEquality SingFailureType Source # 
Instance details

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

Methods

testEquality :: forall (a :: k) (b :: k). SingFailureType a -> SingFailureType b -> Maybe (a :~: b) #

data SingIsMichelson :: IsMichelson -> Type where Source #

Constructors

SFromMichelson :: SingIsMichelson ('FromMichelson :: IsMichelson) 
SAdditional :: SingIsMichelson ('Additional :: IsMichelson) 
SPhantom :: SingIsMichelson ('Phantom :: IsMichelson) 
SStructural :: SingIsMichelson ('Structural :: IsMichelson) 

Instances

Instances details
TestCoercion SingIsMichelson Source # 
Instance details

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

Methods

testCoercion :: forall (a :: k) (b :: k). SingIsMichelson a -> SingIsMichelson b -> Maybe (Coercion a b) #

TestEquality SingIsMichelson Source # 
Instance details

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

Methods

testEquality :: forall (a :: k) (b :: k). SingIsMichelson a -> SingIsMichelson b -> Maybe (a :~: b) #

data SingHasAnns :: HasAnns -> Type where Source #

Constructors

SDoesNotHaveAnns :: SingHasAnns ('DoesNotHaveAnns :: HasAnns) 
SDoesHaveStandardAnns :: SingHasAnns ('DoesHaveStandardAnns :: HasAnns) 
SDoesHaveNonStandardAnns :: SingHasAnns ('DoesHaveNonStandardAnns :: HasAnns) 

Instances

Instances details
TestCoercion SingHasAnns Source # 
Instance details

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

Methods

testCoercion :: forall (a :: k) (b :: k). SingHasAnns a -> SingHasAnns b -> Maybe (Coercion a b) #

TestEquality SingHasAnns Source # 
Instance details

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

Methods

testEquality :: forall (a :: k) (b :: k). SingHasAnns a -> SingHasAnns b -> Maybe (a :~: b) #