module Morley.Michelson.TypeCheck.TypeCheckedOp
( TypeCheckedInstr
, TypeCheckedOp(..)
, IllTypedInstr(..)
, someInstrToOp
, someViewToOp
) where
import Data.Singletons (SingI)
import Morley.Michelson.Printer.Util (RenderDoc(..), renderOpsListNoBraces)
import Morley.Michelson.TypeCheck.Types (HST(..), SomeTcInstr(..), SomeTcInstrOut(..))
import Morley.Michelson.Typed.Aliases
import Morley.Michelson.Typed.Annotation
import Morley.Michelson.Typed.Convert (instrToOps)
import Morley.Michelson.Typed.Instr (Instr, castInstr)
import Morley.Michelson.Typed.View (SomeView'(..), View'(..))
import Morley.Michelson.Untyped qualified as U
import Morley.Michelson.Untyped.Instr (InstrAbstract(..))
import Morley.Util.TH (deriveGADTNFData)
type TypeCheckedInstr op = InstrAbstract (TypeCheckedOp op)
data TypeCheckedOp op where
WellTypedOp :: (SingI inp, SingI out) => Instr inp out -> TypeCheckedOp op
IllTypedOp :: IllTypedInstr op -> TypeCheckedOp op
deriving stock instance Show op => Show (TypeCheckedOp op)
deriving stock instance Functor TypeCheckedOp
instance Eq op => Eq (TypeCheckedOp op) where
WellTypedOp Instr inp out
i1 == :: TypeCheckedOp op -> TypeCheckedOp op -> 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 op
i1 == IllTypedOp IllTypedInstr op
i2 = IllTypedInstr op
i1 IllTypedInstr op -> IllTypedInstr op -> Bool
forall a. Eq a => a -> a -> Bool
== IllTypedInstr op
i2
TypeCheckedOp op
_ == TypeCheckedOp op
_ = Bool
False
data IllTypedInstr op
= SemiTypedInstr (TypeCheckedInstr op)
| NonTypedInstr op
deriving stock (Int -> IllTypedInstr op -> ShowS
[IllTypedInstr op] -> ShowS
IllTypedInstr op -> String
(Int -> IllTypedInstr op -> ShowS)
-> (IllTypedInstr op -> String)
-> ([IllTypedInstr op] -> ShowS)
-> Show (IllTypedInstr op)
forall op. Show op => Int -> IllTypedInstr op -> ShowS
forall op. Show op => [IllTypedInstr op] -> ShowS
forall op. Show op => IllTypedInstr op -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IllTypedInstr op] -> ShowS
$cshowList :: forall op. Show op => [IllTypedInstr op] -> ShowS
show :: IllTypedInstr op -> String
$cshow :: forall op. Show op => IllTypedInstr op -> String
showsPrec :: Int -> IllTypedInstr op -> ShowS
$cshowsPrec :: forall op. Show op => Int -> IllTypedInstr op -> ShowS
Show, IllTypedInstr op -> IllTypedInstr op -> Bool
(IllTypedInstr op -> IllTypedInstr op -> Bool)
-> (IllTypedInstr op -> IllTypedInstr op -> Bool)
-> Eq (IllTypedInstr op)
forall op. Eq op => IllTypedInstr op -> IllTypedInstr op -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IllTypedInstr op -> IllTypedInstr op -> Bool
$c/= :: forall op. Eq op => IllTypedInstr op -> IllTypedInstr op -> Bool
== :: IllTypedInstr op -> IllTypedInstr op -> Bool
$c== :: forall op. Eq op => IllTypedInstr op -> IllTypedInstr op -> Bool
Eq, (forall x. IllTypedInstr op -> Rep (IllTypedInstr op) x)
-> (forall x. Rep (IllTypedInstr op) x -> IllTypedInstr op)
-> Generic (IllTypedInstr op)
forall x. Rep (IllTypedInstr op) x -> IllTypedInstr op
forall x. IllTypedInstr op -> Rep (IllTypedInstr op) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall op x. Rep (IllTypedInstr op) x -> IllTypedInstr op
forall op x. IllTypedInstr op -> Rep (IllTypedInstr op) x
$cto :: forall op x. Rep (IllTypedInstr op) x -> IllTypedInstr op
$cfrom :: forall op x. IllTypedInstr op -> Rep (IllTypedInstr op) x
Generic, (forall a b. (a -> b) -> IllTypedInstr a -> IllTypedInstr b)
-> (forall a b. a -> IllTypedInstr b -> IllTypedInstr a)
-> Functor IllTypedInstr
forall a b. a -> IllTypedInstr b -> IllTypedInstr a
forall a b. (a -> b) -> IllTypedInstr a -> IllTypedInstr b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> IllTypedInstr b -> IllTypedInstr a
$c<$ :: forall a b. a -> IllTypedInstr b -> IllTypedInstr a
fmap :: forall a b. (a -> b) -> IllTypedInstr a -> IllTypedInstr b
$cfmap :: forall a b. (a -> b) -> IllTypedInstr a -> IllTypedInstr b
Functor)
deriving anyclass instance (NFData (TypeCheckedOp op), NFData op) => NFData (IllTypedInstr op)
instance RenderDoc op => RenderDoc (TypeCheckedOp op) where
renderDoc :: RenderContext -> TypeCheckedOp op -> 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 op
instr)) = RenderContext -> TypeCheckedInstr op -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
pn TypeCheckedInstr op
instr
renderDoc RenderContext
pn (IllTypedOp (NonTypedInstr op
op)) = RenderContext -> op -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
pn op
op
someInstrToOp :: SomeTcInstr inp -> TypeCheckedOp op
someInstrToOp :: forall (inp :: [T]) op. SomeTcInstr inp -> TypeCheckedOp op
someInstrToOp (HST inp
hst :/ SomeTcInstrOut inp
rest) = case HST inp
hst of
HST inp
SNil -> SomeTcInstrOut inp -> TypeCheckedOp op
forall (inp :: [T]) op.
SingI inp =>
SomeTcInstrOut inp -> TypeCheckedOp op
go SomeTcInstrOut inp
rest
(::&){} -> SomeTcInstrOut inp -> TypeCheckedOp op
forall (inp :: [T]) op.
SingI inp =>
SomeTcInstrOut inp -> TypeCheckedOp op
go SomeTcInstrOut inp
rest
where
go :: SingI inp => SomeTcInstrOut inp -> TypeCheckedOp op
go :: forall (inp :: [T]) op.
SingI inp =>
SomeTcInstrOut inp -> TypeCheckedOp op
go (Instr inp out
i ::: HST out
_) = Instr inp out -> TypeCheckedOp op
forall (inp :: [T]) (out :: [T]) op.
(SingI inp, SingI out) =>
Instr inp out -> TypeCheckedOp op
WellTypedOp Instr inp out
i
go (AnyOutInstr forall (out :: [T]). Instr inp out
i) = Instr inp '[] -> TypeCheckedOp op
forall (inp :: [T]) (out :: [T]) op.
(SingI inp, SingI out) =>
Instr inp out -> TypeCheckedOp op
WellTypedOp (forall (out :: [T]). Instr inp out
i @'[])
someViewToOp :: SomeView st -> U.View' (TypeCheckedOp op)
someViewToOp :: forall (st :: T) op. SomeView st -> View' (TypeCheckedOp op)
someViewToOp (SomeView View{ViewName
Notes arg
Notes ret
ViewCode' Instr arg st ret
vCode :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewCode' instr arg st ret
vReturn :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> Notes ret
vArgument :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> Notes arg
vName :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewName
vCode :: ViewCode' Instr arg st ret
vReturn :: Notes ret
vArgument :: Notes arg
vName :: ViewName
..}) = View :: forall op. ViewName -> Ty -> Ty -> [op] -> View' op
U.View
{ viewCode :: [TypeCheckedOp op]
U.viewCode = [ViewCode' Instr arg st ret -> TypeCheckedOp op
forall (inp :: [T]) (out :: [T]) op.
(SingI inp, SingI out) =>
Instr inp out -> TypeCheckedOp op
WellTypedOp ViewCode' Instr arg st ret
vCode]
, viewName :: ViewName
U.viewName = ViewName
vName
, viewArgument :: Ty
U.viewArgument = Notes arg -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes arg
vArgument
, viewReturn :: Ty
U.viewReturn = Notes ret -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes ret
vReturn
}
$(deriveGADTNFData ''TypeCheckedOp)