module Michelson.TypeCheck.TypeCheckedOp
( TypeCheckedInstr
, TypeCheckedOp(..)
, IllTypedInstr(..)
, someInstrToOp
) where
import Data.Singletons (SingI)
import Michelson.Printer.Util (RenderDoc(..), renderOpsListNoBraces)
import Michelson.TypeCheck.Types (HST(..), SomeInstr(..), SomeInstrOut(..))
import Michelson.Typed.Convert (instrToOps)
import Michelson.Typed.Instr (Instr, castInstr)
import Michelson.Untyped.Instr (ExpandedOp, InstrAbstract(..))
import Util.TH (deriveGADTNFData)
type TypeCheckedInstr = InstrAbstract TypeCheckedOp
data TypeCheckedOp where
WellTypedOp :: (SingI inp, SingI out) => Instr inp out -> TypeCheckedOp
IllTypedOp :: IllTypedInstr -> TypeCheckedOp
instance Eq TypeCheckedOp where
WellTypedOp Instr inp out
i1 == :: TypeCheckedOp -> TypeCheckedOp -> Bool
== WellTypedOp Instr inp out
i2 = Instr inp out -> Maybe (Instr inp out)
forall (inp1 :: [T]) (out1 :: [T]) (inp2 :: [T]) (out2 :: [T]).
(SingI inp1, SingI out1, SingI inp2, SingI out2) =>
Instr inp1 out1 -> Maybe (Instr inp2 out2)
castInstr Instr inp out
i1 Maybe (Instr inp out) -> Maybe (Instr inp out) -> Bool
forall a. Eq a => a -> a -> Bool
== Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
i2
IllTypedOp IllTypedInstr
i1 == IllTypedOp IllTypedInstr
i2 = IllTypedInstr
i1 IllTypedInstr -> IllTypedInstr -> Bool
forall a. Eq a => a -> a -> Bool
== IllTypedInstr
i2
TypeCheckedOp
_ == TypeCheckedOp
_ = Bool
False
data IllTypedInstr
= SemiTypedInstr TypeCheckedInstr
| NonTypedInstr ExpandedOp
deriving stock (IllTypedInstr -> IllTypedInstr -> Bool
(IllTypedInstr -> IllTypedInstr -> Bool)
-> (IllTypedInstr -> IllTypedInstr -> Bool) -> Eq IllTypedInstr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IllTypedInstr -> IllTypedInstr -> Bool
$c/= :: IllTypedInstr -> IllTypedInstr -> Bool
== :: IllTypedInstr -> IllTypedInstr -> Bool
$c== :: IllTypedInstr -> IllTypedInstr -> Bool
Eq, (forall x. IllTypedInstr -> Rep IllTypedInstr x)
-> (forall x. Rep IllTypedInstr x -> IllTypedInstr)
-> Generic IllTypedInstr
forall x. Rep IllTypedInstr x -> IllTypedInstr
forall x. IllTypedInstr -> Rep IllTypedInstr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep IllTypedInstr x -> IllTypedInstr
$cfrom :: forall x. IllTypedInstr -> Rep IllTypedInstr x
Generic)
deriving anyclass instance NFData TypeCheckedOp => NFData IllTypedInstr
instance RenderDoc TypeCheckedOp where
renderDoc :: RenderContext -> TypeCheckedOp -> Doc
renderDoc RenderContext
_ (WellTypedOp Instr inp out
instr) = Bool -> [ExpandedOp] -> Doc
forall op. RenderDoc op => Bool -> [op] -> Doc
renderOpsListNoBraces Bool
False (Instr inp out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
Instr inp out -> [ExpandedOp]
instrToOps Instr inp out
instr)
renderDoc RenderContext
pn (IllTypedOp (SemiTypedInstr TypeCheckedInstr
instr)) = RenderContext -> TypeCheckedInstr -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
pn TypeCheckedInstr
instr
renderDoc RenderContext
pn (IllTypedOp (NonTypedInstr ExpandedOp
op)) = RenderContext -> ExpandedOp -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
pn ExpandedOp
op
someInstrToOp :: SomeInstr inp -> TypeCheckedOp
someInstrToOp :: SomeInstr inp -> TypeCheckedOp
someInstrToOp (HST inp
hst :/ SomeInstrOut inp
rest) = case HST inp
hst of
HST inp
SNil -> SomeInstrOut inp -> TypeCheckedOp
forall (inp :: [T]). SingI inp => SomeInstrOut inp -> TypeCheckedOp
go SomeInstrOut inp
rest
(::&){} -> SomeInstrOut inp -> TypeCheckedOp
forall (inp :: [T]). SingI inp => SomeInstrOut inp -> TypeCheckedOp
go SomeInstrOut inp
rest
where
go :: forall inp. SingI inp => SomeInstrOut inp -> TypeCheckedOp
go :: SomeInstrOut inp -> TypeCheckedOp
go (Instr inp out
i ::: HST out
_) = Instr inp out -> TypeCheckedOp
forall (inp :: [T]) (out :: [T]).
(SingI inp, SingI out) =>
Instr inp out -> TypeCheckedOp
WellTypedOp Instr inp out
i
go (AnyOutInstr forall (out :: [T]). Instr inp out
i) = Instr inp '[] -> TypeCheckedOp
forall (inp :: [T]) (out :: [T]).
(SingI inp, SingI out) =>
Instr inp out -> TypeCheckedOp
WellTypedOp (Instr inp '[]
forall (out :: [T]). Instr inp out
i @'[])
$(deriveGADTNFData ''TypeCheckedOp)