{-# OPTIONS_HADDOCK not-home #-}
module Morley.Michelson.Typed.ClassifiedInstr.Internal.WithClassifiedInstr
( module Morley.Michelson.Typed.ClassifiedInstr.Internal.WithClassifiedInstr
) where
import Data.Singletons (Sing, SingI(..))
import Morley.Michelson.Typed.ClassifiedInstr.Internal.MainImpl
import Morley.Michelson.Typed.ClassifiedInstr.Internal.Types
import Morley.Michelson.Typed.Instr (Instr)
class WithClassifiedInstr instr where
type WCIConstraint instr (cls' :: InstrClass) :: Constraint
withClassifiedInstr
:: forall t inp out r. ClassifyInstr t
=> (forall cls. (SingI cls, WCIConstraint instr cls)
=> Sing (GetClassified cls :: t)
-> ClassifiedInstr cls inp out
-> r)
-> instr inp out
-> r
instance WithClassifiedInstr Instr where
type WCIConstraint Instr _ = ()
withClassifiedInstr :: forall t (inp :: [T]) (out :: [T]) r.
ClassifyInstr t =>
(forall (cls :: InstrClass).
(SingI cls, WCIConstraint Instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> Instr inp out -> r
withClassifiedInstr forall (cls :: InstrClass).
(SingI cls, WCIConstraint Instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r
f Instr inp out
instr = case Instr inp out -> WellClassifiedInstr inp out
forall (inp :: [T]) (out :: [T]).
Instr inp out -> WellClassifiedInstr inp out
classifyInstr Instr inp out
instr of
WCI ClassifiedInstr cls inp out
cinstr -> Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r
forall (cls :: InstrClass).
(SingI cls, WCIConstraint Instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r
f (ClassifiedInstr cls inp out -> Sing (GetClassified cls)
forall t (c :: InstrClass) (inp :: [T]) (out :: [T]).
(SingI c, ClassifyInstr t) =>
ClassifiedInstr c inp out -> Sing (GetClassified c)
getInstrClass ClassifiedInstr cls inp out
cinstr) ClassifiedInstr cls inp out
cinstr
instance SingI cls => WithClassifiedInstr (ClassifiedInstr cls) where
type WCIConstraint (ClassifiedInstr cls) cls' = cls ~ cls'
withClassifiedInstr :: forall t (inp :: [T]) (out :: [T]) r.
ClassifyInstr t =>
(forall (cls :: InstrClass).
(SingI cls, WCIConstraint (ClassifiedInstr cls) cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> ClassifiedInstr cls inp out -> r
withClassifiedInstr forall (cls :: InstrClass).
(SingI cls, WCIConstraint (ClassifiedInstr cls) cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r
f ClassifiedInstr cls inp out
cinstr = Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r
forall (cls :: InstrClass).
(SingI cls, WCIConstraint (ClassifiedInstr cls) cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r
f (ClassifiedInstr cls inp out -> Sing (GetClassified cls)
forall t (c :: InstrClass) (inp :: [T]) (out :: [T]).
(SingI c, ClassifyInstr t) =>
ClassifiedInstr c inp out -> Sing (GetClassified c)
getInstrClass ClassifiedInstr cls inp out
cinstr) ClassifiedInstr cls inp out
cinstr