-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# LANGUAGE MagicHash #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Instructions working on product types derived from Haskell ones.
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.Label (Label)
import Morley.Util.Named
import Morley.Util.Type

-- Fields lookup (helper)
----------------------------------------------------------------------------

-- | Result of field lookup - its type and path to it in
-- the tree.
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

-- | Find field of some product type by its name.
--
-- Name might be either field record name, or one in 'NamedF' if
-- field is wrapped using 'Named.(:!)' or 'Named.(:?)'.
type GetNamed name a = LNRequireFound name a (GLookupNamed name (G.Rep a))

-- | Force result of 'GLookupNamed' to be 'Just'
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)

-- | Get type of field by datatype it is contained in and field name.
type GetFieldType dt name = LnrFieldType (GetNamed name dt)

----------------------------------------------------------------------------
-- Value accessing instruction
----------------------------------------------------------------------------

-- | Make an instruction which accesses given field of the given datatype.
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 @(G.Rep dt) @(LnrBranch (GetNamed name dt))
    @(GetFieldType dt name)

-- | Make an instruction which copies given field of the given datatype.
--
-- This behaves exactly as @Seq DUP (instrToField #name)@, but does not require
-- the entire datatype to be dupable (the field ofc still must be dupable).
--
-- If we follow the path from the root to the copied field in the pairs tree,
-- the more nodes contain non-dupable elements in the subtree, the less
-- efficient this function becomes.
-- Assuming that all fields are accessed equally often, the most optimal
-- representation would be to put all dupable elements to one subtree
-- of the root, and all non-dupable elements in the second subtree of the root.
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 (GetFieldType dt name)]
  '[ToT (GetFieldType dt name), 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 (GetFieldType dt name)] '[ToT (GetFieldType dt name)]
forall (inp :: [T]). Instr inp inp
Nop

-- | \"Open\" version of 'instrGetField', meaning that it accepts
-- continuations that accept the copied field. This allows chaining
-- getters without requiring 'DupableScope' on the intermediate fields.
--
-- Accepted continuations:
--
-- 1. The one that leaves the field on stack (and does a duplication inside).
--    Used when the datatype had an unfortunate placement of non-dupable fields,
--    or the intermediate field contains non-dupable elements, so the duplication
--    cannot occur automatically in between.
-- 2. The one that consumes the field, used in case we managed to call @DUP@
--    earlier to make the instruction's implementation smaller, and now we
--    only need to access the field with @CAR@ and @CDR@s.
--
-- Note that only one continuation will be chosen eventually, no contract size
-- overhead is expected in this regard.
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 @(G.Rep 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

-- | Constraint for 'instrGetField'.
type InstrGetFieldC dt name =
  ( GenericIsoValue dt
  , GInstrGet name (G.Rep dt)
      (LnrBranch (GetNamed name dt))
      (LnrFieldType (GetNamed name dt))
  )

{- Note about bulkiness of `instrToField` type signature:

Read this only if you are going to modify the signature qualitatively.

It may seem that you can replace 'LnrBranch' and 'LnrFieldType' getters since
their result is already assigned to a type variable, but if you do so,
on attempt to access non-existing field GHC will prompt you a couple of huge
"cannot deduce type" errors along with desired "field is not present".
To make error messages clearer we prevent GHC from deducing 'GInstrAccess' when
no field is found via using those getters.
-}

-- | Generic traversal for 'instrToField'.
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)

