Safe Haskell	Safe-Inferred
Language	Haskell2010

Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

Description

Data kinds plus singletons defining possible classifications for instructions.

Synopsis

data NumChildren
- = MayHaveChildren
- | HasIndirectChildren
- | NoChildren
- | OneChild
- | TwoChildren
data FailureType
- = AlwaysFailing
- | FailingNormal
data IsMichelson
- = FromMichelson
- | Additional
- | Phantom
- | Structural
data HasAnns
- = DoesNotHaveAnns
- | DoesHaveStandardAnns
- | DoesHaveNonStandardAnns
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
- SAlwaysFailing :: SingFailureType ('AlwaysFailing :: FailureType)
- SFailingNormal :: SingFailureType ('FailingNormal :: FailureType)
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
- SDoesNotHaveAnns :: SingHasAnns ('DoesNotHaveAnns :: HasAnns)
- SDoesHaveStandardAnns :: SingHasAnns ('DoesHaveStandardAnns :: HasAnns)
- SDoesHaveNonStandardAnns :: SingHasAnns ('DoesHaveNonStandardAnns :: HasAnns)
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.

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 #
Lift NumChildren Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods lift :: Quote m => NumChildren -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => NumChildren -> Code m NumChildren #
SingI2 InstrClassSym2 Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (InstrClassSym2 x y) #
SingI1 InstrClassSym1 Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing (InstrClassSym1 x) #
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 (a6989586621679458070 :: NumChildren) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply InstrClassSym0 (a6989586621679458070 :: NumChildren) = InstrClassSym1 a6989586621679458070
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 #
Lift FailureType Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods lift :: Quote m => FailureType -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => FailureType -> Code m FailureType #
SingI2 InstrClassSym2 Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (InstrClassSym2 x y) #
SingI d => SingI2 (InstrClassSym3 d :: FailureType -> IsMichelson -> TyFun HasAnns InstrClass -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (InstrClassSym3 d x y) #
SingI1 InstrClassSym1 Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing (InstrClassSym1 x) #
SingI d => SingI1 (InstrClassSym2 d :: FailureType -> TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing (InstrClassSym2 d x) #
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 a6989586621679458070 :: 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 (a6989586621679458070 :: NumChildren) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply InstrClassSym0 (a6989586621679458070 :: NumChildren) = InstrClassSym1 a6989586621679458070
type Apply (InstrClassSym1 a6989586621679458070 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679458071 :: FailureType) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply (InstrClassSym1 a6989586621679458070 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679458071 :: FailureType) = InstrClassSym2 a6989586621679458070 a6989586621679458071
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 #
Lift IsMichelson Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods lift :: Quote m => IsMichelson -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => IsMichelson -> Code m IsMichelson #
(SingI n1, SingI n2) => SingI2 ('InstrClass n1 n2 :: IsMichelson -> HasAnns -> InstrClass) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing ('InstrClass n1 n2 x y) #
SingI2 InstrClassSym2 Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (InstrClassSym2 x y) #
SingI d => SingI2 (InstrClassSym3 d :: FailureType -> IsMichelson -> TyFun HasAnns InstrClass -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (InstrClassSym3 d x y) #
SingI1 InstrClassSym1 Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing (InstrClassSym1 x) #
SingI d => SingI1 (InstrClassSym2 d :: FailureType -> TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing (InstrClassSym2 d x) #
(SingI d1, SingI d2) => SingI1 (InstrClassSym3 d1 d2 :: IsMichelson -> TyFun HasAnns InstrClass -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing (InstrClassSym3 d1 d2 x) #
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 a6989586621679458070 :: 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 a6989586621679458070 a6989586621679458071 :: 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 (a6989586621679458070 :: NumChildren) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply InstrClassSym0 (a6989586621679458070 :: NumChildren) = InstrClassSym1 a6989586621679458070
type Apply (InstrClassSym1 a6989586621679458070 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679458071 :: FailureType) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply (InstrClassSym1 a6989586621679458070 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679458071 :: FailureType) = InstrClassSym2 a6989586621679458070 a6989586621679458071
type Apply (InstrClassSym2 a6989586621679458070 a6989586621679458071 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) (a6989586621679458072 :: IsMichelson) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply (InstrClassSym2 a6989586621679458070 a6989586621679458071 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) (a6989586621679458072 :: IsMichelson) = InstrClassSym3 a6989586621679458070 a6989586621679458071 a6989586621679458072
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 #
Lift HasAnns Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods lift :: Quote m => HasAnns -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => HasAnns -> Code m HasAnns #
(SingI n1, SingI n2) => SingI2 ('InstrClass n1 n2 :: IsMichelson -> HasAnns -> InstrClass) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing ('InstrClass n1 n2 x y) #
SingI2 InstrClassSym2 Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (InstrClassSym2 x y) #
SingI d => SingI2 (InstrClassSym3 d :: FailureType -> IsMichelson -> TyFun HasAnns InstrClass -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (InstrClassSym3 d x y) #
(SingI n1, SingI n2, SingI n3) => SingI1 ('InstrClass n1 n2 n3 :: HasAnns -> InstrClass) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing ('InstrClass n1 n2 n3 x) #
SingI1 InstrClassSym1 Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing (InstrClassSym1 x) #
SingI d => SingI1 (InstrClassSym2 d :: FailureType -> TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing (InstrClassSym2 d x) #
(SingI d1, SingI d2) => SingI1 (InstrClassSym3 d1 d2 :: IsMichelson -> TyFun HasAnns InstrClass -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing (InstrClassSym3 d1 d2 x) #
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 a6989586621679458070 :: 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 a6989586621679458070 a6989586621679458071 :: 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 a6989586621679458070 a6989586621679458071 a6989586621679458072 :: 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 a6989586621679458070 a6989586621679458071 a6989586621679458072 :: TyFun HasAnns InstrClass -> Type) (a6989586621679458073 :: HasAnns) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply (InstrClassSym3 a6989586621679458070 a6989586621679458071 a6989586621679458072 :: TyFun HasAnns InstrClass -> Type) (a6989586621679458073 :: HasAnns) = 'InstrClass a6989586621679458070 a6989586621679458071 a6989586621679458072 a6989586621679458073
type Apply InstrClassSym0 (a6989586621679458070 :: NumChildren) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply InstrClassSym0 (a6989586621679458070 :: NumChildren) = InstrClassSym1 a6989586621679458070
type Apply (InstrClassSym1 a6989586621679458070 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679458071 :: FailureType) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply (InstrClassSym1 a6989586621679458070 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679458071 :: FailureType) = InstrClassSym2 a6989586621679458070 a6989586621679458071
type Apply (InstrClassSym2 a6989586621679458070 a6989586621679458071 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) (a6989586621679458072 :: IsMichelson) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply (InstrClassSym2 a6989586621679458070 a6989586621679458071 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) (a6989586621679458072 :: IsMichelson) = InstrClassSym3 a6989586621679458070 a6989586621679458071 a6989586621679458072
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

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

data InstrClass Source #

A product type of all classifications.

Constructors

InstrClass NumChildren FailureType IsMichelson HasAnns

Instances

Instances details

SingKind InstrClass Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Associated Types type Demote InstrClass = (r :: Type) # Methods fromSing :: forall (a :: InstrClass). Sing a -> Demote InstrClass # toSing :: Demote InstrClass -> SomeSing InstrClass #
(SDecide NumChildren, SDecide FailureType, SDecide IsMichelson, SDecide HasAnns) => SDecide InstrClass Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods (%~) :: forall (a :: InstrClass) (b :: InstrClass). Sing a -> Sing b -> Decision (a :~: b) #
(SDecide NumChildren, SDecide FailureType, SDecide IsMichelson, SDecide HasAnns) => TestCoercion SingInstrClass Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods 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 #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods testEquality :: forall (a :: k) (b :: k). SingInstrClass a -> SingInstrClass b -> Maybe (a :~: b) #
(SingI n1, SingI n2) => SingI2 ('InstrClass n1 n2 :: IsMichelson -> HasAnns -> InstrClass) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing ('InstrClass n1 n2 x y) #
SingI2 InstrClassSym2 Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (InstrClassSym2 x y) #
SingI d => SingI2 (InstrClassSym3 d :: FailureType -> IsMichelson -> TyFun HasAnns InstrClass -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (InstrClassSym3 d x y) #
(SingI n1, SingI n2, SingI n3) => SingI1 ('InstrClass n1 n2 n3 :: HasAnns -> InstrClass) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing ('InstrClass n1 n2 n3 x) #
SingI1 InstrClassSym1 Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing (InstrClassSym1 x) #
SingI d => SingI1 (InstrClassSym2 d :: FailureType -> TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing (InstrClassSym2 d x) #
(SingI d1, SingI d2) => SingI1 (InstrClassSym3 d1 d2 :: IsMichelson -> TyFun HasAnns InstrClass -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing (InstrClassSym3 d1 d2 x) #
(SingI n1, SingI n2, SingI n3, SingI n4) => SingI ('InstrClass n1 n2 n3 n4 :: InstrClass) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods sing :: Sing ('InstrClass n1 n2 n3 n4) #
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 a6989586621679458070 :: 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 a6989586621679458070 a6989586621679458071 :: 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 a6989586621679458070 a6989586621679458071 a6989586621679458072 :: TyFun HasAnns InstrClass -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods suppressUnusedWarnings :: () #
type Demote InstrClass Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Demote InstrClass = InstrClass
type Sing Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Sing = SingInstrClass
type Apply (InstrClassSym3 a6989586621679458070 a6989586621679458071 a6989586621679458072 :: TyFun HasAnns InstrClass -> Type) (a6989586621679458073 :: HasAnns) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply (InstrClassSym3 a6989586621679458070 a6989586621679458071 a6989586621679458072 :: TyFun HasAnns InstrClass -> Type) (a6989586621679458073 :: HasAnns) = 'InstrClass a6989586621679458070 a6989586621679458071 a6989586621679458072 a6989586621679458073
type Apply InstrClassSym0 (a6989586621679458070 :: NumChildren) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply InstrClassSym0 (a6989586621679458070 :: NumChildren) = InstrClassSym1 a6989586621679458070
type Apply (InstrClassSym1 a6989586621679458070 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679458071 :: FailureType) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply (InstrClassSym1 a6989586621679458070 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679458071 :: FailureType) = InstrClassSym2 a6989586621679458070 a6989586621679458071
type Apply (InstrClassSym2 a6989586621679458070 a6989586621679458071 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) (a6989586621679458072 :: IsMichelson) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply (InstrClassSym2 a6989586621679458070 a6989586621679458071 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) (a6989586621679458072 :: IsMichelson) = InstrClassSym3 a6989586621679458070 a6989586621679458071 a6989586621679458072

class ClassifyInstr k where Source #

Associated Types

type GetClassified (c :: InstrClass) :: k Source #

Methods

getClassified :: SingInstrClass c -> Sing (GetClassified c :: k) Source #

Instances

Instances details

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 #
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 #
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 #
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 #

data SingInstrClass :: InstrClass -> Type where Source #

Constructors

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

Instances details

(SDecide NumChildren, SDecide FailureType, SDecide IsMichelson, SDecide HasAnns) => TestCoercion SingInstrClass Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods 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 #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods testEquality :: forall (a :: k) (b :: k). SingInstrClass a -> SingInstrClass b -> Maybe (a :~: b) #

data InstrClassSym0 :: (~>) NumChildren ((~>) FailureType ((~>) IsMichelson ((~>) HasAnns InstrClass))) where Source #

Constructors

InstrClassSym0KindInference :: SameKind (Apply InstrClassSym0 arg) (InstrClassSym1 arg) => InstrClassSym0 a6989586621679458070

Instances

Instances details

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 Apply InstrClassSym0 (a6989586621679458070 :: NumChildren) Source #
Instance details 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 #

Constructors

InstrClassSym1KindInference :: SameKind (Apply (InstrClassSym1 a6989586621679458070) arg) (InstrClassSym2 a6989586621679458070 arg) => InstrClassSym1 a6989586621679458070 a6989586621679458071

Instances

Instances details

SingI1 InstrClassSym1 Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing (InstrClassSym1 x) #
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 a6989586621679458070 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods suppressUnusedWarnings :: () #
type Apply (InstrClassSym1 a6989586621679458070 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679458071 :: FailureType) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply (InstrClassSym1 a6989586621679458070 :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) (a6989586621679458071 :: FailureType) = InstrClassSym2 a6989586621679458070 a6989586621679458071

data InstrClassSym2 (a6989586621679458070 :: NumChildren) (a6989586621679458071 :: FailureType) :: (~>) IsMichelson ((~>) HasAnns InstrClass) where Source #

Constructors

InstrClassSym2KindInference :: SameKind (Apply (InstrClassSym2 a6989586621679458070 a6989586621679458071) arg) (InstrClassSym3 a6989586621679458070 a6989586621679458071 arg) => InstrClassSym2 a6989586621679458070 a6989586621679458071 a6989586621679458072

Instances

Instances details

SingI2 InstrClassSym2 Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (InstrClassSym2 x y) #
SingI d => SingI1 (InstrClassSym2 d :: FailureType -> TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing (InstrClassSym2 d x) #
(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 a6989586621679458070 a6989586621679458071 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods suppressUnusedWarnings :: () #
type Apply (InstrClassSym2 a6989586621679458070 a6989586621679458071 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) (a6989586621679458072 :: IsMichelson) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply (InstrClassSym2 a6989586621679458070 a6989586621679458071 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) (a6989586621679458072 :: IsMichelson) = InstrClassSym3 a6989586621679458070 a6989586621679458071 a6989586621679458072

data InstrClassSym3 (a6989586621679458070 :: NumChildren) (a6989586621679458071 :: FailureType) (a6989586621679458072 :: IsMichelson) :: (~>) HasAnns InstrClass where Source #

Constructors

InstrClassSym3KindInference :: SameKind (Apply (InstrClassSym3 a6989586621679458070 a6989586621679458071 a6989586621679458072) arg) (InstrClassSym4 a6989586621679458070 a6989586621679458071 a6989586621679458072 arg) => InstrClassSym3 a6989586621679458070 a6989586621679458071 a6989586621679458072 a6989586621679458073

Instances

Instances details

SingI d => SingI2 (InstrClassSym3 d :: FailureType -> IsMichelson -> TyFun HasAnns InstrClass -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (InstrClassSym3 d x y) #
(SingI d1, SingI d2) => SingI1 (InstrClassSym3 d1 d2 :: IsMichelson -> TyFun HasAnns InstrClass -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods liftSing :: forall (x :: k1). Sing x -> Sing (InstrClassSym3 d1 d2 x) #
(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 a6989586621679458070 a6989586621679458071 a6989586621679458072 :: TyFun HasAnns InstrClass -> Type) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types Methods suppressUnusedWarnings :: () #
type Apply (InstrClassSym3 a6989586621679458070 a6989586621679458071 a6989586621679458072 :: TyFun HasAnns InstrClass -> Type) (a6989586621679458073 :: HasAnns) Source #
Instance details Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types type Apply (InstrClassSym3 a6989586621679458070 a6989586621679458071 a6989586621679458072 :: TyFun HasAnns InstrClass -> Type) (a6989586621679458073 :: HasAnns) = 'InstrClass a6989586621679458070 a6989586621679458071 a6989586621679458072 a6989586621679458073

type family InstrClassSym4 (a6989586621679458070 :: NumChildren) (a6989586621679458071 :: FailureType) (a6989586621679458072 :: IsMichelson) (a6989586621679458073 :: HasAnns) :: InstrClass where ... Source #

Equations

InstrClassSym4 a6989586621679458070 a6989586621679458071 a6989586621679458072 a6989586621679458073 = 'InstrClass a6989586621679458070 a6989586621679458071 a6989586621679458072 a6989586621679458073

type family MayHaveChildrenSym0 :: NumChildren where ... Source #

Equations

MayHaveChildrenSym0 = 'MayHaveChildren

type family HasIndirectChildrenSym0 :: NumChildren where ... Source #

Equations

HasIndirectChildrenSym0 = 'HasIndirectChildren

type family NoChildrenSym0 :: NumChildren where ... Source #

Equations

NoChildrenSym0 = 'NoChildren

type family OneChildSym0 :: NumChildren where ... Source #

Equations

OneChildSym0 = 'OneChild