Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Data kinds plus singletons defining possible classifications for instructions.
Synopsis
- data NumChildren
- data FailureType
- data IsMichelson
- data HasAnns
- data SingNumChildren :: NumChildren -> Type where
- SMayHaveChildren :: SingNumChildren ('MayHaveChildren :: NumChildren)
- SHasIndirectChildren :: SingNumChildren ('HasIndirectChildren :: NumChildren)
- SNoChildren :: SingNumChildren ('NoChildren :: NumChildren)
- SOneChild :: SingNumChildren ('OneChild :: NumChildren)
- STwoChildren :: SingNumChildren ('TwoChildren :: NumChildren)
- data SingFailureType :: FailureType -> Type where
- data SingIsMichelson :: IsMichelson -> Type where
- SFromMichelson :: SingIsMichelson ('FromMichelson :: IsMichelson)
- SAdditional :: SingIsMichelson ('Additional :: IsMichelson)
- SPhantom :: SingIsMichelson ('Phantom :: IsMichelson)
- SStructural :: SingIsMichelson ('Structural :: IsMichelson)
- data SingHasAnns :: HasAnns -> Type where
- data InstrClass = InstrClass NumChildren FailureType IsMichelson HasAnns
- class ClassifyInstr k where
- type GetClassified (c :: InstrClass) :: k
- getClassified :: SingInstrClass c -> Sing (GetClassified c :: k)
- data SingInstrClass :: InstrClass -> Type where
- SInstrClass :: forall (n :: NumChildren) (n :: FailureType) (n :: IsMichelson) (n :: HasAnns). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> SingInstrClass ('InstrClass n n n n :: InstrClass)
- data InstrClassSym0 :: (~>) NumChildren ((~>) FailureType ((~>) IsMichelson ((~>) HasAnns InstrClass))) where
- InstrClassSym0KindInference :: SameKind (Apply InstrClassSym0 arg) (InstrClassSym1 arg) => InstrClassSym0 a6989586621679458070
- data InstrClassSym1 (a6989586621679458070 :: NumChildren) :: (~>) FailureType ((~>) IsMichelson ((~>) HasAnns InstrClass)) where
- InstrClassSym1KindInference :: SameKind (Apply (InstrClassSym1 a6989586621679458070) arg) (InstrClassSym2 a6989586621679458070 arg) => InstrClassSym1 a6989586621679458070 a6989586621679458071
- data InstrClassSym2 (a6989586621679458070 :: NumChildren) (a6989586621679458071 :: FailureType) :: (~>) IsMichelson ((~>) HasAnns InstrClass) where
- InstrClassSym2KindInference :: SameKind (Apply (InstrClassSym2 a6989586621679458070 a6989586621679458071) arg) (InstrClassSym3 a6989586621679458070 a6989586621679458071 arg) => InstrClassSym2 a6989586621679458070 a6989586621679458071 a6989586621679458072
- data InstrClassSym3 (a6989586621679458070 :: NumChildren) (a6989586621679458071 :: FailureType) (a6989586621679458072 :: IsMichelson) :: (~>) HasAnns InstrClass where
- InstrClassSym3KindInference :: SameKind (Apply (InstrClassSym3 a6989586621679458070 a6989586621679458071 a6989586621679458072) arg) (InstrClassSym4 a6989586621679458070 a6989586621679458071 a6989586621679458072 arg) => InstrClassSym3 a6989586621679458070 a6989586621679458071 a6989586621679458072 a6989586621679458073
- type family InstrClassSym4 (a6989586621679458070 :: NumChildren) (a6989586621679458071 :: FailureType) (a6989586621679458072 :: IsMichelson) (a6989586621679458073 :: HasAnns) :: InstrClass where ...
- type family MayHaveChildrenSym0 :: NumChildren where ...
- type family HasIndirectChildrenSym0 :: NumChildren where ...
- type family NoChildrenSym0 :: NumChildren where ...
- type family OneChildSym0 :: NumChildren where ...
- type family TwoChildrenSym0 :: NumChildren where ...
- type family AlwaysFailingSym0 :: FailureType where ...
- type family FailingNormalSym0 :: FailureType where ...
- type family FromMichelsonSym0 :: IsMichelson where ...
- type family AdditionalSym0 :: IsMichelson where ...
- type family PhantomSym0 :: IsMichelson where ...
- type family StructuralSym0 :: IsMichelson where ...
- type family DoesNotHaveAnnsSym0 :: HasAnns where ...
- type family DoesHaveStandardAnnsSym0 :: HasAnns where ...
- type family DoesHaveNonStandardAnnsSym0 :: HasAnns where ...
Documentation
data NumChildren Source #
Number of children instructions a given instruction constructor has.
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
data FailureType Source #
Whether an instruction always fails. An example of always-failing
instruction is NEVER
.
AlwaysFailing | Instruction always fails. |
FailingNormal | Instruction might fail if inputs are incorrect, but will generally work. |
Instances
data IsMichelson Source #
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
Whether an instruction carries Michelson annotations.
DoesNotHaveAnns | |
DoesHaveStandardAnns | Standard means that the first constructor argument contains all
annotations as |
DoesHaveNonStandardAnns |
Instances
data SingNumChildren :: NumChildren -> Type where Source #
Instances
TestCoercion SingNumChildren Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types testCoercion :: forall (a :: k) (b :: k). SingNumChildren a -> SingNumChildren b -> Maybe (Coercion a b) # | |
TestEquality SingNumChildren Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types testEquality :: forall (a :: k) (b :: k). SingNumChildren a -> SingNumChildren b -> Maybe (a :~: b) # |
data SingFailureType :: FailureType -> Type where Source #
SAlwaysFailing :: SingFailureType ('AlwaysFailing :: FailureType) | |
SFailingNormal :: SingFailureType ('FailingNormal :: FailureType) |
Instances
TestCoercion SingFailureType Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types testCoercion :: forall (a :: k) (b :: k). SingFailureType a -> SingFailureType b -> Maybe (Coercion a b) # | |
TestEquality SingFailureType Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types testEquality :: forall (a :: k) (b :: k). SingFailureType a -> SingFailureType b -> Maybe (a :~: b) # |
data SingIsMichelson :: IsMichelson -> Type where Source #
SFromMichelson :: SingIsMichelson ('FromMichelson :: IsMichelson) | |
SAdditional :: SingIsMichelson ('Additional :: IsMichelson) | |
SPhantom :: SingIsMichelson ('Phantom :: IsMichelson) | |
SStructural :: SingIsMichelson ('Structural :: IsMichelson) |
Instances
TestCoercion SingIsMichelson Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types testCoercion :: forall (a :: k) (b :: k). SingIsMichelson a -> SingIsMichelson b -> Maybe (Coercion a b) # | |
TestEquality SingIsMichelson Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types testEquality :: forall (a :: k) (b :: k). SingIsMichelson a -> SingIsMichelson b -> Maybe (a :~: b) # |
data SingHasAnns :: HasAnns -> Type where Source #
Instances
TestCoercion SingHasAnns Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types testCoercion :: forall (a :: k) (b :: k). SingHasAnns a -> SingHasAnns b -> Maybe (Coercion a b) # | |
TestEquality SingHasAnns Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types testEquality :: forall (a :: k) (b :: k). SingHasAnns a -> SingHasAnns b -> Maybe (a :~: b) # |
data InstrClass Source #
A product type of all classifications.
Instances
class ClassifyInstr k where Source #
type GetClassified (c :: InstrClass) :: k Source #
getClassified :: SingInstrClass c -> Sing (GetClassified c :: k) Source #
Instances
ClassifyInstr FailureType Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type GetClassified c :: k Source # getClassified :: forall (c :: InstrClass). SingInstrClass c -> Sing (GetClassified c) Source # | |
ClassifyInstr HasAnns Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type GetClassified c :: k Source # getClassified :: forall (c :: InstrClass). SingInstrClass c -> Sing (GetClassified c) Source # | |
ClassifyInstr IsMichelson Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type GetClassified c :: k Source # getClassified :: forall (c :: InstrClass). SingInstrClass c -> Sing (GetClassified c) Source # | |
ClassifyInstr NumChildren Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type GetClassified c :: k Source # getClassified :: forall (c :: InstrClass). SingInstrClass c -> Sing (GetClassified c) Source # |
data SingInstrClass :: InstrClass -> Type where Source #
SInstrClass :: forall (n :: NumChildren) (n :: FailureType) (n :: IsMichelson) (n :: HasAnns). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> SingInstrClass ('InstrClass n n n n :: InstrClass) |
Instances
(SDecide NumChildren, SDecide FailureType, SDecide IsMichelson, SDecide HasAnns) => TestCoercion SingInstrClass Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types testCoercion :: forall (a :: k) (b :: k). SingInstrClass a -> SingInstrClass b -> Maybe (Coercion a b) # | |
(SDecide NumChildren, SDecide FailureType, SDecide IsMichelson, SDecide HasAnns) => TestEquality SingInstrClass Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types testEquality :: forall (a :: k) (b :: k). SingInstrClass a -> SingInstrClass b -> Maybe (a :~: b) # |
data InstrClassSym0 :: (~>) NumChildren ((~>) FailureType ((~>) IsMichelson ((~>) HasAnns InstrClass))) where Source #
InstrClassSym0KindInference :: SameKind (Apply InstrClassSym0 arg) (InstrClassSym1 arg) => InstrClassSym0 a6989586621679458070 |
Instances
SingI InstrClassSym0 Source # | |
SuppressUnusedWarnings InstrClassSym0 Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types suppressUnusedWarnings :: () # | |
type Apply InstrClassSym0 (a6989586621679458070 :: NumChildren) Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply InstrClassSym0 (a6989586621679458070 :: NumChildren) = InstrClassSym1 a6989586621679458070 |
data InstrClassSym1 (a6989586621679458070 :: NumChildren) :: (~>) FailureType ((~>) IsMichelson ((~>) HasAnns InstrClass)) where Source #
InstrClassSym1KindInference :: SameKind (Apply (InstrClassSym1 a6989586621679458070) arg) (InstrClassSym2 a6989586621679458070 arg) => InstrClassSym1 a6989586621679458070 a6989586621679458071 |
Instances
data InstrClassSym2 (a6989586621679458070 :: NumChildren) (a6989586621679458071 :: FailureType) :: (~>) IsMichelson ((~>) HasAnns InstrClass) where Source #
InstrClassSym2KindInference :: SameKind (Apply (InstrClassSym2 a6989586621679458070 a6989586621679458071) arg) (InstrClassSym3 a6989586621679458070 a6989586621679458071 arg) => InstrClassSym2 a6989586621679458070 a6989586621679458071 a6989586621679458072 |
Instances
data InstrClassSym3 (a6989586621679458070 :: NumChildren) (a6989586621679458071 :: FailureType) (a6989586621679458072 :: IsMichelson) :: (~>) HasAnns InstrClass where Source #
InstrClassSym3KindInference :: SameKind (Apply (InstrClassSym3 a6989586621679458070 a6989586621679458071 a6989586621679458072) arg) (InstrClassSym4 a6989586621679458070 a6989586621679458071 a6989586621679458072 arg) => InstrClassSym3 a6989586621679458070 a6989586621679458071 a6989586621679458072 a6989586621679458073 |
Instances
type family InstrClassSym4 (a6989586621679458070 :: NumChildren) (a6989586621679458071 :: FailureType) (a6989586621679458072 :: IsMichelson) (a6989586621679458073 :: HasAnns) :: InstrClass where ... Source #
InstrClassSym4 a6989586621679458070 a6989586621679458071 a6989586621679458072 a6989586621679458073 = 'InstrClass a6989586621679458070 a6989586621679458071 a6989586621679458072 a6989586621679458073 |
type family MayHaveChildrenSym0 :: NumChildren where ... Source #
type family HasIndirectChildrenSym0 :: NumChildren where ... Source #
type family NoChildrenSym0 :: NumChildren where ... Source #
type family OneChildSym0 :: NumChildren where ... Source #
type family TwoChildrenSym0 :: NumChildren where ... Source #
type family AlwaysFailingSym0 :: FailureType where ... Source #
type family FailingNormalSym0 :: FailureType where ... Source #
type family FromMichelsonSym0 :: IsMichelson where ... Source #
type family AdditionalSym0 :: IsMichelson where ... Source #
type family PhantomSym0 :: IsMichelson where ... Source #
type family StructuralSym0 :: IsMichelson where ... Source #
type family DoesNotHaveAnnsSym0 :: HasAnns where ... Source #
type family DoesHaveStandardAnnsSym0 :: HasAnns where ... Source #
type family DoesHaveNonStandardAnnsSym0 :: HasAnns where ... Source #