-- | If the current node in the tree is dupable, this provides the more
-- efficient implementation.
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) (ToT fieldTy : GValueType x : s)
-> Instr (GValueType x : s) (ToT fieldTy : 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 : s) (ToT fieldTy : GValueType x : s)
-> Instr (ToT fieldTy : 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` Proxy (GValueType x : s)
-> Instr '[ToT fieldTy] '[res]
-> Instr
     ('[ToT fieldTy] ++ (GValueType x : s))
     ('[res] ++ (GValueType x : s))
forall (a :: [T]) (b :: [T]) (s :: [T]).
KnownList a =>
Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
FrameInstr Proxy (GValueType x : s)
forall {k} (t :: k). Proxy t
Proxy 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)
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]
_ = Proxy s
-> Instr '[ToT f'] '[res, ToT f']
-> Instr ('[ToT f'] ++ s) ('[res, ToT f'] ++ s)
forall (a :: [T]) (b :: [T]) (s :: [T]).
KnownList a =>
Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
FrameInstr Proxy s
forall {k} (t :: k). Proxy t
Proxy 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 : GValueType x : GValueType y : s)
-> Instr
     ('TPair (GValueType x) (GValueType y) : s)
     (res : 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
  ('TPair (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
     ('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)
  ('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) (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
  ('TPair (GValueType x) (GValueType y) : s)
  (GValueType y : GValueType x : s)
-> Instr
     (GValueType y : GValueType x : s)
     (res : GValueType y : GValueType x : s)
-> Instr
     ('TPair (GValueType x) (GValueType y) : s)
     (res : GValueType y : 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
       (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
  ('TPair (GValueType x) (GValueType y) : s)
  (res : GValueType y : GValueType x : s)
-> Instr
     (res : GValueType y : GValueType x : 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 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)

-- Examples
----------------------------------------------------------------------------

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 IsLabel "int" (Label "int")
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 IsLabel "bytes2" (Label "bytes2")
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
$cto :: forall x. Rep MyType2 x -> MyType2
$cfrom :: forall x. MyType2 -> Rep MyType2 x
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
fromVal :: Value (ToT MyType2) -> MyType2
$cfromVal :: Value (ToT MyType2) -> MyType2
toVal :: MyType2 -> Value (ToT MyType2)
$ctoVal :: MyType2 -> Value (ToT 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 IsLabel "getUnit" (Label "getUnit")
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 IsLabel "getMyType1" (Label "getMyType1")
Label "getMyType1"
#getMyType1 Instr
  ('TPair
     ('TPair 'TInt 'TString)
     ('TPair 'TUnit ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes))))
     : s)
  ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s)
-> Instr
     ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : 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 IsLabel "int" (Label "int")
Label "int"
#int

----------------------------------------------------------------------------
-- Value modification instruction
----------------------------------------------------------------------------

-- | For given complex type @dt@ and its field @fieldTy@ update the field value.
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)

-- | \"Open\" version of 'instrSetField', meaning that it accepts a continuation
-- that describes how to update the field. This allows chaining setters with
-- zero overhead and without requiring 'DupableScope' on the intermediate fields
-- (if we supported only closed setters that work directly with one datatype, we
-- would need to duplicate intermediate fields to chain setters).
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 @(G.Rep dt) @(LnrBranch (GetNamed name dt))
    @(GetFieldType dt name) Instr
  '[new, ToT (GetFieldType dt name)] '[ToT (GetFieldType dt name)]
cont

-- | Constraint for 'instrSetField'.
type InstrSetFieldC dt name =
  ( GenericIsoValue dt
  , GInstrSetField name (G.Rep dt)
      (LnrBranch (GetNamed name dt))
      (LnrFieldType (GetNamed name dt))
  )

-- | Generic traversal for 'instrSetField'.
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 = Proxy s
-> Instr '[new, ToT f'] '[ToT f']
-> Instr ('[new, ToT f'] ++ s) ('[ToT f'] ++ s)
forall (a :: [T]) (b :: [T]) (s :: [T]).
KnownList a =>
Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
FrameInstr Proxy s
forall {k} (t :: k). Proxy t
Proxy 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)
     (GValueType x : GValueType y : s)
-> Instr
     (new : 'TPair (GValueType x) (GValueType y) : s)
     (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 : 'TPair (GValueType x) (GValueType y) : s)
  (GValueType x : GValueType y : s)
-> Instr
     (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`
    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)
     (GValueType y : GValueType x : s)
