{-# LANGUAGE MagicHash #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Morley.Michelson.Typed.Haskell.Instr.Product
( InstrGetFieldC
, InstrSetFieldC
, InstrConstructC
, instrToField
, instrGetField
, instrGetFieldOpen
, instrSetField
, instrSetFieldOpen
, instrConstruct
, instrConstructStack
, instrDeconstruct
, InstrDeconstructC
, GetFieldType
, GFieldTypes
, GLookupNamed
, ConstructorFieldTypes
, ConstructorFieldNames
, FieldConstructor (..)
, CastFieldConstructors (..)
) where
import Data.Constraint (Bottom(..))
import Data.Vinyl.Core (Rec(..))
import GHC.Exts (Proxy#, proxy#)
import GHC.Generics ((:*:)(..), (:+:)(..))
import GHC.Generics qualified as G
import GHC.TypeLits (ErrorMessage(..), Symbol, TypeError)
import Morley.Michelson.Text
import Morley.Michelson.Typed.Haskell.Instr.Helpers
import Morley.Michelson.Typed.Haskell.Value
import Morley.Michelson.Typed.Instr
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.T (T)
import Morley.Util.Generic
import Morley.Util.Label (Label)
import Morley.Util.Named
import Morley.Util.Type
data LookupNamedResult = LNR Type Path
type family LnrFieldType (lnr :: LookupNamedResult) where
LnrFieldType ('LNR f _) = f
type family LnrBranch (lnr :: LookupNamedResult) :: Path where
LnrBranch ('LNR _ p) = p
type GetNamed name a = LNRequireFound name a (GLookupNamed name (GRep a))
type family LNRequireFound
(name :: Symbol)
(a :: Type)
(mf :: Maybe LookupNamedResult)
:: LookupNamedResult where
LNRequireFound _ _ ('Just lnr) = lnr
LNRequireFound name a 'Nothing = TypeError
('Text "Datatype " ':<>: 'ShowType a ':<>:
'Text " has no field " ':<>: 'ShowType name)
type family GLookupNamed (name :: Symbol) (x :: Type -> Type)
:: Maybe LookupNamedResult where
GLookupNamed name (G.D1 _ x) = GLookupNamed name x
GLookupNamed name (G.C1 _ x) = GLookupNamed name x
GLookupNamed name (G.S1 ('G.MetaSel ('Just recName) _ _ _) (G.Rec0 a)) =
If (name == recName)
('Just $ 'LNR a '[])
'Nothing
GLookupNamed name (G.S1 _ (G.Rec0 (NamedF f a fieldName))) =
If (name == fieldName)
('Just $ 'LNR (NamedInner (NamedF f a fieldName)) '[])
'Nothing
GLookupNamed _ (G.S1 _ _) = 'Nothing
GLookupNamed name (x :*: y) =
LNMergeFound name (GLookupNamed name x) (GLookupNamed name y)
GLookupNamed name (_ :+: _) = TypeError
('Text "Cannot seek for a field " ':<>: 'ShowType name ':<>:
'Text " in sum type")
GLookupNamed _ G.U1 = 'Nothing
GLookupNamed _ G.V1 = TypeError
('Text "Cannot access fields of void-like type")
type family LNMergeFound
(name :: Symbol)
(f1 :: Maybe LookupNamedResult)
(f2 :: Maybe LookupNamedResult)
:: Maybe LookupNamedResult where
LNMergeFound _ 'Nothing 'Nothing = 'Nothing
LNMergeFound _ ('Just ('LNR a p)) 'Nothing = 'Just $ 'LNR a ('L ': p)
LNMergeFound _ 'Nothing ('Just ('LNR a p)) = 'Just $ 'LNR a ('R ': p)
LNMergeFound name ('Just _) ('Just _) = TypeError
('Text "Ambiguous reference to datatype field: " ':<>: 'ShowType name)
type GetFieldType dt name = LnrFieldType (GetNamed name dt)
instrToField
:: forall dt name st.
InstrGetFieldC dt name
=> Label name -> Instr (ToT dt ': st) (ToT (GetFieldType dt name) ': st)
instrToField :: forall dt (name :: Symbol) (st :: [T]).
InstrGetFieldC dt name =>
Label name -> Instr (ToT dt : st) (ToT (GetFieldType dt name) : st)
instrToField Label name
_ =
forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(s :: [T]).
GInstrGet name x path fieldTy =>
Instr (GValueType x : s) (ToT fieldTy : s)
gInstrToField @name @(GRep dt) @(LnrBranch (GetNamed name dt))
@(GetFieldType dt name)
instrGetField
:: forall dt name st.
(InstrGetFieldC dt name, DupableScope (ToT (GetFieldType dt name)))
=> Label name -> Instr (ToT dt ': st) (ToT (GetFieldType dt name) ': ToT dt ': st)
instrGetField :: forall dt (name :: Symbol) (st :: [T]).
(InstrGetFieldC dt name,
DupableScope (ToT (GetFieldType dt name))) =>
Label name
-> Instr (ToT dt : st) (ToT (GetFieldType dt name) : ToT dt : st)
instrGetField = forall dt (name :: Symbol) (res :: T) (st :: [T]).
InstrGetFieldC dt name =>
Instr
'[ToT (GetFieldType dt name)] '[res, ToT (GetFieldType dt name)]
-> Instr '[ToT (GetFieldType dt name)] '[res]
-> Label name
-> Instr (ToT dt : st) (res : ToT dt : st)
instrGetFieldOpen @dt Instr
'[ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))]
'[ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))),
ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))]
Instr
'[ToT (GetFieldType dt name)]
'[ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))),
ToT (GetFieldType dt name)]
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ (a : a : s), DupableScope a) =>
Instr inp out
DUP Instr
'[ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))]
'[ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))]
Instr
'[ToT (GetFieldType dt name)]
'[ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))]
forall (inp :: [T]). Instr inp inp
Nop
instrGetFieldOpen
:: forall dt name res st.
(InstrGetFieldC dt name)
=> Instr '[ToT (GetFieldType dt name)] '[res, ToT (GetFieldType dt name)]
-> Instr '[ToT (GetFieldType dt name)] '[res]
-> Label name
-> Instr (ToT dt ': st) (res ': ToT dt ': st)
instrGetFieldOpen :: forall dt (name :: Symbol) (res :: T) (st :: [T]).
InstrGetFieldC dt name =>
Instr
'[ToT (GetFieldType dt name)] '[res, ToT (GetFieldType dt name)]
-> Instr '[ToT (GetFieldType dt name)] '[res]
-> Label name
-> Instr (ToT dt : st) (res : ToT dt : st)
instrGetFieldOpen Instr
'[ToT (GetFieldType dt name)] '[res, ToT (GetFieldType dt name)]
contWDup Instr '[ToT (GetFieldType dt name)] '[res]
contWoDup Label name
_ =
forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(res :: T) (s :: [T]).
GInstrGet name x path fieldTy =>
Instr '[ToT fieldTy] '[res, ToT fieldTy]
-> Instr '[ToT fieldTy] '[res]
-> Instr (GValueType x : s) (res : GValueType x : s)
gInstrGetFieldOpen @name @(GRep dt) @(LnrBranch (GetNamed name dt))
@(GetFieldType dt name) Instr
'[ToT (GetFieldType dt name)] '[res, ToT (GetFieldType dt name)]
contWDup Instr '[ToT (GetFieldType dt name)] '[res]
contWoDup
type InstrGetFieldC dt name =
( GenericIsoValue dt
, GInstrGet name (GRep dt)
(LnrBranch (GetNamed name dt))
(LnrFieldType (GetNamed name dt))
)
class GIsoValue x =>
GInstrGet
(name :: Symbol)
(x :: Type -> Type)
(path :: Path)
(fieldTy :: Type) where
gInstrToField
:: Instr (GValueType x ': s) (ToT fieldTy ': s)
gInstrGetFieldOpen
:: Instr '[ToT fieldTy] '[res, ToT fieldTy]
-> Instr '[ToT fieldTy] '[res]
-> Instr (GValueType x ': s) (res ': GValueType x ': s)
gTryShortCircuitNonDup
:: forall name x path fieldTy res s.
(GInstrGet name x path fieldTy)
=> Instr '[ToT fieldTy] '[res]
-> Maybe $ Instr (GValueType x ': s) (res ': GValueType x ': s)
gTryShortCircuitNonDup :: forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(res :: T) (s :: [T]).
GInstrGet name x path fieldTy =>
Instr '[ToT fieldTy] '[res]
-> Maybe $ Instr (GValueType x : s) (res : GValueType x : s)
gTryShortCircuitNonDup Instr '[ToT fieldTy] '[res]
cont =
case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(DupableScope $ GValueType x) of
Left{} -> Maybe $ Instr (GValueType x : s) (res : GValueType x : s)
forall a. Maybe a
Nothing
Right Dict (DupableScope $ GValueType x)
Dict -> Instr (GValueType x : s) (res : GValueType x : s)
-> Maybe $ Instr (GValueType x : s) (res : GValueType x : s)
forall a. a -> Maybe a
Just (Instr (GValueType x : s) (res : GValueType x : s)
-> Maybe $ Instr (GValueType x : s) (res : GValueType x : s))
-> Instr (GValueType x : s) (res : GValueType x : s)
-> Maybe $ Instr (GValueType x : s) (res : GValueType x : s)
forall a b. (a -> b) -> a -> b
$
Instr (GValueType x : s) (GValueType x : GValueType x : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ (a : a : s), DupableScope a) =>
Instr inp out
DUP Instr (GValueType x : s) (GValueType x : GValueType x : s)
-> Instr (GValueType x : GValueType x : s) (res : GValueType x : s)
-> Instr (GValueType x : s) (res : GValueType x : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(s :: [T]).
GInstrGet name x path fieldTy =>
Instr (GValueType x : s) (ToT fieldTy : s)
gInstrToField @name @x @path @fieldTy Instr
(GValueType x : GValueType x : s) (ToT fieldTy : GValueType x : s)
-> Instr (ToT fieldTy : GValueType x : s) (res : GValueType x : s)
-> Instr (GValueType x : GValueType x : s) (res : GValueType x : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr '[ToT fieldTy] '[res]
-> Instr
('[ToT fieldTy] ++ (GValueType x : s))
('[res] ++ (GValueType x : s))
forall (s :: [T]) (a :: [T]) (b :: [T]).
Instr a b -> Instr (a ++ s) (b ++ s)
frameInstr Instr '[ToT fieldTy] '[res]
cont
instance GInstrGet name x path f => GInstrGet name (G.M1 t i x) path f where
gInstrToField :: forall (s :: [T]). Instr (GValueType (M1 t i x) : s) (ToT f : s)
gInstrToField = forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(s :: [T]).
GInstrGet name x path fieldTy =>
Instr (GValueType x : s) (ToT fieldTy : s)
gInstrToField @name @x @path @f
gInstrGetFieldOpen :: forall (res :: T) (s :: [T]).
Instr '[ToT f] '[res, ToT f]
-> Instr '[ToT f] '[res]
-> Instr
(GValueType (M1 t i x) : s) (res : GValueType (M1 t i x) : s)
gInstrGetFieldOpen = forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(res :: T) (s :: [T]).
GInstrGet name x path fieldTy =>
Instr '[ToT fieldTy] '[res, ToT fieldTy]
-> Instr '[ToT fieldTy] '[res]
-> Instr (GValueType x : s) (res : GValueType x : s)
gInstrGetFieldOpen @name @x @path @f
instance (IsoValue f, ToT f ~ ToT f') =>
GInstrGet name (G.Rec0 f) '[] f' where
gInstrToField :: forall (s :: [T]). Instr (GValueType (Rec0 f) : s) (ToT f' : s)
gInstrToField = Instr (GValueType (Rec0 f) : s) (ToT f' : s)
Instr (ToT f' : s) (ToT f' : s)
forall (inp :: [T]). Instr inp inp
Nop
gInstrGetFieldOpen :: forall (res :: T) (s :: [T]).
Instr '[ToT f'] '[res, ToT f']
-> Instr '[ToT f'] '[res]
-> Instr (GValueType (Rec0 f) : s) (res : GValueType (Rec0 f) : s)
gInstrGetFieldOpen Instr '[ToT f'] '[res, ToT f']
contWDup Instr '[ToT f'] '[res]
_ = Instr '[ToT f'] '[res, ToT f']
-> Instr ('[ToT f'] ++ s) ('[res, ToT f'] ++ s)
forall (s :: [T]) (a :: [T]) (b :: [T]).
Instr a b -> Instr (a ++ s) (b ++ s)
frameInstr Instr '[ToT f'] '[res, ToT f']
contWDup
instance (GInstrGet name x path f, GIsoValue y) => GInstrGet name (x :*: y) ('L ': path) f where
gInstrToField :: forall (s :: [T]). Instr (GValueType (x :*: y) : s) (ToT f : s)
gInstrToField = Instr ('TPair (GValueType x) (GValueType y) : s) (GValueType x : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : s)) =>
Instr inp out
CAR Instr ('TPair (GValueType x) (GValueType y) : s) (GValueType x : s)
-> Instr (GValueType x : s) (ToT f : s)
-> Instr ('TPair (GValueType x) (GValueType y) : s) (ToT f : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(s :: [T]).
GInstrGet name x path fieldTy =>
Instr (GValueType x : s) (ToT fieldTy : s)
gInstrToField @name @x @path @f
gInstrGetFieldOpen :: forall (res :: T) (s :: [T]).
Instr '[ToT f] '[res, ToT f]
-> Instr '[ToT f] '[res]
-> Instr
(GValueType (x :*: y) : s) (res : GValueType (x :*: y) : s)
gInstrGetFieldOpen Instr '[ToT f] '[res, ToT f]
contWDup Instr '[ToT f] '[res]
contWoDup =
forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(res :: T) (s :: [T]).
GInstrGet name x path fieldTy =>
Instr '[ToT fieldTy] '[res]
-> Maybe $ Instr (GValueType x : s) (res : GValueType x : s)
gTryShortCircuitNonDup @name @(x :*: y) @('L ': path) @f Instr '[ToT f] '[res]
contWoDup Maybe
(Instr
('TPair (GValueType x) (GValueType y) : s)
(res : 'TPair (GValueType x) (GValueType y) : s))
-> Instr
('TPair (GValueType x) (GValueType y) : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
-> Instr
('TPair (GValueType x) (GValueType y) : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
forall a. Maybe a -> a -> a
?:
Instr
('TPair (GValueType x) (GValueType y) : s)
(GValueType x : GValueType y : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : b : s)) =>
Instr inp out
UNPAIR
Instr
('TPair (GValueType x) (GValueType y) : s)
(GValueType x : GValueType y : s)
-> Instr
(GValueType x : GValueType y : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
-> Instr
('TPair (GValueType x) (GValueType y) : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(res :: T) (s :: [T]).
GInstrGet name x path fieldTy =>
Instr '[ToT fieldTy] '[res, ToT fieldTy]
-> Instr '[ToT fieldTy] '[res]
-> Instr (GValueType x : s) (res : GValueType x : s)
gInstrGetFieldOpen @name @x @path @f Instr '[ToT f] '[res, ToT f]
contWDup Instr '[ToT f] '[res]
contWoDup
Instr
(GValueType x : GValueType y : s)
(res : GValueType x : GValueType y : s)
-> Instr
(res : GValueType x : GValueType y : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
-> Instr
(GValueType x : GValueType y : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr
(GValueType x : GValueType y : s)
('TPair (GValueType x) (GValueType y) : s)
-> Instr
(res : GValueType x : GValueType y : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr
(GValueType x : GValueType y : s)
('TPair (GValueType x) (GValueType y) : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR
instance (GInstrGet name y path f, GIsoValue x) => GInstrGet name (x :*: y) ('R ': path) f where
gInstrToField :: forall (s :: [T]). Instr (GValueType (x :*: y) : s) (ToT f : s)
gInstrToField = Instr ('TPair (GValueType x) (GValueType y) : s) (GValueType y : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (b : s)) =>
Instr inp out
CDR Instr ('TPair (GValueType x) (GValueType y) : s) (GValueType y : s)
-> Instr (GValueType y : s) (ToT f : s)
-> Instr ('TPair (GValueType x) (GValueType y) : s) (ToT f : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(s :: [T]).
GInstrGet name x path fieldTy =>
Instr (GValueType x : s) (ToT fieldTy : s)
gInstrToField @name @y @path @f
gInstrGetFieldOpen :: forall (res :: T) (s :: [T]).
Instr '[ToT f] '[res, ToT f]
-> Instr '[ToT f] '[res]
-> Instr
(GValueType (x :*: y) : s) (res : GValueType (x :*: y) : s)
gInstrGetFieldOpen Instr '[ToT f] '[res, ToT f]
contWDup Instr '[ToT f] '[res]
contWoDup =
forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(res :: T) (s :: [T]).
GInstrGet name x path fieldTy =>
Instr '[ToT fieldTy] '[res]
-> Maybe $ Instr (GValueType x : s) (res : GValueType x : s)
gTryShortCircuitNonDup @name @(x :*: y) @('R ': path) @f Instr '[ToT f] '[res]
contWoDup Maybe
(Instr
('TPair (GValueType x) (GValueType y) : s)
(res : 'TPair (GValueType x) (GValueType y) : s))
-> Instr
('TPair (GValueType x) (GValueType y) : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
-> Instr
('TPair (GValueType x) (GValueType y) : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
forall a. Maybe a -> a -> a
?:
Instr
('TPair (GValueType x) (GValueType y) : s)
(GValueType x : GValueType y : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : b : s)) =>
Instr inp out
UNPAIR Instr
('TPair (GValueType x) (GValueType y) : s)
(GValueType x : GValueType y : s)
-> Instr
(GValueType x : GValueType y : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
-> Instr
('TPair (GValueType x) (GValueType y) : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr
(GValueType x : GValueType y : s) (GValueType y : GValueType x : s)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP
Instr
(GValueType x : GValueType y : s) (GValueType y : GValueType x : s)
-> Instr
(GValueType y : GValueType x : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
-> Instr
(GValueType x : GValueType y : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(res :: T) (s :: [T]).
GInstrGet name x path fieldTy =>
Instr '[ToT fieldTy] '[res, ToT fieldTy]
-> Instr '[ToT fieldTy] '[res]
-> Instr (GValueType x : s) (res : GValueType x : s)
gInstrGetFieldOpen @name @y @path @f Instr '[ToT f] '[res, ToT f]
contWDup Instr '[ToT f] '[res]
contWoDup
Instr
(GValueType y : GValueType x : s)
(res : GValueType y : GValueType x : s)
-> Instr
(res : GValueType y : GValueType x : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
-> Instr
(GValueType y : GValueType x : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr
(GValueType y : GValueType x : s)
('TPair (GValueType x) (GValueType y) : s)
-> Instr
(res : GValueType y : GValueType x : s)
(res : 'TPair (GValueType x) (GValueType y) : s)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP (Instr
(GValueType y : GValueType x : s) (GValueType x : GValueType y : s)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP Instr
(GValueType y : GValueType x : s) (GValueType x : GValueType y : s)
-> Instr
(GValueType x : GValueType y : s)
('TPair (GValueType x) (GValueType y) : s)
-> Instr
(GValueType y : GValueType x : s)
('TPair (GValueType x) (GValueType y) : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr
(GValueType x : GValueType y : s)
('TPair (GValueType x) (GValueType y) : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR)
type MyType1 = ("int" :! Integer, "bytes" :! ByteString, "bytes2" :? ByteString)
_getIntInstr1 :: Instr (ToT MyType1 ': s) (ToT Integer ': s)
_getIntInstr1 :: forall (s :: [T]). Instr (ToT MyType1 : s) (ToT Integer : s)
_getIntInstr1 = forall dt (name :: Symbol) (st :: [T]).
InstrGetFieldC dt name =>
Label name -> Instr (ToT dt : st) (ToT (GetFieldType dt name) : st)
instrToField @MyType1 Label "int"
#int
_getTextInstr1 :: Instr (ToT MyType1 ': s) (ToT (Maybe ByteString) ': s)
_getTextInstr1 :: forall (s :: [T]).
Instr (ToT MyType1 : s) (ToT (Maybe ByteString) : s)
_getTextInstr1 = forall dt (name :: Symbol) (st :: [T]).
InstrGetFieldC dt name =>
Label name -> Instr (ToT dt : st) (ToT (GetFieldType dt name) : st)
instrToField @MyType1 Label "bytes2"
#bytes2
data MyType2 = MyType2
{ MyType2 -> Integer
getInt :: Integer
, MyType2 -> MText
getText :: MText
, MyType2 -> ()
getUnit :: ()
, MyType2 -> MyType1
getMyType1 :: MyType1
} deriving stock ((forall x. MyType2 -> Rep MyType2 x)
-> (forall x. Rep MyType2 x -> MyType2) -> Generic MyType2
forall x. Rep MyType2 x -> MyType2
forall x. MyType2 -> Rep MyType2 x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MyType2 -> Rep MyType2 x
from :: forall x. MyType2 -> Rep MyType2 x
$cto :: forall x. Rep MyType2 x -> MyType2
to :: forall x. Rep MyType2 x -> MyType2
Generic)
deriving anyclass (WellTypedToT MyType2
WellTypedToT MyType2
-> (MyType2 -> Value (ToT MyType2))
-> (Value (ToT MyType2) -> MyType2)
-> IsoValue MyType2
Value (ToT MyType2) -> MyType2
MyType2 -> Value (ToT MyType2)
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
$ctoVal :: MyType2 -> Value (ToT MyType2)
toVal :: MyType2 -> Value (ToT MyType2)
$cfromVal :: Value (ToT MyType2) -> MyType2
fromVal :: Value (ToT MyType2) -> MyType2
IsoValue)
_getIntInstr2 :: Instr (ToT MyType2 ': s) (ToT () ': s)
_getIntInstr2 :: forall (s :: [T]). Instr (ToT MyType2 : s) (ToT () : s)
_getIntInstr2 = forall dt (name :: Symbol) (st :: [T]).
InstrGetFieldC dt name =>
Label name -> Instr (ToT dt : st) (ToT (GetFieldType dt name) : st)
instrToField @MyType2 Label "getUnit"
#getUnit
_getIntInstr2' :: Instr (ToT MyType2 ': s) (ToT Integer ': s)
_getIntInstr2' :: forall (s :: [T]). Instr (ToT MyType2 : s) (ToT Integer : s)
_getIntInstr2' =
forall dt (name :: Symbol) (st :: [T]).
InstrGetFieldC dt name =>
Label name -> Instr (ToT dt : st) (ToT (GetFieldType dt name) : st)
instrToField @MyType2 Label "getMyType1"
#getMyType1 Instr
('TPair
('TPair 'TInt 'TString)
('TPair 'TUnit ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes))))
: s)
(ToT
(LnrFieldType
(LNRequireFound
"getMyType1"
MyType2
(LNMergeFound
"getMyType1"
(LNMergeFound
"getMyType1"
(If ("getMyType1" == "getInt") ('Just $ 'LNR Integer '[]) 'Nothing)
(If ("getMyType1" == "getText") ('Just $ 'LNR MText '[]) 'Nothing))
(LNMergeFound
"getMyType1"
(If ("getMyType1" == "getUnit") ('Just $ 'LNR () '[]) 'Nothing)
(If
("getMyType1" == "getMyType1")
('Just $ 'LNR MyType1 '[])
'Nothing)))))
: s)
-> Instr
(ToT
(LnrFieldType
(LNRequireFound
"getMyType1"
MyType2
(LNMergeFound
"getMyType1"
(LNMergeFound
"getMyType1"
(If ("getMyType1" == "getInt") ('Just $ 'LNR Integer '[]) 'Nothing)
(If ("getMyType1" == "getText") ('Just $ 'LNR MText '[]) 'Nothing))
(LNMergeFound
"getMyType1"
(If ("getMyType1" == "getUnit") ('Just $ 'LNR () '[]) 'Nothing)
(If
("getMyType1" == "getMyType1")
('Just $ 'LNR MyType1 '[])
'Nothing)))))
: s)
('TInt : s)
-> Instr
('TPair
('TPair 'TInt 'TString)
('TPair 'TUnit ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes))))
: s)
('TInt : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` forall dt (name :: Symbol) (st :: [T]).
InstrGetFieldC dt name =>
Label name -> Instr (ToT dt : st) (ToT (GetFieldType dt name) : st)
instrToField @MyType1 Label "int"
#int
instrSetField
:: forall dt name st.
InstrSetFieldC dt name
=> Label name -> Instr (ToT (GetFieldType dt name) ': ToT dt ': st) (ToT dt ': st)
instrSetField :: forall dt (name :: Symbol) (st :: [T]).
InstrSetFieldC dt name =>
Label name
-> Instr (ToT (GetFieldType dt name) : ToT dt : st) (ToT dt : st)
instrSetField =
forall dt (name :: Symbol) (new :: T) (st :: [T]).
InstrSetFieldC dt name =>
Instr
'[new, ToT (GetFieldType dt name)] '[ToT (GetFieldType dt name)]
-> Label name -> Instr (new : ToT dt : st) (ToT dt : st)
instrSetFieldOpen @dt (Instr
'[ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))]
'[]
-> Instr
'[ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))),
ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))]
'[ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))]
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr
'[ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))]
'[]
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP)
instrSetFieldOpen
:: forall dt name new st.
InstrSetFieldC dt name
=> Instr '[new, ToT (GetFieldType dt name)] '[ToT (GetFieldType dt name)]
-> Label name
-> Instr (new ': ToT dt ': st) (ToT dt ': st)
instrSetFieldOpen :: forall dt (name :: Symbol) (new :: T) (st :: [T]).
InstrSetFieldC dt name =>
Instr
'[new, ToT (GetFieldType dt name)] '[ToT (GetFieldType dt name)]
-> Label name -> Instr (new : ToT dt : st) (ToT dt : st)
instrSetFieldOpen Instr
'[new, ToT (GetFieldType dt name)] '[ToT (GetFieldType dt name)]
cont Label name
_ =
forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(new :: T) (s :: [T]).
GInstrSetField name x path fieldTy =>
Instr '[new, ToT fieldTy] '[ToT fieldTy]
-> Instr (new : GValueType x : s) (GValueType x : s)
gInstrSetFieldOpen @name @(GRep dt) @(LnrBranch (GetNamed name dt))
@(GetFieldType dt name) Instr
'[new, ToT (GetFieldType dt name)] '[ToT (GetFieldType dt name)]
cont
type InstrSetFieldC dt name =
( GenericIsoValue dt
, GInstrSetField name (GRep dt)
(LnrBranch (GetNamed name dt))
(LnrFieldType (GetNamed name dt))
)
class GIsoValue x =>
GInstrSetField
(name :: Symbol)
(x :: Type -> Type)
(path :: Path)
(fieldTy :: Type) where
gInstrSetFieldOpen
:: Instr '[new, ToT fieldTy] '[ToT fieldTy]
-> Instr (new ': GValueType x ': s) (GValueType x ': s)
instance GInstrSetField name x path f => GInstrSetField name (G.M1 t i x) path f where
gInstrSetFieldOpen :: forall (new :: T) (s :: [T]).
Instr '[new, ToT f] '[ToT f]
-> Instr
(new : GValueType (M1 t i x) : s) (GValueType (M1 t i x) : s)
gInstrSetFieldOpen = forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(new :: T) (s :: [T]).
GInstrSetField name x path fieldTy =>
Instr '[new, ToT fieldTy] '[ToT fieldTy]
-> Instr (new : GValueType x : s) (GValueType x : s)
gInstrSetFieldOpen @name @x @path @f
instance (IsoValue f, ToT f ~ ToT f') =>
GInstrSetField name (G.Rec0 f) '[] f' where
gInstrSetFieldOpen :: forall (new :: T) (s :: [T]).
Instr '[new, ToT f'] '[ToT f']
-> Instr (new : GValueType (Rec0 f) : s) (GValueType (Rec0 f) : s)
gInstrSetFieldOpen Instr '[new, ToT f'] '[ToT f']
cont = Instr '[new, ToT f'] '[ToT f']
-> Instr ('[new, ToT f'] ++ s) ('[ToT f'] ++ s)
forall (s :: [T]) (a :: [T]) (b :: [T]).
Instr a b -> Instr (a ++ s) (b ++ s)
frameInstr Instr '[new, ToT f'] '[ToT f']
cont
instance (GInstrSetField name x path f, GIsoValue y) => GInstrSetField name (x :*: y) ('L ': path) f where
gInstrSetFieldOpen :: forall (new :: T) (s :: [T]).
Instr '[new, ToT f] '[ToT f]
-> Instr
(new : GValueType (x :*: y) : s) (GValueType (x :*: y) : s)
gInstrSetFieldOpen Instr '[new, ToT f] '[ToT f]
cont =
Instr
('TPair (GValueType x) (GValueType y) : s)
(GValueType x : GValueType y : s)
-> Instr
(new : 'TPair (GValueType x) (GValueType y) : s)
(new : GValueType x : GValueType y : s)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr
('TPair (GValueType x) (GValueType y) : s)
(GValueType x : GValueType y : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : b : s)) =>
Instr inp out
UNPAIR Instr
(new : 'TPair (GValueType x) (GValueType y) : s)
(new : GValueType x : GValueType y : s)
-> Instr
(new : GValueType x : GValueType y : s)
('TPair (GValueType x) (GValueType y) : s)
-> Instr
(new : 'TPair (GValueType x) (GValueType y) : s)
('TPair (GValueType x) (GValueType y) : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq`
forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(new :: T) (s :: [T]).
GInstrSetField name x path fieldTy =>
Instr '[new, ToT fieldTy] '[ToT fieldTy]
-> Instr (new : GValueType x : s) (GValueType x : s)
gInstrSetFieldOpen @name @x @path @f Instr '[new, ToT f] '[ToT f]
cont Instr
(new : GValueType x : GValueType y : s)
(GValueType x : GValueType y : s)
-> Instr
(GValueType x : GValueType y : s)
('TPair (GValueType x) (GValueType y) : s)
-> Instr
(new : GValueType x : GValueType y : s)
('TPair (GValueType x) (GValueType y) : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq`
Instr
(GValueType x : GValueType y : s)
('TPair (GValueType x) (GValueType y) : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR
instance (GInstrSetField name y path f, GIsoValue x) => GInstrSetField name (x :*: y) ('R ': path) f where
gInstrSetFieldOpen :: forall (new :: T) (s :: [T]).
Instr '[new, ToT f] '[ToT f]
-> Instr
(new : GValueType (x :*: y) : s) (GValueType (x :*: y) : s)
gInstrSetFieldOpen Instr '[new, ToT f] '[ToT f]
cont =
Instr
('TPair (GValueType x) (GValueType y) : s)
(GValueType y : GValueType x : s)
-> Instr
(new : 'TPair (GValueType x) (GValueType y) : s)
(new : GValueType y : GValueType x : s)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP (Instr
('TPair (GValueType x) (GValueType y) : s)
(GValueType x : GValueType y : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : b : s)) =>
Instr inp out
UNPAIR Instr
('TPair (GValueType x) (GValueType y) : s)
(GValueType x : GValueType y : s)
-> Instr
(GValueType x : GValueType y : s) (GValueType y : GValueType x : s)
-> Instr
('TPair (GValueType x) (GValueType y) : s)
(GValueType y : GValueType x : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr
(GValueType x : GValueType y : s) (GValueType y : GValueType x : s)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP) Instr
(new : 'TPair (GValueType x) (GValueType y) : s)
(new : GValueType y : GValueType x : s)
-> Instr
(new : GValueType y : GValueType x : s)
('TPair (GValueType x) (GValueType y) : s)
-> Instr
(new : 'TPair (GValueType x) (GValueType y) : s)
('TPair (GValueType x) (GValueType y) : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq`
forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
(new :: T) (s :: [T]).
GInstrSetField name x path fieldTy =>
Instr '[new, ToT fieldTy] '[ToT fieldTy]
-> Instr (new : GValueType x : s) (GValueType x : s)
gInstrSetFieldOpen @name @y @path @f Instr '[new, ToT f] '[ToT f]
cont Instr
(new : GValueType y : GValueType x : s)
(GValueType y : GValueType x : s)
-> Instr
(GValueType y : GValueType x : s)
('TPair (GValueType x) (GValueType y) : s)
-> Instr
(new : GValueType y : GValueType x : s)
('TPair (GValueType x) (GValueType y) : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq`
Instr
(GValueType y : GValueType x : s) (GValueType x : GValueType y : s)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP Instr
(GValueType y : GValueType x : s) (GValueType x : GValueType y : s)
-> Instr
(GValueType x : GValueType y : s)
('TPair (GValueType x) (GValueType y) : s)
-> Instr
(GValueType y : GValueType x : s)
('TPair (GValueType x) (GValueType y) : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr
(GValueType x : GValueType y : s)
('TPair (GValueType x) (GValueType y) : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR
_setIntInstr1 :: Instr (ToT Integer ': ToT MyType2 ': s) (ToT MyType2 ': s)
_setIntInstr1 :: forall (s :: [T]).
Instr (ToT Integer : ToT MyType2 : s) (ToT MyType2 : s)
_setIntInstr1 = forall dt (name :: Symbol) (st :: [T]).
InstrSetFieldC dt name =>
Label name
-> Instr (ToT (GetFieldType dt name) : ToT dt : st) (ToT dt : st)
instrSetField @MyType2 Label "getInt"
#getInt
newtype FieldConstructor (st :: [k]) (field :: Type) =
FieldConstructor (Instr (ToTs' st) (ToT field ': ToTs' st))
class ToTs xs ~ ToTs ys => CastFieldConstructors xs ys where
castFieldConstructorsImpl :: Rec (FieldConstructor st) xs -> Rec (FieldConstructor st) ys
instance CastFieldConstructors '[] '[] where
castFieldConstructorsImpl :: forall {k} (st :: [k]).
Rec (FieldConstructor st) '[] -> Rec (FieldConstructor st) '[]
castFieldConstructorsImpl Rec (FieldConstructor st) '[]
RNil = Rec (FieldConstructor st) '[]
forall {u} (a :: u -> *). Rec a '[]
RNil
instance (CastFieldConstructors xs ys, ToTs xs ~ ToTs ys, ToT x ~ ToT y)
=> CastFieldConstructors (x ': xs) (y ': ys) where
castFieldConstructorsImpl :: forall {k} (st :: [k]).
Rec (FieldConstructor st) (x : xs)
-> Rec (FieldConstructor st) (y : ys)
castFieldConstructorsImpl (FieldConstructor Instr (ToTs' st) (ToT r : ToTs' st)
fctr :& Rec (FieldConstructor st) rs
xs) =
Instr (ToTs' st) (ToT y : ToTs' st) -> FieldConstructor st y
forall k (st :: [k]) field.
Instr (ToTs' st) (ToT field : ToTs' st)
-> FieldConstructor st field
FieldConstructor Instr (ToTs' st) (ToT y : ToTs' st)
Instr (ToTs' st) (ToT r : ToTs' st)
fctr FieldConstructor st y
-> Rec (FieldConstructor st) ys
-> Rec (FieldConstructor st) (y : ys)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& (forall (xs :: [*]) (ys :: [*]) {k} (st :: [k]).
CastFieldConstructors xs ys =>
Rec (FieldConstructor st) xs -> Rec (FieldConstructor st) ys
castFieldConstructorsImpl @xs @ys Rec (FieldConstructor st) xs
Rec (FieldConstructor st) rs
xs)
instrConstruct
:: forall dt st. InstrConstructC dt
=> Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> Instr st (ToT dt ': st)
instrConstruct :: forall dt (st :: [T]).
InstrConstructC dt =>
Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> Instr st (ToT dt : st)
instrConstruct = (Instr st (GValueType (Rep dt) : st),
Rec (FieldConstructor st) '[])
-> Instr st (GValueType (Rep dt) : st)
forall a b. (a, b) -> a
fst ((Instr st (GValueType (Rep dt) : st),
Rec (FieldConstructor st) '[])
-> Instr st (GValueType (Rep dt) : st))
-> (Rec (FieldConstructor st) (GFieldTypes (Rep dt) '[])
-> (Instr st (GValueType (Rep dt) : st),
Rec (FieldConstructor st) '[]))
-> Rec (FieldConstructor st) (GFieldTypes (Rep dt) '[])
-> Instr st (GValueType (Rep dt) : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (x :: * -> *) (rest :: [*]) (st :: [T]).
GInstrConstruct x rest =>
Rec (FieldConstructor st) (GFieldTypes x rest)
-> (Instr st (GValueType x : st), Rec (FieldConstructor st) rest)
gInstrConstruct @(GRep dt) @'[]
instrConstructStack
:: forall dt stack st .
( InstrConstructC dt
, stack ~ ToTs (ConstructorFieldTypes dt)
)
=> Instr (stack ++ st) (ToT dt ': st)
instrConstructStack :: forall dt (stack :: [T]) (st :: [T]).
(InstrConstructC dt, stack ~ ToTs (ConstructorFieldTypes dt)) =>
Instr (stack ++ st) (ToT dt : st)
instrConstructStack = forall (x :: * -> *) (rest :: [*]) (end :: [T]).
GInstrConstruct x rest =>
Proxy# end
-> Instr
(ToTs (GFieldTypes x rest) ++ end)
(GValueType x : (ToTs rest ++ end))
gInstrConstructStack @(GRep dt) @'[] (forall (a :: [T]). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @st)
type ConstructorFieldTypes dt = GFieldTypes (GRep dt) '[]
type ConstructorFieldNames dt = GFieldNames (GRep dt)
type InstrConstructC dt = (GenericIsoValue dt, GInstrConstruct (GRep dt) '[])
type family GFieldNames x :: [Symbol] where
GFieldNames (G.D1 _ x) = GFieldNames x
GFieldNames (G.C1 _ x) = GFieldNames x
GFieldNames (x :*: y) = GFieldNames x ++ GFieldNames y
GFieldNames (G.S1 ('G.MetaSel ('Just fieldName) _ _ _) _) = '[fieldName]
GFieldNames (G.S1 _ (G.Rec0 (NamedF _ _ fieldName))) = '[fieldName]
GFieldNames (G.S1 ('G.MetaSel _ _ _ _) _) = TypeError ('Text "All fields have to be named")
GFieldNames (_ :+: _) = TypeError ('Text "Cannot get field names of sum type")
GFieldNames G.V1 = TypeError ('Text "Must be at least one constructor")
class GInstrConstruct (x :: Type -> Type) (rest :: [Type]) where
type GFieldTypes x rest :: [Type]
gInstrConstruct
:: Rec (FieldConstructor st) (GFieldTypes x rest)
-> (Instr st (GValueType x ': st), Rec (FieldConstructor st) rest)
gInstrConstructStack :: Proxy# end -> Instr (ToTs (GFieldTypes x rest) ++ end)
(GValueType x ': ToTs rest ++ end)
instance GInstrConstruct x rest => GInstrConstruct (G.M1 t i x) rest where
type GFieldTypes (G.M1 t i x) rest = GFieldTypes x rest
gInstrConstruct :: forall (st :: [T]).
Rec (FieldConstructor st) (GFieldTypes (M1 t i x) rest)
-> (Instr st (GValueType (M1 t i x) : st),
Rec (FieldConstructor st) rest)
gInstrConstruct = forall (x :: * -> *) (rest :: [*]) (st :: [T]).
GInstrConstruct x rest =>
Rec (FieldConstructor st) (GFieldTypes x rest)
-> (Instr st (GValueType x : st), Rec (FieldConstructor st) rest)
gInstrConstruct @x @rest
gInstrConstructStack :: forall (end :: [T]).
Proxy# end
-> Instr
(ToTs (GFieldTypes (M1 t i x) rest) ++ end)
(GValueType (M1 t i x) : (ToTs rest ++ end))
gInstrConstructStack Proxy# end
p = forall (x :: * -> *) (rest :: [*]) (end :: [T]).
GInstrConstruct x rest =>
Proxy# end
-> Instr
(ToTs (GFieldTypes x rest) ++ end)
(GValueType x : (ToTs rest ++ end))
gInstrConstructStack @x @rest Proxy# end
p
instance ( GInstrConstruct x (GFieldTypes y rest), GInstrConstruct y rest
) => GInstrConstruct (x :*: y) rest where
type GFieldTypes (x :*: y) rest = GFieldTypes x (GFieldTypes y rest)
gInstrConstruct :: forall (st :: [T]).
Rec (FieldConstructor st) (GFieldTypes (x :*: y) rest)
-> (Instr st (GValueType (x :*: y) : st),
Rec (FieldConstructor st) rest)
gInstrConstruct Rec (FieldConstructor st) (GFieldTypes (x :*: y) rest)
fs
| (Instr st (GValueType x : st)
linstr, Rec (FieldConstructor st) (GFieldTypes y rest)
rest) <- forall (x :: * -> *) (rest :: [*]) (st :: [T]).
GInstrConstruct x rest =>
Rec (FieldConstructor st) (GFieldTypes x rest)
-> (Instr st (GValueType x : st), Rec (FieldConstructor st) rest)
gInstrConstruct @x @(GFieldTypes y rest) Rec (FieldConstructor st) (GFieldTypes x (GFieldTypes y rest))
Rec (FieldConstructor st) (GFieldTypes (x :*: y) rest)
fs
, (Instr st (GValueType y : st)
rinstr, Rec (FieldConstructor st) rest
rest') <- forall (x :: * -> *) (rest :: [*]) (st :: [T]).
GInstrConstruct x rest =>
Rec (FieldConstructor st) (GFieldTypes x rest)
-> (Instr st (GValueType x : st), Rec (FieldConstructor st) rest)
gInstrConstruct @y @rest Rec (FieldConstructor st) (GFieldTypes y rest)
rest
= (Instr st (GValueType x : st)
linstr Instr st (GValueType x : st)
-> Instr
(GValueType x : st) ('TPair (GValueType x) (GValueType y) : st)
-> Instr st ('TPair (GValueType x) (GValueType y) : st)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr st (GValueType y : st)
-> Instr (GValueType x : st) (GValueType x : GValueType y : st)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr st (GValueType y : st)
rinstr Instr (GValueType x : st) (GValueType x : GValueType y : st)
-> Instr
(GValueType x : GValueType y : st)
('TPair (GValueType x) (GValueType y) : st)
-> Instr
(GValueType x : st) ('TPair (GValueType x) (GValueType y) : st)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr
(GValueType x : GValueType y : st)
('TPair (GValueType x) (GValueType y) : st)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR, Rec (FieldConstructor st) rest
rest')
gInstrConstructStack :: forall (end :: [T]).
Proxy# end
-> Instr
(ToTs (GFieldTypes (x :*: y) rest) ++ end)
(GValueType (x :*: y) : (ToTs rest ++ end))
gInstrConstructStack Proxy# end
p =
let linstr :: Instr
(ToTs (GFieldTypes x (GFieldTypes y rest)) ++ end)
(GValueType x : (ToTs (GFieldTypes y rest) ++ end))
linstr = forall (x :: * -> *) (rest :: [*]) (end :: [T]).
GInstrConstruct x rest =>
Proxy# end
-> Instr
(ToTs (GFieldTypes x rest) ++ end)
(GValueType x : (ToTs rest ++ end))
gInstrConstructStack @x @(GFieldTypes y rest) Proxy# end
p
rinstr :: Instr
(ToTs (GFieldTypes y rest) ++ end)
(GValueType y : (ToTs rest ++ end))
rinstr = forall (x :: * -> *) (rest :: [*]) (end :: [T]).
GInstrConstruct x rest =>
Proxy# end
-> Instr
(ToTs (GFieldTypes x rest) ++ end)
(GValueType x : (ToTs rest ++ end))
gInstrConstructStack @y @rest Proxy# end
p
in Instr
(ToTs (GFieldTypes x (GFieldTypes y rest)) ++ end)
(GValueType x : (ToTs (GFieldTypes y rest) ++ end))
linstr Instr
(ToTs (GFieldTypes x (GFieldTypes y rest)) ++ end)
(GValueType x : (ToTs (GFieldTypes y rest) ++ end))
-> Instr
(GValueType x : (ToTs (GFieldTypes y rest) ++ end))
('TPair (GValueType x) (GValueType y) : (ToTs rest ++ end))
-> Instr
(ToTs (GFieldTypes x (GFieldTypes y rest)) ++ end)
('TPair (GValueType x) (GValueType y) : (ToTs rest ++ end))
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr
(ToTs (GFieldTypes y rest) ++ end)
(GValueType y : (ToTs rest ++ end))
-> Instr
(GValueType x : (ToTs (GFieldTypes y rest) ++ end))
(GValueType x : GValueType y : (ToTs rest ++ end))
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr
(ToTs (GFieldTypes y rest) ++ end)
(GValueType y : (ToTs rest ++ end))
rinstr Instr
(GValueType x : (ToTs (GFieldTypes y rest) ++ end))
(GValueType x : GValueType y : (ToTs rest ++ end))
-> Instr
(GValueType x : GValueType y : (ToTs rest ++ end))
('TPair (GValueType x) (GValueType y) : (ToTs rest ++ end))
-> Instr
(GValueType x : (ToTs (GFieldTypes y rest) ++ end))
('TPair (GValueType x) (GValueType y) : (ToTs rest ++ end))
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr
(GValueType x : GValueType y : (ToTs rest ++ end))
('TPair (GValueType x) (GValueType y) : (ToTs rest ++ end))
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR
instance GInstrConstruct G.U1 rest where
type GFieldTypes G.U1 rest = rest
gInstrConstruct :: forall (st :: [T]).
Rec (FieldConstructor st) (GFieldTypes U1 rest)
-> (Instr st (GValueType U1 : st), Rec (FieldConstructor st) rest)
gInstrConstruct Rec (FieldConstructor st) (GFieldTypes U1 rest)
rest = (Instr st ('TUnit : st)
Instr st (GValueType U1 : st)
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TUnit : s)) =>
Instr inp out
UNIT, Rec (FieldConstructor st) rest
Rec (FieldConstructor st) (GFieldTypes U1 rest)
rest)
gInstrConstructStack :: forall (end :: [T]).
Proxy# end
-> Instr
(ToTs (GFieldTypes U1 rest) ++ end)
(GValueType U1 : (ToTs rest ++ end))
gInstrConstructStack Proxy# end
_ = Instr (ToTs rest ++ end) ('TUnit : (ToTs rest ++ end))
Instr
(ToTs (GFieldTypes U1 rest) ++ end)
(GValueType U1 : (ToTs rest ++ end))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TUnit : s)) =>
Instr inp out
UNIT
instance ( TypeError ('Text "Cannot construct sum type")
, Bottom
) => GInstrConstruct (x :+: y) rest where
type GFieldTypes (x :+: y) rest = '[]
gInstrConstruct :: forall (st :: [T]).
Rec (FieldConstructor st) (GFieldTypes (x :+: y) rest)
-> (Instr st (GValueType (x :+: y) : st),
Rec (FieldConstructor st) rest)
gInstrConstruct = forall a. Bottom => a
Rec (FieldConstructor st) '[]
-> (Instr st ('TOr (GValueType x) (GValueType y) : st),
Rec (FieldConstructor st) rest)
Rec (FieldConstructor st) (GFieldTypes (x :+: y) rest)
-> (Instr st (GValueType (x :+: y) : st),
Rec (FieldConstructor st) rest)
forall a. a
no
gInstrConstructStack :: forall (end :: [T]).
Proxy# end
-> Instr
(ToTs (GFieldTypes (x :+: y) rest) ++ end)
(GValueType (x :+: y) : (ToTs rest ++ end))
gInstrConstructStack Proxy# end
_ = Instr end ('TOr (GValueType x) (GValueType y) : (ToTs rest ++ end))
Instr
(ToTs (GFieldTypes (x :+: y) rest) ++ end)
(GValueType (x :+: y) : (ToTs rest ++ end))
forall a. Bottom => a
forall a. a
no
instance ( TypeError ('Text "Cannot construct void-like type")
, Bottom
) => GInstrConstruct G.V1 rest where
type GFieldTypes G.V1 rest = '[]
gInstrConstruct :: forall (st :: [T]).
Rec (FieldConstructor st) (GFieldTypes V1 rest)
-> (Instr st (GValueType V1 : st), Rec (FieldConstructor st) rest)
gInstrConstruct = forall a. Bottom => a
Rec (FieldConstructor st) '[]
-> (Instr st ('TNever : st), Rec (FieldConstructor st) rest)
Rec (FieldConstructor st) (GFieldTypes V1 rest)
-> (Instr st (GValueType V1 : st), Rec (FieldConstructor st) rest)
forall a. a
no
gInstrConstructStack :: forall (end :: [T]).
Proxy# end
-> Instr
(ToTs (GFieldTypes V1 rest) ++ end)
(GValueType V1 : (ToTs rest ++ end))
gInstrConstructStack Proxy# end
_ = Instr end ('TNever : (ToTs rest ++ end))
Instr
(ToTs (GFieldTypes V1 rest) ++ end)
(GValueType V1 : (ToTs rest ++ end))
forall a. Bottom => a
forall a. a
no
instance GInstrConstruct (G.Rec0 a) rest where
type GFieldTypes (G.Rec0 a) rest = a ': rest
gInstrConstruct :: forall (st :: [T]).
Rec (FieldConstructor st) (GFieldTypes (Rec0 a) rest)
-> (Instr st (GValueType (Rec0 a) : st),
Rec (FieldConstructor st) rest)
gInstrConstruct (FieldConstructor Instr (ToTs' st) (ToT r : ToTs' st)
i :& Rec (FieldConstructor st) rs
rest) = (Instr st (GValueType (Rec0 a) : st)
Instr (ToTs' st) (ToT r : ToTs' st)
i, Rec (FieldConstructor st) rest
Rec (FieldConstructor st) rs
rest)
gInstrConstructStack :: forall (end :: [T]).
Proxy# end
-> Instr
(ToTs (GFieldTypes (Rec0 a) rest) ++ end)
(GValueType (Rec0 a) : (ToTs rest ++ end))
gInstrConstructStack Proxy# end
_ = Instr (ToT a : (ToTs rest ++ end)) (ToT a : (ToTs rest ++ end))
Instr
(ToTs (GFieldTypes (Rec0 a) rest) ++ end)
(GValueType (Rec0 a) : (ToTs rest ++ end))
forall (inp :: [T]). Instr inp inp
Nop
_constructInstr1 :: Instr (ToT MyType1 ': s) (ToT MyType2 ': ToT MyType1 ': s)
_constructInstr1 :: forall (s :: [T]).
Instr (ToT MyType1 : s) (ToT MyType2 : ToT MyType1 : s)
_constructInstr1 =
forall dt (st :: [T]).
InstrConstructC dt =>
Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> Instr st (ToT dt : st)
instrConstruct @MyType2 (Rec
(FieldConstructor (ToT MyType1 : s))
(ConstructorFieldTypes MyType2)
-> Instr (ToT MyType1 : s) (ToT MyType2 : ToT MyType1 : s))
-> Rec
(FieldConstructor (ToT MyType1 : s))
(ConstructorFieldTypes MyType2)
-> Instr (ToT MyType1 : s) (ToT MyType2 : ToT MyType1 : s)
forall a b. (a -> b) -> a -> b
$
Instr
(ToTs' ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
(ToT Integer
: ToTs' ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
-> FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s) Integer
forall k (st :: [k]) field.
Instr (ToTs' st) (ToT field : ToTs' st)
-> FieldConstructor st field
FieldConstructor (Value' Instr 'TInt
-> Instr
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s)
('TInt : 'TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH (forall a. IsoValue a => a -> Value (ToT a)
toVal @Integer Integer
5)) FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s) Integer
-> Rec
(FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
'[MText, (), MyType1]
-> Rec
(FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
'[Integer, MText, (), MyType1]
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&
Instr
(ToTs' ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
(ToT MText
: ToTs' ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
-> FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s) MText
forall k (st :: [k]) field.
Instr (ToTs' st) (ToT field : ToTs' st)
-> FieldConstructor st field
FieldConstructor (Value' Instr 'TString
-> Instr
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s)
('TString : 'TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH (forall a. IsoValue a => a -> Value (ToT a)
toVal @MText [mt||])) FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s) MText
-> Rec
(FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
'[(), MyType1]
-> Rec
(FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
'[MText, (), MyType1]
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&
Instr
(ToTs' ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
(ToT ()
: ToTs' ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
-> FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s) ()
forall k (st :: [k]) field.
Instr (ToTs' st) (ToT field : ToTs' st)
-> FieldConstructor st field
FieldConstructor Instr
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s)
('TUnit : 'TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s)
Instr
(ToTs' ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
(ToT ()
: ToTs' ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TUnit : s)) =>
Instr inp out
UNIT FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s) ()
-> Rec
(FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
'[MyType1]
-> Rec
(FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
'[(), MyType1]
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&
Instr
(ToTs' ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
(ToT MyType1
: ToTs' ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
-> FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s) MyType1
forall k (st :: [k]) field.
Instr (ToTs' st) (ToT field : ToTs' st)
-> FieldConstructor st field
FieldConstructor Instr
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s)
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes))
: 'TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s)
Instr
(ToTs' ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
(ToT MyType1
: ToTs' ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ (a : a : s), DupableScope a) =>
Instr inp out
DUP FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s) MyType1
-> Rec
(FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
'[]
-> Rec
(FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
'[MyType1]
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&
Rec
(FieldConstructor
('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
'[]
forall {u} (a :: u -> *). Rec a '[]
RNil
_constructInstr2 :: Instr s (ToT MyType1 ': s)
_constructInstr2 :: forall (s :: [T]). Instr s (ToT MyType1 : s)
_constructInstr2 =
forall dt (st :: [T]).
InstrConstructC dt =>
Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> Instr st (ToT dt : st)
instrConstruct @MyType1 (Rec (FieldConstructor s) (ConstructorFieldTypes MyType1)
-> Instr s (ToT MyType1 : s))
-> Rec (FieldConstructor s) (ConstructorFieldTypes MyType1)
-> Instr s (ToT MyType1 : s)
forall a b. (a -> b) -> a -> b
$
Instr (ToTs' s) (ToT (NamedF Identity Integer "int") : ToTs' s)
-> FieldConstructor s (NamedF Identity Integer "int")
forall k (st :: [k]) field.
Instr (ToTs' st) (ToT field : ToTs' st)
-> FieldConstructor st field
FieldConstructor (Value' Instr 'TInt -> Instr s ('TInt : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH (forall a. IsoValue a => a -> Value (ToT a)
toVal @Integer Integer
5)) FieldConstructor s (NamedF Identity Integer "int")
-> Rec
(FieldConstructor s)
'[NamedF Identity ByteString "bytes",
NamedF Maybe ByteString "bytes2"]
-> Rec
(FieldConstructor s)
'[NamedF Identity Integer "int",
NamedF Identity ByteString "bytes",
NamedF Maybe ByteString "bytes2"]
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&
Instr
(ToTs' s) (ToT (NamedF Identity ByteString "bytes") : ToTs' s)
-> FieldConstructor s (NamedF Identity ByteString "bytes")
forall k (st :: [k]) field.
Instr (ToTs' st) (ToT field : ToTs' st)
-> FieldConstructor st field
FieldConstructor (Value' Instr 'TBytes -> Instr s ('TBytes : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH (forall a. IsoValue a => a -> Value (ToT a)
toVal @ByteString ByteString
"bytestring1")) FieldConstructor s (NamedF Identity ByteString "bytes")
-> Rec (FieldConstructor s) '[NamedF Maybe ByteString "bytes2"]
-> Rec
(FieldConstructor s)
'[NamedF Identity ByteString "bytes",
NamedF Maybe ByteString "bytes2"]
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&
Instr (ToTs' s) (ToT (NamedF Maybe ByteString "bytes2") : ToTs' s)
-> FieldConstructor s (NamedF Maybe ByteString "bytes2")
forall k (st :: [k]) field.
Instr (ToTs' st) (ToT field : ToTs' st)
-> FieldConstructor st field
FieldConstructor (Value' Instr ('TOption 'TBytes) -> Instr s ('TOption 'TBytes : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH (forall a. IsoValue a => a -> Value (ToT a)
toVal @(Maybe ByteString) (ByteString -> Maybe ByteString
forall a. a -> Maybe a
Just ByteString
"bytestring2"))) FieldConstructor s (NamedF Maybe ByteString "bytes2")
-> Rec (FieldConstructor s) '[]
-> Rec (FieldConstructor s) '[NamedF Maybe ByteString "bytes2"]
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&
Rec (FieldConstructor s) '[]
forall {u} (a :: u -> *). Rec a '[]
RNil
type InstrDeconstructC dt st = ( GenericIsoValue dt, GInstrDeconstruct (GRep dt) '[] st)
instrDeconstruct
:: forall dt stack (st :: [T]) .
(InstrDeconstructC dt st
, stack ~ ToTs (GFieldTypes (GRep dt) '[])
)
=> Instr (ToT dt ': st) (stack ++ st)
instrDeconstruct :: forall dt (stack :: [T]) (st :: [T]).
(InstrDeconstructC dt st,
stack ~ ToTs (GFieldTypes (GRep dt) '[])) =>
Instr (ToT dt : st) (stack ++ st)
instrDeconstruct = forall (x :: * -> *) (rest :: [*]) (st :: [T]).
GInstrDeconstruct x rest st =>
Instr
(GValueType x : (ToTs rest ++ st))
(ToTs (GFieldTypes x rest) ++ st)
gInstrDeconstruct @(GRep dt) @'[] @st
class GInstrDeconstruct (x :: Type -> Type) (rest :: [Type]) (st :: [T]) where
gInstrDeconstruct :: Instr (GValueType x ': ToTs rest ++ st)
(ToTs (GFieldTypes x rest) ++ st)
instance GInstrDeconstruct x rest st => GInstrDeconstruct (G.M1 t i x) rest st where
gInstrDeconstruct :: Instr
(GValueType (M1 t i x) : (ToTs rest ++ st))
(ToTs (GFieldTypes (M1 t i x) rest) ++ st)
gInstrDeconstruct = forall (x :: * -> *) (rest :: [*]) (st :: [T]).
GInstrDeconstruct x rest st =>
Instr
(GValueType x : (ToTs rest ++ st))
(ToTs (GFieldTypes x rest) ++ st)
gInstrDeconstruct @x @rest @st
instance ( GInstrDeconstruct x (GFieldTypes y rest) st
, GInstrDeconstruct y rest st
) => GInstrDeconstruct (x :*: y) rest st where
gInstrDeconstruct :: Instr
(GValueType (x :*: y) : (ToTs rest ++ st))
(ToTs (GFieldTypes (x :*: y) rest) ++ st)
gInstrDeconstruct =
let linstr :: Instr
(GValueType x : (ToTs (GFieldTypes y rest) ++ st))
(ToTs (GFieldTypes x (GFieldTypes y rest)) ++ st)
linstr = forall (x :: * -> *) (rest :: [*]) (st :: [T]).
GInstrDeconstruct x rest st =>
Instr
(GValueType x : (ToTs rest ++ st))
(ToTs (GFieldTypes x rest) ++ st)
gInstrDeconstruct @x @(GFieldTypes y rest) @st
rinstr :: Instr
(GValueType y : (ToTs rest ++ st))
(ToTs (GFieldTypes y rest) ++ st)
rinstr = forall (x :: * -> *) (rest :: [*]) (st :: [T]).
GInstrDeconstruct x rest st =>
Instr
(GValueType x : (ToTs rest ++ st))
(ToTs (GFieldTypes x rest) ++ st)
gInstrDeconstruct @y @rest @st
in Instr
('TPair (GValueType x) (GValueType y) : (ToTs rest ++ st))
(GValueType x : GValueType y : (ToTs rest ++ st))
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : b : s)) =>
Instr inp out
UNPAIR Instr
('TPair (GValueType x) (GValueType y) : (ToTs rest ++ st))
(GValueType x : GValueType y : (ToTs rest ++ st))
-> Instr
(GValueType x : GValueType y : (ToTs rest ++ st))
(ToTs (GFieldTypes x (GFieldTypes y rest)) ++ st)
-> Instr
('TPair (GValueType x) (GValueType y) : (ToTs rest ++ st))
(ToTs (GFieldTypes x (GFieldTypes y rest)) ++ st)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr
(GValueType y : (ToTs rest ++ st))
(ToTs (GFieldTypes y rest) ++ st)
-> Instr
(GValueType x : GValueType y : (ToTs rest ++ st))
(GValueType x : (ToTs (GFieldTypes y rest) ++ st))
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr
(GValueType y : (ToTs rest ++ st))
(ToTs (GFieldTypes y rest) ++ st)
rinstr Instr
(GValueType x : GValueType y : (ToTs rest ++ st))
(GValueType x : (ToTs (GFieldTypes y rest) ++ st))
-> Instr
(GValueType x : (ToTs (GFieldTypes y rest) ++ st))
(ToTs (GFieldTypes x (GFieldTypes y rest)) ++ st)
-> Instr
(GValueType x : GValueType y : (ToTs rest ++ st))
(ToTs (GFieldTypes x (GFieldTypes y rest)) ++ st)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr
(GValueType x : (ToTs (GFieldTypes y rest) ++ st))
(ToTs (GFieldTypes x (GFieldTypes y rest)) ++ st)
linstr
instance GInstrDeconstruct G.U1 rest st where
gInstrDeconstruct :: Instr
(GValueType U1 : (ToTs rest ++ st))
(ToTs (GFieldTypes U1 rest) ++ st)
gInstrDeconstruct = Instr ('TUnit : (ToTs rest ++ st)) (ToTs rest ++ st)
Instr
(GValueType U1 : (ToTs rest ++ st))
(ToTs (GFieldTypes U1 rest) ++ st)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
instance ( TypeError ('Text "Cannot deconstruct sum type")
, Bottom
) => GInstrDeconstruct (x :+: y) rest st where
gInstrDeconstruct :: Instr
(GValueType (x :+: y) : (ToTs rest ++ st))
(ToTs (GFieldTypes (x :+: y) rest) ++ st)
gInstrDeconstruct = Instr ('TOr (GValueType x) (GValueType y) : (ToTs rest ++ st)) st
Instr
(GValueType (x :+: y) : (ToTs rest ++ st))
(ToTs (GFieldTypes (x :+: y) rest) ++ st)
forall a. Bottom => a
forall a. a
no
instance ( TypeError ('Text "Cannot deconstruct void-like type")
, Bottom
) => GInstrDeconstruct G.V1 rest st where
gInstrDeconstruct :: Instr
(GValueType V1 : (ToTs rest ++ st))
(ToTs (GFieldTypes V1 rest) ++ st)
gInstrDeconstruct = Instr ('TNever : (ToTs rest ++ st)) st
Instr
(GValueType V1 : (ToTs rest ++ st))
(ToTs (GFieldTypes V1 rest) ++ st)
forall a. Bottom => a
forall a. a
no
instance GInstrDeconstruct (G.Rec0 a) rest st where
gInstrDeconstruct :: Instr
(GValueType (Rec0 a) : (ToTs rest ++ st))
(ToTs (GFieldTypes (Rec0 a) rest) ++ st)
gInstrDeconstruct = Instr
(GValueType (Rec0 a) : (ToTs rest ++ st))
(ToTs (GFieldTypes (Rec0 a) rest) ++ st)
Instr (ToT a : (ToTs rest ++ st)) (ToT a : (ToTs rest ++ st))
forall (inp :: [T]). Instr inp inp
Nop