Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Data kinds plus singletons defining possible classifications for instructions.
Synopsis
- data InstrClass = InstrClass NumChildren FailureType IsMichelson HasAnns
- data HasAnns
- data IsMichelson
- data FailureType
- data NumChildren
- class ClassifyInstr k where
- type GetClassified (c :: InstrClass) :: k
- getClassified :: SingInstrClass c -> Sing (GetClassified c :: k)
- data SingHasAnns :: HasAnns -> Type where
- type family DoesHaveNonStandardAnnsSym0 :: HasAnns where ...
- type family DoesHaveStandardAnnsSym0 :: HasAnns where ...
- type family DoesNotHaveAnnsSym0 :: HasAnns where ...
- data SingIsMichelson :: IsMichelson -> Type where
- SFromMichelson :: SingIsMichelson ('FromMichelson :: IsMichelson)
- SAdditional :: SingIsMichelson ('Additional :: IsMichelson)
- SPhantom :: SingIsMichelson ('Phantom :: IsMichelson)
- SStructural :: SingIsMichelson ('Structural :: IsMichelson)
- type family StructuralSym0 :: IsMichelson where ...
- type family PhantomSym0 :: IsMichelson where ...
- type family AdditionalSym0 :: IsMichelson where ...
- type family FromMichelsonSym0 :: IsMichelson where ...
- data SingFailureType :: FailureType -> Type where
- type family FailingNormalSym0 :: FailureType where ...
- type family AlwaysFailingSym0 :: FailureType where ...
- 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)
- type family TwoChildrenSym0 :: NumChildren where ...
- type family OneChildSym0 :: NumChildren where ...
- type family NoChildrenSym0 :: NumChildren where ...
- type family HasIndirectChildrenSym0 :: NumChildren where ...
- type family MayHaveChildrenSym0 :: NumChildren where ...
- 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)
- type family InstrClassSym4 (a6989586621679387875 :: NumChildren) (a6989586621679387876 :: FailureType) (a6989586621679387877 :: IsMichelson) (a6989586621679387878 :: HasAnns) :: InstrClass where ...
- data InstrClassSym3 (a6989586621679387875 :: NumChildren) (a6989586621679387876 :: FailureType) (a6989586621679387877 :: IsMichelson) :: (~>) HasAnns InstrClass where
- InstrClassSym3KindInference :: SameKind (Apply (InstrClassSym3 a6989586621679387875 a6989586621679387876 a6989586621679387877) arg) (InstrClassSym4 a6989586621679387875 a6989586621679387876 a6989586621679387877 arg) => InstrClassSym3 a6989586621679387875 a6989586621679387876 a6989586621679387877 a6989586621679387878
- data InstrClassSym2 (a6989586621679387875 :: NumChildren) (a6989586621679387876 :: FailureType) :: (~>) IsMichelson ((~>) HasAnns InstrClass) where
- InstrClassSym2KindInference :: SameKind (Apply (InstrClassSym2 a6989586621679387875 a6989586621679387876) arg) (InstrClassSym3 a6989586621679387875 a6989586621679387876 arg) => InstrClassSym2 a6989586621679387875 a6989586621679387876 a6989586621679387877
- data InstrClassSym1 (a6989586621679387875 :: NumChildren) :: (~>) FailureType ((~>) IsMichelson ((~>) HasAnns InstrClass)) where
- InstrClassSym1KindInference :: SameKind (Apply (InstrClassSym1 a6989586621679387875) arg) (InstrClassSym2 a6989586621679387875 arg) => InstrClassSym1 a6989586621679387875 a6989586621679387876
- data InstrClassSym0 :: (~>) NumChildren ((~>) FailureType ((~>) IsMichelson ((~>) HasAnns InstrClass))) where
- InstrClassSym0KindInference :: SameKind (Apply InstrClassSym0 arg) (InstrClassSym1 arg) => InstrClassSym0 a6989586621679387875
Documentation
data InstrClass Source #
A product type of all classifications.
Instances
Whether an instruction carries Michelson annotations.
DoesNotHaveAnns | |
DoesHaveStandardAnns | Standard means that the first constructor argument contains all
annotations as |
DoesHaveNonStandardAnns |
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
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 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
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 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) # |
type family DoesHaveNonStandardAnnsSym0 :: HasAnns where ... Source #
type family DoesHaveStandardAnnsSym0 :: HasAnns where ... Source #
type family DoesNotHaveAnnsSym0 :: HasAnns where ... Source #
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) # |
type family StructuralSym0 :: IsMichelson where ... Source #
type family PhantomSym0 :: IsMichelson where ... Source #
type family AdditionalSym0 :: IsMichelson where ... Source #
type family FromMichelsonSym0 :: IsMichelson where ... Source #
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) # |
type family FailingNormalSym0 :: FailureType where ... Source #
type family AlwaysFailingSym0 :: FailureType where ... Source #
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) # |
type family TwoChildrenSym0 :: NumChildren where ... Source #
type family OneChildSym0 :: NumChildren where ... Source #
type family NoChildrenSym0 :: NumChildren where ... Source #
type family HasIndirectChildrenSym0 :: NumChildren where ... Source #
type family MayHaveChildrenSym0 :: NumChildren where ... 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) # |
type family InstrClassSym4 (a6989586621679387875 :: NumChildren) (a6989586621679387876 :: FailureType) (a6989586621679387877 :: IsMichelson) (a6989586621679387878 :: HasAnns) :: InstrClass where ... Source #
InstrClassSym4 a6989586621679387875 a6989586621679387876 a6989586621679387877 a6989586621679387878 = 'InstrClass a6989586621679387875 a6989586621679387876 a6989586621679387877 a6989586621679387878 |
data InstrClassSym3 (a6989586621679387875 :: NumChildren) (a6989586621679387876 :: FailureType) (a6989586621679387877 :: IsMichelson) :: (~>) HasAnns InstrClass where Source #
InstrClassSym3KindInference :: SameKind (Apply (InstrClassSym3 a6989586621679387875 a6989586621679387876 a6989586621679387877) arg) (InstrClassSym4 a6989586621679387875 a6989586621679387876 a6989586621679387877 arg) => InstrClassSym3 a6989586621679387875 a6989586621679387876 a6989586621679387877 a6989586621679387878 |
Instances
(SingI d1, SingI d2, SingI d3) => SingI (InstrClassSym3 d1 d2 d3 :: TyFun HasAnns InstrClass -> Type) Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types sing :: Sing (InstrClassSym3 d1 d2 d3) # | |
SuppressUnusedWarnings (InstrClassSym3 a6989586621679387875 a6989586621679387876 a6989586621679387877 :: TyFun HasAnns InstrClass -> Type) Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types suppressUnusedWarnings :: () # | |
type Apply (InstrClassSym3 a6989586621679387875 a6989586621679387876 a6989586621679387877 :: TyFun HasAnns InstrClass -> Type) (a6989586621679387878 :: HasAnns) Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply (InstrClassSym3 a6989586621679387875 a6989586621679387876 a6989586621679387877 :: TyFun HasAnns InstrClass -> Type) (a6989586621679387878 :: HasAnns) = 'InstrClass a6989586621679387875 a6989586621679387876 a6989586621679387877 a6989586621679387878 |
data InstrClassSym2 (a6989586621679387875 :: NumChildren) (a6989586621679387876 :: FailureType) :: (~>) IsMichelson ((~>) HasAnns InstrClass) where Source #
InstrClassSym2KindInference :: SameKind (Apply (InstrClassSym2 a6989586621679387875 a6989586621679387876) arg) (InstrClassSym3 a6989586621679387875 a6989586621679387876 arg) => InstrClassSym2 a6989586621679387875 a6989586621679387876 a6989586621679387877 |
Instances
(SingI d1, SingI d2) => SingI (InstrClassSym2 d1 d2 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types sing :: Sing (InstrClassSym2 d1 d2) # | |
SuppressUnusedWarnings (InstrClassSym2 a6989586621679387875 a6989586621679387876 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types suppressUnusedWarnings :: () # | |
type Apply (InstrClassSym2 a6989586621679387875 a6989586621679387876 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) (a6989586621679387877 :: IsMichelson) Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply (InstrClassSym2 a6989586621679387875 a6989586621679387876 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) (a6989586621679387877 :: IsMichelson) = InstrClassSym3 a6989586621679387875 a6989586621679387876 a6989586621679387877 |
data InstrClassSym1 (a6989586621679387875 :: NumChildren) :: (~>) FailureType ((~>) IsMichelson ((~>) HasAnns InstrClass)) where Source #
InstrClassSym1KindInference :: SameKind (Apply (InstrClassSym1 a6989586621679387875) arg) (InstrClassSym2 a6989586621679387875 arg) => InstrClassSym1 a6989586621679387875 a6989586621679387876 |
Instances
SingI d => SingI (InstrClassSym1 d :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types sing :: Sing (InstrClassSym1 d) # | |
SuppressUnusedWarnings (InstrClassSym1 a6989586621679387875 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types suppressUnusedWarnings :: () # | |
type Apply (InstrClassSym1 a6989586621679387875 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679387876 :: FailureType) Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply (InstrClassSym1 a6989586621679387875 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679387876 :: FailureType) = InstrClassSym2 a6989586621679387875 a6989586621679387876 |
data InstrClassSym0 :: (~>) NumChildren ((~>) FailureType ((~>) IsMichelson ((~>) HasAnns InstrClass))) where Source #
InstrClassSym0KindInference :: SameKind (Apply InstrClassSym0 arg) (InstrClassSym1 arg) => InstrClassSym0 a6989586621679387875 |
Instances
SingI InstrClassSym0 Source # | |
SuppressUnusedWarnings InstrClassSym0 Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types suppressUnusedWarnings :: () # | |
type Apply InstrClassSym0 (a6989586621679387875 :: NumChildren) Source # | |
Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply InstrClassSym0 (a6989586621679387875 :: NumChildren) = InstrClassSym1 a6989586621679387875 |