-> Instr
     (new : '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`
    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 : 'TPair (GValueType x) (GValueType y) : s)
  (GValueType y : GValueType x : s)
-> Instr
     (GValueType y : GValueType x : s) (GValueType x : GValueType y : s)
-> Instr
     (new : 'TPair (GValueType x) (GValueType y) : s)
     (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
  (new : 'TPair (GValueType x) (GValueType y) : s)
  (GValueType x : GValueType y : s)
-> Instr
     (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` 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

-- Examples
----------------------------------------------------------------------------

_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 IsLabel "getInt" (Label "getInt")
Label "getInt"
#getInt

----------------------------------------------------------------------------
-- Value construction instruction
----------------------------------------------------------------------------

-- | Way to construct one of the fields in a complex datatype.
newtype FieldConstructor (st :: [k]) (field :: Type) =
  FieldConstructor (Instr (ToTs' st) (ToT field ': ToTs' st))

-- | Ability to pass list of fields with the same ToTs.
-- It may be useful if you don't want to work with NamedF in ConstructorFieldTypes.
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)

-- | For given complex type @dt@ and its field @fieldTy@ update the field value.
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 @(G.Rep 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 @(G.Rep dt) @'[] (forall (a :: [T]). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @st)

-- | Types of all fields in a datatype.
type ConstructorFieldTypes dt = GFieldTypes (G.Rep dt) '[]

-- | Names of all fields in a datatype.
type ConstructorFieldNames dt = GFieldNames (G.Rep dt)

-- | Constraint for 'instrConstruct' and 'gInstrConstructStack'.
type InstrConstructC dt = (GenericIsoValue dt, GInstrConstruct (G.Rep dt) '[])

-- | Retrieve field names of a constructor.
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")

-- | Generic traversal for 'instrConstruct'.
class GInstrConstruct (x :: Type -> Type) (rest :: [Type]) where
  type GFieldTypes x rest :: [Type]
  -- We return the remaining, unprocessed, portion of the record along
  -- with the instruction.
  gInstrConstruct
    :: Rec (FieldConstructor st) (GFieldTypes x rest)
    -> (Instr st (GValueType x ': st), Rec (FieldConstructor st) rest)

  -- Why do we need a proxy? Without it, there doesn't seem to be any way to
  -- access the @end@ type variable in method implementations, and we need to.
  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) (GValueType x : GValueType y : st)
-> Instr st (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 st (GValueType x : GValueType y : st)
-> Instr
     (GValueType x : GValueType y : 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
  (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))
     (GValueType x : GValueType y : (ToTs rest ++ end))
-> Instr
     (ToTs (GFieldTypes x (GFieldTypes y rest)) ++ end)
     (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
  (ToTs (GFieldTypes x (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
     (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
  (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 (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 (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) (GFieldTypes (x :+: y) rest)
-> (Instr st (GValueType (x :+: y) : st),
    Rec (FieldConstructor st) rest)
no
  gInstrConstructStack :: forall (end :: [T]).
Proxy# end
-> Instr
     (ToTs (GFieldTypes (x :+: y) rest) ++ end)
     (GValueType (x :+: y) : (ToTs rest ++ end))
gInstrConstructStack Proxy# end
_ = Instr
  (ToTs (GFieldTypes (x :+: y) rest) ++ end)
  (GValueType (x :+: y) : (ToTs rest ++ end))
forall a. Bottom => 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) (GFieldTypes V1 rest)
-> (Instr st (GValueType V1 : st), Rec (FieldConstructor st) rest)
no
  gInstrConstructStack :: forall (end :: [T]).
Proxy# end
-> Instr
     (ToTs (GFieldTypes V1 rest) ++ end)
     (GValueType V1 : (ToTs rest ++ end))
gInstrConstructStack Proxy# end
_ = Instr
  (ToTs (GFieldTypes V1 rest) ++ end)
  (GValueType V1 : (ToTs rest ++ end))
forall a. Bottom => 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
  (ToTs (GFieldTypes (Rec0 a) rest) ++ end)
  (GValueType (Rec0 a) : (ToTs rest ++ end))
forall (inp :: [T]). Instr inp inp
Nop

-- Examples
----------------------------------------------------------------------------

_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
      ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
   (ConstructorFieldTypes MyType2)
 -> Instr
      ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s)
      (ToT MyType2
         : 'TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
-> Rec
     (FieldConstructor
        ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s))
     (ConstructorFieldTypes MyType2)
-> Instr
     ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : s)
     (ToT MyType2
        : 'TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : 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
  (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
  (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

----------------------------------------------------------------------------
-- Value deconstruction
----------------------------------------------------------------------------

-- | Constraint for 'instrConstruct'.
type InstrDeconstructC dt st = ( GenericIsoValue dt, GInstrDeconstruct (G.Rep dt) '[] st)

-- | For given complex type @dt@ deconstruct it to its field types.
instrDeconstruct
  :: forall dt stack (st :: [T]) .
  (InstrDeconstructC dt st
  , stack ~ ToTs (GFieldTypes (G.Rep dt) '[])
  )
  => Instr (ToT dt ': st) (stack ++ st)
instrDeconstruct :: forall dt (stack :: [T]) (st :: [T]).
(InstrDeconstructC dt st,
 stack ~ ToTs (GFieldTypes (Rep 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 @(G.Rep dt) @'[] @st

-- | Generic traversal for 'instrDeconstruct'.
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))
     (GValueType x : (ToTs (GFieldTypes y rest) ++ st))
-> Instr
     ('TPair (GValueType x) (GValueType y) : (ToTs rest ++ st))
     (GValueType x : (ToTs (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
  ('TPair (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
     ('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 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
  (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
  (GValueType (x :+: y) : (ToTs rest ++ st))
  (ToTs (GFieldTypes (x :+: y) rest) ++ st)
forall a. Bottom => 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
  (GValueType V1 : (ToTs rest ++ st))
  (ToTs (GFieldTypes V1 rest) ++ st)
forall a. Bottom => 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)
forall (inp :: [T]). Instr inp inp
Nop